diff options
Diffstat (limited to 'compiler/Invariants.ml')
| -rw-r--r-- | compiler/Invariants.ml | 164 |
1 files changed, 82 insertions, 82 deletions
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; |