diff options
author | Escherichia | 2024-03-12 15:02:17 +0100 |
---|---|---|
committer | Escherichia | 2024-03-28 14:59:01 +0100 |
commit | a64fdc8b1be70de43afe35ff788ba3240318daac (patch) | |
tree | 779601c91a6f034ed3e53c9d139eb9b6fdab1ba2 /compiler/InterpreterPaths.ml | |
parent | 65f7deb0043949049129c6a8e490d151b555fa16 (diff) |
WIP Beginning working on better errors: began replacing raise (Failure) and assert by craise and cassert. Does not compile yet, still need to propagate the meta variable where it's relevant
Diffstat (limited to 'compiler/InterpreterPaths.ml')
-rw-r--r-- | compiler/InterpreterPaths.ml | 123 |
1 files changed, 62 insertions, 61 deletions
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 999b8ab0..e411db9b 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -8,6 +8,7 @@ open InterpreterUtils open InterpreterBorrowsCore open InterpreterBorrows open InterpreterExpansion +open Errors module Synth = SynthesizeSymbolic (** The local logger *) @@ -68,7 +69,7 @@ type projection_access = { TODO: use exceptions? *) -let rec access_projection (access : projection_access) (ctx : eval_ctx) +let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx : eval_ctx) (* Function to (eventually) update the value we find *) (update : typed_value -> typed_value) (p : projection) (v : typed_value) : (eval_ctx * updated_read_value) path_access_result = @@ -85,10 +86,10 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) (lazy ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: " ^ show_ety v.ty)); - raise - (Failure + craise + meta "Assertion failed: new value doesn't have the same type as its \ - destination")); + destination"); Ok (ctx, { read = v; updated = nv }) | pe :: p' -> ( (* Match on the projection element and the value *) @@ -101,10 +102,10 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) | ProjAdt (def_id, opt_variant_id), TAdtId def_id' -> assert (def_id = def_id'); assert (opt_variant_id = adt.variant_id) - | _ -> raise (Failure "Unreachable")); + | _ -> craise meta "Unreachable"); (* Actually project *) let fv = FieldId.nth adt.field_values field_id in - match access_projection access ctx update p' fv with + match access_projection meta access ctx update p' fv with | Error err -> Error err | Ok (ctx, res) -> (* Update the field value *) @@ -119,7 +120,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) assert (arity = List.length adt.field_values); let fv = FieldId.nth adt.field_values field_id in (* Project *) - match access_projection access ctx update p' fv with + match access_projection meta access ctx update p' fv with | Error err -> Error err | Ok (ctx, res) -> (* Update the field value *) @@ -146,7 +147,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) * 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 + match access_projection meta access ctx update p' bv with | Error err -> Error err | Ok (ctx, res) -> let nv = @@ -163,18 +164,18 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) | VSharedBorrow bid -> (* Lookup the loan content, and explore from there *) if access.lookup_shared_borrows then - match lookup_loan ek bid ctx with + match lookup_loan meta ek bid ctx with | _, Concrete (VMutLoan _) -> - raise (Failure "Expected a shared loan") + craise meta "Expected a shared loan" | _, Concrete (VSharedLoan (bids, sv)) -> ( (* Explore the shared value *) - match access_projection access ctx update p' sv with + match access_projection meta 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 + update_loan meta ek bid (VSharedLoan (bids, res.updated)) ctx in @@ -190,22 +191,22 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } | AIgnoredSharedLoan _ ) ) -> - raise (Failure "Expected a shared (abstraction) loan") + craise meta "Expected a shared (abstraction) loan" | _, Abstract (ASharedLoan (bids, sv, _av)) -> ( (* Explore the shared value *) - match access_projection access ctx update p' sv with + match access_projection meta 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 + match lookup_loan meta ek bid ctx with | _, Abstract (ASharedLoan (_, _, av)) -> av - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in (* Update the shared loan with the new value returned by {!access_projection} *) let ctx = - update_aloan ek bid + update_aloan meta ek bid (ASharedLoan (bids, res.updated, av)) ctx in @@ -215,7 +216,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) | VReservedMutBorrow bid -> Error (FailReservedMutBorrow bid) | VMutBorrow (bid, bv) -> if access.enter_mut_borrows then - match access_projection access ctx update p' bv with + match access_projection meta access ctx update p' bv with | Error err -> Error err | Ok (ctx, res) -> let nv = @@ -231,7 +232,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) 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 + match access_projection meta access ctx update (pe :: p') sv with | Error err -> Error err | Ok (ctx, res) -> let nv = @@ -245,7 +246,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) 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")) + craise meta "Inconsistent projection") (** Generic function to access (read/write) the value at a given place. @@ -253,14 +254,14 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx) environment, if we managed to access the place, or the precise reason why we failed. *) -let access_place (access : projection_access) +let access_place (meta : Meta.meta) (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 ctx p.var_id in (* Apply the projection *) - match access_projection access ctx update p.projection value with + match access_projection meta access ctx update p.projection value with | Error err -> Error err | Ok (ctx, res) -> (* Update the value *) @@ -300,12 +301,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 (access : access_kind) (p : place) (ctx : eval_ctx) : +let try_read_place (meta : Meta.meta) (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 access update p ctx with + match access_place meta 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 @@ -318,31 +319,31 @@ let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) : ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env in log#serror msg; - raise (Failure "Unexpected environment update")); + craise meta "Unexpected environment update"); Ok read_value -let read_place (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value +let read_place (meta : Meta.meta) (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)) + match try_read_place meta access p ctx with + | Error e -> craise meta ("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 : place) (nv : typed_value) +let try_write_place (meta : Meta.meta) (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 access update p ctx with + match access_place meta access update p ctx with | Error err -> Error err | Ok (ctx, _) -> (* We ignore the read value *) Ok ctx -let write_place (access : access_kind) (p : place) (nv : typed_value) +let write_place (meta : Meta.meta) (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)) + match try_write_place meta access p nv ctx with + | Error e -> craise meta ("Unreachable: " ^ show_path_fail_kind e) | Ok ctx -> ctx let compute_expanded_bottom_adt_value (ctx : eval_ctx) (def_id : TypeDeclId.id) @@ -395,7 +396,7 @@ let compute_expanded_bottom_tuple_value (field_types : ety list) : typed_value = 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 : place) +let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind) (p : place) (remaining_pes : int) (pe : projection_elem) (ty : ety) (ctx : eval_ctx) : eval_ctx = (* Debugging *) @@ -435,20 +436,20 @@ let expand_bottom_value_from_projection (access : access_kind) (p : place) (* Generate the field values *) compute_expanded_bottom_tuple_value types | _ -> - raise - (Failure - ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty)) + craise + meta + ("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 + match try_write_place meta access p' nv ctx with | Ok ctx -> ctx - | Error _ -> raise (Failure "Unreachable") + | Error _ -> craise meta "Unreachable" -let rec update_ctx_along_read_place (config : config) (access : access_kind) +let rec update_ctx_along_read_place (meta : Meta.meta) (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 + match try_read_place meta access p ctx with | Ok _ -> cf ctx | Error err -> let cc = @@ -467,17 +468,17 @@ let rec update_ctx_along_read_place (config : config) (access : access_kind) (Some (Synth.mk_mplace prefix ctx)) | FailBottom (_, _, _) -> (* 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") + craise meta "Found [Bottom] while reading a place" + | FailBorrow _ -> craise meta "Could not read a borrow" in - comp cc (update_ctx_along_read_place config access p) cf ctx + comp cc (update_ctx_along_read_place meta config access p) cf ctx -let rec update_ctx_along_write_place (config : config) (access : access_kind) +let rec update_ctx_along_write_place (meta : Meta.meta) (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 *) - match try_read_place access p ctx with + match try_read_place meta access p ctx with | Ok _ -> cf ctx | Error err -> (* Update the context *) @@ -494,19 +495,19 @@ let rec update_ctx_along_write_place (config : config) (access : access_kind) (* Expand the {!Bottom} value *) fun cf ctx -> let ctx = - expand_bottom_value_from_projection access p remaining_pes pe ty + expand_bottom_value_from_projection meta access p remaining_pes pe ty ctx in cf ctx - | FailBorrow _ -> raise (Failure "Could not write to a borrow") + | FailBorrow _ -> craise meta "Could not write to a borrow" in (* Retry *) - comp cc (update_ctx_along_write_place config access p) cf ctx + comp cc (update_ctx_along_write_place meta config access p) cf ctx (** Small utility used to break control-flow *) exception UpdateCtx of cm_fun -let rec end_loans_at_place (config : config) (access : access_kind) (p : place) +let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access_kind) (p : place) : cm_fun = fun cf ctx -> (* Iterator to explore a value and update the context whenever we find @@ -545,7 +546,7 @@ let rec end_loans_at_place (config : config) (access : access_kind) (p : place) in (* First, retrieve the value *) - let v = read_place access p ctx in + let v = read_place meta 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 @@ -559,15 +560,15 @@ let rec end_loans_at_place (config : config) (access : access_kind) (p : place) with UpdateCtx 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 access p) cf ctx + comp cc (end_loans_at_place meta config access p) cf ctx -let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun = +let drop_outer_loans_at_lplace (meta : Meta.meta) (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.ty) ctx in + let v = read_place meta access p ctx in + let ctx = write_place meta 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 *) @@ -587,7 +588,7 @@ let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun = match c with | LoanContent (VSharedLoan (bids, _)) -> end_borrows config bids | LoanContent (VMutLoan bid) -> end_borrow config bid - | BorrowContent _ -> raise (Failure "Unreachable") + | BorrowContent _ -> craise meta "Unreachable" in (* Retry *) comp cc drop cf ctx @@ -600,7 +601,7 @@ let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun = (* Pop *) let ctx, v = ctx_remove_dummy_var ctx dummy_id in (* Reinsert *) - let ctx = write_place access p v ctx in + let ctx = write_place meta access p v ctx in (* Sanity check *) assert (not (outer_loans_in_value v)); (* Continue *) @@ -609,7 +610,7 @@ let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun = (* Continue *) cc cf ctx -let prepare_lplace (config : config) (p : place) (cf : typed_value -> m_fun) : +let prepare_lplace (meta : Meta.meta) (config : config) (p : place) (cf : typed_value -> m_fun) : m_fun = fun ctx -> log#ldebug @@ -618,13 +619,13 @@ let prepare_lplace (config : config) (p : place) (cf : typed_value -> m_fun) : ^ "\n- Initial context:\n" ^ eval_ctx_to_string ctx)); (* Access the place *) let access = Write in - let cc = update_ctx_along_write_place config access p in + let cc = update_ctx_along_write_place meta config access p in (* End the borrows and loans, starting with the borrows *) - let cc = comp cc (drop_outer_loans_at_lplace config p) in + let cc = comp cc (drop_outer_loans_at_lplace meta config p) in (* Read the value and check it *) let read_check cf : m_fun = fun ctx -> - let v = read_place access p ctx in + let v = read_place meta access p ctx in (* Sanity checks *) assert (not (outer_loans_in_value v)); (* Continue *) |