From ef01ffedcff24c657c8046428cae36251f80636c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jan 2022 23:00:33 +0100
Subject: Update InterpreterExpansion and InterpreterPaths to use CPS

---
 src/Cps.ml                  |   5 +-
 src/InterpreterExpansion.ml | 158 ++++++++++++++++++---------------------
 src/InterpreterPaths.ml     | 178 +++++++++++++++++++++++---------------------
 3 files changed, 170 insertions(+), 171 deletions(-)

diff --git a/src/Cps.ml b/src/Cps.ml
index fca22fd3..10bf1c6d 100644
--- a/src/Cps.ml
+++ b/src/Cps.ml
@@ -14,7 +14,7 @@ type statement_eval_res =
   | Panic
 
 (** Synthesized expresssion - dummy for now *)
-type sexpr = SExpr
+type sexpr = SOne | SList of sexpr list
 
 type eval_result = sexpr option
 
@@ -53,6 +53,9 @@ let comp_update (f : cm_fun) (g : C.eval_ctx -> C.eval_ctx) : cm_fun =
 (** This is just a test, to check that [comp] is general enough to handle a case
     where a function must compute a value and give it to the continuation.
     It happens for functions like [eval_operand].
+
+    Keeping this here also makes it a good reference, when one wants to figure
+    out the signatures he should use for such a composition.
  *)
 let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun)
     (g : m_fun -> V.typed_value -> m_fun) : cm_fun =
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 5d2d4f6f..b3a0e3f2 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -12,6 +12,7 @@ module L = Logging
 open TypesUtils
 module Inv = Invariants
 module S = Synthesis
+open Cps
 open ValuesUtils
 open InterpreterUtils
 open InterpreterProjectors
@@ -262,8 +263,8 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
   see
 
 let expand_symbolic_value_shared_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (ref_ty : T.rty) (ctx : C.eval_ctx) :
-    C.eval_ctx =
+    (original_sv : V.symbolic_value) (ref_ty : T.rty) : cm_fun =
+ fun cf ctx ->
   (* First, replace the projectors on borrows.
    * The important point is that the symbolic value to expand may appear
    * several times, if it has been copied. In this case, we need to introduce
@@ -370,12 +371,14 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   in
   (* Update the synthesized program *)
   S.synthesize_symbolic_expansion_no_branching original_sv see;
-  (* Return *)
-  ctx
+  (* Continue *)
+  cf ctx
 
+(** TODO: simplify and merge with the other expansion function *)
 let expand_symbolic_value_borrow (config : C.config)
     (original_sv : V.symbolic_value) (region : T.RegionId.id T.region)
-    (ref_ty : T.rty) (rkind : T.ref_kind) (ctx : C.eval_ctx) : C.eval_ctx =
+    (ref_ty : T.rty) (rkind : T.ref_kind) : cm_fun =
+ fun cf ctx ->
   (* Check that we are allowed to expand the reference *)
   assert (not (region_in_set region ctx.ended_regions));
   (* Match on the reference kind *)
@@ -401,23 +404,28 @@ let expand_symbolic_value_borrow (config : C.config)
       in
       (* Update the synthesized program *)
       S.synthesize_symbolic_expansion_no_branching original_sv see;
-      (* Return *)
-      ctx
+      (* Continue *)
+      cf ctx
   | T.Shared ->
-      expand_symbolic_value_shared_borrow config original_sv ref_ty ctx
+      expand_symbolic_value_shared_borrow config original_sv ref_ty cf ctx
 
 (** Expand a symbolic value which is not an enumeration with several variants
     (i.e., in a situation where it doesn't lead to branching).
+    
+    [allow_branching]: if `true` we can branch (by expanding enumerations with
+    stricly more than one variant), otherwise we can't.
  *)
-let expand_symbolic_value_no_branching (config : C.config)
-    (sp : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
+let expand_symbolic_value (config : C.config) (allow_branching : bool)
+    (sp : V.symbolic_value) : cm_fun =
+ fun cf ctx ->
   (* Remember the initial context for printing purposes *)
   let ctx0 = ctx in
   (* Compute the expanded value - note that when doing so, we may introduce
    * fresh symbolic values in the context (which thus gets updated) *)
   let original_sv = sp in
   let rty = original_sv.V.sv_ty in
-  let ctx =
+  let cc : cm_fun =
+   fun cf ctx ->
     match rty with
     (* "Regular" ADTs *)
     | T.Adt (T.AdtId def_id, regions, types) -> (
@@ -428,15 +436,22 @@ let expand_symbolic_value_no_branching (config : C.config)
           compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
             def_id regions types ctx
         with
-        | [ see ] ->
+        | seel ->
+            (* Check for branching *)
+            assert (List.length seel <= 1 || allow_branching);
             (* Apply in the context *)
-            let ctx =
-              apply_symbolic_expansion_non_borrow config original_sv see ctx
+            let ctxl =
+              List.map
+                (fun see ->
+                  apply_symbolic_expansion_non_borrow config original_sv see ctx)
+                seel
             in
-            (* Update the synthesized program *)
-            S.synthesize_symbolic_expansion_no_branching original_sv see;
+            (* Continue *)
+            let resl = List.map (fun ctx -> Option.get (cf ctx)) ctxl in
+            (* Synthesize *)
+            let res = S.synthesize_symbolic_expansion original_sv resl in
             (* Return *)
-            ctx
+            Some res
         | _ ->
             failwith
               "expand_symbolic_value_no_branching: the expansion lead to \
@@ -451,8 +466,8 @@ let expand_symbolic_value_no_branching (config : C.config)
         in
         (* Update the synthesized program *)
         S.synthesize_symbolic_expansion_no_branching original_sv see;
-        (* Return *)
-        ctx
+        (* Continue *)
+        cf ctx
     (* Boxes *)
     | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
         let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in
@@ -462,62 +477,36 @@ let expand_symbolic_value_no_branching (config : C.config)
         in
         (* Update the synthesized program *)
         S.synthesize_symbolic_expansion_no_branching original_sv see;
-        (* Return *)
-        ctx
+        (* Continue *)
+        cf ctx
     (* Borrows *)
     | T.Ref (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow config original_sv region ref_ty rkind ctx
+        expand_symbolic_value_borrow config original_sv region ref_ty rkind cf
+          ctx
     | _ ->
         failwith
           ("expand_symbolic_value_no_branching: unreachable: " ^ T.show_rty rty)
   in
-  (* Debugging *)
   (* Debug *)
-  log#ldebug
-    (lazy
-      ("expand_symbolic_value: "
-      ^ symbolic_value_to_string ctx0 sp
-      ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
-      ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
-  (* Sanity check: the symbolic value has disappeared *)
-  assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
-  (* Return *)
-  ctx
-
-(** Expand a symbolic enumeration value.
-
-    This might lead to branching.
- *)
-let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
-    (ctx : C.eval_ctx) : C.eval_ctx list =
-  (* Compute the expanded value - note that when doing so, we may introduce
-   * fresh symbolic values in the context (which thus gets updated) *)
-  let original_sv = sp in
-  let rty = original_sv.V.sv_ty in
-  match rty with
-  (*  The value should be a "regular" ADTs *)
-  | T.Adt (T.AdtId def_id, regions, types) ->
-      (* Compute the expanded value - there should be exactly one because we
-       * don't allow to expand enumerations with strictly more than one variant *)
-      let expand_enumerations = true in
-      let seel =
-        compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
-          def_id regions types ctx
-      in
-      (* Update the synthesized program *)
-      S.synthesize_symbolic_expansion_enum_branching original_sv seel;
-      (* Apply in the context *)
-      let apply see : C.eval_ctx =
-        let ctx =
-          apply_symbolic_expansion_non_borrow config original_sv see ctx
-        in
+  let cc =
+    comp_unit cc (fun ctx ->
+        log#ldebug
+          (lazy
+            ("expand_symbolic_value_no_branching: "
+            ^ symbolic_value_to_string ctx0 sp
+            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
+            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
-        (* Return *)
-        ctx
-      in
-      List.map apply seel
-  | _ -> failwith "Unexpected"
+        assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)))
+  in
+  (* Continue *)
+  cc cf ctx
+
+(** See [expand_symbolic_value] *)
+let expand_symbolic_value_no_branching (config : C.config)
+    (sp : V.symbolic_value) : cm_fun =
+  let allow_branching = false in
+  expand_symbolic_value config allow_branching sp
 
 (** Expand all the symbolic values which contain borrows.
     Allows us to restrict ourselves to a simpler model for the projectors over
@@ -527,8 +516,8 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
     an enumeration with strictly more than one variant, a slice, etc.) or if
     we need to expand a recursive type (because this leads to looping).
  *)
-let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx)
-    : C.eval_ctx =
+let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
+ fun cf ctx ->
   (* The visitor object, to look for symbolic values in the concrete environment *)
   let obj =
     object
@@ -544,13 +533,15 @@ let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx)
     end
   in
 
-  let rec expand (ctx : C.eval_ctx) : C.eval_ctx =
+  let rec expand : cm_fun =
+   fun cf ctx ->
     try
       obj#visit_eval_ctx () ctx;
-      ctx
+      (* Nothing to expand: continue *)
+      cf ctx
     with FoundSymbolicValue sv ->
       (* Expand and recheck the environment *)
-      let ctx =
+      let cc : cm_fun =
         match sv.V.sv_ty with
         | T.Adt (AdtId def_id, _, _) ->
             (* [expand_symbolic_value_no_branching] checks if there are branchings,
@@ -571,27 +562,26 @@ let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx)
                 ("Attempted to greedily expand a recursive definition (option \
                   [greedy_expand_symbolics_with_borrows] of [config]): "
                 ^ Print.name_to_string def.name)
-            else expand_symbolic_value_no_branching config sv ctx
+            else expand_symbolic_value_no_branching config sv
         | T.Adt ((Tuple | Assumed Box), _, _) | T.Ref (_, _, _) ->
             (* Ok *)
-            expand_symbolic_value_no_branching config sv ctx
+            expand_symbolic_value_no_branching config sv
         | T.Array _ -> raise Errors.Unimplemented
         | T.Slice _ -> failwith "Can't expand symbolic slices"
         | T.TypeVar _ | Bool | Char | Never | Integer _ | Str ->
             failwith "Unreachable"
       in
-      expand ctx
+      (* Compose and continue *)
+      comp cc expand cf ctx
   in
-  expand ctx
+  (* Apply *)
+  expand cf ctx
 
 (** If this mode is activated through the [config], greedily expand the symbolic
     values which need to be expanded. See [config] for more information.
  *)
-let greedy_expand_symbolic_values (config : C.config) (ctx : C.eval_ctx) :
-    C.eval_ctx =
-  let ctx =
-    if config.greedy_expand_symbolics_with_borrows then
-      greedy_expand_symbolics_with_borrows config ctx
-    else ctx
-  in
-  ctx
+let greedy_expand_symbolic_values (config : C.config) : cm_fun =
+ fun cf ctx ->
+  if config.greedy_expand_symbolics_with_borrows then
+    greedy_expand_symbolics_with_borrows config cf ctx
+  else cf ctx
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 431a2076..f364c386 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -5,6 +5,7 @@ module C = Contexts
 module Subst = Substitute
 module L = Logging
 module S = Synthesis
+open Cps
 open TypesUtils
 open ValuesUtils
 open InterpreterUtils
@@ -458,69 +459,78 @@ let expand_bottom_value_from_projection (config : C.config)
     expanding symbolic values) until we manage to fully read the place.
  *)
 let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
-    (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
+    (p : E.place) : cm_fun =
+ fun cf ctx ->
   (* Attempt to read the place: if it fails, update the environment and retry *)
   match read_place config access p ctx with
-  | Ok _ -> ctx
+  | Ok _ -> cf ctx
   | Error err ->
-      let ctx =
+      let cc =
         match err with
-        | FailSharedLoan bids -> end_outer_borrows config bids ctx
-        | FailMutLoan bid -> end_outer_borrow config bid ctx
+        | FailSharedLoan bids -> end_outer_borrows config bids
+        | FailMutLoan bid -> end_outer_borrow config bid
         | FailInactivatedMutBorrow bid ->
-            activate_inactivated_mut_borrow config bid ctx
+            activate_inactivated_mut_borrow config bid
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching config sp ctx
+            expand_symbolic_value_no_branching config sp
         | FailBottom (_, _, _) ->
             (* We can't expand [Bottom] values while reading them *)
             failwith "Found [Bottom] while reading a place"
         | FailBorrow _ -> failwith "Could not read a borrow"
       in
-      update_ctx_along_read_place config access p ctx
+      comp cc (update_ctx_along_read_place config access p) cf ctx
 
 (** Update the environment to be able to write to a place.
 
     See [update_env_alond_read_place].
 *)
 let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
-    (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Attempt to *read* (yes, "read": we check the access to the place, and
+    (p : E.place) : cm_fun =
+ fun cf ctx ->
+  (* Attempt to *read* (yes, *read*: we check the access to the place, and
      write to it later) the place: if it fails, update the environment and retry *)
   match read_place config access p ctx with
-  | Ok _ -> ctx
+  | Ok _ -> cf ctx
   | Error err ->
-      let ctx =
+      (* Update the context *)
+      let cc =
         match err with
-        | FailSharedLoan bids -> end_outer_borrows config bids ctx
-        | FailMutLoan bid -> end_outer_borrow config bid ctx
+        | FailSharedLoan bids -> end_outer_borrows config bids
+        | FailMutLoan bid -> end_outer_borrow config bid
         | FailInactivatedMutBorrow bid ->
-            activate_inactivated_mut_borrow config bid ctx
+            activate_inactivated_mut_borrow config bid
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching config sp ctx
+            expand_symbolic_value_no_branching config sp
         | FailBottom (remaining_pes, pe, ty) ->
             (* Expand the [Bottom] value *)
-            expand_bottom_value_from_projection config access p remaining_pes pe
-              ty ctx
+            fun cf ctx ->
+             let ctx =
+               expand_bottom_value_from_projection config access p remaining_pes
+                 pe ty ctx
+             in
+             cf ctx
         | FailBorrow _ -> failwith "Could not write to a borrow"
       in
-      update_ctx_along_write_place config access p ctx
+      (* Retry *)
+      comp cc (update_ctx_along_write_place config access p) cf ctx
 
-exception UpdateCtx of C.eval_ctx
+exception UpdateCtx of cm_fun
 (** Small utility used to break control-flow *)
 
 (** End the loans at a given place: read the value, if it contains a loan,
     end this loan, repeat.
 
-    This is used when reading, borrowing, writing to a value. We typically
+    This is used when reading or borrowing values. We typically
     first call [update_ctx_along_read_place] or [update_ctx_along_write_place]
     to get access to the value, then call this function to "prepare" the value:
     when moving values, we can't move a value which contains loans and thus need
     to end them, etc.
  *)
 let rec end_loans_at_place (config : C.config) (access : access_kind)
-    (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
+    (p : E.place) : cm_fun =
+ fun cf ctx ->
   (* Iterator to explore a value and update the context whenever we find
    * loans.
    * We use exceptions to make it handy: whenever we update the
@@ -536,8 +546,8 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
             (* Nothing special to do *) super#visit_borrow_content env bc
         | V.InactivatedMutBorrow bid ->
             (* We need to activate inactivated borrows *)
-            let ctx = activate_inactivated_mut_borrow config bid ctx in
-            raise (UpdateCtx ctx)
+            let cc = activate_inactivated_mut_borrow config bid in
+            raise (UpdateCtx cc)
 
       method! visit_loan_content env lc =
         match lc with
@@ -547,12 +557,12 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
             match access with
             | Read -> super#visit_SharedLoan env bids v
             | Write | Move ->
-                let ctx = end_outer_borrows config bids ctx in
-                raise (UpdateCtx ctx))
+                let cc = end_outer_borrows config bids in
+                raise (UpdateCtx cc))
         | V.MutLoan bid ->
             (* We always need to end mutable borrows *)
-            let ctx = end_outer_borrow config bid ctx in
-            raise (UpdateCtx ctx)
+            let cc = end_outer_borrow config bid in
+            raise (UpdateCtx cc)
     end
   in
 
@@ -568,11 +578,12 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
       *)
       try
         obj#visit_typed_value () v;
-        (* No context update required: return the current context *)
-        ctx
-      with UpdateCtx ctx ->
-        (* The context was updated: do a recursive call to reinspect the value *)
-        end_loans_at_place config access p ctx)
+        (* No context update required: apply the continuation *)
+        cf ctx
+      with UpdateCtx cc ->
+        (* We need to update the context: compose the caugth continuation with
+         * a recursive call to reinspect the value *)
+        comp cc (end_loans_at_place config access p) cf ctx)
 
 (** Drop (end) loans and borrows at a given place, which should be
     seen as an l-value (we will write to it later, but need to drop
@@ -608,7 +619,8 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
     - the borrow corresponding to the loan `mut_loan l3` is outside of `*x`
  *)
 let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
-    (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
+    (p : E.place) : cm_fun =
+ fun cf ctx ->
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
   let access = Write in
@@ -616,43 +628,50 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
   let ctx = write_place_unwrap config access p (mk_bottom v.V.ty) ctx in
   let ctx = C.ctx_push_dummy_var ctx v in
   (* Auxiliary function *)
-  let rec drop (ctx : C.eval_ctx) : C.eval_ctx =
+  let rec drop : cm_fun =
+   fun cf ctx ->
     (* Read the value *)
     let v = C.ctx_read_first_dummy_var ctx in
     (* Check if there are loans or borrows to end *)
     match get_first_outer_loan_or_borrow_in_value end_borrows v with
     | None ->
-        (* We are done *)
-        ctx
+        (* We are done: simply call the continuation *)
+        cf ctx
     | Some c ->
         (* There are: end them then retry *)
-        let ctx =
+        let cc =
           match c with
           | LoanContent (V.SharedLoan (bids, _)) ->
-              end_outer_borrows config bids ctx
+              end_outer_borrows config bids
           | LoanContent (V.MutLoan bid)
           | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow bid) ->
-              end_outer_borrow config bid ctx
+              end_outer_borrow config bid
           | BorrowContent (V.InactivatedMutBorrow bid) ->
               (* First activate the borrow *)
-              activate_inactivated_mut_borrow config bid ctx
+              activate_inactivated_mut_borrow config bid
         in
         (* Retry *)
-        drop ctx
+        comp cc drop cf ctx
   in
-  (* Apply *)
-  let ctx = drop ctx in
-  (* Pop the temporary value *)
-  let ctx, v = C.ctx_pop_dummy_var ctx in
-  (* Reinsert the value *)
-  let ctx = write_place_unwrap config access p v ctx in
-  (* Sanity check *)
-  if end_borrows then (
-    assert (not (loans_in_value v));
-    assert (not (borrows_in_value v)))
-  else assert (not (outer_loans_in_value v));
-  (* Return *)
-  ctx
+  (* Apply the drop function *)
+  let cc = drop in
+  (* Pop the temporary value and reinsert it *)
+  let cc =
+    comp cc (fun cf ctx ->
+        (* Pop *)
+        let ctx, v = C.ctx_pop_dummy_var ctx in
+        (* Reinsert *)
+        let ctx = write_place_unwrap config access p v ctx in
+        (* Sanity check *)
+        if end_borrows then (
+          assert (not (loans_in_value v));
+          assert (not (borrows_in_value v)))
+        else assert (not (outer_loans_in_value v));
+        (* Continue *)
+        cf ctx)
+  in
+  (* Continue *)
+  cc cf ctx
 
 (** Copy a value, and return the resulting value.
 
@@ -740,37 +759,24 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
     end all the loans and the borrows we find.
  *)
 let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place)
-    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
-  (* TODO *)
+    (cf : V.typed_value -> m_fun) : m_fun =
+ fun ctx ->
+  (* Access the place *)
   let access = Write in
-  let ctx = update_ctx_along_write_place config access p ctx in
+  let cc = update_ctx_along_write_place config access p in
   (* End the borrows and loans, starting with the borrows *)
-  let ctx = drop_outer_borrows_loans_at_lplace config end_borrows p ctx in
+  let cc = comp cc (drop_outer_borrows_loans_at_lplace config end_borrows p) in
   (* Read the value and check it *)
-  let v = read_place_unwrap config access p ctx in
-  (* Sanity checks *)
-  if end_borrows then (
-    assert (not (loans_in_value v));
-    assert (not (borrows_in_value v)))
-  else assert (not (outer_loans_in_value v));
-  (* Return *)
-  (ctx, v)
-
-(** Read the value at a given place.
-    As long as it is a loan, end the loan.
-    This function doesn't perform a recursive exploration:
-    it won't dive into the value to end all the inner
-    loans (contrary to [drop_borrows_loans_at_lplace] for
-    instance).
- *)
-let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
-    (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
-  let v = read_place_unwrap config access p ctx in
-  match v.V.value with
-  | V.Loan (V.SharedLoan (bids, _)) ->
-      let ctx = end_outer_borrows config bids ctx in
-      end_loan_exactly_at_place config access p ctx
-  | V.Loan (V.MutLoan bid) ->
-      let ctx = end_outer_borrow config bid ctx in
-      end_loan_exactly_at_place config access p ctx
-  | _ -> ctx
+  let read_check cf : m_fun =
+   fun ctx ->
+    let v = read_place_unwrap config access p ctx in
+    (* Sanity checks *)
+    if end_borrows then (
+      assert (not (loans_in_value v));
+      assert (not (borrows_in_value v)))
+    else assert (not (outer_loans_in_value v));
+    (* Continue *)
+    cf v ctx
+  in
+  (* Compose and apply the continuations *)
+  comp cc read_check cf ctx
-- 
cgit v1.2.3