Basic support to track uncaught exceptions in Sail->C

8 files changed, 36 insertions, 8 deletions

diff --git a/language/jib.ott b/language/jib.ott
index d5c7f571..8cccac5f 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -59,6 +59,7 @@ name :: '' ::=
   | id nat                :: :: name
   | have_exception nat    :: :: have_exception
   | current_exception nat :: :: current_exception
+  | throw_location nat    :: :: throw_location
   | return nat            :: :: return
 
 op :: '' ::=
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 6809d557..54b3a561 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -1324,6 +1324,7 @@ let sgen_cval_param cval =
 let rec sgen_clexp = function
   | CL_id (Have_exception _, _) -> "have_exception"
   | CL_id (Current_exception _, _) -> "current_exception"
+  | CL_id (Throw_location _, _) -> "throw_location"
   | CL_id (Return _, _) -> assert false
   | CL_id (Name (id, _), _) -> "&" ^ sgen_id id
   | CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ zencode_uid field ^ ")"
@@ -1335,6 +1336,7 @@ let rec sgen_clexp = function
 let rec sgen_clexp_pure = function
   | CL_id (Have_exception _, _) -> "have_exception"
   | CL_id (Current_exception _, _) -> "current_exception"
+  | CL_id (Throw_location _, _) -> "throw_location"
   | CL_id (Return _, _) -> assert false
   | CL_id (Name (id, _), _) -> sgen_id id
   | CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ zencode_uid field
@@ -1788,6 +1790,8 @@ let codegen_type_def ctx = function
           ^^ string "struct zexception *current_exception = NULL;"
           ^^ hardline
           ^^ string "bool have_exception = false;"
+          ^^ hardline
+          ^^ string "sail_string *throw_location = NULL;"
         else
           empty
 
@@ -2219,10 +2223,15 @@ let compile_ast env output_chan c_includes ast =
     let exn_boilerplate =
       if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else
         ([ "  current_exception = sail_malloc(sizeof(struct zexception));";
-           "  CREATE(zexception)(current_exception);" ],
-         [ "  KILL(zexception)(current_exception);";
+           "  CREATE(zexception)(current_exception);";
+           "  throw_location = sail_malloc(sizeof(sail_string));";
+           "  CREATE(sail_string)(throw_location);" ],
+         [ "  if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception: %s\\n\", *throw_location);}";
+           "  KILL(zexception)(current_exception);";
            "  sail_free(current_exception);";
-           "  if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception\\n\"); exit(EXIT_FAILURE);}" ])
+           "  KILL(sail_string)(throw_location);";
+           "  sail_free(throw_location);";
+           "  if (have_exception) {exit(EXIT_FAILURE);}" ])
     in
 
     let letbind_initializers =
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index c751e2db..5eac2481 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -58,6 +58,7 @@ open Value2
 open Anf
 
 let opt_memo_cache = ref false
+let opt_track_throw = ref true
 
 let optimize_aarch64_fast_struct = ref false
 
@@ -876,7 +877,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
   | AE_throw (aval, typ) ->
      (* Cleanup info will be handled by fix_exceptions *)
      let throw_setup, cval, _ = compile_aval l ctx aval in
-     throw_setup @ [ithrow cval],
+     throw_setup @ [ithrow l cval],
      (fun clexp -> icomment "unreachable after throw"),
      []
 
@@ -1056,6 +1057,10 @@ let fix_exception_block ?return:(return=None) ctx instrs =
        before
        @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval;
           icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool))]
+       @ (if !opt_track_throw then
+            let loc_string = Reporting.short_loc_to_string l in
+            [icopy l (CL_id (throw_location, CT_string)) (V_lit (VL_string loc_string, CT_string))]
+          else [])
        @ generate_cleanup (historic @ before)
        @ [igoto end_block_label]
        @ rewrite_exception (historic @ before) after
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index c863b6ba..9014d8f7 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -61,6 +61,11 @@ open Type_check
    ARM v8.5 spec. It is unsound in general. *)
 val optimize_aarch64_fast_struct : bool ref
 
+(** If true (default) track the location of the last exception thrown,
+   useful for debugging C but we want to turn it off for SMT generation
+   where we can't use strings *)
+val opt_track_throw : bool ref
+ 
 (** {2 Jib context} *)
 
 (** Dynamic context for compiling Sail to Jib. We need to pass a
diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index ca11696e..69a73804 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -69,7 +69,9 @@ let string_of_name =
      "return" ^ ssa_num n
   | Current_exception n ->
      "current_exception" ^ ssa_num n
-
+  | Throw_location n ->
+     "throw_location" ^ ssa_num n
+    
 let rec string_of_clexp = function
   | CL_id (id, ctyp) -> string_of_name id
   | CL_field (clexp, field) -> string_of_clexp clexp ^ "." ^ string_of_uid field
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index b971c1fa..fe3238a4 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -504,6 +504,7 @@ let rename_variables graph root children =
     | Name (id, _) -> Name (id, i)
     | Have_exception _ -> Have_exception i
     | Current_exception _ -> Current_exception i
+    | Throw_location _ -> Throw_location i
     | Return _ -> Return i
   in
 
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 0b551416..dbb855b9 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -113,7 +113,7 @@ let iblock ?loc:(l=Parse_ast.Unknown) instrs =
 let itry_block ?loc:(l=Parse_ast.Unknown) instrs =
   I_aux (I_try_block instrs, (instr_number (), l))
 
-let ithrow ?loc:(l=Parse_ast.Unknown) cval =
+let ithrow l cval =
   I_aux (I_throw cval, (instr_number (), l))
 
 let icomment ?loc:(l=Parse_ast.Unknown) str =
@@ -153,6 +153,8 @@ module Name = struct
     | _, Have_exception _ -> -1
     | Current_exception _, _ -> 1
     | _, Current_exception _ -> -1
+    | Throw_location _, _ -> 1
+    | _, Throw_location _ -> -1
 end
 
 module NameSet = Set.Make(Name)
@@ -160,6 +162,7 @@ module NameMap = Map.Make(Name)
 
 let current_exception = Current_exception (-1)
 let have_exception = Have_exception (-1)
+let throw_location = Throw_location (-1)
 let return = Return (-1)
 
 let name id = Name (id, -1)
@@ -268,6 +271,8 @@ let string_of_name ?deref_current_exception:(dce=false) ?zencode:(zencode=true)
      "(*current_exception)" ^ ssa_num n
   | Current_exception n ->
      "current_exception" ^ ssa_num n
+  | Throw_location n ->
+     "throw_location" ^ ssa_num n
 
 let string_of_op = function
   | Bnot -> "@not"
diff --git a/src/sail.ml b/src/sail.ml
index 42904e80..ea642470 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -149,10 +149,10 @@ let options = Arg.align ([
     set_target "ir",
     " print intermediate representation");
   ( "-smt",
-    set_target "smt",
+    Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw],
     " print SMT translated version of input");
   ( "-smt_auto",
-    Arg.Tuple [set_target "smt"; Arg.Set Jib_smt.opt_auto],
+    Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw; Arg.Set Jib_smt.opt_auto],
     " generate SMT and automatically call the solver (implies -smt)");
   ( "-smt_ignore_overflow",
     Arg.Set Jib_smt.opt_ignore_overflow,