diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CfimAst.ml | 8 | ||||
| -rw-r--r-- | src/CfimAstUtils.ml | 14 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 34 | ||||
| -rw-r--r-- | src/Contexts.ml | 18 | ||||
| -rw-r--r-- | src/Expressions.ml | 4 | ||||
| -rw-r--r-- | src/ExtractAst.ml | 2 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 46 | ||||
| -rw-r--r-- | src/Interpreter.ml | 34 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 10 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 8 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 10 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 16 | ||||
| -rw-r--r-- | src/Invariants.ml | 8 | ||||
| -rw-r--r-- | src/Modules.ml | 29 | ||||
| -rw-r--r-- | src/PrePasses.ml | 2 | ||||
| -rw-r--r-- | src/Print.ml | 161 | ||||
| -rw-r--r-- | src/PrintPure.ml | 68 | ||||
| -rw-r--r-- | src/PrintSymbolicAst.ml | 12 | ||||
| -rw-r--r-- | src/Pure.ml | 18 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 46 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 44 | ||||
| -rw-r--r-- | src/PureUtils.ml | 24 | ||||
| -rw-r--r-- | src/Substitute.ml | 26 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 84 | ||||
| -rw-r--r-- | src/Translate.ml | 86 | ||||
| -rw-r--r-- | src/TranslateCore.ml | 38 | ||||
| -rw-r--r-- | src/Types.ml | 12 | ||||
| -rw-r--r-- | src/TypesAnalysis.ml | 50 | ||||
| -rw-r--r-- | src/TypesUtils.ml | 10 |
29 files changed, 463 insertions, 459 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index ab7bcb4a..279430df 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -3,7 +3,7 @@ open Types open Values open Expressions -module FunDefId = IdGen () +module FunDeclId = IdGen () type var = { index : VarId.id; (** Unique variable identifier *) @@ -32,7 +32,7 @@ type assumed_fun_id = (** `core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>` *) [@@deriving show, ord] -type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id +type fun_id = Local of FunDeclId.id | Assumed of assumed_fun_id [@@deriving show, ord] type assertion = { cond : operand; expected : bool } [@@deriving show] @@ -169,8 +169,8 @@ and switch_targets = concrete = true; }] -type fun_def = { - def_id : FunDefId.id; +type fun_decl = { + def_id : FunDeclId.id; name : fun_name; signature : fun_sig; arg_count : int; diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml index 04d3e6b0..c694d61b 100644 --- a/src/CfimAstUtils.ml +++ b/src/CfimAstUtils.ml @@ -16,19 +16,19 @@ let statement_has_loops (st : statement) : bool = false with Found -> true -(** Check if a [fun_def] contains loops *) -let fun_def_has_loops (fd : fun_def) : bool = statement_has_loops fd.body +(** Check if a [fun_decl] contains loops *) +let fun_decl_has_loops (fd : fun_decl) : bool = statement_has_loops fd.body -let lookup_fun_sig (fun_id : fun_id) (fun_defs : fun_def FunDefId.Map.t) : +let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = match fun_id with - | Local id -> (FunDefId.Map.find id fun_defs).signature + | Local id -> (FunDeclId.Map.find id fun_decls).signature | Assumed aid -> Assumed.get_assumed_sig aid -let lookup_fun_name (fun_id : fun_id) (fun_defs : fun_def FunDefId.Map.t) : +let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : Identifiers.fun_name = match fun_id with - | Local id -> (FunDefId.Map.find id fun_defs).name + | Local id -> (FunDeclId.Map.find id fun_decls).name | Assumed aid -> Assumed.get_assumed_name aid (** Small utility: list the transitive parents of a region var group. @@ -64,6 +64,6 @@ let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in parents -let fun_def_get_input_vars (fdef : fun_def) : var list = +let fun_decl_get_input_vars (fdef : fun_decl) : var list = let locals = List.tl fdef.locals in Collections.List.prefix fdef.arg_count locals diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 4c7fc58b..e78b157a 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -102,7 +102,7 @@ let type_id_of_json (js : json) : (T.type_id, string) result = combine_error_msgs js "type_id_of_json" (match js with | `Assoc [ ("Adt", id) ] -> - let* id = T.TypeDefId.id_of_json id in + let* id = T.TypeDeclId.id_of_json id in Ok (T.AdtId id) | `String "Tuple" -> Ok T.Tuple | `Assoc [ ("Assumed", aty) ] -> @@ -168,8 +168,8 @@ let variant_of_json (js : json) : (T.variant, string) result = Ok { T.variant_name = name; fields } | _ -> Error "") -let type_def_kind_of_json (js : json) : (T.type_def_kind, string) result = - combine_error_msgs js "type_def_kind_of_json" +let type_decl_kind_of_json (js : json) : (T.type_decl_kind, string) result = + combine_error_msgs js "type_decl_kind_of_json" (match js with | `Assoc [ ("Struct", fields) ] -> let* fields = list_of_json field_of_json fields in @@ -194,8 +194,8 @@ let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result combine_error_msgs js "region_var_group_of_json" (list_of_json region_var_group_of_json js) -let type_def_of_json (js : json) : (T.type_def, string) result = - combine_error_msgs js "type_def_of_json" +let type_decl_of_json (js : json) : (T.type_decl, string) result = + combine_error_msgs js "type_decl_of_json" (match js with | `Assoc [ @@ -206,11 +206,11 @@ let type_def_of_json (js : json) : (T.type_def, string) result = ("regions_hierarchy", regions_hierarchy); ("kind", kind); ] -> - let* def_id = T.TypeDefId.id_of_json def_id in + let* def_id = T.TypeDeclId.id_of_json def_id in let* name = name_of_json name in let* region_params = list_of_json region_var_of_json region_params in let* type_params = list_of_json type_var_of_json type_params in - let* kind = type_def_kind_of_json kind in + let* kind = type_decl_kind_of_json kind in let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in Ok { @@ -317,7 +317,7 @@ let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result = combine_error_msgs js "field_proj_kind_of_json" (match js with | `Assoc [ ("ProjAdt", `List [ def_id; opt_variant_id ]) ] -> - let* def_id = T.TypeDefId.id_of_json def_id in + let* def_id = T.TypeDeclId.id_of_json def_id in let* opt_variant_id = option_of_json T.VariantId.id_of_json opt_variant_id in @@ -423,7 +423,7 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result = | `String "AggregatedTuple" -> Ok E.AggregatedTuple | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ] -> - let* id = T.TypeDefId.id_of_json id in + let* id = T.TypeDeclId.id_of_json id in let* opt_variant_id = option_of_json T.VariantId.id_of_json opt_variant_id in @@ -479,7 +479,7 @@ let fun_id_of_json (js : json) : (A.fun_id, string) result = combine_error_msgs js "fun_id_of_json" (match js with | `Assoc [ ("Local", id) ] -> - let* id = A.FunDefId.id_of_json id in + let* id = A.FunDeclId.id_of_json id in Ok (A.Local id) | `Assoc [ ("Assumed", fid) ] -> let* fid = assumed_fun_id_of_json fid in @@ -606,8 +606,8 @@ and switch_targets_of_json (js : json) : (A.switch_targets, string) result = Ok (A.SwitchInt (int_ty, tgts, otherwise)) | _ -> Error "") -let fun_def_of_json (js : json) : (A.fun_def, string) result = - combine_error_msgs js "fun_def_of_json" +let fun_decl_of_json (js : json) : (A.fun_decl, string) result = + combine_error_msgs js "fun_decl_of_json" (match js with | `Assoc [ @@ -618,7 +618,7 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result = ("locals", locals); ("body", body); ] -> - let* def_id = A.FunDefId.id_of_json def_id in + let* def_id = A.FunDeclId.id_of_json def_id in let* name = fun_name_of_json name in let* signature = fun_sig_of_json signature in let* arg_count = int_of_json arg_count in @@ -642,12 +642,12 @@ let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) let type_declaration_group_of_json (js : json) : (M.type_declaration_group, string) result = combine_error_msgs js "type_declaration_group_of_json" - (g_declaration_group_of_json T.TypeDefId.id_of_json js) + (g_declaration_group_of_json T.TypeDeclId.id_of_json js) let fun_declaration_group_of_json (js : json) : (M.fun_declaration_group, string) result = combine_error_msgs js "fun_declaration_group_of_json" - (g_declaration_group_of_json A.FunDefId.id_of_json js) + (g_declaration_group_of_json A.FunDeclId.id_of_json js) let declaration_group_of_json (js : json) : (M.declaration_group, string) result = @@ -675,7 +675,7 @@ let cfim_module_of_json (js : json) : (M.cfim_module, string) result = let* declarations = list_of_json declaration_group_of_json declarations in - let* types = list_of_json type_def_of_json types in - let* functions = list_of_json fun_def_of_json functions in + let* types = list_of_json type_decl_of_json types in + let* functions = list_of_json fun_decl_of_json functions in Ok { M.name; declarations; types; functions } | _ -> Error "") diff --git a/src/Contexts.ml b/src/Contexts.ml index 97584639..b5431f0f 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -200,13 +200,13 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) : } type type_context = { - type_defs_groups : M.type_declaration_group TypeDefId.Map.t; - type_defs : type_def TypeDefId.Map.t; + type_decls_groups : M.type_declaration_group TypeDeclId.Map.t; + type_decls : type_decl TypeDeclId.Map.t; type_infos : TypesAnalysis.type_infos; } [@@deriving show] -type fun_context = { fun_defs : fun_def FunDefId.Map.t } [@@deriving show] +type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show] type eval_ctx = { type_context : type_context; @@ -237,12 +237,12 @@ let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder = lookup ctx.env (** TODO: make this more efficient with maps *) -let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def = - TypeDefId.Map.find tid ctx.type_context.type_defs +let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl = + TypeDeclId.Map.find tid ctx.type_context.type_decls (** TODO: make this more efficient with maps *) -let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def = - FunDefId.Map.find fid ctx.fun_context.fun_defs +let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl = + FunDeclId.Map.find fid ctx.fun_context.fun_decls (** Retrieve a variable's value in an environment *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = @@ -370,8 +370,8 @@ let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs = let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs = env_lookup_abs ctx.env abs_id -let ctx_type_def_is_rec (ctx : eval_ctx) (id : TypeDefId.id) : bool = - let decl_group = TypeDefId.Map.find id ctx.type_context.type_defs_groups in +let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool = + let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in match decl_group with M.Rec _ -> true | M.NonRec _ -> false (** Visitor to iterate over the values in the *current* frame *) diff --git a/src/Expressions.ml b/src/Expressions.ml index 199184ed..a118ca67 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -2,7 +2,7 @@ open Types open Values type field_proj_kind = - | ProjAdt of TypeDefId.id * VariantId.id option + | ProjAdt of TypeDeclId.id * VariantId.id option | ProjOption of VariantId.id (** Option is an assumed type, coming from the standard library *) | ProjTuple of int @@ -119,7 +119,7 @@ type operand = type aggregate_kind = | AggregatedTuple | AggregatedAdt of - TypeDefId.id * VariantId.id option * erased_region list * ety list + TypeDeclId.id * VariantId.id option * erased_region list * ety list [@@deriving show] (* TODO: move the aggregate kind to operands *) diff --git a/src/ExtractAst.ml b/src/ExtractAst.ml index da88dc04..dd793291 100644 --- a/src/ExtractAst.ml +++ b/src/ExtractAst.ml @@ -45,7 +45,7 @@ type term = Otherwise, we can use `App` (with the record constructor). *) -type fun_def = { +type fun_decl = { name : string; inputs : pattern list; (** We can match over the inputs, hence the use of [pattern]. In practice, diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index c4323090..d8d14ddf 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -13,13 +13,13 @@ module F = Format Controls whether we should use `type ...` or `and ...` (for mutually recursive datatypes). *) -type type_def_qualif = Type | And +type type_decl_qualif = Type | And (** A qualifier for function definitions. Controls whether we should use `let ...`, `let rec ...` or `and ...` *) -type fun_def_qualif = Let | LetRec | And +type fun_decl_qualif = Let | LetRec | And (** Small helper to compute the name of an int type *) let fstar_int_name (int_ty : integer_type) = @@ -275,7 +275,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : fname ^ suffix in - let decreases_clause_name (_fid : FunDefId.id) (fname : fun_name) : string = + let decreases_clause_name (_fid : FunDeclId.id) (fname : fun_name) : string = let fname = get_fun_name fname in (* Converting to snake case should be a no-op, but it doesn't cost much *) let fname = to_snake_case fname in @@ -306,7 +306,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : | Assumed State -> "st" | AdtId adt_id -> let def = - TypeDefId.Map.find adt_id ctx.type_context.type_defs + TypeDeclId.Map.find adt_id ctx.type_context.type_decls in (* We do the following: * - convert to snake_case @@ -424,10 +424,10 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) We need to do this preemptively, beforce extracting any definition, because of recursive definitions. *) -let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) : +let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : extraction_ctx = (* Compute and register the type def name *) - let ctx = ctx_add_type_def def ctx in + let ctx = ctx_add_type_decl def ctx in (* Compute and register: * - the variant names, if this is an enumeration * - the field names, if this is a structure @@ -451,8 +451,8 @@ let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) : (* Return *) ctx -let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter) - (def : type_def) (fields : field list) : unit = +let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) + (def : type_decl) (fields : field list) : unit = (* We want to generate a definition which looks like this: * ``` * type t = { x : int; y : bool; } @@ -509,8 +509,8 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt "}") -let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter) - (def : type_def) (def_name : string) (type_params : string list) +let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter) + (def : type_decl) (def_name : string) (type_params : string list) (variants : variant list) : unit = (* We want to generate a definition which looks like this: * ``` @@ -614,8 +614,8 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter) Note that all the names used for extraction should already have been registered. *) -let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : type_def_qualif) (def : type_def) : unit = +let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) + (qualif : type_decl_qualif) (def : type_decl) : unit = (* Retrieve the definition name *) let def_name = ctx_get_local_type def.def_id ctx in (* Add the type params - note that we need those bindings only for the @@ -653,9 +653,9 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *) F.pp_close_box fmt (); (match def.kind with - | Struct fields -> extract_type_def_struct_body ctx_body fmt def fields + | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields | Enum variants -> - extract_type_def_enum_body ctx_body fmt def def_name type_params variants); + extract_type_decl_enum_body ctx_body fmt def def_name type_params variants); (* Close the box for the definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) @@ -664,7 +664,7 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (** Compute the names for all the pure functions generated from a rust function (forward function and backward functions). *) -let extract_fun_def_register_names (ctx : extraction_ctx) (keep_fwd : bool) +let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) (has_decreases_clause : bool) (def : pure_fun_translation) : extraction_ctx = let fwd, back_ls = def in @@ -673,11 +673,11 @@ let extract_fun_def_register_names (ctx : extraction_ctx) (keep_fwd : bool) if has_decreases_clause then ctx_add_decrases_clause fwd ctx else ctx in (* Register the forward function name *) - let ctx = ctx_add_fun_def (keep_fwd, def) fwd ctx in + let ctx = ctx_add_fun_decl (keep_fwd, def) fwd ctx in (* Register the backward functions' names *) let ctx = List.fold_left - (fun ctx back -> ctx_add_fun_def (keep_fwd, def) back ctx) + (fun ctx back -> ctx_add_fun_decl (keep_fwd, def) back ctx) ctx back_ls in (* Return *) @@ -986,7 +986,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) - the previous context augmented with bindings for the input values *) let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) - (def : fun_def) : extraction_ctx * extraction_ctx = + (def : fun_decl) : extraction_ctx * extraction_ctx = (* Add the type parameters - note that we need those bindings only for the * body translation (they are not top-level) *) let ctx, _ = ctx_add_type_params def.signature.type_params ctx in @@ -1045,7 +1045,7 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) ``` *) let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) - (def : fun_def) : unit = + (def : fun_decl) : unit = (* Retrieve the function name *) let def_name = ctx_get_decreases_clause def.def_id ctx in (* Add a break before *) @@ -1097,9 +1097,9 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) equal to the definition to extract, if we extract a forward function) because it is useful for the decrease clause. *) -let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : fun_def_qualif) (has_decreases_clause : bool) (fwd_def : fun_def) - (def : fun_def) : unit = +let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) + (qualif : fun_decl_qualif) (has_decreases_clause : bool) (fwd_def : fun_decl) + (def : fun_decl) : unit = (* Retrieve the function name *) let def_name = ctx_get_local_function def.def_id def.back_id ctx in (* (* Add the type parameters - note that we need those bindings only for the @@ -1220,7 +1220,7 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter) ``` *) let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) - (def : fun_def) : unit = + (def : fun_decl) : unit = (* We only insert unit tests for forward functions *) assert (def.back_id = None); (* Check if this is a unit function *) diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 91ad6843..d073c238 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -15,16 +15,16 @@ let log = L.interpreter_log let compute_type_fun_contexts (m : M.cfim_module) : C.type_context * C.fun_context = - let type_decls, _ = M.split_declarations m.declarations in - let type_defs, fun_defs = M.compute_defs_maps m in - let type_defs_groups, _funs_defs_groups = + let type_decls_list, _ = M.split_declarations m.declarations in + let type_decls, fun_decls = M.compute_defs_maps m in + let type_decls_groups, _funs_defs_groups = M.split_declarations_to_group_maps m.declarations in let type_infos = - TypesAnalysis.analyze_type_declarations type_defs type_decls + TypesAnalysis.analyze_type_declarations type_decls type_decls_list in - let type_context = { C.type_defs_groups; type_defs; type_infos } in - let fun_context = { C.fun_defs } in + let type_context = { C.type_decls_groups; type_decls; type_infos } in + let fun_context = { C.fun_decls } in (type_context, fun_context) let initialize_eval_context (type_context : C.type_context) @@ -52,7 +52,7 @@ let initialize_eval_context (type_context : C.type_context) - the instantiated function signature *) let initialize_symbolic_context_for_fun (type_context : C.type_context) - (fun_context : C.fun_context) (fdef : A.fun_def) : + (fun_context : C.fun_context) (fdef : A.fun_decl) : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig = (* The abstractions are not initialized the same way as for function * calls: they contain *loan* projectors, because they "provide" us @@ -113,7 +113,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) the synthesis (mostly by ending abstractions). *) let evaluate_function_symbolic_synthesize_backward_from_return - (config : C.config) (fdef : A.fun_def) (inst_sg : A.inst_fun_sig) + (config : C.config) (fdef : A.fun_decl) (inst_sg : A.inst_fun_sig) (back_id : T.RegionGroupId.id) (ctx : C.eval_ctx) : SA.expression option = (* We need to instantiate the function signature - to retrieve * the return type. Note that it is important to re-generate @@ -189,7 +189,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return *) let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) (type_context : C.type_context) (fun_context : C.fun_context) - (fdef : A.fun_def) (back_id : T.RegionGroupId.id option) : + (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) : V.symbolic_value list * SA.expression option = (* Debug *) let name_to_string () = @@ -252,9 +252,9 @@ module Test = struct environment. *) let test_unit_function (config : C.partial_config) (m : M.cfim_module) - (fid : A.FunDefId.id) : unit = + (fid : A.FunDeclId.id) : unit = (* Retrieve the function declaration *) - let fdef = A.FunDefId.nth m.functions fid in + let fdef = A.FunDeclId.nth m.functions fid in (* Debug *) log#ldebug @@ -291,7 +291,7 @@ module Test = struct (** Small helper: return true if the function is a unit function (no parameters, no arguments) - TODO: move *) - let fun_def_is_unit (def : A.fun_def) : bool = + let fun_decl_is_unit (def : A.fun_decl) : bool = def.A.arg_count = 0 && List.length def.A.signature.region_params = 0 && List.length def.A.signature.type_params = 0 @@ -300,8 +300,8 @@ module Test = struct (** Test all the unit functions in a list of function definitions *) let test_unit_functions (config : C.partial_config) (m : M.cfim_module) : unit = - let unit_funs = List.filter fun_def_is_unit m.functions in - let test_unit_fun (def : A.fun_def) : unit = + let unit_funs = List.filter fun_decl_is_unit m.functions in + let test_unit_fun (def : A.fun_decl) : unit = test_unit_function config m def.A.def_id in List.iter test_unit_fun unit_funs @@ -309,7 +309,7 @@ module Test = struct (** Execute the symbolic interpreter on a function. *) let test_function_symbolic (config : C.partial_config) (synthesize : bool) (type_context : C.type_context) (fun_context : C.fun_context) - (fdef : A.fun_def) : unit = + (fdef : A.fun_decl) : unit = (* Debug *) log#ldebug (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name)); @@ -337,10 +337,10 @@ module Test = struct let test_functions_symbolic (config : C.partial_config) (synthesize : bool) (m : M.cfim_module) : unit = let no_loop_funs = - List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) m.functions + List.filter (fun f -> not (CfimAstUtils.fun_decl_has_loops f)) m.functions in let type_context, fun_context = compute_type_fun_contexts m in - let test_fun (def : A.fun_def) : unit = + let test_fun (def : A.fun_decl) : unit = (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 85259b89..979ed780 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -220,16 +220,16 @@ let apply_symbolic_expansion_non_borrow (config : C.config) doesn't allow the expansion of enumerations *containing several variants*. *) let compute_expanded_symbolic_adt_value (expand_enumerations : bool) - (kind : V.sv_kind) (def_id : T.TypeDefId.id) + (kind : V.sv_kind) (def_id : T.TypeDeclId.id) (regions : T.RegionId.id T.region list) (types : T.rty list) (ctx : C.eval_ctx) : V.symbolic_expansion list = (* Lookup the definition and check if it is an enumeration with several * variants *) - let def = C.ctx_lookup_type_def ctx def_id in + let def = C.ctx_lookup_type_decl ctx def_id in assert (List.length regions = List.length def.T.region_params); (* Retrieve, for every variant, the list of its instantiated field types *) let variants_fields_types = - Subst.type_def_get_instantiated_variants_fields_rtypes def regions types + Subst.type_decl_get_instantiated_variants_fields_rtypes def regions types in (* Check if there is strictly more than one variant *) if List.length variants_fields_types > 1 && not expand_enumerations then @@ -677,7 +677,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = (* [expand_symbolic_value_no_branching] checks if there are branchings, * but we prefer to also check it here - this leads to cleaner messages * and debugging *) - let def = C.ctx_lookup_type_def ctx def_id in + let def = C.ctx_lookup_type_decl ctx def_id in (match def.kind with | T.Struct _ | T.Enum ([] | [ _ ]) -> () | T.Enum (_ :: _) -> @@ -688,7 +688,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = [greedy_expand_symbolics_with_borrows] of [config]): " ^ Print.name_to_string def.name))); (* Also, we need to check if the definition is recursive *) - if C.ctx_type_def_is_rec ctx def_id then + if C.ctx_type_decl_is_rec ctx def_id then raise (Failure ("Attempted to greedily expand a recursive definition \ diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 9e4466b8..3043bc7a 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -89,9 +89,9 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) let field_tys = match adt_id with | T.AdtId def_id -> - let def = C.ctx_lookup_type_def ctx def_id in + let def = C.ctx_lookup_type_decl ctx def_id in assert (def.region_params = []); - Subst.type_def_get_instantiated_field_etypes def variant_id + Subst.type_decl_get_instantiated_field_etypes def variant_id type_params | T.Tuple -> type_params | T.Assumed _ -> failwith "Unreachable" @@ -601,8 +601,8 @@ let eval_rvalue_aggregate (config : C.config) cf aggregated ctx | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> (* Sanity checks *) - let type_def = C.ctx_lookup_type_def ctx def_id in - assert (List.length type_def.region_params = List.length regions); + let type_decl = C.ctx_lookup_type_decl ctx def_id in + assert (List.length type_decl.region_params = List.length regions); let expected_field_types = Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id types diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index d8b1322b..826e8563 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -351,18 +351,18 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place) | Ok ctx -> ctx (** Compute an expanded ADT bottom value *) -let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.Map.t) - (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) +let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t) + (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) (regions : T.erased_region list) (types : T.ety list) : V.typed_value = (* Lookup the definition and check if it is an enumeration - it should be an enumeration if and only if the projection element is a field projection with *some* variant id. Retrieve the list of fields at the same time. *) - let def = T.TypeDefId.Map.find def_id tyctx in + let def = T.TypeDeclId.Map.find def_id tyctx in assert (List.length regions = List.length def.T.region_params); (* Compute the field types *) let field_types = - Subst.type_def_get_instantiated_field_etypes def opt_variant_id types + Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types in (* Initialize the expanded value *) let fields = List.map mk_bottom field_types in @@ -444,7 +444,7 @@ let expand_bottom_value_from_projection (config : C.config) | ( Field (ProjAdt (def_id, opt_variant_id), _), T.Adt (T.AdtId def_id', regions, types) ) -> assert (def_id = def_id'); - compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id + compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id opt_variant_id regions types (* Option *) | Field (ProjOption variant_id, _), T.Adt (T.Assumed T.Option, [], [ ty ]) diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index c3b60fa9..dc8fc7f7 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -233,7 +233,7 @@ let set_discriminant (config : C.config) (p : E.place) let bottom_v = match type_id with | T.AdtId def_id -> - compute_expanded_bottom_adt_value ctx.type_context.type_defs + compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id (Some variant_id) regions types | T.Assumed T.Option -> assert (regions = []); @@ -247,7 +247,7 @@ let set_discriminant (config : C.config) (p : E.place) let bottom_v = match type_id with | T.AdtId def_id -> - compute_expanded_bottom_adt_value ctx.type_context.type_defs + compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id (Some variant_id) regions types | T.Assumed T.Option -> assert (regions = []); @@ -997,20 +997,20 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = call.type_params call.args call.dest (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_local_function_call_concrete (config : C.config) (fid : A.FunDefId.id) +and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> assert (region_params = []); (* Retrieve the (correctly instantiated) body *) - let def = C.ctx_lookup_fun_def ctx fid in + let def = C.ctx_lookup_fun_decl ctx fid in let tsubst = Subst.make_type_subst (List.map (fun v -> v.T.index) def.A.signature.type_params) type_params in - let locals, body = Subst.fun_def_substitute_in_body tsubst def in + let locals, body = Subst.fun_decl_substitute_in_body tsubst def in (* Evaluate the input operands *) assert (List.length args = def.A.arg_count); @@ -1063,12 +1063,12 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDefId.id) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDefId.id) +and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Retrieve the (correctly instantiated) signature *) - let def = C.ctx_lookup_fun_def ctx fid in + let def = C.ctx_lookup_fun_decl ctx fid in let sg = def.A.signature in (* Instantiate the signature and introduce fresh abstraction and region ids * while doing so *) @@ -1239,7 +1239,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) -and eval_local_function_call (config : C.config) (fid : A.FunDefId.id) +and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = match config.mode with diff --git a/src/Invariants.ml b/src/Invariants.ml index 0e4b1e23..78d7cb8d 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -410,7 +410,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.Adt av, T.Adt (T.AdtId def_id, regions, tys) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) - let def = C.ctx_lookup_type_def ctx def_id in + let def = C.ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) assert (List.length regions = List.length def.region_params); assert (List.length tys = List.length def.type_params); @@ -422,7 +422,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> failwith "Erroneous typing"); (* Check that the field types are correct *) let field_types = - Subst.type_def_get_instantiated_field_etypes def av.V.variant_id + Subst.type_decl_get_instantiated_field_etypes def av.V.variant_id tys in let fields_with_types = @@ -509,7 +509,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) - let def = C.ctx_lookup_type_def ctx def_id in + let def = C.ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) assert (List.length regions = List.length def.region_params); assert (List.length tys = List.length def.type_params); @@ -521,7 +521,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> failwith "Erroneous typing"); (* Check that the field types are correct *) let field_types = - Subst.type_def_get_instantiated_field_rtypes def av.V.variant_id + Subst.type_decl_get_instantiated_field_rtypes def av.V.variant_id regions tys in let fields_with_types = diff --git a/src/Modules.ml b/src/Modules.ml index 1199d74a..3ee4c9ed 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -4,9 +4,10 @@ open CfimAst type 'id g_declaration_group = NonRec of 'id | Rec of 'id list [@@deriving show] -type type_declaration_group = TypeDefId.id g_declaration_group [@@deriving show] +type type_declaration_group = TypeDeclId.id g_declaration_group +[@@deriving show] -type fun_declaration_group = FunDefId.id g_declaration_group [@@deriving show] +type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] (** Module declaration *) type declaration_group = @@ -17,22 +18,22 @@ type declaration_group = type cfim_module = { name : string; declarations : declaration_group list; - types : type_def list; - functions : fun_def list; + types : type_decl list; + functions : fun_decl list; } -(** CFIM module *) +(** LLBC module - TODO: rename to crate *) let compute_defs_maps (m : cfim_module) : - type_def TypeDefId.Map.t * fun_def FunDefId.Map.t = + type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t = let types_map = List.fold_left - (fun m (def : type_def) -> TypeDefId.Map.add def.def_id def m) - TypeDefId.Map.empty m.types + (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m) + TypeDeclId.Map.empty m.types in let funs_map = List.fold_left - (fun m (def : fun_def) -> FunDefId.Map.add def.def_id def m) - FunDefId.Map.empty m.functions + (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m) + FunDeclId.Map.empty m.functions in (types_map, funs_map) @@ -54,8 +55,8 @@ let split_declarations (decls : declaration_group list) : declaration groups. *) let split_declarations_to_group_maps (decls : declaration_group list) : - type_declaration_group TypeDefId.Map.t - * fun_declaration_group FunDefId.Map.t = + type_declaration_group TypeDeclId.Map.t + * fun_declaration_group FunDeclId.Map.t = let module G (M : Map.S) = struct let add_group (map : M.key g_declaration_group M.t) (group : M.key g_declaration_group) : M.key g_declaration_group M.t = @@ -68,8 +69,8 @@ let split_declarations_to_group_maps (decls : declaration_group list) : List.fold_left add_group M.empty groups end in let types, funs = split_declarations decls in - let module TG = G (TypeDefId.Map) in + let module TG = G (TypeDeclId.Map) in let types = TG.create_map types in - let module FG = G (FunDefId.Map) in + let module FG = G (FunDeclId.Map) in let funs = FG.create_map funs in (types, funs) diff --git a/src/PrePasses.ml b/src/PrePasses.ml index e9d2dad1..925b82aa 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -24,7 +24,7 @@ let log = L.pre_passes_log ``` *) -let filter_drop_assigns (f : A.fun_def) : A.fun_def = +let filter_drop_assigns (f : A.fun_decl) : A.fun_decl = (* The visitor *) let obj = object (self) diff --git a/src/Print.ml b/src/Print.ml index e64e7d73..64351e3e 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -48,7 +48,7 @@ module Types = struct type 'r type_formatter = { r_to_string : 'r -> string; type_var_id_to_string : T.TypeVarId.id -> string; - type_def_id_to_string : T.TypeDefId.id -> string; + type_decl_id_to_string : T.TypeDeclId.id -> string; } type stype_formatter = T.RegionVarId.id T.region type_formatter @@ -73,7 +73,7 @@ module Types = struct let type_id_to_string (fmt : 'r type_formatter) (id : T.type_id) : string = match id with - | T.AdtId id -> fmt.type_def_id_to_string id + | T.AdtId id -> fmt.type_decl_id_to_string id | T.Tuple -> "" | T.Assumed aty -> ( match aty with @@ -130,8 +130,8 @@ module Types = struct ^ String.concat ", " (List.map (field_to_string fmt) v.fields) ^ ")" - let type_def_to_string (type_def_id_to_string : T.TypeDefId.id -> string) - (def : T.type_def) : string = + let type_decl_to_string (type_decl_id_to_string : T.TypeDeclId.id -> string) + (def : T.type_decl) : string = let regions = def.region_params in let types = def.type_params in let rid_to_string rid = @@ -145,7 +145,7 @@ module Types = struct | Some tv -> type_var_to_string tv | None -> failwith "Unreachable" in - let fmt = { r_to_string; type_var_id_to_string; type_def_id_to_string } in + let fmt = { r_to_string; type_var_id_to_string; type_decl_id_to_string } in let name = name_to_string def.name in let params = if List.length regions + List.length types > 0 then @@ -180,32 +180,32 @@ module Values = struct rvar_to_string : T.RegionVarId.id -> string; r_to_string : T.RegionId.id -> string; type_var_id_to_string : T.TypeVarId.id -> string; - type_def_id_to_string : T.TypeDefId.id -> string; - adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string; + type_decl_id_to_string : T.TypeDeclId.id -> string; + adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string; var_id_to_string : V.VarId.id -> string; adt_field_names : - T.TypeDefId.id -> T.VariantId.id option -> string list option; + T.TypeDeclId.id -> T.VariantId.id option -> string list option; } let value_to_etype_formatter (fmt : value_formatter) : PT.etype_formatter = { PT.r_to_string = PT.erased_region_to_string; PT.type_var_id_to_string = fmt.type_var_id_to_string; - PT.type_def_id_to_string = fmt.type_def_id_to_string; + PT.type_decl_id_to_string = fmt.type_decl_id_to_string; } let value_to_rtype_formatter (fmt : value_formatter) : PT.rtype_formatter = { PT.r_to_string = PT.region_to_string fmt.r_to_string; PT.type_var_id_to_string = fmt.type_var_id_to_string; - PT.type_def_id_to_string = fmt.type_def_id_to_string; + PT.type_decl_id_to_string = fmt.type_decl_id_to_string; } let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter = { PT.r_to_string = PT.region_to_string fmt.rvar_to_string; PT.type_var_id_to_string = fmt.type_var_id_to_string; - PT.type_def_id_to_string = fmt.type_def_id_to_string; + PT.type_decl_id_to_string = fmt.type_decl_id_to_string; } let var_id_to_string (id : V.VarId.id) : string = @@ -260,7 +260,7 @@ module Values = struct let adt_ident = match av.variant_id with | Some vid -> fmt.adt_variant_to_string def_id vid - | None -> fmt.type_def_id_to_string def_id + | None -> fmt.type_decl_id_to_string def_id in if List.length field_values > 0 then match fmt.adt_field_names def_id av.V.variant_id with @@ -372,7 +372,7 @@ module Values = struct let adt_ident = match av.variant_id with | Some vid -> fmt.adt_variant_to_string def_id vid - | None -> fmt.type_def_id_to_string def_id + | None -> fmt.type_decl_id_to_string def_id in if List.length field_values > 0 then match fmt.adt_field_names def_id av.V.variant_id with @@ -565,21 +565,22 @@ module Contexts = struct let ctx_to_rtype_formatter (fmt : ctx_formatter) : PT.rtype_formatter = PV.value_to_rtype_formatter fmt - let type_ctx_to_adt_variant_to_string_fun (ctx : T.type_def T.TypeDefId.Map.t) - : T.TypeDefId.id -> T.VariantId.id -> string = + let type_ctx_to_adt_variant_to_string_fun + (ctx : T.type_decl T.TypeDeclId.Map.t) : + T.TypeDeclId.id -> T.VariantId.id -> string = fun def_id variant_id -> - let def = T.TypeDefId.Map.find def_id ctx in + let def = T.TypeDeclId.Map.find def_id ctx in match def.kind with | Struct _ -> failwith "Unreachable" | Enum variants -> let variant = T.VariantId.nth variants variant_id in name_to_string def.name ^ "::" ^ variant.variant_name - let type_ctx_to_adt_field_names_fun (ctx : T.type_def T.TypeDefId.Map.t) : - T.TypeDefId.id -> T.VariantId.id option -> string list option = + let type_ctx_to_adt_field_names_fun (ctx : T.type_decl T.TypeDeclId.Map.t) : + T.TypeDeclId.id -> T.VariantId.id option -> string list option = fun def_id opt_variant_id -> - let def = T.TypeDefId.Map.find def_id ctx in - let fields = TU.type_def_get_fields def opt_variant_id in + let def = T.TypeDeclId.Map.find def_id ctx in + let fields = TU.type_decl_get_fields def opt_variant_id in (* There are two cases: either all the fields have names, or none of them * has names *) let has_names = @@ -599,25 +600,25 @@ module Contexts = struct let v = C.lookup_type_var ctx vid in v.name in - let type_def_id_to_string def_id = - let def = C.ctx_lookup_type_def ctx def_id in + let type_decl_id_to_string def_id = + let def = C.ctx_lookup_type_decl ctx def_id in name_to_string def.name in let adt_variant_to_string = - type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs + type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls in let var_id_to_string vid = let bv = C.ctx_lookup_binder ctx vid in binder_to_string bv in let adt_field_names = - type_ctx_to_adt_field_names_fun ctx.type_context.type_defs + type_ctx_to_adt_field_names_fun ctx.type_context.type_decls in { rvar_to_string; r_to_string; type_var_id_to_string; - type_def_id_to_string; + type_decl_id_to_string; adt_variant_to_string; var_id_to_string; adt_field_names; @@ -683,14 +684,14 @@ module CfimAst = struct rvar_to_string : T.RegionVarId.id -> string; r_to_string : T.RegionId.id -> string; type_var_id_to_string : T.TypeVarId.id -> string; - type_def_id_to_string : T.TypeDefId.id -> string; - adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string; + type_decl_id_to_string : T.TypeDeclId.id -> string; + adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string; adt_field_to_string : - T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string option; + T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option; var_id_to_string : V.VarId.id -> string; adt_field_names : - T.TypeDefId.id -> T.VariantId.id option -> string list option; - fun_def_id_to_string : A.FunDefId.id -> string; + T.TypeDeclId.id -> T.VariantId.id option -> string list option; + fun_decl_id_to_string : A.FunDeclId.id -> string; } let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter = @@ -698,7 +699,7 @@ module CfimAst = struct PV.rvar_to_string = fmt.rvar_to_string; PV.r_to_string = fmt.r_to_string; PV.type_var_id_to_string = fmt.type_var_id_to_string; - PV.type_def_id_to_string = fmt.type_def_id_to_string; + PV.type_decl_id_to_string = fmt.type_decl_id_to_string; PV.adt_variant_to_string = fmt.adt_variant_to_string; PV.var_id_to_string = fmt.var_id_to_string; PV.adt_field_names = fmt.adt_field_names; @@ -711,55 +712,57 @@ module CfimAst = struct { PT.r_to_string = PT.erased_region_to_string; PT.type_var_id_to_string = fmt.type_var_id_to_string; - PT.type_def_id_to_string = fmt.type_def_id_to_string; + PT.type_decl_id_to_string = fmt.type_decl_id_to_string; } let ast_to_rtype_formatter (fmt : ast_formatter) : PT.rtype_formatter = { PT.r_to_string = PT.region_to_string fmt.r_to_string; PT.type_var_id_to_string = fmt.type_var_id_to_string; - PT.type_def_id_to_string = fmt.type_def_id_to_string; + PT.type_decl_id_to_string = fmt.type_decl_id_to_string; } let ast_to_stype_formatter (fmt : ast_formatter) : PT.stype_formatter = { PT.r_to_string = PT.region_to_string fmt.rvar_to_string; PT.type_var_id_to_string = fmt.type_var_id_to_string; - PT.type_def_id_to_string = fmt.type_def_id_to_string; + PT.type_decl_id_to_string = fmt.type_decl_id_to_string; } - let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def T.TypeDefId.Map.t) : - T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string option = + let type_ctx_to_adt_field_to_string_fun (ctx : T.type_decl T.TypeDeclId.Map.t) + : + T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option + = fun def_id opt_variant_id field_id -> - let def = T.TypeDefId.Map.find def_id ctx in - let fields = TU.type_def_get_fields def opt_variant_id in + let def = T.TypeDeclId.Map.find def_id ctx in + let fields = TU.type_decl_get_fields def opt_variant_id in let field = T.FieldId.nth fields field_id in field.T.field_name let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : ast_formatter = let ctx_fmt = PC.eval_ctx_to_ctx_formatter ctx in let adt_field_to_string = - type_ctx_to_adt_field_to_string_fun ctx.type_context.type_defs + type_ctx_to_adt_field_to_string_fun ctx.type_context.type_decls in - let fun_def_id_to_string def_id = - let def = C.ctx_lookup_fun_def ctx def_id in + let fun_decl_id_to_string def_id = + let def = C.ctx_lookup_fun_decl ctx def_id in fun_name_to_string def.name in { rvar_to_string = ctx_fmt.PV.rvar_to_string; r_to_string = ctx_fmt.PV.r_to_string; type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string; - type_def_id_to_string = ctx_fmt.PV.type_def_id_to_string; + type_decl_id_to_string = ctx_fmt.PV.type_decl_id_to_string; adt_variant_to_string = ctx_fmt.PV.adt_variant_to_string; var_id_to_string = ctx_fmt.PV.var_id_to_string; adt_field_names = ctx_fmt.PV.adt_field_names; adt_field_to_string; - fun_def_id_to_string; + fun_decl_id_to_string; } - let fun_def_to_ast_formatter (type_defs : T.type_def T.TypeDefId.Map.t) - (fun_defs : A.fun_def A.FunDefId.Map.t) (fdef : A.fun_def) : ast_formatter - = + let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t) + (fun_decls : A.fun_decl A.FunDeclId.Map.t) (fdef : A.fun_decl) : + ast_formatter = let rvar_to_string r = let rvar = T.RegionVarId.nth fdef.signature.region_params r in PT.region_var_to_string rvar @@ -770,33 +773,33 @@ module CfimAst = struct let var = T.TypeVarId.nth fdef.signature.type_params vid in PT.type_var_to_string var in - let type_def_id_to_string def_id = - let def = T.TypeDefId.Map.find def_id type_defs in + let type_decl_id_to_string def_id = + let def = T.TypeDeclId.Map.find def_id type_decls in name_to_string def.name in let adt_variant_to_string = - PC.type_ctx_to_adt_variant_to_string_fun type_defs + PC.type_ctx_to_adt_variant_to_string_fun type_decls in let var_id_to_string vid = let var = V.VarId.nth fdef.locals vid in var_to_string var in - let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_defs in - let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_defs in - let fun_def_id_to_string def_id = - let def = A.FunDefId.Map.find def_id fun_defs in + let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in + let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in + let fun_decl_id_to_string def_id = + let def = A.FunDeclId.Map.find def_id fun_decls in fun_name_to_string def.name in { rvar_to_string; r_to_string; type_var_id_to_string; - type_def_id_to_string; + type_decl_id_to_string; adt_variant_to_string; var_id_to_string; adt_field_names; adt_field_to_string; - fun_def_id_to_string; + fun_decl_id_to_string; } let rec projection_to_string (fmt : ast_formatter) (inside : string) @@ -907,7 +910,7 @@ module CfimAst = struct match akind with | E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")" | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) -> - let adt_name = fmt.type_def_id_to_string def_id in + let adt_name = fmt.type_decl_id_to_string def_id in let variant_name = match opt_variant_id with | None -> adt_name @@ -959,7 +962,7 @@ module CfimAst = struct let args = "(" ^ String.concat ", " args ^ ")" in let name_params = match call.A.func with - | A.Local fid -> fmt.fun_def_id_to_string fid ^ params + | A.Local fid -> fmt.fun_decl_id_to_string fid ^ params | A.Assumed fid -> ( match fid with | A.Replace -> "core::mem::replace" ^ params @@ -1034,8 +1037,8 @@ module CfimAst = struct let var_to_string (v : A.var) : string = match v.name with None -> PV.var_id_to_string v.index | Some name -> name - let fun_def_to_string (fmt : ast_formatter) (indent : string) - (indent_incr : string) (def : A.fun_def) : string = + let fun_decl_to_string (fmt : ast_formatter) (indent : string) + (indent_incr : string) (def : A.fun_decl) : string = let sty_fmt = ast_to_stype_formatter fmt in let sty_to_string = PT.sty_to_string sty_fmt in let ety_fmt = ast_to_etype_formatter fmt in @@ -1099,18 +1102,18 @@ module PA = CfimAst (* local module *) module Module = struct (** This function pretty-prints a type definition by using a definition context *) - let type_def_to_string (type_context : T.type_def T.TypeDefId.Map.t) - (def : T.type_def) : string = - let type_def_id_to_string (id : T.TypeDefId.id) : string = - let def = T.TypeDefId.Map.find id type_context in + let type_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t) + (def : T.type_decl) : string = + let type_decl_id_to_string (id : T.TypeDeclId.id) : string = + let def = T.TypeDeclId.Map.find id type_context in name_to_string def.name in - PT.type_def_to_string type_def_id_to_string def + PT.type_decl_to_string type_decl_id_to_string def (** Generate an [ast_formatter] by using a definition context in combination with the variables local to a function's definition *) - let def_ctx_to_ast_formatter (type_context : T.type_def T.TypeDefId.Map.t) - (fun_context : A.fun_def A.FunDefId.Map.t) (def : A.fun_def) : + let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t) + (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) : PA.ast_formatter = let rvar_to_string vid = let var = T.RegionVarId.nth def.signature.region_params vid in @@ -1124,12 +1127,12 @@ module Module = struct let var = T.TypeVarId.nth def.signature.type_params vid in PT.type_var_to_string var in - let type_def_id_to_string def_id = - let def = T.TypeDefId.Map.find def_id type_context in + let type_decl_id_to_string def_id = + let def = T.TypeDeclId.Map.find def_id type_context in name_to_string def.name in - let fun_def_id_to_string def_id = - let def = A.FunDefId.Map.find def_id fun_context in + let fun_decl_id_to_string def_id = + let def = A.FunDeclId.Map.find def_id fun_context in fun_name_to_string def.name in let var_id_to_string vid = @@ -1147,34 +1150,34 @@ module Module = struct rvar_to_string; r_to_string; type_var_id_to_string; - type_def_id_to_string; + type_decl_id_to_string; adt_variant_to_string; adt_field_to_string; var_id_to_string; adt_field_names; - fun_def_id_to_string; + fun_decl_id_to_string; } (** This function pretty-prints a function definition by using a definition context *) - let fun_def_to_string (type_context : T.type_def T.TypeDefId.Map.t) - (fun_context : A.fun_def A.FunDefId.Map.t) (def : A.fun_def) : string = + let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t) + (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) : string = let fmt = def_ctx_to_ast_formatter type_context fun_context def in - PA.fun_def_to_string fmt "" " " def + PA.fun_decl_to_string fmt "" " " def let module_to_string (m : M.cfim_module) : string = let types_defs_map, funs_defs_map = M.compute_defs_maps m in (* The types *) - let type_defs = List.map (type_def_to_string types_defs_map) m.M.types in + let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in (* The functions *) - let fun_defs = - List.map (fun_def_to_string types_defs_map funs_defs_map) m.M.functions + let fun_decls = + List.map (fun_decl_to_string types_defs_map funs_defs_map) m.M.functions in (* Put everything together *) - let all_defs = List.append type_defs fun_defs in + let all_defs = List.append type_decls fun_decls in String.concat "\n\n" all_defs end diff --git a/src/PrintPure.ml b/src/PrintPure.ml index c1da7610..e96edeed 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -5,31 +5,31 @@ module T = Types module V = Values module E = Expressions module A = CfimAst -module TypeDefId = T.TypeDefId +module TypeDeclId = T.TypeDeclId module TypeVarId = T.TypeVarId module RegionId = T.RegionId module VariantId = T.VariantId module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId -module FunDefId = A.FunDefId +module FunDeclId = A.FunDeclId type type_formatter = { type_var_id_to_string : TypeVarId.id -> string; - type_def_id_to_string : TypeDefId.id -> string; + type_decl_id_to_string : TypeDeclId.id -> string; } type value_formatter = { type_var_id_to_string : TypeVarId.id -> string; - type_def_id_to_string : TypeDefId.id -> string; - adt_variant_to_string : TypeDefId.id -> VariantId.id -> string; + type_decl_id_to_string : TypeDeclId.id -> string; + adt_variant_to_string : TypeDeclId.id -> VariantId.id -> string; var_id_to_string : VarId.id -> string; - adt_field_names : TypeDefId.id -> VariantId.id option -> string list option; + adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option; } let value_to_type_formatter (fmt : value_formatter) : type_formatter = { type_var_id_to_string = fmt.type_var_id_to_string; - type_def_id_to_string = fmt.type_def_id_to_string; + type_decl_id_to_string = fmt.type_decl_id_to_string; } (* TODO: we need to store which variables we have encountered so far, and @@ -37,19 +37,19 @@ let value_to_type_formatter (fmt : value_formatter) : type_formatter = *) type ast_formatter = { type_var_id_to_string : TypeVarId.id -> string; - type_def_id_to_string : TypeDefId.id -> string; - adt_variant_to_string : TypeDefId.id -> VariantId.id -> string; + type_decl_id_to_string : TypeDeclId.id -> string; + adt_variant_to_string : TypeDeclId.id -> VariantId.id -> string; var_id_to_string : VarId.id -> string; adt_field_to_string : - TypeDefId.id -> VariantId.id option -> FieldId.id -> string option; - adt_field_names : TypeDefId.id -> VariantId.id option -> string list option; - fun_def_id_to_string : A.FunDefId.id -> string; + TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option; + adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option; + fun_decl_id_to_string : A.FunDeclId.id -> string; } let ast_to_value_formatter (fmt : ast_formatter) : value_formatter = { type_var_id_to_string = fmt.type_var_id_to_string; - type_def_id_to_string = fmt.type_def_id_to_string; + type_decl_id_to_string = fmt.type_decl_id_to_string; adt_variant_to_string = fmt.adt_variant_to_string; var_id_to_string = fmt.var_id_to_string; adt_field_names = fmt.adt_field_names; @@ -71,65 +71,65 @@ let integer_type_to_string = Print.Types.integer_type_to_string let scalar_value_to_string = Print.Values.scalar_value_to_string -let mk_type_formatter (type_defs : T.type_def TypeDefId.Map.t) +let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t) (type_params : type_var list) : type_formatter = let type_var_id_to_string vid = let var = T.TypeVarId.nth type_params vid in type_var_to_string var in - let type_def_id_to_string def_id = - let def = T.TypeDefId.Map.find def_id type_defs in + let type_decl_id_to_string def_id = + let def = T.TypeDeclId.Map.find def_id type_decls in name_to_string def.name in - { type_var_id_to_string; type_def_id_to_string } + { type_var_id_to_string; type_decl_id_to_string } -(* TODO: there is a bit of duplication with Print.fun_def_to_ast_formatter. +(* TODO: there is a bit of duplication with Print.fun_decl_to_ast_formatter. TODO: use the pure defs as inputs? Note that it is a bit annoying for the functions (there is a difference between the forward/backward functions...) while we only need those definitions to lookup proper names for the def ids. *) -let mk_ast_formatter (type_defs : T.type_def TypeDefId.Map.t) - (fun_defs : A.fun_def FunDefId.Map.t) (type_params : type_var list) : +let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) + (fun_decls : A.fun_decl FunDeclId.Map.t) (type_params : type_var list) : ast_formatter = let type_var_id_to_string vid = let var = T.TypeVarId.nth type_params vid in type_var_to_string var in - let type_def_id_to_string def_id = - let def = T.TypeDefId.Map.find def_id type_defs in + let type_decl_id_to_string def_id = + let def = T.TypeDeclId.Map.find def_id type_decls in name_to_string def.name in let adt_variant_to_string = - Print.Contexts.type_ctx_to_adt_variant_to_string_fun type_defs + Print.Contexts.type_ctx_to_adt_variant_to_string_fun type_decls in let var_id_to_string vid = (* TODO: somehow lookup in the context *) "^" ^ VarId.to_string vid in let adt_field_names = - Print.Contexts.type_ctx_to_adt_field_names_fun type_defs + Print.Contexts.type_ctx_to_adt_field_names_fun type_decls in let adt_field_to_string = - Print.CfimAst.type_ctx_to_adt_field_to_string_fun type_defs + Print.CfimAst.type_ctx_to_adt_field_to_string_fun type_decls in - let fun_def_id_to_string def_id = - let def = A.FunDefId.Map.find def_id fun_defs in + let fun_decl_id_to_string def_id = + let def = A.FunDeclId.Map.find def_id fun_decls in fun_name_to_string def.name in { type_var_id_to_string; - type_def_id_to_string; + type_decl_id_to_string; adt_variant_to_string; var_id_to_string; adt_field_names; adt_field_to_string; - fun_def_id_to_string; + fun_decl_id_to_string; } let type_id_to_string (fmt : type_formatter) (id : type_id) : string = match id with - | AdtId id -> fmt.type_def_id_to_string id + | AdtId id -> fmt.type_decl_id_to_string id | Tuple -> "" | Assumed aty -> ( match aty with @@ -167,7 +167,7 @@ let variant_to_string fmt (v : variant) : string = ^ String.concat ", " (List.map (field_to_string fmt) v.fields) ^ ")" -let type_def_to_string (fmt : type_formatter) (def : type_def) : string = +let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string = let types = def.type_params in let name = name_to_string def.name in let params = @@ -245,7 +245,7 @@ let adt_g_value_to_string (fmt : value_formatter) let adt_ident = match variant_id with | Some vid -> fmt.adt_variant_to_string def_id vid - | None -> fmt.type_def_id_to_string def_id + | None -> fmt.type_decl_id_to_string def_id in if field_values <> [] then match fmt.adt_field_names def_id variant_id with @@ -358,7 +358,7 @@ let inst_fun_sig_to_string (fmt : ast_formatter) (sg : inst_fun_sig) : string = let regular_fun_id_to_string (fmt : ast_formatter) (fun_id : A.fun_id) : string = match fun_id with - | A.Local fid -> fmt.fun_def_id_to_string fid + | A.Local fid -> fmt.fun_decl_id_to_string fid | A.Assumed fid -> ( match fid with | A.Replace -> "core::mem::replace" @@ -474,7 +474,7 @@ and switch_to_string (fmt : ast_formatter) (indent : string) let branches = List.map branch_to_string branches in "match " ^ scrut ^ " with\n" ^ String.concat "\n" branches -let fun_def_to_string (fmt : ast_formatter) (def : fun_def) : string = +let fun_decl_to_string (fmt : ast_formatter) (def : fun_decl) : string = let type_fmt = ast_to_type_formatter fmt in let name = fun_name_to_string def.basename ^ fun_suffix def.back_id in let signature = fun_sig_to_string fmt def.signature in diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml index 25b39e2e..1679aa6c 100644 --- a/src/PrintSymbolicAst.ml +++ b/src/PrintSymbolicAst.ml @@ -20,7 +20,7 @@ module PT = Print.Types type formatting_ctx = { type_context : C.type_context; - fun_context : A.fun_def A.FunDefId.Map.t; + fun_context : A.fun_decl A.FunDeclId.Map.t; type_vars : T.type_var list; } @@ -35,24 +35,24 @@ let formatting_ctx_to_formatter (ctx : formatting_ctx) : formatter = let v = T.TypeVarId.nth ctx.type_vars vid in v.name in - let type_def_id_to_string def_id = - let def = T.TypeDefId.Map.find def_id ctx.type_context.type_defs in + let type_decl_id_to_string def_id = + let def = T.TypeDeclId.Map.find def_id ctx.type_context.type_decls in P.name_to_string def.name in let adt_variant_to_string = - P.Contexts.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs + P.Contexts.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls in (* We shouldn't use [var_id_to_string] *) let var_id_to_string _ = failwith "Unexpected use of var_id_to_string" in let adt_field_names = - P.Contexts.type_ctx_to_adt_field_names_fun ctx.type_context.type_defs + P.Contexts.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls in { rvar_to_string; r_to_string; type_var_id_to_string; - type_def_id_to_string; + type_decl_id_to_string; adt_variant_to_string; var_id_to_string; adt_field_names; diff --git a/src/Pure.ml b/src/Pure.ml index 0f4280c3..b1c8e254 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -3,13 +3,13 @@ module T = Types module V = Values module E = Expressions module A = CfimAst -module TypeDefId = T.TypeDefId +module TypeDeclId = T.TypeDeclId module TypeVarId = T.TypeVarId module RegionGroupId = T.RegionGroupId module VariantId = T.VariantId module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId -module FunDefId = A.FunDefId +module FunDeclId = A.FunDeclId module SynthPhaseId = IdGen () (** We give an identifier to every phase of the synthesis (forward, backward @@ -45,7 +45,7 @@ let option_some_id = T.option_some_id let option_none_id = T.option_none_id -type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty +type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty [@@deriving show, ord] (** Ancestor for iter visitor for [ty] *) @@ -115,16 +115,16 @@ type field = { field_name : string option; field_ty : ty } [@@deriving show] type variant = { variant_name : string; fields : field list } [@@deriving show] -type type_def_kind = Struct of field list | Enum of variant list +type type_decl_kind = Struct of field list | Enum of variant list [@@deriving show] type type_var = T.type_var [@@deriving show] -type type_def = { - def_id : TypeDefId.id; +type type_decl = { + def_id : TypeDeclId.id; name : name; type_params : type_var list; - kind : type_def_kind; + kind : type_decl_kind; } [@@deriving show] @@ -595,8 +595,8 @@ type fun_sig = { type inst_fun_sig = { inputs : ty list; outputs : ty list } -type fun_def = { - def_id : FunDefId.id; +type fun_decl = { + def_id : FunDeclId.id; back_id : T.RegionGroupId.id option; basename : fun_name; (** The "base" name of the function. diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index f45c59bb..c1cacac5 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -157,7 +157,7 @@ type pn_ctx = string VarId.Map.t ``` - TODO: inputs and end abstraction... *) -let compute_pretty_names (def : fun_def) : fun_def = +let compute_pretty_names (def : fun_decl) : fun_decl = (* Small helpers *) (* * When we do branchings, we need to merge (the constraints saved in) the @@ -322,7 +322,7 @@ let compute_pretty_names (def : fun_def) : fun_def = { def with body } (** Remove the meta-information *) -let remove_meta (def : fun_def) : fun_def = +let remove_meta (def : fun_decl) : fun_decl = let obj = object inherit [_] map_expression as super @@ -360,7 +360,7 @@ let remove_meta (def : fun_def) : fun_def = pass (if they are useless). *) let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool) - (def : fun_def) : fun_def = + (def : fun_decl) : fun_decl = let obj = object (self) inherit [_] map_expression as super @@ -504,7 +504,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (call0 : call) (* We need to use the regions hierarchy *) (* First, lookup the signature of the CFIM function *) let sg = - CfimAstUtils.lookup_fun_sig id0 ctx.fun_context.fun_defs + CfimAstUtils.lookup_fun_sig id0 ctx.fun_context.fun_decls in (* Compute the set of ancestors of the function in call1 *) let call1_ancestors = @@ -585,7 +585,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (call0 : call) (** Filter the useless assignments (removes the useless variables, filters the function calls) *) let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx) - (def : fun_def) : fun_def = + (def : fun_decl) : fun_decl = (* We first need a transformation on *left-values*, which filters the useless * variables and tells us whether the value contains any variable which has * not been replaced by `_` (in which case we need to keep the assignment, @@ -707,8 +707,8 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx) symbolic to pure. Here, we remove the definitions altogether, because they are now useless *) -let filter_if_backward_with_no_outputs (config : config) (def : fun_def) : - fun_def option = +let filter_if_backward_with_no_outputs (config : config) (def : fun_decl) : + fun_decl option = if config.filter_useless_functions && Option.is_some def.back_id && def.signature.outputs = [] @@ -745,7 +745,7 @@ let keep_forward (config : config) (trans : pure_fun_translation) : bool = (** Add unit arguments (optionally) to functions with no arguments, and change their output type to use `result` *) -let to_monadic (config : config) (def : fun_def) : fun_def = +let to_monadic (config : config) (def : fun_decl) : fun_decl = (* Update the body *) let obj = object @@ -812,7 +812,7 @@ let to_monadic (config : config) (def : fun_def) : fun_def = (** Convert the unit variables to `()` if they are used as right-values or `_` if they are used as left values in patterns. *) -let unit_vars_to_unit (def : fun_def) : fun_def = +let unit_vars_to_unit (def : fun_decl) : fun_decl = (* The map visitor *) let obj = object @@ -846,7 +846,7 @@ let unit_vars_to_unit (def : fun_def) : fun_def = function calls, and when translating end abstractions. Here, we can do something simpler, in one micro-pass. *) -let eliminate_box_functions (_ctx : trans_ctx) (def : fun_def) : fun_def = +let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = (* The map visitor *) let obj = object @@ -894,7 +894,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_def) : fun_def = See the explanations in [config]. *) -let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_def) : fun_def +let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl = (* Set up the var id generator *) let cnt = get_expression_min_var_counter def.body.e in @@ -937,7 +937,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_def) : fun_def (** Unfold the monadic let-bindings to explicit matches. *) let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx) - (def : fun_def) : fun_def = + (def : fun_decl) : fun_decl = (* We may need to introduce fresh variables for the state *) let var_cnt = get_expression_min_var_counter def.body.e in let _, fresh_var_id = VarId.mk_stateful_generator var_cnt in @@ -1066,8 +1066,8 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx) [ctx]: used only for printing. *) -let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : - fun_def option = +let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) : + fun_decl option = (* Debug *) log#ldebug (lazy @@ -1080,7 +1080,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : (* First, find names for the variables which are unnamed *) let def = compute_pretty_names def in log#ldebug - (lazy ("compute_pretty_name:\n\n" ^ fun_def_to_string ctx def ^ "\n")); + (lazy ("compute_pretty_name:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); (* TODO: we might want to leverage more the assignment meta-data, for * aggregates for instance. *) @@ -1091,7 +1091,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : * Rk.: some passes below use the fact that we removed the meta-data * (otherwise we would have to "unmeta" expressions before matching) *) let def = remove_meta def in - log#ldebug (lazy ("remove_meta:\n\n" ^ fun_def_to_string ctx def ^ "\n")); + log#ldebug (lazy ("remove_meta:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); (* Remove the backward functions with no outputs. * Note that the calls to those functions should already have been removed, @@ -1108,13 +1108,13 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : * TODO: this is not true with the state-error monad, unless we unfold the monadic binds. * Also, from now onwards, the outputs list has length 1. *) let def = to_monadic config def in - log#ldebug (lazy ("to_monadic:\n\n" ^ fun_def_to_string ctx def ^ "\n")); + log#ldebug (lazy ("to_monadic:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); (* Convert the unit variables to `()` if they are used as right-values or * `_` if they are used as left values. *) let def = unit_vars_to_unit def in log#ldebug - (lazy ("unit_vars_to_unit:\n\n" ^ fun_def_to_string ctx def ^ "\n")); + (lazy ("unit_vars_to_unit:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); (* Inline the useless variable reassignments *) let inline_named_vars = true in @@ -1124,7 +1124,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : in log#ldebug (lazy - ("inline_useless_var_assignments:\n\n" ^ fun_def_to_string ctx def + ("inline_useless_var_assignments:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); (* Eliminate the box functions - note that the "box" types were eliminated @@ -1132,12 +1132,12 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : let def = eliminate_box_functions ctx def in log#ldebug (lazy - ("eliminate_box_functions:\n\n" ^ fun_def_to_string ctx def ^ "\n")); + ("eliminate_box_functions:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); (* Filter the useless variables, assignments, function calls, etc. *) let def = filter_useless config.filter_useless_monadic_calls ctx def in log#ldebug - (lazy ("filter_useless:\n\n" ^ fun_def_to_string ctx def ^ "\n")); + (lazy ("filter_useless:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); (* Decompose the monadic let-bindings - F* specific * TODO: remove? With the state-error monad, it is becoming completely @@ -1149,7 +1149,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : let def = decompose_monadic_let_bindings ctx def in log#ldebug (lazy - ("decompose_monadic_let_bindings:\n\n" ^ fun_def_to_string ctx def + ("decompose_monadic_let_bindings:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); def) else ( @@ -1165,7 +1165,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : let def = unfold_monadic_let_bindings config ctx def in log#ldebug (lazy - ("unfold_monadic_let_bindings:\n\n" ^ fun_def_to_string ctx def + ("unfold_monadic_let_bindings:\n\n" ^ fun_decl_to_string ctx def ^ "\n")); def) else ( diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index ba638743..2c8a5a28 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -92,7 +92,7 @@ type formatter = { (`None` if forward function) TODO: use the fun id for the assumed functions. *) - decreases_clause_name : FunDefId.id -> fun_name -> string; + decreases_clause_name : FunDeclId.id -> fun_name -> string; (** Generates the name of the definition used to prove/reason about termination. The generated code uses this clause where needed, but its body must be defined by the user. @@ -340,13 +340,13 @@ type extraction_ctx = { (** Debugging function *) let id_to_string (id : id) (ctx : extraction_ctx) : string = - let fun_defs = ctx.trans_ctx.fun_context.fun_defs in - let type_defs = ctx.trans_ctx.type_context.type_defs in + let fun_decls = ctx.trans_ctx.fun_context.fun_decls in + let type_decls = ctx.trans_ctx.type_context.type_decls in (* TODO: factorize the pretty-printing with what is in PrintPure *) let get_type_name (id : type_id) : string = match id with | AdtId id -> - let def = TypeDefId.Map.find id type_defs in + let def = TypeDeclId.Map.find id type_decls in Print.name_to_string def.name | Assumed aty -> show_assumed_ty aty | Tuple -> failwith "Unreachable" @@ -356,7 +356,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let fun_name = match fid with | A.Local fid -> - Print.fun_name_to_string (FunDefId.Map.find fid fun_defs).name + Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name | A.Assumed aid -> A.show_assumed_fun_id aid in let fun_kind = @@ -369,7 +369,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let fun_name = match fid with | A.Local fid -> - Print.fun_name_to_string (FunDefId.Map.find fid fun_defs).name + Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name | A.Assumed aid -> A.show_assumed_fun_id aid in "decreases clause for function: " ^ fun_name @@ -390,7 +390,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = else failwith "Unreachable" | Assumed Vec -> failwith "Unreachable" | AdtId id -> ( - let def = TypeDefId.Map.find id type_defs in + let def = TypeDeclId.Map.find id type_decls in match def.kind with | Struct _ -> failwith "Unreachable" | Enum variants -> @@ -407,7 +407,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = (* We can't directly have access to the fields of a vector *) failwith "Unreachable" | AdtId id -> ( - let def = TypeDefId.Map.find id type_defs in + let def = TypeDeclId.Map.find id type_decls in match def.kind with | Enum _ -> failwith "Unreachable" | Struct fields -> @@ -444,7 +444,7 @@ let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get (FunId (id, rg)) ctx -let ctx_get_local_function (id : FunDefId.id) (rg : RegionGroupId.id option) +let ctx_get_local_function (id : FunDeclId.id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get_function (A.Local id) rg ctx @@ -452,7 +452,7 @@ let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string = assert (id <> Tuple); ctx_get (TypeId id) ctx -let ctx_get_local_type (id : TypeDefId.id) (ctx : extraction_ctx) : string = +let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string = ctx_get_type (AdtId id) ctx let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string = @@ -475,7 +475,7 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id) (ctx : extraction_ctx) : string = ctx_get (VariantId (def_id, variant_id)) ctx -let ctx_get_decreases_clause (def_id : FunDefId.id) (ctx : extraction_ctx) : +let ctx_get_decreases_clause (def_id : FunDeclId.id) (ctx : extraction_ctx) : string = ctx_get (DecreasesClauseId (A.Local def_id)) ctx @@ -520,57 +520,57 @@ let ctx_add_type_params (vars : type_var list) (ctx : extraction_ctx) : (fun ctx (var : type_var) -> ctx_add_type_var var.name var.index ctx) ctx vars -let ctx_add_type_def_struct (def : type_def) (ctx : extraction_ctx) : +let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) : extraction_ctx * string = let cons_name = ctx.fmt.struct_constructor def.name in let ctx = ctx_add (StructId (AdtId def.def_id)) cons_name ctx in (ctx, cons_name) -let ctx_add_type_def (def : type_def) (ctx : extraction_ctx) : extraction_ctx = +let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx = let def_name = ctx.fmt.type_name def.name in let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in ctx -let ctx_add_field (def : type_def) (field_id : FieldId.id) (field : field) +let ctx_add_field (def : type_decl) (field_id : FieldId.id) (field : field) (ctx : extraction_ctx) : extraction_ctx * string = let name = ctx.fmt.field_name def.name field_id field.field_name in let ctx = ctx_add (FieldId (AdtId def.def_id, field_id)) name ctx in (ctx, name) -let ctx_add_fields (def : type_def) (fields : (FieldId.id * field) list) +let ctx_add_fields (def : type_decl) (fields : (FieldId.id * field) list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map (fun ctx (vid, v) -> ctx_add_field def vid v ctx) ctx fields -let ctx_add_variant (def : type_def) (variant_id : VariantId.id) +let ctx_add_variant (def : type_decl) (variant_id : VariantId.id) (variant : variant) (ctx : extraction_ctx) : extraction_ctx * string = let name = ctx.fmt.variant_name def.name variant.variant_name in let ctx = ctx_add (VariantId (AdtId def.def_id, variant_id)) name ctx in (ctx, name) -let ctx_add_variants (def : type_def) (variants : (VariantId.id * variant) list) +let ctx_add_variants (def : type_decl) (variants : (VariantId.id * variant) list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map (fun ctx (vid, v) -> ctx_add_variant def vid v ctx) ctx variants -let ctx_add_struct (def : type_def) (ctx : extraction_ctx) : +let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) : extraction_ctx * string = let name = ctx.fmt.struct_constructor def.name in let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in (ctx, name) -let ctx_add_decrases_clause (def : fun_def) (ctx : extraction_ctx) : +let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = let name = ctx.fmt.decreases_clause_name def.def_id def.basename in ctx_add (DecreasesClauseId (A.Local def.def_id)) name ctx -let ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def) +let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = (* Lookup the CFIM def to compute the region group information *) let def_id = def.def_id in - let cfim_def = FunDefId.Map.find def_id ctx.trans_ctx.fun_context.fun_defs in + let cfim_def = FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls in let sg = cfim_def.signature in let num_rgs = List.length sg.regions_hierarchy in let keep_fwd, (_, backs) = trans_group in @@ -655,7 +655,7 @@ let initialize_names_map (init : names_map_init) : names_map = (* Return *) nm -let compute_type_def_name (fmt : formatter) (def : type_def) : string = +let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = fmt.type_name def.name (** A helper function: generates a function suffix from a region group diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 26dc6294..aa8d1f53 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -101,7 +101,7 @@ let ty_as_integer (t : ty) : T.integer_type = match t with Integer int_ty -> int_ty | _ -> raise (Failure "Unreachable") (* TODO: move *) -let type_def_is_enum (def : T.type_def) : bool = +let type_decl_is_enum (def : T.type_decl) : bool = match def.kind with T.Struct _ -> false | Enum _ -> true let mk_state_ty : ty = Adt (Assumed State, []) @@ -182,11 +182,11 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty in fun id -> TypeVarId.Map.find id mp -(** Retrieve the list of fields for the given variant of a [type_def]. +(** Retrieve the list of fields for the given variant of a [type_decl]. Raises [Invalid_argument] if the arguments are incorrect. *) -let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option) +let type_decl_get_fields (def : type_decl) (opt_variant_id : VariantId.id option) : field list = match (def.kind, opt_variant_id) with | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields @@ -199,15 +199,15 @@ let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option) (Invalid_argument ("The variant id should be [Some] if and only if the definition is \ an enumeration:\n\ - - def: " ^ show_type_def def ^ "\n- opt_variant_id: " + - def: " ^ show_type_decl def ^ "\n- opt_variant_id: " ^ opt_variant_id)) (** Instantiate the type variables for the chosen variant in an ADT definition, and return the list of the types of its fields *) -let type_def_get_instantiated_fields_types (def : type_def) +let type_decl_get_instantiated_fields_types (def : type_decl) (opt_variant_id : VariantId.id option) (types : ty list) : ty list = let ty_subst = make_type_subst def.type_params types in - let fields = type_def_get_fields def opt_variant_id in + let fields = type_decl_get_fields def opt_variant_id in List.map (fun f -> ty_substitute ty_subst f.field_ty) fields let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) : @@ -225,17 +225,17 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) : - if all functions only call functions we already explored, they are not mutually recursive *) -let functions_not_mutually_recursive (funs : fun_def list) : bool = +let functions_not_mutually_recursive (funs : fun_decl list) : bool = (* Compute the set of function identifiers in the group *) let ids = FunIdSet.of_list (List.map - (fun (f : fun_def) -> Regular (A.Local f.def_id, f.back_id)) + (fun (f : fun_decl) -> Regular (A.Local f.def_id, f.back_id)) funs) in let ids = ref ids in (* Explore every body *) - let body_only_calls_itself (fdef : fun_def) : bool = + let body_only_calls_itself (fdef : fun_decl) : bool = (* Remove the current id from the id set *) ids := FunIdSet.remove (Regular (A.Local fdef.def_id, fdef.back_id)) !ids; @@ -271,7 +271,7 @@ let rec expression_requires_parentheses (e : texpression) : bool = (** Module to perform type checking - we use this for sanity checks only *) module TypeCheck = struct - type tc_ctx = { type_defs : type_def TypeDefId.Map.t } + type tc_ctx = { type_decls : type_decl TypeDeclId.Map.t } let check_constant_value (ty : ty) (v : constant_value) : unit = match (ty, v) with @@ -290,8 +290,8 @@ module TypeCheck = struct tys | Adt (AdtId def_id, tys) -> (* "Regular" ADT *) - let def = TypeDefId.Map.find def_id ctx.type_defs in - type_def_get_instantiated_fields_types def variant_id tys + let def = TypeDeclId.Map.find def_id ctx.type_decls in + type_decl_get_instantiated_fields_types def variant_id tys | Adt (Assumed aty, tys) -> ( (* Assumed type *) match aty with diff --git a/src/Substitute.ml b/src/Substitute.ml index 62822785..4a1f42eb 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -102,7 +102,7 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) : (** Instantiate the type variables in an ADT definition, and return, for every variant, the list of the types of its fields *) -let type_def_get_instantiated_variants_fields_rtypes (def : T.type_def) +let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl) (regions : T.RegionId.id T.region list) (types : T.rty list) : (T.VariantId.id option * T.rty list) list = let r_subst = @@ -130,7 +130,7 @@ let type_def_get_instantiated_variants_fields_rtypes (def : T.type_def) (** Instantiate the type variables in an ADT definition, and return the list of types of the fields for the chosen variant *) -let type_def_get_instantiated_field_rtypes (def : T.type_def) +let type_decl_get_instantiated_field_rtypes (def : T.type_decl) (opt_variant_id : T.VariantId.id option) (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list = let r_subst = @@ -141,16 +141,16 @@ let type_def_get_instantiated_field_rtypes (def : T.type_def) let ty_subst = make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types in - let fields = TU.type_def_get_fields def opt_variant_id in + let fields = TU.type_decl_get_fields def opt_variant_id in List.map (fun f -> ty_substitute r_subst ty_subst f.T.field_ty) fields (** Return the types of the properly instantiated ADT's variant, provided a context *) let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx) - (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) + (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list = - let def = C.ctx_lookup_type_def ctx def_id in - type_def_get_instantiated_field_rtypes def opt_variant_id regions types + let def = C.ctx_lookup_type_decl ctx def_id in + type_decl_get_instantiated_field_rtypes def opt_variant_id regions types (** Return the types of the properly instantiated ADT value (note that here, ADT is understood in its broad meaning: ADT, assumed value or tuple) *) @@ -181,12 +181,12 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx) (** Instantiate the type variables in an ADT definition, and return the list of types of the fields for the chosen variant *) -let type_def_get_instantiated_field_etypes (def : T.type_def) +let type_decl_get_instantiated_field_etypes (def : T.type_decl) (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list = let ty_subst = make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types in - let fields = TU.type_def_get_fields def opt_variant_id in + let fields = TU.type_decl_get_fields def opt_variant_id in List.map (fun f -> erase_regions_substitute_types ty_subst f.T.field_ty) fields @@ -194,10 +194,10 @@ let type_def_get_instantiated_field_etypes (def : T.type_def) (** Return the types of the properly instantiated ADT's variant, provided a context *) let ctx_adt_get_instantiated_field_etypes (ctx : C.eval_ctx) - (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) + (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list = - let def = C.ctx_lookup_type_def ctx def_id in - type_def_get_instantiated_field_etypes def opt_variant_id types + let def = C.ctx_lookup_type_decl ctx def_id in + type_decl_get_instantiated_field_etypes def opt_variant_id types (** Apply a type substitution to a place *) let place_substitute (_tsubst : T.TypeVarId.id -> T.ety) (p : E.place) : E.place @@ -320,8 +320,8 @@ and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety) (** Apply a type substitution to a function body. Return the local variables and the body. *) -let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety) - (def : A.fun_def) : A.var list * A.statement = +let fun_decl_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety) + (def : A.fun_decl) : A.var list * A.statement = let rsubst r = r in let locals = List.map diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 7f747a74..8f1eeb39 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -41,8 +41,8 @@ type config = { } type type_context = { - cfim_type_defs : T.type_def TypeDefId.Map.t; - type_defs : type_def TypeDefId.Map.t; + cfim_type_decls : T.type_decl TypeDeclId.Map.t; + type_decls : type_decl TypeDeclId.Map.t; (** We use this for type-checking (for sanity checks) when translating values and functions. This map is empty when we translate the types, then contains all @@ -66,7 +66,7 @@ type fun_sig_named_outputs = { } type fun_context = { - cfim_fun_defs : A.fun_def FunDefId.Map.t; + cfim_fun_decls : A.fun_decl FunDeclId.Map.t; fun_sigs : fun_sig_named_outputs RegularFunIdMap.t; (** *) } @@ -83,7 +83,7 @@ type call_info = { type bs_ctx = { type_context : type_context; fun_context : fun_context; - fun_def : A.fun_def; + fun_decl : A.fun_decl; bid : T.RegionGroupId.id option; (** TODO: rename *) ret_ty : ty; (** The return type - we use it to translate `Panic` *) sv_to_var : var V.SymbolicValueId.Map.t; @@ -106,34 +106,34 @@ type bs_ctx = { (** Body synthesis context *) let type_check_rvalue (ctx : bs_ctx) (v : typed_rvalue) : unit = - let ctx = { TypeCheck.type_defs = ctx.type_context.type_defs } in + let ctx = { TypeCheck.type_decls = ctx.type_context.type_decls } in TypeCheck.check_typed_rvalue ctx v let type_check_lvalue (ctx : bs_ctx) (v : typed_lvalue) : unit = - let ctx = { TypeCheck.type_defs = ctx.type_context.type_defs } in + let ctx = { TypeCheck.type_decls = ctx.type_context.type_decls } in TypeCheck.check_typed_lvalue ctx v (* TODO: move *) let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter = - Print.CfimAst.fun_def_to_ast_formatter ctx.type_context.cfim_type_defs - ctx.fun_context.cfim_fun_defs ctx.fun_def + Print.CfimAst.fun_decl_to_ast_formatter ctx.type_context.cfim_type_decls + ctx.fun_context.cfim_fun_decls ctx.fun_decl let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter = - let type_params = ctx.fun_def.signature.type_params in - let type_defs = ctx.type_context.cfim_type_defs in - let fun_defs = ctx.fun_context.cfim_fun_defs in - PrintPure.mk_ast_formatter type_defs fun_defs type_params + let type_params = ctx.fun_decl.signature.type_params in + let type_decls = ctx.type_context.cfim_type_decls in + let fun_decls = ctx.fun_context.cfim_fun_decls in + PrintPure.mk_ast_formatter type_decls fun_decls type_params let ty_to_string (ctx : bs_ctx) (ty : ty) : string = let fmt = bs_ctx_to_pp_ast_formatter ctx in let fmt = PrintPure.ast_to_type_formatter fmt in PrintPure.ty_to_string fmt ty -let type_def_to_string (ctx : bs_ctx) (def : type_def) : string = +let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = let type_params = def.type_params in - let type_defs = ctx.type_context.cfim_type_defs in - let fmt = PrintPure.mk_type_formatter type_defs type_params in - PrintPure.type_def_to_string fmt def + let type_decls = ctx.type_context.cfim_type_decls in + let fmt = PrintPure.mk_type_formatter type_decls type_params in + PrintPure.type_decl_to_string fmt def let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string = let fmt = bs_ctx_to_pp_ast_formatter ctx in @@ -141,17 +141,17 @@ let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string = let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string = let type_params = sg.type_params in - let type_defs = ctx.type_context.cfim_type_defs in - let fun_defs = ctx.fun_context.cfim_fun_defs in - let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in + let type_decls = ctx.type_context.cfim_type_decls in + let fun_decls = ctx.fun_context.cfim_fun_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in PrintPure.fun_sig_to_string fmt sg -let fun_def_to_string (ctx : bs_ctx) (def : Pure.fun_def) : string = +let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = let type_params = def.signature.type_params in - let type_defs = ctx.type_context.cfim_type_defs in - let fun_defs = ctx.fun_context.cfim_fun_defs in - let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in - PrintPure.fun_def_to_string fmt def + let type_decls = ctx.type_context.cfim_type_decls in + let fun_decls = ctx.fun_context.cfim_fun_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in + PrintPure.fun_decl_to_string fmt def (* TODO: move *) let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = @@ -173,15 +173,15 @@ let get_instantiated_fun_sig (fun_id : A.fun_id) (* Apply *) fun_sig_substitute tsubst sg -let bs_ctx_lookup_cfim_type_def (id : TypeDefId.id) (ctx : bs_ctx) : T.type_def +let bs_ctx_lookup_cfim_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl = - TypeDefId.Map.find id ctx.type_context.cfim_type_defs + TypeDeclId.Map.find id ctx.type_context.cfim_type_decls -let bs_ctx_lookup_cfim_fun_def (id : FunDefId.id) (ctx : bs_ctx) : A.fun_def = - FunDefId.Map.find id ctx.fun_context.cfim_fun_defs +let bs_ctx_lookup_cfim_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl = + FunDeclId.Map.find id ctx.fun_context.cfim_fun_decls (* TODO: move *) -let bs_ctx_lookup_local_function_sig (def_id : FunDefId.id) +let bs_ctx_lookup_local_function_sig (def_id : FunDeclId.id) (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig = let id = (A.Local def_id, back_id) in (RegularFunIdMap.find id ctx.fun_context.fun_sigs).sg @@ -264,7 +264,7 @@ let translate_variants (vl : T.variant list) : variant list = List.map translate_variant vl (** Translate a type def kind to IM *) -let translate_type_def_kind (kind : T.type_def_kind) : type_def_kind = +let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind = match kind with | T.Struct fields -> Struct (translate_fields fields) | T.Enum variants -> Enum (translate_variants variants) @@ -274,14 +274,14 @@ let translate_type_def_kind (kind : T.type_def_kind) : type_def_kind = TODO: this is not symbolic to pure but IM to pure. Still, I don't see the point of moving this definition for now. *) -let translate_type_def (def : T.type_def) : type_def = +let translate_type_decl (def : T.type_decl) : type_decl = (* Translate *) let def_id = def.T.def_id in let name = def.name in (* Can't translate types with regions for now *) assert (def.region_params = []); let type_params = def.type_params in - let kind = translate_type_def_kind def.T.kind in + let kind = translate_type_decl_kind def.T.kind in { def_id; name; type_params; kind } (** Translate a type, seen as an input/output of a forward function @@ -1292,8 +1292,8 @@ and translate_expansion (config : config) (p : S.mplace option) match type_id with | T.AdtId adt_id -> (* Detect if this is an enumeration or not *) - let tdef = bs_ctx_lookup_cfim_type_def adt_id ctx in - let is_enum = type_def_is_enum tdef in + let tdef = bs_ctx_lookup_cfim_type_decl adt_id ctx in + let is_enum = type_decl_is_enum tdef in if is_enum then (* This is an enumeration: introduce an [ExpandEnum] let-binding *) let variant_id = Option.get variant_id in @@ -1441,13 +1441,13 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression) let ty = next_e.ty in { e; ty } -let translate_fun_def (config : config) (ctx : bs_ctx) (body : S.expression) : - fun_def = - let def = ctx.fun_def in +let translate_fun_decl (config : config) (ctx : bs_ctx) (body : S.expression) : + fun_decl = + let def = ctx.fun_decl in let bid = ctx.bid in log#ldebug (lazy - ("SymbolicToPure.translate_fun_def: " + ("SymbolicToPure.translate_fun_decl: " ^ Print.fun_name_to_string def.A.name ^ " (" ^ Print.option_to_string T.RegionGroupId.to_string bid @@ -1485,13 +1485,13 @@ let translate_fun_def (config : config) (ctx : bs_ctx) (body : S.expression) : (* Debugging *) log#ldebug (lazy - ("SymbolicToPure.translate_fun_def: translated:\n" - ^ fun_def_to_string ctx def)); + ("SymbolicToPure.translate_fun_decl: translated:\n" + ^ fun_decl_to_string ctx def)); (* return *) def -let translate_type_defs (type_defs : T.type_def list) : type_def list = - List.map translate_type_def type_defs +let translate_type_decls (type_decls : T.type_decl list) : type_decl list = + List.map translate_type_decl type_decls (** Translates function signatures. diff --git a/src/Translate.ml b/src/Translate.ml index 9b651288..3b42d13c 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -51,7 +51,7 @@ type symbolic_fun_translation = V.symbolic_value list * SA.expression for the forward function and the backward functions. *) let translate_function_to_symbolics (config : C.partial_config) - (trans_ctx : trans_ctx) (fdef : A.fun_def) : + (trans_ctx : trans_ctx) (fdef : A.fun_decl) : symbolic_fun_translation * symbolic_fun_translation list = (* Debug *) log#ldebug @@ -91,7 +91,7 @@ let translate_function_to_symbolics (config : C.partial_config) let translate_function_to_pure (config : C.partial_config) (mp_config : Micro.config) (trans_ctx : trans_ctx) (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t) - (pure_type_defs : Pure.type_def Pure.TypeDefId.Map.t) (fdef : A.fun_def) : + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) : pure_fun_translation = (* Debug *) log#ldebug @@ -122,12 +122,12 @@ let translate_function_to_pure (config : C.partial_config) let type_context = { SymbolicToPure.types_infos = type_context.type_infos; - cfim_type_defs = type_context.type_defs; - type_defs = pure_type_defs; + cfim_type_decls = type_context.type_decls; + type_decls = pure_type_decls; } in let fun_context = - { SymbolicToPure.cfim_fun_defs = fun_context.fun_defs; fun_sigs } + { SymbolicToPure.cfim_fun_decls = fun_context.fun_decls; fun_sigs } in let ctx = { @@ -139,7 +139,7 @@ let translate_function_to_pure (config : C.partial_config) var_counter; type_context; fun_context; - fun_def = fdef; + fun_decl = fdef; forward_inputs = []; (* Empty for now *) backward_inputs = T.RegionGroupId.Map.empty; @@ -152,7 +152,7 @@ let translate_function_to_pure (config : C.partial_config) in (* We need to initialize the input/output variables *) - let forward_input_vars = CfimAstUtils.fun_def_get_input_vars fdef in + let forward_input_vars = CfimAstUtils.fun_decl_get_input_vars fdef in let forward_input_varnames = List.map (fun (v : A.var) -> v.name) forward_input_vars in @@ -175,13 +175,13 @@ let translate_function_to_pure (config : C.partial_config) (* Translate the forward function *) let pure_forward = - SymbolicToPure.translate_fun_def sp_config + SymbolicToPure.translate_fun_decl sp_config (add_forward_inputs (fst symbolic_forward) ctx) (snd symbolic_forward) in (* Translate the backward functions *) - let translate_backward (rg : T.region_var_group) : Pure.fun_def = + let translate_backward (rg : T.region_var_group) : Pure.fun_decl = (* For the backward inputs/outputs initialization: we use the fact that * there are no nested borrows for now, and so that the region groups * can't have parents *) @@ -235,7 +235,7 @@ let translate_function_to_pure (config : C.partial_config) in (* Translate *) - SymbolicToPure.translate_fun_def sp_config ctx symbolic + SymbolicToPure.translate_fun_decl sp_config ctx symbolic in let pure_backwards = List.map translate_backward fdef.signature.regions_hierarchy @@ -246,7 +246,7 @@ let translate_function_to_pure (config : C.partial_config) let translate_module_to_pure (config : C.partial_config) (mp_config : Micro.config) (m : M.cfim_module) : - trans_ctx * Pure.type_def list * (bool * pure_fun_translation) list = + trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list = (* Debug *) log#ldebug (lazy "translate_module_to_pure"); @@ -255,12 +255,12 @@ let translate_module_to_pure (config : C.partial_config) let trans_ctx = { type_context; fun_context } in (* Translate all the type definitions *) - let type_defs = SymbolicToPure.translate_type_defs m.types in + let type_decls = SymbolicToPure.translate_type_decls m.types in (* Compute the type definition map *) - let type_defs_map = - Pure.TypeDefId.Map.of_list - (List.map (fun (def : Pure.type_def) -> (def.def_id, def)) type_defs) + let type_decls_map = + Pure.TypeDeclId.Map.of_list + (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls) in (* Translate all the function *signatures* *) @@ -272,11 +272,11 @@ let translate_module_to_pure (config : C.partial_config) in let local_sigs = List.map - (fun (fdef : A.fun_def) -> + (fun (fdef : A.fun_decl) -> ( A.Local fdef.def_id, List.map (fun (v : A.var) -> v.name) - (CfimAstUtils.fun_def_get_input_vars fdef), + (CfimAstUtils.fun_decl_get_input_vars fdef), fdef.signature )) m.functions in @@ -289,7 +289,7 @@ let translate_module_to_pure (config : C.partial_config) let pure_translations = List.map (translate_function_to_pure config mp_config trans_ctx fun_sigs - type_defs_map) + type_decls_map) m.functions in @@ -301,14 +301,14 @@ let translate_module_to_pure (config : C.partial_config) in (* Return *) - (trans_ctx, type_defs, pure_translations) + (trans_ctx, type_decls, pure_translations) type gen_ctx = { m : M.cfim_module; extract_ctx : PureToExtract.extraction_ctx; - trans_types : Pure.type_def Pure.TypeDefId.Map.t; - trans_funs : (bool * pure_fun_translation) Pure.FunDefId.Map.t; - functions_with_decreases_clause : Pure.FunDefId.Set.t; + trans_types : Pure.type_decl Pure.TypeDeclId.Map.t; + trans_funs : (bool * pure_fun_translation) Pure.FunDeclId.Map.t; + functions_with_decreases_clause : Pure.FunDeclId.Set.t; } (** Extraction context *) @@ -316,7 +316,7 @@ type gen_config = { extract_types : bool; extract_decreases_clauses : bool; extract_template_decreases_clauses : bool; - extract_fun_defs : bool; + extract_fun_decls : bool; test_unit_functions : bool; } @@ -327,15 +327,15 @@ type gen_config = { let extract_definitions (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) : unit = (* Export the definition groups to the file, in the proper order *) - let export_type (qualif : ExtractToFStar.type_def_qualif) - (id : Pure.TypeDefId.id) : unit = - let def = Pure.TypeDefId.Map.find id ctx.trans_types in - ExtractToFStar.extract_type_def ctx.extract_ctx fmt qualif def + let export_type (qualif : ExtractToFStar.type_decl_qualif) + (id : Pure.TypeDeclId.id) : unit = + let def = Pure.TypeDeclId.Map.find id ctx.trans_types in + ExtractToFStar.extract_type_decl ctx.extract_ctx fmt qualif def in (* Utility to check a function has a decrease clause *) - let has_decreases_clause (def : Pure.fun_def) : bool = - Pure.FunDefId.Set.mem def.def_id ctx.functions_with_decreases_clause + let has_decreases_clause (def : Pure.fun_decl) : bool = + Pure.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause in (* In case of (non-mutually) recursive functions, we use a simple procedure to @@ -364,7 +364,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) fwd) pure_ls; (* Extract the function definitions *) - (if config.extract_fun_defs then + (if config.extract_fun_decls then (* Check if the functions are mutually recursive - this really works * to check if the forward and backward translations of a single * recursive function are mutually recursive *) @@ -386,7 +386,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) let has_decr_clause = has_decreases_clause def && config.extract_decreases_clauses in - ExtractToFStar.extract_fun_def ctx.extract_ctx fmt qualif + ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause fwd_def def) fls); (* Insert unit tests if necessary *) @@ -413,14 +413,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) ids | Fun (NonRec id) -> (* Lookup *) - let pure_fun = Pure.FunDefId.Map.find id ctx.trans_funs in + let pure_fun = Pure.FunDeclId.Map.find id ctx.trans_funs in (* Translate *) export_functions false [ pure_fun ] | Fun (Rec ids) -> (* General case of mutually recursive functions *) (* Lookup *) let pure_funs = - List.map (fun id -> Pure.FunDefId.Map.find id ctx.trans_funs) ids + List.map (fun id -> Pure.FunDeclId.Map.find id ctx.trans_funs) ids in (* Translate *) export_functions true pure_funs @@ -494,7 +494,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* We need to compute which functions are recursive, in order to know * whether we should generate a decrease clause or not. *) let rec_functions = - Pure.FunDefId.Set.of_list + Pure.FunDeclId.Set.of_list (List.concat (List.map (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> []) @@ -507,7 +507,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) * sure there are no name clashes. *) let ctx = List.fold_left - (fun ctx def -> ExtractToFStar.extract_type_def_register_names ctx def) + (fun ctx def -> ExtractToFStar.extract_type_decl_register_names ctx def) ctx trans_types in @@ -516,9 +516,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (fun ctx (keep_fwd, def) -> (* Note that we generate a decrease clause for all the recursive functions *) let gen_decr_clause = - Pure.FunDefId.Set.mem (fst def).Pure.def_id rec_functions + Pure.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions in - ExtractToFStar.extract_fun_def_register_names ctx keep_fwd + ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause def) ctx trans_funs in @@ -542,11 +542,11 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* Put the translated definitions in maps *) let trans_types = - Pure.TypeDefId.Map.of_list - (List.map (fun (d : Pure.type_def) -> (d.def_id, d)) trans_types) + Pure.TypeDeclId.Map.of_list + (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types) in let trans_funs = - Pure.FunDefId.Map.of_list + Pure.FunDeclId.Map.of_list (List.map (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) -> (fd.def_id, (keep_fwd, (fd, bdl)))) @@ -571,7 +571,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) extract_types = false; extract_decreases_clauses = config.extract_decreases_clauses; extract_template_decreases_clauses = false; - extract_fun_defs = false; + extract_fun_decls = false; test_unit_functions = false; } in @@ -603,7 +603,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) let fun_config = { base_gen_config with - extract_fun_defs = true; + extract_fun_decls = true; test_unit_functions = config.test_unit_functions; } in @@ -618,7 +618,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) extract_decreases_clauses = config.extract_decreases_clauses; extract_template_decreases_clauses = config.extract_template_decreases_clauses; - extract_fun_defs = true; + extract_fun_decls = true; test_unit_functions = config.test_unit_functions; } in diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index f74b552b..3a22d388 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -12,34 +12,34 @@ let log = L.translate_log type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context } -type pure_fun_translation = Pure.fun_def * Pure.fun_def list +type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list -let type_def_to_string (ctx : trans_ctx) (def : Pure.type_def) : string = +let type_decl_to_string (ctx : trans_ctx) (def : Pure.type_decl) : string = let type_params = def.type_params in - let type_defs = ctx.type_context.type_defs in - let fmt = PrintPure.mk_type_formatter type_defs type_params in - PrintPure.type_def_to_string fmt def + let type_decls = ctx.type_context.type_decls in + let fmt = PrintPure.mk_type_formatter type_decls type_params in + PrintPure.type_decl_to_string fmt def -let type_id_to_string (ctx : trans_ctx) (def : Pure.type_def) : string = +let type_id_to_string (ctx : trans_ctx) (def : Pure.type_decl) : string = let type_params = def.type_params in - let type_defs = ctx.type_context.type_defs in - let fmt = PrintPure.mk_type_formatter type_defs type_params in - PrintPure.type_def_to_string fmt def + let type_decls = ctx.type_context.type_decls in + let fmt = PrintPure.mk_type_formatter type_decls type_params in + PrintPure.type_decl_to_string fmt def let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = let type_params = sg.type_params in - let type_defs = ctx.type_context.type_defs in - let fun_defs = ctx.fun_context.fun_defs in - let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in + let type_decls = ctx.type_context.type_decls in + let fun_decls = ctx.fun_context.fun_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in PrintPure.fun_sig_to_string fmt sg -let fun_def_to_string (ctx : trans_ctx) (def : Pure.fun_def) : string = +let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let type_params = def.signature.type_params in - let type_defs = ctx.type_context.type_defs in - let fun_defs = ctx.fun_context.fun_defs in - let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in - PrintPure.fun_def_to_string fmt def + let type_decls = ctx.type_context.type_decls in + let fun_decls = ctx.fun_context.fun_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in + PrintPure.fun_decl_to_string fmt def -let fun_def_id_to_string (ctx : trans_ctx) (id : Pure.FunDefId.id) : string = +let fun_decl_id_to_string (ctx : trans_ctx) (id : Pure.FunDeclId.id) : string = Print.fun_name_to_string - (Pure.FunDefId.Map.find id ctx.fun_context.fun_defs).name + (Pure.FunDeclId.Map.find id ctx.fun_context.fun_decls).name diff --git a/src/Types.ml b/src/Types.ml index b099e7a5..6393e0d8 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -2,7 +2,7 @@ open Identifiers module TypeVarId = IdGen () -module TypeDefId = IdGen () +module TypeDeclId = IdGen () module VariantId = IdGen () @@ -101,7 +101,7 @@ let option_some_id = VariantId.of_int 1 ADTs are very general in our encoding: they account for "regular" ADTs, tuples and also assumed types. *) -type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty +type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty [@@deriving show, ord] (** Ancestor for iter visitor for [ty] *) @@ -198,15 +198,15 @@ type field = { field_name : string option; field_ty : sty } [@@deriving show] type variant = { variant_name : string; fields : field list } [@@deriving show] -type type_def_kind = Struct of field list | Enum of variant list +type type_decl_kind = Struct of field list | Enum of variant list [@@deriving show] -type type_def = { - def_id : TypeDefId.id; +type type_decl = { + def_id : TypeDeclId.id; name : type_name; region_params : region_var list; type_params : type_var list; - kind : type_def_kind; + kind : type_decl_kind; regions_hierarchy : region_var_groups; (** Stores the hierarchy between the regions (which regions have the same lifetime, which lifetime should end before which other lifetime, diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml index 5429d709..d8895b55 100644 --- a/src/TypesAnalysis.ml +++ b/src/TypesAnalysis.ml @@ -8,7 +8,7 @@ type subtype_info = { [@@deriving show] type type_param_info = subtype_info [@@deriving show] -(** See [type_def_info] *) +(** See [type_decl_info] *) type expl_info = subtype_info [@@deriving show] @@ -31,7 +31,7 @@ type 'p g_type_info = { [@@deriving show] (** Generic definition *) -type type_def_info = type_param_info list g_type_info [@@deriving show] +type type_decl_info = type_param_info list g_type_info [@@deriving show] (** Information about a type definition. *) type ty_info = type_borrows_info [@@deriving show] @@ -44,7 +44,7 @@ type partial_type_info = type_param_info list option g_type_info Allows us to factorize code: [analyze_full_ty] is used both to analyze type definitions and types. *) -type type_infos = type_def_info TypeDefId.Map.t [@@deriving show] +type type_infos = type_decl_info TypeDeclId.Map.t [@@deriving show] let expl_info_init = { under_borrow = false; under_mut_borrow = false } @@ -59,17 +59,17 @@ let type_borrows_info_init : type_borrows_info = let initialize_g_type_info (param_infos : 'p) : 'p g_type_info = { borrows_info = type_borrows_info_init; param_infos } -let initialize_type_def_info (def : type_def) : type_def_info = +let initialize_type_decl_info (def : type_decl) : type_decl_info = let param_info = { under_borrow = false; under_mut_borrow = false } in let param_infos = List.map (fun _ -> param_info) def.type_params in initialize_g_type_info param_infos -let type_def_info_to_partial_type_info (info : type_def_info) : +let type_decl_info_to_partial_type_info (info : type_decl_info) : partial_type_info = { borrows_info = info.borrows_info; param_infos = Some info.param_infos } -let partial_type_info_to_type_def_info (info : partial_type_info) : - type_def_info = +let partial_type_info_to_type_decl_info (info : partial_type_info) : + type_decl_info = { borrows_info = info.borrows_info; param_infos = Option.get info.param_infos; @@ -179,7 +179,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref) ty_info tys | Adt (AdtId adt_id, regions, tys) -> (* Lookup the information for this type definition *) - let adt_info = TypeDefId.Map.find adt_id infos in + let adt_info = TypeDeclId.Map.find adt_id infos in (* Update the type info with the information from the adt *) let ty_info = update_ty_info ty_info adt_info.borrows_info in (* Check if 'static appears in the region parameters *) @@ -238,8 +238,8 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref) (* Explore *) analyze expl_info_init ty_info ty -let analyze_type_def (updated : bool ref) (infos : type_infos) (def : type_def) - : type_infos = +let analyze_type_decl (updated : bool ref) (infos : type_infos) + (def : type_decl) : type_infos = (* Retrieve all the types of all the fields of all the variants *) let fields_tys : sty list = match def.kind with @@ -250,31 +250,31 @@ let analyze_type_def (updated : bool ref) (infos : type_infos) (def : type_def) in (* Explore the types and accumulate information *) let r_is_static r = r = Static in - let type_def_info = TypeDefId.Map.find def.def_id infos in - let type_def_info = type_def_info_to_partial_type_info type_def_info in - let type_def_info = + let type_decl_info = TypeDeclId.Map.find def.def_id infos in + let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in + let type_decl_info = List.fold_left - (fun type_def_info ty -> - analyze_full_ty r_is_static updated infos type_def_info ty) - type_def_info fields_tys + (fun type_decl_info ty -> + analyze_full_ty r_is_static updated infos type_decl_info ty) + type_decl_info fields_tys in - let type_def_info = partial_type_info_to_type_def_info type_def_info in + let type_decl_info = partial_type_info_to_type_decl_info type_decl_info in (* Update the information for the type definition we explored *) - let infos = TypeDefId.Map.add def.def_id type_def_info infos in + let infos = TypeDeclId.Map.add def.def_id type_decl_info infos in (* Return *) infos -let analyze_type_declaration_group (type_defs : type_def TypeDefId.Map.t) +let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t) (infos : type_infos) (decl : type_declaration_group) : type_infos = (* Collect the identifiers used in the declaration group *) let ids = match decl with NonRec id -> [ id ] | Rec ids -> ids in (* Retrieve the type definitions *) - let decl_defs = List.map (fun id -> TypeDefId.Map.find id type_defs) ids in + let decl_defs = List.map (fun id -> TypeDeclId.Map.find id type_decls) ids in (* Initialize the type information for the current definitions *) let infos = List.fold_left (fun infos def -> - TypeDefId.Map.add def.def_id (initialize_type_def_info def) infos) + TypeDeclId.Map.add def.def_id (initialize_type_decl_info def) infos) infos decl_defs in (* Analyze the types - this function simply computes a fixed-point *) @@ -282,7 +282,7 @@ let analyze_type_declaration_group (type_defs : type_def TypeDefId.Map.t) let rec analyze (infos : type_infos) : type_infos = let infos = List.fold_left - (fun infos def -> analyze_type_def updated infos def) + (fun infos def -> analyze_type_decl updated infos def) infos decl_defs in if !updated then ( @@ -298,11 +298,11 @@ let analyze_type_declaration_group (type_defs : type_def TypeDefId.Map.t) Rk.: pay attention to the difference between type definitions and types! *) -let analyze_type_declarations (type_defs : type_def TypeDefId.Map.t) +let analyze_type_declarations (type_decls : type_decl TypeDeclId.Map.t) (decls : type_declaration_group list) : type_infos = List.fold_left - (fun infos decl -> analyze_type_declaration_group type_defs infos decl) - TypeDefId.Map.empty decls + (fun infos decl -> analyze_type_declaration_group type_decls infos decl) + TypeDeclId.Map.empty decls (** Analyze a type to check whether it contains borrows, etc., provided we have already analyzed the type definitions in the context. diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index db10ed47..e463fbc5 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -2,12 +2,12 @@ open Types open Utils module TA = TypesAnalysis -(** Retrieve the list of fields for the given variant of a [type_def]. +(** Retrieve the list of fields for the given variant of a [type_decl]. Raises [Invalid_argument] if the arguments are incorrect. *) -let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option) - : field list = +let type_decl_get_fields (def : type_decl) + (opt_variant_id : VariantId.id option) : field list = match (def.kind, opt_variant_id) with | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields | Struct fields, None -> fields @@ -19,7 +19,7 @@ let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option) (Invalid_argument ("The variant id should be [Some] if and only if the definition is \ an enumeration:\n\ - - def: " ^ show_type_def def ^ "\n- opt_variant_id: " + - def: " ^ show_type_decl def ^ "\n- opt_variant_id: " ^ opt_variant_id)) (** Return [true] if a [ty] is actually `unit` *) @@ -37,7 +37,7 @@ let ty_as_adt (ty : 'r ty) : type_id * 'r list * 'r ty list = let ty_is_custom_adt (ty : 'r ty) : bool = match ty with Adt (AdtId _, _, _) -> true | _ -> false -let ty_as_custom_adt (ty : 'r ty) : TypeDefId.id * 'r list * 'r ty list = +let ty_as_custom_adt (ty : 'r ty) : TypeDeclId.id * 'r list * 'r ty list = match ty with | Adt (AdtId id, regions, tys) -> (id, regions, tys) | _ -> failwith "Unreachable" |