summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-27 00:32:31 +0100
committerSon Ho2022-01-27 00:32:31 +0100
commit4e140fb31464173c7692668419f5938e34177015 (patch)
tree8f151907821f7f8e9f84695cdd04ec0c8a9f248e
parent1e3e6f6ecdbc277322f3631dac683fe938134d0c (diff)
Make give_back_symbolic_value fail in case we need to reinsert inside an
AProjLoans: there is something wrong
-rw-r--r--TODO.md4
-rw-r--r--src/InterpreterBorrows.ml16
2 files changed, 16 insertions, 4 deletions
diff --git a/TODO.md b/TODO.md
index b9ae7934..8edb8fe6 100644
--- a/TODO.md
+++ b/TODO.md
@@ -61,8 +61,8 @@
abstractions) is wrong.
We get things like :
`AProjLoans (s0 <: &'a mut T) [AProjBorrows (s1 <: &'a mut T)]`
- while in the case of `s1` we should ignore the outer borrow (we
- gave back something because this borrow ended...).
+ while in the case of `s1` we should ignore the outer borrow (what we give
+ back actually has type `T`...)
* write a function to check that the code we are about to synthesize is in the proper
subset. In particular:
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 24521335..ad7b5b2c 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -437,6 +437,8 @@ let give_back_symbolic_value (_config : C.config)
let mv = nsv in
(* Substitution function, to replace the borrow projectors over symbolic values *)
let subst (_abs : V.abs) local_given_back =
+ (* See the below comments: there is something wrong here *)
+ let _ = raise Errors.Unimplemented in
(* Compute the projection over the given back value *)
let child_proj =
match nsv.sv_kind with
@@ -450,11 +452,21 @@ let give_back_symbolic_value (_config : C.config)
* (and MUST) forget the borrows *)
V.AIgnoredProjBorrows
| V.FunCallGivenBack ->
- (* The value was fed as input to a function, and was given back *)
+ (* TODO: there is something wrong here.
+ * Consider this:
+ * ```
+ * abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
+ * abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
+ * ```
+ *
+ * Upon ending abs1, we give back some fresh symbolic value `s1`,
+ * that we reinsert where the loan for `s0` is. However, the mutable
+ * borrow in the type `&'a mut T` was ended: we give back a value of
+ * type `T`! We thus *mustn't* introduce a projector here.
+ *)
V.AProjBorrows (nsv, sv.V.sv_ty)
| _ -> failwith "Unreachable"
in
- (* TODO: this actually doesn't work, or at least there is something subtle... *)
V.AProjLoans (sv, (mv, child_proj) :: local_given_back)
in
update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx