Merge remote-tracking branch 'refs/remotes/origin/main'

14 files changed, 495 insertions, 142 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2789517e..f38cb66e 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -21,6 +21,9 @@ open InterpreterStatements
 
 (* TODO: remove the config parameters when they are useless *)
 
+(** The local logger *)
+let log = L.interpreter_log
+
 module Test = struct
   let initialize_context (type_context : C.type_context)
       (fun_defs : A.fun_def list) (type_vars : T.type_var list) : C.eval_ctx =
@@ -66,29 +69,23 @@ module Test = struct
     let input_svs =
       List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
     in
-    (* Create the abstractions and insert them in the context *)
-    let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
-      let abs_id = rg.A.id in
-      let parents =
-        List.fold_left
-          (fun s pid -> V.AbstractionId.Set.add pid s)
-          V.AbstractionId.Set.empty rg.A.parents
-      in
-      let regions =
-        List.fold_left
-          (fun s rid -> T.RegionId.Set.add rid s)
-          T.RegionId.Set.empty rg.A.regions
-      in
+    (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+    let empty_absl =
+      create_empty_abstractions_from_abs_region_groups
+        inst_sg.A.regions_hierarchy
+    in
+    (* Add the avalues to the abstractions and insert them in the context *)
+    let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx =
       (* 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
+      (* Insert the avalues in the abstraction *)
+      let abs = { abs with avalues } in
       (* Insert the abstraction in the context *)
       let ctx = { ctx with env = Abs abs :: ctx.env } in
       (* Return *)
       ctx
     in
-    let ctx = List.fold_left create_abs ctx inst_sg.regions_hierarchy in
+    let ctx = List.fold_left insert_abs ctx empty_absl in
     (* Split the variables between return var, inputs and remaining locals *)
     let ret_var = List.hd fdef.locals in
     let input_vars, local_vars =
@@ -113,7 +110,7 @@ module Test = struct
     let fdef = A.FunDefId.nth fun_defs fid in
 
     (* Debug *)
-    L.log#ldebug
+    log#ldebug
       (lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name));
 
     (* Sanity check - *)
@@ -164,7 +161,7 @@ module Test = struct
     let fdef = A.FunDefId.nth fun_defs fid in
 
     (* Debug *)
-    L.log#ldebug
+    log#ldebug
       (lazy
         ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name));
 
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 1dd4d247..c651e2f1 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].
 
@@ -743,12 +813,30 @@ and end_borrows (config : C.config) (io : inner_outer)
 
 and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id)
     (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Remember the original context for printing purposes *)
+  let ctx0 = ctx in
+  log#ldebug
+    (lazy
+      ("end_abstraction: "
+      ^ V.AbstractionId.to_string abs_id
+      ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0));
   (* Lookup the abstraction *)
   let abs = C.ctx_lookup_abs ctx abs_id in
   (* End the parent abstractions first *)
   let ctx = end_abstractions config abs.parents ctx in
+  log#ldebug
+    (lazy
+      ("end_abstraction: "
+      ^ V.AbstractionId.to_string abs_id
+      ^ "\n- context after parent abstractions ended:\n"
+      ^ eval_ctx_to_string ctx));
   (* End the loans inside the abstraction *)
   let ctx = end_abstraction_loans config abs_id ctx in
+  log#ldebug
+    (lazy
+      ("end_abstraction: "
+      ^ V.AbstractionId.to_string abs_id
+      ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx));
   (* End the abstraction itself by redistributing the borrows it contains *)
   let ctx = end_abstraction_borrows config abs_id ctx in
   (* End the regions owned by the abstraction - note that we don't need to
@@ -762,7 +850,16 @@ and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id)
   in
   (* Remove all the references to the id of the current abstraction, and remove
    * the abstraction itself *)
-  end_abstraction_remove_from_context config abs_id ctx
+  let ctx = end_abstraction_remove_from_context config abs_id ctx in
+  (* Debugging *)
+  log#ldebug
+    (lazy
+      ("end_abstraction: "
+      ^ V.AbstractionId.to_string abs_id
+      ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
+      ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx));
+  (* Return *)
+  ctx
 
 and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t)
     (ctx : C.eval_ctx) : C.eval_ctx =
@@ -862,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
@@ -891,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 *)
@@ -905,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
@@ -1031,7 +1130,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
       | None ->
           (* No loan to end inside the value *)
           (* Some sanity checks *)
-          L.log#ldebug
+          log#ldebug
             (lazy
               ("activate_inactivated_mut_borrow: resulting value:\n"
              ^ V.show_typed_value sv));
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index bc2f5971..b590eff6 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -9,6 +9,9 @@ module Subst = Substitute
 module L = Logging
 open InterpreterUtils
 
+(** The local logger *)
+let log = L.borrows_log
+
 (** TODO: cleanup this a bit, once we have a better understanding about
     what we need.
     TODO: I'm not sure in which file this should be moved... *)
@@ -302,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))
@@ -415,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 345c3df3..e19f8bb4 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -16,6 +16,9 @@ open InterpreterUtils
 open InterpreterProjectors
 open InterpreterBorrows
 
+(** The local logger *)
+let log = L.expansion_log
+
 (** Projector kind *)
 type proj_kind = LoanProj | BorrowProj
 
@@ -60,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 *)
@@ -82,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
@@ -98,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 *)
@@ -366,6 +371,8 @@ let expand_symbolic_value_borrow (config : C.config)
 let expand_symbolic_value_no_branching (config : C.config)
     (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) :
     C.eval_ctx =
+  (* Remember the initial context for printing purposes *)
+  let ctx0 = ctx in
   (* Compute the expanded value - note that when doing so, we may introduce
    * fresh symbolic values in the context (which thus gets updated) *)
   let original_sv = sp in
@@ -424,6 +431,14 @@ let expand_symbolic_value_no_branching (config : C.config)
         failwith
           ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
   in
+  (* Debugging *)
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("expand_symbolic_value: "
+      ^ symbolic_value_to_string ctx0 sp
+      ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
+      ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Sanity check: the symbolic value has disappeared *)
   assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
   (* Return *)
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 0b4bc90f..f3b07cc2 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -14,6 +14,9 @@ open InterpreterUtils
 open InterpreterExpansion
 open InterpreterPaths
 
+(** The local logger *)
+let log = L.expressions_log
+
 (** TODO: change the name *)
 type eval_error = Panic
 
@@ -70,7 +73,37 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
   | _, Unit | _, ConstantAdt _ | _, ConstantValue _ ->
       failwith "Improperly typed constant value"
 
-(** Prepare the evaluation of an operand. *)
+(** Prepare the evaluation of an operand.
+
+    Evaluating an operand requires updating the context to get access to a
+    given place (by ending borrows, expanding symbolic values...) then
+    applying the operand operation (move, copy, etc.).
+    
+    Sometimes, we want to decouple the two operations.
+    Consider the following example:
+    ```
+    context = {
+      x -> shared_borrow l0
+      y -> shared_loan {l0} v
+    }
+    
+    dest <- f(move x, move y);
+    ...
+    ```
+    Because of the way end_borrow is implemented, when giving back the borrow
+    `l0` upon evaluating `move y`, we won't notice that `shared_borrow l0` has
+    disappeared from the environment (it has been moved and not assigned yet,
+    and so is hanging in "thin air").
+    
+    By first "preparing" the operands evaluation, we make sure no such thing
+    happens. To be more precise, we make sure all the updates to borrows triggered
+    by access *and* move operations have already been applied.
+    
+    As a side note: doing this is actually not completely necessary because when
+    generating MIR, rustc introduces intermediate assignments for all the function
+    parameters. Still, it is better for soundness purposes, and corresponds to
+    what we do in the formal semantics.
+ *)
 let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
     : C.eval_ctx * V.typed_value =
   let ctx, v =
@@ -94,7 +127,7 @@ let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
 let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
     C.eval_ctx * V.typed_value =
   (* Debug *)
-  L.log#ldebug
+  log#ldebug
     (lazy
       ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n"
      ^ operand_to_string ctx op ^ "\n"));
@@ -108,7 +141,6 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
       let access = Read in
       let ctx, v = prepare_rplace config access p ctx in
       (* Copy the value *)
-      L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v));
       assert (not (bottom_in_value ctx.ended_regions v));
       let allow_adt_copy = false in
       copy_value allow_adt_copy config ctx v
@@ -117,16 +149,24 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
       let access = Move in
       let ctx, v = prepare_rplace config access p ctx in
       (* Move the value *)
-      L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v));
       assert (not (bottom_in_value ctx.ended_regions v));
       let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
       match write_place config access p bottom ctx with
       | Error _ -> failwith "Unreachable"
       | Ok ctx -> (ctx, v))
 
+(** Small utility.
+
+    See [eval_operand_prepare].
+ *)
+let eval_operands_prepare (config : C.config) (ctx : C.eval_ctx)
+    (ops : E.operand list) : C.eval_ctx * V.typed_value list =
+  List.fold_left_map (fun ctx op -> eval_operand_prepare config ctx op) ctx ops
+
 (** Evaluate several operands. *)
 let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : E.operand list)
     : C.eval_ctx * V.typed_value list =
+  let ctx, _ = eval_operands_prepare config ctx ops in
   List.fold_left_map (fun ctx op -> eval_operand config ctx op) ctx ops
 
 let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : E.operand)
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 07c615a0..491e4c21 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -12,6 +12,9 @@ open InterpreterBorrowsCore
 open InterpreterBorrows
 open InterpreterExpansion
 
+(** The local logger *)
+let log = L.paths_log
+
 (** Paths *)
 
 (** When we fail reading from or writing to a path, it might be because we
@@ -76,7 +79,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
       let nv = update v in
       (* Type checking *)
       if nv.ty <> v.ty then (
-        L.log#lerror
+        log#lerror
           (lazy
             ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: "
            ^ T.show_ety v.ty));
@@ -244,7 +247,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
           let pe = "- pe: " ^ E.show_projection_elem pe in
           let v = "- v:\n" ^ V.show_value v in
           let ty = "- ty:\n" ^ T.show_ety ty in
-          L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
+          log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
           failwith "Inconsistent projection")
 
 (** Generic function to access (read/write) the value at a given place.
@@ -314,7 +317,7 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
             ^ C.show_env ctx1.env ^ "\n\nOld environment:\n"
             ^ C.show_env ctx.env
           in
-          L.log#serror msg;
+          log#serror msg;
           failwith "Unexpected environment update");
       Ok read_value
 
@@ -402,7 +405,7 @@ let expand_bottom_value_from_projection (config : C.config)
     (access : access_kind) (p : E.place) (remaining_pes : int)
     (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx =
   (* Debugging *)
-  L.log#ldebug
+  log#ldebug
     (lazy
       ("expand_bottom_value_from_projection:\n" ^ "pe: "
      ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty));
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..917f1265 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -15,13 +15,16 @@ open InterpreterExpansion
 open InterpreterPaths
 open InterpreterExpressions
 
+(** The local logger *)
+let log = L.statements_log
+
 (** Result of evaluating a statement *)
 type statement_eval_res = Unit | Break of int | Continue of int | Return
 
 (** Drop a value at a given place *)
 let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx
     =
-  L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p));
+  log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p));
   (* Prepare the place (by ending the loans, then the borrows) *)
   let ctx, v = prepare_lplace config p ctx in
   (* Replace the value with [Bottom] *)
@@ -167,7 +170,7 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id)
 let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
     C.eval_ctx * V.typed_value =
   (* Debug *)
-  L.log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx));
+  log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx));
   (* Eval *)
   let ret_vid = V.VarId.zero in
   (* List the local variables, but the return variable *)
@@ -182,7 +185,7 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
   in
   let locals = list_locals ctx.env in
   (* Debug *)
-  L.log#ldebug
+  log#ldebug
     (lazy
       ("ctx_pop_frame: locals to drop: ["
       ^ String.concat "," (List.map V.VarId.to_string locals)
@@ -194,7 +197,7 @@ let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) :
       ctx locals
   in
   (* Debug *)
-  L.log#ldebug
+  log#ldebug
     (lazy
       ("ctx_pop_frame: after dropping local variables:\n"
      ^ eval_ctx_to_string ctx));
@@ -510,11 +513,59 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
   (* Return *)
   (ctx, inst_sig)
 
+(** Helper
+ 
+    Create abstractions (with no avalues, which have to be inserted afterwards)
+    from a list of abs region groups.
+ *)
+let create_empty_abstractions_from_abs_region_groups
+    (rgl : A.abs_region_group list) : V.abs list =
+  (* We use a reference to progressively create a map from abstraction ids
+   * to set of ancestor regions. Note that abs_to_ancestors_regions[abs_id]
+   * returns the union of:
+   * - the regions of the ancestors of abs_id
+   * - the regions of abs_id
+   *)
+  let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+    ref V.AbstractionId.Map.empty
+  in
+  (* Auxiliary function to create one abstraction *)
+  let create_abs (rg : A.abs_region_group) : V.abs =
+    let abs_id = rg.A.id in
+    let parents =
+      List.fold_left
+        (fun s pid -> V.AbstractionId.Set.add pid s)
+        V.AbstractionId.Set.empty rg.A.parents
+    in
+    let regions =
+      List.fold_left
+        (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))
+        T.RegionId.Set.empty rg.A.parents
+    in
+    let ancestors_regions_union_current_regions =
+      T.RegionId.Set.union ancestors_regions regions
+    in
+    abs_to_ancestors_regions :=
+      V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
+        !abs_to_ancestors_regions;
+    (* Create the abstraction *)
+    { V.abs_id; parents; regions; ancestors_regions; avalues = [] }
+  in
+  (* Apply *)
+  List.map create_abs rgl
+
 (** Evaluate a statement *)
 let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
     : (C.eval_ctx * statement_eval_res) eval_result list =
   (* Debugging *)
-  L.log#ldebug
+  log#ldebug
     (lazy
       ("\n**About to evaluate statement**: [\n"
       ^ statement_to_string_with_tab ctx st
@@ -814,36 +865,30 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       (fun ((arg, rty) : V.typed_value * T.rty) ->
         arg.V.ty = Subst.erase_regions rty)
       args_with_rtypes);
-  (* Create the abstractions from the region groups and add them to the context *)
-  let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
-    let abs_id = rg.A.id in
-    let parents =
-      List.fold_left
-        (fun s pid -> V.AbstractionId.Set.add pid s)
-        V.AbstractionId.Set.empty rg.A.parents
-    in
-    let regions =
-      List.fold_left
-        (fun s rid -> T.RegionId.Set.add rid s)
-        T.RegionId.Set.empty rg.A.regions
-    in
+  (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+  let empty_absl =
+    create_empty_abstractions_from_abs_region_groups inst_sg.A.regions_hierarchy
+  in
+  (* Add the avalues to the abstractions and insert them in the context *)
+  let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx =
     (* 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 abs.regions
+            abs.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
+    (* Add the avalues to the abstraction *)
+    let abs = { abs with avalues } in
     (* Insert the abstraction in the context *)
     let ctx = { ctx with env = Abs abs :: ctx.env } in
     (* Return *)
     ctx
   in
-  let ctx = List.fold_left create_abs ctx inst_sg.A.regions_hierarchy in
+  let ctx = List.fold_left insert_abs ctx empty_absl in
   (* Move the return value to its destination *)
   let ctx = assign_to_place config ctx ret_value dest in
   (* Synthesis *)
@@ -896,7 +941,7 @@ and eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx)
     (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
     C.eval_ctx eval_result =
   (* Debug *)
-  L.log#ldebug
+  log#ldebug
     (lazy
       (let type_params =
          "["
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 1f8e47e0..6c5d3289 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -10,28 +10,29 @@ module L = Logging
 open ValuesUtils
 open Utils
 open TypesUtils
+module PA = Print.EvalCtxCfimAst
 
 (** Some utilities *)
 
 let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
 
-let ety_to_string = Print.EvalCtxCfimAst.ety_to_string
+let ety_to_string = PA.ety_to_string
 
-let rty_to_string = Print.EvalCtxCfimAst.rty_to_string
+let rty_to_string = PA.rty_to_string
 
-let typed_value_to_string = Print.EvalCtxCfimAst.typed_value_to_string
+let symbolic_value_to_string = PA.symbolic_value_to_string
 
-let typed_avalue_to_string = Print.EvalCtxCfimAst.typed_avalue_to_string
+let typed_value_to_string = PA.typed_value_to_string
 
-let place_to_string = Print.EvalCtxCfimAst.place_to_string
+let typed_avalue_to_string = PA.typed_avalue_to_string
 
-let operand_to_string = Print.EvalCtxCfimAst.operand_to_string
+let place_to_string = PA.place_to_string
 
-let statement_to_string ctx =
-  Print.EvalCtxCfimAst.statement_to_string ctx "" "  "
+let operand_to_string = PA.operand_to_string
 
-let statement_to_string_with_tab ctx =
-  Print.EvalCtxCfimAst.statement_to_string ctx "  " "  "
+let statement_to_string ctx = PA.statement_to_string ctx "" "  "
+
+let statement_to_string_with_tab ctx = PA.statement_to_string ctx "  " "  "
 
 let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
   sv0.V.sv_id = sv1.V.sv_id
diff --git a/src/Invariants.ml b/src/Invariants.ml
index e214e820..3fc390b5 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -12,7 +12,8 @@ open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 
-let debug_invariants : bool ref = ref false
+(** The local logger *)
+let log = L.invariants_log
 
 type borrow_info = {
   loan_kind : T.ref_kind;
@@ -35,20 +36,24 @@ let set_outer_mut (info : outer_borrow_info) : outer_borrow_info =
 let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info =
   { outer_borrow = true; outer_shared = true }
 
-(* TODO: we need to factorize print functions for strings *)
-let ids_reprs_to_string (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
+(* TODO: we need to factorize print functions for sets *)
+let ids_reprs_to_string (indent : string)
+    (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
   let bindings = V.BorrowId.Map.bindings reprs in
   let bindings =
     List.map
       (fun (id, repr_id) ->
-        V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id)
+        indent ^ V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id)
       bindings
   in
   String.concat "\n" bindings
 
-let borrows_infos_to_string (infos : borrow_info V.BorrowId.Map.t) : string =
+let borrows_infos_to_string (indent : string)
+    (infos : borrow_info V.BorrowId.Map.t) : string =
   let bindings = V.BorrowId.Map.bindings infos in
-  let bindings = List.map (fun (_, info) -> show_borrow_info info) bindings in
+  let bindings =
+    List.map (fun (_, info) -> indent ^ show_borrow_info info) bindings
+  in
   String.concat "\n" bindings
 
 type borrow_kind = Mut | Shared | Inactivated
@@ -67,9 +72,24 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
   let borrows_infos : borrow_info V.BorrowId.Map.t ref =
     ref V.BorrowId.Map.empty
   in
+  let context_to_string () : string =
+    eval_ctx_to_string ctx ^ "- representants:\n"
+    ^ ids_reprs_to_string "  " !ids_reprs
+    ^ "\n- info:\n"
+    ^ borrows_infos_to_string "  " !borrows_infos
+  in
+  (* Ignored loans - when we find an ignored loan while building the borrows_infos
+   * map, we register it in this list; once the borrows_infos map is completely
+   * built, we check that all the borrow ids of the ignored loans are in this
+   * map *)
+  let ignored_loans : (T.ref_kind * V.BorrowId.id) list ref = ref [] in
 
-  (* First, register all the loans *)
+  (* first, register all the loans *)
   (* Some utilities to register the loans *)
+  let register_ignored_loan (rkind : T.ref_kind) (bid : V.BorrowId.id) : unit =
+    ignored_loans := (rkind, bid) :: !ignored_loans
+  in
+
   let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.set_t) : unit
       =
     let reprs = !ids_reprs in
@@ -150,11 +170,11 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
           match lc with
           | V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid
           | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
+          | V.AIgnoredMutLoan (bid, _) -> register_ignored_loan T.Mut bid
+          | V.AIgnoredSharedLoan _
           | V.AEndedMutLoan { given_back = _; child = _ }
           | V.AEndedSharedLoan (_, _)
-          | V.AIgnoredMutLoan (_, _) (* We might want to do something here *)
-          | V.AEndedIgnoredMutLoan { given_back = _; child = _ }
-          | V.AIgnoredSharedLoan _ ->
+          | V.AEndedIgnoredMutLoan { given_back = _; child = _ } ->
               (* Do nothing *)
               ()
         in
@@ -178,13 +198,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     | None ->
         let err =
           "find_info: could not find the representant of borrow "
-          ^ V.BorrowId.to_string bid ^ "\n" ^ "\n- Context:\n"
-          ^ eval_ctx_to_string ctx ^ "\n- representants:\n"
-          ^ ids_reprs_to_string !ids_reprs
-          ^ "\n- info:\n"
-          ^ borrows_infos_to_string !borrows_infos
+          ^ V.BorrowId.to_string bid ^ "\n" ^ context_to_string ()
         in
-        L.log#serror err;
+        log#serror err;
         failwith err
   in
 
@@ -201,6 +217,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     borrows_infos := infos
   in
 
+  let register_ignored_borrow = register_ignored_loan in
+
   let register_borrow (kind : borrow_kind) (bid : V.BorrowId.id) : unit =
     (* Lookup the info *)
     let info = find_info bid in
@@ -246,7 +264,9 @@ 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 (Some bid, _) -> register_ignored_borrow Mut bid
+          | V.AIgnoredMutBorrow (None, _)
+          | V.AEndedIgnoredMutBorrow _ | V.AProjSharedBorrow _ ->
               (* Do nothing *)
               ()
         in
@@ -259,17 +279,18 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
   borrows_visitor#visit_eval_ctx () ctx;
 
   (* Debugging *)
-  if !debug_invariants then (
-    L.log#ldebug
-      (lazy
-        ("\nAbout to check context invariant:\n" ^ eval_ctx_to_string ctx ^ "\n"));
-    L.log#ldebug
-      (lazy
-        ("\nBorrows information:\n"
-        ^ borrows_infos_to_string !borrows_infos
-        ^ "\n")));
+  log#ldebug
+    (lazy ("\nAbout to check context invariant:\n" ^ context_to_string ()));
 
   (* Finally, check that everything is consistant *)
+  (* First, check all the ignored loans are present at the proper place *)
+  List.iter
+    (fun (rkind, bid) ->
+      let info = find_info bid in
+      assert (info.loan_kind = rkind))
+    !ignored_loans;
+
+  (* Then, check the borrow infos *)
   V.BorrowId.Map.iter
     (fun _ info ->
       (* Note that we can't directly compare the sets - I guess they are
@@ -347,7 +368,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 *)
@@ -464,6 +486,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_value info tv
 
+      (* TODO: there is a lot of duplication with [visit_typed_value]
+       * which is quite annoying. There might be a way of factorizing
+       * that by factorizing the definitions of value and avalue, but
+       * the generation of visitors then doesn't work properly (TODO:
+       * report that). Still, it is actually not that problematic
+       * because this code shouldn't change a lot in the future,
+       * so the cost of maintenance should be pretty low.
+       * *)
       method! visit_typed_avalue info atv =
         (* Check the current pair (value, type) *)
         (match (atv.V.value, atv.V.ty) with
@@ -526,7 +556,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 -> (
@@ -569,7 +604,6 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | _ -> failwith "Erroneous typing");
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
-      (** TODO: there is a lot of duplication with [visit_typed_value]... *)
     end
   in
   visitor#visit_eval_ctx () ctx
diff --git a/src/Logging.ml b/src/Logging.ml
index a1060014..36ede236 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -3,7 +3,32 @@ module L = Easy_logging.Logging
 
 let _ = L.make_logger "MainLogger" Debug [ Cli Debug ]
 
-let log = L.get_logger "MainLogger"
+(** The main logger *)
+let main_log = L.get_logger "MainLogger"
+
+(** Below, we create subgloggers for various submodules, so that we can precisely
+    toggle logging on/off, depending on which information we need *)
+
+(** Logger for Interpreter *)
+let interpreter_log = L.get_logger "MainLogger.Interpreter"
+
+(** Logger for InterpreterStatements *)
+let statements_log = L.get_logger "MainLogger.Interpreter.Statements"
+
+(** Logger for InterpreterExpressions *)
+let expressions_log = L.get_logger "MainLogger.Interpreter.Expressions"
+
+(** Logger for InterpreterPaths *)
+let paths_log = L.get_logger "MainLogger.Interpreter.Paths"
+
+(** Logger for InterpreterExpansion *)
+let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion"
+
+(** Logger for InterpreterBorrows *)
+let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"
+
+(** Logger for Invariants *)
+let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants"
 
 (** Terminal colors - TODO: comes from easy_logging (did not manage to reuse the module directly) *)
 type color =
@@ -109,7 +134,7 @@ let format_tags (tags : string list) =
       "[" ^ elems_str ^ "] "
 
 (* Change the formatters *)
-let _ =
+let main_logger_handler =
   (* TODO: comes from easy_logging *)
   let formatter (item : L.log_item) : string =
     let item_level_fmt =
@@ -125,5 +150,6 @@ let _ =
       item_msg_fmt
   in
   (* There should be exactly one handler *)
-  let handlers = log#get_handlers in
-  List.map (fun h -> H.set_formatter h formatter) handlers
+  let handlers = main_log#get_handlers in
+  List.iter (fun h -> H.set_formatter h formatter) handlers;
+  match handlers with [ handler ] -> handler | _ -> failwith "Unexpected"
diff --git a/src/Print.ml b/src/Print.ml
index f714e847..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
@@ -390,7 +393,7 @@ module Values = struct
         ^ typed_avalue_to_string fmt av
         ^ ")"
     | AEndedIgnoredMutLoan ml ->
-        "@ended_ignored_mut_borrow{ given_back="
+        "@ended_ignored_mut_loan{ given_back="
         ^ typed_avalue_to_string fmt ml.given_back
         ^ "; child: "
         ^ typed_avalue_to_string fmt ml.child
@@ -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
@@ -973,6 +986,12 @@ module EvalCtxCfimAst = struct
     let fmt = PC.ctx_to_rtype_formatter fmt in
     PT.rty_to_string fmt t
 
+  let symbolic_value_to_string (ctx : C.eval_ctx) (sv : V.symbolic_value) :
+      string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_rtype_formatter fmt in
+    PV.symbolic_value_to_string fmt sv
+
   let typed_value_to_string (ctx : C.eval_ctx) (v : V.typed_value) : string =
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
     PV.typed_value_to_string fmt v
diff --git a/src/Values.ml b/src/Values.ml
index b6bb414b..bcb08dc8 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,9 +449,38 @@ 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))
+          > }
+          
           ```
+
+          Note that we could use AIgnoredMutLoan in the case the borrow id is not
+          None, which would allow us to simplify the rules (to not have rules
+          to specifically handle the case of AIgnoredMutBorrow with Some borrow
+          id) and also remove the AEndedIgnoredMutBorrow variant.
+          For now, the rules are implemented and it allows us to make the avalues
+          more precise and clearer, so we will keep it that way.
+   
           TODO: this is annoying, we are duplicating information. Maybe we
           could introduce an "Ignored" value? We have to pay attention to
           two things:
@@ -460,6 +497,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 +563,9 @@ 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's ancestors (not
+          including the regions of this abstraction itself) *)
   avalues : typed_avalue list;  (** The values in this abstraction *)
 }
 [@@deriving
diff --git a/src/main.ml b/src/main.ml
index ac49b782..d8e9aa40 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -4,6 +4,7 @@ open Print
 module T = Types
 module A = CfimAst
 module I = Interpreter
+module EL = Easy_logging.Logging
 
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.
@@ -19,6 +20,7 @@ Usage: %s [OPTIONS] FILE
     Sys.argv.(0)
 
 let () =
+  (* Read the command line arguments *)
   let spec = [] in
   let spec = Arg.align spec in
   let filename = ref "" in
@@ -39,12 +41,23 @@ let () =
   if !filename = "" then (
     print_string usage;
     exit 1);
+  (* Set up the logging - for now we use default values - TODO: use the
+   * command-line arguments *)
+  Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
+  main_log#set_level EL.Debug;
+  interpreter_log#set_level EL.Debug;
+  statements_log#set_level EL.Debug;
+  expressions_log#set_level EL.Warning;
+  expansion_log#set_level EL.Debug;
+  borrows_log#set_level EL.Debug;
+  invariants_log#set_level EL.Warning;
+  (* Load the module *)
   let json = Yojson.Basic.from_file !filename in
   match cfim_module_of_json json with
-  | Error s -> log#error "error: %s\n" s
+  | Error s -> main_log#error "error: %s\n" s
   | Ok m ->
       (* Print the module *)
-      log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
+      main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
 
       (* Test the unit functions with the concrete interpreter *)
       I.Test.test_unit_functions m.types m.functions;