Skip to content

Commit 994ecbc

Browse files
tautschnigtautschnig
committed
Remove unnecessary uses of ns.follow from the simplifier
There is no need to use ns.follow when either 1) we only compare the result to types that can never be hidden behind tags or 2) the tag case is handled explicitly.
1 parent 29a49d8 commit 994ecbc

File tree

4 files changed

+39
-47
lines changed

4 files changed

+39
-47
lines changed

‎src/util/simplify_expr.cpp

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ bool simplify_exprt::simplify_abs(exprt &expr)
6767

6868
if(expr.op0().is_constant())
6969
{
70-
const typet &type=ns.follow(expr.op0().type());
70+
const typet &type = expr.op0().type();
7171

7272
if(type.id()==ID_floatbv)
7373
{
@@ -107,7 +107,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
107107

108108
if(expr.op0().is_constant())
109109
{
110-
const typet &type=ns.follow(expr.op0().type());
110+
const typet &type = expr.op0().type();
111111

112112
if(type.id()==ID_floatbv)
113113
{
@@ -163,8 +163,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
163163
if(expr.operands().size()!=1)
164164
return true;
165165

166-
const typet &expr_type=ns.follow(expr.type());
167-
const typet &op_type=ns.follow(expr.op0().type());
166+
const typet &expr_type = expr.type();
167+
const typet &op_type = expr.op0().type();
168168

169169
// eliminate casts of infinity
170170
if(expr.op0().id()==ID_infinity)
@@ -778,11 +778,12 @@ bool simplify_exprt::simplify_dereference(exprt &expr)
778778
if(address_of.object().id()==ID_index)
779779
{
780780
const index_exprt &old=to_index_expr(address_of.object());
781-
if(ns.follow(old.array().type()).id()==ID_array)
781+
if(old.array().type().id() == ID_array)
782782
{
783-
index_exprt idx(old.array(),
784-
plus_exprt(old.index(), pointer.op1()),
785-
ns.follow(old.array().type()).subtype());
783+
index_exprt idx(
784+
old.array(),
785+
plus_exprt(old.index(), pointer.op1()),
786+
old.array().type().subtype());
786787
simplify_rec(idx);
787788
expr.swap(idx);
788789
return false;
@@ -1347,7 +1348,7 @@ bool simplify_exprt::simplify_object(exprt &expr)
13471348
{
13481349
// kill integers from sum
13491350
Forall_operands(it, expr)
1350-
if(ns.follow(it->type()).id()==ID_pointer)
1351+
if(it->type().id() == ID_pointer)
13511352
{
13521353
exprt tmp=*it;
13531354
expr.swap(tmp);
@@ -1359,7 +1360,7 @@ bool simplify_exprt::simplify_object(exprt &expr)
13591360
else if(expr.id()==ID_typecast)
13601361
{
13611362
auto const &typecast_expr = to_typecast_expr(expr);
1362-
const typet &op_type = ns.follow(typecast_expr.op().type());
1363+
const typet &op_type = typecast_expr.op().type();
13631364

13641365
if(op_type.id()==ID_pointer)
13651366
{
@@ -1563,7 +1564,7 @@ optionalt<std::string> simplify_exprt::expr2bits(
15631564
bool little_endian)
15641565
{
15651566
// extract bits from lowest to highest memory address
1566-
const typet &type=ns.follow(expr.type());
1567+
const typet &type = expr.type();
15671568

15681569
if(expr.id()==ID_constant)
15691570
{

‎src/util/simplify_expr_floatbv.cpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ bool simplify_exprt::simplify_isinf(exprt &expr)
2121
if(expr.operands().size()!=1)
2222
return true;
2323

24-
if(ns.follow(expr.op0().type()).id()!=ID_floatbv)
24+
if(expr.op0().type().id() != ID_floatbv)
2525
return true;
2626

2727
if(expr.op0().is_constant())
@@ -72,7 +72,7 @@ bool simplify_exprt::simplify_abs(exprt &expr)
7272

7373
if(expr.op0().is_constant())
7474
{
75-
const typet &type=ns.follow(expr.op0().type());
75+
const typet &type = expr.op0().type();
7676

7777
if(type.id()==ID_floatbv)
7878
{
@@ -114,7 +114,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
114114

115115
if(expr.op0().is_constant())
116116
{
117-
const typet &type=ns.follow(expr.op0().type());
117+
const typet &type = expr.op0().type();
118118

119119
if(type.id()==ID_floatbv)
120120
{
@@ -144,8 +144,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
144144

145145
auto const &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);
146146

147-
const typet &dest_type = ns.follow(floatbv_typecast_expr.type());
148-
const typet &src_type = ns.follow(floatbv_typecast_expr.op().type());
147+
const typet &dest_type = floatbv_typecast_expr.type();
148+
const typet &src_type = floatbv_typecast_expr.op().type();
149149

150150
// eliminate redundant casts
151151
if(dest_type==src_type)
@@ -171,8 +171,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
171171
casted_expr.op1().id()==ID_typecast &&
172172
casted_expr.op0().operands().size()==1 &&
173173
casted_expr.op1().operands().size()==1 &&
174-
ns.follow(casted_expr.op0().type())==dest_type &&
175-
ns.follow(casted_expr.op1().type())==dest_type)
174+
casted_expr.op0().type()==dest_type &&
175+
casted_expr.op1().type()==dest_type)
176176
{
177177
exprt result(casted_expr.id(), floatbv_typecast_expr.type());
178178
result.operands().resize(3);
@@ -282,7 +282,7 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
282282

283283
bool simplify_exprt::simplify_floatbv_op(exprt &expr)
284284
{
285-
const typet &type=ns.follow(expr.type());
285+
const typet &type = expr.type();
286286

287287
PRECONDITION(type.id() == ID_floatbv);
288288
PRECONDITION(
@@ -298,10 +298,10 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
298298
exprt op2=expr.op2(); // rounding mode
299299

300300
INVARIANT(
301-
ns.follow(op0.type()) == type,
301+
op0.type() == type,
302302
"expression type of operand must match type of expression");
303303
INVARIANT(
304-
ns.follow(op1.type()) == type,
304+
op1.type() == type,
305305
"expression type of operand must match type of expression");
306306

307307
// Remember that floating-point addition is _NOT_ associative.

‎src/util/simplify_expr_int.cpp

Lines changed: 11 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -447,7 +447,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
447447
// floating-point addition is _NOT_ associative; thus,
448448
// there is special case for float
449449

450-
if(ns.follow(plus_expr.type()).id() == ID_floatbv)
450+
if(plus_expr.type().id() == ID_floatbv)
451451
{
452452
// we only merge neighboring constants!
453453
Forall_expr(it, operands)
@@ -660,9 +660,9 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
660660

661661
forall_operands(it, expr)
662662
{
663-
if(it->id()==ID_typecast &&
664-
it->operands().size()==1 &&
665-
ns.follow(it->op0().type()).id()==ID_bool)
663+
if(
664+
it->id() == ID_typecast && it->operands().size() == 1 &&
665+
it->op0().type().id() == ID_bool)
666666
{
667667
}
668668
else if(it->is_zero() || it->is_one())
@@ -1355,9 +1355,6 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
13551355
(expr.id()==ID_equal || expr.id()==ID_notequal))
13561356
return simplify_inequality_pointer_object(expr);
13571357

1358-
tmp0.type() = ns.follow(tmp0.type());
1359-
tmp1.type() = ns.follow(tmp1.type());
1360-
13611358
if(tmp0.type().id()==ID_c_enum_tag)
13621359
tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
13631360

@@ -1547,7 +1544,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
15471544
// pretty much all of the simplifications below are unsound
15481545
// for IEEE float because of NaN!
15491546

1550-
if(ns.follow(expr.op0().type()).id()==ID_floatbv)
1547+
if(expr.op0().type().id() == ID_floatbv)
15511548
return true;
15521549

15531550
// eliminate strict inequalities
@@ -1800,18 +1797,18 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
18001797
// (double)value REL const ---> value rel const
18011798
// if 'const' can be represented exactly.
18021799

1803-
if(expr.op0().id()==ID_typecast &&
1804-
expr.op0().operands().size()==1 &&
1805-
ns.follow(expr.op0().type()).id()==ID_floatbv &&
1806-
ns.follow(expr.op0().op0().type()).id()==ID_floatbv)
1800+
if(
1801+
expr.op0().id() == ID_typecast && expr.op0().operands().size() == 1 &&
1802+
expr.op0().type().id() == ID_floatbv &&
1803+
expr.op0().op0().type().id() == ID_floatbv)
18071804
{
18081805
ieee_floatt const_val(to_constant_expr(expr.op1()));
18091806
ieee_floatt const_val_converted=const_val;
18101807
const_val_converted.change_spec(
1811-
ieee_float_spect(to_floatbv_type(ns.follow(expr.op0().op0().type()))));
1808+
ieee_float_spect(to_floatbv_type(expr.op0().op0().type())));
18121809
ieee_floatt const_val_converted_back=const_val_converted;
18131810
const_val_converted_back.change_spec(
1814-
ieee_float_spect(to_floatbv_type(ns.follow(expr.op0().type()))));
1811+
ieee_float_spect(to_floatbv_type(expr.op0().type())));
18151812
if(const_val_converted_back==const_val)
18161813
{
18171814
exprt result=expr;

‎src/util/simplify_expr_pointer.cpp

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,7 @@ bool simplify_exprt::simplify_address_of(exprt &expr)
176176
if(expr.operands().size()!=1)
177177
return true;
178178

179-
if(ns.follow(expr.type()).id()!=ID_pointer)
179+
if(expr.type().id() != ID_pointer)
180180
return true;
181181

182182
exprt &object=expr.op0();
@@ -248,7 +248,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
248248
if(ptr.operands().size()!=1)
249249
return true;
250250

251-
const typet &op_type=ns.follow(ptr.op0().type());
251+
const typet &op_type = ptr.op0().type();
252252

253253
if(op_type.id()==ID_pointer)
254254
{
@@ -280,17 +280,15 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
280280
// We do a bit of special treatment for (TYPE *)(a+(int)&o),
281281
// which is re-written to 'a'.
282282

283-
typet type=ns.follow(expr.type());
283+
typet type = expr.type();
284284
exprt tmp=ptr.op0();
285285
if(tmp.id()==ID_plus && tmp.operands().size()==2)
286286
{
287287
if(tmp.op0().id()==ID_typecast &&
288288
tmp.op0().operands().size()==1 &&
289289
tmp.op0().op0().id()==ID_address_of)
290290
{
291-
expr=tmp.op1();
292-
if(type!=expr.type())
293-
expr.make_typecast(type);
291+
expr = typecast_exprt::conditional_cast(tmp.op1(), type);
294292

295293
simplify_node(expr);
296294
return false;
@@ -299,9 +297,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
299297
tmp.op1().operands().size()==1 &&
300298
tmp.op1().op0().id()==ID_address_of)
301299
{
302-
expr=tmp.op0();
303-
if(type!=expr.type())
304-
expr.make_typecast(type);
300+
expr = typecast_exprt::conditional_cast(tmp.op0(), type);
305301

306302
simplify_node(expr);
307303
return false;
@@ -663,9 +659,7 @@ bool simplify_exprt::simplify_object_size(exprt &expr)
663659
if(op.op0().id()==ID_symbol)
664660
{
665661
// just get the type
666-
const typet &type=ns.follow(op.op0().type());
667-
668-
exprt size=size_of_expr(type, ns);
662+
exprt size = size_of_expr(op.op0().type(), ns);
669663

670664
if(size.is_not_nil())
671665
{

0 commit comments

Comments
 (0)