From a64fdc8b1be70de43afe35ff788ba3240318daac Mon Sep 17 00:00:00 2001 From: Escherichia Date: Tue, 12 Mar 2024 15:02:17 +0100 Subject: 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 --- compiler/Invariants.ml | 69 +++++++++++++++++++++++++------------------------- 1 file changed, 35 insertions(+), 34 deletions(-) (limited to 'compiler/Invariants.ml') 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 -- cgit v1.2.3 From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 21 Mar 2024 12:34:40 +0100 Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to do and we need to see how translate_crate can give meta to the functions it calls --- compiler/Invariants.ml | 168 ++++++++++++++++++++++++------------------------- 1 file changed, 84 insertions(+), 84 deletions(-) (limited to 'compiler/Invariants.ml') diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 871bf90d..a8077ab7 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -55,7 +55,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (* Link all the id representants to a borrow information *) let borrows_infos : borrow_info BorrowId.Map.t ref = ref BorrowId.Map.empty in let context_to_string () : string = - eval_ctx_to_string ctx ^ "- representants:\n" + eval_ctx_to_string meta ctx ^ "- representants:\n" ^ ids_reprs_to_string " " !ids_reprs ^ "\n- info:\n" ^ borrows_infos_to_string " " !borrows_infos @@ -77,12 +77,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let infos = !borrows_infos in (* Use the first borrow id as representant *) let repr_bid = BorrowId.Set.min_elt bids in - assert (not (BorrowId.Map.mem repr_bid infos)); + cassert (not (BorrowId.Map.mem repr_bid infos)) meta "TODO: Error message"; (* Insert the mappings to the representant *) let reprs = BorrowId.Set.fold (fun bid reprs -> - assert (not (BorrowId.Map.mem bid reprs)); + cassert (not (BorrowId.Map.mem bid reprs)) meta "TODO: Error message"; BorrowId.Map.add bid repr_bid reprs) bids reprs in @@ -105,8 +105,8 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let reprs = !ids_reprs in let infos = !borrows_infos in (* Sanity checks *) - assert (not (BorrowId.Map.mem bid reprs)); - assert (not (BorrowId.Map.mem bid infos)); + cassert (not (BorrowId.Map.mem bid reprs)) meta "TODO: Error message"; + cassert (not (BorrowId.Map.mem bid infos)) meta "TODO: Error message"; (* Add the mapping for the representant *) let reprs = BorrowId.Map.add bid bid reprs in (* Add the mapping for the loan info *) @@ -212,10 +212,10 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : | RShared, (BShared | BReserved) | RMut, BMut -> () | _ -> 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); + cassert (kind <> BReserved || not info.loan_in_abs) meta "A reserved borrow can't point to a value inside an abstraction"; (* Insert the borrow id *) let borrow_ids = info.borrow_ids in - assert (not (BorrowId.Set.mem bid borrow_ids)); + cassert (not (BorrowId.Set.mem bid borrow_ids)) meta "TODO: Error message"; let info = { info with borrow_ids = BorrowId.Set.add bid borrow_ids } in (* Update the info in the map *) update_info bid info @@ -270,7 +270,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : List.iter (fun (rkind, bid) -> let info = find_info bid in - assert (info.loan_kind = rkind)) + cassert (info.loan_kind = rkind) meta "Not all the ignored loans are present at the proper place") !ignored_loans; (* Then, check the borrow infos *) @@ -278,11 +278,11 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (fun _ info -> (* Note that we can't directly compare the sets - I guess they are * different depending on the order in which we add the elements... *) - assert ( + cassert ( BorrowId.Set.elements info.loan_ids - = BorrowId.Set.elements info.borrow_ids); + = BorrowId.Set.elements info.borrow_ids) meta "TODO: Error message"; match info.loan_kind with - | RMut -> assert (BorrowId.Set.cardinal info.loan_ids = 1) + | RMut -> cassert (BorrowId.Set.cardinal info.loan_ids = 1) meta "TODO: Error message" | RShared -> ()) !borrows_infos @@ -290,14 +290,14 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : - borrows/loans can't contain ⊥ or reserved mut borrows - shared loans can't contain mutable loans *) -let check_borrowed_values_invariant (ctx : eval_ctx) : unit = +let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let visitor = object inherit [_] iter_eval_ctx as super method! visit_VBottom info = (* No ⊥ inside borrowed values *) - assert (Config.allow_bottom_below_borrow || not info.outer_borrow) + cassert (Config.allow_bottom_below_borrow || not info.outer_borrow) meta "There should be no ⊥ inside borrowed values" method! visit_ABottom _info = (* ⊥ inside an abstraction is not the same as in a regular value *) @@ -310,7 +310,7 @@ let check_borrowed_values_invariant (ctx : eval_ctx) : unit = | VSharedLoan (_, _) -> set_outer_shared info | VMutLoan _ -> (* No mutable loan inside a shared loan *) - assert (not info.outer_shared); + cassert (not info.outer_shared) meta "There should be no mutable loan inside a shared loan"; set_outer_mut info in (* Continue exploring *) @@ -322,7 +322,7 @@ let check_borrowed_values_invariant (ctx : eval_ctx) : unit = match bc with | VSharedBorrow _ -> set_outer_shared info | VReservedMutBorrow _ -> - assert (not info.outer_borrow); + cassert (not info.outer_borrow) meta "TODO: Error message"; set_outer_shared info | VMutBorrow (_, _) -> set_outer_mut info in @@ -369,7 +369,7 @@ let check_borrowed_values_invariant (ctx : eval_ctx) : 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) + | VScalar sv, TInteger int_ty -> cassert (sv.int_ty = int_ty) meta "TODO: Error message" | VBool _, TBool | VChar _, TChar -> () | _ -> craise meta "Erroneous typing" @@ -393,17 +393,17 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = method! visit_EBinding info binder v = (* We also check that the regions are erased *) - assert (ty_is_ety v.ty); + cassert (ty_is_ety v.ty) meta "The regions should be erased"; super#visit_EBinding info binder v method! visit_symbolic_value inside_abs v = (* Check that the types have regions *) - assert (ty_is_rty v.sv_ty); + cassert (ty_is_rty v.sv_ty) meta "The types should have regions"; super#visit_symbolic_value inside_abs v method! visit_typed_value info tv = (* Check that the types have erased regions *) - assert (ty_is_ety tv.ty); + cassert (ty_is_ety tv.ty) meta "The types should have erased regions"; (* Check the current pair (value, type) *) (match (tv.value, tv.ty) with | VLiteral cv, TLiteral ty -> check_literal_type meta cv ty @@ -413,13 +413,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - assert ( - List.length generics.regions = List.length def.generics.regions); - assert (List.length generics.types = List.length def.generics.types); + cassert ( + List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message"; + cassert (List.length generics.types = List.length def.generics.types) meta "TODO: Error message"; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - assert (VariantId.to_int variant_id < List.length variants) + cassert (VariantId.to_int variant_id < List.length variants) meta "The variant id should be consistent" | None, Struct _ -> () | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) @@ -429,24 +429,24 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = in let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : typed_value * ty) -> assert (v.ty = ty)) + (fun ((v, ty) : typed_value * ty) -> cassert (v.ty = ty) meta "The field types are not correct") fields_with_types (* Tuple case *) | VAdt av, TAdt (TTuple, generics) -> - assert (generics.regions = []); - assert (generics.const_generics = []); - assert (av.variant_id = None); + cassert (generics.regions = []) meta "TODO: Error message"; + cassert (generics.const_generics = []) meta "TODO: Error message"; + cassert (av.variant_id = None) meta "TODO: Error message"; (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : typed_value * ty) -> assert (v.ty = ty)) + (fun ((v, ty) : typed_value * ty) -> cassert (v.ty = ty) meta "The fields does not have the proper values or there are not as many fields as field types at the same time TODO: error message") fields_with_types (* Assumed type case *) | VAdt av, TAdt (TAssumed aty_id, generics) -> ( - assert (av.variant_id = None); + cassert (av.variant_id = None) meta "TODO: Error message"; match ( aty_id, av.field_values, @@ -456,20 +456,20 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = with (* Box *) | TBox, [ inner_value ], [], [ inner_ty ], [] -> - assert (inner_value.ty = inner_ty) + cassert (inner_value.ty = inner_ty) meta "TODO: Error message" | TArray, inner_values, _, [ inner_ty ], [ cg ] -> (* *) - assert ( + cassert ( List.for_all (fun (v : typed_value) -> v.ty = inner_ty) - inner_values); + inner_values) meta "TODO: Error message"; (* The length is necessarily concrete *) let len = (ValuesUtils.literal_as_scalar (TypesUtils.const_generic_as_literal cg)) .value in - assert (Z.of_int (List.length inner_values) = len) + cassert (Z.of_int (List.length inner_values) = len) meta "TODO: Error message" | (TSlice | TStr), _, _, _, _ -> craise meta "Unexpected" | _ -> craise meta "Erroneous type") | VBottom, _ -> (* Nothing to check *) () @@ -481,27 +481,27 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - assert (sv.ty = ref_ty) + cassert (sv.ty = ref_ty) meta "TODO: Error message" | _ -> craise meta "Inconsistent context") | VMutBorrow (_, bv), RMut -> - assert ( + cassert ( (* Check that the borrowed value has the proper type *) - bv.ty = ref_ty) + bv.ty = ref_ty) meta "TODO: Error message" | _ -> craise meta "Erroneous typing") | VLoan lc, ty -> ( match lc with - | VSharedLoan (_, sv) -> assert (sv.ty = ty) + | VSharedLoan (_, sv) -> cassert (sv.ty = ty) meta "TODO: Error message" | VMutLoan bid -> ( (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with - | Concrete (VMutBorrow (_, bv)) -> assert (bv.ty = ty) + | Concrete (VMutBorrow (_, bv)) -> cassert (bv.ty = ty) meta "The borrowed value does not have the proper type" | Abstract (AMutBorrow (_, sv)) -> - assert (Substitute.erase_regions sv.ty = ty) + cassert (Substitute.erase_regions sv.ty = ty) meta "The borrowed value does not have the proper type" | _ -> craise meta "Inconsistent context")) | VSymbolic sv, ty -> let ty' = Substitute.erase_regions sv.sv_ty in - assert (ty' = ty) + cassert (ty' = ty) meta "TODO: Error message" | _ -> craise meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_value info tv @@ -516,7 +516,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * *) method! visit_typed_avalue info atv = (* Check that the types have regions *) - assert (ty_is_rty atv.ty); + cassert (ty_is_rty atv.ty) meta "The types should have regions"; (* Check the current pair (value, type) *) (match (atv.value, atv.ty) with (* ADT case *) @@ -525,16 +525,16 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - assert ( - List.length generics.regions = List.length def.generics.regions); - assert (List.length generics.types = List.length def.generics.types); - assert ( + cassert ( + List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message"; + cassert (List.length generics.types = List.length def.generics.types) meta "TODO: Error message"; + cassert ( List.length generics.const_generics - = List.length def.generics.const_generics); + = List.length def.generics.const_generics) meta "TODO: Error message"; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - assert (VariantId.to_int variant_id < List.length variants) + cassert (VariantId.to_int variant_id < List.length variants) meta "The variant id should be consistent" | None, Struct _ -> () | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) @@ -544,24 +544,24 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = in let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : typed_avalue * ty) -> assert (v.ty = ty)) + (fun ((v, ty) : typed_avalue * ty) -> cassert (v.ty = ty) meta "TODO: Error message") fields_with_types (* Tuple case *) | AAdt av, TAdt (TTuple, generics) -> - assert (generics.regions = []); - assert (generics.const_generics = []); - assert (av.variant_id = None); + cassert (generics.regions = []) meta "TODO: Error message"; + cassert (generics.const_generics = []) meta "TODO: Error message"; + cassert (av.variant_id = None) meta "TODO: Error message"; (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : typed_avalue * ty) -> assert (v.ty = ty)) + (fun ((v, ty) : typed_avalue * ty) -> cassert (v.ty = ty) meta "The fields do not have the proper values or there are not as many fields as field types at the same time TODO: Error message") fields_with_types (* Assumed type case *) | AAdt av, TAdt (TAssumed aty_id, generics) -> ( - assert (av.variant_id = None); + cassert (av.variant_id = None) meta "TODO: Error message"; match ( aty_id, av.field_values, @@ -571,27 +571,27 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = with (* Box *) | TBox, [ boxed_value ], [], [ boxed_ty ], [] -> - assert (boxed_value.ty = boxed_ty) + cassert (boxed_value.ty = boxed_ty) meta "TODO: Error message" | _ -> craise meta "Erroneous type") | ABottom, _ -> (* Nothing to check *) () | ABorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with | AMutBorrow (_, av), RMut -> (* Check that the child value has the proper type *) - assert (av.ty = ref_ty) + cassert (av.ty = ref_ty) meta "TODO: Error message" | ASharedBorrow bid, RShared -> ( (* Lookup the borrowed value to check it has the proper type *) 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) + cassert (sv.ty = Substitute.erase_regions ref_ty) meta "TODO: Error message" | _ -> craise meta "Inconsistent context") - | AIgnoredMutBorrow (_opt_bid, av), RMut -> assert (av.ty = ref_ty) + | AIgnoredMutBorrow (_opt_bid, av), RMut -> cassert (av.ty = ref_ty) meta "TODO: Error message" | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ }, RMut ) -> - assert (given_back.ty = ref_ty); - assert (child.ty = ref_ty) + cassert (given_back.ty = ref_ty) meta "TODO: Error message"; + cassert (child.ty = ref_ty) meta "TODO: Error message" | AProjSharedBorrow _, RShared -> () | _ -> craise meta "Inconsistent context") | ALoan lc, aty -> ( @@ -599,54 +599,54 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av) -> ( let borrowed_aty = aloan_get_expected_child_type aty in - assert (child_av.ty = borrowed_aty); + cassert (child_av.ty = borrowed_aty) meta "TODO: Error message"; (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> - assert (bv.ty = Substitute.erase_regions borrowed_aty) + cassert (bv.ty = Substitute.erase_regions borrowed_aty) meta "TODO: Error message" | Abstract (AMutBorrow (_, sv)) -> - assert ( + cassert ( Substitute.erase_regions sv.ty - = Substitute.erase_regions borrowed_aty) + = Substitute.erase_regions borrowed_aty) meta "TODO: Error message" | _ -> craise meta "Inconsistent context") | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - assert (child_av.ty = borrowed_aty) + cassert (child_av.ty = borrowed_aty) meta "TODO: Error message" | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - assert (sv.ty = Substitute.erase_regions borrowed_aty); + cassert (sv.ty = Substitute.erase_regions borrowed_aty) meta "TODO: Error message"; (* TODO: the type of aloans doesn't make sense, see above *) - assert (child_av.ty = borrowed_aty) + cassert (child_av.ty = borrowed_aty) meta "TODO: Error message" | AEndedMutLoan { given_back; child; given_back_meta = _ } | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in - assert (given_back.ty = borrowed_aty); - assert (child.ty = borrowed_aty) + cassert (given_back.ty = borrowed_aty) meta "TODO: Error message"; + cassert (child.ty = borrowed_aty) meta "TODO: Error message" | AIgnoredSharedLoan child_av -> - assert (child_av.ty = aloan_get_expected_child_type aty)) + cassert (child_av.ty = aloan_get_expected_child_type aty) meta "TODO: Error message") | ASymbolic aproj, ty -> ( let ty1 = Substitute.erase_regions ty in match aproj with | AProjLoans (sv, _) -> let ty2 = Substitute.erase_regions sv.sv_ty in - assert (ty1 = ty2); + cassert (ty1 = ty2) meta "TODO: Error message"; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - assert (ty_has_regions_in_set abs.regions sv.sv_ty) + cassert (ty_has_regions_in_set abs.regions sv.sv_ty) meta "The symbolic values should contain regions of interest or they should have been reduced to [] TODO: error message" | AProjBorrows (sv, proj_ty) -> let ty2 = Substitute.erase_regions sv.sv_ty in - assert (ty1 = ty2); + cassert (ty1 = ty2) meta "TODO: Error message"; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - assert (ty_has_regions_in_set abs.regions proj_ty) + cassert (ty_has_regions_in_set abs.regions proj_ty) meta "The symbolic values should contain regions of interest or they should have been reduced to [] TODO: error message" | AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> match proj with - | AProjBorrows (_sv, ty') -> assert (ty' = ty) + | AProjBorrows (_sv, ty') -> cassert (ty' = ty) meta "TODO: Error message" | AEndedProjBorrows _ | AIgnoredProjBorrows -> () | _ -> craise meta "Unexpected") given_back_ls @@ -657,7 +657,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (lazy ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv ^ "\n- value: " - ^ typed_avalue_to_string ctx atv + ^ typed_avalue_to_string meta ctx atv ^ "\n- type: " ^ ty_to_string ctx atv.ty)); craise meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) @@ -766,15 +766,15 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = *) (* A symbolic value can't be both in the regular environment and inside * projectors of borrows in abstractions *) - assert (info.env_count = 0 || info.aproj_borrows = []); + cassert (info.env_count = 0 || info.aproj_borrows = []) meta "A symbolic value can't be both in the regular environment and inside projectors of borrows in abstractions"; (* A symbolic value containing borrows can't be duplicated (i.e., copied): * it must be expanded first *) if ty_has_borrows ctx.type_ctx.type_infos info.ty then - assert (info.env_count <= 1); + cassert (info.env_count <= 1) meta "A symbolic value containing borrows can't be duplicated (i.e., copied): it must be expanded first"; (* A duplicated symbolic value is necessarily primitively copyable *) - assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty); + cassert (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta "A duplicated symbolic value should necessarily be primitively copyable"; - assert (info.aproj_borrows = [] || info.aproj_loans <> []); + cassert (info.aproj_borrows = [] || info.aproj_loans <> []) meta "TODO: Error message"; (* At the same time: * - check that the loans don't intersect * - compute the set of regions for which we project loans @@ -786,7 +786,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = let regions = RegionId.Set.fold (fun rid regions -> - assert (not (RegionId.Set.mem rid regions)); + cassert (not (RegionId.Set.mem rid regions)) meta "The loan projectors should contain the region projectors"; RegionId.Set.add rid regions) regions linfo.regions in @@ -796,8 +796,8 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Check that the union of the loan projectors contains the borrow projections. *) List.iter (fun binfo -> - assert ( - projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions)) + cassert ( + projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta "The union of the loan projectors should contain the borrow projections") info.aproj_borrows; () in @@ -806,9 +806,9 @@ let check_symbolic_values (meta : Meta.meta) (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)); + log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string meta ctx)); check_loans_borrows_relation_invariant meta ctx; - check_borrowed_values_invariant ctx; + check_borrowed_values_invariant meta ctx; check_typing_invariant meta ctx; check_symbolic_values meta ctx) else log#ldebug (lazy "Not checking invariants (check is not activated)") -- cgit v1.2.3 From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Wed, 27 Mar 2024 10:22:06 +0100 Subject: Added sanity_check and sanity_check_opt_meta helpers and changed sanity checks related cassert to these helpers to have a proper error message --- compiler/Invariants.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/Invariants.ml') diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index a8077ab7..50f008b8 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -105,8 +105,8 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let reprs = !ids_reprs in let infos = !borrows_infos in (* Sanity checks *) - cassert (not (BorrowId.Map.mem bid reprs)) meta "TODO: Error message"; - cassert (not (BorrowId.Map.mem bid infos)) meta "TODO: Error message"; + sanity_check (not (BorrowId.Map.mem bid reprs)) meta; + sanity_check (not (BorrowId.Map.mem bid infos)) meta; (* Add the mapping for the representant *) let reprs = BorrowId.Map.add bid bid reprs in (* Add the mapping for the loan info *) -- cgit v1.2.3 From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 13:56:31 +0100 Subject: Should answer all comments, there are still some TODO: error message left --- compiler/Invariants.ml | 164 ++++++++++++++++++++++++------------------------- 1 file changed, 82 insertions(+), 82 deletions(-) (limited to 'compiler/Invariants.ml') diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 50f008b8..9b389ba5 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -55,7 +55,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (* Link all the id representants to a borrow information *) let borrows_infos : borrow_info BorrowId.Map.t ref = ref BorrowId.Map.empty in let context_to_string () : string = - eval_ctx_to_string meta ctx ^ "- representants:\n" + eval_ctx_to_string ~meta:(Some meta) ctx ^ "- representants:\n" ^ ids_reprs_to_string " " !ids_reprs ^ "\n- info:\n" ^ borrows_infos_to_string " " !borrows_infos @@ -77,12 +77,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let infos = !borrows_infos in (* Use the first borrow id as representant *) let repr_bid = BorrowId.Set.min_elt bids in - cassert (not (BorrowId.Map.mem repr_bid infos)) meta "TODO: Error message"; + sanity_check (not (BorrowId.Map.mem repr_bid infos)) meta; (* Insert the mappings to the representant *) let reprs = BorrowId.Set.fold (fun bid reprs -> - cassert (not (BorrowId.Map.mem bid reprs)) meta "TODO: Error message"; + sanity_check (not (BorrowId.Map.mem bid reprs)) meta; BorrowId.Map.add bid repr_bid reprs) bids reprs in @@ -212,10 +212,10 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : | RShared, (BShared | BReserved) | RMut, BMut -> () | _ -> craise meta "Invariant not satisfied"); (* A reserved borrow can't point to a value inside an abstraction *) - cassert (kind <> BReserved || not info.loan_in_abs) meta "A reserved borrow can't point to a value inside an abstraction"; + sanity_check (kind <> BReserved || not info.loan_in_abs) meta; (* Insert the borrow id *) let borrow_ids = info.borrow_ids in - cassert (not (BorrowId.Set.mem bid borrow_ids)) meta "TODO: Error message"; + sanity_check (not (BorrowId.Set.mem bid borrow_ids)) meta; let info = { info with borrow_ids = BorrowId.Set.add bid borrow_ids } in (* Update the info in the map *) update_info bid info @@ -270,7 +270,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : List.iter (fun (rkind, bid) -> let info = find_info bid in - cassert (info.loan_kind = rkind) meta "Not all the ignored loans are present at the proper place") + sanity_check (info.loan_kind = rkind) meta) !ignored_loans; (* Then, check the borrow infos *) @@ -278,11 +278,11 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (fun _ info -> (* Note that we can't directly compare the sets - I guess they are * different depending on the order in which we add the elements... *) - cassert ( + sanity_check ( BorrowId.Set.elements info.loan_ids - = BorrowId.Set.elements info.borrow_ids) meta "TODO: Error message"; + = BorrowId.Set.elements info.borrow_ids) meta; match info.loan_kind with - | RMut -> cassert (BorrowId.Set.cardinal info.loan_ids = 1) meta "TODO: Error message" + | RMut -> sanity_check (BorrowId.Set.cardinal info.loan_ids = 1) meta | RShared -> ()) !borrows_infos @@ -297,7 +297,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = method! visit_VBottom info = (* No ⊥ inside borrowed values *) - cassert (Config.allow_bottom_below_borrow || not info.outer_borrow) meta "There should be no ⊥ inside borrowed values" + sanity_check (Config.allow_bottom_below_borrow || not info.outer_borrow) meta method! visit_ABottom _info = (* ⊥ inside an abstraction is not the same as in a regular value *) @@ -310,7 +310,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | VSharedLoan (_, _) -> set_outer_shared info | VMutLoan _ -> (* No mutable loan inside a shared loan *) - cassert (not info.outer_shared) meta "There should be no mutable loan inside a shared loan"; + sanity_check (not info.outer_shared) meta; set_outer_mut info in (* Continue exploring *) @@ -322,7 +322,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match bc with | VSharedBorrow _ -> set_outer_shared info | VReservedMutBorrow _ -> - cassert (not info.outer_borrow) meta "TODO: Error message"; + sanity_check (not info.outer_borrow) meta; set_outer_shared info | VMutBorrow (_, _) -> set_outer_mut info in @@ -369,7 +369,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) : unit = match (cv, ty) with - | VScalar sv, TInteger int_ty -> cassert (sv.int_ty = int_ty) meta "TODO: Error message" + | VScalar sv, TInteger int_ty -> sanity_check (sv.int_ty = int_ty) meta | VBool _, TBool | VChar _, TChar -> () | _ -> craise meta "Erroneous typing" @@ -393,17 +393,17 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = method! visit_EBinding info binder v = (* We also check that the regions are erased *) - cassert (ty_is_ety v.ty) meta "The regions should be erased"; + sanity_check (ty_is_ety v.ty) meta; super#visit_EBinding info binder v method! visit_symbolic_value inside_abs v = (* Check that the types have regions *) - cassert (ty_is_rty v.sv_ty) meta "The types should have regions"; + sanity_check (ty_is_rty v.sv_ty) meta; super#visit_symbolic_value inside_abs v method! visit_typed_value info tv = (* Check that the types have erased regions *) - cassert (ty_is_ety tv.ty) meta "The types should have erased regions"; + sanity_check (ty_is_ety tv.ty) meta; (* Check the current pair (value, type) *) (match (tv.value, tv.ty) with | VLiteral cv, TLiteral ty -> check_literal_type meta cv ty @@ -413,40 +413,40 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - cassert ( - List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message"; - cassert (List.length generics.types = List.length def.generics.types) meta "TODO: Error message"; + sanity_check ( + List.length generics.regions = List.length def.generics.regions) meta; + sanity_check (List.length generics.types = List.length def.generics.types) meta; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - cassert (VariantId.to_int variant_id < List.length variants) meta "The variant id should be consistent" + sanity_check (VariantId.to_int variant_id < List.length variants) meta | None, Struct _ -> () | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) let field_types = - AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def + AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def av.variant_id generics in let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : typed_value * ty) -> cassert (v.ty = ty) meta "The field types are not correct") + (fun ((v, ty) : typed_value * ty) -> sanity_check (v.ty = ty) meta) fields_with_types (* Tuple case *) | VAdt av, TAdt (TTuple, generics) -> - cassert (generics.regions = []) meta "TODO: Error message"; - cassert (generics.const_generics = []) meta "TODO: Error message"; - cassert (av.variant_id = None) meta "TODO: Error message"; + sanity_check (generics.regions = []) meta; + sanity_check (generics.const_generics = []) meta; + sanity_check (av.variant_id = None) meta; (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : typed_value * ty) -> cassert (v.ty = ty) meta "The fields does not have the proper values or there are not as many fields as field types at the same time TODO: error message") + (fun ((v, ty) : typed_value * ty) -> sanity_check (v.ty = ty) meta) fields_with_types (* Assumed type case *) | VAdt av, TAdt (TAssumed aty_id, generics) -> ( - cassert (av.variant_id = None) meta "TODO: Error message"; + sanity_check (av.variant_id = None) meta; match ( aty_id, av.field_values, @@ -456,20 +456,20 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = with (* Box *) | TBox, [ inner_value ], [], [ inner_ty ], [] -> - cassert (inner_value.ty = inner_ty) meta "TODO: Error message" + sanity_check (inner_value.ty = inner_ty) meta | TArray, inner_values, _, [ inner_ty ], [ cg ] -> (* *) - cassert ( + sanity_check ( List.for_all (fun (v : typed_value) -> v.ty = inner_ty) - inner_values) meta "TODO: Error message"; + inner_values) meta; (* The length is necessarily concrete *) let len = (ValuesUtils.literal_as_scalar (TypesUtils.const_generic_as_literal cg)) .value in - cassert (Z.of_int (List.length inner_values) = len) meta "TODO: Error message" + sanity_check (Z.of_int (List.length inner_values) = len) meta | (TSlice | TStr), _, _, _, _ -> craise meta "Unexpected" | _ -> craise meta "Erroneous type") | VBottom, _ -> (* Nothing to check *) () @@ -481,27 +481,27 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - cassert (sv.ty = ref_ty) meta "TODO: Error message" + sanity_check (sv.ty = ref_ty) meta | _ -> craise meta "Inconsistent context") | VMutBorrow (_, bv), RMut -> - cassert ( + sanity_check ( (* Check that the borrowed value has the proper type *) - bv.ty = ref_ty) meta "TODO: Error message" + bv.ty = ref_ty) meta | _ -> craise meta "Erroneous typing") | VLoan lc, ty -> ( match lc with - | VSharedLoan (_, sv) -> cassert (sv.ty = ty) meta "TODO: Error message" + | VSharedLoan (_, sv) -> sanity_check (sv.ty = ty) meta | VMutLoan bid -> ( (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with - | Concrete (VMutBorrow (_, bv)) -> cassert (bv.ty = ty) meta "The borrowed value does not have the proper type" + | Concrete (VMutBorrow (_, bv)) -> sanity_check (bv.ty = ty) meta | Abstract (AMutBorrow (_, sv)) -> - cassert (Substitute.erase_regions sv.ty = ty) meta "The borrowed value does not have the proper type" + sanity_check (Substitute.erase_regions sv.ty = ty) meta | _ -> craise meta "Inconsistent context")) | VSymbolic sv, ty -> let ty' = Substitute.erase_regions sv.sv_ty in - cassert (ty' = ty) meta "TODO: Error message" + sanity_check (ty' = ty) meta | _ -> craise meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_value info tv @@ -516,7 +516,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * *) method! visit_typed_avalue info atv = (* Check that the types have regions *) - cassert (ty_is_rty atv.ty) meta "The types should have regions"; + sanity_check (ty_is_rty atv.ty) meta; (* Check the current pair (value, type) *) (match (atv.value, atv.ty) with (* ADT case *) @@ -525,43 +525,43 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - cassert ( - List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message"; - cassert (List.length generics.types = List.length def.generics.types) meta "TODO: Error message"; - cassert ( + sanity_check ( + List.length generics.regions = List.length def.generics.regions) meta; + sanity_check (List.length generics.types = List.length def.generics.types) meta; + sanity_check ( List.length generics.const_generics - = List.length def.generics.const_generics) meta "TODO: Error message"; + = List.length def.generics.const_generics) meta; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - cassert (VariantId.to_int variant_id < List.length variants) meta "The variant id should be consistent" + sanity_check (VariantId.to_int variant_id < List.length variants) meta | None, Struct _ -> () | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) let field_types = - AssociatedTypes.type_decl_get_inst_norm_field_rtypes ctx def + AssociatedTypes.type_decl_get_inst_norm_field_rtypes meta ctx def av.variant_id generics in let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : typed_avalue * ty) -> cassert (v.ty = ty) meta "TODO: Error message") + (fun ((v, ty) : typed_avalue * ty) -> sanity_check (v.ty = ty) meta) fields_with_types (* Tuple case *) | AAdt av, TAdt (TTuple, generics) -> - cassert (generics.regions = []) meta "TODO: Error message"; - cassert (generics.const_generics = []) meta "TODO: Error message"; - cassert (av.variant_id = None) meta "TODO: Error message"; + sanity_check (generics.regions = []) meta; + sanity_check (generics.const_generics = []) meta; + sanity_check (av.variant_id = None) meta; (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : typed_avalue * ty) -> cassert (v.ty = ty) meta "The fields do not have the proper values or there are not as many fields as field types at the same time TODO: Error message") + (fun ((v, ty) : typed_avalue * ty) -> sanity_check (v.ty = ty) meta) fields_with_types (* Assumed type case *) | AAdt av, TAdt (TAssumed aty_id, generics) -> ( - cassert (av.variant_id = None) meta "TODO: Error message"; + sanity_check (av.variant_id = None) meta; match ( aty_id, av.field_values, @@ -571,27 +571,27 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = with (* Box *) | TBox, [ boxed_value ], [], [ boxed_ty ], [] -> - cassert (boxed_value.ty = boxed_ty) meta "TODO: Error message" + sanity_check (boxed_value.ty = boxed_ty) meta | _ -> craise meta "Erroneous type") | ABottom, _ -> (* Nothing to check *) () | ABorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with | AMutBorrow (_, av), RMut -> (* Check that the child value has the proper type *) - cassert (av.ty = ref_ty) meta "TODO: Error message" + sanity_check (av.ty = ref_ty) meta | ASharedBorrow bid, RShared -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan meta ek_all bid ctx in match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - cassert (sv.ty = Substitute.erase_regions ref_ty) meta "TODO: Error message" + sanity_check (sv.ty = Substitute.erase_regions ref_ty) meta | _ -> craise meta "Inconsistent context") - | AIgnoredMutBorrow (_opt_bid, av), RMut -> cassert (av.ty = ref_ty) meta "TODO: Error message" + | AIgnoredMutBorrow (_opt_bid, av), RMut -> sanity_check (av.ty = ref_ty) meta | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ }, RMut ) -> - cassert (given_back.ty = ref_ty) meta "TODO: Error message"; - cassert (child.ty = ref_ty) meta "TODO: Error message" + sanity_check (given_back.ty = ref_ty) meta; + sanity_check (child.ty = ref_ty) meta | AProjSharedBorrow _, RShared -> () | _ -> craise meta "Inconsistent context") | ALoan lc, aty -> ( @@ -599,54 +599,54 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av) -> ( let borrowed_aty = aloan_get_expected_child_type aty in - cassert (child_av.ty = borrowed_aty) meta "TODO: Error message"; + sanity_check (child_av.ty = borrowed_aty) meta; (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> - cassert (bv.ty = Substitute.erase_regions borrowed_aty) meta "TODO: Error message" + sanity_check (bv.ty = Substitute.erase_regions borrowed_aty) meta | Abstract (AMutBorrow (_, sv)) -> - cassert ( + sanity_check ( Substitute.erase_regions sv.ty - = Substitute.erase_regions borrowed_aty) meta "TODO: Error message" + = Substitute.erase_regions borrowed_aty) meta | _ -> craise meta "Inconsistent context") | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - cassert (child_av.ty = borrowed_aty) meta "TODO: Error message" + sanity_check (child_av.ty = borrowed_aty) meta | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - cassert (sv.ty = Substitute.erase_regions borrowed_aty) meta "TODO: Error message"; + sanity_check (sv.ty = Substitute.erase_regions borrowed_aty) meta; (* TODO: the type of aloans doesn't make sense, see above *) - cassert (child_av.ty = borrowed_aty) meta "TODO: Error message" + sanity_check (child_av.ty = borrowed_aty) meta | AEndedMutLoan { given_back; child; given_back_meta = _ } | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in - cassert (given_back.ty = borrowed_aty) meta "TODO: Error message"; - cassert (child.ty = borrowed_aty) meta "TODO: Error message" + sanity_check (given_back.ty = borrowed_aty) meta; + sanity_check (child.ty = borrowed_aty) meta | AIgnoredSharedLoan child_av -> - cassert (child_av.ty = aloan_get_expected_child_type aty) meta "TODO: Error message") + sanity_check (child_av.ty = aloan_get_expected_child_type aty) meta) | ASymbolic aproj, ty -> ( let ty1 = Substitute.erase_regions ty in match aproj with | AProjLoans (sv, _) -> let ty2 = Substitute.erase_regions sv.sv_ty in - cassert (ty1 = ty2) meta "TODO: Error message"; + sanity_check (ty1 = ty2) meta; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - cassert (ty_has_regions_in_set abs.regions sv.sv_ty) meta "The symbolic values should contain regions of interest or they should have been reduced to [] TODO: error message" + sanity_check (ty_has_regions_in_set abs.regions sv.sv_ty) meta | AProjBorrows (sv, proj_ty) -> let ty2 = Substitute.erase_regions sv.sv_ty in - cassert (ty1 = ty2) meta "TODO: Error message"; + sanity_check (ty1 = ty2) meta; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - cassert (ty_has_regions_in_set abs.regions proj_ty) meta "The symbolic values should contain regions of interest or they should have been reduced to [] TODO: error message" + sanity_check (ty_has_regions_in_set abs.regions proj_ty) meta | AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> match proj with - | AProjBorrows (_sv, ty') -> cassert (ty' = ty) meta "TODO: Error message" + | AProjBorrows (_sv, ty') -> sanity_check (ty' = ty) meta | AEndedProjBorrows _ | AIgnoredProjBorrows -> () | _ -> craise meta "Unexpected") given_back_ls @@ -657,7 +657,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (lazy ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv ^ "\n- value: " - ^ typed_avalue_to_string meta ctx atv + ^ typed_avalue_to_string ~meta:(Some meta) ctx atv ^ "\n- type: " ^ ty_to_string ctx atv.ty)); craise meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) @@ -766,15 +766,15 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = *) (* A symbolic value can't be both in the regular environment and inside * projectors of borrows in abstractions *) - cassert (info.env_count = 0 || info.aproj_borrows = []) meta "A symbolic value can't be both in the regular environment and inside projectors of borrows in abstractions"; + sanity_check (info.env_count = 0 || info.aproj_borrows = []) meta; (* A symbolic value containing borrows can't be duplicated (i.e., copied): * it must be expanded first *) if ty_has_borrows ctx.type_ctx.type_infos info.ty then - cassert (info.env_count <= 1) meta "A symbolic value containing borrows can't be duplicated (i.e., copied): it must be expanded first"; + sanity_check (info.env_count <= 1) meta; (* A duplicated symbolic value is necessarily primitively copyable *) - cassert (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta "A duplicated symbolic value should necessarily be primitively copyable"; + sanity_check (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta; - cassert (info.aproj_borrows = [] || info.aproj_loans <> []) meta "TODO: Error message"; + sanity_check (info.aproj_borrows = [] || info.aproj_loans <> []) meta; (* At the same time: * - check that the loans don't intersect * - compute the set of regions for which we project loans @@ -786,7 +786,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = let regions = RegionId.Set.fold (fun rid regions -> - cassert (not (RegionId.Set.mem rid regions)) meta "The loan projectors should contain the region projectors"; + sanity_check (not (RegionId.Set.mem rid regions)) meta; RegionId.Set.add rid regions) regions linfo.regions in @@ -796,8 +796,8 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Check that the union of the loan projectors contains the borrow projections. *) List.iter (fun binfo -> - cassert ( - projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta "The union of the loan projectors should contain the borrow projections") + sanity_check ( + projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta) info.aproj_borrows; () in @@ -806,7 +806,7 @@ let check_symbolic_values (meta : Meta.meta) (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 meta ctx)); + log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); check_loans_borrows_relation_invariant meta ctx; check_borrowed_values_invariant meta ctx; check_typing_invariant meta ctx; -- cgit v1.2.3 From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 17:14:27 +0100 Subject: formatting --- compiler/Invariants.ml | 124 +++++++++++++++++++++++++++++++------------------ 1 file changed, 80 insertions(+), 44 deletions(-) (limited to 'compiler/Invariants.ml') diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 9b389ba5..1c10bf7e 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -48,14 +48,16 @@ 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 (meta : Meta.meta) (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 (* Link all the id representants to a borrow information *) let borrows_infos : borrow_info BorrowId.Map.t ref = ref BorrowId.Map.empty in let context_to_string () : string = - eval_ctx_to_string ~meta:(Some meta) ctx ^ "- representants:\n" + eval_ctx_to_string ~meta:(Some meta) ctx + ^ "- representants:\n" ^ ids_reprs_to_string " " !ids_reprs ^ "\n- info:\n" ^ borrows_infos_to_string " " !borrows_infos @@ -194,9 +196,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let infos = BorrowId.Map.update repr_bid (fun x -> - match x with - | Some _ -> Some info - | None -> craise meta "Unreachable") + match x with Some _ -> Some info | None -> craise meta "Unreachable") !borrows_infos in borrows_infos := infos @@ -278,9 +278,10 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (fun _ info -> (* Note that we can't directly compare the sets - I guess they are * different depending on the order in which we add the elements... *) - sanity_check ( - BorrowId.Set.elements info.loan_ids - = BorrowId.Set.elements info.borrow_ids) meta; + sanity_check + (BorrowId.Set.elements info.loan_ids + = BorrowId.Set.elements info.borrow_ids) + meta; match info.loan_kind with | RMut -> sanity_check (BorrowId.Set.cardinal info.loan_ids = 1) meta | RShared -> ()) @@ -297,7 +298,9 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = method! visit_VBottom info = (* No ⊥ inside borrowed values *) - sanity_check (Config.allow_bottom_below_borrow || not info.outer_borrow) meta + sanity_check + (Config.allow_bottom_below_borrow || not info.outer_borrow) + meta method! visit_ABottom _info = (* ⊥ inside an abstraction is not the same as in a regular value *) @@ -367,7 +370,8 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let info = { outer_borrow = false; outer_shared = false } in visitor#visit_eval_ctx info ctx -let check_literal_type (meta : Meta.meta) (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 -> sanity_check (sv.int_ty = int_ty) meta | VBool _, TBool | VChar _, TChar -> () @@ -413,13 +417,18 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - sanity_check ( - List.length generics.regions = List.length def.generics.regions) meta; - sanity_check (List.length generics.types = List.length def.generics.types) meta; + sanity_check + (List.length generics.regions = List.length def.generics.regions) + meta; + sanity_check + (List.length generics.types = List.length def.generics.types) + meta; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - sanity_check (VariantId.to_int variant_id < List.length variants) meta + sanity_check + (VariantId.to_int variant_id < List.length variants) + meta | None, Struct _ -> () | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) @@ -429,7 +438,8 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = in let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : typed_value * ty) -> sanity_check (v.ty = ty) meta) + (fun ((v, ty) : typed_value * ty) -> + sanity_check (v.ty = ty) meta) fields_with_types (* Tuple case *) | VAdt av, TAdt (TTuple, generics) -> @@ -442,7 +452,8 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : typed_value * ty) -> sanity_check (v.ty = ty) meta) + (fun ((v, ty) : typed_value * ty) -> + sanity_check (v.ty = ty) meta) fields_with_types (* Assumed type case *) | VAdt av, TAdt (TAssumed aty_id, generics) -> ( @@ -459,10 +470,11 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = sanity_check (inner_value.ty = inner_ty) meta | TArray, inner_values, _, [ inner_ty ], [ cg ] -> (* *) - sanity_check ( - List.for_all - (fun (v : typed_value) -> v.ty = inner_ty) - inner_values) meta; + sanity_check + (List.for_all + (fun (v : typed_value) -> v.ty = inner_ty) + inner_values) + meta; (* The length is necessarily concrete *) let len = (ValuesUtils.literal_as_scalar @@ -484,9 +496,10 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = sanity_check (sv.ty = ref_ty) meta | _ -> craise meta "Inconsistent context") | VMutBorrow (_, bv), RMut -> - sanity_check ( - (* Check that the borrowed value has the proper type *) - bv.ty = ref_ty) meta + sanity_check + ((* Check that the borrowed value has the proper type *) + bv.ty = ref_ty) + meta | _ -> craise meta "Erroneous typing") | VLoan lc, ty -> ( match lc with @@ -495,7 +508,8 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with - | Concrete (VMutBorrow (_, bv)) -> sanity_check (bv.ty = ty) meta + | Concrete (VMutBorrow (_, bv)) -> + sanity_check (bv.ty = ty) meta | Abstract (AMutBorrow (_, sv)) -> sanity_check (Substitute.erase_regions sv.ty = ty) meta | _ -> craise meta "Inconsistent context")) @@ -525,16 +539,22 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - sanity_check ( - List.length generics.regions = List.length def.generics.regions) meta; - sanity_check (List.length generics.types = List.length def.generics.types) meta; - sanity_check ( - List.length generics.const_generics - = List.length def.generics.const_generics) meta; + sanity_check + (List.length generics.regions = List.length def.generics.regions) + meta; + sanity_check + (List.length generics.types = List.length def.generics.types) + meta; + sanity_check + (List.length generics.const_generics + = List.length def.generics.const_generics) + meta; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - sanity_check (VariantId.to_int variant_id < List.length variants) meta + sanity_check + (VariantId.to_int variant_id < List.length variants) + meta | None, Struct _ -> () | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) @@ -544,7 +564,8 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = in let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : typed_avalue * ty) -> sanity_check (v.ty = ty) meta) + (fun ((v, ty) : typed_avalue * ty) -> + sanity_check (v.ty = ty) meta) fields_with_types (* Tuple case *) | AAdt av, TAdt (TTuple, generics) -> @@ -557,7 +578,8 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : typed_avalue * ty) -> sanity_check (v.ty = ty) meta) + (fun ((v, ty) : typed_avalue * ty) -> + sanity_check (v.ty = ty) meta) fields_with_types (* Assumed type case *) | AAdt av, TAdt (TAssumed aty_id, generics) -> ( @@ -587,7 +609,8 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | Abstract (ASharedLoan (_, sv, _)) -> sanity_check (sv.ty = Substitute.erase_regions ref_ty) meta | _ -> craise meta "Inconsistent context") - | AIgnoredMutBorrow (_opt_bid, av), RMut -> sanity_check (av.ty = ref_ty) meta + | AIgnoredMutBorrow (_opt_bid, av), RMut -> + sanity_check (av.ty = ref_ty) meta | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ }, RMut ) -> sanity_check (given_back.ty = ref_ty) meta; @@ -604,18 +627,23 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let glc = lookup_borrow meta ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> - sanity_check (bv.ty = Substitute.erase_regions borrowed_aty) meta + sanity_check + (bv.ty = Substitute.erase_regions borrowed_aty) + meta | Abstract (AMutBorrow (_, sv)) -> - sanity_check ( - Substitute.erase_regions sv.ty - = Substitute.erase_regions borrowed_aty) meta + sanity_check + (Substitute.erase_regions sv.ty + = Substitute.erase_regions borrowed_aty) + meta | _ -> craise meta "Inconsistent context") | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in sanity_check (child_av.ty = borrowed_aty) meta | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - sanity_check (sv.ty = Substitute.erase_regions borrowed_aty) meta; + sanity_check + (sv.ty = Substitute.erase_regions borrowed_aty) + meta; (* TODO: the type of aloans doesn't make sense, see above *) sanity_check (child_av.ty = borrowed_aty) meta | AEndedMutLoan { given_back; child; given_back_meta = _ } @@ -624,7 +652,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = sanity_check (given_back.ty = borrowed_aty) meta; sanity_check (child.ty = borrowed_aty) meta | AIgnoredSharedLoan child_av -> - sanity_check (child_av.ty = aloan_get_expected_child_type aty) meta) + sanity_check + (child_av.ty = aloan_get_expected_child_type aty) + meta) | ASymbolic aproj, ty -> ( let ty1 = Substitute.erase_regions ty in match aproj with @@ -772,7 +802,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = if ty_has_borrows ctx.type_ctx.type_infos info.ty then sanity_check (info.env_count <= 1) meta; (* A duplicated symbolic value is necessarily primitively copyable *) - sanity_check (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta; + sanity_check + (info.env_count <= 1 || ty_is_primitively_copyable info.ty) + meta; sanity_check (info.aproj_borrows = [] || info.aproj_loans <> []) meta; (* At the same time: @@ -796,8 +828,10 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Check that the union of the loan projectors contains the borrow projections. *) List.iter (fun binfo -> - sanity_check ( - projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta) + sanity_check + (projection_contains meta info.ty loan_regions binfo.proj_ty + binfo.regions) + meta) info.aproj_borrows; () in @@ -806,7 +840,9 @@ let check_symbolic_values (meta : Meta.meta) (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 ~meta:(Some meta) ctx)); + log#ldebug + (lazy + ("Checking invariants:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); check_loans_borrows_relation_invariant meta ctx; check_borrowed_values_invariant meta ctx; check_typing_invariant meta ctx; -- cgit v1.2.3 From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 13:21:08 +0100 Subject: added file and line arg to craise and cassert --- compiler/Invariants.ml | 178 ++++++++++++++++++++++++------------------------- 1 file changed, 89 insertions(+), 89 deletions(-) (limited to 'compiler/Invariants.ml') diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 1c10bf7e..830661d2 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -79,12 +79,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let infos = !borrows_infos in (* Use the first borrow id as representant *) let repr_bid = BorrowId.Set.min_elt bids in - sanity_check (not (BorrowId.Map.mem repr_bid infos)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem repr_bid infos)) meta; (* Insert the mappings to the representant *) let reprs = BorrowId.Set.fold (fun bid reprs -> - sanity_check (not (BorrowId.Map.mem bid reprs)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid reprs)) meta; BorrowId.Map.add bid repr_bid reprs) bids reprs in @@ -107,8 +107,8 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let reprs = !ids_reprs in let infos = !borrows_infos in (* Sanity checks *) - sanity_check (not (BorrowId.Map.mem bid reprs)) meta; - sanity_check (not (BorrowId.Map.mem bid infos)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid reprs)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid infos)) meta; (* Add the mapping for the representant *) let reprs = BorrowId.Map.add bid bid reprs in (* Add the mapping for the loan info *) @@ -186,7 +186,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string () in log#serror err; - craise meta err + craise __FILE__ __LINE__ meta err in let update_info (bid : BorrowId.id) (info : borrow_info) : unit = @@ -196,7 +196,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let infos = BorrowId.Map.update repr_bid (fun x -> - match x with Some _ -> Some info | None -> craise meta "Unreachable") + match x with Some _ -> Some info | None -> craise __FILE__ __LINE__ meta "Unreachable") !borrows_infos in borrows_infos := infos @@ -210,12 +210,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (* Check that the borrow kind is consistent *) (match (info.loan_kind, kind) with | RShared, (BShared | BReserved) | RMut, BMut -> () - | _ -> craise meta "Invariant not satisfied"); + | _ -> craise __FILE__ __LINE__ meta "Invariant not satisfied"); (* A reserved borrow can't point to a value inside an abstraction *) - sanity_check (kind <> BReserved || not info.loan_in_abs) meta; + sanity_check __FILE__ __LINE__ (kind <> BReserved || not info.loan_in_abs) meta; (* Insert the borrow id *) let borrow_ids = info.borrow_ids in - sanity_check (not (BorrowId.Set.mem bid borrow_ids)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem bid borrow_ids)) meta; let info = { info with borrow_ids = BorrowId.Set.add bid borrow_ids } in (* Update the info in the map *) update_info bid info @@ -270,7 +270,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : List.iter (fun (rkind, bid) -> let info = find_info bid in - sanity_check (info.loan_kind = rkind) meta) + sanity_check __FILE__ __LINE__ (info.loan_kind = rkind) meta) !ignored_loans; (* Then, check the borrow infos *) @@ -278,12 +278,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (fun _ info -> (* Note that we can't directly compare the sets - I guess they are * different depending on the order in which we add the elements... *) - sanity_check + sanity_check __FILE__ __LINE__ (BorrowId.Set.elements info.loan_ids = BorrowId.Set.elements info.borrow_ids) meta; match info.loan_kind with - | RMut -> sanity_check (BorrowId.Set.cardinal info.loan_ids = 1) meta + | RMut -> sanity_check __FILE__ __LINE__ (BorrowId.Set.cardinal info.loan_ids = 1) meta | RShared -> ()) !borrows_infos @@ -298,7 +298,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = method! visit_VBottom info = (* No ⊥ inside borrowed values *) - sanity_check + sanity_check __FILE__ __LINE__ (Config.allow_bottom_below_borrow || not info.outer_borrow) meta @@ -313,7 +313,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | VSharedLoan (_, _) -> set_outer_shared info | VMutLoan _ -> (* No mutable loan inside a shared loan *) - sanity_check (not info.outer_shared) meta; + sanity_check __FILE__ __LINE__ (not info.outer_shared) meta; set_outer_mut info in (* Continue exploring *) @@ -325,7 +325,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match bc with | VSharedBorrow _ -> set_outer_shared info | VReservedMutBorrow _ -> - sanity_check (not info.outer_borrow) meta; + sanity_check __FILE__ __LINE__ (not info.outer_borrow) meta; set_outer_shared info | VMutBorrow (_, _) -> set_outer_mut info in @@ -373,9 +373,9 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) : unit = match (cv, ty) with - | VScalar sv, TInteger int_ty -> sanity_check (sv.int_ty = int_ty) meta + | VScalar sv, TInteger int_ty -> sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta | VBool _, TBool | VChar _, TChar -> () - | _ -> craise meta "Erroneous typing" + | _ -> craise __FILE__ __LINE__ meta "Erroneous typing" let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (* TODO: the type of aloans doens't make sense: they have a type @@ -397,17 +397,17 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = method! visit_EBinding info binder v = (* We also check that the regions are erased *) - sanity_check (ty_is_ety v.ty) meta; + sanity_check __FILE__ __LINE__ (ty_is_ety v.ty) meta; super#visit_EBinding info binder v method! visit_symbolic_value inside_abs v = (* Check that the types have regions *) - sanity_check (ty_is_rty v.sv_ty) meta; + sanity_check __FILE__ __LINE__ (ty_is_rty v.sv_ty) meta; super#visit_symbolic_value inside_abs v method! visit_typed_value info tv = (* Check that the types have erased regions *) - sanity_check (ty_is_ety tv.ty) meta; + sanity_check __FILE__ __LINE__ (ty_is_ety tv.ty) meta; (* Check the current pair (value, type) *) (match (tv.value, tv.ty) with | VLiteral cv, TLiteral ty -> check_literal_type meta cv ty @@ -417,20 +417,20 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - sanity_check + sanity_check __FILE__ __LINE__ (List.length generics.regions = List.length def.generics.regions) meta; - sanity_check + sanity_check __FILE__ __LINE__ (List.length generics.types = List.length def.generics.types) meta; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - sanity_check + sanity_check __FILE__ __LINE__ (VariantId.to_int variant_id < List.length variants) meta | None, Struct _ -> () - | _ -> craise meta "Erroneous typing"); + | _ -> craise __FILE__ __LINE__ meta "Erroneous typing"); (* Check that the field types are correct *) let field_types = AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def @@ -439,13 +439,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let fields_with_types = List.combine av.field_values field_types in List.iter (fun ((v, ty) : typed_value * ty) -> - sanity_check (v.ty = ty) meta) + sanity_check __FILE__ __LINE__ (v.ty = ty) meta) fields_with_types (* Tuple case *) | VAdt av, TAdt (TTuple, generics) -> - sanity_check (generics.regions = []) meta; - sanity_check (generics.const_generics = []) meta; - sanity_check (av.variant_id = None) meta; + sanity_check __FILE__ __LINE__ (generics.regions = []) meta; + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; + sanity_check __FILE__ __LINE__ (av.variant_id = None) meta; (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = @@ -453,11 +453,11 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = in List.iter (fun ((v, ty) : typed_value * ty) -> - sanity_check (v.ty = ty) meta) + sanity_check __FILE__ __LINE__ (v.ty = ty) meta) fields_with_types (* Assumed type case *) | VAdt av, TAdt (TAssumed aty_id, generics) -> ( - sanity_check (av.variant_id = None) meta; + sanity_check __FILE__ __LINE__ (av.variant_id = None) meta; match ( aty_id, av.field_values, @@ -467,10 +467,10 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = with (* Box *) | TBox, [ inner_value ], [], [ inner_ty ], [] -> - sanity_check (inner_value.ty = inner_ty) meta + sanity_check __FILE__ __LINE__ (inner_value.ty = inner_ty) meta | TArray, inner_values, _, [ inner_ty ], [ cg ] -> (* *) - sanity_check + sanity_check __FILE__ __LINE__ (List.for_all (fun (v : typed_value) -> v.ty = inner_ty) inner_values) @@ -481,9 +481,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (TypesUtils.const_generic_as_literal cg)) .value in - sanity_check (Z.of_int (List.length inner_values) = len) meta - | (TSlice | TStr), _, _, _, _ -> craise meta "Unexpected" - | _ -> craise meta "Erroneous type") + sanity_check __FILE__ __LINE__ (Z.of_int (List.length inner_values) = len) meta + | (TSlice | TStr), _, _, _, _ -> craise __FILE__ __LINE__ meta "Unexpected" + | _ -> craise __FILE__ __LINE__ meta "Erroneous type") | VBottom, _ -> (* Nothing to check *) () | VBorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with @@ -493,30 +493,30 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - sanity_check (sv.ty = ref_ty) meta - | _ -> craise meta "Inconsistent context") + sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) meta + | _ -> craise __FILE__ __LINE__ meta "Inconsistent context") | VMutBorrow (_, bv), RMut -> - sanity_check + sanity_check __FILE__ __LINE__ ((* Check that the borrowed value has the proper type *) bv.ty = ref_ty) meta - | _ -> craise meta "Erroneous typing") + | _ -> craise __FILE__ __LINE__ meta "Erroneous typing") | VLoan lc, ty -> ( match lc with - | VSharedLoan (_, sv) -> sanity_check (sv.ty = ty) meta + | VSharedLoan (_, sv) -> sanity_check __FILE__ __LINE__ (sv.ty = ty) meta | VMutLoan bid -> ( (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> - sanity_check (bv.ty = ty) meta + sanity_check __FILE__ __LINE__ (bv.ty = ty) meta | Abstract (AMutBorrow (_, sv)) -> - sanity_check (Substitute.erase_regions sv.ty = ty) meta - | _ -> craise meta "Inconsistent context")) + sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = ty) meta + | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")) | VSymbolic sv, ty -> let ty' = Substitute.erase_regions sv.sv_ty in - sanity_check (ty' = ty) meta - | _ -> craise meta "Erroneous typing"); + sanity_check __FILE__ __LINE__ (ty' = ty) meta + | _ -> craise __FILE__ __LINE__ meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_value info tv @@ -530,7 +530,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * *) method! visit_typed_avalue info atv = (* Check that the types have regions *) - sanity_check (ty_is_rty atv.ty) meta; + sanity_check __FILE__ __LINE__ (ty_is_rty atv.ty) meta; (* Check the current pair (value, type) *) (match (atv.value, atv.ty) with (* ADT case *) @@ -539,24 +539,24 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - sanity_check + sanity_check __FILE__ __LINE__ (List.length generics.regions = List.length def.generics.regions) meta; - sanity_check + sanity_check __FILE__ __LINE__ (List.length generics.types = List.length def.generics.types) meta; - sanity_check + sanity_check __FILE__ __LINE__ (List.length generics.const_generics = List.length def.generics.const_generics) meta; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - sanity_check + sanity_check __FILE__ __LINE__ (VariantId.to_int variant_id < List.length variants) meta | None, Struct _ -> () - | _ -> craise meta "Erroneous typing"); + | _ -> craise __FILE__ __LINE__ meta "Erroneous typing"); (* Check that the field types are correct *) let field_types = AssociatedTypes.type_decl_get_inst_norm_field_rtypes meta ctx def @@ -565,13 +565,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let fields_with_types = List.combine av.field_values field_types in List.iter (fun ((v, ty) : typed_avalue * ty) -> - sanity_check (v.ty = ty) meta) + sanity_check __FILE__ __LINE__ (v.ty = ty) meta) fields_with_types (* Tuple case *) | AAdt av, TAdt (TTuple, generics) -> - sanity_check (generics.regions = []) meta; - sanity_check (generics.const_generics = []) meta; - sanity_check (av.variant_id = None) meta; + sanity_check __FILE__ __LINE__ (generics.regions = []) meta; + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; + sanity_check __FILE__ __LINE__ (av.variant_id = None) meta; (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = @@ -579,11 +579,11 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = in List.iter (fun ((v, ty) : typed_avalue * ty) -> - sanity_check (v.ty = ty) meta) + sanity_check __FILE__ __LINE__ (v.ty = ty) meta) fields_with_types (* Assumed type case *) | AAdt av, TAdt (TAssumed aty_id, generics) -> ( - sanity_check (av.variant_id = None) meta; + sanity_check __FILE__ __LINE__ (av.variant_id = None) meta; match ( aty_id, av.field_values, @@ -593,66 +593,66 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = with (* Box *) | TBox, [ boxed_value ], [], [ boxed_ty ], [] -> - sanity_check (boxed_value.ty = boxed_ty) meta - | _ -> craise meta "Erroneous type") + sanity_check __FILE__ __LINE__ (boxed_value.ty = boxed_ty) meta + | _ -> craise __FILE__ __LINE__ meta "Erroneous type") | ABottom, _ -> (* Nothing to check *) () | ABorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with | AMutBorrow (_, av), RMut -> (* Check that the child value has the proper type *) - sanity_check (av.ty = ref_ty) meta + sanity_check __FILE__ __LINE__ (av.ty = ref_ty) meta | ASharedBorrow bid, RShared -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan meta ek_all bid ctx in match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - sanity_check (sv.ty = Substitute.erase_regions ref_ty) meta - | _ -> craise meta "Inconsistent context") + sanity_check __FILE__ __LINE__ (sv.ty = Substitute.erase_regions ref_ty) meta + | _ -> craise __FILE__ __LINE__ meta "Inconsistent context") | AIgnoredMutBorrow (_opt_bid, av), RMut -> - sanity_check (av.ty = ref_ty) meta + sanity_check __FILE__ __LINE__ (av.ty = ref_ty) meta | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ }, RMut ) -> - sanity_check (given_back.ty = ref_ty) meta; - sanity_check (child.ty = ref_ty) meta + sanity_check __FILE__ __LINE__ (given_back.ty = ref_ty) meta; + sanity_check __FILE__ __LINE__ (child.ty = ref_ty) meta | AProjSharedBorrow _, RShared -> () - | _ -> craise meta "Inconsistent context") + | _ -> craise __FILE__ __LINE__ meta "Inconsistent context") | ALoan lc, aty -> ( match lc with | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av) -> ( let borrowed_aty = aloan_get_expected_child_type aty in - sanity_check (child_av.ty = borrowed_aty) meta; + sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta; (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> - sanity_check + sanity_check __FILE__ __LINE__ (bv.ty = Substitute.erase_regions borrowed_aty) meta | Abstract (AMutBorrow (_, sv)) -> - sanity_check + sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = Substitute.erase_regions borrowed_aty) meta - | _ -> craise meta "Inconsistent context") + | _ -> craise __FILE__ __LINE__ meta "Inconsistent context") | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - sanity_check (child_av.ty = borrowed_aty) meta + sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - sanity_check + sanity_check __FILE__ __LINE__ (sv.ty = Substitute.erase_regions borrowed_aty) meta; (* TODO: the type of aloans doesn't make sense, see above *) - sanity_check (child_av.ty = borrowed_aty) meta + sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta | AEndedMutLoan { given_back; child; given_back_meta = _ } | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in - sanity_check (given_back.ty = borrowed_aty) meta; - sanity_check (child.ty = borrowed_aty) meta + sanity_check __FILE__ __LINE__ (given_back.ty = borrowed_aty) meta; + sanity_check __FILE__ __LINE__ (child.ty = borrowed_aty) meta | AIgnoredSharedLoan child_av -> - sanity_check + sanity_check __FILE__ __LINE__ (child_av.ty = aloan_get_expected_child_type aty) meta) | ASymbolic aproj, ty -> ( @@ -660,25 +660,25 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match aproj with | AProjLoans (sv, _) -> let ty2 = Substitute.erase_regions sv.sv_ty in - sanity_check (ty1 = ty2) meta; + sanity_check __FILE__ __LINE__ (ty1 = ty2) meta; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - sanity_check (ty_has_regions_in_set abs.regions sv.sv_ty) meta + sanity_check __FILE__ __LINE__ (ty_has_regions_in_set abs.regions sv.sv_ty) meta | AProjBorrows (sv, proj_ty) -> let ty2 = Substitute.erase_regions sv.sv_ty in - sanity_check (ty1 = ty2) meta; + sanity_check __FILE__ __LINE__ (ty1 = ty2) meta; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - sanity_check (ty_has_regions_in_set abs.regions proj_ty) meta + sanity_check __FILE__ __LINE__ (ty_has_regions_in_set abs.regions proj_ty) meta | AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> match proj with - | AProjBorrows (_sv, ty') -> sanity_check (ty' = ty) meta + | AProjBorrows (_sv, ty') -> sanity_check __FILE__ __LINE__ (ty' = ty) meta | AEndedProjBorrows _ | AIgnoredProjBorrows -> () - | _ -> craise meta "Unexpected") + | _ -> craise __FILE__ __LINE__ meta "Unexpected") given_back_ls | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()) | AIgnored, _ -> () @@ -689,7 +689,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = ^ "\n- value: " ^ typed_avalue_to_string ~meta:(Some meta) ctx atv ^ "\n- type: " ^ ty_to_string ctx atv.ty)); - craise meta "Erroneous typing"); + craise __FILE__ __LINE__ meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv end @@ -796,17 +796,17 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = *) (* A symbolic value can't be both in the regular environment and inside * projectors of borrows in abstractions *) - sanity_check (info.env_count = 0 || info.aproj_borrows = []) meta; + sanity_check __FILE__ __LINE__ (info.env_count = 0 || info.aproj_borrows = []) meta; (* A symbolic value containing borrows can't be duplicated (i.e., copied): * it must be expanded first *) if ty_has_borrows ctx.type_ctx.type_infos info.ty then - sanity_check (info.env_count <= 1) meta; + sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta; (* A duplicated symbolic value is necessarily primitively copyable *) - sanity_check + sanity_check __FILE__ __LINE__ (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta; - sanity_check (info.aproj_borrows = [] || info.aproj_loans <> []) meta; + sanity_check __FILE__ __LINE__ (info.aproj_borrows = [] || info.aproj_loans <> []) meta; (* At the same time: * - check that the loans don't intersect * - compute the set of regions for which we project loans @@ -818,7 +818,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = let regions = RegionId.Set.fold (fun rid regions -> - sanity_check (not (RegionId.Set.mem rid regions)) meta; + sanity_check __FILE__ __LINE__ (not (RegionId.Set.mem rid regions)) meta; RegionId.Set.add rid regions) regions linfo.regions in @@ -828,7 +828,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Check that the union of the loan projectors contains the borrow projections. *) List.iter (fun binfo -> - sanity_check + sanity_check __FILE__ __LINE__ (projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta) -- cgit v1.2.3 From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 14:07:36 +0100 Subject: formatting and changed save_error condition for failing from b to not b --- compiler/Invariants.ml | 61 +++++++++++++++++++++++++++++++++++++------------- 1 file changed, 45 insertions(+), 16 deletions(-) (limited to 'compiler/Invariants.ml') diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 830661d2..642d7a37 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -196,7 +196,9 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let infos = BorrowId.Map.update repr_bid (fun x -> - match x with Some _ -> Some info | None -> craise __FILE__ __LINE__ meta "Unreachable") + match x with + | Some _ -> Some info + | None -> craise __FILE__ __LINE__ meta "Unreachable") !borrows_infos in borrows_infos := infos @@ -212,7 +214,9 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : | RShared, (BShared | BReserved) | RMut, BMut -> () | _ -> craise __FILE__ __LINE__ meta "Invariant not satisfied"); (* A reserved borrow can't point to a value inside an abstraction *) - sanity_check __FILE__ __LINE__ (kind <> BReserved || not info.loan_in_abs) meta; + sanity_check __FILE__ __LINE__ + (kind <> BReserved || not info.loan_in_abs) + meta; (* Insert the borrow id *) let borrow_ids = info.borrow_ids in sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem bid borrow_ids)) meta; @@ -283,7 +287,10 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : = BorrowId.Set.elements info.borrow_ids) meta; match info.loan_kind with - | RMut -> sanity_check __FILE__ __LINE__ (BorrowId.Set.cardinal info.loan_ids = 1) meta + | RMut -> + sanity_check __FILE__ __LINE__ + (BorrowId.Set.cardinal info.loan_ids = 1) + meta | RShared -> ()) !borrows_infos @@ -373,7 +380,8 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) : unit = match (cv, ty) with - | VScalar sv, TInteger int_ty -> sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta + | VScalar sv, TInteger int_ty -> + sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta | VBool _, TBool | VChar _, TChar -> () | _ -> craise __FILE__ __LINE__ meta "Erroneous typing" @@ -481,8 +489,11 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (TypesUtils.const_generic_as_literal cg)) .value in - sanity_check __FILE__ __LINE__ (Z.of_int (List.length inner_values) = len) meta - | (TSlice | TStr), _, _, _, _ -> craise __FILE__ __LINE__ meta "Unexpected" + sanity_check __FILE__ __LINE__ + (Z.of_int (List.length inner_values) = len) + meta + | (TSlice | TStr), _, _, _, _ -> + craise __FILE__ __LINE__ meta "Unexpected" | _ -> craise __FILE__ __LINE__ meta "Erroneous type") | VBottom, _ -> (* Nothing to check *) () | VBorrow bc, TRef (_, ref_ty, rkind) -> ( @@ -503,7 +514,8 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | _ -> craise __FILE__ __LINE__ meta "Erroneous typing") | VLoan lc, ty -> ( match lc with - | VSharedLoan (_, sv) -> sanity_check __FILE__ __LINE__ (sv.ty = ty) meta + | VSharedLoan (_, sv) -> + sanity_check __FILE__ __LINE__ (sv.ty = ty) meta | VMutLoan bid -> ( (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in @@ -511,7 +523,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | Concrete (VMutBorrow (_, bv)) -> sanity_check __FILE__ __LINE__ (bv.ty = ty) meta | Abstract (AMutBorrow (_, sv)) -> - sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = ty) meta + sanity_check __FILE__ __LINE__ + (Substitute.erase_regions sv.ty = ty) + meta | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")) | VSymbolic sv, ty -> let ty' = Substitute.erase_regions sv.sv_ty in @@ -607,7 +621,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - sanity_check __FILE__ __LINE__ (sv.ty = Substitute.erase_regions ref_ty) meta + sanity_check __FILE__ __LINE__ + (sv.ty = Substitute.erase_regions ref_ty) + meta | _ -> craise __FILE__ __LINE__ meta "Inconsistent context") | AIgnoredMutBorrow (_opt_bid, av), RMut -> sanity_check __FILE__ __LINE__ (av.ty = ref_ty) meta @@ -649,7 +665,9 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | AEndedMutLoan { given_back; child; given_back_meta = _ } | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in - sanity_check __FILE__ __LINE__ (given_back.ty = borrowed_aty) meta; + sanity_check __FILE__ __LINE__ + (given_back.ty = borrowed_aty) + meta; sanity_check __FILE__ __LINE__ (child.ty = borrowed_aty) meta | AIgnoredSharedLoan child_av -> sanity_check __FILE__ __LINE__ @@ -664,19 +682,24 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - sanity_check __FILE__ __LINE__ (ty_has_regions_in_set abs.regions sv.sv_ty) meta + sanity_check __FILE__ __LINE__ + (ty_has_regions_in_set abs.regions sv.sv_ty) + meta | AProjBorrows (sv, proj_ty) -> let ty2 = Substitute.erase_regions sv.sv_ty in sanity_check __FILE__ __LINE__ (ty1 = ty2) meta; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - sanity_check __FILE__ __LINE__ (ty_has_regions_in_set abs.regions proj_ty) meta + sanity_check __FILE__ __LINE__ + (ty_has_regions_in_set abs.regions proj_ty) + meta | AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> match proj with - | AProjBorrows (_sv, ty') -> sanity_check __FILE__ __LINE__ (ty' = ty) meta + | AProjBorrows (_sv, ty') -> + sanity_check __FILE__ __LINE__ (ty' = ty) meta | AEndedProjBorrows _ | AIgnoredProjBorrows -> () | _ -> craise __FILE__ __LINE__ meta "Unexpected") given_back_ls @@ -796,7 +819,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = *) (* A symbolic value can't be both in the regular environment and inside * projectors of borrows in abstractions *) - sanity_check __FILE__ __LINE__ (info.env_count = 0 || info.aproj_borrows = []) meta; + sanity_check __FILE__ __LINE__ + (info.env_count = 0 || info.aproj_borrows = []) + meta; (* A symbolic value containing borrows can't be duplicated (i.e., copied): * it must be expanded first *) if ty_has_borrows ctx.type_ctx.type_infos info.ty then @@ -806,7 +831,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta; - sanity_check __FILE__ __LINE__ (info.aproj_borrows = [] || info.aproj_loans <> []) meta; + sanity_check __FILE__ __LINE__ + (info.aproj_borrows = [] || info.aproj_loans <> []) + meta; (* At the same time: * - check that the loans don't intersect * - compute the set of regions for which we project loans @@ -818,7 +845,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = let regions = RegionId.Set.fold (fun rid regions -> - sanity_check __FILE__ __LINE__ (not (RegionId.Set.mem rid regions)) meta; + sanity_check __FILE__ __LINE__ + (not (RegionId.Set.mem rid regions)) + meta; RegionId.Set.add rid regions) regions linfo.regions in -- cgit v1.2.3