SMT: Fix dead-code FIXME in jib_compile

Add an Assumption event that is true whenever a property's type
quantifier is true, rather than wrapping body in a if-statement that
ends up creating a dead branch.

5 files changed, 27 insertions, 18 deletions

diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index bd4813ed..331fed83 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -651,7 +651,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
   | E_exit exp ->
      let aexp = anf exp in
      let aval, wrap = to_aval aexp in
-     wrap (mk_aexp (AE_app (mk_id "sail_exit", [aval], unit_typ)))
+     wrap (mk_aexp (AE_app (mk_id "__exit", [aval], unit_typ)))
 
   | E_return ret_exp ->
      let aexp = anf ret_exp in
@@ -663,7 +663,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) 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 (mk_id "sail_assert", [aval1; aval2], unit_typ))))
+     wrap1 (wrap2 (mk_aexp (AE_app (mk_id "__assert", [aval1; aval2], unit_typ))))
 
   | E_cons (exp1, exp2) ->
      let aexp1 = anf exp1 in
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 98a71f19..f7438b96 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -650,13 +650,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      []
 
   | AE_if (aval, then_aexp, else_aexp, if_typ) ->
-     (* FIXME:
      if is_dead_aexp then_aexp then
        compile_aexp ctx else_aexp
      else if is_dead_aexp else_aexp then
        compile_aexp ctx then_aexp
      else
-      *)
        let if_ctyp = ctyp_of_typ ctx if_typ in
        let compile_branch aexp =
          let setup, call, cleanup = compile_aexp ctx aexp in
@@ -1499,8 +1497,8 @@ let sort_ctype_defs cdefs =
   ctype_defs @ cdefs
 
 let compile_ast ctx (Defs defs) =
-  let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in
-  let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in
+  let assert_vs = Initial_check.extern_of_string (mk_id "__assert") "(bool, string) -> unit" in
+  let exit_vs = Initial_check.extern_of_string (mk_id "__exit") "unit -> unit" in
 
   let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
 
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 587d6778..9303051d 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -66,7 +66,7 @@ let opt_ignore_overflow = ref false
 
 let opt_auto = ref false
 
-type event = Overflow | Assertion | Match | Return
+type event = Overflow | Assertion | Assumption | Match | Return
 
 type query =
    | Q_all of event   (* All events of type are true *)
@@ -76,13 +76,7 @@ type query =
    | Q_or of query list
 
 let default_query =
-  Q_or [Q_and [Q_all Assertion; Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow]
-
-let event_name = function
-  | Overflow -> "overflow"
-  | Assertion -> "assert"
-  | Match -> "match"
-  | Return -> "end"
+  Q_or [Q_and [Q_all Assertion; Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow; Q_not (Q_all Assumption)]
 
 module Event = struct
   type t = event
@@ -90,12 +84,15 @@ module Event = struct
     match e1, e2 with
     | Overflow, Overflow -> 0
     | Assertion, Assertion -> 0
+    | Assumption, Assumption -> 0
     | Match, Match -> 0
     | Return, Return -> 0
     | Overflow, _ -> 1
     | _, Overflow -> -1
     | Assertion, _ -> 1
     | _, Assertion -> -1
+    | Assumption, _ -> 1
+    | _, Assumption -> -1
     | Match, _ -> 1
     | _, Match -> -1
 end
@@ -1334,7 +1331,7 @@ let smt_instr ctx =
        | _ ->
           Reporting.unreachable l __POS__ "Bad arguments for internal_vector_update"
        end
-     else if string_of_id function_id = "sail_assert" then
+     else if string_of_id function_id = "__assert" then
        begin match args with
        | [assertion; _] ->
           let smt = smt_cval ctx assertion in
@@ -1343,6 +1340,15 @@ let smt_instr ctx =
        | _ ->
           Reporting.unreachable l __POS__ "Bad arguments for assertion"
        end
+     else if string_of_id function_id = "__assume" then
+       begin match args with
+       | [assumption] ->
+          let smt = smt_cval ctx assumption in
+          add_event ctx Assumption smt;
+          []
+       | _ ->
+          Reporting.unreachable l __POS__ "Bad arguments for assumption"
+       end
      else if not extern then
        let smt_args = List.map (smt_cval ctx) args in
        [define_const ctx id ret_ctyp (Fn (zencode_id function_id, smt_args))]
diff --git a/src/property.ml b/src/property.ml
index 871011e7..56bdbe2e 100644
--- a/src/property.ml
+++ b/src/property.ml
@@ -79,9 +79,9 @@ let add_property_guards props (Defs defs) =
              let add_constraints_to_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp, pexp_aux)), fcl_aux)) =
                let add_guard exp =
                  (* FIXME: Use an assert *)
-                 let exp' = mk_exp (E_if (mk_exp (E_constraint (List.fold_left nc_and nc_true constraints)),
-                                          strip_exp exp,
-                                          mk_lit_exp L_true)) in
+                 let exp' = mk_exp (E_block [mk_exp (E_app (mk_id "__assume", [mk_exp (E_constraint (List.fold_left nc_and nc_true constraints))]));
+                                             strip_exp exp])
+                 in
                  try Type_check.check_exp (env_of exp) exp' (typ_of exp) with
                  | Type_error (_, l, err) ->
                     let msg =
diff --git a/src/type_check.ml b/src/type_check.ml
index ec5258d6..c0560a83 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -5060,3 +5060,8 @@ let initial_env =
                                   Parse_ast.Unknown)],Parse_ast.Unknown),
        function_typ [atom_typ (nvar (mk_kid "n"))]
          (app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]) no_effect)
+  (* __assume is used by property.ml to add guards for SMT generation,
+     but which don't affect flow-typing. *)
+  |> Env.add_val_spec (mk_id "__assume")
+      (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown),
+       function_typ [bool_typ] unit_typ no_effect)