Skip to content

Commit c4240b4

Browse files
author
Daniel Kroening
committed
fix exprt::opX accesses in simplifier
This improves type safety.
1 parent b20cf69 commit c4240b4

File tree

5 files changed

+44
-35
lines changed

5 files changed

+44
-35
lines changed

src/util/simplify_expr.cpp

Lines changed: 22 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -547,13 +547,12 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
547547
// (void*)(intX)expr -> (void*)expr
548548
if(
549549
expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
550-
expr.op().operands().size() == 1 &&
551550
(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv) &&
552551
to_bitvector_type(op_type).get_width() >=
553552
to_bitvector_type(expr_type).get_width())
554553
{
555554
auto new_expr = expr;
556-
new_expr.op() = expr.op().op0();
555+
new_expr.op() = to_typecast_expr(expr.op()).op();
557556
return changed(simplify_typecast(new_expr)); // rec. call
558557
}
559558

@@ -634,10 +633,10 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
634633
// (T1 *)(T2 *)x -> (T1 *)x
635634
if(
636635
expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
637-
op_type.id() == ID_pointer && expr.op().operands().size() == 1)
636+
op_type.id() == ID_pointer)
638637
{
639638
auto new_expr = expr;
640-
new_expr.op() = expr.op().op0();
639+
new_expr.op() = to_typecast_expr(expr.op()).op();
641640
return changed(simplify_typecast(new_expr)); // recursive call
642641
}
643642

@@ -1360,25 +1359,27 @@ simplify_exprt::resultt<> simplify_exprt::simplify_object(const exprt &expr)
13601359
const exprt &casted_expr = typecast_expr.op();
13611360
if(casted_expr.id() == ID_plus && casted_expr.operands().size() == 2)
13621361
{
1363-
const exprt &cand = casted_expr.op0().id() == ID_typecast
1364-
? casted_expr.op0()
1365-
: casted_expr.op1();
1362+
const auto &plus_expr = to_plus_expr(casted_expr);
13661363

1367-
if(cand.id()==ID_typecast &&
1368-
cand.operands().size()==1 &&
1369-
cand.op0().id()==ID_address_of)
1370-
{
1371-
return cand.op0();
1372-
}
1373-
else if(cand.id()==ID_typecast &&
1374-
cand.operands().size()==1 &&
1375-
cand.op0().id()==ID_plus &&
1376-
cand.op0().operands().size()==2 &&
1377-
cand.op0().op0().id()==ID_typecast &&
1378-
cand.op0().op0().operands().size()==1 &&
1379-
cand.op0().op0().op0().id()==ID_address_of)
1364+
const exprt &cand = plus_expr.op0().id() == ID_typecast
1365+
? plus_expr.op0()
1366+
: plus_expr.op1();
1367+
1368+
if(cand.id() == ID_typecast)
13801369
{
1381-
return cand.op0().op0().op0();
1370+
const auto &typecast_op = to_typecast_expr(cand).op();
1371+
1372+
if(typecast_op.id() == ID_address_of)
1373+
{
1374+
return typecast_op;
1375+
}
1376+
else if(
1377+
typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1378+
typecast_op.op0().id() == ID_typecast &&
1379+
to_typecast_expr(typecast_op.op0()).op().id() == ID_address_of)
1380+
{
1381+
return cand.op0().op0().op0();
1382+
}
13821383
}
13831384
}
13841385
}

src/util/simplify_expr_array.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "simplify_expr_class.h"
1010

1111
#include "arith_tools.h"
12+
#include "byte_operators.h"
1213
#include "namespace.h"
1314
#include "pointer_offset_size.h"
1415
#include "replace_expr.h"
@@ -163,6 +164,8 @@ simplify_exprt::simplify_index(const index_exprt &expr)
163164
else if(array.id()==ID_byte_extract_little_endian ||
164165
array.id()==ID_byte_extract_big_endian)
165166
{
167+
const auto &byte_extract_expr = to_byte_extract_expr(array);
168+
166169
if(array.type().id() == ID_array || array.type().id() == ID_vector)
167170
{
168171
optionalt<typet> subtype;
@@ -179,12 +182,13 @@ simplify_exprt::simplify_index(const index_exprt &expr)
179182
return unchanged(expr);
180183

181184
// add offset to index
182-
mult_exprt offset(from_integer(*sub_size, array.op1().type()), index);
183-
plus_exprt final_offset(array.op1(), offset);
185+
mult_exprt offset(
186+
from_integer(*sub_size, byte_extract_expr.offset().type()), index);
187+
plus_exprt final_offset(byte_extract_expr.offset(), offset);
184188
simplify_node(final_offset);
185189

186190
exprt result_expr(array.id(), expr.type());
187-
result_expr.add_to_operands(array.op0(), final_offset);
191+
result_expr.add_to_operands(byte_extract_expr.op(), final_offset);
188192

189193
return changed(simplify_rec(result_expr));
190194
}

src/util/simplify_expr_boolean.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -136,10 +136,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
136136

137137
// search for a and !a
138138
for(const exprt &op : new_operands)
139-
if(op.id()==ID_not &&
140-
op.operands().size()==1 &&
141-
op.type().id()==ID_bool &&
142-
expr_set.find(op.op0())!=expr_set.end())
139+
if(
140+
op.id() == ID_not && op.type().id() == ID_bool &&
141+
expr_set.find(to_not_expr(op).op()) != expr_set.end())
143142
{
144143
return make_boolean_expr(expr.id() == ID_or);
145144
}

src/util/simplify_expr_pointer.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -313,7 +313,8 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
313313
tmp.op0().operands().size()==1 &&
314314
tmp.op0().op0().id()==ID_address_of)
315315
{
316-
auto new_expr = typecast_exprt::conditional_cast(tmp.op1(), type);
316+
auto new_expr =
317+
typecast_exprt::conditional_cast(to_plus_expr(tmp).op1(), type);
317318

318319
simplify_node(new_expr);
319320
return new_expr;

src/util/simplify_expr_struct.cpp

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,8 @@ simplify_exprt::simplify_member(const member_exprt &expr)
130130
else if(op.id()==ID_byte_extract_little_endian ||
131131
op.id()==ID_byte_extract_big_endian)
132132
{
133+
const auto &byte_extract_expr = to_byte_extract_expr(op);
134+
133135
if(op_type.id()==ID_struct)
134136
{
135137
// This rewrites byte_extract(s, o, struct_type).member
@@ -151,20 +153,20 @@ simplify_exprt::simplify_member(const member_exprt &expr)
151153
if(!offset_int.has_value())
152154
return unchanged(expr);
153155

154-
const exprt &struct_offset=op.op1();
156+
const exprt &struct_offset = byte_extract_expr.offset();
155157
exprt member_offset = from_integer(*offset_int, struct_offset.type());
156158
plus_exprt final_offset(struct_offset, member_offset);
157159
simplify_node(final_offset);
158160

159-
byte_extract_exprt result(op.id(), op.op0(), final_offset, expr.type());
161+
byte_extract_exprt result(
162+
op.id(), byte_extract_expr.op(), final_offset, expr.type());
160163

161164
return changed(simplify_rec(result)); // recursive call
162165
}
163166
else if(op_type.id() == ID_union)
164167
{
165168
// rewrite byte_extract(X, 0).member to X
166169
// if the type of X is that of the member
167-
const auto &byte_extract_expr = to_byte_extract_expr(op);
168170
if(byte_extract_expr.offset().is_zero())
169171
{
170172
const union_typet &union_type = to_union_type(op_type);
@@ -204,12 +206,14 @@ simplify_exprt::simplify_member(const member_exprt &expr)
204206
}
205207
else if(op.id() == ID_typecast)
206208
{
209+
const auto &typecast_expr = to_typecast_expr(op);
210+
207211
// Try to look through member(cast(x)) if the cast is between structurally
208212
// identical types:
209-
if(op_type == op.op0().type())
213+
if(op_type == typecast_expr.op().type())
210214
{
211215
auto new_expr = expr;
212-
new_expr.struct_op() = op.op0();
216+
new_expr.struct_op() = typecast_expr.op();
213217
return changed(simplify_member(new_expr));
214218
}
215219

@@ -224,7 +228,7 @@ simplify_exprt::simplify_member(const member_exprt &expr)
224228
if(requested_offset.has_value())
225229
{
226230
auto equivalent_member = get_subexpression_at_offset(
227-
op.op0(), *requested_offset, expr.type(), ns);
231+
typecast_expr.op(), *requested_offset, expr.type(), ns);
228232

229233
// Guess: turning this into a byte-extract operation is not really an
230234
// optimisation.

0 commit comments

Comments
 (0)