Skip to content

Commit d48e62b

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 01ede2d commit d48e62b

File tree

4 files changed

+39
-47
lines changed

4 files changed

+39
-47
lines changed

‎src/util/simplify_expr.cpp

+12-11
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

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

+11-14
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

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

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

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

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

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

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

296294
simplify_node(expr);
297295
return false;
@@ -300,9 +298,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
300298
tmp.op1().operands().size()==1 &&
301299
tmp.op1().op0().id()==ID_address_of)
302300
{
303-
expr=tmp.op0();
304-
if(type!=expr.type())
305-
expr.make_typecast(type);
301+
expr = typecast_exprt::conditional_cast(tmp.op0(), type);
306302

307303
simplify_node(expr);
308304
return false;
@@ -664,9 +660,7 @@ bool simplify_exprt::simplify_object_size(exprt &expr)
664660
if(op.op0().id()==ID_symbol)
665661
{
666662
// just get the type
667-
const typet &type=ns.follow(op.op0().type());
668-
669-
exprt size=size_of_expr(type, ns);
663+
exprt size = size_of_expr(op.op0().type(), ns);
670664

671665
if(size.is_not_nil())
672666
{

0 commit comments

Comments
 (0)