diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 8 | ||||
| -rw-r--r-- | src/jib/jib_smt.mli | 3 | ||||
| -rw-r--r-- | src/rewrites.ml | 1 | ||||
| -rw-r--r-- | src/sail.ml | 20 |
4 files changed, 29 insertions, 3 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 56029c5f..753196a8 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -2032,6 +2032,14 @@ 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 name_file env ast = + let jib, ctx = compile env ast in + let out_chan = open_out name_file in + Marshal.to_channel out_chan jib []; + 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 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..28d10fd3 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -139,6 +139,9 @@ module Make_optimizer(S : Sequence) : sig val optimize : smt_def Stack.t -> smt_def S.t end +val to_axiomatic_model : + string -> Type_check.Env.t -> Type_check.tannot defs -> unit + (** Generate SMT for all the $property and $counterexample pragmas in an AST, and write it to appropriately named files. *) val generate_smt : diff --git a/src/rewrites.ml b/src/rewrites.ml index c94e2f57..4ea52c4d 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5023,7 +5023,6 @@ let rewrites_target tgt = | "c" -> rewrites_c | "ir" -> rewrites_c @ [("properties", [])] | "smt" -> rewrites_c @ [("properties", [])] - | "smtfuzz" -> rewrites_c @ [("properties", [])] | "sail" -> [] | "latex" -> [] | "interpreter" -> rewrites_interpreter diff --git a/src/sail.ml b/src/sail.ml index eae7c4cf..60257c8d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -62,6 +62,8 @@ 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_fuzz = ref false let opt_libs_lem = ref ([]:string list) let opt_libs_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) @@ -161,6 +163,9 @@ 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], + " compile Sail to IR suitable for sail-axiomatic tool"); ( "-c", Arg.Tuple [set_target "c"; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); @@ -349,7 +354,7 @@ let options = Arg.align ([ Arg.Set Profile.opt_profile, " (debug) provide basic profiling information for rewriting passes within Sail"); ( "-dsmtfuzz", - set_target "smtfuzz", + Arg.Tuple [set_target "smt"; Arg.Set opt_smt_fuzz], " (debug) fuzz sail SMT builtins"); ( "-v", Arg.Set opt_print_version, @@ -482,9 +487,20 @@ let target name out_name ast type_envs = flush output_chan; if close then close_out output_chan else () - | Some "smtfuzz" -> + | Some "smt" when !opt_smt_fuzz -> Jib_smt_fuzz.fuzz 0 type_envs ast + | Some "smt" when !opt_smt_axiomatic -> + 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" + in + Reporting.opt_warnings := true; + Jib_smt.to_axiomatic_model name_file type_envs ast_smt | Some "smt" -> let open Ast_util in let props = Property.find_properties ast in |