Skip to content

Commit

Permalink
Assignments to bit-fields yield results of bit-field type
Browse files Browse the repository at this point in the history
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).
  • Loading branch information
tautschnig committed Dec 14, 2023
1 parent 5eb6fee commit ed713ff
Show file tree
Hide file tree
Showing 4 changed files with 90 additions and 8 deletions.
6 changes: 5 additions & 1 deletion regression/cbmc/Bitfields1/main.c
Original file line number Diff line number Diff line change
Expand Up @@ -51,9 +51,13 @@ int main() {
bf.d=2;
assert(bf.d==1);

// assignments have the underlying type
// assignments have the underlying type, except for GCC
assert(sizeof(bf.d=1)==sizeof(_Bool));
#if defined(__GNUC__) && !defined(__INTEL_COMPILER) && !defined(__clang__)
assert(sizeof(bf.a += 1) == 1);
#else
assert(sizeof(bf.a += 1) == sizeof(unsigned long));
#endif

bf.Type=IntelCacheTrace;

Expand Down
36 changes: 36 additions & 0 deletions regression/cbmc/Bitfields5/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
#include <assert.h>
#include <limits.h>

struct S0
{
unsigned f2 : CHAR_BIT + 1;
int x;
};

#ifdef _MSC_VER
# define _Static_assert static_assert
#endif

int main()
{
struct S0 g = {0};
// All compilers in compiler explorer appear to agree that comma and
// assignment expressions over bit-fields permit the use of sizeof. With GCC,
// the result is the declared width (rounded to bytes), all others use the
// size of the underlying type.
// https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm
// for a discussion that this isn't actually specified (while being a
// sizeof/typeof peculiarity)
#if defined(__GNUC__) && !defined(__INTEL_COMPILER) && !defined(__clang__)
# define WIDTH 2
#else
# define WIDTH sizeof(unsigned)
#endif
_Static_assert(sizeof(++g.f2) == WIDTH, "");
_Static_assert(sizeof(0, g.f2) == WIDTH, "");
_Static_assert(sizeof(g.f2 = g.f2) == WIDTH, "");
if(g.f2 <= -1)
assert(0);
if((g.f2 = g.f2) <= -1)
assert(0);
}
8 changes: 8 additions & 0 deletions regression/cbmc/Bitfields5/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
48 changes: 41 additions & 7 deletions src/ansi-c/c_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -970,9 +970,39 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)

if(type.id()==ID_c_bit_field)
{
error().source_location = expr.source_location();
error() << "sizeof cannot be applied to bit fields" << eom;
throw 0;
// only comma or side-effect expressions are permitted
const exprt &op = skip_typecast(to_unary_expr(as_const(expr)).op());
if(op.id() == ID_comma || op.id() == ID_side_effect)
{
const c_bit_field_typet &bf_type = to_c_bit_field_type(type);
if(config.ansi_c.mode == configt::ansi_ct::flavourt::GCC)
{
new_expr = from_integer(
(bf_type.get_width() + config.ansi_c.char_width - 1) /
config.ansi_c.char_width,
size_type());
}
else
{
auto size_of_opt = size_of_expr(bf_type.underlying_type(), *this);

Check warning on line 987 in src/ansi-c/c_typecheck_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_typecheck_expr.cpp#L987

Added line #L987 was not covered by tests

if(!size_of_opt.has_value())

Check warning on line 989 in src/ansi-c/c_typecheck_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_typecheck_expr.cpp#L989

Added line #L989 was not covered by tests
{
error().source_location = expr.source_location();
error() << "type has no size: "
<< to_string(bf_type.underlying_type()) << eom;
throw 0;

Check warning on line 994 in src/ansi-c/c_typecheck_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_typecheck_expr.cpp#L991-L994

Added lines #L991 - L994 were not covered by tests
}

new_expr = size_of_opt.value();

Check warning on line 997 in src/ansi-c/c_typecheck_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_typecheck_expr.cpp#L997

Added line #L997 was not covered by tests
}
}
else
{
error().source_location = expr.source_location();
error() << "sizeof cannot be applied to bit fields" << eom;
throw 0;

Check warning on line 1004 in src/ansi-c/c_typecheck_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/ansi-c/c_typecheck_expr.cpp#L1002-L1004

Added lines #L1002 - L1004 were not covered by tests
}
}
else if(type.id() == ID_bool)
{
Expand Down Expand Up @@ -1876,8 +1906,11 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
{
// promote to underlying type
typet underlying_type = to_c_bit_field_type(type0).underlying_type();
typet type_before{type0};
to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type);
expr.type()=underlying_type;
typecast_exprt result{expr, type_before};
expr.swap(result);
}
else if(type0.id() == ID_bool || type0.id() == ID_c_bool)
{
Expand Down Expand Up @@ -4345,10 +4378,11 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
}

// Add a cast to the underlying type for bit fields.
// In particular, sizeof(s.f=1) works for bit fields.
if(op0.type().id()==ID_c_bit_field)
op0 =
typecast_exprt(op0, to_c_bit_field_type(op0.type()).underlying_type());
if(op0.type() != op1.type() && op0.type().id() == ID_c_bit_field)
{
op1 =
typecast_exprt{op1, to_c_bit_field_type(op0.type()).underlying_type()};
}

const typet o_type0=op0.type();
const typet o_type1=op1.type();
Expand Down

0 comments on commit ed713ff

Please sign in to comment.