Add location to all assertion strings

Sail currently replaces empty assertion messages with their location, so `assert(false, "")` and `assert(false)` (which is equivalent to the former) will print their location, but `assert(false, "foo")` won't.

This changes the behaviour so that instead all assertions print their location.

The previous substitution was applied during type checking, but now it is done in the ANF step.

Author: Tim Hutt

lib/int128/rts.c

@@ -16,11 +16,14 @@ void sail_match_failure(const_sail_string msg)
   exit(EXIT_FAILURE);
 }
 
-unit sail_assert(bool b, const_sail_string msg)
+unit sail_assert(bool b, const_sail_string msg, const_sail_string loc)
 {
   if (b) return UNIT;
-  fprintf(stderr, "Assertion failed: %s\n", msg);
-  exit(EXIT_FAILURE);
+  if (msg[0] == '\0') {
+    fprintf(stderr, "Assertion failed at %s\n", loc);
+  } else {
+    fprintf(stderr, "Assertion failed at %s: %s\n", loc, msg);
+  }  exit(EXIT_FAILURE);
 }
 
 unit sail_exit(unit u)
@@ -244,7 +247,7 @@ bool write_ram(const sail_int addr_size,     // Either 32 or 64
       // Then shift buf 8 bits right.
       mpz_fdiv_q_2exp(write_buf, write_buf, 8);
     }
-    
+
     return true;
   }
 }
@@ -253,7 +256,7 @@ sbits fast_read_ram(const int64_t data_size,
 		    const uint64_t addr)
 {
   uint64_t r = 0;
-  
+
   uint64_t byte;
   for(uint64_t i = (uint64_t) data_size; i > 0; --i) {
     byte = read_mem(addr + (i - 1));

lib/int128/rts.h

@@ -16,7 +16,7 @@ void sail_match_failure(const_sail_string msg);
  * sail_assert implements the assert construct in Sail. If any
  * assertion fails we immediately exit the model.
  */
-unit sail_assert(bool b, const_sail_string msg);
+unit sail_assert(bool b, const_sail_string msg, const_sail_string loc);
 
 unit sail_exit(unit);
 

lib/sail_config.c

@@ -71,29 +71,29 @@ void sail_config_set_string(const char *json)
     else {
         snprintf(error_message, sizeof error_message, "Failed to parse JSON configuration at offset %ld", parse_end - json);
     }
-    sail_assert(false, error_message);
+    sail_assert(false, error_message, "sail_config_set_string()");
   }
 }
 
 void sail_config_set_file(const char *path)
 {
   FILE *f = fopen(path, "rb");
-  sail_assert(f != NULL, "Failed to open configuration file");
+  sail_assert(f != NULL, "Failed to open configuration file", path);
 
   int rc = fseek(f, 0, SEEK_END);
-  sail_assert(rc != -1, "Failed to seek to end of configuration file");
+  sail_assert(rc != -1, "Failed to seek to end of configuration file", path);
 
   long fsize = ftell(f);
-  sail_assert(fsize != -1, "Failed to get size of configuration file");
+  sail_assert(fsize != -1, "Failed to get size of configuration file", path);
 
   rc = fseek(f, 0, SEEK_SET);
-  sail_assert(rc != -1, "Failed to seek to start of configuration file");
+  sail_assert(rc != -1, "Failed to seek to start of configuration file", path);
 
   char *buffer = (char *)sail_malloc(fsize + 1);
 
   size_t ret_size = fread(buffer, fsize, 1, f);
 
-  sail_assert(ret_size == 1, "Failed to read configuration");
+  sail_assert(ret_size == 1, "Failed to read configuration", path);
 
   buffer[fsize] = 0;
   fclose(f);
@@ -102,7 +102,7 @@ void sail_config_set_file(const char *path)
   // sail_config_set_string() relies on null termination
   // to find the end of the string.
   for (size_t i = 0; i < fsize; ++i) {
-    sail_assert(buffer[i] != 0, "Null byte in JSON configuration");
+    sail_assert(buffer[i] != 0, "Null byte in JSON configuration", path);
   }
 
   sail_config_set_string(buffer);
@@ -289,7 +289,7 @@ void sail_config_unwrap_int(sail_int *n, const sail_config_json config)
 {
   cJSON *json = (cJSON *)config;
   if (mpz_set_str(*n, json->valuestring, 10) == -1) {
-    sail_assert(false, "Failed to parse integer from configuration");
+    sail_assert(false, "Failed to parse integer from configuration", "sail_config_unwrap_int()");
   }
 }
 

lib/sail_failure.c

@@ -56,10 +56,14 @@ void sail_match_failure(const_sail_string msg)
   exit(EXIT_FAILURE);
 }
 
-unit sail_assert(bool b, const_sail_string msg)
+unit sail_assert(bool b, const_sail_string msg, const_sail_string loc)
 {
   if (b) return UNIT;
-  fprintf(stderr, "Assertion failed: %s\n", msg);
+  if (msg[0] == '\0') {
+    fprintf(stderr, "Assertion failed at %s\n", loc);
+  } else {
+    fprintf(stderr, "Assertion failed at %s: %s\n", loc, msg);
+  }
   exit(EXIT_FAILURE);
 }
 

lib/sail_failure.h

@@ -63,7 +63,7 @@ void sail_match_failure(const_sail_string msg);
  * sail_assert implements the assert construct in Sail. If any
  * assertion fails we immediately exit the model.
  */
-unit sail_assert(bool b, const_sail_string msg);
+unit sail_assert(bool b, const_sail_string msg, const_sail_string loc);
 
 #ifdef __cplusplus
 }

lib/sv/sail.sv

@@ -25,7 +25,9 @@ function automatic sail_unit sail_prerr(sail_unit s);
    return SAIL_UNIT;
 endfunction // sail_prerr
 
-function automatic sail_unit sail_assert(bit b, sail_unit msg);
+// TODO: Is this actually used? It looks like asserts actually get written to
+// if (not condition) then $fatal(msg);
+function automatic sail_unit sail_assert(bit b, sail_unit loc, sail_unit msg);
    return SAIL_UNIT;
 endfunction // sail_assert
 
@@ -55,9 +57,9 @@ function automatic sail_unit sail_prerr(string s);
    return SAIL_UNIT;
 endfunction // sail_prerr
 
-function automatic sail_unit sail_assert(bit b, string msg);
+function automatic sail_unit sail_assert(bit b, string loc, string msg);
    if (!b) begin
-      $display("%s", msg);
+      $error("Assertion failed at %s: %s", loc, msg);
    end;
    return SAIL_UNIT;
 endfunction // sail_assert

src/lib/anf.ml

@@ -785,7 +785,12 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) =
       let aexp2 = anf exp2 in
       let aval1, wrap1 = to_aval aexp1 in
       let aval2, wrap2 = to_aval aexp2 in
-      wrap1 (wrap2 (mk_aexp (AE_app (Extern (mk_id "sail_assert", None), [aval1; aval2], unit_typ))))
+      (* Add the location of the assertion as a parameter. *)
+      let loc_string = Reporting.short_loc_to_string l in
+      let loc_aexp = mk_aexp (ae_lit (L_aux (L_string loc_string, l)) string_typ) in
+      let loc_aval, loc_wrap = to_aval loc_aexp in
+      (* TODO: What are these wrap functions? Do I need to use loc_wrap? *)
+      wrap1 (wrap2 (mk_aexp (AE_app (Extern (mk_id "sail_assert", None), [aval1; aval2; loc_aval], unit_typ))))
   | E_cons (exp1, exp2) ->
       let aexp1 = anf exp1 in
       let aexp2 = anf exp2 in

src/lib/jib_compile.ml

@@ -1206,7 +1206,8 @@ module Make (C : CONFIG) = struct
         let str = string_of_id id in
         if str = "sail_assert" && C.assert_to_exception then (
           match args with
-          | [cond; msg] ->
+          | [cond; msg; _loc] ->
+              (* TODO: Should we include the location in the assertion message? *)
               let cond_setup, cond_cval, cond_cleanup = compile_aval l ctx cond in
               let msg_setup, msg_cval, _ = compile_aval l ctx msg in
               let exn_setup, exn_cval = assert_exception l msg_cval in

src/lib/smt_gen.ml

@@ -1526,6 +1526,8 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
   let ternary_primop f =
     Some (fun args ret_ctyp -> match args with [v1; v2; v3] -> f v1 v2 v3 ret_ctyp | _ -> arity_error)
 
+  let ternary_primop_simple f = Some (fun args _ -> match args with [v1; v2; v3] -> f v1 v2 v3 | _ -> arity_error)
+
   let builtin ?(allow_io = true) ?(undefined = Undefined_disable) = function
     | "eq_bit" -> binary_primop (binary_smt "=")
     | "eq_bool" -> binary_primop (binary_smt "=")
@@ -1651,10 +1653,11 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
             return (Fn (op, [bv]))
         )
     | "sail_assert" when allow_io ->
-        binary_primop_simple (fun b msg ->
+        ternary_primop_simple (fun b msg loc ->
             let* b = smt_cval b in
             let* msg = smt_cval msg in
-            return (Fn ("sail_assert", [b; msg]))
+            let* loc = smt_cval loc in
+            return (Fn ("sail_assert", [b; msg; loc]))
         )
     | "reg_deref" when allow_io ->
         unary_primop_simple (fun reg_ref ->

src/lib/type_check.ml

@@ -1974,13 +1974,6 @@ let irule r env exp =
     let bt = Printexc.get_raw_backtrace () in
     Printexc.raise_with_backtrace (Type_error (l, err)) bt
 
-(* This function adds useful assertion messages to asserts missing them *)
-let assert_msg = function
-  | E_aux (E_lit (L_aux (L_string "", _)), (l, _)) ->
-      let open Reporting in
-      locate (fun _ -> l) (mk_lit_exp (L_string (short_loc_to_string l)))
-  | msg -> msg
-
 let strip_exp exp = map_exp_annot (fun (l, tannot) -> (l, untyped_annot tannot)) exp
 let strip_pat pat = map_pat_annot (fun (l, tannot) -> (l, untyped_annot tannot)) pat
 let strip_pexp pexp = map_pexp_annot (fun (l, tannot) -> (l, untyped_annot tannot)) pexp
@@ -2644,7 +2637,6 @@ and check_block' f_p env exps ret_typ =
           let _, exps = check_block' f_p env exps ret_typ in
           (s_p, annotated_exp :: exps)
       | E_aux (E_assert (constr_exp, msg), (assert_l, _)), _ ->
-          let msg = assert_msg msg in
           let constr_exp = crule check_exp env constr_exp bool_typ in
           let checked_msg = crule check_exp env msg string_typ in
           let env, added_constraint =
@@ -3899,7 +3891,6 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
       | None -> typ_error l "Could not infer type of list literal"
     end
   | E_assert (test, msg) ->
-      let msg = assert_msg msg in
       let checked_test = crule check_exp env test bool_typ in
       let checked_msg = crule check_exp env msg string_typ in
       annot_exp (E_assert (checked_test, checked_msg)) unit_typ