summaryrefslogtreecommitdiff
path: root/compiler/Invariants.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Invariants.ml')
-rw-r--r--compiler/Invariants.ml513
1 files changed, 252 insertions, 261 deletions
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 5c8ec7af..e0e3f354 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -1,29 +1,23 @@
(* The following module defines functions to check that some invariants
* are always maintained by evaluation contexts *)
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module Assoc = AssociatedTypes
-module A = LlbcAst
-module L = Logging
+open Types
+open Values
+open Contexts
open Cps
open TypesUtils
open InterpreterUtils
open InterpreterBorrowsCore
(** The local logger *)
-let log = L.invariants_log
+let log = Logging.invariants_log
type borrow_info = {
- loan_kind : T.ref_kind;
+ loan_kind : ref_kind;
loan_in_abs : bool;
(* true if the loan was found in an abstraction *)
- loan_ids : V.BorrowId.Set.t;
- borrow_ids : V.BorrowId.Set.t;
+ loan_ids : BorrowId.Set.t;
+ borrow_ids : BorrowId.Set.t;
}
[@@deriving show]
@@ -39,30 +33,26 @@ let set_outer_mut (info : outer_borrow_info) : outer_borrow_info =
let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info =
{ outer_borrow = true; outer_shared = true }
-let ids_reprs_to_string (indent : string)
- (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
- V.BorrowId.Map.to_string (Some indent) V.BorrowId.to_string reprs
+let ids_reprs_to_string (indent : string) (reprs : BorrowId.id BorrowId.Map.t) :
+ string =
+ BorrowId.Map.to_string (Some indent) BorrowId.to_string reprs
let borrows_infos_to_string (indent : string)
- (infos : borrow_info V.BorrowId.Map.t) : string =
- V.BorrowId.Map.to_string (Some indent) show_borrow_info infos
+ (infos : borrow_info BorrowId.Map.t) : string =
+ BorrowId.Map.to_string (Some indent) show_borrow_info infos
-type borrow_kind = Mut | Shared | Reserved
+type borrow_kind = BMut | BShared | BReserved
(** Check that:
- 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 : C.eval_ctx) : unit =
+let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
(* Link all the borrow ids to a representant - necessary because of shared
* borrows/loans *)
- let ids_reprs : V.BorrowId.id V.BorrowId.Map.t ref =
- ref V.BorrowId.Map.empty
- in
+ 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 V.BorrowId.Map.t ref =
- ref V.BorrowId.Map.empty
- in
+ 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"
^ ids_reprs_to_string " " !ids_reprs
@@ -73,62 +63,61 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
* map, we register it in this list; once the borrows_infos map is completely
* built, we check that all the borrow ids of the ignored loans are in this
* map *)
- let ignored_loans : (T.ref_kind * V.BorrowId.id) list ref = ref [] in
+ let ignored_loans : (ref_kind * BorrowId.id) list ref = ref [] in
(* first, register all the loans *)
(* Some utilities to register the loans *)
- let register_ignored_loan (rkind : T.ref_kind) (bid : V.BorrowId.id) : unit =
+ let register_ignored_loan (rkind : ref_kind) (bid : BorrowId.id) : unit =
ignored_loans := (rkind, bid) :: !ignored_loans
in
- let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.Set.t) : unit
- =
+ let register_shared_loan (loan_in_abs : bool) (bids : BorrowId.Set.t) : unit =
let reprs = !ids_reprs in
let infos = !borrows_infos in
(* Use the first borrow id as representant *)
- let repr_bid = V.BorrowId.Set.min_elt bids in
- assert (not (V.BorrowId.Map.mem repr_bid infos));
+ let repr_bid = BorrowId.Set.min_elt bids in
+ assert (not (BorrowId.Map.mem repr_bid infos));
(* Insert the mappings to the representant *)
let reprs =
- V.BorrowId.Set.fold
+ BorrowId.Set.fold
(fun bid reprs ->
- assert (not (V.BorrowId.Map.mem bid reprs));
- V.BorrowId.Map.add bid repr_bid reprs)
+ assert (not (BorrowId.Map.mem bid reprs));
+ BorrowId.Map.add bid repr_bid reprs)
bids reprs
in
(* Insert the loan info *)
let info =
{
- loan_kind = T.Shared;
+ loan_kind = RShared;
loan_in_abs;
loan_ids = bids;
- borrow_ids = V.BorrowId.Set.empty;
+ borrow_ids = BorrowId.Set.empty;
}
in
- let infos = V.BorrowId.Map.add repr_bid info infos in
+ let infos = BorrowId.Map.add repr_bid info infos in
(* Update *)
ids_reprs := reprs;
borrows_infos := infos
in
- let register_mut_loan (loan_in_abs : bool) (bid : V.BorrowId.id) : unit =
+ let register_mut_loan (loan_in_abs : bool) (bid : BorrowId.id) : unit =
let reprs = !ids_reprs in
let infos = !borrows_infos in
(* Sanity checks *)
- assert (not (V.BorrowId.Map.mem bid reprs));
- assert (not (V.BorrowId.Map.mem bid infos));
+ assert (not (BorrowId.Map.mem bid reprs));
+ assert (not (BorrowId.Map.mem bid infos));
(* Add the mapping for the representant *)
- let reprs = V.BorrowId.Map.add bid bid reprs in
+ let reprs = BorrowId.Map.add bid bid reprs in
(* Add the mapping for the loan info *)
let info =
{
- loan_kind = T.Mut;
+ loan_kind = RMut;
loan_in_abs;
- loan_ids = V.BorrowId.Set.singleton bid;
- borrow_ids = V.BorrowId.Set.empty;
+ loan_ids = BorrowId.Set.singleton bid;
+ borrow_ids = BorrowId.Set.empty;
}
in
- let infos = V.BorrowId.Map.add bid info infos in
+ let infos = BorrowId.Map.add bid info infos in
(* Update *)
ids_reprs := reprs;
borrows_infos := infos
@@ -136,22 +125,22 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
let loans_visitor =
object
- inherit [_] C.iter_eval_ctx as super
+ inherit [_] iter_eval_ctx as super
- method! visit_Var _ binder v =
+ method! visit_EBinding _ binder v =
let inside_abs = false in
- super#visit_Var inside_abs binder v
+ super#visit_EBinding inside_abs binder v
- method! visit_Abs _ abs =
+ method! visit_EAbs _ abs =
let inside_abs = true in
- super#visit_Abs inside_abs abs
+ super#visit_EAbs inside_abs abs
method! visit_loan_content inside_abs lc =
(* Register the loan *)
let _ =
match lc with
- | V.SharedLoan (bids, _) -> register_shared_loan inside_abs bids
- | V.MutLoan bid -> register_mut_loan inside_abs bid
+ | VSharedLoan (bids, _) -> register_shared_loan inside_abs bids
+ | VMutLoan bid -> register_mut_loan inside_abs bid
in
(* Continue exploring *)
super#visit_loan_content inside_abs lc
@@ -159,14 +148,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
method! visit_aloan_content inside_abs lc =
let _ =
match lc with
- | V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid
- | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
- | V.AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid
- | V.AIgnoredMutLoan (None, _)
- | V.AIgnoredSharedLoan _
- | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
- | V.AEndedSharedLoan (_, _)
- | V.AEndedIgnoredMutLoan
+ | AMutLoan (bid, _) -> register_mut_loan inside_abs bid
+ | ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
+ | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan RMut bid
+ | AIgnoredMutLoan (None, _)
+ | AIgnoredSharedLoan _
+ | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+ | AEndedSharedLoan (_, _)
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ } ->
(* Do nothing *)
()
@@ -182,27 +171,27 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
(* Then, register all the borrows *)
(* Some utilities to register the borrows *)
- let find_info (bid : V.BorrowId.id) : borrow_info =
+ let find_info (bid : BorrowId.id) : borrow_info =
(* Find the representant *)
- match V.BorrowId.Map.find_opt bid !ids_reprs with
+ match BorrowId.Map.find_opt bid !ids_reprs with
| Some repr_bid ->
(* Lookup the info *)
- V.BorrowId.Map.find repr_bid !borrows_infos
+ BorrowId.Map.find repr_bid !borrows_infos
| None ->
let err =
"find_info: could not find the representant of borrow "
- ^ V.BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
+ ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
in
log#serror err;
raise (Failure err)
in
- let update_info (bid : V.BorrowId.id) (info : borrow_info) : unit =
+ let update_info (bid : BorrowId.id) (info : borrow_info) : unit =
(* Find the representant *)
- let repr_bid = V.BorrowId.Map.find bid !ids_reprs in
+ let repr_bid = BorrowId.Map.find bid !ids_reprs in
(* Update the info *)
let infos =
- V.BorrowId.Map.update repr_bid
+ BorrowId.Map.update repr_bid
(fun x ->
match x with
| Some _ -> Some info
@@ -214,39 +203,39 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
let register_ignored_borrow = register_ignored_loan in
- let register_borrow (kind : borrow_kind) (bid : V.BorrowId.id) : unit =
+ let register_borrow (kind : borrow_kind) (bid : BorrowId.id) : unit =
(* Lookup the info *)
let info = find_info bid in
(* Check that the borrow kind is consistent *)
(match (info.loan_kind, kind) with
- | T.Shared, (Shared | Reserved) | T.Mut, Mut -> ()
+ | RShared, (BShared | BReserved) | RMut, BMut -> ()
| _ -> raise (Failure "Invariant not satisfied"));
(* A reserved borrow can't point to a value inside an abstraction *)
- assert (kind <> Reserved || not info.loan_in_abs);
+ assert (kind <> BReserved || not info.loan_in_abs);
(* Insert the borrow id *)
let borrow_ids = info.borrow_ids in
- assert (not (V.BorrowId.Set.mem bid borrow_ids));
- let info = { info with borrow_ids = V.BorrowId.Set.add bid borrow_ids } in
+ assert (not (BorrowId.Set.mem bid borrow_ids));
+ let info = { info with borrow_ids = BorrowId.Set.add bid borrow_ids } in
(* Update the info in the map *)
update_info bid info
in
let borrows_visitor =
object
- inherit [_] C.iter_eval_ctx as super
+ inherit [_] iter_eval_ctx as super
method! visit_abstract_shared_borrow _ asb =
match asb with
- | V.AsbBorrow bid -> register_borrow Shared bid
- | V.AsbProjReborrows _ -> ()
+ | AsbBorrow bid -> register_borrow BShared bid
+ | AsbProjReborrows _ -> ()
method! visit_borrow_content env bc =
(* Register the loan *)
let _ =
match bc with
- | V.SharedBorrow bid -> register_borrow Shared bid
- | V.MutBorrow (bid, _) -> register_borrow Mut bid
- | V.ReservedMutBorrow bid -> register_borrow Reserved bid
+ | VSharedBorrow bid -> register_borrow BShared bid
+ | VMutBorrow (bid, _) -> register_borrow BMut bid
+ | VReservedMutBorrow bid -> register_borrow BReserved bid
in
(* Continue exploring *)
super#visit_borrow_content env bc
@@ -254,12 +243,12 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
method! visit_aborrow_content env bc =
let _ =
match bc with
- | V.AMutBorrow (bid, _) -> register_borrow Mut bid
- | V.ASharedBorrow bid -> register_borrow Shared bid
- | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
- | V.AIgnoredMutBorrow (None, _)
- | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _
- | V.AEndedSharedBorrow | V.AProjSharedBorrow _ ->
+ | AMutBorrow (bid, _) -> register_borrow BMut bid
+ | ASharedBorrow bid -> register_borrow BShared bid
+ | AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow RMut bid
+ | AIgnoredMutBorrow (None, _)
+ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow
+ | AProjSharedBorrow _ ->
(* Do nothing *)
()
in
@@ -284,28 +273,28 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
!ignored_loans;
(* Then, check the borrow infos *)
- V.BorrowId.Map.iter
+ BorrowId.Map.iter
(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 (
- V.BorrowId.Set.elements info.loan_ids
- = V.BorrowId.Set.elements info.borrow_ids);
+ BorrowId.Set.elements info.loan_ids
+ = BorrowId.Set.elements info.borrow_ids);
match info.loan_kind with
- | T.Mut -> assert (V.BorrowId.Set.cardinal info.loan_ids = 1)
- | T.Shared -> ())
+ | RMut -> assert (BorrowId.Set.cardinal info.loan_ids = 1)
+ | RShared -> ())
!borrows_infos
(** Check that:
- borrows/loans can't contain ⊥ or reserved mut borrows
- shared loans can't contain mutable loans
*)
-let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
+let check_borrowed_values_invariant (ctx : eval_ctx) : unit =
let visitor =
object
- inherit [_] C.iter_eval_ctx as super
+ inherit [_] iter_eval_ctx as super
- method! visit_Bottom info =
+ method! visit_VBottom info =
(* No ⊥ inside borrowed values *)
assert (Config.allow_bottom_below_borrow || not info.outer_borrow)
@@ -317,8 +306,8 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
(* Update the info *)
let info =
match lc with
- | V.SharedLoan (_, _) -> set_outer_shared info
- | V.MutLoan _ ->
+ | VSharedLoan (_, _) -> set_outer_shared info
+ | VMutLoan _ ->
(* No mutable loan inside a shared loan *)
assert (not info.outer_shared);
set_outer_mut info
@@ -330,11 +319,11 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
(* Update the info *)
let info =
match bc with
- | V.SharedBorrow _ -> set_outer_shared info
- | V.ReservedMutBorrow _ ->
+ | VSharedBorrow _ -> set_outer_shared info
+ | VReservedMutBorrow _ ->
assert (not info.outer_borrow);
set_outer_shared info
- | V.MutBorrow (_, _) -> set_outer_mut info
+ | VMutBorrow (_, _) -> set_outer_mut info
in
(* Continue exploring *)
super#visit_borrow_content info bc
@@ -343,17 +332,16 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
(* Update the info *)
let info =
match lc with
- | V.AMutLoan (_, _) -> set_outer_mut info
- | V.ASharedLoan (_, _, _) -> set_outer_shared info
- | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
- ->
+ | AMutLoan (_, _) -> set_outer_mut info
+ | ASharedLoan (_, _, _) -> set_outer_shared info
+ | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } ->
set_outer_mut info
- | V.AEndedSharedLoan (_, _) -> set_outer_shared info
- | V.AIgnoredMutLoan (_, _) -> set_outer_mut info
- | V.AEndedIgnoredMutLoan
+ | AEndedSharedLoan (_, _) -> set_outer_shared info
+ | AIgnoredMutLoan (_, _) -> set_outer_mut info
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ } ->
set_outer_mut info
- | V.AIgnoredSharedLoan _ -> set_outer_shared info
+ | AIgnoredSharedLoan _ -> set_outer_shared info
in
(* Continue exploring *)
super#visit_aloan_content info lc
@@ -362,12 +350,12 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
(* Update the info *)
let info =
match bc with
- | V.AMutBorrow (_, _) -> set_outer_mut info
- | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info
- | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
- | V.AEndedIgnoredMutBorrow _ ->
+ | AMutBorrow (_, _) -> set_outer_mut info
+ | ASharedBorrow _ | AEndedSharedBorrow -> set_outer_shared info
+ | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _
+ ->
set_outer_mut info
- | V.AProjSharedBorrow _ -> set_outer_shared info
+ | AProjSharedBorrow _ -> set_outer_shared info
in
(* Continue exploring *)
super#visit_aborrow_content info bc
@@ -378,130 +366,140 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
let info = { outer_borrow = false; outer_shared = false } in
visitor#visit_eval_ctx info ctx
-let check_literal_type (cv : V.literal) (ty : PV.literal_type) : unit =
+let check_literal_type (cv : literal) (ty : literal_type) : unit =
match (cv, ty) with
- | PV.Scalar sv, PV.Integer int_ty -> assert (sv.int_ty = int_ty)
- | PV.Bool _, PV.Bool | PV.Char _, PV.Char -> ()
+ | VScalar sv, TInteger int_ty -> assert (sv.int_ty = int_ty)
+ | VBool _, TBool | VChar _, TChar -> ()
| _ -> raise (Failure "Erroneous typing")
-let check_typing_invariant (ctx : C.eval_ctx) : unit =
+let check_typing_invariant (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
* children. In order to isolate the problem (for future modifications)
- * we introduce function, so that we can easily spot all the involved
+ * we introduce this function, so that we can easily spot all the involved
* places.
* *)
- let aloan_get_expected_child_type (ty : 'r T.ty) : 'r T.ty =
+ let aloan_get_expected_child_type (ty : ty) : ty =
let _, ty, _ = ty_get_ref ty in
ty
in
let visitor =
object
- inherit [_] C.iter_eval_ctx as super
+ inherit [_] iter_eval_ctx as super
method! visit_abs _ abs = super#visit_abs (Some abs) abs
+ method! visit_EBinding info binder v =
+ (* We also check that the regions are erased *)
+ assert (ty_is_ety v.ty);
+ 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);
+ 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);
(* Check the current pair (value, type) *)
- (match (tv.V.value, tv.V.ty) with
- | V.Literal cv, T.Literal ty -> check_literal_type cv ty
+ (match (tv.value, tv.ty) with
+ | VLiteral cv, TLiteral ty -> check_literal_type cv ty
(* ADT case *)
- | V.Adt av, T.Adt (T.AdtId def_id, generics) ->
+ | VAdt av, TAdt (TAdtId def_id, generics) ->
(* Retrieve the definition to check the variant id, the number of
* parameters, etc. *)
- let def = C.ctx_lookup_type_decl ctx def_id in
+ 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);
(* Check that the variant id is consistent *)
- (match (av.V.variant_id, def.T.kind) with
- | Some variant_id, T.Enum variants ->
- assert (T.VariantId.to_int variant_id < List.length variants)
- | None, T.Struct _ -> ()
+ (match (av.variant_id, def.kind) with
+ | Some variant_id, Enum variants ->
+ assert (VariantId.to_int variant_id < List.length variants)
+ | None, Struct _ -> ()
| _ -> raise (Failure "Erroneous typing"));
(* Check that the field types are correct *)
let field_types =
- Assoc.type_decl_get_inst_norm_field_etypes ctx def av.V.variant_id
- generics
- in
- let fields_with_types =
- List.combine av.V.field_values field_types
+ AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def
+ av.variant_id generics
in
+ let fields_with_types = List.combine av.field_values field_types in
List.iter
- (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty))
+ (fun ((v, ty) : typed_value * ty) -> assert (v.ty = ty))
fields_with_types
(* Tuple case *)
- | V.Adt av, T.Adt (T.Tuple, generics) ->
+ | VAdt av, TAdt (TTuple, generics) ->
assert (generics.regions = []);
assert (generics.const_generics = []);
- assert (av.V.variant_id = None);
+ assert (av.variant_id = None);
(* 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.V.field_values generics.types
+ List.combine av.field_values generics.types
in
List.iter
- (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty))
+ (fun ((v, ty) : typed_value * ty) -> assert (v.ty = ty))
fields_with_types
(* Assumed type case *)
- | V.Adt av, T.Adt (T.Assumed aty_id, generics) -> (
- assert (av.V.variant_id = None);
+ | VAdt av, TAdt (TAssumed aty_id, generics) -> (
+ assert (av.variant_id = None);
match
( aty_id,
- av.V.field_values,
+ av.field_values,
generics.regions,
generics.types,
generics.const_generics )
with
(* Box *)
- | T.Box, [ inner_value ], [], [ inner_ty ], [] ->
- assert (inner_value.V.ty = inner_ty)
- | T.Array, inner_values, _, [ inner_ty ], [ cg ] ->
+ | TBox, [ inner_value ], [], [ inner_ty ], [] ->
+ assert (inner_value.ty = inner_ty)
+ | TArray, inner_values, _, [ inner_ty ], [ cg ] ->
(* *)
assert (
List.for_all
- (fun (v : V.typed_value) -> v.V.ty = inner_ty)
+ (fun (v : typed_value) -> v.ty = inner_ty)
inner_values);
(* The length is necessarily concrete *)
let len =
- (PrimitiveValuesUtils.literal_as_scalar
+ (ValuesUtils.literal_as_scalar
(TypesUtils.const_generic_as_literal cg))
.value
in
assert (Z.of_int (List.length inner_values) = len)
- | (T.Slice | T.Str), _, _, _, _ -> raise (Failure "Unexpected")
+ | (TSlice | TStr), _, _, _, _ -> raise (Failure "Unexpected")
| _ -> raise (Failure "Erroneous type"))
- | V.Bottom, _ -> (* Nothing to check *) ()
- | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
+ | VBottom, _ -> (* Nothing to check *) ()
+ | VBorrow bc, TRef (_, ref_ty, rkind) -> (
match (bc, rkind) with
- | V.SharedBorrow bid, T.Shared | V.ReservedMutBorrow bid, T.Mut -> (
+ | 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
match glc with
- | Concrete (V.SharedLoan (_, sv))
- | Abstract (V.ASharedLoan (_, sv, _)) ->
- assert (sv.V.ty = ref_ty)
+ | Concrete (VSharedLoan (_, sv))
+ | Abstract (ASharedLoan (_, sv, _)) ->
+ assert (sv.ty = ref_ty)
| _ -> raise (Failure "Inconsistent context"))
- | V.MutBorrow (_, bv), T.Mut ->
+ | VMutBorrow (_, bv), RMut ->
assert (
(* Check that the borrowed value has the proper type *)
- bv.V.ty = ref_ty)
+ bv.ty = ref_ty)
| _ -> raise (Failure "Erroneous typing"))
- | V.Loan lc, ty -> (
+ | VLoan lc, ty -> (
match lc with
- | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
- | V.MutLoan bid -> (
+ | 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
match glc with
- | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty)
- | Abstract (V.AMutBorrow (_, sv)) ->
- assert (Subst.erase_regions sv.V.ty = ty)
+ | Concrete (VMutBorrow (_, bv)) -> assert (bv.ty = ty)
+ | Abstract (AMutBorrow (_, sv)) ->
+ assert (Substitute.erase_regions sv.ty = ty)
| _ -> raise (Failure "Inconsistent context")))
- | V.Symbolic sv, ty ->
- let ty' = Subst.erase_regions sv.V.sv_ty in
+ | VSymbolic sv, ty ->
+ let ty' = Substitute.erase_regions sv.sv_ty in
assert (ty' = ty)
| _ -> raise (Failure "Erroneous typing"));
(* Continue exploring to inspect the subterms *)
@@ -516,13 +514,15 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
* so the cost of maintenance should be pretty low.
* *)
method! visit_typed_avalue info atv =
+ (* Check that the types have regions *)
+ assert (ty_is_rty atv.ty);
(* Check the current pair (value, type) *)
- (match (atv.V.value, atv.V.ty) with
+ (match (atv.value, atv.ty) with
(* ADT case *)
- | V.AAdt av, T.Adt (T.AdtId def_id, generics) ->
+ | AAdt av, TAdt (TAdtId def_id, generics) ->
(* Retrieve the definition to check the variant id, the number of
* parameters, etc. *)
- let def = C.ctx_lookup_type_decl ctx def_id in
+ 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);
@@ -531,162 +531,153 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
List.length generics.const_generics
= List.length def.generics.const_generics);
(* Check that the variant id is consistent *)
- (match (av.V.variant_id, def.T.kind) with
- | Some variant_id, T.Enum variants ->
- assert (T.VariantId.to_int variant_id < List.length variants)
- | None, T.Struct _ -> ()
+ (match (av.variant_id, def.kind) with
+ | Some variant_id, Enum variants ->
+ assert (VariantId.to_int variant_id < List.length variants)
+ | None, Struct _ -> ()
| _ -> raise (Failure "Erroneous typing"));
(* Check that the field types are correct *)
let field_types =
- Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.V.variant_id
- generics
- in
- let fields_with_types =
- List.combine av.V.field_values field_types
+ AssociatedTypes.type_decl_get_inst_norm_field_rtypes ctx def
+ av.variant_id generics
in
+ let fields_with_types = List.combine av.field_values field_types in
List.iter
- (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty))
+ (fun ((v, ty) : typed_avalue * ty) -> assert (v.ty = ty))
fields_with_types
(* Tuple case *)
- | V.AAdt av, T.Adt (T.Tuple, generics) ->
+ | AAdt av, TAdt (TTuple, generics) ->
assert (generics.regions = []);
assert (generics.const_generics = []);
- assert (av.V.variant_id = None);
+ assert (av.variant_id = None);
(* 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.V.field_values generics.types
+ List.combine av.field_values generics.types
in
List.iter
- (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty))
+ (fun ((v, ty) : typed_avalue * ty) -> assert (v.ty = ty))
fields_with_types
(* Assumed type case *)
- | V.AAdt av, T.Adt (T.Assumed aty_id, generics) -> (
- assert (av.V.variant_id = None);
+ | AAdt av, TAdt (TAssumed aty_id, generics) -> (
+ assert (av.variant_id = None);
match
( aty_id,
- av.V.field_values,
+ av.field_values,
generics.regions,
generics.types,
generics.const_generics )
with
(* Box *)
- | T.Box, [ boxed_value ], [], [ boxed_ty ], [] ->
- assert (boxed_value.V.ty = boxed_ty)
+ | TBox, [ boxed_value ], [], [ boxed_ty ], [] ->
+ assert (boxed_value.ty = boxed_ty)
| _ -> raise (Failure "Erroneous type"))
- | V.ABottom, _ -> (* Nothing to check *) ()
- | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
+ | ABottom, _ -> (* Nothing to check *) ()
+ | ABorrow bc, TRef (_, ref_ty, rkind) -> (
match (bc, rkind) with
- | V.AMutBorrow (_, av), T.Mut ->
+ | AMutBorrow (_, av), RMut ->
(* Check that the child value has the proper type *)
- assert (av.V.ty = ref_ty)
- | V.ASharedBorrow bid, T.Shared -> (
+ 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
match glc with
- | Concrete (V.SharedLoan (_, sv))
- | Abstract (V.ASharedLoan (_, sv, _)) ->
- assert (sv.V.ty = Subst.erase_regions ref_ty)
+ | Concrete (VSharedLoan (_, sv))
+ | Abstract (ASharedLoan (_, sv, _)) ->
+ assert (sv.ty = Substitute.erase_regions ref_ty)
| _ -> raise (Failure "Inconsistent context"))
- | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut ->
- assert (av.V.ty = ref_ty)
- | ( V.AEndedIgnoredMutBorrow
- { given_back; child; given_back_meta = _ },
- T.Mut ) ->
- assert (given_back.V.ty = ref_ty);
- assert (child.V.ty = ref_ty)
- | V.AProjSharedBorrow _, T.Shared -> ()
+ | 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"))
- | V.ALoan lc, aty -> (
+ | ALoan lc, aty -> (
match lc with
- | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (Some bid, child_av)
+ | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av)
-> (
let borrowed_aty = aloan_get_expected_child_type aty in
- assert (child_av.V.ty = borrowed_aty);
+ 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
match glc with
- | Concrete (V.MutBorrow (_, bv)) ->
- assert (bv.V.ty = Subst.erase_regions borrowed_aty)
- | Abstract (V.AMutBorrow (_, sv)) ->
+ | Concrete (VMutBorrow (_, bv)) ->
+ assert (bv.ty = Substitute.erase_regions borrowed_aty)
+ | Abstract (AMutBorrow (_, sv)) ->
assert (
- Subst.erase_regions sv.V.ty
- = Subst.erase_regions borrowed_aty)
+ Substitute.erase_regions sv.ty
+ = Substitute.erase_regions borrowed_aty)
| _ -> raise (Failure "Inconsistent context"))
- | V.AIgnoredMutLoan (None, child_av) ->
+ | AIgnoredMutLoan (None, child_av) ->
let borrowed_aty = aloan_get_expected_child_type aty in
- assert (child_av.V.ty = borrowed_aty)
- | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
- ->
+ assert (child_av.ty = borrowed_aty)
+ | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) ->
let borrowed_aty = aloan_get_expected_child_type aty in
- assert (sv.V.ty = Subst.erase_regions borrowed_aty);
+ assert (sv.ty = Substitute.erase_regions borrowed_aty);
(* TODO: the type of aloans doesn't make sense, see above *)
- assert (child_av.V.ty = borrowed_aty)
- | V.AEndedMutLoan { given_back; child; given_back_meta = _ }
- | V.AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ }
- ->
+ assert (child_av.ty = borrowed_aty)
+ | 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.V.ty = borrowed_aty);
- assert (child.V.ty = borrowed_aty)
- | V.AIgnoredSharedLoan child_av ->
- assert (child_av.V.ty = aloan_get_expected_child_type aty))
- | V.ASymbolic aproj, ty -> (
- let ty1 = Subst.erase_regions ty in
+ assert (given_back.ty = borrowed_aty);
+ assert (child.ty = borrowed_aty)
+ | AIgnoredSharedLoan child_av ->
+ assert (child_av.ty = aloan_get_expected_child_type aty))
+ | ASymbolic aproj, ty -> (
+ let ty1 = Substitute.erase_regions ty in
match aproj with
- | V.AProjLoans (sv, _) ->
- let ty2 = Subst.erase_regions sv.V.sv_ty in
+ | AProjLoans (sv, _) ->
+ let ty2 = Substitute.erase_regions sv.sv_ty in
assert (ty1 = ty2);
(* 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.V.sv_ty)
- | V.AProjBorrows (sv, proj_ty) ->
- let ty2 = Subst.erase_regions sv.V.sv_ty in
+ assert (ty_has_regions_in_set abs.regions sv.sv_ty)
+ | AProjBorrows (sv, proj_ty) ->
+ let ty2 = Substitute.erase_regions sv.sv_ty in
assert (ty1 = ty2);
(* 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)
- | V.AEndedProjLoans (_msv, given_back_ls) ->
+ | AEndedProjLoans (_msv, given_back_ls) ->
List.iter
(fun (_, proj) ->
match proj with
- | V.AProjBorrows (_sv, ty') -> assert (ty' = ty)
- | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ()
+ | AProjBorrows (_sv, ty') -> assert (ty' = ty)
+ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()
| _ -> raise (Failure "Unexpected"))
given_back_ls
- | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ())
- | V.AIgnored, _ -> ()
+ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
+ | AIgnored, _ -> ()
| _ ->
log#lerror
(lazy
- ("Erroneous typing:" ^ "\n- raw value: "
- ^ V.show_typed_avalue atv ^ "\n- value: "
+ ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
+ ^ "\n- value: "
^ typed_avalue_to_string ctx atv
- ^ "\n- type: " ^ rty_to_string ctx atv.V.ty));
+ ^ "\n- type: " ^ ty_to_string ctx atv.ty));
raise (Failure "Erroneous typing"));
(* Continue exploring to inspect the subterms *)
super#visit_typed_avalue info atv
end
in
- visitor#visit_eval_ctx (None : V.abs option) ctx
+ visitor#visit_eval_ctx (None : abs option) ctx
type proj_borrows_info = {
- abs_id : V.AbstractionId.id;
- regions : T.RegionId.Set.t;
- proj_ty : T.rty;
+ abs_id : AbstractionId.id;
+ regions : RegionId.Set.t;
+ proj_ty : rty; (** The regions shouldn't be erased *)
as_shared_value : bool; (** True if the value is below a shared borrow *)
}
[@@deriving show]
-type proj_loans_info = {
- abs_id : V.AbstractionId.id;
- regions : T.RegionId.Set.t;
-}
+type proj_loans_info = { abs_id : AbstractionId.id; regions : RegionId.Set.t }
[@@deriving show]
type sv_info = {
- ty : T.rty;
+ ty : rty; (** The regions shouldn't be erased *)
env_count : int;
aproj_borrows : proj_borrows_info list;
aproj_loans : proj_loans_info list;
@@ -706,32 +697,32 @@ type sv_info = {
- the union of the aproj_loans contains the aproj_borrows applied on the
same symbolic values
*)
-let check_symbolic_values (ctx : C.eval_ctx) : unit =
+let check_symbolic_values (ctx : eval_ctx) : unit =
(* Small utility *)
- let module M = V.SymbolicValueId.Map in
+ let module M = SymbolicValueId.Map in
let infos : sv_info M.t ref = ref M.empty in
- let lookup_info (sv : V.symbolic_value) : sv_info =
- match M.find_opt sv.V.sv_id !infos with
+ let lookup_info (sv : symbolic_value) : sv_info =
+ match M.find_opt sv.sv_id !infos with
| Some info -> info
| None ->
{ ty = sv.sv_ty; env_count = 0; aproj_borrows = []; aproj_loans = [] }
in
- let update_info (sv : V.symbolic_value) (info : sv_info) =
+ let update_info (sv : symbolic_value) (info : sv_info) =
infos := M.add sv.sv_id info !infos
in
- let add_env_sv (sv : V.symbolic_value) : unit =
+ let add_env_sv (sv : symbolic_value) : unit =
let info = lookup_info sv in
let info = { info with env_count = info.env_count + 1 } in
update_info sv info
in
- let add_aproj_borrows (sv : V.symbolic_value) abs_id regions proj_ty
+ let add_aproj_borrows (sv : symbolic_value) abs_id regions proj_ty
as_shared_value : unit =
let info = lookup_info sv in
let binfo = { abs_id; regions; proj_ty; as_shared_value } in
let info = { info with aproj_borrows = binfo :: info.aproj_borrows } in
update_info sv info
in
- let add_aproj_loans (sv : V.symbolic_value) abs_id regions : unit =
+ let add_aproj_loans (sv : symbolic_value) abs_id regions : unit =
let info = lookup_info sv in
let linfo = { abs_id; regions } in
let info = { info with aproj_loans = linfo :: info.aproj_loans } in
@@ -740,14 +731,14 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit =
(* Visitor *)
let obj =
object
- inherit [_] C.iter_eval_ctx as super
+ inherit [_] iter_eval_ctx as super
method! visit_abs _ abs = super#visit_abs (Some abs) abs
- method! visit_Symbolic _ sv = add_env_sv sv
+ method! visit_VSymbolic _ sv = add_env_sv sv
method! visit_abstract_shared_borrow abs asb =
let abs = Option.get abs in
match asb with
- | V.AsbBorrow _ -> ()
+ | AsbBorrow _ -> ()
| AsbProjReborrows (sv, proj_ty) ->
add_aproj_borrows sv abs.abs_id abs.regions proj_ty true
@@ -766,7 +757,7 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit =
log#ldebug
(lazy
("check_symbolic_values: collected information:\n"
- ^ V.SymbolicValueId.Map.to_string (Some " ") show_sv_info !infos));
+ ^ SymbolicValueId.Map.to_string (Some " ") show_sv_info !infos));
(* Check *)
let check_info _id info =
(* TODO: check that:
@@ -792,14 +783,14 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit =
List.fold_left
(fun regions linfo ->
let regions =
- T.RegionId.Set.fold
+ RegionId.Set.fold
(fun rid regions ->
- assert (not (T.RegionId.Set.mem rid regions));
- T.RegionId.Set.add rid regions)
+ assert (not (RegionId.Set.mem rid regions));
+ RegionId.Set.add rid regions)
regions linfo.regions
in
regions)
- T.RegionId.Set.empty info.aproj_loans
+ RegionId.Set.empty info.aproj_loans
in
(* Check that the union of the loan projectors contains the borrow projections. *)
List.iter
@@ -812,7 +803,7 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit =
M.iter check_info !infos
-let check_invariants (ctx : C.eval_ctx) : unit =
+let check_invariants (ctx : eval_ctx) : unit =
if !Config.check_invariants then (
log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx));
check_loans_borrows_relation_invariant ctx;