diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Invariants.ml | 2 | ||||
| -rw-r--r-- | compiler/Values.ml | 26 |
2 files changed, 14 insertions, 14 deletions
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index ff7fa1fc..ead064a4 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -219,7 +219,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = (match (info.loan_kind, kind) with | T.Shared, (Shared | Reserved) | T.Mut, Mut -> () | _ -> raise (Failure "Invariant not satisfied")); - (* An reserved borrow can't point to a value inside an abstraction *) + (* A reserved borrow can't point to a value inside an abstraction *) assert (kind <> Reserved || not info.loan_in_abs); (* Insert the borrow id *) let borrow_ids = info.borrow_ids in diff --git a/compiler/Values.ml b/compiler/Values.ml index 071f5e0f..44b22f9f 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -113,15 +113,15 @@ and borrow_content = | MutBorrow of (BorrowId.id[@opaque]) * typed_value (** A mutably borrowed value. *) | ReservedMutBorrow of mvalue * (BorrowId.id[@opaque]) - (** An reserved mut borrow. + (** A reserved mut borrow. This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}. When evaluating a two-phase mutable borrow, we first introduce a reserved 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 reserved - borrows - though there shouldn't be any other reserved borrows if the program - is well typed) of this value and replace the reserved borrow with a - mutable borrow. + borrows - though there shouldn't be any other reserved borrows) of this value + and replace the reserved borrow with a mutable borrow (as well as the shared + loan with a mutable loan). A simple use case of two-phase borrows: {[ @@ -134,23 +134,23 @@ and borrow_content = 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 + l = Vec::len(move v2); // We need v2 here, and v1 *below* + Vec::push(move v1, move l); // In practice, v1 gets promoted only here ]} The meta-value is used for the same purposes as with shared borrows, - at the exception that in case of reserved borrows it is not + at the exception that in the case of reserved borrows it is not *necessary* for the synthesis: we keep it only as meta-information. To be more precise: - when generating the synthesized program, we may need to convert shared borrows to pure values - we never need to do so for reserved borrows: such borrows must - be activated at the moment we use them (meaning we convert a *mutable* - borrow to a pure value). However, we save meta-data about the assignments, - which is used to make the code cleaner: when generating this meta-data, - we may need to convert reserved borrows to pure values, in which - situation we convert the meta-value we stored in the reserved - borrow. + be promoted at the moment we use them (meaning in the synthesis we + convert a *mutable* borrow to a pure value). However, we save + meta-data about the assignments, which is used to make the code + cleaner: when generating this meta-data, we may need to convert + reserved borrows to pure values, in which situation we convert + the meta-value we stored in the reserved borrow. *) and loan_content = |