diff options
Diffstat (limited to 'compiler/InterpreterPaths.ml')
| -rw-r--r-- | compiler/InterpreterPaths.ml | 190 |
1 files changed, 95 insertions, 95 deletions
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index a76ebfeb..faba1088 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -69,7 +69,7 @@ type projection_access = { TODO: use exceptions? *) -let rec access_projection (meta : Meta.meta) (access : projection_access) +let rec access_projection (span : Meta.span) (access : projection_access) (ctx : eval_ctx) (* Function to (eventually) update the value we find *) (update : typed_value -> typed_value) (p : projection) (v : typed_value) : @@ -87,7 +87,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (lazy ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: " ^ show_ety v.ty)); - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Assertion failed: new value doesn't have the same type as its \ destination"); Ok (ctx, { read = v; updated = nv }) @@ -100,14 +100,14 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (* Check consistency *) (match (proj_kind, type_id) with | ProjAdt (def_id, opt_variant_id), TAdtId def_id' -> - sanity_check __FILE__ __LINE__ (def_id = def_id') meta; + sanity_check __FILE__ __LINE__ (def_id = def_id') span; sanity_check __FILE__ __LINE__ (opt_variant_id = adt.variant_id) - meta - | _ -> craise __FILE__ __LINE__ meta "Unreachable"); + span + | _ -> craise __FILE__ __LINE__ span "Unreachable"); (* Actually project *) let fv = FieldId.nth adt.field_values field_id in - match access_projection meta access ctx update p' fv with + match access_projection span access ctx update p' fv with | Error err -> Error err | Ok (ctx, res) -> (* Update the field value *) @@ -121,10 +121,10 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> ( sanity_check __FILE__ __LINE__ (arity = List.length adt.field_values) - meta; + span; let fv = FieldId.nth adt.field_values field_id in (* Project *) - match access_projection meta access ctx update p' fv with + match access_projection span access ctx update p' fv with | Error err -> Error err | Ok (ctx, res) -> (* Update the field value *) @@ -151,7 +151,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) * it shouldn't happen due to user code, and we leverage it * when implementing box dereferencement for the concrete * interpreter *) - match access_projection meta access ctx update p' bv with + match access_projection span access ctx update p' bv with | Error err -> Error err | Ok (ctx, res) -> let nv = @@ -168,18 +168,18 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) | VSharedBorrow bid -> (* Lookup the loan content, and explore from there *) if access.lookup_shared_borrows then - match lookup_loan meta ek bid ctx with + match lookup_loan span ek bid ctx with | _, Concrete (VMutLoan _) -> - craise __FILE__ __LINE__ meta "Expected a shared loan" + craise __FILE__ __LINE__ span "Expected a shared loan" | _, Concrete (VSharedLoan (bids, sv)) -> ( (* Explore the shared value *) - match access_projection meta access ctx update p' sv with + match access_projection span 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 meta ek bid + update_loan span ek bid (VSharedLoan (bids, res.updated)) ctx in @@ -189,29 +189,29 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) Abstract ( AMutLoan (_, _) | AEndedMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AIgnoredSharedLoan _ ) ) -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Expected a shared (abstraction) loan" | _, Abstract (ASharedLoan (bids, sv, _av)) -> ( (* Explore the shared value *) - match access_projection meta access ctx update p' sv with + match access_projection span access ctx update p' sv with | Error err -> Error err | Ok (ctx, res) -> (* Relookup the child avalue *) let av = - match lookup_loan meta ek bid ctx with + match lookup_loan span ek bid ctx with | _, Abstract (ASharedLoan (_, _, av)) -> av - | _ -> craise __FILE__ __LINE__ meta "Unexpected" + | _ -> craise __FILE__ __LINE__ span "Unexpected" in (* Update the shared loan with the new value returned by {!access_projection} *) let ctx = - update_aloan meta ek bid + update_aloan span ek bid (ASharedLoan (bids, res.updated, av)) ctx in @@ -221,7 +221,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) | VReservedMutBorrow bid -> Error (FailReservedMutBorrow bid) | VMutBorrow (bid, bv) -> if access.enter_mut_borrows then - match access_projection meta access ctx update p' bv with + match access_projection span access ctx update p' bv with | Error err -> Error err | Ok (ctx, res) -> let nv = @@ -238,7 +238,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) we mustn't ignore the current projection element *) if access.enter_shared_loans then match - access_projection meta access ctx update (pe :: p') sv + access_projection span access ctx update (pe :: p') sv with | Error err -> Error err | Ok (ctx, res) -> @@ -252,7 +252,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) let pe = "- pe: " ^ show_projection_elem pe in let v = "- v:\n" ^ show_value v in let ty = "- ty:\n" ^ show_ety ty in - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty)) (** Generic function to access (read/write) the value at a given place. @@ -261,18 +261,18 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) environment, if we managed to access the place, or the precise reason why we failed. *) -let access_place (meta : Meta.meta) (access : projection_access) +let access_place (span : Meta.span) (access : projection_access) (* Function to (eventually) update the value we find *) (update : typed_value -> typed_value) (p : place) (ctx : eval_ctx) : (eval_ctx * typed_value) path_access_result = (* Lookup the variable's value *) - let value = ctx_lookup_var_value meta ctx p.var_id in + let value = ctx_lookup_var_value span ctx p.var_id in (* Apply the projection *) - match access_projection meta access ctx update p.projection value with + match access_projection span access ctx update p.projection value with | Error err -> Error err | Ok (ctx, res) -> (* Update the value *) - let ctx = ctx_update_var_value meta ctx p.var_id res.updated in + let ctx = ctx_update_var_value span ctx p.var_id res.updated in (* Return *) Ok (ctx, res.read) @@ -308,12 +308,12 @@ 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 (meta : Meta.meta) (access : access_kind) (p : place) +let try_read_place (span : Meta.span) (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 - match access_place meta access update p ctx with + match access_place span 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 @@ -325,41 +325,41 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place) "Unexpected environment update:\nNew environment:\n" ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env in - craise __FILE__ __LINE__ meta msg); + craise __FILE__ __LINE__ span msg); Ok read_value -let read_place (meta : Meta.meta) (access : access_kind) (p : place) +let read_place (span : Meta.span) (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value = - match try_read_place meta access p ctx with + match try_read_place span access p ctx with | Error e -> - craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e) + craise __FILE__ __LINE__ span ("Unreachable: " ^ show_path_fail_kind e) | Ok v -> v (** Attempt to update the value at a given place *) -let try_write_place (meta : Meta.meta) (access : access_kind) (p : place) +let try_write_place (span : Meta.span) (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 - match access_place meta access update p ctx with + match access_place span access update p ctx with | Error err -> Error err | Ok (ctx, _) -> (* We ignore the read value *) Ok ctx -let write_place (meta : Meta.meta) (access : access_kind) (p : place) +let write_place (span : Meta.span) (access : access_kind) (p : place) (nv : typed_value) (ctx : eval_ctx) : eval_ctx = - match try_write_place meta access p nv ctx with + match try_write_place span access p nv ctx with | Error e -> - craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e) + craise __FILE__ __LINE__ span ("Unreachable: " ^ show_path_fail_kind e) | Ok ctx -> ctx -let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) +let compute_expanded_bottom_adt_value (span : Meta.span) (ctx : eval_ctx) (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option) (generics : generic_args) : typed_value = sanity_check __FILE__ __LINE__ (TypesUtils.generic_args_only_erased_regions generics) - meta; + span; (* 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 @@ -367,22 +367,22 @@ let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) let def = ctx_lookup_type_decl ctx def_id in sanity_check __FILE__ __LINE__ (List.length generics.regions = List.length def.generics.regions) - meta; + span; (* Compute the field types *) let field_types = - AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def + AssociatedTypes.type_decl_get_inst_norm_field_etypes span ctx def opt_variant_id generics in (* Initialize the expanded value *) - let fields = List.map (mk_bottom meta) field_types in + let fields = List.map (mk_bottom span) field_types in 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 (meta : Meta.meta) +let compute_expanded_bottom_tuple_value (span : Meta.span) (field_types : ety list) : typed_value = (* Generate the field values *) - let fields = List.map (mk_bottom meta) field_types in + let fields = List.map (mk_bottom span) field_types in 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 @@ -409,7 +409,7 @@ let compute_expanded_bottom_tuple_value (meta : Meta.meta) 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 (meta : Meta.meta) +let expand_bottom_value_from_projection (span : Meta.span) (access : access_kind) (p : place) (remaining_pes : int) (pe : projection_elem) (ty : ety) (ctx : eval_ctx) : eval_ctx = (* Debugging *) @@ -438,39 +438,39 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (* "Regular" ADTs *) | ( Field (ProjAdt (def_id, opt_variant_id), _), TAdt (TAdtId def_id', generics) ) -> - sanity_check __FILE__ __LINE__ (def_id = def_id') meta; - compute_expanded_bottom_adt_value meta ctx def_id opt_variant_id + sanity_check __FILE__ __LINE__ (def_id = def_id') span; + compute_expanded_bottom_adt_value span ctx def_id opt_variant_id generics (* Tuples *) | ( Field (ProjTuple arity, _), TAdt (TTuple, { regions = []; types; const_generics = []; trait_refs = [] }) ) -> - sanity_check __FILE__ __LINE__ (arity = List.length types) meta; + sanity_check __FILE__ __LINE__ (arity = List.length types) span; (* Generate the field values *) - compute_expanded_bottom_tuple_value meta types + compute_expanded_bottom_tuple_value span types | _ -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("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 meta access p' nv ctx with + match try_write_place span access p' nv ctx with | Ok ctx -> ctx - | Error _ -> craise __FILE__ __LINE__ meta "Unreachable" + | Error _ -> craise __FILE__ __LINE__ span "Unreachable" -let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) +let rec update_ctx_along_read_place (config : config) (span : Meta.span) (access : access_kind) (p : place) : cm_fun = fun ctx -> (* Attempt to read the place: if it fails, update the environment and retry *) - match try_read_place meta access p ctx with + match try_read_place span access p ctx with | Ok _ -> (ctx, fun e -> e) | Error err -> let ctx, cc = match err with - | FailSharedLoan bids -> end_borrows config meta bids ctx - | FailMutLoan bid -> end_borrow config meta bid ctx + | FailSharedLoan bids -> end_borrows config span bids ctx + | FailMutLoan bid -> end_borrow config span bid ctx | FailReservedMutBorrow bid -> - promote_reserved_mut_borrow config meta bid ctx + promote_reserved_mut_borrow config span bid ctx | FailSymbolic (i, sp) -> (* Expand the symbolic value *) let proj, _ = @@ -478,54 +478,54 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) (List.length p.projection - i) in let prefix = { p with projection = proj } in - expand_symbolic_value_no_branching config meta sp - (Some (Synth.mk_mplace meta prefix ctx)) + expand_symbolic_value_no_branching config span sp + (Some (Synth.mk_mplace span prefix ctx)) ctx | FailBottom (_, _, _) -> (* We can't expand {!Bottom} values while reading them *) - craise __FILE__ __LINE__ meta "Found bottom while reading a place" + craise __FILE__ __LINE__ span "Found bottom while reading a place" | FailBorrow _ -> - craise __FILE__ __LINE__ meta "Could not read a borrow" + craise __FILE__ __LINE__ span "Could not read a borrow" in - comp cc (update_ctx_along_read_place config meta access p ctx) + comp cc (update_ctx_along_read_place config span access p ctx) -let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) +let rec update_ctx_along_write_place (config : config) (span : Meta.span) (access : access_kind) (p : place) : cm_fun = fun 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 try_read_place meta access p ctx with + match try_read_place span access p ctx with | Ok _ -> (ctx, fun e -> e) | Error err -> (* Update the context *) let ctx, cc = match err with - | FailSharedLoan bids -> end_borrows config meta bids ctx - | FailMutLoan bid -> end_borrow config meta bid ctx + | FailSharedLoan bids -> end_borrows config span bids ctx + | FailMutLoan bid -> end_borrow config span bid ctx | FailReservedMutBorrow bid -> - promote_reserved_mut_borrow config meta bid ctx + promote_reserved_mut_borrow config span bid ctx | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) - expand_symbolic_value_no_branching config meta sp - (Some (Synth.mk_mplace meta p ctx)) + expand_symbolic_value_no_branching config span sp + (Some (Synth.mk_mplace span p ctx)) ctx | FailBottom (remaining_pes, pe, ty) -> (* Expand the {!Bottom} value *) let ctx = - expand_bottom_value_from_projection meta access p remaining_pes pe + expand_bottom_value_from_projection span access p remaining_pes pe ty ctx in (ctx, fun e -> e) | FailBorrow _ -> - craise __FILE__ __LINE__ meta "Could not write to a borrow" + craise __FILE__ __LINE__ span "Could not write to a borrow" in (* Retry *) - comp cc (update_ctx_along_write_place config meta access p ctx) + comp cc (update_ctx_along_write_place config span access p ctx) (** Small utility used to break control-flow *) exception UpdateCtx of (eval_ctx * (eval_result -> eval_result)) -let rec end_loans_at_place (config : config) (meta : Meta.meta) +let rec end_loans_at_place (config : config) (span : Meta.span) (access : access_kind) (p : place) : cm_fun = fun ctx -> (* Iterator to explore a value and update the context whenever we find @@ -543,7 +543,7 @@ let rec end_loans_at_place (config : config) (meta : Meta.meta) (* Nothing special to do *) super#visit_borrow_content env bc | VReservedMutBorrow bid -> (* We need to activate reserved borrows *) - let res = promote_reserved_mut_borrow config meta bid ctx in + let res = promote_reserved_mut_borrow config span bid ctx in raise (UpdateCtx res) method! visit_loan_content env lc = @@ -554,17 +554,17 @@ let rec end_loans_at_place (config : config) (meta : Meta.meta) match access with | Read -> super#visit_VSharedLoan env bids v | Write | Move -> - let res = end_borrows config meta bids ctx in + let res = end_borrows config span bids ctx in raise (UpdateCtx res)) | VMutLoan bid -> (* We always need to end mutable borrows *) - let res = end_borrow config meta bid ctx in + let res = end_borrow config span bid ctx in raise (UpdateCtx res) end in (* First, retrieve the value *) - let v = read_place meta access p ctx in + let v = read_place span access p ctx in (* 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 @@ -578,16 +578,16 @@ let rec end_loans_at_place (config : config) (meta : Meta.meta) with UpdateCtx (ctx, cc) -> (* We need to update the context: compose the caugth continuation with * a recursive call to reinspect the value *) - comp cc (end_loans_at_place config meta access p ctx) + comp cc (end_loans_at_place config span access p ctx) -let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place) +let drop_outer_loans_at_lplace (config : config) (span : Meta.span) (p : place) : cm_fun = fun ctx -> (* Move the current value in the place outside of this place and into * a temporary dummy variable *) let access = Write in - let v = read_place meta access p ctx in - let ctx = write_place meta access p (mk_bottom meta v.ty) ctx in + let v = read_place span access p ctx in + let ctx = write_place span access p (mk_bottom span 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: while there are loans to end in the @@ -595,7 +595,7 @@ let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place) let rec drop : cm_fun = fun ctx -> (* Read the value *) - let v = ctx_lookup_dummy_var meta ctx dummy_id in + let v = ctx_lookup_dummy_var span ctx dummy_id in (* Check if there are loans (and only loans) to end *) let with_borrows = false in match get_first_outer_loan_or_borrow_in_value with_borrows v with @@ -607,11 +607,11 @@ let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place) let ctx, cc = match c with | LoanContent (VSharedLoan (bids, _)) -> - end_borrows config meta bids ctx - | LoanContent (VMutLoan bid) -> end_borrow config meta bid ctx + end_borrows config span bids ctx + | LoanContent (VMutLoan bid) -> end_borrow config span bid ctx | BorrowContent _ -> (* Can't get there: we are only looking up the loans *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" in (* Retry *) comp cc (drop ctx) @@ -620,29 +620,29 @@ let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place) let ctx, cc = drop ctx in (* Pop the temporary value and reinsert it *) (* Pop *) - let ctx, v = ctx_remove_dummy_var meta ctx dummy_id in + let ctx, v = ctx_remove_dummy_var span ctx dummy_id in (* Sanity check *) - sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) meta; + sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) span; (* Reinsert *) - let ctx = write_place meta access p v ctx in + let ctx = write_place span access p v ctx in (* Return *) (ctx, cc) -let prepare_lplace (config : config) (meta : Meta.meta) (p : place) +let prepare_lplace (config : config) (span : Meta.span) (p : place) (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) = log#ldebug (lazy ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Access the place *) let access = Write in - let ctx, cc = update_ctx_along_write_place config meta access p ctx in + let ctx, cc = update_ctx_along_write_place config span access p ctx in (* End the loans at the place we are about to overwrite *) - let ctx, cc = comp cc (drop_outer_loans_at_lplace config meta p ctx) in + let ctx, cc = comp cc (drop_outer_loans_at_lplace config span p ctx) in (* Read the value and check it *) - let v = read_place meta access p ctx in + let v = read_place span access p ctx in (* Sanity checks *) - sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) meta; + sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) span; (* Return *) (v, ctx, cc) |