diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/anf.ml | 4 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 6 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 24 |
3 files changed, 19 insertions, 15 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))] |