(**************************************************************************) (* Sail *) (* *) (* Copyright (c) 2013-2017 *) (* Kathyrn Gray *) (* Shaked Flur *) (* Stephen Kell *) (* Gabriel Kerneis *) (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) (* Alasdair Armstrong *) (* Brian Campbell *) (* Thomas Bauereiss *) (* Anthony Fox *) (* Jon French *) (* Dominic Mulligan *) (* Stephen Kell *) (* Mark Wassell *) (* *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) (* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) (* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) (* notice, this list of conditions and the following disclaimer in *) (* the documentation and/or other materials provided with the *) (* distribution. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) (* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) (* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) (* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) (* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) (* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) (* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) (* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) (* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) (* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) (* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) (* SUCH DAMAGE. *) (**************************************************************************) open Process_file module Big_int = Nat_big_num module Json = Yojson.Basic let lib = ref ([] : string list) let opt_interactive_script : string option ref = ref None (* Note: May cause a deprecated warning for json type, but this cannot be fixed without breaking Ubuntu 18.04 CI *) let opt_config : Json.t 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_sanity = ref false let opt_includes_c = ref ([]:string list) let opt_specialize_c = 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) let opt_file_arguments = ref ([]:string list) let opt_process_elf : string option ref = ref None let opt_ocaml_generators = ref ([]:string list) let opt_splice = ref ([]:string list) let opt_have_feature = ref None let opt_infer_effects = ref false let set_target name = Arg.Unit (fun _ -> opt_target := Some name) let load_json_config file = try Json.from_file file with | Yojson.Json_error desc | Sys_error desc -> prerr_endline "Error when loading configuration file:"; prerr_endline desc; exit 1 let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), " select output filename prefix"); ( "-i", Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.Set Interactive.opt_auto_interpreter_rewrites; Arg.Set Initial_check.opt_undefined_gen], " start interactive interpreter"); ( "-is", Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.Set Interactive.opt_auto_interpreter_rewrites; Arg.Set Initial_check.opt_undefined_gen; Arg.String (fun s -> opt_interactive_script := Some s)], " start interactive interpreter and execute commands in script"); ( "-iout", Arg.String (fun file -> Value.output_redirect (open_out file)), " print interpreter output to file"); ( "-interact_custom", Arg.Set Interactive.opt_interactive, " drop to an interactive session after running Sail. Differs from \ -i in that it does not set up the interpreter in the interactive \ shell."); ( "-emacs", Arg.Set Interactive.opt_emacs_mode, " run sail interactively as an emacs mode child process"); ( "-no_warn", Arg.Clear Reporting.opt_warnings, " do not print warnings"); ( "-config", Arg.String (fun file -> opt_config := Some (load_json_config file)), " JSON configuration file"); ( "-tofrominterp", set_target "tofrominterp", " output OCaml functions to translate between shallow embedding and interpreter"); ( "-tofrominterp_lem", Arg.Tuple [set_target "tofrominterp"; Arg.Set ToFromInterp_backend.lem_mode], " output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp"); ( "-tofrominterp_mwords", Arg.Tuple [set_target "tofrominterp"; Arg.Set ToFromInterp_backend.mword_mode], " output embedding translation in machine-word mode rather than bit-list mode, implies -tofrominterp"); ( "-tofrominterp_output_dir", Arg.String (fun dir -> opt_tofrominterp_output_dir := Some dir), " set a custom directory to output embedding translation OCaml"); ( "-ocaml", Arg.Tuple [set_target "ocaml"; Arg.Set Initial_check.opt_undefined_gen], " 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], " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml"); ( "-ocaml_build_dir", Arg.String (fun dir -> Ocaml_backend.opt_ocaml_build_dir := dir), " 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), " produce random generators for the given types"); ( "-smt_solver", Arg.String (fun s -> Constraint.set_solver (String.trim s)), " choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices."); ( "-smt_linearize", Arg.Set Type_check.opt_smt_linearize, "(experimental) force linearization for constraints involving exponentials"); ( "-latex", Arg.Tuple [set_target "latex"; Arg.Clear Type_check.opt_expand_valspec], " pretty print the input to LaTeX"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix := prefix), " set a custom prefix for generated LaTeX labels and macro commands (default sail)"); ( "-latex_full_valspecs", Arg.Clear Latex.opt_simple_val, " print full valspecs in LaTeX output"); ( "-latex_abbrevs", Arg.String (fun s -> let abbrevs = String.split_on_char ';' s in let filtered = List.filter (fun abbrev -> not (String.equal "" abbrev)) abbrevs in match List.find_opt (fun abbrev -> not (String.equal "." (String.sub abbrev (String.length abbrev - 1) 1))) filtered with | None -> Latex.opt_abbrevs := filtered | Some abbrev -> raise (Arg.Bad (abbrev ^ " does not end in a '.'"))), " semicolon-separated list of abbreviations to fix spacing for in LaTeX output (default 'e.g.;i.e.')"); ( "-marshal", Arg.Tuple [set_target "marshal"; Arg.Set Initial_check.opt_undefined_gen], " OCaml-marshal out the rewritten AST to a file"); ( "-ir", set_target "ir", " print intermediate representation"); ( "-smt", Arg.Tuple [set_target "smt"], " print SMT translated version of input"); ( "-smt_auto", Arg.Tuple [set_target "smt"; 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, " ignore integer overflow in generated SMT"); ( "-smt_propagate_vars", Arg.Set Jib_smt.opt_propagate_vars, " propgate variables through generated SMT"); ( "-smt_int_size", Arg.String (fun n -> Jib_smt.opt_default_lint_size := int_of_string n), " set a bound of n on the maximum integer bitwidth for generated SMT (default 128)"); ( "-smt_bits_size", Arg.String (fun n -> Jib_smt.opt_default_lbits_index := int_of_string n), " set a bound of 2 ^ n for bitvector bitwidth in generated SMT (default 8)"); ( "-smt_vector_size", Arg.String (fun n -> Jib_smt.opt_default_vector_index := int_of_string n), " set a bound of 2 ^ n for generic vectors in generated SMT (default 5)"); ( "-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], " output a C translated version of the input"); ( "-c2", Arg.Tuple [set_target "c2"; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input (experimental code-generation)"); ( "-c_include", Arg.String (fun i -> opt_includes_c := i::!opt_includes_c), " provide additional include for C output"); ( "-c_no_main", Arg.Set C_backend.opt_no_main, " do not generate the main() function" ); ( "-c_no_rts", Arg.Set C_backend.opt_no_rts, " do not include the Sail runtime" ); ( "-c_no_lib", Arg.Tuple [Arg.Set C_backend.opt_no_lib; Arg.Set C_backend.opt_no_rts], " do not include the Sail runtime or library" ); ( "-c_prefix", Arg.String (fun prefix -> C_backend.opt_prefix := prefix), " prefix generated C functions" ); ( "-c_extra_params", Arg.String (fun params -> C_backend.opt_extra_params := Some params), " generate C functions with additional parameters" ); ( "-c_extra_args", Arg.String (fun args -> C_backend.opt_extra_arguments := Some args), " supply extra argument to every generated C function call" ); ( "-c_specialize", Arg.Set opt_specialize_c, " specialize integer arguments in C output"); ( "-c_preserve", Arg.String (fun str -> Specialize.add_initial_calls (Ast_util.IdSet.singleton (Ast_util.mk_id str))), " make sure the provided function identifier is preserved in C output"); ( "-c_fold_unit", Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str), " remove comma separated list of functions from C output, replacing them with unit"); ( "-c_coverage", Arg.String (fun str -> C_backend.opt_branch_coverage := Some (open_out str)), " Turn on coverage tracking and output information about all branches and functions to a file"); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an ELF file so that it can be executed by compiled C code"); ( "-O", Arg.Tuple [Arg.Set C_backend.optimize_primops; Arg.Set C_backend.optimize_hoist_allocations; Arg.Set Initial_check.opt_fast_undefined; Arg.Set Type_check.opt_no_effects; Arg.Set C_backend.optimize_struct_updates; Arg.Set C_backend.optimize_alias], " turn on optimizations for C compilation"); ( "-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " apply constant folding optimizations"); ( "-Ofixed_int", Arg.Set C_backend.optimize_fixed_int, " assume fixed size integers rather than GMP arbitrary precision integers"); ( "-Ofixed_bits", Arg.Set C_backend.optimize_fixed_bits, " assume fixed size bitvectors rather than arbitrary precision bitvectors"); ( "-Oaarch64_fast", Arg.Set Jib_compile.optimize_aarch64_fast_struct, " apply ARMv8.5 specific optimizations (potentially unsound in general)"); ( "-Ofast_undefined", Arg.Set Initial_check.opt_fast_undefined, " turn on fast-undefined mode"); ( "-static", Arg.Set C_backend.opt_static, " make generated C functions static"); ( "-trace", Arg.Tuple [Arg.Set Ocaml_backend.opt_trace_ocaml], " instrument output with tracing"); ( "-lem", set_target "lem", " output a Lem translated version of the input"); ( "-lem_output_dir", Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), " set a custom directory to output generated Lem"); ( "-isa_output_dir", Arg.String (fun dir -> Process_file.opt_isa_output_dir := Some dir), " set a custom directory to output generated Isabelle auxiliary theories"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), " provide additional library to open in Lem output"); ( "-lem_sequential", Arg.Set Pretty_print_lem.opt_sequential, " use sequential state monad for Lem output"); ( "-lem_mwords", Arg.Set Pretty_print_lem.opt_mwords, " use native machine word library for Lem output"); ( "-coq", set_target "coq", " output a Coq translated version of the input"); ( "-coq_output_dir", Arg.String (fun dir -> Process_file.opt_coq_output_dir := Some dir), " set a custom directory to output generated Coq"); ( "-coq_lib", Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), " provide additional library to open in Coq output"); ( "-coq_alt_modules", Arg.String (fun l -> opt_alt_modules_coq := l::!opt_alt_modules_coq), " provide alternative modules to open in Coq output"); ( "-coq_alt_modules2", Arg.String (fun l -> opt_alt_modules2_coq := l::!opt_alt_modules2_coq), " provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads"); ( "-dcoq_undef_axioms", Arg.Set Pretty_print_coq.opt_undef_axioms, " generate axioms for functions that are declared but not defined"); ( "-dcoq_warn_nonex", Arg.Set Rewrites.opt_coq_warn_nonexhaustive, " generate warnings for non-exhaustive pattern matches in the Coq backend"); ( "-dcoq_debug_on", Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f::!Pretty_print_coq.opt_debug_on), " produce debug messages for Coq output on given function"); ( "-mono_split", Arg.String (fun s -> let l = Util.split_on_char ':' s in match l with | [fname;line;var] -> Rewrites.opt_mono_split := ((fname,int_of_string line),var)::!Rewrites.opt_mono_split | _ -> raise (Arg.Bad (s ^ " not of form ::"))), ":: to case split for monomorphisation"); ( "-memo_z3", Arg.Set opt_memo_z3, " memoize calls to z3, improving performance when typechecking repeatedly"); ( "-no_memo_z3", Arg.Clear opt_memo_z3, " do not memoize calls to z3 (default)"); ( "-memo", Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set Jib_compile.opt_memo_cache], " memoize calls to z3, and intermediate compilation results"); ( "-have_feature", Arg.String (fun symbol -> opt_have_feature := Some symbol), " check if a feature symbol is set by default"); ( "-splice", Arg.String (fun s -> opt_splice := s :: !opt_splice), " add functions from file, replacing existing definitions where necessary"); ( "-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"); ( "-no_lexp_bounds_check", Arg.Set Type_check.opt_no_lexp_bounds_check, " turn off bounds checking for vector assignments in l-expressions"); ( "-no_effects", Arg.Set Type_check.opt_no_effects, " (experimental) turn off effect checking"); ( "-infer_effects", Arg.Set opt_infer_effects, " (experimental) infer effects"); ( "-just_check", Arg.Set opt_just_check, " (experimental) terminate immediately after typechecking"); ( "-dmono_analysis", Arg.Set_int Rewrites.opt_dmono_analysis, " (debug) dump information about monomorphisation analysis: 0 silent, 3 max"); ( "-auto_mono", Arg.Set Rewrites.opt_auto_mono, " automatically infer how to monomorphise code"); ( "-mono_rewrites", Arg.Set Rewrites.opt_mono_rewrites, " turn on rewrites for combining bitvector operations"); ( "-dno_complex_nexps_rewrite", Arg.Clear Rewrites.opt_mono_complex_nexps, " do not move complex size expressions in function signatures into constraints (monomorphisation)"); ( "-dall_split_errors", Arg.Set Rewrites.opt_dall_split_errors, " display all case split errors from monomorphisation, rather than one"); ( "-dmono_continue", Arg.Set Rewrites.opt_dmono_continue, " continue despite monomorphisation errors"); ( "-const_prop_mutrec", Arg.String (fun name -> Constant_propagation_mutrec.targets := Ast_util.mk_id name :: !Constant_propagation_mutrec.targets), " unroll function in a set of mutually recursive functions"); ( "-verbose", Arg.Int (fun verbosity -> Util.opt_verbosity := verbosity), " produce verbose output"); ( "-output_sail", set_target "sail", " print Sail code after type checking and initial rewriting"); ( "-reformat", Arg.String (fun dir -> opt_reformat := Some dir), " reformat the input Sail code placing output into a separate directory"); ( "-ddump_initial_ast", Arg.Set opt_ddump_initial_ast, " (debug) dump the initial ast to stdout"); ( "-ddump_tc_ast", Arg.Set opt_ddump_tc_ast, " (debug) dump the typechecked ast to stdout"); ( "-ddump_rewrite_ast", Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0); Specialize.opt_ddump_spec_ast := Some (l, 0)), " (debug) dump the ast after each rewriting step to _.lem"); ( "-ddump_smt_graphs", Arg.Set Jib_smt.opt_debug_graphs, " (debug) dump flow analysis for properties when generating SMT"); ( "-dtc_verbose", Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), " (debug) verbose typechecker output: 0 is silent"); ( "-dsmt_verbose", Arg.Set Constraint.opt_smt_verbose, " (debug) print SMTLIB constraints sent to SMT solver"); ( "-dno_cast", Arg.Set opt_dno_cast, " (debug) typecheck without any implicit casting"); ( "-dsanity", Arg.Set opt_sanity, " (debug) sanity check the AST (slow)"); ( "-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers"); ( "-dprofile", Arg.Set Profile.opt_profile, " (debug) provide basic profiling information for rewriting passes within Sail"); ( "-dsmtfuzz", Arg.Tuple [set_target "smt"; Arg.Set opt_smt_fuzz], " (debug) fuzz sail SMT builtins"); ( "-v", Arg.Set opt_print_version, " print version"); ] ) let version = let open Manifest in let default = Printf.sprintf "Sail %s @ %s" branch commit in (* version is parsed from the output of git describe *) match String.split_on_char '-' version with | (vnum :: _) -> Printf.sprintf "Sail %s (%s @ %s)" vnum branch commit | _ -> default let usage_msg = version ^ "\nusage: sail ... \n" let _ = Arg.parse options (fun s -> opt_file_arguments := (!opt_file_arguments) @ [s]) usage_msg let prover_regstate tgt ast type_envs = match tgt with | Some "coq" -> State.add_regstate_defs true type_envs ast | Some "lem" -> State.add_regstate_defs !Pretty_print_lem.opt_mwords type_envs ast | _ -> type_envs, ast let target name out_name ast type_envs = match name with | None -> () | Some "sail" -> Pretty_print_sail.pp_ast stdout ast | Some "ocaml" -> let ocaml_generator_info = match !opt_ocaml_generators with | [] -> None | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast.defs, !opt_ocaml_generators) in let out = match !opt_file_out with None -> "out" | Some s -> s in Ocaml_backend.ocaml_compile out ast ocaml_generator_info | Some "tofrominterp" -> let out = match !opt_file_out with None -> "out" | Some s -> s in ToFromInterp_backend.tofrominterp_output !opt_tofrominterp_output_dir out ast | Some "marshal" -> let out_filename = match !opt_file_out with None -> "out" | Some s -> s in let f = open_out_bin (out_filename ^ ".defs") in let remove_prover (l, tannot) = if Type_check.is_empty_tannot tannot then (l, Type_check.empty_tannot) else (l, Type_check.replace_env (Type_check.Env.set_prover None (Type_check.env_of_tannot tannot)) tannot) in Marshal.to_string (Ast_util.map_ast_annot remove_prover ast, Type_check.Env.set_prover None type_envs) [Marshal.Compat_32] |> Base64.encode_string |> output_string f; close_out f | Some "c" -> 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_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 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 "c2" -> let module StringMap = Map.Make(String) 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_passes 2 int_specialization type_envs ast_c) else ast_c, type_envs in let output_name = match !opt_file_out with Some f -> f | None -> "out" in Reporting.opt_warnings := true; let codegen ctx cdefs = let open Json.Util in let codegen_opts = match !opt_config with | Some config -> C_codegen.options_from_json (member "codegen" config) cdefs | None -> C_codegen.default_options cdefs in let module Codegen = C_codegen.Make( struct let opts = codegen_opts end ) in Codegen.emulator ctx output_name cdefs in C_backend.compile_ast_clib type_envs ast_c codegen; | Some "ir" -> 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")) | None -> false, stdout in Reporting.opt_warnings := true; let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in let buf = Buffer.create 256 in Jib_ir.Flat_ir_formatter.output_defs buf cdefs; output_string output_chan (Buffer.contents buf); flush output_chan; if close then close_out output_chan else () | Some "smt" when !opt_smt_fuzz -> Jib_smt_fuzz.fuzz 0 type_envs ast | 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 ^ ".smt_model" | None -> "sail.smt_model" in Reporting.opt_warnings := true; 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 Bindings.bindings props |> List.map fst |> IdSet.of_list |> Specialize.add_initial_calls; 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 Reporting.opt_warnings := true; Jib_smt.generate_smt props name_file type_envs ast_smt; | Some "lem" -> output "" (Lem_out (!opt_libs_lem)) [(out_name, type_envs, ast)] | Some "coq" -> output "" (Coq_out (!opt_libs_coq)) [(out_name, type_envs, ast)] | Some "latex" -> Reporting.opt_warnings := true; let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in begin try if not (Sys.is_directory latex_dir) then begin prerr_endline ("Failure: latex output location exists and is not a directory: " ^ latex_dir); exit 1 end with Sys_error(_) -> Unix.mkdir latex_dir 0o755 end; Latex.opt_directory := latex_dir; let chan = open_out (Filename.concat latex_dir "commands.tex") in output_string chan (Pretty_print_sail.to_string (Latex.defs ast)); close_out chan | Some t -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Undefined target: " ^ t)) let feature_check () = match !opt_have_feature with | None -> () | Some symbol -> if Process_file.have_symbol symbol then exit 0 else exit 2 let main () = feature_check (); if !opt_print_version then print_endline version else begin let reset_effect_checking = !opt_infer_effects && not !Type_check.opt_no_effects in let () = if !opt_infer_effects then Type_check.opt_no_effects := true 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) in Reporting.opt_warnings := false; (* Don't show warnings during re-writing for now *) let ast, type_envs = if !opt_infer_effects then let ast = Spec_analysis.infer_effects ast in let _ = if reset_effect_checking then Type_check.opt_no_effects := true in Type_error.check Type_check.initial_env ast else ast, type_envs in begin match !opt_process_elf, !opt_file_out with | Some elf, Some out -> begin let open Elf_loader in let chan = open_out out in load_elf ~writer:(write_file chan) elf; output_string chan "elf_entry\n"; output_string chan (Big_int.to_string !opt_elf_entry ^ "\n"); close_out chan; exit 0 end | Some _, None -> prerr_endline "Failure: No output file given for processed ELF (option -o)."; exit 1 | None, _ -> () end; if !opt_sanity then ignore (rewrite_ast_check type_envs ast) else (); let type_envs, ast = prover_regstate !opt_target ast type_envs in let ast, type_envs = match !opt_target with Some tgt -> rewrite_ast_target tgt type_envs ast | None -> ast, type_envs in target !opt_target out_name ast type_envs; if !Interactive.opt_interactive then (Interactive.ast := ast; Interactive.env := type_envs) else (); if !opt_memo_z3 then Constraint.save_digests () else () end let _ = try begin try ignore (main ()) with Failure s -> raise (Reporting.err_general Parse_ast.Unknown ("Failure " ^ s)) end with Reporting.Fatal_error e -> Reporting.print_error e; Interactive.opt_suppress_banner := true; if !opt_memo_z3 then Constraint.save_digests () else (); if !Interactive.opt_interactive then () else exit 1