Skip to content

Commit d3acb55

Browse files
danielsndanielsn
authored
Zero init for common types (#1520)
1 parent 334ca6d commit d3acb55

File tree

5 files changed

+102
-7
lines changed

5 files changed

+102
-7
lines changed

‎cprover_bindings/src/goto_program/expr.rs‎

Lines changed: 27 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,8 @@ pub enum ExprValue {
8484
Dereference(Expr),
8585
/// `1.0`
8686
DoubleConstant(f64),
87+
// {}
88+
EmptyUnion,
8789
/// `1.0f`
8890
FloatConstant(f32),
8991
/// `function(arguments)`
@@ -542,6 +544,13 @@ impl Expr {
542544
Self::double_constant(c)
543545
}
544546

547+
pub fn empty_union(typ: Type, st: &SymbolTable) -> Self {
548+
assert!(typ.is_union() || typ.is_union_tag());
549+
assert!(typ.lookup_components(st).unwrap().is_empty());
550+
let typ = typ.aggr_tag().unwrap();
551+
expr!(EmptyUnion, typ)
552+
}
553+
545554
/// `1.0f`
546555
pub fn float_constant(c: f32) -> Self {
547556
expr!(FloatConstant(c), Type::float())
@@ -553,6 +562,18 @@ impl Expr {
553562
Self::float_constant(c)
554563
}
555564

565+
/// `typ x[__CPROVER_infinity()] = >>> {elem} <<<`
566+
/// i.e. initilize an infinite sized sparse array.
567+
/// This is useful for maps:
568+
/// ```
569+
/// bool x[__CPROVER_infinity()] = {false};
570+
/// x[idx_1] = true;
571+
/// if (x[idx_2]) { ... }
572+
/// ```
573+
pub fn infinite_array_constant(self) -> Self {
574+
expr!(ArrayOf { elem: self }, self.typ.clone().infinite_array_of())
575+
}
576+
556577
/// `self[index]`
557578
pub fn index_array(self, index: Expr) -> Self {
558579
assert!(index.typ.is_integer());
@@ -566,7 +587,7 @@ impl Expr {
566587
where
567588
T: Into<BigInt>,
568589
{
569-
assert!(typ.is_integer());
590+
assert!(typ.is_integer() || typ.is_bitfield());
570591
let i = i.into();
571592
// TODO: <https://github.com/model-checking/kani/issues/996>
572593
// if i != 0 && i != 1 {
@@ -806,11 +827,12 @@ impl Expr {
806827
symbol_table: &SymbolTable,
807828
) -> Self {
808829
assert!(
809-
typ.is_struct_tag(),
810-
"Error in struct_expr; must be given struct_tag.\n\t{:?}\n\t{:?}",
830+
typ.is_struct_tag() || typ.is_struct(),
831+
"Error in struct_expr; must be given struct.\n\t{:?}\n\t{:?}",
811832
typ,
812833
values
813834
);
835+
let typ = typ.aggr_tag().unwrap();
814836
let fields = typ.lookup_components(symbol_table).unwrap();
815837
assert_eq!(
816838
fields.len(),
@@ -869,8 +891,9 @@ impl Expr {
869891
symbol_table: &SymbolTable,
870892
) -> Self {
871893
let field = field.into();
872-
assert!(typ.is_union_tag());
894+
assert!(typ.is_union_tag() || typ.is_union());
873895
assert_eq!(typ.lookup_field_type(field, symbol_table).as_ref(), Some(value.typ()));
896+
let typ = typ.aggr_tag().unwrap();
874897
expr!(Union { value, field }, typ)
875898
}
876899
}

‎cprover_bindings/src/goto_program/symtab_transformer/transformer.rs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -258,6 +258,7 @@ pub trait Transformer: Sized {
258258
ExprValue::CBoolConstant(value) => self.transform_expr_c_bool_constant(typ, value),
259259
ExprValue::Dereference(child) => self.transform_expr_dereference(typ, child),
260260
ExprValue::DoubleConstant(value) => self.transform_expr_double_constant(typ, value),
261+
ExprValue::EmptyUnion => self.transform_expr_empty_union(typ),
261262
ExprValue::FloatConstant(value) => self.transform_expr_float_constant(typ, value),
262263
ExprValue::FunctionCall { function, arguments } => {
263264
self.transform_expr_function_call(typ, function, arguments)
@@ -361,6 +362,11 @@ pub trait Transformer: Sized {
361362
Expr::double_constant(*value)
362363
}
363364

365+
/// Transforms an empty union expr (`{}`)
366+
fn transform_expr_empty_union(&mut self, typ: &Type) -> Expr {
367+
Expr::empty_union(typ.clone(), self.symbol_table())
368+
}
369+
364370
/// Transforms a float constant expr (`1.0f`)
365371
fn transform_expr_float_constant(&mut self, _typ: &Type, value: &f32) -> Expr {
366372
Expr::float_constant(*value)

‎cprover_bindings/src/goto_program/typ.rs‎

Lines changed: 66 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -418,6 +418,11 @@ impl Type {
418418
}
419419
}
420420

421+
pub fn is_bitfield(&self) -> bool {
422+
let concrete = self.unwrap_typedef();
423+
matches!(concrete, CBitField { .. })
424+
}
425+
421426
pub fn is_bool(&self) -> bool {
422427
let concrete = self.unwrap_typedef();
423428
match concrete {
@@ -1211,7 +1216,7 @@ impl Type {
12111216
}
12121217

12131218
pub fn one(&self) -> Expr {
1214-
if self.is_integer() {
1219+
if self.is_integer() || self.is_bitfield() {
12151220
Expr::int_constant(1, self.clone())
12161221
} else if self.is_c_bool() {
12171222
Expr::c_true()
@@ -1225,8 +1230,10 @@ impl Type {
12251230
}
12261231

12271232
pub fn zero(&self) -> Expr {
1228-
if self.is_integer() {
1233+
if self.is_integer() || self.is_bitfield() {
12291234
Expr::int_constant(0, self.clone())
1235+
} else if self.is_bool() {
1236+
Expr::bool_false()
12301237
} else if self.is_c_bool() {
12311238
Expr::c_false()
12321239
} else if self.is_float() {
@@ -1236,7 +1243,63 @@ impl Type {
12361243
} else if self.is_pointer() {
12371244
Expr::pointer_constant(0, self.clone())
12381245
} else {
1239-
unreachable!("Can't convert {:?} to a one value", self);
1246+
unreachable!("Can't convert {:?} to a zero value", self);
1247+
}
1248+
}
1249+
1250+
pub fn zero_initializer(&self, st: &SymbolTable) -> Expr {
1251+
let concrete = self.unwrap_typedef();
1252+
match concrete {
1253+
// Base case
1254+
Bool
1255+
| CBitField { .. }
1256+
| CInteger(_)
1257+
| Double
1258+
| Float
1259+
| Pointer { .. }
1260+
| Signedbv { .. }
1261+
| Unsignedbv { .. } => self.zero(),
1262+
1263+
// Recursive cases
1264+
Array { typ, size } => typ.zero_initializer(st).array_constant(*size),
1265+
InfiniteArray { typ } => typ.zero_initializer(st).infinite_array_constant(),
1266+
Struct { components, .. } => {
1267+
let values: Vec<Expr> =
1268+
components.iter().map(|c| c.typ().zero_initializer(st)).collect();
1269+
Expr::struct_expr_from_padded_values(self.clone(), values, st)
1270+
}
1271+
StructTag(tag) => st.lookup(*tag).unwrap().typ.zero_initializer(st),
1272+
TypeDef { .. } => unreachable!("Should have been normalized away"),
1273+
Union { components, .. } => {
1274+
if components.is_empty() {
1275+
Expr::empty_union(self.clone(), st)
1276+
} else {
1277+
let largest = components.iter().max_by_key(|c| c.sizeof_in_bits(st)).unwrap();
1278+
Expr::union_expr(
1279+
self.clone(),
1280+
largest.name(),
1281+
largest.typ().zero_initializer(st),
1282+
st,
1283+
)
1284+
}
1285+
}
1286+
UnionTag(tag) => st.lookup(*tag).unwrap().typ.zero_initializer(st),
1287+
Vector { typ, size } => {
1288+
let zero = typ.zero_initializer(st);
1289+
let size = (*size).try_into().unwrap();
1290+
let elems = vec![zero; size];
1291+
Expr::vector_expr(self.clone(), elems)
1292+
}
1293+
1294+
// Cases that can't be zero init
1295+
// Note that other than flexible array, none of these can be fields in a struct or union
1296+
Code { .. }
1297+
| Constructor
1298+
| Empty
1299+
| FlexibleArray { .. }
1300+
| IncompleteStruct { .. }
1301+
| IncompleteUnion { .. }
1302+
| VariadicCode { .. } => panic!("Can't zero init {:?}", self),
12401303
}
12411304
}
12421305
}

‎cprover_bindings/src/irep/irep_id.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -582,6 +582,7 @@ pub enum IrepId {
582582
Popcount,
583583
CountLeadingZeros,
584584
CountTrailingZeros,
585+
EmptyUnion,
585586
FunctionType,
586587
Noreturn,
587588
CNoreturn,
@@ -1444,6 +1445,7 @@ impl ToString for IrepId {
14441445
IrepId::Popcount => "popcount",
14451446
IrepId::CountLeadingZeros => "count_leading_zeros",
14461447
IrepId::CountTrailingZeros => "count_trailing_zeros",
1448+
IrepId::EmptyUnion => "empty_union",
14471449
IrepId::FunctionType => "function_type",
14481450
IrepId::Noreturn => "noreturn",
14491451
IrepId::CNoreturn => "#noreturn",

‎cprover_bindings/src/irep/to_irep.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -219,6 +219,7 @@ impl ToIrep for ExprValue {
219219
)],
220220
}
221221
}
222+
ExprValue::EmptyUnion => Irep::just_id(IrepId::EmptyUnion),
222223
ExprValue::FloatConstant(i) => {
223224
let c: u32 = i.to_bits();
224225
Irep {

0 commit comments

Comments
 (0)