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 | |
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')
-rw-r--r-- | compiler/Config.ml | 2 | ||||
-rw-r--r-- | compiler/Errors.ml | 27 | ||||
-rw-r--r-- | compiler/InterpreterBorrows.ml | 487 | ||||
-rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 175 | ||||
-rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 85 | ||||
-rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 78 | ||||
-rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 5 | ||||
-rw-r--r-- | compiler/InterpreterPaths.ml | 123 | ||||
-rw-r--r-- | compiler/InterpreterProjectors.ml | 91 | ||||
-rw-r--r-- | compiler/InterpreterStatements.ml | 266 | ||||
-rw-r--r-- | compiler/Invariants.ml | 69 | ||||
-rw-r--r-- | compiler/Main.ml | 4 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 613 | ||||
-rw-r--r-- | compiler/Translate.ml | 82 | ||||
-rw-r--r-- | compiler/dune | 1 |
15 files changed, 1076 insertions, 1032 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 65aa7555..099cdc8b 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -318,7 +318,7 @@ let type_check_pure_code = ref false (** Shall we fail hard if we encounter an issue, or should we attempt to go as far as possible while leaving "holes" in the generated code? *) -let fail_hard = ref true +let fail_hard = ref false (** If true, add the type name as a prefix to the variant names. diff --git a/compiler/Errors.ml b/compiler/Errors.ml new file mode 100644 index 00000000..65c2cbb0 --- /dev/null +++ b/compiler/Errors.ml @@ -0,0 +1,27 @@ +let meta_to_string (span : Meta.span ) = + let file = match span.file with Virtual s | Local s -> s in + let loc_to_string (l : Meta.loc) : string = + string_of_int l.line ^ ":" ^ string_of_int l.col + in + "Source: '" ^ file ^ "', lines " ^ loc_to_string span.beg_loc ^ "-" + ^ loc_to_string span.end_loc + +let format_error_message (meta : Meta.meta) msg = + msg ^ ":" ^ meta_to_string meta.span + +exception CFailure of string + + +let error_list : (Meta.meta * string) list ref = ref [] +let save_error (meta : Meta.meta ) (msg : string) = error_list := (meta, msg)::(!error_list) + +let craise (meta : Meta.meta) (msg : string) = + if !Config.fail_hard then + raise (Failure (format_error_message meta msg)) + else + let () = save_error meta msg in + raise (CFailure msg) + +let cassert (b : bool) (meta : Meta.meta) (msg : string) = + if b then + craise meta msg
\ No newline at end of file diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 17810705..ae251fbf 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -7,6 +7,7 @@ open TypesUtils open InterpreterUtils open InterpreterBorrowsCore open InterpreterProjectors +open Errors (** The local logger *) let log = Logging.borrows_log @@ -29,7 +30,7 @@ let log = Logging.borrows_log loans. This is used to merge borrows with abstractions, to compute loop fixed points for instance. *) -let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) +let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id option) (allow_inner_loans : bool) (l : BorrowId.id) (ctx : eval_ctx) : ( eval_ctx * (AbstractionId.id option * g_borrow_content) option, priority_borrows_or_abs ) @@ -41,7 +42,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) in let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content) = - assert (Option.is_none !replaced_bc); + cassert (Option.is_none !replaced_bc) meta "TODO: error message"; replaced_bc := Some (abs_id, bc) in (* Raise an exception if: @@ -180,7 +181,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) * Also note that, as we are moving the borrowed value inside the * abstraction (and not really giving the value back to the context) * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *) - raise (Failure "Unimplemented") + craise meta "Unimplemented" (* ABottom *)) else (* Update the outer borrows before diving into the child avalue *) @@ -223,8 +224,8 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) method! visit_abs outer abs = (* Update the outer abs *) let outer_abs, outer_borrows = outer in - assert (Option.is_none outer_abs); - assert (Option.is_none outer_borrows); + cassert (Option.is_none outer_abs) meta "TODO: error message"; + cassert (Option.is_none outer_borrows) meta "TODO: error message"; let outer = (Some abs.abs_id, None) in super#visit_abs outer abs end @@ -244,11 +245,11 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) give the value back. TODO: this was not the case before, so some sanity checks are not useful anymore. *) -let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) +let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv : typed_value) (ctx : eval_ctx) : eval_ctx = (* Sanity check *) - assert (not (loans_in_value nv)); - assert (not (bottom_in_value ctx.ended_regions nv)); + cassert (not (loans_in_value nv)) meta "TODO: error message"; + cassert (not (bottom_in_value ctx.ended_regions nv)) meta "TODO: error message"; (* Debug *) log#ldebug (lazy @@ -258,7 +259,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - assert (not !replaced); + cassert (not !replaced) meta "Exactly one loan should have been updated"; replaced := true in (* Whenever giving back symbolic values, they shouldn't contain already ended regions *) @@ -300,7 +301,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) ("give_back_value: improper type:\n- expected: " ^ ty_to_string ctx ty ^ "\n- received: " ^ ty_to_string ctx nv.ty); - raise (Failure "Value given back doesn't have the proper type")); + craise meta "Value given back doesn't have the proper type"); (* Replace *) set_replaced (); nv.value) @@ -345,7 +346,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) ABorrow (AEndedIgnoredMutBorrow { given_back; child; given_back_meta }) - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" else (* Continue exploring *) ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child) @@ -360,7 +361,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* Preparing a bit *) let regions, ancestors_regions = match opt_abs with - | None -> raise (Failure "Unreachable") + | None -> craise meta "Unreachable" | Some abs -> (abs.regions, abs.ancestors_regions) in (* Rk.: there is a small issue with the types of the aloan values. @@ -426,7 +427,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* We remember in which abstraction we are before diving - * this is necessary for projecting values: we need to know * over which regions to project *) - assert (Option.is_none opt_abs); + cassert (Option.is_none opt_abs) meta "TODO: error message"; super#visit_EAbs (Some abs) abs end in @@ -434,16 +435,16 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - assert !replaced; + cassert !replaced meta "Only one loan should have been given back"; (* Apply the reborrows *) apply_registered_reborrows ctx (** Give back a *modified* symbolic value. *) -let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) +let give_back_symbolic_value (meta : Meta.meta) (_config : config) (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Sanity checks *) - assert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty); + cassert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta "TODO: error message"; (* Store the given-back value as a meta-value for synthesis purposes *) let mv = nsv in (* Substitution function, to replace the borrow projectors over symbolic values *) @@ -465,11 +466,11 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) type [T]! We thus *mustn't* introduce a projector here. *) (* AProjBorrows (nsv, sv.sv_ty) *) - raise (Failure "TODO") + craise meta "TODO: error message" in AProjLoans (sv, (mv, child_proj) :: local_given_back) in - update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx + update_intersecting_aproj_loans meta proj_regions proj_ty sv subst ctx (** Auxiliary function to end borrows. See {!give_back}. @@ -484,12 +485,12 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) end abstraction when ending this abstraction. When doing this, we need to convert the {!avalue} to a {!type:value} by introducing the proper symbolic values. *) -let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) +let give_back_avalue_to_same_abstraction (meta : Meta.meta) (_config : config) (bid : BorrowId.id) (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - assert (not !replaced); + cassert (not !replaced) meta "Only one loan should have been updated"; replaced := true in let obj = @@ -532,7 +533,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) ("give_back_avalue_to_same_abstraction: improper type:\n\ - expected: " ^ ty_to_string ctx ty ^ "\n- received: " ^ ty_to_string ctx nv.ty); - raise (Failure "Value given back doesn't have the proper type")); + craise meta "Value given back doesn't have the proper type"); (* This is the loan we are looking for: apply the projection to * the value we give back and replaced this mutable loan with * an ended loan *) @@ -558,7 +559,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) * we don't register the fact that we inserted the value somewhere * (i.e., we don't call {!set_replaced}) *) (* Sanity check *) - assert (nv.ty = ty); + cassert (nv.ty = ty) meta "TODO: error message"; ALoan (AEndedIgnoredMutLoan { given_back = nv; child; given_back_meta = nsv })) @@ -574,7 +575,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - assert !replaced; + cassert !replaced meta "Only one loan should be given back"; (* Return *) ctx @@ -587,11 +588,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) we update. TODO: this was not the case before, so some sanity checks are not useful anymore. *) -let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = +let give_back_shared (meta : Meta.meta) _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - assert (not !replaced); + cassert (not !replaced) meta "Only one loan should be updated"; replaced := true in let obj = @@ -656,7 +657,7 @@ let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - assert !replaced; + cassert !replaced meta "Exactly one loan should be given back"; (* Return *) ctx @@ -665,12 +666,12 @@ let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = to an environment by inserting a new borrow id in the set of borrows tracked by a shared value, referenced by the [original_bid] argument. *) -let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id) +let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = (* Keep track of changes *) let r = ref false in let set_ref () = - assert (not !r); + cassert (not !r) meta "TODO: error message"; r := true in @@ -700,7 +701,7 @@ let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id) let env = obj#visit_env () ctx.env in (* Check that we reborrowed once *) - assert !r; + cassert !r meta "Not reborrowed once"; { ctx with env } (** Convert an {!type:avalue} to a {!type:value}. @@ -738,7 +739,7 @@ let convert_avalue_to_given_back_value (av : typed_avalue) : symbolic_value = borrows. This kind of internal reshuffling. should be similar to ending abstractions (it is tantamount to ending *sub*-abstractions). *) -let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content) +let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_borrow_content) (ctx : eval_ctx) : eval_ctx = (* Debug *) log#ldebug @@ -757,24 +758,24 @@ let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content) match bc with | Concrete (VMutBorrow (l', tv)) -> (* Sanity check *) - assert (l' = l); - assert (not (loans_in_value tv)); + cassert (l' = l) meta "TODO: error message"; + cassert (not (loans_in_value tv)) meta "TODO: error message"; (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere"; (* Update the context *) - give_back_value config l tv ctx + give_back_value meta config l tv ctx | Concrete (VSharedBorrow l' | VReservedMutBorrow l') -> (* Sanity check *) - assert (l' = l); + cassert (l' = l) meta "TODO: error message"; (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere"; (* Update the context *) - give_back_shared config l ctx + give_back_shared meta config l ctx | Abstract (AMutBorrow (l', av)) -> (* Sanity check *) - assert (l' = l); + cassert (l' = l) meta "TODO: error message"; (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere"; (* Convert the avalue to a (fresh symbolic) value. Rem.: we shouldn't do this here. We should do this in a function @@ -782,27 +783,27 @@ let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content) *) let sv = convert_avalue_to_given_back_value av in (* Update the context *) - give_back_avalue_to_same_abstraction config l av + give_back_avalue_to_same_abstraction meta config l av (mk_typed_value_from_symbolic_value sv) ctx | Abstract (ASharedBorrow l') -> (* Sanity check *) - assert (l' = l); + cassert (l' = l) meta "TODO: error message"; (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere"; (* Update the context *) - give_back_shared config l ctx + give_back_shared meta config l ctx | Abstract (AProjSharedBorrow asb) -> (* Sanity check *) - assert (borrow_in_asb l asb); + cassert (borrow_in_asb l asb) meta "TODO: error message"; (* Update the context *) - give_back_shared config l ctx + give_back_shared meta config l ctx | Abstract ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow ) -> - raise (Failure "Unreachable") + craise meta "Unreachable" -let check_borrow_disappeared (fun_name : string) (l : BorrowId.id) +let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowId.id) (ctx0 : eval_ctx) : cm_fun = let check_disappeared (ctx : eval_ctx) : unit = let _ = @@ -815,9 +816,9 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id) ^ ": borrow didn't disappear:\n- original context:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)); - raise (Failure "Borrow not eliminated") + craise meta "Borrow not eliminated" in - match lookup_loan_opt ek_all l ctx with + match lookup_loan_opt meta ek_all l ctx with | None -> () (* Ok *) | Some _ -> log#lerror @@ -826,7 +827,7 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id) ^ ": loan didn't disappear:\n- original context:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)); - raise (Failure "Loan not eliminated") + craise meta "Loan not eliminated" in unit_to_cm_fun check_disappeared @@ -851,7 +852,7 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id) perform anything smart and is trusted, and another function for the book-keeping. *) -let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) +let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun = fun cf ctx -> (* Check that we don't loop *) @@ -867,10 +868,10 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) (* Utility function for the sanity checks: check that the borrow disappeared * from the context *) let ctx0 = ctx in - let cf_check : cm_fun = check_borrow_disappeared "end borrow" l ctx0 in + let cf_check : cm_fun = check_borrow_disappeared meta "end borrow" l ctx0 in (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *) let allow_inner_loans = false in - match end_borrow_get_borrow allowed_abs allow_inner_loans l ctx with + match end_borrow_get_borrow meta allowed_abs allow_inner_loans l ctx with (* Two cases: - error: we found outer borrows (the borrow is inside a borrowed value) or inner loans (the borrow contains loans) @@ -899,29 +900,29 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) * inside another borrow *) let allowed_abs' = None in (* End the outer borrows *) - let cc = end_borrows_aux config chain allowed_abs' bids in + let cc = end_borrows_aux meta config chain allowed_abs' bids in (* Retry to end the borrow *) - let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in + let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in (* Check and apply *) comp cc cf_check cf ctx | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) -> let allowed_abs' = None in (* End the outer borrow *) - let cc = end_borrow_aux config chain allowed_abs' bid in + let cc = end_borrow_aux meta config chain allowed_abs' bid in (* Retry to end the borrow *) - let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in + let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in (* Check and apply *) comp cc cf_check cf ctx | OuterAbs abs_id -> (* The borrow is inside an abstraction: end the whole abstraction *) - let cf_end_abs = end_abstraction_aux config chain abs_id in + let cf_end_abs = end_abstraction_aux meta config chain abs_id in (* Compose with a sanity check *) comp cf_end_abs cf_check cf ctx) | Ok (ctx, None) -> log#ldebug (lazy "End borrow: borrow not found"); (* It is possible that we can't find a borrow in symbolic mode (ending * an abstraction may end several borrows at once *) - assert (config.mode = SymbolicMode); + cassert (config.mode = SymbolicMode) meta "Borrow should be in symbolic mode"; (* Do a sanity check and continue *) cf_check cf ctx (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update @@ -930,10 +931,10 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) (* Sanity check: the borrowed value shouldn't contain loans *) (match bc with | Concrete (VMutBorrow (_, bv)) -> - assert (Option.is_none (get_first_loan_in_value bv)) + cassert (Option.is_none (get_first_loan_in_value bv)) meta "Borrowed value shouldn't contain loans" | _ -> ()); (* Give back the value *) - let ctx = give_back config l bc ctx in + let ctx = give_back meta config l bc ctx in (* Do a sanity check and continue *) let cc = cf_check in (* Save a snapshot of the environment for the name generation *) @@ -941,7 +942,7 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) (* Compose *) cc cf ctx -and end_borrows_aux (config : config) (chain : borrow_or_abs_ids) +and end_borrows_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun = fun cf -> (* This is not necessary, but we prefer to reorder the borrow ids, @@ -949,10 +950,10 @@ and end_borrows_aux (config : config) (chain : borrow_or_abs_ids) * a matter of taste, and may make debugging easier *) let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in List.fold_left - (fun cf id -> end_borrow_aux config chain allowed_abs id cf) + (fun cf id -> end_borrow_aux meta config chain allowed_abs id cf) cf ids -and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) +and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun cf ctx -> (* Check that we don't loop *) @@ -983,14 +984,14 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) (* Check that we can end the abstraction *) if abs.can_end then () else - raise - (Failure + craise + meta ("Can't end abstraction " ^ AbstractionId.to_string abs.abs_id - ^ " as it is set as non-endable")); + ^ " as it is set as non-endable"); (* End the parent abstractions first *) - let cc = end_abstractions_aux config chain abs.parents in + let cc = end_abstractions_aux meta config chain abs.parents in let cc = comp_unit cc (fun ctx -> log#ldebug @@ -1002,7 +1003,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) in (* End the loans inside the abstraction *) - let cc = comp cc (end_abstraction_loans config chain abs_id) in + let cc = comp cc (end_abstraction_loans meta config chain abs_id) in let cc = comp_unit cc (fun ctx -> log#ldebug @@ -1013,7 +1014,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) in (* End the abstraction itself by redistributing the borrows it contains *) - let cc = comp cc (end_abstraction_borrows config chain abs_id) in + let cc = comp cc (end_abstraction_borrows meta config chain abs_id) in (* End the regions owned by the abstraction - note that we don't need to * relookup the abstraction: the set of regions in an abstraction never @@ -1043,7 +1044,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) in (* Sanity check: ending an abstraction must preserve the invariants *) - let cc = comp cc Invariants.cf_check_invariants in + let cc = comp cc (Invariants.cf_check_invariants meta) in (* Save a snapshot of the environment for the name generation *) let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in @@ -1051,7 +1052,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) (* Apply the continuation *) cc cf ctx -and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids) +and end_abstractions_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids) (abs_ids : AbstractionId.Set.t) : cm_fun = fun cf -> (* This is not necessary, but we prefer to reorder the abstraction ids, @@ -1059,10 +1060,10 @@ and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids) * a matter of taste, and may make debugging easier *) let abs_ids = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in List.fold_left - (fun cf id -> end_abstraction_aux config chain id cf) + (fun cf id -> end_abstraction_aux meta config chain id cf) cf abs_ids -and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids) +and end_abstraction_loans (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun cf ctx -> (* Lookup the abstraction *) @@ -1071,7 +1072,7 @@ and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids) * * We ignore the "ignored mut/shared loans": as we should have already ended * the parent abstractions, they necessarily come from children. *) - let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in + let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in match opt_loan with | None -> (* No loans: nothing to update *) @@ -1080,23 +1081,23 @@ and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids) (* There are loans: end the corresponding borrows, then recheck *) let cc : cm_fun = match bids with - | Borrow bid -> end_borrow_aux config chain None bid - | Borrows bids -> end_borrows_aux config chain None bids + | Borrow bid -> end_borrow_aux meta config chain None bid + | Borrows bids -> end_borrows_aux meta config chain None bids in (* Reexplore, looking for loans *) - let cc = comp cc (end_abstraction_loans config chain abs_id) in + let cc = comp cc (end_abstraction_loans meta config chain abs_id) in (* Continue *) cc cf ctx | Some (SymbolicValue sv) -> (* There is a proj_loans over a symbolic value: end the proj_borrows * which intersect this proj_loans, then end the proj_loans itself *) - let cc = end_proj_loans_symbolic config chain abs_id abs.regions sv in + let cc = end_proj_loans_symbolic meta config chain abs_id abs.regions sv in (* Reexplore, looking for loans *) - let cc = comp cc (end_abstraction_loans config chain abs_id) in + let cc = comp cc (end_abstraction_loans meta config chain abs_id) in (* Continue *) cc cf ctx -and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) +and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun cf ctx -> log#ldebug @@ -1147,7 +1148,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) method! visit_aproj env sproj = (match sproj with - | AProjLoans _ -> raise (Failure "Unexpected") + | AProjLoans _ -> craise meta "Unexpected" | AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty)) | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj env sproj @@ -1156,7 +1157,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) method! visit_borrow_content _ bc = match bc with | VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc) - | VReservedMutBorrow _ -> raise (Failure "Unreachable") + | VReservedMutBorrow _ -> craise meta "Unreachable" end in (* Lookup the abstraction *) @@ -1181,16 +1182,16 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) (* Replace the mut borrow to register the fact that we ended * it and store with it the freshly generated given back value *) let ended_borrow = ABorrow (AEndedMutBorrow (sv, av)) in - let ctx = update_aborrow ek_all bid ended_borrow ctx in + let ctx = update_aborrow meta ek_all bid ended_borrow ctx in (* Give the value back *) let sv = mk_typed_value_from_symbolic_value sv in - give_back_value config bid sv ctx + give_back_value meta config bid sv ctx | ASharedBorrow bid -> (* Replace the shared borrow to account for the fact it ended *) let ended_borrow = ABorrow AEndedSharedBorrow in - let ctx = update_aborrow ek_all bid ended_borrow ctx in + let ctx = update_aborrow meta ek_all bid ended_borrow ctx in (* Give back *) - give_back_shared config bid ctx + give_back_shared meta config bid ctx | AProjSharedBorrow asb -> (* Retrieve the borrow ids *) let bids = @@ -1205,21 +1206,21 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) * can use to identify the whole set *) let repr_bid = List.hd bids in (* Replace the shared borrow with Bottom *) - let ctx = update_aborrow ek_all repr_bid ABottom ctx in + let ctx = update_aborrow meta ek_all repr_bid ABottom ctx in (* Give back the shared borrows *) let ctx = List.fold_left - (fun ctx bid -> give_back_shared config bid ctx) + (fun ctx bid -> give_back_shared meta config bid ctx) ctx bids in (* Continue *) ctx | AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow -> - raise (Failure "Unexpected") + craise meta "Unexpected" in (* Reexplore *) - end_abstraction_borrows config chain abs_id cf ctx + end_abstraction_borrows meta config chain abs_id cf ctx (* There are symbolic borrows: end them, then reexplore *) | FoundAProjBorrows (sv, proj_ty) -> log#ldebug @@ -1230,13 +1231,13 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) let nsv = mk_fresh_symbolic_value proj_ty in (* Replace the proj_borrows - there should be exactly one *) let ended_borrow = AEndedProjBorrows nsv in - let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in + let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in (* Give back the symbolic value *) let ctx = - give_back_symbolic_value config abs.regions proj_ty sv nsv ctx + give_back_symbolic_value meta config abs.regions proj_ty sv nsv ctx in (* Reexplore *) - end_abstraction_borrows config chain abs_id cf ctx + end_abstraction_borrows meta config chain abs_id cf ctx (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *) | FoundBorrowContent bc -> log#ldebug @@ -1249,27 +1250,27 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) (* Replace the shared borrow with bottom *) let allow_inner_loans = false in match - end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx + end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx with - | Error _ -> raise (Failure "Unreachable") + | Error _ -> craise meta "Unreachable" | Ok (ctx, _) -> (* Give back *) - give_back_shared config bid ctx) + give_back_shared meta config bid ctx) | VMutBorrow (bid, v) -> ( (* Replace the mut borrow with bottom *) let allow_inner_loans = false in match - end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx + end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx with - | Error _ -> raise (Failure "Unreachable") + | Error _ -> craise meta "Unreachable" | Ok (ctx, _) -> (* Give the value back - note that the mut borrow was below a * shared borrow: the value is thus unchanged *) - give_back_value config bid v ctx) - | VReservedMutBorrow _ -> raise (Failure "Unreachable") + give_back_value meta config bid v ctx) + | VReservedMutBorrow _ -> craise meta "Unreachable" in (* Reexplore *) - end_abstraction_borrows config chain abs_id cf ctx + end_abstraction_borrows meta config chain abs_id cf ctx (** Remove an abstraction from the context, as well as all its references *) and end_abstraction_remove_from_context (_config : config) @@ -1296,12 +1297,12 @@ and end_abstraction_remove_from_context (_config : config) intersecting proj_borrows, either in the concrete context or in an abstraction *) -and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids) +and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value) : cm_fun = fun cf ctx -> (* Small helpers for sanity checks *) - let check ctx = no_aproj_over_symbolic_in_context sv ctx in + let check ctx = no_aproj_over_symbolic_in_context meta sv ctx in let cf_check (cf : m_fun) : m_fun = fun ctx -> check ctx; @@ -1309,13 +1310,13 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids) in (* Find the first proj_borrows which intersects the proj_loans *) let explore_shared = true in - match lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx with + match lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx with | None -> (* We couldn't find any in the context: it means that the symbolic value * is in the concrete environment (or that we dropped it, in which case * it is completely absent). We thus simply need to replace the loans * projector with an ended projector. *) - let ctx = update_aproj_loans_to_ended abs_id sv ctx in + let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in (* Sanity check *) check ctx; (* Continue *) @@ -1359,15 +1360,15 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids) AbstractionId.Set.empty abs_ids in (* End the abstractions and continue *) - end_abstractions_aux config chain abs_ids cf ctx + end_abstractions_aux meta config chain abs_ids cf ctx in (* End the internal borrows projectors and the loans projector *) let cf_end_internal : cm_fun = fun cf ctx -> (* All the proj_borrows are owned: simply erase them *) - let ctx = remove_intersecting_aproj_borrows_shared regions sv ctx in + let ctx = remove_intersecting_aproj_borrows_shared meta regions sv ctx in (* End the loan itself *) - let ctx = update_aproj_loans_to_ended abs_id sv ctx in + let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in (* Sanity check *) check ctx; (* Continue *) @@ -1399,48 +1400,48 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids) *) (* End the projector of borrows - TODO: not completely sure what to * replace it with... Maybe we should introduce an ABottomProj? *) - let ctx = update_aproj_borrows abs_id sv AIgnoredProjBorrows ctx in + let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in (* Sanity check: no other occurrence of an intersecting projector of borrows *) - assert ( + cassert ( Option.is_none - (lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx)); + (lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx)) meta "no other occurrence of an intersecting projector of borrows"; (* End the projector of loans *) - let ctx = update_aproj_loans_to_ended abs_id sv ctx in + let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in (* Sanity check *) check ctx; (* Continue *) cf ctx) else (* The borrows proj comes from a different abstraction: end it. *) - let cc = end_abstraction_aux config chain abs_id' in + let cc = end_abstraction_aux meta config chain abs_id' in (* Retry ending the projector of loans *) let cc = - comp cc (end_proj_loans_symbolic config chain abs_id regions sv) + comp cc (end_proj_loans_symbolic meta config chain abs_id regions sv) in (* Sanity check *) let cc = comp cc cf_check in (* Continue *) cc cf ctx -let end_borrow config : BorrowId.id -> cm_fun = end_borrow_aux config [] None +let end_borrow (meta : Meta.meta ) config : BorrowId.id -> cm_fun = end_borrow_aux meta config [] None -let end_borrows config : BorrowId.Set.t -> cm_fun = - end_borrows_aux config [] None +let end_borrows (meta : Meta.meta ) config : BorrowId.Set.t -> cm_fun = + end_borrows_aux meta config [] None -let end_abstraction config = end_abstraction_aux config [] -let end_abstractions config = end_abstractions_aux config [] +let end_abstraction meta config = end_abstraction_aux meta config [] +let end_abstractions meta config = end_abstractions_aux meta config [] -let end_borrow_no_synth config id ctx = - get_cf_ctx_no_synth (end_borrow config id) ctx +let end_borrow_no_synth meta config id ctx = + get_cf_ctx_no_synth (end_borrow meta config id) ctx -let end_borrows_no_synth config ids ctx = - get_cf_ctx_no_synth (end_borrows config ids) ctx +let end_borrows_no_synth meta config ids ctx = + get_cf_ctx_no_synth (end_borrows meta config ids) ctx -let end_abstraction_no_synth config id ctx = - get_cf_ctx_no_synth (end_abstraction config id) ctx +let end_abstraction_no_synth meta config id ctx = + get_cf_ctx_no_synth (end_abstraction meta config id) ctx -let end_abstractions_no_synth config ids ctx = - get_cf_ctx_no_synth (end_abstractions config ids) ctx +let end_abstractions_no_synth meta config ids ctx = + get_cf_ctx_no_synth (end_abstractions meta config ids) ctx (** Helper function: see {!activate_reserved_mut_borrow}. @@ -1458,7 +1459,7 @@ let end_abstractions_no_synth config ids ctx = The loan to update mustn't be a borrowed value. *) -let promote_shared_loan_to_mut_loan (l : BorrowId.id) +let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) (cf : typed_value -> m_fun) : m_fun = fun ctx -> (* Debug *) @@ -1473,38 +1474,38 @@ let promote_shared_loan_to_mut_loan (l : BorrowId.id) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - match lookup_loan ek l ctx with + match lookup_loan meta ek l ctx with | _, Concrete (VMutLoan _) -> - raise (Failure "Expected a shared loan, found a mut loan") + craise meta "Expected a shared loan, found a mut loan" | _, Concrete (VSharedLoan (bids, sv)) -> (* Check that there is only one borrow id (l) and update the loan *) - assert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1); + cassert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1) meta "There should only be one borrow id"; (* We need to check that there aren't any loans in the value: we should have gotten rid of those already, but it is better to do a sanity check. *) - assert (not (loans_in_value sv)); + cassert (not (loans_in_value sv)) meta "There shouldn't be any loans in the value"; (* Check there isn't {!Bottom} (this is actually an invariant *) - assert (not (bottom_in_value ctx.ended_regions sv)); + cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a !Bottom"; (* Check there aren't reserved borrows *) - assert (not (reserved_in_value sv)); + cassert (not (reserved_in_value sv)) meta "There shouldn't have reserved borrows"; (* Update the loan content *) - let ctx = update_loan ek l (VMutLoan l) ctx in + let ctx = update_loan meta ek l (VMutLoan l) ctx in (* Continue *) cf sv ctx | _, Abstract _ -> (* I don't think it is possible to have two-phase borrows involving borrows * returned by abstractions. I'm not sure how we could handle that anyway. *) - raise - (Failure + craise + meta "Can't promote a shared loan to a mutable loan if the loan is \ - inside an abstraction") + inside an abstraction" (** Helper function: see {!activate_reserved_mut_borrow}. This function updates a shared borrow to a mutable borrow (and that is all: it doesn't touch the corresponding loan). *) -let replace_reserved_borrow_with_mut_borrow (l : BorrowId.id) (cf : m_fun) +let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) (cf : m_fun) (borrowed_value : typed_value) : m_fun = fun ctx -> (* Lookup the reserved borrow - note that we don't go inside borrows/loans: @@ -1514,32 +1515,32 @@ let replace_reserved_borrow_with_mut_borrow (l : BorrowId.id) (cf : m_fun) { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } in let ctx = - match lookup_borrow ek l ctx with + match lookup_borrow meta ek l ctx with | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) -> - raise (Failure "Expected a reserved mutable borrow") + craise meta "Expected a reserved mutable borrow" | Concrete (VReservedMutBorrow _) -> (* Update it *) - update_borrow ek l (VMutBorrow (l, borrowed_value)) ctx + update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx | Abstract _ -> (* This can't happen for sure *) - raise - (Failure + craise + meta "Can't promote a shared borrow to a mutable borrow if the borrow \ - is inside an abstraction") + is inside an abstraction" in (* Continue *) cf ctx (** Promote a reserved mut borrow to a mut borrow. *) -let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun +let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : BorrowId.id) : cm_fun = fun cf ctx -> (* Lookup the value *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - match lookup_loan ek l ctx with - | _, Concrete (VMutLoan _) -> raise (Failure "Unreachable") + match lookup_loan meta ek l ctx with + | _, Concrete (VMutLoan _) -> craise meta "Unreachable" | _, Concrete (VSharedLoan (bids, sv)) -> ( (* If there are loans inside the value, end them. Note that there can't be reserved borrows inside the value. @@ -1549,11 +1550,11 @@ let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun (* End the loans *) let cc = match lc with - | VSharedLoan (bids, _) -> end_borrows config bids - | VMutLoan bid -> end_borrow config bid + | VSharedLoan (bids, _) -> end_borrows meta config bids + | VMutLoan bid -> end_borrow meta config bid in (* Recursive call *) - let cc = comp cc (promote_reserved_mut_borrow config l) in + let cc = comp cc (promote_reserved_mut_borrow meta config l) in (* Continue *) cc cf ctx | None -> @@ -1563,36 +1564,36 @@ let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun (lazy ("activate_reserved_mut_borrow: resulting value:\n" ^ typed_value_to_string ctx sv)); - assert (not (loans_in_value sv)); - assert (not (bottom_in_value ctx.ended_regions sv)); - assert (not (reserved_in_value sv)); + cassert (not (loans_in_value sv)) meta "TODO: error message"; + cassert (not (bottom_in_value ctx.ended_regions sv)) meta "TODO: error message"; + cassert (not (reserved_in_value sv)) meta "TODO: error message"; (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) let bids = BorrowId.Set.remove l bids in - let cc = end_borrows config bids in + let cc = end_borrows meta config bids in (* Promote the loan - TODO: this will fail if the value contains * any loans. In practice, it shouldn't, but we could also * look for loans inside the value and end them before promoting * the borrow. *) - let cc = comp cc (promote_shared_loan_to_mut_loan l) in + let cc = comp cc (promote_shared_loan_to_mut_loan meta l) in (* Promote the borrow - the value should have been checked by {!promote_shared_loan_to_mut_loan} *) let cc = comp cc (fun cf borrowed_value -> - replace_reserved_borrow_with_mut_borrow l cf borrowed_value) + replace_reserved_borrow_with_mut_borrow meta l cf borrowed_value) in (* Continue *) cc cf ctx) | _, Abstract _ -> (* I don't think it is possible to have two-phase borrows involving borrows * returned by abstractions. I'm not sure how we could handle that anyway. *) - raise - (Failure + craise + meta "Can't activate a reserved mutable borrow referencing a loan inside\n\ - \ an abstraction") + \ an abstraction" -let destructure_abs (abs_kind : abs_kind) (can_end : bool) +let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs = (* Accumulator to store the destructured values *) let avalues = ref [] in @@ -1605,7 +1606,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) ignore the children altogether. Instead, we explore them and make sure we don't register values while doing so. *) - let push_fail _ = raise (Failure "Unreachable") in + let push_fail _ = craise meta "Unreachable" in (* Function to explore an avalue and destructure it *) let rec list_avalues (allow_borrows : bool) (push : typed_avalue -> unit) (av : typed_avalue) : unit = @@ -1620,7 +1621,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) match lc with | ASharedLoan (bids, sv, child_av) -> (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.value)); + cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet"; (* Destructure the shared value *) let avl, sv = if destructure_shared_values then list_values sv else ([], sv) @@ -1647,8 +1648,8 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) push { value; ty } | AIgnoredMutLoan (opt_bid, child_av) -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); - assert (opt_bid = None); + cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet"; + cassert (opt_bid = None) meta "TODO: error message"; (* Simply explore the child *) list_avalues false push_fail child_av | AEndedMutLoan @@ -1658,12 +1659,12 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) { child = child_av; given_back = _; given_back_meta = _ } | AIgnoredSharedLoan child_av -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); + cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet"; (* Simply explore the child *) list_avalues false push_fail child_av) | ABorrow bc -> ( (* Sanity check - rem.: may be redundant with [push_fail] *) - assert allow_borrows; + cassert allow_borrows meta "TODO: error message"; (* Explore the borrow content *) match bc with | AMutBorrow (bid, child_av) -> @@ -1678,19 +1679,19 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) push av | AIgnoredMutBorrow (opt_bid, child_av) -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); - assert (opt_bid = None); + cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet"; + cassert (opt_bid = None) meta "TODO: error message"; (* Just explore the child *) list_avalues false push_fail child_av | AEndedIgnoredMutBorrow { child = child_av; given_back = _; given_back_meta = _ } -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); + cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet"; (* Just explore the child *) list_avalues false push_fail child_av | AProjSharedBorrow asb -> (* We don't support nested borrows *) - assert (asb = []); + cassert (asb = []) meta "Nested borrows are not supported yet"; (* Nothing specific to do *) () | AEndedMutBorrow _ | AEndedSharedBorrow -> @@ -1698,11 +1699,11 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) be in the context anymore (if we end *one* borrow in an abstraction, we have to end them all and remove the abstraction from the context) *) - raise (Failure "Unreachable")) + craise meta "Unreachable") | ASymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) + cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message" and list_values (v : typed_value) : typed_avalue list * typed_value = let ty = v.ty in match v.value with @@ -1714,19 +1715,19 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) let avl = List.concat avll in let adt = { adt with field_values } in (avl, { v with value = VAdt adt }) - | VBottom -> raise (Failure "Unreachable") + | VBottom -> craise meta "Unreachable" | VBorrow _ -> (* We don't support nested borrows for now *) - raise (Failure "Unreachable") + craise meta "Unreachable" | VLoan lc -> ( match lc with | VSharedLoan (bids, sv) -> let avl, sv = list_values sv in if destructure_shared_values then ( (* Rem.: the shared value can't contain loans nor borrows *) - assert (ty_no_regions ty); + cassert (ty_no_regions ty) meta "The shared value can't contain loans nor borrows"; let av : typed_avalue = - assert (not (value_has_loans_or_borrows ctx sv.value)); + cassert (not (value_has_loans_or_borrows ctx sv.value)) meta "The shared value can't contain loans nor borrows"; (* We introduce fresh ids for the symbolic values *) let mk_value_with_fresh_sids (v : typed_value) : typed_value = let visitor = @@ -1747,11 +1748,11 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) let avl = List.append [ av ] avl in (avl, sv)) else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) }) - | VMutLoan _ -> raise (Failure "Unreachable")) + | VMutLoan _ -> craise meta "Unreachable") | VSymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos ty)); + cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message"; ([], v) in @@ -1761,14 +1762,14 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) (* Update *) { abs0 with avalues; kind = abs_kind; can_end } -let abs_is_destructured (destructure_shared_values : bool) (ctx : eval_ctx) +let abs_is_destructured (meta : Meta.meta) (destructure_shared_values : bool) (ctx : eval_ctx) (abs : abs) : bool = let abs' = - destructure_abs abs.kind abs.can_end destructure_shared_values ctx abs + destructure_abs meta abs.kind abs.can_end destructure_shared_values ctx abs in abs = abs' -let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) +let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (destructure_shared_values : bool) (ctx : eval_ctx) (v : typed_value) : abs list = (* Convert the value to a list of avalues *) @@ -1851,20 +1852,20 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) (avl, { v with value = VAdt adt }) | VBorrow bc -> ( let _, ref_ty, kind = ty_as_ref ty in - assert (ty_no_regions ref_ty); + cassert (ty_no_regions ref_ty) meta "TODO: error message"; (* Sanity check *) - assert allow_borrows; + cassert allow_borrows meta "TODO: error message"; (* Convert the borrow content *) match bc with | VSharedBorrow bid -> - assert (ty_no_regions ref_ty); + cassert (ty_no_regions ref_ty) meta "TODO: error message"; let ty = TRef (RFVar r_id, ref_ty, kind) in let value = ABorrow (ASharedBorrow bid) in ([ { value; ty } ], v) | VMutBorrow (bid, bv) -> let r_id = if group then r_id else fresh_region_id () in (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx bv.value)); + cassert (not (value_has_borrows ctx bv.value)) meta "Nested borrows are not supported yet"; (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *) let ty = TRef (RFVar r_id, ref_ty, kind) in let ignored = mk_aignored ref_ty in @@ -1877,16 +1878,16 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) (av :: avl, value) | VReservedMutBorrow _ -> (* This borrow should have been activated *) - raise (Failure "Unexpected")) + craise meta "Unexpected") | VLoan lc -> ( match lc with | VSharedLoan (bids, sv) -> let r_id = if group then r_id else fresh_region_id () in (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.value)); + cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet"; (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) - assert (ty_no_regions ty); + cassert (ty_no_regions ty) meta "TODO: error message"; let ty = mk_ref_ty (RFVar r_id) ty RShared in let ignored = mk_aignored ty in (* Rem.: the shared value might contain loans *) @@ -1904,7 +1905,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) | VMutLoan bid -> (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) - assert (ty_no_regions ty); + cassert (ty_no_regions ty) meta "TODO: error message"; let ty = mk_ref_ty (RFVar r_id) ty RMut in let ignored = mk_aignored ty in let av = ALoan (AMutLoan (bid, ignored)) in @@ -1913,7 +1914,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) | VSymbolic _ -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - assert (not (value_has_borrows ctx v.value)); + cassert (not (value_has_borrows ctx v.value)) meta "TODO: error message"; (* Return nothing *) ([], v) in @@ -1954,7 +1955,7 @@ type merge_abstraction_info = { - all the borrows are destructured (for instance, shared loans can't contain shared loans). *) -let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : +let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : abs) : merge_abstraction_info = let loans : loan_id_set ref = ref BorrowId.Set.empty in let borrows : borrow_id_set ref = ref BorrowId.Set.empty in @@ -1967,26 +1968,26 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : in let push_loans ids (lc : g_loan_content_with_ty) : unit = - assert (BorrowId.Set.disjoint !loans ids); + cassert (BorrowId.Set.disjoint !loans ids) meta "TODO: error message"; loans := BorrowId.Set.union !loans ids; BorrowId.Set.iter (fun id -> - assert (not (BorrowId.Map.mem id !loan_to_content)); + cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message"; loan_to_content := BorrowId.Map.add id lc !loan_to_content; borrows_loans := LoanId id :: !borrows_loans) ids in let push_loan id (lc : g_loan_content_with_ty) : unit = - assert (not (BorrowId.Set.mem id !loans)); + cassert (not (BorrowId.Set.mem id !loans)) meta "TODO: error message"; loans := BorrowId.Set.add id !loans; - assert (not (BorrowId.Map.mem id !loan_to_content)); + cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message"; loan_to_content := BorrowId.Map.add id lc !loan_to_content; borrows_loans := LoanId id :: !borrows_loans in let push_borrow id (bc : g_borrow_content_with_ty) : unit = - assert (not (BorrowId.Set.mem id !borrows)); + cassert (not (BorrowId.Set.mem id !borrows)) meta "TODO: error message"; borrows := BorrowId.Set.add id !borrows; - assert (not (BorrowId.Map.mem id !borrow_to_content)); + cassert (not (BorrowId.Map.mem id !borrow_to_content)) meta "TODO: error message"; borrow_to_content := BorrowId.Map.add id bc !borrow_to_content; borrows_loans := BorrowId id :: !borrows_loans in @@ -2009,23 +2010,23 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : let ty = match Option.get env with | Concrete ty -> ty - | Abstract _ -> raise (Failure "Unreachable") + | Abstract _ -> craise meta "Unreachable" in (match lc with | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc)) - | VMutLoan _ -> raise (Failure "Unreachable")); + | VMutLoan _ -> craise meta "Unreachable"); (* Continue *) super#visit_loan_content env lc method! visit_borrow_content _ _ = (* Can happen if we explore shared values which contain borrows - i.e., if we have nested borrows (we forbid this for now) *) - raise (Failure "Unreachable") + craise meta "Unreachable" method! visit_aloan_content env lc = let ty = match Option.get env with - | Concrete _ -> raise (Failure "Unreachable") + | Concrete _ -> craise meta "Unreachable" | Abstract ty -> ty in (* Register the loans *) @@ -2035,14 +2036,14 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) - raise (Failure "Unreachable")); + craise meta "Unreachable"); (* Continue *) super#visit_aloan_content env lc method! visit_aborrow_content env bc = let ty = match Option.get env with - | Concrete _ -> raise (Failure "Unreachable") + | Concrete _ -> craise meta "Unreachable" | Abstract ty -> ty in (* Explore the borrow content *) @@ -2056,18 +2057,18 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : | AsbProjReborrows _ -> (* Can only happen if the symbolic value (potentially) contains borrows - i.e., we have nested borrows *) - raise (Failure "Unreachable") + craise meta "Unreachable" in List.iter register asb | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedSharedBorrow -> (* The abstraction has been destructured, so those shouldn't appear *) - raise (Failure "Unreachable")); + craise meta "Unreachable"); super#visit_aborrow_content env bc method! visit_symbolic_value _ sv = (* Sanity check: no borrows *) - assert (not (symbolic_value_has_borrows ctx sv)) + cassert (not (symbolic_value_has_borrows ctx sv)) meta "TODO: error message" end in @@ -2134,7 +2135,7 @@ type merge_duplicates_funcs = { Merge two abstractions into one, without updating the context. *) -let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) +let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs0 : abs) (abs1 : abs) : abs = log#ldebug @@ -2145,8 +2146,8 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) (* Check that the abstractions are destructured *) if !Config.sanity_checks then ( let destructure_shared_values = true in - assert (abs_is_destructured destructure_shared_values ctx abs0); - assert (abs_is_destructured destructure_shared_values ctx abs1)); + cassert (abs_is_destructured meta destructure_shared_values ctx abs0) meta "Abstractions should be destructured"; + cassert (abs_is_destructured meta destructure_shared_values ctx abs1) meta "Abstractions should be destructured"); (* Compute the relevant information *) let { @@ -2156,7 +2157,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) loan_to_content = loan_to_content0; borrow_to_content = borrow_to_content0; } = - compute_merge_abstraction_info ctx abs0 + compute_merge_abstraction_info meta ctx abs0 in let { @@ -2166,14 +2167,14 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) loan_to_content = loan_to_content1; borrow_to_content = borrow_to_content1; } = - compute_merge_abstraction_info ctx abs1 + compute_merge_abstraction_info meta ctx abs1 in (* Sanity check: there is no loan/borrows which appears in both abstractions, unless we allow to merge duplicates *) if merge_funs = None then ( - assert (BorrowId.Set.disjoint borrows0 borrows1); - assert (BorrowId.Set.disjoint loans0 loans1)); + cassert (BorrowId.Set.disjoint borrows0 borrows1) meta "TODO: error message"; + cassert (BorrowId.Set.disjoint loans0 loans1)) meta "TODO: error message"; (* Merge. There are several cases: @@ -2214,7 +2215,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) in let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t = let bids = BorrowId.Set.diff bids intersect in - assert (not (BorrowId.Set.is_empty bids)); + cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message"; bids in let filter_bid (bid : BorrowId.id) : BorrowId.id option = @@ -2242,11 +2243,11 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) (Option.get merge_funs).merge_ashared_borrows id ty0 ty1 | AProjSharedBorrow _, AProjSharedBorrow _ -> (* Unreachable because requires nested borrows *) - raise (Failure "Unreachable") + craise meta "Unreachable" | _ -> (* Unreachable because those cases are ignored (ended/ignored borrows) or inconsistent *) - raise (Failure "Unreachable") + craise meta "Unreachable" in let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty) @@ -2254,12 +2255,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) match (bc0, bc1) with | Concrete _, Concrete _ -> (* This can happen only in case of nested borrows *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Abstract (ty0, bc0), Abstract (ty1, bc1) -> merge_aborrow_contents ty0 bc0 ty1 bc1 | Concrete _, Abstract _ | Abstract _, Concrete _ -> (* TODO: is it really unreachable? *) - raise (Failure "Unreachable") + craise meta "Unreachable" in let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty) @@ -2277,7 +2278,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) (* Check that the sets of ids are the same - if it is not the case, it means we actually need to merge more than 2 avalues: we ignore this case for now *) - assert (BorrowId.Set.equal ids0 ids1); + cassert (BorrowId.Set.equal ids0 ids1) meta "Ids are not the same - Case ignored for now"; let ids = ids0 in if BorrowId.Set.is_empty ids then ( (* If the set of ids is empty, we can eliminate this shared loan. @@ -2289,10 +2290,10 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) to preserve (in practice it works because we destructure the shared values in the abstractions, and forbid nested borrows). *) - assert (not (value_has_loans_or_borrows ctx sv0.value)); - assert (not (value_has_loans_or_borrows ctx sv0.value)); - assert (is_aignored child0.value); - assert (is_aignored child1.value); + cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message"; + cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message"; + cassert (is_aignored child0.value) meta "TODO: error message"; + cassert (is_aignored child1.value) meta "TODO: error message"; None) else ( (* Register the loan ids *) @@ -2304,7 +2305,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) | _ -> (* Unreachable because those cases are ignored (ended/ignored borrows) or inconsistent *) - raise (Failure "Unreachable") + craise meta "Unreachable" in (* Note that because we may filter ids from a set of id, this function has @@ -2315,12 +2316,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) match (lc0, lc1) with | Concrete _, Concrete _ -> (* This can not happen: the values should have been destructured *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Abstract (ty0, lc0), Abstract (ty1, lc1) -> merge_aloan_contents ty0 lc0 ty1 lc1 | Concrete _, Abstract _ | Abstract _, Concrete _ -> (* TODO: is it really unreachable? *) - raise (Failure "Unreachable") + craise meta "Unreachable" in (* Note that we first explore the borrows/loans of [abs1], because we @@ -2361,12 +2362,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) a concrete borrow can only happen inside a shared loan *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Abstract (ty, bc) -> { value = ABorrow bc; ty }) | Some bc0, Some bc1 -> - assert (merge_funs <> None); + cassert (merge_funs <> None) meta "TODO: error message"; merge_g_borrow_contents bc0 bc1 - | None, None -> raise (Failure "Unreachable") + | None, None -> craise meta "Unreachable" in push_avalue av) | LoanId bid -> @@ -2399,15 +2400,15 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) | Concrete _ -> (* This shouldn't happen because the avalues should have been destructured. *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Abstract (ty, lc) -> ( match lc with | ASharedLoan (bids, sv, child) -> let bids = filter_bids bids in - assert (not (BorrowId.Set.is_empty bids)); - assert (is_aignored child.value); - assert ( - not (value_has_loans_or_borrows ctx sv.value)); + cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message"; + cassert (is_aignored child.value) meta "TODO: error message"; + cassert ( + not (value_has_loans_or_borrows ctx sv.value)) meta "TODO: error message"; let lc = ASharedLoan (bids, sv, child) in set_loans_as_merged bids; Some { value = ALoan lc; ty } @@ -2418,11 +2419,11 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) - raise (Failure "Unreachable"))) + craise meta "Unreachable")) | Some lc0, Some lc1 -> - assert (merge_funs <> None); + cassert (merge_funs <> None) meta "TODO: error message"; merge_g_loan_contents lc0 lc1 - | None, None -> raise (Failure "Unreachable") + | None, None -> craise meta "Unreachable" in push_opt_avalue av)) borrows_loans; @@ -2440,7 +2441,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) match av.value with | ABorrow _ -> true | ALoan _ -> false - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in let aborrows, aloans = List.partition is_borrow avalues in List.append aborrows aloans @@ -2475,7 +2476,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) in (* Sanity check *) - if !Config.sanity_checks then assert (abs_is_destructured true ctx abs); + if !Config.sanity_checks then cassert (abs_is_destructured meta true ctx abs) meta "TODO: error message"; (* Return *) abs @@ -2486,7 +2487,7 @@ let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id) let env = Substitute.env_subst_rids rsubst ctx.env in { ctx with env } -let merge_into_abstraction (abs_kind : abs_kind) (can_end : bool) +let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) : eval_ctx * AbstractionId.id = @@ -2496,7 +2497,7 @@ let merge_into_abstraction (abs_kind : abs_kind) (can_end : bool) (* Merge them *) let nabs = - merge_into_abstraction_aux abs_kind can_end merge_funs ctx abs0 abs1 + merge_into_abstraction_aux meta abs_kind can_end merge_funs ctx abs0 abs1 in (* Update the environment: replace the abstraction 1 with the result of the merge, diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 44f85d0a..5b84e2c0 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -9,6 +9,7 @@ open Contexts open Utils open TypesUtils open InterpreterUtils +open Errors (** The local logger *) let log = Logging.borrows_log @@ -94,22 +95,22 @@ let add_borrow_or_abs_id_to_chain (msg : string) (id : borrow_or_abs_id) TODO: is there a way of deriving such a comparison? TODO: rename *) -let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) +let rec compare_rtys (meta : Meta.meta) (default : bool) (combine : bool -> bool -> bool) (compare_regions : region -> region -> bool) (ty1 : rty) (ty2 : rty) : bool = - let compare = compare_rtys default combine compare_regions in + let compare = compare_rtys meta default combine compare_regions in (* Sanity check - TODO: don't do this at every recursive call *) - assert (ty_is_rty ty1 && ty_is_rty ty2); + cassert (ty_is_rty ty1 && ty_is_rty ty2) meta "ty1 or ty2 are not rty TODO"; (* Normalize the associated types *) match (ty1, ty2) with | TLiteral lit1, TLiteral lit2 -> - assert (lit1 = lit2); + cassert (lit1 = lit2) meta "Tlitrals are not equal TODO"; default | TAdt (id1, generics1), TAdt (id2, generics2) -> - assert (id1 = id2); + cassert (id1 = id2) meta "ids are not equal TODO"; (* There are no regions in the const generics, so we ignore them, but we still check they are the same, for sanity *) - assert (generics1.const_generics = generics2.const_generics); + cassert (generics1.const_generics = generics2.const_generics) meta "const generics are not the same"; (* We also ignore the trait refs *) @@ -143,7 +144,7 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) combine params_b tys_b | TRef (r1, ty1, kind1), TRef (r2, ty2, kind2) -> (* Sanity check *) - assert (kind1 = kind2); + cassert (kind1 = kind2) meta "kind1 and kind2 are not equal TODO"; (* Explanation for the case where we check if projections intersect: * the projections intersect if the borrows intersect or their contents * intersect. *) @@ -151,19 +152,19 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) let tys_b = compare ty1 ty2 in combine regions_b tys_b | TVar id1, TVar id2 -> - assert (id1 = id2); + cassert (id1 = id2) meta "Ids are not the same TODO"; default | TTraitType _, TTraitType _ -> (* The types should have been normalized. If after normalization we get trait types, we can consider them as variables *) - assert (ty1 = ty2); + cassert (ty1 = ty2) meta "The types are not normalized"; default | _ -> log#lerror (lazy ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1 ^ "\n- ty2: " ^ show_ty ty2)); - raise (Failure "Unreachable") + craise meta "Unreachable" (** Check if two different projections intersect. This is necessary when giving a symbolic value to an abstraction: we need to check that @@ -172,14 +173,14 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) Note that the two abstractions have different views (in terms of regions) of the symbolic value (hence the two region types). *) -let projections_intersect (ty1 : rty) (rset1 : RegionId.Set.t) (ty2 : rty) +let projections_intersect (meta : Meta.meta) (ty1 : rty) (rset1 : RegionId.Set.t) (ty2 : rty) (rset2 : RegionId.Set.t) : bool = let default = false in let combine b1 b2 = b1 || b2 in let compare_regions r1 r2 = region_in_set r1 rset1 && region_in_set r2 rset2 in - compare_rtys default combine compare_regions ty1 ty2 + compare_rtys meta default combine compare_regions ty1 ty2 (** Check if the first projection contains the second projection. We use this function when checking invariants. @@ -187,14 +188,14 @@ let projections_intersect (ty1 : rty) (rset1 : RegionId.Set.t) (ty2 : rty) The regions in the types shouldn't be erased (this function will raise an exception otherwise). *) -let projection_contains (ty1 : rty) (rset1 : RegionId.Set.t) (ty2 : rty) +let projection_contains (meta : Meta.meta) (ty1 : rty) (rset1 : RegionId.Set.t) (ty2 : rty) (rset2 : RegionId.Set.t) : bool = let default = true in let combine b1 b2 = b1 && b2 in let compare_regions r1 r2 = region_in_set r1 rset1 || not (region_in_set r2 rset2) in - compare_rtys default combine compare_regions ty1 ty2 + compare_rtys meta default combine compare_regions ty1 ty2 (** Lookup a loan content. @@ -204,7 +205,7 @@ let projection_contains (ty1 : rty) (rset1 : RegionId.Set.t) (ty2 : rty) the {!InterpreterUtils.abs_or_var_id} is not necessarily {!constructor:Aeneas.InterpreterUtils.abs_or_var_id.VarId} or {!constructor:Aeneas.InterpreterUtils.abs_or_var_id.DummyVarId}: there can be concrete loans in abstractions (in the shared values). *) -let lookup_loan_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : +let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : (abs_or_var_id * g_loan_content) option = (* We store here whether we are inside an abstraction or a value - note that we * could also track that with the environment, it would probably be more idiomatic @@ -268,7 +269,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : super#visit_aloan_content env lc method! visit_EBinding env bv v = - assert (Option.is_none !abs_or_var); + cassert (Option.is_none !abs_or_var) meta "TODO : error message "; abs_or_var := Some (match bv with @@ -278,7 +279,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : abs_or_var := None method! visit_EAbs env abs = - assert (Option.is_none !abs_or_var); + cassert (Option.is_none !abs_or_var) meta "TODO : error message "; if ek.enter_abs then ( abs_or_var := Some (AbsId abs.abs_id); super#visit_EAbs env abs; @@ -293,17 +294,17 @@ let lookup_loan_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : with FoundGLoanContent lc -> ( match !abs_or_var with | Some abs_or_var -> Some (abs_or_var, lc) - | None -> raise (Failure "Inconsistent state")) + | None -> craise meta "Inconsistent state") (** Lookup a loan content. The loan is referred to by a borrow id. Raises an exception if no loan was found. *) -let lookup_loan (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : +let lookup_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : abs_or_var_id * g_loan_content = - match lookup_loan_opt ek l ctx with - | None -> raise (Failure "Unreachable") + match lookup_loan_opt meta ek l ctx with + | None -> craise meta "Unreachable" | Some res -> res (** Update a loan content. @@ -312,14 +313,14 @@ let lookup_loan (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : This is a helper function: it might break invariants. *) -let update_loan (ek : exploration_kind) (l : BorrowId.id) (nlc : loan_content) +let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (nlc : loan_content) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we update exactly one loan: when updating * inside values, we check we don't update more than one loan. Then, upon * returning we check that we updated at least once. *) let r = ref false in let update () : loan_content = - assert (not !r); + cassert (not !r) meta "TODO : error message "; r := true; nlc in @@ -366,7 +367,7 @@ let update_loan (ek : exploration_kind) (l : BorrowId.id) (nlc : loan_content) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one loan *) - assert !r; + cassert !r meta "No loan was updated"; ctx (** Update a abstraction loan content. @@ -375,14 +376,14 @@ let update_loan (ek : exploration_kind) (l : BorrowId.id) (nlc : loan_content) This is a helper function: it might break invariants. *) -let update_aloan (ek : exploration_kind) (l : BorrowId.id) (nlc : aloan_content) +let update_aloan (meta : Meta.meta ) (ek : exploration_kind) (l : BorrowId.id) (nlc : aloan_content) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we update exactly one loan: when updating * inside values, we check we don't update more than one loan. Then, upon * returning we check that we updated at least once. *) let r = ref false in let update () : aloan_content = - assert (not !r); + cassert (not !r) meta "TODO : error message "; r := true; nlc in @@ -415,7 +416,7 @@ let update_aloan (ek : exploration_kind) (l : BorrowId.id) (nlc : aloan_content) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one loan *) - assert !r; + cassert !r meta "No loan was uodated"; ctx (** Lookup a borrow content from a borrow id. *) @@ -481,10 +482,10 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) Raise an exception if no loan was found *) -let lookup_borrow (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : +let lookup_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : g_borrow_content = match lookup_borrow_opt ek l ctx with - | None -> raise (Failure "Unreachable") + | None -> craise meta "Unreachable" | Some lc -> lc (** Update a borrow content. @@ -493,14 +494,14 @@ let lookup_borrow (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : This is a helper function: it might break invariants. *) -let update_borrow (ek : exploration_kind) (l : BorrowId.id) +let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (nbc : borrow_content) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we update exactly one borrow: when updating * inside values, we check we don't update more than one borrow. Then, upon * returning we check that we updated at least once. *) let r = ref false in let update () : borrow_content = - assert (not !r); + cassert (not !r) meta "TODO : error message "; r := true; nbc in @@ -541,7 +542,7 @@ let update_borrow (ek : exploration_kind) (l : BorrowId.id) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one borrow *) - assert !r; + cassert !r meta "No borrow was updated"; ctx (** Update an abstraction borrow content. @@ -550,14 +551,14 @@ let update_borrow (ek : exploration_kind) (l : BorrowId.id) This is a helper function: it might break invariants. *) -let update_aborrow (ek : exploration_kind) (l : BorrowId.id) (nv : avalue) +let update_aborrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (nv : avalue) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we update exactly one borrow: when updating * inside values, we check we don't update more than one borrow. Then, upon * returning we check that we updated at least once. *) let r = ref false in let update () : avalue = - assert (not !r); + cassert (not !r) meta ""; r := true; nv in @@ -588,7 +589,7 @@ let update_aborrow (ek : exploration_kind) (l : BorrowId.id) (nv : avalue) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one borrow *) - assert !r; + cassert !r meta "No borrow was updated"; ctx (** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *) @@ -666,13 +667,13 @@ let get_first_outer_loan_or_borrow_in_value (with_borrows : bool) | FoundLoanContent lc -> Some (LoanContent lc) | FoundBorrowContent bc -> Some (BorrowContent bc) -let proj_borrows_intersects_proj_loans +let proj_borrows_intersects_proj_loans (meta : Meta.meta) (proj_borrows : RegionId.Set.t * symbolic_value * rty) (proj_loans : RegionId.Set.t * symbolic_value) : bool = let b_regions, b_sv, b_ty = proj_borrows in let l_regions, l_sv = proj_loans in if same_symbolic_id b_sv l_sv then - projections_intersect l_sv.sv_ty l_regions b_ty b_regions + projections_intersect meta l_sv.sv_ty l_regions b_ty b_regions else false (** Result of looking up aproj_borrows which intersect a given aproj_loans in @@ -700,24 +701,25 @@ type looked_up_aproj_borrows = This is a helper function. *) -let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) +let lookup_intersecting_aproj_borrows_opt (meta : Meta.meta) (lookup_shared : bool) (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : looked_up_aproj_borrows option = let found : looked_up_aproj_borrows option ref = ref None in let set_non_shared ((id, ty) : AbstractionId.id * rty) : unit = match !found with | None -> found := Some (NonSharedProj (id, ty)) - | Some _ -> raise (Failure "Unreachable") + | Some _ -> craise meta "Unreachable" in let add_shared (x : AbstractionId.id * rty) : unit = match !found with | None -> found := Some (SharedProjs [ x ]) | Some (SharedProjs pl) -> found := Some (SharedProjs (x :: pl)) - | Some (NonSharedProj _) -> raise (Failure "Unreachable") + | Some (NonSharedProj _) -> craise meta "Unreachable" in let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty = if proj_borrows_intersects_proj_loans + meta (abs.regions, sv', proj_ty) (regions, sv) then @@ -733,7 +735,7 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) method! visit_abstract_shared_borrow abs asb = (* Sanity check *) (match !found with - | Some (NonSharedProj _) -> raise (Failure "Unreachable") + | Some (NonSharedProj _) -> craise meta "Unreachable" | _ -> ()); (* Explore *) if lookup_shared then @@ -772,20 +774,20 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) Returns the id of the owning abstraction, and the projection type used in this abstraction. *) -let lookup_intersecting_aproj_borrows_not_shared_opt (regions : RegionId.Set.t) +let lookup_intersecting_aproj_borrows_not_shared_opt (meta : Meta.meta) (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : (AbstractionId.id * rty) option = let lookup_shared = false in - match lookup_intersecting_aproj_borrows_opt lookup_shared regions sv ctx with + match lookup_intersecting_aproj_borrows_opt meta lookup_shared regions sv ctx with | None -> None | Some (NonSharedProj (abs_id, rty)) -> Some (abs_id, rty) - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" (** Similar to {!lookup_intersecting_aproj_borrows_opt}, but updates the values. This is a helper function: it might break invariants. *) -let update_intersecting_aproj_borrows (can_update_shared : bool) +let update_intersecting_aproj_borrows (meta : Meta.meta) (can_update_shared : bool) (update_shared : AbstractionId.id -> rty -> abstract_shared_borrows) (update_non_shared : AbstractionId.id -> rty -> aproj) (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx @@ -793,16 +795,17 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) (* Small helpers for sanity checks *) let shared = ref None in let add_shared () = - match !shared with None -> shared := Some true | Some b -> assert b + match !shared with None -> shared := Some true | Some b -> cassert b meta "TODO : error message " in let set_non_shared () = match !shared with | None -> shared := Some false - | Some _ -> raise (Failure "Found unexpected intersecting proj_borrows") + | Some _ -> craise meta "Found unexpected intersecting proj_borrows" in let check_proj_borrows is_shared abs sv' proj_ty = if proj_borrows_intersects_proj_loans + meta (abs.regions, sv', proj_ty) (regions, sv) then ( @@ -818,7 +821,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) method! visit_abstract_shared_borrows abs asb = (* Sanity check *) - (match !shared with Some b -> assert b | _ -> ()); + (match !shared with Some b -> cassert b meta "TODO : error message " | _ -> ()); (* Explore *) if can_update_shared then let abs = Option.get abs in @@ -850,7 +853,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Check that we updated the context at least once *) - assert (Option.is_some !shared); + cassert (Option.is_some !shared) meta "Context was not updated at least once"; (* Return *) ctx @@ -861,11 +864,11 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) This is a helper function: it might break invariants. *) -let update_intersecting_aproj_borrows_non_shared (regions : RegionId.Set.t) +let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta) (regions : RegionId.Set.t) (sv : symbolic_value) (nv : aproj) (ctx : eval_ctx) : eval_ctx = (* Small helpers *) let can_update_shared = false in - let update_shared _ _ = raise (Failure "Unexpected") in + let update_shared _ _ = craise meta "Unexpected" in let updated = ref false in let update_non_shared _ _ = (* We can update more than one borrow! *) @@ -874,11 +877,11 @@ let update_intersecting_aproj_borrows_non_shared (regions : RegionId.Set.t) in (* Update *) let ctx = - update_intersecting_aproj_borrows can_update_shared update_shared + update_intersecting_aproj_borrows meta can_update_shared update_shared update_non_shared regions sv ctx in (* Check that we updated at least once *) - assert !updated; + cassert !updated meta "Not updated at least once"; (* Return *) ctx @@ -887,14 +890,14 @@ let update_intersecting_aproj_borrows_non_shared (regions : RegionId.Set.t) This is a helper function: it might break invariants. *) -let remove_intersecting_aproj_borrows_shared (regions : RegionId.Set.t) +let remove_intersecting_aproj_borrows_shared (meta : Meta.meta) (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Small helpers *) let can_update_shared = true in let update_shared _ _ = [] in - let update_non_shared _ _ = raise (Failure "Unexpected") in + let update_non_shared _ _ = craise meta "Unexpected" in (* Update *) - update_intersecting_aproj_borrows can_update_shared update_shared + update_intersecting_aproj_borrows meta can_update_shared update_shared update_non_shared regions sv ctx (** Updates the proj_loans intersecting some projection. @@ -928,12 +931,12 @@ let remove_intersecting_aproj_borrows_shared (regions : RegionId.Set.t) Note that the symbolic value at this place is necessarily equal to [sv], which is why we don't give it as parameters. *) -let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t) +let update_intersecting_aproj_loans (meta : Meta.meta) (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value) (subst : abs -> (msymbolic_value * aproj) list -> aproj) (ctx : eval_ctx) : eval_ctx = (* *) - assert (ty_is_rty proj_ty); + cassert (ty_is_rty proj_ty) meta "proj_ty is not rty TODO"; (* Small helpers for sanity checks *) let updated = ref false in let update abs local_given_back : aproj = @@ -955,9 +958,9 @@ let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t) | AProjLoans (sv', given_back) -> let abs = Option.get abs in if same_symbolic_id sv sv' then ( - assert (sv.sv_ty = sv'.sv_ty); + cassert (sv.sv_ty = sv'.sv_ty) meta "TODO : error message "; if - projections_intersect proj_ty proj_regions sv'.sv_ty abs.regions + projections_intersect meta proj_ty proj_regions sv'.sv_ty abs.regions then update abs given_back else super#visit_aproj (Some abs) sproj) else super#visit_aproj (Some abs) sproj @@ -966,7 +969,7 @@ let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Check that we updated the context at least once *) - assert !updated; + cassert !updated meta "Context was not updated at least once"; (* Return *) ctx @@ -980,13 +983,13 @@ let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t) Sanity check: we check that there is exactly one projector which corresponds to the couple (abstraction id, symbolic value). *) -let lookup_aproj_loans (abs_id : AbstractionId.id) (sv : symbolic_value) +let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symbolic_value) (ctx : eval_ctx) : (msymbolic_value * aproj) list = (* Small helpers for sanity checks *) let found = ref None in let set_found x = (* There is at most one projector which corresponds to the description *) - assert (Option.is_none !found); + cassert (Option.is_none !found) meta "More than one projecto corresponds to the description"; found := Some x in (* The visitor *) @@ -1004,9 +1007,9 @@ let lookup_aproj_loans (abs_id : AbstractionId.id) (sv : symbolic_value) super#visit_aproj abs sproj | AProjLoans (sv', given_back) -> let abs = Option.get abs in - assert (abs.abs_id = abs_id); + cassert (abs.abs_id = abs_id) meta "TODO : error message "; if sv'.sv_id = sv.sv_id then ( - assert (sv' = sv); + cassert (sv' = sv) meta "TODO : error message "; set_found given_back) else ()); super#visit_aproj abs sproj @@ -1025,13 +1028,13 @@ let lookup_aproj_loans (abs_id : AbstractionId.id) (sv : symbolic_value) Sanity check: we check that there is exactly one projector which corresponds to the couple (abstraction id, symbolic value). *) -let update_aproj_loans (abs_id : AbstractionId.id) (sv : symbolic_value) +let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symbolic_value) (nproj : aproj) (ctx : eval_ctx) : eval_ctx = (* Small helpers for sanity checks *) let found = ref false in let update () = (* We update at most once *) - assert (not !found); + cassert (not !found) meta "Updated more than once"; found := true; nproj in @@ -1050,9 +1053,9 @@ let update_aproj_loans (abs_id : AbstractionId.id) (sv : symbolic_value) super#visit_aproj abs sproj | AProjLoans (sv', _) -> let abs = Option.get abs in - assert (abs.abs_id = abs_id); + cassert (abs.abs_id = abs_id) meta "TODO : error message "; if sv'.sv_id = sv.sv_id then ( - assert (sv' = sv); + cassert (sv' = sv) meta "TODO : error message "; update ()) else super#visit_aproj (Some abs) sproj end @@ -1060,7 +1063,7 @@ let update_aproj_loans (abs_id : AbstractionId.id) (sv : symbolic_value) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Sanity check *) - assert !found; + cassert !found meta "TODO : error message "; (* Return *) ctx @@ -1074,13 +1077,13 @@ let update_aproj_loans (abs_id : AbstractionId.id) (sv : symbolic_value) TODO: factorize with {!update_aproj_loans}? *) -let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value) +let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symbolic_value) (nproj : aproj) (ctx : eval_ctx) : eval_ctx = (* Small helpers for sanity checks *) let found = ref false in let update () = (* We update at most once *) - assert (not !found); + cassert (not !found) meta "Updated more than once"; found := true; nproj in @@ -1099,9 +1102,9 @@ let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value) super#visit_aproj abs sproj | AProjBorrows (sv', _proj_ty) -> let abs = Option.get abs in - assert (abs.abs_id = abs_id); + cassert (abs.abs_id = abs_id) meta "TODO : error message "; if sv'.sv_id = sv.sv_id then ( - assert (sv' = sv); + cassert (sv' = sv) meta "TODO : error message "; update ()) else super#visit_aproj (Some abs) sproj end @@ -1109,7 +1112,7 @@ let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Sanity check *) - assert !found; + cassert !found meta "TODO : error message "; (* Return *) ctx @@ -1118,18 +1121,18 @@ let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value) Converts an {!Values.aproj.AProjLoans} to an {!Values.aproj.AEndedProjLoans}. The projector is identified by a symbolic value and an abstraction id. *) -let update_aproj_loans_to_ended (abs_id : AbstractionId.id) +let update_aproj_loans_to_ended (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Lookup the projector of loans *) - let given_back = lookup_aproj_loans abs_id sv ctx in + let given_back = lookup_aproj_loans meta abs_id sv ctx in (* Create the new value for the projector *) let nproj = AEndedProjLoans (sv, given_back) in (* Insert it *) - let ctx = update_aproj_loans abs_id sv nproj ctx in + let ctx = update_aproj_loans meta abs_id sv nproj ctx in (* Return *) ctx -let no_aproj_over_symbolic_in_context (sv : symbolic_value) (ctx : eval_ctx) : +let no_aproj_over_symbolic_in_context (meta : Meta.meta) (sv : symbolic_value) (ctx : eval_ctx) : unit = (* The visitor *) let obj = @@ -1146,7 +1149,7 @@ let no_aproj_over_symbolic_in_context (sv : symbolic_value) (ctx : eval_ctx) : in (* Apply *) try obj#visit_eval_ctx () ctx - with Found -> raise (Failure "update_aproj_loans_to_ended: failed") + with Found -> craise meta "update_aproj_loans_to_ended: failed" (** Helper function @@ -1155,7 +1158,7 @@ let no_aproj_over_symbolic_in_context (sv : symbolic_value) (ctx : eval_ctx) : **Remark:** we don't take the *ignored* mut/shared loans into account. *) -let get_first_non_ignored_aloan_in_abstraction (abs : abs) : +let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) : borrow_ids_or_symbolic_value option = (* Explore to find a loan *) let obj = @@ -1184,7 +1187,7 @@ let get_first_non_ignored_aloan_in_abstraction (abs : abs) : | VMutLoan _ -> (* The mut loan linked to the mutable borrow present in a shared * value in an abstraction should be in an AProjBorrows *) - raise (Failure "Unreachable") + craise meta "Unreachable" | VSharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids)) method! visit_aproj env sproj = @@ -1208,9 +1211,9 @@ let get_first_non_ignored_aloan_in_abstraction (abs : abs) : (* There are loan projections over symbolic values *) Some (SymbolicValue sv) -let lookup_shared_value_opt (ctx : eval_ctx) (bid : BorrowId.id) : +let lookup_shared_value_opt (meta : Meta.meta) (ctx : eval_ctx) (bid : BorrowId.id) : typed_value option = - match lookup_loan_opt ek_all bid ctx with + match lookup_loan_opt meta ek_all bid ctx with | None -> None | Some (_, lc) -> ( match lc with @@ -1218,5 +1221,5 @@ let lookup_shared_value_opt (ctx : eval_ctx) (bid : BorrowId.id) : Some sv | _ -> None) -let lookup_shared_value (ctx : eval_ctx) (bid : BorrowId.id) : typed_value = - Option.get (lookup_shared_value_opt ctx bid) +let lookup_shared_value (meta : Meta.meta) (ctx : eval_ctx) (bid : BorrowId.id) : typed_value = + Option.get (lookup_shared_value_opt meta ctx bid) diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 66c97cde..b07ba943 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -11,6 +11,7 @@ open InterpreterBorrows open InterpreterLoopsCore open InterpreterLoopsMatchCtxs open InterpreterLoopsJoinCtxs +open Errors (** The local logger *) let log = Logging.loops_fixed_point_log @@ -135,7 +136,7 @@ let cleanup_fresh_values_and_abs (config : config) (fixed_ids : ids_sets) : called typically after we merge abstractions together (see {!collapse_ctx} for instance). *) -let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t) +let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = let reorder_in_fresh_abs (abs : abs) : abs = (* Split between the loans and borrows *) @@ -143,7 +144,7 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t) match av.value with | ABorrow _ -> true | ALoan _ -> false - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in let aborrows, aloans = List.partition is_borrow abs.avalues in @@ -156,13 +157,13 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t) let get_borrow_id (av : typed_avalue) : BorrowId.id = match av.value with | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in let get_loan_id (av : typed_avalue) : BorrowId.id = match av.value with | ALoan (AMutLoan (lid, _)) -> lid | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in (* We use ordered maps to reorder the borrows and loans *) let reorder (get_bid : typed_avalue -> BorrowId.id) @@ -186,7 +187,7 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t) { ctx with env } -let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun = +let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_fun = fun cf ctx0 -> let ctx = ctx0 in (* Compute the set of borrows which appear in the abstractions, so that @@ -266,12 +267,12 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun = borrow_substs := (lid, nlid) :: !borrow_substs; (* Rem.: the below sanity checks are not really necessary *) - assert (AbstractionId.Set.is_empty abs.parents); - assert (abs.original_parents = []); - assert (RegionId.Set.is_empty abs.ancestors_regions); + cassert (AbstractionId.Set.is_empty abs.parents) meta "abs.parents is not empty TODO"; + cassert (abs.original_parents = []) meta "original_parents is not empty TODO"; + cassert (RegionId.Set.is_empty abs.ancestors_regions) meta "ancestors_regions is not empty TODO"; (* Introduce the new abstraction for the shared values *) - assert (ty_no_regions sv.ty); + cassert (ty_no_regions sv.ty) meta "TODO : error message "; let rty = sv.ty in (* Create the shared loan child *) @@ -322,7 +323,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun = let collect_shared_values_in_abs (abs : abs) : unit = let collect_shared_value lids (sv : typed_value) = (* Sanity check: we don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.value)); + cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows not supported yet"; (* Filter the loan ids whose corresponding borrows appear in abstractions (see the documentation of the function) *) @@ -356,7 +357,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun = TODO: implement this more general behavior. *) method! visit_symbolic_value env sv = - assert (not (symbolic_value_has_borrows ctx sv)); + cassert (not (symbolic_value_has_borrows ctx sv)) meta "There should be no symbolic values with borrows inside the abstraction"; super#visit_symbolic_value env sv end in @@ -432,11 +433,11 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun = SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e)) e !sid_subst) -let prepare_ashared_loans_no_synth (loop_id : LoopId.id) (ctx : eval_ctx) : +let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id) (ctx : eval_ctx) : eval_ctx = - get_cf_ctx_no_synth (prepare_ashared_loans (Some loop_id)) ctx + get_cf_ctx_no_synth (prepare_ashared_loans meta (Some loop_id)) ctx -let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) +let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id : LoopId.id) (eval_loop_body : st_cm_fun) (ctx0 : eval_ctx) : eval_ctx * ids_sets * abs RegionGroupId.Map.t = (* The continuation for when we exit the loop - we register the @@ -453,7 +454,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) For more details, see the comments for {!prepare_ashared_loans} *) - let ctx = prepare_ashared_loans_no_synth loop_id ctx0 in + let ctx = prepare_ashared_loans_no_synth meta loop_id ctx0 in (* Debug *) log#ldebug @@ -472,15 +473,15 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) | Return | Panic | Break _ -> None | Unit -> (* See the comment in {!eval_loop} *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Continue i -> (* For now we don't support continues to outer loops *) - assert (i = 0); + cassert (i = 0) meta "Continues to outer loops not supported yet"; register_ctx ctx; None | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* We don't support nested loops for now *) - raise (Failure "Nested loops are not supported for now") + craise meta "Nested loops are not supported for now" in (* The fixed ids. They are the ids of the original ctx, after we ended @@ -573,7 +574,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) log#ldebug (lazy "compute_fixed_point: equiv_ctx:"); let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in let check_equivalent = true in - let lookup_shared_value _ = raise (Failure "Unreachable") in + let lookup_shared_value _ = craise meta "Unreachable" in Option.is_some (match_ctxs check_equivalent fixed_ids lookup_shared_value lookup_shared_value ctx1 ctx2) @@ -581,10 +582,10 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) let max_num_iter = Config.loop_fixed_point_max_num_iters in let rec compute_fixed_point (ctx : eval_ctx) (i0 : int) (i : int) : eval_ctx = if i = 0 then - raise - (Failure + craise + meta ("Could not compute a loop fixed point in " ^ string_of_int i0 - ^ " iterations")) + ^ " iterations") else (* Evaluate the loop body to register the different contexts upon reentry *) let _ = eval_loop_body cf_exit_loop_body ctx in @@ -633,10 +634,10 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) method! visit_abs _ abs = match abs.kind with | Loop (loop_id', _, kind) -> - assert (loop_id' = loop_id); - assert (kind = LoopSynthInput); + cassert (loop_id' = loop_id) meta "TODO : error message "; + cassert (kind = LoopSynthInput) meta "TODO : error message "; (* The abstractions introduced so far should be endable *) - assert (abs.can_end = true); + cassert (abs.can_end = true) meta "The abstractions introduced so far can not end"; add_aid abs.abs_id; abs | _ -> abs @@ -669,12 +670,12 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) None | Break _ -> (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Return -> log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop: Return"); (* Should we consume the return value and pop the frame? @@ -693,9 +694,9 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) in (* By default, the [SynthInput] abs can't end *) let ctx = ctx_set_abs_can_end ctx abs_id true in - assert ( + cassert ( let abs = ctx_lookup_abs ctx abs_id in - abs.kind = SynthInput rg_id); + abs.kind = SynthInput rg_id) meta "TODO : error message "; (* End this abstraction *) let ctx = InterpreterBorrows.end_abstraction_no_synth config abs_id ctx @@ -717,14 +718,14 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) let _ = RegionGroupId.Map.iter (fun _ ids -> - assert (AbstractionId.Set.disjoint !aids_union ids); + cassert (AbstractionId.Set.disjoint !aids_union ids) meta "The sets of abstractions we need to end per region group are not pairwise disjoint"; aids_union := AbstractionId.Set.union ids !aids_union) !fp_ended_aids in (* We also check that all the regions need to end - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating... *) - assert (AbstractionId.Set.equal !aids_union !fp_aids); + cassert (AbstractionId.Set.equal !aids_union !fp_aids) meta "Not all regions need to end TODO"; (* Merge the abstractions which need to be merged, and compute the map from region id to abstraction id *) @@ -781,7 +782,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) fp := fp'; id0 := id0'; () - with ValueMatchFailure _ -> raise (Failure "Unexpected")) + with ValueMatchFailure _ -> craise meta "Unexpected") ids; (* Register the mapping *) let abs = ctx_lookup_abs !fp !id0 in @@ -792,7 +793,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *) let fp = - reorder_loans_borrows_in_fresh_abs (Option.get !fixed_ids).aids !fp + reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (Option.get !fixed_ids).aids !fp in (* Update the abstraction's [can_end] field and their kinds. @@ -814,8 +815,8 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) method! visit_abs _ abs = match abs.kind with | Loop (loop_id', _, kind) -> - assert (loop_id' = loop_id); - assert (kind = LoopSynthInput); + cassert (loop_id' = loop_id) meta "TODO : error message "; + cassert (kind = LoopSynthInput) meta "TODO : error message "; let kind : abs_kind = if remove_rg_id then Loop (loop_id, None, LoopSynthInput) else abs.kind @@ -849,7 +850,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) (* Return *) (fp, fixed_ids, rg_to_abs) -let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) +let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_sets) (src_ctx : eval_ctx) (tgt_ctx : eval_ctx) : borrow_loan_corresp = log#ldebug (lazy @@ -877,10 +878,10 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in let open InterpreterBorrowsCore in let lookup_shared_loan lid ctx : typed_value = - match snd (lookup_loan ek_all lid ctx) with + match snd (lookup_loan meta ek_all lid ctx) with | Concrete (VSharedLoan (_, v)) -> v | Abstract (ASharedLoan (_, v, _)) -> v - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in let lookup_in_src id = lookup_shared_loan id src_ctx in @@ -940,7 +941,7 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) ids.loan_ids in (* Check that the loan and borrows are related *) - assert (BorrowId.Set.equal ids.borrow_ids loan_ids)) + cassert (BorrowId.Set.equal ids.borrow_ids loan_ids) meta "The loan and borrows are not related") new_absl; (* For every target abstraction (going back to the [list_nth_mut] example, @@ -983,7 +984,7 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) loan_to_borrow_id_map = tgt_loan_to_borrow; } -let compute_fp_ctx_symbolic_values (ctx : eval_ctx) (fp_ctx : eval_ctx) : +let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) (fp_ctx : eval_ctx) : SymbolicValueId.Set.t * symbolic_value list = let old_ids, _ = compute_ctx_ids ctx in let fp_ids, fp_ids_maps = compute_ctx_ids fp_ctx in @@ -1064,10 +1065,10 @@ let compute_fp_ctx_symbolic_values (ctx : eval_ctx) (fp_ctx : eval_ctx) : method! visit_VSharedBorrow env bid = let open InterpreterBorrowsCore in let v = - match snd (lookup_loan ek_all bid fp_ctx) with + match snd (lookup_loan meta ek_all bid fp_ctx) with | Concrete (VSharedLoan (_, v)) -> v | Abstract (ASharedLoan (_, v, _)) -> v - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in self#visit_typed_value env v diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 88f290c4..fc2a97e5 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -7,6 +7,7 @@ open InterpreterUtils open InterpreterBorrows open InterpreterLoopsCore open InterpreterLoopsMatchCtxs +open Errors (** The local logger *) let log = Logging.loops_join_ctxs_log @@ -18,7 +19,7 @@ let log = Logging.loops_join_ctxs_log called typically after we merge abstractions together (see {!collapse_ctx} for instance). *) -let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t) +let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = let reorder_in_fresh_abs (abs : abs) : abs = (* Split between the loans and borrows *) @@ -26,7 +27,7 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t) match av.value with | ABorrow _ -> true | ALoan _ -> false - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in let aborrows, aloans = List.partition is_borrow abs.avalues in @@ -39,13 +40,13 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t) let get_borrow_id (av : typed_avalue) : BorrowId.id = match av.value with | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in let get_loan_id (av : typed_avalue) : BorrowId.id = match av.value with | ALoan (AMutLoan (lid, _)) -> lid | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in (* We use ordered maps to reorder the borrows and loans *) let reorder (get_bid : typed_avalue -> BorrowId.id) @@ -128,7 +129,7 @@ let reorder_loans_borrows_in_fresh_abs (old_abs_ids : AbstractionId.Set.t) This can happen when merging environments (note that such environments are not well-formed - they become well formed again after collapsing). *) -let collapse_ctx (loop_id : LoopId.id) +let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id) (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = (* Debug *) @@ -274,7 +275,7 @@ let collapse_ctx (loop_id : LoopId.id) ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string !ctx ^ "\n\n")); (* Reorder the loans and borrows in the fresh abstractions *) - let ctx = reorder_loans_borrows_in_fresh_abs old_ids.aids !ctx in + let ctx = reorder_loans_borrows_in_fresh_abs meta old_ids.aids !ctx in log#ldebug (lazy @@ -285,7 +286,7 @@ let collapse_ctx (loop_id : LoopId.id) (* Return the new context *) ctx -let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx) +let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id) (ctx : eval_ctx) : merge_duplicates_funcs = (* Rem.: the merge functions raise exceptions (that we catch). *) let module S : MatchJoinState = struct @@ -306,8 +307,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx) *) let merge_amut_borrows id ty0 child0 _ty1 child1 = (* Sanity checks *) - assert (is_aignored child0.value); - assert (is_aignored child1.value); + cassert (is_aignored child0.value) meta "Children are not [AIgnored]"; + cassert (is_aignored child1.value) meta "Children are not [AIgnored]"; (* We need to pick a type for the avalue. The types on the left and on the right may use different regions: it doesn't really matter (here, we pick @@ -325,8 +326,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx) let _ = let _, ty0, _ = ty_as_ref ty0 in let _, ty1, _ = ty_as_ref ty1 in - assert (not (ty_has_borrows ctx.type_ctx.type_infos ty0)); - assert (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) + cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta ""; + cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta "" in (* Same remarks as for [merge_amut_borrows] *) @@ -337,8 +338,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx) let merge_amut_loans id ty0 child0 _ty1 child1 = (* Sanity checks *) - assert (is_aignored child0.value); - assert (is_aignored child1.value); + cassert (is_aignored child0.value) meta "Children are not [AIgnored]"; + cassert (is_aignored child1.value) meta "Children are not [AIgnored]"; (* Same remarks as for [merge_amut_borrows] *) let ty = ty0 in let child = child0 in @@ -348,15 +349,15 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx) let merge_ashared_loans ids ty0 (sv0 : typed_value) child0 _ty1 (sv1 : typed_value) child1 = (* Sanity checks *) - assert (is_aignored child0.value); - assert (is_aignored child1.value); + cassert (is_aignored child0.value) meta "Children are not [AIgnored]"; + cassert (is_aignored child1.value) meta "Children are not [AIgnored]"; (* Same remarks as for [merge_amut_borrows]. This time we need to also merge the shared values. We rely on the join matcher [JM] to do so. *) - assert (not (value_has_loans_or_borrows ctx sv0.value)); - assert (not (value_has_loans_or_borrows ctx sv1.value)); + cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta ""; + cassert (not (value_has_loans_or_borrows ctx sv1.value)) meta ""; let ty = ty0 in let child = child0 in let sv = M.match_typed_values ctx ctx sv0 sv1 in @@ -370,10 +371,10 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx) merge_ashared_loans; } -let merge_into_abstraction (loop_id : LoopId.id) (abs_kind : abs_kind) +let merge_into_abstraction (meta : Meta.meta) (loop_id : LoopId.id) (abs_kind : abs_kind) (can_end : bool) (ctx : eval_ctx) (aid0 : AbstractionId.id) (aid1 : AbstractionId.id) : eval_ctx * AbstractionId.id = - let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in + let merge_funs = mk_collapse_ctx_merge_duplicate_funs meta loop_id ctx in merge_into_abstraction abs_kind can_end (Some merge_funs) ctx aid0 aid1 (** Collapse an environment, merging the duplicated borrows/loans. @@ -383,13 +384,13 @@ let merge_into_abstraction (loop_id : LoopId.id) (abs_kind : abs_kind) We do this because when we join environments, we may introduce duplicated loans and borrows. See the explanations for {!join_ctxs}. *) -let collapse_ctx_with_merge (loop_id : LoopId.id) (old_ids : ids_sets) +let collapse_ctx_with_merge (meta : Meta.meta) (loop_id : LoopId.id) (old_ids : ids_sets) (ctx : eval_ctx) : eval_ctx = - let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in - try collapse_ctx loop_id (Some merge_funs) old_ids ctx - with ValueMatchFailure _ -> raise (Failure "Unexpected") + let merge_funs = mk_collapse_ctx_merge_duplicate_funs meta loop_id ctx in + try collapse_ctx meta loop_id (Some merge_funs) old_ids ctx + with ValueMatchFailure _ -> craise meta "Unexpected" -let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) +let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) (ctx1 : eval_ctx) : ctx_or_update = (* Debug *) log#ldebug @@ -422,14 +423,14 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) match ee with | EBinding (BVar _, _) -> (* Variables are necessarily in the prefix *) - raise (Failure "Unreachable") + craise meta "Unreachable" | EBinding (BDummy did, _) -> - assert (not (DummyVarId.Set.mem did fixed_ids.dids)) + cassert (not (DummyVarId.Set.mem did fixed_ids.dids)) meta "" | EAbs abs -> - assert (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) + cassert (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta "" | EFrame -> (* This should have been eliminated *) - raise (Failure "Unreachable") + craise meta "Unreachable" in List.iter check_valid env0; List.iter check_valid env1; @@ -465,7 +466,7 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) are not in the prefix anymore *) if DummyVarId.Set.mem b0 fixed_ids.dids then ( (* Still in the prefix: match the values *) - assert (b0 = b1); + cassert (b0 = b1) meta "Bindings are not the same. We are not in the prefix anymore"; let b = b0 in let v = M.match_typed_values ctx0 ctx1 v0 v1 in let var = EBinding (BDummy b, v) in @@ -487,7 +488,8 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) (* Variable bindings *must* be in the prefix and consequently their ids must be the same *) - assert (b0 = b1); + cassert (b0 = b1) meta "Variable bindings *must* be in the prefix and consequently their + ids must be the same"; (* Match the values *) let b = b0 in let v = M.match_typed_values ctx0 ctx1 v0 v1 in @@ -505,7 +507,7 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) (* Same as for the dummy values: there are two cases *) if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then ( (* Still in the prefix: the abstractions must be the same *) - assert (abs0 = abs1); + cassert (abs0 = abs1) meta "The abstractions are not the same"; (* Continue *) abs :: join_prefixes env0' env1') else (* Not in the prefix anymore *) @@ -520,7 +522,7 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx) let env0, env1 = match (env0, env1) with | EFrame :: env0, EFrame :: env1 -> (env0, env1) - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in log#ldebug @@ -634,7 +636,7 @@ let refresh_abs (old_abs : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = in { ctx with env } -let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id) +let loop_join_origin_with_continue_ctxs (meta : Meta.meta) (config : config) (loop_id : LoopId.id) (fixed_ids : ids_sets) (old_ctx : eval_ctx) (ctxl : eval_ctx list) : (eval_ctx * eval_ctx list) * eval_ctx = (* # Join with the new contexts, one by one @@ -647,7 +649,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id) *) let joined_ctx = ref old_ctx in let rec join_one_aux (ctx : eval_ctx) : eval_ctx = - match join_ctxs loop_id fixed_ids !joined_ctx ctx with + match join_ctxs meta loop_id fixed_ids !joined_ctx ctx with | Ok nctx -> joined_ctx := nctx; ctx @@ -659,7 +661,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id) | LoansInRight bids -> InterpreterBorrows.end_borrows_no_synth config bids ctx | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> - raise (Failure "Unexpected") + craise meta "Unexpected" in join_one_aux ctx in @@ -677,7 +679,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id) ^ eval_ctx_to_string ctx)); (* Collapse the context we want to add to the join *) - let ctx = collapse_ctx loop_id None fixed_ids ctx in + let ctx = collapse_ctx meta loop_id None fixed_ids ctx in log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n" @@ -696,14 +698,14 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id) (* Collapse again - the join might have introduce abstractions we want to merge with the others (note that those abstractions may actually lead to borrows/loans duplications) *) - joined_ctx := collapse_ctx_with_merge loop_id fixed_ids !joined_ctx; + joined_ctx := collapse_ctx_with_merge meta loop_id fixed_ids !joined_ctx; log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n" ^ eval_ctx_to_string !joined_ctx)); (* Sanity check *) - if !Config.sanity_checks then Invariants.check_invariants !joined_ctx; + if !Config.sanity_checks then Invariants.check_invariants meta !joined_ctx; (* Return *) ctx1 in diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index dd7bd7a7..67c1155c 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -14,6 +14,7 @@ open InterpreterUtils open InterpreterBorrowsCore open InterpreterBorrows open InterpreterLoopsCore +open Errors module S = SynthesizeSymbolic (** The local logger *) @@ -1400,7 +1401,7 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : eval_ctx) (match_ctxs check_equivalent fixed_ids lookup_shared_value lookup_shared_value ctx0 ctx1) -let prepare_match_ctx_with_target (config : config) (loop_id : LoopId.id) +let prepare_match_ctx_with_target (meta : Meta.meta) (config : config) (loop_id : LoopId.id) (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun = fun cf tgt_ctx -> (* Debug *) @@ -1599,7 +1600,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in let open InterpreterBorrowsCore in let lookup_shared_loan lid ctx : typed_value = - match snd (lookup_loan ek_all lid ctx) with + match snd (lookup_loan meta ek_all lid ctx) with | Concrete (VSharedLoan (_, v)) -> v | Abstract (ASharedLoan (_, v, _)) -> v | _ -> raise (Failure "Unreachable") 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 *) diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 4dc53586..d4a237b2 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -6,12 +6,13 @@ module Assoc = AssociatedTypes open TypesUtils open InterpreterUtils open InterpreterBorrowsCore +open Errors (** The local logger *) let log = Logging.projectors_log (** [ty] shouldn't contain erased regions *) -let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) +let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx) (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t) (v : typed_value) (ty : rty) : abstract_shared_borrows = (* Sanity check - TODO: move those elsewhere (here we perform the check at every @@ -34,12 +35,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) let proj_fields = List.map (fun (fv, fty) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions fv + apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions fv fty) fields_types in List.concat proj_fields - | VBottom, _ -> raise (Failure "Unreachable") + | VBottom, _ -> craise meta "Unreachable" | VBorrow bc, TRef (r, ref_ty, kind) -> (* Retrieve the bid of the borrow and the asb of the projected borrowed value *) let bid, asb = @@ -48,28 +49,28 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let asb = - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions + apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions bv ref_ty in (bid, asb) | VSharedBorrow bid, RShared -> (* Lookup the shared value *) let ek = ek_all in - let sv = lookup_loan ek bid ctx in + let sv = lookup_loan meta ek bid ctx in let asb = match sv with | _, Concrete (VSharedLoan (_, sv)) | _, Abstract (ASharedLoan (_, sv, _)) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow + apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions sv ref_ty - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in (bid, asb) | VReservedMutBorrow _, _ -> - raise - (Failure - "Can't apply a proj_borrow over a reserved mutable borrow") - | _ -> raise (Failure "Unreachable") + craise + meta + "Can't apply a proj_borrow over a reserved mutable borrow" + | _ -> craise meta "Unreachable" in let asb = (* Check if the region is in the set of projected regions (note that @@ -80,14 +81,14 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : eval_ctx) else asb in asb - | VLoan _, _ -> raise (Failure "Unreachable") + | VLoan _, _ -> craise meta "Unreachable" | VSymbolic s, _ -> (* Check that the projection doesn't contain ended regions *) - assert (not (projections_intersect s.sv_ty ctx.ended_regions ty regions)); + assert (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)); [ AsbProjReborrows (s, ty) ] - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" -let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) +let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (ctx : eval_ctx) (fresh_reborrow : BorrowId.id -> BorrowId.id) (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) : typed_avalue = @@ -111,12 +112,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) let proj_fields = List.map (fun (fv, fty) -> - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow + apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions fv fty) fields_types in AAdt { variant_id = adt.variant_id; field_values = proj_fields } - | VBottom, _ -> raise (Failure "Unreachable") + | VBottom, _ -> craise meta "Unreachable" | VBorrow bc, TRef (r, ref_ty, kind) -> if (* Check if the region is in the set of projected regions (note that @@ -129,7 +130,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let bv = - apply_proj_borrows check_symbolic_no_ended ctx + apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions bv ref_ty in AMutBorrow (bid, bv) @@ -147,11 +148,11 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) *) ASharedBorrow bid | VReservedMutBorrow _, _ -> - raise - (Failure + craise + meta "Can't apply a proj_borrow over a reserved mutable \ - borrow") - | _ -> raise (Failure "Unreachable") + borrow" + | _ -> craise meta "Unreachable" in ABorrow bc else @@ -163,7 +164,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) | VMutBorrow (bid, bv), RMut -> (* Apply the projection on the borrowed value *) let bv = - apply_proj_borrows check_symbolic_no_ended ctx + apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions bv ref_ty in (* If the borrow id is in the ancestor's regions, we still need @@ -176,25 +177,25 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) | VSharedBorrow bid, RShared -> (* Lookup the shared value *) let ek = ek_all in - let sv = lookup_loan ek bid ctx in + let sv = lookup_loan meta ek bid ctx in let asb = match sv with | _, Concrete (VSharedLoan (_, sv)) | _, Abstract (ASharedLoan (_, sv, _)) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow + apply_proj_borrows_on_shared_borrow meta ctx fresh_reborrow regions sv ref_ty - | _ -> raise (Failure "Unexpected") + | _ -> craise meta "Unexpected" in AProjSharedBorrow asb | VReservedMutBorrow _, _ -> - raise - (Failure + craise + meta "Can't apply a proj_borrow over a reserved mutable \ - borrow") - | _ -> raise (Failure "Unreachable") + borrow" + | _ -> craise meta "Unreachable" in ABorrow bc - | VLoan _, _ -> raise (Failure "Unreachable") + | VLoan _, _ -> craise meta "Unreachable" | VSymbolic s, _ -> (* Check that the projection doesn't contain already ended regions, * if necessary *) @@ -211,7 +212,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: " ^ RegionId.Set.to_string None rset2 ^ "\n")); - assert (not (projections_intersect ty1 rset1 ty2 rset2))); + assert (not (projections_intersect meta ty1 rset1 ty2 rset2))); ASymbolic (AProjBorrows (s, ty)) | _ -> log#lerror @@ -219,11 +220,11 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : eval_ctx) ("apply_proj_borrows: unexpected inputs:\n- input value: " ^ typed_value_to_string ctx v ^ "\n- proj rty: " ^ ty_to_string ctx ty)); - raise (Failure "Unreachable") + craise meta "Unreachable" in { value; ty } -let symbolic_expansion_non_borrow_to_value (sv : symbolic_value) +let symbolic_expansion_non_borrow_to_value (meta : Meta.meta) (sv : symbolic_value) (see : symbolic_expansion) : typed_value = let ty = Subst.erase_regions sv.sv_ty in let value = @@ -235,11 +236,11 @@ let symbolic_expansion_non_borrow_to_value (sv : symbolic_value) in VAdt { variant_id; field_values } | SeMutRef (_, _) | SeSharedRef (_, _) -> - raise (Failure "Unexpected symbolic reference expansion") + craise meta "Unexpected symbolic reference expansion" in { value; ty } -let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value) +let symbolic_expansion_non_shared_borrow_to_value (meta : Meta.meta) (sv : symbolic_value) (see : symbolic_expansion) : typed_value = match see with | SeMutRef (bid, bv) -> @@ -248,14 +249,14 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : symbolic_value) let value = VBorrow (VMutBorrow (bid, bv)) in { value; ty } | SeSharedRef (_, _) -> - raise (Failure "Unexpected symbolic shared reference expansion") - | _ -> symbolic_expansion_non_borrow_to_value sv see + craise meta "Unexpected symbolic shared reference expansion" + | _ -> symbolic_expansion_non_borrow_to_value meta sv see (** Apply (and reduce) a projector over loans to a value. TODO: detailed comments. See [apply_proj_borrows] *) -let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t) +let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t) (see : symbolic_expansion) (original_sv_ty : rty) : typed_avalue = (* Sanity check: if we have a proj_loans over a symbolic value, it should @@ -305,7 +306,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : RegionId.Set.t) else (* Not in the set: ignore *) (ALoan (AIgnoredSharedLoan child_av), ref_ty) - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in { value; ty } @@ -467,7 +468,7 @@ let apply_reborrows (reborrows : (BorrowId.id * BorrowId.id) list) (* Return *) ctx -let prepare_reborrows (config : config) (allow_reborrows : bool) : +let prepare_reborrows (meta : Meta.meta) (config : config) (allow_reborrows : bool) : (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx) = let reborrows : (BorrowId.id * BorrowId.id) list ref = ref [] in (* The function to generate and register fresh reborrows *) @@ -476,7 +477,7 @@ let prepare_reborrows (config : config) (allow_reborrows : bool) : let bid' = fresh_borrow_id () in reborrows := (bid, bid') :: !reborrows; bid') - else raise (Failure "Unexpected reborrow") + else craise meta "Unexpected reborrow" in (* The function to apply the reborrows in a context *) let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx = @@ -491,7 +492,7 @@ let prepare_reborrows (config : config) (allow_reborrows : bool) : (fresh_reborrow, apply_registered_reborrows) (** [ty] shouldn't have erased regions *) -let apply_proj_borrows_on_input_value (config : config) (ctx : eval_ctx) +let apply_proj_borrows_on_input_value (meta : Meta.meta) (config : config) (ctx : eval_ctx) (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) : eval_ctx * typed_avalue = assert (ty_is_rty ty); @@ -499,11 +500,11 @@ let apply_proj_borrows_on_input_value (config : config) (ctx : eval_ctx) let allow_reborrows = true in (* Prepare the reborrows *) let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows + prepare_reborrows meta config allow_reborrows in (* Apply the projector *) let av = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions + apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions v ty in (* Apply the reborrows *) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 6b9f47ce..bd6fab1a 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -11,6 +11,7 @@ open InterpreterProjectors open InterpreterExpansion open InterpreterPaths open InterpreterExpressions +open Errors module Subst = Substitute module S = SynthesizeSymbolic @@ -93,7 +94,7 @@ let push_vars (vars : (var * typed_value) list) : cm_fun = dummy variable and putting in its destination (after having checked that preparing the destination didn't introduce ⊥). *) -let assign_to_place (config : config) (rv : typed_value) (p : place) : cm_fun = +let assign_to_place (meta : Meta.meta) (config : config) (rv : typed_value) (p : place) : cm_fun = fun cf ctx -> log#ldebug (lazy @@ -118,7 +119,7 @@ let assign_to_place (config : config) (rv : typed_value) (p : place) : cm_fun = let ctx = ctx_push_dummy_var ctx dest_vid mv in (* Write to the destination *) (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) - assert (not (bottom_in_value ctx.ended_regions rv)); + cassert (not (bottom_in_value ctx.ended_regions rv)) meta "TODO: Error message"; (* Update the destination *) let ctx = write_place Write p rv ctx in (* Debug *) @@ -135,7 +136,7 @@ let assign_to_place (config : config) (rv : typed_value) (p : place) : cm_fun = comp cc move_dest cf ctx (** Evaluate an assertion, when the scrutinee is not symbolic *) -let eval_assertion_concrete (config : config) (assertion : assertion) : +let eval_assertion_concrete (meta : Meta.meta) (config : config) (assertion : assertion) : st_cm_fun = fun cf ctx -> (* There won't be any symbolic expansions: fully evaluate the operand *) @@ -147,8 +148,8 @@ let eval_assertion_concrete (config : config) (assertion : assertion) : (* Branch *) if b = assertion.expected then cf Unit ctx else cf Panic ctx | _ -> - raise - (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) + craise + meta ("Expected a boolean, got: " ^ typed_value_to_string ctx v) in (* Compose and apply *) comp eval_op eval_assert cf ctx @@ -159,14 +160,14 @@ let eval_assertion_concrete (config : config) (assertion : assertion) : a call to [assert ...] then continue in the success branch (and thus expand the boolean to [true]). *) -let eval_assertion (config : config) (assertion : assertion) : st_cm_fun = +let eval_assertion (meta : Meta.meta) (config : config) (assertion : assertion) : st_cm_fun = fun cf ctx -> (* Evaluate the operand *) let eval_op = eval_operand config assertion.cond in (* Evaluate the assertion *) let eval_assert cf (v : typed_value) : m_fun = fun ctx -> - assert (v.ty = TLiteral TBool); + cassert (v.ty = TLiteral TBool) meta "TODO: Error message"; (* We make a choice here: we could completely decouple the concrete and * symbolic executions here but choose not to. In the case where we * know the concrete value of the boolean we test, we use this value @@ -175,10 +176,10 @@ let eval_assertion (config : config) (assertion : assertion) : st_cm_fun = match v.value with | VLiteral (VBool _) -> (* Delegate to the concrete evaluation function *) - eval_assertion_concrete config assertion cf ctx + eval_assertion_concrete meta config assertion cf ctx | VSymbolic sv -> - assert (config.mode = SymbolicMode); - assert (sv.sv_ty = TLiteral TBool); + cassert (config.mode = SymbolicMode) meta "TODO: Error message"; + cassert (sv.sv_ty = TLiteral TBool) meta "TODO: Error message"; (* We continue the execution as if the test had succeeded, and thus * perform the symbolic expansion: sv ~~> true. * We will of course synthesize an assertion in the generated code @@ -192,8 +193,8 @@ let eval_assertion (config : config) (assertion : assertion) : st_cm_fun = (* Add the synthesized assertion *) S.synthesize_assertion ctx v expr | _ -> - raise - (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) + craise + meta ("Expected a boolean, got: " ^ typed_value_to_string ctx v) in (* Compose and apply *) comp eval_op eval_assert cf ctx @@ -209,7 +210,7 @@ let eval_assertion (config : config) (assertion : assertion) : st_cm_fun = a variant with all its fields set to {!Bottom}. For instance, something like: [Cons Bottom Bottom]. *) -let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) : +let set_discriminant (meta : Meta.meta) (config : config) (p : place) (variant_id : VariantId.id) : st_cm_fun = fun cf ctx -> log#ldebug @@ -234,7 +235,7 @@ let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) : a variant with all its fields set to {!Bottom} *) match av.variant_id with - | None -> raise (Failure "Found a struct value while expected an enum") + | None -> craise meta "Found a struct value while expected an enum" | Some variant_id' -> if variant_id' = variant_id then (* Nothing to do *) cf Unit ctx @@ -245,20 +246,20 @@ let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) : | TAdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in - assign_to_place config bottom_v p (cf Unit) ctx) + assign_to_place meta config bottom_v p (cf Unit) ctx) | TAdt ((TAdtId _ as type_id), generics), VBottom -> let bottom_v = match type_id with | TAdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in - assign_to_place config bottom_v p (cf Unit) ctx + assign_to_place meta config bottom_v p (cf Unit) ctx | _, VSymbolic _ -> - assert (config.mode = SymbolicMode); + cassert (config.mode = SymbolicMode) meta "The Config mode should be SymbolicMode"; (* This is a bit annoying: in theory we should expand the symbolic value * then set the discriminant, because in the case the discriminant is * exactly the one we set, the fields are left untouched, and in the @@ -266,10 +267,10 @@ let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) : * For now, we forbid setting the discriminant of a symbolic value: * setting a discriminant should only be used to initialize a value, * or reset an already initialized value, really. *) - raise (Failure "Unexpected value") - | _, (VAdt _ | VBottom) -> raise (Failure "Inconsistent state") + craise meta "Unexpected value" + | _, (VAdt _ | VBottom) -> craise meta "Inconsistent state" | _, (VLiteral _ | VBorrow _ | VLoan _) -> - raise (Failure "Unexpected value") + craise meta "Unexpected value" in (* Compose and apply *) comp cc update_value cf ctx @@ -284,15 +285,15 @@ let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) (** Small helper: compute the type of the return value for a specific instantiation of an assumed function. *) -let get_assumed_function_return_type (ctx : eval_ctx) (fid : assumed_fun_id) +let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) (fid : assumed_fun_id) (generics : generic_args) : ety = - assert (generics.trait_refs = []); + cassert (generics.trait_refs = []) meta "TODO: Error message"; (* [Box::free] has a special treatment *) match fid with | BoxFree -> - assert (generics.regions = []); - assert (List.length generics.types = 1); - assert (generics.const_generics = []); + cassert (generics.regions = []) meta "TODO: Error message"; + cassert (List.length generics.types = 1) meta "TODO: Error message"; + cassert (generics.const_generics = []) meta "TODO: Error message"; mk_unit_ty | _ -> (* Retrieve the function's signature *) @@ -319,7 +320,7 @@ let move_return_value (config : config) (pop_return_value : bool) cc (fun v ctx -> cf (Some v) ctx) ctx else cf None ctx -let pop_frame (config : config) (pop_return_value : bool) +let pop_frame (meta : Meta.meta) (config : config) (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun = fun ctx -> (* Debug *) @@ -329,7 +330,7 @@ let pop_frame (config : config) (pop_return_value : bool) let ret_vid = VarId.zero in let rec list_locals env = match env with - | [] -> raise (Failure "Inconsistent environment") + | [] -> craise meta "Inconsistent environment" | EAbs _ :: env -> list_locals env | EBinding (BDummy _, _) :: env -> list_locals env | EBinding (BVar var, _) :: env -> @@ -353,7 +354,7 @@ let pop_frame (config : config) (pop_return_value : bool) match ret_value with | None -> () | Some ret_value -> - assert (not (bottom_in_value ctx.ended_regions ret_value))) + cassert (not (bottom_in_value ctx.ended_regions ret_value)) meta "TODO: Error message" ) in (* Drop the outer *loans* we find in the local variables *) @@ -384,7 +385,7 @@ let pop_frame (config : config) (pop_return_value : bool) * no outer loans) as dummy variables in the caller frame *) let rec pop env = match env with - | [] -> raise (Failure "Inconsistent environment") + | [] -> craise meta "Inconsistent environment" | EAbs abs :: env -> EAbs abs :: pop env | EBinding (_, v) :: env -> let vid = fresh_dummy_var_id () in @@ -401,15 +402,15 @@ let pop_frame (config : config) (pop_return_value : bool) comp cc cf_pop cf ctx (** Pop the current frame and assign the returned value to its destination. *) -let pop_frame_assign (config : config) (dest : place) : cm_fun = - let cf_pop = pop_frame config true in +let pop_frame_assign (meta : Meta.meta) (config : config) (dest : place) : cm_fun = + let cf_pop = pop_frame meta config true in let cf_assign cf ret_value : m_fun = - assign_to_place config (Option.get ret_value) dest cf + assign_to_place meta config (Option.get ret_value) dest cf in comp cf_pop cf_assign (** Auxiliary function - see {!eval_assumed_function_call} *) -let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = +let eval_box_new_concrete (meta : Meta.meta) (config : config) (generics : generic_args) : cm_fun = fun cf ctx -> (* Check and retrieve the arguments *) match @@ -422,7 +423,7 @@ let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = :: EBinding (_ret_var, _) :: EFrame :: _ ) -> (* Required type checking *) - assert (input_value.ty = boxed_ty); + cassert (input_value.ty = boxed_ty) meta "TODO: Error message"; (* Move the input value *) let cf_move = @@ -441,7 +442,7 @@ let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = (* Move this value to the return variable *) let dest = mk_place_from_var_id VarId.zero in - let cf_assign = assign_to_place config box_v dest in + let cf_assign = assign_to_place meta config box_v dest in (* Continue *) cf_assign cf @@ -449,7 +450,7 @@ let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = (* Compose and apply *) comp cf_move cf_create cf ctx - | _ -> raise (Failure "Inconsistent state") + | _ -> craise meta "Inconsistent state" (** Auxiliary function - see {!eval_assumed_function_call}. @@ -470,7 +471,7 @@ let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun = It thus updates the box value (by calling {!drop_value}) and updates the destination (by setting it to [()]). *) -let eval_box_free (config : config) (generics : generic_args) +let eval_box_free (meta : Meta.meta) (config : config) (generics : generic_args) (args : operand list) (dest : place) : cm_fun = fun cf ctx -> match (generics.regions, generics.types, generics.const_generics, args) with @@ -478,32 +479,33 @@ let eval_box_free (config : config) (generics : generic_args) (* Required type checking *) let input_box = InterpreterPaths.read_place Write input_box_place ctx in (let input_ty = ty_get_box input_box.ty in - assert (input_ty = boxed_ty)); + cassert (input_ty = boxed_ty)) meta "TODO: Error message"; (* Drop the value *) let cc = drop_value config input_box_place in (* Update the destination by setting it to [()] *) - let cc = comp cc (assign_to_place config mk_unit_value dest) in + let cc = comp cc (assign_to_place meta config mk_unit_value dest) in (* Continue *) cc cf ctx - | _ -> raise (Failure "Inconsistent state") + | _ -> craise meta "Inconsistent state" (** Evaluate a non-local function call in concrete mode *) -let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) +let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fid : assumed_fun_id) (call : call) : cm_fun = let args = call.args in let dest = call.dest in match call.func with | FnOpMove _ -> (* Closure case: TODO *) - raise (Failure "Closures are not supported yet") + craise meta "Closures are not supported yet" | FnOpRegular func -> ( let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - assert (generics.const_generics = []); + cassert (generics.const_generics = []) meta "The const generic vars environment + in concrete mode is not fully handled yet"; (* There are two cases (and this is extremely annoying): - the function is not box_free - the function is box_free @@ -512,7 +514,7 @@ let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) match fid with | BoxFree -> (* Degenerate case: box_free *) - eval_box_free config generics args dest + eval_box_free meta config generics args dest | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) @@ -534,7 +536,7 @@ let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) (* Create and push the return variable *) let ret_vid = VarId.zero in - let ret_ty = get_assumed_function_return_type ctx fid generics in + let ret_ty = get_assumed_function_return_type meta ctx fid generics in let ret_var = mk_var ret_vid (Some "@return") ret_ty in let cc = comp cc (push_uninitialized_var ret_var) in @@ -551,20 +553,20 @@ let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) * access to a body. *) let cf_eval_body : cm_fun = match fid with - | BoxNew -> eval_box_new_concrete config generics + | BoxNew -> eval_box_new_concrete meta config generics | BoxFree -> (* Should have been treated above *) - raise (Failure "Unreachable") + craise meta "Unreachable" | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut -> - raise (Failure "Unimplemented") + craise meta "Unimplemented" in let cc = comp cc cf_eval_body in (* Pop the frame *) - let cc = comp cc (pop_frame_assign config dest) in + let cc = comp cc (pop_frame_assign meta config dest) in (* Continue *) cc cf ctx @@ -727,7 +729,7 @@ let create_push_abstractions_from_abs_region_groups which means that whenever we call a provided trait method, we do not refer to a trait clause but directly to the method provided in the trait declaration. *) -let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) +let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) (call : call) (ctx : eval_ctx) : fun_id_or_trait_method_ref * generic_args @@ -738,7 +740,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) match call.func with | FnOpMove _ -> (* Closure case: TODO *) - raise (Failure "Closures are not supported yet") + craise meta "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> @@ -762,7 +764,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) (func.func, func.generics, None, def, regions_hierarchy, inst_sg) | FunId (FAssumed _) -> (* Unreachable: must be a transparent function *) - raise (Failure "Unreachable") + craise meta "Unreachable" | TraitMethod (trait_ref, method_name, _) -> ( log#ldebug (lazy @@ -822,7 +824,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) | None -> (* If not found, lookup the methods provided by the trait *declaration* (remember: for now, we forbid overriding provided methods) *) - assert (trait_impl.provided_methods = []); + cassert (trait_impl.provided_methods = []) meta "Overriding provided methods is currently forbidden"; let trait_decl = ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id @@ -922,7 +924,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) inst_sg ))) (** Evaluate a statement *) -let rec eval_statement (config : config) (st : statement) : st_cm_fun = +let rec eval_statement (meta : Meta.meta) (config : config) (st : statement) : st_cm_fun = fun cf ctx -> (* Debugging *) log#ldebug @@ -937,7 +939,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = * checking the invariants *) let cc = comp cc (greedy_expand_symbolic_values config) in (* Sanity check *) - let cc = comp cc Invariants.cf_check_invariants in + let cc = comp cc (Invariants.cf_check_invariants meta) in (* Evaluate *) let cf_eval_st cf : m_fun = @@ -953,7 +955,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = match rvalue with | Global (gid, generics) -> (* Evaluate the global *) - eval_global config p gid generics cf ctx + eval_global meta config p gid generics cf ctx | _ -> (* Evaluate the rvalue *) let cf_eval_rvalue = eval_rvalue_not_global config rvalue in @@ -966,13 +968,13 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = match res with | Error EPanic -> cf Panic ctx | Ok rv -> ( - let expr = assign_to_place config rv p (cf Unit) ctx in + let expr = assign_to_place meta config rv p (cf Unit) ctx in (* Update the synthesized AST - here we store meta-information. * We do it only in specific cases (it is not always useful, and * also it can lead to issues - for instance, if we borrow a * reserved borrow, we later can't translate it to pure values...) *) match rvalue with - | Global _ -> raise (Failure "Unreachable") + | Global _ -> craise meta "Unreachable" | Use _ | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> @@ -990,10 +992,10 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = comp cf_eval_rvalue cf_assign cf ctx) | FakeRead p -> eval_fake_read config p (cf Unit) ctx | SetDiscriminant (p, variant_id) -> - set_discriminant config p variant_id cf ctx + set_discriminant meta config p variant_id cf ctx | Drop p -> drop_value config p (cf Unit) ctx - | Assert assertion -> eval_assertion config assertion cf ctx - | Call call -> eval_function_call config call cf ctx + | Assert assertion -> eval_assertion meta config assertion cf ctx + | Call call -> eval_function_call meta config call cf ctx | Panic -> cf Panic ctx | Return -> cf Return ctx | Break i -> cf (Break i) ctx @@ -1001,12 +1003,12 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = | Nop -> cf Unit ctx | Sequence (st1, st2) -> (* Evaluate the first statement *) - let cf_st1 = eval_statement config st1 in + let cf_st1 = eval_statement meta config st1 in (* Evaluate the sequence *) let cf_st2 cf res = match res with (* Evaluation successful: evaluate the second statement *) - | Unit -> eval_statement config st2 cf + | Unit -> eval_statement meta config st2 cf (* Control-flow break: transmit. We enumerate the cases on purpose *) | Panic | Break _ | Continue _ | Return | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> @@ -1016,14 +1018,14 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = comp cf_st1 cf_st2 cf ctx | Loop loop_body -> InterpreterLoops.eval_loop config st.meta - (eval_statement config loop_body) + (eval_statement meta config loop_body) cf ctx - | Switch switch -> eval_switch config switch cf ctx + | Switch switch -> eval_switch meta config switch cf ctx in (* Compose and apply *) comp cc cf_eval_st cf ctx -and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) +and eval_global (meta : Meta.meta) (config : config) (dest : place) (gid : GlobalDeclId.id) (generics : generic_args) : st_cm_fun = fun cf ctx -> let global = ctx_lookup_global_decl ctx gid in @@ -1032,11 +1034,11 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) (* Treat the evaluation of the global as a call to the global body *) let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in - (eval_transparent_function_call_concrete config global.body call) cf ctx + (eval_transparent_function_call_concrete meta config global.body call) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) - assert (ty_no_regions global.ty); + cassert (ty_no_regions global.ty) meta "TODO: Error message"; (* Instantiate the type *) (* There shouldn't be any reference to Self *) let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in @@ -1050,13 +1052,13 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) in let sval = mk_fresh_symbolic_value ty in let cc = - assign_to_place config (mk_typed_value_from_symbolic_value sval) dest + assign_to_place meta config (mk_typed_value_from_symbolic_value sval) dest in let e = cc (cf Unit) ctx in S.synthesize_global_eval gid generics sval e (** Evaluate a switch *) -and eval_switch (config : config) (switch : switch) : st_cm_fun = +and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_fun = fun cf ctx -> (* We evaluate the operand in two steps: * first we prepare it, then we check if its value is concrete or @@ -1081,20 +1083,20 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = (* Evaluate the if and the branch body *) let cf_branch cf : m_fun = (* Branch *) - if b then eval_statement config st1 cf - else eval_statement config st2 cf + if b then eval_statement meta config st1 cf + else eval_statement meta config st2 cf in (* Compose the continuations *) cf_branch cf ctx | VSymbolic sv -> (* Expand the symbolic boolean, and continue by evaluating * the branches *) - let cf_true : st_cm_fun = eval_statement config st1 in - let cf_false : st_cm_fun = eval_statement config st2 in + let cf_true : st_cm_fun = eval_statement meta config st1 in + let cf_false : st_cm_fun = eval_statement meta config st2 in expand_symbolic_bool config sv (S.mk_opt_place_from_op op ctx) cf_true cf_false cf ctx - | _ -> raise (Failure "Inconsistent state") + | _ -> craise meta "Inconsistent state" in (* Compose *) comp cf_eval_op cf_if cf ctx @@ -1109,11 +1111,11 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = (* Evaluate the branch *) let cf_eval_branch cf = (* Sanity check *) - assert (sv.int_ty = int_ty); + cassert (sv.int_ty = int_ty) meta "TODO: Error message"; (* Find the branch *) match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with - | None -> eval_statement config otherwise cf - | Some (_, tgt) -> eval_statement config tgt cf + | None -> eval_statement meta config otherwise cf + | Some (_, tgt) -> eval_statement meta config tgt cf in (* Compose *) cf_eval_branch cf ctx @@ -1122,7 +1124,7 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = * proper branches *) let stgts = List.map - (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st)) + (fun (cv, tgt_st) -> (cv, eval_statement meta config tgt_st)) stgts in (* Several branches may be grouped together: every branch is described @@ -1136,12 +1138,12 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = stgts) in (* Translate the otherwise branch *) - let otherwise = eval_statement config otherwise in + let otherwise = eval_statement meta config otherwise in (* Expand and continue *) expand_symbolic_int config sv (S.mk_opt_place_from_op op ctx) int_ty stgts otherwise cf ctx - | _ -> raise (Failure "Inconsistent state") + | _ -> craise meta "Inconsistent state" in (* Compose *) comp cf_eval_op cf_switch cf ctx @@ -1167,9 +1169,9 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with | None -> ( match otherwise with - | None -> raise (Failure "No otherwise branch") - | Some otherwise -> eval_statement config otherwise cf ctx) - | Some (_, tgt) -> eval_statement config tgt cf ctx) + | None -> craise meta "No otherwise branch" + | Some otherwise -> eval_statement meta config otherwise cf ctx) + | Some (_, tgt) -> eval_statement meta config tgt cf ctx) | VSymbolic sv -> (* Expand the symbolic value - may lead to branching *) let cf_expand = @@ -1177,8 +1179,8 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = in (* Re-evaluate the switch - the value is not symbolic anymore, which means we will go to the other branch *) - cf_expand (eval_switch config switch) cf ctx - | _ -> raise (Failure "Inconsistent state") + cf_expand (eval_switch meta config switch) cf ctx + | _ -> craise meta "Inconsistent state" in (* Compose *) comp cf_read_p cf_match cf ctx @@ -1187,54 +1189,54 @@ and eval_switch (config : config) (switch : switch) : st_cm_fun = cf_match cf ctx (** Evaluate a function call (auxiliary helper for [eval_statement]) *) -and eval_function_call (config : config) (call : call) : st_cm_fun = +and eval_function_call (meta : Meta.meta) (config : config) (call : call) : st_cm_fun = (* There are several cases: - this is a local function, in which case we execute its body - this is an assumed function, in which case there is a special treatment - this is a trait method *) match config.mode with - | ConcreteMode -> eval_function_call_concrete config call - | SymbolicMode -> eval_function_call_symbolic config call + | ConcreteMode -> eval_function_call_concrete meta config call + | SymbolicMode -> eval_function_call_symbolic meta config call -and eval_function_call_concrete (config : config) (call : call) : st_cm_fun = +and eval_function_call_concrete (meta : Meta.meta) (config : config) (call : call) : st_cm_fun = fun cf ctx -> match call.func with - | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpMove _ -> craise meta "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> - eval_transparent_function_call_concrete config fid call cf ctx + eval_transparent_function_call_concrete meta config fid call cf ctx | FunId (FAssumed fid) -> (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) - eval_assumed_function_call_concrete config fid call (cf Unit) ctx - | TraitMethod _ -> raise (Failure "Unimplemented")) + eval_assumed_function_call_concrete meta config fid call (cf Unit) ctx + | TraitMethod _ -> craise meta "Unimplemented") -and eval_function_call_symbolic (config : config) (call : call) : st_cm_fun = +and eval_function_call_symbolic (meta : Meta.meta) (config : config) (call : call) : st_cm_fun = match call.func with - | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpMove _ -> craise meta "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular _) | TraitMethod _ -> - eval_transparent_function_call_symbolic config call + eval_transparent_function_call_symbolic meta config call | FunId (FAssumed fid) -> - eval_assumed_function_call_symbolic config fid call func) + eval_assumed_function_call_symbolic meta config fid call func) (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_transparent_function_call_concrete (config : config) +and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config) (fid : FunDeclId.id) (call : call) : st_cm_fun = let args = call.args in let dest = call.dest in match call.func with - | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpMove _ -> craise meta "Closures are not supported yet" | FnOpRegular func -> let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) - assert (generics.const_generics = []); + cassert (generics.const_generics = []) meta "The const generic vars environment in concrete mode is not fully handled yet"; fun cf ctx -> (* Retrieve the (correctly instantiated) body *) let def = ctx_lookup_fun_decl ctx fid in @@ -1242,14 +1244,14 @@ and eval_transparent_function_call_concrete (config : config) let body = match def.body with | None -> - raise - (Failure + craise + meta ("Can't evaluate a call to an opaque function: " - ^ name_to_string ctx def.name)) + ^ name_to_string ctx def.name) | Some body -> body in (* TODO: we need to normalize the types if we want to correctly support traits *) - assert (generics.trait_refs = []); + cassert (generics.trait_refs = []) meta "Traits are not supported yet TODO: error message"; (* There shouldn't be any reference to Self *) let tr_self = UnknownTrait __FUNCTION__ in let subst = @@ -1258,7 +1260,7 @@ and eval_transparent_function_call_concrete (config : config) let locals, body_st = Subst.fun_body_substitute_in_body subst body in (* Evaluate the input operands *) - assert (List.length args = body.arg_count); + cassert (List.length args = body.arg_count) meta "TODO: Error message"; let cc = eval_operands config args in (* Push a frame delimiter - we use {!comp_transmit} to transmit the result @@ -1271,7 +1273,7 @@ and eval_transparent_function_call_concrete (config : config) let ret_var, locals = match locals with | ret_ty :: locals -> (ret_ty, locals) - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in let input_locals, locals = Collections.List.split_at locals body.arg_count @@ -1294,7 +1296,7 @@ and eval_transparent_function_call_concrete (config : config) let cc = comp cc (push_uninitialized_vars locals) in (* Execute the function body *) - let cc = comp cc (eval_function_body config body_st) in + let cc = comp cc (eval_function_body meta config body_st) in (* Pop the stack frame and move the return value to its destination *) let cf_finish cf res = @@ -1303,10 +1305,10 @@ and eval_transparent_function_call_concrete (config : config) | Return -> (* Pop the stack frame, retrieve the return value, move it to * its destination and continue *) - pop_frame_assign config dest (cf Unit) + pop_frame_assign meta config dest (cf Unit) | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> - raise (Failure "Unreachable") + craise meta "Unreachable" in let cc = comp cc cf_finish in @@ -1314,16 +1316,16 @@ and eval_transparent_function_call_concrete (config : config) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_transparent_function_call_symbolic (config : config) (call : call) : +and eval_transparent_function_call_symbolic (meta : Meta.meta) (config : config) (call : call) : st_cm_fun = fun cf ctx -> let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg = - eval_transparent_function_call_symbolic_inst call ctx + eval_transparent_function_call_symbolic_inst meta call ctx in (* Sanity check *) - assert (List.length call.args = List.length def.signature.inputs); + cassert (List.length call.args = List.length def.signature.inputs) meta "TODO: Error message"; (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config func def.signature + eval_function_call_symbolic_from_inst_sig meta config func def.signature regions_hierarchy inst_sg generics trait_method_generics call.args call.dest cf ctx @@ -1338,7 +1340,7 @@ and eval_transparent_function_call_symbolic (config : config) (call : call) : overriding them. We treat them as regular method, which take an additional trait ref as input. *) -and eval_function_call_symbolic_from_inst_sig (config : config) +and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : config) (fid : fun_id_or_trait_method_ref) (sg : fun_sig) (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig) (generics : generic_args) @@ -1377,20 +1379,20 @@ and eval_function_call_symbolic_from_inst_sig (config : config) let args_with_rtypes = List.combine args inst_sg.inputs in (* Check the type of the input arguments *) - assert ( + cassert ( List.for_all (fun ((arg, rty) : typed_value * rty) -> arg.ty = Subst.erase_regions rty) - args_with_rtypes); + args_with_rtypes) meta "TODO: Error message"; (* Check that the input arguments don't contain symbolic values that can't * be fed to functions (i.e., symbolic values output from function return * values and which contain borrows of borrows can't be used as function * inputs *) - assert ( + cassert ( List.for_all (fun arg -> not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) - args); + args) meta "The input argument should not contain symbolic values that can't be fed to functions TODO: error message"; (* Initialize the abstractions and push them in the context. * First, we define the function which, given an initialized, empty @@ -1429,7 +1431,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) let cc = comp cc cf_call in (* Move the return value to its destination *) - let cc = comp cc (assign_to_place config ret_value dest) in + let cc = comp cc (assign_to_place meta config ret_value dest) in (* End the abstractions which don't contain loans and don't have parent * abstractions. @@ -1450,7 +1452,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (* Check if it contains non-ignored loans *) && Option.is_none (InterpreterBorrowsCore - .get_first_non_ignored_aloan_in_abstraction abs)) + .get_first_non_ignored_aloan_in_abstraction meta abs)) !abs_ids in (* Check if there are abstractions to end *) @@ -1485,7 +1487,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) cc (cf Unit) ctx (** Evaluate a non-local function call in symbolic mode *) -and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) +and eval_assumed_function_call_symbolic (meta : Meta.meta) (config : config) (fid : assumed_fun_id) (call : call) (func : fn_ptr) : st_cm_fun = fun cf ctx -> let generics = func.generics in @@ -1493,10 +1495,10 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) let dest = call.dest in (* Sanity check: make sure the type parameters don't contain regions - * this is a current limitation of our synthesis *) - assert ( + cassert ( List.for_all (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty)) - generics.types); + generics.types) meta "The parameters should not contain regions TODO: error message"; (* There are two cases (and this is extremely annoying): - the function is not box_free @@ -1507,7 +1509,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) | BoxFree -> (* Degenerate case: box_free - note that this is not really a function * call: no need to call a "synthesize_..." function *) - eval_box_free config generics args dest (cf Unit) ctx + eval_box_free meta config generics args dest (cf Unit) ctx | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined @@ -1517,7 +1519,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) match fid with | BoxFree -> (* Should have been treated above *) - raise (Failure "Unreachable") + craise meta "Unreachable" | _ -> let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FAssumed fid) @@ -1533,14 +1535,14 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) in (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config (FunId (FAssumed fid)) sg + eval_function_call_symbolic_from_inst_sig meta config (FunId (FAssumed fid)) sg regions_hierarchy inst_sig generics None args dest cf ctx (** Evaluate a statement seen as a function body *) -and eval_function_body (config : config) (body : statement) : st_cm_fun = +and eval_function_body (meta : Meta.meta) (config : config) (body : statement) : st_cm_fun = fun cf ctx -> log#ldebug (lazy "eval_function_body:"); - let cc = eval_statement config body in + let cc = eval_statement meta config body in let cf_finish cf res = log#ldebug (lazy "eval_function_body: cf_finish"); (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we @@ -1549,7 +1551,7 @@ and eval_function_body (config : config) (body : statement) : st_cm_fun = * checking the invariants *) let cc = greedy_expand_symbolic_values config in (* Sanity check *) - let cc = comp_check_ctx cc Invariants.check_invariants in + let cc = comp_check_ctx cc (Invariants.check_invariants meta) in (* Continue *) cc (cf res) in diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index b87cdff7..871bf90d 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -8,6 +8,7 @@ open Cps open TypesUtils open InterpreterUtils open InterpreterBorrowsCore +open Errors (** The local logger *) let log = Logging.invariants_log @@ -47,7 +48,7 @@ type borrow_kind = BMut | BShared | BReserved - loans and borrows are correctly related - a two-phase borrow can't point to a value inside an abstraction *) -let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit = +let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Link all the borrow ids to a representant - necessary because of shared * borrows/loans *) let ids_reprs : BorrowId.id BorrowId.Map.t ref = ref BorrowId.Map.empty in @@ -183,7 +184,7 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit = ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string () in log#serror err; - raise (Failure err) + craise meta err in let update_info (bid : BorrowId.id) (info : borrow_info) : unit = @@ -195,7 +196,7 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit = (fun x -> match x with | Some _ -> Some info - | None -> raise (Failure "Unreachable")) + | None -> craise meta "Unreachable") !borrows_infos in borrows_infos := infos @@ -209,7 +210,7 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit = (* Check that the borrow kind is consistent *) (match (info.loan_kind, kind) with | RShared, (BShared | BReserved) | RMut, BMut -> () - | _ -> raise (Failure "Invariant not satisfied")); + | _ -> craise meta "Invariant not satisfied"); (* A reserved borrow can't point to a value inside an abstraction *) assert (kind <> BReserved || not info.loan_in_abs); (* Insert the borrow id *) @@ -366,13 +367,13 @@ let check_borrowed_values_invariant (ctx : eval_ctx) : unit = let info = { outer_borrow = false; outer_shared = false } in visitor#visit_eval_ctx info ctx -let check_literal_type (cv : literal) (ty : literal_type) : unit = +let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) : unit = match (cv, ty) with | VScalar sv, TInteger int_ty -> assert (sv.int_ty = int_ty) | VBool _, TBool | VChar _, TChar -> () - | _ -> raise (Failure "Erroneous typing") + | _ -> craise meta "Erroneous typing" -let check_typing_invariant (ctx : eval_ctx) : unit = +let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (* TODO: the type of aloans doens't make sense: they have a type * of the shape [& (mut) T] where they should have type [T]... * This messes a bit the type invariant checks when checking the @@ -405,7 +406,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit = assert (ty_is_ety tv.ty); (* Check the current pair (value, type) *) (match (tv.value, tv.ty) with - | VLiteral cv, TLiteral ty -> check_literal_type cv ty + | VLiteral cv, TLiteral ty -> check_literal_type meta cv ty (* ADT case *) | VAdt av, TAdt (TAdtId def_id, generics) -> (* Retrieve the definition to check the variant id, the number of @@ -420,7 +421,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit = | Some variant_id, Enum variants -> assert (VariantId.to_int variant_id < List.length variants) | None, Struct _ -> () - | _ -> raise (Failure "Erroneous typing")); + | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) let field_types = AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def @@ -469,39 +470,39 @@ let check_typing_invariant (ctx : eval_ctx) : unit = .value in assert (Z.of_int (List.length inner_values) = len) - | (TSlice | TStr), _, _, _, _ -> raise (Failure "Unexpected") - | _ -> raise (Failure "Erroneous type")) + | (TSlice | TStr), _, _, _, _ -> craise meta "Unexpected" + | _ -> craise meta "Erroneous type") | VBottom, _ -> (* Nothing to check *) () | VBorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with | VSharedBorrow bid, RShared | VReservedMutBorrow bid, RMut -> ( (* Lookup the borrowed value to check it has the proper type *) - let _, glc = lookup_loan ek_all bid ctx in + let _, glc = lookup_loan meta ek_all bid ctx in match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> assert (sv.ty = ref_ty) - | _ -> raise (Failure "Inconsistent context")) + | _ -> craise meta "Inconsistent context") | VMutBorrow (_, bv), RMut -> assert ( (* Check that the borrowed value has the proper type *) bv.ty = ref_ty) - | _ -> raise (Failure "Erroneous typing")) + | _ -> craise meta "Erroneous typing") | VLoan lc, ty -> ( match lc with | VSharedLoan (_, sv) -> assert (sv.ty = ty) | VMutLoan bid -> ( (* Lookup the borrowed value to check it has the proper type *) - let glc = lookup_borrow ek_all bid ctx in + let glc = lookup_borrow meta ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> assert (bv.ty = ty) | Abstract (AMutBorrow (_, sv)) -> assert (Substitute.erase_regions sv.ty = ty) - | _ -> raise (Failure "Inconsistent context"))) + | _ -> craise meta "Inconsistent context")) | VSymbolic sv, ty -> let ty' = Substitute.erase_regions sv.sv_ty in assert (ty' = ty) - | _ -> raise (Failure "Erroneous typing")); + | _ -> craise meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_value info tv @@ -535,7 +536,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit = | Some variant_id, Enum variants -> assert (VariantId.to_int variant_id < List.length variants) | None, Struct _ -> () - | _ -> raise (Failure "Erroneous typing")); + | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) let field_types = AssociatedTypes.type_decl_get_inst_norm_field_rtypes ctx def @@ -571,7 +572,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit = (* Box *) | TBox, [ boxed_value ], [], [ boxed_ty ], [] -> assert (boxed_value.ty = boxed_ty) - | _ -> raise (Failure "Erroneous type")) + | _ -> craise meta "Erroneous type") | ABottom, _ -> (* Nothing to check *) () | ABorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with @@ -580,19 +581,19 @@ let check_typing_invariant (ctx : eval_ctx) : unit = assert (av.ty = ref_ty) | ASharedBorrow bid, RShared -> ( (* Lookup the borrowed value to check it has the proper type *) - let _, glc = lookup_loan ek_all bid ctx in + let _, glc = lookup_loan meta ek_all bid ctx in match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> assert (sv.ty = Substitute.erase_regions ref_ty) - | _ -> raise (Failure "Inconsistent context")) + | _ -> craise meta "Inconsistent context") | AIgnoredMutBorrow (_opt_bid, av), RMut -> assert (av.ty = ref_ty) | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ }, RMut ) -> assert (given_back.ty = ref_ty); assert (child.ty = ref_ty) | AProjSharedBorrow _, RShared -> () - | _ -> raise (Failure "Inconsistent context")) + | _ -> craise meta "Inconsistent context") | ALoan lc, aty -> ( match lc with | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av) @@ -600,7 +601,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit = let borrowed_aty = aloan_get_expected_child_type aty in assert (child_av.ty = borrowed_aty); (* Lookup the borrowed value to check it has the proper type *) - let glc = lookup_borrow ek_all bid ctx in + let glc = lookup_borrow meta ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> assert (bv.ty = Substitute.erase_regions borrowed_aty) @@ -608,7 +609,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit = assert ( Substitute.erase_regions sv.ty = Substitute.erase_regions borrowed_aty) - | _ -> raise (Failure "Inconsistent context")) + | _ -> craise meta "Inconsistent context") | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in assert (child_av.ty = borrowed_aty) @@ -647,7 +648,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit = match proj with | AProjBorrows (_sv, ty') -> assert (ty' = ty) | AEndedProjBorrows _ | AIgnoredProjBorrows -> () - | _ -> raise (Failure "Unexpected")) + | _ -> craise meta "Unexpected") given_back_ls | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()) | AIgnored, _ -> () @@ -658,7 +659,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit = ^ "\n- value: " ^ typed_avalue_to_string ctx atv ^ "\n- type: " ^ ty_to_string ctx atv.ty)); - raise (Failure "Erroneous typing")); + craise meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv end @@ -697,7 +698,7 @@ type sv_info = { - the union of the aproj_loans contains the aproj_borrows applied on the same symbolic values *) -let check_symbolic_values (ctx : eval_ctx) : unit = +let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Small utility *) let module M = SymbolicValueId.Map in let infos : sv_info M.t ref = ref M.empty in @@ -796,24 +797,24 @@ let check_symbolic_values (ctx : eval_ctx) : unit = List.iter (fun binfo -> assert ( - projection_contains info.ty loan_regions binfo.proj_ty binfo.regions)) + projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions)) info.aproj_borrows; () in M.iter check_info !infos -let check_invariants (ctx : eval_ctx) : unit = +let check_invariants (meta : Meta.meta) (ctx : eval_ctx) : unit = if !Config.sanity_checks then ( log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx)); - check_loans_borrows_relation_invariant ctx; + check_loans_borrows_relation_invariant meta ctx; check_borrowed_values_invariant ctx; - check_typing_invariant ctx; - check_symbolic_values ctx) + check_typing_invariant meta ctx; + check_symbolic_values meta ctx) else log#ldebug (lazy "Not checking invariants (check is not activated)") (** Same as {!check_invariants}, but written in CPS *) -let cf_check_invariants : cm_fun = +let cf_check_invariants (meta : Meta.meta) : cm_fun = fun cf ctx -> - check_invariants ctx; + check_invariants meta ctx; cf ctx diff --git a/compiler/Main.ml b/compiler/Main.ml index e703f1a0..e4e4ce1f 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -113,7 +113,7 @@ let () = Arg.Clear lean_gen_lakefile, " Generate a default lakefile.lean (Lean only)" ); ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC"); - ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error"); + ("-abort-on-error", Arg.Set fail_hard, " Fail hard (fail on first error) in case of error"); ( "-tuple-nested-proj", Arg.Set use_nested_tuple_projectors, " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \ @@ -274,7 +274,7 @@ let () = if !test_unit_functions then Test.test_unit_functions m; (* Translate the functions *) - Aeneas.Translate.translate_crate filename dest_dir m; + Aeneas.Translate.translate_crate meta filename dest_dir m; (* Print total elapsed time *) log#linfo diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 3fa550cc..b612ab70 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -5,6 +5,7 @@ open PureUtils open InterpreterUtils open FunsAnalysis open TypesAnalysis +open Errors module T = Types module V = Values module C = Contexts @@ -395,40 +396,40 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : (* Some generic translation functions (we need to translate different "flavours" of types: forward types, backward types, etc.) *) -let rec translate_generic_args (translate_ty : T.ty -> ty) +let rec translate_generic_args (meta : Meta.meta) (translate_ty : T.ty -> ty) (generics : T.generic_args) : generic_args = (* We ignore the regions: if they didn't cause trouble for the symbolic execution, then everything's fine *) let types = List.map translate_ty generics.types in let const_generics = generics.const_generics in let trait_refs = - List.map (translate_trait_ref translate_ty) generics.trait_refs + List.map (translate_trait_ref meta translate_ty) generics.trait_refs in { types; const_generics; trait_refs } -and translate_trait_ref (translate_ty : T.ty -> ty) (tr : T.trait_ref) : +and translate_trait_ref (meta : Meta.meta) (translate_ty : T.ty -> ty) (tr : T.trait_ref) : trait_ref = - let trait_id = translate_trait_instance_id translate_ty tr.trait_id in - let generics = translate_generic_args translate_ty tr.generics in + let trait_id = translate_trait_instance_id meta translate_ty tr.trait_id in + let generics = translate_generic_args meta translate_ty tr.generics in let trait_decl_ref = - translate_trait_decl_ref translate_ty tr.trait_decl_ref + translate_trait_decl_ref meta translate_ty tr.trait_decl_ref in { trait_id; generics; trait_decl_ref } -and translate_trait_decl_ref (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref) +and translate_trait_decl_ref (meta : Meta.meta) (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref) : trait_decl_ref = - let decl_generics = translate_generic_args translate_ty tr.decl_generics in + let decl_generics = translate_generic_args meta translate_ty tr.decl_generics in { trait_decl_id = tr.trait_decl_id; decl_generics } -and translate_trait_instance_id (translate_ty : T.ty -> ty) +and translate_trait_instance_id (meta : Meta.meta) (translate_ty : T.ty -> ty) (id : T.trait_instance_id) : trait_instance_id = - let translate_trait_instance_id = translate_trait_instance_id translate_ty in + let translate_trait_instance_id = translate_trait_instance_id meta translate_ty in match id with | T.Self -> Self | TraitImpl id -> TraitImpl id | BuiltinOrAuto _ -> (* We should have eliminated those in the prepasses *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Clause id -> Clause id | ParentClause (inst_id, decl_id, clause_id) -> let inst_id = translate_trait_instance_id inst_id in @@ -436,16 +437,16 @@ and translate_trait_instance_id (translate_ty : T.ty -> ty) | ItemClause (inst_id, decl_id, item_name, clause_id) -> let inst_id = translate_trait_instance_id inst_id in ItemClause (inst_id, decl_id, item_name, clause_id) - | TraitRef tr -> TraitRef (translate_trait_ref translate_ty tr) - | FnPointer _ | Closure _ -> raise (Failure "Closures are not supported yet") - | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s)) + | TraitRef tr -> TraitRef (translate_trait_ref meta translate_ty tr) + | FnPointer _ | Closure _ -> craise meta "Closures are not supported yet" + | UnknownTrait s -> craise meta ("Unknown trait found: " ^ s) (** Translate a signature type - TODO: factor out the different translation functions *) -let rec translate_sty (ty : T.ty) : ty = +let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty = let translate = translate_sty in match ty with | T.TAdt (type_id, generics) -> ( - let generics = translate_sgeneric_args generics in + let generics = translate_sgeneric_args meta generics in match type_id with | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics) | T.TTuple -> @@ -458,81 +459,81 @@ let rec translate_sty (ty : T.ty) : ty = match generics.types with | [ ty ] -> ty | _ -> - raise - (Failure - "Box/vec/option type with incorrect number of arguments") + craise + meta + "Box/vec/option type with incorrect number of arguments" ) | T.TArray -> TAdt (TAssumed TArray, generics) | T.TSlice -> TAdt (TAssumed TSlice, generics) | T.TStr -> TAdt (TAssumed TStr, generics))) | TVar vid -> TVar vid | TLiteral ty -> TLiteral ty - | TNever -> raise (Failure "Unreachable") - | TRef (_, rty, _) -> translate rty + | TNever -> craise meta "Unreachable" + | TRef (_, rty, _) -> translate meta rty | TRawPtr (ty, rkind) -> let mut = match rkind with RMut -> Mut | RShared -> Const in - let ty = translate ty in + let ty = translate meta ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) | TTraitType (trait_ref, type_name) -> - let trait_ref = translate_strait_ref trait_ref in + let trait_ref = translate_strait_ref meta trait_ref in TTraitType (trait_ref, type_name) - | TArrow _ -> raise (Failure "TODO") + | TArrow _ -> craise meta "TODO" -and translate_sgeneric_args (generics : T.generic_args) : generic_args = - translate_generic_args translate_sty generics +and translate_sgeneric_args (meta : Meta.meta) (generics : T.generic_args) : generic_args = + translate_generic_args meta (translate_sty meta) generics -and translate_strait_ref (tr : T.trait_ref) : trait_ref = - translate_trait_ref translate_sty tr +and translate_strait_ref (meta : Meta.meta) (tr : T.trait_ref) : trait_ref = + translate_trait_ref meta (translate_sty meta) tr -and translate_strait_instance_id (id : T.trait_instance_id) : trait_instance_id +and translate_strait_instance_id (meta : Meta.meta) (id : T.trait_instance_id) : trait_instance_id = - translate_trait_instance_id translate_sty id + translate_trait_instance_id meta (translate_sty meta) id -let translate_trait_clause (clause : T.trait_clause) : trait_clause = +let translate_trait_clause (meta : Meta.meta) (clause : T.trait_clause) : trait_clause = let { T.clause_id; meta = _; trait_id; clause_generics } = clause in - let generics = translate_sgeneric_args clause_generics in + let generics = translate_sgeneric_args meta clause_generics in { clause_id; trait_id; generics } -let translate_strait_type_constraint (ttc : T.trait_type_constraint) : +let translate_strait_type_constraint (meta : Meta.meta) (ttc : T.trait_type_constraint) : trait_type_constraint = let { T.trait_ref; type_name; ty } = ttc in - let trait_ref = translate_strait_ref trait_ref in - let ty = translate_sty ty in + let trait_ref = translate_strait_ref meta trait_ref in + let ty = translate_sty meta ty in { trait_ref; type_name; ty } -let translate_predicates (preds : T.predicates) : predicates = +let translate_predicates (meta : Meta.meta) (preds : T.predicates) : predicates = let trait_type_constraints = - List.map translate_strait_type_constraint preds.trait_type_constraints + List.map (translate_strait_type_constraint meta) preds.trait_type_constraints in { trait_type_constraints } -let translate_generic_params (generics : T.generic_params) : generic_params = +let translate_generic_params (meta : Meta.meta) (generics : T.generic_params) : generic_params = let { T.regions = _; types; const_generics; trait_clauses } = generics in - let trait_clauses = List.map translate_trait_clause trait_clauses in + let trait_clauses = List.map (translate_trait_clause meta) trait_clauses in { types; const_generics; trait_clauses } -let translate_field (f : T.field) : field = +let translate_field (meta : Meta.meta) (f : T.field) : field = let field_name = f.field_name in - let field_ty = translate_sty f.field_ty in + let field_ty = translate_sty meta f.field_ty in { field_name; field_ty } -let translate_fields (fl : T.field list) : field list = - List.map translate_field fl +let translate_fields (meta : Meta.meta) (fl : T.field list) : field list = + List.map (translate_field meta) fl -let translate_variant (v : T.variant) : variant = +let translate_variant (meta : Meta.meta) (v : T.variant) : variant = let variant_name = v.variant_name in - let fields = translate_fields v.fields in + let fields = translate_fields meta v.fields in { variant_name; fields } -let translate_variants (vl : T.variant list) : variant list = - List.map translate_variant vl +let translate_variants (meta : Meta.meta) (vl : T.variant list) : variant list = + List.map (translate_variant meta) vl (** Translate a type def kind from LLBC *) -let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind = +let translate_type_decl_kind (meta : Meta.meta) (kind : T.type_decl_kind) : type_decl_kind = match kind with - | T.Struct fields -> Struct (translate_fields fields) - | T.Enum variants -> Enum (translate_variants variants) + | T.Struct fields -> Struct (translate_fields meta fields) + | T.Enum variants -> Enum (translate_variants meta variants) | T.Opaque -> Opaque (** Translate a type definition from LLBC @@ -540,7 +541,7 @@ let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind = Remark: this is not symbolic to pure but LLBC to pure. Still, I don't see the point of moving this definition for now. *) -let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : +let translate_type_decl (meta : Meta.meta) (ctx : Contexts.decls_ctx) (def : T.type_decl) : type_decl = log#ldebug (lazy @@ -555,10 +556,10 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : let { T.regions; types; const_generics; trait_clauses } = def.generics in (* Can't translate types with regions for now *) assert (regions = []); - let trait_clauses = List.map translate_trait_clause trait_clauses in + let trait_clauses = List.map (translate_trait_clause meta) trait_clauses in let generics = { types; const_generics; trait_clauses } in - let kind = translate_type_decl_kind def.T.kind in - let preds = translate_predicates def.preds in + let kind = translate_type_decl_kind meta def.T.kind in + let preds = translate_predicates meta def.preds in let is_local = def.is_local in let meta = def.meta in { @@ -573,7 +574,7 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : preds; } -let translate_type_id (id : T.type_id) : type_id = +let translate_type_id (meta : Meta.meta) (id : T.type_id) : type_id = match id with | TAdtId adt_id -> TAdtId adt_id | TAssumed aty -> @@ -585,7 +586,7 @@ let translate_type_id (id : T.type_id) : type_id = | T.TBox -> (* Boxes have to be eliminated: this type id shouldn't be translated *) - raise (Failure "Unreachable") + craise meta "Unreachable" in TAssumed aty | TTuple -> TTuple @@ -598,15 +599,15 @@ let translate_type_id (id : T.type_id) : type_id = TODO: factor out the various translation functions. *) -let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = - let translate = translate_fwd_ty type_infos in +let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos) (ty : T.ty) : ty = + let translate = translate_fwd_ty meta type_infos in match ty with | T.TAdt (type_id, generics) -> ( - let t_generics = translate_fwd_generic_args type_infos generics in + let t_generics = translate_fwd_generic_args meta type_infos generics in (* Eliminate boxes and simplify tuples *) match type_id with | TAdtId _ | TAssumed (TArray | TSlice | TStr) -> - let type_id = translate_type_id type_id in + let type_id = translate_type_id meta type_id in TAdt (type_id, t_generics) | TTuple -> (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the @@ -623,12 +624,12 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = match t_generics.types with | [ bty ] -> bty | _ -> - raise - (Failure + craise + meta "Unreachable: box/vec/option receives exactly one type \ - parameter"))) + parameter")) | TVar vid -> TVar vid - | TNever -> raise (Failure "Unreachable") + | TNever -> craise meta "Unreachable" | TLiteral lty -> TLiteral lty | TRef (_, rty, _) -> translate rty | TRawPtr (ty, rkind) -> @@ -637,32 +638,32 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) | TTraitType (trait_ref, type_name) -> - let trait_ref = translate_fwd_trait_ref type_infos trait_ref in + let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in TTraitType (trait_ref, type_name) - | TArrow _ -> raise (Failure "TODO") + | TArrow _ -> craise meta "TODO" -and translate_fwd_generic_args (type_infos : type_infos) +and translate_fwd_generic_args (meta : Meta.meta) (type_infos : type_infos) (generics : T.generic_args) : generic_args = - translate_generic_args (translate_fwd_ty type_infos) generics + translate_generic_args meta (translate_fwd_ty meta type_infos) generics -and translate_fwd_trait_ref (type_infos : type_infos) (tr : T.trait_ref) : +and translate_fwd_trait_ref (meta : Meta.meta) (type_infos : type_infos) (tr : T.trait_ref) : trait_ref = - translate_trait_ref (translate_fwd_ty type_infos) tr + translate_trait_ref meta (translate_fwd_ty meta type_infos) tr -and translate_fwd_trait_instance_id (type_infos : type_infos) +and translate_fwd_trait_instance_id (meta : Meta.meta) (type_infos : type_infos) (id : T.trait_instance_id) : trait_instance_id = - translate_trait_instance_id (translate_fwd_ty type_infos) id + translate_trait_instance_id meta (translate_fwd_ty meta type_infos) id (** Simply calls [translate_fwd_ty] *) -let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty = +let ctx_translate_fwd_ty (meta : Meta.meta) (ctx : bs_ctx) (ty : T.ty) : ty = let type_infos = ctx.type_ctx.type_infos in - translate_fwd_ty type_infos ty + translate_fwd_ty meta type_infos ty (** Simply calls [translate_fwd_generic_args] *) -let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) : +let ctx_translate_fwd_generic_args (meta : Meta.meta) (ctx : bs_ctx) (generics : T.generic_args) : generic_args = let type_infos = ctx.type_ctx.type_infos in - translate_fwd_generic_args type_infos generics + translate_fwd_generic_args meta type_infos generics (** Translate a type, when some regions may have ended. @@ -670,21 +671,21 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) : [inside_mut]: are we inside a mutable borrow? *) -let rec translate_back_ty (type_infos : type_infos) +let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos) (keep_region : T.region -> bool) (inside_mut : bool) (ty : T.ty) : ty option = - let translate = translate_back_ty type_infos keep_region inside_mut in + let translate = translate_back_ty meta type_infos keep_region inside_mut in (* A small helper for "leave" types *) let wrap ty = if inside_mut then Some ty else None in match ty with | T.TAdt (type_id, generics) -> ( match type_id with | TAdtId _ | TAssumed (TArray | TSlice | TStr) -> - let type_id = translate_type_id type_id in + let type_id = translate_type_id meta type_id in if inside_mut then (* We do not want to filter anything, so we translate the generics as "forward" types *) - let generics = translate_fwd_generic_args type_infos generics in + let generics = translate_fwd_generic_args meta type_infos generics in Some (TAdt (type_id, generics)) else (* If not inside a mutable reference: check if at least one @@ -695,7 +696,7 @@ let rec translate_back_ty (type_infos : type_infos) *) let types = List.filter_map translate generics.types in if types <> [] then - let generics = translate_fwd_generic_args type_infos generics in + let generics = translate_fwd_generic_args meta type_infos generics in Some (TAdt (type_id, generics)) else None | TAssumed TBox -> ( @@ -705,8 +706,8 @@ let rec translate_back_ty (type_infos : type_infos) match generics.types with | [ bty ] -> translate bty | _ -> - raise - (Failure "Unreachable: boxes receive exactly one type parameter") + craise + meta "Unreachable: boxes receive exactly one type parameter" ) | TTuple -> ( (* Tuples can contain borrows (which we eliminate) *) @@ -718,7 +719,7 @@ let rec translate_back_ty (type_infos : type_infos) * is the identity *) Some (mk_simpl_tuple_ty tys_t))) | TVar vid -> wrap (TVar vid) - | TNever -> raise (Failure "Unreachable") + | TNever -> craise meta "Unreachable" | TLiteral lty -> wrap (TLiteral lty) | TRef (r, rty, rkind) -> ( match rkind with @@ -729,7 +730,7 @@ let rec translate_back_ty (type_infos : type_infos) (* Dive in, remembering the fact that we are inside a mutable borrow *) let inside_mut = true in if keep_region r then - translate_back_ty type_infos keep_region inside_mut rty + translate_back_ty meta type_infos keep_region inside_mut rty else None) | TRawPtr _ -> (* TODO: not sure what to do here *) @@ -740,23 +741,23 @@ let rec translate_back_ty (type_infos : type_infos) if inside_mut then (* Translate the trait ref as a "forward" trait ref - we do not want to filter any type *) - let trait_ref = translate_fwd_trait_ref type_infos trait_ref in + let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in Some (TTraitType (trait_ref, type_name)) else None - | TArrow _ -> raise (Failure "TODO") + | TArrow _ -> craise meta "TODO" (** Simply calls [translate_back_ty] *) -let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) +let ctx_translate_back_ty (meta : Meta.meta) (ctx : bs_ctx) (keep_region : 'r -> bool) (inside_mut : bool) (ty : T.ty) : ty option = let type_infos = ctx.type_ctx.type_infos in - translate_back_ty type_infos keep_region inside_mut ty + translate_back_ty meta type_infos keep_region inside_mut ty -let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx = +let mk_type_check_ctx (meta : Meta.meta) (ctx : bs_ctx) : PureTypeCheck.tc_ctx = let const_generics = T.ConstGenericVarId.Map.of_list (List.map (fun (cg : T.const_generic_var) -> - (cg.index, ctx_translate_fwd_ty ctx (T.TLiteral cg.ty))) + (cg.index, ctx_translate_fwd_ty meta ctx (T.TLiteral cg.ty))) ctx.sg.generics.const_generics) in let env = VarId.Map.empty in @@ -767,23 +768,23 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx = const_generics; } -let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit = - let ctx = mk_type_check_ctx ctx in +let type_check_pattern (meta : Meta.meta) (ctx : bs_ctx) (v : typed_pattern) : unit = + let ctx = mk_type_check_ctx meta ctx in let _ = PureTypeCheck.check_typed_pattern ctx v in () -let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit = +let type_check_texpression (meta : Meta.meta) (ctx : bs_ctx) (e : texpression) : unit = if !Config.type_check_pure_code then - let ctx = mk_type_check_ctx ctx in + let ctx = mk_type_check_ctx meta ctx in PureTypeCheck.check_texpression ctx e -let translate_fun_id_or_trait_method_ref (ctx : bs_ctx) +let translate_fun_id_or_trait_method_ref (meta : Meta.meta) (ctx : bs_ctx) (id : A.fun_id_or_trait_method_ref) : fun_id_or_trait_method_ref = match id with | FunId fun_id -> FunId fun_id | TraitMethod (trait_ref, method_name, fun_decl_id) -> let type_infos = ctx.type_ctx.type_infos in - let trait_ref = translate_fwd_trait_ref type_infos trait_ref in + let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in TraitMethod (trait_ref, method_name, fun_decl_id) let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) @@ -805,7 +806,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) that we need to call. This function may be [None] if it has to be ignored (because it does nothing). *) -let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id) +let bs_ctx_register_backward_call (meta : Meta.meta) (abs : V.abs) (call_id : V.FunCallId.id) (back_id : T.RegionGroupId.id) (back_args : texpression list) (ctx : bs_ctx) : bs_ctx * texpression option = (* Insert the abstraction in the call informations *) @@ -903,7 +904,7 @@ let compute_raw_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t) } (** TODO: not very clean. *) -let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) +let get_fun_effect_info (meta : Meta.meta) (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option) (gid : T.RegionGroupId.id option) : fun_effect_info = match lid with @@ -930,7 +931,7 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) match gid with | None -> loop_info.fwd_effect_info | Some gid -> RegionGroupId.Map.find gid loop_info.back_effect_infos) - | _ -> raise (Failure "Unreachable")) + | _ -> craise meta "Unreachable") (** Translate a function signature to a decomposed function signature. @@ -943,7 +944,7 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) We use [bid] ("backward function id") only if we split the forward and the backward functions. *) -let translate_fun_sig_with_regions_hierarchy_to_decomposed +let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta) (decls_ctx : C.decls_ctx) (fun_id : A.fun_id_or_trait_method_ref) (regions_hierarchy : T.region_var_groups) (sg : A.fun_sig) (input_names : string option list) : decomposed_fun_sig = @@ -983,7 +984,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (* Compute the forward inputs *) let fwd_fuel = mk_fuel_input_ty_as_list fwd_effect_info in let fwd_inputs_no_fuel_no_state = - List.map (translate_fwd_ty type_infos) sg.inputs + List.map (translate_fwd_ty meta type_infos) sg.inputs in (* State input for the forward function *) let fwd_state_ty = @@ -995,7 +996,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed List.concat [ fwd_fuel; fwd_inputs_no_fuel_no_state; fwd_state_ty ] in (* Compute the backward output, without the effect information *) - let fwd_output = translate_fwd_ty type_infos sg.output in + let fwd_output = translate_fwd_ty meta type_infos sg.output in (* Compute the type information for the backward function *) (* Small helper to translate types for backward functions *) @@ -1017,12 +1018,12 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed let keep_region r = match r with | T.RStatic -> raise Unimplemented - | RErased -> raise (Failure "Unexpected erased region") - | RBVar _ -> raise (Failure "Unexpected bound region") + | RErased -> craise meta "Unexpected erased region" + | RBVar _ -> craise meta "Unexpected bound region" | RFVar rid -> T.RegionId.Set.mem rid gr_regions in let inside_mut = false in - translate_back_ty type_infos keep_region inside_mut ty + translate_back_ty meta type_infos keep_region inside_mut ty in let translate_back_inputs_for_gid (gid : T.RegionGroupId.id) : ty list = (* For now we don't supported nested borrows, so we check that there @@ -1190,10 +1191,10 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed in (* Generic parameters *) - let generics = translate_generic_params sg.generics in + let generics = translate_generic_params meta sg.generics in (* Return *) - let preds = translate_predicates sg.preds in + let preds = translate_predicates meta sg.preds in { generics; llbc_generics = sg.generics; @@ -1204,17 +1205,17 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed fwd_info; } -let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx) +let translate_fun_sig_to_decomposed (meta : Meta.meta) (decls_ctx : C.decls_ctx) (fun_id : FunDeclId.id) (sg : A.fun_sig) (input_names : string option list) : decomposed_fun_sig = (* Retrieve the list of parent backward functions *) let regions_hierarchy = FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies in - translate_fun_sig_with_regions_hierarchy_to_decomposed decls_ctx + translate_fun_sig_with_regions_hierarchy_to_decomposed meta decls_ctx (FunId (FRegular fun_id)) regions_hierarchy sg input_names -let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx) +let translate_fun_sig_from_decl_to_decomposed (meta : Meta.meta) (decls_ctx : C.decls_ctx) (fdef : LlbcAst.fun_decl) : decomposed_fun_sig = let input_names = match fdef.body with @@ -1225,7 +1226,7 @@ let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx) (LlbcAstUtils.fun_body_get_input_vars body) in let sg = - translate_fun_sig_to_decomposed decls_ctx fdef.def_id fdef.signature + translate_fun_sig_to_decomposed meta decls_ctx fdef.def_id fdef.signature input_names in log#ldebug @@ -1357,21 +1358,21 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * var * typed_pattern = (** WARNING: do not call this function directly. Call [fresh_named_var_for_symbolic_value] instead. *) -let fresh_var_llbc_ty (basename : string option) (ty : T.ty) (ctx : bs_ctx) : +let fresh_var_llbc_ty (meta : Meta.meta) (basename : string option) (ty : T.ty) (ctx : bs_ctx) : bs_ctx * var = (* Generate the fresh variable *) let id, var_counter = VarId.fresh !(ctx.var_counter) in - let ty = ctx_translate_fwd_ty ctx ty in + let ty = ctx_translate_fwd_ty meta ctx ty in let var = { id; basename; ty } in (* Update the context *) ctx.var_counter := var_counter; (* Return *) (ctx, var) -let fresh_named_var_for_symbolic_value (basename : string option) +let fresh_named_var_for_symbolic_value (meta : Meta.meta) (basename : string option) (sv : V.symbolic_value) (ctx : bs_ctx) : bs_ctx * var = (* Generate the fresh variable *) - let ctx, var = fresh_var_llbc_ty basename sv.sv_ty ctx in + let ctx, var = fresh_var_llbc_ty meta basename sv.sv_ty ctx in (* Insert in the map *) let sv_to_var = V.SymbolicValueId.Map.add_strict sv.sv_id var ctx.sv_to_var in (* Update the context *) @@ -1379,19 +1380,19 @@ let fresh_named_var_for_symbolic_value (basename : string option) (* Return *) (ctx, var) -let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : +let fresh_var_for_symbolic_value (meta : Meta.meta) (sv : V.symbolic_value) (ctx : bs_ctx) : bs_ctx * var = - fresh_named_var_for_symbolic_value None sv ctx + fresh_named_var_for_symbolic_value meta None sv ctx -let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx) +let fresh_vars_for_symbolic_values (meta : Meta.meta) (svl : V.symbolic_value list) (ctx : bs_ctx) : bs_ctx * var list = - List.fold_left_map (fun ctx sv -> fresh_var_for_symbolic_value sv ctx) ctx svl + List.fold_left_map (fun ctx sv -> fresh_var_for_symbolic_value meta sv ctx) ctx svl -let fresh_named_vars_for_symbolic_values +let fresh_named_vars_for_symbolic_values (meta : Meta.meta) (svl : (string option * V.symbolic_value) list) (ctx : bs_ctx) : bs_ctx * var list = List.fold_left_map - (fun ctx (name, sv) -> fresh_named_var_for_symbolic_value name sv ctx) + (fun ctx (name, sv) -> fresh_named_var_for_symbolic_value meta name sv ctx) ctx svl (** This generates a fresh variable **which is not to be linked to any symbolic value** *) @@ -1469,22 +1470,22 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) fresh_opt_vars back_vars ctx (** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *) -let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = +let lookup_var_for_symbolic_value (meta : Meta.meta) (sv : V.symbolic_value) (ctx : bs_ctx) : var = match V.SymbolicValueId.Map.find_opt sv.sv_id ctx.sv_to_var with | Some v -> v | None -> - raise - (Failure + craise + meta ("Could not find var for symbolic value: " - ^ V.SymbolicValueId.to_string sv.sv_id)) + ^ V.SymbolicValueId.to_string sv.sv_id) (** Peel boxes as long as the value is of the form [Box<T>] *) -let rec unbox_typed_value (v : V.typed_value) : V.typed_value = +let rec unbox_typed_value (meta : Meta.meta) (v : V.typed_value) : V.typed_value = match (v.value, v.ty) with | V.VAdt av, T.TAdt (T.TAssumed T.TBox, _) -> ( match av.field_values with - | [ bv ] -> unbox_typed_value bv - | _ -> raise (Failure "Unreachable")) + | [ bv ] -> unbox_typed_value meta bv + | _ -> craise meta "Unreachable") | _ -> v (** Translate a symbolic value. @@ -1493,15 +1494,15 @@ let rec unbox_typed_value (v : V.typed_value) : V.typed_value = of (translated) type unit, it is important that we do not lookup variables in case the symbolic value has type unit. *) -let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) : +let symbolic_value_to_texpression (meta : Meta.meta) (ctx : bs_ctx) (sv : V.symbolic_value) : texpression = (* Translate the type *) - let ty = ctx_translate_fwd_ty ctx sv.sv_ty in + let ty = ctx_translate_fwd_ty meta ctx sv.sv_ty in (* If the type is unit, directly return unit *) if ty_is_unit ty then mk_unit_rvalue else (* Otherwise lookup the variable *) - let var = lookup_var_for_symbolic_value sv ctx in + let var = lookup_var_for_symbolic_value meta sv ctx in mk_texpression_from_var var (** Translate a typed value. @@ -1520,13 +1521,13 @@ let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) : - end abstraction - return *) -let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) +let rec typed_value_to_texpression (meta : Meta.meta) (ctx : bs_ctx) (ectx : C.eval_ctx) (v : V.typed_value) : texpression = (* We need to ignore boxes *) - let v = unbox_typed_value v in - let translate = typed_value_to_texpression ctx ectx in + let v = unbox_typed_value meta v in + let translate = typed_value_to_texpression meta ctx ectx in (* Translate the type *) - let ty = ctx_translate_fwd_ty ctx v.ty in + let ty = ctx_translate_fwd_ty meta ctx v.ty in (* Translate the value *) let value = match v.value with @@ -1554,27 +1555,27 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) let cons = { e = cons_e; ty = cons_ty } in (* Apply the constructor *) mk_apps cons field_values) - | VBottom -> raise (Failure "Unreachable") + | VBottom -> craise meta "Unreachable" | VLoan lc -> ( match lc with | VSharedLoan (_, v) -> translate v - | VMutLoan _ -> raise (Failure "Unreachable")) + | VMutLoan _ -> craise meta "Unreachable") | VBorrow bc -> ( match bc with | VSharedBorrow bid -> (* Lookup the shared value in the context, and continue *) - let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in + let sv = InterpreterBorrowsCore.lookup_shared_value meta ectx bid in translate sv | VReservedMutBorrow bid -> (* Same as for shared borrows. However, note that we use reserved borrows * only in *meta-data*: a value *actually used* in the translation can't come * from an unpromoted reserved borrow *) - let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in + let sv = InterpreterBorrowsCore.lookup_shared_value meta ectx bid in translate sv | VMutBorrow (_, v) -> (* Borrows are the identity in the extraction *) translate v) - | VSymbolic sv -> symbolic_value_to_texpression ctx sv + | VSymbolic sv -> symbolic_value_to_texpression meta ctx sv in (* Debugging *) log#ldebug @@ -1584,7 +1585,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) ^ "\n- translated expression:\n" ^ texpression_to_string ctx value)); (* Sanity check *) - type_check_texpression ctx value; + type_check_texpression meta ctx value; (* Return *) value @@ -1603,9 +1604,9 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) ^^ ]} *) -let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) +let rec typed_avalue_to_consumed (meta : Meta.meta) (ctx : bs_ctx) (ectx : C.eval_ctx) (av : V.typed_avalue) : texpression option = - let translate = typed_avalue_to_consumed ctx ectx in + let translate = typed_avalue_to_consumed meta ctx ectx in let value = match av.value with | AAdt adt_v -> ( @@ -1625,27 +1626,27 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) * [mk_simpl_tuple_rvalue] is the identity *) let rv = mk_simpl_tuple_texpression field_values in Some rv) - | ABottom -> raise (Failure "Unreachable") - | ALoan lc -> aloan_content_to_consumed ctx ectx lc - | ABorrow bc -> aborrow_content_to_consumed ctx bc - | ASymbolic aproj -> aproj_to_consumed ctx aproj + | ABottom -> craise meta "Unreachable" + | ALoan lc -> aloan_content_to_consumed meta ctx ectx lc + | ABorrow bc -> aborrow_content_to_consumed meta ctx bc + | ASymbolic aproj -> aproj_to_consumed meta ctx aproj | AIgnored -> None in (* Sanity check - Rk.: we do this at every recursive call, which is a bit * expansive... *) (match value with | None -> () - | Some value -> type_check_texpression ctx value); + | Some value -> type_check_texpression meta ctx value); (* Return *) value -and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) +and aloan_content_to_consumed (meta : Meta.meta) (ctx : bs_ctx) (ectx : C.eval_ctx) (lc : V.aloan_content) : texpression option = match lc with - | AMutLoan (_, _) | ASharedLoan (_, _, _) -> raise (Failure "Unreachable") + | AMutLoan (_, _) | ASharedLoan (_, _, _) -> craise meta "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_meta } -> (* Return the meta-value *) - Some (typed_value_to_texpression ctx ectx given_back_meta) + Some (typed_value_to_texpression meta ctx ectx given_back_meta) | AEndedSharedLoan (_, _) -> (* We don't dive into shared loans: there is nothing to give back * inside (note that there could be a mutable borrow in the shared @@ -1654,7 +1655,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) None | AIgnoredMutLoan (_, _) -> (* There can be *inner* not ended mutable loans, but not outer ones *) - raise (Failure "Unreachable") + craise meta "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -1662,11 +1663,11 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (* Ignore *) None -and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : +and aborrow_content_to_consumed (meta : Meta.meta) (_ctx : bs_ctx) (bc : V.aborrow_content) : texpression option = match bc with | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> - raise (Failure "Unreachable") + craise meta "Unreachable" | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) None @@ -1677,31 +1678,31 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : (* Ignore *) None -and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = +and aproj_to_consumed (meta : Meta.meta) (ctx : bs_ctx) (aproj : V.aproj) : texpression option = match aproj with | V.AEndedProjLoans (msv, []) -> (* The symbolic value was left unchanged *) - Some (symbolic_value_to_texpression ctx msv) + Some (symbolic_value_to_texpression meta ctx msv) | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) -> assert (child_aproj = AIgnoredProjBorrows); (* The symbolic value was updated *) - Some (symbolic_value_to_texpression ctx mnv) + Some (symbolic_value_to_texpression meta ctx mnv) | V.AEndedProjLoans (_, _) -> (* The symbolic value was updated, and the given back values come from sevearl * abstractions *) raise Unimplemented | AEndedProjBorrows _ -> (* We consider consumed values *) None | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> - raise (Failure "Unreachable") + craise meta "Unreachable" (** Convert the abstraction values in an abstraction to consumed values. See [typed_avalue_to_consumed]. *) -let abs_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (abs : V.abs) : +let abs_to_consumed (meta : Meta.meta) (ctx : bs_ctx) (ectx : C.eval_ctx) (abs : V.abs) : texpression list = log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs)); - List.filter_map (typed_avalue_to_consumed ctx ectx) abs.avalues + List.filter_map (typed_avalue_to_consumed meta ctx ectx) abs.avalues let translate_mprojection_elem (pe : E.projection_elem) : mprojection_elem option = @@ -1736,7 +1737,7 @@ let translate_opt_mplace (p : S.mplace option) : mplace option = [mp]: it is possible to provide some meta-place information, to guide the heuristics which later find pretty names for the variables. *) -let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) +let rec typed_avalue_to_given_back (meta : Meta.meta) (mp : mplace option) (av : V.typed_avalue) (ctx : bs_ctx) : bs_ctx * typed_pattern option = let ctx, value = match av.value with @@ -1748,7 +1749,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) let mp = None in let ctx, field_values = List.fold_left_map - (fun ctx fv -> typed_avalue_to_given_back mp fv ctx) + (fun ctx fv -> typed_avalue_to_given_back meta mp fv ctx) ctx adt_v.field_values in let field_values = List.filter_map (fun x -> x) field_values in @@ -1770,29 +1771,29 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) * is the identity *) let lv = mk_simpl_tuple_pattern field_values in (ctx, Some lv)) - | ABottom -> raise (Failure "Unreachable") - | ALoan lc -> aloan_content_to_given_back mp lc ctx - | ABorrow bc -> aborrow_content_to_given_back mp bc ctx - | ASymbolic aproj -> aproj_to_given_back mp aproj ctx + | ABottom -> craise meta "Unreachable" + | ALoan lc -> aloan_content_to_given_back meta mp lc ctx + | ABorrow bc -> aborrow_content_to_given_back meta mp bc ctx + | ASymbolic aproj -> aproj_to_given_back meta mp aproj ctx | AIgnored -> (ctx, None) in (* Sanity check - Rk.: we do this at every recursive call, which is a bit * expansive... *) - (match value with None -> () | Some value -> type_check_pattern ctx value); + (match value with None -> () | Some value -> type_check_pattern meta ctx value); (* Return *) (ctx, value) -and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) +and aloan_content_to_given_back (meta : Meta.meta) (_mp : mplace option) (lc : V.aloan_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match lc with - | AMutLoan (_, _) | ASharedLoan (_, _, _) -> raise (Failure "Unreachable") + | AMutLoan (_, _) | ASharedLoan (_, _, _) -> craise meta "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ } | AEndedSharedLoan (_, _) -> (* We consider given back values, and thus ignore those *) (ctx, None) | AIgnoredMutLoan (_, _) -> (* There can be *inner* not ended mutable loans, but not outer ones *) - raise (Failure "Unreachable") + craise meta "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -1800,14 +1801,14 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) (* Ignore *) (ctx, None) -and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) +and aborrow_content_to_given_back (meta : Meta.meta) (mp : mplace option) (bc : V.aborrow_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match bc with | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> - raise (Failure "Unreachable") + craise meta "Unreachable" | AEndedMutBorrow (msv, _) -> (* Return the meta-symbolic-value *) - let ctx, var = fresh_var_for_symbolic_value msv ctx in + let ctx, var = fresh_var_for_symbolic_value meta msv ctx in (ctx, Some (mk_typed_pattern_from_var var mp)) | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) @@ -1816,7 +1817,7 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) (* Ignore *) (ctx, None) -and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : +and aproj_to_given_back (meta : Meta.meta) (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match aproj with | V.AEndedProjLoans (_, child_projs) -> @@ -1829,16 +1830,16 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : (ctx, None) | AEndedProjBorrows mv -> (* Return the meta-value *) - let ctx, var = fresh_var_for_symbolic_value mv ctx in + let ctx, var = fresh_var_for_symbolic_value meta mv ctx in (ctx, Some (mk_typed_pattern_from_var var mp)) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> - raise (Failure "Unreachable") + craise meta "Unreachable" (** Convert the abstraction values in an abstraction to given back values. See [typed_avalue_to_given_back]. *) -let abs_to_given_back (mpl : mplace option list option) (abs : V.abs) +let abs_to_given_back (meta : Meta.meta) (mpl : mplace option list option) (abs : V.abs) (ctx : bs_ctx) : bs_ctx * typed_pattern list = let avalues = match mpl with @@ -1847,17 +1848,17 @@ let abs_to_given_back (mpl : mplace option list option) (abs : V.abs) in let ctx, values = List.fold_left_map - (fun ctx (mp, av) -> typed_avalue_to_given_back mp av ctx) + (fun ctx (mp, av) -> typed_avalue_to_given_back meta mp av ctx) ctx avalues in let values = List.filter_map (fun x -> x) values in (ctx, values) (** Simply calls [abs_to_given_back] *) -let abs_to_given_back_no_mp (abs : V.abs) (ctx : bs_ctx) : +let abs_to_given_back_no_mp (meta : Meta.meta) (abs : V.abs) (ctx : bs_ctx) : bs_ctx * typed_pattern list = let mpl = List.map (fun _ -> None) abs.avalues in - abs_to_given_back (Some mpl) abs ctx + abs_to_given_back meta (Some mpl) abs ctx (** Return the ordered list of the (transitive) parents of a given abstraction. @@ -1916,38 +1917,38 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) (* Return the computed information *) !info -let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = +let rec translate_expression (metadata : Meta.meta) (e : S.expression) (ctx : bs_ctx) : texpression = match e with | S.Return (ectx, opt_v) -> (* We reached a return. Remark: we can't get there if we are inside a loop. *) - translate_return ectx opt_v ctx + translate_return metadata ectx opt_v ctx | ReturnWithLoop (loop_id, is_continue) -> (* We reached a return and are inside a loop. *) translate_return_with_loop loop_id is_continue ctx | Panic -> translate_panic ctx - | FunCall (call, e) -> translate_function_call call e ctx - | EndAbstraction (ectx, abs, e) -> translate_end_abstraction ectx abs e ctx + | FunCall (call, e) -> translate_function_call metadata call e ctx + | EndAbstraction (ectx, abs, e) -> translate_end_abstraction metadata ectx abs e ctx | EvalGlobal (gid, generics, sv, e) -> - translate_global_eval gid generics sv e ctx - | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx - | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx + translate_global_eval metadata gid generics sv e ctx + | Assertion (ectx, v, e) -> translate_assertion metadata ectx v e ctx + | Expansion (p, sv, exp) -> translate_expansion metadata p sv exp ctx | IntroSymbolic (ectx, p, sv, v, e) -> - translate_intro_symbolic ectx p sv v e ctx - | Meta (meta, e) -> translate_emeta meta e ctx + translate_intro_symbolic metadata ectx p sv v e ctx + | Meta (meta, e) -> translate_emeta metadata meta e ctx | ForwardEnd (ectx, loop_input_values, e, back_e) -> (* Translate the end of a function, or the end of a loop. The case where we (re-)enter a loop is handled here. *) - translate_forward_end ectx loop_input_values e back_e ctx - | Loop loop -> translate_loop loop ctx + translate_forward_end metadata ectx loop_input_values e back_e ctx + | Loop loop -> translate_loop metadata loop ctx and translate_panic (ctx : bs_ctx) : texpression = (* Here we use the function return type - note that it is ok because * we don't match on panics which happen inside the function body - * but it won't be true anymore once we translate individual blocks *) - (* If we use a state monad, we need to add a lambda for the state variable *) + (* If we use a state modune partie nad, we need to add a lambda for the state variable *) (* Note that only forward functions return a state *) let effect_info = ctx_get_effect_info ctx in (* TODO: we should use a [Fail] function *) @@ -1997,7 +1998,7 @@ and translate_panic (ctx : bs_ctx) : texpression = Remark: in case we merge the forward/backward functions, we introduce those in [translate_forward_end]. *) -and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) +and translate_return (meta : Meta.meta) (ectx : C.eval_ctx) (opt_v : V.typed_value option) (ctx : bs_ctx) : texpression = (* There are two cases: - either we reach the return of a forward function or a forward loop body, @@ -2011,7 +2012,7 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) | None -> (* Forward function *) let v = Option.get opt_v in - typed_value_to_texpression ctx ectx v + typed_value_to_texpression meta ctx ectx v | Some _ -> (* Backward function *) (* Sanity check *) @@ -2084,7 +2085,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *) mk_emeta (Tag "return_with_loop") (mk_result_return_texpression output) -and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : +and translate_function_call (meta : Meta.meta) (call : S.call) (e : S.expression) (ctx : bs_ctx) : texpression = log#ldebug (lazy @@ -2093,9 +2094,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : ^ "\n\n- call.generics:\n" ^ ctx_generic_args_to_string ctx call.generics)); (* Translate the function call *) - let generics = ctx_translate_fwd_generic_args ctx call.generics in + let generics = ctx_translate_fwd_generic_args meta ctx call.generics in let args = - let args = List.map (typed_value_to_texpression ctx call.ctx) call.args in + let args = List.map (typed_value_to_texpression meta ctx call.ctx) call.args in let args_mplaces = List.map translate_opt_mplace call.args_places in List.map (fun (arg, mp) -> mk_opt_mplace_texpression mp arg) @@ -2108,11 +2109,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : match call.call_id with | S.Fun (fid, call_id) -> (* Regular function call *) - let fid_t = translate_fun_id_or_trait_method_ref ctx fid in + let fid_t = translate_fun_id_or_trait_method_ref meta ctx fid in let func = Fun (FromLlbc (fid_t, None)) in (* Retrieve the effect information about this function (can fail, * takes a state as input, etc.) *) - let effect_info = get_fun_effect_info ctx fid None None in + let effect_info = get_fun_effect_info meta ctx fid None None in (* Depending on the function effects: - add the fuel - add the state input argument @@ -2133,7 +2134,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let sg = Option.get call.sg in let decls_ctx = ctx.decls_ctx in let dsg = - translate_fun_sig_with_regions_hierarchy_to_decomposed decls_ctx fid + translate_fun_sig_with_regions_hierarchy_to_decomposed meta decls_ctx fid call.regions_hierarchy sg (List.map (fun _ -> None) sg.inputs) in @@ -2144,10 +2145,10 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | None -> (UnknownTrait __FUNCTION__, generics) | Some (all_generics, tr_self) -> let all_generics = - ctx_translate_fwd_generic_args ctx all_generics + ctx_translate_fwd_generic_args meta ctx all_generics in let tr_self = - translate_fwd_trait_instance_id ctx.type_ctx.type_infos + translate_fwd_trait_instance_id meta ctx.type_ctx.type_infos tr_self in (tr_self, all_generics) @@ -2179,7 +2180,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | PeIdent (s, _) -> s | PeImpl _ -> (* We shouldn't get there *) - raise (Failure "Unexpected")) + craise meta "Unexpected") in name ^ "_back" in @@ -2225,7 +2226,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (ctx, dsg.fwd_info.ignore_output, Some back_funs_map, back_funs) in (* Compute the pattern for the destination *) - let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in + let ctx, dest = fresh_var_for_symbolic_value meta call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in let dest = (* Here there is something subtle: as we might ignore the output @@ -2262,7 +2263,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : is_rec = false; } in - let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in + let ctx, dest = fresh_var_for_symbolic_value meta call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop Not, effect_info, args, dest) | S.Unop E.Neg -> ( @@ -2280,10 +2281,10 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : is_rec = false; } in - let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in + let ctx, dest = fresh_var_for_symbolic_value meta call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Neg int_ty), effect_info, args, dest) - | _ -> raise (Failure "Unreachable")) + | _ -> craise meta "Unreachable") | S.Unop (E.Cast cast_kind) -> ( match cast_kind with | CastScalar (src_ty, tgt_ty) -> @@ -2297,10 +2298,10 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : is_rec = false; } in - let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in + let ctx, dest = fresh_var_for_symbolic_value meta call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest) - | CastFnPtr _ -> raise (Failure "TODO: function casts")) + | CastFnPtr _ -> craise meta "TODO: function casts") | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> @@ -2319,10 +2320,10 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : is_rec = false; } in - let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in + let ctx, dest = fresh_var_for_symbolic_value meta call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Binop (binop, int_ty0), effect_info, args, dest) - | _ -> raise (Failure "Unreachable")) + | _ -> craise meta "Unreachable") in let func = { id = FunOrOp fun_id; generics } in let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in @@ -2333,11 +2334,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let func = { e = Qualif func; ty = func_ty } in let call = mk_apps func args in (* Translate the next expression *) - let next_e = translate_expression e ctx in + let next_e = translate_expression meta e ctx in (* Put together *) mk_let effect_info.can_fail dest_v call next_e -and translate_end_abstraction (ectx : C.eval_ctx) (abs : V.abs) +and translate_end_abstraction (meta : Meta.meta) (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : texpression = log#ldebug (lazy @@ -2345,15 +2346,15 @@ and translate_end_abstraction (ectx : C.eval_ctx) (abs : V.abs) ^ V.show_abs_kind abs.kind)); match abs.kind with | V.SynthInput rg_id -> - translate_end_abstraction_synth_input ectx abs e ctx rg_id + translate_end_abstraction_synth_input meta ectx abs e ctx rg_id | V.FunCall (call_id, rg_id) -> - translate_end_abstraction_fun_call ectx abs e ctx call_id rg_id - | V.SynthRet rg_id -> translate_end_abstraction_synth_ret ectx abs e ctx rg_id + translate_end_abstraction_fun_call meta ectx abs e ctx call_id rg_id + | V.SynthRet rg_id -> translate_end_abstraction_synth_ret meta ectx abs e ctx rg_id | V.Loop (loop_id, rg_id, abs_kind) -> - translate_end_abstraction_loop ectx abs e ctx loop_id rg_id abs_kind - | V.Identity -> translate_end_abstraction_identity ectx abs e ctx + translate_end_abstraction_loop meta ectx abs e ctx loop_id rg_id abs_kind + | V.Identity -> translate_end_abstraction_identity meta ectx abs e ctx -and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) +and translate_end_abstraction_synth_input (meta : Meta.meta) (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression = log#ldebug @@ -2403,7 +2404,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) in (* Get the list of values consumed by the abstraction upon ending *) - let consumed_values = abs_to_consumed ctx ectx abs in + let consumed_values = abs_to_consumed meta ctx ectx abs in log#ldebug (lazy @@ -2428,7 +2429,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) (fun (var, v) -> assert ((var : var).ty = (v : texpression).ty)) variables_values; (* Translate the next expression *) - let next_e = translate_expression e ctx in + let next_e = translate_expression meta e ctx in (* Generate the assignemnts *) let monadic = false in List.fold_right @@ -2436,7 +2437,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) mk_let monadic (mk_typed_pattern_from_var var None) value e) variables_values next_e -and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) +and translate_end_abstraction_fun_call (meta : Meta.meta) (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (call_id : V.FunCallId.id) (rg_id : T.RegionGroupId.id) : texpression = let call_info = V.FunCallId.Map.find call_id ctx.calls in @@ -2446,12 +2447,12 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) | S.Fun (fun_id, _) -> fun_id | Unop _ | Binop _ -> (* Those don't have backward functions *) - raise (Failure "Unreachable") + craise meta "Unreachable" in let effect_info = get_fun_effect_info ctx fun_id None (Some rg_id) in (* Retrieve the values consumed upon ending the loans inside this * abstraction: those give us the remaining input values *) - let back_inputs = abs_to_consumed ctx ectx abs in + let back_inputs = abs_to_consumed meta ctx ectx abs in (* If the function is stateful: * - add the state input argument * - generate a fresh state variable for the returned state @@ -2471,7 +2472,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) let output_mpl = List.append (List.map translate_opt_mplace call.args_places) [ None ] in - let ctx, outputs = abs_to_given_back (Some output_mpl) abs ctx in + let ctx, outputs = abs_to_given_back meta (Some output_mpl) abs ctx in (* Group the output values together: first the updated inputs *) let output = mk_simpl_tuple_pattern outputs in (* Add the returned state if the function is stateful *) @@ -2483,10 +2484,10 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) (* Retrieve the function id, and register the function call in the context if necessary.Arith_status *) let ctx, func = - bs_ctx_register_backward_call abs call_id rg_id back_inputs ctx + bs_ctx_register_backward_call meta abs call_id rg_id back_inputs ctx in (* Translate the next expression *) - let next_e = translate_expression e ctx in + let next_e = translate_expression meta e ctx in (* Put everything together *) let inputs = back_inputs in let args_mplaces = List.map (fun _ -> None) inputs in @@ -2511,21 +2512,21 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) let call = mk_apps func args in mk_let effect_info.can_fail output call next_e -and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs) +and translate_end_abstraction_identity (meta : Meta.meta) (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : texpression = (* We simply check that the abstraction only contains shared borrows/loans, and translate the next expression *) (* We can do this simply by checking that it consumes and gives back nothing *) - let inputs = abs_to_consumed ctx ectx abs in - let ctx, outputs = abs_to_given_back None abs ctx in + let inputs = abs_to_consumed meta ctx ectx abs in + let ctx, outputs = abs_to_given_back meta None abs ctx in assert (inputs = []); assert (outputs = []); (* Translate the next expression *) - translate_expression e ctx + translate_expression meta e ctx -and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) +and translate_end_abstraction_synth_ret (meta : Meta.meta) (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression = (* If we end the abstraction which consumed the return value of the function @@ -2561,13 +2562,13 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) let inputs = T.RegionGroupId.Map.find rg_id ctx.backward_inputs_no_state in (* Retrieve the values consumed upon ending the loans inside this * abstraction: as there are no nested borrows, there should be none. *) - let consumed = abs_to_consumed ctx ectx abs in + let consumed = abs_to_consumed meta ctx ectx abs in assert (consumed = []); (* Retrieve the values given back upon ending this abstraction - note that * we don't provide meta-place information, because those assignments will * be inlined anyway... *) log#ldebug (lazy ("abs: " ^ abs_to_string ctx abs)); - let ctx, given_back = abs_to_given_back_no_mp abs ctx in + let ctx, given_back = abs_to_given_back_no_mp meta abs ctx in (* Link the inputs to those given back values - note that this also * checks we have the same number of values, of course *) let given_back_inputs = List.combine given_back inputs in @@ -2583,7 +2584,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) assert (given_back.ty = input.ty)) given_back_inputs; (* Translate the next expression *) - let next_e = translate_expression e ctx in + let next_e = translate_expression meta e ctx in (* Generate the assignments *) let monadic = false in List.fold_right @@ -2591,7 +2592,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) mk_let monadic given_back (mk_texpression_from_var input_var) e) given_back_inputs next_e -and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) +and translate_end_abstraction_loop (meta : Meta.meta) (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (loop_id : V.LoopId.id) (rg_id : T.RegionGroupId.id option) (abs_kind : V.loop_abs_kind) : texpression = @@ -2604,13 +2605,13 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) match abs_kind with | V.LoopSynthInput -> (* Actually the same case as [SynthInput] *) - translate_end_abstraction_synth_input ectx abs e ctx rg_id + translate_end_abstraction_synth_input meta ectx abs e ctx rg_id | V.LoopCall -> ( (* We need to introduce a call to the backward function corresponding to a forward call which happened earlier *) let fun_id = E.FRegular ctx.fun_decl.def_id in let effect_info = - get_fun_effect_info ctx (FunId fun_id) (Some vloop_id) (Some rg_id) + get_fun_effect_info meta ctx (FunId fun_id) (Some vloop_id) (Some rg_id) in let loop_info = LoopId.Map.find loop_id ctx.loops in (* Retrieve the additional backward inputs. Note that those are actually @@ -2636,7 +2637,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) (* Concatenate all the inputs *) let inputs = List.concat [ back_inputs; back_state ] in (* Retrieve the values given back by this function *) - let ctx, outputs = abs_to_given_back None abs ctx in + let ctx, outputs = abs_to_given_back meta None abs ctx in (* Group the output values together: first the updated inputs *) let output = mk_simpl_tuple_pattern outputs in (* Add the returned state if the function is stateful *) @@ -2646,7 +2647,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) | Some nstate -> mk_simpl_tuple_pattern [ nstate; output ] in (* Translate the next expression *) - let next_e = translate_expression e ctx in + let next_e = translate_expression meta e ctx in (* Put everything together *) let args_mplaces = List.map (fun _ -> None) inputs in let args = @@ -2683,7 +2684,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) *) let next_e = if ctx.inside_loop then - let consumed_values = abs_to_consumed ctx ectx abs in + let consumed_values = abs_to_consumed meta ctx ectx abs in let var_values = List.combine outputs consumed_values in let var_values = List.filter_map @@ -2701,23 +2702,23 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) (* Create the let-binding *) mk_let effect_info.can_fail output call next_e) -and translate_global_eval (gid : A.GlobalDeclId.id) (generics : T.generic_args) +and translate_global_eval (meta : Meta.meta) (gid : A.GlobalDeclId.id) (generics : T.generic_args) (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression = - let ctx, var = fresh_var_for_symbolic_value sval ctx in + let ctx, var = fresh_var_for_symbolic_value meta sval ctx in let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in let generics = ctx_translate_fwd_generic_args ctx generics in let global_expr = { id = Global gid; generics } in (* We use translate_fwd_ty to translate the global type *) - let ty = ctx_translate_fwd_ty ctx decl.ty in + let ty = ctx_translate_fwd_ty meta ctx decl.ty in let gval = { e = Qualif global_expr; ty } in - let e = translate_expression e ctx in + let e = translate_expression meta e ctx in mk_let false (mk_typed_pattern_from_var var None) gval e -and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value) +and translate_assertion (meta : Meta.meta) (ectx : C.eval_ctx) (v : V.typed_value) (e : S.expression) (ctx : bs_ctx) : texpression = - let next_e = translate_expression e ctx in + let next_e = translate_expression meta e ctx in let monadic = true in - let v = typed_value_to_texpression ctx ectx v in + let v = typed_value_to_texpression meta ctx ectx v in let args = [ v ] in let func = { id = FunOrOp (Fun (Pure Assert)); generics = empty_generic_args } @@ -2727,10 +2728,10 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value) let assertion = mk_apps func args in mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e -and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) +and translate_expansion (meta : Meta.meta) (p : S.mplace option) (sv : V.symbolic_value) (exp : S.expansion) (ctx : bs_ctx) : texpression = (* Translate the scrutinee *) - let scrutinee = symbolic_value_to_texpression ctx sv in + let scrutinee = symbolic_value_to_texpression meta ctx sv in let scrutinee_mplace = translate_opt_mplace p in (* Translate the branches *) match exp with @@ -2739,12 +2740,12 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) | V.SeLiteral _ -> (* We do not *register* symbolic expansions to literal values in the symbolic ADT *) - raise (Failure "Unreachable") + craise meta "Unreachable" | SeMutRef (_, nsv) | SeSharedRef (_, nsv) -> (* The (mut/shared) borrow type is extracted to identity: we thus simply introduce an reassignment *) - let ctx, var = fresh_var_for_symbolic_value nsv ctx in - let next_e = translate_expression e ctx in + let ctx, var = fresh_var_for_symbolic_value meta nsv ctx in + let next_e = translate_expression meta e ctx in let monadic = false in mk_let monadic (mk_typed_pattern_from_var var None) @@ -2752,11 +2753,11 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) next_e | SeAdt _ -> (* Should be in the [ExpandAdt] case *) - raise (Failure "Unreachable")) + craise meta "Unreachable") | ExpandAdt branches -> ( (* We don't do the same thing if there is a branching or not *) match branches with - | [] -> raise (Failure "Unreachable") + | [] -> craise meta "Unreachable" | [ (variant_id, svl, branch) ] when not (TypesUtils.ty_is_custom_adt sv.V.sv_ty @@ -2768,19 +2769,19 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) we *ignore* this branch (and go to the next one) if the ADT is a custom adt, and [always_deconstruct_adts_with_matches] is true. *) - translate_ExpandAdt_one_branch sv scrutinee scrutinee_mplace + translate_ExpandAdt_one_branch meta sv scrutinee scrutinee_mplace variant_id svl branch ctx | branches -> let translate_branch (variant_id : T.VariantId.id option) (svl : V.symbolic_value list) (branch : S.expression) : match_branch = - let ctx, vars = fresh_vars_for_symbolic_values svl ctx in + let ctx, vars = fresh_vars_for_symbolic_values meta svl ctx in let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in let pat_ty = scrutinee.ty in let pat = mk_adt_pattern pat_ty variant_id vars in - let branch = translate_expression branch ctx in + let branch = translate_expression meta branch ctx in { pat; branch } in let branches = @@ -2801,8 +2802,8 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) | ExpandBool (true_e, false_e) -> (* We don't need to update the context: we don't introduce any new values/variables *) - let true_e = translate_expression true_e ctx in - let false_e = translate_expression false_e ctx in + let true_e = translate_expression meta true_e ctx in + let false_e = translate_expression meta false_e ctx in let e = Switch ( mk_opt_mplace_texpression scrutinee_mplace scrutinee, @@ -2822,12 +2823,12 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) match_branch = (* We don't need to update the context: we don't introduce any new values/variables *) - let branch = translate_expression branch_e ctx in + let branch = translate_expression meta branch_e ctx in let pat = mk_typed_pattern_from_literal (VScalar v) in { pat; branch } in let branches = List.map translate_branch branches in - let otherwise = translate_expression otherwise ctx in + let otherwise = translate_expression meta otherwise ctx in let pat_ty = TLiteral (TInteger int_ty) in let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in let otherwise : match_branch = @@ -2867,15 +2868,15 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) as inductives, in which case it is not always possible to use a notation for the field projections. *) -and translate_ExpandAdt_one_branch (sv : V.symbolic_value) +and translate_ExpandAdt_one_branch (meta : Meta.meta) (sv : V.symbolic_value) (scrutinee : texpression) (scrutinee_mplace : mplace option) (variant_id : variant_id option) (svl : V.symbolic_value list) (branch : S.expression) (ctx : bs_ctx) : texpression = (* TODO: always introduce a match, and use micro-passes to turn the the match into a let? *) let type_id, _ = TypesUtils.ty_as_adt sv.V.sv_ty in - let ctx, vars = fresh_vars_for_symbolic_values svl ctx in - let branch = translate_expression branch ctx in + let ctx, vars = fresh_vars_for_symbolic_values meta svl ctx in + let branch = translate_expression meta branch ctx in match type_id with | TAdtId adt_id -> (* Detect if this is an enumeration or not *) @@ -2942,7 +2943,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) | TAssumed TBox -> (* There should be exactly one variable *) let var = - match vars with [ v ] -> v | _ -> raise (Failure "Unreachable") + match vars with [ v ] -> v | _ -> craise meta "Unreachable" in (* We simply introduce an assignment - the box type is the * identity when extracted ([box a = a]) *) @@ -2956,9 +2957,9 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) * through the functions provided by the API (note that we don't * know how to expand values like vectors or arrays, because they have a variable number * of fields!) *) - raise (Failure "Attempt to expand a non-expandable value") + craise meta "Attempt to expand a non-expandable value" -and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) +and translate_intro_symbolic (meta : Meta.meta) (ectx : C.eval_ctx) (p : S.mplace option) (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression) (ctx : bs_ctx) : texpression = log#ldebug @@ -2968,10 +2969,10 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) let mplace = translate_opt_mplace p in (* Introduce a fresh variable for the symbolic value. *) - let ctx, var = fresh_var_for_symbolic_value sv ctx in + let ctx, var = fresh_var_for_symbolic_value meta sv ctx in (* Translate the next expression *) - let next_e = translate_expression e ctx in + let next_e = translate_expression meta e ctx in (* Translate the value: there are several cases, depending on whether this is a "regular" let-binding, an array aggregate, a const generic or @@ -2979,12 +2980,12 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) *) let v = match v with - | VaSingleValue v -> typed_value_to_texpression ctx ectx v + | VaSingleValue v -> typed_value_to_texpression meta ctx ectx v | VaArray values -> (* We use a struct update to encode the array aggregate, in order to preserve the structure and allow generating code of the shape `[x0, ...., xn]` *) - let values = List.map (typed_value_to_texpression ctx ectx) values in + let values = List.map (typed_value_to_texpression meta ctx ectx) values in let values = FieldId.mapi (fun fid v -> (fid, v)) values in let su : struct_update = { struct_id = TAssumed TArray; init = None; updates = values } @@ -3004,7 +3005,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) let var = mk_typed_pattern_from_var var mplace in mk_let monadic var v next_e -and translate_forward_end (ectx : C.eval_ctx) +and translate_forward_end (meta : Meta.meta) (ectx : C.eval_ctx) (loop_input_values : V.typed_value S.symbolic_value_id_map option) (fwd_e : S.expression) (back_e : S.expression S.region_group_id_map) (ctx : bs_ctx) : texpression = @@ -3061,7 +3062,7 @@ and translate_forward_end (ectx : C.eval_ctx) in (ctx, e, finish) in - let e = translate_expression e ctx in + let e = translate_expression meta e ctx in finish e in @@ -3215,13 +3216,13 @@ and translate_forward_end (ectx : C.eval_ctx) loop_info.input_svl in let args = - List.map (typed_value_to_texpression ctx ectx) loop_input_values + List.map (typed_value_to_texpression meta ctx ectx) loop_input_values in let org_args = args in (* Lookup the effect info for the loop function *) let fid = E.FRegular ctx.fun_decl.def_id in - let effect_info = get_fun_effect_info ctx (FunId fid) None ctx.bid in + let effect_info = get_fun_effect_info meta ctx (FunId fid) None ctx.bid in (* Introduce a fresh output value for the forward function *) let ctx, fwd_output, output_pat = @@ -3341,7 +3342,7 @@ and translate_forward_end (ectx : C.eval_ctx) *) mk_emeta_symbolic_assignments loop_info.input_vars org_args e -and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = +and translate_loop (meta : Meta.meta) (loop : S.loop) (ctx : bs_ctx) : texpression = let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in (* Translate the loop inputs - some inputs are symbolic values already @@ -3368,7 +3369,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (Print.list_to_string (ty_to_string ctx)) loop.rg_to_given_back_tys ^ "\n")); - let ctx, _ = fresh_vars_for_symbolic_values svl ctx in + let ctx, _ = fresh_vars_for_symbolic_values meta svl ctx in ctx in @@ -3398,7 +3399,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = List.map (fun ty -> assert (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty)); - ctx_translate_fwd_ty !ctx ty) + ctx_translate_fwd_ty meta !ctx ty) tys) loop.rg_to_given_back_tys in @@ -3525,7 +3526,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (* Update the context to translate the function end *) let ctx_end = { ctx with loop_id = Some loop_id } in - let fun_end = translate_expression loop.end_expr ctx_end in + let fun_end = translate_expression meta loop.end_expr ctx_end in (* Update the context for the loop body *) let ctx_loop = { ctx_end with inside_loop = true } in @@ -3536,7 +3537,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = in (* Translate the loop body *) - let loop_body = translate_expression loop.loop_expr ctx_loop in + let loop_body = translate_expression meta loop.loop_expr ctx_loop in (* Create the loop node and return *) let loop = @@ -3557,14 +3558,14 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let ty = fun_end.ty in { e = loop; ty } -and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) : +and translate_emeta (metadata : Meta.meta) (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) : texpression = - let next_e = translate_expression e ctx in + let next_e = translate_expression metadata e ctx in let meta = match meta with | S.Assignment (ectx, lp, rv, rp) -> let lp = translate_mplace lp in - let rv = typed_value_to_texpression ctx ectx rv in + let rv = typed_value_to_texpression metadata ctx ectx rv in let rp = translate_opt_mplace rp in Some (Assignment (lp, rv, rp)) | S.Snapshot ectx -> @@ -3663,7 +3664,7 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression) (* We should have checked the command line arguments before *) raise (Failure "Unexpected") -let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = +let translate_fun_decl (meta : Meta.meta) (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* Translate *) let def = ctx.fun_decl in assert (ctx.bid = None); @@ -3685,9 +3686,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = | None -> None | Some body -> let effect_info = - get_fun_effect_info ctx (FunId (FRegular def_id)) None None + get_fun_effect_info meta ctx (FunId (FRegular def_id)) None None in - let body = translate_expression body ctx in + let body = translate_expression meta body ctx in (* Add a match over the fuel, if necessary *) let body = if function_decreases_fuel effect_info then @@ -3695,7 +3696,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = else body in (* Sanity check *) - type_check_texpression ctx body; + type_check_texpression meta ctx body; (* Introduce the fuel parameter, if necessary *) let fuel = if function_uses_fuel effect_info then @@ -3770,11 +3771,11 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* return *) def -let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = - List.map (translate_type_decl ctx) +let translate_type_decls (meta : Meta.meta) (ctx : Contexts.decls_ctx) : type_decl list = + List.map (translate_type_decl meta ctx) (TypeDeclId.Map.values ctx.type_ctx.type_decls) -let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) +let translate_trait_decl (metadata : Meta.meta) (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) : trait_decl = let { def_id; @@ -3797,20 +3798,20 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params llbc_generics in - let preds = translate_predicates preds in - let parent_clauses = List.map translate_trait_clause llbc_parent_clauses in + let generics = translate_generic_params metadata llbc_generics in + let preds = translate_predicates metadata preds in + let parent_clauses = List.map (translate_trait_clause metadata) llbc_parent_clauses in let consts = List.map - (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id))) + (fun (name, (ty, id)) -> (name, (translate_fwd_ty metadata type_infos ty, id))) consts in let types = List.map (fun (name, (trait_clauses, ty)) -> ( name, - ( List.map translate_trait_clause trait_clauses, - Option.map (translate_fwd_ty type_infos) ty ) )) + ( List.map (translate_trait_clause metadata) trait_clauses, + Option.map (translate_fwd_ty metadata type_infos) ty ) )) types in { @@ -3830,7 +3831,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) provided_methods; } -let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) +let translate_trait_impl (metadata : Meta.meta) (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) : trait_impl = let { A.def_id; @@ -3850,27 +3851,27 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) in let type_infos = ctx.type_ctx.type_infos in let impl_trait = - translate_trait_decl_ref (translate_fwd_ty type_infos) llbc_impl_trait + translate_trait_decl_ref metadata (translate_fwd_ty metadata type_infos) llbc_impl_trait in let name = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in - let generics = translate_generic_params llbc_generics in - let preds = translate_predicates preds in - let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in + let generics = translate_generic_params metadata llbc_generics in + let preds = translate_predicates metadata preds in + let parent_trait_refs = List.map (translate_strait_ref metadata) parent_trait_refs in let consts = List.map - (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id))) + (fun (name, (ty, id)) -> (name, (translate_fwd_ty metadata type_infos ty, id))) consts in let types = List.map (fun (name, (trait_refs, ty)) -> ( name, - ( List.map (translate_fwd_trait_ref type_infos) trait_refs, - translate_fwd_ty type_infos ty ) )) + ( List.map (translate_fwd_trait_ref metadata type_infos) trait_refs, + translate_fwd_ty metadata type_infos ty ) )) types in { diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 9af3c71b..04aadafe 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -3,6 +3,7 @@ open Types open Values open LlbcAst open Contexts +open Errors module SA = SymbolicAst module Micro = PureMicroPasses open TranslateCore @@ -40,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : of backward functions, we also provide names for the outputs. TODO: maybe we should introduce a record for this. *) -let translate_function_to_pure (trans_ctx : trans_ctx) +let translate_function_to_pure (meta : Meta.meta) (trans_ctx : trans_ctx) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : pure_fun_translation_no_loops = @@ -175,7 +176,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx in { ctx with forward_inputs } - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in (* Add the backward inputs *) @@ -194,7 +195,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast) (* TODO: factor out the return type *) -let translate_crate_to_pure (crate : crate) : +let translate_crate_to_pure (meta : Meta.meta) (crate : crate) : trans_ctx * Pure.type_decl list * pure_fun_translation list @@ -207,7 +208,7 @@ let translate_crate_to_pure (crate : crate) : let trans_ctx = compute_contexts crate in (* Translate all the type definitions *) - let type_decls = SymbolicToPure.translate_type_decls trans_ctx in + let type_decls = SymbolicToPure.translate_type_decls meta trans_ctx in (* Compute the type definition map *) let type_decls_map = @@ -221,7 +222,7 @@ let translate_crate_to_pure (crate : crate) : (List.map (fun (fdef : LlbcAst.fun_decl) -> ( fdef.def_id, - SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx + SymbolicToPure.translate_fun_sig_from_decl_to_decomposed meta trans_ctx fdef )) (FunDeclId.Map.values crate.fun_decls)) in @@ -229,21 +230,21 @@ let translate_crate_to_pure (crate : crate) : (* Translate all the *transparent* functions *) let pure_translations = List.map - (translate_function_to_pure trans_ctx type_decls_map fun_dsigs) + (translate_function_to_pure meta trans_ctx type_decls_map fun_dsigs) (FunDeclId.Map.values crate.fun_decls) in (* Translate the trait declarations *) let trait_decls = List.map - (SymbolicToPure.translate_trait_decl trans_ctx) + (SymbolicToPure.translate_trait_decl meta trans_ctx) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in (* Translate the trait implementations *) let trait_impls = List.map - (SymbolicToPure.translate_trait_impl trans_ctx) + (SymbolicToPure.translate_trait_impl meta trans_ctx) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in @@ -351,9 +352,9 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) [is_rec]: [true] if the types are recursive. Necessarily [true] if there is > 1 type to extract. *) -let export_types_group (fmt : Format.formatter) (config : gen_config) +let export_types_group (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (is_rec : bool) (ids : Pure.TypeDeclId.id list) : unit = - assert (ids <> []); + cassert (ids <> []) meta "TODO: Error message"; let export_type = export_type fmt config ctx in let ids_set = Pure.TypeDeclId.Set.of_list ids in let export_type_decl kind id = export_type ids_set kind id true false in @@ -395,11 +396,11 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) if List.exists (fun b -> b) builtin then (* Sanity check *) - assert (List.for_all (fun b -> b) builtin) + cassert (List.for_all (fun b -> b) builtin) meta "TODO: Error message" else if List.exists dont_extract defs then (* Check if we have to ignore declarations *) (* Sanity check *) - assert (List.for_all dont_extract defs) + cassert (List.for_all dont_extract defs) meta "TODO: Error message" else ( (* Extract the type declarations. @@ -441,13 +442,14 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) TODO: check correct behavior with opaque globals. *) -let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) +let export_global (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (id : GlobalDeclId.id) : unit = let global_decls = ctx.trans_ctx.global_ctx.global_decls in let global = GlobalDeclId.Map.find id global_decls in let trans = FunDeclId.Map.find global.body ctx.trans_funs in - assert (trans.loops = []); - let body = trans.f in + assert (trans.fwd.loops = []); + assert (trans.backs = []); + let body = trans.fwd.f in let is_opaque = Option.is_none body.Pure.body in (* Check if we extract the global *) @@ -491,7 +493,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) Rem.: this function doesn't check [config.extract_fun_decls]: it should have been checked by the caller. *) -let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) +let export_functions_group_scc (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (is_rec : bool) (decls : Pure.fun_decl list) : unit = (* Utility to check a function has a decrease clause *) let has_decreases_clause (def : Pure.fun_decl) : bool = @@ -502,7 +504,7 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) (* Extract the function declarations *) (* Check if the functions are mutually recursive *) let is_mut_rec = List.length decls > 1 in - assert ((not is_mut_rec) || is_rec); + cassert ((not is_mut_rec) || is_rec) meta "TODO: Error message"; let decls_length = List.length decls in (* We open and close the declaration group with [{start, end}_fun_decl_group]. @@ -566,7 +568,7 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) In case of (non-mutually) recursive functions, we use a simple procedure to check if the forward and backward functions are mutually recursive. *) -let export_functions_group (fmt : Format.formatter) (config : gen_config) +let export_functions_group (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit = (* Check if the definition are builtin - if yes they must be ignored. Note that if one definition in the group is builtin, then all the @@ -582,7 +584,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) if List.exists (fun b -> b) builtin then (* Sanity check *) - assert (List.for_all (fun b -> b) builtin) + cassert (List.for_all (fun b -> b) builtin) meta "TODO: Error message" else (* Utility to check a function has a decrease clause *) let has_decreases_clause (def : Pure.fun_decl) : bool = @@ -614,11 +616,11 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) | FStar -> Extract.extract_template_fstar_decreases_clause ctx fmt decl | Coq -> - raise - (Failure "Coq doesn't have decreases/termination clauses") + craise + meta "Coq doesn't have decreases/termination clauses" | HOL4 -> - raise - (Failure "HOL4 doesn't have decreases/termination clauses") + craise + meta "HOL4 doesn't have decreases/termination clauses" in extract_decrease f.f; List.iter extract_decrease f.loops) @@ -637,7 +639,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) (* Extract the subgroups *) let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit = - export_functions_group_scc fmt config ctx is_rec decls + export_functions_group_scc meta fmt config ctx is_rec decls in List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups); @@ -692,16 +694,16 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config) split the definitions between different files (or not), we can control what is precisely extracted. *) -let extract_definitions (fmt : Format.formatter) (config : gen_config) +let extract_definitions (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) : unit = (* Export the definition groups to the file, in the proper order. - [extract_decl]: extract the type declaration (if not filtered) - [extract_extra_info]: extra the extra type information (e.g., the [Arguments] information in Coq). *) - let export_functions_group = export_functions_group fmt config ctx in - let export_global = export_global fmt config ctx in - let export_types_group = export_types_group fmt config ctx in + let export_functions_group = export_functions_group meta fmt config ctx in + let export_global = export_global meta fmt config ctx in + let export_types_group = export_types_group meta fmt config ctx in let export_trait_decl_group id = export_trait_decl fmt config ctx id true false in @@ -783,7 +785,7 @@ type extract_file_info = { custom_includes : string list; } -let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) +let extract_file (meta : Meta.meta) (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) : unit = (* Open the file and create the formatter *) let out = open_out fi.filename in @@ -883,7 +885,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) Format.pp_open_vbox fmt 0; (* Extract the definitions *) - extract_definitions fmt config ctx; + extract_definitions meta fmt config ctx; (* Close the box and end the formatting *) Format.pp_close_box fmt (); @@ -903,11 +905,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) close_out out (** Translate a crate and write the synthesized code to an output file. *) -let translate_crate (filename : string) (dest_dir : string) (crate : crate) : +let translate_crate (meta : Meta.meta) (filename : string) (dest_dir : string) (crate : crate) : unit = (* Translate the module to the pure AST *) let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls = - translate_crate_to_pure crate + translate_crate_to_pure meta crate in (* Initialize the names map by registering the keywords used in the @@ -1036,7 +1038,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : match Filename.chop_suffix_opt ~suffix:".llbc" filename with | None -> (* Note that we already checked the suffix upon opening the file *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Some filename -> (* Retrieve the file basename *) let basename = Filename.basename filename in @@ -1078,7 +1080,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : let ( ^^ ) = Filename.concat in if !Config.split_files then mkdir_if (dest_dir ^^ crate_name); if needs_clauses_module then ( - assert !Config.split_files; + cassert !Config.split_files meta "TODO: Error message"; mkdir_if (dest_dir ^^ crate_name ^^ "Clauses"))); (* Copy the "Primitives" file, if necessary *) @@ -1228,7 +1230,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = []; } in - extract_file opaque_config ctx file_info; + extract_file meta opaque_config ctx file_info; (* Return the additional dependencies *) [ opaque_imported_module ]) else [] @@ -1269,7 +1271,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = opaque_types_module; } in - extract_file types_config ctx file_info; + extract_file meta types_config ctx file_info; (* Extract the template clauses *) (if needs_clauses_module && !Config.extract_template_decreases_clauses then @@ -1298,7 +1300,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = []; } in - extract_file template_clauses_config ctx file_info); + extract_file meta template_clauses_config ctx file_info); (* Extract the opaque fun declarations, if needed *) let opaque_funs_module = @@ -1354,7 +1356,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = [ types_module ]; } in - extract_file opaque_config ctx file_info; + extract_file meta opaque_config ctx file_info; (* Return the additional dependencies *) [ opaque_imported_module ]) else [] @@ -1395,7 +1397,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : [ types_module ] @ opaque_funs_module @ clauses_module; } in - extract_file fun_config ctx file_info) + extract_file meta fun_config ctx file_info) else let gen_config = { @@ -1428,7 +1430,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = []; } in - extract_file gen_config ctx file_info); + extract_file meta gen_config ctx file_info); (* Generate the build file *) match !Config.backend with diff --git a/compiler/dune b/compiler/dune index 3a40e086..6bdfd153 100644 --- a/compiler/dune +++ b/compiler/dune @@ -19,6 +19,7 @@ ConstStrings Contexts Cps + Errors Expressions ExpressionsUtils Extract |