summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml175
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)