Start implementing support for loops

19 files changed, 1566 insertions, 264 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 7c3ce538..3e882365 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -30,7 +30,10 @@ let backend = ref FStar
 
 (** {1 Interpreter} *)
 
-(** Check that invariants are maintained whenever we execute a statement *)
+(** Check that invariants are maintained whenever we execute a statement
+
+    TODO: rename to sanity_checks.
+ *)
 let check_invariants = ref true
 
 (** Expand all symbolic values containing borrows upon introduction - allows
@@ -72,6 +75,17 @@ let allow_bottom_below_borrow = true
  *)
 let return_unit_end_abs_with_no_loans = true
 
+(** The maximum number of iterations we can do to find a loop fixed point.
+
+    This is mostly for sanity: we should always find a fixed point in a
+    reasonable number of iterations. If we fail to do so, it is likely a bug: we
+    thus use this bound to detect a loop, fail and report the case to the
+    user.
+ *)
+let loop_fixed_point_max_num_iters = 100
+
+(** {1 Translation} *)
+
 (** Forbids using field projectors for structures.
 
     If we don't use field projectors, whenever we symbolically expand a structure
@@ -103,8 +117,6 @@ let dont_use_field_projectors = ref false
 
 let always_deconstruct_adts_with_matches = ref false
 
-(** {1 Translation} *)
-
 (** Controls whether we need to use a state to model the external world
     (I/O, for instance).
  *)
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 96749f07..be758ffe 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -76,6 +76,8 @@ let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()
 let abstraction_id_counter, fresh_abstraction_id =
   AbstractionId.fresh_stateful_generator ()
 
+let loop_id_counter, fresh_loop_id = LoopId.fresh_stateful_generator ()
+
 let fun_call_id_counter, fresh_fun_call_id =
   FunCallId.fresh_stateful_generator ()
 
@@ -98,6 +100,7 @@ let reset_global_counters () =
   borrow_id_counter := BorrowId.generator_zero;
   region_id_counter := RegionId.generator_zero;
   abstraction_id_counter := AbstractionId.generator_zero;
+  loop_id_counter := LoopId.generator_zero;
   fun_call_id_counter := FunCallId.generator_zero;
   dummy_var_id_counter := DummyVarId.generator_zero
 
@@ -359,9 +362,76 @@ let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs =
   in
   lookup env
 
+(** Remove an abstraction from the context, as well as all the references to
+    this abstraction (for instance, remove the abs id from all the parent sets
+    of all the other abstractions).
+ *)
+let env_remove_abs (env : env) (abs_id : V.AbstractionId.id) :
+    env * V.abs option =
+  let rec remove (env : env) : env * V.abs option =
+    match env with
+    | [] -> raise (Failure "Unreachable")
+    | Frame :: _ -> (env, None)
+    | Var (bv, v) :: env ->
+        let env, abs_opt = remove env in
+        (Var (bv, v) :: env, abs_opt)
+    | Abs abs :: env ->
+        if abs.abs_id = abs_id then (env, Some abs)
+        else
+          let env, abs_opt = remove env in
+          (* Update the parents set *)
+          let parents = V.AbstractionId.Set.remove abs_id abs.parents in
+          (Abs { abs with V.parents } :: env, abs_opt)
+  in
+  remove env
+
+(** Substitue an abstraction in an environment.
+
+    Note that we substitute an abstraction (identified by its id) with a different
+    abstraction which **doesn't necessarily have the same id**. Because of this,
+    we also substitute the abstraction id wherever it is used (i.e., in the
+    parent sets of the other abstractions).
+ *)
+let env_subst_abs (env : env) (abs_id : V.AbstractionId.id) (nabs : V.abs) :
+    env * V.abs option =
+  let rec update (env : env) : env * V.abs option =
+    match env with
+    | [] -> raise (Failure "Unreachable")
+    | Frame :: _ -> (* We're done *) (env, None)
+    | Var (bv, v) :: env ->
+        let env, opt_abs = update env in
+        (Var (bv, v) :: env, opt_abs)
+    | Abs abs :: env ->
+        if abs.abs_id = abs_id then (Abs nabs :: env, Some abs)
+        else
+          let env, opt_abs = update env in
+          (* Update the parents set *)
+          let parents = abs.parents in
+          let parents =
+            if V.AbstractionId.Set.mem abs_id parents then
+              let parents = V.AbstractionId.Set.remove abs_id parents in
+              V.AbstractionId.Set.add nabs.abs_id parents
+            else parents
+          in
+          (Abs { abs with V.parents } :: env, opt_abs)
+  in
+  update env
+
 let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs =
   env_lookup_abs ctx.env abs_id
 
+(** See the comments for {!env_remove_abs} *)
+let ctx_remove_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) :
+    eval_ctx * V.abs option =
+  let env, abs = env_remove_abs ctx.env abs_id in
+  ({ ctx with env }, abs)
+
+(** See the comments for {!env_subst_abs} *)
+let ctx_subst_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) (nabs : V.abs)
+    : eval_ctx * V.abs option =
+  let env, abs_opt = env_subst_abs ctx.env abs_id nabs in
+  ({ ctx with env }, abs_opt)
+
 let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
   let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
   match decl_group with Rec _ -> true | NonRec _ -> false
diff --git a/compiler/Cps.ml b/compiler/Cps.ml
index de35198f..dc51c614 100644
--- a/compiler/Cps.ml
+++ b/compiler/Cps.ml
@@ -16,9 +16,16 @@ type statement_eval_res =
   | Continue of int
   | Return
   | Panic
-
-(** Synthesized expresssion - dummy for now *)
-type sexpr = SOne | SList of sexpr list
+  | EndEnterLoop
+      (** When we enter a loop, we delegate the end of the function is
+          synthesized with a call to the loop translation. We use this
+          evaluation result to transmit the fact that we end evaluation
+          because we entered a loop.
+       *)
+  | EndContinue
+      (** For loop translations: we end with a continue (i.e., a recursive call
+          to the translation for the loop body).
+       *)
 
 type eval_result = SA.expression option
 
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index dc203105..d1241b9d 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -93,7 +93,8 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
   in
   let region_can_end _ = true in
   let ctx =
-    create_push_abstractions_from_abs_region_groups call_id V.SynthInput
+    create_push_abstractions_from_abs_region_groups
+      (fun rg_id -> V.SynthInput rg_id)
       inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
   in
   (* Split the variables between return var, inputs and remaining locals *)
@@ -151,7 +152,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return
   (* Insert the return value in the return abstractions (by applying
    * borrow projections) *)
   let cf_consume_ret ret_value ctx =
-    let ret_call_id = C.fresh_fun_call_id () in
     let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) :
         C.eval_ctx * V.typed_avalue list =
       let ctx, avalue =
@@ -172,7 +172,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return
     in
     assert (region_can_end back_id);
     let ctx =
-      create_push_abstractions_from_abs_region_groups ret_call_id V.SynthRet
+      create_push_abstractions_from_abs_region_groups
+        (fun rg_id -> V.SynthRet rg_id)
         ret_inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
     in
 
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 3d8ca3bf..b85f6692 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -23,14 +23,17 @@ let log = L.borrows_log
     borrows, we end them, before finally ending the borrow we wanted to end in the
     first place.
 
-    [allowed_abs]: if not [None], allows to get a borrow in the given
-    abstraction without ending the whole abstraction first. This parameter
-    allows us to use {!end_borrow_aux} as an auxiliary function for
-    {!end_abstraction_aux} (we end all the borrows in the abstraction one by one
-    before removing the abstraction from the context).
+    - [allowed_abs]: if not [None], allows to get a borrow in the given
+      abstraction without ending the whole abstraction first. This parameter
+      allows us to use {!end_borrow_aux} as an auxiliary function for
+      {!end_abstraction_aux} (we end all the borrows in the abstraction one by one
+      before removing the abstraction from the context).
+    - [allow_inner_loans]: if [true], allow to end borrows containing inner
+      loans. This is used to merge borrows with abstractions, to compute loop
+      fixed points for instance.
 *)
 let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
-    (l : V.BorrowId.id) (ctx : C.eval_ctx) :
+    (allow_inner_loans : bool) (l : V.BorrowId.id) (ctx : C.eval_ctx) :
     (C.eval_ctx * g_borrow_content option, priority_borrows_or_abs) result =
   (* We use a reference to communicate the kind of borrow we found, if we
    * find one *)
@@ -63,16 +66,18 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
         | Some borrows -> raise (FoundPriority (OuterBorrows borrows))
         | None -> ()));
     (* Then check if there are inner loans *)
-    match borrowed_value with
-    | None -> ()
-    | Some v -> (
-        match get_first_loan_in_value v with
-        | None -> ()
-        | Some c -> (
-            match c with
-            | V.SharedLoan (bids, _) ->
-                raise (FoundPriority (InnerLoans (Borrows bids)))
-            | V.MutLoan bid -> raise (FoundPriority (InnerLoans (Borrow bid)))))
+    if not allow_inner_loans then
+      match borrowed_value with
+      | None -> ()
+      | Some v -> (
+          match get_first_loan_in_value v with
+          | None -> ()
+          | Some c -> (
+              match c with
+              | V.SharedLoan (bids, _) ->
+                  raise (FoundPriority (InnerLoans (Borrows bids)))
+              | V.MutLoan bid -> raise (FoundPriority (InnerLoans (Borrow bid)))
+              ))
   in
 
   (* The environment is used to keep track of the outer loans *)
@@ -436,8 +441,11 @@ let give_back_symbolic_value (_config : C.config)
   (* Sanity checks *)
   assert (sv.sv_id <> nsv.sv_id);
   (match nsv.sv_kind with
-  | V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
-  | V.FunCallRet | V.SynthInput | V.Global -> raise (Failure "Unrechable"));
+  | V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
+    ->
+      ()
+  | FunCallRet | SynthInput | Global | LoopOutput ->
+      raise (Failure "Unrechable"));
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -782,12 +790,41 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
     (av : V.typed_avalue) : V.symbolic_value =
   let sv_kind =
     match abs_kind with
-    | V.FunCall -> V.FunCallGivenBack
-    | V.SynthRet -> V.SynthRetGivenBack
-    | V.SynthInput -> V.SynthInputGivenBack
+    | V.FunCall _ -> V.FunCallGivenBack
+    | V.SynthRet _ -> V.SynthRetGivenBack
+    | V.SynthInput _ -> V.SynthInputGivenBack
+    | V.Loop _ -> V.LoopGivenBack
   in
   mk_fresh_symbolic_value sv_kind av.V.ty
 
+let check_borrow_disappeared (fun_name : string) (l : V.BorrowId.id)
+    (ctx0 : C.eval_ctx) : cm_fun =
+  let check_disappeared (ctx : C.eval_ctx) : unit =
+    let _ =
+      match lookup_borrow_opt ek_all l ctx with
+      | None -> () (* Ok *)
+      | Some _ ->
+          log#lerror
+            (lazy
+              (fun_name ^ ": " ^ V.BorrowId.to_string l
+             ^ ": borrow didn't disappear:\n- original context:\n"
+             ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
+             ^ eval_ctx_to_string ctx));
+          raise (Failure "Borrow not eliminated")
+    in
+    match lookup_loan_opt ek_all l ctx with
+    | None -> () (* Ok *)
+    | Some _ ->
+        log#lerror
+          (lazy
+            (fun_name ^ ": " ^ V.BorrowId.to_string l
+           ^ ": loan didn't disappear:\n- original context:\n"
+           ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
+           ^ eval_ctx_to_string ctx));
+        raise (Failure "Loan not eliminated")
+  in
+  unit_to_cm_fun check_disappeared
+
 (** End a borrow identified by its borrow id in a context.
 
     This function **preserves invariants** provided [allowed_abs] is [None]: if the
@@ -825,39 +862,10 @@ let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids)
   (* Utility function for the sanity checks: check that the borrow disappeared
    * from the context *)
   let ctx0 = ctx in
-  let check_disappeared (ctx : C.eval_ctx) : unit =
-    let _ =
-      match lookup_borrow_opt ek_all l ctx with
-      | None -> () (* Ok *)
-      | Some _ ->
-          log#lerror
-            (lazy
-              ("end borrow: " ^ V.BorrowId.to_string l
-             ^ ": borrow didn't disappear:\n- original context:\n"
-             ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
-             ^ eval_ctx_to_string ctx));
-          raise (Failure "Borrow not eliminated")
-    in
-    match lookup_loan_opt ek_all l ctx with
-    | None -> () (* Ok *)
-    | Some _ ->
-        log#lerror
-          (lazy
-            ("end borrow: " ^ V.BorrowId.to_string l
-           ^ ": loan didn't disappear:\n- original context:\n"
-           ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
-           ^ eval_ctx_to_string ctx));
-        raise (Failure "Loan not eliminated")
-  in
-  let cf_check_disappeared : cm_fun = unit_to_cm_fun check_disappeared in
-  (* The complete sanity check: also check that after we ended a borrow,
-   * the invariant is preserved *)
-  let cf_check : cm_fun =
-    comp cf_check_disappeared Invariants.cf_check_invariants
-  in
-
+  let cf_check : cm_fun = check_borrow_disappeared "end borrow" l ctx0 in
   (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *)
-  match end_borrow_get_borrow allowed_abs l ctx with
+  let allow_inner_loans = false in
+  match end_borrow_get_borrow allowed_abs allow_inner_loans l ctx with
   (* Two cases:
      - error: we found outer borrows (the borrow is inside a borrowed value) or
        inner loans (the borrow contains loans)
@@ -1211,14 +1219,20 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
         match bc with
         | V.SharedBorrow (_, bid) -> (
             (* Replace the shared borrow with bottom *)
-            match end_borrow_get_borrow (Some abs_id) bid ctx with
+            let allow_inner_loans = false in
+            match
+              end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx
+            with
             | Error _ -> raise (Failure "Unreachable")
             | Ok (ctx, _) ->
                 (* Give back *)
                 give_back_shared config bid ctx)
         | V.MutBorrow (bid, v) -> (
             (* Replace the mut borrow with bottom *)
-            match end_borrow_get_borrow (Some abs_id) bid ctx with
+            let allow_inner_loans = false in
+            match
+              end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx
+            with
             | Error _ -> raise (Failure "Unreachable")
             | Ok (ctx, _) ->
                 (* Give the value back - note that the mut borrow was below a
@@ -1233,22 +1247,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
 and end_abstraction_remove_from_context (_config : C.config)
     (abs_id : V.AbstractionId.id) : cm_fun =
  fun cf ctx ->
-  let rec remove_from_env (env : C.env) : C.env * V.abs option =
-    match env with
-    | [] -> raise (Failure "Unreachable")
-    | C.Frame :: _ -> (env, None)
-    | Var (bv, v) :: env ->
-        let env, abs_opt = remove_from_env env in
-        (Var (bv, v) :: env, abs_opt)
-    | C.Abs abs :: env ->
-        if abs.abs_id = abs_id then (env, Some abs)
-        else
-          let env, abs_opt = remove_from_env env in
-          let parents = V.AbstractionId.Set.remove abs_id abs.parents in
-          (C.Abs { abs with V.parents } :: env, abs_opt)
-  in
-  let env, abs = remove_from_env ctx.C.env in
-  let ctx = { ctx with C.env } in
+  let ctx, abs = C.ctx_remove_abs ctx abs_id in
   let abs = Option.get abs in
   (* Apply the continuation *)
   let expr = cf ctx in
@@ -1403,6 +1402,24 @@ let end_borrows config : V.BorrowId.Set.t -> cm_fun =
 let end_abstraction config = end_abstraction_aux config []
 let end_abstractions config = end_abstractions_aux config []
 
+(** Auxiliary function - call a function which requires a continuation,
+    and return the let context given to the continuation *)
+let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx =
+  let nctx = ref None in
+  let cf ctx =
+    assert (!nctx = None);
+    nctx := Some ctx;
+    None
+  in
+  let _ = f cf ctx in
+  Option.get !nctx
+
+let end_borrow_no_synth config id ctx =
+  get_cf_ctx_no_synth (end_borrow config id) ctx
+
+let end_abstraction_no_synth config id ctx =
+  get_cf_ctx_no_synth (end_abstraction config id) ctx
+
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
     This function updates the shared loan to a mutable loan (we then update
@@ -1552,3 +1569,440 @@ let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) :
         (Failure
            "Can't activate a reserved mutable borrow referencing a loan inside\n\
            \         an abstraction")
+
+let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (ctx : C.eval_ctx)
+    (abs0 : V.abs) : V.abs =
+  (* Accumulator to store the destructured values *)
+  let avalues = ref [] in
+  (* Utility function to store a value in the accumulator *)
+  let push_avalue av = avalues := av :: !avalues in
+  (* We use this function to make sure we never register values (i.e.,
+     loans or borrows) when we shouldn't - see it as a sanity check:
+     for now, we don't allow nested borrows, which means we should register
+     values from children of borrows. In this condition, we could simply
+     ignore the children altogether. Instead, we explore them and make sure
+     we don't register values while doing so.
+  *)
+  let push_fail _ = raise (Failure "Unreachable") in
+  (* Function to explore an avalue and destructure it *)
+  let rec list_avalues (allow_borrows : bool) (push : V.typed_avalue -> unit)
+      (av : V.typed_avalue) : unit =
+    let ty = av.V.ty in
+    match av.V.value with
+    | V.APrimitive _ | ABottom | AIgnored -> ()
+    | AAdt adt ->
+        (* Simply explore the children *)
+        List.iter (list_avalues allow_borrows push) adt.field_values
+    | ALoan lc -> (
+        (* Explore the loan content *)
+        match lc with
+        | V.ASharedLoan (bids, sv, child_av) ->
+            (* We don't support nested borrows for now *)
+            assert (not (value_has_borrows ctx sv.V.value));
+            (* Push a value *)
+            let ignored = mk_aignored child_av.V.ty in
+            let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
+            push { V.value; ty };
+            (* Explore the child *)
+            list_avalues false push_fail child_av
+        | V.AMutLoan (bid, child_av) ->
+            let ignored = mk_aignored child_av.V.ty in
+            let value = V.ALoan (V.AMutLoan (bid, ignored)) in
+            push { V.value; ty };
+            (* Explore the child *)
+            list_avalues false push_fail child_av
+        | V.AEndedMutLoan
+            { child = child_av; given_back = _; given_back_meta = _ }
+        | V.AEndedSharedLoan (_, child_av)
+        | V.AIgnoredMutLoan (_, child_av)
+        | V.AEndedIgnoredMutLoan
+            { child = child_av; given_back = _; given_back_meta = _ }
+        | V.AIgnoredSharedLoan child_av ->
+            (* We don't support nested borrows for now *)
+            assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+            (* Simply explore the child *)
+            list_avalues false push_fail child_av)
+    | ABorrow bc -> (
+        (* Sanity check - rem.: may be redundant with [push_fail] *)
+        assert allow_borrows;
+        (* Explore the borrow content *)
+        match bc with
+        | V.AMutBorrow (mv, bid, child_av) ->
+            let ignored = mk_aignored child_av.V.ty in
+            let value = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in
+            push { V.value; ty };
+            (* Explore the child *)
+            list_avalues false push_fail child_av
+        | V.ASharedBorrow _ ->
+            (* Nothing specific to do: keep the value as it is *)
+            push av
+        | V.AIgnoredMutBorrow (_, child_av)
+        | V.AEndedIgnoredMutBorrow
+            { child = child_av; given_back_loans_proj = _; given_back_meta = _ }
+          ->
+            (* We don't support nested borrows for now *)
+            assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+            (* Just explore the child *)
+            list_avalues false push_fail child_av
+        | V.AProjSharedBorrow _ ->
+            (* Nothing specific to do: keep the value as it is *)
+            push_avalue av
+        | V.AEndedMutBorrow _ | V.AEndedSharedBorrow ->
+            (* If we get there it means the abstraction ended: it should not
+               be in the context anymore (if we end *one* borrow in an abstraction,
+               we have to end them all and remove the abstraction from the context)
+            *)
+            raise (Failure "Unreachable"))
+    | ASymbolic _ ->
+        (* For now, we fore all symbolic values containing borrows to be eagerly
+           expanded *)
+        assert (not (ty_has_borrows ctx.type_context.type_infos ty))
+  in
+  (* Destructure the avalues *)
+  List.iter (list_avalues true push_avalue) abs0.V.avalues;
+  let avalues = List.rev !avalues in
+  (* Update *)
+  { abs0 with V.avalues; kind = abs_kind; can_end }
+
+let abs_is_destructured (ctx : C.eval_ctx) (abs : V.abs) : bool =
+  let abs' = destructure_abs abs.kind abs.can_end ctx abs in
+  abs = abs'
+
+let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
+    (ctx : C.eval_ctx) (v : V.typed_value) : V.abs list =
+  (* Convert the value to a list of avalues *)
+  let absl = ref [] in
+  let push_abs (r_id : T.RegionId.id) (avalues : V.typed_avalue list) : unit =
+    if avalues = [] then ()
+    else
+      (* Reverse the list of avalues *)
+      let avalues = List.rev avalues in
+      (* Create the abs *)
+      let abs =
+        {
+          V.abs_id = C.fresh_abstraction_id ();
+          kind = abs_kind;
+          can_end;
+          parents = V.AbstractionId.Set.empty;
+          original_parents = [];
+          regions = T.RegionId.Set.singleton r_id;
+          ancestors_regions = T.RegionId.Set.empty;
+          avalues;
+        }
+      in
+      (* Add to the list of abstractions *)
+      absl := abs :: !absl
+  in
+
+  (* [group]: group in one abstraction (because we dived into a borrow/loan) *)
+  let rec to_avalues (allow_borrows : bool) (group : bool)
+      (r_id : T.RegionId.id) (v : V.typed_value) : V.typed_avalue list =
+    let ty = v.V.ty in
+    match v.V.value with
+    | V.Primitive _ -> []
+    | V.Bottom ->
+        (* Can happen: we *do* convert dummy values to abstractions, and dummy
+           values can contain bottoms *)
+        []
+    | V.Adt adt ->
+        (* Two cases, depending on whether we have to group all the borrows/loans
+           inside one abstraction or not *)
+        if group then
+          (* Convert to avalues, and transmit to the parent *)
+          List.concat
+            (List.map (to_avalues allow_borrows group r_id) adt.field_values)
+        else (
+          (* Create one abstraction per field, and transmit nothing to the parent *)
+          List.iter
+            (fun fv ->
+              let r_id = C.fresh_region_id () in
+              let values = to_avalues allow_borrows group r_id fv in
+              push_abs r_id values)
+            adt.field_values;
+          [])
+    | V.Borrow bc -> (
+        let _, ref_ty, kind = ty_as_ref ty in
+        (* Sanity check *)
+        assert allow_borrows;
+        (* Convert the borrow content *)
+        match bc with
+        | SharedBorrow (_, bid) ->
+            let ref_ty = ety_no_regions_to_rty ref_ty in
+            let ty = T.Ref (T.Var r_id, ref_ty, kind) in
+            let value = V.ABorrow (V.ASharedBorrow bid) in
+            [ { V.value; ty } ]
+        | MutBorrow (bid, bv) ->
+            let r_id = if group then r_id else C.fresh_region_id () in
+            (* We don't support nested borrows for now *)
+            assert (not (value_has_borrows ctx bv.V.value));
+            (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+            let mv = bv in
+            let ref_ty = ety_no_regions_to_rty ref_ty in
+            let ty = T.Ref (T.Var r_id, ref_ty, kind) in
+            let ignored = mk_aignored ref_ty in
+            let value = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in
+            let value = { V.value; ty } in
+            (* Continue exploring, looking for loans (and forbidding borrows,
+               because we don't support nested borrows for now) *)
+            value :: to_avalues false true r_id bv
+        | ReservedMutBorrow _ ->
+            (* This borrow should have been activated *)
+            raise (Failure "Unexpected"))
+    | V.Loan lc -> (
+        match lc with
+        | V.SharedLoan (bids, sv) ->
+            let r_id = if group then r_id else C.fresh_region_id () in
+            (* We don't support nested borrows for now *)
+            assert (not (value_has_borrows ctx sv.V.value));
+            (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+            let ty = ety_no_regions_to_rty ty in
+            let ignored = mk_aignored ty in
+            let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
+            let value = { V.value; ty } in
+            (* Continue exploring, looking for loans (and forbidding borrows,
+               because we don't support nested borrows for now) *)
+            value :: to_avalues false true r_id sv
+        | V.MutLoan bid ->
+            (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+            let ty = ety_no_regions_to_rty ty in
+            let ignored = mk_aignored ty in
+            let value = V.ALoan (V.AMutLoan (bid, ignored)) in
+            [ { V.value; ty } ])
+    | V.Symbolic _ ->
+        (* For now, we force all the symbolic values containing borrows to
+           be eagerly expanded *)
+        (* We don't support nested borrows for now *)
+        assert (not (value_has_borrows ctx v.V.value));
+        (* Return nothing *)
+        []
+  in
+  (* Generate the avalues *)
+  let r_id = C.fresh_region_id () in
+  let values = to_avalues true false r_id v in
+  (* Introduce an abstraction for the returned values *)
+  push_abs r_id values;
+  (* Return *)
+  List.rev !absl
+
+let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
+    (ctx : C.eval_ctx) (abs0 : V.abs) (abs1 : V.abs) : V.abs =
+  (* Check that the abstractions are destructured *)
+  if !Config.check_invariants then (
+    assert (abs_is_destructured ctx abs0);
+    assert (abs_is_destructured ctx abs1));
+
+  (* Visit the abstractions, list their borrows and loans *)
+  let borrows = ref V.BorrowId.Set.empty in
+  let loans = ref V.BorrowId.Set.empty in
+
+  let push_loans ids = loans := V.BorrowId.Set.union !loans ids in
+  let push_loan id = loans := V.BorrowId.Set.add id !loans in
+  let push_borrow id = borrows := V.BorrowId.Set.add id !borrows in
+
+  let iter_avalues =
+    object
+      inherit [_] V.iter_typed_avalue as super
+
+      method! visit_loan_content env lc =
+        (* Can happen if we explore shared values whose sub-values are
+           reborrowed *)
+        (match lc with
+        | SharedLoan (bids, _) -> push_loans bids
+        | MutLoan _ -> raise (Failure "Unreachable"));
+        (* Continue *)
+        super#visit_loan_content env lc
+
+      method! visit_borrow_content _ _ =
+        (* Can happen if we explore shared values which contain borrows -
+           i.e., if we have nested borrows (we forbid this for now) *)
+        raise (Failure "Unreachable")
+
+      method! visit_aloan_content env lc =
+        (* Register the loans *)
+        (match lc with
+        | V.ASharedLoan (bids, _, _) -> push_loans bids
+        | V.AMutLoan (bid, _) -> push_loan bid
+        | V.AEndedMutLoan _ | V.AEndedSharedLoan _ | V.AIgnoredMutLoan _
+        | V.AEndedIgnoredMutLoan _ | V.AIgnoredSharedLoan _ ->
+            (* The abstraction has been destructured, so those shouldn't appear *)
+            raise (Failure "Unreachable"));
+        (* Continue *)
+        super#visit_aloan_content env lc
+
+      method! visit_aborrow_content env bc =
+        (* Explore the borrow content *)
+        (match bc with
+        | V.AMutBorrow (_, bid, _) -> push_borrow bid
+        | V.ASharedBorrow bid -> push_borrow bid
+        | V.AProjSharedBorrow asb ->
+            let register asb =
+              match asb with
+              | V.AsbBorrow bid -> push_borrow bid
+              | V.AsbProjReborrows _ ->
+                  (* Can only happen if the symbolic value (potentially) contains
+                     borrows - i.e., we have nested borrows *)
+                  raise (Failure "Unreachable")
+            in
+            List.iter register asb
+        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
+        | V.AEndedMutBorrow _ | V.AEndedSharedBorrow ->
+            (* The abstraction has been destructured, so those shouldn't appear *)
+            raise (Failure "Unreachable"));
+        super#visit_aborrow_content env bc
+
+      method! visit_symbolic_value _ _ =
+        (* Sanity check *)
+        raise (Failure "Unrechable")
+    end
+  in
+
+  List.iter (iter_avalues#visit_typed_avalue ()) abs0.V.avalues;
+  List.iter (iter_avalues#visit_typed_avalue ()) abs1.V.avalues;
+
+  (* List the values, ignoring the loans/borrows which whose associated
+     borrows/loans are in the other abstraction already - note that we
+     take advantage of the fact that the values are destructured.
+
+     We convert the loans/borrows we want to ignore to [Ignored] values,
+     then filter them.
+  *)
+  let intersect = V.BorrowId.Set.inter !loans !borrows in
+  let filter_bids (bids : V.BorrowId.Set.t) : V.BorrowId.Set.t option =
+    let bids = V.BorrowId.Set.diff bids intersect in
+    if V.BorrowId.Set.is_empty bids then None else Some bids
+  in
+  let filter_bid (bid : V.BorrowId.id) : V.BorrowId.id option =
+    if V.BorrowId.Set.mem bid intersect then None else Some bid
+  in
+
+  let map_avalues =
+    object (self : 'self)
+      inherit [_] V.map_typed_avalue as super
+
+      method! visit_Loan env lc =
+        (* Can happen if we explore shared values whose sub-values are
+           reborrowed *)
+        match lc with
+        | SharedLoan (bids, sv) -> (
+            match filter_bids bids with
+            | None -> (self#visit_typed_value env sv).V.value
+            | Some bids -> super#visit_Loan env (SharedLoan (bids, sv)))
+        | MutLoan _ -> raise (Failure "Unreachable")
+
+      method! visit_borrow_content _ _ =
+        (* Can happen if we explore shared values which contain borrows -
+           i.e., if we have nested borrows (we forbid this for now) *)
+        raise (Failure "Unreachable")
+
+      method! visit_ALoan env lc =
+        (* Register the loans *)
+        match lc with
+        | V.ASharedLoan (bids, sv, asv) -> (
+            match filter_bids bids with
+            | None ->
+                let sv = super#visit_typed_value env sv in
+                assert (is_aignored asv.V.value);
+                (* Check if the shared value contains loans or borrows - rem.: there shouldn't
+                   be borrows actually, because for now we forbid nested borrows.
+
+                   If it doesn't, we can ignore the value altogether.
+                *)
+                if
+                  loans_in_value sv
+                  || ty_has_borrows ctx.type_context.type_infos sv.V.ty
+                then
+                  (* The value is not shared anymore, but it contains shared sub-values.
+
+                     It would be good to deconstruct the sub-values. For now, let's fail
+                     (rem.: it would be sound to have a shared aloan with an empty set
+                     of borrow ids).
+                  *)
+                  raise (Failure "Unimplemented")
+                else V.AIgnored
+            | Some bids -> super#visit_ALoan env (ASharedLoan (bids, sv, asv)))
+        | V.AMutLoan (bid, child) -> (
+            assert (is_aignored child.V.value);
+            match filter_bid bid with
+            | None -> V.AIgnored
+            | Some _ -> super#visit_ALoan env lc)
+        | V.AEndedMutLoan _ | V.AEndedSharedLoan _ | V.AIgnoredMutLoan _
+        | V.AEndedIgnoredMutLoan _ | V.AIgnoredSharedLoan _ ->
+            (* The abstraction has been destructured, so those shouldn't appear *)
+            raise (Failure "Unreachable")
+
+      method! visit_ABorrow env bc =
+        (* Explore the borrow content *)
+        match bc with
+        | V.AMutBorrow (_, bid, child) -> (
+            assert (is_aignored child.V.value);
+            match filter_bid bid with
+            | None -> V.AIgnored
+            | Some _ -> super#visit_ABorrow env bc)
+        | V.ASharedBorrow bid -> (
+            match filter_bid bid with
+            | None -> V.AIgnored
+            | Some _ -> super#visit_ABorrow env bc)
+        | V.AProjSharedBorrow asb ->
+            let filter asb =
+              match asb with
+              | V.AsbBorrow bid -> (
+                  match filter_bid bid with None -> None | Some _ -> Some asb)
+              | V.AsbProjReborrows _ ->
+                  (* Can only happen if the symbolic value (potentially) contains
+                     borrows - i.e., we have nested borrows *)
+                  raise (Failure "Unreachable")
+            in
+            let asb = List.filter_map filter asb in
+            V.ABorrow (V.AProjSharedBorrow asb)
+        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
+        | V.AEndedMutBorrow _ | V.AEndedSharedBorrow ->
+            (* The abstraction has been destructured, so those shouldn't appear *)
+            raise (Failure "Unreachable")
+
+      method! visit_symbolic_value _ _ =
+        (* Sanity check *)
+        raise (Failure "Unrechable")
+    end
+  in
+
+  (* Apply the transformation *)
+  let avalues =
+    List.map
+      (map_avalues#visit_typed_avalue ())
+      (List.append abs0.avalues abs1.avalues)
+  in
+
+  (* Filter the ignored values *)
+  let avalues =
+    List.filter (fun (v : V.typed_avalue) -> not (is_aignored v.value)) avalues
+  in
+
+  (* Create the new abstraction *)
+  let abs_id = C.fresh_abstraction_id () in
+  (* Note that one of the two abstractions might a parent of the other *)
+  let parents =
+    V.AbstractionId.Set.diff
+      (V.AbstractionId.Set.union abs0.parents abs1.parents)
+      (V.AbstractionId.Set.of_list [ abs0.abs_id; abs1.abs_id ])
+  in
+  let original_parents = V.AbstractionId.Set.elements parents in
+  let regions = T.RegionId.Set.union abs0.regions abs1.regions in
+  let ancestors_regions =
+    T.RegionId.Set.diff (T.RegionId.Set.union abs0.regions abs1.regions) regions
+  in
+  let abs =
+    {
+      V.abs_id;
+      kind = abs_kind;
+      can_end;
+      parents;
+      original_parents;
+      regions;
+      ancestors_regions;
+      avalues;
+    }
+  in
+  (* Sanity check *)
+  if !Config.check_invariants then assert (abs_is_destructured ctx abs);
+  (* Return *)
+  abs
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index f21fdcd5..a1a8fb0c 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -30,6 +30,13 @@ val end_abstraction : C.config -> V.AbstractionId.id -> cm_fun
 (** End a set of abstractions while preserving the invariants. *)
 val end_abstractions : C.config -> V.AbstractionId.Set.t -> cm_fun
 
+(** End a borrow and return the resulting environment, ignoring synthesis *)
+val end_borrow_no_synth : C.config -> V.BorrowId.id -> C.eval_ctx -> C.eval_ctx
+
+(** End an abstraction and return the resulting environment, ignoring synthesis *)
+val end_abstraction_no_synth :
+  C.config -> V.AbstractionId.id -> C.eval_ctx -> C.eval_ctx
+
 (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants.
 
     Reserved borrows are special mutable borrows which are created as shared borrows
@@ -40,3 +47,85 @@ val end_abstractions : C.config -> V.AbstractionId.Set.t -> cm_fun
     other shared borrows which point to this loan).
  *)
 val promote_reserved_mut_borrow : C.config -> V.BorrowId.id -> cm_fun
+
+(** Transform an abstraction to an abstraction where the values are not
+    structured.
+
+    For instance:
+    {[
+      abs {
+        (mut_borrow l0, mut_borrow l1, _)
+      }
+
+          ~~>
+
+      abs {
+        mut_borrow l0
+        mut_borrow l1
+      }
+    ]}
+
+    Rem.: we do this to simplify the merging of abstractions. We can do this
+    because for now, we don't support nested borrows.
+
+    Paramters:
+    - [abs_kind]
+    - [can_end]
+    - [ctx]
+    - [abs]
+ *)
+val destructure_abs : V.abs_kind -> bool -> C.eval_ctx -> V.abs -> V.abs
+
+(** Return [true] if the values in an abstraction are destructured.
+
+    We simply destructure it and check that it gives the identity.
+ *)
+val abs_is_destructured : C.eval_ctx -> V.abs -> bool
+
+(** Turn a value into a abstractions.
+
+    We are conservative, and don't group borrows/loans into the same abstraction
+    unless necessary.
+
+    For instance:
+    {[
+      _ -> (mut_borrow l1 (mut_loan l2), mut_borrow l3)
+
+      ~~>
+
+      abs'0 { mut_borrow l1, mut_loan l2 }
+      abs'1 { mut_borrow l3 }
+    ]}
+
+    Parameters:
+    - [abs_kind]
+    - [can_end]
+    - [ctx]
+    - [v]
+ *)
+val convert_value_to_abstractions :
+  V.abs_kind -> bool -> C.eval_ctx -> V.typed_value -> V.abs list
+
+(** Merge two abstractions together.
+
+    Merging two abstractions together implies removing the loans/borrows
+    which appear in one and whose associated loans/borrows appear in the
+    other. For instance:
+    {[
+      abs'0 { mut_borrow l0, mut_loan l1 }
+      abs'1 { mut_borrow l1, mut_borrow l2 }
+
+          ~~>
+
+      abs'01 { mut_borrow l0, mut_borrow l2 }
+    ]}
+
+    Parameters:
+    - [kind]
+    - [can_end]
+    - [ctx]
+    - [abs0]
+    - [abs1]
+ *)
+val merge_abstractions :
+  V.abs_kind -> bool -> C.eval_ctx -> V.abs -> V.abs -> V.abs
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index d3be1bed..8d23e4da 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -182,6 +182,28 @@ let projection_contains (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty)
   in
   compare_rtys default combine compare_regions ty1 ty2
 
+(** Compute the set of borrow ids, loan ids and abstraction ids in a context. *)
+let compute_borrow_abs_ids_in_context (ctx : C.eval_ctx) :
+    V.BorrowId.Set.t * V.AbstractionId.Set.t =
+  let bids = ref V.BorrowId.Set.empty in
+  let aids = ref V.AbstractionId.Set.empty in
+  let obj =
+    object
+      inherit [_] C.iter_eval_ctx
+      method! visit_borrow_id _ id = bids := V.BorrowId.Set.add id !bids
+
+      method! visit_loan_id _ id =
+        (* Actually, this is not necessary because all loans have a
+           corresponding borrow *)
+        bids := V.BorrowId.Set.add id !bids
+
+      method! visit_abstraction_id _ id =
+        aids := V.AbstractionId.Set.add id !aids
+    end
+  in
+  obj#visit_eval_ctx () ctx;
+  (!bids, !aids)
+
 (** Lookup a loan content.
 
     The loan is referred to by a borrow id.
@@ -704,7 +726,7 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
       inherit [_] C.iter_eval_ctx as super
       method! visit_abs _ abs = super#visit_abs (Some abs) abs
 
-      method! visit_abstract_shared_borrows abs asb =
+      method! visit_abstract_shared_borrow abs asb =
         (* Sanity check *)
         (match !found with
         | Some (NonSharedProj _) -> raise (Failure "Unreachable")
@@ -712,14 +734,11 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
         (* Explore *)
         if lookup_shared then
           let abs = Option.get abs in
-          let check asb =
-            match asb with
-            | V.AsbBorrow _ -> ()
-            | V.AsbProjReborrows (sv', proj_ty) ->
-                let is_shared = true in
-                check_add_proj_borrows is_shared abs sv' proj_ty
-          in
-          List.iter check asb
+          match asb with
+          | V.AsbBorrow _ -> ()
+          | V.AsbProjReborrows (sv', proj_ty) ->
+              let is_shared = true in
+              check_add_proj_borrows is_shared abs sv' proj_ty
         else ()
 
       method! visit_aproj abs sproj =
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
new file mode 100644
index 00000000..702420cd
--- /dev/null
+++ b/compiler/InterpreterLoops.ml
@@ -0,0 +1,521 @@
+module T = Types
+module PV = PrimitiveValues
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module A = LlbcAst
+module L = Logging
+open TypesUtils
+open ValuesUtils
+module Inv = Invariants
+module S = SynthesizeSymbolic
+module UF = UnionFind
+open Utils
+open Cps
+open InterpreterUtils
+open InterpreterBorrows
+open InterpreterProjectors
+open InterpreterExpansion
+open InterpreterPaths
+open InterpreterExpressions
+
+(** The local logger *)
+let log = L.loops_log
+
+type cnt_thresholds = {
+  aid : V.AbstractionId.id;
+  sid : V.SymbolicValueId.id;
+  bid : V.BorrowId.id;
+  did : C.DummyVarId.id;
+}
+
+(** Union Find *)
+module UnionFind = UF.Make (UF.StoreMap)
+
+(** A small utility *)
+type abs_borrows_loans_maps = {
+  abs_ids : V.AbstractionId.id list;
+  abs_to_borrows : V.BorrowId.Set.t V.AbstractionId.Map.t;
+  abs_to_loans : V.BorrowId.Set.t V.AbstractionId.Map.t;
+  borrow_to_abs : V.AbstractionId.id V.BorrowId.Map.t;
+  loan_to_abs : V.AbstractionId.id V.BorrowId.Map.t;
+}
+
+(** Compute various maps linking the abstractions and the borrows/loans they contain.
+
+    The [explore] function is used to filter abstractions.
+ *)
+let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) :
+    abs_borrows_loans_maps =
+  let abs_ids = ref [] in
+  let abs_to_borrows = ref V.AbstractionId.Map.empty in
+  let abs_to_loans = ref V.AbstractionId.Map.empty in
+  let borrow_to_abs = ref V.BorrowId.Map.empty in
+  let loan_to_abs = ref V.BorrowId.Map.empty in
+
+  let register_borrow_id abs_id bid =
+    abs_to_borrows :=
+      V.AbstractionId.Map.update abs_id
+        (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids)))
+        !abs_to_borrows;
+    assert (not (V.BorrowId.Map.mem bid !borrow_to_abs));
+    borrow_to_abs := V.BorrowId.Map.add bid abs_id !borrow_to_abs
+  in
+
+  let register_loan_id abs_id bid =
+    abs_to_loans :=
+      V.AbstractionId.Map.update abs_id
+        (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids)))
+        !abs_to_loans;
+    assert (not (V.BorrowId.Map.mem bid !loan_to_abs));
+    loan_to_abs := V.BorrowId.Map.add bid abs_id !loan_to_abs
+  in
+
+  let explore_abs =
+    object (self : 'self)
+      inherit [_] V.iter_typed_avalue as super
+
+      (** Make sure we don't register the ignored ids *)
+      method! visit_aloan_content abs_id lc =
+        match lc with
+        | AMutLoan _ | ASharedLoan _ ->
+            (* Process those normally *)
+            super#visit_aloan_content abs_id lc
+        | AIgnoredMutLoan (_, child)
+        | AEndedIgnoredMutLoan { child; given_back = _; given_back_meta = _ }
+        | AIgnoredSharedLoan child ->
+            (* Ignore the id of the loan, if there is *)
+            self#visit_typed_avalue abs_id child
+        | AEndedMutLoan _ | AEndedSharedLoan _ -> raise (Failure "Unreachable")
+
+      (** Make sure we don't register the ignored ids *)
+      method! visit_aborrow_content abs_id bc =
+        match bc with
+        | AMutBorrow _ | ASharedBorrow _ | AProjSharedBorrow _ ->
+            (* Process those normally *)
+            super#visit_aborrow_content abs_id bc
+        | AIgnoredMutBorrow (_, child)
+        | AEndedIgnoredMutBorrow
+            { child; given_back_loans_proj = _; given_back_meta = _ } ->
+            (* Ignore the id of the borrow, if there is *)
+            self#visit_typed_avalue abs_id child
+        | AEndedMutBorrow _ | AEndedSharedBorrow ->
+            raise (Failure "Unreachable")
+
+      method! visit_borrow_id abs_id bid = register_borrow_id abs_id bid
+      method! visit_loan_id abs_id lid = register_loan_id abs_id lid
+    end
+  in
+
+  List.iter
+    (fun (ee : C.env_elem) ->
+      match ee with
+      | Var _ | Frame -> ()
+      | Abs abs ->
+          let abs_id = abs.abs_id in
+          if explore abs then (
+            abs_to_borrows :=
+              V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty
+                !abs_to_borrows;
+            abs_to_loans :=
+              V.AbstractionId.Map.add abs_id V.BorrowId.Set.empty !abs_to_loans;
+            abs_ids := abs.abs_id :: !abs_ids;
+            List.iter (explore_abs#visit_typed_avalue abs.abs_id) abs.avalues)
+          else ())
+    env;
+
+  {
+    abs_ids = List.rev !abs_ids;
+    abs_to_borrows = !abs_to_borrows;
+    abs_to_loans = !abs_to_loans;
+    borrow_to_abs = !borrow_to_abs;
+    loan_to_abs = !loan_to_abs;
+  }
+
+(** Collapse an environment.
+
+    We do this to simplify an environment, for the purpose of finding a loop
+    fixed point.
+
+    We do the following:
+    - we look for all the *new* dummy values (we use id thresholds to decide
+      wether a value is new or not - the ids generated by our counters are
+      monotonic), and we convert to abstractions (if they contain loans or
+      borrows)
+    - whenever there is a new abstraction in the context, and some of its
+      its borrows are associated to loans in another new abstraction, we
+      merge them.
+    In effect, this allows us to merge newly introduced abstractions/borrows
+    with their parent abstractions.
+ *)
+let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
+    (ctx0 : C.eval_ctx) : C.eval_ctx =
+  let abs_kind = V.Loop loop_id in
+  let can_end = true in
+  let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
+    V.AbstractionId.Ord.compare thresh.aid id >= 0
+  in
+  let is_fresh_did (id : C.DummyVarId.id) : bool =
+    C.DummyVarId.Ord.compare thresh.did id >= 0
+  in
+  (* Convert the dummy values to abstractions *)
+  (* Note that we preserve the order of the dummy values: we replace them with
+     abstractions in place - this makes matching easier *)
+  let env =
+    List.concat
+      (List.map
+         (fun ee ->
+           match ee with
+           | C.Abs _ | C.Frame | C.Var (VarBinder _, _) -> [ ee ]
+           | C.Var (DummyBinder id, v) ->
+               if is_fresh_did id then
+                 let absl =
+                   convert_value_to_abstractions abs_kind can_end ctx0 v
+                 in
+                 List.map (fun abs -> C.Abs abs) absl
+               else [ ee ])
+         ctx0.env)
+  in
+
+  (* Explore all the *new* abstractions, and compute various maps *)
+  let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in
+  let ids_maps = compute_abs_borrows_loans_maps explore env in
+  let {
+    abs_ids;
+    abs_to_borrows;
+    abs_to_loans = _;
+    borrow_to_abs = _;
+    loan_to_abs;
+  } =
+    ids_maps
+  in
+
+  (* Use the maps to merge the abstractions together *)
+  let merged_abs : V.AbstractionId.id UF.elem V.AbstractionId.Map.t =
+    V.AbstractionId.Map.of_list (List.map (fun id -> (id, UF.make id)) abs_ids)
+  in
+
+  let ctx = ref { ctx0 with C.env } in
+
+  (* Merge all the mergeable abs.
+
+     We iterate over the abstractions, then over the borrows in the abstractions.
+     We do this because we want to control the order in which abstractions
+     are merged (the ids are iterated in increasing order). Otherwise, we
+     could simply iterate over all the borrows in [borrow_to_abs]...
+  *)
+  List.iter
+    (fun abs_id0 ->
+      let bids = V.AbstractionId.Map.find abs_id0 abs_to_borrows in
+      let bids = V.BorrowId.Set.elements bids in
+      List.iter
+        (fun bid ->
+          match V.BorrowId.Map.find_opt bid loan_to_abs with
+          | None -> (* Nothing to do *) ()
+          | Some abs_id1 ->
+              (* We need to merge - unless we have already merged *)
+              (* First, find the representatives for the two abstractions (the
+                 representative is the abstraction into which we merged) *)
+              let abs_ref0 =
+                UF.find (V.AbstractionId.Map.find abs_id0 merged_abs)
+              in
+              let abs_id0 = UF.get abs_ref0 in
+              let abs_ref1 =
+                UF.find (V.AbstractionId.Map.find abs_id1 merged_abs)
+              in
+              let abs_id1 = UF.get abs_ref1 in
+              (* If the two ids are the same, it means the abstractions were already merged *)
+              if abs_id0 = abs_id1 then ()
+              else
+                (* We actually need to merge the abstractions *)
+                (* Lookup the abstractions *)
+                let abs0 = C.ctx_lookup_abs !ctx abs_id0 in
+                let abs1 = C.ctx_lookup_abs !ctx abs_id1 in
+                (* Merge them - note that we take care to merge [abs0] into [abs1]
+                   (the order is important).
+                *)
+                let nabs = merge_abstractions abs_kind can_end !ctx abs1 abs0 in
+                (* Update the environment *)
+                ctx := fst (C.ctx_subst_abs !ctx abs_id1 nabs);
+                ctx := fst (C.ctx_remove_abs !ctx abs_id0);
+                (* Update the union find *)
+                let abs_ref_merged = UF.union abs_ref0 abs_ref1 in
+                UF.set abs_ref_merged nabs.abs_id)
+        bids)
+    abs_ids;
+
+  (* Return the new context *)
+  !ctx
+
+(* TODO: document.
+   TODO: we might not use the bounds properly, use sets instead.
+*)
+type match_ctx = {
+  ctx : C.eval_ctx;
+  aids : V.AbstractionId.Set.t;
+  sids : V.SymbolicValueId.Set.t;
+  bids : V.BorrowId.Set.t;
+}
+
+let mk_match_ctx (ctx : C.eval_ctx) : match_ctx =
+  let aids = V.AbstractionId.Set.empty in
+  let sids = V.SymbolicValueId.Set.empty in
+  let bids = V.BorrowId.Set.empty in
+  { ctx; aids; sids; bids }
+
+type joined_ctx_or_update =
+  | EndAbs of V.AbstractionId.id
+  | EndBorrow of V.BorrowId.id
+  | JoinedCtx of match_ctx
+
+(** Merge a borrow with the abstraction containing the associated loan, where
+    the abstraction must be a *loop abstraction* (we don't synthesize code during
+    the operation).
+
+    For instance:
+    {[
+      abs'0 { mut_loan l0 }
+      x -> mut_borrow l0 sx
+
+            ~~>
+
+      abs'0 {}
+      x -> ⊥
+    ]}
+ *)
+let merge_borrow_with_parent_loop_abs (config : C.config) (bid : V.BorrowId.id)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* TODO: use the function from InterpreterBorrows *)
+  failwith "Unimplemented"
+(* (* Lookup the borrow *)
+     let ek =
+       { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
+     in
+     (* TODO: use [end_borrow_get_borrow]? *)
+     match lookup_borrow ek bid ctx with
+     | None -> ctx
+   | Some b -> failwith "Unimplemented"*)
+
+(** See {!merge_borrow_with_parent_loop_abs} *)
+let rec merge_borrows_with_parent_loop_abs (config : C.config)
+    (bids : V.BorrowId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
+  V.BorrowId.Set.fold
+    (fun id ctx -> merge_borrow_with_parent_loop_abs config id ctx)
+    bids ctx
+
+(* TODO: we probably don't need an [match_ctx], and actually we might not use
+   the bounds propertly.
+*)
+let match_ctx_with_target (config : C.config) (tgt_mctx : match_ctx) : cm_fun =
+ fun cf src_ctx ->
+  (* We first reorganize [ctx] so that we can match it with [tgt_mctx] *)
+  (* First, collect all the borrows and abstractions which are in [ctx]
+     and not in [tgt_mctx]: we need to end them *)
+  let src_bids, src_aids =
+    InterpreterBorrowsCore.compute_borrow_abs_ids_in_context src_ctx
+  in
+  let tgt_bids, tgt_aids =
+    InterpreterBorrowsCore.compute_borrow_abs_ids_in_context tgt_mctx.ctx
+  in
+  let bids = V.BorrowId.Set.diff src_bids tgt_bids in
+  let aids = V.AbstractionId.Set.diff src_aids tgt_aids in
+  (* End those borrows and abstractions *)
+  let cc = InterpreterBorrows.end_borrows config bids in
+  let cc = comp cc (InterpreterBorrows.end_abstractions config aids) in
+  (* In the target context, merge all the borrows introduced by the loop with
+     their parent abstractions
+  *)
+  let tgt_ctx =
+    merge_borrows_with_parent_loop_abs config
+      (V.BorrowId.Set.diff tgt_bids src_bids)
+      tgt_mctx.ctx
+  in
+  (* Replace the source context with the target context - TODO: explain
+     why this works *)
+  let cf_apply_match : cm_fun = fun cf _ -> cf tgt_ctx in
+  let cc = comp cc cf_apply_match in
+  (* Sanity check on the resulting context *)
+  let cc = comp_check_ctx cc Inv.check_invariants in
+  (* Apply and continue *)
+  cc cf src_ctx
+
+(** Join a context at the entry of a loop with a context upon reaching
+    a continue in this loop.
+ *)
+let loop_join_entry_ctx_with_continue_ctx (ctx0 : match_ctx) (ctx1 : C.eval_ctx)
+    : joined_ctx_or_update =
+  failwith "Unimplemented"
+
+(** See {!loop_join_entry_ctx_with_continue_ctx} *)
+let rec loop_join_entry_ctx_with_continue_ctxs (ctx0 : match_ctx)
+    (ctxs : C.eval_ctx list) : joined_ctx_or_update =
+  match ctxs with
+  | [] -> JoinedCtx ctx0
+  | ctx1 :: ctxs -> (
+      let res = loop_join_entry_ctx_with_continue_ctx ctx0 ctx1 in
+      match res with
+      | EndAbs _ | EndBorrow _ -> res
+      | JoinedCtx ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs)
+
+let compute_loop_entry_fixed_point (config : C.config)
+    (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : match_ctx =
+  (* The continuation for when we exit the loop - we use it to register the
+     environments upon loop *reentry*
+  *)
+  let ctxs = ref [] in
+  let register_ctx ctx = ctxs := ctx :: !ctxs in
+  let cf_exit_loop_body (res : statement_eval_res) : m_fun =
+   fun ctx ->
+    match res with
+    | Return | Panic | Break _ -> None
+    | Unit ->
+        (* See the comment in {!eval_loop} *)
+        raise (Failure "Unreachable")
+    | Continue i ->
+        (* For now we don't support continues to outer loops *)
+        assert (i = 0);
+        register_ctx ctx;
+        None
+    | EndEnterLoop | EndContinue ->
+        (* We don't support nested loops for now *)
+        raise (Failure "Nested loops are not supported for now")
+  in
+  (* Join the contexts at the loop entry *)
+  (* TODO: return result:
+   * - end borrows in ctx0
+   * - ok: return joined env
+   * TODO: keep initial env somewhere?
+   * TODO: the returned env is an eval_ctx or smth else?
+   * Maybe simply keep track of existentially quantified variables?
+   *)
+  let join_ctxs (ctx0 : match_ctx) : joined_ctx_or_update =
+    let ctx1 = loop_join_entry_ctx_with_continue_ctxs ctx0 !ctxs in
+    ctxs := [];
+    ctx1
+  in
+  (* Check if two contexts are equivalent - modulo alpha conversion on the
+     existentially quantified borrows/abstractions/symbolic values *)
+  let equiv_ctxs (_ctx1 : match_ctx) (_ctx2 : match_ctx) : bool =
+    failwith "Unimplemented"
+  in
+  let max_num_iter = Config.loop_fixed_point_max_num_iters in
+  let rec compute_fixed_point (mctx : match_ctx) (i : int) : match_ctx =
+    if i = 0 then
+      raise
+        (Failure
+           ("Could not compute a loop fixed point in "
+          ^ string_of_int max_num_iter ^ " iterations"))
+    else
+      (* The join on the environments may fail if we need to end some borrows/abstractions
+         in the original context first: reorganize the original environment for as
+         long as we need to *)
+      let rec eval_iteration_then_join (mctx : match_ctx) =
+        (* Evaluate the loop body *)
+        let _ = eval_loop_body cf_exit_loop_body mctx.ctx in
+        (* Check if the join succeeded, or if we need to end abstractions/borrows
+           in the original environment first *)
+        match join_ctxs mctx with
+        | EndAbs id ->
+            let ctx1 =
+              InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx
+            in
+            eval_iteration_then_join { mctx with ctx = ctx1 }
+        | EndBorrow id ->
+            let ctx1 =
+              InterpreterBorrows.end_borrow_no_synth config id mctx.ctx
+            in
+            eval_iteration_then_join { mctx with ctx = ctx1 }
+        | JoinedCtx mctx1 ->
+            (* The join succeeded: check if we reached a fixed point, otherwise
+               iterate *)
+            if equiv_ctxs mctx mctx1 then mctx1
+            else compute_fixed_point mctx1 (i - 1)
+      in
+      eval_iteration_then_join mctx
+  in
+  compute_fixed_point (mk_match_ctx ctx0) max_num_iter
+
+(** Evaluate a loop in concrete mode *)
+let eval_loop_concrete (config : C.config) (eval_loop_body : st_cm_fun) :
+    st_cm_fun =
+ fun cf ctx ->
+  (* Continuation for after we evaluate the loop body: depending the result
+     of doing one loop iteration:
+     - redoes a loop iteration
+     - exits the loop
+     - other...
+
+     We need a specific function because of the {!Continue} case: in case we
+     continue, we might have to reevaluate the current loop body with the
+     new context (and repeat this an indefinite number of times).
+  *)
+  let rec reeval_loop_body (res : statement_eval_res) : m_fun =
+    match res with
+    | Return | Panic -> cf res
+    | Break i ->
+        (* Break out of the loop by calling the continuation *)
+        let res = if i = 0 then Unit else Break (i - 1) in
+        cf res
+    | Continue 0 ->
+        (* Re-evaluate the loop body *)
+        eval_loop_body reeval_loop_body
+    | Continue i ->
+        (* Continue to an outer loop *)
+        cf (Continue (i - 1))
+    | Unit ->
+        (* We can't get there.
+         * Note that if we decide not to fail here but rather do
+         * the same thing as for [Continue 0], we could make the
+         * code slightly simpler: calling {!reeval_loop_body} with
+         * {!Unit} would account for the first iteration of the loop.
+         * We prefer to write it this way for consistency and sanity,
+         * though. *)
+        raise (Failure "Unreachable")
+    | EndEnterLoop | EndContinue ->
+        (* We can't get there: this is only used in symbolic mode *)
+        raise (Failure "Unreachable")
+  in
+
+  (* Apply *)
+  eval_loop_body reeval_loop_body ctx
+
+(** Evaluate a loop in symbolic mode *)
+let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
+    st_cm_fun =
+ fun cf ctx ->
+  (* Compute the fixed point at the loop entrance *)
+  let mctx = compute_loop_entry_fixed_point config eval_loop_body ctx in
+  (* Synthesize the end of the function *)
+  let end_expr = match_ctx_with_target config mctx (cf EndEnterLoop) ctx in
+  (* Synthesize the loop body by evaluating it, with the continuation for
+     after the loop starting at the *fixed point*, but with a special
+     treatment for the [Break] and [Continue] cases *)
+  let cf_loop : st_m_fun =
+   fun res ctx ->
+    match res with
+    | Return | Panic -> cf res ctx
+    | Break i ->
+        (* Break out of the loop by calling the continuation *)
+        let res = if i = 0 then Unit else Break (i - 1) in
+        cf res ctx
+    | Continue i ->
+        (* We don't support nested loops for now *)
+        assert (i = 0);
+        match_ctx_with_target config mctx (cf EndContinue) ctx
+    | Unit | EndEnterLoop | EndContinue ->
+        (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
+           For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
+        *)
+        raise (Failure "Unreachable")
+  in
+  let loop_expr = eval_loop_body cf_loop mctx.ctx in
+  (* Put together *)
+  S.synthesize_loop end_expr loop_expr
+
+(** Evaluate a loop *)
+let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun =
+ fun cf ctx ->
+  match config.C.mode with
+  | ConcreteMode -> eval_loop_concrete config eval_loop_body cf ctx
+  | SymbolicMode -> eval_loop_symbolic config eval_loop_body cf ctx
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 3bf7b723..5f74d1a7 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -683,8 +683,8 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
     [region_can_end]: gives the region groups from which we generate functions
     which can end or not.
  *)
-let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
-    (kind : V.abs_kind) (rgl : A.abs_region_group list)
+let create_empty_abstractions_from_abs_region_groups
+    (kind : T.RegionGroupId.id -> V.abs_kind) (rgl : A.abs_region_group list)
     (region_can_end : T.RegionGroupId.id -> bool) : 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]
@@ -696,8 +696,8 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
     ref V.AbstractionId.Map.empty
   in
   (* Auxiliary function to create one abstraction *)
-  let create_abs (back_id : T.RegionGroupId.id) (rg : A.abs_region_group) :
-      V.abs =
+  let create_abs (rg_id : T.RegionGroupId.id) (rg : A.abs_region_group) : V.abs
+      =
     let abs_id = rg.T.id in
     let original_parents = rg.parents in
     let parents =
@@ -720,16 +720,14 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
     let ancestors_regions_union_current_regions =
       T.RegionId.Set.union ancestors_regions regions
     in
-    let can_end = region_can_end back_id in
+    let can_end = region_can_end rg_id 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;
-      call_id;
-      back_id;
-      kind;
+      kind = kind rg_id;
       can_end;
       parents;
       original_parents;
@@ -741,16 +739,15 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
   (* Apply *)
   T.RegionGroupId.mapi create_abs rgl
 
-let create_push_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
-    (kind : V.abs_kind) (rgl : A.abs_region_group list)
+let create_push_abstractions_from_abs_region_groups
+    (kind : T.RegionGroupId.id -> V.abs_kind) (rgl : A.abs_region_group list)
     (region_can_end : T.RegionGroupId.id -> bool)
     (compute_abs_avalues :
       V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let empty_absl =
-    create_empty_abstractions_from_abs_region_groups call_id kind rgl
-      region_can_end
+    create_empty_abstractions_from_abs_region_groups kind rgl region_can_end
   in
 
   (* Compute and add the avalues to the abstractions, the insert the abstractions
@@ -847,48 +844,16 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
           (* Evaluation successful: evaluate the second statement *)
           | Unit -> eval_statement config st2 cf
           (* Control-flow break: transmit. We enumerate the cases on purpose *)
-          | Panic | Break _ | Continue _ | Return -> cf res
+          | Panic | Break _ | Continue _ | Return | EndEnterLoop | EndContinue
+            ->
+              cf res
         in
         (* Compose and apply *)
         comp cf_st1 cf_st2 cf ctx
     | A.Loop loop_body ->
-        (* For now, we don't support loops in symbolic mode *)
-        assert (config.C.mode = C.ConcreteMode);
-        (* Continuation for after we evaluate the loop body: depending the result
-           of doing one loop iteration:
-           - redoes a loop iteration
-           - exits the loop
-           - other...
-
-           We need a specific function because of the {!Continue} case: in case we
-           continue, we might have to reevaluate the current loop body with the
-           new context (and repeat this an indefinite number of times).
-        *)
-        let rec reeval_loop_body res : m_fun =
-          match res with
-          | Return | Panic -> cf res
-          | Break i ->
-              (* Break out of the loop by calling the continuation *)
-              let res = if i = 0 then Unit else Break (i - 1) in
-              cf res
-          | Continue 0 ->
-              (* Re-evaluate the loop body *)
-              eval_statement config loop_body reeval_loop_body
-          | Continue i ->
-              (* Continue to an outer loop *)
-              cf (Continue (i - 1))
-          | Unit ->
-              (* We can't get there.
-               * Note that if we decide not to fail here but rather do
-               * the same thing as for [Continue 0], we could make the
-               * code slightly simpler: calling {!reeval_loop_body} with
-               * {!Unit} would account for the first iteration of the loop.
-               * We prefer to write it this way for consistency and sanity,
-               * though. *)
-              raise (Failure "Unreachable")
-        in
-        (* Apply *)
-        eval_statement config loop_body reeval_loop_body ctx
+        InterpreterLoops.eval_loop config
+          (eval_statement config loop_body)
+          cf ctx
     | A.Switch switch -> eval_switch config switch cf ctx
   in
   (* Compose and apply *)
@@ -1124,11 +1089,12 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
   let cf_finish cf res =
     match res with
     | Panic -> cf Panic
-    | Break _ | Continue _ | Unit -> raise (Failure "Unreachable")
     | Return ->
         (* Pop the stack frame, retrieve the return value, move it to
          * its destination and continue *)
         pop_frame_assign config dest (cf Unit)
+    | Break _ | Continue _ | Unit | EndEnterLoop | EndContinue ->
+        raise (Failure "Unreachable")
   in
   let cc = comp cc cf_finish in
 
@@ -1219,7 +1185,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     let call_id = C.fresh_fun_call_id () in
     let region_can_end _ = true in
     let ctx =
-      create_push_abstractions_from_abs_region_groups call_id V.FunCall
+      create_push_abstractions_from_abs_region_groups
+        (fun rg_id -> V.FunCall (call_id, rg_id))
         inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
     in
 
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index 1bfd1c78..46afa782 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -48,8 +48,7 @@ val instantiate_fun_sig : T.ety list -> LA.fun_sig -> LA.inst_fun_sig
     - [ctx]
 *)
 val create_push_abstractions_from_abs_region_groups :
-  V.FunCallId.id ->
-  V.abs_kind ->
+  (T.RegionGroupId.id -> V.abs_kind) ->
   LA.abs_region_group list ->
   (T.RegionGroupId.id -> bool) ->
   (V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list) ->
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 8d23e8d8..62dce004 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -221,14 +221,13 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
 
       method! visit_symbolic_value _ s =
         match s.sv_kind with
-        | V.FunCallRet ->
+        | V.FunCallRet | V.LoopOutput ->
             if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
               raise Found
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack ->
+        | V.SynthRetGivenBack | V.Global | V.LoopGivenBack ->
             ()
-        | V.Global -> ()
     end
   in
   (* We use exceptions *)
@@ -246,3 +245,11 @@ let rvalue_get_place (rv : E.rvalue) : E.place option =
   | Use (Constant _) -> None
   | Ref (p, _) -> Some p
   | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
+
+(** See {!ValuesUtils.value_has_borrows}. *)
+let value_has_borrows (ctx : C.eval_ctx) (v : V.value) : bool =
+  ValuesUtils.value_has_borrows ctx.type_context.type_infos v
+
+(** See {!ValuesUtils.value_has_loans_or_borrows}. *)
+let value_has_loans_or_borrows (ctx : C.eval_ctx) (v : V.value) : bool =
+  ValuesUtils.value_has_loans_or_borrows ctx.type_context.type_infos v
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 9bd6b78b..d9ed9cea 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -233,13 +233,10 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     object
       inherit [_] C.iter_eval_ctx as super
 
-      method! visit_abstract_shared_borrows _ asb =
-        let visit asb =
-          match asb with
-          | V.AsbBorrow bid -> register_borrow Shared bid
-          | V.AsbProjReborrows _ -> ()
-        in
-        List.iter visit asb
+      method! visit_abstract_shared_borrow _ asb =
+        match asb with
+        | V.AsbBorrow bid -> register_borrow Shared bid
+        | V.AsbProjReborrows _ -> ()
 
       method! visit_borrow_content env bc =
         (* Register the loan *)
@@ -709,15 +706,12 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit =
       method! visit_abs _ abs = super#visit_abs (Some abs) abs
       method! visit_Symbolic _ sv = add_env_sv sv
 
-      method! visit_abstract_shared_borrows abs asb =
+      method! visit_abstract_shared_borrow abs asb =
         let abs = Option.get abs in
-        let visit asb =
-          match asb with
-          | V.AsbBorrow _ -> ()
-          | AsbProjReborrows (sv, proj_ty) ->
-              add_aproj_borrows sv abs.abs_id abs.regions proj_ty true
-        in
-        List.iter visit asb
+        match asb with
+        | V.AsbBorrow _ -> ()
+        | AsbProjReborrows (sv, proj_ty) ->
+            add_aproj_borrows sv abs.abs_id abs.regions proj_ty true
 
       method! visit_aproj abs aproj =
         (let abs = Option.get abs in
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 1d57fa5b..8cfc25d3 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -24,6 +24,9 @@ let pure_to_extract_log = L.get_logger "MainLogger.ExtractBase"
 (** Logger for Interpreter *)
 let interpreter_log = L.get_logger "MainLogger.Interpreter"
 
+(** Logger for InterpreterLoops *)
+let loops_log = L.get_logger "MainLogger.Interpreter.Loops"
+
 (** Logger for InterpreterStatements *)
 let statements_log = L.get_logger "MainLogger.Interpreter.Statements"
 
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 9d95db7f..b0e4735a 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -91,8 +91,15 @@ type expression =
           function, the map from region group ids to expressions gives the end
           of the translation for the backward functions.
        *)
+  | Loop of loop
   | Meta of meta * expression  (** Meta information *)
 
+and loop = {
+  end_expr : expression;
+      (** The end of the function (upon the moment it enters the loop) *)
+  loop_expr : expression;  (** The symbolically executed loop body *)
+}
+
 and expansion =
   | ExpandNoBranch of V.symbolic_expansion * expression
       (** A symbolic expansion which doesn't generate a branching.
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3bd6c5b3..45e35742 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -236,17 +236,17 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
   { ctx with calls }
 
 (** [back_args]: the *additional* list of inputs received by the backward function *)
-let bs_ctx_register_backward_call (abs : V.abs) (back_args : texpression list)
-    (ctx : bs_ctx) : bs_ctx * fun_or_op_id =
+let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
+    (back_id : T.RegionGroupId.id) (back_args : texpression list) (ctx : bs_ctx)
+    : bs_ctx * fun_or_op_id =
   (* Insert the abstraction in the call informations *)
-  let back_id = abs.back_id in
-  let info = V.FunCallId.Map.find abs.call_id ctx.calls in
+  let info = V.FunCallId.Map.find call_id ctx.calls in
   assert (not (T.RegionGroupId.Map.mem back_id info.backwards));
   let backwards =
     T.RegionGroupId.Map.add back_id (abs, back_args) info.backwards
   in
   let info = { info with backwards } in
-  let calls = V.FunCallId.Map.add abs.call_id info ctx.calls in
+  let calls = V.FunCallId.Map.add call_id info ctx.calls in
   (* Insert the abstraction in the abstractions map *)
   let abstractions = ctx.abstractions in
   assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions));
@@ -256,7 +256,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (back_args : texpression list)
   (* Retrieve the fun_id *)
   let fun_id =
     match info.forward.call_id with
-    | S.Fun (fid, _) -> Fun (FromLlbc (fid, Some abs.back_id))
+    | S.Fun (fid, _) -> Fun (FromLlbc (fid, Some back_id))
     | S.Unop _ | S.Binop _ -> raise (Failure "Unreachable")
   in
   (* Update the context and return *)
@@ -470,8 +470,8 @@ let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
   translate_back_ty types_infos keep_region inside_mut ty
 
 (** List the ancestors of an abstraction *)
-let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs) :
-    V.AbstractionId.id list =
+let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs)
+    (call_id : V.FunCallId.id) : V.AbstractionId.id list =
   (* We could do something more "elegant" without references, but it is
    * so much simpler to use references... *)
   let abs_set = ref V.AbstractionId.Set.empty in
@@ -485,14 +485,16 @@ let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs) :
   List.iter gather abs.original_parents;
   let ids = !abs_set in
   (* List the ancestors, in the proper order *)
-  let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
+  let call_info = V.FunCallId.Map.find call_id ctx.calls in
   List.filter
     (fun id -> V.AbstractionId.Set.mem id ids)
     call_info.forward.abstractions
 
-let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) :
-    (V.abs * texpression list) list =
-  let abs_ids = list_ancestor_abstractions_ids ctx abs in
+(** List the ancestor abstractions of an abstraction introduced because of
+    a function call *)
+let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs)
+    (call_id : V.FunCallId.id) : (V.abs * texpression list) list =
+  let abs_ids = list_ancestor_abstractions_ids ctx abs call_id in
   List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids
 
 (** Small utility.
@@ -1143,10 +1145,10 @@ let abs_to_given_back_no_mp (abs : V.abs) (ctx : bs_ctx) :
     Is used for instance when collecting the input values given to all the
     parent functions, in order to properly instantiate an 
  *)
-let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) :
+let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
     S.call * (V.abs * texpression list) list =
-  let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
-  let abs_ancestors = list_ancestor_abstractions ctx abs in
+  let call_info = V.FunCallId.Map.find call_id ctx.calls in
+  let abs_ancestors = list_ancestor_abstractions ctx abs call_id in
   (call_info.forward, abs_ancestors)
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -1171,6 +1173,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
             (ctx, e)
       in
       translate_expression e ctx
+  | Loop _loop -> raise (Failure "Unimplemented")
 
 and translate_panic (ctx : bs_ctx) : texpression =
   (* Here we use the function return type - note that it is ok because
@@ -1357,7 +1360,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       ("translate_end_abstraction: abstraction kind: "
      ^ V.show_abs_kind abs.kind));
   match abs.kind with
-  | V.SynthInput ->
+  | V.SynthInput rg_id ->
       (* When we end an input abstraction, this input abstraction gets back
        * the borrows which it introduced in the context through the input
        * values: by listing those values, we get the values which are given
@@ -1368,7 +1371,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
        * for a parent backward function.
        *)
       let bid = Option.get ctx.bid in
-      assert (abs.back_id = bid);
+      assert (rg_id = bid);
 
       (* The translation is done as follows:
        * - for a given backward function, we choose a set of variables [v_i]
@@ -1406,8 +1409,8 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
         (fun (var, value) (e : texpression) ->
           mk_let monadic (mk_typed_pattern_from_var var None) value e)
         variables_values next_e
-  | V.FunCall ->
-      let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
+  | V.FunCall (call_id, rg_id) ->
+      let call_info = V.FunCallId.Map.find call_id ctx.calls in
       let call = call_info.forward in
       let fun_id =
         match call.call_id with
@@ -1417,11 +1420,11 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
             raise (Failure "Unreachable")
       in
       let effect_info =
-        get_fun_effect_info ctx.fun_context.fun_infos fun_id (Some abs.back_id)
+        get_fun_effect_info ctx.fun_context.fun_infos fun_id (Some rg_id)
       in
       let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
       (* Retrieve the original call and the parent abstractions *)
-      let _forward, backwards = get_abs_ancestors ctx abs in
+      let _forward, backwards = get_abs_ancestors ctx abs call_id in
       (* Retrieve the values consumed when we called the forward function and
        * ended the parent backward functions: those give us part of the input
        * values (rem: for now, as we disallow nested lifetimes, there can't be
@@ -1470,7 +1473,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       (* Sanity check: the inputs and outputs have the proper number and the proper type *)
       let _ =
         let inst_sg =
-          get_instantiated_fun_sig fun_id (Some abs.back_id) type_args ctx
+          get_instantiated_fun_sig fun_id (Some rg_id) type_args ctx
         in
         log#ldebug
           (lazy
@@ -1497,7 +1500,9 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       in
       (* Retrieve the function id, and register the function call in the context
        * if necessary *)
-      let ctx, func = bs_ctx_register_backward_call abs back_inputs ctx in
+      let ctx, func =
+        bs_ctx_register_backward_call abs call_id rg_id back_inputs ctx
+      in
       (* Translate the next expression *)
       let next_e = translate_expression e ctx in
       (* Put everything together *)
@@ -1535,7 +1540,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
         assert (List.length inputs = List.length fwd_inputs);
         next_e)
       else mk_let effect_info.can_fail output call next_e
-  | V.SynthRet ->
+  | V.SynthRet rg_id ->
       (* If we end the abstraction which consumed the return value of the function
          we are synthesizing, we get back the borrows which were inside. Those borrows
          are actually input arguments of the backward function we are synthesizing.
@@ -1566,7 +1571,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       *)
       (* First, retrieve the list of variables used for the inputs for the
        * backward function *)
-      let inputs = T.RegionGroupId.Map.find abs.back_id ctx.backward_inputs in
+      let inputs = T.RegionGroupId.Map.find rg_id ctx.backward_inputs in
       (* Retrieve the values consumed upon ending the loans inside this
        * abstraction: as there are no nested borrows, there should be none. *)
       let consumed = abs_to_consumed ctx abs in
@@ -1597,6 +1602,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
         (fun (given_back, input_var) e ->
           mk_let monadic given_back (mk_texpression_from_var input_var) e)
         given_back_inputs next_e
+  | Loop _ -> raise (Failure "Unimplemented")
 
 and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
     (e : S.expression) (ctx : bs_ctx) : texpression =
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 5bcbd482..02b6e47c 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -155,3 +155,10 @@ let synthesize_assertion (v : V.typed_value) (e : expression option) =
 let synthesize_forward_end (e : expression)
     (el : expression T.RegionGroupId.Map.t) =
   Some (ForwardEnd (e, el))
+
+let synthesize_loop (end_expr : expression option)
+    (loop_expr : expression option) : expression option =
+  match (end_expr, loop_expr) with
+  | None, None -> None
+  | Some end_expr, Some loop_expr -> Some (Loop { end_expr; loop_expr })
+  | _ -> raise (Failure "Unreachable")
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 046f0482..86cb9098 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -10,12 +10,16 @@ module BorrowId = IdGen ()
 module SymbolicValueId = IdGen ()
 module AbstractionId = IdGen ()
 module FunCallId = IdGen ()
+module LoopId = IdGen ()
 
 type big_int = PrimitiveValues.big_int [@@deriving show]
 type scalar_value = PrimitiveValues.scalar_value [@@deriving show]
 type primitive_value = PrimitiveValues.primitive_value [@@deriving show]
 
-(** The kind of a symbolic value, which precises how the value was generated *)
+(** The kind of a symbolic value, which precises how the value was generated.
+
+    TODO: remove? This is not useful anymore.
+  *)
 type sv_kind =
   | FunCallRet  (** The value is the return value of a function call *)
   | FunCallGivenBack
@@ -38,6 +42,9 @@ type sv_kind =
   | SynthInputGivenBack
       (** The value was given back upon ending one of the input abstractions *)
   | Global  (** The value is a global *)
+  | LoopOutput  (** The output of a loop (seen as a forward computation) *)
+  | LoopGivenBack
+      (** A value given back by a loop (when ending abstractions while going backwards) *)
 [@@deriving show]
 
 (** A symbolic value *)
@@ -48,9 +55,14 @@ type symbolic_value = {
 }
 [@@deriving show]
 
+type borrow_id = BorrowId.id [@@deriving show]
+type borrow_id_set = BorrowId.Set.t [@@deriving show]
+type loan_id = BorrowId.id [@@deriving show]
+type loan_id_set = BorrowId.Set.t [@@deriving show]
+
 (** Ancestor for {!typed_value} iter visitor *)
 class ['self] iter_typed_value_base =
-  object (_self : 'self)
+  object (self : 'self)
     inherit [_] VisitorsRuntime.iter
 
     method visit_primitive_value : 'env -> primitive_value -> unit =
@@ -59,11 +71,19 @@ class ['self] iter_typed_value_base =
     method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
     method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> ()
     method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
+    method visit_borrow_id : 'env -> borrow_id -> unit = fun _ _ -> ()
+    method visit_loan_id : 'env -> loan_id -> unit = fun _ _ -> ()
+
+    method visit_borrow_id_set : 'env -> borrow_id_set -> unit =
+      fun env ids -> BorrowId.Set.iter (self#visit_borrow_id env) ids
+
+    method visit_loan_id_set : 'env -> loan_id_set -> unit =
+      fun env ids -> BorrowId.Set.iter (self#visit_loan_id env) ids
   end
 
 (** Ancestor for {!typed_value} map visitor for *)
 class ['self] map_typed_value_base =
-  object (_self : 'self)
+  object (self : 'self)
     inherit [_] VisitorsRuntime.map
 
     method visit_primitive_value : 'env -> primitive_value -> primitive_value =
@@ -76,6 +96,14 @@ class ['self] map_typed_value_base =
       fun _ sv -> sv
 
     method visit_ety : 'env -> ety -> ety = fun _ ty -> ty
+    method visit_borrow_id : 'env -> borrow_id -> borrow_id = fun _ id -> id
+    method visit_loan_id : 'env -> loan_id -> loan_id = fun _ id -> id
+
+    method visit_borrow_id_set : 'env -> borrow_id_set -> borrow_id_set =
+      fun env ids -> BorrowId.Set.map (self#visit_borrow_id env) ids
+
+    method visit_loan_id_set : 'env -> loan_id_set -> loan_id_set =
+      fun env ids -> BorrowId.Set.map (self#visit_loan_id env) ids
   end
 
 (** An untyped value, used in the environments *)
@@ -99,7 +127,7 @@ and adt_value = {
 }
 
 and borrow_content =
-  | SharedBorrow of mvalue * (BorrowId.id[@opaque])
+  | SharedBorrow of mvalue * borrow_id
       (** A shared borrow.
       
           We remember the shared value which was borrowed as a meta value.
@@ -110,9 +138,8 @@ and borrow_content =
           for as long as they are shared (i.e., as long as we can use the
           shared borrow).
        *)
-  | MutBorrow of (BorrowId.id[@opaque]) * typed_value
-      (** A mutably borrowed value. *)
-  | ReservedMutBorrow of mvalue * (BorrowId.id[@opaque])
+  | MutBorrow of borrow_id * typed_value  (** A mutably borrowed value. *)
+  | ReservedMutBorrow of mvalue * borrow_id
       (** A reserved mut borrow.
 
           This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}.
@@ -154,8 +181,8 @@ and borrow_content =
        *)
 
 and loan_content =
-  | SharedLoan of (BorrowId.Set.t[@opaque]) * typed_value
-  | MutLoan of (BorrowId.id[@opaque])
+  | SharedLoan of loan_id_set * typed_value
+  | MutLoan of loan_id
       (** TODO: we might want to add a set of borrow ids (useful for reserved
           borrows, and extremely useful when giving shared values to abstractions).
        *)
@@ -192,30 +219,42 @@ and typed_value = { value : value; ty : ety }
         concrete = true;
       }]
 
-(** We have to override the {!iter_typed_value_visit_mvalue.visit_mvalue} method,
-    to ignore meta-values *)
+(** "Meta"-symbolic value.
+
+     See the explanations for {!mvalue}
+
+     TODO: we may want to create wrappers, to prevent mixing meta values
+     and regular values.
+ *)
+type msymbolic_value = symbolic_value [@@deriving show]
+
 class ['self] iter_typed_value =
   object (_self : 'self)
     inherit [_] iter_typed_value_visit_mvalue
+
+    (** We have to override the {!iter_typed_value_visit_mvalue.visit_mvalue} method,
+        to ignore meta-values *)
     method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
+
+    method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
+      fun _ _ -> ()
+
+    method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
   end
 
-(** We have to override the {!iter_typed_value_visit_mvalue.visit_mvalue} method,
-    to ignore meta-values *)
 class ['self] map_typed_value =
   object (_self : 'self)
     inherit [_] map_typed_value_visit_mvalue
-    method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
-  end
 
-(** "Meta"-symbolic value.
+    (** We have to override the {!iter_typed_value_visit_mvalue.visit_mvalue} method,
+        to ignore meta-values *)
+    method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
 
-     See the explanations for {!mvalue}
+    method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
 
-     TODO: we may want to create wrappers, to prevent mixing meta values
-     and regular values.
- *)
-type msymbolic_value = symbolic_value [@@deriving show]
+    method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
+      fun _ m -> m
+  end
 
 (** When giving shared borrows to functions (i.e., inserting shared borrows inside
     abstractions) we need to reborrow the shared values. When doing so, we lookup
@@ -232,31 +271,58 @@ type msymbolic_value = symbolic_value [@@deriving show]
     which borrows are inside which other borrows...
 *)
 type abstract_shared_borrow =
-  | AsbBorrow of (BorrowId.id[@opaque])
-  | AsbProjReborrows of (symbolic_value[@opaque]) * (rty[@opaque])
-[@@deriving show]
+  | AsbBorrow of borrow_id
+  | AsbProjReborrows of symbolic_value * rty
+[@@deriving
+  show,
+    visitors
+      {
+        name = "iter_abstract_shared_borrow";
+        variety = "iter";
+        ancestors = [ "iter_typed_value" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+      },
+    visitors
+      {
+        name = "map_abstract_shared_borrow";
+        variety = "map";
+        ancestors = [ "map_typed_value" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+      }]
 
 (** A set of abstract shared borrows *)
-type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show]
+type abstract_shared_borrows = abstract_shared_borrow list
+[@@deriving
+  show,
+    visitors
+      {
+        name = "iter_abstract_shared_borrows";
+        variety = "iter";
+        ancestors = [ "iter_abstract_shared_borrow" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+      },
+    visitors
+      {
+        name = "map_abstract_shared_borrows";
+        variety = "map";
+        ancestors = [ "map_abstract_shared_borrow" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+      }]
 
 (** Ancestor for {!aproj} iter visitor *)
 class ['self] iter_aproj_base =
   object (_self : 'self)
-    inherit [_] iter_typed_value
-    method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
-
-    method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
-      fun _ _ -> ()
+    inherit [_] iter_abstract_shared_borrows
   end
 
 (** Ancestor for {!aproj} map visitor *)
 class ['self] map_aproj_base =
   object (_self : 'self)
-    inherit [_] map_typed_value
-    method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
-
-    method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
-      fun _ m -> m
+    inherit [_] map_abstract_shared_borrows
   end
 
 type aproj =
@@ -335,29 +401,24 @@ type aproj =
       }]
 
 type region = RegionVarId.id Types.region [@@deriving show]
+type abstraction_id = AbstractionId.id [@@deriving show]
 
 (** Ancestor for {!typed_avalue} iter visitor *)
 class ['self] iter_typed_avalue_base =
   object (_self : 'self)
     inherit [_] iter_aproj
-    method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> ()
     method visit_region : 'env -> region -> unit = fun _ _ -> ()
-
-    method visit_abstract_shared_borrows
-        : 'env -> abstract_shared_borrows -> unit =
-      fun _ _ -> ()
+    method visit_abstraction_id : 'env -> abstraction_id -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for {!typed_avalue} map visitor *)
 class ['self] map_typed_avalue_base =
   object (_self : 'self)
     inherit [_] map_aproj
-    method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id
     method visit_region : 'env -> region -> region = fun _ r -> r
 
-    method visit_abstract_shared_borrows
-        : 'env -> abstract_shared_borrows -> abstract_shared_borrows =
-      fun _ asb -> asb
+    method visit_abstraction_id : 'env -> abstraction_id -> abstraction_id =
+      fun _ x -> x
   end
 
 (** Abstraction values are used inside of abstractions to properly model
@@ -405,7 +466,7 @@ and adt_avalue = {
     translation.
 *)
 and aloan_content =
-  | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue
+  | AMutLoan of loan_id * typed_avalue
       (** A mutable loan owned by an abstraction.
          
           Example:
@@ -424,7 +485,7 @@ and aloan_content =
             px -> mut_borrow l0 (mut_borrow @s1)
           ]}
        *)
-  | ASharedLoan of (BorrowId.Set.t[@opaque]) * typed_value * typed_avalue
+  | ASharedLoan of loan_id_set * typed_value * typed_avalue
       (** A shared loan owned by an abstraction.
 
           Example:
@@ -474,7 +535,7 @@ and aloan_content =
           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
+  | AIgnoredMutLoan of loan_id * typed_avalue
       (** An ignored mutable loan.
       
           We need to keep track of ignored mutable loans, because we may have
@@ -533,7 +594,7 @@ and aloan_content =
     ids)?
 *)
 and aborrow_content =
-  | AMutBorrow of mvalue * (BorrowId.id[@opaque]) * typed_avalue
+  | AMutBorrow of mvalue * borrow_id * typed_avalue
       (** A mutable borrow owned by an abstraction.
       
           Is used when an abstraction "consumes" borrows, when giving borrows
@@ -559,7 +620,7 @@ and aborrow_content =
           is only used for the synthesis.
           TODO: do we really use it actually?
      *)
-  | ASharedBorrow of (BorrowId.id[@opaque])
+  | ASharedBorrow of borrow_id
       (** A shared borrow owned by an abstraction.
     
           Example:
@@ -577,7 +638,7 @@ and aborrow_content =
             > abs0 { a_shared_borrow l0 }
           ]}
      *)
-  | AIgnoredMutBorrow of BorrowId.id option * typed_avalue
+  | AIgnoredMutBorrow of borrow_id option * typed_avalue
       (** An ignored mutable borrow.
       
           We need to keep track of ignored mut borrows because when ending such
@@ -732,13 +793,32 @@ and typed_avalue = { value : avalue; ty : rty }
 
 (** The kind of an abstraction, which keeps track of its origin *)
 type abs_kind =
-  | FunCall  (** The abstraction was introduced because of a function call *)
-  | SynthInput
+  | FunCall of (FunCallId.id * RegionGroupId.id)
+      (** The abstraction was introduced because of a function call.
+
+          It contains he identifier of the function call which introduced this
+          abstraction, as well as the id of the backward function this
+          abstraction stands for (backward functions are identified by the group
+          of regions to which they are associated). This is not used by the
+          symbolic execution: this is only used for pretty-printing and
+          debugging in the symbolic AST, generated by the symbolic
+          execution.
+       *)
+  | SynthInput of RegionGroupId.id
       (** The abstraction keeps track of the input values of the function
-          we are currently synthesizing. *)
-  | SynthRet
+          we are currently synthesizing.
+
+          We introduce one abstraction per (group of) region(s) in the function
+          signature, the region group id identifies this group. Similarly to
+          the [FunCall] case, this is not used by the symbolic execution.
+       *)
+  | SynthRet of RegionGroupId.id
       (** The abstraction "absorbed" the value returned by the function we
-          are currently synthesizing *)
+          are currently synthesizing
+
+          See the explanations for [SynthInput].
+       *)
+  | Loop of LoopId.id  (** The abstraction corresponds to a loop *)
 [@@deriving show]
 
 (** Abstractions model the parts in the borrow graph where the borrowing relations
@@ -748,23 +828,7 @@ type abs_kind =
     which are a special kind of value.
 *)
 type abs = {
-  abs_id : (AbstractionId.id[@opaque]);
-  call_id : (FunCallId.id[@opaque]);
-      (** The identifier of the function call which introduced this
-          abstraction. This is not used by the symbolic execution:
-          this is only used for pretty-printing and debugging, in the
-          symbolic AST, generated by the symbolic execution.
-       *)
-  back_id : (RegionGroupId.id[@opaque]);
-      (** The region group id to which this abstraction is linked.
-      
-          In most situations, it gives the id of the backward function (hence
-          the name), but it is a bit more subtle in the case of synth input
-          and synth ret abstractions.
-
-          This is not used by the symbolic execution: it is a utility for
-          the symbolic AST, generated by the symbolic execution.
-       *)
+  abs_id : abstraction_id;
   kind : (abs_kind[@opaque]);
   can_end : (bool[@opaque]);
       (** Controls whether the region can be ended or not.
@@ -779,7 +843,7 @@ type abs = {
        *)
   parents : (AbstractionId.Set.t[@opaque]);  (** The parent abstractions *)
   original_parents : (AbstractionId.id list[@opaque]);
-      (** The original list of parents, ordered. This is used for synthesis. *)
+      (** The original list of parents, ordered. This is used for synthesis. TODO: remove? *)
   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
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 524f86a4..df00bfb2 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -12,6 +12,8 @@ let mk_unit_value : typed_value =
 
 let mk_typed_value (ty : ety) (value : value) : typed_value = { value; ty }
 let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
+let mk_abottom (ty : rty) : typed_avalue = { value = ABottom; ty }
+let mk_aignored (ty : rty) : typed_avalue = { value = AIgnored; ty }
 
 (** Box a value *)
 let mk_box_value (v : typed_value) : typed_value =
@@ -21,6 +23,9 @@ let mk_box_value (v : typed_value) : typed_value =
 
 let is_bottom (v : value) : bool = match v with Bottom -> true | _ -> false
 
+let is_aignored (v : avalue) : bool =
+  match v with AIgnored -> true | _ -> false
+
 let is_symbolic (v : value) : bool =
   match v with Symbolic _ -> true | _ -> false
 
@@ -32,7 +37,9 @@ let as_mut_borrow (v : typed_value) : BorrowId.id * typed_value =
   | Borrow (MutBorrow (bid, bv)) -> (bid, bv)
   | _ -> raise (Failure "Unexpected")
 
-(** Check if a value contains a borrow *)
+(** Check if a value contains a *concrete* borrow (i.e., a [Borrow] value -
+    we don't check if there are borrows hidden in symbolic values).
+ *)
 let borrows_in_value (v : typed_value) : bool =
   let obj =
     object
@@ -46,7 +53,9 @@ let borrows_in_value (v : typed_value) : bool =
     false
   with Found -> true
 
-(** Check if a value contains reserved mutable borrows *)
+(** Check if a value contains reserved mutable borrows (which are necessarily
+    *concrete*: a symbolic value can't "hide" reserved borrows).
+ *)
 let reserved_in_value (v : typed_value) : bool =
   let obj =
     object
@@ -60,7 +69,9 @@ let reserved_in_value (v : typed_value) : bool =
     false
   with Found -> true
 
-(** Check if a value contains a loan *)
+(** Check if a value contains a loan (which is necessarily *concrete*: symbolic
+    values can't "hide" loans).
+ *)
 let loans_in_value (v : typed_value) : bool =
   let obj =
     object
@@ -74,6 +85,21 @@ let loans_in_value (v : typed_value) : bool =
     false
   with Found -> true
 
+(** Check if a value contains concrete borrows or loans *)
+let concrete_borrows_loans_in_value (v : typed_value) : bool =
+  let obj =
+    object
+      inherit [_] iter_typed_value
+      method! visit_borrow_content _env _ = raise Found
+      method! visit_loan_content _env _ = raise Found
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true
+
 (** Check if a value contains outer loans (i.e., loans which are not in borrwed
     values. *)
 let outer_loans_in_value (v : typed_value) : bool =
@@ -81,7 +107,9 @@ let outer_loans_in_value (v : typed_value) : bool =
     object
       inherit [_] iter_typed_value
       method! visit_loan_content _env _ = raise Found
-      method! visit_borrow_content _ _ = ()
+
+      method! visit_borrow_content _ _ =
+        (* Do nothing so as *not to dive* in borrowed values *) ()
     end
   in
   (* We use exceptions *)
@@ -119,3 +147,49 @@ let rec value_strip_shared_loans (v : typed_value) : typed_value =
   match v.value with
   | Loan (SharedLoan (_, v')) -> value_strip_shared_loans v'
   | _ -> v
+
+(** Check if a value has borrows in **a general sense**.
+
+    It checks if:
+    - there are concrete borrows
+    - there are symbolic values which may contain borrows
+ *)
+let value_has_borrows (infos : TA.type_infos) (v : value) : bool =
+  let obj =
+    object
+      inherit [_] iter_typed_value
+      method! visit_borrow_content _env _ = raise Found
+
+      method! visit_symbolic_value _ sv =
+        if ty_has_borrow_under_mut infos sv.sv_ty then raise Found else ()
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_value () v;
+    false
+  with Found -> true
+
+(** Check if a value has loans or borrows in **a general sense**.
+
+    It checks if:
+    - there are concrete loans or concrete borrows
+    - there are symbolic values which may contain borrows (symbolic values
+      can't contain loans).
+ *)
+let value_has_loans_or_borrows (infos : TA.type_infos) (v : value) : bool =
+  let obj =
+    object
+      inherit [_] iter_typed_value
+      method! visit_borrow_content _env _ = raise Found
+      method! visit_loan_content _env _ = raise Found
+
+      method! visit_symbolic_value _ sv =
+        if ty_has_borrow_under_mut infos sv.sv_ty then raise Found else ()
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_value () v;
+    false
+  with Found -> true
diff --git a/compiler/dune b/compiler/dune
index b825ef7e..9e92b583 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -10,7 +10,7 @@
  (public_name aeneas) ;; The name as revealed to the projects importing this library
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries charon core_unix)
+ (libraries charon core_unix unionFind)
  (modules
   Assumed
   Collections
@@ -29,6 +29,7 @@
   InterpreterExpansion
   InterpreterExpressions
   Interpreter
+  InterpreterLoops
   InterpreterPaths
   InterpreterProjectors
   InterpreterStatements