diff options
| -rw-r--r-- | src/Interpreter.ml | 175 |
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) |