diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 86 |
1 files changed, 65 insertions, 21 deletions
diff --git a/src/sail.ml b/src/sail.ml index 920542bc..fdf4f5b9 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -54,7 +54,6 @@ module Big_int = Nat_big_num let lib = ref ([] : string list) let opt_file_out : string option ref = ref None -let opt_interactive = ref false let opt_interactive_script : string option ref = ref None let opt_print_version = ref false let opt_print_initial_env = ref false @@ -73,16 +72,17 @@ 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_slice = ref ([]:string list) let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), "<prefix> select output filename prefix"); ( "-i", - Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen], + Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.Set Initial_check.opt_undefined_gen], " start interactive interpreter"); ( "-is", - Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen; + Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.Set Initial_check.opt_undefined_gen; Arg.String (fun s -> opt_interactive_script := Some s)], "<filename> start interactive interpreter and execute commands in script"); ( "-iout", @@ -147,6 +147,9 @@ let options = Arg.align ([ ( "-trace", Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml], " Instrument ouput with tracing"); + ( "-smt_trace", + Arg.Tuple [Arg.Set C_backend.opt_smt_trace], + " Instrument ouput with tracing for SMT"); ( "-cgen", Arg.Set opt_print_cgen, " Generate CGEN source"); @@ -200,6 +203,9 @@ let options = Arg.align ([ ( "-memo_z3", Arg.Set opt_memo_z3, " memoize calls to z3, improving performance when typechecking repeatedly"); + ( "-memo", + Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache], + " memoize calls to z3, and intermediate compilation results"); ( "-undefined_gen", Arg.Set Initial_check.opt_undefined_gen, " generate undefined_type functions for types in the specification"); @@ -237,8 +243,8 @@ let options = Arg.align ([ Arg.Set Rewrites.opt_dmono_continue, " continue despite monomorphisation errors"); ( "-verbose", - Arg.Set opt_print_verbose, - " (debug) pretty-print the input to standard output"); + Arg.Int (fun verbosity -> Util.opt_verbosity := verbosity), + " produce verbose output"); ( "-ddump_tc_ast", Arg.Set opt_ddump_tc_ast, " (debug) dump the typechecked ast to stdout"); @@ -251,6 +257,9 @@ let options = Arg.align ([ ( "-dtc_verbose", Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), "<verbosity> (debug) verbose typechecker output: 0 is silent"); + ( "-dsmt_verbose", + Arg.Set Constraint.opt_smt_verbose, + " (debug) print SMTLIB constraints sent to Z3"); ( "-dno_cast", Arg.Set opt_dno_cast, " (debug) typecheck without any implicit casting"); @@ -266,15 +275,30 @@ let options = Arg.align ([ ( "-dprofile", Arg.Set Profile.opt_profile, " (debug) provides basic profiling information for rewriting passes within Sail"); + ( "-slice", + Arg.String (fun s -> opt_slice := s::!opt_slice), + "<id> produce version of input restricted to the given function"); ( "-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; _; _] -> + (try + let vnum = float_of_string vnum +. 2.0 in + Printf.sprintf "Sail %.1f (%s @ %s)" vnum branch commit + with + | Failure _ -> default) + | _ -> default + let usage_msg = - ("Sail 2.0\n" - ^ "usage: sail <options> <file1.sail> ... <fileN.sail>\n" - ) + version + ^ "\nusage: sail <options> <file1.sail> ... <fileN.sail>\n" let _ = Arg.parse options @@ -282,9 +306,6 @@ let _ = opt_file_arguments := (!opt_file_arguments) @ [s]) usage_msg -let interactive_ast = ref (Ast.Defs []) -let interactive_env = ref Type_check.initial_env - let load_files type_envs files = if !opt_memo_z3 then Constraint.load_digests () else (); @@ -313,9 +334,22 @@ let load_files type_envs files = (out_name, ast, type_envs) +let print_version () = + let open Manifest in + let default = Printf.sprintf "Sail %s @ %s" branch commit in + (* version is the output of git describe *) + match String.split_on_char '-' version with + | [vnum; _; _] -> + (try + let vnum = float_of_string vnum +. 2.0 in + Printf.printf "Sail %.1f (%s @ %s)\n" vnum branch commit + with + | Failure _ -> print_endline default) + | _ -> print_endline default + let main() = if !opt_print_version - then Printf.printf "Sail 2.0\n" + then print_version () else 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 *) @@ -343,11 +377,10 @@ let main() = | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast, !opt_ocaml_generators) in - (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) begin - (if !(opt_interactive) + (if !(Interactive.opt_interactive) then - (interactive_ast := Process_file.rewrite_ast_interpreter ast; interactive_env := type_envs) + (Interactive.ast := Process_file.rewrite_ast_interpreter ast; Interactive.env := type_envs) else ()); (if !(opt_sanity) then @@ -357,6 +390,12 @@ let main() = (if !(opt_print_verbose) then ((Pretty_print_sail.pp_defs stdout) ast) else ()); + (match !opt_slice with + | [] -> () + | ids -> + let ids = List.map Ast_util.mk_id ids in + let ids = Ast_util.IdSet.of_list ids in + Pretty_print_sail.pp_defs stdout (Specialize.slice_defs type_envs ast ids)); (if !(opt_print_ocaml) then let ast_ocaml = rewrite_ast_ocaml ast in @@ -367,7 +406,7 @@ let main() = then let ast_c = rewrite_ast_c ast in let ast_c, type_envs = Specialize.specialize ast_c type_envs in - let ast_c = Spec_analysis.top_sort_defs ast_c in + (* let ast_c = Spec_analysis.top_sort_defs ast_c in *) Util.opt_warnings := true; C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c else ()); @@ -379,13 +418,13 @@ let main() = let mwords = !Pretty_print_lem.opt_mwords in let type_envs, ast_lem = State.add_regstate_defs mwords type_envs ast in let ast_lem = rewrite_ast_lem ast_lem in - output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem] + output "" (Lem_out (!opt_libs_lem)) [out_name,type_envs,ast_lem] else ()); (if !(opt_print_coq) then let type_envs, ast_coq = State.add_regstate_defs true type_envs ast in let ast_coq = rewrite_ast_coq ast_coq in - output "" (Coq_out (!opt_libs_coq)) [out_name,ast_coq] + output "" (Coq_out (!opt_libs_coq)) [out_name,type_envs,ast_coq] else ()); (if !(opt_print_latex) then @@ -406,11 +445,16 @@ let main() = close_out chan end 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)) + try ignore (main ()) + with Failure s -> raise (Reporting.err_general Parse_ast.Unknown ("Failure " ^ s)) end - with Reporting.Fatal_error e -> Reporting.report_error e + with Reporting.Fatal_error e -> + Reporting.print_error e; + Interactive.opt_suppress_banner := true; + if !Interactive.opt_interactive then () else exit 1 |