Add messages for assert failures without user defined messages

Also fix some C optimisations

4 files changed, 43 insertions, 19 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index b198c340..d3bb7c2a 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -429,11 +429,9 @@ let analyze_primop' ctx id args typ =
      | _ -> no_change
      end
 
-       (*
   | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] when is_stack_typ ctx typ ->
      let len = F_op (f, "-", F_op (t, "-", v_one)) in
      AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ))
-        *)
 
   | "vector_access", [AV_C_fragment (vec, _); AV_C_fragment (n, _)] ->
      AE_val (AV_C_fragment (F_op (v_one, "&", F_op (vec, ">>", n)), typ))
@@ -2946,7 +2944,6 @@ let sgen_finish = function
      Printf.sprintf "  finish_%s();" (sgen_id id)
   | _ -> assert false
 
-       (*
 let instrument_tracing ctx =
   let module StringSet = Set.Make(String) in
   let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in
@@ -2969,12 +2966,14 @@ let instrument_tracing ctx =
             trace_arg cval :: iraw "trace_argsep();" :: trace_args cvals
        in
        let trace_end = iraw "trace_end();" in
-       let trace_ret =
+       let trace_ret = iraw "trace_unknown();"
+                            (*
          let ctyp_name = sgen_ctyp_name ctyp in
          if StringSet.mem ctyp_name traceable then
            iraw (Printf.sprintf "trace_%s(%s);" (sgen_ctyp_name ctyp) (sgen_clexp_pure clexp))
          else
            iraw "trace_unknown();"
+                             *)
        in
        [trace_start]
        @ trace_args args
@@ -2997,7 +2996,6 @@ let instrument_tracing ctx =
   | CDEF_fundef (function_id, heap_return, args, body) ->
      CDEF_fundef (function_id, heap_return, args, instrument body)
   | cdef -> cdef
-        *)
 
 let bytecode_ast ctx rewrites (Defs defs) =
   let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in
@@ -3050,9 +3048,7 @@ let compile_ast ctx c_includes (Defs defs) =
     let cdefs, ctx = specialize_variants ctx [] cdefs in
     let cdefs = sort_ctype_defs cdefs in
     let cdefs = optimize ctx cdefs in
-    (*
     let cdefs = if !opt_trace then List.map (instrument_tracing ctx) cdefs else cdefs in
-     *)
     let docs = List.map (codegen_def ctx) cdefs in
 
     let preamble = separate hardline
diff --git a/src/reporting.ml b/src/reporting.ml
index 3f5f1627..858e5c41 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -169,6 +169,14 @@ let format_pos2 ff p1 p2 =
     Format.pp_print_flush ff ()
   end
 
+let format_just_pos ff p1 p2 =
+  let open Lexing in
+  Format.fprintf ff "file \"%s\", line %d, character %d to line %d, character %d"
+                 p1.pos_fname
+                 p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1)
+                 p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
+  Format.pp_print_flush ff ()
+
 (* reads the part between p1 and p2 from the file *)
 
 let read_from_file_pos2 p1 p2 =
@@ -187,12 +195,21 @@ let read_from_file_pos2 p1 p2 =
   let _ = close_in ic in
   (buf, not (multi = None))
 
-let rec format_loc_aux ff = function
-  | Parse_ast.Unknown -> Format.fprintf ff "no location information available"
-  | Parse_ast.Generated l -> Format.fprintf ff "code generated: original nearby source is "; (format_loc_aux ff l)
-  | Parse_ast.Unique (n, l) -> Format.fprintf ff "code unique (%d): original nearby source is " n; (format_loc_aux ff l)
-  | Parse_ast.Range (p1,p2) -> format_pos2 ff p1 p2
-  | Parse_ast.Documented (_, l) -> format_loc_aux ff l
+let rec format_loc_aux ?code:(code=true) ff = function
+  | Parse_ast.Unknown ->
+     Format.fprintf ff "no location information available"
+  | Parse_ast.Generated l ->
+     Format.fprintf ff "code generated: original nearby source is ";
+     format_loc_aux ~code:code ff l
+  | Parse_ast.Unique (n, l) ->
+     Format.fprintf ff "code unique (%d): original nearby source is " n;
+     format_loc_aux ~code:code ff l
+  | Parse_ast.Range (p1, p2) when code ->
+     format_pos2 ff p1 p2
+  | Parse_ast.Range (p1, p2) ->
+     format_just_pos ff p1 p2
+  | Parse_ast.Documented (_, l) ->
+     format_loc_aux ~code:code ff l
 
 let format_loc_source ff = function
   | Parse_ast.Range (p1, p2) ->
@@ -215,9 +232,9 @@ let print_err_loc l =
 let print_pos p = format_pos Format.std_formatter p
 let print_err_pos p = format_pos Format.err_formatter p
 
-let loc_to_string l =
+let loc_to_string ?code:(code=true) l =
   let _ = Format.flush_str_formatter () in
-  let _ = format_loc_aux Format.str_formatter l in
+  let _ = format_loc_aux ~code:code Format.str_formatter l in
   let s = Format.flush_str_formatter () in
   s
 
@@ -254,7 +271,7 @@ let issues = "\n\nPlease report this as an issue on GitHub at https://github.com
 let dest_err = function
   | Err_general (l, m) -> ("Error", false, Loc l, m)
   | Err_unreachable (l, (file, line, _, _), m) ->
-     ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)\n" file line), false, Loc l, m ^ issues)
+     ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line), false, Loc l, m ^ issues)
   | Err_todo (l, m) -> ("Todo" ^ m, false, Loc l, "")
   | Err_syntax (p, m) -> ("Syntax error", false, Pos p, m)
   | Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
diff --git a/src/reporting.mli b/src/reporting.mli
index a6878d6a..63ed3eee 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -62,7 +62,8 @@
 
 (** {2 Auxiliary Functions } *)
 
-val loc_to_string : Parse_ast.l -> string
+(** [loc_to_string] includes code from file if code optional argument is true (default) *)
+val loc_to_string : ?code:bool -> Parse_ast.l -> string
 
 (** [print_err fatal print_loc_source l head mes] prints an error / warning message to
     std-err. It starts with printing location information stored in [l]
diff --git a/src/type_check.ml b/src/type_check.ml
index 0079d59f..23629b51 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2247,6 +2247,14 @@ let irule r env exp =
   with
   | Type_error (l, err) -> decr depth; typ_raise l err
 
+
+(* This function adds useful assertion messages to asserts missing them *)
+let assert_msg test = function
+  | E_aux (E_lit (L_aux (L_string "", _)), (l, _)) ->
+     let open Reporting in
+     locate (fun _ -> l) (mk_lit_exp (L_string (loc_to_string ~code:false l ^ ": " ^ string_of_exp test)))
+  | msg -> msg
+
 let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp
 let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -> (l, ())) pat
 let strip_pexp : 'a pexp -> unit pexp = function pexp -> map_pexp_annot (fun (l, _) -> (l, ())) pexp
@@ -2281,9 +2289,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
          | (E_aux (E_assign (lexp, bind), _) :: exps) ->
             let texp, env = bind_assignment env lexp bind in
             texp :: check_block l env exps typ
-         | ((E_aux (E_assert (constr_exp, assert_msg), _) as exp) :: exps) ->
+         | ((E_aux (E_assert (constr_exp, msg), _) as exp) :: exps) ->
+            let msg = assert_msg constr_exp msg in
             let constr_exp = crule check_exp env constr_exp bool_typ in
-            let checked_msg = crule check_exp env assert_msg string_typ in
+            let checked_msg = crule check_exp env msg string_typ in
             let env = match assert_constraint env true constr_exp with
               | Some nc ->
                  typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint nc ^ " for assert"));
@@ -3291,6 +3300,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let vec_typ = dvector_typ env (nint (List.length vec)) (typ_of inferred_item) in
      annot_exp (E_vector (inferred_item :: checked_items)) vec_typ
   | E_assert (test, msg) ->
+     let msg = assert_msg test 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_effect (E_assert (checked_test, checked_msg)) unit_typ (mk_effect [BE_escape])