diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 171 |
1 files changed, 128 insertions, 43 deletions
diff --git a/src/sail.ml b/src/sail.ml index 905f03d7..519ec916 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -52,48 +52,111 @@ open Process_file let lib = ref ([] : string list) let opt_file_out : string option ref = ref None +let opt_interactive = ref false let opt_print_version = ref false let opt_print_initial_env = ref false let opt_print_verbose = ref false let opt_print_lem_ast = ref false let opt_print_lem = ref false +let opt_print_sil = ref false let opt_print_ocaml = ref false +let opt_convert = ref false +let opt_memo_z3 = ref false +let opt_sanity = ref false let opt_libs_lem = ref ([]:string list) let opt_libs_ocaml = ref ([]:string list) let opt_file_arguments = ref ([]:string list) +let opt_mono_split = ref ([]:((string * int) * string) list) + let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), "<prefix> select output filename prefix"); + ( "-i", + Arg.Set opt_interactive, + " start interactive interpreter"); + ( "-ocaml", + Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], + " output an OCaml translated version of the input"); + ( "-ocaml_trace", + Arg.Tuple [Arg.Set opt_print_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_lib", + Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml), + "<filename> provide additional library to open in OCaml output"); ( "-lem_ast", Arg.Set opt_print_lem_ast, " output a Lem AST representation of the input"); + ( "-sil", + Arg.Tuple [Arg.Set opt_print_sil; Arg.Set Initial_check.opt_undefined_gen], + " output a SIL translated version of the input"); ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); - ( "-ocaml", - Arg.Set opt_print_ocaml, - " output an OCaml translated version of the input"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), "<filename> provide additional library to open in Lem output"); - ( "-ocaml_lib", - Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml), - "<filename> provide additional library to open in OCaml output"); -(* - ( "-i", - Arg.String (fun l -> lib := l::!lib), - "<library_filename> treat this file as input only and generate no output for it"); -*) - ( "-print_initial_env", - Arg.Set opt_print_initial_env, - " print the built-in initial type environment and terminate"); + ( "-lem_sequential", + Arg.Set Process_file.opt_lem_sequential, + " use sequential state monad for Lem output"); + ( "-lem_mwords", + Arg.Set Process_file.opt_lem_mwords, + " use native machine word library for Lem output"); + ( "-mono-split", + Arg.String (fun s -> + let l = Util.split_on_char ':' s in + match l with + | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split + | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))), + "<filename>:<line>:<variable> to case split for monomorphisation"); + ( "-memo_z3", + Arg.Set opt_memo_z3, + " memoize calls to z3, improving performance when typechecking repeatedly"); + ( "-undefined_gen", + Arg.Set Initial_check.opt_undefined_gen, + " generate undefined_type functions for types in the specification"); + ( "-no_effects", + Arg.Set Type_check.opt_no_effects, + " (experimental) turn off effect checking"); + ( "-new_parser", + Arg.Set Process_file.opt_new_parser, + " (experimental) use new parser"); + ( "-convert", + Arg.Set opt_convert, + " (experimental) convert sail to new syntax for use with -new_parser"); + ( "-just_check", + Arg.Set opt_just_check, + " (experimental) terminate immediately after typechecking"); + ( "-ddump_raw_mono_ast", + Arg.Set opt_ddump_raw_mono_ast, + " (debug) dump the monomorphised ast before type-checking"); + ( "-dmono_analysis", + Arg.Set_int opt_dmono_analysis, + " (debug) dump information about monomorphisation analysis: 0 silent, 3 max"); + ( "-auto_mono", + Arg.Set opt_auto_mono, + " automatically infer how to monomorphise code"); ( "-verbose", Arg.Set opt_print_verbose, " (debug) pretty-print the input to standard output"); - ( "-skip_constraints", - Arg.Clear Type_internal.do_resolve_constraints, - " (debug) skip constraint resolution in type-checking"); + ( "-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)), + "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem"); + ( "-dtc_verbose", + Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), + "<verbosity> (debug) verbose typechecker output: 0 is silent"); + ( "-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"); ( "-v", Arg.Set opt_print_version, " print version"); @@ -110,50 +173,72 @@ 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 main() = - if !(opt_print_version) + if !opt_print_version then Printf.printf "Sail private release \n" - else if !(opt_print_initial_env) then - let ppd_initial_typ_env = - String.concat "" - (List.map - (function (comment,tenv) -> - "(* "^comment^" *)\n" ^ - String.concat "" - (List.map - (function (id,tannot) -> - id ^ " : " ^ - Pretty_print.pp_format_annot_ascii tannot - ^ "\n") - tenv)) - Type_internal.initial_typ_env_list) in - Printf.printf "%s" ppd_initial_typ_env ; - else + else + if !opt_memo_z3 then Constraint.load_digests () else (); let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in - let ast = + 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,kenv,ord) = convert_ast ast in - let (ast,type_envs) = check_ast ast kenv ord in - let ast = rewrite_ast ast in + let ast = convert_ast Ast_util.inc_ord ast in + + if !opt_convert + then (Pretty_print_sail2.pp_defs stdout ast; exit 0) + else (); + + let (ast, type_envs) = check_ast ast in + + let (ast, type_envs) = + match !opt_mono_split, !opt_auto_mono with + | [], false -> ast, type_envs + | locs, _ -> monomorphise_ast locs type_envs ast + in + + let ast = + if !Initial_check.opt_undefined_gen then + rewrite_undefined (rewrite_ast ast) + else rewrite_ast 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 + + if !opt_memo_z3 then Constraint.save_digests () else (); + (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) - begin + begin + (if !(opt_interactive) + then + (interactive_ast := ast; interactive_env := type_envs) + else ()); + (if !(opt_sanity) + then + let _ = rewrite_ast_check ast in + () + else ()); (if !(opt_print_verbose) then ((Pretty_print.pp_defs stdout) ast) else ()); (if !(opt_print_lem_ast) then output "" Lem_ast_out [out_name,ast] else ()); + (if !(opt_print_sil) + then + let ast = rewrite_ast_sil ast in + Pretty_print_sail2.pp_defs stdout ast + else ()); (if !(opt_print_ocaml) - then let ast_ocaml = rewrite_ast_ocaml ast in - if !(opt_libs_ocaml) = [] - then output "" (Ocaml_out None) [out_name,ast_ocaml] - else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml] + then + let ast_ocaml = rewrite_ast_ocaml ast in + let out = match !opt_file_out with None -> "out" | Some s -> s in + Ocaml_backend.ocaml_compile out ast_ocaml else ()); (if !(opt_print_lem) then let ast_lem = rewrite_ast_lem ast in |