summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-04 22:38:25 +0100
committerSon Ho2022-01-04 22:38:25 +0100
commit84bd12c6d832f20529bbfa763ac1a2de3909d382 (patch)
tree4cfd9eaba4d68850d0cda71ece44263832fe10d2
parente70b541f6c3b6fb29f9807258cc88b4d88178f6a (diff)
Make good progress on visit_typed_value for check_typing_invariant
Diffstat (limited to '')
-rw-r--r--src/Invariants.ml59
1 files changed, 55 insertions, 4 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index e1ba0b22..03cafd60 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -346,14 +346,65 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
inherit [_] C.iter_eval_ctx as super
method! visit_typed_value info tv =
- (* Check this pair (value, type) *)
+ (* Check the current pair (value, type) *)
(match (tv.V.value, tv.V.ty) with
| V.Concrete cv, ty -> check_constant_value_type cv ty
- | V.Adt av, _ -> raise Unimplemented
+ (* 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 = T.TypeDefId.nth ctx.type_context 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, _ -> raise Unimplemented
+ | 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 *)
+ raise Unimplemented
+ | V.MutBorrow (_, bv), T.Mut -> assert (bv.V.ty = ref_ty)
+ | _ -> failwith "Erroneous typing")
| V.Loan lc, _ -> raise Unimplemented
- | V.Symbolic spc, _ -> raise Unimplemented
+ | V.Symbolic spc, ty ->
+ let ty' = Subst.erase_regions spc.V.svalue.V.sv_ty in
+ assert (ty' = ty)
| _ -> failwith "Erroneous typing");
(* Continue exploring to inspect the subterms *)
super#visit_typed_value info tv