Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2

Complete the constants extraction by making all functions fail

14 files changed, 328 insertions, 178 deletions

diff --git a/src/Cps.ml b/src/Cps.ml
index d7c50f26..2d7dd2be 100644
--- a/src/Cps.ml
+++ b/src/Cps.ml
@@ -77,7 +77,6 @@ let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun)
   comp f g
 
 let apply (f : cm_fun) (g : m_fun) : m_fun = fun ctx -> f g ctx
-
 let id_cm_fun : cm_fun = fun cf ctx -> cf ctx
 
 (** If we have a list of [inputs] of type `'a list` and a function [f] which
@@ -92,7 +91,37 @@ let id_cm_fun : cm_fun = fun cf ctx -> cf ctx
     
     See the unit test below for an illustration.
  *)
-let fold_left_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd)
+let fold_left_apply_continuation (f : 'a -> ('c -> 'd) -> 'c -> 'd)
+    (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd =
+  let rec eval_list (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd =
+   fun ctx ->
+    match inputs with
+    | [] -> cf ctx
+    | x :: inputs -> comp (f x) (fun cf -> eval_list inputs cf) cf ctx
+  in
+  eval_list inputs cf
+
+(** Unit test/example for [fold_left_apply_continuation] *)
+let _ =
+  fold_left_apply_continuation
+    (fun x cf (ctx : int) -> cf (ctx + x))
+    [ 1; 20; 300; 4000 ]
+    (fun (ctx : int) -> assert (ctx = 4321))
+    0
+
+(** If we have a list of [inputs] of type `'a list` and a function [f] which
+    evaluates one element of type `'a` to compute a result of type `'b` before
+    giving it to a continuation, the following function performs a fold operation:
+    it evaluates all the inputs one by one by accumulating the results in a list,
+    and gives the list to a continuation.
+    
+    Note that we make sure that the results are listed in the order in
+    which they were computed (the first element of the list is the result
+    of applying [f] to the first element of the inputs).
+    
+    See the unit test below for an illustration.
+ *)
+let fold_left_list_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd)
     (inputs : 'a list) (cf : 'b list -> 'c -> 'd) : 'c -> 'd =
   let rec eval_list (inputs : 'a list) (cf : 'b list -> 'c -> 'd)
       (outputs : 'b list) : 'c -> 'd =
@@ -104,9 +133,9 @@ let fold_left_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd)
   in
   eval_list inputs cf []
 
-(** Unit test/example for [fold_left_apply_continuation] *)
+(** Unit test/example for [fold_left_list_apply_continuation] *)
 let _ =
-  fold_left_apply_continuation
+  fold_left_list_apply_continuation
     (fun x cf (ctx : unit) -> cf (10 + x) ctx)
     [ 0; 1; 2; 3; 4 ]
     (fun values _ctx -> assert (values = [ 10; 11; 12; 13; 14 ]))
diff --git a/src/ExpressionsUtils.ml b/src/ExpressionsUtils.ml
new file mode 100644
index 00000000..c3ccfb15
--- /dev/null
+++ b/src/ExpressionsUtils.ml
@@ -0,0 +1,10 @@
+module E = Expressions
+
+let unop_can_fail (unop : E.unop) : bool =
+  match unop with Neg | Cast _ -> true | Not -> false
+
+let binop_can_fail (binop : E.binop) : bool =
+  match binop with
+  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
+  | Div | Rem | Add | Sub | Mul -> true
+  | Shl | Shr -> raise Errors.Unimplemented
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index ca20352f..ee4f71c1 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -9,6 +9,7 @@
 
 open LlbcAst
 open Modules
+module EU = ExpressionsUtils
 
 type fun_info = {
   can_fail : bool;
@@ -50,12 +51,14 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
     let divergent = ref false in
 
     let visit_fun (f : fun_decl) : unit =
-      print_endline ("@ fun: " ^ Print.fun_name_to_string f.name);
       let obj =
         object (self)
           inherit [_] iter_statement as super
 
           method may_fail b =
+            (* The fail flag is disabled for globals : the global body is
+             * normalised into its declaration, which is always successful.
+             *)
             if f.is_global then () else
             can_fail := !can_fail || b
 
@@ -63,8 +66,14 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
             self#may_fail true;
             super#visit_Assert env a
 
+            method! visit_rvalue _env rv =
+              match rv with
+              | Use _ | Ref _ | Discriminant _ | Aggregate _ -> ()
+              | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail
+              | BinaryOp (bop, _, _) ->
+                  can_fail := EU.binop_can_fail bop || !can_fail
+    
           method! visit_Call env call =
-            print_string "@ dep: ";
             pp_fun_id Format.std_formatter call.func;
             print_newline ();
 
@@ -90,15 +99,18 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
             super#visit_Loop env loop
         end
       in
-      match f.body with
+      (match f.body with
       | None ->
           (* Opaque function *)
           obj#may_fail true;
           stateful := use_state
-      | Some body -> obj#visit_statement () body.body
+      | Some body -> obj#visit_statement () body.body);
+      (* We ignore on purpose functions that cannot fail: the result of the analysis
+       * is not used yet to adjust the translation so that the functions which
+       * syntactically can't fail don't use an error monad. *)
+      can_fail := not f.is_global
     in
     List.iter visit_fun d;
-    print_endline ("@ can_fail: " ^ Bool.to_string !can_fail);
     { can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
   in
 
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5affea4c..f4f01ff8 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -86,9 +86,10 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
     in
     (ctx, avalues)
   in
+  let region_can_end _ = true in
   let ctx =
     create_push_abstractions_from_abs_region_groups call_id V.SynthInput
-      inst_sg.A.regions_hierarchy compute_abs_avalues ctx
+      inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
   in
   (* Split the variables between return var, inputs and remaining locals *)
   let body = Option.get fdef.body in
@@ -127,6 +128,21 @@ let evaluate_function_symbolic_synthesize_backward_from_return
   (* Move the return value out of the return variable *)
   let cf_pop_frame = ctx_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
+   * regions as non-endable, and, second, end those parent regions in
+   * proper order. *)
+  let parent_rgs = list_parent_region_groups sg back_id in
+  let parent_input_abs_ids =
+    T.RegionGroupId.mapi
+      (fun rg_id rg ->
+        if T.RegionGroupId.Set.mem rg_id parent_rgs then Some rg.T.id else None)
+      inst_sg.regions_hierarchy
+  in
+  let parent_input_abs_ids =
+    List.filter_map (fun x -> x) parent_input_abs_ids
+  in
+
   (* Insert the return value in the return abstractions (by applying
    * borrow projections) *)
   let cf_consume_ret ret_value ctx =
@@ -139,10 +155,20 @@ let evaluate_function_symbolic_synthesize_backward_from_return
       in
       (ctx, [ avalue ])
     in
-    (* Initialize and insert the abstractions in the context *)
+
+    (* Initialize and insert the abstractions in the context.
+     *
+     * We take care of disallowing ending the return regions which we
+     * shouldn't end (see the documentation of the `can_end` field of [abs]
+     * for more information. *)
+    let parent_and_current_rgs = T.RegionGroupId.Set.add back_id parent_rgs in
+    let region_can_end rid =
+      T.RegionGroupId.Set.mem rid parent_and_current_rgs
+    in
+    assert (region_can_end back_id);
     let ctx =
       create_push_abstractions_from_abs_region_groups ret_call_id V.SynthRet
-        ret_inst_sg.A.regions_hierarchy compute_abs_avalues ctx
+        ret_inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
     in
 
     (* We now need to end the proper *input* abstractions - pay attention
@@ -150,17 +176,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return
      * abstractions (of course, the corresponding return abstractions will
      * automatically be ended, because they consumed values coming from the
      * input abstractions...) *)
-    let parent_rgs = list_parent_region_groups sg back_id in
-    let parent_input_abs_ids =
-      T.RegionGroupId.mapi
-        (fun rg_id rg ->
-          if T.RegionGroupId.Set.mem rg_id parent_rgs then Some rg.T.id
-          else None)
-        inst_sg.regions_hierarchy
-    in
-    let parent_input_abs_ids =
-      List.filter_map (fun x -> x) parent_input_abs_ids
-    in
     (* End the parent abstractions and the current abstraction - note that we
      * end them in an order which follows the regions hierarchy: it should lead
      * to generated code which has a better consistency between the parent
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index f5f3a8fa..a13ac786 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -985,6 +985,9 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
   (* Lookup the abstraction *)
   let abs = C.ctx_lookup_abs ctx abs_id in
 
+  (* Check that we can end the abstraction *)
+  assert abs.can_end;
+
   (* End the parent abstractions first *)
   let cc = end_abstractions config chain abs.parents in
   let cc =
@@ -1439,12 +1442,22 @@ let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun =
     - it mustn't contain [Bottom]
     - it mustn't contain inactivated borrows
     TODO: this kind of checks should be put in an auxiliary helper, because
-    they are redundant
+    they are redundant.
+
+    The loan to update mustn't be a borrowed value.
  *)
 let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
-  (* Lookup the shared loan *)
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("promote_shared_loan_to_mut_loan:\n- loan: " ^ V.BorrowId.to_string l
+     ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+  (* Lookup the shared loan - note that we can't promote a shared loan
+   * in a shared value, but we can do it in a mutably borrowed value.
+   * This is important because we can do: `let y = &two-phase ( *x );`
+   *)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
@@ -1545,7 +1558,10 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
              the borrow we want to promote *)
           let bids = V.BorrowId.Set.remove l bids in
           let cc = end_outer_borrows config bids in
-          (* Promote the loan *)
+          (* 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
+           * the borrow. *)
           let cc = comp cc (promote_shared_loan_to_mut_loan l) in
           (* Promote the borrow - the value should have been checked by
              [promote_shared_loan_to_mut_loan]
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 0b65a372..c34051a8 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -188,8 +188,6 @@ let replace_symbolic_values (at_most_once : bool)
   in
   (* Apply the substitution *)
   let ctx = obj#visit_eval_ctx None ctx in
-  (* Check that we substituted *)
-  assert !replaced;
   (* Return *)
   ctx
 
@@ -469,8 +467,24 @@ 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 value which is not an enumeration with several variants
-    (i.e., in a situation where it doesn't lead to branching).
+(** 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 =
+ fun ctx ->
+  (* Compute the expanded value *)
+  let original_sv = sp in
+  let original_sv_place = sp_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 *)
+  let see_true = V.SeConcrete (V.Bool true) in
+  let see_false = V.SeConcrete (V.Bool false) in
+  let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
+  (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
+  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.
@@ -554,14 +568,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
     (* Booleans *)
     | T.Bool ->
         assert allow_branching;
-        (* Expand the symbolic value to true or false and continue execution *)
-        let see_true = V.SeConcrete (V.Bool true) in
-        let see_false = V.SeConcrete (V.Bool false) in
-        let seel = [ see_true; see_false ] in
-        let seel = List.map (fun see -> (Some see, cf)) seel in
-        (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
-        apply_branching_symbolic_expansions_non_borrow config original_sv
-          original_sv_place seel ctx
+        expand_symbolic_bool config sp sp_place cf cf ctx
     | _ ->
         raise
           (Failure ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty))
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 57ee0526..04ad1b3c 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -7,6 +7,7 @@ open Errors
 module C = Contexts
 module Subst = Substitute
 module L = Logging
+module PV = Print.Values
 open TypesUtils
 open ValuesUtils
 module Inv = Invariants
@@ -49,50 +50,93 @@ let expand_primitively_copyable_at_place (config : C.config)
   (* Apply *)
   expand cf ctx
 
+(** Read a place (CPS-style function).
+
+    We also check that the value *doesn't contain bottoms or inactivated
+    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
+  (* 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 *)
+  assert (not (inactivated_in_value v));
+  (* Call the continuation *)
+  cf v ctx
+
 (** Small utility.
 
+    Prepare the access to a place in a right-value (typically an operand) by
+    reorganizing the environment.
+
+    We reorganize the environment so that:
+    - we can access the place (we prepare *along* the path)
+    - the value at the place itself doesn't contain loans (the `access_kind`
+      controls whether we only end mutable loans, or also shared loans).
+
+    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.
  *)
-let prepare_rplace (config : C.config) (expand_prim_copy : bool)
-    (access : access_kind) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun =
+let access_rplace_reorganize_and_read (config : C.config)
+    (expand_prim_copy : bool) (access : access_kind) (p : E.place)
+    (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
+  (* Make sure we can evaluate the path *)
   let cc = update_ctx_along_read_place config access p in
+  (* End the proper loans at the place itself *)
   let cc = comp cc (end_loans_at_place config access p) in
+  (* Expand the copyable values which contain borrows (which are necessarily shared
+   * borrows) *)
   let cc =
     if expand_prim_copy then
       comp cc (expand_primitively_copyable_at_place config access p)
     else cc
   in
-  let read_place cf : m_fun =
-   fun ctx ->
-    let v = read_place_unwrap config access p ctx in
-    cf v ctx
-  in
+  (* Read the place - note that this checks that the value doesn't contain bottoms *)
+  let read_place = read_place config access p in
+  (* Compose *)
   comp cc read_place cf ctx
 
-(** Convert a constant operand value to a typed value *)
-let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_value =
-  (* Check the type while converting -
-   * we actually need some information contained in the type *)
+let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool)
+    (access : access_kind) (p : E.place) : cm_fun =
+ fun cf ctx ->
+  access_rplace_reorganize_and_read config expand_prim_copy access p
+    (fun _v -> cf)
+    ctx
+
+(** Convert an operand constant operand value to a typed value *)
+let typecheck_constant_value (ty : T.ety)
+    (cv : V.constant_value) : V.typed_value =
+  (* Check the type while converting - we actually need some information
+  * contained in the type *)
+  log#ldebug
+    (lazy
+      ("typecheck_constant_value:" ^ "\n- cv: "
+      ^ PV.constant_value_to_string cv));
   match (ty, cv) with
   (* Scalar, boolean... *)
-  | T.Bool, (Bool v)   -> { V.value = V.Concrete (Bool v);   ty }
-  | T.Char, (Char v)   -> { V.value = V.Concrete (Char v);   ty }
-  | T.Str,  (String v) -> { V.value = V.Concrete (String v); ty }
-  | T.Integer int_ty, (V.Scalar v) ->
+  | T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty }
+  | T.Char, Char v -> { V.value = V.Concrete (Char v); ty }
+  | T.Str, String v -> { V.value = V.Concrete (String v); ty }
+  | T.Integer int_ty, V.Scalar v ->
       (* Check the type and the ranges *)
       assert (int_ty = v.int_ty);
       assert (check_scalar_value_in_range v);
       { V.value = V.Concrete (V.Scalar v); ty }
   (* Remaining cases (invalid) - listing as much as we can on purpose
     (allows to catch errors at compilation if the definitions change) *)
-  | _, _ -> failwith "Improperly typed constant value"
+  | _, _ ->
+      failwith "Improperly typed constant value"
 
-(** Prepare the evaluation of an operand.
+(** Reorganize the environment in preparation for the evaluation of an operand.
 
-    Evaluating an operand requires updating the context to get access to a
-    given place (by ending borrows, expanding symbolic values...) then
+    Evaluating an operand requires reorganizing the environment to get access
+    to a given place (by ending borrows, expanding symbolic values...) then
     applying the operand operation (move, copy, etc.).
     
     Sometimes, we want to decouple the two operations.
@@ -106,7 +150,7 @@ let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_valu
     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").
@@ -114,58 +158,56 @@ let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_valu
     By first "preparing" the operands evaluation, we make sure no such thing
     happens. To be more precise, we make sure all the updates to borrows triggered
     by access *and* move operations have already been applied.
+
+    Rk.: in the formalization, we always have an explicit "reorganization" step
+    in the rule premises, before the actual operand evaluation.
     
-    As a side note: doing this is actually not completely necessary because when
+    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 formal semantics.
+    what we do in the formalization (because we don't enforce constraints
+    in the formalization).
  *)
-let eval_operand_prepare (config : C.config) (op : E.operand)
-    (cf : V.typed_value -> m_fun) : m_fun =
- fun ctx ->
-  let prepare (cf : V.typed_value -> m_fun) : m_fun =
-   fun ctx ->
+let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
+    cm_fun =
+ fun cf ctx ->
+  let prepare : cm_fun =
+   fun cf ctx ->
     match op with
     | Expressions.Constant (ty, cv) ->
-        cf (typecheck_constant_value ty cv) ctx
+        typecheck_constant_value ty cv |> ignore;
+        cf ctx
     | Expressions.Copy p ->
         (* Access the value *)
         let access = Read in
         (* Expand the symbolic values, if necessary *)
         let expand_prim_copy = true in
-        prepare_rplace config expand_prim_copy access p cf ctx
+        access_rplace_reorganize config expand_prim_copy access p cf ctx
     | Expressions.Move p ->
         (* Access the value *)
         let access = Move in
         let expand_prim_copy = false in
-        prepare_rplace config expand_prim_copy access p cf ctx
+        access_rplace_reorganize config expand_prim_copy access p cf ctx
   in
-  (* Sanity check *)
-  let check cf v : m_fun =
-   fun ctx ->
-    assert (not (bottom_in_value ctx.ended_regions v));
-    cf v ctx
-  in
-  (* Compose and apply *)
-  comp prepare check cf ctx
+  (* Apply *)
+  prepare cf ctx
 
-(** Evaluate an operand. *)
-let eval_operand (config : C.config) (op : E.operand)
+(** Evaluate an operand, without reorganizing the context before *)
+let eval_operand_no_reorganize (config : C.config) (op : E.operand)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug
     (lazy
-      ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n"
-     ^ eval_ctx_to_string ctx ^ "\n"));
+      ("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op
+     ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Evaluate *)
   match op with
   | Expressions.Constant (ty, cv) -> cf (typecheck_constant_value ty cv) ctx
   | Expressions.Copy p ->
       (* Access the value *)
       let access = Read in
-      let expand_prim_copy = true in
-      let cc = prepare_rplace config expand_prim_copy access p in
+      let cc = read_place config access p in
       (* Copy the value *)
       let copy cf v : m_fun =
        fun ctx ->
@@ -175,8 +217,8 @@ let eval_operand (config : C.config) (op : E.operand)
           Option.is_none
             (find_first_primitively_copyable_sv_with_borrows
                ctx.type_context.type_infos v));
-        let allow_adt_copy = false in
         (* Actually perform the copy *)
+        let allow_adt_copy = false in
         let ctx, v = copy_value allow_adt_copy config ctx v in
         (* Continue *)
         cf v ctx
@@ -186,11 +228,11 @@ let eval_operand (config : C.config) (op : E.operand)
   | Expressions.Move p ->
       (* Access the value *)
       let access = Move in
-      let expand_prim_copy = false in
-      let cc = prepare_rplace config expand_prim_copy access p in
+      let cc = read_place config access p in
       (* Move the value *)
       let move cf v : m_fun =
        fun ctx ->
+        (* 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
@@ -200,24 +242,49 @@ let eval_operand (config : C.config) (op : E.operand)
       (* 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 ->
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n"
+     ^ eval_ctx_to_string ctx ^ "\n"));
+  (* We reorganize the context, then evaluate the operand *)
+  comp
+    (prepare_eval_operand_reorganize config op)
+    (eval_operand_no_reorganize config op)
+    cf ctx
+
 (** Small utility.
 
-    See [eval_operand_prepare].
+    See [prepare_eval_operand_reorganize].
  *)
-let eval_operands_prepare (config : C.config) (ops : E.operand list)
-    (cf : V.typed_value list -> m_fun) : m_fun =
-  fold_left_apply_continuation (eval_operand_prepare config) ops cf
+let prepare_eval_operands_reorganize (config : C.config) (ops : E.operand list)
+    : cm_fun =
+  fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops
 
 (** Evaluate several operands. *)
 let eval_operands (config : C.config) (ops : E.operand list)
     (cf : V.typed_value list -> m_fun) : m_fun =
  fun ctx ->
   (* Prepare the operands *)
-  let prepare = eval_operands_prepare config ops in
+  let prepare = prepare_eval_operands_reorganize config ops in
   (* Evaluate the operands *)
-  let eval = fold_left_apply_continuation (eval_operand config) ops in
+  let eval =
+    fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops
+  in
   (* Compose and apply *)
-  comp prepare (fun cf (_ : V.typed_value list) -> eval cf) cf ctx
+  comp prepare eval cf ctx
 
 let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand)
     (cf : V.typed_value * V.typed_value -> m_fun) : m_fun =
@@ -436,7 +503,9 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
   (* Access the value *)
   let access = Read in
   let expand_prim_copy = false in
-  let prepare = prepare_rplace config expand_prim_copy access p in
+  let prepare =
+    access_rplace_reorganize_and_read config expand_prim_copy access p
+  in
   (* Read the value *)
   let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
     (* The value may be shared: we need to ignore the shared loans *)
@@ -474,7 +543,9 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
   (* Access the value *)
   let access = Read in
   let expand_prim_copy = false in
-  let prepare = prepare_rplace config expand_prim_copy access p in
+  let prepare =
+    access_rplace_reorganize_and_read config expand_prim_copy access p
+  in
   (* Read the value *)
   let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
    fun ctx ->
@@ -506,7 +577,9 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
       (* Access the value *)
       let access = if bkind = E.Shared then Read else Write in
       let expand_prim_copy = false in
-      let prepare = prepare_rplace config expand_prim_copy access p in
+      let prepare =
+        access_rplace_reorganize_and_read config expand_prim_copy access p
+      in
       (* Evaluate the borrowing operation *)
       let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
        fun ctx ->
@@ -547,7 +620,9 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
       (* Access the value *)
       let access = Write in
       let expand_prim_copy = false in
-      let prepare = prepare_rplace config expand_prim_copy access p in
+      let prepare =
+        access_rplace_reorganize_and_read config expand_prim_copy access p
+      in
       (* Evaluate the borrowing operation *)
       let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
        fun ctx ->
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 52742703..edd27138 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -304,7 +304,11 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
         lookup_shared_borrows = false;
       }
 
-(** Read the value at a given place *)
+(** 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)
     (ctx : C.eval_ctx) : V.typed_value path_access_result =
   let access = access_kind_to_projection_access access in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index e5564d59..8f981174 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -150,13 +150,10 @@ let eval_assertion_concrete (config : C.config) (assertion : A.assertion) :
  *)
 let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
  fun cf ctx ->
-  (* There may be a symbolic expansion, so don't fully evaluate the operand
-   * (if we moved the value, we can't expand it because it is hanging in
-   * thin air, outside of the environment...): simply update the environment
-   * to make sure we have access to the value we want to check. *)
-  let prepare = eval_operand_prepare config assertion.cond in
+  (* Evaluate the operand *)
+  let eval_op = eval_operand config assertion.cond in
   (* Evaluate the assertion *)
-  let eval cf (v : V.typed_value) : m_fun =
+  let eval_assert cf (v : V.typed_value) : m_fun =
    fun ctx ->
     assert (v.ty = T.Bool);
     (* We make a choice here: we could completely decouple the concrete and
@@ -171,20 +168,22 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
     | Symbolic sv ->
         assert (config.mode = C.SymbolicMode);
         assert (sv.V.sv_ty = T.Bool);
-        (* Expand the symbolic value, then call the evaluation function for the
-         * non-symbolic case *)
-        let allow_branching = true in
+        (* Expand the symbolic value and call the proper continuation functions
+         * for the true and false cases - TODO: call an "assert" function instead *)
+        let cf_true : m_fun = fun ctx -> cf Unit ctx in
+        let cf_false : m_fun = fun ctx -> cf Panic ctx in
         let expand =
-          expand_symbolic_value config allow_branching sv
+          expand_symbolic_bool config sv
             (S.mk_opt_place_from_op assertion.cond ctx)
+            cf_true cf_false
         in
-        comp expand (eval_assertion_concrete config assertion) cf ctx
+        expand ctx
     | _ ->
         raise
           (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v))
   in
   (* Compose and apply *)
-  comp prepare eval cf ctx
+  comp eval_op eval_assert cf ctx
 
 (** Updates the discriminant of a value at a given place.
 
@@ -678,9 +677,13 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
  
     Create abstractions (with no avalues, which have to be inserted afterwards)
     from a list of abs region groups.
+    
+    [region_can_end]: gives the region groups from which we generate functions
+    which can end or not.
  *)
 let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
-    (kind : V.abs_kind) (rgl : A.abs_region_group list) : V.abs list =
+    (kind : V.abs_kind) (rgl : A.abs_region_group list)
+    (region_can_end : T.RegionGroupId.id -> bool) : V.abs list =
   (* We use a reference to progressively create a map from abstraction ids
    * to set of ancestor regions. Note that abs_to_ancestors_regions[abs_id]
    * returns the union of:
@@ -715,6 +718,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
     let ancestors_regions_union_current_regions =
       T.RegionId.Set.union ancestors_regions regions
     in
+    let can_end = region_can_end back_id in
     abs_to_ancestors_regions :=
       V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
         !abs_to_ancestors_regions;
@@ -724,6 +728,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
       call_id;
       back_id;
       kind;
+      can_end;
       parents;
       original_parents;
       regions;
@@ -738,6 +743,9 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
 
     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
@@ -747,12 +755,14 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
 *)
 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)
     (compute_abs_avalues :
       V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let empty_absl =
     create_empty_abstractions_from_abs_region_groups call_id kind rgl
+      region_can_end
   in
 
   (* Compute and add the avalues to the abstractions, the insert the abstractions
@@ -832,8 +842,14 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
         eval_function_call config call cf ctx
     | A.FakeRead p ->
         let expand_prim_copy = false in
-        let cf_prepare = prepare_rplace config expand_prim_copy Read p in
-        let cf_continue cf _ = cf 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.SetDiscriminant (p, variant_id) ->
         set_discriminant config p variant_id cf ctx
@@ -914,7 +930,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
    * (and would thus floating in thin air...)!
    * *)
   (* Prepare the operand *)
-  let cf_prepare_op cf : m_fun = eval_operand_prepare config op cf in
+  let cf_eval_op cf : m_fun = eval_operand config op cf in
   (* Match on the targets *)
   let cf_match (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
    fun ctx ->
@@ -922,39 +938,29 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
     | A.If (st1, st2) -> (
         match op_v.value with
         | V.Concrete (V.Bool b) ->
-            (* Evaluate the operand *)
-            let cf_eval_op cf : m_fun = eval_operand config op cf in
             (* Evaluate the if and the branch body *)
-            let cf_branch cf op_v' : m_fun =
-              assert (op_v' = op_v);
+            let cf_branch cf : m_fun =
               (* Branch *)
               if b then eval_statement config st1 cf
               else eval_statement config st2 cf
             in
             (* Compose the continuations *)
-            comp cf_eval_op cf_branch cf ctx
+            cf_branch cf ctx
         | V.Symbolic sv ->
-            (* Expand the symbolic value *)
-            let allows_branching = true in
-            let cf_expand cf =
-              expand_symbolic_value config allows_branching sv
-                (S.mk_opt_place_from_op op ctx)
-                cf
-            in
-            (* Retry *)
-            let cf_eval_if cf = eval_switch config op tgts cf in
-            (* Compose *)
-            comp cf_expand cf_eval_if cf ctx
+            (* Expand the symbolic boolean, and continue by evaluating
+             * the branches *)
+            let cf_true : m_fun = eval_statement config st1 cf in
+            let cf_false : m_fun = eval_statement config st2 cf in
+            expand_symbolic_bool config sv
+              (S.mk_opt_place_from_op op ctx)
+              cf_true cf_false ctx
         | _ -> raise (Failure "Inconsistent state"))
     | A.SwitchInt (int_ty, stgts, otherwise) -> (
         match op_v.value with
         | V.Concrete (V.Scalar sv) ->
-            (* Evaluate the operand *)
-            let cf_eval_op cf = eval_operand config op cf in
             (* Evaluate the branch *)
-            let cf_eval_branch cf op_v' =
+            let cf_eval_branch cf =
               (* Sanity check *)
-              assert (op_v' = op_v);
               assert (sv.V.int_ty = int_ty);
               (* Find the branch *)
               match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with
@@ -962,13 +968,10 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
               | Some (_, tgt) -> eval_statement config tgt cf
             in
             (* Compose *)
-            comp cf_eval_op cf_eval_branch cf ctx
+            cf_eval_branch cf ctx
         | V.Symbolic sv ->
-            (* Expand the symbolic value - note that contrary to the boolean
-             * case, we can't expand then retry, because when switching over
-             * arbitrary integers we need to have an `otherwise` case, in
-             * which the scrutinee remains symbolic: if we expand the symbolic,
-             * reevaluate the switch, we loop... *)
+            (* Expand the symbolic value and continue by evaluating the
+             * proper branches *)
             let stgts =
               List.map
                 (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st cf))
@@ -993,7 +996,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
         | _ -> raise (Failure "Inconsistent state"))
   in
   (* Compose the continuations *)
-  comp cf_prepare_op cf_match cf ctx
+  comp cf_eval_op cf_match cf ctx
 
 (** Evaluate a function call (auxiliary helper for [eval_statement]) *)
 and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
@@ -1169,9 +1172,10 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     in
     (* Actually initialize and insert the abstractions *)
     let call_id = C.fresh_fun_call_id () in
+    let region_can_end _ = true in
     let ctx =
       create_push_abstractions_from_abs_region_groups call_id V.FunCall
-        inst_sg.A.regions_hierarchy compute_abs_avalues ctx
+        inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
     in
 
     (* Apply the continuation *)
diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml
index 84e8e00f..0e679fca 100644
--- a/src/LlbcAstUtils.ml
+++ b/src/LlbcAstUtils.ml
@@ -7,7 +7,6 @@ let statement_has_loops (st : statement) : bool =
   let obj =
     object
       inherit [_] iter_statement
-
       method! visit_Loop _ _ = raise Found
     end
   in
@@ -38,6 +37,8 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     We don't do that in an efficient manner, but it doesn't matter.
     
     TODO: rename to "list_ancestors_..."
+
+    This list *doesn't* include the current region.
  *)
 let rec list_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) :
     T.RegionGroupId.Set.t =
diff --git a/src/Print.ml b/src/Print.ml
index 722f76ce..337116ec 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -940,7 +940,7 @@ module LlbcAst = struct
         indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
     | A.AssignGlobal { dst; global } ->
         indent ^ fmt.var_id_to_string dst ^ " := global " ^ fmt.global_decl_id_to_string global
-    | A.FakeRead p -> "fake_read " ^ place_to_string fmt p
+    | A.FakeRead p -> indent ^ "fake_read " ^ place_to_string fmt p
     | A.SetDiscriminant (p, variant_id) ->
         (* TODO: improve this to lookup the variant name by using the def id *)
         indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", "
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 992b8cb8..8d3b5258 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -11,11 +11,8 @@ module RegularFunIdOrderedType = struct
   type t = regular_fun_id
 
   let compare = compare_regular_fun_id
-
   let to_string = show_regular_fun_id
-
   let pp_t = pp_regular_fun_id
-
   let show_t = show_regular_fun_id
 end
 
@@ -25,26 +22,14 @@ module FunIdOrderedType = struct
   type t = fun_id
 
   let compare = compare_fun_id
-
   let to_string = show_fun_id
-
   let pp_t = pp_fun_id
-
   let show_t = show_fun_id
 end
 
 module FunIdMap = Collections.MakeMap (FunIdOrderedType)
 module FunIdSet = Collections.MakeSet (FunIdOrderedType)
 
-(* TODO : move *)
-let binop_can_fail (binop : E.binop) : bool =
-  match binop with
-  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
-  | Div | Rem | Add | Sub | Mul -> true
-  | Shl | Shr -> raise Errors.Unimplemented
-
-(*let mk_arrow_ty (arg_ty : ty) (ret_ty : ty) : ty = Arrow (arg_ty, ret_ty)*)
-
 let dest_arrow_ty (ty : ty) : ty * ty =
   match ty with
   | Arrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
@@ -72,7 +57,6 @@ let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty =
   let obj =
     object
       inherit [_] map_ty
-
       method! visit_TypeVar _ var_id = tsubst var_id
     end
   in
@@ -198,7 +182,6 @@ let remove_meta (e : texpression) : texpression =
   let obj =
     object
       inherit [_] map_expression as super
-
       method! visit_Meta env _ e = super#visit_expression env e.e
     end
   in
@@ -414,7 +397,6 @@ let type_decl_is_enum (def : T.type_decl) : bool =
   match def.kind with T.Struct _ -> false | Enum _ -> true | Opaque -> false
 
 let mk_state_ty : ty = Adt (Assumed State, [])
-
 let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
 
 let mk_result_fail_texpression (ty : ty) : texpression =
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 84536005..a057b015 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1198,7 +1198,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
             assert (int_ty0 = int_ty1);
             let effect_info =
               {
-                can_fail = binop_can_fail binop;
+                can_fail = ExpressionsUtils.binop_can_fail binop;
                 input_state = false;
                 output_state = false;
               }
diff --git a/src/Values.ml b/src/Values.ml
index 4e45db03..4585b443 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -6,13 +6,9 @@ open Types
  * inside abstractions) *)
 
 module VarId = IdGen ()
-
 module BorrowId = IdGen ()
-
 module SymbolicValueId = IdGen ()
-
 module AbstractionId = IdGen ()
-
 module FunCallId = IdGen ()
 
 (** A variable *)
@@ -83,13 +79,9 @@ type symbolic_value = {
 class ['self] iter_typed_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
-
     method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
-
     method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
-
     method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> ()
-
     method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
   end
 
@@ -228,7 +220,6 @@ and typed_value = { value : value; ty : ety }
 class ['self] iter_typed_value =
   object (_self : 'self)
     inherit [_] iter_typed_value_visit_mvalue
-
     method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
   end
 
@@ -236,7 +227,6 @@ class ['self] iter_typed_value =
 class ['self] map_typed_value =
   object (_self : 'self)
     inherit [_] map_typed_value_visit_mvalue
-
     method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
   end
 
@@ -275,7 +265,6 @@ type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show]
 class ['self] iter_aproj_base =
   object (_self : 'self)
     inherit [_] iter_typed_value
-
     method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
 
     method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
@@ -286,7 +275,6 @@ class ['self] iter_aproj_base =
 class ['self] map_aproj_base =
   object (_self : 'self)
     inherit [_] map_typed_value
-
     method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
 
     method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
@@ -374,9 +362,7 @@ type region = RegionVarId.id Types.region [@@deriving show]
 class ['self] iter_typed_avalue_base =
   object (_self : 'self)
     inherit [_] iter_aproj
-
     method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> ()
-
     method visit_region : 'env -> region -> unit = fun _ _ -> ()
 
     method visit_abstract_shared_borrows
@@ -388,9 +374,7 @@ class ['self] iter_typed_avalue_base =
 class ['self] map_typed_avalue_base =
   object (_self : 'self)
     inherit [_] map_aproj
-
     method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id
-
     method visit_region : 'env -> region -> region = fun _ r -> r
 
     method visit_abstract_shared_borrows
@@ -798,6 +782,17 @@ type abs = {
           the symbolic AST, generated by the symbolic execution.
        *)
   kind : (abs_kind[@opaque]);
+  can_end : (bool[@opaque]);
+      (** Controls whether the region can be ended or not.
+          
+          This allows to "pin" some regions, and is useful when generating
+          backward functions.
+          
+          For instance, if we have: `fn f<'a, 'b>(...) -> (&'a mut T, &'b mut T)`,
+          when generating the backward function for 'a, we have to make sure we
+          don't need to end the return region for 'b (if it is the case, it means
+          the function doesn't borrow check).
+       *)
   parents : (AbstractionId.Set.t[@opaque]);  (** The parent abstractions *)
   original_parents : (AbstractionId.id list[@opaque]);
       (** The original list of parents, ordered. This is used for synthesis. *)