diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 20 |
1 files changed, 18 insertions, 2 deletions
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 |