From 3124621776369ef1f344acfde61338a412833119 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Oct 2018 13:48:55 +0000 Subject: [PATCH] Evaluating sizeof over __CPROVER_bool requires special cases __CPROVER_bool is just a single bit, and not part of any language standard describing the semantics of sizeof. We can declare arrays of __CPROVER_bool, which will thus have elements that are not aligned on byte boundaries. Using sizeof with such an array thus requires specific handling. --- regression/ansi-c/cprover_bool1/main.c | 46 +++++++++++++++++++++ regression/ansi-c/cprover_bool1/test.desc | 8 ++++ src/ansi-c/c_typecheck_expr.cpp | 13 ++++++ src/ansi-c/padding.cpp | 20 +++++++++ src/util/pointer_offset_size.cpp | 50 +++++++++++++++++++++-- src/util/simplify_expr.cpp | 4 +- src/util/simplify_expr_struct.cpp | 6 ++- 7 files changed, 141 insertions(+), 6 deletions(-) create mode 100644 regression/ansi-c/cprover_bool1/main.c create mode 100644 regression/ansi-c/cprover_bool1/test.desc diff --git a/regression/ansi-c/cprover_bool1/main.c b/regression/ansi-c/cprover_bool1/main.c new file mode 100644 index 00000000000..fc504662a69 --- /dev/null +++ b/regression/ansi-c/cprover_bool1/main.c @@ -0,0 +1,46 @@ +#define STATIC_ASSERT(condition) int some_array##__LINE__[(condition) ? 1 : -1] + +struct bits +{ + __CPROVER_bool b1; + __CPROVER_bool b2; + __CPROVER_bool b3; + __CPROVER_bool b4; + __CPROVER_bool b5; + __CPROVER_bool b6; + __CPROVER_bool b7; + __CPROVER_bool b8; + int i; +}; + +STATIC_ASSERT(sizeof(struct bits) == 2 * sizeof(int)); + +#include + +#if CHAR_BIT >= 8 +#pragma pack(1) +struct packed_bits +{ + __CPROVER_bool b1; + __CPROVER_bool b2; + __CPROVER_bool b3; + __CPROVER_bool b4; + __CPROVER_bool b5; + __CPROVER_bool b6; + __CPROVER_bool b7; + __CPROVER_bool b8; + int i; +}; +#pragma pack() + +STATIC_ASSERT(sizeof(struct packed_bits) == sizeof(int) + 1); +#endif + +// a _Bool is at least one byte wide +STATIC_ASSERT(sizeof(_Bool[CHAR_BIT]) >= CHAR_BIT); +// __CPROVER_bool is just a single bit +STATIC_ASSERT(sizeof(__CPROVER_bool[CHAR_BIT]) == 1); + +int main() +{ +} diff --git a/regression/ansi-c/cprover_bool1/test.desc b/regression/ansi-c/cprover_bool1/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/cprover_bool1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index ad7e82b721d..cf627c8d9c5 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -985,6 +985,12 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr) error() << "sizeof cannot be applied to bit fields" << eom; throw 0; } + else if(type.id() == ID_bool) + { + err_location(expr); + error() << "sizeof cannot be applied to single bits" << eom; + throw 0; + } else if(type.id() == ID_empty) { // This is a gcc extension. @@ -1740,6 +1746,13 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr) throw 0; } + if(op.type().id() == ID_bool) + { + err_location(expr); + error() << "cannot take address of a single bit" << eom; + throw 0; + } + // special case: address of label if(op.id()==ID_label) { diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index a3adef091c6..d0180334e50 100644 --- a/src/ansi-c/padding.cpp +++ b/src/ansi-c/padding.cpp @@ -226,6 +226,10 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns) const auto width = to_c_bit_field_type(it->type()).get_width(); bit_field_bits += width; } + else if(it->type().id() == ID_bool) + { + ++bit_field_bits; + } else { // keep track of offset @@ -281,6 +285,10 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns) const std::size_t width = to_c_bit_field_type(it->type()).get_width(); bit_field_bits+=width; } + else if(it->type().id() == ID_bool) + { + ++bit_field_bits; + } else if(bit_field_bits!=0) { // not on a byte-boundary? @@ -347,6 +355,18 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns) continue; } } + else if(it_type.id() == ID_bool) + { + a = alignment(it_type, ns); + if(max_alignment < a) + max_alignment = a; + + ++bit_field_bits; + const std::size_t bytes = bit_field_bits / config.ansi_c.char_width; + bit_field_bits %= config.ansi_c.char_width; + offset += bytes; + continue; + } else a=alignment(it_type, ns); diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 8878776a884..653ab08812f 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -42,6 +42,12 @@ member_offset_iterator &member_offset_iterator::operator++() current.second += bit_field_bits / 8; bit_field_bits %= 8; } + else if(comp.type().id() == ID_bool) + { + ++bit_field_bits; + current.second += bit_field_bits / 8; + bit_field_bits %= 8; + } else { DATA_INVARIANT( @@ -288,7 +294,16 @@ exprt member_offset_expr( bit_field_bits += w; const std::size_t bytes = bit_field_bits / 8; bit_field_bits %= 8; - result=plus_exprt(result, from_integer(bytes, result.type())); + if(bytes > 0) + result = plus_exprt(result, from_integer(bytes, result.type())); + } + else if(c.type().id() == ID_bool) + { + ++bit_field_bits; + const std::size_t bytes = bit_field_bits / 8; + bit_field_bits %= 8; + if(bytes > 0) + result = plus_exprt(result, from_integer(bytes, result.type())); } else { @@ -315,6 +330,15 @@ exprt size_of_expr( { const auto &array_type = to_array_type(type); + // special-case arrays of bits + if(array_type.subtype().id() == ID_bool) + { + auto bits = pointer_offset_bits(array_type, ns); + + if(bits.has_value()) + return from_integer((*bits + 7) / 8, size_type()); + } + exprt sub = size_of_expr(array_type.subtype(), ns); if(sub.is_nil()) return nil_exprt(); @@ -335,7 +359,18 @@ exprt size_of_expr( } else if(type.id()==ID_vector) { - exprt sub = size_of_expr(to_vector_type(type).subtype(), ns); + const auto &vector_type = to_vector_type(type); + + // special-case vectors of bits + if(vector_type.subtype().id() == ID_bool) + { + auto bits = pointer_offset_bits(vector_type, ns); + + if(bits.has_value()) + return from_integer((*bits + 7) / 8, size_type()); + } + + exprt sub = size_of_expr(vector_type.subtype(), ns); if(sub.is_nil()) return nil_exprt(); @@ -381,7 +416,16 @@ exprt size_of_expr( bit_field_bits += w; const std::size_t bytes = bit_field_bits / 8; bit_field_bits %= 8; - result=plus_exprt(result, from_integer(bytes, result.type())); + if(bytes > 0) + result = plus_exprt(result, from_integer(bytes, result.type())); + } + else if(c.type().id() == ID_bool) + { + ++bit_field_bits; + const std::size_t bytes = bit_field_bits / 8; + bit_field_bits %= 8; + if(bytes > 0) + result = plus_exprt(result, from_integer(bytes, result.type())); } else { diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 43cf28c87a2..60b0bfdcb5b 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1947,10 +1947,10 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) { const struct_typet &struct_type=to_struct_type(tp); const irep_idt &component_name=with.where().get(ID_component_name); + const typet &c_type = struct_type.get_component(component_name).type(); // is this a bit field? - if(struct_type.get_component(component_name).type().id()== - ID_c_bit_field) + if(c_type.id() == ID_c_bit_field || c_type.id() == ID_bool) { // don't touch -- might not be byte-aligned } diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index cb0b6eb5242..7c9ae292896 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -152,8 +152,12 @@ bool simplify_exprt::simplify_member(exprt &expr) const struct_typet::componentt &component= struct_type.get_component(component_name); - if(component.is_nil() || component.type().id()==ID_c_bit_field) + if( + component.is_nil() || component.type().id() == ID_c_bit_field || + component.type().id() == ID_bool) + { return true; + } // add member offset to index auto offset_int = member_offset(struct_type, component_name, ns);