Skip to content

Commit 0aacbe4

Browse files
committed
Assignments to bit-fields yield results of bit-field type
Do not pre-emptively cast side effects over bit-fields to the underlying type. sizeof just has a very peculiar semantics, which is discussed in https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm. Issue was found by CSmith (test generated with random seed 1700653858).
1 parent 52688d7 commit 0aacbe4

File tree

3 files changed

+52
-11
lines changed

3 files changed

+52
-11
lines changed

regression/cbmc/Bitfields5/main.c

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
#include <assert.h>
2+
#include <limits.h>
3+
4+
struct S0
5+
{
6+
unsigned long f2 : CHAR_BIT + 1;
7+
int x;
8+
};
9+
10+
int main()
11+
{
12+
struct S0 g = {0};
13+
// All compilers in compiler explorer appear to agree that comma and
14+
// assignment expressions over bit-fields have the declared width (rounded to
15+
// bytes) of the bit-field as sizeof result.
16+
// https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm
17+
// for a discussion that this isn't actually specified (while being a
18+
// sizeof/typeof peculiarity)
19+
_Static_assert(sizeof(++g.f2) == 2, "");
20+
_Static_assert(sizeof(0, g.f2) == 2, "");
21+
_Static_assert(sizeof(g.f2 = g.f2) == 2, "");
22+
if(g.f2 <= -1)
23+
assert(0);
24+
if((g.f2 = g.f2) <= -1)
25+
assert(0);
26+
}

regression/cbmc/Bitfields5/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+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 18 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -970,9 +970,22 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
970970

971971
if(type.id()==ID_c_bit_field)
972972
{
973-
error().source_location = expr.source_location();
974-
error() << "sizeof cannot be applied to bit fields" << eom;
975-
throw 0;
973+
// only comma or side-effect expressions are permitted
974+
const exprt &op = to_unary_expr(as_const(expr)).op();
975+
if(op.id() == ID_comma || op.id() == ID_side_effect)
976+
{
977+
const c_bit_field_typet &bf_type = to_c_bit_field_type(type);
978+
new_expr = from_integer(
979+
(bf_type.get_width() + config.ansi_c.char_width - 1) /
980+
config.ansi_c.char_width,
981+
size_type());
982+
}
983+
else
984+
{
985+
error().source_location = expr.source_location();
986+
error() << "sizeof cannot be applied to bit fields" << eom;
987+
throw 0;
988+
}
976989
}
977990
else if(type.id() == ID_bool)
978991
{
@@ -1872,13 +1885,13 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
18721885
typecast_exprt(op0, enum_type.underlying_type());
18731886
expr.type() = enum_type.underlying_type();
18741887
}
1875-
else if(type0.id() == ID_c_bit_field)
1888+
/*else if(type0.id() == ID_c_bit_field)
18761889
{
18771890
// promote to underlying type
18781891
typet underlying_type = to_c_bit_field_type(type0).underlying_type();
18791892
to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type);
18801893
expr.type()=underlying_type;
1881-
}
1894+
}*/
18821895
else if(type0.id() == ID_bool || type0.id() == ID_c_bool)
18831896
{
18841897
implicit_typecast_arithmetic(to_unary_expr(expr).op());
@@ -4344,12 +4357,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
43444357
}
43454358
}
43464359

4347-
// Add a cast to the underlying type for bit fields.
4348-
// In particular, sizeof(s.f=1) works for bit fields.
4349-
if(op0.type().id()==ID_c_bit_field)
4350-
op0 =
4351-
typecast_exprt(op0, to_c_bit_field_type(op0.type()).underlying_type());
4352-
43534360
const typet o_type0=op0.type();
43544361
const typet o_type1=op1.type();
43554362

0 commit comments

Comments
 (0)