Update AProjLoans and AEndedProjLoans to take a list of given back

values

7 files changed, 442 insertions, 167 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index c64b4b72..477cba9b 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -421,55 +421,37 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
   (* Apply the reborrows *)
   apply_registered_reborrows ctx
 
-(** Give back a symbolic value.
-
-    When we give back a symbolic value, we replace the symbolic value with
-    a new symbolic value if we found an intersecting projection over the
-    borrows of this symbolic value inside a different abstraction.
-    Otherwise, we give back the same symbolic value, to signify the fact that
-    it was left unchanged.
-  *)
+(** Give back a *modified* symbolic value. *)
 let give_back_symbolic_value (_config : C.config)
     (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value)
     (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Sanity checks *)
+  assert (sv.sv_id <> nsv.sv_id);
+  (match nsv.sv_kind with
+  | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
+  | V.FunCallRet | V.SynthInput -> failwith "Unrechable");
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = mk_typed_value_from_symbolic_value nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
-  let subst (_abs : V.abs) _abs_proj_ty =
+  let subst (_abs : V.abs) local_given_back =
     (* Compute the projection over the given back value *)
     let child_proj =
-      (* If it is the same symbolic value, it means it was left unchanged:
-       * we don't have to project it *)
-      if sv.sv_id = nsv.sv_id then None
-      else (
-        (* Not the same symbolic value: it was updated (because given to a
-         * function or returned) *)
-        (* For now, we can only have the following case *)
-        assert (nsv.sv_kind = V.SynthGivenBack);
-        match nsv.sv_kind with
-        | V.SynthGivenBack ->
-            (* The given back value comes from the return value of the function
-             * we are currently synthesizing (as it is given back, it means
-             * we ended one of the regions appearing in the signature: we are
-             * currently synthesizing one of the backward functions *)
-            (* As we don't allow borrow overwrites on returned value, we can
-             * (and MUST) forget the borrows *)
-            None
-        | V.FunCallGivenBack ->
-            (* The value was fed as input to a function, and was given back *)
-            (* For now, we don't allow borrow overwrites on returned values,
-             * meaning the given back value can't have borrows below mutable
-             * borrows. *)
-            let has_borrow_below_mut =
-              ty_has_borrow_under_mut ctx.type_context.type_infos nsv.sv_ty
-            in
-            assert (not has_borrow_below_mut);
-            (* We don't allow overwrites: we must thus not project over the
-             * given back value *)
-            None
-        | _ -> failwith "Unreachable")
+      match nsv.sv_kind with
+      | V.SynthRetGivenBack ->
+          (* The given back value comes from the return value of the function
+           * we are currently synthesizing (as it is given back, it means
+           * we ended one of the regions appearing in the signature: we are
+           * currently synthesizing one of the backward functions).
+           * 
+           * As we don't allow borrow overwrites on returned value, we can
+           * (and MUST) forget the borrows *)
+          V.AIgnoredProjBorrows
+      | V.FunCallGivenBack ->
+          (* The value was fed as input to a function, and was given back *)
+          V.AProjBorrows (nsv, sv.V.sv_ty)
+      | _ -> failwith "Unreachable"
     in
-    V.AEndedProjLoans (mv, child_proj)
+    V.AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
   update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
 
@@ -1066,7 +1048,7 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
         | V.AProjBorrows (_, _)
         | V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
             ()
-        | V.AProjLoans sv -> raise (FoundSymbolicValue sv));
+        | V.AProjLoans (sv, _) -> raise (FoundSymbolicValue sv));
         super#visit_aproj env sproj
     end
   in
@@ -1078,20 +1060,24 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
   with
   (* There are loans: end them, then recheck *)
   | FoundBorrowIds bids ->
-      (* End the outer borrows *)
+      (* End the corresponding borrows *)
       let cc : cm_fun =
         match bids with
         | Borrow bid -> end_outer_borrow config bid
         | Borrows bids -> end_outer_borrows config bids
       in
-      (* Retry *)
+      (* Reexplore, looking for loans *)
       let cc = comp cc (end_abstraction_loans config chain abs_id) in
       (* Continue *)
       cc cf ctx
   | FoundSymbolicValue sv ->
       (* There is a proj_loans over a symbolic value: end the proj_borrows
-       * which intersect this proj_loans *)
-      end_proj_loans_symbolic config chain abs_id abs.regions sv cf ctx
+       * which intersect this proj_loans, then end the proj_loans itself *)
+      let cc = end_proj_loans_symbolic config chain abs_id abs.regions sv in
+      (* Reexplore, looking for loans *)
+      let cc = comp cc (end_abstraction_loans config chain abs_id) in
+      (* Continue *)
+      cc cf ctx
 
 and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
     (abs_id : V.AbstractionId.id) : cm_fun =
@@ -1208,10 +1194,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
       let ended_borrow =
         V.AEndedProjBorrows (mk_typed_value_from_symbolic_value nsv)
       in
-      let ctx =
-        update_intersecting_aproj_borrows_non_shared abs.regions sv ended_borrow
-          ctx
-      in
+      let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
         give_back_symbolic_value config abs.regions proj_ty sv nsv ctx
@@ -1255,77 +1238,127 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
     (abs_id : V.AbstractionId.id) (regions : T.RegionId.Set.t)
     (sv : V.symbolic_value) : cm_fun =
  fun cf ctx ->
+  (* Small helpers for sanity checks *)
+  let check ctx = no_aproj_over_symbolic_in_context sv ctx in
+  let cf_check (cf : m_fun) : m_fun =
+   fun ctx ->
+    check ctx;
+    cf ctx
+  in
   (* Find the first proj_borrows which intersects the proj_loans *)
   let explore_shared = true in
   match lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx with
   | None ->
       (* We couldn't find any in the context: it means that the symbolic value
        * is in the concrete environment (or that we dropped it, in which case
-       * it is completely absent) *)
-      (* Update the loans depending on the current symbolic value - it is
-       * left unchanged *)
-      let ctx = give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx in
+       * it is completely absent). We thus simply need to replace the loans
+       * projector with an ended projector. *)
+      let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+      (* Sanity check *)
+      check ctx;
       (* Continue *)
       cf ctx
   | Some (SharedProjs projs) ->
       (* We found projectors over shared values - split between the projectors
-           * which belong to the current *)
-      (* TODO: we might want to allow ending shared projectors/borrows in
-       * abstractions without ending the abstractions themselves, if we end
-       * those abstractions immediately after: some abstractions may be mutually
-       * dependent, which is ok when it is about shared values *)
+       * which belong to the current abstraction and the others.
+       * The context looks like this:
+       * ```
+       * abs'0 {
+       *   // The loan was initially like this:
+       *   // `shared_loan lids (s <: ...) [s]`
+       *   // but if we get there it means it was already ended:
+       *   ended_shared_loan (s <: ...) [s]
+       *   proj_shared_borrows [...; (s <: ...); ...]
+       *   proj_shared_borrows [...; (s <: ...); ...]
+       *   ...
+       * }
+       *
+       * abs'1 [
+       *   proj_shared_borrows [...; (s <: ...); ...]
+       *   ...
+       * }
+       *
+       * ...
+       *
+       * // No `s` outside of abstractions
+       * 
+       * ```
+       *)
       let _owned_projs, external_projs =
         List.partition (fun (abs_id', _) -> abs_id' = abs_id) projs
       in
-      if external_projs = [] then
-        (* There are external projs: end the corresponding abstractions *)
+      (* End the external borrow projectors (end their abstractions) *)
+      let cf_end_external : cm_fun =
+       fun cf ctx ->
         let abs_ids = List.map fst external_projs in
         let abs_ids =
           List.fold_left
             (fun s id -> V.AbstractionId.Set.add id s)
             V.AbstractionId.Set.empty abs_ids
         in
-        (* We could end the owned projections, but it is simpler to simply return
-         * and let the caller recheck if there are proj_loans to end *)
+        (* End the abstractions and continue *)
         end_abstractions config chain abs_ids cf ctx
-      else
+      in
+      (* End the internal borrows projectors and the loans projector *)
+      let cf_end_internal : cm_fun =
+       fun cf ctx ->
         (* All the proj_borrows are owned: simply erase them *)
         let ctx = remove_intersecting_aproj_borrows_shared regions sv ctx in
-        (* Remove the proj_loans - note that the symbolic value was left unchanged *)
-        let ctx =
-          give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx
-        in
+        (* End the loan itself *)
+        let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+        (* Sanity check *)
+        check ctx;
         (* Continue *)
         cf ctx
+      in
+      (* Compose and apply *)
+      let cc = comp cf_end_external cf_end_internal in
+      cc cf ctx
   | Some (NonSharedProj (abs_id', _proj_ty)) ->
-      (* We found one in the context: if it comes from this abstraction, we can
-       * end it directly, otherwise we need to end the abstraction where it
-       * came from first *)
-      if abs_id' = abs_id then
-        (* As the symbolic value was left unchanged, we give it back *)
-        let given_back_sv = sv in
-        (* Replace the proj_borrows *)
-        let given_back = mk_typed_value_from_symbolic_value given_back_sv in
-        let npb = V.AEndedProjBorrows given_back in
-        let ctx =
-          update_intersecting_aproj_borrows_non_shared regions sv npb ctx
-        in
-        (* Replace the proj_loans - note that the loaned (symbolic) value
-         * was left unchanged *)
-        let ctx =
-          give_back_symbolic_value config regions sv.V.sv_ty sv given_back_sv
-            ctx
-        in
+      (* We found one projector of borrows in an abstraction: if it comes
+       * from this abstraction, we can end it directly, otherwise we need
+       * to end the abstraction where it came from first *)
+      if abs_id' = abs_id then (
+        (* Note that it happens when a function returns a `&mut ...` which gets
+         * expanded to `mut_borrow l s`, and we end the borrow `l` (so `s` gets
+         * reinjected in the parent abstraction without having been modified).
+         *
+         * The context looks like this:
+         * ```
+         * abs'0 {
+         *   [s <: ...]
+         *   (s <: ...)
+         * }
+         *
+         * // Note that `s` can't appear in other abstractions or in the
+         * // regular environment (because we forbid the duplication of
+         * // symbolic values which contain borrows).
+         * ```
+         *)
+        (* End the projector of borrows - TODO: not completely sure what to
+         * replace it with... Maybe we should introduce an ABottomProj? *)
+        let ctx = update_aproj_borrows abs_id sv V.AIgnoredProjBorrows ctx in
+        (* Sanity check: no other occurrence of an intersecting projector of borrows *)
+        assert (
+          Option.is_none
+            (lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx));
+        (* End the projector of loans *)
+        let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+        (* Sanity check *)
+        check ctx;
         (* Continue *)
-        cf ctx
+        cf ctx)
       else
-        (* End the abstraction.
-         * Don't retry ending the current proj_loans after ending the abstraction:
-         * it may have been eliminated (if it is a proj over mutable value),
-         * or maybe not (if it is a proj over shared values): simply return,
-         * as the caller function will recheck if there are loans to end in the
-         * current abstraction *)
-        end_abstraction config chain abs_id' cf ctx
+        (* The borrows proj comes from a different abstraction: end it. *)
+        let cc = end_abstraction config chain abs_id' in
+        (* Retry ending the projector of loans *)
+        let cc =
+          comp cc (end_proj_loans_symbolic config chain abs_id regions sv)
+        in
+        (* Sanity check *)
+        let cc = comp cc cf_check in
+        (* Continue *)
+        cc cf ctx
 
 and end_outer_borrow config : V.BorrowId.id -> cm_fun =
   end_borrow config [] None
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 5f73fa3a..6e582e92 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -7,6 +7,7 @@ module V = Values
 module C = Contexts
 module Subst = Substitute
 module L = Logging
+open Utils
 open TypesUtils
 open InterpreterUtils
 
@@ -617,7 +618,7 @@ type looked_up_aproj_borrows =
     [lookup_shared]: if `true` also explore projectors over shared values,
     otherwise ignore.
     
-    This is a helper function: it might break invariants.
+    This is a helper function.
 *)
 let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
     (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
@@ -783,7 +784,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool)
 (** Simply calls [update_intersecting_aproj_borrows] to update a
     proj_borrows over a non-shared value.
     
-    We check that we update exactly one proj_borrows.
+    We check that we update *at least* one proj_borrows.
 
     This is a helper function: it might break invariants.
  *)
@@ -794,7 +795,7 @@ let update_intersecting_aproj_borrows_non_shared (regions : T.RegionId.Set.t)
   let update_shared _ _ = failwith "Unexpected" in
   let updated = ref false in
   let update_non_shared _ _ =
-    assert (not !updated);
+    (* We can update more than one borrow! *)
     updated := true;
     nv
   in
@@ -826,31 +827,42 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
 (** Updates the proj_loans intersecting some projection.
 
     This is a helper function: it might break invariants.
-
-    Note that in practice, when we update a proj_loans, we always update exactly
-    one aproj_loans, in a specific abstraction.
-    
-    We make this function more general, by checking projection intersections
-    (rather than simply checking the abstraction and symbolic value ids)
-    for sanity checking: we check whether we need to update a loan based
-    on intersection criteria, but also check at the same time that we update
-    *exactly one* projector.
     
-    Note that the new value [nv] with which to replace the proj_loans could
-    be untyped: we request a typed value for sanity checking.
+    Note that we can update more than one projector of loans! Consider the
+    following example:
+    ```
+    fn f<'a, 'b>(...) -> (&'a mut u32, &'b mut u32));
+    fn g<'c>(&'c mut u32, &'c mut u32);
+
+    let p = f(...);
+    g(move p);
+
+    // Symbolic context after the call to g:
+    // abs'a {'a} { [s@0 <: (&'a mut u32, &'b mut u32)] }
+    // abs'b {'b} { [s@0 <: (&'a mut u32, &'b mut u32)] }
+    //
+    // abs'c {'c} { (s@0 <: (&'c mut u32, &'c mut u32)) }
+    ```
     
-    [subst]: takes as parameters the abstraction and the projection type
-    where we perform the substitution.
+    Note that for sanity, this function checks that we update *at least* one
+    projector of loans.
+        
+    [subst]: takes as parameters the abstraction in which we perform the
+    substitution and the list of given back values at the projector of
+    loans where we perform the substitution (see the fields in [AProjLoans]).
+    Note that the symbolic value at this place is necessarily equal to [sv],
+    which is why we don't give it as parameters.
  *)
 let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
     (proj_ty : T.rty) (sv : V.symbolic_value)
-    (subst : V.abs -> T.rty -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
+    (subst : V.abs -> (V.typed_value * V.aproj) list -> V.aproj)
+    (ctx : C.eval_ctx) : C.eval_ctx =
   (* Small helpers for sanity checks *)
   let updated = ref false in
-  let update abs local_proj_ty : V.aproj =
-    assert (not !updated);
+  let update abs local_given_back : V.aproj =
+    (* Note that we can update more than once! *)
     updated := true;
-    subst abs local_proj_ty
+    subst abs local_given_back
   in
   (* The visitor *)
   let obj =
@@ -864,14 +876,14 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
         | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _
         | AIgnoredProjBorrows ->
             super#visit_aproj abs sproj
-        | AProjLoans sv' ->
+        | AProjLoans (sv', given_back) ->
             let abs = Option.get abs in
             if same_symbolic_id sv sv' then (
               assert (sv.sv_ty = sv'.sv_ty);
               if
                 projections_intersect proj_ty proj_regions sv'.V.sv_ty
                   abs.regions
-              then update abs sv'.V.sv_ty
+              then update abs given_back
               else super#visit_aproj (Some abs) sproj)
             else super#visit_aproj (Some abs) sproj
     end
@@ -882,3 +894,181 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
   assert !updated;
   (* Return *)
   ctx
+
+(** Helper function: lookup an [AProjLoans] by using an abstraction id and a
+    symbolic value.
+    
+    We return the information from the looked up projector of loans. See the
+    fields in [AProjLoans] (we don't return the symbolic value, because it
+    is equal to [sv]).
+    
+    Sanity check: we check that there is exactly one projector which corresponds
+    to the couple (abstraction id, symbolic value).
+ *)
+let lookup_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value)
+    (ctx : C.eval_ctx) : (V.mvalue * V.aproj) list =
+  (* Small helpers for sanity checks *)
+  let found = ref None in
+  let set_found x =
+    (* There is at most one projector which corresponds to the description *)
+    assert (Option.is_none !found);
+    found := Some x
+  in
+  (* The visitor *)
+  let obj =
+    object
+      inherit [_] C.iter_eval_ctx as super
+
+      method! visit_abs _ abs =
+        if abs.abs_id = abs_id then super#visit_abs (Some abs) abs else ()
+
+      method! visit_aproj (abs : V.abs option) sproj =
+        (match sproj with
+        | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _
+        | AIgnoredProjBorrows ->
+            super#visit_aproj abs sproj
+        | AProjLoans (sv', given_back) ->
+            let abs = Option.get abs in
+            assert (abs.abs_id = abs_id);
+            if sv'.sv_id = sv.sv_id then (
+              assert (sv' = sv);
+              set_found given_back)
+            else ());
+        super#visit_aproj abs sproj
+    end
+  in
+  (* Apply *)
+  obj#visit_eval_ctx None ctx;
+  (* Return *)
+  Option.get !found
+
+(** Helper function: might break invariants.
+
+    Update a projector over loans. The projector is identified by a symbolic
+    value and an abstraction id.
+
+    Sanity check: we check that there is exactly one projector which corresponds
+    to the couple (abstraction id, symbolic value).
+ *)
+let update_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value)
+    (nproj : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Small helpers for sanity checks *)
+  let found = ref false in
+  let update () =
+    (* We update at most once *)
+    assert (not !found);
+    found := true;
+    nproj
+  in
+  (* The visitor *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_abs _ abs =
+        if abs.abs_id = abs_id then super#visit_abs (Some abs) abs else abs
+
+      method! visit_aproj (abs : V.abs option) sproj =
+        match sproj with
+        | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _
+        | AIgnoredProjBorrows ->
+            super#visit_aproj abs sproj
+        | AProjLoans (sv', _) ->
+            let abs = Option.get abs in
+            assert (abs.abs_id = abs_id);
+            if sv'.sv_id = sv.sv_id then (
+              assert (sv' = sv);
+              update ())
+            else super#visit_aproj (Some abs) sproj
+    end
+  in
+  (* Apply *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Sanity check *)
+  assert !found;
+  (* Return *)
+  ctx
+
+(** Helper function: might break invariants.
+
+    Update a projector over borrows. The projector is identified by a symbolic
+    value and an abstraction id.
+
+    Sanity check: we check that there is exactly one projector which corresponds
+    to the couple (abstraction id, symbolic value).
+    
+    TODO: factorize with [update_aproj_loans]?
+ *)
+let update_aproj_borrows (abs_id : V.AbstractionId.id) (sv : V.symbolic_value)
+    (nproj : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Small helpers for sanity checks *)
+  let found = ref false in
+  let update () =
+    (* We update at most once *)
+    assert (not !found);
+    found := true;
+    nproj
+  in
+  (* The visitor *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_abs _ abs =
+        if abs.abs_id = abs_id then super#visit_abs (Some abs) abs else abs
+
+      method! visit_aproj (abs : V.abs option) sproj =
+        match sproj with
+        | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _
+        | AIgnoredProjBorrows ->
+            super#visit_aproj abs sproj
+        | AProjBorrows (sv', _proj_ty) ->
+            let abs = Option.get abs in
+            assert (abs.abs_id = abs_id);
+            if sv'.sv_id = sv.sv_id then (
+              assert (sv' = sv);
+              update ())
+            else super#visit_aproj (Some abs) sproj
+    end
+  in
+  (* Apply *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Sanity check *)
+  assert !found;
+  (* Return *)
+  ctx
+
+(** Helper function: might break invariants.
+
+    Converts an [AProjLoans] to an [AEndedProjLoans]. The projector is identified
+    by a symbolic value and an abstraction id.
+ *)
+let update_aproj_loans_to_ended (abs_id : V.AbstractionId.id)
+    (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Lookup the projector of loans *)
+  let given_back = lookup_aproj_loans abs_id sv ctx in
+  (* Create the new value for the projector *)
+  let nproj = V.AEndedProjLoans given_back in
+  (* Insert it *)
+  let ctx = update_aproj_loans abs_id sv nproj ctx in
+  (* Return *)
+  ctx
+
+let no_aproj_over_symbolic_in_context (sv : V.symbolic_value) (ctx : C.eval_ctx)
+    : unit =
+  (* The visitor *)
+  let obj =
+    object
+      inherit [_] C.iter_eval_ctx as super
+
+      method! visit_aproj env sproj =
+        (match sproj with
+        | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()
+        | AProjLoans (sv', _) | AProjBorrows (sv', _) ->
+            if sv'.sv_id = sv.sv_id then raise Found else ());
+        super#visit_aproj env sproj
+    end
+  in
+  (* Apply *)
+  try obj#visit_eval_ctx () ctx
+  with Found -> failwith "update_aproj_loans_to_ended: failed"
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index ce48b611..b2d952b1 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -74,7 +74,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
 
       method! visit_aproj current_abs aproj =
         (match aproj with
-        | AProjLoans sv | AProjBorrows (sv, _) ->
+        | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
             assert (not (same_symbolic_id sv original_sv))
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
@@ -91,22 +91,23 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
         (* Explore in depth first - we won't update anything: we simply
          * want to check we don't have to expand inner symbolic value *)
         match (aproj, proj_kind) with
-        | V.AEndedProjLoans (_, None), _ | V.AEndedProjBorrows _, _ ->
-            V.ASymbolic aproj
-        | V.AEndedProjLoans (_, Some child_proj), _ ->
-            (* Explore the child projection to make sure we don't have to expand
+        | V.AEndedProjBorrows _, _ -> V.ASymbolic aproj
+        | V.AEndedProjLoans _, _ ->
+            (* Explore the given back values to make sure we don't have to expand
              * anything in there *)
-            V.ASymbolic (self#visit_aproj (Some current_abs) child_proj)
-        | V.AProjLoans sv, LoanProj ->
+            V.ASymbolic (self#visit_aproj (Some current_abs) aproj)
+        | V.AProjLoans (sv, given_back), LoanProj ->
             (* Check if this is the symbolic value we are looking for *)
-            if same_symbolic_id sv original_sv then
+            if same_symbolic_id sv original_sv then (
+              (* There mustn't be any given back values *)
+              assert (given_back = []);
               (* Apply the projector *)
               let projected_value =
                 apply_proj_loans_on_symbolic_expansion proj_regions expansion
                   original_sv.V.sv_ty
               in
               (* Replace *)
-              projected_value.V.value
+              projected_value.V.value)
             else
               (* Not the searched symbolic value: nothing to do *)
               super#visit_ASymbolic (Some current_abs) aproj
@@ -328,7 +329,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
 
       method! visit_aproj proj_regions aproj =
         (match aproj with
-        | AProjLoans sv | AProjBorrows (sv, _) ->
+        | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
             assert (not (same_symbolic_id sv original_sv))
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
@@ -350,11 +351,10 @@ let expand_symbolic_value_shared_borrow (config : C.config)
             match reborrow_ashared (Option.get proj_regions) sv proj_ty with
             | None -> super#visit_ASymbolic proj_regions aproj
             | Some asb -> V.ABorrow (V.AProjSharedBorrow asb))
-        | AEndedProjLoans (_, None) -> V.ASymbolic aproj
-        | AEndedProjLoans (_, Some child_aproj) ->
-            (* Sanity check: make sure there is nothing to expand inside children
-             * projections *)
-            V.ASymbolic (self#visit_aproj proj_regions child_aproj)
+        | AEndedProjLoans _ ->
+            (* Sanity check: make sure there is nothing to expand inside the
+             * children projections *)
+            V.ASymbolic (self#visit_aproj proj_regions aproj)
     end
   in
   (* Call the visitor *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 761c2fbd..157ac68d 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -87,7 +87,7 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
 let mk_aproj_loans_value_from_symbolic_value (regions : T.RegionId.Set.t)
     (svalue : V.symbolic_value) : V.typed_avalue =
   if ty_has_regions_in_set regions svalue.sv_ty then
-    let av = V.ASymbolic (V.AProjLoans svalue) in
+    let av = V.ASymbolic (V.AProjLoans (svalue, [])) in
     let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in
     av
   else { V.value = V.AIgnored; ty = svalue.V.sv_ty }
@@ -169,7 +169,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
 
       method! visit_aproj env aproj =
         (match aproj with
-        | AProjLoans sv | AProjBorrows (sv, _) ->
+        | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
             if sv.V.sv_id = sv_id then raise Found else ()
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj env aproj
@@ -238,7 +238,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
               raise Found
             else ()
         | V.SynthInput -> ()
-        | V.FunCallGivenBack | V.SynthGivenBack -> failwith "Unreachable"
+        | V.FunCallGivenBack | V.SynthRetGivenBack -> failwith "Unreachable"
     end
   in
   (* We use exceptions *)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 52de4c5e..8582722d 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -595,21 +595,22 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.ASymbolic aproj, ty -> (
             let ty1 = Subst.erase_regions ty in
             match aproj with
-            | V.AProjLoans sv | V.AProjBorrows (sv, _) ->
+            | V.AProjLoans (sv, _) | V.AProjBorrows (sv, _) ->
                 let ty2 = Subst.erase_regions sv.V.sv_ty in
                 assert (ty1 = ty2);
                 (* Also check that the symbolic values contain regions of interest -
                  * otherwise they should have been reduced to `_` *)
                 let abs = Option.get info in
                 assert (ty_has_regions_in_set abs.regions sv.V.sv_ty)
-            | V.AEndedProjLoans (_, Some proj) -> (
-                match proj with
-                | V.AProjBorrows (_sv, ty') -> assert (ty' = ty)
-                | V.AEndedProjBorrows _ -> ()
-                | _ -> failwith "Unexpected")
-            | V.AEndedProjLoans (_, None)
-            | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
-                ())
+            | V.AEndedProjLoans given_back_ls ->
+                List.iter
+                  (fun (_, proj) ->
+                    match proj with
+                    | V.AProjBorrows (_sv, ty') -> assert (ty' = ty)
+                    | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ()
+                    | _ -> failwith "Unexpected")
+                  given_back_ls
+            | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ())
         | V.AIgnored, _ -> ()
         | _ -> failwith "Erroneous typing");
         (* Continue exploring to inspect the subterms *)
@@ -700,7 +701,7 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
       method! visit_aproj abs aproj =
         (let abs = Option.get abs in
          match aproj with
-         | AProjLoans sv -> add_aproj_loans sv abs.abs_id abs.regions
+         | AProjLoans (sv, _) -> add_aproj_loans sv abs.abs_id abs.regions
          | AProjBorrows (sv, proj_ty) ->
              add_aproj_borrows sv abs.abs_id abs.regions proj_ty false
          | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
@@ -715,11 +716,17 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
       ^ V.SymbolicValueId.Map.to_string (Some "  ") show_sv_info !infos));
   (* Check *)
   let check_info _id info =
+    (* TODO: check that:
+     * - the loans are mutually disjoint
+     * - the borrows are mutually disjoint
+     * - the unions of the loans/borrows give everything
+     *)
     assert (info.env_count = 0 || info.aproj_borrows = []);
     if ty_has_borrows ctx.type_context.type_infos info.ty then
       assert (info.env_count <= 1);
     assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
   in
+
   M.iter check_info !infos
 
 let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit =
diff --git a/src/Print.ml b/src/Print.ml
index 6c39366c..024d835d 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -309,14 +309,25 @@ module Values = struct
 
   let rec aproj_to_string (fmt : value_formatter) (pv : V.aproj) : string =
     match pv with
-    | AProjLoans sv ->
-        "[" ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv ^ "]"
+    | AProjLoans (sv, given_back) ->
+        let given_back =
+          if given_back = [] then ""
+          else
+            let given_back = List.map snd given_back in
+            let given_back = List.map (aproj_to_string fmt) given_back in
+            " (" ^ String.concat "," given_back ^ ") "
+        in
+        "["
+        ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv
+        ^ given_back ^ "]"
     | AProjBorrows (sv, rty) ->
         "(" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
-    | AEndedProjLoans (_mv, aproj_opt) -> (
-        match aproj_opt with
-        | None -> "_"
-        | Some aproj -> aproj_to_string fmt aproj)
+    | AEndedProjLoans given_back ->
+        if given_back = [] then "_"
+        else
+          let given_back = List.map snd given_back in
+          let given_back = List.map (aproj_to_string fmt) given_back in
+          "ended_aproj_loans (" ^ String.concat "," given_back ^ ")"
     | AEndedProjBorrows _mv -> "_"
     | AIgnoredProjBorrows -> "_"
 
diff --git a/src/Values.ml b/src/Values.ml
index 8e6bda43..4946b811 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -59,11 +59,13 @@ type sv_kind =
       (** The value is an input value of the function whose body we are
           currently synthesizing.
        *)
-  | SynthGivenBack
+  | SynthRetGivenBack
       (** The value is a borrowed value that the function whose body we are
           synthesizing returned, and which was given back because we ended
           one of the lifetimes of this function (we do this to synthesize
           the backward functions).
+          
+          TODO: add a SynthInputGivenBack
        *)
 [@@deriving show]
 
@@ -236,25 +238,57 @@ class ['self] map_aproj_base =
   end
 
 type aproj =
-  | AProjLoans of symbolic_value
+  | AProjLoans of symbolic_value * (mvalue * aproj) list
+      (** A projector of loans over a symbolic value.
+      
+          Note that the borrows of a symbolic value may be spread between
+          different abstractions, meaning that the projector of loans might
+          receive *several* (symbolic) given back values.
+          
+          This is the case in the following example:
+          ```
+          fn f<'a> (...) -> (&'a mut u32, &'a mut u32);
+          fn g<'b, 'c>(p : (&'b mut u32, &'c mut u32));
+          
+          let p = f(...);
+          g(move p);
+          
+          // Symbolic context after the call to g:
+          // abs'a {'a} { [s@0 <: (&'a mut u32, &'a mut u32)] }
+          //
+          // abs'b {'b} { (s@0 <: (&'b mut u32, &'c mut u32)) }
+          // abs'c {'c} { (s@0 <: (&'b mut u32, &'c mut u32)) }
+          ```
+          
+          Upon evaluating the call to `f`, we introduce a symbolic value `s@0`
+          and a projector of loans (projector loans from the region 'c).
+          This projector will later receive two given back values: one for
+          'a and one for 'b.
+          
+          We accumulate those values in the list of projections (note that
+          the meta value stores the value which was given back).
+          
+          We can later end the projector of loans if `s@0` is not referenced
+          anywhere in the context below a projector of borrows which intersects
+          this projector of loans.
+       *)
   | AProjBorrows of symbolic_value * rty
       (** Note that an AProjBorrows only operates on a value which is not below
-          a shared loan: under a shared loan, we use [abstract_shared_borrow]. *)
-  | AEndedProjLoans of mvalue * aproj option
-      (** When ending a proj_loans over a symbolic value, we may need to insert
-          (and keep track of) a proj_borrows over the given back value, if the
-          symbolic value was consumed by an abstraction then updated.
-          
-          Rk.: for now the option is useless, because we forbid borrow overwrites on
-          returned values. A consequence is that when a proj_loans over a symbolic
-          value ends, we don't project the given back value.
-          
-          The meta-value is the value which was given back (and thus consumed by
-          the loan when it ended).
+          a shared loan: under a shared loan, we use [abstract_shared_borrow].
+          
+          Also note that once given to a borrow projection, a symbolic value
+          can't get updated/expanded: this means that we don't need to save
+          any meta-value here.
+       *)
+  | AEndedProjLoans of (mvalue * aproj) list
+      (** An ended projector of loans over a symbolic value.
+      
+          See the explanations for [AProjLoans]
        *)
   | AEndedProjBorrows of mvalue
-      (** The only purpose of [AEndedProjBorrows] is to store the (symbolic) value
-          which was generated upon ending the borrow (this is useful for synthesis)
+      (** The only purpose of [AEndedProjBorrows] is to store, for synthesis
+          purposes, the symbolic value which was generated and given back upon
+          ending the borrow.
        *)
   | AIgnoredProjBorrows
 [@@deriving
@@ -415,8 +449,8 @@ and aloan_content =
        *)
   | AEndedSharedLoan of typed_value * typed_avalue
       (** Similar to [AEndedMutLoan] but in this case there are no avalues to
-          give back. Actually, we could probably forget the shared value
-          altogether (and just keep the child avalue).
+          give back. We keep the shared value because it now behaves as a
+          "regular" value (which contains borrows we might want to end...).
        *)
   | AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue
       (** An ignored mutable loan.