Add location to all assertion strings

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 =
@@ -3901,7 +3893,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

src/sail_sv_backend/jib_sv.ml

@@ -898,9 +898,10 @@ module Make (Config : CONFIG) = struct
           else (
             let _, ret = svir_creturn l ctx creturn in
             match args with
-            | [cond; msg] ->
+            | [cond; msg; loc] ->
                 let* cond = Smt.smt_cval cond in
                 let* msg = Smt.smt_cval msg in
+                let* loc = Smt.smt_cval loc in
                 (* If the assert is only reachable under some path-condition, then the assert should pass
                    whenever the path-condition is not true. *)
                 let cond =
@@ -909,7 +910,10 @@ module Make (Config : CONFIG) = struct
                       Fn ("or", [Fn ("not", [pathcond]); Fn ("not", [Var (Name (mk_id "assert_reachable#", -1))]); cond])
                   | None -> cond
                 in
-                wrap (SVS_block [SVS_aux (SVS_assert (ngen_asrt (), cond, msg), l); SVS_aux (SVS_assign (ret, Unit), l)])
+                wrap
+                  (SVS_block
+                     [SVS_aux (SVS_assert (ngen_asrt (), cond, msg, loc), l); SVS_aux (SVS_assign (ret, Unit), l)]
+                  )
             | _ -> Reporting.unreachable l __POS__ "Invalid arguments for sail_assert"
           )
         else if Id.compare id (mk_id "sail_cons") = 0 then extern_generate l ctx creturn id "sail_cons" args
@@ -1009,10 +1013,27 @@ module Make (Config : CONFIG) = struct
     match aux with
     | SVS_comment str -> concat_map string ["/* "; str; " */"]
     | SVS_split_comb -> string "/* split comb */"
-    | SVS_assert (name, cond, msg) ->
+    | SVS_assert (name, cond, msg, loc) ->
         ( if not Config.no_assert_fatal then
             separate space
-              [string "if"; parens (pp_smt cond) ^^ semi; string "else"; string "$fatal" ^^ parens (pp_smt msg)]
+              [
+                string "if";
+                parens (pp_smt cond) ^^ semi;
+                string "else";
+                string "$fatal"
+                ^^ parens
+                     (separate (comma ^^ space)
+                        [
+                          (* The 'finish_number' parameter. 1 prints the time and location. *)
+                          string "1";
+                          (* Use a couple of spaces as a separate so it doesn't look so weird
+                  if the assertion string is empty. *)
+                          string "Assertion failed at %s  %s";
+                          pp_smt loc;
+                          pp_smt msg;
+                        ]
+                     );
+              ]
             ^^ terminator
           else empty
         )
@@ -2057,7 +2078,7 @@ module Make (Config : CONFIG) = struct
 
       method! vstatement s =
         match s with
-        | SVS_aux (SVS_assert (name, _, _), _) ->
+        | SVS_aux (SVS_assert (name, _, _, _), _) ->
             names := name :: !names;
             DoChildren
         | _ -> DoChildren

src/sail_sv_backend/sv_ir.ml

@@ -136,7 +136,7 @@ and sv_statement_aux =
   | SVS_case of { head_exp : smt_exp; cases : (smt_exp * sv_statement) list; fallthrough : sv_statement option }
   | SVS_if of smt_exp * sv_statement option * sv_statement option
   | SVS_block of sv_statement list
-  | SVS_assert of Jib.name * smt_exp * smt_exp
+  | SVS_assert of Jib.name * smt_exp * smt_exp * smt_exp
   | SVS_foreach of sv_name * smt_exp * sv_statement
   | SVS_for of sv_for * sv_statement
   | SVS_raw of string * Jib.name list * Jib.name list
@@ -285,10 +285,10 @@ let rec visit_sv_statement (vis : svir_visitor) outer_statement =
         let fallthrough' = map_no_copy_opt (visit_sv_statement vis) fallthrough in
         if head_exp == head_exp' && cases == cases' && fallthrough == fallthrough' then no_change
         else SVS_aux (SVS_case { head_exp = head_exp'; cases = cases'; fallthrough = fallthrough' }, l)
-    | SVS_assert (name, cond, msg) ->
+    | SVS_assert (name, cond, msg, loc) ->
         let cond' = visit_smt_exp vis cond in
         let msg' = visit_smt_exp vis msg in
-        if cond == cond' && msg == msg' then no_change else SVS_aux (SVS_assert (name, cond', msg'), l)
+        if cond == cond' && msg == msg' then no_change else SVS_aux (SVS_assert (name, cond', msg', loc), l)
     | SVS_foreach (i, exp, stmt) ->
         let exp' = visit_smt_exp vis exp in
         let stmt' = visit_sv_statement vis stmt in

src/sail_sv_backend/sv_ir.mli

@@ -132,7 +132,7 @@ and sv_statement_aux =
   | SVS_case of { head_exp : smt_exp; cases : (smt_exp * sv_statement) list; fallthrough : sv_statement option }
   | SVS_if of smt_exp * sv_statement option * sv_statement option
   | SVS_block of sv_statement list
-  | SVS_assert of Jib.name * smt_exp * smt_exp
+  | SVS_assert of Jib.name * (* condition *) smt_exp * (* message *) smt_exp * (* location string *) smt_exp
   | SVS_foreach of sv_name * smt_exp * sv_statement
   | SVS_for of sv_for * sv_statement
   | SVS_raw of string * Jib.name list * Jib.name list

src/sail_sv_backend/sv_optimize.ml

@@ -596,7 +596,7 @@ module RemoveUnusedVariables = struct
         begin
           match else_stmt_opt with Some else_stmt -> statement_uses stack uses else_stmt | None -> ()
         end
-    | SVS_assert (name, cond, msg) ->
+    | SVS_assert (name, cond, msg, _loc) ->
         smt_uses stack uses cond;
         smt_uses stack uses msg
     | SVS_case { head_exp; cases; fallthrough } ->