summaryrefslogtreecommitdiff
path: root/compiler/Invariants.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Invariants.ml')
-rw-r--r--compiler/Invariants.ml61
1 files changed, 45 insertions, 16 deletions
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