summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-05 19:12:56 +0100
committerSon Ho2022-01-05 19:12:56 +0100
commit4feb960fe3b5d58a5420b0c569bcea645a420b9f (patch)
tree971aaf0545bad11e224fe8c21b228d3b3e7bbc1e
parent5c0bf06ba5248f9d428452cd4d0654259e6fe80d (diff)
Implement apply_proj_borrows_on_input_value
-rw-r--r--src/Interpreter.ml27
1 files changed, 19 insertions, 8 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 0adff0dc..f18124f8 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -416,11 +416,6 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
in
{ V.value; V.ty }
-let apply_proj_borrows_in_context (check_symbolic_no_ended : bool)
- (ctx : C.eval_ctx) (regions : T.RegionId.set_t) (v : V.typed_value)
- (ty : T.rty) : C.eval_ctx * V.typed_avalue =
- raise Unimplemented
-
(** Convert a symbolic expansion to a value.
If the expansion is a mutable reference expansion, it converts it to a borrow.
@@ -849,6 +844,24 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool)
in
(fresh_reborrow, apply_registered_reborrows)
+let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx)
+ (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
+ C.eval_ctx * V.typed_avalue =
+ let check_symbolic_no_ended = true in
+ let allow_reborrows = true in
+ (* Prepare the reborrows *)
+ let fresh_reborrow, apply_registered_reborrows =
+ prepare_reborrows config allow_reborrows ctx
+ in
+ (* Apply the projector *)
+ let av =
+ apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions v ty
+ in
+ (* Apply the reborrows *)
+ let ctx = apply_registered_reborrows ctx in
+ (* Return *)
+ (ctx, av)
+
(** Auxiliary function to end borrows. See [give_back].
When we end a mutable borrow, we need to "give back" the value it contained
@@ -4275,12 +4288,10 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
T.RegionId.Set.empty rg.A.regions
in
(* Project over the input values *)
- let check_symbolic_no_ended = true in
let ctx, args_projs =
List.fold_left_map
(fun ctx (arg, arg_rty) ->
- apply_proj_borrows_in_context check_symbolic_no_ended ctx regions arg
- arg_rty)
+ apply_proj_borrows_on_input_value config ctx regions arg arg_rty)
ctx args_with_rtypes
in
(* Group the input and output values *)