Update eval_operand_prepare to not give a value to the continuation

1 files changed, 95 insertions, 51 deletions

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 ->