diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 40 |
1 files changed, 29 insertions, 11 deletions
diff --git a/src/sail.ml b/src/sail.ml index 4fd35902..417d3ef4 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -109,7 +109,7 @@ let options = Arg.align ([ Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators), "<types> produce random generators for the given types"); ( "-latex", - Arg.Set opt_print_latex, + Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ], " pretty print the input to latex"); ( "-c", Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen], @@ -128,11 +128,15 @@ let options = Arg.align ([ 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_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"); + ( "-Oexperimental", + Arg.Set C_backend.optimize_experimental, + " turn on additional, experimental optimisations"); ( "-static", Arg.Set C_backend.opt_static, " Make generated C functions static"); @@ -167,7 +171,7 @@ let options = Arg.align ([ Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f::!Pretty_print_coq.opt_debug_on), "<function> produce debug messages for Coq output on given function"); ( "-latex_prefix", - Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix), + Arg.String (fun prefix -> Latex.opt_prefix := prefix), " set a custom prefix for generated latex command (default sail)"); ( "-mono_split", Arg.String (fun s -> @@ -223,7 +227,7 @@ let options = Arg.align ([ Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)), "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem"); ( "-ddump_flow_graphs", - Arg.Set C_backend.opt_ddump_flow_graphs, + Arg.Set C_backend.opt_debug_flow_graphs, " (debug) dump flow analysis for Sail functions when compiling to C"); ( "-dtc_verbose", Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), @@ -237,6 +241,12 @@ let options = Arg.align ([ ( "-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers"); + ( "-dfunction", + Arg.String (fun f -> C_backend.opt_debug_function := f), + " (debug) print debugging output for a single function"); + ( "-dprofile", + Arg.Set Profile.opt_profile, + " (debug) provides basic profiling information for rewriting passes within Sail"); ( "-Xconstraint_synonyms", Arg.Set Type_check.opt_constraint_synonyms, " (extension) allow constraint synonyms"); @@ -262,14 +272,18 @@ let interactive_env = ref Type_check.initial_env let load_files 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 = convert_ast Ast_util.inc_ord 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; let ast = rewrite_ast ast in @@ -356,15 +370,19 @@ let main() = (if !(opt_print_latex) then begin + Util.opt_warnings := true; let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in - try - if not (Sys.is_directory latex_dir) then begin - prerr_endline ("Failure: latex output directory exists but is not a directory: " ^ latex_dir); - exit 1 - end - with Sys_error(_) -> Unix.mkdir latex_dir 0o755; + begin + try + if not (Sys.is_directory latex_dir) then begin + prerr_endline ("Failure: latex output directory exists but 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.latex_defs latex_dir ast)); + output_string chan (Pretty_print_sail.to_string (Latex.defs ast)); close_out chan end else ()); |