From 6dbd0facf0962d869d0c3957f668b035a4a6605c Mon Sep 17 00:00:00 2001 From: Alasdair Date: Mon, 28 Sep 2020 15:57:17 +0100 Subject: Refactor: Rename 'a defs to 'a ast Change internal terminology so we more clearly distinguish between a list of definitions 'defs' and functions that take an entire abstract syntax trees 'ast'. --- src/ast_defs.ml | 2 +- src/ast_util.ml | 6 +- src/ast_util.mli | 14 +-- src/constant_fold.ml | 2 +- src/constant_propagation.ml | 4 +- src/constant_propagation.mli | 4 +- src/constant_propagation_mutrec.ml | 4 +- src/initial_check.mli | 6 +- src/interactive.mli | 2 +- src/jib/c_backend.mli | 7 +- src/jib/jib_compile.mli | 2 +- src/jib/jib_smt.ml | 2 +- src/jib/jib_smt.mli | 8 +- src/monomorphise.ml | 2 +- src/monomorphise.mli | 12 +-- src/pretty_print.mli | 2 +- src/pretty_print_lem.ml | 2 +- src/process_file.ml | 12 +-- src/process_file.mli | 18 ++-- src/property.mli | 4 +- src/rewriter.ml | 14 +-- src/rewriter.mli | 10 +-- src/rewrites.ml | 178 ++++++++++++++++++------------------- src/rewrites.mli | 12 +-- src/sail.ml | 2 +- src/slice.mli | 6 +- src/spec_analysis.mli | 2 +- src/specialize.ml | 12 +-- src/specialize.mli | 8 +- src/splice.ml | 2 +- src/state.ml | 4 +- src/type_check.ml | 4 +- src/type_check.mli | 2 +- src/type_error.ml | 2 +- 34 files changed, 187 insertions(+), 186 deletions(-) (limited to 'src') diff --git a/src/ast_defs.ml b/src/ast_defs.ml index 7d7c7ac5..0ce71618 100644 --- a/src/ast_defs.ml +++ b/src/ast_defs.ml @@ -50,4 +50,4 @@ open Ast -type 'a defs = Defs of 'a def list +type 'a ast = Defs of 'a def list diff --git a/src/ast_util.ml b/src/ast_util.ml index a342fc6b..b0137880 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -713,7 +713,7 @@ and map_def_annot f = function | DEF_reg_dec ds -> DEF_reg_dec (map_decspec_annot f ds) | DEF_internal_mutrec fds -> DEF_internal_mutrec (List.map (map_fundef_annot f) fds) | DEF_pragma (name, arg, l) -> DEF_pragma (name, arg, l) -and map_defs_annot f = function +and map_ast_annot f = function | Defs defs -> Defs (List.map (map_def_annot f) defs) and map_loop_measure_annot f = function @@ -1086,7 +1086,7 @@ let ids_of_def = function | DEF_spec vs -> IdSet.singleton (id_of_val_spec vs) | DEF_internal_mutrec fds -> IdSet.of_list (List.map id_of_fundef fds) | _ -> IdSet.empty -let ids_of_defs (Defs defs) = +let ids_of_ast (Defs defs) = List.fold_left IdSet.union IdSet.empty (List.map ids_of_def defs) let val_spec_ids (Defs defs) = @@ -1540,7 +1540,7 @@ let rec split_defs' f defs acc = | def :: defs when f def -> Some (acc, def, defs) | def :: defs -> split_defs' f defs (def :: acc) -let split_defs f (Defs defs) = +let split_ast f (Defs defs) = match split_defs' f defs [] with | None -> None | Some (pre_defs, def, post_defs) -> diff --git a/src/ast_util.mli b/src/ast_util.mli index 5d740277..d9f80778 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -355,7 +355,7 @@ val map_valspec_annot : ('a annot -> 'b annot) -> 'a val_spec -> 'b val_spec val map_scattered_annot : ('a annot -> 'b annot) -> 'a scattered_def -> 'b scattered_def val map_def_annot : ('a annot -> 'b annot) -> 'a def -> 'b def -val map_defs_annot : ('a annot -> 'b annot) -> 'a defs -> 'b defs +val map_ast_annot : ('a annot -> 'b annot) -> 'a ast -> 'b ast (** {2 Extract locations from terms} *) val id_loc : id -> Parse_ast.l @@ -455,17 +455,17 @@ val rename_valspec : id -> 'a val_spec -> 'a val_spec val rename_fundef : id -> 'a fundef -> 'a fundef -val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option +val split_ast : ('a def -> bool) -> 'a ast -> ('a ast * 'a def * 'a ast) option -val append_ast : 'a defs -> 'a defs -> 'a defs -val concat_ast : 'a defs list -> 'a defs +val append_ast : 'a ast -> 'a ast -> 'a ast +val concat_ast : 'a ast list -> 'a ast val type_union_id : type_union -> id val ids_of_def : 'a def -> IdSet.t -val ids_of_defs : 'a defs -> IdSet.t +val ids_of_ast : 'a ast -> IdSet.t -val val_spec_ids : 'a defs -> IdSet.t +val val_spec_ids : 'a ast -> IdSet.t val pat_ids : 'a pat -> IdSet.t @@ -502,7 +502,7 @@ val extern_assoc : string -> (string * string) list -> string option the closest annotation or even finding an annotation at all. This is used by the Emacs mode to provide type-at-cursor functionality and we don't mind if it's a bit fuzzy in that context. *) -val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a defs -> (Ast.l * 'a) option +val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a ast -> (Ast.l * 'a) option (** {2 Substitutions} diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 1c273df1..c9314002 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -302,7 +302,7 @@ let rec rewrite_constant_function_calls' fixed target ast = rewriters_base with rewrite_exp = (fun _ -> rw_exp fixed target ok not_ok istate) } in - let ast = rewrite_defs_base rw_defs ast in + let ast = rewrite_ast_base rw_defs ast in (* We keep iterating until we have no more re-writes to do *) if !rewrite_count > 0 then rewrite_constant_function_calls' fixed target ast diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index c190cffc..b7bc0a69 100644 --- a/src/constant_propagation.ml +++ b/src/constant_propagation.ml @@ -307,7 +307,7 @@ let const_props target defs ref_vars = let interpreter_istate = (* Do not interpret undefined_X functions *) let open Interpreter in - let undefined_builtin_ids = ids_of_defs (Defs Initial_check.undefined_builtin_val_specs) in + let undefined_builtin_ids = ids_of_ast (Defs Initial_check.undefined_builtin_val_specs) in let remove_primop id = StringMap.remove (string_of_id id) in let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in let (lstate, gstate) = Constant_fold.initial_state defs Type_check.initial_env in @@ -894,4 +894,4 @@ let remove_impossible_int_cases _ = in let open Rewriter in let rewrite_exp _ = fold_exp { id_exp_alg with e_case = e_case; e_if = e_if } in - rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } + rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp } diff --git a/src/constant_propagation.mli b/src/constant_propagation.mli index 1312290a..fb2ad179 100644 --- a/src/constant_propagation.mli +++ b/src/constant_propagation.mli @@ -61,7 +61,7 @@ open Type_check val const_prop : string -> - tannot defs -> + tannot ast -> IdSet.t -> tannot exp Bindings.t * nexp KBindings.t -> tannot exp Bindings.t -> @@ -70,4 +70,4 @@ val const_prop : val referenced_vars : tannot exp -> IdSet.t -val remove_impossible_int_cases : 'a -> tannot defs -> tannot defs +val remove_impossible_int_cases : 'a -> tannot ast -> tannot ast diff --git a/src/constant_propagation_mutrec.ml b/src/constant_propagation_mutrec.ml index a8c26bff..67d218dd 100644 --- a/src/constant_propagation_mutrec.ml +++ b/src/constant_propagation_mutrec.ml @@ -191,7 +191,7 @@ let prop_args_pexp target defs ksubsts args pexp = in construct_pexp (pat', guard, exp', annot) -let rewrite_defs target env (Defs defs) = +let rewrite_ast target env (Defs defs) = let rec rewrite = function | [] -> [] | DEF_internal_mutrec mutrecs :: ds -> @@ -206,7 +206,7 @@ let rewrite_defs target env (Defs defs) = | [] -> [infer_exp env (mk_lit_exp L_unit)] | args' -> args' in - if not (IdSet.mem id' (ids_of_defs (Defs !valspecs))) then begin + if not (IdSet.mem id' (ids_of_ast (Defs !valspecs))) then begin (* Generate copy of function with constant arguments propagated in *) let (FD_aux (FD_function (_, _, _, fcls), _)) = List.find (fun fd -> Id.compare id (id_of_fundef fd) = 0) mutrecs diff --git a/src/initial_check.mli b/src/initial_check.mli index 48bdc785..0a5db7c2 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -97,14 +97,14 @@ val undefined_builtin_val_specs : unit def list (** If the generate flag is false, then we won't generate any auxilliary definitions, like the initialize_registers function *) -val process_ast : ?generate:bool -> Parse_ast.defs -> unit defs +val process_ast : ?generate:bool -> Parse_ast.defs -> unit ast (** {2 Parsing expressions and definitions from strings} *) val extern_of_string : id -> string -> unit def val val_spec_of_string : id -> string -> unit def -val ast_of_def_string : string -> unit defs -val ast_of_def_string_with : (Parse_ast.def list -> Parse_ast.def list) -> string -> unit defs +val ast_of_def_string : string -> unit ast +val ast_of_def_string_with : (Parse_ast.def list -> Parse_ast.def list) -> string -> unit ast val exp_of_string : string -> unit exp val typ_of_string : string -> typ val constraint_of_string : string -> n_constraint diff --git a/src/interactive.mli b/src/interactive.mli index 46b52022..0b087dc7 100644 --- a/src/interactive.mli +++ b/src/interactive.mli @@ -57,7 +57,7 @@ val opt_emacs_mode : bool ref val opt_suppress_banner : bool ref val opt_auto_interpreter_rewrites : bool ref -val ast : tannot defs ref +val ast : tannot ast ref val env : Env.t ref diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index d4478c88..cbd0d36e 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -48,6 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) +open Ast_defs open Jib open Type_check @@ -99,7 +100,7 @@ val optimize_alias : bool ref val optimize_fixed_int : bool ref val optimize_fixed_bits : bool ref -val jib_of_ast : Env.t -> tannot Ast_defs.defs -> cdef list * Jib_compile.ctx -val compile_ast : Env.t -> out_channel -> string list -> tannot Ast_defs.defs -> unit +val jib_of_ast : Env.t -> tannot ast -> cdef list * Jib_compile.ctx +val compile_ast : Env.t -> out_channel -> string list -> tannot ast -> unit -val compile_ast_clib : Env.t -> tannot Ast_defs.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit +val compile_ast_clib : Env.t -> tannot ast -> (Jib_compile.ctx -> cdef list -> unit) -> unit diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index 38d03d40..a0acdd0d 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -128,7 +128,7 @@ module Make(C: Config) : sig (see Util.progress). *) val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx - val compile_ast : ctx -> tannot defs -> cdef list * ctx + val compile_ast : ctx -> tannot ast -> cdef list * ctx end (** Adds some special functions to the environment that are used to diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 2e0299d9..b03c1134 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -91,7 +91,7 @@ type ctx = { tc_env : Type_check.Env.t; pragma_l : Ast.l; arg_stack : (int * string) Stack.t; - ast : Type_check.tannot defs; + ast : Type_check.tannot ast; shared : ctyp Bindings.t; preserved : IdSet.t; events : smt_exp Stack.t EventMap.t ref; diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli index 421cbf2c..820f06d1 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -92,7 +92,7 @@ type ctx = { generating the SMT for. Used for error messages. *) arg_stack : (int * string) Stack.t; (** Used internally to keep track of function argument names *) - ast : Type_check.tannot defs; + ast : Type_check.tannot ast; (** The fully type-checked ast *) shared : ctyp Bindings.t; (** Shared variables. These variables do not get renamed by @@ -124,7 +124,7 @@ type ctx = { } (** Compile an AST into Jib suitable for SMT generation, and initialise a context. *) -val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * Jib_compile.ctx * ctx +val compile : Type_check.Env.t -> Type_check.tannot ast -> cdef list * Jib_compile.ctx * ctx (* TODO: Currently we internally use mutable stacks and queues to avoid any issues with stack overflows caused by some non @@ -154,7 +154,7 @@ module Make_optimizer(S : Sequence) : sig end val serialize_smt_model : - string -> Type_check.Env.t -> Type_check.tannot defs -> unit + string -> Type_check.Env.t -> Type_check.tannot ast -> unit val deserialize_smt_model : string -> cdef list * ctx @@ -165,5 +165,5 @@ val generate_smt : (string * string * l * 'a val_spec) Bindings.t (* See Property.find_properties *) -> (string -> string) (* Applied to each function name to generate the file name for the smtlib file *) -> Type_check.Env.t - -> Type_check.tannot defs + -> Type_check.tannot ast -> unit diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 318cfa63..968b1172 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3410,7 +3410,7 @@ and rewrite_exp exp = Rewriter.fold_exp { Rewriter.id_exp_alg with e_aux = rewri let mono_rewrite defs = let open Rewriter in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_exp = fun _ -> fold_exp { id_exp_alg with e_aux = rewrite_aux } } defs diff --git a/src/monomorphise.mli b/src/monomorphise.mli index 7db12078..bf6c9520 100644 --- a/src/monomorphise.mli +++ b/src/monomorphise.mli @@ -61,17 +61,17 @@ val monomorphise : string -> (* Target backend *) options -> ((string * int) * string) list -> (* List of splits from the command line *) - Type_check.tannot defs -> - Type_check.tannot defs + Type_check.tannot ast -> + Type_check.tannot ast (* Rewrite (combinations of) variable-sized operations into fixed-sized operations *) -val mono_rewrites : Type_check.tannot defs -> Type_check.tannot defs +val mono_rewrites : Type_check.tannot ast -> Type_check.tannot ast (* Move complex nexps in function signatures into constraints *) -val rewrite_toplevel_nexps : Type_check.tannot defs -> Type_check.tannot defs +val rewrite_toplevel_nexps : Type_check.tannot ast -> Type_check.tannot ast (* Add casts across case splits *) -val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs +val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast (* Replace atom arguments which are fixed by a type parameter for a size with a singleton type *) -val rewrite_atoms_to_singletons : string -> Type_check.tannot defs -> Type_check.tannot defs +val rewrite_atoms_to_singletons : string -> Type_check.tannot ast -> Type_check.tannot ast diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 2738e025..2995b8a3 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -53,4 +53,4 @@ open Ast_defs open Type_check (* Prints on formatter the defs as Lem Ast nodes *) -val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> Env.t -> tannot defs -> string -> unit +val pp_ast_lem : (out_channel * string list) -> (out_channel * string list) -> Env.t -> tannot ast -> string -> unit diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c3006d7a..dff937a7 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1561,7 +1561,7 @@ let find_exc_typ defs = | _ -> false in if List.exists is_exc_typ_def defs then "exception" else "unit" -let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) type_env (Defs defs) top_line = +let pp_ast_lem (types_file,types_modules) (defs_file,defs_modules) type_env (Defs defs) top_line = (* let regtypes = find_regtypes d in *) let state_ids = State.generate_regstate_defs !opt_mwords defs diff --git a/src/process_file.ml b/src/process_file.ml index 2cf0325e..63ea49cc 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -264,9 +264,9 @@ let opt_ddump_tc_ast = ref false let opt_ddump_rewrite_ast = ref None let opt_dno_cast = ref false -let check_ast (env : Type_check.Env.t) (defs : unit defs) : Type_check.tannot defs * Type_check.Env.t = +let check_ast (env : Type_check.Env.t) (ast : unit ast) : Type_check.tannot ast * Type_check.Env.t = let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in - let ast, env = Type_error.check env defs in + let ast, env = Type_error.check env ast in let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in let () = if !opt_just_check then exit 0 else () in (ast, env) @@ -367,7 +367,7 @@ let output_lem filename libs type_env defs = open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in let ((o,_,_,_) as ext_o) = open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in - (Pretty_print.pp_defs_lem + (Pretty_print.pp_ast_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) type_env defs generated_line); @@ -446,11 +446,11 @@ let rewrite env rewriters defs = | Type_check.Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) -let rewrite_ast_initial env = rewrite env [("initial", fun env defs -> Rewriter.rewrite_defs defs, env)] +let rewrite_ast_initial env = rewrite env [("initial", fun env defs -> Rewriter.rewrite_ast defs, env)] -let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_defs_target tgt) +let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_ast_target tgt) -let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check +let rewrite_ast_check env = rewrite env Rewrites.rewrite_ast_check let descatter type_envs ast = let ast = Scattered.descatter ast in diff --git a/src/process_file.mli b/src/process_file.mli index 041026d5..1c4cddc9 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -59,10 +59,10 @@ val have_symbol : string -> bool val add_symbol : string -> unit val preprocess : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.def list -> Parse_ast.def list -val check_ast : Type_check.Env.t -> unit defs -> Type_check.tannot defs * Type_check.Env.t -val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t -val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t -val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t +val check_ast : Type_check.Env.t -> unit ast -> Type_check.tannot ast * Type_check.Env.t +val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t +val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t +val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t val opt_file_out : string option ref val opt_memo_z3 : bool ref @@ -84,9 +84,9 @@ type out_type = | Coq_out of string list (* If present, the strings are files to open in the coq backend*) val output : - string -> (* The path to the library *) - out_type -> (* Backend kind *) - (string * Type_check.Env.t * Type_check.tannot Ast_defs.defs) list -> (*File names paired with definitions *) + string -> (* The path to the library *) + out_type -> (* Backend kind *) + (string * Type_check.Env.t * Type_check.tannot ast) list -> (*File names paired with definitions *) unit (** [always_replace_files] determines whether Sail only updates modified files. @@ -95,6 +95,6 @@ val output : the output file is only updated, if its content really changes. *) val always_replace_files : bool ref -val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot defs * Type_check.Env.t) +val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot ast * Type_check.Env.t) -val descatter : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t +val descatter : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t diff --git a/src/property.mli b/src/property.mli index bba1f638..2d366fa0 100644 --- a/src/property.mli +++ b/src/property.mli @@ -67,7 +67,7 @@ open Type_check where prop_type is either "counterexample" or "property" and the location loc is the location that was attached to the pragma *) -val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t +val find_properties : 'a ast -> (string * string * l * 'a val_spec) Bindings.t (** For a property @@ -87,7 +87,7 @@ val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t generation/proving we want to ensure that inputs outside the constraints of the function are ignored. *) -val rewrite : tannot defs -> tannot defs +val rewrite : tannot ast -> tannot ast type event = Overflow | Assertion | Assumption | Match | Return diff --git a/src/rewriter.ml b/src/rewriter.ml index eb8208dd..49689b96 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -61,7 +61,7 @@ type 'a rewriters = { rewrite_let : 'a rewriters -> 'a letbind -> 'a letbind; rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef; rewrite_def : 'a rewriters -> 'a def -> 'a def; - rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; + rewrite_ast : 'a rewriters -> 'a ast -> 'a ast; } let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a @@ -386,13 +386,13 @@ let rewrite_def rewriters d = match d with | DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp) | DEF_loop_measures (id,_) -> raise (Reporting.err_unreachable (id_loc id) __POS__ "DEF_loop_measures survived to rewriter") -let rewrite_defs_base rewriters (Defs defs) = +let rewrite_ast_base rewriters (Defs defs) = let rec rewrite ds = match ds with | [] -> [] | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in Defs (rewrite defs) -let rewrite_defs_base_progress prefix rewriters (Defs defs) = +let rewrite_ast_base_progress prefix rewriters (Defs defs) = let total = List.length defs in let rec rewrite n = function | [] -> [] @@ -411,7 +411,7 @@ let rec takedrop n xs = let ys, xs = takedrop (n - 1) xs in x :: ys, xs -let rewrite_defs_base_parallel j rewriters (Defs defs) = +let rewrite_ast_base_parallel j rewriters (Defs defs) = let module IntMap = Map.Make(struct type t = int let compare = compare end) in let total = List.length defs in let defs = ref defs in @@ -428,7 +428,7 @@ let rewrite_defs_base_parallel j rewriters (Defs defs) = let pid = Unix.fork () in begin if pid = 0 then - let Defs work = rewrite_defs_base rewriters (Defs work) in + let Defs work = rewrite_ast_base rewriters (Defs work) in let out_chan = open_out result in Marshal.to_channel out_chan work [Marshal.Closures]; close_out out_chan; @@ -468,9 +468,9 @@ let rewriters_base = rewrite_lexp = rewrite_lexp; rewrite_fun = rewrite_fun; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} + rewrite_ast = rewrite_ast_base} -let rewrite_defs (Defs defs) = rewrite_defs_base rewriters_base (Defs defs) +let rewrite_ast (Defs defs) = rewrite_ast_base rewriters_base (Defs defs) type ('a,'pat,'pat_aux) pat_alg = { p_lit : lit -> 'pat_aux diff --git a/src/rewriter.mli b/src/rewriter.mli index 9ea01096..fd874ba0 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -61,7 +61,7 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; rewrite_let : 'a rewriters -> 'a letbind -> 'a letbind; rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef; rewrite_def : 'a rewriters -> 'a def -> 'a def; - rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; + rewrite_ast : 'a rewriters -> 'a ast -> 'a ast; } val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp @@ -69,14 +69,14 @@ val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp val rewriters_base : tannot rewriters (** The identity re-writer *) -val rewrite_defs : tannot defs -> tannot defs +val rewrite_ast : tannot ast -> tannot ast -val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs +val rewrite_ast_base : tannot rewriters -> tannot ast -> tannot ast -val rewrite_defs_base_parallel : int -> tannot rewriters -> tannot defs -> tannot defs +val rewrite_ast_base_parallel : int -> tannot rewriters -> tannot ast -> tannot ast (** Same as rewrite_defs_base but display a progress bar when verbosity >= 1 *) -val rewrite_defs_base_progress : string -> tannot rewriters -> tannot defs -> tannot defs +val rewrite_ast_base_progress : string -> tannot rewriters -> tannot ast -> tannot ast val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp diff --git a/src/rewrites.ml b/src/rewrites.ml index b1cfce86..ff909a35 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -219,7 +219,7 @@ let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with | Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l) | _ -> nexp_aux -let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = +let rewrite_ast_nexp_ids, rewrite_typ_nexp_ids = let rec rewrite_typ env (Typ_aux (typ, l) as typ_aux) = match typ with | Typ_fn (arg_ts, ret_t, eff) -> Typ_aux (Typ_fn (List.map (rewrite_typ env) arg_ts, rewrite_typ env ret_t, eff), l) @@ -271,20 +271,20 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = | d -> Rewriter.rewrite_def rewriters d in - (fun env defs -> rewrite_defs_base { rewriters_base with + (fun env defs -> rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); rewrite_def = rewrite_def env } defs), rewrite_typ -let rewrite_defs_remove_assert defs = +let rewrite_ast_remove_assert defs = let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with | E_constraint _ -> E_assert (exp, str) | _ -> E_assert (E_aux (E_lit (mk_lit L_true), simple_annot l bool_typ), str) in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_assert = e_assert}) } defs @@ -595,7 +595,7 @@ let rewrite_fun_remove_vector_concat_pat (FCL_aux (FCL_Funcl (id,pexp'),(l,annot))) in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) -let rewrite_defs_remove_vector_concat env (Defs defs) = +let rewrite_ast_remove_vector_concat env (Defs defs) = let rewriters = {rewrite_exp = rewrite_exp_remove_vector_concat_pat; rewrite_pat = rewrite_pat; @@ -603,7 +603,7 @@ let rewrite_defs_remove_vector_concat env (Defs defs) = rewrite_lexp = rewrite_lexp; rewrite_fun = rewrite_fun_remove_vector_concat_pat; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} in + rewrite_ast = rewrite_ast_base} in let rewrite_def d = let d = rewriters.rewrite_def rewriters d in match d with @@ -1188,7 +1188,7 @@ let rewrite_fun_remove_bitvector_pat | _ -> funcls in FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot)) -let rewrite_defs_remove_bitvector_pats env (Defs defs) = +let rewrite_ast_remove_bitvector_pats env (Defs defs) = let rewriters = {rewrite_exp = rewrite_exp_remove_bitvector_pat; rewrite_pat = rewrite_pat; @@ -1196,7 +1196,7 @@ let rewrite_defs_remove_bitvector_pats env (Defs defs) = rewrite_lexp = rewrite_lexp; rewrite_fun = rewrite_fun_remove_bitvector_pat; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base } in + rewrite_ast = rewrite_ast_base } in let rewrite_def d = let d = rewriters.rewrite_def rewriters d in match d with @@ -1213,7 +1213,7 @@ let rewrite_defs_remove_bitvector_pats env (Defs defs) = (* Rewrite literal number patterns to guarded patterns Those numeral patterns are not handled very well by Lem (or Isabelle) *) -let rewrite_defs_remove_numeral_pats env = +let rewrite_ast_remove_numeral_pats env = let p_lit outer_env = function | L_aux (L_num n, l) -> let id = fresh_id "l__" Parse_ast.Unknown in @@ -1243,10 +1243,10 @@ let rewrite_defs_remove_numeral_pats env = FCL_aux (FCL_Funcl (id, fold_pexp exp_alg pexp), annot) in let rewrite_fun _ (FD_aux (FD_function (r_o, t_o, e_o, funcls), a)) = FD_aux (FD_function (r_o, t_o, e_o, List.map rewrite_funcl funcls), a) in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp; rewrite_fun = rewrite_fun } -let rewrite_defs_vector_string_pats_to_bit_list env = +let rewrite_ast_vector_string_pats_to_bit_list env = let rewrite_p_aux (pat, (annot : tannot annot)) = let env = env_of_annot annot in match pat with @@ -1266,7 +1266,7 @@ let rewrite_defs_vector_string_pats_to_bit_list env = let rewrite_exp rw exp = fold_exp { id_exp_alg with e_aux = rewrite_e_aux; pat_alg = pat_alg } exp in - rewrite_defs_base { rewriters_base with rewrite_pat = rewrite_pat; rewrite_exp = rewrite_exp } + rewrite_ast_base { rewriters_base with rewrite_pat = rewrite_pat; rewrite_exp = rewrite_exp } let rewrite_bit_lists_to_lits env = (* TODO Make all rewriting passes support bitvector literals instead of @@ -1299,7 +1299,7 @@ let rewrite_bit_lists_to_lits env = with _ -> rewrap e in let rewrite_exp rw = fold_exp { id_exp_alg with e_aux = e_aux; } in - rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } + rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp } (* Remove pattern guards by rewriting them to if-expressions within the pattern expression. *) @@ -1364,9 +1364,9 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd | _ -> funcls (* TODO is the empty list possible here? *) in FD_aux (FD_function(r,t,e,funcls),(l,fdannot)) -let rewrite_defs_guarded_pats env = - rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp_guarded_pats; - rewrite_fun = rewrite_fun_guarded_pats } +let rewrite_ast_guarded_pats env = + rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp_guarded_pats; + rewrite_fun = rewrite_fun_guarded_pats } let rec rewrite_lexp_to_rhs ((LEXP_aux(lexp,((l,_) as annot))) as le) = @@ -1397,7 +1397,7 @@ let updates_vars exp = fst (fold_exp { (compute_exp_alg false (||)) with e_assign = e_assign } exp) -(*Expects to be called after rewrite_defs; thus the following should not appear: +(*Expects to be called after rewrite_ast; thus the following should not appear: internal_exp of any form lit vectors in patterns or expressions *) @@ -1430,14 +1430,14 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f | _ -> rewrite_base full_exp -let rewrite_defs_exp_lift_assign env defs = rewrite_defs_base +let rewrite_ast_exp_lift_assign env defs = rewrite_ast_base {rewrite_exp = rewrite_exp_lift_assign_intro; rewrite_pat = rewrite_pat; rewrite_let = rewrite_let; rewrite_lexp = rewrite_lexp (*_lift_assign_intro*); rewrite_fun = rewrite_fun; rewrite_def = rewrite_def; - rewrite_defs = rewrite_defs_base} defs + rewrite_ast = rewrite_ast_base} defs (* Rewrite assignments to register references into calls to a builtin function @@ -1478,7 +1478,7 @@ let rewrite_register_ref_writes (Defs defs) = TODO: Maybe separate generic removal of redundant returns, and Lem-specific rewriting of early returns *) -let rewrite_defs_early_return env (Defs defs) = +let rewrite_ast_early_return env (Defs defs) = let is_unit (E_aux (exp, _)) = match exp with | E_lit (L_aux (L_unit, _)) -> true | _ -> false in @@ -1649,7 +1649,7 @@ let rewrite_defs_early_return env (Defs defs) = let (Defs early_ret_spec) = fst (Type_error.check initial_env (Defs [gen_vs ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_fun = rewrite_fun_early_return } (Defs (early_ret_spec @ defs)) @@ -1998,7 +1998,7 @@ let rewrite_undefined mwords env = | _ -> exp in let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) } + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) } let rewrite_undefined_if_gen always_bitvector env defs = if !Initial_check.opt_undefined_gen @@ -2077,7 +2077,7 @@ let rewrite_simple_types env (Defs defs) = rewrite_pat = (fun _ -> fold_pat simple_pat) } in let defs = Defs (List.map simple_def defs) in - rewrite_defs_base simple_defs defs + rewrite_ast_base simple_defs defs let rewrite_vector_concat_assignments env defs = let assign_tuple e_aux annot = @@ -2137,7 +2137,7 @@ let rewrite_vector_concat_assignments env defs = e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot) } in let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in - rewrite_defs_base assign_defs defs + rewrite_ast_base assign_defs defs let rewrite_tuple_assignments env defs = let assign_tuple e_aux annot = @@ -2162,7 +2162,7 @@ let rewrite_tuple_assignments env defs = e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot) } in let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in - rewrite_defs_base assign_defs defs + rewrite_ast_base assign_defs defs let rewrite_simple_assignments allow_fields env defs = let rec is_simple (LEXP_aux (aux, _)) = @@ -2188,9 +2188,9 @@ let rewrite_simple_assignments allow_fields env defs = e_aux = (fun (e_aux, annot) -> assign_e_aux e_aux annot) } in let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in - rewrite_defs_base assign_defs defs + rewrite_ast_base assign_defs defs -let rewrite_defs_remove_blocks env = +let rewrite_ast_remove_blocks env = let letbind_wild v body = let l = get_loc_exp v in let env = env_of v in @@ -2212,14 +2212,14 @@ let rewrite_defs_remove_blocks env = let alg = { id_exp_alg with e_aux = e_aux } in - rewrite_defs_base + rewrite_ast_base {rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } @@ -2249,7 +2249,7 @@ let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list | [] -> k [] | exp :: exps -> f exp (fun exp -> mapCont f exps (fun exps -> k (exp :: exps))) -let rewrite_defs_letbind_effects env = +let rewrite_ast_letbind_effects env = let rec value ((E_aux (exp_aux,_)) as exp) = not (effectful exp || updates_vars exp) @@ -2528,17 +2528,17 @@ let rewrite_defs_letbind_effects env = DEF_internal_mutrec (List.map (rewrite_fun rewriters) fdefs) | d -> d in - rewrite_defs_base + rewrite_ast_base {rewrite_exp = rewrite_exp ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } -let rewrite_defs_internal_lets env = +let rewrite_ast_internal_lets env = let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with | LEXP_id id -> P_aux (P_id id, annot) @@ -2581,14 +2581,14 @@ let rewrite_defs_internal_lets env = E_let (LB_aux (LB_val (P_aux (paux, annot), exp1), annot), exp2) in let alg = { id_exp_alg with e_let = e_let; e_var = e_var } in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = (fun _ exp -> fold_exp alg (propagate_exp_effect exp)) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } @@ -2626,7 +2626,7 @@ let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot anno let pexp_rewriters rewrite_pexp = let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } let stringappend_counter = ref 0 @@ -2862,7 +2862,7 @@ let construct_toplevel_string_append_func env f_id pat = let new_fun_def, env = Type_check.check_fundef env new_fun_def in List.flatten [new_val_spec; new_fun_def] -let rewrite_defs_toplevel_string_append env (Defs defs) = +let rewrite_ast_toplevel_string_append env (Defs defs) = let new_defs = ref ([] : tannot def list) in let rec rewrite_pexp (Pat_aux (pexp_aux, pexp_annot) as pexp) = (* merge cases of Pat_exp and Pat_when *) @@ -2899,7 +2899,7 @@ let rewrite_defs_toplevel_string_append env (Defs defs) = Defs (List.map rewrite defs |> List.flatten) -let rec rewrite_defs_pat_string_append env = +let rec rewrite_ast_pat_string_append env = let rec rewrite_pat env ((pat : tannot pat), (guards : tannot exp list), (expr : tannot exp)) = let guards_ref = ref guards in let expr_ref = ref expr in @@ -3147,7 +3147,7 @@ let fresh_mappingpatterns_id () = mappingpatterns_counter := !mappingpatterns_counter + 1; id -let rewrite_defs_mapping_patterns env = +let rewrite_ast_mapping_patterns env = let rec rewrite_pat env (pat, guards, expr) = let guards_ref = ref guards in let expr_ref = ref expr in @@ -3302,7 +3302,7 @@ let rewrite_lit_ocaml (L_aux (lit, _)) = match lit with | L_num _ | L_string _ | L_hex _ | L_bin _ | L_real _ | L_unit -> false | _ -> true -let rewrite_defs_pat_lits rewrite_lit env ast = +let rewrite_ast_pat_lits rewrite_lit env ast = let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) = let guards = ref [] in let counter = ref 0 in @@ -3352,7 +3352,7 @@ let rewrite_defs_pat_lits rewrite_lit env ast = in let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in - let Defs defs = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in + let Defs defs = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in Defs (List.map rewrite_def defs) @@ -3403,7 +3403,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let typ' = typ_of exp in add_e_cast (env_of exp) typ' (E_aux (expaux, swaptyp typ' annot)) | _ -> - (* after rewrite_defs_letbind_effects there cannot be terms that have + (* after rewrite_ast_letbind_effects there cannot be terms that have effects/update local variables in "tail-position": check n_exp_term and where it is used. *) if overwrite then @@ -3525,7 +3525,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = else let e1 = rewrite_var_updates (add_vars overwrite e1 vars) in let e2 = rewrite_var_updates (add_vars overwrite e2 vars) in - (* after rewrite_defs_letbind_effects c has no variable updates *) + (* after rewrite_ast_letbind_effects c has no variable updates *) let env = env_of_annot annot in let typ = typ_of e1 in let eff = union_eff_exps [c;e1;e2] in @@ -3534,7 +3534,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | E_case (e1,ps) | E_try (e1, ps) -> let is_case = match expaux with E_case _ -> true | _ -> false in let vars, varpats = - (* for E_case, e1 needs no rewriting after rewrite_defs_letbind_effects *) + (* for E_case, e1 needs no rewriting after rewrite_ast_letbind_effects *) ((if is_case then [] else [e1]) @ List.map (fun (Pat_aux ((Pat_exp (_,e)|Pat_when (_,_,e)),_)) -> e) ps) |> List.map find_updated_vars @@ -3601,7 +3601,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = Same_vars (E_aux (E_cast (typ, exp'), annot)) end | _ -> - (* after rewrite_defs_letbind_effects this expression is pure and updates + (* after rewrite_ast_letbind_effects this expression is pure and updates no variables: check n_exp_term and where it's used. *) Same_vars (E_aux (expaux,annot)) in @@ -3673,7 +3673,7 @@ let remove_reference_types exp = -let rewrite_defs_remove_superfluous_letbinds env = +let rewrite_ast_remove_superfluous_letbinds env = let e_aux (exp,annot) = match exp with | E_let (LB_aux (LB_val (pat, exp1), _), exp2) @@ -3708,18 +3708,18 @@ let rewrite_defs_remove_superfluous_letbinds env = | _ -> E_aux (exp,annot) in let alg = { id_exp_alg with e_aux = e_aux } in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } (* FIXME: We shouldn't allow nested not-patterns *) -let rewrite_defs_not_pats env = +let rewrite_ast_not_pats env = let rewrite_pexp (pexp_aux, annot) = let rewrite_pexp' pat exp orig_guard = let guards = ref [] in @@ -3766,9 +3766,9 @@ let rewrite_defs_not_pats env = rewrite_pexp' pat exp (Some (strip_exp guard)) in let rw_exp = { id_exp_alg with pat_aux = rewrite_pexp } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) } + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) } -let rewrite_defs_remove_superfluous_returns env = +let rewrite_ast_remove_superfluous_returns env = let add_opt_cast typopt1 typopt2 annot exp = match typopt1, typopt2 with @@ -3810,18 +3810,18 @@ let rewrite_defs_remove_superfluous_returns env = | _ -> E_aux (exp,annot) in let alg = { id_exp_alg with e_aux = e_aux } in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } -let rewrite_defs_remove_e_assign env (Defs defs) = +let rewrite_ast_remove_e_assign env (Defs defs) = let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs [("foreach#", "forall ('vars_in 'vars_out : Type). (int, int, int, bool, 'vars_in, 'vars_out) -> 'vars_out"); ("while#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out"); @@ -3830,14 +3830,14 @@ let rewrite_defs_remove_e_assign env (Defs defs) = ("until#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out")]))) in let rewrite_exp _ e = replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = rewrite_exp ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } (Defs (loop_specs @ defs)) let merge_funcls env (Defs defs) = @@ -3899,7 +3899,7 @@ and pat_of_mpat (MP_aux (mpat, annot)) = | MP_typ (mpat, typ) -> P_aux (P_typ (typ, pat_of_mpat mpat), annot) | MP_as (mpat, id) -> P_aux (P_as (pat_of_mpat mpat, id), annot) -let rewrite_defs_realise_mappings _ (Defs defs) = +let rewrite_ast_realise_mappings _ (Defs defs) = let realise_mpexps forwards mpexp1 mpexp2 = let mpexp_pat, mpexp_exp = if forwards then mpexp1, mpexp2 @@ -4112,7 +4112,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) = [] end in - let has_def id = IdSet.mem id (ids_of_defs (Defs defs)) in + let has_def id = IdSet.mem id (ids_of_ast (Defs defs)) in (if has_def forwards_id then [] else forwards_fun) @ (if has_def backwards_id then [] else backwards_fun) @@ -4483,14 +4483,14 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) = let rewrite env = let alg = { id_exp_alg with e_aux = rewrite_case } in - rewrite_defs_base + rewrite_ast_base { rewrite_exp = (fun _ -> fold_exp alg) ; rewrite_pat = rewrite_pat ; rewrite_let = rewrite_let ; rewrite_lexp = rewrite_lexp ; rewrite_fun = rewrite_fun ; rewrite_def = rewrite_def - ; rewrite_defs = rewrite_defs_base + ; rewrite_ast = rewrite_ast_base } @@ -4722,7 +4722,7 @@ let rewrite_loops_with_escape_effect env defs = in E_aux (E_loop (l,m,guard,body),ann) | _ -> exp in - rewrite_defs_base { rewriters_base with rewrite_exp } defs + rewrite_ast_base { rewriters_base with rewrite_exp } defs let recheck_defs env defs = Type_error.check initial_env defs let recheck_defs_without_effects env defs = @@ -4853,7 +4853,7 @@ let rewrite_truncate_hex_literals _type_env defs = E_aux (E_lit (L_aux (L_bin truncation, l_ann)), annot) | _ -> E_aux (e, annot) in - rewrite_defs_base + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_aux = rewrite_aux }) } defs @@ -4910,8 +4910,8 @@ let if_flag_env flag f env defs = if !flag then f env defs else defs, env type rewriter = - | Basic_rewriter of (Env.t -> tannot defs -> tannot defs) - | Checking_rewriter of (Env.t -> tannot defs -> tannot defs * Env.t) + | Basic_rewriter of (Env.t -> tannot ast -> tannot ast) + | Checking_rewriter of (Env.t -> tannot ast -> tannot ast * Env.t) | Bool_rewriter of (bool -> rewriter) | String_rewriter of (string -> rewriter) | Literal_rewriter of ((lit -> bool) -> rewriter) @@ -4957,11 +4957,11 @@ let all_rewrites = [ ("recheck_defs", Checking_rewriter recheck_defs); ("recheck_defs_without_effects", Checking_rewriter recheck_defs_without_effects); ("optimize_recheck_defs", Basic_rewriter (fun _ -> Optimize.recheck)); - ("realise_mappings", Basic_rewriter rewrite_defs_realise_mappings); + ("realise_mappings", Basic_rewriter rewrite_ast_realise_mappings); ("remove_duplicate_valspecs", Basic_rewriter remove_duplicate_valspecs); - ("toplevel_string_append", Basic_rewriter rewrite_defs_toplevel_string_append); - ("pat_string_append", Basic_rewriter rewrite_defs_pat_string_append); - ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns); + ("toplevel_string_append", Basic_rewriter rewrite_ast_toplevel_string_append); + ("pat_string_append", Basic_rewriter rewrite_ast_pat_string_append); + ("mapping_builtins", Basic_rewriter rewrite_ast_mapping_patterns); ("truncate_hex_literals", Basic_rewriter rewrite_truncate_hex_literals); ("mono_rewrites", Basic_rewriter mono_rewrites); ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps); @@ -4970,31 +4970,31 @@ let all_rewrites = [ ("atoms_to_singletons", String_rewriter (fun target -> (Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons target)))); ("add_bitvector_casts", Basic_rewriter Monomorphise.add_bitvector_casts); ("remove_impossible_int_cases", Basic_rewriter Constant_propagation.remove_impossible_int_cases); - ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_defs target))); + ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_ast target))); ("make_cases_exhaustive", Basic_rewriter MakeExhaustive.rewrite); ("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b))); - ("vector_string_pats_to_bit_list", Basic_rewriter rewrite_defs_vector_string_pats_to_bit_list); - ("remove_not_pats", Basic_rewriter rewrite_defs_not_pats); - ("pattern_literals", Literal_rewriter (fun f -> Basic_rewriter (rewrite_defs_pat_lits f))); + ("vector_string_pats_to_bit_list", Basic_rewriter rewrite_ast_vector_string_pats_to_bit_list); + ("remove_not_pats", Basic_rewriter rewrite_ast_not_pats); + ("pattern_literals", Literal_rewriter (fun f -> Basic_rewriter (rewrite_ast_pat_lits f))); ("vector_concat_assignments", Basic_rewriter rewrite_vector_concat_assignments); ("tuple_assignments", Basic_rewriter rewrite_tuple_assignments); ("simple_assignments", Basic_rewriter (rewrite_simple_assignments false)); ("simple_struct_assignments", Basic_rewriter (rewrite_simple_assignments true)); - ("remove_vector_concat", Basic_rewriter rewrite_defs_remove_vector_concat); - ("remove_bitvector_pats", Basic_rewriter rewrite_defs_remove_bitvector_pats); - ("remove_numeral_pats", Basic_rewriter rewrite_defs_remove_numeral_pats); - ("guarded_pats", Basic_rewriter rewrite_defs_guarded_pats); + ("remove_vector_concat", Basic_rewriter rewrite_ast_remove_vector_concat); + ("remove_bitvector_pats", Basic_rewriter rewrite_ast_remove_bitvector_pats); + ("remove_numeral_pats", Basic_rewriter rewrite_ast_remove_numeral_pats); + ("guarded_pats", Basic_rewriter rewrite_ast_guarded_pats); ("bit_lists_to_lits", Basic_rewriter rewrite_bit_lists_to_lits); - ("exp_lift_assign", Basic_rewriter rewrite_defs_exp_lift_assign); - ("early_return", Basic_rewriter rewrite_defs_early_return); - ("nexp_ids", Basic_rewriter rewrite_defs_nexp_ids); + ("exp_lift_assign", Basic_rewriter rewrite_ast_exp_lift_assign); + ("early_return", Basic_rewriter rewrite_ast_early_return); + ("nexp_ids", Basic_rewriter rewrite_ast_nexp_ids); ("fix_val_specs", Basic_rewriter rewrite_fix_val_specs); - ("remove_blocks", Basic_rewriter rewrite_defs_remove_blocks); - ("letbind_effects", Basic_rewriter rewrite_defs_letbind_effects); - ("remove_e_assign", Basic_rewriter rewrite_defs_remove_e_assign); - ("internal_lets", Basic_rewriter rewrite_defs_internal_lets); - ("remove_superfluous_letbinds", Basic_rewriter rewrite_defs_remove_superfluous_letbinds); - ("remove_superfluous_returns", Basic_rewriter rewrite_defs_remove_superfluous_returns); + ("remove_blocks", Basic_rewriter rewrite_ast_remove_blocks); + ("letbind_effects", Basic_rewriter rewrite_ast_letbind_effects); + ("remove_e_assign", Basic_rewriter rewrite_ast_remove_e_assign); + ("internal_lets", Basic_rewriter rewrite_ast_internal_lets); + ("remove_superfluous_letbinds", Basic_rewriter rewrite_ast_remove_superfluous_letbinds); + ("remove_superfluous_returns", Basic_rewriter rewrite_ast_remove_superfluous_returns); ("merge_function_clauses", Basic_rewriter merge_funcls); ("minimise_recursive_functions", Basic_rewriter minimise_recursive_functions); ("move_termination_measures", Basic_rewriter move_termination_measures); @@ -5084,7 +5084,7 @@ let rewrites_coq = [ ("minimise_recursive_functions", []); ("recheck_defs", []); ("exp_lift_assign", []); - (* ("remove_assert", rewrite_defs_remove_assert); *) + (* ("remove_assert", rewrite_ast_remove_assert); *) ("move_termination_measures", []); ("top_sort_defs", []); ("early_return", []); @@ -5189,7 +5189,7 @@ let rewrites_target tgt = | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Invalid target for rewriting: " ^ tgt)) -let rewrite_defs_target tgt = +let rewrite_ast_target tgt = List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) (rewrites_target tgt) let rewrite_check_annot = @@ -5216,9 +5216,9 @@ let rewrite_check_annot = let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> check_annot (E_aux (exp, annot))); pat_alg = { id_pat_alg with p_aux = (fun (pat, annot) -> check_pat (P_aux (pat, annot))) } } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); rewrite_pat = (fun _ -> check_pat) } -let rewrite_defs_check = [ +let rewrite_ast_check = [ ("check_annotations", fun env defs -> rewrite_check_annot defs, env); ] diff --git a/src/rewrites.mli b/src/rewrites.mli index 4212993e..91a3536c 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -65,17 +65,17 @@ val opt_dmono_continue : bool ref val fresh_id : string -> l -> id (* Move loop termination measures into loop AST nodes *) -val move_loop_measures : 'a defs -> 'a defs +val move_loop_measures : 'a ast -> 'a ast (* Re-write undefined to functions created by -undefined_gen flag *) -val rewrite_undefined : bool -> Env.t -> tannot defs -> tannot defs +val rewrite_undefined : bool -> Env.t -> tannot ast -> tannot ast (* Perform rewrites to create an AST supported for a specific target *) -val rewrite_defs_target : string -> (string * (Env.t -> tannot defs -> tannot defs * Env.t)) list +val rewrite_ast_target : string -> (string * (Env.t -> tannot ast -> tannot ast * Env.t)) list type rewriter = - | Basic_rewriter of (Env.t -> tannot defs -> tannot defs) - | Checking_rewriter of (Env.t -> tannot defs -> tannot defs * Env.t) + | Basic_rewriter of (Env.t -> tannot ast -> tannot ast) + | Checking_rewriter of (Env.t -> tannot ast -> tannot ast * Env.t) | Bool_rewriter of (bool -> rewriter) | String_rewriter of (string -> rewriter) | Literal_rewriter of ((lit -> bool) -> rewriter) @@ -99,6 +99,6 @@ val opt_coq_warn_nonexhaustive : bool ref (* This is a special rewriter pass that checks AST invariants without actually doing any re-writing *) -val rewrite_defs_check : (string * (Env.t -> tannot defs -> tannot defs * Env.t)) list +val rewrite_ast_check : (string * (Env.t -> tannot ast -> tannot ast * Env.t)) list val simple_typ : typ -> typ diff --git a/src/sail.ml b/src/sail.ml index 53a5cc5d..0e9b8e27 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -481,7 +481,7 @@ let target name out_name ast type_envs = 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_defs_annot remove_prover ast, Type_check.Env.set_prover None type_envs) [Marshal.Compat_32] + 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 diff --git a/src/slice.mli b/src/slice.mli index 58d2cf17..ffc6f3bd 100644 --- a/src/slice.mli +++ b/src/slice.mli @@ -65,8 +65,8 @@ module Node : sig val compare : node -> node -> int end -val graph_of_ast : Type_check.tannot defs -> Graph.Make(Node).graph +val graph_of_ast : Type_check.tannot ast -> Graph.Make(Node).graph -val dot_of_ast : out_channel -> Type_check.tannot defs -> unit +val dot_of_ast : out_channel -> Type_check.tannot ast -> unit -val filter_ast : Set.Make(Node).t -> Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs +val filter_ast : Set.Make(Node).t -> Graph.Make(Node).graph -> Type_check.tannot ast -> Type_check.tannot ast diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index a2ed74bf..b111f6f0 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -77,7 +77,7 @@ val is_within_machine64 : typ -> nexp_range list -> triple *) (* produce a new ordering for defs, limiting to those listed in the list, which respects dependencies *) (* val restrict_defs : 'a defs -> string list -> 'a defs *) -val top_sort_defs : tannot defs -> tannot defs +val top_sort_defs : tannot ast -> tannot ast (** Return the set of mutable variables assigned to in the given AST. *) val assigned_vars : 'a exp -> IdSet.t diff --git a/src/specialize.ml b/src/specialize.ml index b703d27a..3634b7bc 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -253,8 +253,8 @@ let rec instantiations_of spec id ast = let rewrite_pat = { id_pat_alg with p_aux = (fun (pat, annot) -> inspect_pat (P_aux (pat, annot))) } in let rewrite_exp = { id_exp_alg with pat_alg = rewrite_pat; e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in - let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); - rewrite_pat = (fun _ -> fold_pat rewrite_pat)} ast in + let _ = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp); + rewrite_pat = (fun _ -> fold_pat rewrite_pat)} ast in !instantiations @@ -279,7 +279,7 @@ let rec rewrite_polymorphic_calls spec id ast = in let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = match typ_aux with @@ -368,7 +368,7 @@ let instantiate_constraints instantiation ncs = List.map (fun c -> List.fold_left (fun c (v, a) -> constraint_subst v a c) c (KBindings.bindings instantiation)) ncs let specialize_id_valspec spec instantiations id ast = - match split_defs (is_valspec id) ast with + match split_ast (is_valspec id) ast with | None -> Reporting.unreachable (id_loc id) __POS__ ("Valspec " ^ string_of_id id ^ " does not exist!") | Some (pre_ast, vs, post_ast) -> let typschm, externs, is_cast, annot = match vs with @@ -450,7 +450,7 @@ let specialize_annotations instantiation fdef = annot) let specialize_id_fundef instantiations id ast = - match split_defs (is_fundef id) ast with + match split_ast (is_fundef id) ast with | None -> ast | Some (pre_ast, DEF_fundef fundef, post_ast) -> let spec_ids = ref IdSet.empty in @@ -511,7 +511,7 @@ let remove_unused_valspecs env ast = in let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in - let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast in + let _ = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast in let unused = IdSet.filter (fun vs_id -> not (IdSet.mem vs_id !calls)) vs_ids in diff --git a/src/specialize.mli b/src/specialize.mli index ae71bfcb..0d522189 100644 --- a/src/specialize.mli +++ b/src/specialize.mli @@ -73,7 +73,7 @@ val int_specialization_with_externs : specialization argument specifies what X should be - it should be one of: [is_int_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util], or some combination of those. *) -val polymorphic_functions : specialization -> 'a defs -> IdSet.t +val polymorphic_functions : specialization -> 'a ast -> IdSet.t val add_initial_calls : IdSet.t -> unit @@ -82,14 +82,14 @@ val add_initial_calls : IdSet.t -> unit AST with [Type_check.initial_env]. The env parameter is the environment to return if there is no polymorphism to remove, in which case specialize returns the AST unmodified. *) -val specialize : specialization -> Env.t -> tannot defs -> tannot defs * Env.t +val specialize : specialization -> Env.t -> tannot ast -> tannot ast * Env.t (** specialize' n performs at most n specialization passes. Useful for int_specialization which is not guaranteed to terminate. *) -val specialize_passes : int -> specialization -> Env.t -> tannot defs -> tannot defs * Env.t +val specialize_passes : int -> specialization -> Env.t -> tannot ast -> tannot ast * Env.t (** return all instantiations of a function id, with the instantiations filtered according to the specialization. *) -val instantiations_of : specialization -> id -> tannot defs -> typ_arg KBindings.t list +val instantiations_of : specialization -> id -> tannot ast -> typ_arg KBindings.t list val string_of_instantiation : typ_arg KBindings.t -> string diff --git a/src/splice.ml b/src/splice.ml index 6198a4c7..cb3307d9 100644 --- a/src/splice.ml +++ b/src/splice.ml @@ -46,7 +46,7 @@ let splice ast file = let parsed_ast = Process_file.parse_file file |> snd in let repl_ast = Initial_check.process_ast ~generate:false (Parse_ast.Defs [(file, parsed_ast)]) in let repl_ast = Rewrites.move_loop_measures repl_ast in - let repl_ast = map_defs_annot (fun (l,_) -> l,Type_check.empty_tannot) repl_ast in + let repl_ast = map_ast_annot (fun (l,_) -> l,Type_check.empty_tannot) repl_ast in let repl_ids, repl_specs = scan_defs repl_ast in let defs1, specs_found = filter_old_ast repl_ids repl_specs ast in let defs2 = filter_replacements specs_found repl_ast in diff --git a/src/state.ml b/src/state.ml index a598be92..3491afd3 100644 --- a/src/state.ml +++ b/src/state.ml @@ -63,7 +63,7 @@ let opt_type_grouped_regstate = ref false let defs_of_string = ast_of_def_string -let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs)) +let is_defined defs name = IdSet.mem (mk_id name) (ids_of_ast (Defs defs)) let has_default_order defs = List.exists (function DEF_default (DT_aux (DT_order _, _)) -> true | _ -> false) defs @@ -375,7 +375,7 @@ let register_refs_lem mwords registers = (* TODO Generate well-typedness predicate for register states (and events), asserting that all lists representing non-bit-vectors have the right length. *) -let generate_isa_lemmas mwords (Defs defs : tannot defs) = +let generate_isa_lemmas mwords (Defs defs : tannot ast) = let rec drop_while f = function | x :: xs when f x -> drop_while f xs | xs -> xs diff --git a/src/type_check.ml b/src/type_check.ml index afe24bc6..ab860a79 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -5420,7 +5420,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should have been rewritten before type checking" -and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t = +and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot ast * Env.t = fun n total env defs -> match defs with | [] -> Defs [], env @@ -5430,7 +5430,7 @@ and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t = let Defs defs, env = check_defs (n + 1) total env defs in Defs (def @ defs), env -and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = +and check : 'a. Env.t -> 'a ast -> tannot ast * Env.t = fun env (Defs defs) -> let total = List.length defs in check_defs 1 total env defs and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list = diff --git a/src/type_check.mli b/src/type_check.mli index 9c2cd236..74ad4441 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -480,7 +480,7 @@ Some invariants that will hold of a fully checked AST are: check throws type_errors rather than Sail generic errors from Reporting. For a function that uses generic errors, use Type_error.check *) -val check : Env.t -> 'a defs -> tannot defs * Env.t +val check : Env.t -> 'a ast -> tannot ast * Env.t (** The same as [check], but exposes the intermediate type-checking environments so we don't have to always re-check the entire AST *) diff --git a/src/type_error.ml b/src/type_error.ml index 3ae06c31..4faa774a 100644 --- a/src/type_error.ml +++ b/src/type_error.ml @@ -186,7 +186,7 @@ let rec collapse_errors = function Err_because (err1, l, err2) | err -> err -let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = +let check : 'a. Env.t -> 'a ast -> tannot ast * Env.t = fun env defs -> try Type_check.check env defs with | Type_error (env, l, err) -> -- cgit v1.2.3