Update eval_operand_prepare to not give a value to the continuation

4 files changed, 181 insertions, 109 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/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 4549365d..bdcadf3a 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -48,13 +48,24 @@ let expand_primitively_copyable_at_place (config : C.config)
   (* Apply *)
   expand cf ctx
 
+(** Read a place (CPS-style function *)
+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
+  cf v ctx
+
 (** Small utility.
 
+    Prepare the access to a place in a right-value (typically an operand) by
+    reorganizing the environment.
+
     [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 ->
   let cc = update_ctx_along_read_place config access p in
   let cc = comp cc (end_loans_at_place config access p) in
@@ -63,13 +74,16 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool)
       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
+  let read_place = read_place config access p in
   comp cc read_place cf ctx
 
+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 rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
     (cv : E.operand_constant_value) : V.typed_value =
@@ -119,10 +133,10 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
   | _, ConstantAdt _ | _, ConstantValue _ ->
       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.
@@ -136,7 +150,7 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
     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").
@@ -144,51 +158,49 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
     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) ->
-        let v = operand_constant_value_to_typed_value ctx ty cv in
-        cf v ctx
+    | Expressions.Constant _ ->
+        (* No need to reorganize the context *)
+        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) ->
@@ -197,8 +209,7 @@ let eval_operand (config : C.config) (op : E.operand)
   | 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 ->
@@ -208,8 +219,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
@@ -219,11 +230,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
@@ -233,24 +244,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 =
@@ -469,7 +505,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 *)
@@ -507,7 +545,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 ->
@@ -539,7 +579,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 ->
@@ -580,7 +622,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/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 1083d643..e2775a1d 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.
 
@@ -823,8 +822,14 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
         comp cf_eval_rvalue cf_assign 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
@@ -905,7 +910,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 ->
@@ -913,39 +918,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
@@ -953,13 +948,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))
@@ -984,7 +976,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 =