Merge branch 'sail2' into separate_bv

1 files changed, 17 insertions, 11 deletions

diff --git a/src/sail.ml b/src/sail.ml
index c4991fe5..eae7c4cf 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -87,7 +87,7 @@ let options = Arg.align ([
     Arg.Set Interactive.opt_emacs_mode,
     " run sail interactively as an emacs mode child process");
   ( "-no_warn",
-    Arg.Clear Util.opt_warnings,
+    Arg.Clear Reporting.opt_warnings,
     " do not print warnings");
   ( "-tofrominterp",
     set_target "tofrominterp",
@@ -348,6 +348,9 @@ let options = Arg.align ([
   ( "-dprofile",
     Arg.Set Profile.opt_profile,
     " (debug) provide basic profiling information for rewriting passes within Sail");
+  ( "-dsmtfuzz",
+    set_target "smtfuzz",
+    " (debug) fuzz sail SMT builtins");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
@@ -450,28 +453,28 @@ let target name out_name ast type_envs =
      close_out f
 
   | Some "c" ->
-     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
+     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in
      let ast_c, type_envs =
        if !opt_specialize_c then
-         Specialize.(specialize' 2 int_specialization ast_c type_envs)
+         Specialize.(specialize_passes 2 int_specialization type_envs ast_c)
        else
          ast_c, type_envs
      in
      let close, output_chan = match !opt_file_out with Some f -> true, open_out (f ^ ".c") | None -> false, stdout in
-     Util.opt_warnings := true;
+     Reporting.opt_warnings := true;
      C_backend.compile_ast type_envs output_chan (!opt_includes_c) ast_c;
      flush output_chan;
      if close then close_out output_chan else ()
 
   | Some "ir" ->
-     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
+     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in
      (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *)
      let close, output_chan =
        match !opt_file_out with
        | Some f -> Util.opt_colors := false; (true, open_out (f ^ ".ir.sail"))
        | None -> false, stdout
      in
-     Util.opt_warnings := true;
+     Reporting.opt_warnings := true;
      let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in
      (* let cdefs = List.map Jib_optimize.flatten_cdef cdefs in *)
      let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_cdef cdefs) in
@@ -479,18 +482,21 @@ let target name out_name ast type_envs =
      flush output_chan;
      if close then close_out output_chan else ()
 
+  | Some "smtfuzz" ->
+     Jib_smt_fuzz.fuzz 0 type_envs ast
+
   | Some "smt" ->
      let open Ast_util in
      let props = Property.find_properties ast in
      Bindings.bindings props |> List.map fst |> IdSet.of_list |> Specialize.add_initial_calls;
-     let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
-     let ast_smt, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_smt type_envs) in
+     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 name_file =
        match !opt_file_out with
        | Some f -> fun str -> f ^ "_" ^ str ^ ".smt2"
        | None -> fun str -> str ^ ".smt2"
      in
-     Util.opt_warnings := true;
+     Reporting.opt_warnings := true;
      Jib_smt.generate_smt props name_file type_envs ast_smt;
 
   | Some "lem" ->
@@ -500,7 +506,7 @@ let target name out_name ast type_envs =
      output "" (Coq_out (!opt_libs_coq)) [(out_name, type_envs, ast)]
 
   | Some "latex" ->
-     Util.opt_warnings := true;
+     Reporting.opt_warnings := true;
      let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in
      begin
        try
@@ -524,7 +530,7 @@ let main () =
   else
     begin
       let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
-      Util.opt_warnings := false; (* Don't show warnings during re-writing for now *)
+      Reporting.opt_warnings := false; (* Don't show warnings during re-writing for now *)
 
       begin match !opt_process_elf, !opt_file_out with
       | Some elf, Some out ->