diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 7 | ||||
| -rw-r--r-- | src/jib/jib_smt.mli | 4 | ||||
| -rw-r--r-- | src/sail.ml | 15 |
3 files changed, 14 insertions, 12 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index a380c518..6ace9d96 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -2032,7 +2032,7 @@ 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 to_axiomatic_model file env 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 []; @@ -2040,12 +2040,13 @@ let to_axiomatic_model file env ast = Marshal.to_channel out_chan ctx.register_map []; close_out out_chan -let from_axiomatic_model file = +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 - cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap } + close_in in_chan; + (cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap }) let generate_smt props name_file env ast = try diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli index 98b4b1c9..cdaf7e39 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -139,10 +139,10 @@ module Make_optimizer(S : Sequence) : sig val optimize : smt_def Stack.t -> smt_def S.t end -val to_axiomatic_model : +val serialize_smt_model : string -> Type_check.Env.t -> Type_check.tannot defs -> unit -val from_axiomatic_model : +val deserialize_smt_model : string -> cdef list * ctx (** Generate SMT for all the $property and $counterexample pragmas in diff --git a/src/sail.ml b/src/sail.ml index 60257c8d..58565d03 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -62,7 +62,7 @@ let opt_memo_z3 = ref false let opt_sanity = ref false let opt_includes_c = ref ([]:string list) let opt_specialize_c = ref false -let opt_smt_axiomatic = ref false +let opt_smt_serialize = ref false let opt_smt_fuzz = ref false let opt_libs_lem = ref ([]:string list) let opt_libs_coq = ref ([]:string list) @@ -163,8 +163,8 @@ let options = Arg.align ([ ( "-smt_vector_size", Arg.String (fun n -> Jib_smt.opt_default_vector_index := int_of_string n), "<n> set a bound of 2 ^ n for generic vectors in generated SMT (default 5)"); - ( "-axiomatic", - Arg.Tuple [set_target "smt"; Arg.Set opt_smt_axiomatic], + ( "-smt_serialize", + Arg.Tuple [set_target "smt"; Arg.Set opt_smt_serialize], " compile Sail to IR suitable for sail-axiomatic tool"); ( "-c", Arg.Tuple [set_target "c"; Arg.Set Initial_check.opt_undefined_gen], @@ -490,17 +490,18 @@ let target name out_name ast type_envs = | Some "smt" when !opt_smt_fuzz -> Jib_smt_fuzz.fuzz 0 type_envs ast - | Some "smt" when !opt_smt_axiomatic -> + | Some "smt" when !opt_smt_serialize -> let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in let ast_smt, type_envs = Specialize.(specialize_passes 2 int_specialization_with_externs type_envs ast_smt) in let jib, ctx = Jib_smt.compile type_envs ast_smt in let name_file = match !opt_file_out with - | Some f -> f ^ ".axiomatic_model" - | None -> "sail.axiomatic_model" + | Some f -> f ^ ".smt_model" + | None -> "sail.smt_model" in Reporting.opt_warnings := true; - Jib_smt.to_axiomatic_model name_file type_envs ast_smt + Jib_smt.serialize_smt_model name_file type_envs ast_smt + | Some "smt" -> let open Ast_util in let props = Property.find_properties ast in |