diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Interpreter.ml | 26 | ||||
| -rw-r--r-- | src/Substitute.ml | 2 |
2 files changed, 14 insertions, 14 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 2192c491..f753206c 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -4185,7 +4185,7 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) A.RegionGroupId.Map.find rg_id asubst_map in (* Generate fresh regions and their substitutions *) - let ctx, fresh_regions, rsubst, _ = + let ctx, _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params ctx in (* Generate the type substitution @@ -4204,15 +4204,15 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) in (* Substitute the signature *) let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in - (* Generate a fresh symbolic value for the result *) - let res_sv_ty = inst_sg.A.output in - let ctx, res_spc = - mk_fresh_symbolic_proj_comp T.RegionId.Set.empty res_sv_ty ctx + (* Generate a fresh symbolic value for the return value *) + let ret_sv_ty = inst_sg.A.output in + let ctx, ret_spc = + mk_fresh_symbolic_proj_comp T.RegionId.Set.empty ret_sv_ty ctx in - let res_value = mk_typed_value_from_proj_comp res_spc in - let res_av = V.ASymbolic (V.AProjLoans res_spc.V.svalue) in - let res_av : V.typed_avalue = - { V.value = res_av; V.ty = res_spc.V.svalue.V.sv_ty } + let ret_value = mk_typed_value_from_proj_comp ret_spc in + let ret_av = V.ASymbolic (V.AProjLoans ret_spc.V.svalue) in + let ret_av : V.typed_avalue = + { V.value = ret_av; V.ty = ret_spc.V.svalue.V.sv_ty } in (* Evaluate the input operands *) let ctx, args = eval_operands config ctx args in @@ -4241,7 +4241,7 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) ctx args_with_rtypes in (* Group the input and output values *) - let avalues = List.append args_projs [ res_av ] in + let avalues = List.append args_projs [ ret_av ] in (* Create the abstraction *) let abs = { V.abs_id; parents; regions; avalues } in (* Insert the abstraction in the context *) @@ -4251,10 +4251,10 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) in let ctx = List.fold_left gen_abs ctx inst_sg.A.regions_hierarchy in (* Move the return value to its destination *) - let ctx = assign_to_place config ctx res_value dest in + let ctx = assign_to_place config ctx ret_value dest in (* Synthesis *) S.synthesize_local_function_call fid region_params type_params args dest - res_spc.V.svalue; + ret_spc.V.svalue; (* Return *) ctx @@ -4264,8 +4264,6 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) (fid : A.FunDefId.id) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : C.eval_ctx eval_result list = - (* Retrieve the (correctly instantiated) body *) - let def = C.ctx_lookup_fun_def ctx fid in match config.mode with | ConcreteMode -> eval_local_function_call_concrete config ctx fid region_params type_params diff --git a/src/Substitute.ml b/src/Substitute.ml index dd89025b..d3c3c430 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -39,6 +39,8 @@ let erase_regions (ty : T.rty) : T.ety = Return the list of new regions and appropriate substitutions from the original region variables to the fresh regions. + + TODO: simplify? we only need the subst `T.RegionVarId.id -> T.RegionId.id` *) let fresh_regions_with_substs (region_vars : T.region_var list) (ctx : C.eval_ctx) : |