diff options
| -rw-r--r-- | src/Interpreter.ml | 20 | ||||
| -rw-r--r-- | src/Values.ml | 25 |
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 = |