From 77f66621eca3864b1f2c304d71e0abd386c6aa4b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 24 Nov 2021 11:28:48 +0100 Subject: Implement a general access_projection function --- src/Interpreter.ml | 257 +++++++++++++++++++++++++++++++---------------------- 1 file changed, 151 insertions(+), 106 deletions(-) diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 7582735d..66a8fbd1 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -777,7 +777,6 @@ let rec activate_inactivated_mut_borrow (config : config) (io : inner_outer) *) promote_inactivated_borrow_to_mut_borrow l borrowed_value env2) -(* (** Paths *) type access_kind = @@ -786,8 +785,8 @@ type access_kind = | Move (** Don't enter borrows or loans *) (** When we fail reading from or writing to a path, it might be because we - ** need to update the environment by ending borrows, expanding symbolic - ** values, etc. *) + need to update the environment by ending borrows, expanding symbolic + values, etc. The following type is used to convey this information. *) type path_fail_kind = | FailSharedLoan of BorrowId.Set.t (** Failure because we couldn't go inside a shared loan *) @@ -804,6 +803,8 @@ type path_fail_kind = were remaining in the path when we reached the error - this allows to properly update the Bottom value, if needs be. *) + | FailBorrow of borrow_content + (** We got stuck because we couldn't enter a borrow *) (** Result of evaluating a path (reading from a path/writing to a path) @@ -813,7 +814,7 @@ type path_fail_kind = type 'a path_access_result = ('a, path_fail_kind) result (** The result of reading from/writing to a place *) -(** Return the shared value referenced by a borrow id *) +(*(** Return the shared value referenced by a borrow id *) let lookup_shared_value_from_borrow_id (bid : BorrowId.id) (env : env) : typed_value = let rec lookup_in_value (v : typed_value) : typed_value option = @@ -845,118 +846,162 @@ let lookup_shared_value_from_borrow_id (bid : BorrowId.id) (env : env) : in match List.find_map lookup_in_env_value env with | None -> failwith "Unreachable" - | Some v -> v + | Some v -> v*) type updated_read_value = { read : typed_value; updated : typed_value } -(* +type projection_access = { + enter_shared_loans : bool; + enter_mut_borrows : bool; + lookup_shared_borrows : bool; +} + (** Generic function to access (read/write) the value at the end of a projection. - We return the eventually updated value, and the value we read at the end of - the place. + We return the (eventually) updated value, the value we read at the end of + the place and the (eventually) updated environment. *) -let rec access_projection (config : config) (access : access_kind) (env : env) +let rec access_projection (access : projection_access) (env : env) (* Function to (eventually) update the value we find *) (update : typed_value -> typed_value) (p : projection) (v : typed_value) : - updated_read_value path_access_result = + (env * updated_read_value) path_access_result = + (* For looking up/updating shared loans *) + let ek : exploration_kind = + { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } + in match p with - | [] -> Ok { read = v; updated = update v } + | [] -> Ok (env, { read = v; updated = update v }) | pe :: p' -> ( - (* The projection is non-empty: we need to enter all the loans we find, - * if we are allowed to do so *) - let rec enter_loans (v : typed_value) : typed_value path_access_result = - match v.value with - | Loan lc -> ( - match (access, lc) with - (* We can enter shared loans only if we are in "read" mode *) - | Read, SharedLoan (_, sv) -> enter_loans sv - | (Write | Move), SharedLoan (bids, _) -> - Error (FailSharedLoan bids) - (* We always have to end mutable loans *) - | _, MutLoan bid -> Error (FailMutLoan bid)) - | _ -> Ok v - in - (* Enter inside the loans and match on the resulting value *) - match enter_loans v with - | Ok v -> ( - (* Match on the projection element and the value *) - match (pe, v.value) with - (* Field projection *) - | Field (ProjAdt (_def_id, opt_variant_id), field_id), Adt adt -> ( - (* Check that the projection is consistent with the current value *) - (match (opt_variant_id, adt.variant_id) with - | None, None -> () - | Some vid, Some vid' -> - if vid <> vid' then failwith "Unreachable" - | _ -> failwith "Unreachable"); - (* Actually project *) - let fv = FieldId.nth adt.field_values field_id in - match access_projection config access env p fv with - | Error err -> Error err - | Ok res -> - (* Update the field value *) - let nvalues = - FieldId.update_nth adt.field_values field_id res.updated - in - let nadt = Adt { adt with field_values = nvalues } in - let updated = { v with value = nadt } in - Ok { res with updated }) - (* Tuples *) - | Field (ProjTuple _, field_id), Tuple values -> ( - let fv = FieldId.nth values field_id in - (* Project *) - match access_projection config access env p fv with - | Error err -> Error err - | Ok res -> - (* Update the field value *) - let nvalues = - FieldId.update_nth values field_id res.updated - in - let ntuple = Tuple nvalues in - let updated = { v with value = ntuple } in - Ok { res with updated }) - (* We can expand [Bottom] values only while *writing* to places *) - | _, Bottom -> failwith "Unreachable" - (* Symbolic value: needs to be expanded *) - | _, Symbolic sp -> - assert (config.mode = SymbolicMode); - (* Expand the symbolic value *) - Error (FailSymbolic (pe, sp)) - (* Box dereferencement *) - | DerefBox, Assumed (Box bv) -> ( - (* We allow moving inside of boxes *) - match access_projection config access env p' bv with - | Error err -> err - | Ok res -> - let nv = { v with value = Assumed (Box res.updated) } in - { res with updated = nv }) - (* Borrow dereferencement *) - | Deref, Borrow bc -> ( - match (access, bc) with - | Read, SharedBorrow bid -> - let sv = lookup_shared_value_from_borrow_id bid env in - (match access_projection config access env p' sv with - | Error err -> Error err - | Ok res -> - let nv = { v with value = Borrow (SharedBorrow - ) - | Write, SharedBorrow _ -> - failwith "Can't write to a shared borrow" - | (Read | Write), MutBorrow (_, bv) -> - access_projection config access env p' bv - | Move, _ -> failwith "Can't move out of a borrow" - (* We need to activate inactivated mutable borrows *) - | _, InactivatedMutBorrow bid -> - Error (FailInactivatedMutBorrow bid)) - (* Remaining cases: error. We enumerate all the value variants - * on purpose, to make sure we statically catch errors if we - * modify the [value] definition. *) - | _, (Concrete _ | Adt _ | Tuple _ | Assumed _ | Borrow _) -> - failwith "Unreachable") - (* Entering loans failed *) - | res -> res) - *) + (* Match on the projection element and the value *) + match (pe, v.value) with + (* Field projection *) + | Field (ProjAdt (_def_id, opt_variant_id), field_id), Adt adt -> ( + (* Check that the projection is consistent with the current value *) + (match (opt_variant_id, adt.variant_id) with + | None, None -> () + | Some vid, Some vid' -> if vid <> vid' then failwith "Unreachable" + | _ -> failwith "Unreachable"); + (* Actually project *) + let fv = FieldId.nth adt.field_values field_id in + match access_projection access env update p fv with + | Error err -> Error err + | Ok (env1, res) -> + (* Update the field value *) + let nvalues = + FieldId.update_nth adt.field_values field_id res.updated + in + let nadt = Adt { adt with field_values = nvalues } in + let updated = { v with value = nadt } in + Ok (env1, { res with updated })) + (* Tuples *) + | Field (ProjTuple arity, field_id), Tuple values -> ( + assert (arity = FieldId.length values); + let fv = FieldId.nth values field_id in + (* Project *) + match access_projection access env update p fv with + | Error err -> Error err + | Ok (env1, res) -> + (* Update the field value *) + let nvalues = FieldId.update_nth values field_id res.updated in + let ntuple = Tuple nvalues in + let updated = { v with value = ntuple } in + Ok (env1, { res with updated }) + (* If we reach Bottom, it may mean we need to expand an uninitialized + * enumeration value *)) + | Field (ProjAdt (_, Some _variant_id), _), Bottom -> + Error (FailBottom (1 + List.length p', pe, v.ty)) + (* Symbolic value: needs to be expanded *) + | _, Symbolic sp -> + (* Expand the symbolic value *) + Error (FailSymbolic (pe, sp)) + (* Box dereferencement *) + | DerefBox, Assumed (Box bv) -> ( + (* We allow moving inside of boxes *) + match access_projection access env update p' bv with + | Error err -> Error err + | Ok (env1, res) -> + let nv = { v with value = Assumed (Box res.updated) } in + Ok (env1, { res with updated = nv })) + (* Borrows *) + | Deref, Borrow bc -> ( + match bc with + | SharedBorrow bid -> + (* Lookup the loan content, and explore from there *) + if access.lookup_shared_borrows then + match lookup_loan ek bid env with + | MutLoan _ -> failwith "Expected a shared loan" + | SharedLoan (bids, sv) -> ( + (* Explore the shared value *) + match access_projection access env update p' sv with + | Error err -> Error err + | Ok (env1, res) -> + (* Update the shared loan with the new value returned + by [access_projection] *) + let env2 = + update_loan ek bid + (SharedLoan (bids, res.updated)) + env1 + in + (* Return - note that we don't need to update the borrow itself *) + Ok (env2, { res with updated = v })) + else Error (FailBorrow bc) + | InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid) + | MutBorrow (bid, bv) -> + if access.enter_mut_borrows then + match access_projection access env update p' bv with + | Error err -> Error err + | Ok (env1, res) -> + let nv = + { v with value = Borrow (MutBorrow (bid, res.updated)) } + in + Ok (env1, { res with updated = nv }) + else Error (FailBorrow bc)) + | _, Loan lc -> ( + match lc with + | MutLoan bid -> Error (FailMutLoan bid) + | SharedLoan (bids, sv) -> + (* If we can enter shared loan, we ignore the loan. Pay attention + to the fact that we need to reexplore the *whole* place (i.e, + we mustn't ignore the current projection element *) + if access.enter_shared_loans then + match access_projection access env update (pe :: p') sv with + | Error err -> Error err + | Ok (env1, res) -> + let nv = + { v with value = Loan (SharedLoan (bids, res.updated)) } + in + Ok (env1, { res with updated = nv }) + else Error (FailSharedLoan bids))) + +(* +(* +TODO: loans + (* Borrow dereferencement *) + | Deref, Borrow bc -> ( + match (access, bc) with + | Read, SharedBorrow bid -> + let sv = lookup_shared_value_from_borrow_id bid env in + (match access_projection config access env p' sv with + | Error err -> Error err + | Ok res -> + let nv = { v with value = Borrow (SharedBorrow + ) + | Write, SharedBorrow _ -> + failwith "Can't write to a shared borrow" + | (Read | Write), MutBorrow (_, bv) -> + access_projection config access env p' bv + | Move, _ -> failwith "Can't move out of a borrow" + (* We need to activate inactivated mutable borrows *) + | _, InactivatedMutBorrow bid -> + Error (FailInactivatedMutBorrow bid)) + (* Remaining cases: error. We enumerate all the value variants + * on purpose, to make sure we statically catch errors if we + * modify the [value] definition. *) + | _, (Concrete _ | Adt _ | Tuple _ | Assumed _ | Borrow _) -> + failwith "Unreachable" + *) +(* (** Read the value at the end of a projection. *) let rec read_projection (config : config) (access : access_kind) (env : env) (p : projection) (v : typed_value) : @@ -1028,7 +1073,7 @@ let rec read_projection (config : config) (access : access_kind) (env : env) | _, (Concrete _ | Adt _ | Tuple _ | Assumed _ | Borrow _ | Loan _) -> failwith "Unreachable") (* Entering loans failed *) - | res -> res) + | res -> res)*) (** Read the value at the end of a place *) let read_place (config : config) (access : access_kind) (p : place) (env0 : env) -- cgit v1.2.3