diff options
Diffstat (limited to '')
| -rw-r--r-- | TODO.md | 4 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 16 |
2 files changed, 16 insertions, 4 deletions
@@ -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 |