Factorize some code

1 files changed, 88 insertions, 50 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 129b856b..4bb449bd 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1317,6 +1317,44 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
   (* Return *)
   ctx
 
+(** Auxiliary function to prepare reborrowing operations (used when
+    applying projectors).
+    
+    Returns two functions:
+    - a function to generate fresh re-borrow ids, and register the reborrows
+    - a function to apply the reborrows in a context
+    Those functions are of course stateful.
+ *)
+let prepare_reborrows (config : C.config) (allow_reborrows : bool)
+    (ctx : C.eval_ctx) :
+    (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) =
+  let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
+  let borrow_counter = ref ctx.C.borrow_counter in
+  (* The function to generate and register fresh reborrows *)
+  let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id =
+    if allow_reborrows then (
+      let bid', cnt' = V.BorrowId.fresh ctx.borrow_counter in
+      borrow_counter := cnt';
+      reborrows := (bid, bid') :: !reborrows;
+      bid')
+    else failwith "Unexpected reborrow"
+  in
+  (* The function to apply the reborrows in a context *)
+  let apply_registered_reborrows (ctx : C.eval_ctx) : C.eval_ctx =
+    match config.C.mode with
+    | C.ConcreteMode ->
+        (* Reborrows are introduced when applying projections in symbolic mode *)
+        assert (!borrow_counter = ctx.C.borrow_counter);
+        assert (!reborrows = []);
+        ctx
+    | C.SymbolicMode ->
+        (* Update the borrow counter *)
+        let ctx = { ctx with C.borrow_counter = !borrow_counter } in
+        (* Apply the reborrows *)
+        apply_reborrows !reborrows ctx
+  in
+  (fresh_reborrow, apply_registered_reborrows)
+
 (** Auxiliary function to end borrows. See [give_back].
     
     When we end a mutable borrow, we need to "give back" the value it contained
@@ -1336,15 +1374,12 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
   in
   (* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
   let check_symbolic_no_ended = true in
-  (* We sometimes need to reborrow values while giving a value back due *)
-  let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
-  let borrow_counter = ref ctx.C.borrow_counter in
-  let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id =
-    let bid', cnt' = V.BorrowId.fresh ctx.borrow_counter in
-    borrow_counter := cnt';
-    reborrows := (bid, bid') :: !reborrows;
-    bid'
+  (* We sometimes need to reborrow values while giving a value back due: prepare that *)
+  let allow_reborrows = true in
+  let fresh_reborrow, apply_registered_reborrows =
+    prepare_reborrows config allow_reborrows ctx
   in
+  (* The visitor to give back the values *)
   let obj =
     object (self)
       inherit [_] C.map_eval_ctx as super
@@ -1446,21 +1481,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
   (* Check we gave back to exactly one loan *)
   assert !replaced;
   (* Apply the reborrows *)
-  let ctx =
-    match config.C.mode with
-    | C.ConcreteMode ->
-        (* Reborrows are introduced when applying projections in symbolic mode *)
-        assert (!borrow_counter = ctx.C.borrow_counter);
-        assert (!reborrows = []);
-        ctx
-    | C.SymbolicMode ->
-        (* Update the borrow counter *)
-        let ctx = { ctx with C.borrow_counter = !borrow_counter } in
-        (* Apply the reborrows *)
-        apply_reborrows !reborrows ctx
-  in
-  (* Return *)
-  ctx
+  apply_registered_reborrows ctx
 
 (** Auxiliary function to end borrows. See [give_back].
 
@@ -2758,39 +2779,23 @@ let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
       raise Unimplemented
   | T.Shared -> raise Unimplemented
 
-(** Apply a symbolic expansion to a context, by replacing the original
-    symbolic value with its expanded value. Is valid only if the expansion
-    is not a borrow (i.e., an adt...).
+(** Auxiliary function.
+    Apply a symbolic expansion to avalues.
 *)
-let apply_symbolic_expansion_non_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (expansion : V.typed_value)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* [apply_proj_borrows] needs a [fresh_reborrow] function, to generate
-     fresh identifiers and register reborrows, whenever needed. As we don't
-     expand borrows, we shouldn't have to apply reborrows. *)
-  let fresh_reborrow (_ : V.BorrowId.id) : V.BorrowId.id =
-    failwith "Unexpected reborrow"
-  in
-  (* For the projectors: it might happen that the expansion contains symbolic
-     variables with already ended regions.
-  *)
+let apply_symbolic_expansion_to_avalues (config : C.config)
+    (allow_reborrows : bool) (original_sv : V.symbolic_value)
+    (expansion : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Symbolic values contained in the expansion might contain already ended regions *)
   let check_symbolic_no_ended = false in
+  (* Prepare reborrows registration *)
+  let fresh_reborrow, apply_registered_reborrows =
+    prepare_reborrows config allow_reborrows ctx
+  in
   (* Visitor to apply the expansion *)
   let obj =
     object
       inherit [_] C.map_eval_ctx as super
 
-      method! visit_Symbolic env spc =
-        if spc.V.svalue = original_sv then expansion.V.value
-        else super#visit_Symbolic env spc
-      (** Replace a symbolic value with its expansion.
-          Note that there may be several references to the same symbolic value
-          in the context, if the value has been copied. Expansion is then a bit
-          subtle in the case we expand shared borrows, in which case we need to
-          introduce a unique borrow identifier for every borrow (this is not
-          the case here: this function should NOT be used to expand borrows).
-      *)
-
       method! visit_abs proj_regions abs =
         assert (Option.is_none proj_regions);
         let proj_regions = Some abs.V.regions in
@@ -2830,7 +2835,40 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
     end
   in
   (* Apply the expansion *)
-  obj#visit_eval_ctx None ctx
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Apply the reborrows *)
+  apply_registered_reborrows ctx
+
+(** Apply a symbolic expansion to a context, by replacing the original
+    symbolic value with its expanded value. Is valid only if the expansion
+    is not a borrow (i.e., an adt...).
+*)
+let apply_symbolic_expansion_non_borrow (config : C.config)
+    (original_sv : V.symbolic_value) (expansion : V.typed_value)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Visitor to apply the expansion to non-abstraction values *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Symbolic env spc =
+        if spc.V.svalue = original_sv then expansion.V.value
+        else super#visit_Symbolic env spc
+      (** Replace a symbolic value with its expansion.
+          Note that there may be several references to the same symbolic value
+          in the context, if the value has been copied. Expansion is then a bit
+          subtle in the case we expand shared borrows, in which case we need to
+          introduce a unique borrow identifier for every borrow (this is not
+          the case here: this function should NOT be used to expand borrows).
+      *)
+    end
+  in
+  (* Apply the expansion to non-abstraction values *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Apply the expansion to abstraction values *)
+  let allow_reborrows = false in
+  apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+    expansion ctx
 
 (** Expand a symbolic value which is not an enumeration with several variants.