diff options
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 53 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 12 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 12 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 14 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 19 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 14 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 2 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 16 | ||||
| -rw-r--r-- | compiler/Print.ml | 4 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 6 | ||||
| -rw-r--r-- | compiler/Values.ml | 22 | ||||
| -rw-r--r-- | compiler/ValuesUtils.ml | 6 |
12 files changed, 91 insertions, 89 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 1b4907ac..585db0eb 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -93,7 +93,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) method! visit_Borrow outer bc = match bc with - | SharedBorrow (_, l') | InactivatedMutBorrow (_, l') -> + | SharedBorrow (_, l') | ReservedMutBorrow (_, l') -> (* Check if this is the borrow we are looking for *) if l = l' then ( (* Check if there are outer borrows or if we are inside an abstraction *) @@ -731,7 +731,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) give_back_value config l tv ctx - | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow (_, l')) -> + | Concrete (V.SharedBorrow (_, l') | V.ReservedMutBorrow (_, l')) -> (* Sanity check *) assert (l' = l); (* Check that the borrow is somewhere - purely a sanity check *) @@ -1120,7 +1120,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) match bc with | V.SharedBorrow (_, _) | V.MutBorrow (_, _) -> raise (FoundBorrowContent bc) - | V.InactivatedMutBorrow _ -> raise (Failure "Unreachable") + | V.ReservedMutBorrow _ -> raise (Failure "Unreachable") end in (* Lookup the abstraction *) @@ -1224,7 +1224,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (* Give the value back - note that the mut borrow was below a * shared borrow: the value is thus unchanged *) give_back_value config bid v ctx) - | V.InactivatedMutBorrow _ -> raise (Failure "Unreachable") + | V.ReservedMutBorrow _ -> raise (Failure "Unreachable") in (* Reexplore *) end_abstraction_borrows config chain abs_id cf ctx @@ -1403,7 +1403,7 @@ let end_borrows config : V.BorrowId.Set.t -> cm_fun = let end_abstraction config = end_abstraction_aux config [] let end_abstractions config = end_abstractions_aux config [] -(** Helper function: see {!activate_inactivated_mut_borrow}. +(** Helper function: see {!activate_reserved_mut_borrow}. This function updates the shared loan to a mutable loan (we then update the borrow with another helper). Of course, the shared loan must contain @@ -1413,7 +1413,7 @@ let end_abstractions config = end_abstractions_aux config [] The returned value (previously shared) is checked: - it mustn't contain loans - it mustn't contain {!V.Bottom} - - it mustn't contain inactivated borrows + - it mustn't contain reserved borrows TODO: this kind of checks should be put in an auxiliary helper, because they are redundant. @@ -1446,8 +1446,8 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) assert (not (loans_in_value sv)); (* Check there isn't {!Bottom} (this is actually an invariant *) assert (not (bottom_in_value ctx.ended_regions sv)); - (* Check there aren't inactivated borrows *) - assert (not (inactivated_in_value sv)); + (* Check there aren't reserved borrows *) + assert (not (reserved_in_value sv)); (* Update the loan content *) let ctx = update_loan ek l (V.MutLoan l) ctx in (* Continue *) @@ -1460,15 +1460,16 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) "Can't promote a shared loan to a mutable loan if the loan is \ inside an abstraction") -(** Helper function: see {!activate_inactivated_mut_borrow}. +(** Helper function: see {!activate_reserved_mut_borrow}. - This function updates a shared borrow to a mutable borrow. + This function updates a shared borrow to a mutable borrow (and that is + all: it doesn't touch the corresponding loan). *) -let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) (cf : m_fun) +let replace_reserved_borrow_with_mut_borrow (l : V.BorrowId.id) (cf : m_fun) (borrowed_value : V.typed_value) : m_fun = fun ctx -> - (* Lookup the inactivated borrow - note that we don't go inside borrows/loans: - there can't be inactivated borrows inside other borrows/loans + (* Lookup the reserved borrow - note that we don't go inside borrows/loans: + there can't be reserved borrows inside other borrows/loans *) let ek = { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } @@ -1476,8 +1477,8 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) (cf : m_fun) let ctx = match lookup_borrow ek l ctx with | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) -> - raise (Failure "Expected an inactivated mutable borrow") - | Concrete (V.InactivatedMutBorrow _) -> + raise (Failure "Expected a reserved mutable borrow") + | Concrete (V.ReservedMutBorrow _) -> (* Update it *) update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx | Abstract _ -> @@ -1490,12 +1491,9 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) (cf : m_fun) (* Continue *) cf ctx -(** Promote an inactivated mut borrow to a mut borrow. - - The borrow must point to a shared value which is borrowed exactly once. - *) -let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) - : cm_fun = +(** Promote a reserved mut borrow to a mut borrow. *) +let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) : + cm_fun = fun cf ctx -> (* Lookup the value *) let ek = @@ -1505,7 +1503,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) | _, Concrete (V.MutLoan _) -> raise (Failure "Unreachable") | _, Concrete (V.SharedLoan (bids, sv)) -> ( (* If there are loans inside the value, end them. Note that there can't be - inactivated borrows inside the value. + reserved borrows inside the value. If we perform an update, do a recursive call to lookup the updated value *) match get_first_loan_in_value sv with | Some lc -> @@ -1516,7 +1514,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) | V.MutLoan bid -> end_borrow config bid in (* Recursive call *) - let cc = comp cc (activate_inactivated_mut_borrow config l) in + let cc = comp cc (promote_reserved_mut_borrow config l) in (* Continue *) cc cf ctx | None -> @@ -1524,11 +1522,11 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) (* Some sanity checks *) log#ldebug (lazy - ("activate_inactivated_mut_borrow: resulting value:\n" + ("activate_reserved_mut_borrow: resulting value:\n" ^ typed_value_to_string ctx sv)); assert (not (loans_in_value sv)); assert (not (bottom_in_value ctx.ended_regions sv)); - assert (not (inactivated_in_value sv)); + assert (not (reserved_in_value sv)); (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) let bids = V.BorrowId.Set.remove l bids in @@ -1543,7 +1541,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) *) let cc = comp cc (fun cf borrowed_value -> - promote_inactivated_borrow_to_mut_borrow l cf borrowed_value) + replace_reserved_borrow_with_mut_borrow l cf borrowed_value) in (* Continue *) cc cf ctx) @@ -1552,6 +1550,5 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) * returned by abstractions. I'm not sure how we could handle that anyway. *) raise (Failure - "Can't activate an inactivated mutable borrow referencing a loan \ - inside\n\ + "Can't activate a reserved mutable borrow referencing a loan inside\n\ \ an abstraction") diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index 0733a15b..f21fdcd5 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -30,5 +30,13 @@ val end_abstraction : C.config -> V.AbstractionId.id -> cm_fun (** End a set of abstractions while preserving the invariants. *) val end_abstractions : C.config -> V.AbstractionId.Set.t -> cm_fun -(** Activate a reserved borrow into a mutable borrow, while preserving the invariants. *) -val activate_inactivated_mut_borrow : C.config -> V.BorrowId.id -> cm_fun +(** Promote a reserved mut borrow to a mut borrow, while preserving the invariants. + + Reserved borrows are special mutable borrows which are created as shared borrows + then promoted to mutable borrows upon their first use. + + This function replaces the reserved borrow with a mutable borrow, then replaces + the corresponding shared loan with a mutable loan (after having ended the + other shared borrows which point to this loan). + *) +val promote_reserved_mut_borrow : C.config -> V.BorrowId.id -> cm_fun diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 7cd447c3..d3be1bed 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -204,9 +204,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) | V.SharedBorrow (mv, bid) -> (* Nothing specific to do *) super#visit_SharedBorrow env mv bid - | V.InactivatedMutBorrow (mv, bid) -> + | V.ReservedMutBorrow (mv, bid) -> (* Nothing specific to do *) - super#visit_InactivatedMutBorrow env mv bid + super#visit_ReservedMutBorrow env mv bid | V.MutBorrow (bid, mv) -> (* Control the dive *) if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv @@ -314,7 +314,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) method! visit_borrow_content env bc = match bc with - | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ -> + | V.SharedBorrow (_, _) | V.ReservedMutBorrow _ -> (* Nothing specific to do *) super#visit_borrow_content env bc | V.MutBorrow (bid, mv) -> @@ -419,7 +419,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) | V.SharedBorrow (_, bid) -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () - | V.InactivatedMutBorrow (_, bid) -> + | V.ReservedMutBorrow (_, bid) -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () @@ -503,10 +503,10 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) | V.SharedBorrow (mv, bid) -> (* Check the id *) if bid = l then update () else super#visit_SharedBorrow env mv bid - | V.InactivatedMutBorrow (mv, bid) -> + | V.ReservedMutBorrow (mv, bid) -> (* Check the id *) if bid = l then update () - else super#visit_InactivatedMutBorrow env mv bid + else super#visit_ReservedMutBorrow env mv bid method! visit_loan_content env lc = match lc with diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index a7c17a45..ea0e1aa9 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -52,7 +52,7 @@ let expand_primitively_copyable_at_place (config : C.config) (** Read a place (CPS-style function). - We also check that the value *doesn't contain bottoms or inactivated + We also check that the value *doesn't contain bottoms or reserved borrows*. *) let read_place (config : C.config) (access : access_kind) (p : E.place) @@ -61,8 +61,8 @@ let read_place (config : C.config) (access : access_kind) (p : E.place) let v = read_place config access p ctx in (* Check that there are no bottoms in the value *) assert (not (bottom_in_value ctx.ended_regions v)); - (* Check that there are no inactivated borrows in the value *) - assert (not (inactivated_in_value v)); + (* Check that there are no reserved borrows in the value *) + assert (not (reserved_in_value v)); (* Call the continuation *) cf v ctx @@ -77,7 +77,7 @@ let read_place (config : C.config) (access : access_kind) (p : E.place) controls whether we only end mutable loans, or also shared loans). We also check, after the reorganization, that the value at the place - *doesn't contain any bottom nor inactivated borrows*. + *doesn't contain any bottom nor reserved borrows*. [expand_prim_copy]: if [true], expand the symbolic values which are primitively copyable and contain borrows. @@ -180,8 +180,8 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) }) | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow") - | V.InactivatedMutBorrow _ -> - raise (Failure "Can't copy an inactivated mut borrow")) + | V.ReservedMutBorrow _ -> + raise (Failure "Can't copy a reserved mut borrow")) | V.Loan lc -> ( (* We can only copy shared loans *) match lc with @@ -673,7 +673,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) in let bc = if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid) - else V.InactivatedMutBorrow (shared_mvalue, bid) + else V.ReservedMutBorrow (shared_mvalue, bid) in let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in (* Continue *) diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 73b446da..3d0c69e8 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -28,8 +28,8 @@ type path_fail_kind = (** Failure because we couldn't go inside a shared loan *) | FailMutLoan of V.BorrowId.id (** Failure because we couldn't go inside a mutable loan *) - | FailInactivatedMutBorrow of V.BorrowId.id - (** Failure because we couldn't go inside an inactivated mutable borrow + | FailReservedMutBorrow of V.BorrowId.id + (** Failure because we couldn't go inside a reserved mutable borrow (which should get activated) *) | FailSymbolic of int * V.symbolic_value (** Failure because we need to enter a symbolic value (and thus need to @@ -216,8 +216,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) (* Return - note that we don't need to update the borrow itself *) Ok (ctx, { res with updated = v })) else Error (FailBorrow bc) - | V.InactivatedMutBorrow (_, bid) -> - Error (FailInactivatedMutBorrow bid) + | V.ReservedMutBorrow (_, bid) -> Error (FailReservedMutBorrow bid) | V.MutBorrow (bid, bv) -> if access.enter_mut_borrows then match access_projection access ctx update p' bv with @@ -480,8 +479,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind) match err with | FailSharedLoan bids -> end_borrows config bids | FailMutLoan bid -> end_borrow config bid - | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config bid + | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config bid | FailSymbolic (i, sp) -> (* Expand the symbolic value *) let proj, _ = @@ -511,8 +509,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind) match err with | FailSharedLoan bids -> end_borrows config bids | FailMutLoan bid -> end_borrow config bid - | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config bid + | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config bid | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) expand_symbolic_value_no_branching config sp @@ -549,9 +546,9 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) match bc with | V.SharedBorrow _ | V.MutBorrow (_, _) -> (* Nothing special to do *) super#visit_borrow_content env bc - | V.InactivatedMutBorrow (_, bid) -> - (* We need to activate inactivated borrows *) - let cc = activate_inactivated_mut_borrow config bid in + | V.ReservedMutBorrow (_, bid) -> + (* We need to activate reserved borrows *) + let cc = promote_reserved_mut_borrow config bid in raise (UpdateCtx cc) method! visit_loan_content env lc = diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 67bbe21f..d656e158 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -66,10 +66,10 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) | _ -> raise (Failure "Unexpected") in (bid, asb) - | V.InactivatedMutBorrow _, _ -> + | V.ReservedMutBorrow _, _ -> raise (Failure - "Can't apply a proj_borrow over an inactivated mutable \ + "Can't apply a proj_borrow over a reserved mutable \ borrow") | _ -> raise (Failure "Unreachable") in @@ -141,10 +141,10 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) in V.AMutBorrow (mv, bid, bv) | V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid - | V.InactivatedMutBorrow _, _ -> + | V.ReservedMutBorrow _, _ -> raise (Failure - "Can't apply a proj_borrow over an inactivated mutable \ + "Can't apply a proj_borrow over a reserved mutable \ borrow") | _ -> raise (Failure "Unreachable") in @@ -179,10 +179,10 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) | _ -> raise (Failure "Unexpected") in V.AProjSharedBorrow asb - | V.InactivatedMutBorrow _, _ -> + | V.ReservedMutBorrow _, _ -> raise (Failure - "Can't apply a proj_borrow over an inactivated mutable \ + "Can't apply a proj_borrow over a reserved mutable \ borrow") | _ -> raise (Failure "Unreachable") in @@ -333,7 +333,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) match v.V.value with | V.Borrow lc -> ( match lc with - | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ -> None + | V.SharedBorrow (_, _) | V.ReservedMutBorrow _ -> None | V.MutBorrow (id, _) -> Some id) | _ -> None in diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 66196349..08a03885 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -809,7 +809,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Update the synthesized AST - here we store meta-information. * We do it only in specific cases (it is not always useful, and * also it can lead to issues - for instance, if we borrow an - * inactivated borrow, we later can't translate it to pure values...) *) + * reserved borrow, we later can't translate it to pure values...) *) match rvalue with | E.Global _ -> raise (Failure "Unreachable") | E.Use _ diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 18a1c835..ff7fa1fc 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -46,7 +46,7 @@ let borrows_infos_to_string (indent : string) (infos : borrow_info V.BorrowId.Map.t) : string = V.BorrowId.Map.to_string (Some indent) show_borrow_info infos -type borrow_kind = Mut | Shared | Inactivated +type borrow_kind = Mut | Shared | Reserved (** Check that: - loans and borrows are correctly related @@ -217,10 +217,10 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = let info = find_info bid in (* Check that the borrow kind is consistent *) (match (info.loan_kind, kind) with - | T.Shared, (Shared | Inactivated) | T.Mut, Mut -> () + | T.Shared, (Shared | Reserved) | T.Mut, Mut -> () | _ -> raise (Failure "Invariant not satisfied")); - (* An inactivated borrow can't point to a value inside an abstraction *) - assert (kind <> Inactivated || not info.loan_in_abs); + (* An 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 assert (not (V.BorrowId.Set.mem bid borrow_ids)); @@ -247,7 +247,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match bc with | V.SharedBorrow (_, bid) -> register_borrow Shared bid | V.MutBorrow (bid, _) -> register_borrow Mut bid - | V.InactivatedMutBorrow (_, bid) -> register_borrow Inactivated bid + | V.ReservedMutBorrow (_, bid) -> register_borrow Reserved bid in (* Continue exploring *) super#visit_borrow_content env bc @@ -298,7 +298,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = !borrows_infos (** Check that: - - borrows/loans can't contain ⊥ or inactivated mut borrows + - borrows/loans can't contain ⊥ or reserved mut borrows - shared loans can't contain mutable loans *) let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) : @@ -333,7 +333,7 @@ let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) : let info = match bc with | V.SharedBorrow _ -> set_outer_shared info - | V.InactivatedMutBorrow _ -> + | V.ReservedMutBorrow _ -> assert (not info.outer_borrow); set_outer_shared info | V.MutBorrow (_, _) -> set_outer_mut info @@ -463,7 +463,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> ( match (bc, rkind) with | V.SharedBorrow (_, bid), T.Shared - | V.InactivatedMutBorrow (_, bid), T.Mut -> ( + | V.ReservedMutBorrow (_, bid), T.Mut -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan ek_all bid ctx in match glc with diff --git a/compiler/Print.ml b/compiler/Print.ml index 53bba8c7..2b2f98f0 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -127,8 +127,8 @@ module Values = struct "&mut@" ^ V.BorrowId.to_string bid ^ " (" ^ typed_value_to_string fmt tv ^ ")" - | InactivatedMutBorrow (_, bid) -> - "⌊inactivated_mut@" ^ V.BorrowId.to_string bid ^ "⌋" + | ReservedMutBorrow (_, bid) -> + "⌊reserved_mut@" ^ V.BorrowId.to_string bid ^ "⌋" and loan_content_to_string (fmt : value_formatter) (lc : V.loan_content) : string = diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 54f14d30..3636d4b8 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -772,10 +772,10 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) : (* The meta-value stored in the shared borrow was added especially * for this case (because we can't use the borrow id for lookups) *) translate mv - | V.InactivatedMutBorrow (mv, _) -> - (* Same as for shared borrows. However, note that we use inactivated borrows + | V.ReservedMutBorrow (mv, _) -> + (* Same as for shared borrows. However, note that we use reserved borrows * only in meta-data: a value actually *used in the translation* can't come - * from an unpromoted inactivated borrow *) + * from an unpromoted reserved borrow *) translate mv | V.MutBorrow (_, v) -> (* Borrows are the identity in the extraction *) diff --git a/compiler/Values.ml b/compiler/Values.ml index 6245608d..071f5e0f 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -112,15 +112,15 @@ and borrow_content = *) | MutBorrow of (BorrowId.id[@opaque]) * typed_value (** A mutably borrowed value. *) - | InactivatedMutBorrow of mvalue * (BorrowId.id[@opaque]) - (** An inactivated mut borrow. + | ReservedMutBorrow of mvalue * (BorrowId.id[@opaque]) + (** An 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 an inactivated + 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 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 + 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. A simple use case of two-phase borrows: @@ -139,24 +139,24 @@ and borrow_content = ]} The meta-value is used for the same purposes as with shared borrows, - at the exception that in case of inactivated borrows it is not + at the exception that in 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 inactivated borrows: such borrows must + - 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 inactivated borrows to pure values, in which - situation we convert the meta-value we stored in the inactivated + 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 = | SharedLoan of (BorrowId.Set.t[@opaque]) * typed_value | MutLoan of (BorrowId.id[@opaque]) - (** TODO: we might want to add a set of borrow ids (useful for inactivated + (** TODO: we might want to add a set of borrow ids (useful for reserved borrows, and extremely useful when giving shared values to abstractions). *) diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml index 0e1714a8..524f86a4 100644 --- a/compiler/ValuesUtils.ml +++ b/compiler/ValuesUtils.ml @@ -46,12 +46,12 @@ let borrows_in_value (v : typed_value) : bool = false with Found -> true -(** Check if a value contains inactivated mutable borrows *) -let inactivated_in_value (v : typed_value) : bool = +(** Check if a value contains reserved mutable borrows *) +let reserved_in_value (v : typed_value) : bool = let obj = object inherit [_] iter_typed_value - method! visit_InactivatedMutBorrow _env _ = raise Found + method! visit_ReservedMutBorrow _env _ = raise Found end in (* We use exceptions *) |