diff options
Diffstat (limited to '')
31 files changed, 1258 insertions, 776 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml new file mode 100644 index 00000000..4e5625cb --- /dev/null +++ b/compiler/AssociatedTypes.ml @@ -0,0 +1,91 @@ +(** This file implements utilities to handle trait associated types, in + particular with normalization helpers. + + When normalizing a type, we simplify the references to the trait associated + types, and choose a representative when there are equalities between types + enforced by local clauses (i.e., clauses of the shape [where Trait1::T = Trait2::U]). + *) + +module T = Types +module TU = TypesUtils +module V = Values +module E = Expressions +module A = LlbcAst +module C = Contexts +module Subst = Substitute +module L = Logging + +(** The local logger *) +let log = L.associated_types_log + +(** Normalize a type by simplyfying the references to trait associated types + and choosing a representative when there are equalities between types + enforced by local clauses (i.e., `where Trait1::T = Trait2::U`. *) +let ctx_normalize_type (_ctx : C.eval_ctx) (_ty : 'r T.ty) : 'r T.ty = + raise (Failure "Unimplemented") + +(** Same as [type_decl_get_instantiated_variants_fields_rtypes] but normalizes the types *) +let type_decl_get_inst_norm_variants_fields_rtypes (ctx : C.eval_ctx) + (def : T.type_decl) (generics : T.rgeneric_args) : + (T.VariantId.id option * T.rty list) list = + let res = + Subst.type_decl_get_instantiated_variants_fields_rtypes def generics + in + List.map + (fun (variant_id, types) -> + (variant_id, List.map (ctx_normalize_type ctx) types)) + res + +(** Same as [type_decl_get_instantiated_field_rtypes] but normalizes the types *) +let type_decl_get_inst_norm_field_rtypes (ctx : C.eval_ctx) (def : T.type_decl) + (opt_variant_id : T.VariantId.id option) (generics : T.rgeneric_args) : + T.rty list = + let types = + Subst.type_decl_get_instantiated_field_rtypes def opt_variant_id generics + in + List.map (ctx_normalize_type ctx) types + +(** Same as [ctx_adt_value_get_instantiated_field_rtypes] but normalizes the types *) +let ctx_adt_value_get_inst_norm_field_rtypes (ctx : C.eval_ctx) + (adt : V.adt_value) (id : T.type_id) (generics : T.rgeneric_args) : + T.rty list = + let types = + Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id generics + in + List.map (ctx_normalize_type ctx) types + +(** Same as [ctx_adt_value_get_instantiated_field_etypes] but normalizes the types *) +let type_decl_get_inst_norm_field_etypes (ctx : C.eval_ctx) (def : T.type_decl) + (opt_variant_id : T.VariantId.id option) (generics : T.egeneric_args) : + T.ety list = + let types = + Subst.type_decl_get_instantiated_field_etypes def opt_variant_id generics + in + List.map (ctx_normalize_type ctx) types + +(** Same as [ctx_adt_get_instantiated_field_etypes] but normalizes the types *) +let ctx_adt_get_inst_norm_field_etypes (ctx : C.eval_ctx) + (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) + (generics : T.egeneric_args) : T.ety list = + let types = + Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id + generics + in + List.map (ctx_normalize_type ctx) types + +(** Same as [substitute_signature] but normalizes the types *) +let ctx_subst_norm_signature (ctx : C.eval_ctx) + (asubst : T.RegionGroupId.id -> V.AbstractionId.id) + (r_subst : T.RegionVarId.id -> T.RegionId.id) + (ty_subst : T.TypeVarId.id -> T.rty) + (cg_subst : T.ConstGenericVarId.id -> T.const_generic) + (tr_subst : T.TraitClauseId.id -> T.rtrait_instance_id) + (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = + let sg = + Subst.substitute_signature asubst r_subst ty_subst cg_subst tr_subst tr_self + sg + in + let { A.regions_hierarchy; inputs; output } = sg in + let inputs = List.map (ctx_normalize_type ctx) inputs in + let output = ctx_normalize_type ctx output in + { regions_hierarchy; inputs; output } diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 25462504..e156c335 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -63,75 +63,81 @@ module Sig = struct let empty_const_generic_params : T.const_generic_var list = [] + let mk_generic_args regions types const_generics : T.sgeneric_args = + { regions; types; const_generics; trait_refs = [] } + + let mk_generic_params regions types const_generics : T.generic_params = + { regions; types; const_generics; trait_clauses = [] } + let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) : T.sty = let ref_kind = if is_mut then T.Mut else T.Shared in mk_ref_ty r ty ref_kind let mk_array_ty (ty : T.sty) (cg : T.const_generic) : T.sty = - Adt (Assumed Array, [], [ ty ], [ cg ]) + Adt (Assumed Array, mk_generic_args [] [ ty ] [ cg ]) + + let mk_slice_ty (ty : T.sty) : T.sty = + Adt (Assumed Slice, mk_generic_args [] [ ty ] []) - let mk_slice_ty (ty : T.sty) : T.sty = Adt (Assumed Slice, [], [ ty ], []) - let range_ty : T.sty = Adt (Assumed Range, [], [ usize_ty ], []) + let range_ty : T.sty = Adt (Assumed Range, mk_generic_args [] [ usize_ty ] []) + + let mk_sig generics regions_hierarchy inputs output : A.fun_sig = + let preds : T.predicates = + { regions_outlive = []; types_outlive = []; trait_type_constraints = [] } + in + { + generics; + preds; + parent_params_info = None; + regions_hierarchy; + inputs; + output; + } (** [fn<T>(&'a mut T, T) -> T] *) let mem_replace_sig : A.fun_sig = (* The signature fields *) - let region_params = [ region_param_0 ] (* <'a> *) in + let regions = [ region_param_0 ] (* <'a> *) in let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in - let type_params = [ type_param_0 ] (* <T> *) in + let types = [ type_param_0 ] (* <T> *) in + let generics = mk_generic_params regions types [] in let inputs = [ mk_ref_ty rvar_0 tvar_0 true (* &'a mut T *); tvar_0 (* T *) ] in let output = tvar_0 (* T *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn<T>(T) -> Box<T>] *) let box_new_sig : A.fun_sig = - { - region_params = []; - regions_hierarchy = []; - type_params = [ type_param_0 ] (* <T> *); - const_generic_params = empty_const_generic_params; - inputs = [ tvar_0 (* T *) ]; - output = mk_box_ty tvar_0 (* Box<T> *); - } + let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in + let regions_hierarchy = [] in + let inputs = [ tvar_0 (* T *) ] in + let output = mk_box_ty tvar_0 (* Box<T> *) in + mk_sig generics regions_hierarchy inputs output (** [fn<T>(Box<T>) -> ()] *) let box_free_sig : A.fun_sig = - { - region_params = []; - regions_hierarchy = []; - type_params = [ type_param_0 ] (* <T> *); - const_generic_params = empty_const_generic_params; - inputs = [ mk_box_ty tvar_0 (* Box<T> *) ]; - output = mk_unit_ty (* () *); - } + let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in + let regions_hierarchy = [] in + let inputs = [ mk_box_ty tvar_0 (* Box<T> *) ] in + let output = mk_unit_ty (* () *) in + mk_sig generics regions_hierarchy inputs output (** Helper for [Box::deref_shared] and [Box::deref_mut]. Returns: [fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T] *) let box_deref_gen_sig (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - { - region_params; - regions_hierarchy; - type_params = [ type_param_0 ] (* <T> *); - const_generic_params = empty_const_generic_params; - inputs = - [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ]; - output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *); - } + let inputs = + [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ] + in + let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in + mk_sig generics regions_hierarchy inputs output (** [fn<'a, T>(&'a Box<T>) -> &'a T] *) let box_deref_shared_sig = box_deref_gen_sig false @@ -141,26 +147,18 @@ module Sig = struct (** [fn<T>() -> Vec<T>] *) let vec_new_sig : A.fun_sig = - let region_params = [] in + let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in let regions_hierarchy = [] in - let type_params = [ type_param_0 ] (* <T> *) in let inputs = [] in let output = mk_vec_ty tvar_0 (* Vec<T> *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn<T>(&'a mut Vec<T>, T)] *) let vec_push_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in let inputs = [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *); @@ -168,21 +166,14 @@ module Sig = struct ] in let output = mk_unit_ty (* () *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn<T>(&'a mut Vec<T>, usize, T)] *) let vec_insert_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in let inputs = [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *); @@ -191,42 +182,28 @@ module Sig = struct ] in let output = mk_unit_ty (* () *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn<T>(&'a Vec<T>) -> usize] *) let vec_len_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in let inputs = [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) false (* &'a Vec<T> *) ] in let output = mk_usize_ty (* usize *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** Helper: [fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T] *) let vec_index_gen_sig (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in let inputs = [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec<T> *); @@ -234,14 +211,7 @@ module Sig = struct ] in let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn<T>(&'a Vec<T>, usize) -> &'a T] *) let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false @@ -266,10 +236,10 @@ module Sig = struct let mk_array_slice_borrow_sig (cgs : T.const_generic_var list) (input_ty : T.TypeVarId.id -> T.sty) (index_ty : T.sty option) (output_ty : T.TypeVarId.id -> T.sty) (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in let inputs = [ mk_ref_ty rvar_0 @@ -285,14 +255,7 @@ module Sig = struct (output_ty type_param_0.index) is_mut (* &'a (mut) output_ty<T> *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = cgs; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig = (* Array<T, N> *) @@ -342,22 +305,15 @@ module Sig = struct [fn<T>(&'a [T]) -> usize] *) let slice_len_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* <T> *) in let inputs = [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ] in let output = mk_usize_ty (* usize *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output end type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 14b5d559..2d396924 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -255,11 +255,28 @@ type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show] type global_context = { global_decls : global_decl GlobalDeclId.Map.t } [@@deriving show] +type trait_decls_context = { trait_decls : trait_decl TraitDeclId.Map.t } +[@@deriving show] + +type trait_impls_context = { trait_impls : trait_impl TraitImplId.Map.t } +[@@deriving show] + +type decls_ctx = { + type_ctx : type_context; + fun_ctx : fun_context; + global_ctx : global_context; + trait_decls_ctx : trait_decls_context; + trait_impls_ctx : trait_impls_context; +} +[@@deriving show] + (** Evaluation context *) type eval_ctx = { type_context : type_context; fun_context : fun_context; global_context : global_context; + trait_decls_context : trait_decls_context; + trait_impls_context : trait_impls_context; region_groups : RegionGroupId.id list; type_vars : type_var list; const_generic_vars : const_generic_var list; @@ -267,6 +284,7 @@ type eval_ctx = { (** The map from const generic vars to their values. Those values can be symbolic values or concrete values (in the latter case: if we run in interpreter mode) *) + trait_clauses : etrait_ref list; env : env; ended_regions : RegionId.Set.t; } @@ -308,6 +326,12 @@ let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl = GlobalDeclId.Map.find gid ctx.global_context.global_decls +let ctx_lookup_trait_decl (ctx : eval_ctx) (id : TraitDeclId.id) : trait_decl = + TraitDeclId.Map.find id ctx.trait_decls_context.trait_decls + +let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl = + TraitImplId.Map.find id ctx.trait_impls_context.trait_impls + (** Retrieve a variable's value in the current frame *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = snd (env_lookup_var env vid) diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index b72fa078..f4406653 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -70,14 +70,14 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_rvalue _env rv = match rv with - | Use _ | Ref _ | Global _ | Discriminant _ | Aggregate _ -> () + | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ -> () | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail | BinaryOp (bop, _, _) -> can_fail := EU.binop_can_fail bop || !can_fail method! visit_Call env call = (match call.func with - | Regular id -> + | FunId (Regular id) -> if FunDeclId.Set.mem id fun_ids then ( can_diverge := true; is_rec := true) @@ -86,9 +86,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) self#may_fail info.can_fail; stateful := !stateful || info.stateful; can_diverge := !can_diverge || info.can_diverge - | Assumed id -> + | FunId (Assumed id) -> (* None of the assumed functions can diverge nor are considered stateful *) - can_fail := !can_fail || Assumed.assumed_can_fail id); + can_fail := !can_fail || Assumed.assumed_can_fail id + | TraitMethod _ -> + (* We consider trait functions can fail, diverge, and are not stateful *) + can_fail := true; + can_diverge := true); super#visit_Call env call method! visit_Panic env = @@ -141,7 +145,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let rec analyze_decl_groups (decls : declaration_group list) : unit = match decls with | [] -> () - | Type _ :: decls' -> analyze_decl_groups decls' + | (Type _ | TraitDecl _ | TraitImpl _) :: decls' -> + analyze_decl_groups decls' | Fun decl :: decls' -> analyze_fun_decl_group decl; analyze_decl_groups decls' diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 37eeb333..eb66013d 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -12,27 +12,30 @@ module SA = SymbolicAst (** The local logger *) let log = L.interpreter_log -let compute_type_fun_global_contexts (m : A.crate) : - C.type_context * C.fun_context * C.global_context = - let type_decls_list, _, _ = split_declarations m.declarations in +let compute_contexts (m : A.crate) : C.decls_ctx = + let type_decls_list, _, _, _, _ = split_declarations m.declarations in let type_decls = m.types in let fun_decls = m.functions in let global_decls = m.globals in - let type_decls_groups, _funs_defs_groups, _globals_defs_groups = + let trait_decls = m.trait_decls in + let trait_impls = m.trait_impls in + let type_decls_groups, _, _, _, _ = split_declarations_to_group_maps m.declarations in let type_infos = TypesAnalysis.analyze_type_declarations type_decls type_decls_list in - let type_context = { C.type_decls_groups; type_decls; type_infos } in - let fun_context = { C.fun_decls } in - let global_context = { C.global_decls } in - (type_context, fun_context, global_context) - -let initialize_eval_context (type_context : C.type_context) - (fun_context : C.fun_context) (global_context : C.global_context) + let type_ctx = { C.type_decls_groups; type_decls; type_infos } in + let fun_ctx = { C.fun_decls } in + let global_ctx = { C.global_decls } in + let trait_decls_ctx = { C.trait_decls } in + let trait_impls_ctx = { C.trait_impls } in + { C.type_ctx; fun_ctx; global_ctx; trait_decls_ctx; trait_impls_ctx } + +let initialize_eval_context (ctx : C.decls_ctx) (region_groups : T.RegionGroupId.id list) (type_vars : T.type_var list) - (const_generic_vars : T.const_generic_var list) : C.eval_ctx = + (const_generic_vars : T.const_generic_var list) + (trait_clauses : T.etrait_ref list) : C.eval_ctx = C.reset_global_counters (); let const_generic_vars_map = T.ConstGenericVarId.Map.of_list @@ -44,33 +47,35 @@ let initialize_eval_context (type_context : C.type_context) const_generic_vars) in { - C.type_context; - C.fun_context; - C.global_context; + C.type_context = ctx.type_ctx; + C.fun_context = ctx.fun_ctx; + C.global_context = ctx.global_ctx; + C.trait_decls_context = ctx.trait_decls_ctx; + C.trait_impls_context = ctx.trait_impls_ctx; C.region_groups; C.type_vars; C.const_generic_vars; C.const_generic_vars_map; + C.trait_clauses; C.env = [ C.Frame ]; C.ended_regions = T.RegionId.Set.empty; } (** Initialize an evaluation context to execute a function. - Introduces local variables initialized in the following manner: - - input arguments are initialized as symbolic values - - the remaining locals are initialized as [⊥] - Abstractions are introduced for the regions present in the function - signature. - - We return: - - the initialized evaluation context - - the list of symbolic values introduced for the input values - - the instantiated function signature + Introduces local variables initialized in the following manner: + - input arguments are initialized as symbolic values + - the remaining locals are initialized as [⊥] + Abstractions are introduced for the regions present in the function + signature. + + We return: + - the initialized evaluation context + - the list of symbolic values introduced for the input values + - the instantiated function signature *) -let initialize_symbolic_context_for_fun (type_context : C.type_context) - (fun_context : C.fun_context) (global_context : C.global_context) - (fdef : A.fun_decl) : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig = +let initialize_symbolic_context_for_fun (ctx : C.decls_ctx) (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 * with the input values (which behave as if they had been returned @@ -88,8 +93,8 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) List.map (fun (g : T.region_var_group) -> g.id) sg.regions_hierarchy in let ctx = - initialize_eval_context type_context fun_context global_context - region_groups sg.type_params sg.const_generic_params + initialize_eval_context ctx region_groups sg.generics.types + sg.generics.const_generics sg.generics.trait_clauses in (* Instantiate the signature *) let type_params = @@ -508,17 +513,12 @@ module Test = struct (lazy ("test_unit_function: " ^ Print.fun_name_to_string fdef.A.name)); (* Sanity check - *) - assert (List.length fdef.A.signature.region_params = 0); - assert (List.length fdef.A.signature.type_params = 0); + assert (fdef.A.signature.generics = TypesUtils.mk_empty_generic_params); assert (body.A.arg_count = 0); (* Create the evaluation context *) - let type_context, fun_context, global_context = - compute_type_fun_global_contexts crate - in - let ctx = - initialize_eval_context type_context fun_context global_context [] [] [] - in + let decls_ctx = compute_contexts crate in + let ctx = initialize_eval_context decls_ctx [] [] [] [] in (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in @@ -546,9 +546,7 @@ module Test = struct (no parameters, no arguments) - TODO: move *) let fun_decl_is_transparent_unit (def : A.fun_decl) : bool = Option.is_some def.body - && def.A.signature.region_params = [] - && def.A.signature.type_params = [] - && def.A.signature.const_generic_params = [] + && def.A.signature.generics = TypesUtils.mk_empty_generic_params && def.A.signature.inputs = [] (** Test all the unit functions in a list of function definitions *) @@ -562,20 +560,4 @@ module Test = struct test_unit_function crate def.A.def_id in A.FunDeclId.Map.iter test_unit_fun unit_funs - - (** Execute the symbolic interpreter on a function. *) - let test_function_symbolic (synthesize : bool) (type_context : C.type_context) - (fun_context : C.fun_context) (global_context : C.global_context) - (fdef : A.fun_decl) : unit = - (* Debug *) - log#ldebug - (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name)); - - (* Evaluate *) - let _ = - evaluate_function_symbolic synthesize type_context fun_context - global_context fdef - in - - () end diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index bf083aa4..e7da045c 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -100,15 +100,18 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) (compare_regions : T.RegionId.id T.region -> T.RegionId.id T.region -> bool) (ty1 : T.rty) (ty2 : T.rty) : bool = let compare = compare_rtys default combine compare_regions in + (* Normalize the associated types *) match (ty1, ty2) with | T.Literal lit1, T.Literal lit2 -> assert (lit1 = lit2); default - | T.Adt (id1, regions1, tys1, cgs1), T.Adt (id2, regions2, tys2, cgs2) -> + | T.Adt (id1, generics1), T.Adt (id2, generics2) -> assert (id1 = id2); (* There are no regions in the const generics, so we ignore them, but we still check they are the same, for sanity *) - assert (cgs1 = cgs2); + assert (generics1.const_generics = generics2.const_generics); + + (* We also ignore the trait refs *) (* The check for the ADTs is very crude: we simply compare the arguments * two by two. @@ -123,14 +126,14 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) * this check would still be a reasonable conservative approximation. *) (* Check the region parameters *) - let regions = List.combine regions1 regions2 in + let regions = List.combine generics1.regions generics2.regions in let params_b = List.fold_left (fun b (r1, r2) -> combine b (compare_regions r1 r2)) default regions in (* Check the type parameters *) - let tys = List.combine tys1 tys2 in + let tys = List.combine generics1.types generics2.types in let tys_b = List.fold_left (fun b (ty1, ty2) -> combine b (compare ty1 ty2)) @@ -150,6 +153,11 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) | T.TypeVar id1, T.TypeVar id2 -> assert (id1 = id2); default + | T.TraitType _, T.TraitType _ -> + (* The types should have been normalized. If after normalization we + get trait types, we can consider them as variables *) + assert (ty1 = ty2); + default | _ -> log#lerror (lazy diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 81e73e3e..ea692386 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -9,6 +9,7 @@ module V = Values module E = Expressions module C = Contexts module Subst = Substitute +module Assoc = AssociatedTypes module L = Logging open TypesUtils module Inv = Invariants @@ -204,7 +205,7 @@ let apply_symbolic_expansion_non_borrow (config : C.config) apply_symbolic_expansion_to_avalues config allow_reborrows original_sv expansion ctx -(** Compute the expansion of a non-assumed (i.e.: not [Option], [Box], etc.) +(** Compute the expansion of a non-assumed (i.e.: not [Box], etc.) adt value. The function might return a list of values if the symbolic value to expand @@ -214,18 +215,15 @@ let apply_symbolic_expansion_non_borrow (config : C.config) doesn't allow the expansion of enumerations *containing several variants*. *) let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool) - (kind : V.sv_kind) (def_id : T.TypeDeclId.id) - (regions : T.RegionId.id T.region list) (types : T.rty list) - (cgs : T.const_generic list) (ctx : C.eval_ctx) : V.symbolic_expansion list - = + (kind : V.sv_kind) (def_id : T.TypeDeclId.id) (generics : T.rgeneric_args) + (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_decl ctx def_id in - assert (List.length regions = List.length def.T.region_params); + assert (List.length generics.regions = List.length def.T.generics.regions); (* Retrieve, for every variant, the list of its instantiated field types *) let variants_fields_types = - Subst.type_decl_get_instantiated_variants_fields_rtypes def regions types - cgs + Assoc.type_decl_get_inst_norm_variants_fields_rtypes ctx def generics in (* Check if there is strictly more than one variant *) if List.length variants_fields_types > 1 && not expand_enumerations then @@ -280,15 +278,14 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) : doesn't allow the expansion of enumerations *containing several variants*. *) let compute_expanded_symbolic_adt_value (expand_enumerations : bool) - (kind : V.sv_kind) (adt_id : T.type_id) - (regions : T.RegionId.id T.region list) (types : T.rty list) - (cgs : T.const_generic list) (ctx : C.eval_ctx) : V.symbolic_expansion list - = - match (adt_id, regions, types) with + (kind : V.sv_kind) (adt_id : T.type_id) (generics : T.rgeneric_args) + (ctx : C.eval_ctx) : V.symbolic_expansion list = + match (adt_id, generics.regions, generics.types) with | T.AdtId def_id, _, _ -> compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind - def_id regions types cgs ctx - | T.Tuple, [], _ -> [ compute_expanded_symbolic_tuple_value kind types ] + def_id generics ctx + | T.Tuple, [], _ -> + [ compute_expanded_symbolic_tuple_value kind generics.types ] | T.Assumed T.Option, [], [ ty ] -> compute_expanded_symbolic_option_value expand_enumerations kind ty | T.Assumed T.Box, [], [ boxed_ty ] -> @@ -543,12 +540,12 @@ let expand_symbolic_value_no_branching (config : C.config) fun cf ctx -> match rty with (* ADTs *) - | T.Adt (adt_id, regions, types, cgs) -> + | T.Adt (adt_id, generics) -> (* Compute the expanded value *) let allow_branching = false in let seel = compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id - regions types cgs ctx + generics ctx in (* There should be exacly one branch *) let see = Collections.List.to_cons_nil seel in @@ -600,12 +597,12 @@ let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value) (* Execute *) match rty with (* ADTs *) - | T.Adt (adt_id, regions, types, cgs) -> + | T.Adt (adt_id, generics) -> let allow_branching = true in (* Compute the expanded value *) let seel = compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id - regions types cgs ctx + generics ctx in (* Apply *) let seel = List.map (fun see -> (Some see, cf_branches)) seel in @@ -679,7 +676,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = ^ symbolic_value_to_string ctx sv)); let cc : cm_fun = match sv.V.sv_ty with - | T.Adt (AdtId def_id, _, _, _) -> + | T.Adt (AdtId def_id, _) -> (* {!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 *) @@ -704,16 +701,16 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = [config]): " ^ Print.name_to_string def.name)) else expand_symbolic_value_no_branching config sv None - | T.Adt ((Tuple | Assumed Box), _, _, _) | T.Ref (_, _, _) -> + | T.Adt ((Tuple | Assumed Box), _) | T.Ref (_, _, _) -> (* Ok *) expand_symbolic_value_no_branching config sv None - | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _, _, _) - -> + | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _) -> (* We can't expand those *) raise (Failure "Attempted to greedily expand an ADT which can't be expanded ") - | T.TypeVar _ | T.Literal _ | Never -> raise (Failure "Unreachable") + | T.TypeVar _ | T.Literal _ | Never | T.TraitType _ -> + raise (Failure "Unreachable") in (* Compose and continue *) comp cc expand cf ctx diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 2f6a7b49..51f6ff05 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -7,6 +7,7 @@ module E = Expressions open Utils module C = Contexts module Subst = Substitute +module Assoc = AssociatedTypes module L = Logging open TypesUtils open ValuesUtils @@ -141,11 +142,18 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) | V.Adt av -> (* Sanity check *) (match v.V.ty with - | T.Adt (T.Assumed (T.Box | Vec), _, _, _) -> + | T.Adt (T.Assumed (T.Box | Vec), _) -> raise (Failure "Can't copy an assumed value other than Option") - | T.Adt (T.AdtId _, _, _, _) -> assert allow_adt_copy - | T.Adt ((T.Assumed Option | T.Tuple), _, _, _) -> () (* Ok *) - | T.Adt (T.Assumed (Slice | T.Array), [], [ ty ], []) -> + | T.Adt (T.AdtId _, _) -> assert allow_adt_copy + | T.Adt ((T.Assumed Option | T.Tuple), _) -> () (* Ok *) + | T.Adt + ( T.Assumed (Slice | T.Array), + { + regions = []; + types = [ ty ]; + const_generics = []; + trait_refs = []; + } ) -> assert (ty_is_primitively_copyable ty) | _ -> raise (Failure "Unreachable")); let ctx, fields = @@ -263,6 +271,9 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) match cv.value with | E.CLiteral lit -> cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx + | E.TraitConst (_trait_ref, _generics, _const_name) -> + (* TODO *) + raise (Failure "Unimplemented") | E.CVar vid -> ( let ctx0 = ctx in (* Lookup the const generic value *) @@ -681,7 +692,8 @@ let eval_rvalue_aggregate (config : C.config) | E.AggregatedTuple -> let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in let v = V.Adt { variant_id = None; field_values = values } in - let ty = T.Adt (T.Tuple, [], tys, []) in + let generics = TypesUtils.mk_generic_args [] tys [] [] in + let ty = T.Adt (T.Tuple, generics) in let aggregated : V.typed_value = { V.value = v; ty } in (* Call the continuation *) cf aggregated ctx @@ -692,20 +704,22 @@ let eval_rvalue_aggregate (config : C.config) assert (List.length values = 1) else raise (Failure "Unreachable"); (* Construt the value *) - let aty = T.Adt (T.Assumed T.Option, [], [ ty ], []) in + let generics = TypesUtils.mk_generic_args [] [ ty ] [] [] in + let aty = T.Adt (T.Assumed T.Option, generics) in let av : V.adt_value = { V.variant_id = Some variant_id; V.field_values = values } in let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in (* Call the continuation *) cf aggregated ctx - | E.AggregatedAdt (def_id, opt_variant_id, regions, types, cgs) -> + | E.AggregatedAdt (def_id, opt_variant_id, generics) -> (* Sanity checks *) let type_decl = C.ctx_lookup_type_decl ctx def_id in - assert (List.length type_decl.region_params = List.length regions); + assert ( + List.length type_decl.generics.regions = List.length generics.regions); let expected_field_types = - Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id - types cgs + Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id + generics in assert ( expected_field_types @@ -714,7 +728,7 @@ let eval_rvalue_aggregate (config : C.config) let av : V.adt_value = { V.variant_id = opt_variant_id; V.field_values = values } in - let aty = T.Adt (T.AdtId def_id, regions, types, cgs) in + let aty = T.Adt (T.AdtId def_id, generics) in let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in (* Call the continuation *) cf aggregated ctx @@ -734,7 +748,8 @@ let eval_rvalue_aggregate (config : C.config) let av : V.adt_value = { V.variant_id = None; V.field_values = values } in - let aty = T.Adt (T.Assumed T.Range, [], [ ety ], []) in + let generics = TypesUtils.mk_generic_args_from_types [ ety ] in + let aty = T.Adt (T.Assumed T.Range, generics) in let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in (* Call the continuation *) cf aggregated ctx @@ -744,7 +759,8 @@ let eval_rvalue_aggregate (config : C.config) (* Sanity check: the number of values is consistent with the length *) let len = (literal_as_scalar (const_generic_as_literal cg)).value in assert (len = Z.of_int (List.length values)); - let ty = T.Adt (T.Assumed T.Array, [], [ ety ], [ cg ]) in + let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in + let ty = T.Adt (T.Assumed T.Array, generics) in (* In order to generate a better AST, we introduce a symbolic value equal to the array. The reason is that otherwise, the array we introduce here might be duplicated in the generated @@ -777,7 +793,7 @@ let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue) (* Delegate to the proper auxiliary function *) match rvalue with | E.Use op -> comp_wrap (eval_operand config op) ctx - | E.Ref (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx + | E.RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx | E.UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx | E.BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx | E.Aggregate (aggregate_kind, ops) -> diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 10205c27..a34a7d06 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -554,10 +554,13 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) C.type_context; fun_context; global_context; + trait_decls_context; + trait_impls_context; region_groups; type_vars; const_generic_vars; const_generic_vars_map; + trait_clauses; env = _; ended_regions = ended_regions0; } = @@ -567,10 +570,13 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) C.type_context = _; fun_context = _; global_context = _; + trait_decls_context = _; + trait_impls_context = _; region_groups = _; type_vars = _; const_generic_vars = _; const_generic_vars_map = _; + trait_clauses = _; env = _; ended_regions = ended_regions1; } = @@ -582,10 +588,13 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx) C.type_context; fun_context; global_context; + trait_decls_context; + trait_impls_context; region_groups; type_vars; const_generic_vars; const_generic_vars_map; + trait_clauses; env; ended_regions; } diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 9248e513..8cab546e 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -149,20 +149,25 @@ let rec match_types (match_distinct_types : 'r T.ty -> 'r T.ty -> 'r T.ty) (match_regions : 'r -> 'r -> 'r) (ty0 : 'r T.ty) (ty1 : 'r T.ty) : 'r T.ty = let match_rec = match_types match_distinct_types match_regions in match (ty0, ty1) with - | Adt (id0, regions0, tys0, cgs0), Adt (id1, regions1, tys1, cgs1) -> + | Adt (id0, generics0), Adt (id1, generics1) -> assert (id0 = id1); - assert (cgs0 = cgs1); + assert (generics0.const_generics = generics1.const_generics); + assert (generics0.trait_refs = generics1.trait_refs); let id = id0 in - let cgs = cgs1 in + let const_generics = generics1.const_generics in + let trait_refs = generics1.trait_refs in let regions = List.map (fun (id0, id1) -> match_regions id0 id1) - (List.combine regions0 regions1) + (List.combine generics0.regions generics1.regions) in - let tys = - List.map (fun (ty0, ty1) -> match_rec ty0 ty1) (List.combine tys0 tys1) + let types = + List.map + (fun (ty0, ty1) -> match_rec ty0 ty1) + (List.combine generics0.types generics1.types) in - Adt (id, regions, tys, cgs) + let generics = { T.regions; types; const_generics; trait_refs } in + Adt (id, generics) | TypeVar vid0, TypeVar vid1 -> assert (vid0 = vid1); let vid = vid0 in diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 04dc8892..465d0028 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -3,6 +3,7 @@ module V = Values module E = Expressions module C = Contexts module Subst = Substitute +module Assoc = AssociatedTypes module L = Logging open Cps open ValuesUtils @@ -97,7 +98,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) match (pe, v.V.value, v.V.ty) with | ( Field (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id), V.Adt adt, - T.Adt (type_id, _, _, _) ) -> ( + T.Adt (type_id, _) ) -> ( (* Check consistency *) (match (proj_kind, type_id) with | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' -> @@ -119,8 +120,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) let updated = { v with value = nadt } in Ok (ctx, { res with updated })) (* Tuples *) - | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _, _) - -> ( + | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _) -> ( assert (arity = List.length adt.field_values); let fv = T.FieldId.nth adt.field_values field_id in (* Project *) @@ -145,9 +145,9 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) (* Box dereferencement *) | ( DerefBox, Adt { variant_id = None; field_values = [ bv ] }, - T.Adt (T.Assumed T.Box, _, _, _) ) -> ( - (* We allow moving inside of boxes. In practice, this kind of - * manipulations should happen only inside unsage code, so + T.Adt (T.Assumed T.Box, _) ) -> ( + (* We allow moving outside of boxes. In practice, this kind of + * manipulations should happen only inside unsafe code, so * it shouldn't happen due to user code, and we leverage it * when implementing box dereferencement for the concrete * interpreter *) @@ -357,24 +357,23 @@ let write_place (access : access_kind) (p : E.place) (nv : V.typed_value) | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e)) | Ok ctx -> ctx -let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t) +let compute_expanded_bottom_adt_value (ctx : C.eval_ctx) (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) - (regions : T.erased_region list) (types : T.ety list) - (cgs : T.const_generic list) : V.typed_value = + (generics : T.egeneric_args) : 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.TypeDeclId.Map.find def_id tyctx in - assert (List.length regions = List.length def.T.region_params); + let def = C.ctx_lookup_type_decl ctx def_id in + assert (List.length generics.regions = List.length def.T.generics.regions); (* Compute the field types *) let field_types = - Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types cgs + Assoc.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id generics in (* Initialize the expanded value *) let fields = List.map mk_bottom field_types in let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in - let ty = T.Adt (T.AdtId def_id, regions, types, cgs) in + let ty = T.Adt (T.AdtId def_id, generics) in { V.value = av; V.ty } let compute_expanded_bottom_option_value (variant_id : T.VariantId.id) @@ -387,7 +386,8 @@ let compute_expanded_bottom_option_value (variant_id : T.VariantId.id) else raise (Failure "Unreachable") in let av = V.Adt { variant_id = Some variant_id; field_values } in - let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ], []) in + let generics = TypesUtils.mk_generic_args [] [ param_ty ] [] [] in + let ty = T.Adt (T.Assumed T.Option, generics) in { V.value = av; ty } let compute_expanded_bottom_tuple_value (field_types : T.ety list) : @@ -395,7 +395,8 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) : (* Generate the field values *) let fields = List.map mk_bottom field_types in let v = V.Adt { variant_id = None; field_values = fields } in - let ty = T.Adt (T.Tuple, [], field_types, []) in + let generics = TypesUtils.mk_generic_args [] field_types [] [] in + let ty = T.Adt (T.Tuple, generics) in { V.value = v; V.ty } (** Auxiliary helper to expand {!V.Bottom} values. @@ -447,19 +448,29 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place) match (pe, ty) with (* "Regular" ADTs *) | ( Field (ProjAdt (def_id, opt_variant_id), _), - T.Adt (T.AdtId def_id', regions, types, cgs) ) -> + T.Adt (T.AdtId def_id', generics) ) -> assert (def_id = def_id'); - compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id - opt_variant_id regions types cgs + compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics (* Option *) | ( Field (ProjOption variant_id, _), - T.Adt (T.Assumed T.Option, [], [ ty ], []) ) -> + T.Adt + ( T.Assumed T.Option, + { + T.regions = []; + types = [ ty ]; + const_generics = []; + trait_refs = []; + } ) ) -> compute_expanded_bottom_option_value variant_id ty (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys, []) -> - assert (arity = List.length tys); + | ( Field (ProjTuple arity, _), + T.Adt + ( T.Tuple, + { T.regions = []; types; const_generics = []; trait_refs = [] } ) ) + -> + assert (arity = List.length types); (* Generate the field values *) - compute_expanded_bottom_tuple_value tys + compute_expanded_bottom_tuple_value types | _ -> raise (Failure diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index 4a9f3b41..041b0a97 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -3,6 +3,7 @@ module V = Values module E = Expressions module C = Contexts module Subst = Substitute +module Assoc = AssociatedTypes module L = Logging open Cps open InterpreterExpansion @@ -56,12 +57,10 @@ val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value (** Compute an expanded ADT ⊥ value *) val compute_expanded_bottom_adt_value : - T.type_decl T.TypeDeclId.Map.t -> + C.eval_ctx -> T.TypeDeclId.id -> T.VariantId.id option -> - T.erased_region list -> - T.ety list -> - T.const_generic list -> + T.egeneric_args -> V.typed_value (** Compute an expanded [Option] ⊥ value *) diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index faed066b..9e0c2b75 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -3,6 +3,7 @@ module V = Values module E = Expressions module C = Contexts module Subst = Substitute +module Assoc = AssociatedTypes module L = Logging open TypesUtils open InterpreterUtils @@ -24,12 +25,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) else match (v.V.value, ty) with | V.Literal _, T.Literal _ -> [] - | V.Adt adt, T.Adt (id, region_params, tys, cgs) -> + | V.Adt adt, T.Adt (id, generics) -> (* Retrieve the types of the fields *) let field_types = - Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id - region_params tys cgs + Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics in + (* Project over the field values *) let fields_types = List.combine adt.V.field_values field_types in let proj_fields = @@ -103,11 +104,10 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) let value : V.avalue = match (v.V.value, ty) with | V.Literal _, T.Literal _ -> V.AIgnored - | V.Adt adt, T.Adt (id, region_params, tys, cgs) -> + | V.Adt adt, T.Adt (id, generics) -> (* Retrieve the types of the fields *) let field_types = - Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id - region_params tys cgs + Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics in (* Project over the field values *) let fields_types = List.combine adt.V.field_values field_types in @@ -268,8 +268,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) let (value, ty) : V.avalue * T.rty = match (see, original_sv_ty) with | SeLiteral _, T.Literal _ -> (V.AIgnored, original_sv_ty) - | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys, _cgs) - -> + | SeAdt (variant_id, field_values), T.Adt (_id, _generics) -> (* Project over the field values *) let field_values = List.map diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 6d520059..d38f8b95 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -17,6 +17,7 @@ open InterpreterProjectors open InterpreterExpansion open InterpreterPaths open InterpreterExpressions +module PCtx = Print.EvalCtxLlbcAst (** The local logger *) let log = L.statements_log @@ -232,9 +233,8 @@ let set_discriminant (config : C.config) (p : E.place) let update_value cf (v : V.typed_value) : m_fun = fun ctx -> match (v.V.ty, v.V.value) with - | ( T.Adt - (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types, cgs), - V.Adt av ) -> ( + | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Adt av + -> ( (* There are two situations: - either the discriminant is already the proper one (in which case we don't do anything) @@ -251,28 +251,26 @@ 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_decls def_id (Some variant_id) - regions types cgs + compute_expanded_bottom_adt_value ctx def_id + (Some variant_id) generics | T.Assumed T.Option -> - assert (regions = []); + assert (generics.regions = []); compute_expanded_bottom_option_value variant_id - (Collections.List.to_cons_nil types) + (Collections.List.to_cons_nil generics.types) | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx) - | ( T.Adt - (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types, cgs), - V.Bottom ) -> + | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Bottom + -> let bottom_v = match type_id with | T.AdtId def_id -> - compute_expanded_bottom_adt_value ctx.type_context.type_decls - def_id (Some variant_id) regions types cgs + compute_expanded_bottom_adt_value ctx def_id (Some variant_id) + generics | T.Assumed T.Option -> - assert (regions = []); + assert (generics.regions = []); compute_expanded_bottom_option_value variant_id - (Collections.List.to_cons_nil types) + (Collections.List.to_cons_nil generics.types) | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx @@ -301,24 +299,34 @@ let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx = let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) (** Small helper: compute the type of the return value for a specific - instantiation of a non-local function. + instantiation of an assumed function. *) -let get_non_local_function_return_type (fid : A.assumed_fun_id) - (region_params : T.erased_region list) (type_params : T.ety list) - (const_generic_params : T.const_generic list) : T.ety = +let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id) + (generics : T.egeneric_args) : T.ety = + assert (generics.trait_refs = []); (* [Box::free] has a special treatment *) - match (fid, region_params, type_params, const_generic_params) with - | A.BoxFree, [], [ _ ], [] -> mk_unit_ty + match fid with + | A.BoxFree -> + assert (generics.regions = []); + assert (List.length generics.types = 1); + assert (generics.const_generics = []); + mk_unit_ty | _ -> (* Retrieve the function's signature *) let sg = Assumed.get_assumed_sig fid in (* Instantiate the return type *) - let tsubst = Subst.make_type_subst_from_vars sg.type_params type_params in - let cgsubst = - Subst.make_const_generic_subst_from_vars sg.const_generic_params - const_generic_params + (* There shouldn't be any reference to Self *) + let tr_self : T.erased_region T.trait_instance_id = + T.UnknownTrait __FUNCTION__ + in + let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = + Subst.make_esubst_from_generics sg.generics generics tr_self in - Subst.erase_regions_substitute_types tsubst cgsubst sg.output + let ty = + Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self + sg.output + in + Assoc.ctx_normalize_type ctx ty let move_return_value (config : C.config) (pop_return_value : bool) (cf : V.typed_value option -> m_fun) : m_fun = @@ -418,19 +426,19 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun = in comp cf_pop cf_assign -(** Auxiliary function - see {!eval_non_local_function_call} *) -let eval_replace_concrete (_config : C.config) - (_region_params : T.erased_region list) (_type_params : T.ety list) - (_cg_args : T.const_generic list) : cm_fun = +(** Auxiliary function - see {!eval_assumed_function_call} *) +let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) : + cm_fun = fun _cf _ctx -> raise Unimplemented -(** Auxiliary function - see {!eval_non_local_function_call} *) -let eval_box_new_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (cg_args : T.const_generic list) : cm_fun = +(** Auxiliary function - see {!eval_assumed_function_call} *) +let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) : + cm_fun = fun cf ctx -> (* Check and retrieve the arguments *) - match (region_params, type_params, cg_args, ctx.env) with + match + (generics.regions, generics.types, generics.const_generics, ctx.env) + with | ( [], [ boxed_ty ], [], @@ -448,7 +456,8 @@ let eval_box_new_concrete (config : C.config) (* Create the new box *) let cf_create cf (moved_input_value : V.typed_value) : m_fun = (* Create the box value *) - let box_ty = T.Adt (T.Assumed T.Box, [], [ boxed_ty ], []) in + let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in + let box_ty = T.Adt (T.Assumed T.Box, generics) in let box_v = V.Adt { variant_id = None; field_values = [ moved_input_value ] } in @@ -467,13 +476,14 @@ let eval_box_new_concrete (config : C.config) | _ -> raise (Failure "Inconsistent state") (** Auxiliary function which factorizes code to evaluate [std::Deref::deref] - and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *) + and [std::DerefMut::deref_mut] - see {!eval_assumed_function_call} *) let eval_box_deref_mut_or_shared_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (cg_args : T.const_generic list) (is_mut : bool) : cm_fun = + (generics : T.egeneric_args) (is_mut : bool) : cm_fun = fun cf ctx -> (* Check the arguments *) - match (region_params, type_params, cg_args, ctx.env) with + match + (generics.regions, generics.types, generics.const_generics, ctx.env) + with | ( [], [ boxed_ty ], [], @@ -495,7 +505,7 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] } in let borrow_kind = if is_mut then E.Mut else E.Shared in - let rv = E.Ref (p, borrow_kind) in + let rv = E.RvRef (p, borrow_kind) in let cf_borrow = eval_rvalue_not_global config rv in (* Move the borrow to its destination *) @@ -514,23 +524,19 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) comp cf_borrow cf_move cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function - see {!eval_non_local_function_call} *) -let eval_box_deref_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (cg_args : T.const_generic list) : cm_fun = +(** Auxiliary function - see {!eval_assumed_function_call} *) +let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) : + cm_fun = let is_mut = false in - eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args - is_mut + eval_box_deref_mut_or_shared_concrete config generics is_mut -(** Auxiliary function - see {!eval_non_local_function_call} *) -let eval_box_deref_mut_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (cg_args : T.const_generic list) : cm_fun = +(** Auxiliary function - see {!eval_assumed_function_call} *) +let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args) + : cm_fun = let is_mut = true in - eval_box_deref_mut_or_shared_concrete config region_params type_params cg_args - is_mut + eval_box_deref_mut_or_shared_concrete config generics is_mut -(** Auxiliary function - see {!eval_non_local_function_call}. +(** Auxiliary function - see {!eval_assumed_function_call}. [Box::free] is not handled the same way as the other assumed functions: - in the regular case, whenever we need to evaluate an assumed function, @@ -549,11 +555,10 @@ let eval_box_deref_mut_concrete (config : C.config) It thus updates the box value (by calling {!drop_value}) and updates the destination (by setting it to [()]). *) -let eval_box_free (config : C.config) (region_params : T.erased_region list) - (type_params : T.ety list) (cg_args : T.const_generic list) +let eval_box_free (config : C.config) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : cm_fun = fun cf ctx -> - match (region_params, type_params, cg_args, args) with + match (generics.regions, generics.types, generics.const_generics, args) with | [], [ boxed_ty ], [], [ E.Move input_box_place ] -> (* Required type checking *) let input_box = InterpreterPaths.read_place Write input_box_place ctx in @@ -570,20 +575,18 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) cc cf ctx | _ -> raise (Failure "Inconsistent state") -(** Auxiliary function - see {!eval_non_local_function_call} *) +(** Auxiliary function - see {!eval_assumed_function_call} *) let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) - (_region_params : T.erased_region list) (_type_params : T.ety list) - (_cg_args : T.const_generic list) : cm_fun = + (_generics : T.egeneric_args) : cm_fun = fun _cf _ctx -> raise Unimplemented (** Evaluate a non-local function call in concrete mode *) -let eval_non_local_function_call_concrete (config : C.config) - (fid : A.assumed_fun_id) (region_params : T.erased_region list) - (type_params : T.ety list) (cg_args : T.const_generic list) +let eval_assumed_function_call_concrete (config : C.config) + (fid : A.assumed_fun_id) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : cm_fun = (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - assert (cg_args = []); + assert (generics.const_generics = []); (* There are two cases (and this is extremely annoying): - the function is not box_free - the function is box_free @@ -592,7 +595,7 @@ let eval_non_local_function_call_concrete (config : C.config) match fid with | A.BoxFree -> (* Degenerate case: box_free *) - eval_box_free config region_params type_params cg_args args dest + eval_box_free config generics args dest | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) @@ -607,16 +610,14 @@ let eval_non_local_function_call_concrete (config : C.config) * but it made it less clear where the computed values came from, * so we reversed the modifications. *) let cf_eval_call cf (args_vl : V.typed_value list) : m_fun = + fun ctx -> (* Push the stack frame: we initialize the frame with the return variable, and one variable per input argument *) let cc = push_frame in (* Create and push the return variable *) let ret_vid = E.VarId.zero in - let ret_ty = - get_non_local_function_return_type fid region_params type_params - cg_args - in + let ret_ty = get_assumed_function_return_type ctx fid generics in let ret_var = mk_var ret_vid (Some "@return") ret_ty in let cc = comp cc (push_uninitialized_var ret_var) in @@ -633,20 +634,14 @@ let eval_non_local_function_call_concrete (config : C.config) * access to a body. *) let cf_eval_body : cm_fun = match fid with - | A.Replace -> - eval_replace_concrete config region_params type_params cg_args - | BoxNew -> - eval_box_new_concrete config region_params type_params cg_args - | BoxDeref -> - eval_box_deref_concrete config region_params type_params cg_args - | BoxDerefMut -> - eval_box_deref_mut_concrete config region_params type_params - cg_args + | A.Replace -> eval_replace_concrete config generics + | BoxNew -> eval_box_new_concrete config generics + | BoxDeref -> eval_box_deref_concrete config generics + | BoxDerefMut -> eval_box_deref_mut_concrete config generics | BoxFree -> (* Should have been treated above *) raise (Failure "Unreachable") | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> - eval_vec_function_concrete config fid region_params type_params - cg_args + eval_vec_function_concrete config fid generics | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut | SliceIndexShared | SliceIndexMut | SliceSubsliceShared @@ -660,13 +655,13 @@ let eval_non_local_function_call_concrete (config : C.config) let cc = comp cc (pop_frame_assign config dest) in (* Continue *) - cc cf + cc cf ctx in (* Compose and apply *) comp cf_eval_ops cf_eval_call -let instantiate_fun_sig (type_params : T.ety list) - (cg_args : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig = +let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args) + (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = (* Generate fresh abstraction ids and create a substitution from region * group ids to abstraction ids *) let rg_abs_ids_bindings = @@ -685,7 +680,7 @@ let instantiate_fun_sig (type_params : T.ety list) T.RegionGroupId.Map.find rg_id asubst_map in (* Generate fresh regions and their substitutions *) - let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in + let _, rsubst, _ = Subst.fresh_regions_with_substs sg.generics.regions in (* Generate the type substitution * Note that we need the substitution to map the type variables to * {!rty} types (not {!ety}). In order to do that, we convert the @@ -694,13 +689,28 @@ let instantiate_fun_sig (type_params : T.ety list) * This is a current limitation of the analysis: there is still some * work to do to properly handle full type parametrization. * *) - let rtype_params = List.map ety_no_regions_to_rty type_params in - let tsubst = Subst.make_type_subst_from_vars sg.type_params rtype_params in + let rtype_params = List.map ety_no_regions_to_rty generics.types in + let tsubst = Subst.make_type_subst_from_vars sg.generics.types rtype_params in let cgsubst = - Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_args + Subst.make_const_generic_subst_from_vars sg.generics.const_generics + generics.const_generics + in + (* TODO: something annoying with the trait ref subst: we need to use region + types, but the arguments use erased regions. For now we use the fact + that no regions should appear inside. In the future: we should merge + ety and rty. *) + let trait_refs = + List.map TypesUtils.etrait_ref_no_regions_to_gr_trait_ref + generics.trait_refs + in + let tr_subst = + Subst.make_trait_subst_from_clauses sg.generics.trait_clauses trait_refs in (* Substitute the signature *) - let inst_sig = Subst.substitute_signature asubst rsubst tsubst cgsubst sg in + let inst_sig = + Assoc.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst tr_subst + tr_self sg + in (* Return *) inst_sig @@ -839,7 +849,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = match rvalue with | E.Global _ -> raise (Failure "Unreachable") | E.Use _ - | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow)) + | E.RvRef (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow)) | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _ | E.Aggregate _ -> let rp = rvalue_get_place rvalue in @@ -896,7 +906,9 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id) match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body (without arguments) *) - (eval_local_function_call_concrete config global.body_id [] [] [] [] dest) + let generics = TypesUtils.mk_empty_generic_args in + (eval_transparent_function_call_concrete config global.body_id generics [] + dest) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be @@ -1040,26 +1052,26 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun = (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = - (* There are two cases: + (* There are several cases: - this is a local function, in which case we execute its body - - this is a non-local function, in which case there is a special treatment + - this is an assumed function, in which case there is a special treatment + - this is a trait method *) match call.func with - | A.Regular fid -> - eval_local_function_call config fid call.region_args call.type_args - call.const_generic_args call.args call.dest - | A.Assumed fid -> - eval_non_local_function_call config fid call.region_args call.type_args - call.const_generic_args call.args call.dest + | A.FunId (A.Regular fid) -> + eval_transparent_function_call config fid call.generics call.args + call.dest + | A.FunId (A.Assumed fid) -> + eval_assumed_function_call config fid call.generics call.args call.dest + | A.TraitMethod _ -> raise (Failure "Unimplemented") (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) - (_region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : - st_cm_fun = +and eval_transparent_function_call_concrete (config : C.config) + (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list) + (dest : E.place) : st_cm_fun = (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - assert (cg_args = []); + assert (generics.const_generics = []); fun cf ctx -> (* Retrieve the (correctly instantiated) body *) let def = C.ctx_lookup_fun_decl ctx fid in @@ -1073,16 +1085,14 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) ^ Print.name_to_string def.name)) | Some body -> body in - let tsubst = - Subst.make_type_subst_from_vars def.A.signature.type_params type_args - in - let cgsubst = - Subst.make_const_generic_subst_from_vars - def.A.signature.const_generic_params cg_args - in - let locals, body_st = - Subst.fun_body_substitute_in_body tsubst cgsubst body + (* TODO: we need to normalize the types if we want to correctly support traits *) + assert (ctx.trait_clauses = [] && generics.trait_refs = []); + (* There shouldn't be any reference to Self *) + let tr_self = T.UnknownTrait __FUNCTION__ in + let subst = + Subst.make_esubst_from_generics def.A.signature.generics generics tr_self in + let locals, body_st = Subst.fun_body_substitute_in_body subst body in (* Evaluate the input operands *) assert (List.length args = body.A.arg_count); @@ -1139,22 +1149,23 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.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.FunDeclId.id) - (region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : - st_cm_fun = +and eval_transparent_function_call_symbolic (config : C.config) + (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list) + (dest : E.place) : st_cm_fun = fun cf ctx -> (* Retrieve the (correctly instantiated) signature *) 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 *) - let inst_sg = instantiate_fun_sig type_args cg_args sg in + (* There shouldn't be any reference to Self *) + let tr_self = T.UnknownTrait __FUNCTION__ in + let inst_sg = instantiate_fun_sig ctx generics tr_self sg in (* Sanity check *) assert (List.length args = List.length def.A.signature.inputs); (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg - region_args type_args cg_args args dest cf ctx + generics args dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -1162,10 +1173,8 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) calls in symbolic mode: only their signatures matter. *) and eval_function_call_symbolic_from_inst_sig (config : C.config) - (fid : A.fun_id) (inst_sg : A.inst_fun_sig) - (_region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : - st_cm_fun = + (fid : A.fun_id) (inst_sg : A.inst_fun_sig) (generics : T.egeneric_args) + (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in @@ -1232,8 +1241,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) let expr = cf ctx in (* Synthesize the symbolic AST *) - S.synthesize_regular_function_call fid call_id ctx abs_ids type_args cg_args - args args_places ret_spc dest_place expr + S.synthesize_regular_function_call fid call_id ctx abs_ids generics args + args_places ret_spc dest_place expr in let cc = comp cc cf_call in @@ -1294,9 +1303,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) cc (cf Unit) ctx (** Evaluate a non-local function call in symbolic mode *) -and eval_non_local_function_call_symbolic (config : C.config) - (fid : A.assumed_fun_id) (region_args : T.erased_region list) - (type_args : T.ety list) (cg_args : T.const_generic list) +and eval_assumed_function_call_symbolic (config : C.config) + (fid : A.assumed_fun_id) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Sanity check: make sure the type parameters don't contain regions - @@ -1304,7 +1312,7 @@ and eval_non_local_function_call_symbolic (config : C.config) assert ( List.for_all (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty)) - type_args); + generics.types); (* There are two cases (and this is extremely annoying): - the function is not box_free @@ -1315,7 +1323,7 @@ and eval_non_local_function_call_symbolic (config : C.config) | A.BoxFree -> (* Degenerate case: box_free - note that this is not really a function * call: no need to call a "synthesize_..." function *) - eval_box_free config region_args type_args cg_args args dest (cf Unit) ctx + eval_box_free config generics args dest (cf Unit) ctx | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined @@ -1327,55 +1335,50 @@ and eval_non_local_function_call_symbolic (config : C.config) (* should have been treated above *) raise (Failure "Unreachable") | _ -> - instantiate_fun_sig type_args cg_args (Assumed.get_assumed_sig fid) + (* There shouldn't be any reference to Self *) + let tr_self = T.UnknownTrait __FUNCTION__ in + instantiate_fun_sig ctx generics tr_self + (Assumed.get_assumed_sig fid) in (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig - region_args type_args cg_args args dest cf ctx + generics args dest cf ctx (** Evaluate a non-local (i.e, assumed) function call such as [Box::deref] (auxiliary helper for [eval_statement]) *) -and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) - (region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : +and eval_assumed_function_call (config : C.config) (fid : A.assumed_fun_id) + (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Debug *) log#ldebug (lazy - (let type_args = - "[" ^ String.concat ", " (List.map (ety_to_string ctx) type_args) ^ "]" - in + (let generics = PCtx.egeneric_args_to_string ctx generics in let args = "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]" in let dest = place_to_string ctx dest in - "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid - ^ "\n- type_args: " ^ type_args ^ "\n- args: " ^ args ^ "\n- dest: " - ^ dest)); + "eval_assumed_function_call:\n- fid:" ^ A.show_assumed_fun_id fid + ^ "\n- generics: " ^ generics ^ "\n- args: " ^ args ^ "\n- dest: " ^ dest)); match config.mode with | C.ConcreteMode -> - eval_non_local_function_call_concrete config fid region_args type_args - cg_args args dest (cf Unit) ctx + eval_assumed_function_call_concrete config fid generics args dest + (cf Unit) ctx | C.SymbolicMode -> - eval_non_local_function_call_symbolic config fid region_args type_args - cg_args args dest cf ctx + eval_assumed_function_call_symbolic config fid generics args dest cf ctx (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) -and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id) - (region_args : T.erased_region list) (type_args : T.ety list) - (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) : +and eval_transparent_function_call (config : C.config) (fid : A.FunDeclId.id) + (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = match config.mode with | ConcreteMode -> - eval_local_function_call_concrete config fid region_args type_args cg_args - args dest + eval_transparent_function_call_concrete config fid generics args dest | SymbolicMode -> - eval_local_function_call_symbolic config fid region_args type_args cg_args - args dest + eval_transparent_function_call_symbolic config fid generics args dest (** Evaluate a statement seen as a function body *) and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli index 814bc964..0a086fb2 100644 --- a/compiler/InterpreterStatements.mli +++ b/compiler/InterpreterStatements.mli @@ -32,7 +32,11 @@ val pop_frame : C.config -> bool -> (V.typed_value option -> m_fun) -> m_fun Note: there are no region parameters, because they should be erased. *) val instantiate_fun_sig : - T.ety list -> T.const_generic list -> LA.fun_sig -> LA.inst_fun_sig + C.eval_ctx -> + T.egeneric_args -> + T.rtrait_instance_id -> + LA.fun_sig -> + LA.inst_fun_sig (** Helper. diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 637f1b1e..1513465c 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -273,7 +273,7 @@ let rvalue_get_place (rv : E.rvalue) : E.place option = match rv with | Use (Copy p | Move p) -> Some p | Use (Constant _) -> None - | Ref (p, _) -> Some p + | RvRef (p, _) -> Some p | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None (** See {!ValuesUtils.symbolic_value_has_borrows} *) diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index f29c7f88..9ac5ce13 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -7,6 +7,7 @@ module V = Values module E = Expressions module C = Contexts module Subst = Substitute +module Assoc = AssociatedTypes module A = LlbcAst module L = Logging open Cps @@ -406,13 +407,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (match (tv.V.value, tv.V.ty) with | V.Literal cv, T.Literal ty -> check_literal_type cv ty (* ADT case *) - | V.Adt av, T.Adt (T.AdtId def_id, regions, tys, cgs) -> + | V.Adt av, T.Adt (T.AdtId def_id, generics) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) 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); + assert ( + List.length generics.regions = List.length def.generics.regions); + assert (List.length generics.types = List.length def.generics.types); (* Check that the variant id is consistent *) (match (av.V.variant_id, def.T.kind) with | Some variant_id, T.Enum variants -> @@ -421,8 +423,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> raise (Failure "Erroneous typing")); (* Check that the field types are correct *) let field_types = - Subst.type_decl_get_instantiated_field_etypes def av.V.variant_id - tys cgs + Assoc.type_decl_get_inst_norm_field_etypes ctx def av.V.variant_id + generics in let fields_with_types = List.combine av.V.field_values field_types @@ -431,20 +433,28 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty)) fields_with_types (* Tuple case *) - | V.Adt av, T.Adt (T.Tuple, regions, tys, cgs) -> - assert (regions = []); - assert (cgs = []); + | V.Adt av, T.Adt (T.Tuple, generics) -> + assert (generics.regions = []); + assert (generics.const_generics = []); assert (av.V.variant_id = None); (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) - let fields_with_types = List.combine av.V.field_values tys in + let fields_with_types = + List.combine av.V.field_values generics.types + in List.iter (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty)) fields_with_types (* Assumed type case *) - | V.Adt av, T.Adt (T.Assumed aty_id, regions, tys, cgs) -> ( + | V.Adt av, T.Adt (T.Assumed aty_id, generics) -> ( assert (av.V.variant_id = None || aty_id = T.Option); - match (aty_id, av.V.field_values, regions, tys, cgs) with + match + ( aty_id, + av.V.field_values, + generics.regions, + generics.types, + generics.const_generics ) + with (* Box *) | T.Box, [ inner_value ], [], [ inner_ty ], [] | T.Option, [ inner_value ], [], [ inner_ty ], [] -> @@ -520,14 +530,17 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (* Check the current pair (value, type) *) (match (atv.V.value, atv.V.ty) with (* ADT case *) - | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys, cgs) -> + | V.AAdt av, T.Adt (T.AdtId def_id, generics) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) 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); - assert (List.length cgs = List.length def.const_generic_params); + assert ( + List.length generics.regions = List.length def.generics.regions); + assert (List.length generics.types = List.length def.generics.types); + assert ( + List.length generics.const_generics + = List.length def.generics.const_generics); (* Check that the variant id is consistent *) (match (av.V.variant_id, def.T.kind) with | Some variant_id, T.Enum variants -> @@ -536,8 +549,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> raise (Failure "Erroneous typing")); (* Check that the field types are correct *) let field_types = - Subst.type_decl_get_instantiated_field_rtypes def av.V.variant_id - regions tys cgs + Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.V.variant_id + generics in let fields_with_types = List.combine av.V.field_values field_types @@ -546,20 +559,28 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty)) fields_with_types (* Tuple case *) - | V.AAdt av, T.Adt (T.Tuple, regions, tys, cgs) -> - assert (regions = []); - assert (cgs = []); + | V.AAdt av, T.Adt (T.Tuple, generics) -> + assert (generics.regions = []); + assert (generics.const_generics = []); assert (av.V.variant_id = None); (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) - let fields_with_types = List.combine av.V.field_values tys in + let fields_with_types = + List.combine av.V.field_values generics.types + in List.iter (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty)) fields_with_types (* Assumed type case *) - | V.AAdt av, T.Adt (T.Assumed aty_id, regions, tys, cgs) -> ( + | V.AAdt av, T.Adt (T.Assumed aty_id, generics) -> ( assert (av.V.variant_id = None); - match (aty_id, av.V.field_values, regions, tys, cgs) with + match + ( aty_id, + av.V.field_values, + generics.regions, + generics.types, + generics.const_generics ) + with (* Box *) | T.Box, [ boxed_value ], [], [ boxed_ty ], [] -> assert (boxed_value.V.ty = boxed_ty) diff --git a/compiler/Logging.ml b/compiler/Logging.ml index 9dc1f5e3..d0f5b0c5 100644 --- a/compiler/Logging.ml +++ b/compiler/Logging.ml @@ -57,6 +57,9 @@ let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows" (** Logger for Invariants *) let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants" +(** Logger for AssociatedTypes *) +let associated_types_log = L.get_logger "MainLogger.AssociatedTypes" + (** Logger for SCC *) let scc_log = L.get_logger "MainLogger.Graph.SCC" diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index b348ba1d..1058fab0 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -107,7 +107,7 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl = false | Assign (_, rv) -> ( match rv with - | Use _ | Ref _ -> not must_end_with_exit + | Use _ | RvRef _ -> not must_end_with_exit | Aggregate (AggregatedTuple, []) -> not must_end_with_exit | _ -> false) | FakeRead _ | Drop _ | Nop -> not must_end_with_exit @@ -376,7 +376,7 @@ let remove_shallow_borrows (crate : A.crate) (f : A.fun_decl) : A.fun_decl = method! visit_Assign env p rv = match (p.projection, rv) with - | [], E.Ref (_, E.Shallow) -> + | [], E.RvRef (_, E.Shallow) -> (* Filter *) filtered := E.VarId.Set.add p.var_id !filtered; Nop diff --git a/compiler/Print.ml b/compiler/Print.ml index 9aa73d7c..aebfd09c 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -21,6 +21,9 @@ module Values = struct type_decl_id_to_string : T.TypeDeclId.id -> string; const_generic_var_id_to_string : T.ConstGenericVarId.id -> string; global_decl_id_to_string : T.GlobalDeclId.id -> string; + trait_decl_id_to_string : T.TraitDeclId.id -> string; + trait_impl_id_to_string : T.TraitImplId.id -> string; + trait_clause_id_to_string : T.TraitClauseId.id -> string; adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string; var_id_to_string : E.VarId.id -> string; adt_field_names : @@ -34,6 +37,9 @@ module Values = struct PT.type_decl_id_to_string = fmt.type_decl_id_to_string; PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string; PT.global_decl_id_to_string = fmt.global_decl_id_to_string; + PT.trait_decl_id_to_string = fmt.trait_decl_id_to_string; + PT.trait_impl_id_to_string = fmt.trait_impl_id_to_string; + PT.trait_clause_id_to_string = fmt.trait_clause_id_to_string; } let value_to_rtype_formatter (fmt : value_formatter) : PT.rtype_formatter = @@ -43,6 +49,9 @@ module Values = struct PT.type_decl_id_to_string = fmt.type_decl_id_to_string; PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string; PT.global_decl_id_to_string = fmt.global_decl_id_to_string; + PT.trait_decl_id_to_string = fmt.trait_decl_id_to_string; + PT.trait_impl_id_to_string = fmt.trait_impl_id_to_string; + PT.trait_clause_id_to_string = fmt.trait_clause_id_to_string; } let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter = @@ -52,6 +61,9 @@ module Values = struct PT.type_decl_id_to_string = fmt.type_decl_id_to_string; PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string; PT.global_decl_id_to_string = fmt.global_decl_id_to_string; + PT.trait_decl_id_to_string = fmt.trait_decl_id_to_string; + PT.trait_impl_id_to_string = fmt.trait_impl_id_to_string; + PT.trait_clause_id_to_string = fmt.trait_clause_id_to_string; } let var_id_to_string (id : E.VarId.id) : string = @@ -86,10 +98,10 @@ module Values = struct List.map (typed_value_to_string fmt) av.field_values in match v.ty with - | T.Adt (T.Tuple, _, _, _) -> + | T.Adt (T.Tuple, _) -> (* Tuple *) "(" ^ String.concat ", " field_values ^ ")" - | T.Adt (T.AdtId def_id, _, _, _) -> + | T.Adt (T.AdtId def_id, _) -> (* "Regular" ADT *) let adt_ident = match av.variant_id with @@ -111,7 +123,7 @@ module Values = struct let field_values = String.concat " " field_values in adt_ident ^ " { " ^ field_values ^ " }" else adt_ident - | T.Adt (T.Assumed aty, _, _, _) -> ( + | T.Adt (T.Assumed aty, _) -> ( (* Assumed type *) match (aty, field_values) with | Box, [ bv ] -> "@Box(" ^ bv ^ ")" @@ -201,10 +213,10 @@ module Values = struct List.map (typed_avalue_to_string fmt) av.field_values in match v.ty with - | T.Adt (T.Tuple, _, _, _) -> + | T.Adt (T.Tuple, _) -> (* Tuple *) "(" ^ String.concat ", " field_values ^ ")" - | T.Adt (T.AdtId def_id, _, _, _) -> + | T.Adt (T.AdtId def_id, _) -> (* "Regular" ADT *) let adt_ident = match av.variant_id with @@ -226,7 +238,7 @@ module Values = struct let field_values = String.concat " " field_values in adt_ident ^ " { " ^ field_values ^ " }" else adt_ident - | T.Adt (T.Assumed aty, _, _, _) -> ( + | T.Adt (T.Assumed aty, _) -> ( (* Assumed type *) match (aty, field_values) with | Box, [ bv ] -> "@Box(" ^ bv ^ ")" @@ -452,6 +464,9 @@ module Contexts = struct 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; + PV.trait_decl_id_to_string = fmt.trait_decl_id_to_string; + PV.trait_impl_id_to_string = fmt.trait_impl_id_to_string; + PV.trait_clause_id_to_string = fmt.trait_clause_id_to_string; } let ast_to_value_formatter (fmt : PA.ast_formatter) : PV.value_formatter = @@ -486,6 +501,15 @@ module Contexts = struct let def = C.ctx_lookup_global_decl ctx def_id in name_to_string def.name in + let trait_decl_id_to_string def_id = + let def = C.ctx_lookup_trait_decl ctx def_id in + name_to_string def.name + in + let trait_impl_id_to_string def_id = + let def = C.ctx_lookup_trait_impl ctx def_id in + name_to_string def.name + in + let trait_clause_id_to_string id = PT.trait_clause_id_to_pretty_string id in let adt_variant_to_string = PT.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls in @@ -506,6 +530,9 @@ module Contexts = struct adt_variant_to_string; var_id_to_string; adt_field_names; + trait_decl_id_to_string; + trait_impl_id_to_string; + trait_clause_id_to_string; } let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : PA.ast_formatter = @@ -521,6 +548,15 @@ module Contexts = struct let def = C.ctx_lookup_global_decl ctx def_id in global_name_to_string def.name in + let trait_decl_id_to_string def_id = + let def = C.ctx_lookup_trait_decl ctx def_id in + name_to_string def.name + in + let trait_impl_id_to_string def_id = + let def = C.ctx_lookup_trait_impl ctx def_id in + name_to_string def.name + in + let trait_clause_id_to_string id = PT.trait_clause_id_to_pretty_string id in { rvar_to_string = ctx_fmt.PV.rvar_to_string; r_to_string = ctx_fmt.PV.r_to_string; @@ -533,6 +569,9 @@ module Contexts = struct adt_field_to_string; fun_decl_id_to_string; global_decl_id_to_string; + trait_decl_id_to_string; + trait_impl_id_to_string; + trait_clause_id_to_string; } (** Split an [env] at every occurrence of [Frame], eliminating those elements. @@ -608,6 +647,12 @@ module EvalCtxLlbcAst = struct let fmt = PC.ctx_to_rtype_formatter fmt in PT.rty_to_string fmt t + let egeneric_args_to_string (ctx : C.eval_ctx) (x : T.egeneric_args) : string + = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + let fmt = PC.ctx_to_etype_formatter fmt in + PT.egeneric_args_to_string fmt x + let borrow_content_to_string (ctx : C.eval_ctx) (bc : V.borrow_content) : string = let fmt = PC.eval_ctx_to_ctx_formatter ctx in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index dfb2c9fd..724f1e0a 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -8,6 +8,9 @@ type type_formatter = { type_decl_id_to_string : TypeDeclId.id -> string; const_generic_var_id_to_string : ConstGenericVarId.id -> string; global_decl_id_to_string : GlobalDeclId.id -> string; + trait_decl_id_to_string : TraitDeclId.id -> string; + trait_impl_id_to_string : TraitImplId.id -> string; + trait_clause_id_to_string : TraitClauseId.id -> string; } type value_formatter = { @@ -18,6 +21,9 @@ type value_formatter = { adt_variant_to_string : TypeDeclId.id -> VariantId.id -> string; var_id_to_string : VarId.id -> string; adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option; + trait_decl_id_to_string : TraitDeclId.id -> string; + trait_impl_id_to_string : TraitImplId.id -> string; + trait_clause_id_to_string : TraitClauseId.id -> string; } let value_to_type_formatter (fmt : value_formatter) : type_formatter = @@ -26,6 +32,9 @@ let value_to_type_formatter (fmt : value_formatter) : type_formatter = type_decl_id_to_string = fmt.type_decl_id_to_string; const_generic_var_id_to_string = fmt.const_generic_var_id_to_string; global_decl_id_to_string = fmt.global_decl_id_to_string; + trait_decl_id_to_string = fmt.trait_decl_id_to_string; + trait_impl_id_to_string = fmt.trait_impl_id_to_string; + trait_clause_id_to_string = fmt.trait_clause_id_to_string; } (* TODO: we need to store which variables we have encountered so far, and @@ -42,6 +51,9 @@ type ast_formatter = { adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option; fun_decl_id_to_string : FunDeclId.id -> string; global_decl_id_to_string : GlobalDeclId.id -> string; + trait_decl_id_to_string : TraitDeclId.id -> string; + trait_impl_id_to_string : TraitImplId.id -> string; + trait_clause_id_to_string : TraitClauseId.id -> string; } let ast_to_value_formatter (fmt : ast_formatter) : value_formatter = @@ -53,6 +65,9 @@ let ast_to_value_formatter (fmt : ast_formatter) : value_formatter = 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; + trait_decl_id_to_string = fmt.trait_decl_id_to_string; + trait_impl_id_to_string = fmt.trait_impl_id_to_string; + trait_clause_id_to_string = fmt.trait_clause_id_to_string; } let ast_to_type_formatter (fmt : ast_formatter) : type_formatter = @@ -70,31 +85,51 @@ let literal_type_to_string = Print.PrimitiveValues.literal_type_to_string let scalar_value_to_string = Print.PrimitiveValues.scalar_value_to_string let literal_to_string = Print.PrimitiveValues.literal_to_string +(* Remark: not using generic_params on purpose, because we may use parameters + which either come from LLBC or from pure, and the [generic_params] type + for those ASTs is not the same. Note that it works because we actually don't + need to know the trait clauses to print the AST: we can thus ignore them. +*) let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t) (global_decls : A.global_decl GlobalDeclId.Map.t) - (type_params : type_var list) + (trait_decls : A.trait_decl TraitDeclId.Map.t) + (trait_impls : A.trait_impl TraitImplId.Map.t) (type_params : type_var list) (const_generic_params : const_generic_var list) : type_formatter = let type_var_id_to_string vid = - let var = T.TypeVarId.nth type_params vid in + let var = TypeVarId.nth type_params vid in type_var_to_string var in let const_generic_var_id_to_string vid = - let var = T.ConstGenericVarId.nth const_generic_params vid in + let var = ConstGenericVarId.nth const_generic_params vid in const_generic_var_to_string var in let type_decl_id_to_string def_id = - let def = T.TypeDeclId.Map.find def_id type_decls in + let def = TypeDeclId.Map.find def_id type_decls in name_to_string def.name in let global_decl_id_to_string def_id = - let def = T.GlobalDeclId.Map.find def_id global_decls in + let def = GlobalDeclId.Map.find def_id global_decls in + name_to_string def.name + in + let trait_decl_id_to_string def_id = + let def = TraitDeclId.Map.find def_id trait_decls in name_to_string def.name in + let trait_impl_id_to_string def_id = + let def = TraitImplId.Map.find def_id trait_impls in + name_to_string def.name + in + let trait_clause_id_to_string id = + Print.PT.trait_clause_id_to_pretty_string id + in { type_var_id_to_string; type_decl_id_to_string; const_generic_var_id_to_string; global_decl_id_to_string; + trait_decl_id_to_string; + trait_impl_id_to_string; + trait_clause_id_to_string; } (* TODO: there is a bit of duplication with Print.fun_decl_to_ast_formatter. @@ -106,7 +141,8 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t) let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) (fun_decls : A.fun_decl FunDeclId.Map.t) (global_decls : A.global_decl GlobalDeclId.Map.t) - (type_params : type_var list) + (trait_decls : A.trait_decl TraitDeclId.Map.t) + (trait_impls : A.trait_impl TraitImplId.Map.t) (type_params : type_var list) (const_generic_params : const_generic_var list) : ast_formatter = let type_var_id_to_string vid = let var = T.TypeVarId.nth type_params vid in @@ -141,6 +177,17 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) let def = GlobalDeclId.Map.find def_id global_decls in global_name_to_string def.name in + let trait_decl_id_to_string def_id = + let def = TraitDeclId.Map.find def_id trait_decls in + name_to_string def.name + in + let trait_impl_id_to_string def_id = + let def = TraitImplId.Map.find def_id trait_impls in + name_to_string def.name + in + let trait_clause_id_to_string id = + Print.PT.trait_clause_id_to_pretty_string id + in { type_var_id_to_string; const_generic_var_id_to_string; @@ -151,6 +198,9 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) adt_field_to_string; fun_decl_id_to_string; global_decl_id_to_string; + trait_decl_id_to_string; + trait_impl_id_to_string; + trait_clause_id_to_string; } let assumed_ty_to_string (aty : assumed_ty) : string = @@ -182,20 +232,18 @@ let const_generic_to_string (fmt : type_formatter) (cg : T.const_generic) : let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string = match ty with - | Adt (id, tys, cgs) -> ( - let tys = List.map (ty_to_string fmt false) tys in - let cgs = List.map (const_generic_to_string fmt) cgs in - let params = List.append tys cgs in + | Adt (id, generics) -> ( match id with | Tuple -> - assert (cgs = []); - "(" ^ String.concat " * " tys ^ ")" + let generics = generic_args_to_strings fmt false generics in + "(" ^ String.concat " * " generics ^ ")" | AdtId _ | Assumed _ -> - let params_s = - if params = [] then "" else " " ^ String.concat " " params + let generics = generic_args_to_strings fmt true generics in + let generics_s = + if generics = [] then "" else " " ^ String.concat " " generics in - let ty_s = type_id_to_string fmt id ^ params_s in - if params <> [] && inside then "(" ^ ty_s ^ ")" else ty_s) + let ty_s = type_id_to_string fmt id ^ generics_s in + if generics <> [] && inside then "(" ^ ty_s ^ ")" else ty_s) | TypeVar tv -> fmt.type_var_id_to_string tv | Literal lty -> literal_type_to_string lty | Arrow (arg_ty, ret_ty) -> @@ -204,6 +252,62 @@ let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string = in if inside then "(" ^ ty ^ ")" else ty +and generic_args_to_strings (fmt : type_formatter) (inside : bool) + (generics : generic_args) : string list = + let tys = List.map (ty_to_string fmt inside) generics.types in + let cgs = List.map (const_generic_to_string fmt) generics.const_generics in + let trait_refs = + List.map (trait_ref_to_string fmt inside) generics.trait_refs + in + List.concat [ tys; cgs; trait_refs ] + +and generic_args_to_string (fmt : type_formatter) (generics : generic_args) : + string = + String.concat " " (generic_args_to_strings fmt true generics) + +and trait_ref_to_string (fmt : type_formatter) (inside : bool) (tr : trait_ref) + : string = + let trait_id = trait_instance_id_to_string fmt false tr.trait_id in + let generics = generic_args_to_string fmt tr.generics in + let s = trait_id ^ generics in + if tr.generics = empty_generic_args || not inside then s else "(" ^ s ^ ")" + +and trait_instance_id_to_string (fmt : type_formatter) (inside : bool) + (id : trait_instance_id) : string = + match id with + | Self -> "Self" + | TraitImpl id -> fmt.trait_impl_id_to_string id + | Clause id -> fmt.trait_clause_id_to_string id + | ParentClause (inst_id, clause_id) -> + let inst_id = trait_instance_id_to_string fmt false inst_id in + let clause_id = fmt.trait_clause_id_to_string clause_id in + "parent(" ^ inst_id ^ ")::" ^ clause_id + | ItemClause (inst_id, item_name, clause_id) -> + let inst_id = trait_instance_id_to_string fmt false inst_id in + let clause_id = fmt.trait_clause_id_to_string clause_id in + "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]" + | TraitRef tr -> trait_ref_to_string fmt inside tr + | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")" + +let trait_clause_to_string (fmt : type_formatter) (clause : trait_clause) : + string = + let clause_id = fmt.trait_clause_id_to_string clause.clause_id in + let trait_id = fmt.trait_decl_id_to_string clause.trait_id in + let generics = generic_args_to_strings fmt true clause.generics in + let generics = + if generics = [] then "" else " " ^ String.concat " " generics + in + "[" ^ clause_id ^ "]: " ^ trait_id ^ generics + +let generic_params_to_strings (fmt : type_formatter) (generics : generic_params) + : string list = + let tys = List.map type_var_to_string generics.types in + let cgs = List.map const_generic_var_to_string generics.const_generics in + let trait_clauses = + List.map (trait_clause_to_string fmt) generics.trait_clauses + in + List.concat [ tys; cgs; trait_clauses ] + let field_to_string fmt inside (f : field) : string = match f.field_name with | None -> ty_to_string fmt inside f.field_ty @@ -217,11 +321,10 @@ let variant_to_string fmt (v : variant) : 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 = - if types = [] then "" - else " " ^ String.concat " " (List.map type_var_to_string types) + if def.generics = empty_generic_params then "" + else " " ^ String.concat " " (generic_params_to_strings fmt def.generics) in match def.kind with | Struct fields -> @@ -353,10 +456,10 @@ let adt_g_value_to_string (fmt : value_formatter) (field_values : 'v list) (ty : ty) : string = let field_values = List.map value_to_string field_values in match ty with - | Adt (Tuple, _, _) -> + | Adt (Tuple, _) -> (* Tuple *) "(" ^ String.concat ", " field_values ^ ")" - | Adt (AdtId def_id, _, _) -> + | Adt (AdtId def_id, _) -> (* "Regular" ADT *) let adt_ident = match variant_id with @@ -378,7 +481,7 @@ let adt_g_value_to_string (fmt : value_formatter) let field_values = String.concat " " field_values in adt_ident ^ " { " ^ field_values ^ " }" else adt_ident - | Adt (Assumed aty, _, _) -> ( + | Adt (Assumed aty, _) -> ( (* Assumed type *) match aty with | State -> @@ -631,7 +734,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string) (* There are two possibilities: either the [app] is an instantiated, * top-level qualifier (function, ADT constructore...), or it is a "regular" * expression *) - let app, tys = + let app, generics = match app.e with | Qualif qualif -> (* Qualifier case *) @@ -656,9 +759,9 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string) in (* Convert the type instantiation *) let ty_fmt = ast_to_type_formatter fmt in - let tys = List.map (ty_to_string ty_fmt true) qualif.type_args in + let generics = generic_args_to_strings ty_fmt true qualif.generics in (* *) - (qualif_s, tys) + (qualif_s, generics) | _ -> (* "Regular" expression case *) let inside = args <> [] || (args = [] && inside) in @@ -673,7 +776,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string) texpression_to_string fmt inside indent1 indent_incr in let args = List.map arg_to_string args in - let all_args = List.append tys args in + let all_args = List.append generics args in (* Put together *) let e = if all_args = [] then app else app ^ " " ^ String.concat " " all_args diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 55513cc2..147c14b9 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -13,6 +13,9 @@ module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId module FunDeclId = A.FunDeclId module GlobalDeclId = A.GlobalDeclId +module TraitDeclId = T.TraitDeclId +module TraitImplId = T.TraitImplId +module TraitClauseId = T.TraitClauseId (** We redefine identifiers for loop: in {!Values}, the identifiers are global (they monotonically increase across functions) while in {!module:Pure} we want @@ -38,6 +41,10 @@ type integer_type = T.integer_type [@@deriving show, ord] type const_generic_var = T.const_generic_var [@@deriving show, ord] type const_generic = T.const_generic [@@deriving show, ord] type const_generic_var_id = T.const_generic_var_id [@@deriving show, ord] +type trait_decl_id = T.trait_decl_id [@@deriving show, ord] +type trait_impl_id = T.trait_impl_id [@@deriving show, ord] +type trait_clause_id = T.trait_clause_id [@@deriving show, ord] +type trait_item_name = T.trait_item_name [@@deriving show, ord] (** The assumed types for the pure AST. @@ -177,6 +184,14 @@ class ['self] iter_ty_base = inherit! [_] T.iter_const_generic inherit! [_] PV.iter_literal_type method visit_type_var_id : 'env -> type_var_id -> unit = fun _ _ -> () + method visit_trait_decl_id : 'env -> trait_decl_id -> unit = fun _ _ -> () + method visit_trait_impl_id : 'env -> trait_impl_id -> unit = fun _ _ -> () + + method visit_trait_clause_id : 'env -> trait_clause_id -> unit = + fun _ _ -> () + + method visit_trait_item_name : 'env -> trait_item_name -> unit = + fun _ _ -> () end (** Ancestor for map visitor for [ty] *) @@ -186,6 +201,18 @@ class ['self] map_ty_base = inherit! [_] T.map_const_generic inherit! [_] PV.map_literal_type method visit_type_var_id : 'env -> type_var_id -> type_var_id = fun _ x -> x + + method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id = + fun _ x -> x + + method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id = + fun _ x -> x + + method visit_trait_clause_id : 'env -> trait_clause_id -> trait_clause_id = + fun _ x -> x + + method visit_trait_item_name : 'env -> trait_item_name -> trait_item_name = + fun _ x -> x end (** Ancestor for reduce visitor for [ty] *) @@ -195,6 +222,18 @@ class virtual ['self] reduce_ty_base = inherit! [_] T.reduce_const_generic inherit! [_] PV.reduce_literal_type method visit_type_var_id : 'env -> type_var_id -> 'a = fun _ _ -> self#zero + + method visit_trait_decl_id : 'env -> trait_decl_id -> 'a = + fun _ _ -> self#zero + + method visit_trait_impl_id : 'env -> trait_impl_id -> 'a = + fun _ _ -> self#zero + + method visit_trait_clause_id : 'env -> trait_clause_id -> 'a = + fun _ _ -> self#zero + + method visit_trait_item_name : 'env -> trait_item_name -> 'a = + fun _ _ -> self#zero end (** Ancestor for mapreduce visitor for [ty] *) @@ -206,10 +245,24 @@ class virtual ['self] mapreduce_ty_base = method visit_type_var_id : 'env -> type_var_id -> type_var_id * 'a = fun _ x -> (x, self#zero) + + method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id * 'a = + fun _ x -> (x, self#zero) + + method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id * 'a = + fun _ x -> (x, self#zero) + + method visit_trait_clause_id + : 'env -> trait_clause_id -> trait_clause_id * 'a = + fun _ x -> (x, self#zero) + + method visit_trait_item_name + : 'env -> trait_item_name -> trait_item_name * 'a = + fun _ x -> (x, self#zero) end type ty = - | Adt of type_id * ty list * const_generic list + | Adt of type_id * generic_args (** {!Adt} encodes ADTs and tuples and assumed types. TODO: what about the ended regions? (ADTs may be parameterized @@ -220,6 +273,23 @@ type ty = | TypeVar of type_var_id | Literal of literal_type | Arrow of ty * ty + +and trait_ref = { trait_id : trait_instance_id; generics : generic_args } + +and generic_args = { + types : ty list; + const_generics : const_generic list; + trait_refs : trait_ref list; +} + +and trait_instance_id = + | Self + | TraitImpl of trait_impl_id + | Clause of trait_clause_id + | ParentClause of trait_instance_id * trait_clause_id + | ItemClause of trait_instance_id * trait_item_name * trait_clause_id + | TraitRef of trait_ref + | UnknownTrait of string [@@deriving show, visitors @@ -265,11 +335,24 @@ type type_decl_kind = Struct of field list | Enum of variant list | Opaque type type_var = T.type_var [@@deriving show] +type trait_clause = { + clause_id : trait_clause_id; + trait_id : trait_decl_id; + generics : generic_args; +} +[@@deriving show] + +type generic_params = { + types : type_var list; + const_generics : const_generic_var list; + trait_clauses : trait_clause list; +} +[@@deriving show] + type type_decl = { def_id : TypeDeclId.id; name : name; - type_params : type_var list; - const_generic_params : const_generic_var list; + generics : generic_params; kind : type_decl_kind; } [@@deriving show] @@ -463,18 +546,13 @@ type qualif_id = | Proj of projection (** Field projector *) [@@deriving show] -(** An instantiated qualified. +(** An instantiated qualifier. Note that for now we have a clear separation between types and expressions, - which explains why we have the [type_params] field: a function or ADT + which explains why we have the [generics] field: a function or ADT constructor is always fully instantiated. *) -type qualif = { - id : qualif_id; - type_args : ty list; - const_generic_args : const_generic list; -} -[@@deriving show] +type qualif = { id : qualif_id; generics : generic_args } [@@deriving show] type field_id = FieldId.id [@@deriving show, ord] type var_id = VarId.id [@@deriving show, ord] diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index d145ce93..77b12811 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -9,17 +9,19 @@ open PureUtils of fields is fixed: it shouldn't be used for arrays, slices, etc. *) let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t) - (type_id : type_id) (variant_id : VariantId.id option) (tys : ty list) - (cgs : const_generic list) : ty list = + (type_id : type_id) (variant_id : VariantId.id option) + (generics : generic_args) : ty list = match type_id with | Tuple -> (* Tuple *) + assert (generics.const_generics = []); + assert (generics.trait_refs = []); assert (variant_id = None); - tys + generics.types | AdtId def_id -> (* "Regular" ADT *) let def = TypeDeclId.Map.find def_id type_decls in - type_decl_get_instantiated_fields_types def variant_id tys cgs + type_decl_get_instantiated_fields_types def variant_id generics | Assumed aty -> ( (* Assumed type *) match aty with @@ -27,14 +29,14 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t) (* This type is opaque *) raise (Failure "Unreachable: opaque type") | Result -> - let ty = Collections.List.to_cons_nil tys in + let ty = Collections.List.to_cons_nil generics.types in let variant_id = Option.get variant_id in if variant_id = result_return_id then [ ty ] else if variant_id = result_fail_id then [ mk_error_ty ] else raise (Failure "Unreachable: improper variant id for result type") | Error -> - assert (tys = []); + assert (generics = empty_generic_args); let variant_id = Option.get variant_id in assert ( variant_id = error_failure_id || variant_id = error_out_of_fuel_id); @@ -45,14 +47,14 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t) else if variant_id = fuel_succ_id then [ mk_fuel_ty ] else raise (Failure "Unreachable: improper variant id for fuel type") | Option -> - let ty = Collections.List.to_cons_nil tys in + let ty = Collections.List.to_cons_nil generics.types in let variant_id = Option.get variant_id in if variant_id = option_some_id then [ ty ] else if variant_id = option_none_id then [] else raise (Failure "Unreachable: improper variant id for option type") | Range -> - let ty = Collections.List.to_cons_nil tys in + let ty = Collections.List.to_cons_nil generics.types in assert (variant_id = None); [ ty; ty ] | Vec | Array | Slice | Str -> @@ -88,12 +90,13 @@ let rec check_typed_pattern (ctx : tc_ctx) (v : typed_pattern) : tc_ctx = { ctx with env } | PatAdt av -> (* Compute the field types *) - let type_id, tys, cgs = ty_as_adt v.ty in + let type_id, generics = ty_as_adt v.ty in let field_tys = - get_adt_field_types ctx.type_decls type_id av.variant_id tys cgs + get_adt_field_types ctx.type_decls type_id av.variant_id generics in let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx = if ty <> v.ty then ( + (* TODO: we need to normalize the types *) log#serror ("check_typed_pattern: not the same types:" ^ "\n- ty: " ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty); @@ -142,31 +145,29 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = (* Note we can only project fields of structures (not enumerations) *) (* Deconstruct the projector type *) let adt_ty, field_ty = destruct_arrow e.ty in - let adt_id, adt_type_args, adt_cg_args = ty_as_adt adt_ty in + let adt_id, adt_generics = ty_as_adt adt_ty in (* Check the ADT type *) assert (adt_id = proj_adt_id); - assert (adt_type_args = qualif.type_args); - assert (adt_cg_args = qualif.const_generic_args); + assert (adt_generics = qualif.generics); (* Retrieve and check the expected field type *) let variant_id = None in let expected_field_tys = get_adt_field_types ctx.type_decls proj_adt_id variant_id - qualif.type_args qualif.const_generic_args + qualif.generics in let expected_field_ty = FieldId.nth expected_field_tys field_id in assert (expected_field_ty = field_ty) | AdtCons id -> ( let expected_field_tys = get_adt_field_types ctx.type_decls id.adt_id id.variant_id - qualif.type_args qualif.const_generic_args + qualif.generics in let field_tys, adt_ty = destruct_arrows e.ty in assert (expected_field_tys = field_tys); match adt_ty with - | Adt (type_id, tys, cgs) -> + | Adt (type_id, generics) -> assert (type_id = id.adt_id); - assert (tys = qualif.type_args); - assert (cgs = qualif.const_generic_args) + assert (generics = qualif.generics) | _ -> raise (Failure "Unreachable"))) | Let (monadic, pat, re, e_next) -> let expected_pat_ty = if monadic then destruct_result re.ty else re.ty in @@ -212,15 +213,14 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = | Some ty -> assert (ty = e.ty)); (* Check the fields *) (* Retrieve and check the expected field type *) - let adt_id, adt_type_args, adt_cg_args = ty_as_adt e.ty in + let adt_id, adt_generics = ty_as_adt e.ty in assert (adt_id = supd.struct_id); (* The id can only be: a custom type decl or an array *) match adt_id with | AdtId _ -> let variant_id = None in let expected_field_tys = - get_adt_field_types ctx.type_decls adt_id variant_id adt_type_args - adt_cg_args + get_adt_field_types ctx.type_decls adt_id variant_id adt_generics in List.iter (fun (fid, fe) -> @@ -229,7 +229,9 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = check_texpression ctx fe) supd.updates | Assumed Array -> - let expected_field_ty = Collections.List.to_cons_nil adt_type_args in + let expected_field_ty = + Collections.List.to_cons_nil adt_generics.types + in List.iter (fun (_, fe) -> assert (expected_field_ty = fe.ty); diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index f099ef9c..1357793b 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -89,14 +89,31 @@ let mk_mplace (var_id : E.VarId.id) (name : string option) (projection : mprojection) : mplace = { var_id; name; projection } +let empty_generic_params : generic_params = + { types = []; const_generics = []; trait_clauses = [] } + +let empty_generic_args : generic_args = + { types = []; const_generics = []; trait_refs = [] } + +let mk_generic_args_from_types (types : ty list) : generic_args = + { types; const_generics = []; trait_refs = [] } + +type subst = { + ty_subst : TypeVarId.id -> ty; + cg_subst : ConstGenericVarId.id -> const_generic; + tr_subst : TraitClauseId.id -> trait_instance_id; + tr_self : trait_instance_id; +} + (** Type substitution *) -let ty_substitute (tsubst : TypeVarId.id -> ty) - (cgsubst : ConstGenericVarId.id -> const_generic) (ty : ty) : ty = +let ty_substitute (subst : subst) (ty : ty) : ty = let obj = object inherit [_] map_ty - method! visit_TypeVar _ var_id = tsubst var_id - method! visit_ConstGenericVar _ var_id = cgsubst var_id + method! visit_TypeVar _ var_id = subst.ty_subst var_id + method! visit_ConstGenericVar _ var_id = subst.cg_subst var_id + method! visit_Clause _ id = subst.tr_subst id + method! visit_Self _ = subst.tr_self end in obj#visit_ty () ty @@ -115,6 +132,18 @@ let make_const_generic_subst (vars : const_generic_var list) (cgs : const_generic list) : ConstGenericVarId.id -> const_generic = Substitute.make_const_generic_subst_from_vars vars cgs +let make_trait_subst (clauses : trait_clause list) (refs : trait_ref list) : + TraitClauseId.id -> trait_instance_id = + let clauses = List.map (fun x -> x.clause_id) clauses in + let refs = List.map (fun x -> TraitRef x) refs in + let ls = List.combine clauses refs in + let mp = + List.fold_left + (fun mp (k, v) -> TraitClauseId.Map.add k v mp) + TraitClauseId.Map.empty ls + in + fun id -> TraitClauseId.Map.find id mp + (** Retrieve the list of fields for the given variant of a {!type:Aeneas.Pure.type_decl}. Raises [Invalid_argument] if the arguments are incorrect. @@ -135,20 +164,27 @@ let type_decl_get_fields (def : type_decl) - def: " ^ show_type_decl def ^ "\n- opt_variant_id: " ^ opt_variant_id)) +let make_subst_from_generics (params : generic_params) (args : generic_args) + (tr_self : trait_instance_id) : subst = + let ty_subst = make_type_subst params.types args.types in + let cg_subst = + make_const_generic_subst params.const_generics args.const_generics + in + let tr_subst = make_trait_subst params.trait_clauses args.trait_refs in + { ty_subst; cg_subst; tr_subst; tr_self } + (** Instantiate the type variables for the chosen variant in an ADT definition, and return the list of the types of its fields *) let type_decl_get_instantiated_fields_types (def : type_decl) - (opt_variant_id : VariantId.id option) (types : ty list) - (cgs : const_generic list) : ty list = - let ty_subst = make_type_subst def.type_params types in - let cg_subst = make_const_generic_subst def.const_generic_params cgs in + (opt_variant_id : VariantId.id option) (generics : generic_args) : ty list = + (* There shouldn't be any reference to Self *) + let tr_self = UnknownTrait __FUNCTION__ in + let subst = make_subst_from_generics def.generics generics tr_self in let fields = type_decl_get_fields def opt_variant_id in - List.map (fun f -> ty_substitute ty_subst cg_subst f.field_ty) fields + List.map (fun f -> ty_substitute subst f.field_ty) fields -let fun_sig_substitute (tsubst : TypeVarId.id -> ty) - (cgsubst : ConstGenericVarId.id -> const_generic) (sg : fun_sig) : - inst_fun_sig = - let subst = ty_substitute tsubst cgsubst in +let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig = + let subst = ty_substitute subst in let inputs = List.map subst sg.inputs in let output = subst sg.output in let doutputs = List.map subst sg.doutputs in @@ -194,9 +230,9 @@ let is_global (e : texpression) : bool = let is_const (e : texpression) : bool = match e.e with Const _ -> true | _ -> false -let ty_as_adt (ty : ty) : type_id * ty list * const_generic list = +let ty_as_adt (ty : ty) : type_id * generic_args = match ty with - | Adt (id, tys, cgs) -> (id, tys, cgs) + | Adt (id, generics) -> (id, generics) | _ -> raise (Failure "Unreachable") (** Remove the external occurrences of {!Meta} *) @@ -294,28 +330,30 @@ let destruct_qualif_app (e : texpression) : qualif * texpression list = (** Destruct an expression into a function call, if possible *) let opt_destruct_function_call (e : texpression) : - (fun_or_op_id * ty list * texpression list) option = + (fun_or_op_id * generic_args * texpression list) option = match opt_destruct_qualif_app e with | None -> None | Some (qualif, args) -> ( match qualif.id with - | FunOrOp fun_id -> Some (fun_id, qualif.type_args, args) + | FunOrOp fun_id -> Some (fun_id, qualif.generics, args) | _ -> None) let opt_destruct_result (ty : ty) : ty option = match ty with - | Adt (Assumed Result, tys, cgs) -> - assert (cgs = []); - Some (Collections.List.to_cons_nil tys) + | Adt (Assumed Result, generics) -> + assert (generics.const_generics = []); + assert (generics.trait_refs = []); + Some (Collections.List.to_cons_nil generics.types) | _ -> None let destruct_result (ty : ty) : ty = Option.get (opt_destruct_result ty) let opt_destruct_tuple (ty : ty) : ty list option = match ty with - | Adt (Tuple, tys, cgs) -> - assert (cgs = []); - Some tys + | Adt (Tuple, generics) -> + assert (generics.const_generics = []); + assert (generics.trait_refs = []); + Some generics.types | _ -> None let mk_abs (x : typed_pattern) (e : texpression) : texpression = @@ -387,14 +425,16 @@ let mk_switch (scrut : texpression) (sb : switch_body) : texpression = - if there is > one type: wrap them in a tuple *) let mk_simpl_tuple_ty (tys : ty list) : ty = - match tys with [ ty ] -> ty | _ -> Adt (Tuple, tys, []) + match tys with + | [ ty ] -> ty + | _ -> Adt (Tuple, mk_generic_args_from_types tys) let mk_bool_ty : ty = Literal Bool -let mk_unit_ty : ty = Adt (Tuple, [], []) +let mk_unit_ty : ty = Adt (Tuple, empty_generic_args) let mk_unit_rvalue : texpression = let id = AdtCons { adt_id = Tuple; variant_id = None } in - let qualif = { id; type_args = []; const_generic_args = [] } in + let qualif = { id; generics = empty_generic_args } in let e = Qualif qualif in let ty = mk_unit_ty in { e; ty } @@ -434,7 +474,7 @@ let mk_simpl_tuple_pattern (vl : typed_pattern list) : typed_pattern = | [ v ] -> v | _ -> let tys = List.map (fun (v : typed_pattern) -> v.ty) vl in - let ty = Adt (Tuple, tys, []) in + let ty = Adt (Tuple, mk_generic_args_from_types tys) in let value = PatAdt { variant_id = None; field_values = vl } in { value; ty } @@ -445,11 +485,11 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression = | _ -> (* Compute the types of the fields, and the type of the tuple constructor *) let tys = List.map (fun (v : texpression) -> v.ty) vl in - let ty = Adt (Tuple, tys, []) in + let ty = Adt (Tuple, mk_generic_args_from_types tys) in let ty = mk_arrows tys ty in (* Construct the tuple constructor qualifier *) let id = AdtCons { adt_id = Tuple; variant_id = None } in - let qualif = { id; type_args = tys; const_generic_args = [] } in + let qualif = { id; generics = mk_generic_args_from_types tys } in (* Put everything together *) let cons = { e = Qualif qualif; ty } in mk_apps cons vl @@ -467,32 +507,36 @@ let ty_as_integer (t : ty) : T.integer_type = let ty_as_literal (t : ty) : T.literal_type = match t with Literal ty -> ty | _ -> raise (Failure "Unreachable") -let mk_state_ty : ty = Adt (Assumed State, [], []) -let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ], []) -let mk_error_ty : ty = Adt (Assumed Error, [], []) -let mk_fuel_ty : ty = Adt (Assumed Fuel, [], []) +let mk_state_ty : ty = Adt (Assumed State, empty_generic_args) + +let mk_result_ty (ty : ty) : ty = + Adt (Assumed Result, mk_generic_args_from_types [ ty ]) + +let mk_error_ty : ty = Adt (Assumed Error, empty_generic_args) +let mk_fuel_ty : ty = Adt (Assumed Fuel, empty_generic_args) let mk_error (error : VariantId.id) : texpression = let ty = mk_error_ty in let id = AdtCons { adt_id = Assumed Error; variant_id = Some error } in - let qualif = { id; type_args = []; const_generic_args = [] } in + let qualif = { id; generics = empty_generic_args } in let e = Qualif qualif in { e; ty } let unwrap_result_ty (ty : ty) : ty = match ty with - | Adt (Assumed Result, [ ty ], cgs) -> - assert (cgs = []); + | Adt + (Assumed Result, { types = [ ty ]; const_generics = []; trait_refs = [] }) + -> ty | _ -> raise (Failure "not a result type") let mk_result_fail_texpression (error : texpression) (ty : ty) : texpression = let type_args = [ ty ] in - let ty = Adt (Assumed Result, type_args, []) in + let ty = Adt (Assumed Result, mk_generic_args_from_types type_args) in let id = AdtCons { adt_id = Assumed Result; variant_id = Some result_fail_id } in - let qualif = { id; type_args; const_generic_args = [] } in + let qualif = { id; generics = mk_generic_args_from_types type_args } in let cons_e = Qualif qualif in let cons_ty = mk_arrow error.ty ty in let cons = { e = cons_e; ty = cons_ty } in @@ -505,11 +549,11 @@ let mk_result_fail_texpression_with_error_id (error : VariantId.id) (ty : ty) : let mk_result_return_texpression (v : texpression) : texpression = let type_args = [ v.ty ] in - let ty = Adt (Assumed Result, type_args, []) in + let ty = Adt (Assumed Result, mk_generic_args_from_types type_args) in let id = AdtCons { adt_id = Assumed Result; variant_id = Some result_return_id } in - let qualif = { id; type_args; const_generic_args = [] } in + let qualif = { id; generics = mk_generic_args_from_types type_args } in let cons_e = Qualif qualif in let cons_ty = mk_arrow v.ty ty in let cons = { e = cons_e; ty = cons_ty } in @@ -518,7 +562,7 @@ let mk_result_return_texpression (v : texpression) : texpression = (** Create a [Fail err] pattern which captures the error *) let mk_result_fail_pattern (error_pat : pattern) (ty : ty) : typed_pattern = let error_pat : typed_pattern = { value = error_pat; ty = mk_error_ty } in - let ty = Adt (Assumed Result, [ ty ], []) in + let ty = Adt (Assumed Result, mk_generic_args_from_types [ ty ]) in let value = PatAdt { variant_id = Some result_fail_id; field_values = [ error_pat ] } in @@ -530,7 +574,7 @@ let mk_result_fail_pattern_ignore_error (ty : ty) : typed_pattern = mk_result_fail_pattern error_pat ty let mk_result_return_pattern (v : typed_pattern) : typed_pattern = - let ty = Adt (Assumed Result, [ v.ty ], []) in + let ty = Adt (Assumed Result, mk_generic_args_from_types [ v.ty ]) in let value = PatAdt { variant_id = Some result_return_id; field_values = [ v ] } in @@ -565,11 +609,11 @@ let rec typed_pattern_to_texpression (pat : typed_pattern) : texpression option let fields_values = List.map (fun e -> Option.get e) fields in (* Retrieve the type id and the type args from the pat type (simpler this way *) - let adt_id, type_args, const_generic_args = ty_as_adt pat.ty in + let adt_id, generics = ty_as_adt pat.ty in (* Create the constructor *) let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in - let qualif = { id = qualif_id; type_args; const_generic_args } in + let qualif = { id = qualif_id; generics } in let cons_e = Qualif qualif in let field_tys = List.map (fun (v : texpression) -> v.ty) fields_values diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index 38850243..64e7716a 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -9,51 +9,53 @@ module E = Expressions module A = LlbcAst module C = Contexts -(** Substitute types variables and regions in a type. *) -let ty_substitute (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : 'r1 T.ty) : - 'r2 T.ty = - let open T in - let visitor = - object - inherit [_] map_ty - method visit_'r _ r = rsubst r - method! visit_TypeVar _ id = tsubst id - - method! visit_type_var_id _ _ = - (* We should never get here because we reimplemented [visit_TypeVar] *) - raise (Failure "Unexpected") +type ('r1, 'r2) subst = { + r_subst : 'r1 -> 'r2; + ty_subst : T.TypeVarId.id -> 'r2 T.ty; + cg_subst : T.ConstGenericVarId.id -> T.const_generic; + (** Substitution from *local* trait clause to trait instance *) + tr_subst : T.TraitClauseId.id -> 'r2 T.trait_instance_id; + (** Substitution for the [Self] trait instance *) + tr_self : 'r2 T.trait_instance_id; +} + +let ty_substitute_visitor (subst : ('r1, 'r2) subst) = + object + inherit [_] T.map_ty + method visit_'r _ r = subst.r_subst r + method! visit_TypeVar _ id = subst.ty_subst id - method! visit_ConstGenericVar _ id = cgsubst id + method! visit_type_var_id _ _ = + (* We should never get here because we reimplemented [visit_TypeVar] *) + raise (Failure "Unexpected") - method! visit_const_generic_var_id _ _ = - (* We should never get here because we reimplemented [visit_Var] *) - raise (Failure "Unexpected") - end - in + method! visit_ConstGenericVar _ id = subst.cg_subst id - visitor#visit_ty () ty + method! visit_const_generic_var_id _ _ = + (* We should never get here because we reimplemented [visit_Var] *) + raise (Failure "Unexpected") -let rty_substitute (rsubst : T.RegionId.id -> T.RegionId.id) - (tsubst : T.TypeVarId.id -> T.rty) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : T.rty) : T.rty = - let rsubst r = - match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid) - in - ty_substitute rsubst tsubst cgsubst ty + method! visit_Clause _ id = subst.tr_subst id + method! visit_Self _ = subst.tr_self + end -let ety_substitute (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : T.ety) : T.ety = - let rsubst r = r in - ty_substitute rsubst tsubst cgsubst ty +(** Substitute types variables and regions in a type. *) +let ty_substitute (subst : ('r1, 'r2) subst) (ty : 'r1 T.ty) : 'r2 T.ty = + let visitor = ty_substitute_visitor subst in + visitor#visit_ty () ty (** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *) let erase_regions (ty : T.rty) : T.ety = - ty_substitute - (fun _ -> T.Erased) - (fun vid -> T.TypeVar vid) - (fun id -> T.ConstGenericVar id) - ty + let subst = + { + r_subst = (fun _ -> T.Erased); + ty_subst = (fun vid -> T.TypeVar vid); + cg_subst = (fun id -> T.ConstGenericVar id); + tr_subst = (fun id -> T.Clause id); + tr_self = T.Self; + } + in + ty_substitute subst ty (** Generate fresh regions for region variables. @@ -78,18 +80,20 @@ let fresh_regions_with_substs (region_vars : T.region_var list) : (* Generate the substitution from region var id to region *) let rid_subst id = T.RegionVarId.Map.find id rid_map in (* Generate the substitution from region to region *) - let rsubst r = + let r_subst r = match r with T.Static -> T.Static | T.Var id -> T.Var (rid_subst id) in (* Return *) - (fresh_region_ids, rid_subst, rsubst) + (fresh_region_ids, rid_subst, r_subst) -(** Erase the regions in a type and substitute the type variables *) -let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) - (ty : 'r T.region T.ty) : T.ety = - let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in - ty_substitute rsubst tsubst cgsubst ty +(** Erase the regions in a type and perform a substitution *) +let erase_regions_substitute_types (ty_subst : T.TypeVarId.id -> T.ety) + (cg_subst : T.ConstGenericVarId.id -> T.const_generic) + (tr_subst : T.TraitClauseId.id -> T.etrait_instance_id) + (tr_self : T.etrait_instance_id) (ty : 'r T.ty) : T.ety = + let r_subst (_ : 'r) : T.erased_region = T.Erased in + let subst = { r_subst; ty_subst; cg_subst; tr_subst; tr_self } in + ty_substitute subst ty (** Create a region substitution from a list of region variable ids and a list of regions (with which to substitute the region variable ids *) @@ -146,16 +150,62 @@ let make_const_generic_subst_from_vars (vars : T.const_generic_var list) (List.map (fun (x : T.const_generic_var) -> x.T.index) vars) cgs -(** Instantiate the type variables in an ADT definition, and return, for - every variant, the list of the types of its fields *) -let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl) - (regions : T.RegionId.id T.region list) (types : T.rty list) - (cgs : T.const_generic list) : (T.VariantId.id option * T.rty list) list = - let r_subst = make_region_subst_from_vars def.T.region_params regions in - let ty_subst = make_type_subst_from_vars def.T.type_params types in +(** Create a trait substitution from a list of trait clause ids and a list of + trait refs *) +let make_trait_subst (clause_ids : T.TraitClauseId.id list) + (trs : 'r T.trait_ref list) : T.TraitClauseId.id -> 'r T.trait_instance_id = + let ls = List.combine clause_ids trs in + let mp = + List.fold_left + (fun mp (k, v) -> T.TraitClauseId.Map.add k (T.TraitRef v) mp) + T.TraitClauseId.Map.empty ls + in + fun id -> T.TraitClauseId.Map.find id mp + +let make_trait_subst_from_clauses (clauses : T.trait_clause list) + (trs : 'r T.trait_ref list) : T.TraitClauseId.id -> 'r T.trait_instance_id = + make_trait_subst + (List.map (fun (x : T.trait_clause) -> x.T.clause_id) clauses) + trs + +let make_subst_from_generics (params : T.generic_params) + (args : 'r T.generic_args) (tr_self : 'r T.trait_instance_id) : + (T.region_var_id T.region, 'r) subst = + let r_subst = make_region_subst_from_vars params.T.regions args.T.regions in + let ty_subst = make_type_subst_from_vars params.T.types args.T.types in + let cg_subst = + make_const_generic_subst_from_vars params.T.const_generics + args.T.const_generics + in + let tr_subst = + make_trait_subst_from_clauses params.T.trait_clauses args.T.trait_refs + in + { r_subst; ty_subst; cg_subst; tr_subst; tr_self } + +let make_esubst_from_generics (params : T.generic_params) + (generics : T.egeneric_args) (tr_self : T.etrait_instance_id) = + let r_subst _ = T.Erased in + let ty_subst = make_type_subst_from_vars params.types generics.T.types in let cg_subst = - make_const_generic_subst_from_vars def.T.const_generic_params cgs + make_const_generic_subst_from_vars params.const_generics + generics.T.const_generics in + let tr_subst = + make_trait_subst_from_clauses params.trait_clauses generics.T.trait_refs + in + { r_subst; ty_subst; cg_subst; tr_subst; tr_self } + +(** Instantiate the type variables in an ADT definition, and return, for + every variant, the list of the types of its fields. + + **IMPORTANT**: this function doesn't normalize the types, you may want to + use the [AssociatedTypes] equivalent instead. +*) +let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl) + (generics : T.rgeneric_args) : (T.VariantId.id option * T.rty list) list = + (* There shouldn't be any reference to Self *) + let tr_self = T.UnknownTrait __FUNCTION__ in + let subst = make_subst_from_generics def.T.generics generics tr_self in let (variants_fields : (T.VariantId.id option * T.field list) list) = match def.T.kind with | T.Enum variants -> @@ -171,191 +221,218 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl) in List.map (fun (id, fields) -> - ( id, - List.map - (fun f -> ty_substitute r_subst ty_subst cg_subst f.T.field_ty) - fields )) + (id, List.map (fun f -> ty_substitute subst f.T.field_ty) fields)) variants_fields (** Instantiate the type variables in an ADT definition, and return the list - of types of the fields for the chosen variant *) + of types of the fields for the chosen variant. + + **IMPORTANT**: this function doesn't normalize the types, you may want to + use the [AssociatedTypes] equivalent instead. +*) 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) - (cgs : T.const_generic list) : T.rty list = - let r_subst = make_region_subst_from_vars def.T.region_params regions in - let ty_subst = make_type_subst_from_vars def.T.type_params types in - let cg_subst = - make_const_generic_subst_from_vars def.T.const_generic_params cgs - in + (opt_variant_id : T.VariantId.id option) (generics : T.rgeneric_args) : + T.rty list = + (* For now, check that there are no clauses - otherwise we might need + to normalize the types *) + assert (def.generics.trait_clauses = []); + (* There shouldn't be any reference to Self *) + let tr_self = T.UnknownTrait __FUNCTION__ in + let subst = make_subst_from_generics def.T.generics generics tr_self in let fields = TU.type_decl_get_fields def opt_variant_id in - List.map - (fun f -> ty_substitute r_subst ty_subst cg_subst f.T.field_ty) - fields + List.map (fun f -> ty_substitute subst f.T.field_ty) fields (** Return the types of the properly instantiated ADT's variant, provided a - context *) + context. + + **IMPORTANT**: this function doesn't normalize the types, you may want to + use the [AssociatedTypes] equivalent instead. +*) let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx) (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) - (regions : T.RegionId.id T.region list) (types : T.rty list) - (cgs : T.const_generic list) : T.rty list = + (generics : T.rgeneric_args) : T.rty list = let def = C.ctx_lookup_type_decl ctx def_id in - type_decl_get_instantiated_field_rtypes def opt_variant_id regions types cgs + type_decl_get_instantiated_field_rtypes def opt_variant_id generics (** Return the types of the properly instantiated ADT value (note that - here, ADT is understood in its broad meaning: ADT, assumed value or tuple) *) + here, ADT is understood in its broad meaning: ADT, assumed value or tuple). + + **IMPORTANT**: this function doesn't normalize the types, you may want to + use the [AssociatedTypes] equivalent instead. + *) let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx) - (adt : V.adt_value) (id : T.type_id) - (region_params : T.RegionId.id T.region list) (type_params : T.rty list) - (cg_params : T.const_generic list) : T.rty list = + (adt : V.adt_value) (id : T.type_id) (generics : T.rgeneric_args) : + T.rty list = match id with | T.AdtId id -> (* Retrieve the types of the fields *) - ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id - region_params type_params cg_params + ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id generics | T.Tuple -> - assert (List.length region_params = 0); - type_params + assert (generics.regions = []); + generics.types | T.Assumed aty -> ( match aty with | T.Box | T.Vec -> - assert (List.length region_params = 0); - assert (List.length type_params = 1); - assert (List.length cg_params = 0); - type_params + assert (generics.regions = []); + assert (List.length generics.types = 1); + assert (generics.const_generics = []); + generics.types | T.Option -> - assert (List.length region_params = 0); - assert (List.length type_params = 1); - assert (List.length cg_params = 0); - if adt.V.variant_id = Some T.option_some_id then type_params + assert (generics.regions = []); + assert (List.length generics.types = 1); + assert (generics.const_generics = []); + if adt.V.variant_id = Some T.option_some_id then generics.types else if adt.V.variant_id = Some T.option_none_id then [] else raise (Failure "Unreachable") | T.Range -> - assert (List.length region_params = 0); - assert (List.length type_params = 1); - assert (List.length cg_params = 0); - type_params + assert (generics.regions = []); + assert (List.length generics.types = 1); + assert (generics.const_generics = []); + generics.types | T.Array | T.Slice | T.Str -> (* Those types don't have fields *) raise (Failure "Unreachable")) (** Instantiate the type variables in an ADT definition, and return the list - of types of the fields for the chosen variant *) + of types of the fields for the chosen variant. + + **IMPORTANT**: this function doesn't normalize the types, you may want to + use the [AssociatedTypes] equivalent instead. +*) let type_decl_get_instantiated_field_etypes (def : T.type_decl) - (opt_variant_id : T.VariantId.id option) (types : T.ety list) - (cgs : T.const_generic list) : T.ety list = - let ty_subst = make_type_subst_from_vars def.T.type_params types in - let cg_subst = - make_const_generic_subst_from_vars def.T.const_generic_params cgs + (opt_variant_id : T.VariantId.id option) (generics : T.egeneric_args) : + T.ety list = + (* For now, check that there are no clauses - otherwise we might need + to normalize the types *) + assert (def.generics.trait_clauses = []); + (* There shouldn't be any reference to Self *) + let tr_self : T.erased_region T.trait_instance_id = + T.UnknownTrait __FUNCTION__ + in + let { r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = + make_esubst_from_generics def.T.generics generics tr_self in let fields = TU.type_decl_get_fields def opt_variant_id in List.map - (fun f -> erase_regions_substitute_types ty_subst cg_subst f.T.field_ty) + (fun (f : T.field) -> + erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self + f.T.field_ty) fields (** Return the types of the properly instantiated ADT's variant, provided a - context *) + context. + + **IMPORTANT**: this function doesn't normalize the types, you may want to + use the [AssociatedTypes] equivalent instead. + *) let ctx_adt_get_instantiated_field_etypes (ctx : C.eval_ctx) (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) - (types : T.ety list) (cgs : T.const_generic list) : T.ety list = + (generics : T.egeneric_args) : T.ety list = let def = C.ctx_lookup_type_decl ctx def_id in - type_decl_get_instantiated_field_etypes def opt_variant_id types cgs + type_decl_get_instantiated_field_etypes def opt_variant_id generics -let statement_substitute_visitor (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) = +let statement_substitute_visitor + (subst : (T.erased_region, T.erased_region) subst) = + (* Keep in synch with [ty_substitute_visitor] *) object inherit [_] A.map_statement - method! visit_ety _ ty = ety_substitute tsubst cgsubst ty - method! visit_ConstGenericVar _ id = cgsubst id + method! visit_'r _ r = subst.r_subst r + method! visit_TypeVar _ id = subst.ty_subst id + + method! visit_type_var_id _ _ = + (* We should never get here because we reimplemented [visit_TypeVar] *) + raise (Failure "Unexpected") + + method! visit_ConstGenericVar _ id = subst.cg_subst id method! visit_const_generic_var_id _ _ = (* We should never get here because we reimplemented [visit_Var] *) raise (Failure "Unexpected") + + method! visit_Clause _ id = subst.tr_subst id + method! visit_Self _ = subst.tr_self end (** Apply a type substitution to a place *) -let place_substitute (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (p : E.place) : - E.place = +let place_substitute (subst : (T.erased_region, T.erased_region) subst) + (p : E.place) : E.place = (* There is in fact nothing to do *) - (statement_substitute_visitor tsubst cgsubst)#visit_place () p + (statement_substitute_visitor subst)#visit_place () p (** Apply a type substitution to an operand *) -let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (op : E.operand) : - E.operand = - (statement_substitute_visitor tsubst cgsubst)#visit_operand () op +let operand_substitute (subst : (T.erased_region, T.erased_region) subst) + (op : E.operand) : E.operand = + (statement_substitute_visitor subst)#visit_operand () op (** Apply a type substitution to an rvalue *) -let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (rv : E.rvalue) : - E.rvalue = - (statement_substitute_visitor tsubst cgsubst)#visit_rvalue () rv +let rvalue_substitute (subst : (T.erased_region, T.erased_region) subst) + (rv : E.rvalue) : E.rvalue = + (statement_substitute_visitor subst)#visit_rvalue () rv (** Apply a type substitution to an assertion *) -let assertion_substitute (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (a : A.assertion) : - A.assertion = - (statement_substitute_visitor tsubst cgsubst)#visit_assertion () a +let assertion_substitute (subst : (T.erased_region, T.erased_region) subst) + (a : A.assertion) : A.assertion = + (statement_substitute_visitor subst)#visit_assertion () a (** Apply a type substitution to a call *) -let call_substitute (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (call : A.call) : - A.call = - (statement_substitute_visitor tsubst cgsubst)#visit_call () call +let call_substitute (subst : (T.erased_region, T.erased_region) subst) + (call : A.call) : A.call = + (statement_substitute_visitor subst)#visit_call () call (** Apply a type substitution to a statement *) -let statement_substitute (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (st : A.statement) : - A.statement = - (statement_substitute_visitor tsubst cgsubst)#visit_statement () st +let statement_substitute (subst : (T.erased_region, T.erased_region) subst) + (st : A.statement) : A.statement = + (statement_substitute_visitor subst)#visit_statement () st (** Apply a type substitution to a function body. Return the local variables and the body. *) -let fun_body_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (body : A.fun_body) : +let fun_body_substitute_in_body + (subst : (T.erased_region, T.erased_region) subst) (body : A.fun_body) : A.var list * A.statement = - let rsubst r = r in let locals = List.map - (fun (v : A.var) -> - { v with A.var_ty = ty_substitute rsubst tsubst cgsubst v.A.var_ty }) + (fun (v : A.var) -> { v with A.var_ty = ty_substitute subst v.A.var_ty }) body.A.locals in - let body = statement_substitute tsubst cgsubst body.body in + let body = statement_substitute subst body.body in (locals, body) -(** Substitute a function signature *) +(** Substitute a function signature. + + **IMPORTANT:** this function doesn't normalize the types. + *) let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id) - (rsubst : T.RegionVarId.id -> T.RegionId.id) - (tsubst : T.TypeVarId.id -> T.rty) - (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (sg : A.fun_sig) : - A.inst_fun_sig = - let rsubst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region = - match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid) + (r_subst : T.RegionVarId.id -> T.RegionId.id) + (ty_subst : T.TypeVarId.id -> T.rty) + (cg_subst : T.ConstGenericVarId.id -> T.const_generic) + (tr_subst : T.TraitClauseId.id -> T.rtrait_instance_id) + (tr_self : T.rtrait_instance_id) (sg : A.fun_sig) : A.inst_fun_sig = + let r_subst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region = + match r with T.Static -> T.Static | T.Var rid -> T.Var (r_subst rid) in - let inputs = List.map (ty_substitute rsubst' tsubst cgsubst) sg.A.inputs in - let output = ty_substitute rsubst' tsubst cgsubst sg.A.output in + let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in + let inputs = List.map (ty_substitute subst) sg.A.inputs in + let output = ty_substitute subst sg.A.output in let subst_region_group (rg : T.region_var_group) : A.abs_region_group = let id = asubst rg.id in - let regions = List.map rsubst rg.regions in + let regions = List.map r_subst rg.regions in let parents = List.map asubst rg.parents in { id; regions; parents } in let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in { A.regions_hierarchy; inputs; output } -(** Substitute type variable identifiers in a type *) -let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id) - (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : 'r T.ty) +(** Substitute variable identifiers in a type *) +let ty_substitute_ids (ty_subst : T.TypeVarId.id -> T.TypeVarId.id) + (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : 'r T.ty) : 'r T.ty = let open T in let visitor = object inherit [_] map_ty method visit_'r _ r = r - method! visit_type_var_id _ id = tsubst id - method! visit_const_generic_var_id _ id = cgsubst id + method! visit_type_var_id _ id = ty_subst id + method! visit_const_generic_var_id _ id = cg_subst id end in @@ -371,10 +448,10 @@ let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id) [visit_'r] if we define a class which visits objects of types [ety] and [rty] while inheriting a class which visit [ty]... *) -let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id) +let subst_ids_visitor (r_subst : T.RegionId.id -> T.RegionId.id) (rvsubst : T.RegionVarId.id -> T.RegionVarId.id) - (tsubst : T.TypeVarId.id -> T.TypeVarId.id) - (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) + (ty_subst : T.TypeVarId.id -> T.TypeVarId.id) + (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id) (bsubst : V.BorrowId.id -> V.BorrowId.id) (asubst : V.AbstractionId.id -> V.AbstractionId.id) = @@ -383,10 +460,10 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id) inherit [_] T.map_ty method visit_'r _ r = - match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid) + match r with T.Static -> T.Static | T.Var rid -> T.Var (r_subst rid) - method! visit_type_var_id _ id = tsubst id - method! visit_const_generic_var_id _ id = cgsubst id + method! visit_type_var_id _ id = ty_subst id + method! visit_const_generic_var_id _ id = cg_subst id end in @@ -395,7 +472,7 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id) inherit [_] C.map_env method! visit_borrow_id _ bid = bsubst bid method! visit_loan_id _ bid = bsubst bid - method! visit_ety _ ty = ty_substitute_ids tsubst cgsubst ty + method! visit_ety _ ty = ty_substitute_ids ty_subst cg_subst ty method! visit_rty env ty = subst_rty#visit_ty env ty method! visit_symbolic_value_id _ id = ssubst id @@ -405,7 +482,7 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id) (** We *do* visit meta-values *) method! visit_mvalue env v = self#visit_typed_value env v - method! visit_region_id _ id = rsubst id + method! visit_region_id _ id = r_subst id method! visit_region_var_id _ id = rvsubst id method! visit_abstraction_id _ id = asubst id end @@ -425,20 +502,20 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id) method visit_env (env : C.env) : C.env = visitor#visit_env () env end -let typed_value_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id) +let typed_value_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id) (rvsubst : T.RegionVarId.id -> T.RegionVarId.id) - (tsubst : T.TypeVarId.id -> T.TypeVarId.id) - (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) + (ty_subst : T.TypeVarId.id -> T.TypeVarId.id) + (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id) (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_value) : V.typed_value = let asubst _ = raise (Failure "Unreachable") in - (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst) + (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst) #visit_typed_value v -let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id) +let typed_value_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id) (v : V.typed_value) : V.typed_value = - typed_value_subst_ids rsubst + typed_value_subst_ids r_subst (fun x -> x) (fun x -> x) (fun x -> x) @@ -446,41 +523,41 @@ let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id) (fun x -> x) v -let typed_avalue_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id) +let typed_avalue_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id) (rvsubst : T.RegionVarId.id -> T.RegionVarId.id) - (tsubst : T.TypeVarId.id -> T.TypeVarId.id) - (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) + (ty_subst : T.TypeVarId.id -> T.TypeVarId.id) + (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id) (bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_avalue) : V.typed_avalue = let asubst _ = raise (Failure "Unreachable") in - (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst) + (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst) #visit_typed_avalue v -let abs_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id) +let abs_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id) (rvsubst : T.RegionVarId.id -> T.RegionVarId.id) - (tsubst : T.TypeVarId.id -> T.TypeVarId.id) - (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) + (ty_subst : T.TypeVarId.id -> T.TypeVarId.id) + (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id) (bsubst : V.BorrowId.id -> V.BorrowId.id) (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : V.abs) : V.abs = - (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst) + (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst) #visit_abs x -let env_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id) +let env_subst_ids (r_subst : T.RegionId.id -> T.RegionId.id) (rvsubst : T.RegionVarId.id -> T.RegionVarId.id) - (tsubst : T.TypeVarId.id -> T.TypeVarId.id) - (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) + (ty_subst : T.TypeVarId.id -> T.TypeVarId.id) + (cg_subst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id) (bsubst : V.BorrowId.id -> V.BorrowId.id) (asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : C.env) : C.env = - (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst) + (subst_ids_visitor r_subst rvsubst ty_subst cg_subst ssubst bsubst asubst) #visit_env x -let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id) +let typed_avalue_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id) (x : V.typed_avalue) : V.typed_avalue = let asubst _ = raise (Failure "Unreachable") in - (subst_ids_visitor rsubst + (subst_ids_visitor r_subst (fun x -> x) (fun x -> x) (fun x -> x) @@ -490,9 +567,9 @@ let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id) #visit_typed_avalue x -let env_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id) (x : C.env) : C.env - = - (subst_ids_visitor rsubst +let env_subst_rids (r_subst : T.RegionId.id -> T.RegionId.id) (x : C.env) : + C.env = + (subst_ids_visitor r_subst (fun x -> x) (fun x -> x) (fun x -> x) diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 17cdcabc..0f107897 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -43,10 +43,7 @@ type call = { borrows (we need to perform lookups). *) abstractions : V.AbstractionId.id list; - (* TODO: rename to "...args" *) - type_params : T.ety list; - (* TODO: rename to "...args" *) - const_generic_params : T.const_generic list; + generics : T.egeneric_args; args : V.typed_value list; args_places : mplace option list; (** Meta information *) dest : V.symbolic_value; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 7dda1f22..6c2c049b 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -52,6 +52,9 @@ type fun_context = { type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t } [@@deriving show] +type trait_decls_context = A.trait_decl A.TraitDeclId.Map.t [@@deriving show] +type trait_impls_context = A.trait_impl A.TraitImplId.Map.t [@@deriving show] + (** Whenever we translate a function call or an ended abstraction, we store the related information (this is useful when translating ended children abstractions). @@ -120,6 +123,8 @@ type bs_ctx = { type_context : type_context; fun_context : fun_context; global_context : global_context; + trait_decls_ctx : trait_decls_context; + trait_impls_ctx : trait_impls_context; fun_decl : A.fun_decl; bid : T.RegionGroupId.id option; (** TODO: rename *) sg : fun_sig; @@ -205,7 +210,7 @@ type bs_ctx = { let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter = Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls - ctx.fun_decl + ctx.trait_decls_ctx ctx.trait_impls_ctx ctx.fun_decl let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter = let rvar_to_string = Print.Types.region_var_id_to_string in @@ -223,16 +228,19 @@ let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter = adt_variant_to_string = ast_fmt.adt_variant_to_string; var_id_to_string; adt_field_names = ast_fmt.adt_field_names; + trait_decl_id_to_string = ast_fmt.trait_decl_id_to_string; + trait_impl_id_to_string = ast_fmt.trait_impl_id_to_string; + trait_clause_id_to_string = ast_fmt.trait_clause_id_to_string; } let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter = - let type_params = ctx.fun_decl.signature.type_params in - let cg_params = ctx.fun_decl.signature.const_generic_params in + let generics = ctx.fun_decl.signature.generics in let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls in let global_decls = ctx.global_context.llbc_global_decls in - PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params - cg_params + PrintPure.mk_ast_formatter type_decls fun_decls global_decls + ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types + generics.const_generics let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string = let fmt = bs_ctx_to_ctx_formatter ctx in @@ -254,12 +262,11 @@ let rty_to_string (ctx : bs_ctx) (ty : T.rty) : string = Print.PT.rty_to_string fmt ty let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = - let type_params = def.type_params in - let cg_params = def.const_generic_params in let type_decls = ctx.type_context.llbc_type_decls in let global_decls = ctx.global_context.llbc_global_decls in let fmt = - PrintPure.mk_type_formatter type_decls global_decls type_params cg_params + PrintPure.mk_type_formatter type_decls global_decls ctx.trait_decls_ctx + ctx.trait_impls_ctx def.generics.types def.generics.const_generics in PrintPure.type_decl_to_string fmt def diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 857fea97..cac56487 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -64,7 +64,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) assert (otherwise_see = None); (* Return *) ExpandInt (int_ty, branches, otherwise) - | T.Adt (_, _, _, _) -> + | T.Adt (_, _) -> (* Branching: it is necessarily an enumeration expansion *) let get_variant (see : V.symbolic_expansion option) : T.VariantId.id option * V.symbolic_value list = @@ -85,7 +85,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> raise (Failure "Ill-formed borrow expansion")) - | T.TypeVar _ | T.Literal Char | Never -> + | T.TypeVar _ | T.Literal Char | Never | T.TraitType _ -> raise (Failure "Ill-formed symbolic expansion") in Some (Expansion (place, sv, expansion)) @@ -97,10 +97,10 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value) synthesize_symbolic_expansion sv place [ Some see ] el let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) - (abstractions : V.AbstractionId.id list) (type_params : T.ety list) - (const_generic_params : T.const_generic list) (args : V.typed_value list) - (args_places : mplace option list) (dest : V.symbolic_value) - (dest_place : mplace option) (e : expression option) : expression option = + (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args) + (args : V.typed_value list) (args_places : mplace option list) + (dest : V.symbolic_value) (dest_place : mplace option) + (e : expression option) : expression option = Option.map (fun e -> let call = @@ -108,8 +108,7 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx) call_id; ctx; abstractions; - type_params; - const_generic_params; + generics; args; dest; args_places; @@ -125,26 +124,27 @@ let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) let synthesize_regular_function_call (fun_id : A.fun_id) (call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx) - (abstractions : V.AbstractionId.id list) (type_params : T.ety list) - (const_generic_params : T.const_generic list) (args : V.typed_value list) - (args_places : mplace option list) (dest : V.symbolic_value) - (dest_place : mplace option) (e : expression option) : expression option = + (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args) + (args : V.typed_value list) (args_places : mplace option list) + (dest : V.symbolic_value) (dest_place : mplace option) + (e : expression option) : expression option = synthesize_function_call (Fun (fun_id, call_id)) - ctx abstractions type_params const_generic_params args args_places dest - dest_place e + ctx abstractions generics args args_places dest dest_place e let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : E.unop) (arg : V.typed_value) (arg_place : mplace option) (dest : V.symbolic_value) (dest_place : mplace option) (e : expression option) : expression option = - synthesize_function_call (Unop unop) ctx [] [] [] [ arg ] [ arg_place ] dest - dest_place e + let generics = TypesUtils.mk_empty_generic_args in + synthesize_function_call (Unop unop) ctx [] generics [ arg ] [ arg_place ] + dest dest_place e let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : E.binop) (arg0 : V.typed_value) (arg0_place : mplace option) (arg1 : V.typed_value) (arg1_place : mplace option) (dest : V.symbolic_value) (dest_place : mplace option) (e : expression option) : expression option = - synthesize_function_call (Binop binop) ctx [] [] [] [ arg0; arg1 ] + let generics = TypesUtils.mk_empty_generic_args in + synthesize_function_call (Binop binop) ctx [] generics [ arg0; arg1 ] [ arg0_place; arg1_place ] dest dest_place e let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : V.abs) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 70ef5e3d..ca661108 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -280,9 +280,7 @@ let translate_crate_to_pure (crate : A.crate) : log#ldebug (lazy "translate_crate_to_pure"); (* Compute the type and function contexts *) - let type_context, fun_context, global_context = - compute_type_fun_global_contexts crate - in + let type_context, fun_context, global_context = compute_contexts crate in let fun_infos = FA.analyze_module crate fun_context.C.fun_decls global_context.C.global_decls !Config.use_state diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index 925f6d39..95c7206a 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -14,11 +14,10 @@ type expl_info = subtype_info [@@deriving show] type type_borrows_info = { contains_static : bool; - (** Does the type (transitively) contains a static borrow? *) - contains_borrow : bool; - (** Does the type (transitively) contains a borrow? *) + (** Does the type (transitively) contain a static borrow? *) + contains_borrow : bool; (** Does the type (transitively) contain a borrow? *) contains_nested_borrows : bool; - (** Does the type (transitively) contains nested borrows? *) + (** Does the type (transitively) contain nested borrows? *) contains_borrow_under_mut : bool; } [@@deriving show] @@ -61,7 +60,7 @@ let initialize_g_type_info (param_infos : 'p) : 'p g_type_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 + let param_infos = List.map (fun _ -> param_info) def.generics.types in initialize_g_type_info param_infos let type_decl_info_to_partial_type_info (info : type_decl_info) : @@ -122,7 +121,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref) let rec analyze (expl_info : expl_info) (ty_info : partial_type_info) (ty : 'r ty) : partial_type_info = match ty with - | Literal _ | Never -> ty_info + | Literal _ | Never | TraitType _ -> ty_info | TypeVar var_id -> ( (* Update the information for the proper parameter, if necessary *) match ty_info.param_infos with @@ -171,20 +170,18 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref) analyze expl_info ty_info rty | Adt ( (Tuple | Assumed (Box | Vec | Option | Slice | Array | Str | Range)), - _, - tys, - _ ) -> + generics ) -> (* Nothing to update: just explore the type parameters *) List.fold_left (fun ty_info ty -> analyze expl_info ty_info ty) - ty_info tys - | Adt (AdtId adt_id, regions, tys, _cgs) -> + ty_info generics.types + | Adt (AdtId adt_id, generics) -> (* Lookup the information for this type definition *) 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 *) - let found_static = List.exists r_is_static regions in + let found_static = List.exists r_is_static generics.regions in let borrows_info = ty_info.borrows_info in let borrows_info = { @@ -196,7 +193,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref) let ty_info = { ty_info with borrows_info } in (* For every instantiated type parameter: update the exploration info * then explore the type *) - let params_tys = List.combine adt_info.param_infos tys in + let params_tys = List.combine adt_info.param_infos generics.types in let ty_info = List.fold_left (fun ty_info (param_info, ty) -> diff --git a/compiler/dune b/compiler/dune index 6785cad4..db099c3c 100644 --- a/compiler/dune +++ b/compiler/dune @@ -12,6 +12,7 @@ (pps ppx_deriving.show ppx_deriving.ord visitors.ppx)) (libraries charon core_unix unionFind ocamlgraph) (modules + AssociatedTypes Assumed Collections Config |