diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/process_file.ml | 1 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 12 | ||||
| -rw-r--r-- | src/rewrites.mli | 3 | ||||
| -rw-r--r-- | src/sail.ml | 31 |
5 files changed, 14 insertions, 34 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index b3c231fe..5c13642f 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -215,5 +215,4 @@ let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefin let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter -let rewrite_ast_sil = rewrite Rewrites.rewrite_defs_sil let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check diff --git a/src/process_file.mli b/src/process_file.mli index 024a8239..d8a88624 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -57,7 +57,6 @@ val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs -val rewrite_ast_sil : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val load_file_no_check : Ast.order -> string -> unit Ast.defs diff --git a/src/rewrites.ml b/src/rewrites.ml index 40772828..2e8ee407 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3009,18 +3009,6 @@ let rewrite_defs_interpreter = [ ("sizeof", rewrite_sizeof); ] -let rewrite_defs_sil = [ - ("top_sort_defs", top_sort_defs); - ("tuple_vector_assignments", rewrite_tuple_vector_assignments); - ("tuple_assignments", rewrite_tuple_assignments); - ("simple_assignments", rewrite_simple_assignments); - ("constraint", rewrite_constraint); - ("trivial_sizeof", rewrite_trivial_sizeof); - ("sizeof", rewrite_sizeof); - ("remove_vector_concat", rewrite_defs_remove_vector_concat); - ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); - ] - let rewrite_check_annot = let check_annot exp = try diff --git a/src/rewrites.mli b/src/rewrites.mli index 8fceadff..12be7f31 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -63,9 +63,6 @@ val rewrite_defs_interpreter : (string * (tannot defs -> tannot defs)) list (* Perform rewrites to exclude AST nodes not supported for lem out*) val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list -(* Perform rewrites to sail intermediate language *) -val rewrite_defs_sil : (string * (tannot defs -> tannot defs)) list - (* This is a special rewriter pass that checks AST invariants without actually doing any re-writing *) val rewrite_defs_check : (string * (tannot defs -> tannot defs)) list diff --git a/src/sail.ml b/src/sail.ml index 774c7d8f..00f90d3b 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -59,12 +59,10 @@ 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_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) @@ -85,15 +83,9 @@ let options = Arg.align ([ ( "-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"); @@ -106,13 +98,23 @@ let options = Arg.align ([ ( "-lem_mwords", Arg.Set Pretty_print_lem.opt_mwords, " use native machine word library for Lem output"); - ( "-mono-split", + ( "-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"); + (* AA: Should use _ to be consistent with other options, but I keep + this case to make sure nothing breaks immediately. *) + ( "-mono-split", + Arg.String (fun s -> + prerr_endline (("Warning" |> Util.yellow |> Util.clear) ^ ": use -mono_split instead"); + 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"); @@ -167,8 +169,8 @@ let options = Arg.align ([ ] ) let usage_msg = - ("Sail " (*^ "pre beta"*) ^ "\n" - ^ "usage: sail <options> <file1.sail> .. <fileN.sail>\n" + ("Sail 2.0\n" + ^ "usage: sail <options> <file1.sail> ... <fileN.sail>\n" ) let _ = @@ -213,7 +215,7 @@ let load_files type_envs files = let main() = if !opt_print_version - then Printf.printf "Sail private release \n" + then Printf.printf "Sail 2.0\n" else let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in @@ -234,11 +236,6 @@ let main() = (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_sail.pp_defs stdout ast - else ()); (if !(opt_print_ocaml) then let ast_ocaml = rewrite_ast_ocaml ast in |