Update the interpreter so that it is not written in CPS style (#120)

* Start turning the compiler in a style which is less CPS

* Update a function in InterpreterExpressions.ml

* WIP work on cps

* WIP

* WIP, currently on InterpreterStatements.ml

* WIP

* Finished CPS-related modification

* Fixed some warning related to documentation comments

* Finished loop support, fixed a loop

* fixed a typed value

* Fixed check_disappeared related error

* cleaned check_disappeared related error

* Start cleaning up

* Do more cleanup

* Make some cleanup and fix an issue

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Do more cleanup

* Rename a function

* Do more cleanup

* Cleanup the loops code and fix some bugs

* Cleanup assign_to_place

* Make a minor cleanup

---------

Co-authored-by: Son Ho <hosonmarc@gmail.com>

1 files changed, 305 insertions, 349 deletions

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 5a4fe7da..5b05dce8 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -26,33 +26,33 @@ let log = Logging.expressions_log
 *)
 let expand_primitively_copyable_at_place (config : config) (meta : Meta.meta)
     (access : access_kind) (p : place) : cm_fun =
- fun cf ctx ->
+ fun ctx ->
   (* Small helper *)
   let rec expand : cm_fun =
-   fun cf ctx ->
+   fun ctx ->
     let v = read_place meta access p ctx in
     match
       find_first_primitively_copyable_sv_with_borrows ctx.type_ctx.type_infos v
     with
-    | None -> cf ctx
+    | None -> (ctx, fun e -> e)
     | Some sv ->
-        let cc =
+        let ctx, cc =
           expand_symbolic_value_no_branching config meta sv
             (Some (mk_mplace meta p ctx))
+            ctx
         in
-        comp cc expand cf ctx
+        comp cc (expand ctx)
   in
   (* Apply *)
-  expand cf ctx
+  expand ctx
 
-(** Read a place (CPS-style function).
+(** Read a place.
 
-    We also check that the value *doesn't contain bottoms or reserved
+    We check that the value *doesn't contain bottoms or reserved
     borrows*.
  *)
-let read_place (meta : Meta.meta) (access : access_kind) (p : place)
-    (cf : typed_value -> m_fun) : m_fun =
- fun ctx ->
+let read_place_check (meta : Meta.meta) (access : access_kind) (p : place)
+    (ctx : eval_ctx) : typed_value =
   let v = read_place meta access p ctx in
   (* Check that there are no bottoms in the value *)
   cassert __FILE__ __LINE__
@@ -62,35 +62,36 @@ let read_place (meta : Meta.meta) (access : access_kind) (p : place)
   cassert __FILE__ __LINE__
     (not (reserved_in_value v))
     meta "There should be no reserved borrows in the value";
-  (* Call the continuation *)
-  cf v ctx
+  (* Return *)
+  v
 
 let access_rplace_reorganize_and_read (config : config) (meta : Meta.meta)
     (expand_prim_copy : bool) (access : access_kind) (p : place)
-    (cf : typed_value -> m_fun) : m_fun =
- fun ctx ->
+    (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
   (* Make sure we can evaluate the path *)
-  let cc = update_ctx_along_read_place config meta access p in
+  let ctx, cc = update_ctx_along_read_place config meta access p ctx in
   (* End the proper loans at the place itself *)
-  let cc = comp cc (end_loans_at_place config meta access p) in
+  let ctx, cc = comp cc (end_loans_at_place config meta access p ctx) 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 meta access p)
-    else cc
+  let ctx, cc =
+    comp cc
+      (if expand_prim_copy then
+         expand_primitively_copyable_at_place config meta access p ctx
+       else (ctx, fun e -> e))
   in
   (* Read the place - note that this checks that the value doesn't contain bottoms *)
-  let read_place = read_place meta access p in
+  let ty_value = read_place_check meta access p ctx in
   (* Compose *)
-  comp cc read_place cf ctx
+  (ty_value, ctx, cc)
 
 let access_rplace_reorganize (config : config) (meta : Meta.meta)
     (expand_prim_copy : bool) (access : access_kind) (p : place) : cm_fun =
- fun cf ctx ->
-  access_rplace_reorganize_and_read config meta expand_prim_copy access p
-    (fun _v -> cf)
-    ctx
+ fun ctx ->
+  let _, ctx, f =
+    access_rplace_reorganize_and_read config meta expand_prim_copy access p ctx
+  in
+  (ctx, f)
 
 (** Convert an operand constant operand value to a typed value *)
 let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal)
@@ -220,21 +221,22 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
       dest <- f(move x, move y);
       ...
     ]}
+
     Because of the way {!end_borrow} is implemented, when giving back the borrow
-    [l0] upon evaluating [move y], we won't notice that [shared_borrow l0] has
-    disappeared from the environment (it has been moved and not assigned yet,
-    and so is hanging in "thin air").
+    [l0] upon evaluating [move y], if we have already moved the value of x,
+    we won't notice that [shared_borrow l0] has disappeared from the environment
+    (it has been moved and not assigned yet, and so is hanging in "thin air").
     
     By first "preparing" the operands evaluation, we make sure no such thing
     happens. To be more precise, we make sure all the updates to borrows triggered
     by access *and* move operations have already been applied.
 
-    Rk.: in the formalization, we always have an explicit "reorganization" step
+    Rem.: in the formalization, we always have an explicit "reorganization" step
     in the rule premises, before the actual operand evaluation, that allows to
     reorganize the environment so that it satisfies the proper conditions. This
     function's role is to do the reorganization.
     
-    Rk.: doing this is actually not completely necessary because when
+    Rem.: doing this is actually not completely necessary because when
     generating MIR, rustc introduces intermediate assignments for all the function
     parameters. Still, it is better for soundness purposes, and corresponds to
     what we do in the formalization (because we don't enforce the same constraints
@@ -242,32 +244,27 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
  *)
 let prepare_eval_operand_reorganize (config : config) (meta : Meta.meta)
     (op : operand) : cm_fun =
- fun cf ctx ->
-  let prepare : cm_fun =
-   fun cf ctx ->
-    match op with
-    | Constant _ ->
-        (* No need to reorganize the context *)
-        cf ctx
-    | Copy p ->
-        (* Access the value *)
-        let access = Read in
-        (* Expand the symbolic values, if necessary *)
-        let expand_prim_copy = true in
-        access_rplace_reorganize config meta expand_prim_copy access p cf ctx
-    | Move p ->
-        (* Access the value *)
-        let access = Move in
-        let expand_prim_copy = false in
-        access_rplace_reorganize config meta expand_prim_copy access p cf ctx
-  in
-  (* Apply *)
-  prepare cf ctx
+ fun ctx ->
+  match op with
+  | Constant _ ->
+      (* No need to reorganize the context *)
+      (ctx, fun e -> e)
+  | Copy p ->
+      (* Access the value *)
+      let access = Read in
+      (* Expand the symbolic values, if necessary *)
+      let expand_prim_copy = true in
+      access_rplace_reorganize config meta expand_prim_copy access p ctx
+  | Move p ->
+      (* Access the value *)
+      let access = Move in
+      let expand_prim_copy = false in
+      access_rplace_reorganize config meta expand_prim_copy access p ctx
 
 (** Evaluate an operand, without reorganizing the context before *)
 let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
-    (op : operand) (cf : typed_value -> m_fun) : m_fun =
- fun ctx ->
+    (op : operand) (ctx : eval_ctx) :
+    typed_value * eval_ctx * (eval_result -> eval_result) =
   (* Debug *)
   log#ldebug
     (lazy
@@ -280,26 +277,29 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
   | Constant cv -> (
       match cv.value with
       | CLiteral lit ->
-          cf (literal_to_typed_value meta (ty_as_literal cv.ty) lit) ctx
-      | CTraitConst (trait_ref, const_name) -> (
+          ( literal_to_typed_value meta (ty_as_literal cv.ty) lit,
+            ctx,
+            fun e -> e )
+      | CTraitConst (trait_ref, const_name) ->
           let ctx0 = ctx in
           (* Simply introduce a fresh symbolic value *)
           let ty = cv.ty in
           let v = mk_fresh_symbolic_typed_value meta ty in
-          (* Continue the evaluation *)
-          let e = cf v ctx in
           (* Wrap the generated expression *)
-          match e with
-          | None -> None
-          | Some e ->
-              Some
-                (SymbolicAst.IntroSymbolic
-                   ( ctx0,
-                     None,
-                     value_as_symbolic meta v.value,
-                     SymbolicAst.VaTraitConstValue (trait_ref, const_name),
-                     e )))
-      | CVar vid -> (
+          let cf e =
+            match e with
+            | None -> None
+            | Some e ->
+                Some
+                  (SymbolicAst.IntroSymbolic
+                     ( ctx0,
+                       None,
+                       value_as_symbolic meta v.value,
+                       SymbolicAst.VaTraitConstValue (trait_ref, const_name),
+                       e ))
+          in
+          (v, ctx, cf)
+      | CVar vid ->
           let ctx0 = ctx in
           (* In concrete mode: lookup the const generic value.
              In symbolic mode: introduce a fresh symbolic value.
@@ -319,74 +319,59 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
                 let v = mk_fresh_symbolic_typed_value meta cv.ty in
                 (ctx, v)
           in
-          (* Continue *)
-          let e = cf cv ctx in
-          (* If we are synthesizing a symbolic AST, it means that we are in symbolic
-             mode: the value of the const generic is necessarily symbolic. *)
-          sanity_check __FILE__ __LINE__ (e = None || is_symbolic cv.value) meta;
           (* We have to wrap the generated expression *)
-          match e with
-          | None -> None
-          | Some e ->
-              (* If we are synthesizing a symbolic AST, it means that we are in symbolic
-                 mode: the value of the const generic is necessarily symbolic. *)
-              sanity_check __FILE__ __LINE__ (is_symbolic cv.value) meta;
-              (* *)
-              Some
-                (SymbolicAst.IntroSymbolic
-                   ( ctx0,
-                     None,
-                     value_as_symbolic meta cv.value,
-                     SymbolicAst.VaCgValue vid,
-                     e )))
+          let cf e =
+            match e with
+            | None -> None
+            | Some e ->
+                (* If we are synthesizing a symbolic AST, it means that we are in symbolic
+                   mode: the value of the const generic is necessarily symbolic. *)
+                sanity_check __FILE__ __LINE__ (is_symbolic cv.value) meta;
+                (* *)
+                Some
+                  (SymbolicAst.IntroSymbolic
+                     ( ctx0,
+                       None,
+                       value_as_symbolic meta cv.value,
+                       SymbolicAst.VaCgValue vid,
+                       e ))
+          in
+          (cv, ctx, cf)
       | CFnPtr _ ->
           craise __FILE__ __LINE__ meta
             "Function pointers are not supported yet")
   | Copy p ->
       (* Access the value *)
       let access = Read in
-      let cc = read_place meta access p in
+      let v = read_place_check meta access p ctx in
+      (* Sanity checks *)
+      exec_assert __FILE__ __LINE__
+        (not (bottom_in_value ctx.ended_regions v))
+        meta "Can not copy a value containing bottom";
+      sanity_check __FILE__ __LINE__
+        (Option.is_none
+           (find_first_primitively_copyable_sv_with_borrows
+              ctx.type_ctx.type_infos v))
+        meta;
       (* Copy the value *)
-      let copy cf v : m_fun =
-       fun ctx ->
-        (* Sanity checks *)
-        exec_assert __FILE__ __LINE__
-          (not (bottom_in_value ctx.ended_regions v))
-          meta "Can not copy a value containing bottom";
-        sanity_check __FILE__ __LINE__
-          (Option.is_none
-             (find_first_primitively_copyable_sv_with_borrows
-                ctx.type_ctx.type_infos v))
-          meta;
-        (* Actually perform the copy *)
-        let allow_adt_copy = false in
-        let ctx, v = copy_value meta allow_adt_copy config ctx v in
-        (* Continue *)
-        cf v ctx
-      in
-      (* Compose and apply *)
-      comp cc copy cf ctx
+      let allow_adt_copy = false in
+      let ctx, v = copy_value meta allow_adt_copy config ctx v in
+      (v, ctx, fun e -> e)
   | Move p ->
       (* Access the value *)
       let access = Move in
-      let cc = read_place meta access p in
+      let v = read_place_check meta access p ctx in
+      (* Check that there are no bottoms in the value we are about to move *)
+      exec_assert __FILE__ __LINE__
+        (not (bottom_in_value ctx.ended_regions v))
+        meta "There should be no bottoms in the value we are about to move";
       (* 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 *)
-        exec_assert __FILE__ __LINE__
-          (not (bottom_in_value ctx.ended_regions v))
-          meta "There should be no bottoms in the value we are about to move";
-        let bottom : typed_value = { value = VBottom; ty = v.ty } in
-        let ctx = write_place meta access p bottom ctx in
-        cf v ctx
-      in
-      (* Compose and apply *)
-      comp cc move cf ctx
+      let bottom : typed_value = { value = VBottom; ty = v.ty } in
+      let ctx = write_place meta access p bottom ctx in
+      (v, ctx, fun e -> e)
 
 let eval_operand (config : config) (meta : Meta.meta) (op : operand)
-    (cf : typed_value -> m_fun) : m_fun =
- fun ctx ->
+    (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
   (* Debug *)
   log#ldebug
     (lazy
@@ -394,10 +379,8 @@ let eval_operand (config : config) (meta : Meta.meta) (op : operand)
       ^ eval_ctx_to_string ~meta:(Some meta) ctx
       ^ "\n"));
   (* We reorganize the context, then evaluate the operand *)
-  comp
-    (prepare_eval_operand_reorganize config meta op)
-    (eval_operand_no_reorganize config meta op)
-    cf ctx
+  let ctx, cc = prepare_eval_operand_reorganize config meta op ctx in
+  comp2 cc (eval_operand_no_reorganize config meta op ctx)
 
 (** Small utility.
 
@@ -409,63 +392,59 @@ let prepare_eval_operands_reorganize (config : config) (meta : Meta.meta)
 
 (** Evaluate several operands. *)
 let eval_operands (config : config) (meta : Meta.meta) (ops : operand list)
-    (cf : typed_value list -> m_fun) : m_fun =
- fun ctx ->
+    (ctx : eval_ctx) :
+    typed_value list * eval_ctx * (eval_result -> eval_result) =
   (* Prepare the operands *)
-  let prepare = prepare_eval_operands_reorganize config meta ops in
+  let ctx, cc = prepare_eval_operands_reorganize config meta ops ctx in
   (* Evaluate the operands *)
-  let eval =
-    fold_left_list_apply_continuation
-      (eval_operand_no_reorganize config meta)
-      ops
-  in
-  (* Compose and apply *)
-  comp prepare eval cf ctx
+  comp2 cc
+    (map_apply_continuation (eval_operand_no_reorganize config meta) ops ctx)
 
 let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand)
-    (op2 : operand) (cf : typed_value * typed_value -> m_fun) : m_fun =
-  let eval_op = eval_operands config meta [ op1; op2 ] in
-  let use_res cf res =
+    (op2 : operand) (ctx : eval_ctx) :
+    (typed_value * typed_value) * eval_ctx * (eval_result -> eval_result) =
+  let res, ctx, cc = eval_operands config meta [ op1; op2 ] ctx in
+  let res =
     match res with
-    | [ v1; v2 ] -> cf (v1, v2)
+    | [ v1; v2 ] -> (v1, v2)
     | _ -> craise __FILE__ __LINE__ meta "Unreachable"
   in
-  comp eval_op use_res cf
+  (res, ctx, cc)
 
 let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop)
-    (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+    (op : operand) (ctx : eval_ctx) :
+    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
   (* Evaluate the operand *)
-  let eval_op = eval_operand config meta op in
+  let v, ctx, cc = eval_operand config meta op ctx in
   (* Apply the unop *)
-  let apply cf (v : typed_value) : m_fun =
+  let r =
     match (unop, v.value) with
-    | Not, VLiteral (VBool b) ->
-        cf (Ok { v with value = VLiteral (VBool (not b)) })
+    | Not, VLiteral (VBool b) -> Ok { v with value = VLiteral (VBool (not b)) }
     | Neg, VLiteral (VScalar sv) -> (
         let i = Z.neg sv.value in
         match mk_scalar sv.int_ty i with
-        | Error _ -> cf (Error EPanic)
-        | Ok sv -> cf (Ok { v with value = VLiteral (VScalar sv) }))
+        | Error _ -> Error EPanic
+        | Ok sv -> Ok { v with value = VLiteral (VScalar sv) })
     | ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)),
         VLiteral (VScalar sv) ) -> (
         (* Cast between integers *)
         sanity_check __FILE__ __LINE__ (src_ty = sv.int_ty) meta;
         let i = sv.value in
         match mk_scalar tgt_ty i with
-        | Error _ -> cf (Error EPanic)
+        | Error _ -> Error EPanic
         | Ok sv ->
             let ty = TLiteral (TInteger tgt_ty) in
             let value = VLiteral (VScalar sv) in
-            cf (Ok { ty; value }))
+            Ok { ty; value })
     | Cast (CastScalar (TBool, TInteger tgt_ty)), VLiteral (VBool sv) -> (
         (* Cast bool -> int *)
         let i = Z.of_int (if sv then 1 else 0) in
         match mk_scalar tgt_ty i with
-        | Error _ -> cf (Error EPanic)
+        | Error _ -> Error EPanic
         | Ok sv ->
             let ty = TLiteral (TInteger tgt_ty) in
             let value = VLiteral (VScalar sv) in
-            cf (Ok { ty; value }))
+            Ok { ty; value })
     | Cast (CastScalar (TInteger _, TBool)), VLiteral (VScalar sv) ->
         (* Cast int -> bool *)
         let b =
@@ -477,43 +456,43 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop)
         in
         let value = VLiteral (VBool b) in
         let ty = TLiteral TBool in
-        cf (Ok { ty; value })
+        Ok { ty; value }
     | _ -> exec_raise __FILE__ __LINE__ meta "Invalid input for unop"
   in
-  comp eval_op apply cf
+  (r, ctx, cc)
 
 let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop)
-    (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
- fun ctx ->
+    (op : operand) (ctx : eval_ctx) :
+    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
   (* Evaluate the operand *)
-  let eval_op = eval_operand config meta op in
+  let v, ctx, cc = eval_operand config meta op ctx in
   (* Generate a fresh symbolic value to store the result *)
-  let apply cf (v : typed_value) : m_fun =
-   fun ctx ->
-    let res_sv_id = fresh_symbolic_value_id () in
-    let res_sv_ty =
-      match (unop, v.ty) with
-      | Not, (TLiteral TBool as lty) -> lty
-      | Neg, (TLiteral (TInteger _) as lty) -> lty
-      | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty
-      | _ -> exec_raise __FILE__ __LINE__ meta "Invalid input for unop"
-    in
-    let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
-    (* Call the continuation *)
-    let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
-    (* Synthesize the symbolic AST *)
-    synthesize_unary_op ctx unop v
-      (mk_opt_place_from_op meta op ctx)
-      res_sv None expr
+  let res_sv_id = fresh_symbolic_value_id () in
+  let res_sv_ty =
+    match (unop, v.ty) with
+    | Not, (TLiteral TBool as lty) -> lty
+    | Neg, (TLiteral (TInteger _) as lty) -> lty
+    | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty
+    | _ -> exec_raise __FILE__ __LINE__ meta "Invalid input for unop"
   in
-  (* Compose and apply *)
-  comp eval_op apply cf ctx
+  let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
+  (* Compute the result *)
+  let res = Ok (mk_typed_value_from_symbolic_value res_sv) in
+  (* Synthesize the symbolic AST *)
+  let cc =
+    cc_comp cc
+      (synthesize_unary_op ctx unop v
+         (mk_opt_place_from_op meta op ctx)
+         res_sv None)
+  in
+  (res, ctx, cc)
 
 let eval_unary_op (config : config) (meta : Meta.meta) (unop : unop)
-    (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+    (op : operand) (ctx : eval_ctx) :
+    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
   match config.mode with
-  | ConcreteMode -> eval_unary_op_concrete config meta unop op cf
-  | SymbolicMode -> eval_unary_op_symbolic config meta unop op cf
+  | ConcreteMode -> eval_unary_op_concrete config meta unop op ctx
+  | SymbolicMode -> eval_unary_op_symbolic config meta unop op ctx
 
 (** Small helper for [eval_binary_op_concrete]: computes the result of applying
     the binop *after* the operands have been successfully evaluated
@@ -593,86 +572,81 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
     | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop"
 
 let eval_binary_op_concrete (config : config) (meta : Meta.meta) (binop : binop)
-    (op1 : operand) (op2 : operand)
-    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+    (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
+    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands config meta op1 op2 in
+  let (v1, v2), ctx, cc = eval_two_operands config meta op1 op2 ctx in
   (* Compute the result of the binop *)
-  let compute cf (res : typed_value * typed_value) =
-    let v1, v2 = res in
-    cf (eval_binary_op_concrete_compute meta binop v1 v2)
-  in
-  (* Compose and apply *)
-  comp eval_ops compute cf
+  let r = eval_binary_op_concrete_compute meta binop v1 v2 in
+  (* Return *)
+  (r, ctx, cc)
 
 let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
-    (op1 : operand) (op2 : operand)
-    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
- fun ctx ->
+    (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
+    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
   (* Evaluate the operands *)
-  let eval_ops = eval_two_operands config meta op1 op2 in
-  (* Compute the result of applying the binop *)
-  let compute cf ((v1, v2) : typed_value * typed_value) : m_fun =
-   fun ctx ->
-    (* Generate a fresh symbolic value to store the result *)
-    let res_sv_id = fresh_symbolic_value_id () in
-    let res_sv_ty =
-      if binop = Eq || binop = Ne then (
-        (* Equality operations *)
-        sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
-        (* Equality/inequality check is primitive only for a subset of types *)
-        exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta
-          "The type is not primitively copyable";
-        TLiteral TBool)
-      else
-        (* Other operations: input types are integers *)
-        match (v1.ty, v2.ty) with
-        | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> (
-            match binop with
-            | Lt | Le | Ge | Gt ->
-                sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta;
-                TLiteral TBool
-            | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
-                sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta;
-                TLiteral (TInteger int_ty1)
-            (* These return `(int, bool)` which isn't a literal type *)
-            | CheckedAdd | CheckedSub | CheckedMul ->
-                craise __FILE__ __LINE__ meta
-                  "Checked operations are not implemented"
-            | Shl | Shr ->
-                (* The number of bits can be of a different integer type
-                   than the operand *)
-                TLiteral (TInteger int_ty1)
-            | Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable")
-        | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop"
-    in
-    let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
-    (* Call the continuattion *)
-    let v = mk_typed_value_from_symbolic_value res_sv in
-    let expr = cf (Ok v) ctx in
-    (* Synthesize the symbolic AST *)
-    let p1 = mk_opt_place_from_op meta op1 ctx in
-    let p2 = mk_opt_place_from_op meta op2 ctx in
-    synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr
+  let (v1, v2), ctx, cc = eval_two_operands config meta op1 op2 ctx in
+  (* Generate a fresh symbolic value to store the result *)
+  let res_sv_id = fresh_symbolic_value_id () in
+  let res_sv_ty =
+    if binop = Eq || binop = Ne then (
+      (* Equality operations *)
+      sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
+      (* Equality/inequality check is primitive only for a subset of types *)
+      exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta
+        "The type is not primitively copyable";
+      TLiteral TBool)
+    else
+      (* Other operations: input types are integers *)
+      match (v1.ty, v2.ty) with
+      | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> (
+          match binop with
+          | Lt | Le | Ge | Gt ->
+              sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta;
+              TLiteral TBool
+          | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
+              sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta;
+              TLiteral (TInteger int_ty1)
+          (* These return `(int, bool)` which isn't a literal type *)
+          | CheckedAdd | CheckedSub | CheckedMul ->
+              craise __FILE__ __LINE__ meta
+                "Checked operations are not implemented"
+          | Shl | Shr ->
+              (* The number of bits can be of a different integer type
+                 than the operand *)
+              TLiteral (TInteger int_ty1)
+          | Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable")
+      | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop"
+  in
+  let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
+  let v = mk_typed_value_from_symbolic_value res_sv in
+  (* Synthesize the symbolic AST *)
+  let p1 = mk_opt_place_from_op meta op1 ctx in
+  let p2 = mk_opt_place_from_op meta op2 ctx in
+  let cc =
+    cc_comp cc (synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None)
   in
   (* Compose and apply *)
-  comp eval_ops compute cf ctx
+  (Ok v, ctx, cc)
 
 let eval_binary_op (config : config) (meta : Meta.meta) (binop : binop)
-    (op1 : operand) (op2 : operand)
-    (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
+    (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
+    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
   match config.mode with
-  | ConcreteMode -> eval_binary_op_concrete config meta binop op1 op2 cf
-  | SymbolicMode -> eval_binary_op_symbolic config meta binop op1 op2 cf
+  | ConcreteMode -> eval_binary_op_concrete config meta binop op1 op2 ctx
+  | SymbolicMode -> eval_binary_op_symbolic config meta binop op1 op2 ctx
 
+(** Evaluate an rvalue which creates a reference (i.e., an rvalue which is
+    `&p` or `&mut p` or `&two-phase p`) *)
 let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place)
-    (bkind : borrow_kind) (cf : typed_value -> m_fun) : m_fun =
- fun ctx ->
+    (bkind : borrow_kind) (ctx : eval_ctx) :
+    typed_value * eval_ctx * (eval_result -> eval_result) =
   match bkind with
   | BShared | BTwoPhaseMut | BShallow ->
       (* **REMARK**: we initially treated shallow borrows like shared borrows.
          In practice this restricted the behaviour too much, so for now we
-         forbid them.
+         forbid them and remove them in the prepasses (see the comments there
+         as to why this is sound).
       *)
       sanity_check __FILE__ __LINE__ (bkind <> BShallow) meta;
 
@@ -685,86 +659,75 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place)
       in
 
       let expand_prim_copy = false in
-      let prepare =
+      let v, ctx, cc =
         access_rplace_reorganize_and_read config meta expand_prim_copy access p
+          ctx
       in
-      (* Evaluate the borrowing operation *)
-      let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
-       fun ctx ->
-        (* Generate the fresh borrow id *)
-        let bid = fresh_borrow_id () in
-        (* Compute the loan value, with which to replace the value at place p *)
-        let nv =
-          match v.value with
-          | VLoan (VSharedLoan (bids, sv)) ->
-              (* Shared loan: insert the new borrow id *)
-              let bids1 = BorrowId.Set.add bid bids in
-              { v with value = VLoan (VSharedLoan (bids1, sv)) }
-          | _ ->
-              (* Not a shared loan: add a wrapper *)
-              let v' = VLoan (VSharedLoan (BorrowId.Set.singleton bid, v)) in
-              { v with value = v' }
-        in
-        (* Update the borrowed value in the context *)
-        let ctx = write_place meta access p nv ctx in
-        (* Compute the rvalue - simply a shared borrow with a the fresh id.
-         * Note that the reference is *mutable* if we do a two-phase borrow *)
-        let ref_kind =
-          match bkind with
-          | BShared | BShallow -> RShared
-          | BTwoPhaseMut -> RMut
-          | _ -> craise __FILE__ __LINE__ meta "Unreachable"
-        in
-        let rv_ty = TRef (RErased, v.ty, ref_kind) in
-        let bc =
-          match bkind with
-          | BShared | BShallow ->
-              (* See the remark at the beginning of the match branch: we
-                 handle shallow borrows like shared borrows *)
-              VSharedBorrow bid
-          | BTwoPhaseMut -> VReservedMutBorrow bid
-          | _ -> craise __FILE__ __LINE__ meta "Unreachable"
-        in
-        let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in
-        (* Continue *)
-        cf rv ctx
+      (* Generate the fresh borrow id *)
+      let bid = fresh_borrow_id () in
+      (* Compute the loan value, with which to replace the value at place p *)
+      let nv =
+        match v.value with
+        | VLoan (VSharedLoan (bids, sv)) ->
+            (* Shared loan: insert the new borrow id *)
+            let bids1 = BorrowId.Set.add bid bids in
+            { v with value = VLoan (VSharedLoan (bids1, sv)) }
+        | _ ->
+            (* Not a shared loan: add a wrapper *)
+            let v' = VLoan (VSharedLoan (BorrowId.Set.singleton bid, v)) in
+            { v with value = v' }
       in
-      (* Compose and apply *)
-      comp prepare eval cf ctx
+      (* Update the value in the context to replace it with the loan *)
+      let ctx = write_place meta access p nv ctx in
+      (* Compute the rvalue - simply a shared borrow with the fresh id.
+       * Note that the reference is *mutable* if we do a two-phase borrow *)
+      let ref_kind =
+        match bkind with
+        | BShared | BShallow -> RShared
+        | BTwoPhaseMut -> RMut
+        | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+      in
+      let rv_ty = TRef (RErased, v.ty, ref_kind) in
+      let bc =
+        match bkind with
+        | BShared | BShallow ->
+            (* See the remark at the beginning of the match branch: we
+               handle shallow borrows like shared borrows *)
+            VSharedBorrow bid
+        | BTwoPhaseMut -> VReservedMutBorrow bid
+        | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+      in
+      let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in
+      (* Return *)
+      (rv, ctx, cc)
   | BMut ->
       (* Access the value *)
       let access = Write in
       let expand_prim_copy = false in
-      let prepare =
+      let v, ctx, cc =
         access_rplace_reorganize_and_read config meta expand_prim_copy access p
+          ctx
       in
-      (* Evaluate the borrowing operation *)
-      let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
-       fun ctx ->
-        (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
-        let bid = fresh_borrow_id () in
-        let rv_ty = TRef (RErased, v.ty, RMut) in
-        let rv : typed_value =
-          { value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty }
-        in
-        (* Compute the value with which to replace the value at place p *)
-        let nv = { v with value = VLoan (VMutLoan bid) } in
-        (* Update the value in the context *)
-        let ctx = write_place meta access p nv ctx in
-        (* Continue *)
-        cf rv ctx
+      (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
+      let bid = fresh_borrow_id () in
+      let rv_ty = TRef (RErased, v.ty, RMut) in
+      let rv : typed_value =
+        { value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty }
       in
-      (* Compose and apply *)
-      comp prepare eval cf ctx
+      (* Compute the loan value with which to replace the value at place p *)
+      let nv = { v with value = VLoan (VMutLoan bid) } in
+      (* Update the value in the context to replace it with the loan *)
+      let ctx = write_place meta access p nv ctx in
+      (* Return *)
+      (rv, ctx, cc)
 
 let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
-    (aggregate_kind : aggregate_kind) (ops : operand list)
-    (cf : typed_value -> m_fun) : m_fun =
+    (aggregate_kind : aggregate_kind) (ops : operand list) (ctx : eval_ctx) :
+    typed_value * eval_ctx * (eval_result -> eval_result) =
   (* Evaluate the operands *)
-  let eval_ops = eval_operands config meta ops in
+  let values, ctx, cc = eval_operands config meta ops ctx in
   (* Compute the value *)
-  let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun =
-   fun ctx ->
+  let v, cf_compute =
     (* Match on the aggregate kind *)
     match aggregate_kind with
     | AggregatedAdt (type_id, opt_variant_id, generics) -> (
@@ -775,8 +738,7 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
             let generics = mk_generic_args [] tys [] [] in
             let ty = TAdt (TTuple, generics) in
             let aggregated : typed_value = { value = v; ty } in
-            (* Call the continuation *)
-            cf aggregated ctx
+            (aggregated, fun e -> e)
         | TAdtId def_id ->
             (* Sanity checks *)
             let type_decl = ctx_lookup_type_decl ctx def_id in
@@ -799,9 +761,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
             let aty = TAdt (TAdtId def_id, generics) in
             let aggregated : typed_value = { value = VAdt av; ty = aty } in
             (* Call the continuation *)
-            cf aggregated ctx
+            (aggregated, fun e -> e)
         | TAssumed _ -> craise __FILE__ __LINE__ meta "Unreachable")
-    | AggregatedArray (ety, cg) -> (
+    | AggregatedArray (ety, cg) ->
         (* Sanity check: all the values have the proper type *)
         sanity_check __FILE__ __LINE__
           (List.for_all (fun (v : typed_value) -> v.ty = ety) values)
@@ -819,38 +781,36 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta)
            code: by introducing a symbolic value we introduce a let-binding
            in the generated code. *)
         let saggregated = mk_fresh_symbolic_typed_value meta ty in
-        (* Call the continuation *)
-        match cf saggregated ctx with
-        | None -> None
-        | Some e ->
-            (* Introduce the symbolic value in the AST *)
-            let sv = ValuesUtils.value_as_symbolic meta saggregated.value in
-            Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)))
+        (* Update the symbolic ast *)
+        let cf e =
+          match e with
+          | None -> None
+          | Some e ->
+              (* Introduce the symbolic value in the AST *)
+              let sv = ValuesUtils.value_as_symbolic meta saggregated.value in
+              Some
+                (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))
+        in
+        (saggregated, cf)
     | AggregatedClosure _ ->
         craise __FILE__ __LINE__ meta "Closures are not supported yet"
   in
-  (* Compose and apply *)
-  comp eval_ops compute cf
+  (v, ctx, cc_comp cc cf_compute)
 
 let eval_rvalue_not_global (config : config) (meta : Meta.meta)
-    (rvalue : rvalue) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
- fun ctx ->
+    (rvalue : rvalue) (ctx : eval_ctx) :
+    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
   log#ldebug (lazy "eval_rvalue");
-  (* Small helpers *)
-  let wrap_in_result (cf : (typed_value, eval_error) result -> m_fun)
-      (v : typed_value) : m_fun =
-    cf (Ok v)
-  in
-  let comp_wrap f = comp f wrap_in_result cf in
+  (* Small helper *)
+  let wrap_in_result (v, ctx, cc) = (Ok v, ctx, cc) in
   (* Delegate to the proper auxiliary function *)
   match rvalue with
-  | Use op -> comp_wrap (eval_operand config meta op) ctx
-  | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config meta p bkind) ctx
-  | UnaryOp (unop, op) -> eval_unary_op config meta unop op cf ctx
-  | BinaryOp (binop, op1, op2) ->
-      eval_binary_op config meta binop op1 op2 cf ctx
+  | Use op -> wrap_in_result (eval_operand config meta op ctx)
+  | RvRef (p, bkind) -> wrap_in_result (eval_rvalue_ref config meta p bkind ctx)
+  | UnaryOp (unop, op) -> eval_unary_op config meta unop op ctx
+  | BinaryOp (binop, op1, op2) -> eval_binary_op config meta binop op1 op2 ctx
   | Aggregate (aggregate_kind, ops) ->
-      comp_wrap (eval_rvalue_aggregate config meta aggregate_kind ops) ctx
+      wrap_in_result (eval_rvalue_aggregate config meta aggregate_kind ops ctx)
   | Discriminant _ ->
       craise __FILE__ __LINE__ meta
         "Unreachable: discriminant reads should have been eliminated from the \
@@ -858,16 +818,12 @@ let eval_rvalue_not_global (config : config) (meta : Meta.meta)
   | Global _ -> craise __FILE__ __LINE__ meta "Unreachable"
 
 let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
- fun cf ctx ->
+ fun ctx ->
   let expand_prim_copy = false in
-  let cf_prepare cf =
-    access_rplace_reorganize_and_read config meta expand_prim_copy Read p cf
+  let v, ctx, cc =
+    access_rplace_reorganize_and_read config meta expand_prim_copy Read p ctx
   in
-  let cf_continue cf v : m_fun =
-   fun ctx ->
-    cassert __FILE__ __LINE__
-      (not (bottom_in_value ctx.ended_regions v))
-      meta "Fake read: the value contains bottom";
-    cf ctx
-  in
-  comp cf_prepare cf_continue cf ctx
+  cassert __FILE__ __LINE__
+    (not (bottom_in_value ctx.ended_regions v))
+    meta "Fake read: the value contains bottom";
+  (ctx, cc)