diff options
Diffstat (limited to 'compiler/InterpreterStatements.ml')
| -rw-r--r-- | compiler/InterpreterStatements.ml | 52 |
1 files changed, 32 insertions, 20 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 0cf8b88a..95a2956b 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -769,12 +769,8 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) ("trait method call:\n- call: " ^ call_to_string ctx call ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" ^ generic_args_to_string ctx func.generics - ^ "\n- trait and method generics:\n" - ^ generic_args_to_string ctx - (Option.get func.trait_and_method_generic_args))); - (* When instantiating, we need to group the generics for the trait ref - and the method *) - let generics = Option.get func.trait_and_method_generic_args in + ^ "\n- trait_ref.trait_decl_ref: " + ^ trait_decl_ref_to_string ctx trait_ref.trait_decl_ref)); (* Lookup the trait method signature - there are several possibilities depending on whethere we call a top-level trait method impl or the method from a local clause *) @@ -794,6 +790,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) | Some (_, id) -> (* This is a required method *) let method_def = ctx_lookup_fun_decl ctx id in + (* We have to concatenate the generics for the impl + and the generics for the method *) + let generics = + merge_generic_args trait_ref.generics func.generics + in (* Instantiate *) let tr_self = TraitRef trait_ref in let fid : fun_id = FRegular id in @@ -898,6 +899,12 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) + (* When instantiating, we need to group the generics for the + trait ref and the generics for the method *) + let generics = + TypesUtils.merge_generic_args + trait_ref.trait_decl_ref.decl_generics func.generics + in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies @@ -942,9 +949,9 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = | Assign (p, rvalue) -> ( (* We handle global assignments separately *) match rvalue with - | Global gid -> + | Global (gid, generics) -> (* Evaluate the global *) - eval_global config p gid cf ctx + eval_global config p gid generics cf ctx | _ -> (* Evaluate the rvalue *) let cf_eval_rvalue = eval_rvalue_not_global config rvalue in @@ -1014,32 +1021,37 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = (* Compose and apply *) comp cc cf_eval_st cf ctx -and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) : - st_cm_fun = +and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) + (generics : generic_args) : st_cm_fun = fun cf ctx -> let global = ctx_lookup_global_decl ctx gid in match config.mode with | ConcreteMode -> - (* Treat the evaluation of the global as a call to the global body (without arguments) *) - let func = - { - func = FunId (FRegular global.body); - generics = TypesUtils.empty_generic_args; - trait_and_method_generic_args = None; - } - in + (* Treat the evaluation of the global as a call to the global body *) + let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in (eval_transparent_function_call_concrete config global.body call) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) assert (ty_no_regions global.ty); - let sval = mk_fresh_symbolic_value global.ty in + (* Instantiate the type *) + (* There shouldn't be any reference to Self *) + let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in + let generics = Subst.generic_args_erase_regions generics in + let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = + Subst.make_subst_from_generics global.generics generics tr_self + in + let ty = + Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self + global.ty + in + let sval = mk_fresh_symbolic_value ty in let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) dest in let e = cc (cf Unit) ctx in - S.synthesize_global_eval gid sval e + S.synthesize_global_eval gid generics sval e (** Evaluate a switch *) and eval_switch (config : config) (switch : switch) : st_cm_fun = |