Skip to content

Commit 16c0cbe

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 dbe6455 commit 16c0cbe

File tree

4 files changed

+90
-8
lines changed

4 files changed

+90
-8
lines changed

regression/cbmc/Bitfields1/main.c

+5-1
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,13 @@ int main() {
5151
bf.d=2;
5252
assert(bf.d==1);
5353

54-
// assignments have the underlying type
54+
// assignments have the underlying type, except for GCC
5555
assert(sizeof(bf.d=1)==sizeof(_Bool));
56+
#if defined(__GNUC__) && !defined(__INTEL_COMPILER) && !defined(__clang__)
57+
assert(sizeof(bf.a += 1) == 1);
58+
#else
5659
assert(sizeof(bf.a += 1) == sizeof(unsigned long));
60+
#endif
5761

5862
bf.Type=IntelCacheTrace;
5963

regression/cbmc/Bitfields5/main.c

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#include <assert.h>
2+
#include <limits.h>
3+
4+
struct S0
5+
{
6+
unsigned f2 : CHAR_BIT + 1;
7+
int x;
8+
};
9+
10+
#ifdef _MSC_VER
11+
# define _Static_assert static_assert
12+
#endif
13+
14+
int main()
15+
{
16+
struct S0 g = {0};
17+
// All compilers in compiler explorer appear to agree that comma and
18+
// assignment expressions over bit-fields permit the use of sizeof. With GCC,
19+
// the result is the declared width (rounded to bytes), all others use the
20+
// size of the underlying type.
21+
// https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm
22+
// for a discussion that this isn't actually specified (while being a
23+
// sizeof/typeof peculiarity)
24+
#if defined(__GNUC__) && !defined(__INTEL_COMPILER) && !defined(__clang__)
25+
# define WIDTH 2
26+
#else
27+
# define WIDTH sizeof(unsigned)
28+
#endif
29+
_Static_assert(sizeof(++g.f2) == WIDTH, "");
30+
_Static_assert(sizeof(0, g.f2) == WIDTH, "");
31+
_Static_assert(sizeof(g.f2 = g.f2) == WIDTH, "");
32+
if(g.f2 <= -1)
33+
assert(0);
34+
if((g.f2 = g.f2) <= -1)
35+
assert(0);
36+
}

regression/cbmc/Bitfields5/test.desc

+8
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

+41-7
Original file line numberDiff line numberDiff line change
@@ -970,9 +970,39 @@ 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 = skip_typecast(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+
if(config.ansi_c.mode == configt::ansi_ct::flavourt::GCC)
979+
{
980+
new_expr = from_integer(
981+
(bf_type.get_width() + config.ansi_c.char_width - 1) /
982+
config.ansi_c.char_width,
983+
size_type());
984+
}
985+
else
986+
{
987+
auto size_of_opt = size_of_expr(bf_type.underlying_type(), *this);
988+
989+
if(!size_of_opt.has_value())
990+
{
991+
error().source_location = expr.source_location();
992+
error() << "type has no size: "
993+
<< to_string(bf_type.underlying_type()) << eom;
994+
throw 0;
995+
}
996+
997+
new_expr = size_of_opt.value();
998+
}
999+
}
1000+
else
1001+
{
1002+
error().source_location = expr.source_location();
1003+
error() << "sizeof cannot be applied to bit fields" << eom;
1004+
throw 0;
1005+
}
9761006
}
9771007
else if(type.id() == ID_bool)
9781008
{
@@ -1876,8 +1906,11 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
18761906
{
18771907
// promote to underlying type
18781908
typet underlying_type = to_c_bit_field_type(type0).underlying_type();
1909+
typet type_before{type0};
18791910
to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type);
18801911
expr.type()=underlying_type;
1912+
typecast_exprt result{expr, type_before};
1913+
expr.swap(result);
18811914
}
18821915
else if(type0.id() == ID_bool || type0.id() == ID_c_bool)
18831916
{
@@ -4345,10 +4378,11 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
43454378
}
43464379

43474380
// 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());
4381+
if(op0.type() != op1.type() && op0.type().id() == ID_c_bit_field)
4382+
{
4383+
op1 =
4384+
typecast_exprt{op1, to_c_bit_field_type(op0.type()).underlying_type()};
4385+
}
43524386

43534387
const typet o_type0=op0.type();
43544388
const typet o_type1=op1.type();

0 commit comments

Comments
 (0)