diff options
Diffstat (limited to 'compiler/InterpreterPaths.ml')
| -rw-r--r-- | compiler/InterpreterPaths.ml | 292 |
1 files changed, 133 insertions, 159 deletions
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 04dc8892..999b8ab0 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -1,9 +1,7 @@ -module T = Types -module V = Values -module E = Expressions -module C = Contexts -module Subst = Substitute -module L = Logging +open Types +open Values +open Expressions +open Contexts open Cps open ValuesUtils open InterpreterUtils @@ -13,7 +11,7 @@ open InterpreterExpansion module Synth = SynthesizeSymbolic (** The local logger *) -let log = L.paths_log +let log = Logging.paths_log (** Paths *) @@ -24,26 +22,26 @@ let log = L.paths_log TODO: compare with borrow_lres? *) type path_fail_kind = - | FailSharedLoan of V.BorrowId.Set.t + | FailSharedLoan of BorrowId.Set.t (** Failure because we couldn't go inside a shared loan *) - | FailMutLoan of V.BorrowId.id + | FailMutLoan of BorrowId.id (** Failure because we couldn't go inside a mutable loan *) - | FailReservedMutBorrow of V.BorrowId.id + | FailReservedMutBorrow of BorrowId.id (** Failure because we couldn't go inside a reserved mutable borrow (which should get activated) *) - | FailSymbolic of int * V.symbolic_value + | FailSymbolic of int * symbolic_value (** Failure because we need to enter a symbolic value (and thus need to expand it). We return the number of elements which remained in the path when we reached the error - this allows to retrieve the path prefix, which is useful for the synthesis. *) - | FailBottom of int * E.projection_elem * T.ety + | FailBottom of int * projection_elem * 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 remained in the path when we reached the error - this allows to properly update the Bottom value, if needs be. *) - | FailBorrow of V.borrow_content + | FailBorrow of borrow_content (** We got stuck because we couldn't enter a borrow *) [@@deriving show] @@ -55,7 +53,7 @@ type path_fail_kind = 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 updated_read_value = { read : typed_value; updated : typed_value } type projection_access = { enter_shared_loans : bool; @@ -70,10 +68,10 @@ type projection_access = { TODO: use exceptions? *) -let rec access_projection (access : projection_access) (ctx : C.eval_ctx) +let rec access_projection (access : projection_access) (ctx : 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 = + (update : typed_value -> typed_value) (p : projection) (v : typed_value) : + (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 } @@ -85,8 +83,8 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) if nv.ty <> v.ty then ( log#lerror (lazy - ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: " - ^ T.show_ety v.ty)); + ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: " + ^ show_ety v.ty)); raise (Failure "Assertion failed: new value doesn't have the same type as its \ @@ -94,60 +92,57 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) 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 (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id), - V.Adt adt, - T.Adt (type_id, _, _, _) ) -> ( + match (pe, v.value, v.ty) with + | ( Field ((ProjAdt (_, _) as proj_kind), field_id), + VAdt adt, + TAdt (type_id, _) ) -> ( (* Check consistency *) (match (proj_kind, type_id) with - | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' -> + | ProjAdt (def_id, opt_variant_id), TAdtId def_id' -> assert (def_id = def_id'); assert (opt_variant_id = adt.variant_id) - | ProjOption variant_id, T.Assumed T.Option -> - assert (Some variant_id = adt.variant_id) | _ -> raise (Failure "Unreachable")); (* Actually project *) - let fv = T.FieldId.nth adt.field_values field_id in + let fv = 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 + FieldId.update_nth adt.field_values field_id res.updated in - let nadt = V.Adt { adt with V.field_values = nvalues } in + let nadt = VAdt { adt with 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, _, _, _) - -> ( + | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> ( assert (arity = List.length adt.field_values); - let fv = T.FieldId.nth adt.field_values field_id in + let fv = 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 + FieldId.update_nth adt.field_values field_id res.updated in - let ntuple = V.Adt { adt with field_values = nvalues } in + let ntuple = VAdt { 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 (_, _) | ProjTuple _ | ProjOption _), _), V.Bottom, _ -> + | Field ((ProjAdt (_, _) | ProjTuple _), _), VBottom, _ -> Error (FailBottom (1 + List.length p', pe, v.ty)) (* Symbolic value: needs to be expanded *) - | _, Symbolic sp, _ -> + | _, VSymbolic sp, _ -> (* Expand the symbolic value *) Error (FailSymbolic (1 + List.length p', 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 + VAdt { variant_id = None; field_values = [ bv ] }, + TAdt (TAssumed TBox, _) ) -> ( + (* We allow moving outside of boxes. In practice, this kind of + * manipulations should happen only inside unsafe code, so * it shouldn't happen due to user code, and we leverage it * when implementing box dereferencement for the concrete * interpreter *) @@ -158,20 +153,20 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) { v with value = - V.Adt { variant_id = None; field_values = [ res.updated ] }; + VAdt { variant_id = None; field_values = [ res.updated ] }; } in Ok (ctx, { res with updated = nv })) (* Borrows *) - | Deref, V.Borrow bc, _ -> ( + | Deref, VBorrow bc, _ -> ( match bc with - | V.SharedBorrow bid -> + | VSharedBorrow 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 _) -> + | _, Concrete (VMutLoan _) -> raise (Failure "Expected a shared loan") - | _, Concrete (V.SharedLoan (bids, sv)) -> ( + | _, Concrete (VSharedLoan (bids, sv)) -> ( (* Explore the shared value *) match access_projection access ctx update p' sv with | Error err -> Error err @@ -180,23 +175,23 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) by {!access_projection} *) let ctx = update_loan ek bid - (V.SharedLoan (bids, res.updated)) + (VSharedLoan (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 + ( AMutLoan (_, _) + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan + | AEndedSharedLoan (_, _) + | AIgnoredMutLoan (_, _) + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AIgnoredSharedLoan _ ) ) -> + | AIgnoredSharedLoan _ ) ) -> raise (Failure "Expected a shared (abstraction) loan") - | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> ( + | _, Abstract (ASharedLoan (bids, sv, _av)) -> ( (* Explore the shared value *) match access_projection access ctx update p' sv with | Error err -> Error err @@ -204,37 +199,34 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) (* Relookup the child avalue *) let av = match lookup_loan ek bid ctx with - | _, Abstract (V.ASharedLoan (_, _, av)) -> av + | _, Abstract (ASharedLoan (_, _, av)) -> av | _ -> raise (Failure "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)) + (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.ReservedMutBorrow bid -> Error (FailReservedMutBorrow bid) - | V.MutBorrow (bid, bv) -> + | VReservedMutBorrow bid -> Error (FailReservedMutBorrow bid) + | VMutBorrow (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)); - } + { v with value = VBorrow (VMutBorrow (bid, res.updated)) } in Ok (ctx, { res with updated = nv }) else Error (FailBorrow bc)) - | _, V.Loan lc, _ -> ( + | _, VLoan lc, _ -> ( match lc with - | V.MutLoan bid -> Error (FailMutLoan bid) - | V.SharedLoan (bids, sv) -> + | VMutLoan bid -> Error (FailMutLoan bid) + | VSharedLoan (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 *) @@ -243,18 +235,15 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) | Error err -> Error err | Ok (ctx, res) -> let nv = - { - v with - value = V.Loan (V.SharedLoan (bids, res.updated)); - } + { v with value = VLoan (VSharedLoan (bids, res.updated)) } in Ok (ctx, { res with updated = nv }) else Error (FailSharedLoan bids)) - | (_, (V.Literal _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r -> + | (_, (VLiteral _ | VAdt _ | VBottom | VBorrow _), _) 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 + let pe = "- pe: " ^ show_projection_elem pe in + let v = "- v:\n" ^ show_value v in + let ty = "- ty:\n" ^ show_ety ty in log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); raise (Failure "Inconsistent projection")) @@ -266,16 +255,16 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) *) 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 = + (update : typed_value -> typed_value) (p : place) (ctx : eval_ctx) : + (eval_ctx * typed_value) path_access_result = (* Lookup the variable's value *) - let value = C.ctx_lookup_var_value ctx p.var_id in + let value = 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 + let ctx = ctx_update_var_value ctx p.var_id res.updated in (* Return *) Ok (ctx, res.read) @@ -311,8 +300,8 @@ let access_kind_to_projection_access (access : access_kind) : projection_access Note that we only access the value at the place, and do not check that the value is "well-formed" (for instance that it doesn't contain bottoms). *) -let try_read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : - V.typed_value path_access_result = +let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) : + 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 @@ -322,26 +311,25 @@ let try_read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : (* Note that we ignore the new environment: it should be the same as the original one. *) - if !Config.check_invariants then + if !Config.sanity_checks 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 + ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env in log#serror msg; raise (Failure "Unexpected environment update")); Ok read_value -let read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : - V.typed_value = +let read_place (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value + = match try_read_place access p ctx with | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e)) | Ok v -> v (** Attempt to update the value at a given place *) -let try_write_place (access : access_kind) (p : E.place) (nv : V.typed_value) - (ctx : C.eval_ctx) : C.eval_ctx path_access_result = +let try_write_place (access : access_kind) (p : place) (nv : typed_value) + (ctx : eval_ctx) : 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 @@ -351,54 +339,42 @@ let try_write_place (access : access_kind) (p : E.place) (nv : V.typed_value) (* We ignore the read value *) Ok ctx -let write_place (access : access_kind) (p : E.place) (nv : V.typed_value) - (ctx : C.eval_ctx) : C.eval_ctx = +let write_place (access : access_kind) (p : place) (nv : typed_value) + (ctx : eval_ctx) : eval_ctx = match try_write_place access p nv ctx with | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e)) | Ok ctx -> ctx -let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t) - (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option) - (regions : T.erased_region list) (types : T.ety list) - (cgs : T.const_generic list) : V.typed_value = +let compute_expanded_bottom_adt_value (ctx : eval_ctx) (def_id : TypeDeclId.id) + (opt_variant_id : VariantId.id option) (generics : generic_args) : + typed_value = + assert (TypesUtils.generic_args_only_erased_regions generics); (* 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.TypeDeclId.Map.find def_id tyctx in - assert (List.length regions = List.length def.T.region_params); + let def = ctx_lookup_type_decl ctx def_id in + assert (List.length generics.regions = List.length def.generics.regions); (* Compute the field types *) let field_types = - Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types cgs + AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id + generics in (* Initialize the expanded value *) let fields = List.map mk_bottom 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, cgs) in - { V.value = av; V.ty } - -let compute_expanded_bottom_option_value (variant_id : T.VariantId.id) - (param_ty : T.ety) : V.typed_value = - (* Note that the variant can be [Some] or [None]: we expand bottom values - * when writing to fields or setting discriminants *) - let field_values = - if variant_id = T.option_some_id then [ mk_bottom param_ty ] - else if variant_id = T.option_none_id then [] - else raise (Failure "Unreachable") - in - let av = V.Adt { variant_id = Some variant_id; field_values } in - let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ], []) in - { V.value = av; ty } + let av = VAdt { variant_id = opt_variant_id; field_values = fields } in + let ty = TAdt (TAdtId def_id, generics) in + { value = av; ty } -let compute_expanded_bottom_tuple_value (field_types : T.ety list) : - V.typed_value = +let compute_expanded_bottom_tuple_value (field_types : ety list) : typed_value = (* Generate the field values *) let fields = List.map mk_bottom 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 } + let v = VAdt { variant_id = None; field_values = fields } in + let generics = TypesUtils.mk_generic_args [] field_types [] [] in + let ty = TAdt (TTuple, generics) in + { value = v; ty } -(** Auxiliary helper to expand {!V.Bottom} values. +(** Auxiliary helper to expand {!Bottom} values. During compilation, rustc desaggregates the ADT initializations. The consequence is that the following rust code: @@ -414,19 +390,19 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) : ]} The consequence is that we may sometimes need to write fields to values - which are currently {!V.Bottom}. When doing this, we first expand the value + 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 (access : access_kind) (p : E.place) - (remaining_pes : int) (pe : E.projection_elem) (ty : T.ety) - (ctx : C.eval_ctx) : C.eval_ctx = +let expand_bottom_value_from_projection (access : access_kind) (p : place) + (remaining_pes : int) (pe : projection_elem) (ty : ety) (ctx : eval_ctx) : + eval_ctx = (* Debugging *) log#ldebug (lazy ("expand_bottom_value_from_projection:\n" ^ "pe: " - ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty)); + ^ show_projection_elem pe ^ "\n" ^ "ty: " ^ show_ety ty)); (* Prepare the update: we need to take the proper prefix of the place during whose evaluation we got stuck *) let projection' = @@ -436,42 +412,40 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place) in let p' = { p with projection = projection' } in (* Compute the expanded value. - The type of the {!V.Bottom} value should be a tuple or an ADT. + The type of the {!Bottom} value should be a tuple or an AD Note that the projection element we got stuck at should be a - field projection, and gives the variant id if the {!V.Bottom} value + 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 {!V.Bottom} + 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, cgs) ) -> + TAdt (TAdtId def_id', generics) ) -> assert (def_id = def_id'); - compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id - opt_variant_id regions types cgs - (* Option *) - | ( Field (ProjOption variant_id, _), - T.Adt (T.Assumed T.Option, [], [ ty ], []) ) -> - compute_expanded_bottom_option_value variant_id ty + compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys, []) -> - assert (arity = List.length tys); + | ( Field (ProjTuple arity, _), + TAdt + (TTuple, { regions = []; types; const_generics = []; trait_refs = [] }) + ) -> + assert (arity = List.length types); (* Generate the field values *) - compute_expanded_bottom_tuple_value tys + compute_expanded_bottom_tuple_value types | _ -> raise (Failure - ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty)) + ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty)) in (* Update the context by inserting the expanded value at the proper place *) match try_write_place access p' nv ctx with | Ok ctx -> ctx | Error _ -> raise (Failure "Unreachable") -let rec update_ctx_along_read_place (config : C.config) (access : access_kind) - (p : E.place) : cm_fun = +let rec update_ctx_along_read_place (config : config) (access : access_kind) + (p : place) : cm_fun = fun cf ctx -> (* Attempt to read the place: if it fails, update the environment and retry *) match try_read_place access p ctx with @@ -492,14 +466,14 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind) expand_symbolic_value_no_branching config sp (Some (Synth.mk_mplace prefix ctx)) | FailBottom (_, _, _) -> - (* We can't expand {!V.Bottom} values while reading them *) + (* We can't expand {!Bottom} values while reading them *) raise (Failure "Found [Bottom] while reading a place") | FailBorrow _ -> raise (Failure "Could not read a borrow") in comp cc (update_ctx_along_read_place config access p) cf ctx -let rec update_ctx_along_write_place (config : C.config) (access : access_kind) - (p : E.place) : cm_fun = +let rec update_ctx_along_write_place (config : config) (access : access_kind) + (p : place) : cm_fun = fun cf 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 *) @@ -517,7 +491,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind) expand_symbolic_value_no_branching config sp (Some (Synth.mk_mplace p ctx)) | FailBottom (remaining_pes, pe, ty) -> - (* Expand the {!V.Bottom} value *) + (* Expand the {!Bottom} value *) fun cf ctx -> let ctx = expand_bottom_value_from_projection access p remaining_pes pe ty @@ -532,8 +506,8 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind) (** Small utility used to break control-flow *) exception UpdateCtx of cm_fun -let rec end_loans_at_place (config : C.config) (access : access_kind) - (p : E.place) : cm_fun = +let rec end_loans_at_place (config : config) (access : access_kind) (p : place) + : cm_fun = fun cf ctx -> (* Iterator to explore a value and update the context whenever we find * loans. @@ -542,28 +516,28 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) * *) let obj = object - inherit [_] V.iter_typed_value as super + inherit [_] iter_typed_value as super method! visit_borrow_content env bc = match bc with - | V.SharedBorrow _ | V.MutBorrow (_, _) -> + | VSharedBorrow _ | VMutBorrow (_, _) -> (* Nothing special to do *) super#visit_borrow_content env bc - | V.ReservedMutBorrow bid -> + | VReservedMutBorrow bid -> (* We need to activate reserved borrows *) let cc = promote_reserved_mut_borrow config bid in raise (UpdateCtx cc) method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, v) -> ( + | VSharedLoan (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 + | Read -> super#visit_VSharedLoan env bids v | Write | Move -> let cc = end_borrows config bids in raise (UpdateCtx cc)) - | V.MutLoan bid -> + | VMutLoan bid -> (* We always need to end mutable borrows *) let cc = end_borrow config bid in raise (UpdateCtx cc) @@ -587,20 +561,20 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) * a recursive call to reinspect the value *) comp cc (end_loans_at_place config access p) cf ctx -let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = +let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun = fun cf ctx -> (* Move the current value in the place outside of this place and into * a dummy variable *) let access = Write in let v = read_place access p ctx in - let ctx = write_place access p (mk_bottom v.V.ty) ctx in - let dummy_id = C.fresh_dummy_var_id () in - let ctx = C.ctx_push_dummy_var ctx dummy_id v in + let ctx = write_place access p (mk_bottom v.ty) ctx in + let dummy_id = fresh_dummy_var_id () in + let ctx = ctx_push_dummy_var ctx dummy_id v in (* Auxiliary function *) let rec drop : cm_fun = fun cf ctx -> (* Read the value *) - let v = C.ctx_lookup_dummy_var ctx dummy_id in + let v = ctx_lookup_dummy_var ctx dummy_id in (* Check if there are loans or borrows to end *) let with_borrows = false in match get_first_outer_loan_or_borrow_in_value with_borrows v with @@ -611,8 +585,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = (* There are: end them then retry *) let cc = match c with - | LoanContent (V.SharedLoan (bids, _)) -> end_borrows config bids - | LoanContent (V.MutLoan bid) -> end_borrow config bid + | LoanContent (VSharedLoan (bids, _)) -> end_borrows config bids + | LoanContent (VMutLoan bid) -> end_borrow config bid | BorrowContent _ -> raise (Failure "Unreachable") in (* Retry *) @@ -624,7 +598,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = let cc = comp cc (fun cf ctx -> (* Pop *) - let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in + let ctx, v = ctx_remove_dummy_var ctx dummy_id in (* Reinsert *) let ctx = write_place access p v ctx in (* Sanity check *) @@ -635,8 +609,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun = (* Continue *) cc cf ctx -let prepare_lplace (config : C.config) (p : E.place) - (cf : V.typed_value -> m_fun) : m_fun = +let prepare_lplace (config : config) (p : place) (cf : typed_value -> m_fun) : + m_fun = fun ctx -> log#ldebug (lazy |