From 021f971e0d505be99ae3a296bb5068b72c1e16fa Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 2 Jul 2019 10:55:05 +0100 Subject: [PATCH 1/2] simplifier: introduce ranged for Way prettier. --- src/util/simplify_expr.cpp | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 314dbd198ff..cdf20cc6f67 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "namespace.h" #include "pointer_offset_size.h" #include "pointer_offset_sum.h" +#include "range.h" #include "rational.h" #include "rational_tools.h" #include "simplify_utils.h" @@ -1392,24 +1393,29 @@ bool simplify_exprt::simplify_if(if_exprt &expr) return false; } + // this pushes the if-then-else into struct and array constructors if(((truevalue.id()==ID_struct && falsevalue.id()==ID_struct) || (truevalue.id()==ID_array && falsevalue.id()==ID_array)) && truevalue.operands().size()==falsevalue.operands().size()) { exprt cond_copy=cond; exprt falsevalue_copy=falsevalue; - expr.swap(truevalue); + exprt truevalue_copy = truevalue; - exprt::operandst::const_iterator f_it= - falsevalue_copy.operands().begin(); - Forall_operands(it, expr) + auto range_false = make_range(falsevalue_copy.operands()); + auto range_true = make_range(truevalue_copy.operands()); + auto new_expr = truevalue; + new_expr.operands().clear(); + + for(const auto &pair : range_true.zip(range_false)) { - if_exprt if_expr(cond_copy, *it, *f_it); - it->swap(if_expr); - simplify_if(to_if_expr(*it)); - ++f_it; + if_exprt if_expr(cond_copy, pair.first, pair.second); + simplify_if(if_expr); + new_expr.operands().push_back(std::move(if_expr)); } + expr.swap(new_expr); + return false; } From f9365548c2af587d3c97cbc827a5672705da5465 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 2 Jul 2019 10:56:13 +0100 Subject: [PATCH 2/2] simplifier: new interface for simplify_if This improves type safety. --- src/util/simplify_expr.cpp | 65 ++++++++++++------------------ src/util/simplify_expr_array.cpp | 5 +-- src/util/simplify_expr_class.h | 2 +- src/util/simplify_expr_int.cpp | 8 +--- src/util/simplify_expr_pointer.cpp | 6 +-- 5 files changed, 32 insertions(+), 54 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index cdf20cc6f67..c2dbceddabc 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -991,9 +991,7 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr) if_exprt tmp{if_expr.cond(), tmp_op1_result, tmp_op2_result}; - simplify_if(tmp); - - return tmp; + return changed(simplify_if(tmp)); } if(pointer.id()==ID_address_of) @@ -1311,13 +1309,12 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) return result; } -bool simplify_exprt::simplify_if(if_exprt &expr) +NODISCARD simplify_exprt::resultt<> +simplify_exprt::simplify_if(const if_exprt &expr) { - exprt &cond=expr.cond(); - exprt &truevalue=expr.true_case(); - exprt &falsevalue=expr.false_case(); - - bool result=true; + const exprt &cond = expr.cond(); + const exprt &truevalue = expr.true_case(); + const exprt &falsevalue = expr.false_case(); if(do_simplify_if) { @@ -1333,26 +1330,21 @@ bool simplify_exprt::simplify_if(if_exprt &expr) if(truevalue.is_true() && falsevalue.is_false()) { // a?1:0 <-> a - exprt tmp; - tmp.swap(cond); - expr.swap(tmp); - return false; + return cond; } else if(truevalue.is_false() && falsevalue.is_true()) { // a?0:1 <-> !a exprt tmp = boolean_negate(cond); simplify_node(tmp); - expr.swap(tmp); - return false; + return std::move(tmp); } else if(falsevalue.is_false()) { // a?b:0 <-> a AND b and_exprt tmp(cond, truevalue); simplify_node(tmp); - expr.swap(tmp); - return false; + return std::move(tmp); } else if(falsevalue.is_true()) { @@ -1361,16 +1353,14 @@ bool simplify_exprt::simplify_if(if_exprt &expr) simplify_node(tmp_not_cond); or_exprt tmp(tmp_not_cond, truevalue); simplify_node(tmp); - expr.swap(tmp); - return false; + return std::move(tmp); } else if(truevalue.is_true()) { // a?1:b <-> a||(!a && b) <-> a OR b or_exprt tmp(cond, falsevalue); simplify_node(tmp); - expr.swap(tmp); - return false; + return std::move(tmp); } else if(truevalue.is_false()) { @@ -1379,19 +1369,13 @@ bool simplify_exprt::simplify_if(if_exprt &expr) simplify_node(tmp_not_cond); and_exprt tmp(tmp_not_cond, falsevalue); simplify_node(tmp); - expr.swap(tmp); - return false; + return std::move(tmp); } } } if(truevalue==falsevalue) - { - exprt tmp; - tmp.swap(truevalue); - expr.swap(tmp); - return false; - } + return truevalue; // this pushes the if-then-else into struct and array constructors if(((truevalue.id()==ID_struct && falsevalue.id()==ID_struct) || @@ -1409,17 +1393,14 @@ bool simplify_exprt::simplify_if(if_exprt &expr) for(const auto &pair : range_true.zip(range_false)) { - if_exprt if_expr(cond_copy, pair.first, pair.second); - simplify_if(if_expr); - new_expr.operands().push_back(std::move(if_expr)); + new_expr.operands().push_back( + simplify_if(if_exprt(cond_copy, pair.first, pair.second))); } - expr.swap(new_expr); - - return false; + return std::move(new_expr); } - return result; + return unchanged(expr); } bool simplify_exprt::get_values( @@ -1994,8 +1975,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) simplify_byte_extract(to_byte_extract_expr(if_expr.true_case())); if_expr.false_case() = simplify_byte_extract(to_byte_extract_expr(if_expr.false_case())); - simplify_if(if_expr); - return std::move(if_expr); + return simplify_if(if_expr); } const auto el_size = pointer_offset_bits(expr.type(), ns); @@ -2523,7 +2503,14 @@ bool simplify_exprt::simplify_node(exprt &expr) expr.id()==ID_ge || expr.id()==ID_le) no_change = simplify_inequality(expr) && no_change; else if(expr.id()==ID_if) - no_change = simplify_if(to_if_expr(expr)) && no_change; + { + auto r = simplify_if(to_if_expr(expr)); + if(r.has_changed()) + { + no_change = false; + expr = r.expr; + } + } else if(expr.id()==ID_lambda) no_change = simplify_lambda(expr) && no_change; else if(expr.id()==ID_with) diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp index 950117c17a5..21cc09dc97e 100644 --- a/src/util/simplify_expr_array.cpp +++ b/src/util/simplify_expr_array.cpp @@ -102,10 +102,7 @@ bool simplify_exprt::simplify_index(exprt &expr) } if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr); - simplify_if(if_expr); - - expr.swap(if_expr); - + expr = simplify_if(if_expr).expr; return false; } } diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 1622cb5f546..d869fb866fc 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -143,7 +143,7 @@ class simplify_exprt NODISCARD resultt<> simplify_power(const exprt &); NODISCARD resultt<> simplify_bitwise(const exprt &); bool simplify_if_preorder(if_exprt &expr); - bool simplify_if(if_exprt &expr); + NODISCARD resultt<> simplify_if(const if_exprt &); bool simplify_bitnot(exprt &expr); bool simplify_not(exprt &expr); bool simplify_boolean(exprt &expr); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index f233131a270..03e1478ee80 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1261,9 +1261,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr) if_exprt if_expr=lift_if(expr, 0); simplify_inequality(if_expr.true_case()); simplify_inequality(if_expr.false_case()); - simplify_if(if_expr); - expr.swap(if_expr); - + expr = simplify_if(if_expr).expr; return false; } @@ -1640,9 +1638,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) if_exprt if_expr=lift_if(expr, 0); simplify_inequality_rhs_is_constant(if_expr.true_case()); simplify_inequality_rhs_is_constant(if_expr.false_case()); - simplify_if(if_expr); - expr.swap(if_expr); - + expr = simplify_if(if_expr); return false; } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 978b5c7e4f3..51cba08f5ab 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -243,8 +243,7 @@ simplify_exprt::simplify_pointer_offset(const exprt &expr) if_exprt if_expr=lift_if(expr, 0); if_expr.true_case() = simplify_pointer_offset(if_expr.true_case()); if_expr.false_case() = simplify_pointer_offset(if_expr.false_case()); - simplify_if(if_expr); - return if_expr; + return changed(simplify_if(if_expr)); } if(ptr.type().id()!=ID_pointer) @@ -577,8 +576,7 @@ simplify_exprt::simplify_is_dynamic_object(const exprt &expr) if_exprt if_expr=lift_if(expr, 0); if_expr.true_case() = simplify_is_dynamic_object(if_expr.true_case()); if_expr.false_case() = simplify_is_dynamic_object(if_expr.false_case()); - simplify_if(if_expr); - return std::move(if_expr); + return changed(simplify_if(if_expr)); } bool no_change = true;