summaryrefslogtreecommitdiff
path: root/src/jib
diff options
context:
space:
mode:
Diffstat (limited to 'src/jib')
-rw-r--r--src/jib/anf.ml2
-rw-r--r--src/jib/c_backend.ml20
-rw-r--r--src/jib/jib_compile.ml9
-rw-r--r--src/jib/jib_smt.ml71
-rw-r--r--src/jib/jib_smt.mli6
5 files changed, 82 insertions, 26 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 5165904d..dbbb10e0 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -670,7 +670,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 "cons", [aval1; aval2], unit_typ))))
+ wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_cons", [aval1; aval2], unit_typ))))
| E_id id ->
let lvar = Env.lookup_id id (env_of exp) in
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 2c9c11ee..52061444 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -397,14 +397,14 @@ let analyze_primop' ctx id args typ =
c_debug (lazy ("Analyzing primop " ^ extern ^ "(" ^ Util.string_of_list ", " (fun aval -> Pretty_print_sail.to_string (pp_aval aval)) args ^ ")"));
match extern, args with
- | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
begin match cval_ctyp v1 with
| CT_fbits _ | CT_sbits _ ->
AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
| _ -> no_change
end
- | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
begin match cval_ctyp v1 with
| CT_fbits _ | CT_sbits _ ->
AE_val (AV_cval (V_call (Neq, [v1; v2]), typ))
@@ -461,19 +461,19 @@ let analyze_primop' ctx id args typ =
| "not_bits", [AV_cval (v, _)] ->
AE_val (AV_cval (V_call (Bvnot, [v]), typ))
- | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
AE_val (AV_cval (V_call (Bvadd, [v1; v2]), typ))
- | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
AE_val (AV_cval (V_call (Bvsub, [v1; v2]), typ))
- | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
AE_val (AV_cval (V_call (Bvand, [v1; v2]), typ))
- | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
AE_val (AV_cval (V_call (Bvor, [v1; v2]), typ))
- | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
AE_val (AV_cval (V_call (Bvxor, [v1; v2]), typ))
| "vector_subrange", [AV_cval (vec, _); AV_cval (f, _); AV_cval (t, _)] ->
@@ -2185,7 +2185,7 @@ let compile_ast env output_chan c_includes ast =
" CREATE(zexception)(current_exception);" ],
[ " KILL(zexception)(current_exception);";
" free(current_exception);";
- " if (have_exception) fprintf(stderr, \"Exiting due to uncaught exception\\n\");" ])
+ " if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception\\n\"); exit(EXIT_FAILURE);}" ])
in
let letbind_initializers =
@@ -2230,9 +2230,9 @@ let compile_ast env output_chan c_includes ast =
@ letbind_finalizers
@ List.concat (List.map (fun r -> snd (register_init_clear r)) regs)
@ finish cdefs
+ @ [ " cleanup_rts();" ]
@ snd exn_boilerplate
- @ [ " cleanup_rts();";
- "}" ] ))
+ @ [ "}" ] ))
in
let model_default_main = separate hardline (List.map string
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 0518b9c5..5e49af7f 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -193,8 +193,10 @@ let rec compile_aval l ctx = function
let ctyp = cval_ctyp cval in
let ctyp' = ctyp_of_typ ctx typ in
if not (ctyp_equal ctyp ctyp') then
- raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp'));
- [], cval, []
+ let gs = ngensym () in
+ [iinit ctyp' gs cval], V_id (gs, ctyp'), [iclear ctyp' gs]
+ else
+ [], cval, []
| AV_id (id, typ) ->
begin
@@ -1568,8 +1570,9 @@ let sort_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 cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in
- let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in
+ let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs; cons_vs])) } in
if !opt_memo_cache then
(try
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 07cab66b..9fb77055 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -418,7 +418,7 @@ let unsigned_size ?checked:(checked=true) ctx n m smt =
else if n > m then
Fn ("concat", [bvzero (n - m); smt])
else
- failwith "bad arguments to unsigned_size"
+ Extract (n - 1, 0, smt)
let int_size ctx = function
| CT_constant n -> required_width n
@@ -536,6 +536,11 @@ let builtin_min_int ctx v1 v2 ret_ctyp =
smt1,
smt2)
+let bvmask ctx len =
+ let all_ones = bvones (lbits_size ctx) in
+ let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in
+ bvnot (bvshl all_ones shift)
+
let builtin_eq_bits ctx v1 v2 =
match cval_ctyp v1, cval_ctyp v2 with
| CT_fbits (n, _), CT_fbits (m, _) ->
@@ -545,15 +550,20 @@ let builtin_eq_bits ctx v1 v2 =
Fn ("=", [smt1; smt2])
| CT_lbits _, CT_lbits _ ->
- Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+ let len1 = Fn ("len", [smt_cval ctx v1]) in
+ let contents1 = Fn ("contents", [smt_cval ctx v1]) in
+ let len2 = Fn ("len", [smt_cval ctx v1]) in
+ let contents2 = Fn ("contents", [smt_cval ctx v1]) in
+ Fn ("and", [Fn ("=", [len1; len2]);
+ Fn ("=", [Fn ("bvand", [bvmask ctx len1; contents1]); Fn ("bvand", [bvmask ctx len2; contents2])])])
| CT_lbits _, CT_fbits (n, _) ->
- let smt2 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v2) in
- Fn ("=", [Fn ("contents", [smt_cval ctx v1]); smt2])
+ let smt1 = unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [smt_cval ctx v1])) in
+ Fn ("=", [smt1; smt_cval ctx v2])
| CT_fbits (n, _), CT_lbits _ ->
- let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in
- Fn ("=", [smt1; Fn ("contents", [smt_cval ctx v2])])
+ let smt2 = unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [smt_cval ctx v2])) in
+ Fn ("=", [smt_cval ctx v1; smt2])
| _ -> builtin_type_error ctx "eq_bits" [v1; v2] None
@@ -566,11 +576,6 @@ let builtin_zeros ctx v ret_ctyp =
Fn ("Bits", [extract (ctx.lbits_index - 1) 0 (smt_cval ctx v); bvzero (lbits_size ctx)])
| _ -> builtin_type_error ctx "zeros" [v] (Some ret_ctyp)
-let bvmask ctx len =
- let all_ones = bvones (lbits_size ctx) in
- let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in
- bvnot (bvshl all_ones shift)
-
let builtin_ones ctx cval = function
| CT_fbits (n, _) -> bvones n
| CT_lbits _ ->
@@ -691,12 +696,23 @@ let builtin_append ctx v1 v2 ret_ctyp =
Fn ("Bits", [bvadd (bvint ctx.lbits_index (Big_int.of_int n)) (Fn ("len", [smt2]));
bvor (bvshl x shift) (Fn ("contents", [smt2]))])
+ | CT_lbits _, CT_fbits (n, _), CT_fbits (m, _) ->
+ let smt1 = smt_cval ctx v1 in
+ let smt2 = smt_cval ctx v2 in
+ Extract (m - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2]))
+
| CT_lbits _, CT_fbits (n, _), CT_lbits _ ->
let smt1 = smt_cval ctx v1 in
let smt2 = smt_cval ctx v2 in
Fn ("Bits", [bvadd (bvint ctx.lbits_index (Big_int.of_int n)) (Fn ("len", [smt1]));
Extract (lbits_size ctx - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2]))])
+ | CT_fbits (n, _), CT_fbits (m, _), CT_lbits _ ->
+ let smt1 = smt_cval ctx v1 in
+ let smt2 = smt_cval ctx v2 in
+ Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int (n + m));
+ unsigned_size ctx (lbits_size ctx) (n + m) (Fn ("concat", [smt1; smt2]))])
+
| CT_lbits _, CT_lbits _, CT_lbits _ ->
let smt1 = smt_cval ctx v1 in
let smt2 = smt_cval ctx v2 in
@@ -704,6 +720,13 @@ let builtin_append ctx v1 v2 ret_ctyp =
let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in
Fn ("Bits", [bvadd (Fn ("len", [smt1])) (Fn ("len", [smt2])); bvor (bvshl x shift) (Fn ("contents", [smt2]))])
+ | CT_lbits _, CT_lbits _, CT_fbits (n, _) ->
+ let smt1 = smt_cval ctx v1 in
+ let smt2 = smt_cval ctx v2 in
+ let x = Fn ("contents", [smt1]) in
+ let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in
+ unsigned_size ctx n (lbits_size ctx) (bvor (bvshl x shift) (Fn ("contents", [smt2])))
+
| _ -> builtin_type_error ctx "append" [v1; v2] (Some ret_ctyp)
let builtin_length ctx v ret_ctyp =
@@ -729,6 +752,9 @@ let builtin_vector_subrange ctx vec i j ret_ctyp =
| CT_fbits (n, _), CT_constant i, CT_constant j ->
Extract (Big_int.to_int i, Big_int.to_int j, smt_cval ctx vec)
+ | CT_lbits _, CT_constant i, CT_constant j ->
+ Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [smt_cval ctx vec]))
+
| _ -> builtin_type_error ctx "vector_subrange" [vec; i; j] (Some ret_ctyp)
let builtin_vector_access ctx vec i ret_ctyp =
@@ -783,9 +809,12 @@ let builtin_unsigned ctx v ret_ctyp =
let builtin_signed ctx v ret_ctyp =
match cval_ctyp v, ret_ctyp with
- | CT_fbits (n, _), CT_fint m when m > n ->
+ | CT_fbits (n, _), CT_fint m when m >= n ->
SignExtend(m - n, smt_cval ctx v)
+ | CT_fbits (n, _), CT_lint ->
+ SignExtend(ctx.lint_size - n, smt_cval ctx v)
+
| ctyp, _ -> builtin_type_error ctx "signed" [v] (Some ret_ctyp)
let builtin_add_bits ctx v1 v2 ret_ctyp =
@@ -1141,6 +1170,8 @@ let rec smt_conversion ctx from_ctyp to_ctyp x =
bvint ctx.lint_size c
| CT_fint sz, CT_lint ->
force_size ctx ctx.lint_size sz x
+ | CT_lbits _, CT_fbits (n, _) ->
+ unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x]))
| _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp))
let define_const ctx id ctyp exp = Define_const (zencode_name id, smt_ctyp ctx ctyp, exp)
@@ -2030,6 +2061,22 @@ let compile env ast =
let rmap = build_register_map CTMap.empty cdefs in
cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap; ast = ast }
+let serialize_smt_model file env ast =
+ let cdefs, ctx = compile env ast in
+ let out_chan = open_out file in
+ Marshal.to_channel out_chan cdefs [];
+ Marshal.to_channel out_chan (Type_check.Env.set_prover None ctx.tc_env) [];
+ Marshal.to_channel out_chan ctx.register_map [];
+ close_out out_chan
+
+let deserialize_smt_model file =
+ let in_chan = open_in file in
+ let cdefs = (Marshal.from_channel in_chan : cdef list) in
+ let env = (Marshal.from_channel in_chan : Type_check.env) in
+ let rmap = (Marshal.from_channel in_chan : id list CTMap.t) in
+ close_in in_chan;
+ (cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap })
+
let generate_smt props name_file env ast =
try
let cdefs, ctx = compile env ast in
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index 2680f937..cdaf7e39 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -139,6 +139,12 @@ module Make_optimizer(S : Sequence) : sig
val optimize : smt_def Stack.t -> smt_def S.t
end
+val serialize_smt_model :
+ string -> Type_check.Env.t -> Type_check.tannot defs -> unit
+
+val deserialize_smt_model :
+ string -> cdef list * ctx
+
(** Generate SMT for all the $property and $counterexample pragmas in
an AST, and write it to appropriately named files. *)
val generate_smt :
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 08:20:57 +0000