summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml20
-rw-r--r--src/Values.ml25
2 files changed, 37 insertions, 8 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 17dd14a4..ee64ec29 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2118,7 +2118,12 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
let ctx = update_loan ek l (V.MutLoan l) ctx in
(* Return *)
(ctx, sv)
- | _, Abstract _ -> raise Unimplemented
+ | _, Abstract _ ->
+ (* I don't think it is possible to have two-phase borrows involving borrows
+ * returned by abstractions. I'm not sure how we could handle that anyway. *)
+ failwith
+ "Can't promote a shared loan to a mutable loan if the loan is inside \
+ an abstraction"
(** Helper function: see [activate_inactivated_mut_borrow].
@@ -2138,7 +2143,11 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id)
| Concrete (V.InactivatedMutBorrow _) ->
(* Update it *)
update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx
- | Abstract _ -> raise Unimplemented
+ | Abstract _ ->
+ (* This can't happen for sure *)
+ failwith
+ "Can't promote a shared borrow to a mutable borrow if the borrow is \
+ inside an abstraction"
(** Promote an inactivated mut borrow to a mut borrow.
@@ -2187,7 +2196,12 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
[promote_shared_loan_to_mut_loan]
*)
promote_inactivated_borrow_to_mut_borrow l borrowed_value ctx)
- | _, Abstract _ -> raise Unimplemented
+ | _, Abstract _ ->
+ (* I don't think it is possible to have two-phase borrows involving borrows
+ * returned by abstractions. I'm not sure how we could handle that anyway. *)
+ failwith
+ "Can't activate an inactivated mutable borrow referencing a loan inside\n\
+ \ an abstraction"
(** Paths *)
diff --git a/src/Values.ml b/src/Values.ml
index f1b2e0a6..b6866621 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -115,13 +115,28 @@ and borrow_content =
| InactivatedMutBorrow of (BorrowId.id[@opaque])
(** An inactivated mut borrow.
- This is used to model two-phase borrows. When evaluating a two-phase
- mutable borrow, we first introduce an inactivated borrow which behaves
- like a shared borrow, until the moment we actually *use* the borrow:
- at this point, we end all the other shared borrows (or inactivated borrows
- - though there shouldn't be any other inactivated borrows if the program
+ This is used to model [two-phase borrows](https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html).
+ When evaluating a two-phase mutable borrow, we first introduce an inactivated
+ borrow which behaves like a shared borrow, until the moment we actually *use*
+ the borrow: at this point, we end all the other shared borrows (or inactivated
+ borrows - though there shouldn't be any other inactivated borrows if the program
is well typed) of this value and replace the inactivated borrow with a
mutable borrow.
+
+ A simple use case of two-phase borrows:
+ ```
+ let mut v = Vec::new();
+ v.push(v.len());
+ ```
+
+ This gets desugared to (something similar to) the following MIR:
+ ```
+ v = Vec::new();
+ v1 = &mut v;
+ v2 = &v; // We need this borrow, but v has already been mutably borrowed!
+ l = Vec::len(move v2);
+ Vec::push(move v1, move l); // In practice, v1 gets activated only here
+ ```
*)
and loan_content =