Move some functions from Interpreter to InterpreterProjectors

3 files changed, 667 insertions, 635 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index a3f22660..afe513be 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -10,9 +10,10 @@ module L = Logging
 open TypesUtils
 open ValuesUtils
 module Inv = Invariants
-open InterpreterUtils
 module S = Synthesis
 open Utils
+open InterpreterUtils
+open InterpreterProjectors
 
 (* TODO: check that the value types are correct when evaluating *)
 (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
@@ -34,450 +35,6 @@ type eval_error = Panic
 
 type 'a eval_result = ('a, eval_error) result
 
-(** The following type identifies the relative position of expressions (in
-    particular borrows) in other expressions.
-    
-    For instance, it is used to control [end_borrow]: we usually only allow
-    to end "outer" borrows, unless we perform a drop.
-*)
-type inner_outer = Inner | Outer
-
-type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id
-
-exception FoundBorrowIds of borrow_ids
-
-let update_if_none opt x = match opt with None -> Some x | _ -> opt
-
-(** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *)
-let update_outer_borrows (io : inner_outer)
-    (outer : V.AbstractionId.id option * borrow_ids option) (x : borrow_ids) :
-    V.AbstractionId.id option * borrow_ids option =
-  match io with
-  | Inner ->
-      (* If we can end inner borrows, we don't keep track of the outer borrows *)
-      outer
-  | Outer ->
-      let abs, opt = outer in
-      (abs, update_if_none opt x)
-
-(** Return the first loan we find in a value *)
-let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
-  let obj =
-    object
-      inherit [_] V.iter_typed_value
-
-      method! visit_loan_content _ lc = raise (FoundLoanContent lc)
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    None
-  with FoundLoanContent lc -> Some lc
-
-(** Check if two different projections intersect. This is necessary when
-    giving a symbolic value to an abstraction: we need to check that
-    the regions which are already ended inside the abstraction don't
-    intersect the regions over which we project in the new abstraction.
-    Note that the two abstractions have different views (in terms of regions)
-    of the symbolic value (hence the two region types).
-*)
-let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t)
-    (ty2 : T.rty) (rset2 : T.RegionId.set_t) : bool =
-  match (ty1, ty2) with
-  | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false
-  | T.Integer int_ty1, T.Integer int_ty2 ->
-      assert (int_ty1 = int_ty2);
-      false
-  | T.Adt (id1, regions1, tys1), T.Adt (id2, regions2, tys2) ->
-      assert (id1 = id2);
-      (* The intersection check for the ADTs is very crude: 
-       * we check if some arguments intersect. As all the type and region
-       * parameters should be used somewhere in the ADT (otherwise rustc
-       * generates an error), it means that it should be equivalent to checking
-       * whether two fields intersect (and anyway comparing the field types is
-       * difficult in case of enumerations...).
-       * If we didn't have the above property enforced by the rust compiler,
-       * this check would still be a reasonable conservative approximation. *)
-      let regions = List.combine regions1 regions2 in
-      let tys = List.combine tys1 tys2 in
-      List.exists
-        (fun (r1, r2) -> region_in_set r1 rset1 && region_in_set r2 rset2)
-        regions
-      || List.exists
-           (fun (ty1, ty2) -> projections_intersect ty1 rset1 ty2 rset2)
-           tys
-  | T.Array ty1, T.Array ty2 | T.Slice ty1, T.Slice ty2 ->
-      projections_intersect ty1 rset1 ty2 rset2
-  | T.Ref (r1, ty1, kind1), T.Ref (r2, ty2, kind2) ->
-      (* Sanity check *)
-      assert (kind1 = kind2);
-      (* The projections intersect if the borrows intersect or their contents
-       * intersect *)
-      (region_in_set r1 rset1 && region_in_set r2 rset2)
-      || projections_intersect ty1 rset1 ty2 rset2
-  | _ -> failwith "Unreachable"
-
-(** Check if the ended regions of a comp projector over a symbolic value
-    intersect the regions listed in another projection *)
-let symbolic_proj_comp_ended_regions_intersect_proj (s : V.symbolic_proj_comp)
-    (ty : T.rty) (regions : T.RegionId.set_t) : bool =
-  projections_intersect s.V.svalue.V.sv_ty s.V.rset_ended ty regions
-
-(** Check that a symbolic value doesn't contain ended regions.
-
-    Note that we don't check that the set of ended regions is empty: we
-    check that the set of ended regions doesn't intersect the set of
-    regions used in the type (this is more general).
-*)
-let symbolic_proj_comp_ended_regions (s : V.symbolic_proj_comp) : bool =
-  let regions = rty_regions s.V.svalue.V.sv_ty in
-  not (T.RegionId.Set.disjoint regions s.rset_ended)
-
-(** Check if a [value] contains ⊥.
-
-    Note that this function is very general: it also checks wether
-    symbolic values contain already ended regions.
- *)
-let bottom_in_value (v : V.typed_value) : bool =
-  let obj =
-    object
-      inherit [_] V.iter_typed_value
-
-      method! visit_Bottom _ = raise Found
-
-      method! visit_symbolic_proj_comp _ s =
-        if symbolic_proj_comp_ended_regions s then raise Found else ()
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    false
-  with Found -> true
-
-(** Check if an [avalue] contains ⊥.
-
-    Note that this function is very general: it also checks wether
-    symbolic values contain already ended regions.
-    
-    TODO: remove?
-*)
-let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) :
-    bool =
-  let obj =
-    object
-      inherit [_] V.iter_typed_avalue
-
-      method! visit_Bottom _ = raise Found
-
-      method! visit_symbolic_proj_comp _ sv =
-        if symbolic_proj_comp_ended_regions sv then raise Found else ()
-
-      method! visit_aproj _ ap =
-        (* Nothing to do actually *)
-        match ap with
-        | V.AProjLoans _sv -> ()
-        | V.AProjBorrows (_sv, _rty) -> ()
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_avalue () v;
-    false
-  with Found -> true
-
-type outer_borrows_or_abs =
-  | OuterBorrows of borrow_ids
-  | OuterAbs of V.AbstractionId.id
-
-exception FoundOuter of outer_borrows_or_abs
-(** Utility exception *)
-
-(** Auxiliary function.
-
-    Apply a proj_borrows on a shared borrow.
-    In the case of shared borrows, we return [abstract_shared_borrows],
-    not avalues.
-*)
-let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
-    (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
-    (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
-    V.abstract_shared_borrows =
-  (* Sanity check - TODO: move this elsewhere (here we perform the check at every
-   * recursive call which is a bit overkill...) *)
-  let ety = Substitute.erase_regions ty in
-  assert (ety = v.V.ty);
-  (* Project *)
-  match (v.V.value, ty) with
-  | V.Concrete _, (T.Bool | T.Char | T.Integer _ | T.Str) -> []
-  | V.Adt adt, T.Adt (id, region_params, tys) ->
-      (* Retrieve the types of the fields *)
-      let field_types =
-        Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id
-          region_params tys
-      in
-      (* Project over the field values *)
-      let fields_types = List.combine adt.V.field_values field_types in
-      let proj_fields =
-        List.map
-          (fun (fv, fty) ->
-            apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions fv
-              fty)
-          fields_types
-      in
-      List.concat proj_fields
-  | V.Bottom, _ -> failwith "Unreachable"
-  | V.Borrow bc, T.Ref (r, ref_ty, kind) ->
-      (* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
-      let bid, asb =
-        (* Not in the set: dive *)
-        match (bc, kind) with
-        | V.MutBorrow (bid, bv), T.Mut ->
-            (* Apply the projection on the borrowed value *)
-            let asb =
-              apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions bv
-                ref_ty
-            in
-            (bid, asb)
-        | V.SharedBorrow bid, T.Shared ->
-            (* Lookup the shared value *)
-            let ek = ek_all in
-            let sv = lookup_loan ek bid ctx in
-            let asb =
-              match sv with
-              | _, Concrete (V.SharedLoan (_, sv))
-              | _, Abstract (V.ASharedLoan (_, sv, _)) ->
-                  apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions
-                    sv ref_ty
-              | _ -> failwith "Unexpected"
-            in
-            (bid, asb)
-        | V.InactivatedMutBorrow _, _ ->
-            failwith
-              "Can't apply a proj_borrow over an inactivated mutable borrow"
-        | _ -> failwith "Unreachable"
-      in
-      let asb =
-        (* Check if the region is in the set of projected regions (note that
-         * we never project over static regions) *)
-        if region_in_set r regions then
-          let bid' = fresh_reborrow bid in
-          V.AsbBorrow bid' :: asb
-        else asb
-      in
-      asb
-  | V.Loan _, _ -> failwith "Unreachable"
-  | V.Symbolic s, _ ->
-      assert (not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions));
-      [ V.AsbProjReborrows (s.V.svalue, ty) ]
-  | _ -> failwith "Unreachable"
-
-(** Apply (and reduce) a projector over borrows to a value.
-
-    - [regions]: the regions we project
-    - [v]: the value over which we project
-    - [ty]: the projection type (is used to map borrows to regions, or to
-      interpret the borrows as belonging to some regions...). Remember that
-      `v` doesn't contain region information.
-      For instance, if we have:
-      `v <: ty` where:
-      - `v = mut_borrow l ...`
-      - `ty = Ref (r, ...)`
-      then we interpret the borrow `l` as belonging to region `r`
-    
-    Also, when applying projections on shared values, we need to apply
-    reborrows. This is a bit annoying because, with the way we compute
-    the projection on borrows, we can't update the context immediately.
-    Instead, we remember the list of borrows we have to insert in the
-    context *afterwards*.
-
-    [check_symbolic_no_ended] controls whether we check or not whether
-    symbolic values don't contain already ended regions.
-    This check is activated when applying projectors upon calling a function
-    (because we need to check that function arguments don't contain ⊥),
-    but deactivated when expanding symbolic values:
-    ```
-    fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
-    
-    let p = f(&mut x, &mut y); // p -> @s0
-    assert(x == ...); // end 'a
-    let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
-    ```
-*)
-let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
-    (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
-    (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
-    V.typed_avalue =
-  (* Sanity check - TODO: move this elsewhere (here we perform the check at every
-   * recursive call which is a bit overkill...) *)
-  let ety = Substitute.erase_regions ty in
-  assert (ety = v.V.ty);
-  (* Match *)
-  let value : V.avalue =
-    match (v.V.value, ty) with
-    | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv
-    | V.Adt adt, T.Adt (id, region_params, tys) ->
-        (* Retrieve the types of the fields *)
-        let field_types =
-          Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id
-            region_params tys
-        in
-        (* Project over the field values *)
-        let fields_types = List.combine adt.V.field_values field_types in
-        let proj_fields =
-          List.map
-            (fun (fv, fty) ->
-              apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                regions fv fty)
-            fields_types
-        in
-        V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields }
-    | V.Bottom, _ -> failwith "Unreachable"
-    | V.Borrow bc, T.Ref (r, ref_ty, kind) ->
-        if
-          (* Check if the region is in the set of projected regions (note that
-           * we never project over static regions) *)
-          region_in_set r regions
-        then
-          (* In the set *)
-          let bc =
-            match (bc, kind) with
-            | V.MutBorrow (bid, bv), T.Mut ->
-                (* Apply the projection on the borrowed value *)
-                let bv =
-                  apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                    regions bv ref_ty
-                in
-                V.AMutBorrow (bid, bv)
-            | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid
-            | V.InactivatedMutBorrow _, _ ->
-                failwith
-                  "Can't apply a proj_borrow over an inactivated mutable borrow"
-            | _ -> failwith "Unreachable"
-          in
-          V.ABorrow bc
-        else
-          (* Not in the set: ignore *)
-          let bc =
-            match (bc, kind) with
-            | V.MutBorrow (_bid, bv), T.Mut ->
-                (* Apply the projection on the borrowed value *)
-                let bv =
-                  apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                    regions bv ref_ty
-                in
-                V.AIgnoredMutBorrow bv
-            | V.SharedBorrow bid, T.Shared ->
-                (* Lookup the shared value *)
-                let ek = ek_all in
-                let sv = lookup_loan ek bid ctx in
-                let asb =
-                  match sv with
-                  | _, Concrete (V.SharedLoan (_, sv))
-                  | _, Abstract (V.ASharedLoan (_, sv, _)) ->
-                      apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
-                        regions sv ref_ty
-                  | _ -> failwith "Unexpected"
-                in
-                V.AProjSharedBorrow asb
-            | V.InactivatedMutBorrow _, _ ->
-                failwith
-                  "Can't apply a proj_borrow over an inactivated mutable borrow"
-            | _ -> failwith "Unreachable"
-          in
-          V.ABorrow bc
-    | V.Loan _, _ -> failwith "Unreachable"
-    | V.Symbolic s, _ ->
-        (* Check that the symbolic value doesn't contain already ended regions,
-         * if necessary *)
-        if check_symbolic_no_ended then
-          assert (
-            not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions));
-        V.ASymbolic (V.AProjBorrows (s.V.svalue, ty))
-    | _ -> failwith "Unreachable"
-  in
-  { V.value; V.ty }
-
-(** Convert a symbolic expansion *which is not a borrow* to a value *)
-let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
-    (see : symbolic_expansion) : V.typed_value =
-  let ty = Subst.erase_regions sv.V.sv_ty in
-  let value =
-    match see with
-    | SeConcrete cv -> V.Concrete cv
-    | SeAdt (variant_id, field_values) ->
-        let field_values =
-          List.map mk_typed_value_from_proj_comp field_values
-        in
-        V.Adt { V.variant_id; V.field_values }
-    | SeMutRef (_, _) | SeSharedRef (_, _) ->
-        failwith "Unexpected symbolic reference expansion"
-  in
-  { V.value; V.ty }
-
-(** Convert a symbolic expansion to a value.
-
-    If the expansion is a mutable reference expansion, it converts it to a borrow.
-    This function is meant to be used when reducing projectors over borrows,
-    during a symbolic expansion.
-  *)
-let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
-    (see : symbolic_expansion) : V.typed_value =
-  match see with
-  | SeMutRef (bid, bv) ->
-      let ty = Subst.erase_regions sv.V.sv_ty in
-      let bv = mk_typed_value_from_proj_comp bv in
-      let value = V.Borrow (V.MutBorrow (bid, bv)) in
-      { V.value; ty }
-  | SeSharedRef (_, _) ->
-      failwith "Unexpected symbolic shared reference expansion"
-  | _ -> symbolic_expansion_non_borrow_to_value sv see
-
-(** Apply (and reduce) a projector over loans to a value.
-
-    TODO: detailed comments. See [apply_proj_borrows]
-*)
-let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
-    (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue =
-  (* Match *)
-  let (value, ty) : V.avalue * T.rty =
-    match (see, original_sv_ty) with
-    | SeConcrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) ->
-        (V.AConcrete cv, original_sv_ty)
-    | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) ->
-        (* Project over the field values *)
-        let field_values =
-          List.map mk_aproj_loans_from_proj_comp field_values
-        in
-        (V.AAdt { V.variant_id; field_values }, original_sv_ty)
-    | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) ->
-        (* Apply the projector to the borrowed value *)
-        let child_av = mk_aproj_loans_from_proj_comp spc in
-        (* Check if the region is in the set of projected regions (note that
-         * we never project over static regions) *)
-        if region_in_set r regions then
-          (* In the set: keep *)
-          (V.ALoan (V.AMutLoan (bid, child_av)), ref_ty)
-        else
-          (* Not in the set: ignore *)
-          (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty)
-    | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) ->
-        (* Apply the projector to the borrowed value *)
-        let child_av = mk_aproj_loans_from_proj_comp spc in
-        (* Check if the region is in the set of projected regions (note that
-         * we never project over static regions) *)
-        if region_in_set r regions then
-          (* In the set: keep *)
-          let shared_value = mk_typed_value_from_proj_comp spc in
-          (V.ALoan (V.ASharedLoan (bids, shared_value, child_av)), ref_ty)
-        else
-          (* Not in the set: ignore *)
-          (V.ALoan (V.AIgnoredSharedLoan child_av), ref_ty)
-    | _ -> failwith "Unreachable"
-  in
-  { V.value; V.ty }
-
 (** 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
@@ -672,196 +229,6 @@ let end_borrow_get_borrow (io : inner_outer)
     Ok (ctx, !replaced_bc)
   with FoundOuter outers -> Error outers
 
-(** Auxiliary function. See [give_back_value].
-
-    Apply reborrows to a context.
-
-    The [reborrows] input is a list of pairs (shared loan id, id to insert in the shared loan).
-*)
-let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* This is a bit brutal, but whenever we insert a reborrow, we remove
-   * it from the list. This allows us to check that all the reborrows were
-   * applied before returning.
-   * We might reimplement that in a more efficient manner by using maps. *)
-  let reborrows = ref reborrows in
-
-  (* Check if a value is a mutable borrow, and return its identifier if
-     it is the case *)
-  let get_borrow_in_mut_borrow (v : V.typed_value) : V.BorrowId.id option =
-    match v.V.value with
-    | V.Borrow lc -> (
-        match lc with
-        | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None
-        | V.MutBorrow (id, _) -> Some id)
-    | _ -> None
-  in
-
-  (* Add the proper reborrows to a set of borrow ids (for a shared loan) *)
-  let insert_reborrows bids =
-    (* Find the reborrows to apply *)
-    let insert, reborrows' =
-      List.partition (fun (bid, _) -> V.BorrowId.Set.mem bid bids) !reborrows
-    in
-    reborrows := reborrows';
-    let insert = List.map snd insert in
-    (* Insert the borrows *)
-    List.fold_left (fun bids bid -> V.BorrowId.Set.add bid bids) bids insert
-  in
-
-  (* Get the list of reborrows for a given borrow id *)
-  let get_reborrows_for_bid bid =
-    (* Find the reborrows to apply *)
-    let insert, reborrows' =
-      List.partition (fun (bid', _) -> bid' = bid) !reborrows
-    in
-    reborrows := reborrows';
-    List.map snd insert
-  in
-
-  let borrows_to_set bids =
-    List.fold_left
-      (fun bids bid -> V.BorrowId.Set.add bid bids)
-      V.BorrowId.Set.empty bids
-  in
-
-  (* Insert reborrows for a given borrow id into a given set of borrows *)
-  let insert_reborrows_for_bid bids bid =
-    (* Find the reborrows to apply *)
-    let insert = get_reborrows_for_bid bid in
-    (* Insert the borrows *)
-    List.fold_left (fun bids bid -> V.BorrowId.Set.add bid bids) bids insert
-  in
-
-  let obj =
-    object
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_typed_value env v =
-        match v.V.value with
-        | V.Borrow (V.MutBorrow (bid, bv)) ->
-            let insert = get_reborrows_for_bid bid in
-            let nbc = super#visit_MutBorrow env bid bv in
-            let nbc = { v with V.value = V.Borrow nbc } in
-            if insert = [] then (* No reborrows: do nothing special *)
-              nbc
-            else
-              (* There are reborrows: insert a shared loan *)
-              let insert = borrows_to_set insert in
-              let value = V.Loan (V.SharedLoan (insert, nbc)) in
-              let ty = v.V.ty in
-              { V.value; ty }
-        | _ -> super#visit_typed_value env v
-      (** We may need to reborrow mutable borrows. Note that this doesn't
-          happen for aborrows *)
-
-      method! visit_loan_content env lc =
-        match lc with
-        | V.SharedLoan (bids, sv) ->
-            (* Insert the reborrows *)
-            let bids = insert_reborrows bids in
-            (* Check if the contained value is a mutable borrow, in which
-             * case we might need to reborrow it by adding more borrow ids
-             * to the current set of borrows - by doing this small
-             * manipulation here, we accumulate the borrow ids in the same
-             * shared loan, right above the mutable borrow, and avoid
-             * stacking shared loans (note that doing this is not a problem
-             * from a soundness point of view, but it is a bit ugly...) *)
-            let bids =
-              match get_borrow_in_mut_borrow sv with
-              | None -> bids
-              | Some bid -> insert_reborrows_for_bid bids bid
-            in
-            (* Update and explore *)
-            super#visit_SharedLoan env bids sv
-        | V.MutLoan bid ->
-            (* Nothing special to do *)
-            super#visit_MutLoan env bid
-      (** We reimplement [visit_loan_content] (rather than one of the sub-
-          functions) on purpose: exhaustive matches are good for maintenance *)
-
-      method! visit_aloan_content env lc =
-        (* TODO: ashared_loan (amut_loan ) case *)
-        match lc with
-        | V.ASharedLoan (bids, v, av) ->
-            (* Insert the reborrows *)
-            let bids = insert_reborrows bids in
-            (* Update and explore *)
-            super#visit_ASharedLoan env bids v av
-        | V.AIgnoredSharedLoan _
-        | V.AMutLoan (_, _)
-        | V.AEndedMutLoan { given_back = _; child = _ }
-        | V.AEndedSharedLoan (_, _)
-        | V.AIgnoredMutLoan (_, _)
-        | V.AEndedIgnoredMutLoan { given_back = _; child = _ } ->
-            (* Nothing particular to do *)
-            super#visit_aloan_content env lc
-    end
-  in
-
-  (* Visit *)
-  let ctx = obj#visit_eval_ctx () ctx in
-  (* Check that there are no reborrows remaining *)
-  assert (!reborrows = []);
-  (* Return *)
-  ctx
-
-(** Auxiliary function to prepare reborrowing operations (used when
-    applying projectors).
-    
-    Returns two functions:
-    - a function to generate fresh re-borrow ids, and register the reborrows
-    - a function to apply the reborrows in a context
-    Those functions are of course stateful.
- *)
-let prepare_reborrows (config : C.config) (allow_reborrows : bool)
-    (ctx : C.eval_ctx) :
-    (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) =
-  let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
-  let borrow_counter = ref ctx.C.borrow_counter in
-  (* The function to generate and register fresh reborrows *)
-  let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id =
-    if allow_reborrows then (
-      let bid', cnt' = V.BorrowId.fresh !borrow_counter in
-      borrow_counter := cnt';
-      reborrows := (bid, bid') :: !reborrows;
-      bid')
-    else failwith "Unexpected reborrow"
-  in
-  (* The function to apply the reborrows in a context *)
-  let apply_registered_reborrows (ctx : C.eval_ctx) : C.eval_ctx =
-    match config.C.mode with
-    | C.ConcreteMode ->
-        (* Reborrows are introduced when applying projections in symbolic mode *)
-        assert (!borrow_counter = ctx.C.borrow_counter);
-        assert (!reborrows = []);
-        ctx
-    | C.SymbolicMode ->
-        (* Update the borrow counter *)
-        let ctx = { ctx with C.borrow_counter = !borrow_counter } in
-        (* Apply the reborrows *)
-        apply_reborrows !reborrows ctx
-  in
-  (fresh_reborrow, apply_registered_reborrows)
-
-let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx)
-    (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
-    C.eval_ctx * V.typed_avalue =
-  let check_symbolic_no_ended = true in
-  let allow_reborrows = true in
-  (* Prepare the reborrows *)
-  let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows ctx
-  in
-  (* Apply the projector *)
-  let av =
-    apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions v ty
-  in
-  (* Apply the reborrows *)
-  let ctx = apply_registered_reborrows ctx in
-  (* Return *)
-  (ctx, av)
-
 (** Auxiliary function to end borrows. See [give_back].
     
     When we end a mutable borrow, we need to "give back" the value it contained
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
new file mode 100644
index 00000000..9c99f8c9
--- /dev/null
+++ b/src/InterpreterProjectors.ml
@@ -0,0 +1,505 @@
+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
+
+(** Auxiliary function.
+
+    Apply a proj_borrows on a shared borrow.
+    In the case of shared borrows, we return [abstract_shared_borrows],
+    not avalues.
+*)
+let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
+    (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
+    (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
+    V.abstract_shared_borrows =
+  (* Sanity check - TODO: move this elsewhere (here we perform the check at every
+   * recursive call which is a bit overkill...) *)
+  let ety = Substitute.erase_regions ty in
+  assert (ety = v.V.ty);
+  (* Project *)
+  match (v.V.value, ty) with
+  | V.Concrete _, (T.Bool | T.Char | T.Integer _ | T.Str) -> []
+  | V.Adt adt, T.Adt (id, region_params, tys) ->
+      (* Retrieve the types of the fields *)
+      let field_types =
+        Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id
+          region_params tys
+      in
+      (* Project over the field values *)
+      let fields_types = List.combine adt.V.field_values field_types in
+      let proj_fields =
+        List.map
+          (fun (fv, fty) ->
+            apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions fv
+              fty)
+          fields_types
+      in
+      List.concat proj_fields
+  | V.Bottom, _ -> failwith "Unreachable"
+  | V.Borrow bc, T.Ref (r, ref_ty, kind) ->
+      (* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
+      let bid, asb =
+        (* Not in the set: dive *)
+        match (bc, kind) with
+        | V.MutBorrow (bid, bv), T.Mut ->
+            (* Apply the projection on the borrowed value *)
+            let asb =
+              apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions bv
+                ref_ty
+            in
+            (bid, asb)
+        | V.SharedBorrow bid, T.Shared ->
+            (* Lookup the shared value *)
+            let ek = ek_all in
+            let sv = lookup_loan ek bid ctx in
+            let asb =
+              match sv with
+              | _, Concrete (V.SharedLoan (_, sv))
+              | _, Abstract (V.ASharedLoan (_, sv, _)) ->
+                  apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions
+                    sv ref_ty
+              | _ -> failwith "Unexpected"
+            in
+            (bid, asb)
+        | V.InactivatedMutBorrow _, _ ->
+            failwith
+              "Can't apply a proj_borrow over an inactivated mutable borrow"
+        | _ -> failwith "Unreachable"
+      in
+      let asb =
+        (* Check if the region is in the set of projected regions (note that
+         * we never project over static regions) *)
+        if region_in_set r regions then
+          let bid' = fresh_reborrow bid in
+          V.AsbBorrow bid' :: asb
+        else asb
+      in
+      asb
+  | V.Loan _, _ -> failwith "Unreachable"
+  | V.Symbolic s, _ ->
+      assert (not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions));
+      [ V.AsbProjReborrows (s.V.svalue, ty) ]
+  | _ -> failwith "Unreachable"
+
+(** Apply (and reduce) a projector over borrows to a value.
+
+    - [regions]: the regions we project
+    - [v]: the value over which we project
+    - [ty]: the projection type (is used to map borrows to regions, or to
+      interpret the borrows as belonging to some regions...). Remember that
+      `v` doesn't contain region information.
+      For instance, if we have:
+      `v <: ty` where:
+      - `v = mut_borrow l ...`
+      - `ty = Ref (r, ...)`
+      then we interpret the borrow `l` as belonging to region `r`
+    
+    Also, when applying projections on shared values, we need to apply
+    reborrows. This is a bit annoying because, with the way we compute
+    the projection on borrows, we can't update the context immediately.
+    Instead, we remember the list of borrows we have to insert in the
+    context *afterwards*.
+
+    [check_symbolic_no_ended] controls whether we check or not whether
+    symbolic values don't contain already ended regions.
+    This check is activated when applying projectors upon calling a function
+    (because we need to check that function arguments don't contain ⊥),
+    but deactivated when expanding symbolic values:
+    ```
+    fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
+    
+    let p = f(&mut x, &mut y); // p -> @s0
+    assert(x == ...); // end 'a
+    let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
+    ```
+*)
+let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
+    (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
+    (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
+    V.typed_avalue =
+  (* Sanity check - TODO: move this elsewhere (here we perform the check at every
+   * recursive call which is a bit overkill...) *)
+  let ety = Substitute.erase_regions ty in
+  assert (ety = v.V.ty);
+  (* Match *)
+  let value : V.avalue =
+    match (v.V.value, ty) with
+    | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv
+    | V.Adt adt, T.Adt (id, region_params, tys) ->
+        (* Retrieve the types of the fields *)
+        let field_types =
+          Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id
+            region_params tys
+        in
+        (* Project over the field values *)
+        let fields_types = List.combine adt.V.field_values field_types in
+        let proj_fields =
+          List.map
+            (fun (fv, fty) ->
+              apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                regions fv fty)
+            fields_types
+        in
+        V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields }
+    | V.Bottom, _ -> failwith "Unreachable"
+    | V.Borrow bc, T.Ref (r, ref_ty, kind) ->
+        if
+          (* Check if the region is in the set of projected regions (note that
+           * we never project over static regions) *)
+          region_in_set r regions
+        then
+          (* In the set *)
+          let bc =
+            match (bc, kind) with
+            | V.MutBorrow (bid, bv), T.Mut ->
+                (* Apply the projection on the borrowed value *)
+                let bv =
+                  apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                    regions bv ref_ty
+                in
+                V.AMutBorrow (bid, bv)
+            | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid
+            | V.InactivatedMutBorrow _, _ ->
+                failwith
+                  "Can't apply a proj_borrow over an inactivated mutable borrow"
+            | _ -> failwith "Unreachable"
+          in
+          V.ABorrow bc
+        else
+          (* Not in the set: ignore *)
+          let bc =
+            match (bc, kind) with
+            | V.MutBorrow (_bid, bv), T.Mut ->
+                (* Apply the projection on the borrowed value *)
+                let bv =
+                  apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                    regions bv ref_ty
+                in
+                V.AIgnoredMutBorrow bv
+            | V.SharedBorrow bid, T.Shared ->
+                (* Lookup the shared value *)
+                let ek = ek_all in
+                let sv = lookup_loan ek bid ctx in
+                let asb =
+                  match sv with
+                  | _, Concrete (V.SharedLoan (_, sv))
+                  | _, Abstract (V.ASharedLoan (_, sv, _)) ->
+                      apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
+                        regions sv ref_ty
+                  | _ -> failwith "Unexpected"
+                in
+                V.AProjSharedBorrow asb
+            | V.InactivatedMutBorrow _, _ ->
+                failwith
+                  "Can't apply a proj_borrow over an inactivated mutable borrow"
+            | _ -> failwith "Unreachable"
+          in
+          V.ABorrow bc
+    | V.Loan _, _ -> failwith "Unreachable"
+    | V.Symbolic s, _ ->
+        (* Check that the symbolic value doesn't contain already ended regions,
+         * if necessary *)
+        if check_symbolic_no_ended then
+          assert (
+            not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions));
+        V.ASymbolic (V.AProjBorrows (s.V.svalue, ty))
+    | _ -> failwith "Unreachable"
+  in
+  { V.value; V.ty }
+
+(** Convert a symbolic expansion *which is not a borrow* to a value *)
+let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
+    (see : symbolic_expansion) : V.typed_value =
+  let ty = Subst.erase_regions sv.V.sv_ty in
+  let value =
+    match see with
+    | SeConcrete cv -> V.Concrete cv
+    | SeAdt (variant_id, field_values) ->
+        let field_values =
+          List.map mk_typed_value_from_proj_comp field_values
+        in
+        V.Adt { V.variant_id; V.field_values }
+    | SeMutRef (_, _) | SeSharedRef (_, _) ->
+        failwith "Unexpected symbolic reference expansion"
+  in
+  { V.value; V.ty }
+
+(** Convert a symbolic expansion to a value.
+
+    If the expansion is a mutable reference expansion, it converts it to a borrow.
+    This function is meant to be used when reducing projectors over borrows,
+    during a symbolic expansion.
+  *)
+let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
+    (see : symbolic_expansion) : V.typed_value =
+  match see with
+  | SeMutRef (bid, bv) ->
+      let ty = Subst.erase_regions sv.V.sv_ty in
+      let bv = mk_typed_value_from_proj_comp bv in
+      let value = V.Borrow (V.MutBorrow (bid, bv)) in
+      { V.value; ty }
+  | SeSharedRef (_, _) ->
+      failwith "Unexpected symbolic shared reference expansion"
+  | _ -> symbolic_expansion_non_borrow_to_value sv see
+
+(** Apply (and reduce) a projector over loans to a value.
+
+    TODO: detailed comments. See [apply_proj_borrows]
+*)
+let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t)
+    (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue =
+  (* Match *)
+  let (value, ty) : V.avalue * T.rty =
+    match (see, original_sv_ty) with
+    | SeConcrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) ->
+        (V.AConcrete cv, original_sv_ty)
+    | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) ->
+        (* Project over the field values *)
+        let field_values =
+          List.map mk_aproj_loans_from_proj_comp field_values
+        in
+        (V.AAdt { V.variant_id; field_values }, original_sv_ty)
+    | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) ->
+        (* Apply the projector to the borrowed value *)
+        let child_av = mk_aproj_loans_from_proj_comp spc in
+        (* Check if the region is in the set of projected regions (note that
+         * we never project over static regions) *)
+        if region_in_set r regions then
+          (* In the set: keep *)
+          (V.ALoan (V.AMutLoan (bid, child_av)), ref_ty)
+        else
+          (* Not in the set: ignore *)
+          (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty)
+    | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) ->
+        (* Apply the projector to the borrowed value *)
+        let child_av = mk_aproj_loans_from_proj_comp spc in
+        (* Check if the region is in the set of projected regions (note that
+         * we never project over static regions) *)
+        if region_in_set r regions then
+          (* In the set: keep *)
+          let shared_value = mk_typed_value_from_proj_comp spc in
+          (V.ALoan (V.ASharedLoan (bids, shared_value, child_av)), ref_ty)
+        else
+          (* Not in the set: ignore *)
+          (V.ALoan (V.AIgnoredSharedLoan child_av), ref_ty)
+    | _ -> failwith "Unreachable"
+  in
+  { V.value; V.ty }
+
+(** Auxiliary function. See [give_back_value].
+
+    Apply reborrows to a context.
+
+    The [reborrows] input is a list of pairs (shared loan id, id to insert
+    in the shared loan).
+    This function is used when applying projectors on shared borrows: when
+    doing so, we might need to reborrow subvalues from the shared value.
+    For instance:
+    ```
+    fn f<'a,'b,'c>(x : &'a 'b 'c u32)
+    ```
+    When introducing the abstractions for 'a, 'b and 'c, we apply a projector
+    on some value `shared_borrow l : &'a &'b &'c u32`.
+    In the 'a abstraction, this shared borrow gets projected. However, when
+    reducing the projectors for the 'b and 'c abstractions, we need to make
+    sure that the borrows living in regions 'b and 'c live as long as those
+    regions. This is done by looking up the shared value and applying reborrows
+    on the borrows we find there (note that those reborrows apply on shared
+    borrows - easy - and mutable borrows - in this case, we reborrow the whole
+    borrow: `mut_borrow ... ~~> shared_loan {...} (mut_borrow ...)`).
+*)
+let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* This is a bit brutal, but whenever we insert a reborrow, we remove
+   * it from the list. This allows us to check that all the reborrows were
+   * applied before returning.
+   * We might reimplement that in a more efficient manner by using maps. *)
+  let reborrows = ref reborrows in
+
+  (* Check if a value is a mutable borrow, and return its identifier if
+     it is the case *)
+  let get_borrow_in_mut_borrow (v : V.typed_value) : V.BorrowId.id option =
+    match v.V.value with
+    | V.Borrow lc -> (
+        match lc with
+        | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None
+        | V.MutBorrow (id, _) -> Some id)
+    | _ -> None
+  in
+
+  (* Add the proper reborrows to a set of borrow ids (for a shared loan) *)
+  let insert_reborrows bids =
+    (* Find the reborrows to apply *)
+    let insert, reborrows' =
+      List.partition (fun (bid, _) -> V.BorrowId.Set.mem bid bids) !reborrows
+    in
+    reborrows := reborrows';
+    let insert = List.map snd insert in
+    (* Insert the borrows *)
+    List.fold_left (fun bids bid -> V.BorrowId.Set.add bid bids) bids insert
+  in
+
+  (* Get the list of reborrows for a given borrow id *)
+  let get_reborrows_for_bid bid =
+    (* Find the reborrows to apply *)
+    let insert, reborrows' =
+      List.partition (fun (bid', _) -> bid' = bid) !reborrows
+    in
+    reborrows := reborrows';
+    List.map snd insert
+  in
+
+  let borrows_to_set bids =
+    List.fold_left
+      (fun bids bid -> V.BorrowId.Set.add bid bids)
+      V.BorrowId.Set.empty bids
+  in
+
+  (* Insert reborrows for a given borrow id into a given set of borrows *)
+  let insert_reborrows_for_bid bids bid =
+    (* Find the reborrows to apply *)
+    let insert = get_reborrows_for_bid bid in
+    (* Insert the borrows *)
+    List.fold_left (fun bids bid -> V.BorrowId.Set.add bid bids) bids insert
+  in
+
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_typed_value env v =
+        match v.V.value with
+        | V.Borrow (V.MutBorrow (bid, bv)) ->
+            let insert = get_reborrows_for_bid bid in
+            let nbc = super#visit_MutBorrow env bid bv in
+            let nbc = { v with V.value = V.Borrow nbc } in
+            if insert = [] then (* No reborrows: do nothing special *)
+              nbc
+            else
+              (* There are reborrows: insert a shared loan *)
+              let insert = borrows_to_set insert in
+              let value = V.Loan (V.SharedLoan (insert, nbc)) in
+              let ty = v.V.ty in
+              { V.value; ty }
+        | _ -> super#visit_typed_value env v
+      (** We may need to reborrow mutable borrows. Note that this doesn't
+          happen for aborrows *)
+
+      method! visit_loan_content env lc =
+        match lc with
+        | V.SharedLoan (bids, sv) ->
+            (* Insert the reborrows *)
+            let bids = insert_reborrows bids in
+            (* Check if the contained value is a mutable borrow, in which
+             * case we might need to reborrow it by adding more borrow ids
+             * to the current set of borrows - by doing this small
+             * manipulation here, we accumulate the borrow ids in the same
+             * shared loan, right above the mutable borrow, and avoid
+             * stacking shared loans (note that doing this is not a problem
+             * from a soundness point of view, but it is a bit ugly...) *)
+            let bids =
+              match get_borrow_in_mut_borrow sv with
+              | None -> bids
+              | Some bid -> insert_reborrows_for_bid bids bid
+            in
+            (* Update and explore *)
+            super#visit_SharedLoan env bids sv
+        | V.MutLoan bid ->
+            (* Nothing special to do *)
+            super#visit_MutLoan env bid
+      (** We reimplement [visit_loan_content] (rather than one of the sub-
+          functions) on purpose: exhaustive matches are good for maintenance *)
+
+      method! visit_aloan_content env lc =
+        (* TODO: ashared_loan (amut_loan ) case *)
+        match lc with
+        | V.ASharedLoan (bids, v, av) ->
+            (* Insert the reborrows *)
+            let bids = insert_reborrows bids in
+            (* Update and explore *)
+            super#visit_ASharedLoan env bids v av
+        | V.AIgnoredSharedLoan _
+        | V.AMutLoan (_, _)
+        | V.AEndedMutLoan { given_back = _; child = _ }
+        | V.AEndedSharedLoan (_, _)
+        | V.AIgnoredMutLoan (_, _)
+        | V.AEndedIgnoredMutLoan { given_back = _; child = _ } ->
+            (* Nothing particular to do *)
+            super#visit_aloan_content env lc
+    end
+  in
+
+  (* Visit *)
+  let ctx = obj#visit_eval_ctx () ctx in
+  (* Check that there are no reborrows remaining *)
+  assert (!reborrows = []);
+  (* Return *)
+  ctx
+
+(** Auxiliary function to prepare reborrowing operations (used when
+    applying projectors).
+    
+    Returns two functions:
+    - a function to generate fresh re-borrow ids, and register the reborrows
+    - a function to apply the reborrows in a context
+    Those functions are of course stateful.
+ *)
+let prepare_reborrows (config : C.config) (allow_reborrows : bool)
+    (ctx : C.eval_ctx) :
+    (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) =
+  let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
+  let borrow_counter = ref ctx.C.borrow_counter in
+  (* The function to generate and register fresh reborrows *)
+  let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id =
+    if allow_reborrows then (
+      let bid', cnt' = V.BorrowId.fresh !borrow_counter in
+      borrow_counter := cnt';
+      reborrows := (bid, bid') :: !reborrows;
+      bid')
+    else failwith "Unexpected reborrow"
+  in
+  (* The function to apply the reborrows in a context *)
+  let apply_registered_reborrows (ctx : C.eval_ctx) : C.eval_ctx =
+    match config.C.mode with
+    | C.ConcreteMode ->
+        (* Reborrows are introduced when applying projections in symbolic mode *)
+        assert (!borrow_counter = ctx.C.borrow_counter);
+        assert (!reborrows = []);
+        ctx
+    | C.SymbolicMode ->
+        (* Update the borrow counter *)
+        let ctx = { ctx with C.borrow_counter = !borrow_counter } in
+        (* Apply the reborrows *)
+        apply_reborrows !reborrows ctx
+  in
+  (fresh_reborrow, apply_registered_reborrows)
+
+let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx)
+    (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) :
+    C.eval_ctx * V.typed_avalue =
+  let check_symbolic_no_ended = true in
+  let allow_reborrows = true in
+  (* Prepare the reborrows *)
+  let fresh_reborrow, apply_registered_reborrows =
+    prepare_reborrows config allow_reborrows ctx
+  in
+  (* Apply the projector *)
+  let av =
+    apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions v ty
+  in
+  (* Apply the reborrows *)
+  let ctx = apply_registered_reborrows ctx in
+  (* Return *)
+  (ctx, av)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index edc8594c..c652a1d3 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -632,3 +632,163 @@ type symbolic_expansion =
   | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list)
   | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp
   | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp
+
+(** The following type identifies the relative position of expressions (in
+    particular borrows) in other expressions.
+    
+    For instance, it is used to control [end_borrow]: we usually only allow
+    to end "outer" borrows, unless we perform a drop.
+*)
+type inner_outer = Inner | Outer
+
+type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id
+
+exception FoundBorrowIds of borrow_ids
+
+let update_if_none opt x = match opt with None -> Some x | _ -> opt
+
+(** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *)
+let update_outer_borrows (io : inner_outer)
+    (outer : V.AbstractionId.id option * borrow_ids option) (x : borrow_ids) :
+    V.AbstractionId.id option * borrow_ids option =
+  match io with
+  | Inner ->
+      (* If we can end inner borrows, we don't keep track of the outer borrows *)
+      outer
+  | Outer ->
+      let abs, opt = outer in
+      (abs, update_if_none opt x)
+
+(** Return the first loan we find in a value *)
+let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
+  let obj =
+    object
+      inherit [_] V.iter_typed_value
+
+      method! visit_loan_content _ lc = raise (FoundLoanContent lc)
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    None
+  with FoundLoanContent lc -> Some lc
+
+(** Check if two different projections intersect. This is necessary when
+    giving a symbolic value to an abstraction: we need to check that
+    the regions which are already ended inside the abstraction don't
+    intersect the regions over which we project in the new abstraction.
+    Note that the two abstractions have different views (in terms of regions)
+    of the symbolic value (hence the two region types).
+*)
+let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t)
+    (ty2 : T.rty) (rset2 : T.RegionId.set_t) : bool =
+  match (ty1, ty2) with
+  | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false
+  | T.Integer int_ty1, T.Integer int_ty2 ->
+      assert (int_ty1 = int_ty2);
+      false
+  | T.Adt (id1, regions1, tys1), T.Adt (id2, regions2, tys2) ->
+      assert (id1 = id2);
+      (* The intersection check for the ADTs is very crude: 
+       * we check if some arguments intersect. As all the type and region
+       * parameters should be used somewhere in the ADT (otherwise rustc
+       * generates an error), it means that it should be equivalent to checking
+       * whether two fields intersect (and anyway comparing the field types is
+       * difficult in case of enumerations...).
+       * If we didn't have the above property enforced by the rust compiler,
+       * this check would still be a reasonable conservative approximation. *)
+      let regions = List.combine regions1 regions2 in
+      let tys = List.combine tys1 tys2 in
+      List.exists
+        (fun (r1, r2) -> region_in_set r1 rset1 && region_in_set r2 rset2)
+        regions
+      || List.exists
+           (fun (ty1, ty2) -> projections_intersect ty1 rset1 ty2 rset2)
+           tys
+  | T.Array ty1, T.Array ty2 | T.Slice ty1, T.Slice ty2 ->
+      projections_intersect ty1 rset1 ty2 rset2
+  | T.Ref (r1, ty1, kind1), T.Ref (r2, ty2, kind2) ->
+      (* Sanity check *)
+      assert (kind1 = kind2);
+      (* The projections intersect if the borrows intersect or their contents
+       * intersect *)
+      (region_in_set r1 rset1 && region_in_set r2 rset2)
+      || projections_intersect ty1 rset1 ty2 rset2
+  | _ -> failwith "Unreachable"
+
+(** Check if the ended regions of a comp projector over a symbolic value
+    intersect the regions listed in another projection *)
+let symbolic_proj_comp_ended_regions_intersect_proj (s : V.symbolic_proj_comp)
+    (ty : T.rty) (regions : T.RegionId.set_t) : bool =
+  projections_intersect s.V.svalue.V.sv_ty s.V.rset_ended ty regions
+
+(** Check that a symbolic value doesn't contain ended regions.
+
+    Note that we don't check that the set of ended regions is empty: we
+    check that the set of ended regions doesn't intersect the set of
+    regions used in the type (this is more general).
+*)
+let symbolic_proj_comp_ended_regions (s : V.symbolic_proj_comp) : bool =
+  let regions = rty_regions s.V.svalue.V.sv_ty in
+  not (T.RegionId.Set.disjoint regions s.rset_ended)
+
+(** Check if a [value] contains ⊥.
+
+    Note that this function is very general: it also checks wether
+    symbolic values contain already ended regions.
+ *)
+let bottom_in_value (v : V.typed_value) : bool =
+  let obj =
+    object
+      inherit [_] V.iter_typed_value
+
+      method! visit_Bottom _ = raise Found
+
+      method! visit_symbolic_proj_comp _ s =
+        if symbolic_proj_comp_ended_regions s then raise Found else ()
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true
+
+(** Check if an [avalue] contains ⊥.
+
+    Note that this function is very general: it also checks wether
+    symbolic values contain already ended regions.
+    
+    TODO: remove?
+*)
+let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) :
+    bool =
+  let obj =
+    object
+      inherit [_] V.iter_typed_avalue
+
+      method! visit_Bottom _ = raise Found
+
+      method! visit_symbolic_proj_comp _ sv =
+        if symbolic_proj_comp_ended_regions sv then raise Found else ()
+
+      method! visit_aproj _ ap =
+        (* Nothing to do actually *)
+        match ap with
+        | V.AProjLoans _sv -> ()
+        | V.AProjBorrows (_sv, _rty) -> ()
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_avalue () v;
+    false
+  with Found -> true
+
+type outer_borrows_or_abs =
+  | OuterBorrows of borrow_ids
+  | OuterAbs of V.AbstractionId.id
+
+exception FoundOuter of outer_borrows_or_abs
+(** Utility exception *)