Move some functions from Interpreter to InterpreterBorrows

2 files changed, 1116 insertions, 1099 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index afe513be..7dc37dff 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -14,6 +14,7 @@ module S = Synthesis
 open Utils
 open InterpreterUtils
 open InterpreterProjectors
+open InterpreterBorrows
 
 (* TODO: check that the value types are correct when evaluating *)
 (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
@@ -35,1105 +36,6 @@ type eval_error = Panic
 
 type 'a eval_result = ('a, eval_error) result
 
-(** Auxiliary function to end borrows: lookup a borrow in the environment,
-    update it (by returning an updated environment where the borrow has been
-    replaced by [Bottom])) if we can end the borrow (for instance, it is not
-    an outer borrow...) or return the reason why we couldn't update the borrow.
-
-    [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 (io : inner_outer)
-    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id)
-    (ctx : C.eval_ctx) :
-    (C.eval_ctx * 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 : 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 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 *)
-  let obj =
-    object
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option)
-          lc =
-        match lc with
-        | 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 = 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 *)
-
-      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 or if we are inside an abstraction *)
-              raise_if_outer outer;
-              (* Register the update *)
-              set_replaced_bc (Concrete bc);
-              (* Update the value *)
-              V.Bottom)
-            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 or if we are inside an abstraction *)
-              raise_if_outer outer;
-              (* Register the update *)
-              set_replaced_bc (Concrete bc);
-              (* Update the value *)
-              V.Bottom)
-            else
-              (* Update the outer borrows before diving into the borrowed value *)
-              let outer = update_outer_borrows io outer (Borrow l') in
-              V.Borrow (super#visit_MutBorrow outer l' bv)
-
-      method! visit_ALoan outer lc =
-        (* Note that the children avalues are just other, independent loans,
-         * so we don't need to update the outer borrows when diving in.
-         * We keep track of the parents/children relationship only because we
-         * need it to properly instantiate the backward functions when generating
-         * the pure translation. *)
-        match lc with
-        | V.AMutLoan (bid, av) ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AMutLoan outer bid av)
-        | V.ASharedLoan (bids, v, av) ->
-            (* Explore the shared value - we need to update the outer borrows *)
-            let souter = update_outer_borrows io outer (Borrows bids) in
-            let v = super#visit_typed_value souter v in
-            (* Explore the child avalue - we keep the same outer borrows *)
-            let av = super#visit_typed_avalue outer av in
-            (* Reconstruct *)
-            V.ALoan (V.ASharedLoan (bids, v, av))
-        | V.AEndedMutLoan { given_back; child } ->
-            (* The loan has ended, so no need to update the outer borrows *)
-            V.ALoan (super#visit_AEndedMutLoan outer given_back child)
-        | V.AEndedSharedLoan (v, av) ->
-            (* The loan has ended, so no need to update the outer borrows *)
-            V.ALoan (super#visit_AEndedSharedLoan outer v av)
-        | V.AIgnoredMutLoan (bid, av) ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredMutLoan outer bid av)
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedIgnoredMutLoan outer given_back child)
-        | V.AIgnoredSharedLoan av ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredSharedLoan outer av)
-      (** We reimplement [visit_ALoan] because we may have to update the
-          outer borrows *)
-
-      method! visit_ABorrow outer bc =
-        match bc with
-        | V.AMutBorrow (bid, av) ->
-            (* Check if this is the borrow we are looking for *)
-            if bid = l then (
-              (* When ending a mut borrow, there are two cases:
-               * - in the general case, we have to end the whole abstraction
-               *   (and thus raise an exception to signal that to the caller)
-               * - in some situations, the associated loan is inside the same
-               *   abstraction as the borrow. In this situation, we can end
-               *   the borrow without ending the whole abstraction, and we
-               *   simply move the child avalue around.
-               *)
-              (* Check there are outer borrows, or if we need to end the whole
-               * abstraction *)
-              raise_if_outer outer;
-              (* Register the update *)
-              set_replaced_bc (Abstract bc);
-              (* Update the value - note that we are necessarily in the second
-               * of the two cases described above *)
-              V.ABottom)
-            else
-              (* Update the outer borrows before diving into the child avalue *)
-              let outer = update_outer_borrows io outer (Borrow bid) in
-              V.ABorrow (super#visit_AMutBorrow outer bid av)
-        | V.ASharedBorrow bid ->
-            (* Check if this is the borrow we are looking for *)
-            if bid = l then (
-              (* Check there are outer borrows, or if we need to end the whole
-               * abstraction *)
-              raise_if_outer outer;
-              (* Register the update *)
-              set_replaced_bc (Abstract bc);
-              (* Update the value - note that we are necessarily in the second
-               * of the two cases described above *)
-              V.ABottom)
-            else V.ABorrow (super#visit_ASharedBorrow outer bid)
-        | V.AIgnoredMutBorrow av ->
-            (* Nothing special to do *)
-            V.ABorrow (super#visit_AIgnoredMutBorrow outer av)
-        | V.AProjSharedBorrow asb ->
-            (* Check if the borrow we are looking for is in the asb *)
-            if borrow_in_asb l asb then (
-              (* Check there are outer borrows, or if we need to end the whole
-               * abstraction *)
-              raise_if_outer outer;
-              (* Register the update *)
-              set_replaced_bc (Abstract bc);
-              (* Update the value - note that we are necessarily in the second
-               * of the two cases described above *)
-              let asb = remove_borrow_from_asb l asb in
-              V.ABorrow (V.AProjSharedBorrow asb))
-            else
-              (* Nothing special to do *)
-              V.ABorrow (super#visit_AProjSharedBorrow outer asb)
-
-      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 ctx = obj#visit_eval_ctx (None, None) ctx in
-    Ok (ctx, !replaced_bc)
-  with FoundOuter outers -> Error outers
-
-(** Auxiliary function to end borrows. See [give_back].
-    
-    When we end a mutable borrow, we need to "give back" the value it contained
-    to its original owner by reinserting it at the proper position.
-
-    Note that this function checks that there is exactly one loan to which we
-    give the value back.
-    TODO: this was not the case before, so some sanity checks are not useful anymore.
- *)
-let give_back_value (config : C.config) (bid : V.BorrowId.id)
-    (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* We use a reference to check that we updated exactly one loan *)
-  let replaced : bool ref = ref false in
-  let set_replaced () =
-    assert (not !replaced);
-    replaced := true
-  in
-  (* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
-  let check_symbolic_no_ended = true in
-  (* We sometimes need to reborrow values while giving a value back due: prepare that *)
-  let allow_reborrows = true in
-  let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows ctx
-  in
-  (* The visitor to give back the values *)
-  let obj =
-    object (self)
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_Loan opt_abs lc =
-        match lc with
-        | V.SharedLoan (bids, v) ->
-            (* We are giving back a value (i.e., the content of a *mutable*
-             * borrow): nothing special to do *)
-            V.Loan (super#visit_SharedLoan opt_abs bids v)
-        | V.MutLoan bid' ->
-            (* Check if this is the loan we are looking for *)
-            if bid' = bid then (
-              set_replaced ();
-              nv.V.value)
-            else V.Loan (super#visit_MutLoan opt_abs bid')
-
-      method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
-          =
-        match av.V.value with
-        | V.ALoan lc ->
-            let value = self#visit_typed_ALoan opt_abs av.V.ty lc in
-            ({ av with V.value } : V.typed_avalue)
-        | _ -> super#visit_typed_avalue opt_abs av
-      (** This is a bit annoying, but as we need the type of the avalue we
-          are exploring, in order to be able to project the value we give
-          back, we need to reimplement [visit_typed_avalue] instead of
-          [visit_ALoan] *)
-
-      method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
-          (lc : V.aloan_content) : V.avalue =
-        (* Preparing a bit *)
-        let regions =
-          match opt_abs with
-          | None -> failwith "Unreachable"
-          | Some abs -> abs.V.regions
-        in
-        match lc with
-        | V.AMutLoan (bid', child) ->
-            if bid' = bid then (
-              (* This is the loan we are looking for: apply the projection to
-               * the value we give back and replaced this mutable loan with
-               * an ended loan *)
-              (* Register the insertion *)
-              set_replaced ();
-              (* Apply the projection *)
-              let given_back =
-                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  regions nv ty
-              in
-              (* Return the new value *)
-              V.ALoan (V.AEndedMutLoan { given_back; child }))
-            else
-              (* Continue exploring *)
-              V.ALoan (super#visit_AMutLoan opt_abs bid' child)
-        | V.ASharedLoan (bids, v, av) ->
-            (* We are giving back a value to a *mutable* loan: nothing special to do *)
-            V.ALoan (super#visit_ASharedLoan opt_abs bids v av)
-        | V.AEndedMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
-        | V.AEndedSharedLoan (v, av) ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
-        | V.AIgnoredMutLoan (bid', child) ->
-            (* This loan is ignored, but we may have to project on a subvalue
-             * of the value which is given back *)
-            if bid' = bid then
-              (* Note that we replace the ignored mut loan by an *ended* ignored
-               * mut loan. Also, this is not the loan we are looking for *per se*:
-               * we don't register the fact that we inserted the value somewhere
-               * (i.e., we don't call [set_replaced]) *)
-              let given_back =
-                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  regions nv ty
-              in
-              V.ALoan (V.AEndedIgnoredMutLoan { given_back; child })
-            else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
-        | V.AIgnoredSharedLoan av ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
-      (** We are not specializing an already existing method, but adding a
-          new method (for projections, we need type information) *)
-
-      method! visit_Abs opt_abs abs =
-        (* We remember in which abstraction we are before diving -
-         * this is necessary for projecting values: we need to know
-         * over which regions to project *)
-        assert (Option.is_none opt_abs);
-        super#visit_Abs (Some abs) abs
-    end
-  in
-
-  (* Explore the environment *)
-  let ctx = obj#visit_eval_ctx None ctx in
-  (* Check we gave back to exactly one loan *)
-  assert !replaced;
-  (* Apply the reborrows *)
-  apply_registered_reborrows ctx
-
-(** Auxiliary function to end borrows. See [give_back].
-
-    This function is similar to [give_back_value] but gives back an [avalue]
-    (coming from an abstraction).
-
-    It is used when ending a borrow inside an abstraction, when the corresponding
-    loan is inside the same abstraction (in which case we don't need to end the whole
-    abstraction).
-    
-    REMARK: this function can't be used to give back the values borrowed by
-    end abstraction when ending this abstraction. When doing this, we need
-    to convert the [avalue] to a [value] by introducing the proper symbolic values.
- *)
-let give_back_avalue (_config : C.config) (bid : V.BorrowId.id)
-    (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* We use a reference to check that we updated exactly one loan *)
-  let replaced : bool ref = ref false in
-  let set_replaced () =
-    assert (not !replaced);
-    replaced := true
-  in
-  let obj =
-    object (self)
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
-          =
-        match av.V.value with
-        | V.ALoan lc ->
-            let value = self#visit_typed_ALoan opt_abs av.V.ty lc in
-            ({ av with V.value } : V.typed_avalue)
-        | _ -> super#visit_typed_avalue opt_abs av
-      (** This is a bit annoying, but as we need the type of the avalue we
-          are exploring, in order to be able to project the value we give
-          back, we need to reimplement [visit_typed_avalue] instead of
-          [visit_ALoan] *)
-
-      method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
-          (lc : V.aloan_content) : V.avalue =
-        match lc with
-        | V.AMutLoan (bid', child) ->
-            if bid' = bid then (
-              (* This is the loan we are looking for: apply the projection to
-               * the value we give back and replaced this mutable loan with
-               * an ended loan *)
-              (* Register the insertion *)
-              set_replaced ();
-              (* Sanity check *)
-              assert (nv.V.ty = ty);
-              (* Return the new value *)
-              V.ALoan (V.AEndedMutLoan { given_back = nv; child }))
-            else
-              (* Continue exploring *)
-              V.ALoan (super#visit_AMutLoan opt_abs bid' child)
-        | V.ASharedLoan (bids, v, av) ->
-            (* We are giving back a value to a *mutable* loan: nothing special to do *)
-            V.ALoan (super#visit_ASharedLoan opt_abs bids v av)
-        | V.AEndedMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
-        | V.AEndedSharedLoan (v, av) ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
-        | V.AIgnoredMutLoan (bid', child) ->
-            (* This loan is ignored, but we may have to project on a subvalue
-             * of the value which is given back *)
-            if bid' = bid then (
-              (* Note that we replace the ignored mut loan by an *ended* ignored
-               * mut loan. Also, this is not the loan we are looking for *per se*:
-               * we don't register the fact that we inserted the value somewhere
-               * (i.e., we don't call [set_replaced]) *)
-              (* Sanity check *)
-              assert (nv.V.ty = ty);
-              V.ALoan (V.AEndedIgnoredMutLoan { given_back = nv; child }))
-            else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
-        | V.AIgnoredSharedLoan av ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
-      (** We are not specializing an already existing method, but adding a
-          new method (for projections, we need type information) *)
-    end
-  in
-
-  (* Explore the environment *)
-  let ctx = obj#visit_eval_ctx None ctx in
-  (* Check we gave back to exactly one loan *)
-  assert !replaced;
-  (* Return *)
-  ctx
-
-(** Auxiliary function to end borrows. See [give_back].
-    
-    When we end a shared borrow, we need to remove the borrow id from the list
-    of borrows to the shared value.
-
-    Note that this function checks that there is exactly one shared loan that
-    we update.
-    TODO: this was not the case before, so some sanity checks are not useful anymore.
- *)
-let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
-    C.eval_ctx =
-  (* We use a reference to check that we updated exactly one loan *)
-  let replaced : bool ref = ref false in
-  let set_replaced () =
-    assert (not !replaced);
-    replaced := true
-  in
-  let obj =
-    object
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_Loan opt_abs lc =
-        match lc with
-        | V.SharedLoan (bids, shared_value) ->
-            if V.BorrowId.Set.mem bid bids then (
-              (* This is the loan we are looking for *)
-              set_replaced ();
-              (* If there remains exactly one borrow identifier, we need
-               * to end the loan. Otherwise, we just remove the current
-               * loan identifier *)
-              if V.BorrowId.Set.cardinal bids = 1 then shared_value.V.value
-              else
-                V.Loan
-                  (V.SharedLoan (V.BorrowId.Set.remove bid bids, shared_value)))
-            else
-              (* Not the loan we are looking for: continue exploring *)
-              V.Loan (super#visit_SharedLoan opt_abs bids shared_value)
-        | V.MutLoan bid' ->
-            (* We are giving back a *shared* borrow: nothing special to do *)
-            V.Loan (super#visit_MutLoan opt_abs bid')
-
-      method! visit_ALoan opt_abs lc =
-        match lc with
-        | V.AMutLoan (bid, av) ->
-            (* Nothing special to do (we are giving back a *shared* borrow) *)
-            V.ALoan (super#visit_AMutLoan opt_abs bid av)
-        | V.ASharedLoan (bids, shared_value, child) ->
-            if V.BorrowId.Set.mem bid bids then (
-              (* This is the loan we are looking for *)
-              set_replaced ();
-              (* If there remains exactly one borrow identifier, we need
-               * to end the loan. Otherwise, we just remove the current
-               * loan identifier *)
-              if V.BorrowId.Set.cardinal bids = 1 then
-                V.ALoan (V.AEndedSharedLoan (shared_value, child))
-              else
-                V.ALoan
-                  (V.ASharedLoan
-                     (V.BorrowId.Set.remove bid bids, shared_value, child)))
-            else
-              (* Not the loan we are looking for: continue exploring *)
-              V.ALoan (super#visit_ASharedLoan opt_abs bids shared_value child)
-        | V.AEndedMutLoan { given_back; child } ->
-            (* Nothing special to do (the loan has ended) *)
-            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
-        | V.AEndedSharedLoan (v, av) ->
-            (* Nothing special to do (the loan has ended) *)
-            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
-        | V.AIgnoredMutLoan (bid, av) ->
-            (* Nothing special to do (we are giving back a *shared* borrow) *)
-            V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid av)
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
-        | V.AIgnoredSharedLoan av ->
-            (* Nothing special to do *)
-            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
-    end
-  in
-
-  (* Explore the environment *)
-  let ctx = obj#visit_eval_ctx None ctx in
-  (* Check we gave back to exactly one loan *)
-  assert !replaced;
-  (* Return *)
-  ctx
-
-(** When copying values, we duplicate the shared borrows. This is tantamount
-    to reborrowing the shared value. The following function applies this change
-    to an environment by inserting a new borrow id in the set of borrows tracked
-    by a shared value, referenced by the [original_bid] argument.
- *)
-let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Keep track of changes *)
-  let r = ref false in
-  let set_ref () =
-    assert (not !r);
-    r := true
-  in
-
-  let obj =
-    object
-      inherit [_] C.map_env as super
-
-      method! visit_SharedLoan env bids sv =
-        (* Shared loan: check if the borrow id we are looking for is in the
-           set of borrow ids. If yes, insert the new borrow id, otherwise
-           explore inside the shared value *)
-        if V.BorrowId.Set.mem original_bid bids then (
-          set_ref ();
-          let bids' = V.BorrowId.Set.add new_bid bids in
-          V.SharedLoan (bids', sv))
-        else super#visit_SharedLoan env bids sv
-
-      method! visit_ASharedLoan env bids v av =
-        (* This case is similar to the [SharedLoan] case *)
-        if V.BorrowId.Set.mem original_bid bids then (
-          set_ref ();
-          let bids' = V.BorrowId.Set.add new_bid bids in
-          V.ASharedLoan (bids', v, av))
-        else super#visit_ASharedLoan env bids v av
-    end
-  in
-
-  let env = obj#visit_env () ctx.env in
-  (* Check that we reborrowed once *)
-  assert !r;
-  { ctx with env }
-
-(** Auxiliary function: see [end_borrow_in_env] *)
-let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* 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 (l', tv)) ->
-      (* Sanity check *)
-      assert (l' = l);
-      (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
-      (* Update the context *)
-      give_back_value config l tv ctx
-  | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') ->
-      (* Sanity check *)
-      assert (l' = l);
-      (* Check that the borrow is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
-      (* Update the context *)
-      give_back_shared config l ctx
-  | Abstract (V.AMutBorrow (l', av)) ->
-      (* Sanity check *)
-      assert (l' = l);
-      (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
-      (* Update the context *)
-      give_back_avalue config l av ctx
-  | Abstract (V.ASharedBorrow l') ->
-      (* Sanity check *)
-      assert (l' = l);
-      (* Check that the borrow is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
-      (* Update the context *)
-      give_back_shared config l ctx
-  | Abstract (V.AProjSharedBorrow asb) ->
-      (* Sanity check *)
-      assert (borrow_in_asb l asb);
-      (* Update the context *)
-      give_back_shared config l ctx
-  | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable"
-
-(** Convert an [avalue] to a [value].
-
-    This function is used when ending abstractions: whenever we end a borrow
-    in an abstraction, we converted the borrowed [avalue] to a fresh symbolic
-    [value], then give back this [value] to the context.
- 
-    Note that some regions may have ended in the symbolic value we generate.
-    For instance, consider the following function signature:
-    ```
-    fn f<'a>(x : &'a mut &'a mut u32);
-    ```
-    When ending the abstraction, the value given back for the outer borrow
-    should be ⊥. In practice, we will give back a symbolic value which can't
-    be expanded (because expanding this symbolic value would require expanding
-    a reference whose region has already ended).
- *)
-let convert_avalue_to_value (av : V.typed_avalue) (ctx : C.eval_ctx) :
-    C.eval_ctx * V.typed_value =
-  (* Convert the type *)
-  let ty = Subst.erase_regions av.V.ty in
-  (* Generate the fresh a symbolic value *)
-  let ctx, sv_id = C.fresh_symbolic_value_id ctx in
-  let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in
-  let value : V.symbolic_proj_comp =
-    (* Note that the set of ended regions is empty: we shouldn't have to take
-     * into account any ended regions at this point, otherwise we would be in
-     * the first case where we should return ⊥ *)
-    { V.svalue; V.rset_ended = T.RegionId.Set.empty }
-  in
-  let value = V.Symbolic value in
-  (ctx, { V.value; V.ty })
-
-(** End a borrow identified by its borrow id in a context
-    
-    First lookup the borrow in the context and replace it with [Bottom].
-    Then, check that there is an associated loan in the context. When moving
-    values, before putting the value in its destination, we get an
-    intermediate state where some values are "outside" the context and thus
-    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] 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` performs
-    all tne necessary checks in case a borrow is inside an abstraction.
- *)
-let rec 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 =
-  match end_borrow_get_borrow io allowed_abs l ctx 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 -> (
-      (* 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);
-          (* Note that we might get there with `allowed_abs <> None`: we might
-           * be trying to end a borrow inside an abstraction, but which is actually
-           * inside another borrow *)
-          let allowed_abs' = None in
-          let ctx = end_borrows config io allowed_abs' bids ctx in
-          (* Retry to end the borrow *)
-          end_borrow config io allowed_abs l ctx
-      | OuterBorrows (Borrow bid) ->
-          (* See the comments for the previous case *)
-          assert (io = Outer);
-          let allowed_abs' = None in
-          let ctx = end_borrow config io allowed_abs' bid ctx in
-          (* Retry to end the borrow *)
-          end_borrow config io allowed_abs l ctx
-      | 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 *)
-          (* Note that we can lookup the loan anywhere *)
-          let ek =
-            {
-              enter_shared_loans = true;
-              enter_mut_borrows = true;
-              enter_abs = true;
-            }
-          in
-          match lookup_loan ek l ctx with
-          | AbsId loan_abs_id, _ ->
-              if loan_abs_id = abs_id then (
-                (* Same abstraction! We can end the borrow *)
-                let ctx = end_borrow config io (Some abs_id) l ctx in
-                (* Sanity check *)
-                assert (Option.is_none (lookup_borrow_opt ek l ctx));
-                ctx)
-              else
-                (* Not the same abstraction: we need to end the whole abstraction.
-                 * By doing that we should have ended the target borrow (see the
-                 * below sanity check) *)
-                let ctx = end_abstraction config abs_id ctx in
-                (* Sanity check: we ended the target borrow *)
-                assert (Option.is_none (lookup_borrow_opt ek l ctx));
-                ctx
-          | VarId _, _ ->
-              (* The loan is not inside the same abstraction (actually inside
-               * a non-abstraction value): we need to end the whole abstraction *)
-              let ctx = end_abstraction config abs_id ctx in
-              (* Sanity check: we ended the target borrow *)
-              assert (Option.is_none (lookup_borrow_opt ek l ctx));
-              ctx))
-  | Ok (ctx, 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);
-      ctx
-  (* We found a borrow: give the value back (i.e., update the corresponding loan) *)
-  | Ok (ctx, Some bc) -> give_back config l bc ctx
-
-and 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 =
-  V.BorrowId.Set.fold
-    (fun id ctx -> end_borrow config io allowed_abs id ctx)
-    lset ctx
-
-and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Lookup the abstraction *)
-  let abs = C.ctx_lookup_abs ctx abs_id in
-  (* End the parent abstractions first *)
-  let ctx = end_abstractions config abs.parents ctx in
-  (* End the loans inside the abstraction *)
-  let ctx = end_abstraction_loans config abs_id ctx in
-  (* End the abstraction itself by redistributing the borrows it contains *)
-  let ctx = end_abstraction_borrows config abs_id ctx in
-  (* End the regions owned by the abstraction *)
-  let ctx = end_abstraction_regions config abs_id ctx in
-  (* Remove all the references to the id of the current abstraction, and remove
-   * the abstraction itself *)
-  end_abstraction_remove_from_context config abs_id ctx
-
-and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  V.AbstractionId.Set.fold
-    (fun id ctx -> end_abstraction config id ctx)
-    abs_ids ctx
-
-and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Lookup the abstraction *)
-  let abs = C.ctx_lookup_abs ctx abs_id in
-  (* End the first loan we find *)
-  let obj =
-    object
-      inherit [_] V.iter_abs as super
-
-      method! visit_aloan_content env lc =
-        match lc with
-        | V.AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid))
-        | V.ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids))
-        | V.AEndedMutLoan { given_back; child } ->
-            super#visit_AEndedMutLoan env given_back child
-        | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av
-        | V.AIgnoredMutLoan (bid, av) ->
-            (* Note that this loan can't come from a parent abstraction, because
-             * we should have ended them already) *)
-            super#visit_AIgnoredMutLoan env bid av
-        | V.AEndedIgnoredMutLoan { given_back; child } ->
-            super#visit_AEndedIgnoredMutLoan env given_back child
-        | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av
-    end
-  in
-  try
-    (* Check if there are loans *)
-    obj#visit_abs () abs;
-    (* No loans: nothing to update *)
-    ctx
-  with (* There are loans: end them, then recheck *)
-  | FoundBorrowIds bids ->
-    let ctx =
-      match bids with
-      | Borrow bid -> end_outer_borrow config bid ctx
-      | Borrows bids -> end_outer_borrows config bids ctx
-    in
-    (* Recheck *)
-    end_abstraction_loans config abs_id ctx
-
-and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Note that the abstraction mustn't contain any loans *)
-  (* We end the borrows, starting with the *inner* ones. This is important
-     when considering nested borrows which have the same lifetime.
-
-     For instance:
-     ```
-     x -> mut_loan l1
-     px -> mut_loan l0
-     abs0 { a_mut_borrow l0 (a_mut_borrow l1 (U32 3)) }
-     ```
-
-     becomes (`U32 3` doesn't contain ⊥, so we give back a symbolic value):
-     ```
-     x -> @s0
-     px -> mut_loan l0
-     abs0 { a_mut_borrow l0 ⊥ }
-     ```
-
-     then (the borrowed value contains ⊥, we give back ⊥):
-     ```
-     x -> @s0
-     px -> ⊥
-     abs0 { ⊥ }
-     ```
-  *)
-  (* We explore in-depth and use exceptions. When exploring a borrow, if
-   * the exploration didn't trigger an exception, it means there are no
-   * inner borrows to end: we can thus trigger an exception for the current
-   * borrow. *)
-  let obj =
-    object
-      inherit [_] V.iter_abs as super
-
-      method! visit_aborrow_content env bc =
-        (* In-depth exploration *)
-        super#visit_aborrow_content env bc;
-        (* No exception was raise: we can raise an exception for the
-         * current borrow *)
-        match bc with
-        | V.AMutBorrow (_, _) | V.ASharedBorrow _ ->
-            (* Raise an exception *)
-            raise (FoundABorrowContent bc)
-        | V.AProjSharedBorrow asb ->
-            (* Raise an exception only if the asb contains borrows *)
-            if
-              List.exists
-                (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
-                asb
-            then raise (FoundABorrowContent bc)
-            else ()
-        | V.AIgnoredMutBorrow _ ->
-            (* Nothing to do for ignored borrows *)
-            ()
-    end
-  in
-  (* Lookup the abstraction *)
-  let abs = C.ctx_lookup_abs ctx abs_id in
-  try
-    (* Explore the abstraction, looking for borrows *)
-    obj#visit_abs () abs;
-    (* No borrows: nothing to update *)
-    ctx
-  with
-  (* There are borrows: end them, then reexplore *)
-  | FoundABorrowContent bc ->
-    (* First, replace the borrow by ⊥ *)
-    let bid =
-      match bc with
-      | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid
-      | V.AProjSharedBorrow asb -> (
-          (* There should be at least one borrow identifier in the set, which we
-           * can use to identify the whole set *)
-          match
-            List.find
-              (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
-              asb
-          with
-          | V.AsbBorrow bid -> bid
-          | _ -> failwith "Unexpected")
-      | V.AIgnoredMutBorrow _ -> failwith "Unexpected"
-    in
-    let ctx = update_aborrow ek_all bid V.ABottom ctx in
-    (* Then give back the value *)
-    let ctx =
-      match bc with
-      | V.AMutBorrow (bid, av) ->
-          (* First, convert the avalue to a (fresh symbolic) value *)
-          let ctx, v = convert_avalue_to_value av ctx in
-          give_back_value config bid v ctx
-      | V.ASharedBorrow bid -> give_back_shared config bid ctx
-      | V.AProjSharedBorrow _ ->
-          (* Nothing to do *)
-          ctx
-      | V.AIgnoredMutBorrow _ -> failwith "Unexpected"
-    in
-    (* Reexplore *)
-    end_abstraction_borrows config abs_id ctx
-
-(** Update the symbolic values in a context to register the regions in the
-    abstraction we are ending as already ended.
-    Note that this function also checks that no symbolic value in an abstraction
-    contains regions which we are ending.
-    Of course, we ignore the abstraction we are currently ending...
- *)
-and end_abstraction_regions (_config : C.config) (abs_id : V.AbstractionId.id)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Lookup the abstraction to retrieve the set of owned regions *)
-  let abs = C.ctx_lookup_abs ctx abs_id in
-  let ended_regions = abs.V.regions in
-  (* Update all the symbolic values in the context *)
-  let obj =
-    object
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_Symbolic _ sproj =
-        let sproj =
-          {
-            sproj with
-            V.rset_ended = T.RegionId.Set.union sproj.V.rset_ended ended_regions;
-          }
-        in
-        V.Symbolic sproj
-
-      method! visit_aproj (abs_regions : T.RegionId.set_t option) aproj =
-        (* Sanity check *)
-        (match aproj with
-        | V.AProjLoans _ -> ()
-        | V.AProjBorrows (sv, ty) -> (
-            match abs_regions with
-            | None -> failwith "Unexpected"
-            | Some abs_regions ->
-                assert (
-                  not
-                    (projections_intersect sv.V.sv_ty ended_regions ty
-                       abs_regions))));
-        (* Return - nothing to update *)
-        aproj
-
-      method! visit_abs (regions : T.RegionId.set_t option) abs =
-        if abs.V.abs_id = abs_id then abs
-        else (
-          assert (Option.is_none regions);
-          (* Check that we don't project over already ended regions *)
-          assert (T.RegionId.Set.disjoint ended_regions abs.V.regions);
-          (* Remember the set of regions owned by the abstraction *)
-          let regions = Some abs.V.regions in
-          super#visit_abs regions abs)
-      (** Whenever we dive in an abstraction, we need to keep track of the
-          set of regions owned by the abstraction.
-          Also: we don't dive in the abstraction we are currently ending... *)
-    end
-  in
-  (* Update the context *)
-  obj#visit_eval_ctx None ctx
-
-(** Remove an abstraction from the context, as well as all its references *)
-and end_abstraction_remove_from_context (_config : C.config)
-    (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx =
-  let map_env_elem (ev : C.env_elem) : C.env_elem option =
-    match ev with
-    | C.Var (_, _) | C.Frame -> Some ev
-    | C.Abs abs ->
-        if abs.abs_id = abs_id then None
-        else
-          let parents = V.AbstractionId.Set.remove abs_id abs.parents in
-          Some (C.Abs { abs with V.parents })
-  in
-  let env = List.filter_map map_env_elem ctx.C.env in
-  { ctx with C.env }
-
-and end_outer_borrow config = end_borrow config Outer None
-
-and end_outer_borrows config = end_borrows config Outer None
-
-and end_inner_borrow config = end_borrow config Inner None
-
-and end_inner_borrows config = end_borrows config Inner None
-
-(** Helper function: see [activate_inactivated_mut_borrow].
-
-    This function updates the shared loan to a mutable loan (we then update
-    the borrow with another helper). Of course, the shared loan must contain
-    exactly one borrow id (the one we give as parameter), otherwise we can't
-    promote it. Also, the shared value mustn't contain any loan.
-
-    The returned value (previously shared) is checked:
-    - it mustn't contain loans
-    - 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
- *)
-let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
-    C.eval_ctx * V.typed_value =
-  (* Lookup the shared loan *)
-  let ek =
-    { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
-  in
-  match lookup_loan ek l ctx with
-  | _, Concrete (V.MutLoan _) ->
-      failwith "Expected a shared loan, found a mut loan"
-  | _, 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:
-         we should have gotten rid of those already, but it is better
-         to do a sanity check. *)
-      assert (not (loans_in_value sv));
-      (* Check there isn't [Bottom] (this is actually an invariant *)
-      assert (not (bottom_in_value sv));
-      (* Check there aren't inactivated borrows *)
-      assert (not (inactivated_in_value sv));
-      (* Update the loan content *)
-      let ctx = update_loan ek l (V.MutLoan l) ctx in
-      (* Return *)
-      (ctx, sv)
-  | _, Abstract _ ->
-      (* I don't think it is possible to have two-phase borrows involving borrows
-       * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      failwith
-        "Can't promote a shared loan to a mutable loan if the loan is inside \
-         an abstraction"
-
-(** Helper function: see [activate_inactivated_mut_borrow].
-
-    This function updates a shared borrow to a mutable borrow.
- *)
-let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id)
-    (borrowed_value : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Lookup the inactivated borrow - note that we don't go inside borrows/loans:
-     there can't be inactivated borrows inside other borrows/loans
-  *)
-  let ek =
-    { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
-  in
-  match lookup_borrow ek l ctx with
-  | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) ->
-      failwith "Expected an inactivated mutable borrow"
-  | Concrete (V.InactivatedMutBorrow _) ->
-      (* Update it *)
-      update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx
-  | Abstract _ ->
-      (* This can't happen for sure *)
-      failwith
-        "Can't promote a shared borrow to a mutable borrow if the borrow is \
-         inside an abstraction"
-
-(** Promote an inactivated mut borrow to a mut borrow.
-
-    The borrow must point to a shared value which is borrowed exactly once.
- *)
-let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
-    (l : V.BorrowId.id) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Lookup the value *)
-  let ek =
-    { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
-  in
-  match lookup_loan ek l ctx with
-  | _, 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 *)
-      match get_first_loan_in_value sv with
-      | Some lc ->
-          (* End the loans *)
-          let ctx =
-            match lc with
-            | V.SharedLoan (bids, _) -> end_outer_borrows config bids ctx
-            | V.MutLoan bid -> end_outer_borrow config bid ctx
-          in
-          (* Recursive call *)
-          activate_inactivated_mut_borrow config io l ctx
-      | None ->
-          (* No loan to end inside the value *)
-          (* Some sanity checks *)
-          L.log#ldebug
-            (lazy
-              ("activate_inactivated_mut_borrow: resulting value:\n"
-             ^ V.show_typed_value sv));
-          assert (not (loans_in_value sv));
-          assert (not (bottom_in_value sv));
-          assert (not (inactivated_in_value sv));
-          (* 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 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 _ ->
-      (* I don't think it is possible to have two-phase borrows involving borrows
-       * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      failwith
-        "Can't activate an inactivated mutable borrow referencing a loan inside\n\
-        \         an abstraction"
-
 (** Paths *)
 
 (** When we fail reading from or writing to a path, it might be because we
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
new file mode 100644
index 00000000..e8503d57
--- /dev/null
+++ b/src/InterpreterBorrows.ml
@@ -0,0 +1,1115 @@
+module T = Types
+module V = Values
+open Scalars
+module E = Expressions
+open Errors
+module C = Contexts
+module Subst = Substitute
+module A = CfimAst
+module L = Logging
+open TypesUtils
+open ValuesUtils
+module Inv = Invariants
+module S = Synthesis
+open Utils
+open InterpreterUtils
+open InterpreterProjectors
+
+(** Auxiliary function to end borrows: lookup a borrow in the environment,
+    update it (by returning an updated environment where the borrow has been
+    replaced by [Bottom])) if we can end the borrow (for instance, it is not
+    an outer borrow...) or return the reason why we couldn't update the borrow.
+
+    [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 (io : inner_outer)
+    (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id)
+    (ctx : C.eval_ctx) :
+    (C.eval_ctx * 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 : 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 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 *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option)
+          lc =
+        match lc with
+        | 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 = 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 *)
+
+      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 or if we are inside an abstraction *)
+              raise_if_outer outer;
+              (* Register the update *)
+              set_replaced_bc (Concrete bc);
+              (* Update the value *)
+              V.Bottom)
+            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 or if we are inside an abstraction *)
+              raise_if_outer outer;
+              (* Register the update *)
+              set_replaced_bc (Concrete bc);
+              (* Update the value *)
+              V.Bottom)
+            else
+              (* Update the outer borrows before diving into the borrowed value *)
+              let outer = update_outer_borrows io outer (Borrow l') in
+              V.Borrow (super#visit_MutBorrow outer l' bv)
+
+      method! visit_ALoan outer lc =
+        (* Note that the children avalues are just other, independent loans,
+         * so we don't need to update the outer borrows when diving in.
+         * We keep track of the parents/children relationship only because we
+         * need it to properly instantiate the backward functions when generating
+         * the pure translation. *)
+        match lc with
+        | V.AMutLoan (bid, av) ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AMutLoan outer bid av)
+        | V.ASharedLoan (bids, v, av) ->
+            (* Explore the shared value - we need to update the outer borrows *)
+            let souter = update_outer_borrows io outer (Borrows bids) in
+            let v = super#visit_typed_value souter v in
+            (* Explore the child avalue - we keep the same outer borrows *)
+            let av = super#visit_typed_avalue outer av in
+            (* Reconstruct *)
+            V.ALoan (V.ASharedLoan (bids, v, av))
+        | V.AEndedMutLoan { given_back; child } ->
+            (* The loan has ended, so no need to update the outer borrows *)
+            V.ALoan (super#visit_AEndedMutLoan outer given_back child)
+        | V.AEndedSharedLoan (v, av) ->
+            (* The loan has ended, so no need to update the outer borrows *)
+            V.ALoan (super#visit_AEndedSharedLoan outer v av)
+        | V.AIgnoredMutLoan (bid, av) ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AIgnoredMutLoan outer bid av)
+        | V.AEndedIgnoredMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedIgnoredMutLoan outer given_back child)
+        | V.AIgnoredSharedLoan av ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AIgnoredSharedLoan outer av)
+      (** We reimplement [visit_ALoan] because we may have to update the
+          outer borrows *)
+
+      method! visit_ABorrow outer bc =
+        match bc with
+        | V.AMutBorrow (bid, av) ->
+            (* Check if this is the borrow we are looking for *)
+            if bid = l then (
+              (* When ending a mut borrow, there are two cases:
+               * - in the general case, we have to end the whole abstraction
+               *   (and thus raise an exception to signal that to the caller)
+               * - in some situations, the associated loan is inside the same
+               *   abstraction as the borrow. In this situation, we can end
+               *   the borrow without ending the whole abstraction, and we
+               *   simply move the child avalue around.
+               *)
+              (* Check there are outer borrows, or if we need to end the whole
+               * abstraction *)
+              raise_if_outer outer;
+              (* Register the update *)
+              set_replaced_bc (Abstract bc);
+              (* Update the value - note that we are necessarily in the second
+               * of the two cases described above *)
+              V.ABottom)
+            else
+              (* Update the outer borrows before diving into the child avalue *)
+              let outer = update_outer_borrows io outer (Borrow bid) in
+              V.ABorrow (super#visit_AMutBorrow outer bid av)
+        | V.ASharedBorrow bid ->
+            (* Check if this is the borrow we are looking for *)
+            if bid = l then (
+              (* Check there are outer borrows, or if we need to end the whole
+               * abstraction *)
+              raise_if_outer outer;
+              (* Register the update *)
+              set_replaced_bc (Abstract bc);
+              (* Update the value - note that we are necessarily in the second
+               * of the two cases described above *)
+              V.ABottom)
+            else V.ABorrow (super#visit_ASharedBorrow outer bid)
+        | V.AIgnoredMutBorrow av ->
+            (* Nothing special to do *)
+            V.ABorrow (super#visit_AIgnoredMutBorrow outer av)
+        | V.AProjSharedBorrow asb ->
+            (* Check if the borrow we are looking for is in the asb *)
+            if borrow_in_asb l asb then (
+              (* Check there are outer borrows, or if we need to end the whole
+               * abstraction *)
+              raise_if_outer outer;
+              (* Register the update *)
+              set_replaced_bc (Abstract bc);
+              (* Update the value - note that we are necessarily in the second
+               * of the two cases described above *)
+              let asb = remove_borrow_from_asb l asb in
+              V.ABorrow (V.AProjSharedBorrow asb))
+            else
+              (* Nothing special to do *)
+              V.ABorrow (super#visit_AProjSharedBorrow outer asb)
+
+      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 ctx = obj#visit_eval_ctx (None, None) ctx in
+    Ok (ctx, !replaced_bc)
+  with FoundOuter outers -> Error outers
+
+(** Auxiliary function to end borrows. See [give_back].
+    
+    When we end a mutable borrow, we need to "give back" the value it contained
+    to its original owner by reinserting it at the proper position.
+
+    Note that this function checks that there is exactly one loan to which we
+    give the value back.
+    TODO: this was not the case before, so some sanity checks are not useful anymore.
+ *)
+let give_back_value (config : C.config) (bid : V.BorrowId.id)
+    (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* We use a reference to check that we updated exactly one loan *)
+  let replaced : bool ref = ref false in
+  let set_replaced () =
+    assert (not !replaced);
+    replaced := true
+  in
+  (* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
+  let check_symbolic_no_ended = true in
+  (* We sometimes need to reborrow values while giving a value back due: prepare that *)
+  let allow_reborrows = true in
+  let fresh_reborrow, apply_registered_reborrows =
+    prepare_reborrows config allow_reborrows ctx
+  in
+  (* The visitor to give back the values *)
+  let obj =
+    object (self)
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Loan opt_abs lc =
+        match lc with
+        | V.SharedLoan (bids, v) ->
+            (* We are giving back a value (i.e., the content of a *mutable*
+             * borrow): nothing special to do *)
+            V.Loan (super#visit_SharedLoan opt_abs bids v)
+        | V.MutLoan bid' ->
+            (* Check if this is the loan we are looking for *)
+            if bid' = bid then (
+              set_replaced ();
+              nv.V.value)
+            else V.Loan (super#visit_MutLoan opt_abs bid')
+
+      method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
+          =
+        match av.V.value with
+        | V.ALoan lc ->
+            let value = self#visit_typed_ALoan opt_abs av.V.ty lc in
+            ({ av with V.value } : V.typed_avalue)
+        | _ -> super#visit_typed_avalue opt_abs av
+      (** This is a bit annoying, but as we need the type of the avalue we
+          are exploring, in order to be able to project the value we give
+          back, we need to reimplement [visit_typed_avalue] instead of
+          [visit_ALoan] *)
+
+      method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
+          (lc : V.aloan_content) : V.avalue =
+        (* Preparing a bit *)
+        let regions =
+          match opt_abs with
+          | None -> failwith "Unreachable"
+          | Some abs -> abs.V.regions
+        in
+        match lc with
+        | V.AMutLoan (bid', child) ->
+            if bid' = bid then (
+              (* This is the loan we are looking for: apply the projection to
+               * the value we give back and replaced this mutable loan with
+               * an ended loan *)
+              (* Register the insertion *)
+              set_replaced ();
+              (* Apply the projection *)
+              let given_back =
+                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                  regions nv ty
+              in
+              (* Return the new value *)
+              V.ALoan (V.AEndedMutLoan { given_back; child }))
+            else
+              (* Continue exploring *)
+              V.ALoan (super#visit_AMutLoan opt_abs bid' child)
+        | V.ASharedLoan (bids, v, av) ->
+            (* We are giving back a value to a *mutable* loan: nothing special to do *)
+            V.ALoan (super#visit_ASharedLoan opt_abs bids v av)
+        | V.AEndedMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
+        | V.AEndedSharedLoan (v, av) ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
+        | V.AIgnoredMutLoan (bid', child) ->
+            (* This loan is ignored, but we may have to project on a subvalue
+             * of the value which is given back *)
+            if bid' = bid then
+              (* Note that we replace the ignored mut loan by an *ended* ignored
+               * mut loan. Also, this is not the loan we are looking for *per se*:
+               * we don't register the fact that we inserted the value somewhere
+               * (i.e., we don't call [set_replaced]) *)
+              let given_back =
+                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                  regions nv ty
+              in
+              V.ALoan (V.AEndedIgnoredMutLoan { given_back; child })
+            else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
+        | V.AEndedIgnoredMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
+        | V.AIgnoredSharedLoan av ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
+      (** We are not specializing an already existing method, but adding a
+          new method (for projections, we need type information) *)
+
+      method! visit_Abs opt_abs abs =
+        (* We remember in which abstraction we are before diving -
+         * this is necessary for projecting values: we need to know
+         * over which regions to project *)
+        assert (Option.is_none opt_abs);
+        super#visit_Abs (Some abs) abs
+    end
+  in
+
+  (* Explore the environment *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Check we gave back to exactly one loan *)
+  assert !replaced;
+  (* Apply the reborrows *)
+  apply_registered_reborrows ctx
+
+(** Auxiliary function to end borrows. See [give_back].
+
+    This function is similar to [give_back_value] but gives back an [avalue]
+    (coming from an abstraction).
+
+    It is used when ending a borrow inside an abstraction, when the corresponding
+    loan is inside the same abstraction (in which case we don't need to end the whole
+    abstraction).
+    
+    REMARK: this function can't be used to give back the values borrowed by
+    end abstraction when ending this abstraction. When doing this, we need
+    to convert the [avalue] to a [value] by introducing the proper symbolic values.
+ *)
+let give_back_avalue (_config : C.config) (bid : V.BorrowId.id)
+    (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* We use a reference to check that we updated exactly one loan *)
+  let replaced : bool ref = ref false in
+  let set_replaced () =
+    assert (not !replaced);
+    replaced := true
+  in
+  let obj =
+    object (self)
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
+          =
+        match av.V.value with
+        | V.ALoan lc ->
+            let value = self#visit_typed_ALoan opt_abs av.V.ty lc in
+            ({ av with V.value } : V.typed_avalue)
+        | _ -> super#visit_typed_avalue opt_abs av
+      (** This is a bit annoying, but as we need the type of the avalue we
+          are exploring, in order to be able to project the value we give
+          back, we need to reimplement [visit_typed_avalue] instead of
+          [visit_ALoan] *)
+
+      method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
+          (lc : V.aloan_content) : V.avalue =
+        match lc with
+        | V.AMutLoan (bid', child) ->
+            if bid' = bid then (
+              (* This is the loan we are looking for: apply the projection to
+               * the value we give back and replaced this mutable loan with
+               * an ended loan *)
+              (* Register the insertion *)
+              set_replaced ();
+              (* Sanity check *)
+              assert (nv.V.ty = ty);
+              (* Return the new value *)
+              V.ALoan (V.AEndedMutLoan { given_back = nv; child }))
+            else
+              (* Continue exploring *)
+              V.ALoan (super#visit_AMutLoan opt_abs bid' child)
+        | V.ASharedLoan (bids, v, av) ->
+            (* We are giving back a value to a *mutable* loan: nothing special to do *)
+            V.ALoan (super#visit_ASharedLoan opt_abs bids v av)
+        | V.AEndedMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
+        | V.AEndedSharedLoan (v, av) ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
+        | V.AIgnoredMutLoan (bid', child) ->
+            (* This loan is ignored, but we may have to project on a subvalue
+             * of the value which is given back *)
+            if bid' = bid then (
+              (* Note that we replace the ignored mut loan by an *ended* ignored
+               * mut loan. Also, this is not the loan we are looking for *per se*:
+               * we don't register the fact that we inserted the value somewhere
+               * (i.e., we don't call [set_replaced]) *)
+              (* Sanity check *)
+              assert (nv.V.ty = ty);
+              V.ALoan (V.AEndedIgnoredMutLoan { given_back = nv; child }))
+            else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
+        | V.AEndedIgnoredMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
+        | V.AIgnoredSharedLoan av ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
+      (** We are not specializing an already existing method, but adding a
+          new method (for projections, we need type information) *)
+    end
+  in
+
+  (* Explore the environment *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Check we gave back to exactly one loan *)
+  assert !replaced;
+  (* Return *)
+  ctx
+
+(** Auxiliary function to end borrows. See [give_back].
+    
+    When we end a shared borrow, we need to remove the borrow id from the list
+    of borrows to the shared value.
+
+    Note that this function checks that there is exactly one shared loan that
+    we update.
+    TODO: this was not the case before, so some sanity checks are not useful anymore.
+ *)
+let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  (* We use a reference to check that we updated exactly one loan *)
+  let replaced : bool ref = ref false in
+  let set_replaced () =
+    assert (not !replaced);
+    replaced := true
+  in
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Loan opt_abs lc =
+        match lc with
+        | V.SharedLoan (bids, shared_value) ->
+            if V.BorrowId.Set.mem bid bids then (
+              (* This is the loan we are looking for *)
+              set_replaced ();
+              (* If there remains exactly one borrow identifier, we need
+               * to end the loan. Otherwise, we just remove the current
+               * loan identifier *)
+              if V.BorrowId.Set.cardinal bids = 1 then shared_value.V.value
+              else
+                V.Loan
+                  (V.SharedLoan (V.BorrowId.Set.remove bid bids, shared_value)))
+            else
+              (* Not the loan we are looking for: continue exploring *)
+              V.Loan (super#visit_SharedLoan opt_abs bids shared_value)
+        | V.MutLoan bid' ->
+            (* We are giving back a *shared* borrow: nothing special to do *)
+            V.Loan (super#visit_MutLoan opt_abs bid')
+
+      method! visit_ALoan opt_abs lc =
+        match lc with
+        | V.AMutLoan (bid, av) ->
+            (* Nothing special to do (we are giving back a *shared* borrow) *)
+            V.ALoan (super#visit_AMutLoan opt_abs bid av)
+        | V.ASharedLoan (bids, shared_value, child) ->
+            if V.BorrowId.Set.mem bid bids then (
+              (* This is the loan we are looking for *)
+              set_replaced ();
+              (* If there remains exactly one borrow identifier, we need
+               * to end the loan. Otherwise, we just remove the current
+               * loan identifier *)
+              if V.BorrowId.Set.cardinal bids = 1 then
+                V.ALoan (V.AEndedSharedLoan (shared_value, child))
+              else
+                V.ALoan
+                  (V.ASharedLoan
+                     (V.BorrowId.Set.remove bid bids, shared_value, child)))
+            else
+              (* Not the loan we are looking for: continue exploring *)
+              V.ALoan (super#visit_ASharedLoan opt_abs bids shared_value child)
+        | V.AEndedMutLoan { given_back; child } ->
+            (* Nothing special to do (the loan has ended) *)
+            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
+        | V.AEndedSharedLoan (v, av) ->
+            (* Nothing special to do (the loan has ended) *)
+            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
+        | V.AIgnoredMutLoan (bid, av) ->
+            (* Nothing special to do (we are giving back a *shared* borrow) *)
+            V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid av)
+        | V.AEndedIgnoredMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
+        | V.AIgnoredSharedLoan av ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av)
+    end
+  in
+
+  (* Explore the environment *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Check we gave back to exactly one loan *)
+  assert !replaced;
+  (* Return *)
+  ctx
+
+(** When copying values, we duplicate the shared borrows. This is tantamount
+    to reborrowing the shared value. The following function applies this change
+    to an environment by inserting a new borrow id in the set of borrows tracked
+    by a shared value, referenced by the [original_bid] argument.
+ *)
+let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Keep track of changes *)
+  let r = ref false in
+  let set_ref () =
+    assert (not !r);
+    r := true
+  in
+
+  let obj =
+    object
+      inherit [_] C.map_env as super
+
+      method! visit_SharedLoan env bids sv =
+        (* Shared loan: check if the borrow id we are looking for is in the
+           set of borrow ids. If yes, insert the new borrow id, otherwise
+           explore inside the shared value *)
+        if V.BorrowId.Set.mem original_bid bids then (
+          set_ref ();
+          let bids' = V.BorrowId.Set.add new_bid bids in
+          V.SharedLoan (bids', sv))
+        else super#visit_SharedLoan env bids sv
+
+      method! visit_ASharedLoan env bids v av =
+        (* This case is similar to the [SharedLoan] case *)
+        if V.BorrowId.Set.mem original_bid bids then (
+          set_ref ();
+          let bids' = V.BorrowId.Set.add new_bid bids in
+          V.ASharedLoan (bids', v, av))
+        else super#visit_ASharedLoan env bids v av
+    end
+  in
+
+  let env = obj#visit_env () ctx.env in
+  (* Check that we reborrowed once *)
+  assert !r;
+  { ctx with env }
+
+(** Auxiliary function: see [end_borrow_in_env] *)
+let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* 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 (l', tv)) ->
+      (* Sanity check *)
+      assert (l' = l);
+      (* Check that the corresponding loan is somewhere - purely a sanity check *)
+      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Update the context *)
+      give_back_value config l tv ctx
+  | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') ->
+      (* Sanity check *)
+      assert (l' = l);
+      (* Check that the borrow is somewhere - purely a sanity check *)
+      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Update the context *)
+      give_back_shared config l ctx
+  | Abstract (V.AMutBorrow (l', av)) ->
+      (* Sanity check *)
+      assert (l' = l);
+      (* Check that the corresponding loan is somewhere - purely a sanity check *)
+      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Update the context *)
+      give_back_avalue config l av ctx
+  | Abstract (V.ASharedBorrow l') ->
+      (* Sanity check *)
+      assert (l' = l);
+      (* Check that the borrow is somewhere - purely a sanity check *)
+      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      (* Update the context *)
+      give_back_shared config l ctx
+  | Abstract (V.AProjSharedBorrow asb) ->
+      (* Sanity check *)
+      assert (borrow_in_asb l asb);
+      (* Update the context *)
+      give_back_shared config l ctx
+  | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable"
+
+(** Convert an [avalue] to a [value].
+
+    This function is used when ending abstractions: whenever we end a borrow
+    in an abstraction, we converted the borrowed [avalue] to a fresh symbolic
+    [value], then give back this [value] to the context.
+ 
+    Note that some regions may have ended in the symbolic value we generate.
+    For instance, consider the following function signature:
+    ```
+    fn f<'a>(x : &'a mut &'a mut u32);
+    ```
+    When ending the abstraction, the value given back for the outer borrow
+    should be ⊥. In practice, we will give back a symbolic value which can't
+    be expanded (because expanding this symbolic value would require expanding
+    a reference whose region has already ended).
+ *)
+let convert_avalue_to_value (av : V.typed_avalue) (ctx : C.eval_ctx) :
+    C.eval_ctx * V.typed_value =
+  (* Convert the type *)
+  let ty = Subst.erase_regions av.V.ty in
+  (* Generate the fresh a symbolic value *)
+  let ctx, sv_id = C.fresh_symbolic_value_id ctx in
+  let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in
+  let value : V.symbolic_proj_comp =
+    (* Note that the set of ended regions is empty: we shouldn't have to take
+     * into account any ended regions at this point, otherwise we would be in
+     * the first case where we should return ⊥ *)
+    { V.svalue; V.rset_ended = T.RegionId.Set.empty }
+  in
+  let value = V.Symbolic value in
+  (ctx, { V.value; V.ty })
+
+(** End a borrow identified by its borrow id in a context
+    
+    First lookup the borrow in the context and replace it with [Bottom].
+    Then, check that there is an associated loan in the context. When moving
+    values, before putting the value in its destination, we get an
+    intermediate state where some values are "outside" the context and thus
+    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] 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` performs
+    all tne necessary checks in case a borrow is inside an abstraction.
+ *)
+let rec 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 =
+  match end_borrow_get_borrow io allowed_abs l ctx 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 -> (
+      (* 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);
+          (* Note that we might get there with `allowed_abs <> None`: we might
+           * be trying to end a borrow inside an abstraction, but which is actually
+           * inside another borrow *)
+          let allowed_abs' = None in
+          let ctx = end_borrows config io allowed_abs' bids ctx in
+          (* Retry to end the borrow *)
+          end_borrow config io allowed_abs l ctx
+      | OuterBorrows (Borrow bid) ->
+          (* See the comments for the previous case *)
+          assert (io = Outer);
+          let allowed_abs' = None in
+          let ctx = end_borrow config io allowed_abs' bid ctx in
+          (* Retry to end the borrow *)
+          end_borrow config io allowed_abs l ctx
+      | 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 *)
+          (* Note that we can lookup the loan anywhere *)
+          let ek =
+            {
+              enter_shared_loans = true;
+              enter_mut_borrows = true;
+              enter_abs = true;
+            }
+          in
+          match lookup_loan ek l ctx with
+          | AbsId loan_abs_id, _ ->
+              if loan_abs_id = abs_id then (
+                (* Same abstraction! We can end the borrow *)
+                let ctx = end_borrow config io (Some abs_id) l ctx in
+                (* Sanity check *)
+                assert (Option.is_none (lookup_borrow_opt ek l ctx));
+                ctx)
+              else
+                (* Not the same abstraction: we need to end the whole abstraction.
+                 * By doing that we should have ended the target borrow (see the
+                 * below sanity check) *)
+                let ctx = end_abstraction config abs_id ctx in
+                (* Sanity check: we ended the target borrow *)
+                assert (Option.is_none (lookup_borrow_opt ek l ctx));
+                ctx
+          | VarId _, _ ->
+              (* The loan is not inside the same abstraction (actually inside
+               * a non-abstraction value): we need to end the whole abstraction *)
+              let ctx = end_abstraction config abs_id ctx in
+              (* Sanity check: we ended the target borrow *)
+              assert (Option.is_none (lookup_borrow_opt ek l ctx));
+              ctx))
+  | Ok (ctx, 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);
+      ctx
+  (* We found a borrow: give the value back (i.e., update the corresponding loan) *)
+  | Ok (ctx, Some bc) -> give_back config l bc ctx
+
+and 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 =
+  V.BorrowId.Set.fold
+    (fun id ctx -> end_borrow config io allowed_abs id ctx)
+    lset ctx
+
+and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Lookup the abstraction *)
+  let abs = C.ctx_lookup_abs ctx abs_id in
+  (* End the parent abstractions first *)
+  let ctx = end_abstractions config abs.parents ctx in
+  (* End the loans inside the abstraction *)
+  let ctx = end_abstraction_loans config abs_id ctx in
+  (* End the abstraction itself by redistributing the borrows it contains *)
+  let ctx = end_abstraction_borrows config abs_id ctx in
+  (* End the regions owned by the abstraction *)
+  let ctx = end_abstraction_regions config abs_id ctx in
+  (* Remove all the references to the id of the current abstraction, and remove
+   * the abstraction itself *)
+  end_abstraction_remove_from_context config abs_id ctx
+
+and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  V.AbstractionId.Set.fold
+    (fun id ctx -> end_abstraction config id ctx)
+    abs_ids ctx
+
+and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Lookup the abstraction *)
+  let abs = C.ctx_lookup_abs ctx abs_id in
+  (* End the first loan we find *)
+  let obj =
+    object
+      inherit [_] V.iter_abs as super
+
+      method! visit_aloan_content env lc =
+        match lc with
+        | V.AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid))
+        | V.ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids))
+        | V.AEndedMutLoan { given_back; child } ->
+            super#visit_AEndedMutLoan env given_back child
+        | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av
+        | V.AIgnoredMutLoan (bid, av) ->
+            (* Note that this loan can't come from a parent abstraction, because
+             * we should have ended them already) *)
+            super#visit_AIgnoredMutLoan env bid av
+        | V.AEndedIgnoredMutLoan { given_back; child } ->
+            super#visit_AEndedIgnoredMutLoan env given_back child
+        | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av
+    end
+  in
+  try
+    (* Check if there are loans *)
+    obj#visit_abs () abs;
+    (* No loans: nothing to update *)
+    ctx
+  with (* There are loans: end them, then recheck *)
+  | FoundBorrowIds bids ->
+    let ctx =
+      match bids with
+      | Borrow bid -> end_outer_borrow config bid ctx
+      | Borrows bids -> end_outer_borrows config bids ctx
+    in
+    (* Recheck *)
+    end_abstraction_loans config abs_id ctx
+
+and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Note that the abstraction mustn't contain any loans *)
+  (* We end the borrows, starting with the *inner* ones. This is important
+     when considering nested borrows which have the same lifetime.
+
+     For instance:
+     ```
+     x -> mut_loan l1
+     px -> mut_loan l0
+     abs0 { a_mut_borrow l0 (a_mut_borrow l1 (U32 3)) }
+     ```
+
+     becomes (`U32 3` doesn't contain ⊥, so we give back a symbolic value):
+     ```
+     x -> @s0
+     px -> mut_loan l0
+     abs0 { a_mut_borrow l0 ⊥ }
+     ```
+
+     then (the borrowed value contains ⊥, we give back ⊥):
+     ```
+     x -> @s0
+     px -> ⊥
+     abs0 { ⊥ }
+     ```
+  *)
+  (* We explore in-depth and use exceptions. When exploring a borrow, if
+   * the exploration didn't trigger an exception, it means there are no
+   * inner borrows to end: we can thus trigger an exception for the current
+   * borrow. *)
+  let obj =
+    object
+      inherit [_] V.iter_abs as super
+
+      method! visit_aborrow_content env bc =
+        (* In-depth exploration *)
+        super#visit_aborrow_content env bc;
+        (* No exception was raise: we can raise an exception for the
+         * current borrow *)
+        match bc with
+        | V.AMutBorrow (_, _) | V.ASharedBorrow _ ->
+            (* Raise an exception *)
+            raise (FoundABorrowContent bc)
+        | V.AProjSharedBorrow asb ->
+            (* Raise an exception only if the asb contains borrows *)
+            if
+              List.exists
+                (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
+                asb
+            then raise (FoundABorrowContent bc)
+            else ()
+        | V.AIgnoredMutBorrow _ ->
+            (* Nothing to do for ignored borrows *)
+            ()
+    end
+  in
+  (* Lookup the abstraction *)
+  let abs = C.ctx_lookup_abs ctx abs_id in
+  try
+    (* Explore the abstraction, looking for borrows *)
+    obj#visit_abs () abs;
+    (* No borrows: nothing to update *)
+    ctx
+  with
+  (* There are borrows: end them, then reexplore *)
+  | FoundABorrowContent bc ->
+    (* First, replace the borrow by ⊥ *)
+    let bid =
+      match bc with
+      | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid
+      | V.AProjSharedBorrow asb -> (
+          (* There should be at least one borrow identifier in the set, which we
+           * can use to identify the whole set *)
+          match
+            List.find
+              (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
+              asb
+          with
+          | V.AsbBorrow bid -> bid
+          | _ -> failwith "Unexpected")
+      | V.AIgnoredMutBorrow _ -> failwith "Unexpected"
+    in
+    let ctx = update_aborrow ek_all bid V.ABottom ctx in
+    (* Then give back the value *)
+    let ctx =
+      match bc with
+      | V.AMutBorrow (bid, av) ->
+          (* First, convert the avalue to a (fresh symbolic) value *)
+          let ctx, v = convert_avalue_to_value av ctx in
+          give_back_value config bid v ctx
+      | V.ASharedBorrow bid -> give_back_shared config bid ctx
+      | V.AProjSharedBorrow _ ->
+          (* Nothing to do *)
+          ctx
+      | V.AIgnoredMutBorrow _ -> failwith "Unexpected"
+    in
+    (* Reexplore *)
+    end_abstraction_borrows config abs_id ctx
+
+(** Update the symbolic values in a context to register the regions in the
+    abstraction we are ending as already ended.
+    Note that this function also checks that no symbolic value in an abstraction
+    contains regions which we are ending.
+    Of course, we ignore the abstraction we are currently ending...
+ *)
+and end_abstraction_regions (_config : C.config) (abs_id : V.AbstractionId.id)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Lookup the abstraction to retrieve the set of owned regions *)
+  let abs = C.ctx_lookup_abs ctx abs_id in
+  let ended_regions = abs.V.regions in
+  (* Update all the symbolic values in the context *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Symbolic _ sproj =
+        let sproj =
+          {
+            sproj with
+            V.rset_ended = T.RegionId.Set.union sproj.V.rset_ended ended_regions;
+          }
+        in
+        V.Symbolic sproj
+
+      method! visit_aproj (abs_regions : T.RegionId.set_t option) aproj =
+        (* Sanity check *)
+        (match aproj with
+        | V.AProjLoans _ -> ()
+        | V.AProjBorrows (sv, ty) -> (
+            match abs_regions with
+            | None -> failwith "Unexpected"
+            | Some abs_regions ->
+                assert (
+                  not
+                    (projections_intersect sv.V.sv_ty ended_regions ty
+                       abs_regions))));
+        (* Return - nothing to update *)
+        aproj
+
+      method! visit_abs (regions : T.RegionId.set_t option) abs =
+        if abs.V.abs_id = abs_id then abs
+        else (
+          assert (Option.is_none regions);
+          (* Check that we don't project over already ended regions *)
+          assert (T.RegionId.Set.disjoint ended_regions abs.V.regions);
+          (* Remember the set of regions owned by the abstraction *)
+          let regions = Some abs.V.regions in
+          super#visit_abs regions abs)
+      (** Whenever we dive in an abstraction, we need to keep track of the
+          set of regions owned by the abstraction.
+          Also: we don't dive in the abstraction we are currently ending... *)
+    end
+  in
+  (* Update the context *)
+  obj#visit_eval_ctx None ctx
+
+(** Remove an abstraction from the context, as well as all its references *)
+and end_abstraction_remove_from_context (_config : C.config)
+    (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx =
+  let map_env_elem (ev : C.env_elem) : C.env_elem option =
+    match ev with
+    | C.Var (_, _) | C.Frame -> Some ev
+    | C.Abs abs ->
+        if abs.abs_id = abs_id then None
+        else
+          let parents = V.AbstractionId.Set.remove abs_id abs.parents in
+          Some (C.Abs { abs with V.parents })
+  in
+  let env = List.filter_map map_env_elem ctx.C.env in
+  { ctx with C.env }
+
+and end_outer_borrow config = end_borrow config Outer None
+
+and end_outer_borrows config = end_borrows config Outer None
+
+and end_inner_borrow config = end_borrow config Inner None
+
+and end_inner_borrows config = end_borrows config Inner None
+
+(** Helper function: see [activate_inactivated_mut_borrow].
+
+    This function updates the shared loan to a mutable loan (we then update
+    the borrow with another helper). Of course, the shared loan must contain
+    exactly one borrow id (the one we give as parameter), otherwise we can't
+    promote it. Also, the shared value mustn't contain any loan.
+
+    The returned value (previously shared) is checked:
+    - it mustn't contain loans
+    - 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
+ *)
+let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
+    C.eval_ctx * V.typed_value =
+  (* Lookup the shared loan *)
+  let ek =
+    { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
+  in
+  match lookup_loan ek l ctx with
+  | _, Concrete (V.MutLoan _) ->
+      failwith "Expected a shared loan, found a mut loan"
+  | _, 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:
+         we should have gotten rid of those already, but it is better
+         to do a sanity check. *)
+      assert (not (loans_in_value sv));
+      (* Check there isn't [Bottom] (this is actually an invariant *)
+      assert (not (bottom_in_value sv));
+      (* Check there aren't inactivated borrows *)
+      assert (not (inactivated_in_value sv));
+      (* Update the loan content *)
+      let ctx = update_loan ek l (V.MutLoan l) ctx in
+      (* Return *)
+      (ctx, sv)
+  | _, Abstract _ ->
+      (* I don't think it is possible to have two-phase borrows involving borrows
+       * returned by abstractions. I'm not sure how we could handle that anyway. *)
+      failwith
+        "Can't promote a shared loan to a mutable loan if the loan is inside \
+         an abstraction"
+
+(** Helper function: see [activate_inactivated_mut_borrow].
+
+    This function updates a shared borrow to a mutable borrow.
+ *)
+let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id)
+    (borrowed_value : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Lookup the inactivated borrow - note that we don't go inside borrows/loans:
+     there can't be inactivated borrows inside other borrows/loans
+  *)
+  let ek =
+    { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
+  in
+  match lookup_borrow ek l ctx with
+  | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) ->
+      failwith "Expected an inactivated mutable borrow"
+  | Concrete (V.InactivatedMutBorrow _) ->
+      (* Update it *)
+      update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx
+  | Abstract _ ->
+      (* This can't happen for sure *)
+      failwith
+        "Can't promote a shared borrow to a mutable borrow if the borrow is \
+         inside an abstraction"
+
+(** Promote an inactivated mut borrow to a mut borrow.
+
+    The borrow must point to a shared value which is borrowed exactly once.
+ *)
+let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
+    (l : V.BorrowId.id) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Lookup the value *)
+  let ek =
+    { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
+  in
+  match lookup_loan ek l ctx with
+  | _, 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 *)
+      match get_first_loan_in_value sv with
+      | Some lc ->
+          (* End the loans *)
+          let ctx =
+            match lc with
+            | V.SharedLoan (bids, _) -> end_outer_borrows config bids ctx
+            | V.MutLoan bid -> end_outer_borrow config bid ctx
+          in
+          (* Recursive call *)
+          activate_inactivated_mut_borrow config io l ctx
+      | None ->
+          (* No loan to end inside the value *)
+          (* Some sanity checks *)
+          L.log#ldebug
+            (lazy
+              ("activate_inactivated_mut_borrow: resulting value:\n"
+             ^ V.show_typed_value sv));
+          assert (not (loans_in_value sv));
+          assert (not (bottom_in_value sv));
+          assert (not (inactivated_in_value sv));
+          (* 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 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 _ ->
+      (* I don't think it is possible to have two-phase borrows involving borrows
+       * returned by abstractions. I'm not sure how we could handle that anyway. *)
+      failwith
+        "Can't activate an inactivated mutable borrow referencing a loan inside\n\
+        \         an abstraction"