summaryrefslogtreecommitdiff
path: root/src/Invariants.ml
diff options
context:
space:
mode:
authorJonathan Protzenko2022-01-06 10:12:44 -0800
committerJonathan Protzenko2022-01-06 10:12:44 -0800
commitc3c1d91a976fdac52830239adb6429f09ea888a8 (patch)
tree15205f3a6356ad80effdc8b48641fff23a89466c /src/Invariants.ml
parent9872966d3c7a97ce8cd9ef16ab934ffa09c23e13 (diff)
parenta310c6036568d8f62e09804c67064686d106afd4 (diff)
Merge remote-tracking branch 'refs/remotes/origin/main'
Diffstat (limited to '')
-rw-r--r--src/Invariants.ml334
1 files changed, 325 insertions, 9 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 509c19ad..e214e820 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -8,7 +8,9 @@ module C = Contexts
module Subst = Substitute
module A = CfimAst
module L = Logging
+open TypesUtils
open InterpreterUtils
+open InterpreterBorrowsCore
let debug_invariants : bool ref = ref false
@@ -27,6 +29,23 @@ type outer_borrow_info = {
outer_shared : bool; (* true if the value is borrowed as shared *)
}
+let set_outer_mut (info : outer_borrow_info) : outer_borrow_info =
+ { info with outer_borrow = true }
+
+let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info =
+ { outer_borrow = true; outer_shared = true }
+
+(* TODO: we need to factorize print functions for strings *)
+let ids_reprs_to_string (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
+ let bindings = V.BorrowId.Map.bindings reprs in
+ let bindings =
+ List.map
+ (fun (id, repr_id) ->
+ V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id)
+ bindings
+ in
+ String.concat "\n" bindings
+
let borrows_infos_to_string (infos : borrow_info V.BorrowId.Map.t) : string =
let bindings = V.BorrowId.Map.bindings infos in
let bindings = List.map (fun (_, info) -> show_borrow_info info) bindings in
@@ -108,11 +127,11 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
object
inherit [_] C.iter_eval_ctx as super
- method! visit_Var _inside_abs binder v =
+ method! visit_Var _ binder v =
let inside_abs = false in
super#visit_Var inside_abs binder v
- method! visit_Abs _inside_abs abs =
+ method! visit_Abs _ abs =
let inside_abs = true in
super#visit_Abs inside_abs abs
@@ -120,7 +139,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
(* Register the loan *)
let _ =
match lc with
- | V.SharedLoan (bids, _tv) -> register_shared_loan inside_abs bids
+ | V.SharedLoan (bids, _) -> register_shared_loan inside_abs bids
| V.MutLoan bid -> register_mut_loan inside_abs bid
in
(* Continue exploring *)
@@ -152,10 +171,23 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
(* Some utilities to register the borrows *)
let find_info (bid : V.BorrowId.id) : borrow_info =
(* Find the representant *)
- let repr_bid = V.BorrowId.Map.find bid !ids_reprs in
- (* Lookup the info *)
- V.BorrowId.Map.find repr_bid !borrows_infos
+ match V.BorrowId.Map.find_opt bid !ids_reprs with
+ | Some repr_bid ->
+ (* Lookup the info *)
+ V.BorrowId.Map.find repr_bid !borrows_infos
+ | None ->
+ let err =
+ "find_info: could not find the representant of borrow "
+ ^ V.BorrowId.to_string bid ^ "\n" ^ "\n- Context:\n"
+ ^ eval_ctx_to_string ctx ^ "\n- representants:\n"
+ ^ ids_reprs_to_string !ids_reprs
+ ^ "\n- info:\n"
+ ^ borrows_infos_to_string !borrows_infos
+ in
+ L.log#serror err;
+ failwith err
in
+
let update_info (bid : V.BorrowId.id) (info : borrow_info) : unit =
(* Find the representant *)
let repr_bid = V.BorrowId.Map.find bid !ids_reprs in
@@ -233,7 +265,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
("\nAbout to check context invariant:\n" ^ eval_ctx_to_string ctx ^ "\n"));
L.log#ldebug
(lazy
- ("Borrows information:\n"
+ ("\nBorrows information:\n"
^ borrows_infos_to_string !borrows_infos
^ "\n")));
@@ -254,9 +286,293 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
- borrows/loans can't contain ⊥ or inactivated 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 : C.eval_ctx) : unit =
+ let visitor =
+ object
+ inherit [_] C.iter_eval_ctx as super
+
+ method! visit_Bottom info =
+ (* No ⊥ inside borrowed values *)
+ assert (not info.outer_borrow)
+
+ method! visit_ABottom _info =
+ (* ⊥ inside an abstraction is not the same as in a regular value *)
+ ()
+
+ method! visit_loan_content info lc =
+ (* Update the info *)
+ let info =
+ match lc with
+ | V.SharedLoan (_, _) -> set_outer_shared info
+ | V.MutLoan _ ->
+ (* No mutable loan inside a shared loan *)
+ assert (not info.outer_shared);
+ set_outer_mut info
+ in
+ (* Continue exploring *)
+ super#visit_loan_content info lc
+
+ method! visit_borrow_content info bc =
+ (* Update the info *)
+ let info =
+ match bc with
+ | V.SharedBorrow _ -> set_outer_shared info
+ | V.InactivatedMutBorrow _ ->
+ assert (not info.outer_borrow);
+ set_outer_shared info
+ | V.MutBorrow (_, _) -> set_outer_mut info
+ in
+ (* Continue exploring *)
+ super#visit_borrow_content info bc
-let check_typing_invariant (_ctx : C.eval_ctx) : unit = ()
+ method! visit_aloan_content info lc =
+ (* 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 = _ } -> set_outer_mut info
+ | V.AEndedSharedLoan (_, _) -> set_outer_shared info
+ | V.AIgnoredMutLoan (_, _) -> set_outer_mut info
+ | V.AEndedIgnoredMutLoan { given_back = _; child = _ } ->
+ set_outer_mut info
+ | V.AIgnoredSharedLoan _ -> set_outer_shared info
+ in
+ (* Continue exploring *)
+ super#visit_aloan_content info lc
+
+ method! visit_aborrow_content info bc =
+ (* Update the info *)
+ let info =
+ match bc with
+ | V.AMutBorrow (_, _) -> set_outer_mut info
+ | V.ASharedBorrow _ -> set_outer_shared info
+ | V.AIgnoredMutBorrow _ -> set_outer_mut info
+ | V.AProjSharedBorrow _ -> set_outer_shared info
+ in
+ (* Continue exploring *)
+ super#visit_aborrow_content info bc
+ end
+ in
+
+ (* Explore *)
+ let info = { outer_borrow = false; outer_shared = false } in
+ visitor#visit_eval_ctx info ctx
+
+let check_constant_value_type (cv : V.constant_value) (ty : T.ety) : unit =
+ match (cv, ty) with
+ | V.Scalar sv, T.Integer int_ty -> assert (sv.int_ty = int_ty)
+ | V.Bool _, T.Bool | V.Char _, T.Char | V.String _, T.Str -> ()
+ | _ -> failwith "Erroneous typing"
+
+let check_typing_invariant (ctx : C.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
+ * places.
+ * *)
+ let aloan_get_expected_child_type (ty : 'r T.ty) : 'r T.ty =
+ let _, ty, _ = ty_get_ref ty in
+ ty
+ in
+
+ let visitor =
+ object
+ inherit [_] C.iter_eval_ctx as super
+
+ method! visit_typed_value info tv =
+ (* Check the current pair (value, type) *)
+ (match (tv.V.value, tv.V.ty) with
+ | V.Concrete cv, ty -> check_constant_value_type cv ty
+ (* ADT case *)
+ | V.Adt av, T.Adt (T.AdtId def_id, regions, tys) ->
+ (* Retrieve the definition to check the variant id, the number of
+ * parameters, etc. *)
+ let def = C.ctx_lookup_type_def ctx def_id in
+ (* Check the number of parameters *)
+ assert (List.length regions = List.length def.region_params);
+ assert (List.length tys = List.length def.type_params);
+ (* 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 _ -> ()
+ | _ -> failwith "Erroneous typing");
+ (* Check that the field types are correct *)
+ let field_types =
+ Subst.type_def_get_instantiated_field_etypes def av.V.variant_id
+ tys
+ in
+ let fields_with_types =
+ List.combine av.V.field_values field_types
+ in
+ List.iter
+ (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty))
+ fields_with_types
+ (* Tuple case *)
+ | V.Adt av, T.Adt (T.Tuple, regions, tys) ->
+ assert (regions = []);
+ assert (av.V.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 tys in
+ List.iter
+ (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty))
+ fields_with_types
+ (* Assumed type case *)
+ | V.Adt av, T.Adt (T.Assumed aty_id, regions, tys) -> (
+ assert (av.V.variant_id = None);
+ match (aty_id, av.V.field_values, regions, tys) with
+ (* Box *)
+ | T.Box, [ boxed_value ], [], [ boxed_ty ] ->
+ assert (boxed_value.V.ty = boxed_ty)
+ | _ -> failwith "Erroneous type")
+ | V.Bottom, _ -> (* Nothing to check *) ()
+ | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
+ match (bc, rkind) with
+ | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut
+ -> (
+ (* 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)
+ | _ -> failwith "Inconsistent context")
+ | V.MutBorrow (_, bv), T.Mut ->
+ assert (
+ (* Check that the borrowed value has the proper type *)
+ bv.V.ty = ref_ty)
+ | _ -> failwith "Erroneous typing")
+ | V.Loan lc, ty -> (
+ match lc with
+ | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
+ | V.MutLoan 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)
+ | _ -> failwith "Inconsistent context"))
+ | V.Symbolic sv, ty ->
+ let ty' = Subst.erase_regions sv.V.sv_ty in
+ assert (ty' = ty)
+ | _ -> failwith "Erroneous typing");
+ (* Continue exploring to inspect the subterms *)
+ super#visit_typed_value info tv
+
+ method! visit_typed_avalue info atv =
+ (* Check the current pair (value, type) *)
+ (match (atv.V.value, atv.V.ty) with
+ | V.AConcrete cv, ty ->
+ check_constant_value_type cv (Subst.erase_regions ty)
+ (* ADT case *)
+ | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) ->
+ (* Retrieve the definition to check the variant id, the number of
+ * parameters, etc. *)
+ let def = C.ctx_lookup_type_def ctx def_id in
+ (* Check the number of parameters *)
+ assert (List.length regions = List.length def.region_params);
+ assert (List.length tys = List.length def.type_params);
+ (* 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 _ -> ()
+ | _ -> failwith "Erroneous typing");
+ (* Check that the field types are correct *)
+ let field_types =
+ Subst.type_def_get_instantiated_field_rtypes def av.V.variant_id
+ regions tys
+ in
+ let fields_with_types =
+ List.combine av.V.field_values field_types
+ in
+ List.iter
+ (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty))
+ fields_with_types
+ (* Tuple case *)
+ | V.AAdt av, T.Adt (T.Tuple, regions, tys) ->
+ assert (regions = []);
+ assert (av.V.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 tys in
+ List.iter
+ (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty))
+ fields_with_types
+ (* Assumed type case *)
+ | V.AAdt av, T.Adt (T.Assumed aty_id, regions, tys) -> (
+ assert (av.V.variant_id = None);
+ match (aty_id, av.V.field_values, regions, tys) with
+ (* Box *)
+ | T.Box, [ boxed_value ], [], [ boxed_ty ] ->
+ assert (boxed_value.V.ty = boxed_ty)
+ | _ -> failwith "Erroneous type")
+ | V.ABottom, _ -> (* Nothing to check *) ()
+ | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
+ match (bc, rkind) with
+ | V.AMutBorrow (_, av), T.Mut ->
+ (* Check that the child value has the proper type *)
+ assert (av.V.ty = ref_ty)
+ | V.ASharedBorrow bid, T.Shared -> (
+ (* 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)
+ | _ -> failwith "Inconsistent context")
+ | V.AIgnoredMutBorrow av, T.Mut -> assert (av.V.ty = ref_ty)
+ | V.AProjSharedBorrow _, T.Shared -> ()
+ | _ -> failwith "Inconsistent context")
+ | V.ALoan lc, aty -> (
+ match lc with
+ | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av)
+ -> (
+ let borrowed_aty = aloan_get_expected_child_type aty in
+ assert (child_av.V.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)) ->
+ assert (
+ Subst.erase_regions sv.V.ty
+ = Subst.erase_regions borrowed_aty)
+ | _ -> failwith "Inconsistent context")
+ | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
+ ->
+ let borrowed_aty = aloan_get_expected_child_type aty in
+ assert (sv.V.ty = Subst.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 }
+ | V.AEndedIgnoredMutLoan { given_back; child } ->
+ 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
+ let ty2 =
+ match aproj with
+ | V.AProjLoans sv | V.AProjBorrows (sv, _) ->
+ Subst.erase_regions sv.V.sv_ty
+ in
+ assert (ty1 = ty2)
+ | _ -> failwith "Erroneous typing");
+ (* Continue exploring to inspect the subterms *)
+ super#visit_typed_avalue info atv
+ (** TODO: there is a lot of duplication with [visit_typed_value]... *)
+ end
+ in
+ visitor#visit_eval_ctx () ctx
let check_invariants (ctx : C.eval_ctx) : unit =
check_loans_borrows_relation_invariant ctx;