Remove the argument [end_borrows] from prepare_lplace and drop_outer_loans_at_lplace

3 files changed, 24 insertions, 52 deletions

diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 89c22f18..6f9b2ffe 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -610,8 +610,8 @@ let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option =
     the outer ones).
     
     [with_borrows]:
-    - if true: return the first loan or borrow we find
-    - if false: return the first loan we find, do not dive into borrowed values
+    - if [true]: return the first loan or borrow we find
+    - if [false]: return the first loan we find, do not dive into borrowed values
  *)
 let get_first_outer_loan_or_borrow_in_value (with_borrows : bool)
     (v : V.typed_value) : loan_or_borrow_content option =
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 4dea4c91..5fcc25eb 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -615,30 +615,20 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
          * a recursive call to reinspect the value *)
         comp cc (end_loans_at_place config access p) cf ctx)
 
-(** Drop (end) outer loans and borrows at a given place, which should be
-    seen as an l-value (we will write to it later, but need to drop
-    the borrows before writing).
+(** Drop (end) outer loans at a given place, which should be seen as an l-value
+    (we will write to it later, but need to drop the loans before writing).
 
     This is used to drop values when evaluating the drop statement or before
     writing to a place.
     
-    [end_borrows]:
-    - if true: end all the loans and borrows we find, starting with the outer
-      ones. This is used when evaluating the {!LlbcAst.Drop} statement (see {!InterpreterStatements.drop_value})
-    - if false: only end the outer loans. This is used by {!InterpreterStatements.assign_to_place}
-      or to drop the loans in the local variables when popping a frame.
-    TODO: remove this option, it is actually not used anymore (should always be
-    false).
-
     Note that we don't do what is defined in the formalization: we move the
-    value to a temporary dummy value, then explore this value and end the
-    loans/borrows inside as long as we find some, starting with the outer
-    ones, then move the resulting value back to where it was. This shouldn't
-    make any difference, really (note that the place is *inside* a borrow,
-    if we end the borrow, we won't be able to reinsert the value back).
+    value to a temporary dummy value, then explore this value and end the outer
+    loans which are inside as long as we find some, then move the resulting
+    value back to where it was. This shouldn't make any difference, really (note
+    that the place is *inside* a borrow, if we end the borrow, we won't be able
+    to reinsert the value back).
  *)
-let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
-    (p : E.place) : cm_fun =
+let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
  fun cf ctx ->
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
@@ -652,7 +642,8 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
     (* Read the value *)
     let v = C.ctx_read_first_dummy_var ctx in
     (* Check if there are loans or borrows to end *)
-    match get_first_outer_loan_or_borrow_in_value end_borrows v with
+    let with_borrows = false in
+    match get_first_outer_loan_or_borrow_in_value with_borrows v with
     | None ->
         (* We are done: simply call the continuation *)
         cf ctx
@@ -662,12 +653,8 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
           match c with
           | LoanContent (V.SharedLoan (bids, _)) ->
               end_outer_borrows config bids
-          | LoanContent (V.MutLoan bid)
-          | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow (_, bid)) ->
-              end_outer_borrow config bid
-          | BorrowContent (V.InactivatedMutBorrow (_, bid)) ->
-              (* First activate the borrow *)
-              activate_inactivated_mut_borrow config bid
+          | LoanContent (V.MutLoan bid) -> end_outer_borrow config bid
+          | BorrowContent _ -> raise (Failure "Unreachable")
         in
         (* Retry *)
         comp cc drop cf ctx
@@ -682,10 +669,7 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
         (* Reinsert *)
         let ctx = write_place_unwrap config access p v ctx in
         (* Sanity check *)
-        if end_borrows then (
-          assert (not (loans_in_value v));
-          assert (not (borrows_in_value v)))
-        else assert (not (outer_loans_in_value v));
+        assert (not (outer_loans_in_value v));
         (* Continue *)
         cf ctx)
   in
@@ -768,18 +752,14 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
 (** Small utility.
     
     Prepare a place which is to be used as the destination of an assignment:
-    update the environment along the paths, end the loans at this place, etc.
+    update the environment along the paths, end the outer loans at this place, etc.
 
     Return the updated context and the (updated) value at the end of the
-    place. This value should not contain any loan or borrow (and we check
+    place. This value should not contain any outer loan (and we check
     it is the case). Note that this value is very likely to contain {!V.Bottom}
     subvalues.
-    
-    [end_borrows]: if false, we only end the outer loans we find. If true, we
-    end all the loans and the borrows we find.
-    TODO: end_borrows is not necessary anymore.
  *)
-let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place)
+let prepare_lplace (config : C.config) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug
@@ -790,16 +770,13 @@ let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place)
   let access = Write in
   let cc = update_ctx_along_write_place config access p in
   (* End the borrows and loans, starting with the borrows *)
-  let cc = comp cc (drop_outer_borrows_loans_at_lplace config end_borrows p) in
+  let cc = comp cc (drop_outer_loans_at_lplace config p) in
   (* Read the value and check it *)
   let read_check cf : m_fun =
    fun ctx ->
     let v = read_place_unwrap config access p ctx in
     (* Sanity checks *)
-    if end_borrows then (
-      assert (not (loans_in_value v));
-      assert (not (borrows_in_value v)))
-    else assert (not (outer_loans_in_value v));
+    assert (not (outer_loans_in_value v));
     (* Continue *)
     cf v ctx
   in
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index ebba0e56..84a6716c 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -34,8 +34,7 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
    * symbolic values along the path, for instance *)
   let cc = update_ctx_along_read_place config access p in
   (* Prepare the place (by ending the outer loans *at* the place). *)
-  let end_borrows = false in
-  let cc = comp cc (prepare_lplace config end_borrows p) in
+  let cc = comp cc (prepare_lplace config p) in
   (* Replace the value with {!Bottom} *)
   let replace cf (v : V.typed_value) ctx =
     (* Move the value at destination (that we will overwrite) to a dummy variable
@@ -109,8 +108,7 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) :
   (* Push the rvalue to a dummy variable, for bookkeeping *)
   let cc = push_dummy_var rv in
   (* Prepare the destination *)
-  let end_borrows = false in
-  let cc = comp cc (prepare_lplace config end_borrows p) in
+  let cc = comp cc (prepare_lplace config p) in
   (* Retrieve the rvalue from the dummy variable *)
   let cc = comp cc (fun cf _lv -> pop_dummy_var cf) in
   (* Update the destination *)
@@ -223,8 +221,7 @@ let set_discriminant (config : C.config) (p : E.place)
   (* Access the value *)
   let access = Write in
   let cc = update_ctx_along_read_place config access p in
-  let end_borrows = false in
-  let cc = comp cc (prepare_lplace config end_borrows p) in
+  let cc = comp cc (prepare_lplace config p) in
   (* Update the value *)
   let update_value cf (v : V.typed_value) : m_fun =
    fun ctx ->
@@ -366,13 +363,11 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
   (* Drop the outer *loans* we find in the local variables *)
   let cf_drop_loans_in_locals cf (ret_value : V.typed_value) : m_fun =
     (* Drop the loans *)
-    let end_borrows = false in
     let locals = List.rev locals in
     let cf_drop =
       List.fold_left
         (fun cf lid ->
-          drop_outer_borrows_loans_at_lplace config end_borrows
-            (mk_place_from_var_id lid) cf)
+          drop_outer_loans_at_lplace config (mk_place_from_var_id lid) cf)
         (cf ret_value) locals
     in
     (* Apply *)