Add a meta-value in SharedBorrow to carry the shared value

9 files changed, 78 insertions, 53 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index f87d053c..b231722d 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -89,7 +89,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
 
       method! visit_Borrow outer bc =
         match bc with
-        | SharedBorrow l' | InactivatedMutBorrow l' ->
+        | SharedBorrow (_, l') | InactivatedMutBorrow l' ->
             (* Check if this is the borrow we are looking for *)
             if l = l' then (
               (* Check if there are outer borrows or if we are inside an abstraction *)
@@ -713,7 +713,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
       (* Update the context *)
       give_back_value config l tv ctx
-  | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') ->
+  | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow l') ->
       (* Sanity check *)
       assert (l' = l);
       (* Check that the borrow is somewhere - purely a sanity check *)
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 81f9d0d3..b4ab7706 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -194,9 +194,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
 
       method! visit_borrow_content env bc =
         match bc with
-        | V.SharedBorrow bid ->
+        | V.SharedBorrow (mv, bid) ->
             (* Nothing specific to do *)
-            super#visit_SharedBorrow env bid
+            super#visit_SharedBorrow env mv bid
         | V.InactivatedMutBorrow bid ->
             (* Nothing specific to do *)
             super#visit_InactivatedMutBorrow env bid
@@ -305,7 +305,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
 
       method! visit_borrow_content env bc =
         match bc with
-        | V.SharedBorrow _ | V.InactivatedMutBorrow _ ->
+        | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ ->
             (* Nothing specific to do *)
             super#visit_borrow_content env bc
         | V.MutBorrow (bid, mv) ->
@@ -407,7 +407,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
             if bid = l then raise (FoundGBorrowContent (Concrete bc))
             else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
             else ()
-        | V.SharedBorrow bid ->
+        | V.SharedBorrow (_, bid) ->
             (* Check the borrow id *)
             if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
         | V.InactivatedMutBorrow bid ->
@@ -490,9 +490,9 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
             if bid = l then update ()
             else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
             else V.MutBorrow (bid, mv)
-        | V.SharedBorrow bid ->
+        | V.SharedBorrow (mv, bid) ->
             (* Check the id *)
-            if bid = l then update () else super#visit_SharedBorrow env bid
+            if bid = l then update () else super#visit_SharedBorrow env mv bid
         | V.InactivatedMutBorrow bid ->
             (* Check the id *)
             if bid = l then update ()
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 69e12545..2dd36535 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -298,6 +298,8 @@ let expand_symbolic_value_shared_borrow (config : C.config)
       | _ -> failwith "Unexpected"
     else None
   in
+  (* The fresh symbolic value for the shared value *)
+  let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
   (* Visitor to replace the projectors on borrows *)
   let obj =
     object (self)
@@ -306,7 +308,8 @@ let expand_symbolic_value_shared_borrow (config : C.config)
       method! visit_Symbolic env sv =
         if same_symbolic_id sv original_sv then
           let bid = fresh_borrow () in
-          V.Borrow (V.SharedBorrow bid)
+          V.Borrow
+            (V.SharedBorrow (mk_typed_value_from_symbolic_value shared_sv, bid))
         else super#visit_Symbolic env sv
 
       method! visit_Abs proj_regions abs =
@@ -362,7 +365,6 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
   assert (not (V.BorrowId.Set.is_empty bids));
-  let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
   let see = V.SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 3ebce9bf..84f51c94 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -508,33 +508,34 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
       (* Evaluate the borrowing operation *)
       let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
        fun ctx ->
-        (* Compute the rvalue - simply a shared borrow with a fresh id *)
+        (* Generate the fresh borrow id *)
         let bid = C.fresh_borrow_id () in
-        (* Note that the reference is *mutable* if we do a two-phase borrow *)
-        let rv_ty =
-          T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
-        in
-        let bc =
-          if bkind = E.Shared then V.SharedBorrow bid
-          else V.InactivatedMutBorrow bid
-        in
-        let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
-        (* Compute the value with which to replace the value at place p *)
-        let nv =
+        (* Compute the loan value, with which to replace the value at place p *)
+        let nv, shared_mvalue =
           match v.V.value with
           | V.Loan (V.SharedLoan (bids, sv)) ->
               (* Shared loan: insert the new borrow id *)
               let bids1 = V.BorrowId.Set.add bid bids in
-              { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }
+              ({ v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }, sv)
           | _ ->
               (* Not a shared loan: add a wrapper *)
               let v' =
                 V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v))
               in
-              { v with V.value = v' }
+              ({ v with V.value = v' }, v)
         in
-        (* Update the value in the context *)
+        (* Update the borrowed value in the context *)
         let ctx = write_place_unwrap config access p nv ctx in
+        (* Compute the rvalue - simply a shared borrow with a the fresh id.
+         * Note that the reference is *mutable* if we do a two-phase borrow *)
+        let rv_ty =
+          T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
+        in
+        let bc =
+          if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid)
+          else V.InactivatedMutBorrow bid
+        in
+        let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
         (* Continue *)
         cf rv ctx
       in
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index e45dbb3a..300e50c5 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -160,7 +160,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
       (* Borrows *)
       | Deref, V.Borrow bc, _ -> (
           match bc with
-          | V.SharedBorrow bid ->
+          | V.SharedBorrow (_, bid) ->
               (* Lookup the loan content, and explore from there *)
               if access.lookup_shared_borrows then
                 match lookup_loan ek bid ctx with
@@ -643,7 +643,7 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
           | LoanContent (V.SharedLoan (bids, _)) ->
               end_outer_borrows config bids
           | LoanContent (V.MutLoan bid)
-          | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow bid) ->
+          | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow (_, bid)) ->
               end_outer_borrow config bid
           | BorrowContent (V.InactivatedMutBorrow bid) ->
               (* First activate the borrow *)
@@ -715,12 +715,12 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
   | V.Borrow bc -> (
       (* We can only copy shared borrows *)
       match bc with
-      | SharedBorrow bid ->
+      | SharedBorrow (mv, bid) ->
           (* We need to create a new borrow id for the copied borrow, and
            * update the context accordingly *)
           let bid' = C.fresh_borrow_id () in
           let ctx = reborrow_shared bid bid' ctx in
-          (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
+          (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) })
       | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow"
       | V.InactivatedMutBorrow _ ->
           failwith "Can't copy an inactivated mut borrow")
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 946bacea..76b7d6ae 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -56,7 +56,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
                   bv ref_ty
               in
               (bid, asb)
-          | V.SharedBorrow bid, T.Shared ->
+          | V.SharedBorrow (_, bid), T.Shared ->
               (* Lookup the shared value *)
               let ek = ek_all in
               let sv = lookup_loan ek bid ctx in
@@ -172,7 +172,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
                       fresh_reborrow regions ancestors_regions bv ref_ty
                   in
                   V.AMutBorrow (mv, bid, bv)
-              | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid
+              | V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid
               | V.InactivatedMutBorrow _, _ ->
                   failwith
                     "Can't apply a proj_borrow over an inactivated mutable \
@@ -197,7 +197,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
                   in
                   (* Return *)
                   V.AIgnoredMutBorrow (opt_bid, bv)
-              | V.SharedBorrow bid, T.Shared ->
+              | V.SharedBorrow (_, bid), T.Shared ->
                   (* Lookup the shared value *)
                   let ek = ek_all in
                   let sv = lookup_loan ek bid ctx in
@@ -370,7 +370,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
     match v.V.value with
     | V.Borrow lc -> (
         match lc with
-        | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None
+        | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ -> None
         | V.MutBorrow (id, _) -> Some id)
     | _ -> None
   in
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 6ebd3375..ee58a1a3 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -242,7 +242,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
         (* Register the loan *)
         let _ =
           match bc with
-          | V.SharedBorrow bid -> register_borrow Shared bid
+          | V.SharedBorrow (_, bid) -> register_borrow Shared bid
           | V.MutBorrow (bid, _) -> register_borrow Mut bid
           | V.InactivatedMutBorrow bid -> register_borrow Inactivated bid
         in
@@ -451,8 +451,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.Bottom, _ -> (* Nothing to check *) ()
         | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
             match (bc, rkind) with
-            | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut
-              -> (
+            | V.SharedBorrow (_, bid), T.Shared
+            | V.InactivatedMutBorrow bid, T.Mut -> (
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan ek_all bid ctx in
                 match glc with
diff --git a/src/Print.ml b/src/Print.ml
index cefa3ea5..da6158b5 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -278,7 +278,7 @@ module Values = struct
   and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
       string =
     match bc with
-    | SharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
+    | SharedBorrow (_, bid) -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
     | MutBorrow (bid, tv) ->
         "&mut@" ^ V.BorrowId.to_string bid ^ " ("
         ^ typed_value_to_string fmt tv
diff --git a/src/Values.ml b/src/Values.ml
index 90250c63..57d188da 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -131,7 +131,17 @@ and adt_value = {
 }
 
 and borrow_content =
-  | SharedBorrow of (BorrowId.id[@opaque])  (** A shared value *)
+  | SharedBorrow of mvalue * (BorrowId.id[@opaque])
+      (** A shared borrow.
+      
+          We remember the shared value which was borrowed as a meta value.
+          This is necessary for synthesis: upon translating to "pure" values,
+          we can't perform any lookup because we don't have an environment
+          anymore. Note that it is ok to keep the shared value and copy
+          the shared value this way, because shared values are immutable
+          for as long as they are shared (i.e., as long as we can use the
+          shared borrow).
+       *)
   | MutBorrow of (BorrowId.id[@opaque]) * typed_value
       (** A mutably borrowed value. *)
   | InactivatedMutBorrow of (BorrowId.id[@opaque])
@@ -168,12 +178,23 @@ and loan_content =
           borrows, and extremely useful when giving shared values to abstractions).
        *)
 
+and mvalue = typed_value
+(** "Meta"-value: information we store for the synthesis.
+
+     Note that we never automatically visit the meta-values with the
+     visitors: they really are meta information, and shouldn't be considered
+     as part of the environment during a symbolic execution.
+     
+     TODO: we may want to create wrappers, to prevent accidently mixing meta
+     values and regular values.
+ *)
+
 and typed_value = { value : value; ty : ety }
 [@@deriving
   show,
     visitors
       {
-        name = "iter_typed_value";
+        name = "iter_typed_value_visit_mvalue";
         variety = "iter";
         ancestors = [ "iter_typed_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -181,7 +202,7 @@ and typed_value = { value : value; ty : ety }
       },
     visitors
       {
-        name = "map_typed_value";
+        name = "map_typed_value_visit_mvalue";
         variety = "map";
         ancestors = [ "map_typed_value_base" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -189,16 +210,21 @@ and typed_value = { value : value; ty : ety }
       }]
 (** "Regular" typed value (we map variables to typed values) *)
 
-type mvalue = typed_value [@@deriving show]
-(** "Meta"-value: information we store for the synthesis.
+(** We have to override the [visit_mvalue] method, to ignore meta-values *)
+class ['self] iter_typed_value =
+  object (_self : 'self)
+    inherit [_] iter_typed_value_visit_mvalue
 
-     Note that we never automatically visit the meta-values with the
-     visitors: they really are meta information, and shouldn't be considered
-     as part of the environment during a symbolic execution.
-     
-     TODO: we may want to create wrappers, to prevent mixing meta values
-     and regular values.
- *)
+    method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
+  end
+
+(** We have to override the [visit_mvalue] method, to ignore meta-values *)
+class ['self] map_typed_value =
+  object (_self : 'self)
+    inherit [_] map_typed_value_visit_mvalue
+
+    method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
+  end
 
 type msymbolic_value = symbolic_value [@@deriving show]
 (** "Meta"-symbolic value.
@@ -238,8 +264,6 @@ class ['self] iter_aproj_base =
 
     method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
 
-    method visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
-
     method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
       fun _ _ -> ()
   end
@@ -251,8 +275,6 @@ class ['self] map_aproj_base =
 
     method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
 
-    method visit_mvalue : 'env -> mvalue -> mvalue = fun _ v -> v
-
     method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
       fun _ m -> m
   end