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

@@ -780,12 +780,14 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) =
       let aexp = anf ret_exp in
       let aval, wrap = to_aval aexp in
       wrap (mk_aexp (AE_return (aval, typ_of exp)))
-  | E_assert (exp1, exp2) ->
+  | E_assert (exp1, exp2, exp3) ->
       let aexp1 = anf exp1 in
       let aexp2 = anf exp2 in
+      let aexp3 = anf exp3 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))))
+      let aval3, wrap3 = to_aval aexp3 in
+      wrap1 (wrap2 ( wrap3(mk_aexp (AE_app (Extern (mk_id "sail_assert", None), [aval1; aval2; aval3], unit_typ)))))
   | E_cons (exp1, exp2) ->
       let aexp1 = anf exp1 in
       let aexp2 = anf exp2 in

src/lib/ast_util.ml

@@ -932,7 +932,7 @@ and map_exp_annot_aux f = function
   | E_exit exp -> E_exit (map_exp_annot f exp)
   | E_throw exp -> E_throw (map_exp_annot f exp)
   | E_return exp -> E_return (map_exp_annot f exp)
-  | E_assert (test, msg) -> E_assert (map_exp_annot f test, map_exp_annot f msg)
+  | E_assert (test, msg, loc) -> E_assert (map_exp_annot f test, map_exp_annot f msg, map_exp_annot f loc)
   | E_internal_value v -> E_internal_value v
   | E_var (lexp, exp1, exp2) -> E_var (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
   | E_internal_plet (pat, exp1, exp2) ->
@@ -1340,7 +1340,7 @@ let rec string_of_exp (E_aux (exp, _)) =
       "while " ^ string_of_measure measure ^ string_of_exp cond ^ " do " ^ string_of_exp body
   | E_loop (Until, measure, cond, body) ->
       "repeat " ^ string_of_measure measure ^ string_of_exp body ^ " until " ^ string_of_exp cond
-  | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
+  | E_assert (test, msg, _loc) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
   | E_exit exp -> "exit " ^ string_of_exp exp
   | E_throw exp -> "throw " ^ string_of_exp exp
   | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs
@@ -1886,7 +1886,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
     | E_ref id' -> E_ref id'
     | E_throw exp -> E_throw (subst id value exp)
     | E_try (exp, pexps) -> E_try (subst id value exp, List.map (subst_pexp id value) pexps)
-    | E_assert (exp1, exp2) -> E_assert (subst id value exp1, subst id value exp2)
+    | E_assert (exp1, exp2, exp3) -> E_assert (subst id value exp1, subst id value exp2, subst id value exp3)
     | E_internal_value v -> E_internal_value v
     | E_var (lexp, exp1, exp2) -> E_var (subst_lexp id value lexp, subst id value exp1, subst id value exp2)
     | E_internal_assume (nc, exp) -> E_internal_assume (nc, subst id value exp)
@@ -2109,7 +2109,7 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp =
     | E_ref id -> E_ref (locate_id f id)
     | E_throw exp -> E_throw (locate f exp)
     | E_try (exp, cases) -> E_try (locate f exp, List.map (locate_pexp f) cases)
-    | E_assert (exp, message) -> E_assert (locate f exp, locate f message)
+    | E_assert (exp, message, loc) -> E_assert (locate f exp, locate f message, locate f loc)
     | E_constraint constr -> E_constraint (locate_nc f constr)
     | E_var (lexp, exp1, exp2) -> E_var (locate_lexp f lexp, locate f exp1, locate f exp2)
     | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (locate_pat f pat, locate f exp1, locate f exp2)

src/lib/constant_propagation.ml

@@ -568,9 +568,9 @@ let const_props target env ast =
       | E_return e ->
           let e', _ = const_prop_exp substs assigns e in
           re (E_return e') Bindings.empty
-      | E_assert (e1, e2) ->
-          let e1', e2', assigns = non_det_exp_2 e1 e2 in
-          re (E_assert (e1', e2')) assigns
+      | E_assert (e1, e2, e3) ->
+          let e1', e2', e3', assigns = non_det_exp_3 e1 e2 e3 in
+          re (E_assert (e1', e2', e3')) assigns
       | E_internal_assume (nc, e) ->
           let e', _ = const_prop_exp substs assigns e in
           re (E_internal_assume (nc, e')) assigns

src/lib/extraction/Ast.ml

@@ -20,7 +20,7 @@ module Coq_def_annot =
   type 'a record = { doc_comment : string option;
                      attrs : (Parse_ast.l * (string * attribute_data option))
                              list;
-                     visibility : visibility; loc : Parse_ast.l; env : 
+                     visibility : visibility; loc : Parse_ast.l; env :
                      'a }
  end
 
@@ -226,7 +226,7 @@ and 'a exp_aux =
 | E_ref of id
 | E_throw of 'a exp
 | E_try of 'a exp * 'a pexp list
-| E_assert of 'a exp * 'a exp
+| E_assert of 'a exp * 'a exp * 'a exp
 | E_var of 'a lexp * 'a exp * 'a exp
 | E_internal_plet of 'a pat * 'a exp * 'a exp
 | E_internal_return of 'a exp

src/lib/extraction/Ast.mli

@@ -20,7 +20,7 @@ module Coq_def_annot :
   type 'a record = { doc_comment : string option;
                      attrs : (Parse_ast.l * (string * attribute_data option))
                              list;
-                     visibility : visibility; loc : Parse_ast.l; env : 
+                     visibility : visibility; loc : Parse_ast.l; env :
                      'a }
  end
 
@@ -226,7 +226,7 @@ and 'a exp_aux =
 | E_ref of id
 | E_throw of 'a exp
 | E_try of 'a exp * 'a pexp list
-| E_assert of 'a exp * 'a exp
+| E_assert of 'a exp * 'a exp * 'a exp
 | E_var of 'a lexp * 'a exp * 'a exp
 | E_internal_plet of 'a pat * 'a exp * 'a exp
 | E_internal_return of 'a exp

src/lib/extraction/Semantics.ml

@@ -420,8 +420,8 @@ module Make =
      | E_try (head_exp, arms) ->
        E_aux ((E_try ((substitute n v head_exp),
          (map (substitute_arm n v) arms))), annot0)
-     | E_assert (x0, msg) ->
-       E_aux ((E_assert ((substitute n v x0), (substitute n v msg))), annot0)
+     | E_assert (x0, msg, loc) ->
+       E_aux ((E_assert ((substitute n v x0), (substitute n v msg), (substitute n v loc))), annot0)
      | E_var (l, x0, body) ->
        E_aux ((E_var ((substitute_lexp n v l), (substitute n v x0),
          (substitute n v body))), annot0)
@@ -1052,8 +1052,8 @@ module Make =
                then wrap (E_block xs0)
                else Monad.bind (step0 x0) (fun x' ->
                       wrap (E_block (x' :: xs0)))
-             | E_assert (e0, e1) ->
-               let x0 = E_aux ((E_assert (e0, e1)), annot1) in
+             | E_assert (e0, e1, e2) ->
+               let x0 = E_aux ((E_assert (e0, e1, e2)), annot1) in
                if is_value x0
                then wrap (E_block xs0)
                else Monad.bind (step0 x0) (fun x' ->
@@ -1441,7 +1441,7 @@ module Make =
               | Monad.Caught exn ->
                 wrap (E_match ((E_aux ((E_internal_value exn), annot0)),
                   (app arms (T.fallthrough :: []))))))
-       | E_assert (x, msg) ->
+       | E_assert (x, msg, loc) ->
          Monad.bind (get_bool x) (fun b ->
            match b with
            | Evaluated b0 ->
@@ -1453,9 +1453,9 @@ module Make =
                  else Monad.Assertion_failed s0
                | Unevaluated ->
                  Monad.bind (step0 msg) (fun msg' ->
-                   wrap (E_assert (x, msg'))))
+                   wrap (E_assert (x, msg', loc))))
            | Unevaluated ->
-             Monad.bind (step0 x) (fun x' -> wrap (E_assert (x', msg))))
+             Monad.bind (step0 x) (fun x' -> wrap (E_assert (x', msg, loc))))
        | E_var (l, x, body) ->
          wrap (E_block ((E_aux ((E_assign (l, x)), annot0)) :: (body :: [])))
        | E_internal_plet (_, _, _) -> Monad.Runtime_type_error (fst annot0)

src/lib/initial_check.ml

@@ -1365,7 +1365,9 @@ and to_ast_exp ctx exp =
         | P.E_throw exp -> E_throw (to_ast_exp ctx exp)
         | P.E_config key -> E_config [key]
         | P.E_return exp -> E_return (to_ast_exp ctx exp)
-        | P.E_assert (cond, msg) -> E_assert (to_ast_exp ctx cond, to_ast_exp ctx msg)
+        | P.E_assert (cond, msg) ->
+            let loc = E_lit (L_aux (L_string (Reporting.short_loc_to_string l), l)) in
+            E_assert (to_ast_exp ctx cond, to_ast_exp ctx msg, mk_exp loc)
         | P.E_internal_plet (pat, exp1, exp2) ->
             if !opt_magic_hash then E_internal_plet (to_ast_pat ctx pat, to_ast_exp ctx exp1, to_ast_exp ctx exp2)
             else raise (Reporting.err_general l "Internal plet construct found without -dmagic_hash")

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/monomorphise.ml

@@ -595,7 +595,7 @@ let stop_at_false_assertions e =
               let e2, stop = exp e2 in
               (E_aux (E_let (LB_aux (LB_val (p, e1), lbann), e2), ann), stop)
         end
-    | E_assert (e1, _) when exp_false e1 -> (ea, Some (typ_of_annot ann))
+    | E_assert (e1, _, _) when exp_false e1 -> (ea, Some (typ_of_annot ann))
     | E_throw e -> (ea, Some (typ_of_annot ann))
     | _ -> (ea, None)
   in
@@ -631,7 +631,7 @@ let apply_pat_choices choices =
         | _ -> exp
       )
   in
-  let rewrite_assert (e1, e2) = E_assert (rewrite_assert_cond e1, e2) in
+  let rewrite_assert (e1, e2, e3) = E_assert (rewrite_assert_cond e1, e2, e3) in
   let rewrite_case (e, cases) =
     match List.assoc (exp_loc e) choices with
     | choice, max, subst -> (
@@ -1123,7 +1123,7 @@ let split_defs target all_errors (splits : split_req list) env ast =
         | E_throw e -> re (E_throw e)
         | E_try (e, cases) -> re (E_try (map_exp e, List.concat (List.map map_pexp cases)))
         | E_return e -> re (E_return (map_exp e))
-        | E_assert (e1, e2) -> re (E_assert (map_exp e1, map_exp e2))
+        | E_assert (e1, e2, e3) -> re (E_assert (map_exp e1, map_exp e2, map_exp e3))
         | E_var (le, e1, e2) -> re (E_var (map_lexp le, map_exp e1, map_exp e2))
         | E_internal_plet (p, e1, e2) -> re (E_internal_plet (check_single_pat p, map_exp e1, map_exp e2))
         | E_internal_return e -> re (E_internal_return (map_exp e))
@@ -2458,7 +2458,7 @@ module Analysis = struct
           in
           let ds, assigns, rs = split3 (List.map analyse_handler cases) in
           (merge_deps (deps :: ds), List.fold_left dep_bindings_merge Bindings.empty assigns, List.fold_left merge r rs)
-      | E_assert (e1, _) -> analyse_sub env assigns e1
+      | E_assert (e1, _, _) -> analyse_sub env assigns e1
       | E_internal_assume (nc, e1) -> analyse_sub env assigns e1
       | E_internal_plet _ | E_internal_return _ | E_internal_value _ ->
           raise
@@ -2788,7 +2788,7 @@ module Analysis = struct
         let kbound = kids_bound_by_pat p in
         let sets2 = KBindings.filter (fun kid _ -> not (KidSet.mem kid kbound)) sets2 in
         merge_set_asserts_by_kid sets1 sets2
-    | E_assert (exp1, _) -> sets_from_assert exp1
+    | E_assert (exp1, _, _) -> sets_from_assert exp1
     | _ -> KBindings.empty
 
   let print_set_assertions set_assertions =
@@ -4218,7 +4218,7 @@ module BitvectorSizeCasts = struct
             let result_typ = Env.base_typ_of env (typ_of_annot ann) in
             let rec aux = function
               | [] -> []
-              | (E_aux (E_assert (assert_exp, msg), _) as h) :: t ->
+              | (E_aux (E_assert (assert_exp, _msg, _loc), _) as h) :: t ->
                   (* Check the assertion for constraints that instantiate kids *)
                   let is_known_kid kid = KBindings.mem kid (Env.get_typ_vars env) in
                   begin

src/lib/nl_flow.ml

@@ -70,7 +70,8 @@ let rec pat_id (P_aux (aux, _)) =
 
 let add_assert cond (E_aux (aux, (l, uannot)) as exp) =
   let msg = mk_lit_exp (L_string "") in
-  let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (cond, msg))) in
+  let loc = E_lit (L_aux (L_string (Reporting.short_loc_to_string l), l)) in
+  let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (cond, msg, mk_exp loc))) in
   match aux with
   | E_block exps -> E_aux (E_block (assertion :: exps), (l, empty_uannot))
   | _ -> E_aux (E_block (assertion :: [exp]), (l, uannot))

src/lib/pretty_print_sail.ml

@@ -592,8 +592,8 @@ module Printer (Config : PRINT_CONFIG) = struct
     | E_app (id, exps) when not Config.resugar -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
     | E_app (id, exps) when List.length exps != 2 -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
     | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc)
-    | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1)
-    | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
+    | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _), _) -> string "assert" ^^ parens (doc_exp exp1)
+    | E_assert (exp1, exp2, _) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
     | E_exit exp -> string "exit" ^^ parens (doc_exp exp)
     | E_vector exps -> brackets (separate_map (comma ^^ space) doc_exp exps)
     | E_internal_value v ->