Add an optional borrow identifier to AIgnoredMutBorrow, introduce the

AEndedIgnoredMutBorrow variant and fix a couple of bugs

9 files changed, 220 insertions, 51 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2789517e..9ac8149b 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -67,6 +67,9 @@ module Test = struct
       List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
     in
     (* Create the abstractions and insert them in the context *)
+    let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+      ref V.AbstractionId.Map.empty
+    in
     let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
       let abs_id = rg.A.id in
       let parents =
@@ -79,10 +82,20 @@ module Test = struct
           (fun s rid -> T.RegionId.Set.add rid s)
           T.RegionId.Set.empty rg.A.regions
       in
+      let ancestors_regions =
+        List.fold_left
+          (fun acc parent_id ->
+            T.RegionId.Set.union acc
+              (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+          regions rg.A.parents
+      in
+      abs_to_ancestors_regions :=
+        V.AbstractionId.Map.add abs_id ancestors_regions
+          !abs_to_ancestors_regions;
       (* Project over the values - we use *loan* projectors, as explained above *)
       let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in
       (* Create the abstraction *)
-      let abs = { V.abs_id; parents; regions; avalues } in
+      let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in
       (* Insert the abstraction in the context *)
       let ctx = { ctx with env = Abs abs :: ctx.env } in
       (* Return *)
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index c9637f46..b52454b1 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -169,9 +169,14 @@ let end_borrow_get_borrow (io : inner_outer)
                * of the two cases described above *)
               V.ABottom)
             else V.ABorrow (super#visit_ASharedBorrow outer bid)
-        | V.AIgnoredMutBorrow av ->
+        | V.AIgnoredMutBorrow (opt_bid, av) ->
             (* Nothing special to do *)
-            V.ABorrow (super#visit_AIgnoredMutBorrow outer av)
+            V.ABorrow (super#visit_AIgnoredMutBorrow outer opt_bid av)
+        | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+            (* Nothing special to do *)
+            V.ABorrow
+              (super#visit_AEndedIgnoredMutBorrow outer given_back_loans_proj
+                 child)
         | V.AProjSharedBorrow asb ->
             (* Check if the borrow we are looking for is in the asb *)
             if borrow_in_asb l asb then (
@@ -232,7 +237,18 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
     object (self)
       inherit [_] C.map_eval_ctx as super
 
-      method! visit_Loan opt_abs lc =
+      method! visit_typed_value opt_abs (v : V.typed_value) : V.typed_value =
+        match v.V.value with
+        | V.Loan lc ->
+            let value = self#visit_typed_Loan opt_abs v.V.ty lc in
+            ({ v with V.value } : V.typed_value)
+        | _ -> super#visit_typed_value opt_abs v
+      (** This is a bit annoying, but as we need the type of the value we
+          are exploring, for sanity checks, we need to implement
+          [visit_typed_avalue] instead of
+          overriding [visit_ALoan] *)
+
+      method visit_typed_Loan opt_abs ty lc =
         match lc with
         | V.SharedLoan (bids, v) ->
             (* We are giving back a value (i.e., the content of a *mutable*
@@ -241,6 +257,15 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
         | V.MutLoan bid' ->
             (* Check if this is the loan we are looking for *)
             if bid' = bid then (
+              (* Sanity check *)
+              let expected_ty = ty in
+              if nv.V.ty <> expected_ty then (
+                log#serror
+                  ("give_back_value: improper type:\n- expected: "
+                 ^ ety_to_string ctx ty ^ "\n- received: "
+                 ^ ety_to_string ctx nv.V.ty);
+                failwith "Value given back doesn't have the proper type");
+              (* Replace *)
               set_replaced ();
               nv.V.value)
             else V.Loan (super#visit_MutLoan opt_abs bid')
@@ -257,15 +282,46 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
           back, we need to reimplement [visit_typed_avalue] instead of
           [visit_ALoan] *)
 
+      method! visit_ABorrow (opt_abs : V.abs option) (bc : V.aborrow_content)
+          : V.avalue =
+        match bc with
+        | V.AIgnoredMutBorrow (bid', child) ->
+            if bid' = Some bid then
+              (* Insert a loans projector - note that if this case happens,
+               * it is necessarily because we ended a parent abstraction,
+               * and the given back value is thus a symbolic value *)
+              match nv.V.value with
+              | V.Symbolic sv ->
+                  (* The loan projector *)
+                  let given_back_loans_proj =
+                    mk_aproj_loans_from_symbolic_value sv
+                  in
+                  (* Continue giving back in the child value *)
+                  let child = super#visit_typed_avalue opt_abs child in
+                  (* Return *)
+                  V.ABorrow
+                    (V.AEndedIgnoredMutBorrow { given_back_loans_proj; child })
+              | _ -> failwith "Unreachable"
+            else
+              (* Continue exploring *)
+              V.ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child)
+        | _ ->
+            (* Continue exploring *)
+            super#visit_ABorrow opt_abs bc
+      (** We need to inspect ignored mutable borrows, to insert loan projectors
+          if necessary.
+       *)
+
       method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
           (lc : V.aloan_content) : V.avalue =
         (* Preparing a bit *)
-        let regions =
+        let regions, ancestors_regions =
           match opt_abs with
           | None -> failwith "Unreachable"
-          | Some abs -> abs.V.regions
+          | Some abs -> (abs.V.regions, abs.V.ancestors_regions)
         in
-        (* Rk.: there is a small issue with the types of the aloan values *)
+        (* Rk.: there is a small issue with the types of the aloan values.
+         * See the comment at the level of definition of [typed_avalue] *)
         let borrowed_value_aty =
           let _, ty, _ = ty_get_ref ty in
           ty
@@ -281,8 +337,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
               (* Apply the projection *)
               let given_back =
                 apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  regions nv borrowed_value_aty
+                  regions ancestors_regions nv borrowed_value_aty
               in
+              (* Continue giving back in the child value *)
+              let child = super#visit_typed_avalue opt_abs child in
               (* Return the new value *)
               V.ALoan (V.AEndedMutLoan { given_back; child }))
             else
@@ -307,8 +365,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
                * (i.e., we don't call [set_replaced]) *)
               let given_back =
                 apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  regions nv borrowed_value_aty
+                  regions ancestors_regions nv borrowed_value_aty
               in
+              (* Continue giving back in the child value *)
+              let child = super#visit_typed_avalue opt_abs child in
               V.ALoan (V.AEndedIgnoredMutLoan { given_back; child })
             else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
         | V.AEndedIgnoredMutLoan { given_back; child } ->
@@ -378,13 +438,22 @@ let give_back_avalue (_config : C.config) (bid : V.BorrowId.id)
         match lc with
         | V.AMutLoan (bid', child) ->
             if bid' = bid then (
+              (* Sanity check - about why we need to call [ty_get_ref]
+               * (and don't do the same thing as in [give_back_value])
+               * see the comment at the level of the definition of
+               * [typed_avalue] *)
+              let _, expected_ty, _ = ty_get_ref ty in
+              if nv.V.ty <> expected_ty then (
+                log#serror
+                  ("give_back_avalue: improper type:\n- expected: "
+                 ^ rty_to_string ctx ty ^ "\n- received: "
+                 ^ rty_to_string ctx nv.V.ty);
+                failwith "Value given back doesn't have the proper type");
               (* 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
@@ -600,7 +669,8 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       assert (borrow_in_asb l asb);
       (* Update the context *)
       give_back_shared config l ctx
-  | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable"
+  | Abstract (V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _) ->
+      failwith "Unreachable"
 
 (** Convert an [avalue] to a [value].
 
@@ -889,7 +959,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
                 asb
             then raise (FoundABorrowContent bc)
             else ()
-        | V.AIgnoredMutBorrow _ ->
+        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
             (* Nothing to do for ignored borrows *)
             ()
     end
@@ -918,7 +988,8 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
           with
           | V.AsbBorrow bid -> bid
           | _ -> failwith "Unexpected")
-      | V.AIgnoredMutBorrow _ -> failwith "Unexpected"
+      | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+          failwith "Unexpected"
     in
     let ctx = update_aborrow ek_all bid V.ABottom ctx in
     (* Then give back the value *)
@@ -932,7 +1003,8 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
       | V.AProjSharedBorrow _ ->
           (* Nothing to do *)
           ctx
-      | V.AIgnoredMutBorrow _ -> failwith "Unexpected"
+      | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+          failwith "Unexpected"
     in
     (* Reexplore *)
     end_abstraction_borrows config abs_id ctx
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index aaab18cb..b590eff6 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -305,7 +305,10 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
         | V.ASharedBorrow bid ->
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
             else super#visit_ASharedBorrow env bid
-        | V.AIgnoredMutBorrow av -> super#visit_AIgnoredMutBorrow env av
+        | V.AIgnoredMutBorrow (opt_bid, av) ->
+            super#visit_AIgnoredMutBorrow env opt_bid av
+        | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+            super#visit_AEndedIgnoredMutBorrow env given_back_loans_proj child
         | V.AProjSharedBorrow asb ->
             if borrow_in_asb l asb then
               raise (FoundGBorrowContent (Abstract bc))
@@ -418,8 +421,12 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue)
         | V.ASharedBorrow bid ->
             if bid = l then update ()
             else V.ABorrow (super#visit_ASharedBorrow env bid)
-        | V.AIgnoredMutBorrow av ->
-            V.ABorrow (super#visit_AIgnoredMutBorrow env av)
+        | V.AIgnoredMutBorrow (opt_bid, av) ->
+            V.ABorrow (super#visit_AIgnoredMutBorrow env opt_bid av)
+        | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+            V.ABorrow
+              (super#visit_AEndedIgnoredMutBorrow env given_back_loans_proj
+                 child)
         | V.AProjSharedBorrow asb ->
             if borrow_in_asb l asb then update ()
             else V.ABorrow (super#visit_AProjSharedBorrow env asb)
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index aebcda3c..e19f8bb4 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -63,15 +63,17 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
     object
       inherit [_] C.map_eval_ctx as super
 
-      method! visit_abs proj_regions abs =
-        assert (Option.is_none proj_regions);
-        let proj_regions = Some abs.V.regions in
-        super#visit_abs proj_regions abs
+      method! visit_abs current_abs abs =
+        assert (Option.is_none current_abs);
+        let current_abs = Some abs in
+        super#visit_abs current_abs abs
       (** When visiting an abstraction, we remember the regions it owns to be
           able to properly reduce projectors when expanding symbolic values *)
 
-      method! visit_ASymbolic proj_regions aproj =
-        let proj_regions = Option.get proj_regions in
+      method! visit_ASymbolic current_abs aproj =
+        let current_abs = Option.get current_abs in
+        let proj_regions = current_abs.regions in
+        let ancestors_regions = current_abs.ancestors_regions in
         match (aproj, proj_kind) with
         | V.AProjLoans sv, LoanProj ->
             (* Check if this is the symbolic value we are looking for *)
@@ -85,7 +87,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
               projected_value.V.value
             else
               (* Not the searched symbolic value: nothing to do *)
-              super#visit_ASymbolic (Some proj_regions) aproj
+              super#visit_ASymbolic (Some current_abs) aproj
         | V.AProjBorrows (sv, proj_ty), BorrowProj ->
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then
@@ -101,16 +103,16 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
               (* Apply the projector *)
               let projected_value =
                 apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  proj_regions expansion proj_ty
+                  proj_regions ancestors_regions expansion proj_ty
               in
               (* Replace *)
               projected_value.V.value
             else
               (* Not the searched symbolic value: nothing to do *)
-              super#visit_ASymbolic (Some proj_regions) aproj
+              super#visit_ASymbolic (Some current_abs) aproj
         | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj ->
             (* Nothing to do *)
-            super#visit_ASymbolic (Some proj_regions) aproj
+            super#visit_ASymbolic (Some current_abs) aproj
     end
   in
   (* Apply the expansion *)
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 036082eb..cbd07f3e 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -129,8 +129,8 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
 *)
 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 =
+    (regions : T.RegionId.set_t) (ancestors_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
@@ -151,7 +151,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
           List.map
             (fun (fv, fty) ->
               apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                regions fv fty)
+                regions ancestors_regions fv fty)
             fields_types
         in
         V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields }
@@ -169,7 +169,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
                 (* Apply the projection on the borrowed value *)
                 let bv =
                   apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                    regions bv ref_ty
+                    regions ancestors_regions bv ref_ty
                 in
                 V.AMutBorrow (bid, bv)
             | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid
@@ -183,13 +183,19 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
           (* Not in the set: ignore *)
           let bc =
             match (bc, kind) with
-            | V.MutBorrow (_bid, bv), T.Mut ->
+            | 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
+                    regions ancestors_regions bv ref_ty
                 in
-                V.AIgnoredMutBorrow bv
+                (* If the borrow id is in the ancestor's regions, we still need
+                 * to remember it *)
+                let opt_bid =
+                  if region_in_set r ancestors_regions then Some bid else None
+                in
+                (* Return *)
+                V.AIgnoredMutBorrow (opt_bid, bv)
             | V.SharedBorrow bid, T.Shared ->
                 (* Lookup the shared value *)
                 let ek = ek_all in
@@ -493,8 +499,8 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool) :
   (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 =
+    (regions : T.RegionId.set_t) (ancestors_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 *)
@@ -503,7 +509,8 @@ let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx)
   in
   (* Apply the projector *)
   let av =
-    apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions v ty
+    apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions
+      ancestors_regions v ty
   in
   (* Apply the reborrows *)
   let ctx = apply_registered_reborrows ctx in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 36d11a9e..82f95556 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -815,6 +815,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
         arg.V.ty = Subst.erase_regions rty)
       args_with_rtypes);
   (* Create the abstractions from the region groups and add them to the context *)
+  let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+    ref V.AbstractionId.Map.empty
+  in
   let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
     let abs_id = rg.A.id in
     let parents =
@@ -827,17 +830,27 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
         (fun s rid -> T.RegionId.Set.add rid s)
         T.RegionId.Set.empty rg.A.regions
     in
+    let ancestors_regions =
+      List.fold_left
+        (fun acc parent_id ->
+          T.RegionId.Set.union acc
+            (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+        regions rg.A.parents
+    in
+    abs_to_ancestors_regions :=
+      V.AbstractionId.Map.add abs_id ancestors_regions !abs_to_ancestors_regions;
     (* Project over the input values *)
     let ctx, args_projs =
       List.fold_left_map
         (fun ctx (arg, arg_rty) ->
-          apply_proj_borrows_on_input_value config ctx regions arg arg_rty)
+          apply_proj_borrows_on_input_value config ctx regions ancestors_regions
+            arg arg_rty)
         ctx args_with_rtypes
     in
     (* Group the input and output values *)
     let avalues = List.append args_projs [ ret_av ] in
     (* Create the abstraction *)
-    let abs = { V.abs_id; parents; regions; avalues } in
+    let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in
     (* Insert the abstraction in the context *)
     let ctx = { ctx with env = Abs abs :: ctx.env } in
     (* Return *)
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 3c5d24e3..be5f3ed3 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -253,7 +253,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
           match bc with
           | V.AMutBorrow (bid, _) -> register_borrow Mut bid
           | V.ASharedBorrow bid -> register_borrow Shared bid
-          | V.AIgnoredMutBorrow _ | V.AProjSharedBorrow _ ->
+          | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
+          | V.AProjSharedBorrow _ ->
               (* Do nothing *)
               ()
         in
@@ -347,7 +348,8 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
           match bc with
           | V.AMutBorrow (_, _) -> set_outer_mut info
           | V.ASharedBorrow _ -> set_outer_shared info
-          | V.AIgnoredMutBorrow _ -> set_outer_mut info
+          | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+              set_outer_mut info
           | V.AProjSharedBorrow _ -> set_outer_shared info
         in
         (* Continue exploring *)
@@ -526,7 +528,12 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 | Abstract (V.ASharedLoan (_, sv, _)) ->
                     assert (sv.V.ty = Subst.erase_regions ref_ty)
                 | _ -> failwith "Inconsistent context")
-            | V.AIgnoredMutBorrow av, T.Mut -> assert (av.V.ty = ref_ty)
+            | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut ->
+                assert (av.V.ty = ref_ty)
+            | V.AEndedIgnoredMutBorrow { given_back_loans_proj; child }, T.Mut
+              ->
+                assert (given_back_loans_proj.V.ty = ref_ty);
+                assert (child.V.ty = ref_ty)
             | V.AProjSharedBorrow _, T.Shared -> ()
             | _ -> failwith "Inconsistent context")
         | V.ALoan lc, aty -> (
diff --git a/src/Print.ml b/src/Print.ml
index ce31338d..5ae722b9 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -7,6 +7,9 @@ module A = CfimAst
 module C = Contexts
 module M = Modules
 
+let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
+  match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
+
 (** Pretty-printing for types *)
 module Types = struct
   let type_var_to_string (tv : T.type_var) : string = tv.name
@@ -406,8 +409,18 @@ module Values = struct
         ^ typed_avalue_to_string fmt av
         ^ ")"
     | ASharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
-    | AIgnoredMutBorrow av ->
-        "@ignored_mut_borrow(" ^ typed_avalue_to_string fmt av ^ ")"
+    | AIgnoredMutBorrow (opt_bid, av) ->
+        "@ignored_mut_borrow("
+        ^ option_to_string V.BorrowId.to_string opt_bid
+        ^ ", "
+        ^ typed_avalue_to_string fmt av
+        ^ ")"
+    | AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+        "@ended_ignored_mut_borrow{ given_back_loans_proj="
+        ^ typed_avalue_to_string fmt given_back_loans_proj
+        ^ "; child="
+        ^ typed_avalue_to_string fmt child
+        ^ ")"
     | AProjSharedBorrow sb ->
         "@ignored_shared_borrow("
         ^ abstract_shared_borrows_to_string fmt sb
diff --git a/src/Values.ml b/src/Values.ml
index b6bb414b..c9dff56a 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -195,6 +195,8 @@ class ['self] iter_typed_avalue_base =
   object (_self : 'self)
     inherit [_] iter_typed_value
 
+    method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> ()
+
     method visit_region : 'env -> region -> unit = fun _ _ -> ()
 
     method visit_aproj : 'env -> aproj -> unit = fun _ _ -> ()
@@ -211,6 +213,8 @@ class ['self] map_typed_avalue_base =
   object (_self : 'self)
     inherit [_] map_typed_value
 
+    method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id
+
     method visit_region : 'env -> region -> region = fun _ r -> r
 
     method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p
@@ -421,11 +425,15 @@ and aborrow_content =
           > abs0 { a_shared_bororw l0 }
           ```
      *)
-  | AIgnoredMutBorrow of typed_avalue
+  | AIgnoredMutBorrow of BorrowId.id option * typed_avalue
       (** An ignored mutable borrow.
-
-          This is mostly useful for typing concerns: when a borrow doesn't
-          belong to an abstraction, it would be weird to ignore it altogether.
+      
+          We need to keep track of ignored mut borrows because when ending such
+          borrows, we need to project the loans of the given back value to
+          insert them in the proper abstractions.
+          
+          Note that we need to do so only for borrows consumed by parent
+          abstractions (hence the optional borrow id).
 
           Example:
           ========
@@ -441,8 +449,29 @@ and aborrow_content =
           > x -> mut_loan l0
           > px -> mut_loan l1
           > ppx -> ⊥
-          > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow (U32 0)) } // TODO: duplication
-          > abs'b { a_ignored_mut_borrow (a_mut_borrow l0 (U32 0)) }
+          > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None (U32 0)) } // TODO: duplication
+          > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 (U32 0)) }
+          
+          ... // abs'a ends
+          
+          > x -> mut_loan l0
+          > px -> @s0
+          > ppx -> ⊥
+          > abs'b {
+          >   a_ended_ignored_mut_borrow (a_proj_loans (@s0 <: &'b mut u32)) // <-- loan projector
+          >                              (a_mut_borrow l0 (U32 0))
+          > }
+          
+          ... // `@s0` gets expanded to `&mut l2 @s1`
+
+          > x -> mut_loan l0
+          > px -> &mut l2 @s1
+          > ppx -> ⊥
+          > abs'b {
+          >   a_ended_ignored_mut_borrow (a_mut_loan l2) // <-- loan l2 is here
+          >                              (a_mut_borrow l0 (U32 0))
+          > }
+          
           ```
           TODO: this is annoying, we are duplicating information. Maybe we
           could introduce an "Ignored" value? We have to pay attention to
@@ -460,6 +489,10 @@ and aborrow_content =
             abstraction so that we can properly call the backward functions
             when generating the pure translation.
        *)
+  | AEndedIgnoredMutBorrow of {
+      given_back_loans_proj : typed_avalue;
+      child : typed_avalue;
+    }  (** See the explanations for [AIgnoredMutBorrow] *)
   | AProjSharedBorrow of abstract_shared_borrows
       (** A projected shared borrow.
 
@@ -522,6 +555,8 @@ type abs = {
   abs_id : (AbstractionId.id[@opaque]);
   parents : (AbstractionId.set_t[@opaque]);  (** The parent abstractions *)
   regions : (RegionId.set_t[@opaque]);  (** Regions owned by this abstraction *)
+  ancestors_regions : (RegionId.set_t[@opaque]);
+      (** Union of the regions owned by this abstraction and its ancestors *)
   avalues : typed_avalue list;  (** The values in this abstraction *)
 }
 [@@deriving