Make progress on converting InterpreterExpressions to CPS

2 files changed, 165 insertions, 102 deletions

diff --git a/src/Cps.ml b/src/Cps.ml
index 10bf1c6d..ef8fc8ee 100644
--- a/src/Cps.ml
+++ b/src/Cps.ml
@@ -5,6 +5,9 @@ module T = Types
 module V = Values
 module C = Contexts
 
+(** TODO: change the name *)
+type eval_error = EPanic
+
 (** Result of evaluating a statement *)
 type statement_eval_res =
   | Unit
@@ -64,3 +67,25 @@ let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun)
 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
+    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).
+ *)
+let fold_left_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 =
+   fun ctx ->
+    match inputs with
+    | [] -> cf (List.rev outputs) ctx
+    | x :: inputs ->
+        comp (f x) (fun cf v -> eval_list inputs cf (v :: outputs)) cf ctx
+  in
+  eval_list inputs cf []
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index b5ada10f..4f4cf4e5 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -10,6 +10,7 @@ open TypesUtils
 open ValuesUtils
 module Inv = Invariants
 module S = Synthesis
+open Cps
 open InterpreterUtils
 open InterpreterExpansion
 open InterpreterPaths
@@ -17,10 +18,7 @@ open InterpreterPaths
 (** The local logger *)
 let log = L.expressions_log
 
-(** TODO: change the name *)
-type eval_error = Panic
-
-type 'a eval_result = ('a, eval_error) result
+(*type 'a eval_result = ('a, eval_error) result*)
 
 (** As long as there are symbolic values at a given place (potentially in subvalues)
     which contain borrows and are primitively copyable, expand them.
@@ -31,21 +29,23 @@ type 'a eval_result = ('a, eval_error) result
     loans.
 *)
 let expand_primitively_copyable_at_place (config : C.config)
-    (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
+    (access : access_kind) (p : E.place) : cm_fun =
+ fun cf ctx ->
   (* Small helper *)
-  let rec expand ctx =
+  let rec expand : cm_fun =
+   fun cf ctx ->
     let v = read_place_unwrap config access p ctx in
     match
       find_first_primitively_copyable_sv_with_borrows
         ctx.type_context.type_infos v
     with
-    | None -> ctx
+    | None -> cf ctx
     | Some sv ->
-        let ctx = expand_symbolic_value_no_branching config sv ctx in
-        expand ctx
+        let cc = expand_symbolic_value_no_branching config sv in
+        comp cc expand cf ctx
   in
   (* Apply *)
-  expand ctx
+  expand cf ctx
 
 (** Small utility.
 
@@ -53,17 +53,21 @@ let expand_primitively_copyable_at_place (config : C.config)
     copyable and contain borrows.
  *)
 let prepare_rplace (config : C.config) (expand_prim_copy : bool)
-    (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
-    C.eval_ctx * V.typed_value =
-  let ctx = update_ctx_along_read_place config access p ctx in
-  let ctx = end_loans_at_place config access p ctx in
-  let ctx =
+    (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
+  let cc =
     if expand_prim_copy then
-      expand_primitively_copyable_at_place config access p ctx
-    else ctx
+      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 v = read_place_unwrap config access p ctx in
-  (ctx, v)
+  comp cc read_place cf ctx
 
 (** Convert a constant operand value to a typed value *)
 let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
@@ -139,31 +143,40 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
     parameters. Still, it is better for soundness purposes, and corresponds to
     what we do in the formal semantics.
  *)
-let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand)
-    : C.eval_ctx * V.typed_value =
-  let ctx, v =
+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 ->
     match op with
     | Expressions.Constant (ty, cv) ->
         let v = constant_value_to_typed_value ctx ty cv in
-        (ctx, v)
+        cf v 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 ctx
+        prepare_rplace 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 ctx
+        prepare_rplace config expand_prim_copy access p cf ctx
   in
-  assert (not (bottom_in_value ctx.ended_regions v));
-  (ctx, v)
+  (* 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
 
 (** Evaluate an operand. *)
-let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
-    C.eval_ctx * V.typed_value =
+let eval_operand (config : C.config) (op : E.operand)
+    (cf : V.typed_value -> m_fun) : m_fun =
+ fun ctx ->
   (* Debug *)
   log#ldebug
     (lazy
@@ -173,98 +186,124 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
   match op with
   | Expressions.Constant (ty, cv) ->
       let v = constant_value_to_typed_value ctx ty cv in
-      (ctx, v)
+      cf v ctx
   | Expressions.Copy p ->
       (* Access the value *)
       let access = Read in
       let expand_prim_copy = true in
-      let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
+      let cc = prepare_rplace config expand_prim_copy access p in
       (* Copy the value *)
-      assert (not (bottom_in_value ctx.ended_regions v));
-      assert (
-        Option.is_none
-          (find_first_primitively_copyable_sv_with_borrows
-             ctx.type_context.type_infos v));
-      let allow_adt_copy = false in
-      copy_value allow_adt_copy config ctx v
-  | Expressions.Move p -> (
+      let copy cf v : m_fun =
+       fun ctx ->
+        (* Sanity checks *)
+        assert (not (bottom_in_value ctx.ended_regions v));
+        assert (
+          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 ctx, v = copy_value allow_adt_copy config ctx v in
+        (* Continue *)
+        cf v ctx
+      in
+      (* Compose and apply *)
+      comp cc copy cf ctx
+  | Expressions.Move p ->
       (* Access the value *)
       let access = Move in
       let expand_prim_copy = false in
-      let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
+      let cc = prepare_rplace config expand_prim_copy access p in
       (* Move the value *)
-      assert (not (bottom_in_value ctx.ended_regions v));
-      let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
-      match write_place config access p bottom ctx with
-      | Error _ -> failwith "Unreachable"
-      | Ok ctx -> (ctx, v))
+      let move cf v : m_fun =
+       fun ctx ->
+        assert (not (bottom_in_value ctx.ended_regions v));
+        let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
+        match write_place config access p bottom ctx with
+        | Error _ -> failwith "Unreachable"
+        | Ok ctx -> cf v ctx
+      in
+      (* Compose and apply *)
+      comp cc move cf ctx
 
 (** Small utility.
 
     See [eval_operand_prepare].
  *)
-let eval_operands_prepare (config : C.config) (ctx : C.eval_ctx)
-    (ops : E.operand list) : C.eval_ctx * V.typed_value list =
-  List.fold_left_map (fun ctx op -> eval_operand_prepare config ctx op) ctx ops
+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
 
 (** Evaluate several operands. *)
-let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : E.operand list)
-    : C.eval_ctx * V.typed_value list =
-  let ctx, _ = eval_operands_prepare config ctx ops in
-  List.fold_left_map (fun ctx op -> eval_operand config ctx op) ctx ops
+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
+  (* Evaluate the operands *)
+  let eval = fold_left_apply_continuation (eval_operand config) ops in
+  (* Compose and apply *)
+  comp prepare (fun cf (_ : V.typed_value list) -> eval cf) cf ctx
 
-let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : E.operand)
-    (op2 : E.operand) : C.eval_ctx * V.typed_value * V.typed_value =
-  match eval_operands config ctx [ op1; op2 ] with
-  | ctx, [ v1; v2 ] -> (ctx, v1, v2)
-  | _ -> failwith "Unreachable"
+let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand)
+    (cf : V.typed_value * V.typed_value -> m_fun) : m_fun =
+  let eval_op = eval_operands config [ op1; op2 ] in
+  let use_res cf res =
+    match res with [ v1; v2 ] -> cf (v1, v2) | _ -> failwith "Unreachable"
+  in
+  comp eval_op use_res cf
 
-let eval_unary_op_concrete (config : C.config) (ctx : C.eval_ctx)
-    (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result
-    =
+let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand)
+    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operand *)
-  let ctx, v = eval_operand config ctx op in
+  let eval_op = eval_operand config op in
   (* Apply the unop *)
-  match (unop, v.V.value) with
-  | E.Not, V.Concrete (Bool b) ->
-      Ok (ctx, { v with V.value = V.Concrete (Bool (not b)) })
-  | E.Neg, V.Concrete (V.Scalar sv) -> (
-      let i = Z.neg sv.V.value in
-      match mk_scalar sv.int_ty i with
-      | Error _ -> Error Panic
-      | Ok sv -> Ok (ctx, { v with V.value = V.Concrete (V.Scalar sv) }))
-  | _ -> failwith "Invalid input for unop"
+  let apply cf (v : V.typed_value) : m_fun =
+    match (unop, v.V.value) with
+    | E.Not, V.Concrete (Bool b) ->
+        cf (Ok { v with V.value = V.Concrete (Bool (not b)) })
+    | E.Neg, V.Concrete (V.Scalar sv) -> (
+        let i = Z.neg sv.V.value in
+        match mk_scalar sv.int_ty i with
+        | Error _ -> cf (Error EPanic)
+        | Ok sv -> cf (Ok { v with V.value = V.Concrete (V.Scalar sv) }))
+    | _ -> failwith "Invalid input for unop"
+  in
+  comp eval_op apply cf
 
-let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
-    (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result
-    =
+let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
+    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operand *)
-  let ctx, v = eval_operand config ctx op in
+  let eval_op = eval_operand config op in
   (* Generate a fresh symbolic value to store the result *)
-  let res_sv_id = C.fresh_symbolic_value_id () in
-  let res_sv_ty =
-    match (unop, v.V.ty) with
-    | E.Not, T.Bool -> T.Bool
-    | E.Neg, T.Integer int_ty -> T.Integer int_ty
-    | _ -> failwith "Invalid input for unop"
+  let apply cf (v : V.typed_value) : m_fun =
+    let res_sv_id = C.fresh_symbolic_value_id () in
+    let res_sv_ty =
+      match (unop, v.V.ty) with
+      | E.Not, T.Bool -> T.Bool
+      | E.Neg, T.Integer int_ty -> T.Integer int_ty
+      | _ -> failwith "Invalid input for unop"
+    in
+    let res_sv =
+      { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+    in
+    (* Synthesize *)
+    S.synthesize_unary_op unop v res_sv;
+    (* Call the continuation *)
+    cf (Ok (mk_typed_value_from_symbolic_value res_sv))
   in
-  let res_sv =
-    { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
-  in
-  (* Synthesize *)
-  S.synthesize_unary_op unop v res_sv;
-  (* Return *)
-  Ok (ctx, mk_typed_value_from_symbolic_value res_sv)
+  (* Compose and apply *)
+  comp eval_op apply cf
 
-let eval_unary_op (config : C.config) (ctx : C.eval_ctx) (unop : E.unop)
-    (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result =
+let eval_unary_op (config : C.config) (unop : E.unop) (op : E.operand)
+    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
   match config.mode with
-  | C.ConcreteMode -> eval_unary_op_concrete config ctx unop op
-  | C.SymbolicMode -> eval_unary_op_symbolic config ctx unop op
+  | C.ConcreteMode -> eval_unary_op_concrete config unop op cf
+  | C.SymbolicMode -> eval_unary_op_symbolic config unop op cf
 
-let eval_binary_op_concrete (config : C.config) (ctx : C.eval_ctx)
-    (binop : E.binop) (op1 : E.operand) (op2 : E.operand) :
-    (C.eval_ctx * V.typed_value) eval_result =
+let eval_binary_op_concrete (config : C.config) (binop : E.binop)
+    (op1 : E.operand) (op2 : E.operand)
+    (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
   (* Evaluate the operands *)
   let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
   (* Equality check binops (Eq, Ne) accept values from a wide variety of types.
@@ -338,8 +377,8 @@ let eval_binary_op_concrete (config : C.config) (ctx : C.eval_ctx)
         match res with Error _ -> Error Panic | Ok v -> Ok (ctx, v))
     | _ -> failwith "Invalid inputs for binop"
 
-let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
-    (binop : E.binop) (op1 : E.operand) (op2 : E.operand) :
+let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
+    (op1 : E.operand) (op2 : E.operand) :
     (C.eval_ctx * V.typed_value) eval_result =
   (* Evaluate the operands *)
   let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
@@ -376,9 +415,8 @@ let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
   (* Return *)
   Ok (ctx, mk_typed_value_from_symbolic_value res_sv)
 
-let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
-    (op1 : E.operand) (op2 : E.operand) :
-    (C.eval_ctx * V.typed_value) eval_result =
+let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand)
+    (op2 : E.operand) : (C.eval_ctx * V.typed_value) eval_result =
   match config.mode with
   | C.ConcreteMode -> eval_binary_op_concrete config ctx binop op1 op2
   | C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2
@@ -516,8 +554,8 @@ let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx)
     of a symbolic enumeration value), while it is not the case for the
     other rvalues.
  *)
-let eval_rvalue_non_discriminant (config : C.config) (ctx : C.eval_ctx)
-    (rvalue : E.rvalue) : (C.eval_ctx * V.typed_value) eval_result =
+let eval_rvalue_non_discriminant (config : C.config) (rvalue : E.rvalue) :
+    (C.eval_ctx * V.typed_value) eval_result =
   match rvalue with
   | E.Use op -> Ok (eval_operand config ctx op)
   | E.Ref (p, bkind) -> Ok (eval_rvalue_ref config ctx p bkind)
@@ -534,7 +572,7 @@ let eval_rvalue_non_discriminant (config : C.config) (ctx : C.eval_ctx)
     `discriminant` might lead to a branching in case it is applied
     on a symbolic enumeration value.
 *)
-let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
+let eval_rvalue (config : C.config) (rvalue : E.rvalue) :
     (C.eval_ctx * V.typed_value) list eval_result =
   match rvalue with
   | E.Discriminant p -> Ok (eval_rvalue_discriminant config p ctx)