diff options
| -rw-r--r-- | src/Interpreter.ml | 85 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
2 files changed, 33 insertions, 54 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 8948701f..0480990b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -758,37 +758,6 @@ let end_borrow_get_borrow_in_env (io : inner_outer) Ok (env, !replaced_bc) with FoundOuter outers -> Error outers -(** See [give_back_value]. *) -let rec give_back_value_to_value config bid (v : V.typed_value) - (destv : V.typed_value) : V.typed_value = - match destv.V.value with - | V.Concrete _ | V.Bottom | V.Symbolic _ -> destv - | V.Adt av -> - let field_values = - List.map (give_back_value_to_value config bid v) av.field_values - in - { destv with value = Adt { av with field_values } } - | V.Borrow bc -> - (* We may need to insert the value inside a borrowed value *) - let bc' = - match bc with - | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> bc - | V.MutBorrow (bid', destv') -> - MutBorrow (bid', give_back_value_to_value config bid v destv') - in - { destv with value = V.Borrow bc' } - | V.Loan lc -> ( - match lc with - | V.SharedLoan (_, _) -> destv - | V.MutLoan bid' -> - if bid' = bid then v - else { destv with value = V.Loan (V.MutLoan bid') }) - -(** See [give_back_value]. *) -let give_back_value_to_abs (_config : C.config) _bid _v _abs : V.abs = - (* TODO *) - raise Unimplemented - (** See [give_back_shared]. *) let rec give_back_shared_to_value (config : C.config) bid (destv : V.typed_value) : V.typed_value = @@ -845,29 +814,39 @@ let give_back_shared_to_abs _config _bid _abs : V.abs = be independently done before. *) let give_back_value (config : C.config) (bid : V.BorrowId.id) - (v : V.typed_value) (env : C.env) : C.env = - (* TODO: - (* We use a reference to check that we updated exactly one borrow *) - let replaced : bool ref = ref false in - let set_replaced () = - assert (not !replaced); - replaced := true - in - let obj = - object - inherit [_] C.map_env - end - in*) - let give_back_value_to_env_elem ev : C.env_elem = - match ev with - | C.Var (vid, destv) -> - C.Var (vid, give_back_value_to_value config bid v destv) - | C.Abs abs -> - assert (config.mode = SymbolicMode); - C.Abs (give_back_value_to_abs config bid v abs) - | C.Frame -> C.Frame + (nv : V.typed_value) (env : C.env) : C.env = + (* We use a reference to check that we updated exactly one borrow *) + let replaced : bool ref = ref false in + let set_replaced () = + assert (not !replaced); + replaced := true + in + let obj = + object + inherit [_] C.map_env as super + + method! visit_Loan env lc = + match lc with + | V.SharedLoan (bids, v) -> + (* We are giving back a value (i.e., the content of a *mutable* + * borrow): nothing special to do *) + V.Loan (super#visit_SharedLoan env bids v) + | V.MutLoan bid' -> + (* Check if this is the loan we are looking for *) + if bid' = bid then ( + set_replaced (); + nv.V.value) + else V.Loan (super#visit_MutLoan env bid') + + method! visit_ALoan env lc = raise Unimplemented + end in - List.map give_back_value_to_env_elem env + + let env = obj#visit_env () env in + (* Check we gave back to exactly one loan *) + assert !replaced; + (* Return *) + env (** Auxiliary function to end borrows. diff --git a/src/Values.ml b/src/Values.ml index 38193068..e0b0b59d 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -243,7 +243,7 @@ and aloan_content = to be seen like a `mut_borrow ... (mut_borrow ...)`. TODO: be more precise about the ignored borrows (keep track of the borrow - ids) + ids)? *) and aborrow_content = | AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue |