Skip to content

Commit ae2de35

Browse files
danielsndanielsn
authored
Better type checks for compound types (rust-lang#1245)
* Better type checking for compound types * Add checks for datatype fields.
1 parent 20da325 commit ae2de35

File tree

3 files changed

+114
-33
lines changed

3 files changed

+114
-33
lines changed

‎cprover_bindings/src/goto_program/typ.rs

Lines changed: 96 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -152,9 +152,46 @@ impl DatatypeComponent {
152152
}
153153
}
154154

155-
//Constructors
155+
/// Constructors
156156
impl DatatypeComponent {
157+
fn typecheck_datatype_field(typ: &Type) -> bool {
158+
match typ.unwrap_typedef() {
159+
Array { .. }
160+
| Bool
161+
| CBitField { .. }
162+
| CInteger(_)
163+
| Double
164+
| FlexibleArray { .. }
165+
| Float
166+
| Pointer { .. }
167+
| Signedbv { .. }
168+
| Struct { .. }
169+
| StructTag(_)
170+
| Union { .. }
171+
| UnionTag(_)
172+
| Unsignedbv { .. }
173+
| Vector { .. } => true,
174+
175+
Code { .. }
176+
| Constructor
177+
| Empty
178+
| IncompleteStruct { .. }
179+
| IncompleteUnion { .. }
180+
| InfiniteArray { .. }
181+
| VariadicCode { .. } => false,
182+
183+
TypeDef { .. } => unreachable!("typedefs should have been unwrapped"),
184+
}
185+
}
186+
157187
pub fn field<T: Into<InternedString>>(name: T, typ: Type) -> Self {
188+
// TODO https://github.com/model-checking/kani/issues/1243
189+
// assert!(
190+
// Self::typecheck_datatype_field(&typ),
191+
// "Illegal field.\n\tName: {}\n\tType: {:?}",
192+
// name.into(),
193+
// typ
194+
// );
158195
let name = name.into();
159196
Field { name, typ }
160197
}
@@ -831,12 +868,43 @@ impl Type {
831868

832869
/// Constructors
833870
impl Type {
871+
fn typecheck_array_elem(&self) -> bool {
872+
match self.unwrap_typedef() {
873+
Array { .. }
874+
| Bool
875+
| CBitField { .. }
876+
| CInteger(_)
877+
| Double
878+
| Float
879+
| Pointer { .. }
880+
| Signedbv { .. }
881+
| Struct { .. }
882+
| StructTag(_)
883+
| Union { .. }
884+
| UnionTag(_)
885+
| Unsignedbv { .. }
886+
| Vector { .. } => true,
887+
888+
Code { .. }
889+
| Constructor
890+
| Empty
891+
| FlexibleArray { .. }
892+
| IncompleteStruct { .. }
893+
| IncompleteUnion { .. }
894+
| InfiniteArray { .. }
895+
| VariadicCode { .. } => false,
896+
897+
TypeDef { .. } => unreachable!("typedefs should have been unwrapped"),
898+
}
899+
}
900+
834901
/// elem_t[size]
835902
pub fn array_of<T>(self, size: T) -> Self
836903
where
837904
T: TryInto<u64>,
838905
T::Error: Debug,
839906
{
907+
assert!(self.typecheck_array_elem(), "Can't make array of type {:?}", self);
840908
let size: u64 = size.try_into().unwrap();
841909
Array { typ: Box::new(self), size }
842910
}
@@ -908,19 +976,6 @@ impl Type {
908976
Constructor
909977
}
910978

911-
/// A component of a datatype (e.g. a field of a struct or union)
912-
pub fn datatype_component<T: Into<InternedString>>(name: T, typ: Type) -> DatatypeComponent {
913-
let name = name.into();
914-
Field { name, typ }
915-
}
916-
917-
// `__CPROVER_bitvector[bits] $pad<n>`
918-
pub fn datatype_padding<T: Into<InternedString>>(name: T, bits: u64) -> DatatypeComponent {
919-
let name = name.into();
920-
921-
Padding { name, bits }
922-
}
923-
924979
pub fn double() -> Self {
925980
Double
926981
}
@@ -965,6 +1020,7 @@ impl Type {
9651020
}
9661021

9671022
pub fn infinite_array_of(self) -> Self {
1023+
assert!(self.typecheck_array_elem(), "Can't make infinite array of type {:?}", self);
9681024
InfiniteArray { typ: Box::new(self) }
9691025
}
9701026

@@ -1013,13 +1069,27 @@ impl Type {
10131069
StructTag(name)
10141070
}
10151071

1016-
pub fn components_are_unique(components: &[DatatypeComponent]) -> bool {
1072+
fn components_are_unique(components: &[DatatypeComponent]) -> bool {
10171073
let mut names: Vec<_> = components.iter().map(|x| x.name()).collect();
10181074
names.sort();
10191075
names.dedup();
10201076
names.len() == components.len()
10211077
}
10221078

1079+
fn components_are_not_flexible_array(components: &[DatatypeComponent]) -> bool {
1080+
components.iter().all(|x| !x.typ().is_flexible_array())
1081+
}
1082+
1083+
/// A struct can only contain a flexible array as its last element
1084+
/// Check this
1085+
fn components_in_valid_order_for_struct(components: &[DatatypeComponent]) -> bool {
1086+
if let Some((_, cs)) = components.split_last() {
1087+
Type::components_are_not_flexible_array(cs)
1088+
} else {
1089+
true
1090+
}
1091+
}
1092+
10231093
/// struct name {
10241094
/// f1.typ f1.data; ...
10251095
/// }
@@ -1032,6 +1102,12 @@ impl Type {
10321102
"Components contain duplicates: {:?}",
10331103
components
10341104
);
1105+
assert!(
1106+
Type::components_in_valid_order_for_struct(&components),
1107+
"Components are not in valid order for struct: {:?}",
1108+
components
1109+
);
1110+
10351111
let tag = tag.into();
10361112
Struct { tag, components }
10371113
}
@@ -1061,6 +1137,11 @@ impl Type {
10611137
"Components contain duplicates: {:?}",
10621138
components
10631139
);
1140+
assert!(
1141+
Type::components_are_not_flexible_array(&components),
1142+
"Unions cannot contain flexible arrays: {:?}",
1143+
components
1144+
);
10641145
Union { tag, components }
10651146
}
10661147

‎kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
44
use crate::codegen_cprover_gotoc::GotocCtx;
55
use crate::unwrap_or_return_codegen_unimplemented;
6-
use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
6+
use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, Type};
77
use cbmc::NO_PRETTY_NAME;
88
use rustc_ast::ast::Mutability;
99
use rustc_middle::mir::interpret::{
@@ -503,12 +503,12 @@ impl<'tcx> GotocCtx<'tcx> {
503503
.iter()
504504
.enumerate()
505505
.map(|(i, d)| match d {
506-
AllocData::Bytes(bytes) => Type::datatype_component(
506+
AllocData::Bytes(bytes) => DatatypeComponent::field(
507507
&i.to_string(),
508508
Type::unsigned_int(8).array_of(bytes.len()),
509509
),
510510
AllocData::Expr(e) => {
511-
Type::datatype_component(&i.to_string(), e.typ().clone())
511+
DatatypeComponent::field(&i.to_string(), e.typ().clone())
512512
}
513513
})
514514
.collect()

‎kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -308,7 +308,7 @@ impl<'tcx> GotocCtx<'tcx> {
308308
// vtable field name, i.e., 3_vol (idx_method)
309309
let vtable_field_name = self.vtable_field_name(instance.def_id(), idx);
310310

311-
Type::datatype_component(vtable_field_name, fn_ptr)
311+
DatatypeComponent::field(vtable_field_name, fn_ptr)
312312
}
313313

314314
/// Generates a vtable that looks like this:
@@ -382,8 +382,8 @@ impl<'tcx> GotocCtx<'tcx> {
382382
// See the comment on codegen_ty_ref.
383383
let vtable_name = ctx.vtable_name(trait_type);
384384
vec![
385-
Type::datatype_component("data", data_type),
386-
Type::datatype_component("vtable", Type::struct_tag(vtable_name).to_pointer()),
385+
DatatypeComponent::field("data", data_type),
386+
DatatypeComponent::field("vtable", Type::struct_tag(vtable_name).to_pointer()),
387387
]
388388
})
389389
}
@@ -410,9 +410,9 @@ impl<'tcx> GotocCtx<'tcx> {
410410
/// `get_vtable`.
411411
fn trait_vtable_field_types(&mut self, t: ty::Ty<'tcx>) -> Vec<DatatypeComponent> {
412412
let mut vtable_base = vec![
413-
Type::datatype_component("drop", self.trait_vtable_drop_type(t)),
414-
Type::datatype_component("size", Type::size_t()),
415-
Type::datatype_component("align", Type::size_t()),
413+
DatatypeComponent::field("drop", self.trait_vtable_drop_type(t)),
414+
DatatypeComponent::field("size", Type::size_t()),
415+
DatatypeComponent::field("align", Type::size_t()),
416416
];
417417
if let ty::Dynamic(binder, _region) = t.kind() {
418418
// The virtual methods on the trait ref. Some auto traits have no methods.
@@ -589,7 +589,7 @@ impl<'tcx> GotocCtx<'tcx> {
589589
// we do not generate a struct with an array of units
590590
vec![]
591591
} else {
592-
vec![Type::datatype_component(
592+
vec![DatatypeComponent::field(
593593
&0usize.to_string(),
594594
ctx.codegen_ty_raw_array(ty),
595595
)]
@@ -692,7 +692,7 @@ impl<'tcx> GotocCtx<'tcx> {
692692
// We need to pad to the next offset
693693
let bits = next_offset - current_offset;
694694
let name = format!("$pad{}", idx);
695-
Some(Type::datatype_padding(&name, bits))
695+
Some(DatatypeComponent::padding(&name, bits))
696696
} else {
697697
None
698698
}
@@ -729,7 +729,7 @@ impl<'tcx> GotocCtx<'tcx> {
729729
final_fields.push(padding)
730730
}
731731
// we insert the actual field
732-
final_fields.push(Type::datatype_component(fld_name, self.codegen_ty(*fld_ty)));
732+
final_fields.push(DatatypeComponent::field(fld_name, self.codegen_ty(*fld_ty)));
733733
let layout = self.layout_of(*fld_ty);
734734
// we compute the overall offset of the end of the current struct
735735
offset = fld_offset + layout.size.bits();
@@ -839,8 +839,8 @@ impl<'tcx> GotocCtx<'tcx> {
839839
};
840840
self.ensure_struct(pointer_name, NO_PRETTY_NAME, |_, _| {
841841
vec![
842-
Type::datatype_component("data", element_type.to_pointer()),
843-
Type::datatype_component("len", Type::size_t()),
842+
DatatypeComponent::field("data", element_type.to_pointer()),
843+
DatatypeComponent::field("len", Type::size_t()),
844844
]
845845
})
846846
} else if self.use_vtable_fat_pointer(pointee_type) {
@@ -1016,7 +1016,7 @@ impl<'tcx> GotocCtx<'tcx> {
10161016
.fields
10171017
.iter()
10181018
.map(|f| {
1019-
Type::datatype_component(
1019+
DatatypeComponent::field(
10201020
&f.name.to_string(),
10211021
ctx.codegen_ty(f.ty(ctx.tcx, subst)),
10221022
)
@@ -1100,13 +1100,13 @@ impl<'tcx> GotocCtx<'tcx> {
11001100
let discr_offset = ctx.layout_of(discr_t).size.bits_usize();
11011101
let initial_offset =
11021102
ctx.variant_min_offset(variants).unwrap_or(discr_offset);
1103-
let mut fields = vec![Type::datatype_component("case", int)];
1103+
let mut fields = vec![DatatypeComponent::field("case", int)];
11041104
if let Some(padding) =
11051105
ctx.codegen_struct_padding(discr_offset, initial_offset, 0)
11061106
{
11071107
fields.push(padding);
11081108
}
1109-
fields.push(Type::datatype_component(
1109+
fields.push(DatatypeComponent::field(
11101110
"cases",
11111111
ctx.ensure_union(
11121112
&format!("{}-union", name.to_string()),
@@ -1256,7 +1256,7 @@ impl<'tcx> GotocCtx<'tcx> {
12561256
// Skip variant types that cannot be referenced.
12571257
None
12581258
} else {
1259-
Some(Type::datatype_component(
1259+
Some(DatatypeComponent::field(
12601260
&case.name.to_string(),
12611261
self.codegen_enum_case_struct(
12621262
name,

0 commit comments

Comments
 (0)