diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 816 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 833 |
2 files changed, 834 insertions, 815 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index d8256186..4ca7d58f 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -16,6 +16,7 @@ open InterpreterUtils open InterpreterProjectors open InterpreterBorrows open InterpreterExpansion +open InterpreterPaths (* TODO: check that the value types are correct when evaluating *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere @@ -37,777 +38,6 @@ type eval_error = Panic type 'a eval_result = ('a, eval_error) result -(** Paths *) - -(** 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. The following type is used to convey this information. - - TODO: compare with borrow_lres? -*) -type path_fail_kind = - | FailSharedLoan of V.BorrowId.Set.t - (** Failure because we couldn't go inside a shared loan *) - | FailMutLoan of V.BorrowId.id - (** Failure because we couldn't go inside a mutable loan *) - | FailInactivatedMutBorrow of V.BorrowId.id - (** Failure because we couldn't go inside an inactivated mutable borrow - (which should get activated) *) - | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp) - (** Failure because we need to enter a symbolic value (and thus need to expand it) *) - (* TODO: Remove the parentheses *) - | FailBottom of (int * E.projection_elem * T.ety) - (** Failure because we need to enter an any value - we can expand Bottom - values if they are left values. We return the number of elements which - were remaining in the path when we reached the error - this allows to - properly update the Bottom value, if needs be. - *) - | FailBorrow of V.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) - - Note that when we fail, we return information used to update the - environment, as well as the -*) -type 'a path_access_result = ('a, path_fail_kind) result -(** The result of reading from/writing to a place *) - -type updated_read_value = { read : V.typed_value; updated : V.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, the value we read at the end of - the place and the (eventually) updated environment. - - TODO: use exceptions? - *) -let rec access_projection (access : projection_access) (ctx : C.eval_ctx) - (* Function to (eventually) update the value we find *) - (update : V.typed_value -> V.typed_value) (p : E.projection) - (v : V.typed_value) : (C.eval_ctx * 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 - | [] -> - let nv = update v in - (* Type checking *) - if nv.ty <> v.ty then ( - L.log#lerror - (lazy - ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: " - ^ T.show_ety v.ty)); - failwith - "Assertion failed: new value doesn't have the same type as its \ - destination"); - Ok (ctx, { read = v; updated = nv }) - | pe :: p' -> ( - (* Match on the projection element and the value *) - match (pe, v.V.value, v.V.ty) with - (* Field projection - ADTs *) - | ( Field (ProjAdt (def_id, opt_variant_id), field_id), - V.Adt adt, - T.Adt (T.AdtId def_id', _, _) ) -> ( - assert (def_id = def_id'); - (* 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 = T.FieldId.nth adt.field_values field_id in - match access_projection access ctx update p' fv with - | Error err -> Error err - | Ok (ctx, res) -> - (* Update the field value *) - let nvalues = - T.FieldId.update_nth adt.field_values field_id res.updated - in - let nadt = V.Adt { adt with V.field_values = nvalues } in - let updated = { v with value = nadt } in - Ok (ctx, { res with updated })) - (* Tuples *) - | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> ( - assert (arity = List.length adt.field_values); - let fv = T.FieldId.nth adt.field_values field_id in - (* Project *) - match access_projection access ctx update p' fv with - | Error err -> Error err - | Ok (ctx, res) -> - (* Update the field value *) - let nvalues = - T.FieldId.update_nth adt.field_values field_id res.updated - in - let ntuple = V.Adt { adt with field_values = nvalues } in - let updated = { v with value = ntuple } in - Ok (ctx, { res with updated }) - (* If we reach Bottom, it may mean we need to expand an uninitialized - * enumeration value *)) - | Field (ProjAdt (_, _), _), V.Bottom, _ -> - Error (FailBottom (1 + List.length p', pe, v.ty)) - | Field (ProjTuple _, _), V.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, - Adt { variant_id = None; field_values = [ bv ] }, - T.Adt (T.Assumed T.Box, _, _) ) -> ( - (* We allow moving inside of boxes. In practice, this kind of - * manipulations should happen only inside unsage code, so - * it shouldn't happen due to user code, and we leverage it - * when implementing box dereferencement for the concrete - * interpreter *) - match access_projection access ctx update p' bv with - | Error err -> Error err - | Ok (ctx, res) -> - let nv = - { - v with - value = - V.Adt { variant_id = None; field_values = [ res.updated ] }; - } - in - Ok (ctx, { res with updated = nv })) - (* Borrows *) - | Deref, V.Borrow bc, _ -> ( - match bc with - | V.SharedBorrow bid -> - (* Lookup the loan content, and explore from there *) - if access.lookup_shared_borrows then - match lookup_loan ek bid ctx with - | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan" - | _, Concrete (V.SharedLoan (bids, sv)) -> ( - (* Explore the shared value *) - match access_projection access ctx update p' sv with - | Error err -> Error err - | Ok (ctx, res) -> - (* Update the shared loan with the new value returned - by [access_projection] *) - let ctx = - update_loan ek bid - (V.SharedLoan (bids, res.updated)) - ctx - in - (* Return - note that we don't need to update the borrow itself *) - Ok (ctx, { res with updated = v })) - | ( _, - Abstract - ( V.AMutLoan (_, _) - | V.AEndedMutLoan { given_back = _; child = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan { given_back = _; child = _ } - | V.AIgnoredSharedLoan _ ) ) -> - failwith "Expected a shared (abstraction) loan" - | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> ( - (* Explore the shared value *) - match access_projection access ctx update p' sv with - | Error err -> Error err - | Ok (ctx, res) -> - (* Relookup the child avalue *) - let av = - match lookup_loan ek bid ctx with - | _, Abstract (V.ASharedLoan (_, _, av)) -> av - | _ -> failwith "Unexpected" - in - (* Update the shared loan with the new value returned - by [access_projection] *) - let ctx = - update_aloan ek bid - (V.ASharedLoan (bids, res.updated, av)) - ctx - in - (* Return - note that we don't need to update the borrow itself *) - Ok (ctx, { res with updated = v })) - else Error (FailBorrow bc) - | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid) - | V.MutBorrow (bid, bv) -> - if access.enter_mut_borrows then - match access_projection access ctx update p' bv with - | Error err -> Error err - | Ok (ctx, res) -> - let nv = - { - v with - value = V.Borrow (V.MutBorrow (bid, res.updated)); - } - in - Ok (ctx, { res with updated = nv }) - else Error (FailBorrow bc)) - | _, V.Loan lc, _ -> ( - match lc with - | V.MutLoan bid -> Error (FailMutLoan bid) - | V.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 ctx update (pe :: p') sv with - | Error err -> Error err - | Ok (ctx, res) -> - let nv = - { - v with - value = V.Loan (V.SharedLoan (bids, res.updated)); - } - in - Ok (ctx, { res with updated = nv }) - else Error (FailSharedLoan bids)) - | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r -> - let pe, v, ty = r in - let pe = "- pe: " ^ E.show_projection_elem pe in - let v = "- v:\n" ^ V.show_value v in - let ty = "- ty:\n" ^ T.show_ety ty in - L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); - failwith "Inconsistent projection") - -(** Generic function to access (read/write) the value at a given place. - - We return the value we read at the place and the (eventually) updated - environment, if we managed to access the place, or the precise reason - why we failed. - *) -let access_place (access : projection_access) - (* Function to (eventually) update the value we find *) - (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx) - : (C.eval_ctx * V.typed_value) path_access_result = - (* Lookup the variable's value *) - let value = C.ctx_lookup_var_value ctx p.var_id in - (* Apply the projection *) - match access_projection access ctx update p.projection value with - | Error err -> Error err - | Ok (ctx, res) -> - (* Update the value *) - let ctx = C.ctx_update_var_value ctx p.var_id res.updated in - (* Return *) - Ok (ctx, res.read) - -type access_kind = - | Read (** We can go inside borrows and loans *) - | Write (** Don't enter shared borrows or shared loans *) - | Move (** Don't enter borrows or loans *) - -let access_kind_to_projection_access (access : access_kind) : projection_access - = - match access with - | Read -> - { - enter_shared_loans = true; - enter_mut_borrows = true; - lookup_shared_borrows = true; - } - | Write -> - { - enter_shared_loans = false; - enter_mut_borrows = true; - lookup_shared_borrows = false; - } - | Move -> - { - enter_shared_loans = false; - enter_mut_borrows = false; - lookup_shared_borrows = false; - } - -(** Read the value at a given place *) -let read_place (config : C.config) (access : access_kind) (p : E.place) - (ctx : C.eval_ctx) : V.typed_value path_access_result = - let access = access_kind_to_projection_access access in - (* The update function is the identity *) - let update v = v in - match access_place access update p ctx with - | Error err -> Error err - | Ok (ctx1, read_value) -> - (* Note that we ignore the new environment: it should be the same as the - original one. - *) - if config.check_invariants then - if ctx1 <> ctx then ( - let msg = - "Unexpected environment update:\nNew environment:\n" - ^ C.show_env ctx1.env ^ "\n\nOld environment:\n" - ^ C.show_env ctx.env - in - L.log#serror msg; - failwith "Unexpected environment update"); - Ok read_value - -let read_place_unwrap (config : C.config) (access : access_kind) (p : E.place) - (ctx : C.eval_ctx) : V.typed_value = - match read_place config access p ctx with - | Error _ -> failwith "Unreachable" - | Ok v -> v - -(** Update the value at a given place *) -let write_place (_config : C.config) (access : access_kind) (p : E.place) - (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx path_access_result = - let access = access_kind_to_projection_access access in - (* The update function substitutes the value with the new value *) - let update _ = nv in - match access_place access update p ctx with - | Error err -> Error err - | Ok (ctx, _) -> - (* We ignore the read value *) - Ok ctx - -let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place) - (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = - match write_place config access p nv ctx with - | Error _ -> failwith "Unreachable" - | Ok ctx -> ctx - -(** Compute an expanded ADT bottom value *) -let compute_expanded_bottom_adt_value (tyctx : T.type_def list) - (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) - (regions : T.erased_region list) (types : T.ety list) : V.typed_value = - (* Lookup the definition and check if it is an enumeration - it - should be an enumeration if and only if the projection element - is a field projection with *some* variant id. Retrieve the list - of fields at the same time. *) - let def = T.TypeDefId.nth tyctx def_id in - assert (List.length regions = List.length def.T.region_params); - (* Compute the field types *) - let field_types = - Subst.type_def_get_instantiated_field_etypes def opt_variant_id types - in - (* Initialize the expanded value *) - let fields = - List.map - (fun ty : V.typed_value -> ({ V.value = V.Bottom; ty } : V.typed_value)) - field_types - in - let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in - let ty = T.Adt (T.AdtId def_id, regions, types) in - { V.value = av; V.ty } - -(** Compute an expanded tuple bottom value *) -let compute_expanded_bottom_tuple_value (field_types : T.ety list) : - V.typed_value = - (* Generate the field values *) - let fields = - List.map (fun ty : V.typed_value -> { V.value = Bottom; ty }) field_types - in - let v = V.Adt { variant_id = None; field_values = fields } in - let ty = T.Adt (T.Tuple, [], field_types) in - { V.value = v; V.ty } - -(** Auxiliary helper to expand [Bottom] values. - - During compilation, rustc desaggregates the ADT initializations. The - consequence is that the following rust code: - ``` - let x = Cons a b; - ``` - - Looks like this in MIR: - ``` - (x as Cons).0 = a; - (x as Cons).1 = b; - set_discriminant(x, 0); // If `Cons` is the variant of index 0 - ``` - - The consequence is that we may sometimes need to write fields to values - which are currently [Bottom]. When doing this, we first expand the value - to, say, [Cons Bottom Bottom] (note that field projection contains information - about which variant we should project to, which is why we *can* set the - variant index when writing one of its fields). -*) -let expand_bottom_value_from_projection (config : C.config) - (access : access_kind) (p : E.place) (remaining_pes : int) - (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx = - (* Debugging *) - L.log#ldebug - (lazy - ("expand_bottom_value_from_projection:\n" ^ "pe: " - ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty)); - (* Prepare the update: we need to take the proper prefix of the place - during whose evaluation we got stuck *) - let projection' = - fst - (Utilities.list_split_at p.projection - (List.length p.projection - remaining_pes)) - in - let p' = { p with projection = projection' } in - (* Compute the expanded value. - The type of the [Bottom] value should be a tuple or an ADT. - Note that the projection element we got stuck at should be a - field projection, and gives the variant id if the [Bottom] value - is an enumeration value. - Also, the expanded value should be the proper ADT variant or a tuple - with the proper arity, with all the fields initialized to [Bottom] - *) - let nv = - match (pe, ty) with - (* "Regular" ADTs *) - | ( Field (ProjAdt (def_id, opt_variant_id), _), - T.Adt (T.AdtId def_id', regions, types) ) -> - assert (def_id = def_id'); - compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id - opt_variant_id regions types - (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> - assert (arity = List.length tys); - (* Generate the field values *) - compute_expanded_bottom_tuple_value tys - | _ -> - failwith - ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty) - in - (* Update the context by inserting the expanded value at the proper place *) - match write_place config access p' nv ctx with - | Ok ctx -> ctx - | Error _ -> failwith "Unreachable" - -(** Update the environment to be able to read a place. - - When reading a place, we may be stuck along the way because some value - is borrowed, we reach a symbolic value, etc. In this situation [read_place] - fails while returning precise information about the failure. This function - uses this information to update the environment (by ending borrows, - expanding symbolic values) until we manage to fully read the place. - *) -let rec update_ctx_along_read_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - (* Attempt to read the place: if it fails, update the environment and retry *) - match read_place config access p ctx with - | Ok _ -> ctx - | Error err -> - let ctx = - match err with - | FailSharedLoan bids -> end_outer_borrows config bids ctx - | FailMutLoan bid -> end_outer_borrow config bid ctx - | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config Outer bid ctx - | FailSymbolic (pe, sp) -> - (* Expand the symbolic value *) - expand_symbolic_value_no_branching config pe sp ctx - | FailBottom (_, _, _) -> - (* We can't expand [Bottom] values while reading them *) - failwith "Found [Bottom] while reading a place" - | FailBorrow _ -> failwith "Could not read a borrow" - in - update_ctx_along_read_place config access p ctx - -(** Update the environment to be able to write to a place. - - See [update_env_alond_read_place]. -*) -let rec update_ctx_along_write_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - (* Attempt to *read* (yes, "read": we check the access to the place, and - write to it later) the place: if it fails, update the environment and retry *) - match read_place config access p ctx with - | Ok _ -> ctx - | Error err -> - let ctx = - match err with - | FailSharedLoan bids -> end_outer_borrows config bids ctx - | FailMutLoan bid -> end_outer_borrow config bid ctx - | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config Outer bid ctx - | FailSymbolic (pe, sp) -> - (* Expand the symbolic value *) - expand_symbolic_value_no_branching config pe sp ctx - | FailBottom (remaining_pes, pe, ty) -> - (* Expand the [Bottom] value *) - expand_bottom_value_from_projection config access p remaining_pes pe - ty ctx - | FailBorrow _ -> failwith "Could not write to a borrow" - in - update_ctx_along_write_place config access p ctx - -exception UpdateCtx of C.eval_ctx -(** Small utility used to break control-flow *) - -(** End the loans at a given place: read the value, if it contains a loan, - end this loan, repeat. - - This is used when reading, borrowing, writing to a value. We typically - first call [update_ctx_along_read_place] or [update_ctx_along_write_place] - to get access to the value, then call this function to "prepare" the value: - when moving values, we can't move a value which contains loans and thus need - to end them, etc. - *) -let rec end_loans_at_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - (* Iterator to explore a value and update the context whenever we find - * loans. - * We use exceptions to make it handy: whenever we update the - * context, we raise an exception wrapping the updated context. - * *) - let obj = - object - inherit [_] V.iter_typed_value as super - - method! visit_borrow_content env bc = - match bc with - | V.SharedBorrow _ | V.MutBorrow (_, _) -> - (* Nothing special to do *) super#visit_borrow_content env bc - | V.InactivatedMutBorrow bid -> - (* We need to activate inactivated borrows *) - let ctx = activate_inactivated_mut_borrow config Inner bid ctx in - raise (UpdateCtx ctx) - - method! visit_loan_content env lc = - match lc with - | V.SharedLoan (bids, v) -> ( - (* End the loans if we need a modification access, otherwise dive into - the shared value *) - match access with - | Read -> super#visit_SharedLoan env bids v - | Write | Move -> - let ctx = end_outer_borrows config bids ctx in - raise (UpdateCtx ctx)) - | V.MutLoan bid -> - (* We always need to end mutable borrows *) - let ctx = end_outer_borrow config bid ctx in - raise (UpdateCtx ctx) - end - in - - (* First, retrieve the value *) - match read_place config access p ctx with - | Error _ -> failwith "Unreachable" - | Ok v -> ( - (* Inspect the value and update the context while doing so. - If the context gets updated: perform a recursive call (many things - may have been updated in the context: we need to re-read the value - at place [p] - and this value may actually not be accessible - anymore...) - *) - try - obj#visit_typed_value () v; - (* No context update required: return the current context *) - ctx - with UpdateCtx ctx -> - (* The context was updated: do a recursive call to reinspect the value *) - end_loans_at_place config access p ctx) - -(** Drop (end) all the loans and borrows at a given place, which should be - seen as an l-value (we will write to it later, but need to drop the borrows - before writing). - - We start by only dropping the borrows, then we end the loans. The reason - is that some loan we find may be borrowed by another part of the subvalue. - In order to correctly handle the "outer borrow" priority (we should end - the outer borrows first) which is not really applied here (we are preparing - the value for override: we can end the borrows inside, without ending the - borrows we traversed to actually access the value) we first end the borrows - we find in the place, to make sure all the "local" loans are taken care of. - Then, if we find a loan, it means it is "externally" borrowed (the associated - borrow is not in a subvalue of the place under inspection). - Also note that whenever we end a loan, we might propagate back a value inside - the place under inspection: we must re-end all the borrows we find there, - before reconsidering loans. - - Repeat: - - read the value at a given place - - as long as we find a loan or a borrow, end it - - This is used to drop values (when we need to write to a place, we first - drop the value there to properly propagate back values which are not/can't - be borrowed anymore). - *) -let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Iterator to explore a value and update the context whenever we find - borrows/loans. - We use exceptions to make it handy: whenever we update the - context, we raise an exception wrapping the updated context. - - Note that we can end the borrows which are inside the value (while the - value itself might be inside a borrow/loan: we are thus ending inner - borrows). Because a loan inside the value may be linked to a borrow - somewhere else *also inside* the value (it's possible with adts), - we first end all the borrows we find - by using [Inner] to allow - ending inner borrows - then end all the loans we find. - - It is really important to do this in two steps: the borrow linked to a - loan may be inside the value at place p, in which case this borrow may be - an inner borrow that we *can* end, but it may also be outside this - value, in which case we need to end all the outer borrows first... - Also, whenever the context is updated, we need to re-inspect - the value at place p *in two steps* again (end borrows, then end - loans). - - Example: - ======= - We want to end the borrows/loans at `*x` in the following environment: - ``` - x -> mut_borrow l0 (mut_loan l1, mut_borrow l1 (Int 3), mut_loan l2) - y -> mut_borrow l2 (Bool true) - ``` - - We have to consider two things: - - the borrow `mut_borrow l1 (Int 3)` borrows a subvalue of `*x` - - the borrow corresponding to the loan `mut_loan l2` is outside of `*x` - - We first end all the *borrows* (not the loans) inside of `*x`, which gives: - ``` - x -> mut_borrow l0 (Int 3, ⊥, mut_loan l2) - y -> mut_borrow l2 (Bool true) - ``` - - Note that when ending the borrows, we can (and have to) ignore the outer - borrows (in this case `mut_borrow l0 ...`). Otherwise, we would have to end - the borrow `l0` which is incorrect (note that we might have to drop the - borrows/loans at `*x` if we evaluate, for instance, `*x = ...`). - It is ok to ignore outer borrows in this case because whenever - we end a borrow, it is an outer borrow locally to `*x` (i.e., we ignore - the outer borrows when accessing `*x`, but once examining the value at - `*x` we never dive into borrows: whenever we find one, we end it - it is thus - an outer borrow, in some way). - - Then, we end the loans at `*x`. Note that as at this point `*x` doesn't - contain borrows (only loans), the borrows corresponding to those loans - are thus necessarily outside of `*x`: we mustn't ignore outer borrows this - time. This gives: - ``` - x -> mut_borrow l0 (Int 3, ⊥, Bool true) - y -> ⊥ - ``` - *) - let obj = - object - inherit [_] V.iter_typed_value as super - - method! visit_borrow_content end_loans bc = - (* Sanity check: we should have ended all the borrows before starting - to end loans *) - assert (not end_loans); - - (* We need to end all borrows. Note that we ignore the outer borrows - when ending the borrows we find here (we call [end_inner_borrow(s)]: - the value at place p might be below a borrow/loan). Note however - that if we restrain ourselves at the value at place p, the borrow we - found here can be considered as an outer borrow. - *) - match bc with - | V.SharedBorrow bid | V.MutBorrow (bid, _) -> - raise (UpdateCtx (end_inner_borrow config bid ctx)) - | V.InactivatedMutBorrow bid -> - (* We need to activate ithe nactivated borrow - later, we will - * actually end it - Rk.: we could actually end it straight away - * (this is not really important) *) - let ctx = activate_inactivated_mut_borrow config Inner bid ctx in - raise (UpdateCtx ctx) - - method! visit_loan_content end_loans lc = - if - (* If we can, end the loans, otherwise ignore: keep for later *) - end_loans - then - (* We need to end all loans. Note that as all the borrows inside - the value at place p should already have ended, the borrows - associated to the loans we find here should be borrows from - outside this value: we need to call [end_outer_borrow(s)] - (we can't ignore outer borrows this time). - *) - match lc with - | V.SharedLoan (bids, _) -> - raise (UpdateCtx (end_outer_borrows config bids ctx)) - | V.MutLoan bid -> raise (UpdateCtx (end_outer_borrow config bid ctx)) - else super#visit_loan_content end_loans lc - end - in - - (* We do something similar to [end_loans_at_place]. - First, retrieve the value *) - match read_place config Write p ctx with - | Error _ -> failwith "Unreachable" - | Ok v -> ( - (* Inspect the value and update the context while doing so. - If the context gets updated: perform a recursive call (many things - may have been updated in the context: first we need to retrieve the - proper updated value - and this value may actually not be accessible - anymore - *) - try - (* Inspect the value: end the borrows only *) - obj#visit_typed_value false v; - (* Inspect the value: end the loans *) - obj#visit_typed_value true v; - (* No context update required: return the current context *) - ctx - with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx) - -(** Copy a value, and return the resulting value. - - Note that copying values might update the context. For instance, when - copying shared borrows, we need to insert new shared borrows in the context. - - Also, this function is actually more general than it should be: it can be used - to copy concrete ADT values, while ADT copy should be done through the Copy - trait (i.e., by calling a dedicated function). This is why we added a parameter - to control this copy. Note that here by ADT we mean the user-defined ADTs - (not tuples or assumed types). - *) -let rec copy_value (allow_adt_copy : bool) (config : C.config) - (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value = - (* 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 _, _, _) -> assert allow_adt_copy - | T.Adt (T.Tuple, _, _) -> () (* Ok *) - | _ -> failwith "Unreachable"); - let ctx, fields = - List.fold_left_map - (copy_value allow_adt_copy 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 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 allow_adt_copy config ctx sv) - | V.Symbolic sp -> - (* We can copy only if the type is "primitively" copyable. - * Note that in the general case, copy is a trait: copying values - * thus requires calling the proper function. Here, we copy values - * for very simple types such as integers, shared borrows, etc. *) - assert ( - type_is_primitively_copyable (Subst.erase_regions sp.V.svalue.V.sv_ty)); - (* If the type is copyable, we simply return the current value. Side - * remark: what is important to look at when copying symbolic values - * is symbolic expansion. The important subcase is the expansion of shared - * borrows: when doing so, every occurrence of the same symbolic value - * must use a fresh borrow id. *) - (ctx, v) - (** Convert a constant operand value to a typed value *) let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) (cv : E.operand_constant_value) : V.typed_value = @@ -1243,50 +473,6 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : (** Result of evaluating a statement *) type statement_eval_res = Unit | Break of int | Continue of int | Return -(** Small utility. - - Prepare a place which is to be used as the destination of an assignment: - update the environment along the paths, end the borrows and loans at - this place, etc. - - Return the updated context and the (updated) value at the end of the - place. This value should not contain any loan or borrow (and we check - it is the case). Note that it is very likely to contain [Bottom] values. - *) -let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) : - C.eval_ctx * V.typed_value = - (* TODO *) - let access = Write in - let ctx = update_ctx_along_write_place config access p ctx in - (* End the borrows and loans, starting with the borrows *) - let ctx = drop_borrows_loans_at_lplace config p ctx in - (* Read the value and check it *) - let v = read_place_unwrap config access p ctx in - (* Sanity checks *) - assert (not (loans_in_value v)); - assert (not (borrows_in_value v)); - (* Return *) - (ctx, v) - -(** Read the value at a given place. - As long as it is a loan, end the loan. - This function doesn't perform a recursive exploration: - it won't dive into the value to end all the inner - loans (contrary to [drop_borrows_loans_at_lplace] for - instance). - *) -let rec end_loan_exactly_at_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - let v = read_place_unwrap config access p ctx in - match v.V.value with - | V.Loan (V.SharedLoan (bids, _)) -> - let ctx = end_outer_borrows config bids ctx in - end_loan_exactly_at_place config access p ctx - | V.Loan (V.MutLoan bid) -> - let ctx = end_outer_borrow config bid ctx in - end_loan_exactly_at_place config access p ctx - | _ -> ctx - (** Updates the discriminant of a value at a given place. There are two situations: diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml new file mode 100644 index 00000000..7e9fa7dd --- /dev/null +++ b/src/InterpreterPaths.ml @@ -0,0 +1,833 @@ +module T = Types +module V = Values +open Scalars +module E = Expressions +open Errors +module C = Contexts +module Subst = Substitute +module A = CfimAst +module L = Logging +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = Synthesis +open Utils +open InterpreterUtils +open InterpreterProjectors +open InterpreterBorrows +open InterpreterExpansion + +(** Paths *) + +(** 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. The following type is used to convey this information. + + TODO: compare with borrow_lres? +*) +type path_fail_kind = + | FailSharedLoan of V.BorrowId.Set.t + (** Failure because we couldn't go inside a shared loan *) + | FailMutLoan of V.BorrowId.id + (** Failure because we couldn't go inside a mutable loan *) + | FailInactivatedMutBorrow of V.BorrowId.id + (** Failure because we couldn't go inside an inactivated mutable borrow + (which should get activated) *) + | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp) + (** Failure because we need to enter a symbolic value (and thus need to expand it) *) + (* TODO: Remove the parentheses *) + | FailBottom of (int * E.projection_elem * T.ety) + (** Failure because we need to enter an any value - we can expand Bottom + values if they are left values. We return the number of elements which + were remaining in the path when we reached the error - this allows to + properly update the Bottom value, if needs be. + *) + | FailBorrow of V.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) + + Note that when we fail, we return information used to update the + environment, as well as the +*) +type 'a path_access_result = ('a, path_fail_kind) result +(** The result of reading from/writing to a place *) + +type updated_read_value = { read : V.typed_value; updated : V.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, the value we read at the end of + the place and the (eventually) updated environment. + + TODO: use exceptions? + *) +let rec access_projection (access : projection_access) (ctx : C.eval_ctx) + (* Function to (eventually) update the value we find *) + (update : V.typed_value -> V.typed_value) (p : E.projection) + (v : V.typed_value) : (C.eval_ctx * 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 + | [] -> + let nv = update v in + (* Type checking *) + if nv.ty <> v.ty then ( + L.log#lerror + (lazy + ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: " + ^ T.show_ety v.ty)); + failwith + "Assertion failed: new value doesn't have the same type as its \ + destination"); + Ok (ctx, { read = v; updated = nv }) + | pe :: p' -> ( + (* Match on the projection element and the value *) + match (pe, v.V.value, v.V.ty) with + (* Field projection - ADTs *) + | ( Field (ProjAdt (def_id, opt_variant_id), field_id), + V.Adt adt, + T.Adt (T.AdtId def_id', _, _) ) -> ( + assert (def_id = def_id'); + (* 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 = T.FieldId.nth adt.field_values field_id in + match access_projection access ctx update p' fv with + | Error err -> Error err + | Ok (ctx, res) -> + (* Update the field value *) + let nvalues = + T.FieldId.update_nth adt.field_values field_id res.updated + in + let nadt = V.Adt { adt with V.field_values = nvalues } in + let updated = { v with value = nadt } in + Ok (ctx, { res with updated })) + (* Tuples *) + | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> ( + assert (arity = List.length adt.field_values); + let fv = T.FieldId.nth adt.field_values field_id in + (* Project *) + match access_projection access ctx update p' fv with + | Error err -> Error err + | Ok (ctx, res) -> + (* Update the field value *) + let nvalues = + T.FieldId.update_nth adt.field_values field_id res.updated + in + let ntuple = V.Adt { adt with field_values = nvalues } in + let updated = { v with value = ntuple } in + Ok (ctx, { res with updated }) + (* If we reach Bottom, it may mean we need to expand an uninitialized + * enumeration value *)) + | Field (ProjAdt (_, _), _), V.Bottom, _ -> + Error (FailBottom (1 + List.length p', pe, v.ty)) + | Field (ProjTuple _, _), V.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, + Adt { variant_id = None; field_values = [ bv ] }, + T.Adt (T.Assumed T.Box, _, _) ) -> ( + (* We allow moving inside of boxes. In practice, this kind of + * manipulations should happen only inside unsage code, so + * it shouldn't happen due to user code, and we leverage it + * when implementing box dereferencement for the concrete + * interpreter *) + match access_projection access ctx update p' bv with + | Error err -> Error err + | Ok (ctx, res) -> + let nv = + { + v with + value = + V.Adt { variant_id = None; field_values = [ res.updated ] }; + } + in + Ok (ctx, { res with updated = nv })) + (* Borrows *) + | Deref, V.Borrow bc, _ -> ( + match bc with + | V.SharedBorrow bid -> + (* Lookup the loan content, and explore from there *) + if access.lookup_shared_borrows then + match lookup_loan ek bid ctx with + | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan" + | _, Concrete (V.SharedLoan (bids, sv)) -> ( + (* Explore the shared value *) + match access_projection access ctx update p' sv with + | Error err -> Error err + | Ok (ctx, res) -> + (* Update the shared loan with the new value returned + by [access_projection] *) + let ctx = + update_loan ek bid + (V.SharedLoan (bids, res.updated)) + ctx + in + (* Return - note that we don't need to update the borrow itself *) + Ok (ctx, { res with updated = v })) + | ( _, + Abstract + ( V.AMutLoan (_, _) + | V.AEndedMutLoan { given_back = _; child = _ } + | V.AEndedSharedLoan (_, _) + | V.AIgnoredMutLoan (_, _) + | V.AEndedIgnoredMutLoan { given_back = _; child = _ } + | V.AIgnoredSharedLoan _ ) ) -> + failwith "Expected a shared (abstraction) loan" + | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> ( + (* Explore the shared value *) + match access_projection access ctx update p' sv with + | Error err -> Error err + | Ok (ctx, res) -> + (* Relookup the child avalue *) + let av = + match lookup_loan ek bid ctx with + | _, Abstract (V.ASharedLoan (_, _, av)) -> av + | _ -> failwith "Unexpected" + in + (* Update the shared loan with the new value returned + by [access_projection] *) + let ctx = + update_aloan ek bid + (V.ASharedLoan (bids, res.updated, av)) + ctx + in + (* Return - note that we don't need to update the borrow itself *) + Ok (ctx, { res with updated = v })) + else Error (FailBorrow bc) + | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid) + | V.MutBorrow (bid, bv) -> + if access.enter_mut_borrows then + match access_projection access ctx update p' bv with + | Error err -> Error err + | Ok (ctx, res) -> + let nv = + { + v with + value = V.Borrow (V.MutBorrow (bid, res.updated)); + } + in + Ok (ctx, { res with updated = nv }) + else Error (FailBorrow bc)) + | _, V.Loan lc, _ -> ( + match lc with + | V.MutLoan bid -> Error (FailMutLoan bid) + | V.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 ctx update (pe :: p') sv with + | Error err -> Error err + | Ok (ctx, res) -> + let nv = + { + v with + value = V.Loan (V.SharedLoan (bids, res.updated)); + } + in + Ok (ctx, { res with updated = nv }) + else Error (FailSharedLoan bids)) + | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r -> + let pe, v, ty = r in + let pe = "- pe: " ^ E.show_projection_elem pe in + let v = "- v:\n" ^ V.show_value v in + let ty = "- ty:\n" ^ T.show_ety ty in + L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); + failwith "Inconsistent projection") + +(** Generic function to access (read/write) the value at a given place. + + We return the value we read at the place and the (eventually) updated + environment, if we managed to access the place, or the precise reason + why we failed. + *) +let access_place (access : projection_access) + (* Function to (eventually) update the value we find *) + (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx) + : (C.eval_ctx * V.typed_value) path_access_result = + (* Lookup the variable's value *) + let value = C.ctx_lookup_var_value ctx p.var_id in + (* Apply the projection *) + match access_projection access ctx update p.projection value with + | Error err -> Error err + | Ok (ctx, res) -> + (* Update the value *) + let ctx = C.ctx_update_var_value ctx p.var_id res.updated in + (* Return *) + Ok (ctx, res.read) + +type access_kind = + | Read (** We can go inside borrows and loans *) + | Write (** Don't enter shared borrows or shared loans *) + | Move (** Don't enter borrows or loans *) + +let access_kind_to_projection_access (access : access_kind) : projection_access + = + match access with + | Read -> + { + enter_shared_loans = true; + enter_mut_borrows = true; + lookup_shared_borrows = true; + } + | Write -> + { + enter_shared_loans = false; + enter_mut_borrows = true; + lookup_shared_borrows = false; + } + | Move -> + { + enter_shared_loans = false; + enter_mut_borrows = false; + lookup_shared_borrows = false; + } + +(** Read the value at a given place *) +let read_place (config : C.config) (access : access_kind) (p : E.place) + (ctx : C.eval_ctx) : V.typed_value path_access_result = + let access = access_kind_to_projection_access access in + (* The update function is the identity *) + let update v = v in + match access_place access update p ctx with + | Error err -> Error err + | Ok (ctx1, read_value) -> + (* Note that we ignore the new environment: it should be the same as the + original one. + *) + if config.check_invariants then + if ctx1 <> ctx then ( + let msg = + "Unexpected environment update:\nNew environment:\n" + ^ C.show_env ctx1.env ^ "\n\nOld environment:\n" + ^ C.show_env ctx.env + in + L.log#serror msg; + failwith "Unexpected environment update"); + Ok read_value + +let read_place_unwrap (config : C.config) (access : access_kind) (p : E.place) + (ctx : C.eval_ctx) : V.typed_value = + match read_place config access p ctx with + | Error _ -> failwith "Unreachable" + | Ok v -> v + +(** Update the value at a given place *) +let write_place (_config : C.config) (access : access_kind) (p : E.place) + (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx path_access_result = + let access = access_kind_to_projection_access access in + (* The update function substitutes the value with the new value *) + let update _ = nv in + match access_place access update p ctx with + | Error err -> Error err + | Ok (ctx, _) -> + (* We ignore the read value *) + Ok ctx + +let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place) + (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = + match write_place config access p nv ctx with + | Error _ -> failwith "Unreachable" + | Ok ctx -> ctx + +(** Compute an expanded ADT bottom value *) +let compute_expanded_bottom_adt_value (tyctx : T.type_def list) + (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) + (regions : T.erased_region list) (types : T.ety list) : V.typed_value = + (* Lookup the definition and check if it is an enumeration - it + should be an enumeration if and only if the projection element + is a field projection with *some* variant id. Retrieve the list + of fields at the same time. *) + let def = T.TypeDefId.nth tyctx def_id in + assert (List.length regions = List.length def.T.region_params); + (* Compute the field types *) + let field_types = + Subst.type_def_get_instantiated_field_etypes def opt_variant_id types + in + (* Initialize the expanded value *) + let fields = + List.map + (fun ty : V.typed_value -> ({ V.value = V.Bottom; ty } : V.typed_value)) + field_types + in + let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in + let ty = T.Adt (T.AdtId def_id, regions, types) in + { V.value = av; V.ty } + +(** Compute an expanded tuple bottom value *) +let compute_expanded_bottom_tuple_value (field_types : T.ety list) : + V.typed_value = + (* Generate the field values *) + let fields = + List.map (fun ty : V.typed_value -> { V.value = Bottom; ty }) field_types + in + let v = V.Adt { variant_id = None; field_values = fields } in + let ty = T.Adt (T.Tuple, [], field_types) in + { V.value = v; V.ty } + +(** Auxiliary helper to expand [Bottom] values. + + During compilation, rustc desaggregates the ADT initializations. The + consequence is that the following rust code: + ``` + let x = Cons a b; + ``` + + Looks like this in MIR: + ``` + (x as Cons).0 = a; + (x as Cons).1 = b; + set_discriminant(x, 0); // If `Cons` is the variant of index 0 + ``` + + The consequence is that we may sometimes need to write fields to values + which are currently [Bottom]. When doing this, we first expand the value + to, say, [Cons Bottom Bottom] (note that field projection contains information + about which variant we should project to, which is why we *can* set the + variant index when writing one of its fields). +*) +let expand_bottom_value_from_projection (config : C.config) + (access : access_kind) (p : E.place) (remaining_pes : int) + (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx = + (* Debugging *) + L.log#ldebug + (lazy + ("expand_bottom_value_from_projection:\n" ^ "pe: " + ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty)); + (* Prepare the update: we need to take the proper prefix of the place + during whose evaluation we got stuck *) + let projection' = + fst + (Utilities.list_split_at p.projection + (List.length p.projection - remaining_pes)) + in + let p' = { p with projection = projection' } in + (* Compute the expanded value. + The type of the [Bottom] value should be a tuple or an ADT. + Note that the projection element we got stuck at should be a + field projection, and gives the variant id if the [Bottom] value + is an enumeration value. + Also, the expanded value should be the proper ADT variant or a tuple + with the proper arity, with all the fields initialized to [Bottom] + *) + let nv = + match (pe, ty) with + (* "Regular" ADTs *) + | ( Field (ProjAdt (def_id, opt_variant_id), _), + T.Adt (T.AdtId def_id', regions, types) ) -> + assert (def_id = def_id'); + compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id + opt_variant_id regions types + (* Tuples *) + | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> + assert (arity = List.length tys); + (* Generate the field values *) + compute_expanded_bottom_tuple_value tys + | _ -> + failwith + ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty) + in + (* Update the context by inserting the expanded value at the proper place *) + match write_place config access p' nv ctx with + | Ok ctx -> ctx + | Error _ -> failwith "Unreachable" + +(** Update the environment to be able to read a place. + + When reading a place, we may be stuck along the way because some value + is borrowed, we reach a symbolic value, etc. In this situation [read_place] + fails while returning precise information about the failure. This function + uses this information to update the environment (by ending borrows, + expanding symbolic values) until we manage to fully read the place. + *) +let rec update_ctx_along_read_place (config : C.config) (access : access_kind) + (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = + (* Attempt to read the place: if it fails, update the environment and retry *) + match read_place config access p ctx with + | Ok _ -> ctx + | Error err -> + let ctx = + match err with + | FailSharedLoan bids -> end_outer_borrows config bids ctx + | FailMutLoan bid -> end_outer_borrow config bid ctx + | FailInactivatedMutBorrow bid -> + activate_inactivated_mut_borrow config Outer bid ctx + | FailSymbolic (pe, sp) -> + (* Expand the symbolic value *) + expand_symbolic_value_no_branching config pe sp ctx + | FailBottom (_, _, _) -> + (* We can't expand [Bottom] values while reading them *) + failwith "Found [Bottom] while reading a place" + | FailBorrow _ -> failwith "Could not read a borrow" + in + update_ctx_along_read_place config access p ctx + +(** Update the environment to be able to write to a place. + + See [update_env_alond_read_place]. +*) +let rec update_ctx_along_write_place (config : C.config) (access : access_kind) + (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = + (* Attempt to *read* (yes, "read": we check the access to the place, and + write to it later) the place: if it fails, update the environment and retry *) + match read_place config access p ctx with + | Ok _ -> ctx + | Error err -> + let ctx = + match err with + | FailSharedLoan bids -> end_outer_borrows config bids ctx + | FailMutLoan bid -> end_outer_borrow config bid ctx + | FailInactivatedMutBorrow bid -> + activate_inactivated_mut_borrow config Outer bid ctx + | FailSymbolic (pe, sp) -> + (* Expand the symbolic value *) + expand_symbolic_value_no_branching config pe sp ctx + | FailBottom (remaining_pes, pe, ty) -> + (* Expand the [Bottom] value *) + expand_bottom_value_from_projection config access p remaining_pes pe + ty ctx + | FailBorrow _ -> failwith "Could not write to a borrow" + in + update_ctx_along_write_place config access p ctx + +exception UpdateCtx of C.eval_ctx +(** Small utility used to break control-flow *) + +(** End the loans at a given place: read the value, if it contains a loan, + end this loan, repeat. + + This is used when reading, borrowing, writing to a value. We typically + first call [update_ctx_along_read_place] or [update_ctx_along_write_place] + to get access to the value, then call this function to "prepare" the value: + when moving values, we can't move a value which contains loans and thus need + to end them, etc. + *) +let rec end_loans_at_place (config : C.config) (access : access_kind) + (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = + (* Iterator to explore a value and update the context whenever we find + * loans. + * We use exceptions to make it handy: whenever we update the + * context, we raise an exception wrapping the updated context. + * *) + let obj = + object + inherit [_] V.iter_typed_value as super + + method! visit_borrow_content env bc = + match bc with + | V.SharedBorrow _ | V.MutBorrow (_, _) -> + (* Nothing special to do *) super#visit_borrow_content env bc + | V.InactivatedMutBorrow bid -> + (* We need to activate inactivated borrows *) + let ctx = activate_inactivated_mut_borrow config Inner bid ctx in + raise (UpdateCtx ctx) + + method! visit_loan_content env lc = + match lc with + | V.SharedLoan (bids, v) -> ( + (* End the loans if we need a modification access, otherwise dive into + the shared value *) + match access with + | Read -> super#visit_SharedLoan env bids v + | Write | Move -> + let ctx = end_outer_borrows config bids ctx in + raise (UpdateCtx ctx)) + | V.MutLoan bid -> + (* We always need to end mutable borrows *) + let ctx = end_outer_borrow config bid ctx in + raise (UpdateCtx ctx) + end + in + + (* First, retrieve the value *) + match read_place config access p ctx with + | Error _ -> failwith "Unreachable" + | Ok v -> ( + (* Inspect the value and update the context while doing so. + If the context gets updated: perform a recursive call (many things + may have been updated in the context: we need to re-read the value + at place [p] - and this value may actually not be accessible + anymore...) + *) + try + obj#visit_typed_value () v; + (* No context update required: return the current context *) + ctx + with UpdateCtx ctx -> + (* The context was updated: do a recursive call to reinspect the value *) + end_loans_at_place config access p ctx) + +(** Drop (end) all the loans and borrows at a given place, which should be + seen as an l-value (we will write to it later, but need to drop the borrows + before writing). + + We start by only dropping the borrows, then we end the loans. The reason + is that some loan we find may be borrowed by another part of the subvalue. + In order to correctly handle the "outer borrow" priority (we should end + the outer borrows first) which is not really applied here (we are preparing + the value for override: we can end the borrows inside, without ending the + borrows we traversed to actually access the value) we first end the borrows + we find in the place, to make sure all the "local" loans are taken care of. + Then, if we find a loan, it means it is "externally" borrowed (the associated + borrow is not in a subvalue of the place under inspection). + Also note that whenever we end a loan, we might propagate back a value inside + the place under inspection: we must re-end all the borrows we find there, + before reconsidering loans. + + Repeat: + - read the value at a given place + - as long as we find a loan or a borrow, end it + + This is used to drop values (when we need to write to a place, we first + drop the value there to properly propagate back values which are not/can't + be borrowed anymore). + *) +let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Iterator to explore a value and update the context whenever we find + borrows/loans. + We use exceptions to make it handy: whenever we update the + context, we raise an exception wrapping the updated context. + + Note that we can end the borrows which are inside the value (while the + value itself might be inside a borrow/loan: we are thus ending inner + borrows). Because a loan inside the value may be linked to a borrow + somewhere else *also inside* the value (it's possible with adts), + we first end all the borrows we find - by using [Inner] to allow + ending inner borrows - then end all the loans we find. + + It is really important to do this in two steps: the borrow linked to a + loan may be inside the value at place p, in which case this borrow may be + an inner borrow that we *can* end, but it may also be outside this + value, in which case we need to end all the outer borrows first... + Also, whenever the context is updated, we need to re-inspect + the value at place p *in two steps* again (end borrows, then end + loans). + + Example: + ======= + We want to end the borrows/loans at `*x` in the following environment: + ``` + x -> mut_borrow l0 (mut_loan l1, mut_borrow l1 (Int 3), mut_loan l2) + y -> mut_borrow l2 (Bool true) + ``` + + We have to consider two things: + - the borrow `mut_borrow l1 (Int 3)` borrows a subvalue of `*x` + - the borrow corresponding to the loan `mut_loan l2` is outside of `*x` + + We first end all the *borrows* (not the loans) inside of `*x`, which gives: + ``` + x -> mut_borrow l0 (Int 3, ⊥, mut_loan l2) + y -> mut_borrow l2 (Bool true) + ``` + + Note that when ending the borrows, we can (and have to) ignore the outer + borrows (in this case `mut_borrow l0 ...`). Otherwise, we would have to end + the borrow `l0` which is incorrect (note that we might have to drop the + borrows/loans at `*x` if we evaluate, for instance, `*x = ...`). + It is ok to ignore outer borrows in this case because whenever + we end a borrow, it is an outer borrow locally to `*x` (i.e., we ignore + the outer borrows when accessing `*x`, but once examining the value at + `*x` we never dive into borrows: whenever we find one, we end it - it is thus + an outer borrow, in some way). + + Then, we end the loans at `*x`. Note that as at this point `*x` doesn't + contain borrows (only loans), the borrows corresponding to those loans + are thus necessarily outside of `*x`: we mustn't ignore outer borrows this + time. This gives: + ``` + x -> mut_borrow l0 (Int 3, ⊥, Bool true) + y -> ⊥ + ``` + *) + let obj = + object + inherit [_] V.iter_typed_value as super + + method! visit_borrow_content end_loans bc = + (* Sanity check: we should have ended all the borrows before starting + to end loans *) + assert (not end_loans); + + (* We need to end all borrows. Note that we ignore the outer borrows + when ending the borrows we find here (we call [end_inner_borrow(s)]: + the value at place p might be below a borrow/loan). Note however + that if we restrain ourselves at the value at place p, the borrow we + found here can be considered as an outer borrow. + *) + match bc with + | V.SharedBorrow bid | V.MutBorrow (bid, _) -> + raise (UpdateCtx (end_inner_borrow config bid ctx)) + | V.InactivatedMutBorrow bid -> + (* We need to activate ithe nactivated borrow - later, we will + * actually end it - Rk.: we could actually end it straight away + * (this is not really important) *) + let ctx = activate_inactivated_mut_borrow config Inner bid ctx in + raise (UpdateCtx ctx) + + method! visit_loan_content end_loans lc = + if + (* If we can, end the loans, otherwise ignore: keep for later *) + end_loans + then + (* We need to end all loans. Note that as all the borrows inside + the value at place p should already have ended, the borrows + associated to the loans we find here should be borrows from + outside this value: we need to call [end_outer_borrow(s)] + (we can't ignore outer borrows this time). + *) + match lc with + | V.SharedLoan (bids, _) -> + raise (UpdateCtx (end_outer_borrows config bids ctx)) + | V.MutLoan bid -> raise (UpdateCtx (end_outer_borrow config bid ctx)) + else super#visit_loan_content end_loans lc + end + in + + (* We do something similar to [end_loans_at_place]. + First, retrieve the value *) + match read_place config Write p ctx with + | Error _ -> failwith "Unreachable" + | Ok v -> ( + (* Inspect the value and update the context while doing so. + If the context gets updated: perform a recursive call (many things + may have been updated in the context: first we need to retrieve the + proper updated value - and this value may actually not be accessible + anymore + *) + try + (* Inspect the value: end the borrows only *) + obj#visit_typed_value false v; + (* Inspect the value: end the loans *) + obj#visit_typed_value true v; + (* No context update required: return the current context *) + ctx + with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx) + +(** Copy a value, and return the resulting value. + + Note that copying values might update the context. For instance, when + copying shared borrows, we need to insert new shared borrows in the context. + + Also, this function is actually more general than it should be: it can be used + to copy concrete ADT values, while ADT copy should be done through the Copy + trait (i.e., by calling a dedicated function). This is why we added a parameter + to control this copy. Note that here by ADT we mean the user-defined ADTs + (not tuples or assumed types). + *) +let rec copy_value (allow_adt_copy : bool) (config : C.config) + (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value = + (* 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 _, _, _) -> assert allow_adt_copy + | T.Adt (T.Tuple, _, _) -> () (* Ok *) + | _ -> failwith "Unreachable"); + let ctx, fields = + List.fold_left_map + (copy_value allow_adt_copy 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 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 allow_adt_copy config ctx sv) + | V.Symbolic sp -> + (* We can copy only if the type is "primitively" copyable. + * Note that in the general case, copy is a trait: copying values + * thus requires calling the proper function. Here, we copy values + * for very simple types such as integers, shared borrows, etc. *) + assert ( + type_is_primitively_copyable (Subst.erase_regions sp.V.svalue.V.sv_ty)); + (* If the type is copyable, we simply return the current value. Side + * remark: what is important to look at when copying symbolic values + * is symbolic expansion. The important subcase is the expansion of shared + * borrows: when doing so, every occurrence of the same symbolic value + * must use a fresh borrow id. *) + (ctx, v) + +(** Small utility. + + Prepare a place which is to be used as the destination of an assignment: + update the environment along the paths, end the borrows and loans at + this place, etc. + + Return the updated context and the (updated) value at the end of the + place. This value should not contain any loan or borrow (and we check + it is the case). Note that it is very likely to contain [Bottom] values. + *) +let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) : + C.eval_ctx * V.typed_value = + (* TODO *) + let access = Write in + let ctx = update_ctx_along_write_place config access p ctx in + (* End the borrows and loans, starting with the borrows *) + let ctx = drop_borrows_loans_at_lplace config p ctx in + (* Read the value and check it *) + let v = read_place_unwrap config access p ctx in + (* Sanity checks *) + assert (not (loans_in_value v)); + assert (not (borrows_in_value v)); + (* Return *) + (ctx, v) + +(** Read the value at a given place. + As long as it is a loan, end the loan. + This function doesn't perform a recursive exploration: + it won't dive into the value to end all the inner + loans (contrary to [drop_borrows_loans_at_lplace] for + instance). + *) +let rec end_loan_exactly_at_place (config : C.config) (access : access_kind) + (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = + let v = read_place_unwrap config access p ctx in + match v.V.value with + | V.Loan (V.SharedLoan (bids, _)) -> + let ctx = end_outer_borrows config bids ctx in + end_loan_exactly_at_place config access p ctx + | V.Loan (V.MutLoan bid) -> + let ctx = end_outer_borrow config bid ctx in + end_loan_exactly_at_place config access p ctx + | _ -> ctx |