Skip to content

Commit bcedf46

Browse files
tautschnigtautschnig
committed
Simplify selected ID_if operands in preorder traversal
This avoids repeatedly visiting already-simplified operands. On the example from #7357 this reduces symex time from 1172 seconds to 922 seconds.
1 parent 63ca05e commit bcedf46

5 files changed

+232
-75
lines changed

‎src/util/simplify_expr.cpp

+89-28
Original file line numberDiff line numberDiff line change
@@ -1372,23 +1372,6 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
13721372
if(pointer.type().id()!=ID_pointer)
13731373
return unchanged(expr);
13741374

1375-
if(pointer.id()==ID_if && pointer.operands().size()==3)
1376-
{
1377-
const if_exprt &if_expr=to_if_expr(pointer);
1378-
1379-
auto tmp_op1 = expr;
1380-
tmp_op1.op() = if_expr.true_case();
1381-
exprt tmp_op1_result = simplify_dereference(tmp_op1);
1382-
1383-
auto tmp_op2 = expr;
1384-
tmp_op2.op() = if_expr.false_case();
1385-
exprt tmp_op2_result = simplify_dereference(tmp_op2);
1386-
1387-
if_exprt tmp{if_expr.cond(), tmp_op1_result, tmp_op2_result};
1388-
1389-
return changed(simplify_if(tmp));
1390-
}
1391-
13921375
if(pointer.id()==ID_address_of)
13931376
{
13941377
exprt tmp=to_address_of_expr(pointer).object();
@@ -1422,6 +1405,30 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
14221405
return unchanged(expr);
14231406
}
14241407

1408+
simplify_exprt::resultt<>
1409+
simplify_exprt::simplify_dereference_preorder(const dereference_exprt &expr)
1410+
{
1411+
const exprt &pointer = expr.pointer();
1412+
1413+
if(pointer.id() == ID_if)
1414+
{
1415+
if_exprt if_expr = lift_if(expr, 0);
1416+
return changed(simplify_if_preorder(if_expr));
1417+
}
1418+
else
1419+
{
1420+
auto r_it = simplify_rec(pointer); // recursive call
1421+
if(r_it.has_changed())
1422+
{
1423+
auto tmp = expr;
1424+
tmp.pointer() = r_it.expr;
1425+
return tmp;
1426+
}
1427+
}
1428+
1429+
return unchanged(expr);
1430+
}
1431+
14251432
simplify_exprt::resultt<>
14261433
simplify_exprt::simplify_lambda(const lambda_exprt &expr)
14271434
{
@@ -1638,17 +1645,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_object(const exprt &expr)
16381645
simplify_exprt::resultt<>
16391646
simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
16401647
{
1641-
// lift up any ID_if on the object
1642-
if(expr.op().id()==ID_if)
1643-
{
1644-
if_exprt if_expr=lift_if(expr, 0);
1645-
if_expr.true_case() =
1646-
simplify_byte_extract(to_byte_extract_expr(if_expr.true_case()));
1647-
if_expr.false_case() =
1648-
simplify_byte_extract(to_byte_extract_expr(if_expr.false_case()));
1649-
return changed(simplify_if(if_expr));
1650-
}
1651-
16521648
const auto el_size = pointer_offset_bits(expr.type(), ns);
16531649
if(el_size.has_value() && *el_size < 0)
16541650
return unchanged(expr);
@@ -1986,6 +1982,41 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
19861982
return unchanged(expr);
19871983
}
19881984

1985+
simplify_exprt::resultt<>
1986+
simplify_exprt::simplify_byte_extract_preorder(const byte_extract_exprt &expr)
1987+
{
1988+
// lift up any ID_if on the object
1989+
if(expr.op().id() == ID_if)
1990+
{
1991+
if_exprt if_expr = lift_if(expr, 0);
1992+
return changed(simplify_if_preorder(if_expr));
1993+
}
1994+
else
1995+
{
1996+
optionalt<exprt::operandst> new_operands;
1997+
1998+
for(std::size_t i = 0; i < expr.operands().size(); ++i)
1999+
{
2000+
auto r_it = simplify_rec(expr.operands()[i]); // recursive call
2001+
if(r_it.has_changed())
2002+
{
2003+
if(!new_operands.has_value())
2004+
new_operands = expr.operands();
2005+
(*new_operands)[i] = std::move(r_it.expr);
2006+
}
2007+
}
2008+
2009+
if(new_operands.has_value())
2010+
{
2011+
exprt result = expr;
2012+
std::swap(result.operands(), *new_operands);
2013+
return result;
2014+
}
2015+
}
2016+
2017+
return unchanged(expr);
2018+
}
2019+
19892020
simplify_exprt::resultt<>
19902021
simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
19912022
{
@@ -2715,6 +2746,36 @@ simplify_exprt::simplify_node_preorder(const exprt &expr)
27152746
{
27162747
result = simplify_typecast_preorder(to_typecast_expr(expr));
27172748
}
2749+
else if(
2750+
expr.id() == ID_byte_extract_little_endian ||
2751+
expr.id() == ID_byte_extract_big_endian)
2752+
{
2753+
result = simplify_byte_extract_preorder(to_byte_extract_expr(expr));
2754+
}
2755+
else if(expr.id() == ID_dereference)
2756+
{
2757+
result = simplify_dereference_preorder(to_dereference_expr(expr));
2758+
}
2759+
else if(expr.id() == ID_index)
2760+
{
2761+
result = simplify_index_preorder(to_index_expr(expr));
2762+
}
2763+
else if(expr.id() == ID_is_dynamic_object)
2764+
{
2765+
result = simplify_is_dynamic_object_preorder(to_unary_expr(expr));
2766+
}
2767+
else if(expr.id() == ID_member)
2768+
{
2769+
result = simplify_member_preorder(to_member_expr(expr));
2770+
}
2771+
else if(expr.id() == ID_pointer_object)
2772+
{
2773+
result = simplify_pointer_object_preorder(to_pointer_object_expr(expr));
2774+
}
2775+
else if(expr.id() == ID_pointer_offset)
2776+
{
2777+
result = simplify_pointer_offset_preorder(to_pointer_offset_expr(expr));
2778+
}
27182779
else if(expr.has_operands())
27192780
{
27202781
optionalt<exprt::operandst> new_operands;

‎src/util/simplify_expr_array.cpp

+36-13
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include "arith_tools.h"
1212
#include "byte_operators.h"
13+
#include "expr_util.h"
1314
#include "pointer_offset_size.h"
1415
#include "replace_expr.h"
1516
#include "std_expr.h"
@@ -196,22 +197,44 @@ simplify_exprt::simplify_index(const index_exprt &expr)
196197
return changed(simplify_byte_extract(result_expr));
197198
}
198199
}
199-
else if(array.id()==ID_if)
200-
{
201-
const if_exprt &if_expr=to_if_expr(array);
202-
exprt cond=if_expr.cond();
203-
204-
index_exprt idx_false=to_index_expr(expr);
205-
idx_false.array()=if_expr.false_case();
206-
207-
new_expr.array() = if_expr.true_case();
208-
209-
exprt result = if_exprt(cond, new_expr, idx_false, expr.type());
210-
return changed(simplify_rec(result));
211-
}
212200

213201
if(no_change)
214202
return unchanged(expr);
215203
else
216204
return std::move(new_expr);
217205
}
206+
207+
simplify_exprt::resultt<>
208+
simplify_exprt::simplify_index_preorder(const index_exprt &expr)
209+
{
210+
// lift up any ID_if on the array
211+
if(expr.array().id() == ID_if)
212+
{
213+
if_exprt if_expr = lift_if(expr, 0);
214+
return changed(simplify_if_preorder(if_expr));
215+
}
216+
else
217+
{
218+
optionalt<exprt::operandst> new_operands;
219+
220+
for(std::size_t i = 0; i < expr.operands().size(); ++i)
221+
{
222+
auto r_it = simplify_rec(expr.operands()[i]); // recursive call
223+
if(r_it.has_changed())
224+
{
225+
if(!new_operands.has_value())
226+
new_operands = expr.operands();
227+
(*new_operands)[i] = std::move(r_it.expr);
228+
}
229+
}
230+
231+
if(new_operands.has_value())
232+
{
233+
exprt result = expr;
234+
std::swap(result.operands(), *new_operands);
235+
return result;
236+
}
237+
}
238+
239+
return unchanged(expr);
240+
}

‎src/util/simplify_expr_class.h

+10
Original file line numberDiff line numberDiff line change
@@ -173,19 +173,29 @@ class simplify_exprt
173173
NODISCARD resultt<> simplify_with(const with_exprt &);
174174
NODISCARD resultt<> simplify_update(const update_exprt &);
175175
NODISCARD resultt<> simplify_index(const index_exprt &);
176+
NODISCARD resultt<> simplify_index_preorder(const index_exprt &);
176177
NODISCARD resultt<> simplify_member(const member_exprt &);
178+
NODISCARD resultt<> simplify_member_preorder(const member_exprt &);
177179
NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &);
178180
NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &);
181+
NODISCARD resultt<>
182+
simplify_byte_extract_preorder(const byte_extract_exprt &);
179183
NODISCARD resultt<> simplify_pointer_object(const pointer_object_exprt &);
184+
NODISCARD resultt<>
185+
simplify_pointer_object_preorder(const pointer_object_exprt &);
180186
NODISCARD resultt<> simplify_object_size(const object_size_exprt &);
181187
NODISCARD resultt<> simplify_is_dynamic_object(const unary_exprt &);
188+
NODISCARD resultt<> simplify_is_dynamic_object_preorder(const unary_exprt &);
182189
NODISCARD resultt<> simplify_is_invalid_pointer(const unary_exprt &);
183190
NODISCARD resultt<> simplify_object(const exprt &);
184191
NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &);
185192
NODISCARD resultt<> simplify_unary_plus(const unary_plus_exprt &);
186193
NODISCARD resultt<> simplify_dereference(const dereference_exprt &);
194+
NODISCARD resultt<> simplify_dereference_preorder(const dereference_exprt &);
187195
NODISCARD resultt<> simplify_address_of(const address_of_exprt &);
188196
NODISCARD resultt<> simplify_pointer_offset(const pointer_offset_exprt &);
197+
NODISCARD resultt<>
198+
simplify_pointer_offset_preorder(const pointer_offset_exprt &);
189199
NODISCARD resultt<> simplify_bswap(const bswap_exprt &);
190200
NODISCARD resultt<> simplify_isinf(const unary_exprt &);
191201
NODISCARD resultt<> simplify_isnan(const unary_exprt &);

‎src/util/simplify_expr_pointer.cpp

+72-20
Original file line numberDiff line numberDiff line change
@@ -249,16 +249,6 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
249249
{
250250
const exprt &ptr = expr.pointer();
251251

252-
if(ptr.id()==ID_if && ptr.operands().size()==3)
253-
{
254-
if_exprt if_expr=lift_if(expr, 0);
255-
if_expr.true_case() =
256-
simplify_pointer_offset(to_pointer_offset_expr(if_expr.true_case()));
257-
if_expr.false_case() =
258-
simplify_pointer_offset(to_pointer_offset_expr(if_expr.false_case()));
259-
return changed(simplify_if(if_expr));
260-
}
261-
262252
if(ptr.type().id()!=ID_pointer)
263253
return unchanged(expr);
264254

@@ -406,6 +396,30 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
406396
return unchanged(expr);
407397
}
408398

399+
simplify_exprt::resultt<> simplify_exprt::simplify_pointer_offset_preorder(
400+
const pointer_offset_exprt &expr)
401+
{
402+
const exprt &pointer = expr.pointer();
403+
404+
if(pointer.id() == ID_if)
405+
{
406+
if_exprt if_expr = lift_if(expr, 0);
407+
return changed(simplify_if_preorder(if_expr));
408+
}
409+
else
410+
{
411+
auto r_it = simplify_rec(pointer); // recursive call
412+
if(r_it.has_changed())
413+
{
414+
auto tmp = expr;
415+
tmp.pointer() = r_it.expr;
416+
return tmp;
417+
}
418+
}
419+
420+
return unchanged(expr);
421+
}
422+
409423
simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
410424
const binary_relation_exprt &expr)
411425
{
@@ -553,22 +567,36 @@ simplify_exprt::simplify_pointer_object(const pointer_object_exprt &expr)
553567
return unchanged(expr);
554568
}
555569

570+
simplify_exprt::resultt<> simplify_exprt::simplify_pointer_object_preorder(
571+
const pointer_object_exprt &expr)
572+
{
573+
const exprt &pointer = expr.op();
574+
575+
if(pointer.id() == ID_if)
576+
{
577+
if_exprt if_expr = lift_if(expr, 0);
578+
return changed(simplify_if_preorder(if_expr));
579+
}
580+
else
581+
{
582+
auto r_it = simplify_rec(pointer); // recursive call
583+
if(r_it.has_changed())
584+
{
585+
auto tmp = expr;
586+
tmp.pointer() = r_it.expr;
587+
return tmp;
588+
}
589+
}
590+
591+
return unchanged(expr);
592+
}
593+
556594
simplify_exprt::resultt<>
557595
simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
558596
{
559597
auto new_expr = expr;
560598
exprt &op = new_expr.op();
561599

562-
if(op.id()==ID_if && op.operands().size()==3)
563-
{
564-
if_exprt if_expr=lift_if(expr, 0);
565-
if_expr.true_case() =
566-
simplify_is_dynamic_object(to_unary_expr(if_expr.true_case()));
567-
if_expr.false_case() =
568-
simplify_is_dynamic_object(to_unary_expr(if_expr.false_case()));
569-
return changed(simplify_if(if_expr));
570-
}
571-
572600
bool no_change = true;
573601

574602
auto op_result = simplify_object(op);
@@ -612,6 +640,30 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
612640
return std::move(new_expr);
613641
}
614642

643+
simplify_exprt::resultt<>
644+
simplify_exprt::simplify_is_dynamic_object_preorder(const unary_exprt &expr)
645+
{
646+
const exprt &pointer = expr.op();
647+
648+
if(pointer.id() == ID_if)
649+
{
650+
if_exprt if_expr = lift_if(expr, 0);
651+
return changed(simplify_if_preorder(if_expr));
652+
}
653+
else
654+
{
655+
auto r_it = simplify_rec(pointer); // recursive call
656+
if(r_it.has_changed())
657+
{
658+
auto tmp = expr;
659+
tmp.op() = r_it.expr;
660+
return tmp;
661+
}
662+
}
663+
664+
return unchanged(expr);
665+
}
666+
615667
simplify_exprt::resultt<>
616668
simplify_exprt::simplify_is_invalid_pointer(const unary_exprt &expr)
617669
{

0 commit comments

Comments
 (0)