Make minor modifications

4 files changed, 46 insertions, 6 deletions

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]
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index bdcadf3a..6bb2baf0 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -48,11 +48,20 @@ let expand_primitively_copyable_at_place (config : C.config)
   (* Apply *)
   expand cf ctx
 
-(** Read a place (CPS-style function *)
+(** Read a place (CPS-style function).
+
+    We also check that the value *doesn't contain bottoms or inactivated
+    borrows.
+ *)
 let read_place (config : C.config) (access : access_kind) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
   let v = read_place_unwrap 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));
+  (* Call the continuation *)
   cf v ctx
 
 (** Small utility.
@@ -60,6 +69,14 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
     Prepare the access to a place in a right-value (typically an operand) by
     reorganizing the environment.
 
+    We reorganize the environment so that:
+    - we can access the place (we prepare *along* the path)
+    - the value at the place itself doesn't contain loans (the `access_kind`
+      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*.
+
     [expand_prim_copy]: if true, expand the symbolic values which are primitively
     copyable and contain borrows.
  *)
@@ -67,14 +84,20 @@ let access_rplace_reorganize_and_read (config : C.config)
     (expand_prim_copy : bool) (access : access_kind) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
+  (* Make sure we can evaluate the path *)
   let cc = update_ctx_along_read_place config access p in
+  (* End the proper loans at the place itself *)
   let cc = comp cc (end_loans_at_place config access p) in
+  (* Expand the copyable values which contain borrows (which are necessarily shared
+   * borrows) *)
   let cc =
     if expand_prim_copy then
       comp cc (expand_primitively_copyable_at_place config access p)
     else cc
   in
+  (* Read the place - note that this checks that the value doesn't contain bottoms *)
   let read_place = read_place config access p in
+  (* Compose *)
   comp cc read_place cf ctx
 
 let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool)
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 52742703..edd27138 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -304,7 +304,11 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
         lookup_shared_borrows = false;
       }
 
-(** Read the value at a given place *)
+(** Read the value at a given place.
+
+    Note that we only access the value at the place, and do not check that
+    the value is "well-formed" (for instance that it doesn't contain bottoms).
+ *)
 let read_place (config : C.config) (access : access_kind) (p : E.place)
     (ctx : C.eval_ctx) : V.typed_value path_access_result =
   let access = access_kind_to_projection_access access in
diff --git a/src/Print.ml b/src/Print.ml
index 8e29bc67..af6fc982 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -948,7 +948,7 @@ module LlbcAst = struct
     match st with
     | A.Assign (p, rv) ->
         indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
-    | A.FakeRead p -> "fake_read " ^ place_to_string fmt p
+    | A.FakeRead p -> indent ^ "fake_read " ^ place_to_string fmt p
     | A.SetDiscriminant (p, variant_id) ->
         (* TODO: improve this to lookup the variant name by using the def id *)
         indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", "