Move some definitions from Interpreter to InterpreterPaths

2 files changed, 834 insertions, 815 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d8256186..4ca7d58f 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -16,6 +16,7 @@ open InterpreterUtils
 open InterpreterProjectors
 open InterpreterBorrows
 open InterpreterExpansion
+open InterpreterPaths
 
 (* TODO: check that the value types are correct when evaluating *)
 (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
@@ -37,777 +38,6 @@ type eval_error = Panic
 
 type 'a eval_result = ('a, eval_error) result
 
-(** Paths *)
-
-(** When we fail reading from or writing to a path, it might be because we
-    need to update the environment by ending borrows, expanding symbolic
-    values, etc. The following type is used to convey this information.
-    
-    TODO: compare with borrow_lres?
-*)
-type path_fail_kind =
-  | FailSharedLoan of V.BorrowId.Set.t
-      (** Failure because we couldn't go inside a shared loan *)
-  | FailMutLoan of V.BorrowId.id
-      (** Failure because we couldn't go inside a mutable loan *)
-  | FailInactivatedMutBorrow of V.BorrowId.id
-      (** Failure because we couldn't go inside an inactivated mutable borrow
-          (which should get activated) *)
-  | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp)
-      (** Failure because we need to enter a symbolic value (and thus need to expand it) *)
-  (* TODO: Remove the parentheses *)
-  | FailBottom of (int * E.projection_elem * T.ety)
-      (** Failure because we need to enter an any value - we can expand Bottom
-          values if they are left values. We return the number of elements which
-          were remaining in the path when we reached the error - this allows to
-          properly update the Bottom value, if needs be.
-       *)
-  | FailBorrow of V.borrow_content
-      (** We got stuck because we couldn't enter a borrow *)
-
-(** Result of evaluating a path (reading from a path/writing to a path)
-    
-    Note that when we fail, we return information used to update the
-    environment, as well as the 
-*)
-type 'a path_access_result = ('a, path_fail_kind) result
-(** The result of reading from/writing to a place *)
-
-type updated_read_value = { read : V.typed_value; updated : V.typed_value }
-
-type projection_access = {
-  enter_shared_loans : bool;
-  enter_mut_borrows : bool;
-  lookup_shared_borrows : bool;
-}
-
-(** Generic function to access (read/write) the value at the end of a projection.
-
-    We return the (eventually) updated value, the value we read at the end of
-    the place and the (eventually) updated environment.
-    
-    TODO: use exceptions?
- *)
-let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
-    (* Function to (eventually) update the value we find *)
-      (update : V.typed_value -> V.typed_value) (p : E.projection)
-    (v : V.typed_value) : (C.eval_ctx * updated_read_value) path_access_result =
-  (* For looking up/updating shared loans *)
-  let ek : exploration_kind =
-    { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
-  in
-  match p with
-  | [] ->
-      let nv = update v in
-      (* Type checking *)
-      if nv.ty <> v.ty then (
-        L.log#lerror
-          (lazy
-            ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: "
-           ^ T.show_ety v.ty));
-        failwith
-          "Assertion failed: new value doesn't have the same type as its \
-           destination");
-      Ok (ctx, { read = v; updated = nv })
-  | pe :: p' -> (
-      (* Match on the projection element and the value *)
-      match (pe, v.V.value, v.V.ty) with
-      (* Field projection - ADTs *)
-      | ( Field (ProjAdt (def_id, opt_variant_id), field_id),
-          V.Adt adt,
-          T.Adt (T.AdtId def_id', _, _) ) -> (
-          assert (def_id = def_id');
-          (* Check that the projection is consistent with the current value *)
-          (match (opt_variant_id, adt.variant_id) with
-          | None, None -> ()
-          | Some vid, Some vid' -> if vid <> vid' then failwith "Unreachable"
-          | _ -> failwith "Unreachable");
-          (* Actually project *)
-          let fv = T.FieldId.nth adt.field_values field_id in
-          match access_projection access ctx update p' fv with
-          | Error err -> Error err
-          | Ok (ctx, res) ->
-              (* Update the field value *)
-              let nvalues =
-                T.FieldId.update_nth adt.field_values field_id res.updated
-              in
-              let nadt = V.Adt { adt with V.field_values = nvalues } in
-              let updated = { v with value = nadt } in
-              Ok (ctx, { res with updated }))
-      (* Tuples *)
-      | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> (
-          assert (arity = List.length adt.field_values);
-          let fv = T.FieldId.nth adt.field_values field_id in
-          (* Project *)
-          match access_projection access ctx update p' fv with
-          | Error err -> Error err
-          | Ok (ctx, res) ->
-              (* Update the field value *)
-              let nvalues =
-                T.FieldId.update_nth adt.field_values field_id res.updated
-              in
-              let ntuple = V.Adt { adt with field_values = nvalues } in
-              let updated = { v with value = ntuple } in
-              Ok (ctx, { res with updated })
-          (* If we reach Bottom, it may mean we need to expand an uninitialized
-           * enumeration value *))
-      | Field (ProjAdt (_, _), _), V.Bottom, _ ->
-          Error (FailBottom (1 + List.length p', pe, v.ty))
-      | Field (ProjTuple _, _), V.Bottom, _ ->
-          Error (FailBottom (1 + List.length p', pe, v.ty))
-      (* Symbolic value: needs to be expanded *)
-      | _, Symbolic sp, _ ->
-          (* Expand the symbolic value *)
-          Error (FailSymbolic (pe, sp))
-      (* Box dereferencement *)
-      | ( DerefBox,
-          Adt { variant_id = None; field_values = [ bv ] },
-          T.Adt (T.Assumed T.Box, _, _) ) -> (
-          (* We allow moving inside of boxes. In practice, this kind of
-           * manipulations should happen only inside unsage code, so
-           * it shouldn't happen due to user code, and we leverage it
-           * when implementing box dereferencement for the concrete
-           * interpreter *)
-          match access_projection access ctx update p' bv with
-          | Error err -> Error err
-          | Ok (ctx, res) ->
-              let nv =
-                {
-                  v with
-                  value =
-                    V.Adt { variant_id = None; field_values = [ res.updated ] };
-                }
-              in
-              Ok (ctx, { res with updated = nv }))
-      (* Borrows *)
-      | Deref, V.Borrow bc, _ -> (
-          match bc with
-          | V.SharedBorrow bid ->
-              (* Lookup the loan content, and explore from there *)
-              if access.lookup_shared_borrows then
-                match lookup_loan ek bid ctx with
-                | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan"
-                | _, Concrete (V.SharedLoan (bids, sv)) -> (
-                    (* Explore the shared value *)
-                    match access_projection access ctx update p' sv with
-                    | Error err -> Error err
-                    | Ok (ctx, res) ->
-                        (* Update the shared loan with the new value returned
-                           by [access_projection] *)
-                        let ctx =
-                          update_loan ek bid
-                            (V.SharedLoan (bids, res.updated))
-                            ctx
-                        in
-                        (* Return - note that we don't need to update the borrow itself *)
-                        Ok (ctx, { res with updated = v }))
-                | ( _,
-                    Abstract
-                      ( V.AMutLoan (_, _)
-                      | V.AEndedMutLoan { given_back = _; child = _ }
-                      | V.AEndedSharedLoan (_, _)
-                      | V.AIgnoredMutLoan (_, _)
-                      | V.AEndedIgnoredMutLoan { given_back = _; child = _ }
-                      | V.AIgnoredSharedLoan _ ) ) ->
-                    failwith "Expected a shared (abstraction) loan"
-                | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> (
-                    (* Explore the shared value *)
-                    match access_projection access ctx update p' sv with
-                    | Error err -> Error err
-                    | Ok (ctx, res) ->
-                        (* Relookup the child avalue *)
-                        let av =
-                          match lookup_loan ek bid ctx with
-                          | _, Abstract (V.ASharedLoan (_, _, av)) -> av
-                          | _ -> failwith "Unexpected"
-                        in
-                        (* Update the shared loan with the new value returned
-                             by [access_projection] *)
-                        let ctx =
-                          update_aloan ek bid
-                            (V.ASharedLoan (bids, res.updated, av))
-                            ctx
-                        in
-                        (* Return - note that we don't need to update the borrow itself *)
-                        Ok (ctx, { res with updated = v }))
-              else Error (FailBorrow bc)
-          | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid)
-          | V.MutBorrow (bid, bv) ->
-              if access.enter_mut_borrows then
-                match access_projection access ctx update p' bv with
-                | Error err -> Error err
-                | Ok (ctx, res) ->
-                    let nv =
-                      {
-                        v with
-                        value = V.Borrow (V.MutBorrow (bid, res.updated));
-                      }
-                    in
-                    Ok (ctx, { res with updated = nv })
-              else Error (FailBorrow bc))
-      | _, V.Loan lc, _ -> (
-          match lc with
-          | V.MutLoan bid -> Error (FailMutLoan bid)
-          | V.SharedLoan (bids, sv) ->
-              (* If we can enter shared loan, we ignore the loan. Pay attention
-                 to the fact that we need to reexplore the *whole* place (i.e,
-                 we mustn't ignore the current projection element *)
-              if access.enter_shared_loans then
-                match access_projection access ctx update (pe :: p') sv with
-                | Error err -> Error err
-                | Ok (ctx, res) ->
-                    let nv =
-                      {
-                        v with
-                        value = V.Loan (V.SharedLoan (bids, res.updated));
-                      }
-                    in
-                    Ok (ctx, { res with updated = nv })
-              else Error (FailSharedLoan bids))
-      | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r ->
-          let pe, v, ty = r in
-          let pe = "- pe: " ^ E.show_projection_elem pe in
-          let v = "- v:\n" ^ V.show_value v in
-          let ty = "- ty:\n" ^ T.show_ety ty in
-          L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
-          failwith "Inconsistent projection")
-
-(** Generic function to access (read/write) the value at a given place.
-
-    We return the value we read at the place and the (eventually) updated
-    environment, if we managed to access the place, or the precise reason
-    why we failed.
- *)
-let access_place (access : projection_access)
-    (* Function to (eventually) update the value we find *)
-      (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx)
-    : (C.eval_ctx * V.typed_value) path_access_result =
-  (* Lookup the variable's value *)
-  let value = C.ctx_lookup_var_value ctx p.var_id in
-  (* Apply the projection *)
-  match access_projection access ctx update p.projection value with
-  | Error err -> Error err
-  | Ok (ctx, res) ->
-      (* Update the value *)
-      let ctx = C.ctx_update_var_value ctx p.var_id res.updated in
-      (* Return *)
-      Ok (ctx, res.read)
-
-type access_kind =
-  | Read  (** We can go inside borrows and loans *)
-  | Write  (** Don't enter shared borrows or shared loans *)
-  | Move  (** Don't enter borrows or loans *)
-
-let access_kind_to_projection_access (access : access_kind) : projection_access
-    =
-  match access with
-  | Read ->
-      {
-        enter_shared_loans = true;
-        enter_mut_borrows = true;
-        lookup_shared_borrows = true;
-      }
-  | Write ->
-      {
-        enter_shared_loans = false;
-        enter_mut_borrows = true;
-        lookup_shared_borrows = false;
-      }
-  | Move ->
-      {
-        enter_shared_loans = false;
-        enter_mut_borrows = false;
-        lookup_shared_borrows = false;
-      }
-
-(** Read the value at a given place *)
-let 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 *)
-  let update v = v in
-  match access_place access update p ctx with
-  | Error err -> Error err
-  | Ok (ctx1, read_value) ->
-      (* Note that we ignore the new environment: it should be the same as the
-         original one.
-      *)
-      if config.check_invariants then
-        if ctx1 <> ctx then (
-          let msg =
-            "Unexpected environment update:\nNew environment:\n"
-            ^ C.show_env ctx1.env ^ "\n\nOld environment:\n"
-            ^ C.show_env ctx.env
-          in
-          L.log#serror msg;
-          failwith "Unexpected environment update");
-      Ok read_value
-
-let read_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
-    (ctx : C.eval_ctx) : V.typed_value =
-  match read_place config access p ctx with
-  | Error _ -> failwith "Unreachable"
-  | Ok v -> v
-
-(** Update the value at a given place *)
-let 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 *)
-  let update _ = nv in
-  match access_place access update p ctx with
-  | Error err -> Error err
-  | Ok (ctx, _) ->
-      (* We ignore the read value *)
-      Ok ctx
-
-let write_place_unwrap (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
-  | Error _ -> failwith "Unreachable"
-  | Ok ctx -> ctx
-
-(** Compute an expanded ADT bottom value *)
-let compute_expanded_bottom_adt_value (tyctx : T.type_def list)
-    (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
-    (regions : T.erased_region list) (types : T.ety list) : V.typed_value =
-  (* Lookup the definition and check if it is an enumeration - it
-     should be an enumeration if and only if the projection element
-     is a field projection with *some* variant id. Retrieve the list
-     of fields at the same time. *)
-  let def = T.TypeDefId.nth tyctx def_id in
-  assert (List.length regions = List.length def.T.region_params);
-  (* Compute the field types *)
-  let field_types =
-    Subst.type_def_get_instantiated_field_etypes def opt_variant_id types
-  in
-  (* Initialize the expanded value *)
-  let fields =
-    List.map
-      (fun ty : V.typed_value -> ({ V.value = V.Bottom; ty } : V.typed_value))
-      field_types
-  in
-  let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in
-  let ty = T.Adt (T.AdtId def_id, regions, types) in
-  { V.value = av; V.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 *)
-  let fields =
-    List.map (fun ty : V.typed_value -> { V.value = Bottom; ty }) field_types
-  in
-  let v = V.Adt { variant_id = None; field_values = fields } in
-  let ty = T.Adt (T.Tuple, [], field_types) in
-  { V.value = v; V.ty }
-
-(** Auxiliary helper to expand [Bottom] values.
-
-    During compilation, rustc desaggregates the ADT initializations. The
-    consequence is that the following rust code:
-    ```
-    let x = Cons a b;
-    ```
-
-    Looks like this in MIR:
-    ```
-    (x as Cons).0 = a;
-    (x as Cons).1 = b;
-    set_discriminant(x, 0); // If `Cons` is the variant of index 0
-    ```
-
-    The consequence is that we may sometimes need to write fields to values
-    which are currently [Bottom]. When doing this, we first expand the value
-    to, say, [Cons Bottom Bottom] (note that field projection contains information
-    about which variant we should project to, which is why we *can* set the
-    variant index when writing one of its fields).
-*)
-let expand_bottom_value_from_projection (config : C.config)
-    (access : access_kind) (p : E.place) (remaining_pes : int)
-    (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Debugging *)
-  L.log#ldebug
-    (lazy
-      ("expand_bottom_value_from_projection:\n" ^ "pe: "
-     ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty));
-  (* Prepare the update: we need to take the proper prefix of the place
-     during whose evaluation we got stuck *)
-  let projection' =
-    fst
-      (Utilities.list_split_at p.projection
-         (List.length p.projection - remaining_pes))
-  in
-  let p' = { p with projection = projection' } in
-  (* Compute the expanded value.
-     The type of the [Bottom] value should be a tuple or an ADT.
-     Note that the projection element we got stuck at should be a
-     field projection, and gives the variant id if the [Bottom] value
-     is an enumeration value.
-     Also, the expanded value should be the proper ADT variant or a tuple
-     with the proper arity, with all the fields initialized to [Bottom]
-  *)
-  let nv =
-    match (pe, ty) with
-    (* "Regular" ADTs *)
-    | ( Field (ProjAdt (def_id, opt_variant_id), _),
-        T.Adt (T.AdtId def_id', regions, types) ) ->
-        assert (def_id = def_id');
-        compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id
-          opt_variant_id regions types
-    (* Tuples *)
-    | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
-        assert (arity = List.length tys);
-        (* Generate the field values *)
-        compute_expanded_bottom_tuple_value tys
-    | _ ->
-        failwith
-          ("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
-  | Ok ctx -> ctx
-  | Error _ -> failwith "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) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Attempt to read the place: if it fails, update the environment and retry *)
-  match read_place config access p ctx with
-  | Ok _ -> ctx
-  | Error err ->
-      let ctx =
-        match err with
-        | FailSharedLoan bids -> end_outer_borrows config bids ctx
-        | FailMutLoan bid -> end_outer_borrow config bid ctx
-        | FailInactivatedMutBorrow bid ->
-            activate_inactivated_mut_borrow config Outer bid ctx
-        | FailSymbolic (pe, sp) ->
-            (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching config pe sp ctx
-        | FailBottom (_, _, _) ->
-            (* We can't expand [Bottom] values while reading them *)
-            failwith "Found [Bottom] while reading a place"
-        | FailBorrow _ -> failwith "Could not read a borrow"
-      in
-      update_ctx_along_read_place config access p ctx
-
-(** Update the environment to be able to write to a place.
-
-    See [update_env_alond_read_place].
-*)
-let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
-    (p : E.place) (ctx : C.eval_ctx) : C.eval_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
-  | Ok _ -> ctx
-  | Error err ->
-      let ctx =
-        match err with
-        | FailSharedLoan bids -> end_outer_borrows config bids ctx
-        | FailMutLoan bid -> end_outer_borrow config bid ctx
-        | FailInactivatedMutBorrow bid ->
-            activate_inactivated_mut_borrow config Outer bid ctx
-        | FailSymbolic (pe, sp) ->
-            (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching config pe sp ctx
-        | FailBottom (remaining_pes, pe, ty) ->
-            (* Expand the [Bottom] value *)
-            expand_bottom_value_from_projection config access p remaining_pes pe
-              ty ctx
-        | FailBorrow _ -> failwith "Could not write to a borrow"
-      in
-      update_ctx_along_write_place config access p ctx
-
-exception UpdateCtx of C.eval_ctx
-(** Small utility used to break control-flow *)
-
-(** End the loans at a given place: read the value, if it contains a loan,
-    end this loan, repeat.
-
-    This is used when reading, borrowing, writing to a value. 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) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Iterator to explore a value and update the context whenever we find
-   * loans.
-   * We use exceptions to make it handy: whenever we update the
-   * context, we raise an exception wrapping the updated context.
-   * *)
-  let obj =
-    object
-      inherit [_] V.iter_typed_value as super
-
-      method! visit_borrow_content env bc =
-        match bc with
-        | V.SharedBorrow _ | V.MutBorrow (_, _) ->
-            (* Nothing special to do *) super#visit_borrow_content env bc
-        | V.InactivatedMutBorrow bid ->
-            (* We need to activate inactivated borrows *)
-            let ctx = activate_inactivated_mut_borrow config Inner bid ctx in
-            raise (UpdateCtx ctx)
-
-      method! visit_loan_content env lc =
-        match lc with
-        | V.SharedLoan (bids, v) -> (
-            (* End the loans if we need a modification access, otherwise dive into
-               the shared value *)
-            match access with
-            | Read -> super#visit_SharedLoan env bids v
-            | Write | Move ->
-                let ctx = end_outer_borrows config bids ctx in
-                raise (UpdateCtx ctx))
-        | V.MutLoan bid ->
-            (* We always need to end mutable borrows *)
-            let ctx = end_outer_borrow config bid ctx in
-            raise (UpdateCtx ctx)
-    end
-  in
-
-  (* First, retrieve the value *)
-  match read_place config access p ctx with
-  | Error _ -> failwith "Unreachable"
-  | Ok v -> (
-      (* Inspect the value and update the context while doing so.
-         If the context gets updated: perform a recursive call (many things
-         may have been updated in the context: we need to re-read the value
-         at place [p] - and this value may actually not be accessible
-         anymore...)
-      *)
-      try
-        obj#visit_typed_value () v;
-        (* No context update required: return the current context *)
-        ctx
-      with UpdateCtx ctx ->
-        (* The context was updated: do a recursive call to reinspect the value *)
-        end_loans_at_place config access p ctx)
-
-(** Drop (end) all the loans and borrows at a given place, which should be
-    seen as an l-value (we will write to it later, but need to drop the borrows
-    before writing).
-
-    We start by only dropping the borrows, then we end the loans. The reason
-    is that some loan we find may be borrowed by another part of the subvalue.
-    In order to correctly handle the "outer borrow" priority (we should end
-    the outer borrows first) which is not really applied here (we are preparing
-    the value for override: we can end the borrows inside, without ending the
-    borrows we traversed to actually access the value) we first end the borrows
-    we find in the place, to make sure all the "local" loans are taken care of.
-    Then, if we find a loan, it means it is "externally" borrowed (the associated
-    borrow is not in a subvalue of the place under inspection).
-    Also note that whenever we end a loan, we might propagate back a value inside
-    the place under inspection: we must re-end all the borrows we find there,
-    before reconsidering loans.
-
-    Repeat:
-    - read the value at a given place
-    - as long as we find a loan or a borrow, end it
-
-    This is used to drop values (when we need to write to a place, we first
-    drop the value there to properly propagate back values which are not/can't
-    be borrowed anymore).
- *)
-let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Iterator to explore a value and update the context whenever we find
-     borrows/loans.
-     We use exceptions to make it handy: whenever we update the
-     context, we raise an exception wrapping the updated context.
-
-     Note that we can end the borrows which are inside the value (while the
-     value itself might be inside a borrow/loan: we are thus ending inner
-     borrows). Because a loan inside the value may be linked to a borrow
-     somewhere else *also inside* the value (it's possible with adts),
-     we first end all the borrows we find - by using [Inner] to allow
-     ending inner borrows - then end all the loans we find.
-
-     It is really important to do this in two steps: the borrow linked to a
-     loan may be inside the value at place p, in which case this borrow may be
-     an inner borrow that we *can* end, but it may also be outside this
-     value, in which case we need to end all the outer borrows first...
-     Also, whenever the context is updated, we need to re-inspect
-     the value at place p *in two steps* again (end borrows, then end
-     loans).
-
-     Example:
-     =======
-     We want to end the borrows/loans at `*x` in the following environment:
-     ```
-     x -> mut_borrow l0 (mut_loan l1, mut_borrow l1 (Int 3), mut_loan l2)
-     y -> mut_borrow l2 (Bool true)
-     ```
-
-     We have to consider two things:
-     - the borrow `mut_borrow l1 (Int 3)` borrows a subvalue of `*x`
-     - the borrow corresponding to the loan `mut_loan l2` is outside of `*x`
-
-     We first end all the *borrows* (not the loans) inside of `*x`, which gives:
-     ```
-     x -> mut_borrow l0 (Int 3, ⊥, mut_loan l2)
-     y -> mut_borrow l2 (Bool true)
-     ```
-
-     Note that when ending the borrows, we can (and have to) ignore the outer
-     borrows (in this case `mut_borrow l0 ...`). Otherwise, we would have to end
-     the borrow `l0` which is incorrect (note that we might have to drop the
-     borrows/loans at `*x` if we evaluate, for instance, `*x = ...`).
-     It is ok to ignore outer borrows in this case because whenever
-     we end a borrow, it is an outer borrow locally to `*x` (i.e., we ignore
-     the outer borrows when accessing `*x`, but once examining the value at
-     `*x` we never dive into borrows: whenever we find one, we end it - it is thus
-     an outer borrow, in some way).
-
-     Then, we end the loans at `*x`. Note that as at this point `*x` doesn't
-     contain borrows (only loans), the borrows corresponding to those loans
-     are thus necessarily outside of `*x`: we mustn't ignore outer borrows this
-     time. This gives:
-     ```
-     x -> mut_borrow l0 (Int 3, ⊥, Bool true)
-     y -> ⊥
-     ```
-  *)
-  let obj =
-    object
-      inherit [_] V.iter_typed_value as super
-
-      method! visit_borrow_content end_loans bc =
-        (* Sanity check: we should have ended all the borrows before starting
-           to end loans *)
-        assert (not end_loans);
-
-        (* We need to end all borrows. Note that we ignore the outer borrows
-           when ending the borrows we find here (we call [end_inner_borrow(s)]:
-           the value at place p might be below a borrow/loan). Note however
-           that if we restrain ourselves at the value at place p, the borrow we
-           found here can be considered as an outer borrow.
-        *)
-        match bc with
-        | V.SharedBorrow bid | V.MutBorrow (bid, _) ->
-            raise (UpdateCtx (end_inner_borrow config bid ctx))
-        | V.InactivatedMutBorrow bid ->
-            (* We need to activate ithe nactivated borrow - later, we will
-             * actually end it - Rk.: we could actually end it straight away
-             * (this is not really important) *)
-            let ctx = activate_inactivated_mut_borrow config Inner bid ctx in
-            raise (UpdateCtx ctx)
-
-      method! visit_loan_content end_loans lc =
-        if
-          (* If we can, end the loans, otherwise ignore: keep for later *)
-          end_loans
-        then
-          (* We need to end all loans. Note that as all the borrows inside
-             the value at place p should already have ended, the borrows
-             associated to the loans we find here should be borrows from
-             outside this value: we need to call [end_outer_borrow(s)]
-             (we can't ignore outer borrows this time).
-          *)
-          match lc with
-          | V.SharedLoan (bids, _) ->
-              raise (UpdateCtx (end_outer_borrows config bids ctx))
-          | V.MutLoan bid -> raise (UpdateCtx (end_outer_borrow config bid ctx))
-        else super#visit_loan_content end_loans lc
-    end
-  in
-
-  (* We do something similar to [end_loans_at_place].
-     First, retrieve the value *)
-  match read_place config Write p ctx with
-  | Error _ -> failwith "Unreachable"
-  | Ok v -> (
-      (* Inspect the value and update the context while doing so.
-         If the context gets updated: perform a recursive call (many things
-         may have been updated in the context: first we need to retrieve the
-         proper updated value - and this value may actually not be accessible
-         anymore
-      *)
-      try
-        (* Inspect the value: end the borrows only *)
-        obj#visit_typed_value false v;
-        (* Inspect the value: end the loans *)
-        obj#visit_typed_value true v;
-        (* No context update required: return the current context *)
-        ctx
-      with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p 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).
- *)
-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 =
-  (* 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.Concrete _ -> (ctx, v)
-  | V.Adt av ->
-      (* Sanity check *)
-      (match v.V.ty with
-      | T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value"
-      | T.Adt (T.AdtId _, _, _) -> assert allow_adt_copy
-      | T.Adt (T.Tuple, _, _) -> () (* Ok *)
-      | _ -> failwith "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 -> failwith "Can't copy ⊥"
-  | V.Borrow bc -> (
-      (* We can only copy shared borrows *)
-      match bc with
-      | SharedBorrow bid ->
-          (* We need to create a new borrow id for the copied borrow, and
-           * update the context accordingly *)
-          let ctx, bid' = C.fresh_borrow_id ctx in
-          let ctx = reborrow_shared bid bid' ctx in
-          (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
-      | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow"
-      | V.InactivatedMutBorrow _ ->
-          failwith "Can't copy an inactivated mut borrow")
-  | V.Loan lc -> (
-      (* We can only copy shared loans *)
-      match lc with
-      | V.MutLoan _ -> failwith "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 (
-        type_is_primitively_copyable (Subst.erase_regions sp.V.svalue.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)
-
 (** Convert a constant operand value to a typed value *)
 let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
     (cv : E.operand_constant_value) : V.typed_value =
@@ -1243,50 +473,6 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
 (** Result of evaluating a statement *)
 type statement_eval_res = Unit | Break of int | Continue of int | Return
 
-(** Small utility.
-    
-    Prepare a place which is to be used as the destination of an assignment:
-    update the environment along the paths, end the borrows and 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 loan or borrow (and we check
-    it is the case). Note that it is very likely to contain [Bottom] values.
- *)
-let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) :
-    C.eval_ctx * V.typed_value =
-  (* TODO *)
-  let access = Write in
-  let ctx = update_ctx_along_write_place config access p ctx in
-  (* End the borrows and loans, starting with the borrows *)
-  let ctx = drop_borrows_loans_at_lplace config p ctx in
-  (* Read the value and check it *)
-  let v = read_place_unwrap config access p ctx in
-  (* Sanity checks *)
-  assert (not (loans_in_value v));
-  assert (not (borrows_in_value v));
-  (* Return *)
-  (ctx, v)
-
-(** Read the value at a given place.
-    As long as it is a loan, end the loan.
-    This function doesn't perform a recursive exploration:
-    it won't dive into the value to end all the inner
-    loans (contrary to [drop_borrows_loans_at_lplace] for
-    instance).
- *)
-let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
-    (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
-  let v = read_place_unwrap config access p ctx in
-  match v.V.value with
-  | V.Loan (V.SharedLoan (bids, _)) ->
-      let ctx = end_outer_borrows config bids ctx in
-      end_loan_exactly_at_place config access p ctx
-  | V.Loan (V.MutLoan bid) ->
-      let ctx = end_outer_borrow config bid ctx in
-      end_loan_exactly_at_place config access p ctx
-  | _ -> ctx
-
 (** Updates the discriminant of a value at a given place.
 
     There are two situations:
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
new file mode 100644
index 00000000..7e9fa7dd
--- /dev/null
+++ b/src/InterpreterPaths.ml
@@ -0,0 +1,833 @@
+module T = Types
+module V = Values
+open Scalars
+module E = Expressions
+open Errors
+module C = Contexts
+module Subst = Substitute
+module A = CfimAst
+module L = Logging
+open TypesUtils
+open ValuesUtils
+module Inv = Invariants
+module S = Synthesis
+open Utils
+open InterpreterUtils
+open InterpreterProjectors
+open InterpreterBorrows
+open InterpreterExpansion
+
+(** Paths *)
+
+(** When we fail reading from or writing to a path, it might be because we
+    need to update the environment by ending borrows, expanding symbolic
+    values, etc. The following type is used to convey this information.
+    
+    TODO: compare with borrow_lres?
+*)
+type path_fail_kind =
+  | FailSharedLoan of V.BorrowId.Set.t
+      (** Failure because we couldn't go inside a shared loan *)
+  | FailMutLoan of V.BorrowId.id
+      (** Failure because we couldn't go inside a mutable loan *)
+  | FailInactivatedMutBorrow of V.BorrowId.id
+      (** Failure because we couldn't go inside an inactivated mutable borrow
+          (which should get activated) *)
+  | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp)
+      (** Failure because we need to enter a symbolic value (and thus need to expand it) *)
+  (* TODO: Remove the parentheses *)
+  | FailBottom of (int * E.projection_elem * T.ety)
+      (** Failure because we need to enter an any value - we can expand Bottom
+          values if they are left values. We return the number of elements which
+          were remaining in the path when we reached the error - this allows to
+          properly update the Bottom value, if needs be.
+       *)
+  | FailBorrow of V.borrow_content
+      (** We got stuck because we couldn't enter a borrow *)
+
+(** Result of evaluating a path (reading from a path/writing to a path)
+    
+    Note that when we fail, we return information used to update the
+    environment, as well as the 
+*)
+type 'a path_access_result = ('a, path_fail_kind) result
+(** The result of reading from/writing to a place *)
+
+type updated_read_value = { read : V.typed_value; updated : V.typed_value }
+
+type projection_access = {
+  enter_shared_loans : bool;
+  enter_mut_borrows : bool;
+  lookup_shared_borrows : bool;
+}
+
+(** Generic function to access (read/write) the value at the end of a projection.
+
+    We return the (eventually) updated value, the value we read at the end of
+    the place and the (eventually) updated environment.
+    
+    TODO: use exceptions?
+ *)
+let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
+    (* Function to (eventually) update the value we find *)
+      (update : V.typed_value -> V.typed_value) (p : E.projection)
+    (v : V.typed_value) : (C.eval_ctx * updated_read_value) path_access_result =
+  (* For looking up/updating shared loans *)
+  let ek : exploration_kind =
+    { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
+  in
+  match p with
+  | [] ->
+      let nv = update v in
+      (* Type checking *)
+      if nv.ty <> v.ty then (
+        L.log#lerror
+          (lazy
+            ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: "
+           ^ T.show_ety v.ty));
+        failwith
+          "Assertion failed: new value doesn't have the same type as its \
+           destination");
+      Ok (ctx, { read = v; updated = nv })
+  | pe :: p' -> (
+      (* Match on the projection element and the value *)
+      match (pe, v.V.value, v.V.ty) with
+      (* Field projection - ADTs *)
+      | ( Field (ProjAdt (def_id, opt_variant_id), field_id),
+          V.Adt adt,
+          T.Adt (T.AdtId def_id', _, _) ) -> (
+          assert (def_id = def_id');
+          (* Check that the projection is consistent with the current value *)
+          (match (opt_variant_id, adt.variant_id) with
+          | None, None -> ()
+          | Some vid, Some vid' -> if vid <> vid' then failwith "Unreachable"
+          | _ -> failwith "Unreachable");
+          (* Actually project *)
+          let fv = T.FieldId.nth adt.field_values field_id in
+          match access_projection access ctx update p' fv with
+          | Error err -> Error err
+          | Ok (ctx, res) ->
+              (* Update the field value *)
+              let nvalues =
+                T.FieldId.update_nth adt.field_values field_id res.updated
+              in
+              let nadt = V.Adt { adt with V.field_values = nvalues } in
+              let updated = { v with value = nadt } in
+              Ok (ctx, { res with updated }))
+      (* Tuples *)
+      | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> (
+          assert (arity = List.length adt.field_values);
+          let fv = T.FieldId.nth adt.field_values field_id in
+          (* Project *)
+          match access_projection access ctx update p' fv with
+          | Error err -> Error err
+          | Ok (ctx, res) ->
+              (* Update the field value *)
+              let nvalues =
+                T.FieldId.update_nth adt.field_values field_id res.updated
+              in
+              let ntuple = V.Adt { adt with field_values = nvalues } in
+              let updated = { v with value = ntuple } in
+              Ok (ctx, { res with updated })
+          (* If we reach Bottom, it may mean we need to expand an uninitialized
+           * enumeration value *))
+      | Field (ProjAdt (_, _), _), V.Bottom, _ ->
+          Error (FailBottom (1 + List.length p', pe, v.ty))
+      | Field (ProjTuple _, _), V.Bottom, _ ->
+          Error (FailBottom (1 + List.length p', pe, v.ty))
+      (* Symbolic value: needs to be expanded *)
+      | _, Symbolic sp, _ ->
+          (* Expand the symbolic value *)
+          Error (FailSymbolic (pe, sp))
+      (* Box dereferencement *)
+      | ( DerefBox,
+          Adt { variant_id = None; field_values = [ bv ] },
+          T.Adt (T.Assumed T.Box, _, _) ) -> (
+          (* We allow moving inside of boxes. In practice, this kind of
+           * manipulations should happen only inside unsage code, so
+           * it shouldn't happen due to user code, and we leverage it
+           * when implementing box dereferencement for the concrete
+           * interpreter *)
+          match access_projection access ctx update p' bv with
+          | Error err -> Error err
+          | Ok (ctx, res) ->
+              let nv =
+                {
+                  v with
+                  value =
+                    V.Adt { variant_id = None; field_values = [ res.updated ] };
+                }
+              in
+              Ok (ctx, { res with updated = nv }))
+      (* Borrows *)
+      | Deref, V.Borrow bc, _ -> (
+          match bc with
+          | V.SharedBorrow bid ->
+              (* Lookup the loan content, and explore from there *)
+              if access.lookup_shared_borrows then
+                match lookup_loan ek bid ctx with
+                | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan"
+                | _, Concrete (V.SharedLoan (bids, sv)) -> (
+                    (* Explore the shared value *)
+                    match access_projection access ctx update p' sv with
+                    | Error err -> Error err
+                    | Ok (ctx, res) ->
+                        (* Update the shared loan with the new value returned
+                           by [access_projection] *)
+                        let ctx =
+                          update_loan ek bid
+                            (V.SharedLoan (bids, res.updated))
+                            ctx
+                        in
+                        (* Return - note that we don't need to update the borrow itself *)
+                        Ok (ctx, { res with updated = v }))
+                | ( _,
+                    Abstract
+                      ( V.AMutLoan (_, _)
+                      | V.AEndedMutLoan { given_back = _; child = _ }
+                      | V.AEndedSharedLoan (_, _)
+                      | V.AIgnoredMutLoan (_, _)
+                      | V.AEndedIgnoredMutLoan { given_back = _; child = _ }
+                      | V.AIgnoredSharedLoan _ ) ) ->
+                    failwith "Expected a shared (abstraction) loan"
+                | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> (
+                    (* Explore the shared value *)
+                    match access_projection access ctx update p' sv with
+                    | Error err -> Error err
+                    | Ok (ctx, res) ->
+                        (* Relookup the child avalue *)
+                        let av =
+                          match lookup_loan ek bid ctx with
+                          | _, Abstract (V.ASharedLoan (_, _, av)) -> av
+                          | _ -> failwith "Unexpected"
+                        in
+                        (* Update the shared loan with the new value returned
+                             by [access_projection] *)
+                        let ctx =
+                          update_aloan ek bid
+                            (V.ASharedLoan (bids, res.updated, av))
+                            ctx
+                        in
+                        (* Return - note that we don't need to update the borrow itself *)
+                        Ok (ctx, { res with updated = v }))
+              else Error (FailBorrow bc)
+          | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid)
+          | V.MutBorrow (bid, bv) ->
+              if access.enter_mut_borrows then
+                match access_projection access ctx update p' bv with
+                | Error err -> Error err
+                | Ok (ctx, res) ->
+                    let nv =
+                      {
+                        v with
+                        value = V.Borrow (V.MutBorrow (bid, res.updated));
+                      }
+                    in
+                    Ok (ctx, { res with updated = nv })
+              else Error (FailBorrow bc))
+      | _, V.Loan lc, _ -> (
+          match lc with
+          | V.MutLoan bid -> Error (FailMutLoan bid)
+          | V.SharedLoan (bids, sv) ->
+              (* If we can enter shared loan, we ignore the loan. Pay attention
+                 to the fact that we need to reexplore the *whole* place (i.e,
+                 we mustn't ignore the current projection element *)
+              if access.enter_shared_loans then
+                match access_projection access ctx update (pe :: p') sv with
+                | Error err -> Error err
+                | Ok (ctx, res) ->
+                    let nv =
+                      {
+                        v with
+                        value = V.Loan (V.SharedLoan (bids, res.updated));
+                      }
+                    in
+                    Ok (ctx, { res with updated = nv })
+              else Error (FailSharedLoan bids))
+      | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r ->
+          let pe, v, ty = r in
+          let pe = "- pe: " ^ E.show_projection_elem pe in
+          let v = "- v:\n" ^ V.show_value v in
+          let ty = "- ty:\n" ^ T.show_ety ty in
+          L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
+          failwith "Inconsistent projection")
+
+(** Generic function to access (read/write) the value at a given place.
+
+    We return the value we read at the place and the (eventually) updated
+    environment, if we managed to access the place, or the precise reason
+    why we failed.
+ *)
+let access_place (access : projection_access)
+    (* Function to (eventually) update the value we find *)
+      (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx)
+    : (C.eval_ctx * V.typed_value) path_access_result =
+  (* Lookup the variable's value *)
+  let value = C.ctx_lookup_var_value ctx p.var_id in
+  (* Apply the projection *)
+  match access_projection access ctx update p.projection value with
+  | Error err -> Error err
+  | Ok (ctx, res) ->
+      (* Update the value *)
+      let ctx = C.ctx_update_var_value ctx p.var_id res.updated in
+      (* Return *)
+      Ok (ctx, res.read)
+
+type access_kind =
+  | Read  (** We can go inside borrows and loans *)
+  | Write  (** Don't enter shared borrows or shared loans *)
+  | Move  (** Don't enter borrows or loans *)
+
+let access_kind_to_projection_access (access : access_kind) : projection_access
+    =
+  match access with
+  | Read ->
+      {
+        enter_shared_loans = true;
+        enter_mut_borrows = true;
+        lookup_shared_borrows = true;
+      }
+  | Write ->
+      {
+        enter_shared_loans = false;
+        enter_mut_borrows = true;
+        lookup_shared_borrows = false;
+      }
+  | Move ->
+      {
+        enter_shared_loans = false;
+        enter_mut_borrows = false;
+        lookup_shared_borrows = false;
+      }
+
+(** Read the value at a given place *)
+let 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 *)
+  let update v = v in
+  match access_place access update p ctx with
+  | Error err -> Error err
+  | Ok (ctx1, read_value) ->
+      (* Note that we ignore the new environment: it should be the same as the
+         original one.
+      *)
+      if config.check_invariants then
+        if ctx1 <> ctx then (
+          let msg =
+            "Unexpected environment update:\nNew environment:\n"
+            ^ C.show_env ctx1.env ^ "\n\nOld environment:\n"
+            ^ C.show_env ctx.env
+          in
+          L.log#serror msg;
+          failwith "Unexpected environment update");
+      Ok read_value
+
+let read_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
+    (ctx : C.eval_ctx) : V.typed_value =
+  match read_place config access p ctx with
+  | Error _ -> failwith "Unreachable"
+  | Ok v -> v
+
+(** Update the value at a given place *)
+let 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 *)
+  let update _ = nv in
+  match access_place access update p ctx with
+  | Error err -> Error err
+  | Ok (ctx, _) ->
+      (* We ignore the read value *)
+      Ok ctx
+
+let write_place_unwrap (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
+  | Error _ -> failwith "Unreachable"
+  | Ok ctx -> ctx
+
+(** Compute an expanded ADT bottom value *)
+let compute_expanded_bottom_adt_value (tyctx : T.type_def list)
+    (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
+    (regions : T.erased_region list) (types : T.ety list) : V.typed_value =
+  (* Lookup the definition and check if it is an enumeration - it
+     should be an enumeration if and only if the projection element
+     is a field projection with *some* variant id. Retrieve the list
+     of fields at the same time. *)
+  let def = T.TypeDefId.nth tyctx def_id in
+  assert (List.length regions = List.length def.T.region_params);
+  (* Compute the field types *)
+  let field_types =
+    Subst.type_def_get_instantiated_field_etypes def opt_variant_id types
+  in
+  (* Initialize the expanded value *)
+  let fields =
+    List.map
+      (fun ty : V.typed_value -> ({ V.value = V.Bottom; ty } : V.typed_value))
+      field_types
+  in
+  let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in
+  let ty = T.Adt (T.AdtId def_id, regions, types) in
+  { V.value = av; V.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 *)
+  let fields =
+    List.map (fun ty : V.typed_value -> { V.value = Bottom; ty }) field_types
+  in
+  let v = V.Adt { variant_id = None; field_values = fields } in
+  let ty = T.Adt (T.Tuple, [], field_types) in
+  { V.value = v; V.ty }
+
+(** Auxiliary helper to expand [Bottom] values.
+
+    During compilation, rustc desaggregates the ADT initializations. The
+    consequence is that the following rust code:
+    ```
+    let x = Cons a b;
+    ```
+
+    Looks like this in MIR:
+    ```
+    (x as Cons).0 = a;
+    (x as Cons).1 = b;
+    set_discriminant(x, 0); // If `Cons` is the variant of index 0
+    ```
+
+    The consequence is that we may sometimes need to write fields to values
+    which are currently [Bottom]. When doing this, we first expand the value
+    to, say, [Cons Bottom Bottom] (note that field projection contains information
+    about which variant we should project to, which is why we *can* set the
+    variant index when writing one of its fields).
+*)
+let expand_bottom_value_from_projection (config : C.config)
+    (access : access_kind) (p : E.place) (remaining_pes : int)
+    (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Debugging *)
+  L.log#ldebug
+    (lazy
+      ("expand_bottom_value_from_projection:\n" ^ "pe: "
+     ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty));
+  (* Prepare the update: we need to take the proper prefix of the place
+     during whose evaluation we got stuck *)
+  let projection' =
+    fst
+      (Utilities.list_split_at p.projection
+         (List.length p.projection - remaining_pes))
+  in
+  let p' = { p with projection = projection' } in
+  (* Compute the expanded value.
+     The type of the [Bottom] value should be a tuple or an ADT.
+     Note that the projection element we got stuck at should be a
+     field projection, and gives the variant id if the [Bottom] value
+     is an enumeration value.
+     Also, the expanded value should be the proper ADT variant or a tuple
+     with the proper arity, with all the fields initialized to [Bottom]
+  *)
+  let nv =
+    match (pe, ty) with
+    (* "Regular" ADTs *)
+    | ( Field (ProjAdt (def_id, opt_variant_id), _),
+        T.Adt (T.AdtId def_id', regions, types) ) ->
+        assert (def_id = def_id');
+        compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id
+          opt_variant_id regions types
+    (* Tuples *)
+    | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
+        assert (arity = List.length tys);
+        (* Generate the field values *)
+        compute_expanded_bottom_tuple_value tys
+    | _ ->
+        failwith
+          ("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
+  | Ok ctx -> ctx
+  | Error _ -> failwith "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) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Attempt to read the place: if it fails, update the environment and retry *)
+  match read_place config access p ctx with
+  | Ok _ -> ctx
+  | Error err ->
+      let ctx =
+        match err with
+        | FailSharedLoan bids -> end_outer_borrows config bids ctx
+        | FailMutLoan bid -> end_outer_borrow config bid ctx
+        | FailInactivatedMutBorrow bid ->
+            activate_inactivated_mut_borrow config Outer bid ctx
+        | FailSymbolic (pe, sp) ->
+            (* Expand the symbolic value *)
+            expand_symbolic_value_no_branching config pe sp ctx
+        | FailBottom (_, _, _) ->
+            (* We can't expand [Bottom] values while reading them *)
+            failwith "Found [Bottom] while reading a place"
+        | FailBorrow _ -> failwith "Could not read a borrow"
+      in
+      update_ctx_along_read_place config access p ctx
+
+(** Update the environment to be able to write to a place.
+
+    See [update_env_alond_read_place].
+*)
+let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
+    (p : E.place) (ctx : C.eval_ctx) : C.eval_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
+  | Ok _ -> ctx
+  | Error err ->
+      let ctx =
+        match err with
+        | FailSharedLoan bids -> end_outer_borrows config bids ctx
+        | FailMutLoan bid -> end_outer_borrow config bid ctx
+        | FailInactivatedMutBorrow bid ->
+            activate_inactivated_mut_borrow config Outer bid ctx
+        | FailSymbolic (pe, sp) ->
+            (* Expand the symbolic value *)
+            expand_symbolic_value_no_branching config pe sp ctx
+        | FailBottom (remaining_pes, pe, ty) ->
+            (* Expand the [Bottom] value *)
+            expand_bottom_value_from_projection config access p remaining_pes pe
+              ty ctx
+        | FailBorrow _ -> failwith "Could not write to a borrow"
+      in
+      update_ctx_along_write_place config access p ctx
+
+exception UpdateCtx of C.eval_ctx
+(** Small utility used to break control-flow *)
+
+(** End the loans at a given place: read the value, if it contains a loan,
+    end this loan, repeat.
+
+    This is used when reading, borrowing, writing to a value. 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) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Iterator to explore a value and update the context whenever we find
+   * loans.
+   * We use exceptions to make it handy: whenever we update the
+   * context, we raise an exception wrapping the updated context.
+   * *)
+  let obj =
+    object
+      inherit [_] V.iter_typed_value as super
+
+      method! visit_borrow_content env bc =
+        match bc with
+        | V.SharedBorrow _ | V.MutBorrow (_, _) ->
+            (* Nothing special to do *) super#visit_borrow_content env bc
+        | V.InactivatedMutBorrow bid ->
+            (* We need to activate inactivated borrows *)
+            let ctx = activate_inactivated_mut_borrow config Inner bid ctx in
+            raise (UpdateCtx ctx)
+
+      method! visit_loan_content env lc =
+        match lc with
+        | V.SharedLoan (bids, v) -> (
+            (* End the loans if we need a modification access, otherwise dive into
+               the shared value *)
+            match access with
+            | Read -> super#visit_SharedLoan env bids v
+            | Write | Move ->
+                let ctx = end_outer_borrows config bids ctx in
+                raise (UpdateCtx ctx))
+        | V.MutLoan bid ->
+            (* We always need to end mutable borrows *)
+            let ctx = end_outer_borrow config bid ctx in
+            raise (UpdateCtx ctx)
+    end
+  in
+
+  (* First, retrieve the value *)
+  match read_place config access p ctx with
+  | Error _ -> failwith "Unreachable"
+  | Ok v -> (
+      (* Inspect the value and update the context while doing so.
+         If the context gets updated: perform a recursive call (many things
+         may have been updated in the context: we need to re-read the value
+         at place [p] - and this value may actually not be accessible
+         anymore...)
+      *)
+      try
+        obj#visit_typed_value () v;
+        (* No context update required: return the current context *)
+        ctx
+      with UpdateCtx ctx ->
+        (* The context was updated: do a recursive call to reinspect the value *)
+        end_loans_at_place config access p ctx)
+
+(** Drop (end) all the loans and borrows at a given place, which should be
+    seen as an l-value (we will write to it later, but need to drop the borrows
+    before writing).
+
+    We start by only dropping the borrows, then we end the loans. The reason
+    is that some loan we find may be borrowed by another part of the subvalue.
+    In order to correctly handle the "outer borrow" priority (we should end
+    the outer borrows first) which is not really applied here (we are preparing
+    the value for override: we can end the borrows inside, without ending the
+    borrows we traversed to actually access the value) we first end the borrows
+    we find in the place, to make sure all the "local" loans are taken care of.
+    Then, if we find a loan, it means it is "externally" borrowed (the associated
+    borrow is not in a subvalue of the place under inspection).
+    Also note that whenever we end a loan, we might propagate back a value inside
+    the place under inspection: we must re-end all the borrows we find there,
+    before reconsidering loans.
+
+    Repeat:
+    - read the value at a given place
+    - as long as we find a loan or a borrow, end it
+
+    This is used to drop values (when we need to write to a place, we first
+    drop the value there to properly propagate back values which are not/can't
+    be borrowed anymore).
+ *)
+let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Iterator to explore a value and update the context whenever we find
+     borrows/loans.
+     We use exceptions to make it handy: whenever we update the
+     context, we raise an exception wrapping the updated context.
+
+     Note that we can end the borrows which are inside the value (while the
+     value itself might be inside a borrow/loan: we are thus ending inner
+     borrows). Because a loan inside the value may be linked to a borrow
+     somewhere else *also inside* the value (it's possible with adts),
+     we first end all the borrows we find - by using [Inner] to allow
+     ending inner borrows - then end all the loans we find.
+
+     It is really important to do this in two steps: the borrow linked to a
+     loan may be inside the value at place p, in which case this borrow may be
+     an inner borrow that we *can* end, but it may also be outside this
+     value, in which case we need to end all the outer borrows first...
+     Also, whenever the context is updated, we need to re-inspect
+     the value at place p *in two steps* again (end borrows, then end
+     loans).
+
+     Example:
+     =======
+     We want to end the borrows/loans at `*x` in the following environment:
+     ```
+     x -> mut_borrow l0 (mut_loan l1, mut_borrow l1 (Int 3), mut_loan l2)
+     y -> mut_borrow l2 (Bool true)
+     ```
+
+     We have to consider two things:
+     - the borrow `mut_borrow l1 (Int 3)` borrows a subvalue of `*x`
+     - the borrow corresponding to the loan `mut_loan l2` is outside of `*x`
+
+     We first end all the *borrows* (not the loans) inside of `*x`, which gives:
+     ```
+     x -> mut_borrow l0 (Int 3, ⊥, mut_loan l2)
+     y -> mut_borrow l2 (Bool true)
+     ```
+
+     Note that when ending the borrows, we can (and have to) ignore the outer
+     borrows (in this case `mut_borrow l0 ...`). Otherwise, we would have to end
+     the borrow `l0` which is incorrect (note that we might have to drop the
+     borrows/loans at `*x` if we evaluate, for instance, `*x = ...`).
+     It is ok to ignore outer borrows in this case because whenever
+     we end a borrow, it is an outer borrow locally to `*x` (i.e., we ignore
+     the outer borrows when accessing `*x`, but once examining the value at
+     `*x` we never dive into borrows: whenever we find one, we end it - it is thus
+     an outer borrow, in some way).
+
+     Then, we end the loans at `*x`. Note that as at this point `*x` doesn't
+     contain borrows (only loans), the borrows corresponding to those loans
+     are thus necessarily outside of `*x`: we mustn't ignore outer borrows this
+     time. This gives:
+     ```
+     x -> mut_borrow l0 (Int 3, ⊥, Bool true)
+     y -> ⊥
+     ```
+  *)
+  let obj =
+    object
+      inherit [_] V.iter_typed_value as super
+
+      method! visit_borrow_content end_loans bc =
+        (* Sanity check: we should have ended all the borrows before starting
+           to end loans *)
+        assert (not end_loans);
+
+        (* We need to end all borrows. Note that we ignore the outer borrows
+           when ending the borrows we find here (we call [end_inner_borrow(s)]:
+           the value at place p might be below a borrow/loan). Note however
+           that if we restrain ourselves at the value at place p, the borrow we
+           found here can be considered as an outer borrow.
+        *)
+        match bc with
+        | V.SharedBorrow bid | V.MutBorrow (bid, _) ->
+            raise (UpdateCtx (end_inner_borrow config bid ctx))
+        | V.InactivatedMutBorrow bid ->
+            (* We need to activate ithe nactivated borrow - later, we will
+             * actually end it - Rk.: we could actually end it straight away
+             * (this is not really important) *)
+            let ctx = activate_inactivated_mut_borrow config Inner bid ctx in
+            raise (UpdateCtx ctx)
+
+      method! visit_loan_content end_loans lc =
+        if
+          (* If we can, end the loans, otherwise ignore: keep for later *)
+          end_loans
+        then
+          (* We need to end all loans. Note that as all the borrows inside
+             the value at place p should already have ended, the borrows
+             associated to the loans we find here should be borrows from
+             outside this value: we need to call [end_outer_borrow(s)]
+             (we can't ignore outer borrows this time).
+          *)
+          match lc with
+          | V.SharedLoan (bids, _) ->
+              raise (UpdateCtx (end_outer_borrows config bids ctx))
+          | V.MutLoan bid -> raise (UpdateCtx (end_outer_borrow config bid ctx))
+        else super#visit_loan_content end_loans lc
+    end
+  in
+
+  (* We do something similar to [end_loans_at_place].
+     First, retrieve the value *)
+  match read_place config Write p ctx with
+  | Error _ -> failwith "Unreachable"
+  | Ok v -> (
+      (* Inspect the value and update the context while doing so.
+         If the context gets updated: perform a recursive call (many things
+         may have been updated in the context: first we need to retrieve the
+         proper updated value - and this value may actually not be accessible
+         anymore
+      *)
+      try
+        (* Inspect the value: end the borrows only *)
+        obj#visit_typed_value false v;
+        (* Inspect the value: end the loans *)
+        obj#visit_typed_value true v;
+        (* No context update required: return the current context *)
+        ctx
+      with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p 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).
+ *)
+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 =
+  (* 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.Concrete _ -> (ctx, v)
+  | V.Adt av ->
+      (* Sanity check *)
+      (match v.V.ty with
+      | T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value"
+      | T.Adt (T.AdtId _, _, _) -> assert allow_adt_copy
+      | T.Adt (T.Tuple, _, _) -> () (* Ok *)
+      | _ -> failwith "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 -> failwith "Can't copy ⊥"
+  | V.Borrow bc -> (
+      (* We can only copy shared borrows *)
+      match bc with
+      | SharedBorrow bid ->
+          (* We need to create a new borrow id for the copied borrow, and
+           * update the context accordingly *)
+          let ctx, bid' = C.fresh_borrow_id ctx in
+          let ctx = reborrow_shared bid bid' ctx in
+          (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
+      | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow"
+      | V.InactivatedMutBorrow _ ->
+          failwith "Can't copy an inactivated mut borrow")
+  | V.Loan lc -> (
+      (* We can only copy shared loans *)
+      match lc with
+      | V.MutLoan _ -> failwith "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 (
+        type_is_primitively_copyable (Subst.erase_regions sp.V.svalue.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 borrows and 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 loan or borrow (and we check
+    it is the case). Note that it is very likely to contain [Bottom] values.
+ *)
+let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) :
+    C.eval_ctx * V.typed_value =
+  (* TODO *)
+  let access = Write in
+  let ctx = update_ctx_along_write_place config access p ctx in
+  (* End the borrows and loans, starting with the borrows *)
+  let ctx = drop_borrows_loans_at_lplace config p ctx in
+  (* Read the value and check it *)
+  let v = read_place_unwrap config access p ctx in
+  (* Sanity checks *)
+  assert (not (loans_in_value v));
+  assert (not (borrows_in_value v));
+  (* Return *)
+  (ctx, v)
+
+(** Read the value at a given place.
+    As long as it is a loan, end the loan.
+    This function doesn't perform a recursive exploration:
+    it won't dive into the value to end all the inner
+    loans (contrary to [drop_borrows_loans_at_lplace] for
+    instance).
+ *)
+let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
+    (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
+  let v = read_place_unwrap config access p ctx in
+  match v.V.value with
+  | V.Loan (V.SharedLoan (bids, _)) ->
+      let ctx = end_outer_borrows config bids ctx in
+      end_loan_exactly_at_place config access p ctx
+  | V.Loan (V.MutLoan bid) ->
+      let ctx = end_outer_borrow config bid ctx in
+      end_loan_exactly_at_place config access p ctx
+  | _ -> ctx