From 8c3dc80d255ba2000d35c0bcdf9dbe927215bb81 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Jun 2022 06:51:08 +0200
Subject: Add `can_end` in `abs` and use it for the return abs when generating
 the backward functions

---
 src/InterpreterBorrows.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/InterpreterBorrows.ml')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index f5f3a8fa..26374bf7 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 =
-- 
cgit v1.2.3


From 775b2473976075aa6458a51682f3beeee75dc17a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 29 Jun 2022 08:50:17 +0200
Subject: Make minor modifications

---
 src/InterpreterBorrows.ml | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'src/InterpreterBorrows.ml')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 26374bf7..a13ac786 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1442,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
@@ -1548,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]
-- 
cgit v1.2.3