summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/InterpreterBorrows.ml15
-rw-r--r--src/InterpreterUtils.ml5
-rw-r--r--src/Values.ml4
3 files changed, 16 insertions, 8 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 442fe620..ccd41747 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -429,7 +429,7 @@ let give_back_symbolic_value (_config : C.config)
(* Sanity checks *)
assert (sv.sv_id <> nsv.sv_id);
(match nsv.sv_kind with
- | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
+ | V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
| V.FunCallRet | V.SynthInput -> failwith "Unrechable");
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = mk_typed_value_from_symbolic_value nsv in
@@ -758,8 +758,15 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
be expanded (because expanding this symbolic value would require expanding
a reference whose region has already ended).
*)
-let convert_avalue_to_given_back_value (av : V.typed_avalue) : V.typed_value =
- mk_fresh_symbolic_typed_value V.FunCallGivenBack av.V.ty
+let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
+ (av : V.typed_avalue) : V.typed_value =
+ let sv_kind =
+ match abs_kind with
+ | V.FunCall -> V.FunCallGivenBack
+ | V.SynthRet -> V.SynthRetGivenBack
+ | V.SynthInput -> V.SynthInputGivenBack
+ in
+ mk_fresh_symbolic_typed_value sv_kind av.V.ty
(** End a borrow identified by its borrow id in a context.
@@ -1155,7 +1162,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
match bc with
| V.AMutBorrow (_, bid, av) ->
(* First, convert the avalue to a (fresh symbolic) value *)
- let v = convert_avalue_to_given_back_value av in
+ let v = convert_avalue_to_given_back_value abs.kind av in
(* Replace the mut borrow to register the fact that we ended
* it and store with it the freshly generated given back value *)
let ended_borrow = V.ABorrow (V.AEndedMutBorrow (v, av)) in
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 157ac68d..20657945 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -237,8 +237,9 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
raise Found
else ()
- | V.SynthInput -> ()
- | V.FunCallGivenBack | V.SynthRetGivenBack -> failwith "Unreachable"
+ | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
+ | V.SynthRetGivenBack ->
+ ()
end
in
(* We use exceptions *)
diff --git a/src/Values.ml b/src/Values.ml
index 6378269f..95b1bd13 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -66,9 +66,9 @@ type sv_kind =
synthesizing returned, and which was given back because we ended
one of the lifetimes of this function (we do this to synthesize
the backward functions).
-
- TODO: add a SynthInputGivenBack
*)
+ | SynthInputGivenBack
+ (** The value was given back upon ending one of the input abstractions *)
[@@deriving show]
type symbolic_value = {