From b68bc96ce46a8b8b32556ab11d1577d4a124db9b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jan 2022 16:29:42 +0100
Subject: Implement the mut case of expand_symbolic_value_borrow

---
 src/Interpreter.ml | 75 +++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 51 insertions(+), 24 deletions(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index c871d530..0e88be2d 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2787,34 +2787,51 @@ let apply_symbolic_expansion_to_avalues (config : C.config)
   let ctx = apply_expansion BorrowProj ctx in
   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...).
+(** Auxiliary function.
+
+    Simply replace the symbolic values (*not avalues*) in the context with
+    a given value. Will break invariants if not used properly.
 *)
-let apply_symbolic_expansion_non_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Convert the expansion to a value *)
-  let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
-  (* Visitor to apply the expansion to *non-abstraction* values *)
+let replace_symbolic_values (config : C.config) (at_most_once : bool)
+    (original_sv : V.symbolic_value) (nv : V.value) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  (* Count *)
+  let replaced = ref false in
+  let replace () =
+    if at_most_once then assert (not !replaced);
+    replaced := true;
+    nv
+  in
+  (* Visitor to apply the substitution *)
   let obj =
     object
       inherit [_] C.map_eval_ctx as super
 
       method! visit_Symbolic env spc =
-        if spc.V.svalue = original_sv then nv.V.value
+        if spc.V.svalue = original_sv then replace ()
         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 *)
+  (* Apply the substitution *)
   let ctx = obj#visit_eval_ctx None ctx in
+  (* Check that we substituted *)
+  assert !replaced;
+  (* Return *)
+  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 : symbolic_expansion)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Apply the expansion to non-abstraction values *)
+  let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
+  let at_most_once = false in
+  let ctx =
+    replace_symbolic_values config at_most_once original_sv nv.V.value ctx
+  in
   (* Apply the expansion to abstraction values *)
   let allow_reborrows = false in
   apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
@@ -2984,7 +3001,8 @@ let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t)
   let see = SeAdt (None, [ boxed_value ]) in
   (ctx, see)
 
-let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
+let expand_symbolic_value_borrow (config : C.config)
+    (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t)
     (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* Check that we are allowed to expand the reference *)
@@ -2996,7 +3014,18 @@ let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
        * borrow id *)
       let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in
       let ctx, bid = C.fresh_borrow_id ctx in
-      raise Unimplemented
+      let see = SeMutRef (bid, sv) in
+      (* Expand the symbolic values - we simply perform a substitution (and
+       * check that we perform exactly one substitution) *)
+      let nv = symbolic_expansion_to_value_with_borrows original_sv see in
+      let at_most_once = true in
+      let ctx =
+        replace_symbolic_values config at_most_once original_sv nv.V.value ctx
+      in
+      (* Expand the symbolic avalues *)
+      let allow_reborrows = true in
+      apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
+        ctx
   | T.Shared -> raise Unimplemented
 
 (** Expand a symbolic value which is not an enumeration with several variants.
@@ -3043,10 +3072,8 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
       apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
   (* Borrows *)
   | Deref, T.Ref (region, ref_ty, rkind) ->
-      let _ =
-        expand_symbolic_value_borrow ended_regions region ref_ty rkind ctx
-      in
-      raise Unimplemented
+      expand_symbolic_value_borrow config sp.V.svalue ended_regions region
+        ref_ty rkind ctx
   | _ ->
       failwith
         ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
-- 
cgit v1.2.3