Skip to content

Commit 7c2f065

Browse files
tautschnigtautschnig
committed
Move promotion rule application to C front-end
The front-ends handle type conversion when doing arithmetic over enum types. The case of an enum tag is not expected in goto-program conversion. That, however, was only the case for some operators. Made the C front-end properly handle all assignment operators.
1 parent 578617e commit 7c2f065

File tree

4 files changed

+86
-94
lines changed

4 files changed

+86
-94
lines changed

‎regression/cbmc/enum8/main.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#include <assert.h>
2+
3+
enum E
4+
{
5+
A = 1,
6+
B = 16
7+
};
8+
9+
int main()
10+
{
11+
enum E e = A;
12+
e <<= 4;
13+
assert(e == B);
14+
e >>= 4;
15+
assert(e == A);
16+
e |= B;
17+
e ^= A;
18+
assert(e == B);
19+
e -= 15;
20+
assert(e == A);
21+
return 0;
22+
}

‎regression/cbmc/enum8/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: 15 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1845,16 +1845,19 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
18451845

18461846
if(type0.id() == ID_c_enum_tag)
18471847
{
1848-
if(follow_tag(to_c_enum_tag_type(type0)).is_incomplete())
1848+
const c_enum_typet &enum_type = follow_tag(to_c_enum_tag_type(type0));
1849+
if(enum_type.is_incomplete())
18491850
{
18501851
error().source_location = expr.source_location();
18511852
error() << "operator `" << statement
18521853
<< "' given incomplete type `"
18531854
<< to_string(type0) << "'" << eom;
18541855
throw 0;
18551856
}
1856-
else
1857-
expr.type()=type0;
1857+
1858+
// increment/decrement on underlying type
1859+
expr.op0() = typecast_exprt(expr.op0(), enum_type.subtype());
1860+
expr.type() = enum_type.subtype();
18581861
}
18591862
else if(type0.id() == ID_c_bit_field)
18601863
{
@@ -1863,6 +1866,11 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
18631866
expr.op0() = typecast_exprt(expr.op0(), underlying_type);
18641867
expr.type()=underlying_type;
18651868
}
1869+
else if(type0.id() == ID_bool || type0.id() == ID_c_bool)
1870+
{
1871+
implicit_typecast_arithmetic(expr.op0());
1872+
expr.type() = expr.op0().type();
1873+
}
18661874
else if(is_numeric_type(type0))
18671875
{
18681876
expr.type()=type0;
@@ -3311,6 +3319,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
33113319
else if(statement==ID_assign_shl ||
33123320
statement==ID_assign_shr)
33133321
{
3322+
implicit_typecast_arithmetic(op0);
33143323
implicit_typecast_arithmetic(op1);
33153324

33163325
if(is_number(op1.type()))
@@ -3325,12 +3334,6 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
33253334

33263335
typet underlying_type=op0.type();
33273336

3328-
if(underlying_type.id()==ID_c_enum_tag)
3329-
{
3330-
const auto &c_enum_type = to_c_enum_tag_type(underlying_type);
3331-
underlying_type=c_enum_type.subtype();
3332-
}
3333-
33343337
if(underlying_type.id()==ID_unsignedbv ||
33353338
underlying_type.id()==ID_c_bool)
33363339
{
@@ -3353,7 +3356,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
33533356
if(o_type0.id()==ID_bool ||
33543357
o_type0.id()==ID_c_bool)
33553358
{
3356-
implicit_typecast_arithmetic(op1);
3359+
implicit_typecast_arithmetic(op0, op1);
33573360
if(op1.type().id()==ID_bool ||
33583361
op1.type().id()==ID_c_bool ||
33593362
op1.type().id()==ID_c_enum_tag ||
@@ -3366,7 +3369,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
33663369
o_type0.id()==ID_signedbv ||
33673370
o_type0.id()==ID_c_bit_field)
33683371
{
3369-
implicit_typecast(op1, o_type0);
3372+
implicit_typecast_arithmetic(op0, op1);
33703373
return;
33713374
}
33723375
else if(o_type0.id()==ID_vector &&
@@ -3403,7 +3406,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
34033406
else if(o_type0.id()==ID_bool ||
34043407
o_type0.id()==ID_c_bool)
34053408
{
3406-
implicit_typecast_arithmetic(op1);
3409+
implicit_typecast_arithmetic(op0, op1);
34073410
if(op1.type().id()==ID_bool ||
34083411
op1.type().id()==ID_c_bool ||
34093412
op1.type().id()==ID_c_enum_tag ||

‎src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 41 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -99,31 +99,13 @@ void goto_convertt::remove_assignment(
9999

100100
const typet &op0_type = expr.op0().type();
101101

102-
if(op0_type.id()==ID_c_bool)
103-
{
104-
// C/C++ Booleans get very special treatment.
105-
binary_exprt tmp(expr.op0(), new_id, expr.op1(), expr.op1().type());
106-
tmp.op0().make_typecast(expr.op1().type());
107-
rhs=typecast_exprt(is_not_zero(tmp, ns), expr.op0().type());
108-
}
109-
else if(op0_type.id() == ID_c_enum_tag)
110-
{
111-
// We convert c_enums to their underlying type, do the
112-
// operation, and then convert back
113-
const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(op0_type));
114-
auto underlying_type = enum_type.subtype();
115-
auto op0 = typecast_exprt(expr.op0(), underlying_type);
116-
auto op1 = typecast_exprt(expr.op1(), underlying_type);
117-
binary_exprt tmp(op0, new_id, op1, underlying_type);
118-
rhs = typecast_exprt(tmp, expr.op0().type());
119-
}
120-
else
121-
{
122-
rhs.id(new_id);
123-
rhs.copy_to_operands(expr.op0(), expr.op1());
124-
rhs.type()=expr.op0().type();
125-
rhs.add_source_location()=expr.source_location();
126-
}
102+
PRECONDITION(
103+
op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum &&
104+
op0_type.id() != ID_c_bool && op0_type.id() != ID_bool);
105+
rhs.id(new_id);
106+
rhs.copy_to_operands(expr.op0(), expr.op1());
107+
rhs.type() = expr.op0().type();
108+
rhs.add_source_location() = expr.source_location();
127109

128110
code_assignt assignment(expr.op0(), rhs);
129111
assignment.add_source_location()=expr.source_location();
@@ -171,20 +153,19 @@ void goto_convertt::remove_pre(
171153

172154
const typet &op_type = expr.op0().type();
173155

174-
if(op_type.id()==ID_bool)
175-
{
176-
rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
177-
rhs.op0().make_typecast(signed_int_type());
178-
rhs.type()=signed_int_type();
179-
rhs=is_not_zero(rhs, ns);
180-
}
181-
else if(op_type.id()==ID_c_bool)
156+
PRECONDITION(
157+
op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
158+
op_type.id() != ID_c_bool && op_type.id() != ID_bool);
159+
160+
typet constant_type;
161+
162+
if(op_type.id() == ID_pointer)
163+
constant_type = index_type();
164+
else if(is_number(op_type))
165+
constant_type = op_type;
166+
else
182167
{
183-
rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
184-
rhs.op0().make_typecast(signed_int_type());
185-
rhs.type()=signed_int_type();
186-
rhs=is_not_zero(rhs, ns);
187-
rhs.make_typecast(op_type);
168+
UNREACHABLE;
188169
}
189170
else if(op_type.id()==ID_c_enum ||
190171
op_type.id()==ID_c_enum_tag)
@@ -257,56 +238,34 @@ void goto_convertt::remove_post(
257238

258239
const typet &op_type = expr.op0().type();
259240

260-
if(op_type.id()==ID_bool)
261-
{
262-
rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
263-
rhs.op0().make_typecast(signed_int_type());
264-
rhs.type()=signed_int_type();
265-
rhs=is_not_zero(rhs, ns);
266-
}
267-
else if(op_type.id()==ID_c_bool)
241+
PRECONDITION(
242+
op_type.id() != ID_c_enum_tag && op_type.id() != ID_c_enum &&
243+
op_type.id() != ID_c_bool && op_type.id() != ID_bool);
244+
245+
typet constant_type;
246+
247+
if(op_type.id() == ID_pointer)
248+
constant_type = index_type();
249+
else if(is_number(op_type))
250+
constant_type = op_type;
251+
else
268252
{
269-
rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
270-
rhs.op0().make_typecast(signed_int_type());
271-
rhs.type()=signed_int_type();
272-
rhs=is_not_zero(rhs, ns);
273-
rhs.make_typecast(op_type);
253+
UNREACHABLE;
274254
}
275-
else if(op_type.id()==ID_c_enum ||
276-
op_type.id()==ID_c_enum_tag)
255+
256+
exprt constant;
257+
258+
if(constant_type.id() == ID_complex)
277259
{
278-
rhs.copy_to_operands(expr.op0(), from_integer(1, signed_int_type()));
279-
rhs.op0().make_typecast(signed_int_type());
280-
rhs.type()=signed_int_type();
281-
rhs.make_typecast(op_type);
260+
exprt real = from_integer(1, constant_type.subtype());
261+
exprt imag = from_integer(0, constant_type.subtype());
262+
constant = complex_exprt(real, imag, to_complex_type(constant_type));
282263
}
283264
else
284-
{
285-
typet constant_type;
265+
constant = from_integer(1, constant_type);
286266

287-
if(op_type.id()==ID_pointer)
288-
constant_type=index_type();
289-
else if(is_number(op_type) || op_type.id()==ID_c_bool)
290-
constant_type=op_type;
291-
else
292-
{
293-
UNREACHABLE;
294-
}
295-
296-
exprt constant;
297-
298-
if(constant_type.id()==ID_complex)
299-
{
300-
exprt real=from_integer(1, constant_type.subtype());
301-
exprt imag=from_integer(0, constant_type.subtype());
302-
constant=complex_exprt(real, imag, to_complex_type(constant_type));
303-
}
304-
else
305-
constant=from_integer(1, constant_type);
306-
307-
rhs.add_to_operands(expr.op0(), std::move(constant));
308-
rhs.type()=expr.op0().type();
309-
}
267+
rhs.add_to_operands(expr.op0(), std::move(constant));
268+
rhs.type() = expr.op0().type();
310269

311270
code_assignt assignment(expr.op0(), rhs);
312271
assignment.add_source_location()=expr.find_source_location();

0 commit comments

Comments
 (0)