diff options
author | Son Ho | 2023-11-13 14:17:55 +0100 |
---|---|---|
committer | Son Ho | 2023-11-13 14:17:55 +0100 |
commit | cb179ba97d2eafac07ac1208ab1e6ab4446f89df (patch) | |
tree | 2f48417732c107ca64074a3ad7a3c3c95d37b598 /compiler/InterpreterStatements.ml | |
parent | 6c88d30031255c0ac612b67bb5b3c20c2f07e563 (diff) |
Make minor modifications
Diffstat (limited to '')
-rw-r--r-- | compiler/InterpreterStatements.ml | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 3627490d..b78c2691 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1114,8 +1114,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) ^ "\n- def.signature:\n" ^ fun_sig_to_string ctx def.A.signature)); let tr_self = T.UnknownTrait __FUNCTION__ in + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular fid) + ctx.fun_context.regions_hierarchies + in let inst_sg = instantiate_fun_sig ctx call.func.generics tr_self def.A.signature + regions_hierarchy in (call.func.func, call.func.generics, def, inst_sg) | FunId (FAssumed _) -> @@ -1154,9 +1159,14 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let method_def = C.ctx_lookup_fun_decl ctx id in (* Instantiate *) let tr_self = T.TraitRef trait_ref in + let fid : A.fun_id = FRegular id in + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find fid + ctx.fun_context.regions_hierarchies + in let inst_sg = instantiate_fun_sig ctx generics tr_self - method_def.A.signature + method_def.A.signature regions_hierarchy in (* Also update the function identifier: we want to forget the fact that we called a trait method, and treat it as @@ -1164,7 +1174,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) which implements the method. In order to do this properly, we also need to update the generics. *) - let func = E.FunId (FRegular id) in + let func = E.FunId fid in (func, generics, method_def, inst_sg) | None -> (* If not found, lookup the methods provided by the trait *declaration* @@ -1210,10 +1220,14 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) ^ "\n- parent params info: " ^ Print.option_to_string A.show_params_info method_def.signature.parent_params_info)); + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular method_id) + ctx.fun_context.regions_hierarchies + in let tr_self = T.TraitRef trait_ref in let inst_sg = instantiate_fun_sig ctx all_generics tr_self - method_def.A.signature + method_def.A.signature regions_hierarchy in (call.func.func, call.func.generics, method_def, inst_sg)) | _ -> @@ -1236,9 +1250,14 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) let method_def = C.ctx_lookup_fun_decl ctx method_id in log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular method_id) + ctx.fun_context.regions_hierarchies + in let tr_self = T.TraitRef trait_ref in let inst_sg = instantiate_fun_sig ctx generics tr_self method_def.A.signature + regions_hierarchy in (call.func.func, call.func.generics, method_def, inst_sg)) in @@ -1437,10 +1456,15 @@ and eval_assumed_function_call_symbolic (config : C.config) (* Should have been treated above *) raise (Failure "Unreachable") | _ -> + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FAssumed fid) + ctx.fun_context.regions_hierarchies + in (* 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_fun_sig fid) + regions_hierarchy in (* Evaluate the function call *) |