Start updating end_borrow_in_env to take abstractions into account

2 files changed, 223 insertions, 101 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 901d12e3..e0ded437 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -76,6 +76,8 @@ type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
 type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
 (** Generic borrow content: concrete or abstract *)
 
+type abs_or_var = Abs of V.AbstractionId.id | Var of V.VarId.id
+
 exception Found
 (** Utility exception
 
@@ -143,9 +145,16 @@ let loans_in_value (v : V.typed_value) : bool =
 (** Lookup a loan content.
 
     The loan is referred to by a borrow id.
+
+    TODO: group abs_or_var and g_loan_content. 
  *)
 let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
-    g_loan_content option =
+    (abs_or_var * g_loan_content) option =
+  (* We store here whether we are inside an abstraction or a value - note that we
+   * could also track that with the environment, it would probably be more idiomatic
+   * and cleaner *)
+  let abs_or_var : abs_or_var option ref = ref None in
+
   let obj =
     object
       inherit [_] C.iter_env as super
@@ -202,15 +211,28 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
           allow to dive inside abstractions, we allow to go anywhere
           (because there are no use cases requiring finer control) *)
 
-      method! visit_abs env abs =
-        if ek.enter_abs then super#visit_Abs env abs else ()
+      method! visit_Var env bv v =
+        assert (Option.is_none !abs_or_var);
+        abs_or_var := Some (Var bv.C.index);
+        super#visit_Var env bv v;
+        abs_or_var := None
+
+      method! visit_Abs env abs =
+        assert (Option.is_none !abs_or_var);
+        if ek.enter_abs then (
+          abs_or_var := Some (Abs abs.V.abs_id);
+          super#visit_Abs env abs)
+        else ()
     end
   in
   (* We use exceptions *)
   try
     obj#visit_env () env;
     None
-  with FoundGLoanContent lc -> Some lc
+  with FoundGLoanContent lc -> (
+    match !abs_or_var with
+    | Some abs_or_var -> Some (abs_or_var, lc)
+    | None -> failwith "Inconsistent state")
 
 (** Lookup a loan content.
 
@@ -218,10 +240,10 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
     Raises an exception if no loan was found.
  *)
 let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
-    g_loan_content =
+    abs_or_var * g_loan_content =
   match lookup_loan_opt ek l env with
   | None -> failwith "Unreachable"
-  | Some lc -> lc
+  | Some res -> res
 
 (** Update a loan content.
 
@@ -400,7 +422,7 @@ let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
 
     The borrow is referred to by a borrow id.
 
-    This is a helper function: it might break invariants.     
+    This is a helper function: it might break invariants.   
  *)
 let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
     (nbc : V.borrow_content) (env : C.env) : C.env =
@@ -507,12 +529,16 @@ type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id
 let update_if_none opt x = match opt with None -> Some x | _ -> opt
 
 (** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *)
-let update_outer_borrows (io : inner_outer) opt x =
+let update_outer_borrows (io : inner_outer)
+    (outer : V.AbstractionId.id option * borrow_ids option) (x : borrow_ids) :
+    V.AbstractionId.id option * borrow_ids option =
   match io with
   | Inner ->
       (* If we can end inner borrows, we don't keep track of the outer borrows *)
-      None
-  | Outer -> update_if_none opt x
+      outer
+  | Outer ->
+      let abs, opt = outer in
+      (abs, update_if_none opt x)
 
 (** Return the first loan we find in a value *)
 let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
@@ -544,7 +570,11 @@ let bottom_in_value (v : V.typed_value) : bool =
     false
   with Found -> true
 
-exception FoundOuter of borrow_ids
+type outer_borrows_or_abs =
+  | OuterBorrows of borrow_ids
+  | OuterAbs of V.AbstractionId.id
+
+exception FoundOuter of outer_borrows_or_abs
 (** Utility exception *)
 
 (** Auxiliary function to end borrows: lookup a borrow in the environment,
@@ -555,22 +585,40 @@ exception FoundOuter of borrow_ids
     [end_borrow] then simply performs a loop: as long as we need to end (outer)
     borrows, we end them, before finally ending the borrow we wanted to end in the
     first place.
+
+    Note that it is possible to end a borrow in an abstraction, without ending
+    the whole abstraction, if the corresponding loan is inside the abstraction
+    as well. The [allowed_abs] parameter controls whether we allow to end borrows
+    in an abstraction or not, and in which abstraction.
 *)
-let end_borrow_get_borrow_in_env (io : inner_outer) (l : V.BorrowId.id)
-    (env : C.env) : (C.env * V.borrow_content option, borrow_ids) result =
+let end_borrow_get_borrow_in_env (io : inner_outer)
+    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (env : C.env)
+    : (C.env * g_borrow_content option, outer_borrows_or_abs) result =
   (* We use a reference to communicate the kind of borrow we found, if we
    * find one *)
-  let replaced_bc : V.borrow_content option ref = ref None in
-  let set_replaced_bc bc =
+  let replaced_bc : g_borrow_content option ref = ref None in
+  let set_replaced_bc (bc : g_borrow_content) =
     assert (Option.is_none !replaced_bc);
     replaced_bc := Some bc
   in
-  (* Raise an exception if there are outer borrows: this exception is caught
-   * in a wrapper function *)
-  let raise_if_outer outer_borrows =
-    match outer_borrows with
-    | Some borrows -> raise (FoundOuter borrows)
-    | None -> ()
+  (* Raise an exception if there are outer borrows or if we are inside an
+   * abstraction: this exception is caught in a wrapper function *)
+  let raise_if_outer (outer : V.AbstractionId.id option * borrow_ids option) =
+    let outer_abs, outer_borrows = outer in
+    match outer_abs with
+    | Some abs -> (
+        if
+          (* Check if we can end borrows inside this abstraction *)
+          Some abs <> allowed_abs
+        then raise (FoundOuter (OuterAbs abs))
+        else
+          match outer_borrows with
+          | Some borrows -> raise (FoundOuter (OuterBorrows borrows))
+          | None -> ())
+    | None -> (
+        match outer_borrows with
+        | Some borrows -> raise (FoundOuter (OuterBorrows borrows))
+        | None -> ())
   in
 
   (* The environment is used to keep track of the outer loans *)
@@ -578,52 +626,59 @@ let end_borrow_get_borrow_in_env (io : inner_outer) (l : V.BorrowId.id)
     object
       inherit [_] C.map_env as super
 
-      method! visit_Loan outer_borrows lc =
+      method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option)
+          lc =
         match lc with
-        | V.MutLoan bid -> V.Loan (super#visit_MutLoan outer_borrows bid)
+        | V.MutLoan bid -> V.Loan (super#visit_MutLoan outer bid)
         | V.SharedLoan (bids, v) ->
             (* Update the outer borrows before diving into the shared value *)
-            let outer_borrows =
-              update_outer_borrows io outer_borrows (Borrows bids)
-            in
-            V.Loan (super#visit_SharedLoan outer_borrows bids v)
+            let outer = update_outer_borrows io outer (Borrows bids) in
+            V.Loan (super#visit_SharedLoan outer bids v)
       (** We reimplement [visit_Loan] because we may have to update the
-             outer borrows *)
+          outer borrows *)
 
-      method! visit_Borrow outer_borrows bc =
+      method! visit_Borrow outer bc =
         match bc with
         | SharedBorrow l' | InactivatedMutBorrow l' ->
             (* Check if this is the borrow we are looking for *)
             if l = l' then (
-              (* Check if there are outer borrows *)
-              raise_if_outer outer_borrows;
+              (* Check if there are outer borrows or if we are inside an abstraction *)
+              raise_if_outer outer;
               (* Register the update *)
-              set_replaced_bc bc;
+              set_replaced_bc (Concrete bc);
               (* Update the value *)
               V.Bottom)
-            else super#visit_Borrow outer_borrows bc
+            else super#visit_Borrow outer bc
         | V.MutBorrow (l', bv) ->
             (* Check if this is the borrow we are looking for *)
             if l = l' then (
-              (* Check if there are outer borrows *)
-              raise_if_outer outer_borrows;
+              (* Check if there are outer borrows or if we are inside an abstraction *)
+              raise_if_outer outer;
               (* Register the update *)
-              set_replaced_bc bc;
+              set_replaced_bc (Concrete bc);
               (* Update the value *)
               V.Bottom)
             else
               (* Update the outer borrows before diving into the borrowed value *)
-              let outer_borrows =
-                update_outer_borrows io outer_borrows (Borrow l')
-              in
-              V.Borrow (super#visit_MutBorrow outer_borrows l' bv)
+              let outer_borrows = update_outer_borrows io outer (Borrow l') in
+              V.Borrow (super#visit_MutBorrow outer l' bv)
 
-      method! visit_Abs _ _ = raise Unimplemented
+      method! visit_ALoan outer bc = raise Unimplemented
+
+      method! visit_ABorrow outer bc = raise Unimplemented
+
+      method! visit_abs outer abs =
+        (* Update the outer abs *)
+        let outer_abs, outer_borrows = outer in
+        assert (Option.is_none outer_abs);
+        assert (Option.is_none outer_borrows);
+        let outer = (Some abs.V.abs_id, None) in
+        super#visit_abs outer abs
     end
   in
   (* Catch the exceptions - raised if there are outer borrows *)
   try
-    let env = obj#visit_env None env in
+    let env = obj#visit_env (None, None) env in
     Ok (env, !replaced_bc)
   with FoundOuter outers -> Error outers
 
@@ -784,81 +839,146 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
   assert !r;
   { ctx with env }
 
+(** Auxiliary function: see [end_borrow_in_env] *)
+let give_back_in_env (config : C.config) (l : V.BorrowId.id)
+    (bc : g_borrow_content) (env : C.env) : C.env =
+  (* This is used for sanity checks *)
+  let sanity_ek =
+    { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
+  in
+  match bc with
+  | Concrete (V.MutBorrow (_, tv)) ->
+      (* Check that the corresponding loan is somewhere - purely a sanity check *)
+      assert (Option.is_some (lookup_loan_opt sanity_ek l env));
+      give_back_value config l tv env
+  | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') ->
+      assert (l' = l);
+      (* Sanity check *)
+      (* Check that the borrow is somewhere - purely a sanity check *)
+      assert (Option.is_some (lookup_loan_opt sanity_ek l env));
+      give_back_shared config l env
+  | Abstract _ -> raise Unimplemented
+
 (** End a borrow identified by its borrow id in an environment
     
     First lookup the borrow in the environment and replace it with [Bottom].
     Then, check that there is an associated loan in the environment. When moving
-    values, before putting putting the value in its destination, we get an
+    values, before putting the value in its destination, we get an
     intermediate state where some values are "outside" the environment and thus
-    inaccessible. As [give_back_value] just performs a map for instance, we
-    need to check independently that there is indeed a loan ready to receive
-    the value we give back (note that we also have other invariants like: there
-    is exacly one mutable loan associated to a mutable borrow, etc. but they
-    are more easily maintained). Note that in theory, we shouldn't never reach a
-    problematic state as the one we describe above, because when we move a value
-    we need to end all the loans inside before moving it. Still, it is a very
-    useful sanity check.
+    inaccessible. As [give_back_value] just performs a map for instance (TODO:
+    not the case anymore), we need to check independently that there is indeed a
+    loan ready to receive the value we give back (note that we also have other
+    invariants like: there is exacly one mutable loan associated to a mutable
+    borrow, etc. but they are more easily maintained).
+    Note that in theory, we shouldn't never reach a problematic state as the
+    one we describe above, because when we move a value we need to end all the
+    loans inside before moving it. Still, it is a very useful sanity check.
     Finally, give the values back.
 
     Of course, we end outer borrows before updating the target borrow if it
     proves necessary: this is controled by the [io] parameter. If it is [Inner],
     we allow ending inner borrows (without ending the outer borrows first),
     otherwise we only allow ending outer borrows.
+    If a borrow is inside an abstraction, we need to end the whole abstraction,
+    at the exception of the case where the loan corresponding to the borrow is
+    inside the same abstraction. We control this with the [allowed_abs] parameter:
+    if it is not `None`, we allow ending a borrow if it is inside the given
+    abstraction. In practice, if the value is `Some abs_id`, we should have
+    checked that the corresponding loan is inside the abstraction given by
+    `abs_id` before. In practice, only [end_borrow_in_env] should call itself
+    with `allowed_abs = Some ...`, all the other calls should use `allowed_abs = None`:
+    if you look ath the implementation details, `end_borrow_in_env` performs
+    all tne necessary checks in case a borrow is inside an abstraction.
  *)
 let rec end_borrow_in_env (config : C.config) (io : inner_outer)
-    (l : V.BorrowId.id) (env : C.env) : C.env =
-  (* This is used for sanity checks *)
-  let sanity_ek =
-    { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
-  in
-  match end_borrow_get_borrow_in_env io l env with
+    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) (env : C.env)
+    : C.env =
+  match end_borrow_get_borrow_in_env io allowed_abs l env with
   (* Two cases:
    * - error: we found outer borrows (end them first)
    * - success: we didn't find outer borrows when updating (but maybe we actually
        didn't find the borrow we were looking for...)
    *)
-  | Error outer_borrows ->
-      (* End the outer borrows *)
-      let env =
-        match outer_borrows with
-        | Borrows bids -> end_borrows_in_env config io bids env
-        | Borrow bid -> end_borrow_in_env config io bid env
-      in
-      (* Retry to end the borrow *)
-      end_borrow_in_env config io l env
+  | Error outer -> (
+      (* End the outer borrows, abstraction, then try again to end the target
+       * borrow (if necessary) *)
+      match outer with
+      | OuterBorrows (Borrows bids) ->
+          (* Note that when ending outer borrows, we use io=Outer. However,
+           * we shouldn't need to end outer borrows if io=Inner, so we just
+           * add the following assertion *)
+          assert (io = Outer);
+          let allowed_abs' = None in
+          let env = end_borrows_in_env config io allowed_abs' bids env in
+          (* Retry to end the borrow *)
+          end_borrow_in_env config io allowed_abs l env
+      | OuterBorrows (Borrow bid) ->
+          assert (io = Outer);
+          let allowed_abs' = None in
+          let env = end_borrow_in_env config io allowed_abs' bid env in
+          (* Retry to end the borrow *)
+          end_borrow_in_env config io allowed_abs l env
+      | OuterAbs abs_id -> (
+          (* The borrow is inside an asbtraction: check if the corresponding
+           * loan is inside the same abstraction. If this is the case, we end
+           * the borrow without ending the abstraction. If not, we need to
+           * end the whole abstraction *)
+          let ek =
+            {
+              enter_shared_loans = true;
+              enter_mut_borrows = true;
+              enter_abs = true;
+            }
+          in
+          match lookup_loan ek l env with
+          | Abs loan_abs_id, _ ->
+              if loan_abs_id = abs_id then (
+                (* Same abstraction! We can end the borrow *)
+                let env = end_borrow_in_env config io (Some abs_id) l env in
+                (* Sanity check *)
+                assert (Option.is_none (lookup_borrow_opt ek l env));
+                env)
+              else
+                (* Not the same abstraction: we need to end the whole abstraction *)
+                let env = end_abstraction_in_env config abs_id env in
+                (* Sanity check *)
+                assert (Option.is_none (lookup_borrow_opt ek l env));
+                env
+          | Var _, _ ->
+              (* The loan is not inside the same abstraction (actually inside
+               * a non-abstraction value): we need to end the whole abstraction *)
+              let env = end_abstraction_in_env config abs_id env in
+              (* Sanity check *)
+              assert (Option.is_none (lookup_borrow_opt ek l env));
+              env))
   | Ok (env, None) ->
       (* It is possible that we can't find a borrow in symbolic mode (ending
        * an abstraction may end several borrows at once *)
       assert (config.mode = SymbolicMode);
       env
   (* We found a borrow: give the value back (i.e., update the corresponding loan) *)
-  | Ok (env, Some bc) -> (
-      match bc with
-      | V.MutBorrow (_, tv) ->
-          (* Check that the corresponding loan is somewhere - purely a sanity check *)
-          assert (Option.is_some (lookup_loan_opt sanity_ek l env));
-          give_back_value config l tv env
-      | V.SharedBorrow l' | V.InactivatedMutBorrow l' ->
-          assert (l' = l);
-          (* Sanity check *)
-          (* Check that the borrow is somewhere - purely a sanity check *)
-          assert (Option.is_some (lookup_loan_opt sanity_ek l env));
-          give_back_shared config l env)
+  | Ok (env, Some bc) -> give_back_in_env config l bc env
 
 and end_borrows_in_env (config : C.config) (io : inner_outer)
-    (lset : V.BorrowId.Set.t) (env : C.env) : C.env =
+    (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t)
+    (env : C.env) : C.env =
   V.BorrowId.Set.fold
-    (fun id env -> end_borrow_in_env config io id env)
+    (fun id env -> end_borrow_in_env config io allowed_abs id env)
     lset env
 
+and end_abstraction_in_env (config : C.config) (abs : V.AbstractionId.id)
+    (env : C.env) : C.env =
+  raise Unimplemented
+
 (** Same as [end_borrow_in_env], but operating on evaluation contexts *)
-let end_borrow (config : C.config) (io : inner_outer) (l : V.BorrowId.id)
+let end_borrow (config : C.config) (io : inner_outer)
+    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id)
     (ctx : C.eval_ctx) : C.eval_ctx =
   L.log#ldebug
     (lazy
       ("end_borrow " ^ V.BorrowId.to_string l ^ ": context before:\n"
      ^ eval_ctx_to_string ctx));
-  let env = end_borrow_in_env config io l ctx.env in
+  let env = end_borrow_in_env config io allowed_abs l ctx.env in
   let ctx = { ctx with env } in
   L.log#ldebug
     (lazy
@@ -867,14 +987,15 @@ let end_borrow (config : C.config) (io : inner_outer) (l : V.BorrowId.id)
   ctx
 
 (** Same as [end_borrows_in_env], but operating on evaluation contexts *)
-let end_borrows (config : C.config) (io : inner_outer) (lset : V.BorrowId.Set.t)
+let end_borrows (config : C.config) (io : inner_outer)
+    (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t)
     (ctx : C.eval_ctx) : C.eval_ctx =
   L.log#ldebug
     (lazy
       ("end_borrows "
       ^ V.BorrowId.set_to_string lset
       ^ ": context before:\n" ^ eval_ctx_to_string ctx));
-  let env = end_borrows_in_env config io lset ctx.env in
+  let env = end_borrows_in_env config io allowed_abs lset ctx.env in
   let ctx = { ctx with env } in
   L.log#ldebug
     (lazy
@@ -883,13 +1004,13 @@ let end_borrows (config : C.config) (io : inner_outer) (lset : V.BorrowId.Set.t)
       ^ ": context after:\n" ^ eval_ctx_to_string ctx));
   ctx
 
-let end_outer_borrow config = end_borrow config Outer
+let end_outer_borrow config = end_borrow config Outer None
 
-let end_outer_borrows config = end_borrows config Outer
+let end_outer_borrows config = end_borrows config Outer None
 
-let end_inner_borrow config = end_borrow config Inner
+let end_inner_borrow config = end_borrow config Inner None
 
-let end_inner_borrows config = end_borrows config Inner
+let end_inner_borrows config = end_borrows config Inner None
 
 (** Helper function: see [activate_inactivated_mut_borrow].
 
@@ -912,9 +1033,9 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
   match lookup_loan ek l ctx.env with
-  | Concrete (V.MutLoan _) ->
+  | _, Concrete (V.MutLoan _) ->
       failwith "Expected a shared loan, found a mut loan"
-  | Concrete (V.SharedLoan (bids, sv)) ->
+  | _, Concrete (V.SharedLoan (bids, sv)) ->
       (* Check that there is only one borrow id (l) and update the loan *)
       assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1);
       (* We need to check that there aren't any loans in the value:
@@ -930,7 +1051,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
       let ctx = { ctx with env } in
       (* Return *)
       (ctx, sv)
-  | Abstract _ -> raise Unimplemented
+  | _, Abstract _ -> raise Unimplemented
 
 (** Helper function: see [activate_inactivated_mut_borrow].
 
@@ -964,8 +1085,8 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
   match lookup_loan ek l ctx.env with
-  | Concrete (V.MutLoan _) -> failwith "Unreachable"
-  | Concrete (V.SharedLoan (bids, sv)) -> (
+  | _, Concrete (V.MutLoan _) -> failwith "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.
          If we perform an update, do a recursive call to lookup the updated value *)
@@ -992,14 +1113,15 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
           (* 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
-          let ctx = end_borrows config io bids ctx in
+          let allowed_abs = None in
+          let ctx = end_borrows config io allowed_abs bids ctx in
           (* Promote the loan *)
           let ctx, borrowed_value = promote_shared_loan_to_mut_loan l ctx in
           (* Promote the borrow - the value should have been checked by
              [promote_shared_loan_to_mut_loan]
           *)
           promote_inactivated_borrow_to_mut_borrow l borrowed_value ctx)
-  | Abstract _ -> raise Unimplemented
+  | _, Abstract _ -> raise Unimplemented
 
 (** Paths *)
 
@@ -1148,8 +1270,8 @@ let rec access_projection (access : projection_access) (env : C.env)
               (* Lookup the loan content, and explore from there *)
               if access.lookup_shared_borrows then
                 match lookup_loan ek bid env with
-                | Concrete (V.MutLoan _) -> failwith "Expected a shared loan"
-                | Concrete (V.SharedLoan (bids, sv)) -> (
+                | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan"
+                | _, Concrete (V.SharedLoan (bids, sv)) -> (
                     (* Explore the shared value *)
                     match access_projection access env update p' sv with
                     | Error err -> Error err
@@ -1163,7 +1285,7 @@ let rec access_projection (access : projection_access) (env : C.env)
                         in
                         (* Return - note that we don't need to update the borrow itself *)
                         Ok (env, { res with updated = v }))
-                | Abstract _ -> raise Unimplemented
+                | _, Abstract _ -> raise Unimplemented
               else Error (FailBorrow bc)
           | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid)
           | V.MutBorrow (bid, bv) ->
@@ -2021,10 +2143,10 @@ let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
   let v = read_place_unwrap config access p ctx in
   match v.V.value with
   | V.Loan (V.SharedLoan (bids, _)) ->
-      let ctx = end_borrows config Outer bids ctx in
+      let ctx = end_outer_borrows config bids ctx in
       end_loan_exactly_at_place config access p ctx
   | V.Loan (V.MutLoan bid) ->
-      let ctx = end_borrow config Outer bid ctx in
+      let ctx = end_outer_borrow config bid ctx in
       end_loan_exactly_at_place config access p ctx
   | _ -> ctx
 
diff --git a/src/Values.ml b/src/Values.ml
index bd07ce98..f2f2274d 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -3,7 +3,7 @@ open Types
 
 (* TODO: I often write "abstract" (value, borrow content, etc.) while I should
  * write "abstraction" (because those values are not abstract, they simply are
-* inside abstractions) *)
+ * inside abstractions) *)
 
 module VarId = IdGen ()