Add some .mli files

16 files changed, 642 insertions, 381 deletions

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index bd9396c0..d19aca93 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -138,6 +138,7 @@ let () =
   paths_log#set_level EL.Info;
   expressions_log#set_level EL.Info;
   expansion_log#set_level EL.Info;
+  projectors_log#set_level EL.Info;
   borrows_log#set_level EL.Info;
   invariants_log#set_level EL.Info;
   pure_utils_log#set_level EL.Info;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index cf40c5b8..d3b3c7e6 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -131,7 +131,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
   let ret_inst_sg = instantiate_fun_sig type_params sg in
   let ret_rty = ret_inst_sg.output in
   (* Move the return value out of the return variable *)
-  let cf_pop_frame = ctx_pop_frame config in
+  let cf_pop_frame = pop_frame config in
 
   (* We need to find the parents regions/abstractions of the region we
    * will end - this will allow us to, first, mark the other return
@@ -191,7 +191,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
     let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in
     let cf_end_target_abs cf =
       List.fold_left
-        (fun cf id -> end_abstraction config [] id cf)
+        (fun cf id -> end_abstraction config id cf)
         cf target_abs_ids
     in
     (* Generate the Return node *)
@@ -244,7 +244,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
           | None ->
               (* Forward translation *)
               (* Pop the frame and retrieve the returned value at the same time*)
-              let cf_pop = ctx_pop_frame config in
+              let cf_pop = pop_frame config in
               (* Generate the Return node *)
               let cf_return ret_value : m_fun =
                fun _ -> Some (SA.Return (Some ret_value))
@@ -309,7 +309,7 @@ module Test = struct
       match res with
       | Return ->
           (* Ok: drop the local variables and finish *)
-          ctx_pop_frame config (fun _ _ -> None) ctx
+          pop_frame config (fun _ _ -> None) ctx
       | _ ->
           raise
             (Failure
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 288ebc27..1b4907ac 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -12,21 +12,21 @@ open InterpreterBorrowsCore
 open InterpreterProjectors
 
 (** The local logger *)
-let log = InterpreterBorrowsCore.log
+let log = L.borrows_log
 
 (** Auxiliary function to end borrows: lookup a borrow in the environment,
     update it (by returning an updated environment where the borrow has been
     replaced by {!V.Bottom})) if we can end the borrow (for instance, it is not
     an outer borrow...) or return the reason why we couldn't update the borrow.
 
-    [end_borrow] then simply performs a loop: as long as we need to end (outer)
+    [end_borrow_aux] then simply performs a loop: as long as we need to end (outer)
     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} as an auxiliary function for
-    {!end_abstraction} (we end all the borrows in the abstraction one by one
+    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).
 *)
 let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
@@ -705,7 +705,7 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
   assert !r;
   { ctx with env }
 
-(** Auxiliary function: see {!end_borrow} *)
+(** Auxiliary function: see {!end_borrow_aux} *)
 let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* Debug *)
@@ -796,8 +796,8 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
 
     [allowed_abs]: see the comment for {!end_borrow_get_borrow}.
 
-    [chain]: contains the list of borrows/abstraction ids on which {!end_borrow}
-    and {!end_abstraction} were called, to remember the chain of calls. This is
+    [chain]: contains the list of borrows/abstraction ids on which {!end_borrow_aux}
+    and {!end_abstraction_aux} were called, to remember the chain of calls. This is
     useful for debugging purposes, and also for sanity checks to detect cycles
     (which shouldn't happen if the environment is well-formed).
 
@@ -809,12 +809,14 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
     perform anything smart and is trusted, and another function for the
     book-keeping.
  *)
-let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
+let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids)
     (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
   let chain0 = chain in
-  let chain = add_borrow_or_abs_id_to_chain "end_borrow: " (BorrowId l) chain in
+  let chain =
+    add_borrow_or_abs_id_to_chain "end_borrow_aux: " (BorrowId l) chain
+  in
   log#ldebug
     (lazy
       ("end borrow: " ^ V.BorrowId.to_string l ^ ":\n- original context:\n"
@@ -884,22 +886,22 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
            * inside another borrow *)
           let allowed_abs' = None in
           (* End the outer borrows *)
-          let cc = end_borrows config chain allowed_abs' bids in
+          let cc = end_borrows_aux config chain allowed_abs' bids in
           (* Retry to end the borrow *)
-          let cc = comp cc (end_borrow config chain0 allowed_abs l) in
+          let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in
           (* Check and apply *)
           comp cc cf_check cf ctx
       | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) ->
           let allowed_abs' = None in
           (* End the outer borrow *)
-          let cc = end_borrow config chain allowed_abs' bid in
+          let cc = end_borrow_aux config chain allowed_abs' bid in
           (* Retry to end the borrow *)
-          let cc = comp cc (end_borrow config chain0 allowed_abs l) in
+          let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in
           (* Check and apply *)
           comp cc cf_check cf ctx
       | OuterAbs abs_id ->
           (* The borrow is inside an abstraction: end the whole abstraction *)
-          let cf_end_abs = end_abstraction config chain abs_id in
+          let cf_end_abs = end_abstraction_aux config chain abs_id in
           (* Compose with a sanity check *)
           comp cf_end_abs cf_check cf ctx)
   | Ok (ctx, None) ->
@@ -922,7 +924,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
       (* Do a sanity check and continue *)
       cf_check cf ctx
 
-and end_borrows (config : C.config) (chain : borrow_or_abs_ids)
+and end_borrows_aux (config : C.config) (chain : borrow_or_abs_ids)
     (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) : cm_fun
     =
  fun cf ->
@@ -930,20 +932,22 @@ and end_borrows (config : C.config) (chain : borrow_or_abs_ids)
    * so that we actually end from the smallest id to the highest id - just
    * a matter of taste, and may make debugging easier *)
   let ids = V.BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in
-  List.fold_left (fun cf id -> end_borrow config chain allowed_abs id cf) cf ids
+  List.fold_left
+    (fun cf id -> end_borrow_aux config chain allowed_abs id cf)
+    cf ids
 
-and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
+and end_abstraction_aux (config : C.config) (chain : borrow_or_abs_ids)
     (abs_id : V.AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
   let chain =
-    add_borrow_or_abs_id_to_chain "end_abstraction: " (AbsId abs_id) chain
+    add_borrow_or_abs_id_to_chain "end_abstraction_aux: " (AbsId abs_id) chain
   in
   (* Remember the original context for printing purposes *)
   let ctx0 = ctx in
   log#ldebug
     (lazy
-      ("end_abstraction: "
+      ("end_abstraction_aux: "
       ^ V.AbstractionId.to_string abs_id
       ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0));
 
@@ -954,12 +958,12 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
   assert abs.can_end;
 
   (* End the parent abstractions first *)
-  let cc = end_abstractions config chain abs.parents in
+  let cc = end_abstractions_aux config chain abs.parents in
   let cc =
     comp_unit cc (fun ctx ->
         log#ldebug
           (lazy
-            ("end_abstraction: "
+            ("end_abstraction_aux: "
             ^ V.AbstractionId.to_string abs_id
             ^ "\n- context after parent abstractions ended:\n"
             ^ eval_ctx_to_string ctx)))
@@ -971,7 +975,7 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
     comp_unit cc (fun ctx ->
         log#ldebug
           (lazy
-            ("end_abstraction: "
+            ("end_abstraction_aux: "
             ^ V.AbstractionId.to_string abs_id
             ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)))
   in
@@ -1000,7 +1004,7 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
     comp_unit cc (fun ctx ->
         log#ldebug
           (lazy
-            ("end_abstraction: "
+            ("end_abstraction_aux: "
             ^ V.AbstractionId.to_string abs_id
             ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)))
@@ -1012,14 +1016,16 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
   (* Apply the continuation *)
   cc cf ctx
 
-and end_abstractions (config : C.config) (chain : borrow_or_abs_ids)
+and end_abstractions_aux (config : C.config) (chain : borrow_or_abs_ids)
     (abs_ids : V.AbstractionId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the abstraction ids,
    * so that we actually end from the smallest id to the highest id - just
    * a matter of taste, and may make debugging easier *)
   let abs_ids = V.AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in
-  List.fold_left (fun cf id -> end_abstraction config chain id cf) cf abs_ids
+  List.fold_left
+    (fun cf id -> end_abstraction_aux config chain id cf)
+    cf abs_ids
 
 and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
     (abs_id : V.AbstractionId.id) : cm_fun =
@@ -1039,8 +1045,8 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
       (* There are loans: end the corresponding borrows, then recheck *)
       let cc : cm_fun =
         match bids with
-        | Borrow bid -> end_borrow config chain None bid
-        | Borrows bids -> end_borrows config chain None bids
+        | Borrow bid -> end_borrow_aux config chain None bid
+        | Borrows bids -> end_borrows_aux config chain None bids
       in
       (* Reexplore, looking for loans *)
       let cc = comp cc (end_abstraction_loans config chain abs_id) in
@@ -1326,7 +1332,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
             V.AbstractionId.Set.empty abs_ids
         in
         (* End the abstractions and continue *)
-        end_abstractions config chain abs_ids cf ctx
+        end_abstractions_aux config chain abs_ids cf ctx
       in
       (* End the internal borrows projectors and the loans projector *)
       let cf_end_internal : cm_fun =
@@ -1379,7 +1385,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
         cf ctx)
       else
         (* The borrows proj comes from a different abstraction: end it. *)
-        let cc = end_abstraction config chain abs_id' in
+        let cc = end_abstraction_aux config chain abs_id' in
         (* Retry ending the projector of loans *)
         let cc =
           comp cc (end_proj_loans_symbolic config chain abs_id regions sv)
@@ -1389,11 +1395,13 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
         (* Continue *)
         cc cf ctx
 
-let end_outer_borrow config : V.BorrowId.id -> cm_fun =
-  end_borrow config [] None
+let end_borrow config : V.BorrowId.id -> cm_fun = end_borrow_aux config [] None
+
+let end_borrows config : V.BorrowId.Set.t -> cm_fun =
+  end_borrows_aux config [] None
 
-let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun =
-  end_borrows config [] None
+let end_abstraction config = end_abstraction_aux config []
+let end_abstractions config = end_abstractions_aux config []
 
 (** Helper function: see {!activate_inactivated_mut_borrow}.
 
@@ -1504,8 +1512,8 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
           (* End the loans *)
           let cc =
             match lc with
-            | V.SharedLoan (bids, _) -> end_outer_borrows config bids
-            | V.MutLoan bid -> end_outer_borrow config bid
+            | V.SharedLoan (bids, _) -> end_borrows config bids
+            | V.MutLoan bid -> end_borrow config bid
           in
           (* Recursive call *)
           let cc = comp cc (activate_inactivated_mut_borrow config l) in
@@ -1524,7 +1532,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
           let bids = V.BorrowId.Set.remove l bids in
-          let cc = end_outer_borrows config bids in
+          let cc = end_borrows config bids in
           (* Promote the loan - TODO: this will fail if the value contains
            * any loans. In practice, it shouldn't, but we could also
            * look for loans inside the value and end them before promoting
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
new file mode 100644
index 00000000..0733a15b
--- /dev/null
+++ b/compiler/InterpreterBorrows.mli
@@ -0,0 +1,34 @@
+module T = Types
+module V = Values
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+module S = SynthesizeSymbolic
+open Cps
+open InterpreterProjectors
+
+(** When copying values, we duplicate the shared borrows. This is tantamount to
+    reborrowing the shared value. The [reborrow_shared original_id new_bid ctx]
+    applies this change to an environment [ctx] by inserting a new borrow id in
+    the set of borrows tracked by a shared value, referenced by the
+    [original_bid] argument.  *)
+val reborrow_shared : V.BorrowId.id -> V.BorrowId.id -> C.eval_ctx -> C.eval_ctx
+
+(** End a borrow identified by its id, while preserving the invariants.
+
+    If the borrow is inside another borrow/an abstraction or contains loans,
+    [end_borrow] will end those borrows/abstractions/loans first.
+  *)
+val end_borrow : C.config -> V.BorrowId.id -> cm_fun
+
+(** End a set of borrows identified by their ids, while preserving the invariants. *)
+val end_borrows : C.config -> V.BorrowId.Set.t -> cm_fun
+
+(** End an abstraction while preserving the invariants. *)
+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
+
+(** Activate a reserved borrow into a mutable borrow, while preserving the invariants. *)
+val activate_inactivated_mut_borrow : C.config -> V.BorrowId.id -> cm_fun
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 214f2cda..7cd447c3 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -1,6 +1,7 @@
-(* This file defines the basic blocks to implement the semantics of borrows.
- * Note that those functions are not only used in InterpreterBorrows, but
- * also in Invariants or InterpreterProjectors *)
+(** This file defines the basic blocks to implement the semantics of borrows.
+    Note that those functions are not only used in InterpreterBorrows, but
+    also in Invariants or InterpreterProjectors
+ *)
 
 module T = Types
 module V = Values
@@ -35,6 +36,11 @@ let ek_all : exploration_kind =
 type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id
 [@@deriving show]
 
+type borrow_ids_or_symbolic_value =
+  | BorrowIds of borrow_ids
+  | SymbolicValue of V.symbolic_value
+[@@deriving show]
+
 exception FoundBorrowIds of borrow_ids
 
 type priority_borrows_or_abs =
@@ -43,11 +49,6 @@ type priority_borrows_or_abs =
   | InnerLoans of borrow_ids
 [@@deriving show]
 
-type borrow_ids_or_symbolic_value =
-  | BorrowIds of borrow_ids
-  | SymbolicValue of V.symbolic_value
-[@@deriving show]
-
 let update_if_none opt x = match opt with None -> Some x | _ -> opt
 
 (** Utility exception *)
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index cd6df2b0..c2807311 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -468,13 +468,12 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
   let seel = List.map fst see_cf_l in
   S.synthesize_symbolic_expansion sv sv_place seel subterms
 
-(** Expand a symbolic boolean *)
-let expand_symbolic_bool (config : C.config) (sp : V.symbolic_value)
-    (sp_place : SA.mplace option) (cf_true : m_fun) (cf_false : m_fun) : m_fun =
+let expand_symbolic_bool (config : C.config) (sv : V.symbolic_value)
+    (sv_place : SA.mplace option) (cf_true : m_fun) (cf_false : m_fun) : m_fun =
  fun ctx ->
   (* Compute the expanded value *)
-  let original_sv = sp in
-  let original_sv_place = sp_place in
+  let original_sv = sv in
+  let original_sv_place = sv_place in
   let rty = original_sv.V.sv_ty in
   assert (rty = T.Bool);
   (* Expand the symbolic value to true or false and continue execution *)
@@ -485,24 +484,17 @@ let expand_symbolic_bool (config : C.config) (sp : V.symbolic_value)
   apply_branching_symbolic_expansions_non_borrow config original_sv
     original_sv_place seel ctx
 
-(** Expand a symbolic value.
-    
-    [allow_branching]: if [true] we can branch (by expanding enumerations with
-    stricly more than one variant), otherwise we can't.
-    
-    TODO: rename [sp] to [sv]
- *)
 let expand_symbolic_value (config : C.config) (allow_branching : bool)
-    (sp : V.symbolic_value) (sp_place : SA.mplace option) : cm_fun =
+    (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
-  log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sp));
+  log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sv));
   (* Remember the initial context for printing purposes *)
   let ctx0 = ctx in
   (* Compute the expanded value - note that when doing so, we may introduce
    * fresh symbolic values in the context (which thus gets updated) *)
-  let original_sv = sp in
-  let original_sv_place = sp_place in
+  let original_sv = sv in
+  let original_sv_place = sv_place in
   let rty = original_sv.V.sv_ty in
   let cc : cm_fun =
    fun cf ctx ->
@@ -512,7 +504,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
     | T.Adt (T.AdtId def_id, regions, types) ->
         (* Compute the expanded value *)
         let seel =
-          compute_expanded_symbolic_adt_value allow_branching sp.sv_kind def_id
+          compute_expanded_symbolic_adt_value allow_branching sv.sv_kind def_id
             regions types ctx
         in
         (* Check for branching *)
@@ -528,7 +520,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
         let ty = Collections.List.to_cons_nil types in
         (* Compute the expanded value *)
         let seel =
-          compute_expanded_symbolic_option_value allow_branching sp.sv_kind ty
+          compute_expanded_symbolic_option_value allow_branching sv.sv_kind ty
         in
 
         (* Check for branching *)
@@ -540,7 +532,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
     (* Tuples *)
     | T.Adt (T.Tuple, [], tys) ->
         (* Generate the field values *)
-        let see = compute_expanded_symbolic_tuple_value sp.sv_kind tys in
+        let see = compute_expanded_symbolic_tuple_value sv.sv_kind tys in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -552,7 +544,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
           original_sv_place see expr
     (* Boxes *)
     | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
-        let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in
+        let see = compute_expanded_symbolic_box_value sv.sv_kind boxed_ty in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -569,7 +561,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
     (* Booleans *)
     | T.Bool ->
         assert allow_branching;
-        expand_symbolic_bool config sp sp_place cf cf ctx
+        expand_symbolic_bool config sv sv_place cf cf ctx
     | _ ->
         raise
           (Failure ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty))
@@ -580,7 +572,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
         log#ldebug
           (lazy
             ("expand_symbolic_value: "
-            ^ symbolic_value_to_string ctx0 sp
+            ^ symbolic_value_to_string ctx0 sv
             ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
@@ -589,32 +581,6 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
   (* Continue *)
   cc cf ctx
 
-(** Symbolic integers are expanded upon evaluating a [switch], when the integer
-    is not an enumeration discriminant.
-    Note that a discriminant is never symbolic: we evaluate discriminant values
-    upon evaluating [eval_discriminant], which always generates a concrete value
-    (because if we call it on a symbolic enumeration, we expand the enumeration
-    *then* evaluate the discriminant). This is how we can spot "regular" switches
-    over integers.
-
-
-    When expanding a boolean upon evaluating an [if ... then ... else ...],
-    or an enumeration just before matching over it, we can simply expand the
-    boolean/enumeration (generating a list of contexts from which to execute)
-    then retry evaluating the [if ... then ... else ...] or the [match]: as
-    the scrutinee will then have a concrete value, the interpreter will switch
-    to the proper branch.
-    
-    However, when expanding a "regular" integer for a switch, there is always an
-    *otherwise* branch that we can take, for which the integer must remain symbolic
-    (because in this branch the scrutinee can take a range of values). We thus
-    can't simply expand then retry to evaluate the [switch], because then we
-    would loop...
-    
-    For this reason, we take the list of branches to execute as parameters, and
-    directly jump to those branches after the expansion, without reevaluating the
-    switch. The continuation is thus for the execution *after* the switch.
-*)
 let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
     (sv_place : SA.mplace option) (int_type : T.integer_type)
     (tgts : (V.scalar_value * m_fun) list) (otherwise : m_fun) : m_fun =
@@ -636,7 +602,6 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
   (* Then expand and evaluate - this generates the proper symbolic AST *)
   apply_branching_symbolic_expansions_non_borrow config sv sv_place tgts
 
-(** See [expand_symbolic_value] *)
 let expand_symbolic_value_no_branching (config : C.config)
     (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
   let allow_branching = false in
@@ -723,9 +688,6 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
   (* Apply *)
   expand cf ctx
 
-(** If this mode is activated through the [config], greedily expand the symbolic
-    values which need to be expanded. See [config] for more information.
- *)
 let greedy_expand_symbolic_values (config : C.config) : cm_fun =
  fun cf ctx ->
   if config.greedy_expand_symbolics_with_borrows then (
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
new file mode 100644
index 00000000..ee9f9e44
--- /dev/null
+++ b/compiler/InterpreterExpansion.mli
@@ -0,0 +1,73 @@
+module T = Types
+module PV = PrimitiveValues
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+module Inv = Invariants
+module S = SynthesizeSymbolic
+module SA = SymbolicAst
+open Cps
+open InterpreterBorrows
+
+type proj_kind = LoanProj | BorrowProj
+
+(** Expand a symbolic boolean *)
+val expand_symbolic_bool :
+  C.config -> V.symbolic_value -> SA.mplace option -> m_fun -> m_fun -> m_fun
+
+(** Expand a symbolic value.
+    
+    Parameters:
+    - [config]
+    - [allow_branching]: if [true] we can branch (by expanding enumerations with
+      stricly more than one variant), otherwise we can't.
+    - [sv]
+    - [sv_place]
+ *)
+val expand_symbolic_value :
+  C.config -> bool -> V.symbolic_value -> SA.mplace option -> cm_fun
+
+(** Symbolic integers are expanded upon evaluating a [switch], when the integer
+    is not an enumeration discriminant.
+    Note that a discriminant is never symbolic: we evaluate discriminant values
+    upon evaluating [eval_discriminant], which always generates a concrete value
+    (because if we call it on a symbolic enumeration, we expand the enumeration
+    *then* evaluate the discriminant). This is how we can spot "regular" switches
+    over integers.
+
+    When expanding a boolean upon evaluating an [if ... then ... else ...],
+    or an enumeration just before matching over it, we can simply expand the
+    boolean/enumeration (generating a list of contexts from which to execute)
+    then retry evaluating the [if ... then ... else ...] or the [match]: as
+    the scrutinee will then have a concrete value, the interpreter will switch
+    to the proper branch.
+    
+    However, when expanding a "regular" integer for a switch, there is always an
+    *otherwise* branch that we can take, for which the integer must remain symbolic
+    (because in this branch the scrutinee can take a range of values). We thus
+    can't simply expand then retry to evaluate the [switch], because then we
+    would loop...
+    
+    For this reason, we take the list of branches to execute as parameters, and
+    directly jump to those branches after the expansion, without reevaluating the
+    switch. The continuation is thus for the execution *after* the switch.
+ *)
+val expand_symbolic_int :
+  C.config ->
+  V.symbolic_value ->
+  SA.mplace option ->
+  T.integer_type ->
+  (V.scalar_value * m_fun) list ->
+  m_fun ->
+  m_fun
+
+(** See {!expand_symbolic_value} *)
+val expand_symbolic_value_no_branching :
+  C.config -> V.symbolic_value -> SA.mplace option -> cm_fun
+
+(** If this mode is activated through the [config], greedily expand the symbolic
+    values which need to be expanded. See {!C.config} for more information.
+ *)
+val greedy_expand_symbolic_values : C.config -> cm_fun
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index c604bb00..a7c17a45 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -34,7 +34,7 @@ let expand_primitively_copyable_at_place (config : C.config)
   (* Small helper *)
   let rec expand : cm_fun =
    fun cf ctx ->
-    let v = read_place_unwrap config access p ctx in
+    let v = read_place config access p ctx in
     match
       find_first_primitively_copyable_sv_with_borrows
         ctx.type_context.type_infos v
@@ -53,12 +53,12 @@ let expand_primitively_copyable_at_place (config : C.config)
 (** Read a place (CPS-style function).
 
     We also check that the value *doesn't contain bottoms or inactivated
-    borrows.
+    borrows*.
  *)
 let read_place (config : C.config) (access : access_kind) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
-  let v = read_place_unwrap config access p ctx in
+  let v = read_place config access p ctx in
   (* Check that there are no bottoms in the value *)
   assert (not (bottom_in_value ctx.ended_regions v));
   (* Check that there are no inactivated borrows in the value *)
@@ -79,8 +79,8 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
     We also check, after the reorganization, that the value at the place
     *doesn't contain any bottom nor inactivated borrows*.
 
-    [expand_prim_copy]: if true, expand the symbolic values which are primitively
-    copyable and contain borrows.
+    [expand_prim_copy]: if [true], expand the symbolic values which are
+    primitively copyable and contain borrows.
  *)
 let access_rplace_reorganize_and_read (config : C.config)
     (expand_prim_copy : bool) (access : access_kind) (p : E.place)
@@ -131,6 +131,77 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
   (* Remaining cases (invalid) *)
   | _, _ -> raise (Failure "Improperly typed constant value")
 
+(** Copy a value, and return the resulting value.
+
+    Note that copying values might update the context. For instance, when
+    copying shared borrows, we need to insert new shared borrows in the context.
+
+    Also, this function is actually more general than it should be: it can be
+    used to copy concrete ADT values, while ADT copy should be done through the
+    Copy trait (i.e., by calling a dedicated function). This is why we added a
+    parameter to control this copy ([allow_adt_copy]). Note that here by ADT we
+    mean the user-defined ADTs (not tuples or assumed types).
+ *)
+let rec copy_value (allow_adt_copy : bool) (config : C.config)
+    (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value =
+  log#ldebug
+    (lazy
+      ("copy_value: "
+      ^ typed_value_to_string ctx v
+      ^ "\n- context:\n" ^ eval_ctx_to_string ctx));
+  (* Remark: at some point we rewrote this function to use iterators, but then
+   * we reverted the changes: the result was less clear actually. In particular,
+   * the fact that we have exhaustive matches below makes very obvious the cases
+   * in which we need to fail *)
+  match v.V.value with
+  | V.Primitive _ -> (ctx, v)
+  | V.Adt av ->
+      (* Sanity check *)
+      (match v.V.ty with
+      | T.Adt (T.Assumed (T.Box | Vec), _, _) ->
+          raise (Failure "Can't copy an assumed value other than Option")
+      | T.Adt (T.AdtId _, _, _) -> assert allow_adt_copy
+      | T.Adt ((T.Assumed Option | T.Tuple), _, _) -> () (* Ok *)
+      | _ -> raise (Failure "Unreachable"));
+      let ctx, fields =
+        List.fold_left_map
+          (copy_value allow_adt_copy config)
+          ctx av.field_values
+      in
+      (ctx, { v with V.value = V.Adt { av with field_values = fields } })
+  | V.Bottom -> raise (Failure "Can't copy ⊥")
+  | V.Borrow bc -> (
+      (* We can only copy shared borrows *)
+      match bc with
+      | SharedBorrow (mv, bid) ->
+          (* We need to create a new borrow id for the copied borrow, and
+           * update the context accordingly *)
+          let bid' = C.fresh_borrow_id () in
+          let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in
+          (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) })
+      | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
+      | V.InactivatedMutBorrow _ ->
+          raise (Failure "Can't copy an inactivated mut borrow"))
+  | V.Loan lc -> (
+      (* We can only copy shared loans *)
+      match lc with
+      | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan")
+      | V.SharedLoan (_, sv) ->
+          (* We don't copy the shared loan: only the shared value inside *)
+          copy_value allow_adt_copy config ctx sv)
+  | V.Symbolic sp ->
+      (* We can copy only if the type is "primitively" copyable.
+       * Note that in the general case, copy is a trait: copying values
+       * thus requires calling the proper function. Here, we copy values
+       * for very simple types such as integers, shared borrows, etc. *)
+      assert (ty_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty));
+      (* If the type is copyable, we simply return the current value. Side
+       * remark: what is important to look at when copying symbolic values
+       * is symbolic expansion. The important subcase is the expansion of shared
+       * borrows: when doing so, every occurrence of the same symbolic value
+       * must use a fresh borrow id. *)
+      (ctx, v)
+
 (** Reorganize the environment in preparation for the evaluation of an operand.
 
     Evaluating an operand requires reorganizing the environment to get access
@@ -148,7 +219,7 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
       dest <- f(move x, move y);
       ...
     ]}
-    Because of the way [end_borrow] is implemented, when giving back the borrow
+    Because of the way {!end_borrow} is implemented, when giving back the borrow
     [l0] upon evaluating [move y], we won't notice that [shared_borrow l0] has
     disappeared from the environment (it has been moved and not assigned yet,
     and so is hanging in "thin air").
@@ -158,13 +229,15 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
     by access *and* move operations have already been applied.
 
     Rk.: in the formalization, we always have an explicit "reorganization" step
-    in the rule premises, before the actual operand evaluation.
+    in the rule premises, before the actual operand evaluation, that allows to
+    reorganize the environment so that it satisfies the proper conditions. This
+    function's role is to do the reorganization.
     
     Rk.: doing this is actually not completely necessary because when
     generating MIR, rustc introduces intermediate assignments for all the function
     parameters. Still, it is better for soundness purposes, and corresponds to
-    what we do in the formalization (because we don't enforce constraints
-    in the formalization).
+    what we do in the formalization (because we don't enforce the same constraints
+    as MIR in the formalization).
  *)
 let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
     cm_fun =
@@ -234,22 +307,12 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
         (* Check that there are no bottoms in the value we are about to move *)
         assert (not (bottom_in_value ctx.ended_regions v));
         let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
-        match write_place config access p bottom ctx with
-        | Error _ -> raise (Failure "Unreachable")
-        | Ok ctx -> cf v ctx
+        let ctx = write_place config access p bottom ctx in
+        cf v ctx
       in
       (* Compose and apply *)
       comp cc move cf ctx
 
-(** Evaluate an operand.
-
-    Reorganize the context, then evaluate the operand.
-
-    **Warning**: this function shouldn't be used to evaluate a list of
-    operands (for a function call, for instance): we must do *one* reorganization
-    of the environment, before evaluating all the operands at once.
-    Use [eval_operands] instead.
- *)
 let eval_operand (config : C.config) (op : E.operand)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
@@ -602,7 +665,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
               ({ v with V.value = v' }, v)
         in
         (* Update the borrowed value in the context *)
-        let ctx = write_place_unwrap config access p nv ctx in
+        let ctx = write_place config access p nv ctx in
         (* Compute the rvalue - simply a shared borrow with a the fresh id.
          * Note that the reference is *mutable* if we do a two-phase borrow *)
         let rv_ty =
@@ -637,7 +700,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         (* Compute the value with which to replace the value at place p *)
         let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
         (* Update the value in the context *)
-        let ctx = write_place_unwrap config access p nv ctx in
+        let ctx = write_place config access p nv ctx in
         (* Continue *)
         cf rv ctx
       in
@@ -699,10 +762,6 @@ let eval_rvalue_aggregate (config : C.config)
   (* Compose and apply *)
   comp eval_ops compute cf
 
-(** Evaluate an rvalue which is not a global.
-
-    Transmits the computed rvalue to the received continuation.
- *)
 let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue)
     (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
  fun ctx ->
@@ -723,3 +782,16 @@ let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue)
       comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
   | E.Discriminant p -> comp_wrap (eval_rvalue_discriminant config p) ctx
   | E.Global _ -> raise (Failure "Unreachable")
+
+let eval_fake_read (config : C.config) (p : E.place) : cm_fun =
+ fun cf ctx ->
+  let expand_prim_copy = false in
+  let cf_prepare cf =
+    access_rplace_reorganize_and_read config expand_prim_copy Read p cf
+  in
+  let cf_continue cf v : m_fun =
+   fun ctx ->
+    assert (not (bottom_in_value ctx.ended_regions v));
+    cf ctx
+  in
+  comp cf_prepare cf_continue cf ctx
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
new file mode 100644
index 00000000..c610e939
--- /dev/null
+++ b/compiler/InterpreterExpressions.mli
@@ -0,0 +1,37 @@
+module T = Types
+module PV = PrimitiveValues
+module V = Values
+module LA = LlbcAst
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+module Inv = Invariants
+module S = SynthesizeSymbolic
+open Cps
+open InterpreterPaths
+
+(** Evaluate an operand.
+
+    Reorganize the context, then evaluate the operand.
+
+    **Warning**: this function shouldn't be used to evaluate a list of
+    operands (for a function call, for instance): we must do *one* reorganization
+    of the environment, before evaluating all the operands at once.
+    Use {!eval_operands} instead.
+ *)
+val eval_operand : C.config -> E.operand -> (V.typed_value -> m_fun) -> m_fun
+
+(** Evaluate several operands at once. *)
+val eval_operands :
+  C.config -> E.operand list -> (V.typed_value list -> m_fun) -> m_fun
+
+(** Evaluate an rvalue which is not a global.
+
+    Transmits the computed rvalue to the received continuation.
+ *)
+val eval_rvalue_not_global :
+  C.config -> E.rvalue -> ((V.typed_value, eval_error) result -> m_fun) -> m_fun
+
+(** Evaluate a fake read (update the context so that we can read a place) *)
+val eval_fake_read : C.config -> E.place -> cm_fun
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index cc5b5864..73b446da 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -5,7 +5,6 @@ module C = Contexts
 module Subst = Substitute
 module L = Logging
 open Cps
-open TypesUtils
 open ValuesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
@@ -307,12 +306,12 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
         lookup_shared_borrows = false;
       }
 
-(** Read the value at a given place.
+(** Attempt to read the value at a given place.
 
     Note that we only access the value at the place, and do not check that
     the value is "well-formed" (for instance that it doesn't contain bottoms).
  *)
-let read_place (config : C.config) (access : access_kind) (p : E.place)
+let try_read_place (config : C.config) (access : access_kind) (p : E.place)
     (ctx : C.eval_ctx) : V.typed_value path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function is the identity *)
@@ -334,14 +333,14 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
           raise (Failure "Unexpected environment update"));
       Ok read_value
 
-let read_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
+let read_place (config : C.config) (access : access_kind) (p : E.place)
     (ctx : C.eval_ctx) : V.typed_value =
-  match read_place config access p ctx with
+  match try_read_place config access p ctx with
   | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
   | Ok v -> v
 
-(** Update the value at a given place *)
-let write_place (_config : C.config) (access : access_kind) (p : E.place)
+(** Attempt to update the value at a given place *)
+let try_write_place (_config : C.config) (access : access_kind) (p : E.place)
     (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function substitutes the value with the new value *)
@@ -352,13 +351,12 @@ let write_place (_config : C.config) (access : access_kind) (p : E.place)
       (* We ignore the read value *)
       Ok ctx
 
-let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
+let write_place (config : C.config) (access : access_kind) (p : E.place)
     (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
-  match write_place config access p nv ctx with
+  match try_write_place config access p nv ctx with
   | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
   | Ok ctx -> ctx
 
-(** Compute an expanded ADT bottom value *)
 let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
     (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
     (regions : T.erased_region list) (types : T.ety list) : V.typed_value =
@@ -378,7 +376,6 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
   let ty = T.Adt (T.AdtId def_id, regions, types) in
   { V.value = av; V.ty }
 
-(** Compute an expanded Option bottom value *)
 let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
     (param_ty : T.ety) : V.typed_value =
   (* Note that the variant can be [Some] or [None]: we expand bottom values
@@ -392,7 +389,6 @@ let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
   let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ]) in
   { V.value = av; ty }
 
-(** Compute an expanded tuple bottom value *)
 let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
     V.typed_value =
   (* Generate the field values *)
@@ -469,29 +465,21 @@ let expand_bottom_value_from_projection (config : C.config)
              ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty))
   in
   (* Update the context by inserting the expanded value at the proper place *)
-  match write_place config access p' nv ctx with
+  match try_write_place config access p' nv ctx with
   | Ok ctx -> ctx
   | Error _ -> raise (Failure "Unreachable")
 
-(** Update the environment to be able to read a place.
-
-    When reading a place, we may be stuck along the way because some value
-    is borrowed, we reach a symbolic value, etc. In this situation [read_place]
-    fails while returning precise information about the failure. This function
-    uses this information to update the environment (by ending borrows,
-    expanding symbolic values) until we manage to fully read the place.
- *)
 let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
     (p : E.place) : cm_fun =
  fun cf ctx ->
   (* Attempt to read the place: if it fails, update the environment and retry *)
-  match read_place config access p ctx with
+  match try_read_place config access p ctx with
   | Ok _ -> cf ctx
   | Error err ->
       let cc =
         match err with
-        | FailSharedLoan bids -> end_outer_borrows config bids
-        | FailMutLoan bid -> end_outer_borrow config bid
+        | FailSharedLoan bids -> end_borrows config bids
+        | FailMutLoan bid -> end_borrow config bid
         | FailInactivatedMutBorrow bid ->
             activate_inactivated_mut_borrow config bid
         | FailSymbolic (i, sp) ->
@@ -510,23 +498,19 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
       in
       comp cc (update_ctx_along_read_place config access p) cf ctx
 
-(** Update the environment to be able to write to a place.
-
-    See {!update_ctx_along_read_place}.
-*)
 let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
     (p : E.place) : cm_fun =
  fun cf ctx ->
   (* Attempt to *read* (yes, *read*: we check the access to the place, and
      write to it later) the place: if it fails, update the environment and retry *)
-  match read_place config access p ctx with
+  match try_read_place config access p ctx with
   | Ok _ -> cf ctx
   | Error err ->
       (* Update the context *)
       let cc =
         match err with
-        | FailSharedLoan bids -> end_outer_borrows config bids
-        | FailMutLoan bid -> end_outer_borrow config bid
+        | FailSharedLoan bids -> end_borrows config bids
+        | FailMutLoan bid -> end_borrow config bid
         | FailInactivatedMutBorrow bid ->
             activate_inactivated_mut_borrow config bid
         | FailSymbolic (_pe, sp) ->
@@ -549,15 +533,6 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
 (** Small utility used to break control-flow *)
 exception UpdateCtx of cm_fun
 
-(** End the loans at a given place: read the value, if it contains a loan,
-    end this loan, repeat.
-
-    This is used when reading or borrowing values. We typically
-    first call {!update_ctx_along_read_place} or {!update_ctx_along_write_place}
-    to get access to the value, then call this function to "prepare" the value:
-    when moving values, we can't move a value which contains loans and thus need
-    to end them, etc.
- *)
 let rec end_loans_at_place (config : C.config) (access : access_kind)
     (p : E.place) : cm_fun =
  fun cf ctx ->
@@ -587,17 +562,17 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
             match access with
             | Read -> super#visit_SharedLoan env bids v
             | Write | Move ->
-                let cc = end_outer_borrows config bids in
+                let cc = end_borrows config bids in
                 raise (UpdateCtx cc))
         | V.MutLoan bid ->
             (* We always need to end mutable borrows *)
-            let cc = end_outer_borrow config bid in
+            let cc = end_borrow config bid in
             raise (UpdateCtx cc)
     end
   in
 
   (* First, retrieve the value *)
-  match read_place config access p ctx with
+  match try_read_place config access p ctx with
   | Error _ -> raise (Failure "Unreachable")
   | Ok v -> (
       (* Inspect the value and update the context while doing so.
@@ -615,26 +590,13 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
          * a recursive call to reinspect the value *)
         comp cc (end_loans_at_place config access p) cf ctx)
 
-(** Drop (end) outer loans at a given place, which should be seen as an l-value
-    (we will write to it later, but need to drop the loans before writing).
-
-    This is used to drop values when evaluating the drop statement or before
-    writing to a place.
-    
-    Note that we don't do what is defined in the formalization: we move the
-    value to a temporary dummy value, then explore this value and end the outer
-    loans which are inside as long as we find some, then move the resulting
-    value back to where it was. This shouldn't make any difference, really (note
-    that the place is *inside* a borrow, if we end the borrow, we won't be able
-    to reinsert the value back).
- *)
 let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
  fun cf ctx ->
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
   let access = Write in
-  let v = read_place_unwrap config access p ctx in
-  let ctx = write_place_unwrap config access p (mk_bottom v.V.ty) ctx in
+  let v = read_place config access p ctx in
+  let ctx = write_place config access p (mk_bottom v.V.ty) ctx in
   let dummy_id = C.fresh_dummy_var_id () in
   let ctx = C.ctx_push_dummy_var ctx dummy_id v in
   (* Auxiliary function *)
@@ -652,9 +614,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
         (* There are: end them then retry *)
         let cc =
           match c with
-          | LoanContent (V.SharedLoan (bids, _)) ->
-              end_outer_borrows config bids
-          | LoanContent (V.MutLoan bid) -> end_outer_borrow config bid
+          | LoanContent (V.SharedLoan (bids, _)) -> end_borrows config bids
+          | LoanContent (V.MutLoan bid) -> end_borrow config bid
           | BorrowContent _ -> raise (Failure "Unreachable")
         in
         (* Retry *)
@@ -668,7 +629,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
         (* Pop *)
         let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in
         (* Reinsert *)
-        let ctx = write_place_unwrap config access p v ctx in
+        let ctx = write_place config access p v ctx in
         (* Sanity check *)
         assert (not (outer_loans_in_value v));
         (* Continue *)
@@ -677,89 +638,6 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
   (* Continue *)
   cc cf ctx
 
-(** Copy a value, and return the resulting value.
-
-    Note that copying values might update the context. For instance, when
-    copying shared borrows, we need to insert new shared borrows in the context.
- 
-    Also, this function is actually more general than it should be: it can be used
-    to copy concrete ADT values, while ADT copy should be done through the Copy
-    trait (i.e., by calling a dedicated function). This is why we added a parameter
-    to control this copy. Note that here by ADT we mean the user-defined ADTs
-    (not tuples or assumed types).
-    
-    TODO: move
- *)
-let rec copy_value (allow_adt_copy : bool) (config : C.config)
-    (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value =
-  log#ldebug
-    (lazy
-      ("copy_value: "
-      ^ typed_value_to_string ctx v
-      ^ "\n- context:\n" ^ eval_ctx_to_string ctx));
-  (* Remark: at some point we rewrote this function to use iterators, but then
-   * we reverted the changes: the result was less clear actually. In particular,
-   * the fact that we have exhaustive matches below makes very obvious the cases
-   * in which we need to fail *)
-  match v.V.value with
-  | V.Primitive _ -> (ctx, v)
-  | V.Adt av ->
-      (* Sanity check *)
-      (match v.V.ty with
-      | T.Adt (T.Assumed (T.Box | Vec), _, _) ->
-          raise (Failure "Can't copy an assumed value other than Option")
-      | T.Adt (T.AdtId _, _, _) -> assert allow_adt_copy
-      | T.Adt ((T.Assumed Option | T.Tuple), _, _) -> () (* Ok *)
-      | _ -> raise (Failure "Unreachable"));
-      let ctx, fields =
-        List.fold_left_map
-          (copy_value allow_adt_copy config)
-          ctx av.field_values
-      in
-      (ctx, { v with V.value = V.Adt { av with field_values = fields } })
-  | V.Bottom -> raise (Failure "Can't copy ⊥")
-  | V.Borrow bc -> (
-      (* We can only copy shared borrows *)
-      match bc with
-      | SharedBorrow (mv, bid) ->
-          (* We need to create a new borrow id for the copied borrow, and
-           * update the context accordingly *)
-          let bid' = C.fresh_borrow_id () in
-          let ctx = reborrow_shared bid bid' ctx in
-          (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) })
-      | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
-      | V.InactivatedMutBorrow _ ->
-          raise (Failure "Can't copy an inactivated mut borrow"))
-  | V.Loan lc -> (
-      (* We can only copy shared loans *)
-      match lc with
-      | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan")
-      | V.SharedLoan (_, sv) ->
-          (* We don't copy the shared loan: only the shared value inside *)
-          copy_value allow_adt_copy config ctx sv)
-  | V.Symbolic sp ->
-      (* We can copy only if the type is "primitively" copyable.
-       * Note that in the general case, copy is a trait: copying values
-       * thus requires calling the proper function. Here, we copy values
-       * for very simple types such as integers, shared borrows, etc. *)
-      assert (ty_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty));
-      (* If the type is copyable, we simply return the current value. Side
-       * remark: what is important to look at when copying symbolic values
-       * is symbolic expansion. The important subcase is the expansion of shared
-       * borrows: when doing so, every occurrence of the same symbolic value
-       * must use a fresh borrow id. *)
-      (ctx, v)
-
-(** Small utility.
-    
-    Prepare a place which is to be used as the destination of an assignment:
-    update the environment along the paths, end the outer loans at this place, etc.
-
-    Return the updated context and the (updated) value at the end of the
-    place. This value should not contain any outer loan (and we check
-    it is the case). Note that this value is very likely to contain {!V.Bottom}
-    subvalues.
- *)
 let prepare_lplace (config : C.config) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
@@ -775,7 +653,7 @@ let prepare_lplace (config : C.config) (p : E.place)
   (* Read the value and check it *)
   let read_check cf : m_fun =
    fun ctx ->
-    let v = read_place_unwrap config access p ctx in
+    let v = read_place config access p ctx in
     (* Sanity checks *)
     assert (not (outer_loans_in_value v));
     (* Continue *)
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
new file mode 100644
index 00000000..ed00b7c5
--- /dev/null
+++ b/compiler/InterpreterPaths.mli
@@ -0,0 +1,105 @@
+module T = Types
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+open Cps
+open InterpreterExpansion
+module Synth = SynthesizeSymbolic
+
+type access_kind = Read | Write | Move
+
+(** Update the environment to be able to read a place.
+
+    When reading a place, we may be stuck along the way because some value
+    is borrowed, we reach a symbolic value, etc. This function repeatedly
+    updates the environment (by ending borrows, expanding symbolic values, etc.)
+    until it manages to fully access the provided place.
+ *)
+val update_ctx_along_read_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Update the environment to be able to write to a place.
+
+    See {!update_ctx_along_read_place}.
+*)
+val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Read the value at a given place.
+
+    Note that we only access the value at the place, and do not check that
+    the value is "well-formed" (for instance that it doesn't contain bottoms).
+ *)
+val read_place :
+  C.config -> access_kind -> E.place -> C.eval_ctx -> V.typed_value
+
+(** Update the value at a given place.
+
+    This function is an auxiliary function and is not safe: it will not check if
+    the overwritten value contains borrows, loans, etc. and will simply
+    overwrite it.
+ *)
+val write_place :
+  C.config ->
+  access_kind ->
+  E.place ->
+  V.typed_value ->
+  C.eval_ctx ->
+  C.eval_ctx
+
+(** Compute an expanded tuple ⊥ value.
+
+    [compute_expanded_bottom_tuple_value [ty0, ..., tyn]] returns
+    [(⊥:ty0, ..., ⊥:tyn)]
+ *)
+val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value
+
+(** Compute an expanded ADT ⊥ value *)
+val compute_expanded_bottom_adt_value :
+  T.type_decl T.TypeDeclId.Map.t ->
+  T.TypeDeclId.id ->
+  T.VariantId.id option ->
+  T.erased_region list ->
+  T.ety list ->
+  V.typed_value
+
+(** Compute an expanded [Option] ⊥ value *)
+val compute_expanded_bottom_option_value :
+  T.VariantId.id -> T.ety -> V.typed_value
+
+(** Drop (end) outer loans at a given place, which should be seen as an l-value
+    (we will write to it later, but need to drop the loans before writing).
+
+    This is used to drop values when evaluating the drop statement or before
+    writing to a place.
+
+    Note that we don't do what is defined in the formalization: we move the
+    value to a temporary dummy value, then explore this value and end the outer
+    loans which are inside as long as we find some, then move the resulting
+    value back to where it was. This shouldn't make any difference, really (note
+    that the place is *inside* a borrow, if we end the borrow, we won't be able
+    to reinsert the value back).
+ *)
+val drop_outer_loans_at_lplace : C.config -> E.place -> cm_fun
+
+(** End the loans at a given place: read the value, if it contains a loan,
+    end this loan, repeat.
+
+    This is used when reading or borrowing values. We typically
+    first call {!update_ctx_along_read_place} or {!update_ctx_along_write_place}
+    to get access to the value, then call this function to "prepare" the value:
+    when moving values, we can't move a value which contains loans and thus need
+    to end them, etc.
+ *)
+val end_loans_at_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Small utility.
+
+    Prepare a place which is to be used as the destination of an assignment:
+    update the environment along the paths, end the outer loans at this place, etc.
+
+    Return the updated context and the (updated) value at the end of the
+    place. This value should not contain any outer loan (and we check it is the
+    case). Note that this value is very likely to contain ⊥ subvalues.
+  *)
+val prepare_lplace : C.config -> E.place -> (V.typed_value -> m_fun) -> m_fun
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index b77a94c4..67bbe21f 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -8,12 +8,9 @@ open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 
-(** Auxiliary function.
+(** The local logger *)
+let log = L.projectors_log
 
-    Apply a proj_borrows on a shared borrow.
-    Note that when projecting over shared values, we generate
-    {!V.abstract_shared_borrows}, not {!V.avalue}s.
-*)
 let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
     (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
     (regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) :
@@ -93,38 +90,6 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
         [ V.AsbProjReborrows (s, ty) ]
     | _ -> raise (Failure "Unreachable")
 
-(** Apply (and reduce) a projector over borrows to a value.
-
-    - [regions]: the regions we project
-    - [v]: the value over which we project
-    - [ty]: the projection type (is used to map borrows to regions, or to
-      interpret the borrows as belonging to some regions...). Remember that
-      [v] doesn't contain region information.
-      For instance, if we have:
-      [v <: ty] where:
-      - [v = mut_borrow l ...]
-      - [ty = Ref (r, ...)]
-      then we interpret the borrow [l] as belonging to region [r]
-    
-    Also, when applying projections on shared values, we need to apply
-    reborrows. This is a bit annoying because, with the way we compute
-    the projection on borrows, we can't update the context immediately.
-    Instead, we remember the list of borrows we have to insert in the
-    context *afterwards*.
-
-    [check_symbolic_no_ended] controls whether we check or not whether
-    symbolic values don't contain already ended regions.
-    This check is activated when applying projectors upon calling a function
-    (because we need to check that function arguments don't contain ⊥),
-    but deactivated when expanding symbolic values:
-    {[
-      fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
-
-      let p = f(&mut x, &mut y); // p -> @s0
-      assert(x == ...); // end 'a
-      let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
-    ]}
-*)
 let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
     (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
     (regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t)
@@ -251,7 +216,6 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
     in
     { V.value; V.ty }
 
-(** Convert a symbolic expansion *which is not a borrow* to a value *)
 let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
     (see : V.symbolic_expansion) : V.typed_value =
   let ty = Subst.erase_regions sv.V.sv_ty in
@@ -268,12 +232,6 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
   in
   { V.value; V.ty }
 
-(** Convert a symbolic expansion to a value.
-
-    If the expansion is a mutable reference expansion, it converts it to a borrow.
-    This function is meant to be used when reducing projectors over borrows,
-    during a symbolic expansion.
-  *)
 let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
     (see : V.symbolic_expansion) : V.typed_value =
   match see with
@@ -497,14 +455,6 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
   (* Return *)
   ctx
 
-(** Auxiliary function to prepare reborrowing operations (used when
-    applying projectors).
-    
-    Returns two functions:
-    - a function to generate fresh re-borrow ids, and register the reborrows
-    - a function to apply the reborrows in a context
-    Those functions are of course stateful.
- *)
 let prepare_reborrows (config : C.config) (allow_reborrows : bool) :
     (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) =
   let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
new file mode 100644
index 00000000..a6d8bd5c
--- /dev/null
+++ b/compiler/InterpreterProjectors.mli
@@ -0,0 +1,115 @@
+module T = Types
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+open InterpreterBorrowsCore
+
+(** Auxiliary function.
+
+    Apply a proj_borrows on a shared borrow.
+    Note that when projecting over shared values, we generate
+    {!V.abstract_shared_borrows}, not {!V.avalue}s.
+*)
+val apply_proj_loans_on_symbolic_expansion :
+  T.RegionId.Set.t -> V.symbolic_expansion -> T.rty -> V.typed_avalue
+
+(** Convert a symbolic expansion *which is not a borrow* to a value *)
+val symbolic_expansion_non_borrow_to_value :
+  V.symbolic_value -> V.symbolic_expansion -> V.typed_value
+
+(** Convert a symbolic expansion *which is not a shared borrow* to a value.
+
+    If the expansion is a mutable reference expansion, it converts it to a borrow.
+    This function is meant to be used when reducing projectors over borrows,
+    during a symbolic expansion.
+  *)
+val symbolic_expansion_non_shared_borrow_to_value :
+  V.symbolic_value -> V.symbolic_expansion -> V.typed_value
+
+(** Auxiliary function to prepare reborrowing operations (used when
+    applying projectors).
+
+    Returns two functions:
+    - a function to generate fresh re-borrow ids, and register the reborrows
+    - a function to apply the reborrows in a context
+    Those functions are of course stateful.
+
+    Parameters:
+    - [config]
+    - [allow_reborrows]
+ *)
+val prepare_reborrows :
+  C.config ->
+  bool ->
+  (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx)
+
+(** Apply (and reduce) a projector over borrows to a value.
+
+    Parameters:
+    - [check_symbolic_no_ended]: controls whether we check or not whether
+      symbolic values don't contain already ended regions.
+      This check is activated when applying projectors upon calling a function
+      (because we need to check that function arguments don't contain ⊥),
+      but deactivated when expanding symbolic values:
+      {[
+        fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
+
+        let p = f(&mut x, &mut y); // p -> @s0
+        assert(x == ...); // end 'a
+        let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
+      ]}
+    - [ctx]
+
+    - [fresh_reborrow]: a function which generates fresh ids for reborrows, and
+      registers the reborrows (to be applied later to the context).
+
+      When applying projections on shared values, we need to apply
+      reborrows. This is a bit annoying because, with the way we compute
+      the projection on borrows, we can't update the context immediately.
+      Instead, we remember the list of borrows we have to insert in the
+      context *afterwards*.
+
+      See {!prepare_reborrows}
+
+    - [regions]: the regions to project
+    - [ancestor_regions]
+    - [v]: the value on which to apply the projection
+
+    - [ty]: the projection type (is used to map borrows to regions, or in other
+      words to interpret the borrows as belonging to some regions). Remember that
+      [v] doesn't contain region information.
+      For instance, if we have:
+      [v <: ty] where:
+      - [v = mut_borrow l ...]
+      - [ty = Ref (r, ...)]
+      then we interpret the borrow [l] as belonging to region [r]
+*)
+val apply_proj_borrows :
+  bool ->
+  C.eval_ctx ->
+  (V.BorrowId.id -> V.BorrowId.id) ->
+  T.RegionId.Set.t ->
+  T.RegionId.Set.t ->
+  V.typed_value ->
+  T.rty ->
+  V.typed_avalue
+
+(** Parameters:
+    - [config]
+    - [ctx]
+    - [regions]: the regions to project
+    - [ancestors_regions]
+    - [v]: the value on which to apply the projection
+    - [ty]: the type (with regions) to use for the projection
+
+ *)
+val apply_proj_borrows_on_input_value :
+  C.config ->
+  C.eval_ctx ->
+  T.RegionId.Set.t ->
+  T.RegionId.Set.t ->
+  V.typed_value ->
+  T.rty ->
+  C.eval_ctx * V.typed_avalue
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 4d447ffe..66196349 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -39,12 +39,12 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
   let replace cf (v : V.typed_value) ctx =
     (* Move the value at destination (that we will overwrite) to a dummy variable
      * to preserve the borrows it may contain *)
-    let mv = read_place_unwrap config access p ctx in
+    let mv = InterpreterPaths.read_place config access p ctx in
     let dummy_id = C.fresh_dummy_var_id () in
     let ctx = C.ctx_push_dummy_var ctx dummy_id mv in
     (* Update the destination to ⊥ *)
     let nv = { v with value = V.Bottom } in
-    let ctx = write_place_unwrap config access p nv ctx in
+    let ctx = write_place config access p nv ctx in
     log#ldebug
       (lazy
         ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n"
@@ -119,14 +119,14 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) :
    fun ctx ->
     (* Move the value at destination (that we will overwrite) to a dummy variable
      * to preserve the borrows *)
-    let mv = read_place_unwrap config Write p ctx in
+    let mv = InterpreterPaths.read_place config Write p ctx in
     let dest_vid = C.fresh_dummy_var_id () in
     let ctx = C.ctx_push_dummy_var ctx dest_vid mv in
     (* Write to the destination *)
     (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
     assert (not (bottom_in_value ctx.ended_regions rv));
     (* Update the destination *)
-    let ctx = write_place_unwrap config Write p rv ctx in
+    let ctx = write_place config Write p rv ctx in
     (* Debug *)
     log#ldebug
       (lazy
@@ -322,19 +322,10 @@ let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun
   let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
   cc cf ctx
 
-(** Pop the current frame.
-    
-    Drop all the local variables but the return variable, move the return
-    value out of the return variable, remove all the local variables (but not the
-    abstractions!) from the context, remove the {!C.Frame} indicator delimiting the
-    current frame and handle the return value to the continuation.
-    
-    TODO: rename (remove the "ctx_")
- *)
-let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
+let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
-  log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx));
+  log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ctx));
 
   (* List the local variables, but the return variable *)
   let ret_vid = E.VarId.zero in
@@ -352,7 +343,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
   (* Debug *)
   log#ldebug
     (lazy
-      ("ctx_pop_frame: locals in which to drop the outer loans: ["
+      ("pop_frame: locals in which to drop the outer loans: ["
       ^ String.concat "," (List.map E.VarId.to_string locals)
       ^ "]"));
 
@@ -383,7 +374,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
     comp_check_value cc (fun _ ctx ->
         log#ldebug
           (lazy
-            ("ctx_pop_frame: after dropping outer loans in local variables:\n"
+            ("pop_frame: after dropping outer loans in local variables:\n"
            ^ eval_ctx_to_string ctx)))
   in
 
@@ -410,7 +401,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
 
 (** Pop the current frame and assign the returned value to its destination. *)
 let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
-  let cf_pop = ctx_pop_frame config in
+  let cf_pop = pop_frame config in
   let cf_assign cf ret_value : m_fun =
     assign_to_place config ret_value dest cf
   in
@@ -547,7 +538,9 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
   match (region_params, type_params, args) with
   | [], [ boxed_ty ], [ E.Move input_box_place ] ->
       (* Required type checking *)
-      let input_box = read_place_unwrap config Write input_box_place ctx in
+      let input_box =
+        InterpreterPaths.read_place config Write input_box_place ctx
+      in
       (let input_ty = ty_get_box input_box.V.ty in
        assert (input_ty = boxed_ty));
 
@@ -642,15 +635,6 @@ let eval_non_local_function_call_concrete (config : C.config)
       (* Compose and apply *)
       comp cf_eval_ops cf_eval_call
 
-(** Instantiate a function signature, introducing fresh abstraction ids and
-    region ids. This is mostly used in preparation of function calls, when
-    evaluating in symbolic mode of course.
-    
-    Note: there are no region parameters, because they should be erased.
-    
-    **Rk.:** this function is **stateful** and generates fresh abstraction ids
-    for the region groups.
- *)
 let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
     A.inst_fun_sig =
   (* Generate fresh abstraction ids and create a substitution from region
@@ -757,20 +741,6 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
   (* Apply *)
   T.RegionGroupId.mapi create_abs rgl
 
-(** Helper.
-
-    Create a list of abstractions from a list of regions groups, and insert
-    them in the context.
-
-    [region_can_end]: gives the region groups from which we generate functions
-    which can end or not.
-    
-    [compute_abs_avalues]: this function must compute, given an initialized,
-    empty (i.e., with no avalues) abstraction, compute the avalues which
-    should be inserted in this abstraction before we insert it in the context.
-    Note that this function may update the context: it is necessary when
-    computing borrow projections, for instance.
-*)
 let create_push_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
     (kind : V.abs_kind) (rgl : A.abs_region_group list)
     (region_can_end : T.RegionGroupId.id -> bool)
@@ -857,17 +827,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
 
             (* Compose and apply *)
             comp cf_eval_rvalue cf_assign cf ctx)
-    | A.FakeRead p ->
-        let expand_prim_copy = false in
-        let cf_prepare cf =
-          access_rplace_reorganize_and_read config expand_prim_copy Read p cf
-        in
-        let cf_continue cf v : m_fun =
-         fun ctx ->
-          assert (not (bottom_in_value ctx.ended_regions v));
-          cf ctx
-        in
-        comp cf_prepare cf_continue (cf Unit) ctx
+    | A.FakeRead p -> eval_fake_read config p (cf Unit) ctx
     | A.SetDiscriminant (p, variant_id) ->
         set_discriminant config p variant_id cf ctx
     | A.Drop p -> drop_value config p (cf Unit) ctx
@@ -1256,7 +1216,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       abs_ids := with_loans_abs;
       (* End the abstractions which can be ended *)
       let no_loans_abs = V.AbstractionId.Set.of_list no_loans_abs in
-      let cc = InterpreterBorrows.end_abstractions config [] no_loans_abs in
+      let cc = InterpreterBorrows.end_abstractions config no_loans_abs in
       (* Recursive call *)
       let cc = comp cc end_abs_with_no_loans in
       (* Continue *)
@@ -1362,8 +1322,7 @@ and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
       eval_local_function_call_symbolic config fid region_args type_args args
         dest
 
-(** Evaluate a statement seen as a function body (auxiliary helper for
-    [eval_statement]) *)
+(** Evaluate a statement seen as a function body *)
 and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
  fun cf ctx ->
   let cc = eval_statement config body in
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
new file mode 100644
index 00000000..1bfd1c78
--- /dev/null
+++ b/compiler/InterpreterStatements.mli
@@ -0,0 +1,63 @@
+module T = Types
+module PV = PrimitiveValues
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module A = LlbcAst
+module L = Logging
+module Inv = Invariants
+module S = SynthesizeSymbolic
+open Cps
+open InterpreterExpressions
+
+(** Pop the current frame.
+
+    Drop all the local variables (which has the effect of moving their values to
+    dummy variables, after ending the proper borrows of course) but the return
+    variable, move the return value out of the return variable, remove all the
+    local variables (but preserve the abstractions!), remove the {!C.Frame} indicator
+    delimiting the current frame and handle the return value to the continuation.
+ *)
+val pop_frame : C.config -> (V.typed_value -> m_fun) -> m_fun
+
+(** Instantiate a function signature, introducing **fresh** abstraction ids and
+    region ids. This is mostly used in preparation of function calls, when
+    evaluating in symbolic mode of course.
+
+    Note: there are no region parameters, because they should be erased.
+ *)
+val instantiate_fun_sig : T.ety list -> LA.fun_sig -> LA.inst_fun_sig
+
+(** Helper.
+
+    Create a list of abstractions from a list of regions groups, and insert
+    them in the context.
+
+    Parameters:
+    - [call_id]
+    - [kind]
+    - [rgl]: "region group list"
+    - [region_can_end]: gives the region groups from which we generate functions
+      which can end or not.
+    - [compute_abs_avalues]: this function must compute, given an initialized,
+      empty (i.e., with no avalues) abstraction, compute the avalues which
+      should be inserted in this abstraction before we insert it in the context.
+      Note that this function may update the context: it is necessary when
+      computing borrow projections, for instance.
+    - [ctx]
+*)
+val create_push_abstractions_from_abs_region_groups :
+  V.FunCallId.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) ->
+  C.eval_ctx ->
+  C.eval_ctx
+
+(** Evaluate a statement *)
+val eval_statement : C.config -> LA.statement -> st_cm_fun
+
+(** Evaluate a statement seen as a function body *)
+val eval_function_body : C.config -> LA.statement -> st_cm_fun
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 7b95f41d..5f22506b 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -36,6 +36,9 @@ let paths_log = L.get_logger "MainLogger.Interpreter.Paths"
 (** Logger for InterpreterExpansion *)
 let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion"
 
+(** Logger for InterpreterProjectors *)
+let projectors_log = L.get_logger "MainLogger.Interpreter.Projectors"
+
 (** Logger for InterpreterBorrows *)
 let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"