Rewrite copy_value

1 files changed, 144 insertions, 31 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ca011bf0..24b10fff 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -90,6 +90,23 @@ let borrows_in_value (v : V.typed_value) : bool =
     false
   with Found -> true
 
+(** Check a predicate on all the loans in a value - TODO: remove? *)
+let forall_borrows_in_value (pred : V.borrow_content -> bool)
+    (v : V.typed_value) : bool =
+  let obj =
+    object
+      inherit [_] V.iter_typed_value as super
+
+      method! visit_borrow_content env lc =
+        if not (pred lc) then raise Found else super#visit_borrow_content env lc
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    true
+  with Found -> false
+
 (** Check if a value contains inactivated mutable borrows *)
 let inactivated_in_value (v : V.typed_value) : bool =
   let obj =
@@ -120,6 +137,43 @@ let loans_in_value (v : V.typed_value) : bool =
     false
   with Found -> true
 
+(** Check a predicate on all the loans in a value - TODO: remove?*)
+let forall_loans_in_value (pred : V.loan_content -> bool) (v : V.typed_value) :
+    bool =
+  let obj =
+    object
+      inherit [_] V.iter_typed_value as super
+
+      method! visit_loan_content env lc =
+        if not (pred lc) then raise Found else super#visit_loan_content env lc
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    true
+  with Found -> false
+
+(** Return true if there are mutable borrows/loans or inactivated mut borrows
+    in the value - TODO: remove? *)
+let mut_inactivated_borrows_loans_in_value (v : V.typed_value) : bool =
+  let obj =
+    object
+      inherit [_] V.iter_typed_value
+
+      method! visit_MutLoan _ _ = raise Found
+
+      method! visit_MutBorrow _ _ = raise Found
+
+      method! visit_InactivatedMutBorrow _ _ = raise Found
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_typed_value () v;
+    false
+  with Found -> true
+
 (** Lookup a loan content.
 
     The loan is referred to by a borrow id.
@@ -1488,37 +1542,96 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
  *)
 let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) :
     C.eval_ctx * V.typed_value =
-  match v.V.value with
-  | V.Concrete _ -> (ctx, v)
-  | V.Adt av ->
-      (* Sanity check *)
-      (match v.V.ty with
-      | T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value"
-      | T.Adt ((T.AdtId _ | T.Tuple), _, _) -> () (* Ok *)
-      | _ -> failwith "Unreachable");
-      let ctx, fields =
-        List.fold_left_map (copy_value config) ctx av.field_values
-      in
-      (ctx, { v with V.value = V.Adt { av with field_values = fields } })
-  | V.Bottom -> failwith "Can't copy ⊥"
-  | V.Borrow bc -> (
-      (* We can only copy shared borrows *)
-      match bc with
-      | SharedBorrow bid ->
-          let ctx, bid' = C.fresh_borrow_id ctx in
-          let ctx = reborrow_shared config bid bid' ctx in
-          (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
-      | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow"
-      | V.InactivatedMutBorrow _ ->
-          failwith "Can't copy an inactivated mut borrow")
-  | V.Loan lc -> (
-      (* We can only copy shared loans *)
-      match lc with
-      | V.MutLoan _ -> failwith "Can't copy a mutable loan"
-      | V.SharedLoan (_, sv) -> copy_value config ctx sv)
-  | V.Symbolic _sp ->
-      (* TODO: check that the value is copyable *)
-      raise Unimplemented
+  (* Check that there are no inactivated/mutable borrows/loans in the value *)
+  assert (not (mut_inactivated_borrows_loans_in_value v));
+  (* No bottom *)
+  assert (not (bottom_in_value v));
+
+  (* We may need to update the context (to duplicated shared borrows) *)
+  let ctx_r = ref ctx in
+
+  let obj =
+    object
+      inherit [_] V.map_typed_value as super
+
+      method! visit_Bottom _ = failwith "Can't copy ⊥"
+
+      method! visit_ety env ty =
+        (* Sanity check: *)
+        (match ty with
+        | T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value"
+        | _ -> () (* Ok *));
+        (* Ok: continue *)
+        super#visit_ety env ty
+
+      method! visit_borrow_content env bc =
+        (* We can only copy shared borrows *)
+        match bc with
+        | SharedBorrow bid ->
+            (* We need to create a new borrow id for the copied borrow, and
+             * update the context accordingly *)
+            let ctx, bid' = C.fresh_borrow_id !ctx_r in
+            let ctx = reborrow_shared config bid bid' ctx in
+            ctx_r := ctx;
+            SharedBorrow bid'
+        | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow"
+        | V.InactivatedMutBorrow _ ->
+            failwith "Can't copy an inactivated mut borrow"
+
+      method! visit_Loan env lc =
+        (* We can only copy shared loans *)
+        match lc with
+        | V.MutLoan _ -> failwith "Can't copy a mutable loan"
+        | V.SharedLoan (_, sv) ->
+            (* We don't copy the shared loan: only the shared value inside *)
+            let v : V.typed_value = super#visit_typed_value env sv in
+            v.V.value
+
+      method! visit_Symbolic _ _ =
+        (* TODO: check that the value is copyable *)
+        raise Unimplemented
+    end
+  in
+
+  (* Copy and update the context at the same time *)
+  let copied = obj#visit_typed_value () v in
+  (!ctx_r, copied)
+
+(* match v.V.value with
+      | V.Concrete _ -> (ctx, v)
+      | V.Adt av ->
+          (* Sanity check *)
+          (match v.V.ty with
+          | T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value"
+          | T.Adt ((T.AdtId _ | T.Tuple), _, _) -> () (* Ok *)
+          | _ -> failwith "Unreachable");
+          let ctx, fields =
+            List.fold_left_map (copy_value config) ctx av.field_values
+          in
+          (ctx, { v with V.value = V.Adt { av with field_values = fields } })
+      | V.Bottom -> failwith "Can't copy ⊥"
+      | V.Borrow bc -> (
+          (* We can only copy shared borrows *)
+          match bc with
+          | SharedBorrow bid ->
+               (* We need to create a new borrow id for the copied borrow, and
+                * update the context accordingly *)
+              let ctx, bid' = C.fresh_borrow_id ctx in
+              let ctx = reborrow_shared config bid bid' ctx in
+              (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
+          | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow"
+          | V.InactivatedMutBorrow _ ->
+              failwith "Can't copy an inactivated mut borrow")
+      | V.Loan lc -> (
+          (* We can only copy shared loans *)
+          match lc with
+          | V.MutLoan _ -> failwith "Can't copy a mutable loan"
+          | V.SharedLoan (_, sv) ->
+   (* We don't copy the shared loan: only the shared value inside *)
+            copy_value config ctx sv)
+      | V.Symbolic _sp ->
+          (* TODO: check that the value is copyable *)
+          raise Unimplemented*)
 
 (** Convert a constant operand value to a typed value *)
 let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)