From 1e39985a44646f1c352def6e4b29365a113a5dee Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 1 Sep 2023 14:43:11 +0200 Subject: Compute the normalized trait types maps and update Interpreter --- compiler/Interpreter.ml | 88 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 58 insertions(+), 30 deletions(-) (limited to 'compiler/Interpreter.ml') diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index eb66013d..b5e9fcb9 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -32,10 +32,12 @@ let compute_contexts (m : A.crate) : C.decls_ctx = let trait_impls_ctx = { C.trait_impls } in { C.type_ctx; fun_ctx; global_ctx; trait_decls_ctx; trait_impls_ctx } +(** **WARNING**: this function doesn't compute the normalized types + (for the trait type aliases). This should be computed afterwards. + *) 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) - (trait_clauses : T.etrait_ref list) : C.eval_ctx = + (const_generic_vars : T.const_generic_var list) : C.eval_ctx = C.reset_global_counters (); let const_generic_vars_map = T.ConstGenericVarId.Map.of_list @@ -56,11 +58,53 @@ let initialize_eval_context (ctx : C.decls_ctx) C.type_vars; C.const_generic_vars; C.const_generic_vars_map; - C.trait_clauses; + C.norm_trait_etypes = C.ETraitTypeRefMap.empty (* Empty for now *); + C.norm_trait_rtypes = C.RTraitTypeRefMap.empty (* Empty for now *); C.env = [ C.Frame ]; C.ended_regions = T.RegionId.Set.empty; } +(** Instantiate a function signature for a symbolic execution *) +let symbolic_instantiate_fun_sig (ctx : C.eval_ctx) (fdef : A.fun_decl) : + A.inst_fun_sig = + let sg = fdef.signature in + let tr_self = + match fdef.kind with + | RegularKind | TraitMethodImpl _ -> T.UnknownTrait __FUNCTION__ + | TraitMethodDecl _ | TraitMethodProvided _ -> + raise (Failure "Unimplemented") + in + let generics = + let { T.regions; types; const_generics; trait_clauses } = sg.generics in + let regions = List.map (fun _ -> T.Erased) regions in + let types = List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) types in + let const_generics = + List.map + (fun (v : T.const_generic_var) -> T.ConstGenericVar v.T.index) + const_generics + in + (* Annoying that we have to generate this substitution here *) + let r_subst _ = raise (Failure "Unexpected region") in + let ty_subst = Subst.make_type_subst_from_vars sg.generics.types types in + let cg_subst = + Subst.make_const_generic_subst_from_vars sg.generics.const_generics + const_generics + in + let tr_subst _ = raise (Failure "Unexpected local trait clause") in + let subst = { Subst.r_subst; ty_subst; cg_subst; tr_subst; tr_self } in + let trait_refs = + List.map + (fun (c : T.trait_clause) -> + let { T.trait_id = trait_decl_id; generics; _ } = c in + let generics = Subst.generic_args_substitute subst generics in + let trait_decl_ref = { T.trait_decl_id; decl_generics = generics } in + { T.trait_id = T.Clause c.clause_id; generics; trait_decl_ref }) + trait_clauses + in + { T.regions; types; const_generics; trait_refs } + in + instantiate_fun_sig ctx generics tr_self sg + (** Initialize an evaluation context to execute a function. Introduces local variables initialized in the following manner: @@ -94,18 +138,15 @@ let initialize_symbolic_context_for_fun (ctx : C.decls_ctx) (fdef : A.fun_decl) in let ctx = initialize_eval_context ctx region_groups sg.generics.types - sg.generics.const_generics sg.generics.trait_clauses + sg.generics.const_generics in (* Instantiate the signature *) - let type_params = - List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) sg.type_params - in - let cg_params = - List.map - (fun (v : T.const_generic_var) -> T.ConstGenericVar v.T.index) - sg.const_generic_params + let inst_sg = symbolic_instantiate_fun_sig ctx fdef in + (* Compute the normalization maps *) + let ctx = + AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx + inst_sg.trait_type_constraints in - let inst_sg = instantiate_fun_sig type_params cg_params sg in (* Create fresh symbolic values for the inputs *) let input_svs = List.map (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) inst_sg.inputs @@ -180,15 +221,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return * an instantiation of the signature, so that we use fresh * region ids for the return abstractions. *) let sg = fdef.signature in - let type_params = - List.map (fun (v : T.type_var) -> T.TypeVar v.T.index) sg.type_params - in - let cg_params = - List.map - (fun (v : T.const_generic_var) -> T.ConstGenericVar v.T.index) - sg.const_generic_params - in - let ret_inst_sg = instantiate_fun_sig type_params cg_params sg in + let ret_inst_sg = symbolic_instantiate_fun_sig ctx fdef in let ret_rty = ret_inst_sg.output in (* Move the return value out of the return variable *) let pop_return_value = is_regular_return in @@ -362,19 +395,14 @@ let evaluate_function_symbolic_synthesize_backward_from_return for the synthesis) - the symbolic AST generated by the symbolic execution *) -let evaluate_function_symbolic (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) - (global_context : C.global_context) (fdef : A.fun_decl) : - V.symbolic_value list * SA.expression option = +let evaluate_function_symbolic (synthesize : bool) (ctx : C.decls_ctx) + (fdef : A.fun_decl) : V.symbolic_value list * SA.expression option = (* Debug *) let name_to_string () = Print.fun_name_to_string fdef.A.name in log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ())); (* Create the evaluation context *) - let ctx, input_svs, inst_sg = - initialize_symbolic_context_for_fun type_context fun_context global_context - fdef - in + let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in (* Create the continuation to finish the evaluation *) let config = C.mk_config C.SymbolicMode in @@ -518,7 +546,7 @@ module Test = struct (* Create the evaluation context *) let decls_ctx = compute_contexts crate in - let ctx = initialize_eval_context decls_ctx [] [] [] [] 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 -- cgit v1.2.3