From 8e6308dc4017d2a2a0f9b48edcac4d0f40d8e1a9 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 8 Dec 2021 15:24:47 +0100 Subject: Revert the implementation of copy_value --- src/Interpreter.ml | 129 ++++++++++++++++------------------------------------- 1 file changed, 39 insertions(+), 90 deletions(-) (limited to 'src') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 24b10fff..1af050c9 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1542,96 +1542,45 @@ 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 = - (* 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*) + (* Remark: at some point we rewrote this function to use iterators, but then + * we reverted the changes: the result was less clear actually. In particular, + * the fact that we have exhaustive matches below makes very obvious the cases + * in which we need to fail *) + 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) -- cgit v1.2.3