Skip to content

Commit 7fd6f21

Browse files
tautschnigtautschnig
authored
Merge pull request #3183 from tautschnig/cprover_bool-sizeof
Evaluating sizeof over __CPROVER_bool requires special cases
2 parents f5b450f + 3124621 commit 7fd6f21

File tree

7 files changed

+141
-6
lines changed

7 files changed

+141
-6
lines changed

‎regression/ansi-c/cprover_bool1/main.c‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
#define STATIC_ASSERT(condition) int some_array##__LINE__[(condition) ? 1 : -1]
2+
3+
struct bits
4+
{
5+
__CPROVER_bool b1;
6+
__CPROVER_bool b2;
7+
__CPROVER_bool b3;
8+
__CPROVER_bool b4;
9+
__CPROVER_bool b5;
10+
__CPROVER_bool b6;
11+
__CPROVER_bool b7;
12+
__CPROVER_bool b8;
13+
int i;
14+
};
15+
16+
STATIC_ASSERT(sizeof(struct bits) == 2 * sizeof(int));
17+
18+
#include <limits.h>
19+
20+
#if CHAR_BIT >= 8
21+
#pragma pack(1)
22+
struct packed_bits
23+
{
24+
__CPROVER_bool b1;
25+
__CPROVER_bool b2;
26+
__CPROVER_bool b3;
27+
__CPROVER_bool b4;
28+
__CPROVER_bool b5;
29+
__CPROVER_bool b6;
30+
__CPROVER_bool b7;
31+
__CPROVER_bool b8;
32+
int i;
33+
};
34+
#pragma pack()
35+
36+
STATIC_ASSERT(sizeof(struct packed_bits) == sizeof(int) + 1);
37+
#endif
38+
39+
// a _Bool is at least one byte wide
40+
STATIC_ASSERT(sizeof(_Bool[CHAR_BIT]) >= CHAR_BIT);
41+
// __CPROVER_bool is just a single bit
42+
STATIC_ASSERT(sizeof(__CPROVER_bool[CHAR_BIT]) == 1);
43+
44+
int main()
45+
{
46+
}

‎regression/ansi-c/cprover_bool1/test.desc‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎src/ansi-c/c_typecheck_expr.cpp‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -985,6 +985,12 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
985985
error() << "sizeof cannot be applied to bit fields" << eom;
986986
throw 0;
987987
}
988+
else if(type.id() == ID_bool)
989+
{
990+
err_location(expr);
991+
error() << "sizeof cannot be applied to single bits" << eom;
992+
throw 0;
993+
}
988994
else if(type.id() == ID_empty)
989995
{
990996
// This is a gcc extension.
@@ -1740,6 +1746,13 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
17401746
throw 0;
17411747
}
17421748

1749+
if(op.type().id() == ID_bool)
1750+
{
1751+
err_location(expr);
1752+
error() << "cannot take address of a single bit" << eom;
1753+
throw 0;
1754+
}
1755+
17431756
// special case: address of label
17441757
if(op.id()==ID_label)
17451758
{

‎src/ansi-c/padding.cpp‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -226,6 +226,10 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
226226
const auto width = to_c_bit_field_type(it->type()).get_width();
227227
bit_field_bits += width;
228228
}
229+
else if(it->type().id() == ID_bool)
230+
{
231+
++bit_field_bits;
232+
}
229233
else
230234
{
231235
// keep track of offset
@@ -281,6 +285,10 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
281285
const std::size_t width = to_c_bit_field_type(it->type()).get_width();
282286
bit_field_bits+=width;
283287
}
288+
else if(it->type().id() == ID_bool)
289+
{
290+
++bit_field_bits;
291+
}
284292
else if(bit_field_bits!=0)
285293
{
286294
// not on a byte-boundary?
@@ -347,6 +355,18 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
347355
continue;
348356
}
349357
}
358+
else if(it_type.id() == ID_bool)
359+
{
360+
a = alignment(it_type, ns);
361+
if(max_alignment < a)
362+
max_alignment = a;
363+
364+
++bit_field_bits;
365+
const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
366+
bit_field_bits %= config.ansi_c.char_width;
367+
offset += bytes;
368+
continue;
369+
}
350370
else
351371
a=alignment(it_type, ns);
352372

‎src/util/pointer_offset_size.cpp‎

Lines changed: 47 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,12 @@ member_offset_iterator &member_offset_iterator::operator++()
4242
current.second += bit_field_bits / 8;
4343
bit_field_bits %= 8;
4444
}
45+
else if(comp.type().id() == ID_bool)
46+
{
47+
++bit_field_bits;
48+
current.second += bit_field_bits / 8;
49+
bit_field_bits %= 8;
50+
}
4551
else
4652
{
4753
DATA_INVARIANT(
@@ -288,7 +294,16 @@ exprt member_offset_expr(
288294
bit_field_bits += w;
289295
const std::size_t bytes = bit_field_bits / 8;
290296
bit_field_bits %= 8;
291-
result=plus_exprt(result, from_integer(bytes, result.type()));
297+
if(bytes > 0)
298+
result = plus_exprt(result, from_integer(bytes, result.type()));
299+
}
300+
else if(c.type().id() == ID_bool)
301+
{
302+
++bit_field_bits;
303+
const std::size_t bytes = bit_field_bits / 8;
304+
bit_field_bits %= 8;
305+
if(bytes > 0)
306+
result = plus_exprt(result, from_integer(bytes, result.type()));
292307
}
293308
else
294309
{
@@ -315,6 +330,15 @@ exprt size_of_expr(
315330
{
316331
const auto &array_type = to_array_type(type);
317332

333+
// special-case arrays of bits
334+
if(array_type.subtype().id() == ID_bool)
335+
{
336+
auto bits = pointer_offset_bits(array_type, ns);
337+
338+
if(bits.has_value())
339+
return from_integer((*bits + 7) / 8, size_type());
340+
}
341+
318342
exprt sub = size_of_expr(array_type.subtype(), ns);
319343
if(sub.is_nil())
320344
return nil_exprt();
@@ -335,7 +359,18 @@ exprt size_of_expr(
335359
}
336360
else if(type.id()==ID_vector)
337361
{
338-
exprt sub = size_of_expr(to_vector_type(type).subtype(), ns);
362+
const auto &vector_type = to_vector_type(type);
363+
364+
// special-case vectors of bits
365+
if(vector_type.subtype().id() == ID_bool)
366+
{
367+
auto bits = pointer_offset_bits(vector_type, ns);
368+
369+
if(bits.has_value())
370+
return from_integer((*bits + 7) / 8, size_type());
371+
}
372+
373+
exprt sub = size_of_expr(vector_type.subtype(), ns);
339374
if(sub.is_nil())
340375
return nil_exprt();
341376

@@ -381,7 +416,16 @@ exprt size_of_expr(
381416
bit_field_bits += w;
382417
const std::size_t bytes = bit_field_bits / 8;
383418
bit_field_bits %= 8;
384-
result=plus_exprt(result, from_integer(bytes, result.type()));
419+
if(bytes > 0)
420+
result = plus_exprt(result, from_integer(bytes, result.type()));
421+
}
422+
else if(c.type().id() == ID_bool)
423+
{
424+
++bit_field_bits;
425+
const std::size_t bytes = bit_field_bits / 8;
426+
bit_field_bits %= 8;
427+
if(bytes > 0)
428+
result = plus_exprt(result, from_integer(bytes, result.type()));
385429
}
386430
else
387431
{

‎src/util/simplify_expr.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1947,10 +1947,10 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
19471947
{
19481948
const struct_typet &struct_type=to_struct_type(tp);
19491949
const irep_idt &component_name=with.where().get(ID_component_name);
1950+
const typet &c_type = struct_type.get_component(component_name).type();
19501951

19511952
// is this a bit field?
1952-
if(struct_type.get_component(component_name).type().id()==
1953-
ID_c_bit_field)
1953+
if(c_type.id() == ID_c_bit_field || c_type.id() == ID_bool)
19541954
{
19551955
// don't touch -- might not be byte-aligned
19561956
}

‎src/util/simplify_expr_struct.cpp‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -152,8 +152,12 @@ bool simplify_exprt::simplify_member(exprt &expr)
152152
const struct_typet::componentt &component=
153153
struct_type.get_component(component_name);
154154

155-
if(component.is_nil() || component.type().id()==ID_c_bit_field)
155+
if(
156+
component.is_nil() || component.type().id() == ID_c_bit_field ||
157+
component.type().id() == ID_bool)
158+
{
156159
return true;
160+
}
157161

158162
// add member offset to index
159163
auto offset_int = member_offset(struct_type, component_name, ns);

0 commit comments

Comments
 (0)