diff options
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterBorrows.ml | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index f5f3a8fa..a13ac786 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -985,6 +985,9 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) (* Lookup the abstraction *) let abs = C.ctx_lookup_abs ctx abs_id in + (* Check that we can end the abstraction *) + assert abs.can_end; + (* End the parent abstractions first *) let cc = end_abstractions config chain abs.parents in let cc = @@ -1439,12 +1442,22 @@ let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun = - it mustn't contain [Bottom] - it mustn't contain inactivated borrows TODO: this kind of checks should be put in an auxiliary helper, because - they are redundant + they are redundant. + + The loan to update mustn't be a borrowed value. *) let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> - (* Lookup the shared loan *) + (* Debug *) + log#ldebug + (lazy + ("promote_shared_loan_to_mut_loan:\n- loan: " ^ V.BorrowId.to_string l + ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n")); + (* Lookup the shared loan - note that we can't promote a shared loan + * in a shared value, but we can do it in a mutably borrowed value. + * This is important because we can do: `let y = &two-phase ( *x );` + *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in @@ -1545,7 +1558,10 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) the borrow we want to promote *) let bids = V.BorrowId.Set.remove l bids in let cc = end_outer_borrows config bids in - (* Promote the loan *) + (* Promote the loan - TODO: this will fail if the value contains + * any loans. In practice, it shouldn't, but we could also + * look for loans inside the value and end them before promoting + * the borrow. *) let cc = comp cc (promote_shared_loan_to_mut_loan l) in (* Promote the borrow - the value should have been checked by [promote_shared_loan_to_mut_loan] |