diff options
| -rw-r--r-- | aarch64_small/Makefile | 4 | ||||
| -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 |
4 files changed, 16 insertions, 14 deletions
diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile index b0a993ef..2606da05 100644 --- a/aarch64_small/Makefile +++ b/aarch64_small/Makefile @@ -23,8 +23,8 @@ armV8.lem: $(SOURCES) # also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem $(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^ -armV8.axiomatic_model: $(SOURCES) - $(SAIL) $(SAILFLAGS) -axiomatic -o armV8 $^ +armV8.smt_model: $(SOURCES) + $(SAIL) $(SAILFLAGS) -smt_serialize -o armV8 $^ for-rmem/armV8.lem: $(SOURCES) mkdir -p $(dir $@) 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 |