Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

1 files changed, 17 insertions, 43 deletions

diff --git a/src/sail.ml b/src/sail.ml
index e792e652..ea642470 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -53,12 +53,10 @@ open Process_file
 module Big_int = Nat_big_num
 
 let lib = ref ([] : string list)
-let opt_file_out : string option ref = ref None
 let opt_interactive_script : string option ref = ref None
 let opt_print_version = ref false
 let opt_target = ref None
 let opt_tofrominterp_output_dir : string option ref = ref None
-let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_includes_c = ref ([]:string list)
 let opt_specialize_c = ref false
@@ -110,6 +108,9 @@ let options = Arg.align ([
     " output an OCaml translated version of the input");
   ( "-ocaml-nobuild",
     Arg.Set Ocaml_backend.opt_ocaml_nobuild,
+    "");
+  ( "-ocaml_nobuild",
+    Arg.Set Ocaml_backend.opt_ocaml_nobuild,
     " do not build generated OCaml");
   ( "-ocaml_trace",
     Arg.Tuple [set_target "ocaml"; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml],
@@ -119,6 +120,9 @@ let options = Arg.align ([
     " set a custom directory to build generated OCaml");
   ( "-ocaml-coverage",
     Arg.Set Ocaml_backend.opt_ocaml_coverage,
+    "");
+  ( "-ocaml_coverage",
+    Arg.Set Ocaml_backend.opt_ocaml_coverage,
     " build OCaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx).");
   ( "-ocaml_generators",
     Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators),
@@ -145,10 +149,10 @@ let options = Arg.align ([
     set_target "ir",
     " print intermediate representation");
   ( "-smt",
-    set_target "smt",
+    Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw],
     " print SMT translated version of input");
   ( "-smt_auto",
-    Arg.Tuple [set_target "smt"; Arg.Set Jib_smt.opt_auto],
+    Arg.Tuple [set_target "smt"; Arg.Clear Jib_compile.opt_track_throw; Arg.Set Jib_smt.opt_auto],
     " generate SMT and automatically call the solver (implies -smt)");
   ( "-smt_ignore_overflow",
     Arg.Set Jib_smt.opt_ignore_overflow,
@@ -301,9 +305,15 @@ let options = Arg.align ([
   ( "-undefined_gen",
     Arg.Set Initial_check.opt_undefined_gen,
     " generate undefined_type functions for types in the specification");
+  ( "-grouped_regstate",
+    Arg.Set State.opt_type_grouped_regstate,
+    " group registers with same type together in generated register state record");
   ( "-enum_casts",
     Arg.Set Initial_check.opt_enum_casts,
     " allow enumerations to be automatically casted to numeric range types");
+  ( "-new_bitfields",
+    Arg.Set Type_check.opt_new_bitfields,
+    " use new bitfield syntax");
   ( "-non_lexical_flow",
     Arg.Set Nl_flow.opt_nl_flow,
     " allow non-lexical flow typing");
@@ -397,43 +407,6 @@ let _ =
       opt_file_arguments := (!opt_file_arguments) @ [s])
     usage_msg
 
-let load_files ?check:(check=false) type_envs files =
-  if !opt_memo_z3 then Constraint.load_digests () else ();
-
-  let t = Profile.start () in
-  let parsed = List.map (fun f -> (f, parse_file f)) files in
-  let ast =
-    List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes)
-                     -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
-  let ast = Process_file.preprocess_ast options ast in
-  let ast = Initial_check.process_ast ~generate:(not check) ast in
-  (* The separate loop measures declarations would be awkward to type check, so
-     move them into the definitions beforehand. *)
-  let ast = Rewrites.move_loop_measures ast in
-  Profile.finish "parsing" t;
-
-  let t = Profile.start () in
-  let (ast, type_envs) = check_ast type_envs ast in
-  Profile.finish "type checking" t;
-
-  if !opt_memo_z3 then Constraint.save_digests () else ();
-
-  if check then
-    ("out.sail", ast, type_envs)
-  else
-    let ast = Scattered.descatter ast in
-    let ast, type_envs = rewrite_ast_initial type_envs ast in
-    (* Recheck after descattering so that the internal type environments always
-       have complete variant types *)
-    let ast, type_envs = Type_error.check Type_check.initial_env ast in
-
-    let out_name = match !opt_file_out with
-      | None when parsed = [] -> "out.sail"
-      | None -> fst (List.hd parsed)
-      | Some f -> f ^ ".sail" in
-
-    (out_name, ast, type_envs)
-
 let prover_regstate tgt ast type_envs =
   match tgt with
   | Some "coq" ->
@@ -513,7 +486,7 @@ let target name out_name ast type_envs =
   | 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 jib, _, ctx = Jib_smt.compile type_envs ast_smt in
      let name_file =
        match !opt_file_out with
        | Some f -> f ^ ".smt_model"
@@ -576,7 +549,8 @@ let main () =
     print_endline version
   else
     begin
-      let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
+      let out_name, ast, type_envs = load_files options Type_check.initial_env !opt_file_arguments in
+      let ast, type_envs = descatter type_envs ast in
       let ast, type_envs =
         List.fold_right (fun file (ast,_) -> Splice.splice ast file)
           (!opt_splice) (ast, type_envs)