From eda7601b62e8a49f18702b3b9c5e34d1cecce672 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 4 Jul 2019 16:57:08 +0100 Subject: [PATCH 01/18] simplifier: use new interface --- src/util/simplify_expr.cpp | 84 +++++++++----------- src/util/simplify_expr_array.cpp | 94 ++++++++++------------- src/util/simplify_expr_class.h | 14 ++-- src/util/simplify_expr_int.cpp | 78 ++++++++++++------- src/util/simplify_expr_pointer.cpp | 2 +- src/util/simplify_expr_struct.cpp | 119 ++++++++++++----------------- 6 files changed, 189 insertions(+), 202 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index f19d6fdfce9..6e8e075cac3 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -103,10 +103,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr) return unchanged(expr); } -bool simplify_exprt::simplify_sign(exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_sign(const exprt &expr) { if(expr.operands().size()!=1) - return true; + return unchanged(expr); if(expr.op0().is_constant()) { @@ -115,8 +115,7 @@ bool simplify_exprt::simplify_sign(exprt &expr) if(type.id()==ID_floatbv) { ieee_floatt value(to_constant_expr(expr.op0())); - expr = make_boolean_expr(value.get_sign()); - return false; + return make_boolean_expr(value.get_sign()); } else if(type.id()==ID_signedbv || type.id()==ID_unsignedbv) @@ -124,13 +123,12 @@ bool simplify_exprt::simplify_sign(exprt &expr) const auto value = numeric_cast(expr.op0()); if(value.has_value()) { - expr = make_boolean_expr(*value >= 0); - return false; + return make_boolean_expr(*value >= 0); } } } - return true; + return unchanged(expr); } simplify_exprt::resultt<> @@ -1546,14 +1544,15 @@ simplify_exprt::resultt<> simplify_exprt::simplify_lambda(const exprt &expr) return unchanged(expr); } -bool simplify_exprt::simplify_with(exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_with(const exprt &expr) { - bool result=true; + bool no_change = true; if((expr.operands().size()%2)!=1) - return true; + return unchanged(expr); - auto &with_expr = to_with_expr(expr); + // copy + auto with_expr = to_with_expr(expr); const typet old_type_followed = ns.follow(with_expr.old().type()); @@ -1569,17 +1568,20 @@ bool simplify_exprt::simplify_with(exprt &expr) with_expr.where().get(ID_component_name); if(!to_struct_type(old_type_followed).has_component(component_name)) - return result; + return unchanged(expr); std::size_t number = to_struct_type(old_type_followed).component_number(component_name); + if(number >= with_expr.old().operands().size()) + return unchanged(expr); + with_expr.old().operands()[number].swap(with_expr.new_value()); with_expr.operands().erase(++with_expr.operands().begin()); with_expr.operands().erase(++with_expr.operands().begin()); - result=false; + no_change = false; } } } @@ -1588,10 +1590,10 @@ bool simplify_exprt::simplify_with(exprt &expr) with_expr.old().type().id() == ID_vector) { if( - expr.op0().id() == ID_array || expr.op0().id() == ID_constant || - expr.op0().id() == ID_vector) + with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant || + with_expr.old().id() == ID_vector) { - while(expr.operands().size()>1) + while(with_expr.operands().size() > 1) { const auto i = numeric_cast(with_expr.where()); @@ -1607,26 +1609,24 @@ bool simplify_exprt::simplify_with(exprt &expr) with_expr.operands().erase(++with_expr.operands().begin()); with_expr.operands().erase(++with_expr.operands().begin()); - result=false; + no_change = false; } } } - if(expr.operands().size()==1) - { - exprt tmp; - tmp.swap(expr.op0()); - expr.swap(tmp); - result=false; - } + if(with_expr.operands().size() == 1) + return with_expr.old(); - return result; + if(no_change) + return unchanged(expr); + else + return std::move(with_expr); } -bool simplify_exprt::simplify_update(exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_update(const exprt &expr) { if(expr.operands().size()!=3) - return true; + return unchanged(expr); // this is to push updates into (possibly nested) constants @@ -1645,10 +1645,10 @@ bool simplify_exprt::simplify_update(exprt &expr) const auto i = numeric_cast(e.op0()); if(!i.has_value()) - return true; + return unchanged(expr); if(*i < 0 || *i >= value_ptr->operands().size()) - return true; + return unchanged(expr); value_ptr = &value_ptr->operands()[numeric_cast_v(*i)]; } @@ -1660,20 +1660,18 @@ bool simplify_exprt::simplify_update(exprt &expr) const struct_typet &value_ptr_struct_type = to_struct_type(value_ptr_type); if(!value_ptr_struct_type.has_component(component_name)) - return true; + return unchanged(expr); auto &designator_as_struct_expr = to_struct_expr(*value_ptr); value_ptr = &designator_as_struct_expr.component(component_name, ns); CHECK_RETURN(value_ptr->is_not_nil()); } else - return true; // give up, unknown designator + return unchanged(expr); // give up, unknown designator } // found, done *value_ptr=to_update_expr(expr).new_value(); - expr.swap(updated_value); - - return false; + return updated_value; } simplify_exprt::resultt<> simplify_exprt::simplify_object(const exprt &expr) @@ -2603,8 +2601,7 @@ bool simplify_exprt::simplify_node(exprt &expr) expr.id()==ID_gt || expr.id()==ID_lt || expr.id()==ID_ge || expr.id()==ID_le) { - if(!simplify_inequality(expr)) - r = changed(expr); + r = simplify_inequality(expr); } else if(expr.id()==ID_if) { @@ -2616,23 +2613,19 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_with) { - if(!simplify_with(expr)) - r = changed(expr); + r = simplify_with(expr); } else if(expr.id()==ID_update) { - if(!simplify_update(expr)) - r = changed(expr); + r = simplify_update(expr); } else if(expr.id()==ID_index) { - if(!simplify_index(expr)) - r = changed(expr); + r = simplify_index(expr); } else if(expr.id()==ID_member) { - if(!simplify_member(expr)) - r = changed(expr); + r = simplify_member(expr); } else if(expr.id()==ID_byte_update_little_endian || expr.id()==ID_byte_update_big_endian) @@ -2782,8 +2775,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_sign) { - if(!simplify_sign(expr)) - r = changed(expr); + r = simplify_sign(expr); } else if(expr.id() == ID_popcount) { diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp index 21cc09dc97e..d7ba8dd02d3 100644 --- a/src/util/simplify_expr_array.cpp +++ b/src/util/simplify_expr_array.cpp @@ -15,13 +15,18 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_expr.h" #include "string_constant.h" -bool simplify_exprt::simplify_index(exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) { bool no_change = true; + // copy + auto index_expr = to_index_expr(expr); + + // references + auto &index = index_expr.index(); + auto &array = index_expr.array(); + // extra arithmetic optimizations - const exprt &index=to_index_expr(expr).index(); - const exprt &array=to_index_expr(expr).array(); if(index.id()==ID_div && index.operands().size()==2) @@ -31,7 +36,7 @@ bool simplify_exprt::simplify_index(exprt &expr) index.op0().op1()==index.op1()) { exprt tmp=index.op0().op0(); - expr.op1()=tmp; + index = tmp; no_change = false; } else if(index.op0().id()==ID_mult && @@ -39,24 +44,23 @@ bool simplify_exprt::simplify_index(exprt &expr) index.op0().op0()==index.op1()) { exprt tmp=index.op0().op1(); - expr.op1()=tmp; + index = tmp; no_change = false; } } - if(array.id()==ID_lambda) + if(array.id() == ID_lambda) { // simplify (lambda i: e)(x) to e[i/x] const auto &comprehension = to_array_comprehension_expr(array); - if(expr.op1().type() == comprehension.arg().type()) + if(index.type() == comprehension.arg().type()) { exprt tmp = comprehension.body(); - replace_expr(comprehension.arg(), expr.op1(), tmp); - expr.swap(tmp); - simplify_rec(expr); - return false; + replace_expr(comprehension.arg(), index, tmp); + simplify_rec(tmp); + return std::move(tmp); } } else if(array.id()==ID_with) @@ -64,53 +68,45 @@ bool simplify_exprt::simplify_index(exprt &expr) // we have (a WITH [i:=e])[j] if(array.operands().size() != 3) - return true; + return unchanged(expr); const auto &with_expr = to_with_expr(array); - if(with_expr.where() == expr.op1()) + if(with_expr.where() == index) { // simplify (e with [i:=v])[i] to v - exprt tmp = with_expr.new_value(); - expr.swap(tmp); - return false; + return with_expr.new_value(); } else { // Turn (a with i:=x)[j] into (i==j)?x:a[j]. // watch out that the type of i and j might be different. const exprt rhs_casted = - typecast_exprt::conditional_cast(with_expr.where(), expr.op1().type()); - - equal_exprt equality_expr(expr.op1(), rhs_casted); - - simplify_inequality(equality_expr); + typecast_exprt::conditional_cast(with_expr.where(), index.type()); - index_exprt new_index_expr(with_expr.old(), expr.op1(), expr.type()); + exprt equality_expr = simplify_inequality(equal_exprt(index, rhs_casted)); - simplify_index(new_index_expr); // recursive call + exprt new_index_expr = simplify_index(index_exprt( + with_expr.old(), index, index_expr.type())); // recursive call if(equality_expr.is_true()) { - expr = with_expr.new_value(); - return false; + return with_expr.new_value(); } else if(equality_expr.is_false()) { - expr.swap(new_index_expr); - return false; + return new_index_expr; } if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr); - expr = simplify_if(if_expr).expr; - return false; + return simplify_if(if_expr).expr; } } else if( array.id() == ID_constant || array.id() == ID_array || array.id() == ID_vector) { - const auto i = numeric_cast(expr.op1()); + const auto i = numeric_cast(index); if(!i.has_value()) { @@ -122,14 +118,12 @@ bool simplify_exprt::simplify_index(exprt &expr) else { // ok - exprt tmp = array.operands()[numeric_cast_v(*i)]; - expr.swap(tmp); - return false; + return array.operands()[numeric_cast_v(*i)]; } } else if(array.id()==ID_string_constant) { - const auto i = numeric_cast(expr.op1()); + const auto i = numeric_cast(index); const std::string &value = id2string(to_string_constant(array).get_value()); @@ -145,18 +139,14 @@ bool simplify_exprt::simplify_index(exprt &expr) // terminating zero? const char v = (*i == value.size()) ? 0 : value[numeric_cast_v(*i)]; - exprt tmp=from_integer(v, expr.type()); - expr.swap(tmp); - return false; + return from_integer(v, index_expr.type()); } } else if(array.id()==ID_array_of) { if(array.operands().size()==1) { - exprt tmp=array.op0(); - expr.swap(tmp); - return false; + return array.op0(); } } else if(array.id() == ID_array_list) @@ -168,9 +158,7 @@ bool simplify_exprt::simplify_index(exprt &expr) simplify(tmp_index); if(tmp_index==index) { - exprt tmp=array.operands()[i*2+1]; - expr.swap(tmp); - return false; + return array.operands()[i * 2 + 1]; } } } @@ -190,7 +178,7 @@ bool simplify_exprt::simplify_index(exprt &expr) auto sub_size = pointer_offset_size(*subtype, ns); if(!sub_size.has_value()) - return true; + return unchanged(expr); // add offset to index mult_exprt offset(from_integer(*sub_size, array.op1().type()), index); @@ -199,11 +187,10 @@ bool simplify_exprt::simplify_index(exprt &expr) exprt result_expr(array.id(), expr.type()); result_expr.add_to_operands(array.op0(), final_offset); - expr.swap(result_expr); - simplify_rec(expr); + simplify_rec(result_expr); - return false; + return std::move(result_expr); } } else if(array.id()==ID_if) @@ -214,13 +201,16 @@ bool simplify_exprt::simplify_index(exprt &expr) index_exprt idx_false=to_index_expr(expr); idx_false.array()=if_expr.false_case(); - to_index_expr(expr).array()=if_expr.true_case(); + index_expr.array() = if_expr.true_case(); - expr=if_exprt(cond, expr, idx_false, expr.type()); - simplify_rec(expr); + exprt result = if_exprt(cond, index_expr, idx_false, expr.type()); + simplify_rec(result); - return false; + return std::move(result); } - return no_change; + if(no_change) + return unchanged(expr); + else + return std::move(index_expr); } diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 28e03fbbfb4..c81128100e8 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -147,19 +147,19 @@ class simplify_exprt NODISCARD resultt<> simplify_bitnot(const exprt &); NODISCARD resultt<> simplify_not(const exprt &); NODISCARD resultt<> simplify_boolean(const exprt &); - bool simplify_inequality(exprt &expr); + NODISCARD resultt<> simplify_inequality(const exprt &); NODISCARD resultt<> simplify_ieee_float_relation(const binary_relation_exprt &); NODISCARD resultt<> simplify_lambda(const exprt &); - bool simplify_with(exprt &expr); - bool simplify_update(exprt &expr); - bool simplify_index(exprt &expr); - bool simplify_member(exprt &expr); + NODISCARD resultt<> simplify_with(const exprt &); + NODISCARD resultt<> simplify_update(const exprt &); + NODISCARD resultt<> simplify_index(const exprt &); + NODISCARD resultt<> simplify_member(const exprt &); NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &); NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &); NODISCARD resultt<> simplify_pointer_object(const exprt &); NODISCARD resultt<> simplify_object_size(const exprt &); - bool simplify_dynamic_size(exprt &expr); + NODISCARD resultt<> simplify_dynamic_size(const exprt &); NODISCARD resultt<> simplify_is_dynamic_object(const exprt &expr); NODISCARD resultt<> simplify_is_invalid_pointer(const exprt &expr); NODISCARD resultt<> simplify_same_object(const exprt &); @@ -175,7 +175,7 @@ class simplify_exprt NODISCARD resultt<> simplify_isnan(const unary_exprt &); NODISCARD resultt<> simplify_isnormal(const unary_exprt &); NODISCARD resultt<> simplify_abs(const abs_exprt &); - bool simplify_sign(exprt &expr); + NODISCARD resultt<> simplify_sign(const exprt &); NODISCARD resultt<> simplify_popcount(const popcount_exprt &); NODISCARD resultt<> simplify_complex(const exprt &); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 0ea1ee50bb0..c04fc1225dc 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1220,39 +1220,39 @@ simplify_exprt::resultt<> simplify_exprt::simplify_bitnot(const exprt &expr) } /// simplifies inequalities !=, <=, <, >=, >, and also == -bool simplify_exprt::simplify_inequality(exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr) { - exprt::operandst &operands=expr.operands(); + const exprt::operandst &operands = expr.operands(); if(expr.type().id()!=ID_bool) - return true; + return unchanged(expr); if(operands.size()!=2) - return true; + return unchanged(expr); exprt tmp0=expr.op0(); exprt tmp1=expr.op1(); // types must match if(tmp0.type() != tmp1.type()) - return true; + return unchanged(expr); // if rhs is ID_if (and lhs is not), swap operands for == and != if((expr.id()==ID_equal || expr.id()==ID_notequal) && tmp0.id()!=ID_if && tmp1.id()==ID_if) { - expr.op0().swap(expr.op1()); - return simplify_inequality(expr); + auto new_expr = expr; + new_expr.op0().swap(new_expr.op1()); + return simplify_inequality(new_expr); // recursive call } if(tmp0.id()==ID_if && tmp0.operands().size()==3) { if_exprt if_expr=lift_if(expr, 0); - simplify_inequality(if_expr.true_case()); - simplify_inequality(if_expr.false_case()); - expr = simplify_if(if_expr).expr; - return false; + if_expr.true_case() = simplify_inequality(if_expr.true_case()); + if_expr.false_case() = simplify_inequality(if_expr.false_case()); + return changed(simplify_if(if_expr)); } // see if we are comparing pointers that are address_of @@ -1261,12 +1261,24 @@ bool simplify_exprt::simplify_inequality(exprt &expr) (tmp1.id()==ID_address_of || (tmp1.id()==ID_typecast && tmp1.op0().id()==ID_address_of)) && (expr.id()==ID_equal || expr.id()==ID_notequal)) - return simplify_inequality_address_of(expr); + { + exprt tmp = expr; + if(simplify_inequality_address_of(tmp)) + return unchanged(expr); + else + return std::move(tmp); + } if(tmp0.id()==ID_pointer_object && tmp1.id()==ID_pointer_object && (expr.id()==ID_equal || expr.id()==ID_notequal)) - return simplify_inequality_pointer_object(expr); + { + exprt tmp = expr; + if(simplify_inequality_pointer_object(tmp)) + return unchanged(expr); + else + return std::move(tmp); + } if(tmp0.type().id()==ID_c_enum_tag) tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type())); @@ -1280,36 +1292,50 @@ bool simplify_exprt::simplify_inequality(exprt &expr) // are _both_ constant? if(tmp0_const && tmp1_const) { - return simplify_inequality_both_constant(expr); + exprt tmp = expr; + if(simplify_inequality_both_constant(tmp)) + return unchanged(expr); + else + return std::move(tmp); } else if(tmp0_const) { // we want the constant on the RHS + exprt new_expr = expr; + if(expr.id()==ID_ge) - expr.id(ID_le); + new_expr.id(ID_le); else if(expr.id()==ID_le) - expr.id(ID_ge); + new_expr.id(ID_ge); else if(expr.id()==ID_gt) - expr.id(ID_lt); + new_expr.id(ID_lt); else if(expr.id()==ID_lt) - expr.id(ID_gt); + new_expr.id(ID_gt); - expr.op0().swap(expr.op1()); + new_expr.op0().swap(new_expr.op1()); // RHS is constant, LHS is not - simplify_inequality_rhs_is_constant(expr); - return false; + simplify_inequality_rhs_is_constant(new_expr); + return std::move(new_expr); } else if(tmp1_const) { // RHS is constant, LHS is not - return simplify_inequality_rhs_is_constant(expr); + exprt tmp = expr; + if(simplify_inequality_rhs_is_constant(tmp)) + return unchanged(expr); + else + return std::move(tmp); } else { // both are not constant - return simplify_inequality_no_constant(expr); + exprt tmp = expr; + if(simplify_inequality_no_constant(tmp)) + return unchanged(expr); + else + return std::move(tmp); } } @@ -1608,7 +1634,7 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr) // remove zeros simplify_node(expr.op0()); simplify_node(expr.op1()); - simplify_inequality(expr); // recursive call + expr = simplify_inequality(expr); // recursive call return false; } } @@ -1696,7 +1722,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) expr.op1()=from_integer(0, expr.op0().type()); else expr.op1().type()=expr.op0().type(); - simplify_inequality(expr); // do again! + expr = simplify_inequality(expr); // do again! return false; } } @@ -1738,7 +1764,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) expr.op1()=from_integer(i, expr.op1().type()); expr.op0() = simplify_plus(to_plus_expr(expr.op0())); - simplify_inequality(expr); + expr = simplify_inequality(expr); return false; } } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 51cba08f5ab..dedeaacdccc 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -521,7 +521,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) } expr.operands() = std::move(new_inequality_ops); - simplify_inequality(expr); + expr = simplify_inequality(expr); return false; } diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 4d1067b271e..677b65a3f25 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -15,15 +15,15 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_offset_size.h" #include "std_expr.h" -bool simplify_exprt::simplify_member(exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) { if(expr.operands().size()!=1) - return true; + return unchanged(expr); const irep_idt &component_name= to_member_expr(expr).get_component_name(); - exprt &op=expr.op0(); + const exprt &op = expr.op0(); const typet &op_type=ns.follow(op.type()); if(op.id()==ID_with) @@ -34,12 +34,12 @@ bool simplify_exprt::simplify_member(exprt &expr) if(op.operands().size()>=3 && op_type.id()==ID_struct) { - exprt::operandst &operands=op.operands(); + exprt::operandst new_operands = op.operands(); - while(operands.size()>1) + while(new_operands.size() > 1) { - exprt &op1=operands[operands.size()-2]; - exprt &op2=operands[operands.size()-1]; + exprt &op1 = new_operands[new_operands.size() - 2]; + exprt &op2 = new_operands[new_operands.size() - 1]; if(op1.get(ID_component_name)==component_name) { @@ -49,27 +49,22 @@ bool simplify_exprt::simplify_member(exprt &expr) "member expression type must match component type"); exprt tmp; tmp.swap(op2); - expr.swap(tmp); // do this recursively - simplify_rec(expr); + simplify_rec(tmp); - return false; + return std::move(tmp); } else // something else, get rid of it - operands.resize(operands.size()-2); + new_operands.resize(new_operands.size() - 2); } - if(op.operands().size()==1) - { - exprt tmp; - tmp.swap(op.op0()); - op.swap(tmp); - // do this recursively - simplify_member(expr); - } + DATA_INVARIANT(new_operands.size() == 1, "post-condition of loop"); - return false; + auto new_member_expr = expr; + new_member_expr.op0() = new_operands.front(); + // do this recursively + return simplify_member(new_member_expr); } else if(op_type.id()==ID_union) { @@ -78,12 +73,12 @@ bool simplify_exprt::simplify_member(exprt &expr) if(with_expr.where().get(ID_component_name)==component_name) { // WITH(s, .m, v).m -> v - expr=with_expr.new_value(); + auto tmp = with_expr.new_value(); // do this recursively - simplify_rec(expr); + simplify_rec(tmp); - return false; + return std::move(tmp); } } } @@ -103,25 +98,24 @@ bool simplify_exprt::simplify_member(exprt &expr) { // UPDATE(s, .m, v).m -> v exprt tmp=update_expr.new_value(); - expr.swap(tmp); // do this recursively - simplify_rec(expr); + simplify_rec(tmp); - return false; + return std::move(tmp); } // the following optimization only works on structs, // and not on unions else if(op_type.id()==ID_struct) { // UPDATE(s, .m1, v).m2 -> s.m2 - exprt tmp=update_expr.old(); - op.swap(tmp); + auto new_expr = expr; + new_expr.op0() = update_expr.old(); // do this recursively - simplify_rec(expr); + simplify_rec(new_expr); - return false; + return std::move(new_expr); } } } @@ -139,10 +133,7 @@ bool simplify_exprt::simplify_member(exprt &expr) DATA_INVARIANT( op.operands()[number].type() == expr.type(), "member expression type must match component type"); - exprt tmp; - tmp.swap(op.operands()[number]); - expr.swap(tmp); - return false; + return op.operands()[number]; } } } @@ -162,13 +153,13 @@ bool simplify_exprt::simplify_member(exprt &expr) component.is_nil() || component.type().id() == ID_c_bit_field || component.type().id() == ID_bool) { - return true; + return unchanged(expr); } // add member offset to index auto offset_int = member_offset(struct_type, component_name, ns); if(!offset_int.has_value()) - return true; + return unchanged(expr); const exprt &struct_offset=op.op1(); exprt member_offset = from_integer(*offset_int, struct_offset.type()); @@ -176,11 +167,10 @@ bool simplify_exprt::simplify_member(exprt &expr) simplify_node(final_offset); byte_extract_exprt result(op.id(), op.op0(), final_offset, expr.type()); - expr.swap(result); - simplify_rec(expr); + simplify_rec(result); - return false; + return std::move(result); } else if(op_type.id() == ID_union) { @@ -193,12 +183,7 @@ bool simplify_exprt::simplify_member(exprt &expr) const typet &subtype = union_type.component_type(component_name); if(subtype == byte_extract_expr.op().type()) - { - exprt tmp = byte_extract_expr.op(); - expr.swap(tmp); - - return false; - } + return byte_extract_expr.op(); } } } @@ -206,11 +191,7 @@ bool simplify_exprt::simplify_member(exprt &expr) { // trivial? if(to_union_expr(op).op().type() == expr.type()) - { - exprt tmp=to_union_expr(op).op(); - expr.swap(tmp); - return false; - } + return to_union_expr(op).op(); // need to convert! auto target_size = pointer_offset_size(expr.type(), ns); @@ -229,10 +210,7 @@ bool simplify_exprt::simplify_member(exprt &expr) auto tmp = bits2expr(bits_cut, expr.type(), true); if(tmp.has_value()) - { - expr = *tmp; - return false; - } + return std::move(*tmp); } } } @@ -242,9 +220,9 @@ bool simplify_exprt::simplify_member(exprt &expr) // identical types: if(op_type == op.op0().type()) { - expr.op0() = op.op0(); - simplify_member(expr); - return false; + auto new_expr = expr; + new_expr.op0() = op.op0(); + return simplify_member(new_expr); } // Try to translate into an equivalent member (perhaps nested) of the type @@ -267,9 +245,9 @@ bool simplify_exprt::simplify_member(exprt &expr) equivalent_member.value().id() != ID_byte_extract_little_endian && equivalent_member.value().id() != ID_byte_extract_big_endian) { - expr = equivalent_member.value(); - simplify_rec(expr); - return false; + auto tmp = equivalent_member.value(); + simplify_rec(tmp); + return std::move(tmp); } } } @@ -282,12 +260,13 @@ bool simplify_exprt::simplify_member(exprt &expr) member_exprt member_false=to_member_expr(expr); member_false.compound()=if_expr.false_case(); - to_member_expr(expr).compound()=if_expr.true_case(); + member_exprt member_true = to_member_expr(expr); + member_true.compound() = if_expr.true_case(); - expr=if_exprt(cond, expr, member_false, expr.type()); - simplify_rec(expr); + auto tmp = if_exprt(cond, member_true, member_false, expr.type()); + simplify_rec(tmp); - return false; + return std::move(tmp); } else if(op.id() == ID_let) { @@ -297,13 +276,13 @@ bool simplify_exprt::simplify_member(exprt &expr) // let x = 1 in x member_exprt pushed_in_member = to_member_expr(expr); pushed_in_member.op() = to_let_expr(op).where(); - expr = op; - to_let_expr(expr).where() = pushed_in_member; - to_let_expr(expr).type() = to_let_expr(expr).where().type(); + auto new_expr = op; + to_let_expr(new_expr).where() = pushed_in_member; + to_let_expr(new_expr).type() = to_let_expr(new_expr).where().type(); - simplify_rec(expr); - return false; + simplify_rec(new_expr); + return std::move(new_expr); } - return true; + return unchanged(expr); } From ef6cceb1417e5e4a0d0c5cf51efd0703b87ed1cd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 5 Jul 2019 09:57:52 +0100 Subject: [PATCH 02/18] simplifier: prevent spurious adding of type Expressions should not be given a type() child if they don't have one. --- src/util/simplify_utils.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index fcbe1f232ae..7244f8fb3ef 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "simplify_utils.h" +#include "as_const.h" #include @@ -126,8 +127,8 @@ bool sort_and_join(exprt &expr) if(!expr.has_operands()) return true; - const struct saj_tablet &saj_entry= - sort_and_join(expr.id(), expr.type().id()); + const struct saj_tablet &saj_entry = + sort_and_join(expr.id(), as_const(expr).type().id()); if(saj_entry.id.empty()) return true; From a7a20a4a59e22a4023fdd830f7ce4f8a68f020bd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 5 Jul 2019 09:28:18 +0100 Subject: [PATCH 03/18] simplifier: simplify_rec has new interface This improves type safety. --- src/util/simplify_expr.cpp | 137 ++++++++++++++++++----------- src/util/simplify_expr_array.cpp | 11 +-- src/util/simplify_expr_class.h | 2 +- src/util/simplify_expr_pointer.cpp | 23 +++-- src/util/simplify_expr_struct.cpp | 30 ++----- 5 files changed, 116 insertions(+), 87 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 6e8e075cac3..ab712ceb484 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -648,7 +648,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) from_integer(*sub_size, size_type()), typecast_exprt(expr.op().op1(), size_type())); - simplify_rec(new_expr.op()); // rec. call + new_expr.op() = simplify_rec(new_expr.op()); // rec. call return changed(simplify_typecast(new_expr)); // rec. call } @@ -732,8 +732,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) } } - simplify_rec(new_expr); - return std::move(new_expr); + return changed(simplify_rec(new_expr)); // recursive call } } @@ -1072,8 +1071,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) auto result = address_of_exprt(index_exprt(o, from_integer(0, size_type()))); - simplify_rec(result); - return std::move(result); + return changed(simplify_rec(result)); // recursive call } } @@ -1109,8 +1107,7 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr) { exprt tmp=to_address_of_expr(pointer).object(); // one address_of is gone, try again - simplify_rec(tmp); - return tmp; + return changed(simplify_rec(tmp)); } // rewrite *(&a[0] + x) to a[x] else if(pointer.id()==ID_plus && @@ -1128,8 +1125,7 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr) old.array(), pointer_offset_sum(old.index(), pointer.op1()), old.array().type().subtype()); - simplify_rec(idx); - return idx; + return changed(simplify_rec(idx)); } } } @@ -1292,9 +1288,9 @@ bool simplify_exprt::simplify_if_branch( } if(!tresult) - simplify_rec(trueexpr); + trueexpr = simplify_rec(trueexpr); // recursive call if(!fresult) - simplify_rec(falseexpr); + falseexpr = simplify_rec(falseexpr); // recursive call return tresult && fresult; } @@ -1327,7 +1323,7 @@ bool simplify_exprt::simplify_if_cond(exprt &expr) } if(!tmp) - simplify_rec(expr); + expr = simplify_rec(expr); // recursive call result=tmp && result; } @@ -1341,14 +1337,21 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) exprt &truevalue=expr.true_case(); exprt &falsevalue=expr.false_case(); + bool result = true; + // we first want to look at the condition - bool result=simplify_rec(cond); + auto r_cond = simplify_rec(cond); + if(r_cond.has_changed()) + { + cond = r_cond.expr; + result = false; + } // 1 ? a : b -> a and 0 ? a : b -> b if(cond.is_constant()) { exprt tmp=cond.is_true()?truevalue:falsevalue; - simplify_rec(tmp); + tmp = simplify_rec(tmp); expr.swap(tmp); return false; } @@ -1383,7 +1386,12 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) else local_replace_map.insert(std::make_pair(cond, true_exprt())); - result=simplify_rec(truevalue) && result; + auto r_truevalue = simplify_rec(truevalue); + if(r_truevalue.has_changed()) + { + truevalue = r_truevalue.expr; + result = false; + } local_replace_map=map_before; @@ -1403,18 +1411,43 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) else local_replace_map.insert(std::make_pair(cond, false_exprt())); - result=simplify_rec(falsevalue) && result; + auto r_falsevalue = simplify_rec(falsevalue); + if(r_falsevalue.has_changed()) + { + falsevalue = r_falsevalue.expr; + result = false; + } local_replace_map.swap(map_before); #else - result=simplify_rec(truevalue) && result; - result=simplify_rec(falsevalue) && result; + auto r_truevalue = simplify_rec(truevalue); + if(r_truevalue.has_changed()) + { + truevalue = r_truevalue.expr; + result = false; + } + auto r_falsevalue = simplify_rec(falsevalue); + if(r_falsevalue.has_changed()) + { + falsevalue = r_falsevalue.expr; + result = false; + } #endif } else { - result=simplify_rec(truevalue) && result; - result=simplify_rec(falsevalue) && result; + auto r_truevalue = simplify_rec(truevalue); + if(r_truevalue.has_changed()) + { + truevalue = r_truevalue.expr; + result = false; + } + auto r_falsevalue = simplify_rec(falsevalue); + if(r_falsevalue.has_changed()) + { + falsevalue = r_falsevalue.expr; + result = false; + } } return result; @@ -2192,9 +2225,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) auto tmp = expr; tmp.op() = index_exprt(expr.op(), expr.offset()); tmp.offset() = from_integer(0, expr.offset().type()); - simplify_rec(tmp); - - return std::move(tmp); + return changed(simplify_rec(tmp)); } // extract bits of a constant @@ -2240,8 +2271,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) if(!subexpr.has_value() || subexpr.value() == expr) return unchanged(expr); - simplify_rec(subexpr.value()); - return subexpr.value(); + return changed(simplify_rec(subexpr.value())); // recursive call } simplify_exprt::resultt<> @@ -2464,16 +2494,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) } if(result_expr.is_not_nil()) - { - simplify_rec(result_expr); - return result_expr; - } - - if(result_expr.is_not_nil()) - { - simplify_rec(result_expr); - return result_expr; - } + return changed(simplify_rec(result_expr)); } // replace elements of array or struct expressions, possibly using @@ -2517,7 +2538,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) *offset_int + val_offset - m_offset_bits / 8, offset.type()), new_val); - simplify_rec(*it); + *it = simplify_rec(*it); // recursive call val_offset+=bytes_req; } @@ -2568,8 +2589,14 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr) if(expr.has_operands()) { Forall_operands(it, expr) - if(!simplify_rec(*it)) // recursive call + { + auto r_it = simplify_rec(*it); // recursive call + if(r_it.has_changed()) + { + *it = r_it.expr; result=false; + } + } } } @@ -2812,8 +2839,7 @@ bool simplify_exprt::simplify_node(exprt &expr) return no_change; } -/// \return returns true if expression unchanged; returns false if changed -bool simplify_exprt::simplify_rec(exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr) { // look up in cache @@ -2859,34 +2885,45 @@ bool simplify_exprt::simplify_rec(exprt &expr) #endif #endif - if(!result) + if(result) // no change { - POSTCONDITION(tmp.type() == expr.type()); - expr.swap(tmp); + return unchanged(expr); + } + else // change, new expression is 'tmp' + { + POSTCONDITION(as_const(tmp).type() == expr.type()); - #ifdef USE_CACHE +#ifdef USE_CACHE // save in cache - cache_result.first->second=expr; - #endif - } + cache_result.first->second = tmp; +#endif - return result; + return std::move(tmp); + } } +/// \return returns true if expression unchanged; returns false if changed bool simplify_exprt::simplify(exprt &expr) { #ifdef DEBUG_ON_DEMAND if(debug_on) std::cout << "TO-SIMP " << format(expr) << "\n"; #endif - bool res=simplify_rec(expr); + auto result = simplify_rec(expr); #ifdef DEBUG_ON_DEMAND if(debug_on) - std::cout << "FULLSIMP " << format(expr) << "\n"; + std::cout << "FULLSIMP " << format(result.expr) << "\n"; #endif - return res; + if(result.has_changed()) + { + expr = result.expr; + return false; // change + } + else + return true; // no change } +/// \return returns true if expression unchanged; returns false if changed bool simplify(exprt &expr, const namespacet &ns) { return simplify_exprt(ns).simplify(expr); diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp index d7ba8dd02d3..949aae389e5 100644 --- a/src/util/simplify_expr_array.cpp +++ b/src/util/simplify_expr_array.cpp @@ -59,8 +59,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) { exprt tmp = comprehension.body(); replace_expr(comprehension.arg(), index, tmp); - simplify_rec(tmp); - return std::move(tmp); + return changed(simplify_rec(tmp)); } } else if(array.id()==ID_with) @@ -188,9 +187,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) exprt result_expr(array.id(), expr.type()); result_expr.add_to_operands(array.op0(), final_offset); - simplify_rec(result_expr); - - return std::move(result_expr); + return changed(simplify_rec(result_expr)); } } else if(array.id()==ID_if) @@ -204,9 +201,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) index_expr.array() = if_expr.true_case(); exprt result = if_exprt(cond, index_expr, idx_false, expr.type()); - simplify_rec(result); - - return std::move(result); + return changed(simplify_rec(result)); } if(no_change) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index c81128100e8..709acb7619b 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -205,7 +205,7 @@ class simplify_exprt // main recursion bool simplify_node(exprt &expr); bool simplify_node_preorder(exprt &expr); - bool simplify_rec(exprt &expr); + NODISCARD resultt<> simplify_rec(const exprt &); virtual bool simplify(exprt &expr); diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index dedeaacdccc..2dc11ff6a34 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -69,8 +69,13 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr) new_index_expr.array() = array_result.expr; } - if(!simplify_rec(new_index_expr.index())) + auto index_result = simplify_rec(new_index_expr.index()); + + if(index_result.has_changed()) + { no_change = false; + new_index_expr.index() = index_result.expr; + } // rewrite (*(type *)int) [index] by // pushing the index inside @@ -148,8 +153,12 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr) else if(expr.id()==ID_dereference) { auto new_expr = to_dereference_expr(expr); - if(!simplify_rec(new_expr.pointer())) + auto r_pointer = simplify_rec(new_expr.pointer()); + if(r_pointer.has_changed()) + { + new_expr.pointer() = r_pointer.expr; return std::move(new_expr); + } } else if(expr.id()==ID_if) { @@ -157,8 +166,12 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr) bool no_change = true; - if(!simplify_rec(new_if_expr.cond())) + auto r_cond = simplify_rec(new_if_expr.cond()); + if(r_cond.has_changed()) + { + new_if_expr.cond() = r_cond.expr; no_change = false; + } auto true_result = simplify_address_of_arg(new_if_expr.true_case()); if(true_result.has_changed()) @@ -547,9 +560,7 @@ simplify_exprt::simplify_pointer_object(const exprt &expr) p_o_true.op0() = if_expr.true_case(); auto new_expr = if_exprt(cond, p_o_true, p_o_false, expr.type()); - simplify_rec(new_expr); - - return new_expr; + return changed(simplify_rec(new_expr)); } if(op_result.has_changed()) diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 677b65a3f25..ca7b94313b7 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -51,9 +51,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) tmp.swap(op2); // do this recursively - simplify_rec(tmp); - - return std::move(tmp); + return changed(simplify_rec(tmp)); } else // something else, get rid of it new_operands.resize(new_operands.size() - 2); @@ -76,9 +74,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) auto tmp = with_expr.new_value(); // do this recursively - simplify_rec(tmp); - - return std::move(tmp); + return changed(simplify_rec(tmp)); } } } @@ -100,9 +96,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) exprt tmp=update_expr.new_value(); // do this recursively - simplify_rec(tmp); - - return std::move(tmp); + return changed(simplify_rec(tmp)); } // the following optimization only works on structs, // and not on unions @@ -113,9 +107,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) new_expr.op0() = update_expr.old(); // do this recursively - simplify_rec(new_expr); - - return std::move(new_expr); + return changed(simplify_rec(new_expr)); } } } @@ -168,9 +160,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) byte_extract_exprt result(op.id(), op.op0(), final_offset, expr.type()); - simplify_rec(result); - - return std::move(result); + return changed(simplify_rec(result)); // recursive call } else if(op_type.id() == ID_union) { @@ -246,8 +236,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) equivalent_member.value().id() != ID_byte_extract_big_endian) { auto tmp = equivalent_member.value(); - simplify_rec(tmp); - return std::move(tmp); + return changed(simplify_rec(tmp)); } } } @@ -264,9 +253,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) member_true.compound() = if_expr.true_case(); auto tmp = if_exprt(cond, member_true, member_false, expr.type()); - simplify_rec(tmp); - - return std::move(tmp); + return changed(simplify_rec(tmp)); } else if(op.id() == ID_let) { @@ -280,8 +267,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) to_let_expr(new_expr).where() = pushed_in_member; to_let_expr(new_expr).type() = to_let_expr(new_expr).where().type(); - simplify_rec(new_expr); - return std::move(new_expr); + return changed(simplify_rec(new_expr)); } return unchanged(expr); From 5295cb7a61033cb270504cb38c617b9d970e15a7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 12:06:03 +0100 Subject: [PATCH 04/18] simplifier: move if_expr related methods into separate file These have tight coupling, and there is a sufficient number of them. --- src/util/Makefile | 1 + src/util/simplify_expr.cpp | 413 --------------------------------- src/util/simplify_expr_if.cpp | 420 ++++++++++++++++++++++++++++++++++ 3 files changed, 421 insertions(+), 413 deletions(-) create mode 100644 src/util/simplify_expr_if.cpp diff --git a/src/util/Makefile b/src/util/Makefile index baaa4ab5bba..1628e6b325b 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -71,6 +71,7 @@ SRC = allocate_objects.cpp \ simplify_expr_array.cpp \ simplify_expr_boolean.cpp \ simplify_expr_floatbv.cpp \ + simplify_expr_if.cpp \ simplify_expr_int.cpp \ simplify_expr_pointer.cpp \ simplify_expr_struct.cpp \ diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index ab712ceb484..c8f8c6a73fc 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1133,419 +1133,6 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr) return unchanged(expr); } -bool simplify_exprt::simplify_if_implies( - exprt &expr, - const exprt &cond, - bool truth, - bool &new_truth) -{ - if(expr==cond) - { - new_truth = truth; - return false; - } - - if(truth && cond.id()==ID_lt && expr.id()==ID_lt) - { - if(cond.op0()==expr.op0() && - cond.op1().is_constant() && - expr.op1().is_constant() && - cond.op1().type()==expr.op1().type()) - { - mp_integer i1, i2; - - if( - !to_integer(to_constant_expr(cond.op1()), i1) && - !to_integer(to_constant_expr(expr.op1()), i2)) - { - if(i1 >= i2) - { - new_truth = true; - return false; - } - } - } - - if(cond.op1()==expr.op1() && - cond.op0().is_constant() && - expr.op0().is_constant() && - cond.op0().type()==expr.op0().type()) - { - mp_integer i1, i2; - - if( - !to_integer(to_constant_expr(cond.op0()), i1) && - !to_integer(to_constant_expr(expr.op0()), i2)) - { - if(i1 <= i2) - { - new_truth = true; - return false; - } - } - } - } - - return true; -} - -bool simplify_exprt::simplify_if_recursive( - exprt &expr, - const exprt &cond, - bool truth) -{ - if(expr.type().id()==ID_bool) - { - bool new_truth; - - if(!simplify_if_implies(expr, cond, truth, new_truth)) - { - if(new_truth) - { - expr=true_exprt(); - return false; - } - else - { - expr=false_exprt(); - return false; - } - } - } - - bool result = true; - - Forall_operands(it, expr) - result = simplify_if_recursive(*it, cond, truth) && result; - - return result; -} - -bool simplify_exprt::simplify_if_conj( - exprt &expr, - const exprt &cond) -{ - forall_operands(it, cond) - { - if(expr==*it) - { - expr=true_exprt(); - return false; - } - } - - bool result=true; - - Forall_operands(it, expr) - result=simplify_if_conj(*it, cond) && result; - - return result; -} - -bool simplify_exprt::simplify_if_disj( - exprt &expr, - const exprt &cond) -{ - forall_operands(it, cond) - { - if(expr==*it) - { - expr=false_exprt(); - return false; - } - } - - bool result=true; - - Forall_operands(it, expr) - result=simplify_if_disj(*it, cond) && result; - - return result; -} - -bool simplify_exprt::simplify_if_branch( - exprt &trueexpr, - exprt &falseexpr, - const exprt &cond) -{ - bool tresult = true; - bool fresult = true; - - if(cond.id()==ID_and) - { - tresult = simplify_if_conj(trueexpr, cond) && tresult; - fresult = simplify_if_recursive(falseexpr, cond, false) && fresult; - } - else if(cond.id()==ID_or) - { - tresult = simplify_if_recursive(trueexpr, cond, true) && tresult; - fresult = simplify_if_disj(falseexpr, cond) && fresult; - } - else - { - tresult = simplify_if_recursive(trueexpr, cond, true) && tresult; - fresult = simplify_if_recursive(falseexpr, cond, false) && fresult; - } - - if(!tresult) - trueexpr = simplify_rec(trueexpr); // recursive call - if(!fresult) - falseexpr = simplify_rec(falseexpr); // recursive call - - return tresult && fresult; -} - -bool simplify_exprt::simplify_if_cond(exprt &expr) -{ - bool result=true; - bool tmp=false; - - while(!tmp) - { - tmp=true; - - if(expr.id()==ID_and) - { - if(expr.has_operands()) - { - exprt::operandst &operands = expr.operands(); - for(exprt::operandst::iterator it1=operands.begin(); - it1!=operands.end(); it1++) - { - for(exprt::operandst::iterator it2=operands.begin(); - it2!=operands.end(); it2++) - { - if(it1!=it2) - tmp=simplify_if_recursive(*it1, *it2, true) && tmp; - } - } - } - } - - if(!tmp) - expr = simplify_rec(expr); // recursive call - - result=tmp && result; - } - - return result; -} - -bool simplify_exprt::simplify_if_preorder(if_exprt &expr) -{ - exprt &cond=expr.cond(); - exprt &truevalue=expr.true_case(); - exprt &falsevalue=expr.false_case(); - - bool result = true; - - // we first want to look at the condition - auto r_cond = simplify_rec(cond); - if(r_cond.has_changed()) - { - cond = r_cond.expr; - result = false; - } - - // 1 ? a : b -> a and 0 ? a : b -> b - if(cond.is_constant()) - { - exprt tmp=cond.is_true()?truevalue:falsevalue; - tmp = simplify_rec(tmp); - expr.swap(tmp); - return false; - } - - if(do_simplify_if) - { - if(cond.id()==ID_not) - { - exprt tmp; - tmp.swap(cond.op0()); - cond.swap(tmp); - truevalue.swap(falsevalue); - result=false; - } - -#ifdef USE_LOCAL_REPLACE_MAP - replace_mapt map_before(local_replace_map); - - // a ? b : c --> a ? b[a/true] : c - if(cond.id()==ID_and) - { - forall_operands(it, cond) - { - if(it->id()==ID_not) - local_replace_map.insert( - std::make_pair(it->op0(), false_exprt())); - else - local_replace_map.insert( - std::make_pair(*it, true_exprt())); - } - } - else - local_replace_map.insert(std::make_pair(cond, true_exprt())); - - auto r_truevalue = simplify_rec(truevalue); - if(r_truevalue.has_changed()) - { - truevalue = r_truevalue.expr; - result = false; - } - - local_replace_map=map_before; - - // a ? b : c --> a ? b : c[a/false] - if(cond.id()==ID_or) - { - forall_operands(it, cond) - { - if(it->id()==ID_not) - local_replace_map.insert( - std::make_pair(it->op0(), true_exprt())); - else - local_replace_map.insert( - std::make_pair(*it, false_exprt())); - } - } - else - local_replace_map.insert(std::make_pair(cond, false_exprt())); - - auto r_falsevalue = simplify_rec(falsevalue); - if(r_falsevalue.has_changed()) - { - falsevalue = r_falsevalue.expr; - result = false; - } - - local_replace_map.swap(map_before); -#else - auto r_truevalue = simplify_rec(truevalue); - if(r_truevalue.has_changed()) - { - truevalue = r_truevalue.expr; - result = false; - } - auto r_falsevalue = simplify_rec(falsevalue); - if(r_falsevalue.has_changed()) - { - falsevalue = r_falsevalue.expr; - result = false; - } -#endif - } - else - { - auto r_truevalue = simplify_rec(truevalue); - if(r_truevalue.has_changed()) - { - truevalue = r_truevalue.expr; - result = false; - } - auto r_falsevalue = simplify_rec(falsevalue); - if(r_falsevalue.has_changed()) - { - falsevalue = r_falsevalue.expr; - result = false; - } - } - - return result; -} - -simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr) -{ - const exprt &cond = expr.cond(); - const exprt &truevalue = expr.true_case(); - const exprt &falsevalue = expr.false_case(); - - if(do_simplify_if) - { - #if 0 - result = simplify_if_cond(cond) && result; - result = simplify_if_branch(truevalue, falsevalue, cond) && result; - #endif - - if(expr.type()==bool_typet()) - { - // a?b:c <-> (a && b) || (!a && c) - - if(truevalue.is_true() && falsevalue.is_false()) - { - // a?1:0 <-> a - return cond; - } - else if(truevalue.is_false() && falsevalue.is_true()) - { - // a?0:1 <-> !a - exprt tmp = boolean_negate(cond); - simplify_node(tmp); - return std::move(tmp); - } - else if(falsevalue.is_false()) - { - // a?b:0 <-> a AND b - and_exprt tmp(cond, truevalue); - simplify_node(tmp); - return std::move(tmp); - } - else if(falsevalue.is_true()) - { - // a?b:1 <-> !a OR b - exprt tmp_not_cond = boolean_negate(cond); - simplify_node(tmp_not_cond); - or_exprt tmp(tmp_not_cond, truevalue); - simplify_node(tmp); - 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); - return std::move(tmp); - } - else if(truevalue.is_false()) - { - // a?0:b <-> !a && b - exprt tmp_not_cond = boolean_negate(cond); - simplify_node(tmp_not_cond); - and_exprt tmp(tmp_not_cond, falsevalue); - simplify_node(tmp); - return std::move(tmp); - } - } - } - - if(truevalue==falsevalue) - return truevalue; - - // 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; - exprt truevalue_copy = truevalue; - - 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)) - { - new_expr.operands().push_back( - simplify_if(if_exprt(cond_copy, pair.first, pair.second))); - } - - return std::move(new_expr); - } - - return unchanged(expr); -} - bool simplify_exprt::get_values( const exprt &expr, value_listt &value_list) diff --git a/src/util/simplify_expr_if.cpp b/src/util/simplify_expr_if.cpp new file mode 100644 index 00000000000..217ca6f4c1c --- /dev/null +++ b/src/util/simplify_expr_if.cpp @@ -0,0 +1,420 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "simplify_expr_class.h" + +#include "arith_tools.h" +#include "expr_util.h" +#include "range.h" +#include "std_expr.h" + +bool simplify_exprt::simplify_if_implies( + exprt &expr, + const exprt &cond, + bool truth, + bool &new_truth) +{ + if(expr == cond) + { + new_truth = truth; + return false; + } + + if(truth && cond.id() == ID_lt && expr.id() == ID_lt) + { + if( + cond.op0() == expr.op0() && cond.op1().is_constant() && + expr.op1().is_constant() && cond.op1().type() == expr.op1().type()) + { + mp_integer i1, i2; + + if( + !to_integer(to_constant_expr(cond.op1()), i1) && + !to_integer(to_constant_expr(expr.op1()), i2)) + { + if(i1 >= i2) + { + new_truth = true; + return false; + } + } + } + + if( + cond.op1() == expr.op1() && cond.op0().is_constant() && + expr.op0().is_constant() && cond.op0().type() == expr.op0().type()) + { + mp_integer i1, i2; + + if( + !to_integer(to_constant_expr(cond.op0()), i1) && + !to_integer(to_constant_expr(expr.op0()), i2)) + { + if(i1 <= i2) + { + new_truth = true; + return false; + } + } + } + } + + return true; +} + +bool simplify_exprt::simplify_if_recursive( + exprt &expr, + const exprt &cond, + bool truth) +{ + if(expr.type().id() == ID_bool) + { + bool new_truth; + + if(!simplify_if_implies(expr, cond, truth, new_truth)) + { + if(new_truth) + { + expr = true_exprt(); + return false; + } + else + { + expr = false_exprt(); + return false; + } + } + } + + bool result = true; + + Forall_operands(it, expr) + result = simplify_if_recursive(*it, cond, truth) && result; + + return result; +} + +bool simplify_exprt::simplify_if_conj(exprt &expr, const exprt &cond) +{ + forall_operands(it, cond) + { + if(expr == *it) + { + expr = true_exprt(); + return false; + } + } + + bool result = true; + + Forall_operands(it, expr) + result = simplify_if_conj(*it, cond) && result; + + return result; +} + +bool simplify_exprt::simplify_if_disj(exprt &expr, const exprt &cond) +{ + forall_operands(it, cond) + { + if(expr == *it) + { + expr = false_exprt(); + return false; + } + } + + bool result = true; + + Forall_operands(it, expr) + result = simplify_if_disj(*it, cond) && result; + + return result; +} + +bool simplify_exprt::simplify_if_branch( + exprt &trueexpr, + exprt &falseexpr, + const exprt &cond) +{ + bool tresult = true; + bool fresult = true; + + if(cond.id() == ID_and) + { + tresult = simplify_if_conj(trueexpr, cond) && tresult; + fresult = simplify_if_recursive(falseexpr, cond, false) && fresult; + } + else if(cond.id() == ID_or) + { + tresult = simplify_if_recursive(trueexpr, cond, true) && tresult; + fresult = simplify_if_disj(falseexpr, cond) && fresult; + } + else + { + tresult = simplify_if_recursive(trueexpr, cond, true) && tresult; + fresult = simplify_if_recursive(falseexpr, cond, false) && fresult; + } + + if(!tresult) + trueexpr = simplify_rec(trueexpr); // recursive call + if(!fresult) + falseexpr = simplify_rec(falseexpr); // recursive call + + return tresult && fresult; +} + +bool simplify_exprt::simplify_if_cond(exprt &expr) +{ + bool result = true; + bool tmp = false; + + while(!tmp) + { + tmp = true; + + if(expr.id() == ID_and) + { + if(expr.has_operands()) + { + exprt::operandst &operands = expr.operands(); + for(exprt::operandst::iterator it1 = operands.begin(); + it1 != operands.end(); + it1++) + { + for(exprt::operandst::iterator it2 = operands.begin(); + it2 != operands.end(); + it2++) + { + if(it1 != it2) + tmp = simplify_if_recursive(*it1, *it2, true) && tmp; + } + } + } + } + + if(!tmp) + expr = simplify_rec(expr); // recursive call + + result = tmp && result; + } + + return result; +} + +bool simplify_exprt::simplify_if_preorder(if_exprt &expr) +{ + exprt &cond = expr.cond(); + exprt &truevalue = expr.true_case(); + exprt &falsevalue = expr.false_case(); + + bool result = true; + + // we first want to look at the condition + auto r_cond = simplify_rec(cond); + if(r_cond.has_changed()) + { + cond = r_cond.expr; + result = false; + } + + // 1 ? a : b -> a and 0 ? a : b -> b + if(cond.is_constant()) + { + exprt tmp = cond.is_true() ? truevalue : falsevalue; + tmp = simplify_rec(tmp); + expr.swap(tmp); + return false; + } + + if(do_simplify_if) + { + if(cond.id() == ID_not) + { + exprt tmp; + tmp.swap(cond.op0()); + cond.swap(tmp); + truevalue.swap(falsevalue); + result = false; + } + +#ifdef USE_LOCAL_REPLACE_MAP + replace_mapt map_before(local_replace_map); + + // a ? b : c --> a ? b[a/true] : c + if(cond.id() == ID_and) + { + forall_operands(it, cond) + { + if(it->id() == ID_not) + local_replace_map.insert(std::make_pair(it->op0(), false_exprt())); + else + local_replace_map.insert(std::make_pair(*it, true_exprt())); + } + } + else + local_replace_map.insert(std::make_pair(cond, true_exprt())); + + auto r_truevalue = simplify_rec(truevalue); + if(r_truevalue.has_changed()) + { + truevalue = r_truevalue.expr; + result = false; + } + + local_replace_map = map_before; + + // a ? b : c --> a ? b : c[a/false] + if(cond.id() == ID_or) + { + forall_operands(it, cond) + { + if(it->id() == ID_not) + local_replace_map.insert(std::make_pair(it->op0(), true_exprt())); + else + local_replace_map.insert(std::make_pair(*it, false_exprt())); + } + } + else + local_replace_map.insert(std::make_pair(cond, false_exprt())); + + auto r_falsevalue = simplify_rec(falsevalue); + if(r_falsevalue.has_changed()) + { + falsevalue = r_falsevalue.expr; + result = false; + } + + local_replace_map.swap(map_before); +#else + auto r_truevalue = simplify_rec(truevalue); + if(r_truevalue.has_changed()) + { + truevalue = r_truevalue.expr; + result = false; + } + auto r_falsevalue = simplify_rec(falsevalue); + if(r_falsevalue.has_changed()) + { + falsevalue = r_falsevalue.expr; + result = false; + } +#endif + } + else + { + auto r_truevalue = simplify_rec(truevalue); + if(r_truevalue.has_changed()) + { + truevalue = r_truevalue.expr; + result = false; + } + auto r_falsevalue = simplify_rec(falsevalue); + if(r_falsevalue.has_changed()) + { + falsevalue = r_falsevalue.expr; + result = false; + } + } + + return result; +} + +simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr) +{ + const exprt &cond = expr.cond(); + const exprt &truevalue = expr.true_case(); + const exprt &falsevalue = expr.false_case(); + + if(do_simplify_if) + { +#if 0 + result = simplify_if_cond(cond) && result; + result = simplify_if_branch(truevalue, falsevalue, cond) && result; +#endif + + if(expr.type() == bool_typet()) + { + // a?b:c <-> (a && b) || (!a && c) + + if(truevalue.is_true() && falsevalue.is_false()) + { + // a?1:0 <-> a + return cond; + } + else if(truevalue.is_false() && falsevalue.is_true()) + { + // a?0:1 <-> !a + exprt tmp = boolean_negate(cond); + simplify_node(tmp); + return std::move(tmp); + } + else if(falsevalue.is_false()) + { + // a?b:0 <-> a AND b + and_exprt tmp(cond, truevalue); + simplify_node(tmp); + return std::move(tmp); + } + else if(falsevalue.is_true()) + { + // a?b:1 <-> !a OR b + exprt tmp_not_cond = boolean_negate(cond); + simplify_node(tmp_not_cond); + or_exprt tmp(tmp_not_cond, truevalue); + simplify_node(tmp); + 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); + return std::move(tmp); + } + else if(truevalue.is_false()) + { + // a?0:b <-> !a && b + exprt tmp_not_cond = boolean_negate(cond); + simplify_node(tmp_not_cond); + and_exprt tmp(tmp_not_cond, falsevalue); + simplify_node(tmp); + return std::move(tmp); + } + } + } + + if(truevalue == falsevalue) + return truevalue; + + // 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; + exprt truevalue_copy = truevalue; + + 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)) + { + new_expr.operands().push_back( + simplify_if(if_exprt(cond_copy, pair.first, pair.second))); + } + + return std::move(new_expr); + } + + return unchanged(expr); +} From 37b642cad227acc8ebd082dfd2a73367e6e46d67 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 12:13:14 +0100 Subject: [PATCH 05/18] simplify_expr_if: result -> nochange --- src/util/simplify_expr_if.cpp | 70 +++++++++++++++++------------------ 1 file changed, 35 insertions(+), 35 deletions(-) diff --git a/src/util/simplify_expr_if.cpp b/src/util/simplify_expr_if.cpp index 217ca6f4c1c..e019cff7e34 100644 --- a/src/util/simplify_expr_if.cpp +++ b/src/util/simplify_expr_if.cpp @@ -91,12 +91,12 @@ bool simplify_exprt::simplify_if_recursive( } } - bool result = true; + bool no_change = true; Forall_operands(it, expr) - result = simplify_if_recursive(*it, cond, truth) && result; + no_change = simplify_if_recursive(*it, cond, truth) && no_change; - return result; + return no_change; } bool simplify_exprt::simplify_if_conj(exprt &expr, const exprt &cond) @@ -110,12 +110,12 @@ bool simplify_exprt::simplify_if_conj(exprt &expr, const exprt &cond) } } - bool result = true; + bool no_change = true; Forall_operands(it, expr) - result = simplify_if_conj(*it, cond) && result; + no_change = simplify_if_conj(*it, cond) && no_change; - return result; + return no_change; } bool simplify_exprt::simplify_if_disj(exprt &expr, const exprt &cond) @@ -129,12 +129,12 @@ bool simplify_exprt::simplify_if_disj(exprt &expr, const exprt &cond) } } - bool result = true; + bool no_change = true; Forall_operands(it, expr) - result = simplify_if_disj(*it, cond) && result; + no_change = simplify_if_disj(*it, cond) && no_change; - return result; + return no_change; } bool simplify_exprt::simplify_if_branch( @@ -142,36 +142,36 @@ bool simplify_exprt::simplify_if_branch( exprt &falseexpr, const exprt &cond) { - bool tresult = true; - bool fresult = true; + bool tno_change = true; + bool fno_change = true; if(cond.id() == ID_and) { - tresult = simplify_if_conj(trueexpr, cond) && tresult; - fresult = simplify_if_recursive(falseexpr, cond, false) && fresult; + tno_change = simplify_if_conj(trueexpr, cond) && tno_change; + fno_change = simplify_if_recursive(falseexpr, cond, false) && fno_change; } else if(cond.id() == ID_or) { - tresult = simplify_if_recursive(trueexpr, cond, true) && tresult; - fresult = simplify_if_disj(falseexpr, cond) && fresult; + tno_change = simplify_if_recursive(trueexpr, cond, true) && tno_change; + fno_change = simplify_if_disj(falseexpr, cond) && fno_change; } else { - tresult = simplify_if_recursive(trueexpr, cond, true) && tresult; - fresult = simplify_if_recursive(falseexpr, cond, false) && fresult; + tno_change = simplify_if_recursive(trueexpr, cond, true) && tno_change; + fno_change = simplify_if_recursive(falseexpr, cond, false) && fno_change; } - if(!tresult) + if(!tno_change) trueexpr = simplify_rec(trueexpr); // recursive call - if(!fresult) + if(!fno_change) falseexpr = simplify_rec(falseexpr); // recursive call - return tresult && fresult; + return tno_change && fno_change; } bool simplify_exprt::simplify_if_cond(exprt &expr) { - bool result = true; + bool no_change = true; bool tmp = false; while(!tmp) @@ -201,10 +201,10 @@ bool simplify_exprt::simplify_if_cond(exprt &expr) if(!tmp) expr = simplify_rec(expr); // recursive call - result = tmp && result; + no_change = tmp && no_change; } - return result; + return no_change; } bool simplify_exprt::simplify_if_preorder(if_exprt &expr) @@ -213,14 +213,14 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) exprt &truevalue = expr.true_case(); exprt &falsevalue = expr.false_case(); - bool result = true; + bool no_change = true; // we first want to look at the condition auto r_cond = simplify_rec(cond); if(r_cond.has_changed()) { cond = r_cond.expr; - result = false; + no_change = false; } // 1 ? a : b -> a and 0 ? a : b -> b @@ -240,7 +240,7 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) tmp.swap(cond.op0()); cond.swap(tmp); truevalue.swap(falsevalue); - result = false; + no_change = false; } #ifdef USE_LOCAL_REPLACE_MAP @@ -264,7 +264,7 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) if(r_truevalue.has_changed()) { truevalue = r_truevalue.expr; - result = false; + no_change = false; } local_replace_map = map_before; @@ -287,7 +287,7 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) if(r_falsevalue.has_changed()) { falsevalue = r_falsevalue.expr; - result = false; + no_change = false; } local_replace_map.swap(map_before); @@ -296,13 +296,13 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) if(r_truevalue.has_changed()) { truevalue = r_truevalue.expr; - result = false; + no_change = false; } auto r_falsevalue = simplify_rec(falsevalue); if(r_falsevalue.has_changed()) { falsevalue = r_falsevalue.expr; - result = false; + no_change = false; } #endif } @@ -312,17 +312,17 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr) if(r_truevalue.has_changed()) { truevalue = r_truevalue.expr; - result = false; + no_change = false; } auto r_falsevalue = simplify_rec(falsevalue); if(r_falsevalue.has_changed()) { falsevalue = r_falsevalue.expr; - result = false; + no_change = false; } } - return result; + return no_change; } simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr) @@ -334,8 +334,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr) if(do_simplify_if) { #if 0 - result = simplify_if_cond(cond) && result; - result = simplify_if_branch(truevalue, falsevalue, cond) && result; + no_change = simplify_if_cond(cond) && no_change; + no_change = simplify_if_branch(truevalue, falsevalue, cond) && no_change; #endif if(expr.type() == bool_typet()) From 5d180cbcfa1eee525ed7f0f640b7ba1a35ff002b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 12:54:12 +0100 Subject: [PATCH 06/18] simplify_inequality_* methods use new interface This improves type safety. --- src/util/simplify_expr_class.h | 10 +- src/util/simplify_expr_int.cpp | 302 +++++++++++++---------------- src/util/simplify_expr_pointer.cpp | 36 ++-- 3 files changed, 159 insertions(+), 189 deletions(-) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 709acb7619b..7f916065e35 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -196,11 +196,11 @@ class simplify_exprt static tvt objects_equal(const exprt &a, const exprt &b); static tvt objects_equal_address_of(const exprt &a, const exprt &b); NODISCARD resultt<> simplify_address_of_arg(const exprt &); - bool simplify_inequality_both_constant(exprt &); - bool simplify_inequality_no_constant(exprt &); - bool simplify_inequality_rhs_is_constant(exprt &); - bool simplify_inequality_address_of(exprt &expr); - bool simplify_inequality_pointer_object(exprt &expr); + NODISCARD resultt<> simplify_inequality_both_constant(const exprt &); + NODISCARD resultt<> simplify_inequality_no_constant(const exprt &); + NODISCARD resultt<> simplify_inequality_rhs_is_constant(const exprt &); + NODISCARD resultt<> simplify_inequality_address_of(const exprt &); + NODISCARD resultt<> simplify_inequality_pointer_object(const exprt &); // main recursion bool simplify_node(exprt &expr); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index c04fc1225dc..fea2db0c0e0 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1244,7 +1244,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr) { auto new_expr = expr; new_expr.op0().swap(new_expr.op1()); - return simplify_inequality(new_expr); // recursive call + return changed(simplify_inequality(new_expr)); // recursive call } if(tmp0.id()==ID_if && tmp0.operands().size()==3) @@ -1262,22 +1262,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr) (tmp1.id()==ID_typecast && tmp1.op0().id()==ID_address_of)) && (expr.id()==ID_equal || expr.id()==ID_notequal)) { - exprt tmp = expr; - if(simplify_inequality_address_of(tmp)) - return unchanged(expr); - else - return std::move(tmp); + return simplify_inequality_address_of(expr); } if(tmp0.id()==ID_pointer_object && tmp1.id()==ID_pointer_object && (expr.id()==ID_equal || expr.id()==ID_notequal)) { - exprt tmp = expr; - if(simplify_inequality_pointer_object(tmp)) - return unchanged(expr); - else - return std::move(tmp); + return simplify_inequality_pointer_object(expr); } if(tmp0.type().id()==ID_c_enum_tag) @@ -1292,11 +1284,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr) // are _both_ constant? if(tmp0_const && tmp1_const) { - exprt tmp = expr; - if(simplify_inequality_both_constant(tmp)) - return unchanged(expr); - else - return std::move(tmp); + return simplify_inequality_both_constant(expr); } else if(tmp0_const) { @@ -1316,32 +1304,24 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr) new_expr.op0().swap(new_expr.op1()); // RHS is constant, LHS is not - simplify_inequality_rhs_is_constant(new_expr); - return std::move(new_expr); + return changed(simplify_inequality_rhs_is_constant(new_expr)); } else if(tmp1_const) { // RHS is constant, LHS is not - exprt tmp = expr; - if(simplify_inequality_rhs_is_constant(tmp)) - return unchanged(expr); - else - return std::move(tmp); + return simplify_inequality_rhs_is_constant(expr); } else { // both are not constant - exprt tmp = expr; - if(simplify_inequality_no_constant(tmp)) - return unchanged(expr); - else - return std::move(tmp); + return simplify_inequality_no_constant(expr); } } /// simplifies inequalities for the case in which both sides /// of the inequality are constants -bool simplify_exprt::simplify_inequality_both_constant(exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_inequality_both_constant(const exprt &expr) { PRECONDITION(expr.operands().size() == 2); @@ -1372,12 +1352,11 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr) { // if NULL is not zero on this platform, we really don't know what it // is and therefore cannot simplify - return true; + return unchanged(expr); } equal = tmp0_const.is_zero() && tmp1_const.is_zero(); } - expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal); - return false; + return make_boolean_expr(expr.id() == ID_equal ? equal : !equal); } if(tmp0.type().id() == ID_fixedbv) @@ -1386,17 +1365,15 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr) fixedbvt f1(tmp1_const); if(expr.id() == ID_ge) - expr = make_boolean_expr(f0 >= f1); + return make_boolean_expr(f0 >= f1); else if(expr.id() == ID_le) - expr = make_boolean_expr(f0 <= f1); + return make_boolean_expr(f0 <= f1); else if(expr.id() == ID_gt) - expr = make_boolean_expr(f0 > f1); + return make_boolean_expr(f0 > f1); else if(expr.id() == ID_lt) - expr = make_boolean_expr(f0 < f1); + return make_boolean_expr(f0 < f1); else UNREACHABLE; - - return false; } else if(tmp0.type().id() == ID_floatbv) { @@ -1404,65 +1381,59 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr) ieee_floatt f1(tmp1_const); if(expr.id() == ID_ge) - expr = make_boolean_expr(f0 >= f1); + return make_boolean_expr(f0 >= f1); else if(expr.id() == ID_le) - expr = make_boolean_expr(f0 <= f1); + return make_boolean_expr(f0 <= f1); else if(expr.id() == ID_gt) - expr = make_boolean_expr(f0 > f1); + return make_boolean_expr(f0 > f1); else if(expr.id() == ID_lt) - expr = make_boolean_expr(f0 < f1); + return make_boolean_expr(f0 < f1); else UNREACHABLE; - - return false; } else if(tmp0.type().id() == ID_rational) { rationalt r0, r1; if(to_rational(tmp0, r0)) - return true; + return unchanged(expr); if(to_rational(tmp1, r1)) - return true; + return unchanged(expr); if(expr.id() == ID_ge) - expr = make_boolean_expr(r0 >= r1); + return make_boolean_expr(r0 >= r1); else if(expr.id() == ID_le) - expr = make_boolean_expr(r0 <= r1); + return make_boolean_expr(r0 <= r1); else if(expr.id() == ID_gt) - expr = make_boolean_expr(r0 > r1); + return make_boolean_expr(r0 > r1); else if(expr.id() == ID_lt) - expr = make_boolean_expr(r0 < r1); + return make_boolean_expr(r0 < r1); else UNREACHABLE; - - return false; } else { const auto v0 = numeric_cast(tmp0_const); if(!v0.has_value()) - return true; + return unchanged(expr); const auto v1 = numeric_cast(tmp1_const); if(!v1.has_value()) - return true; + return unchanged(expr); if(expr.id() == ID_ge) - expr = make_boolean_expr(*v0 >= *v1); + return make_boolean_expr(*v0 >= *v1); else if(expr.id() == ID_le) - expr = make_boolean_expr(*v0 <= *v1); + return make_boolean_expr(*v0 <= *v1); else if(expr.id() == ID_gt) - expr = make_boolean_expr(*v0 > *v1); + return make_boolean_expr(*v0 > *v1); else if(expr.id() == ID_lt) - expr = make_boolean_expr(*v0 < *v1); + return make_boolean_expr(*v0 < *v1); else UNREACHABLE; - - return false; } } @@ -1514,50 +1485,53 @@ bool simplify_exprt::eliminate_common_addends( return true; } -bool simplify_exprt::simplify_inequality_no_constant(exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_inequality_no_constant(const exprt &expr) { - exprt::operandst &operands=expr.operands(); - // pretty much all of the simplifications below are unsound // for IEEE float because of NaN! if(expr.op0().type().id() == ID_floatbv) - return true; + return unchanged(expr); // eliminate strict inequalities if(expr.id()==ID_notequal) { - expr.id(ID_equal); - simplify_inequality_no_constant(expr); - expr = boolean_negate(expr); - simplify_node(expr); - return false; + auto new_expr = expr; + new_expr.id(ID_equal); + new_expr = simplify_inequality_no_constant(new_expr); + new_expr = boolean_negate(new_expr); + simplify_node(new_expr); + return std::move(new_expr); } else if(expr.id()==ID_gt) { - expr.id(ID_ge); + auto new_expr = expr; + new_expr.id(ID_ge); // swap operands - expr.op0().swap(expr.op1()); - simplify_inequality_no_constant(expr); - expr = boolean_negate(expr); - simplify_node(expr); - return false; + new_expr.op0().swap(new_expr.op1()); + new_expr = simplify_inequality_no_constant(new_expr); + new_expr = boolean_negate(new_expr); + simplify_node(new_expr); + return std::move(new_expr); } else if(expr.id()==ID_lt) { - expr.id(ID_ge); - simplify_inequality_no_constant(expr); - expr = boolean_negate(expr); - simplify_node(expr); - return false; + auto new_expr = expr; + new_expr.id(ID_ge); + new_expr = simplify_inequality_no_constant(new_expr); + new_expr = boolean_negate(new_expr); + simplify_node(new_expr); + return std::move(new_expr); } else if(expr.id()==ID_le) { - expr.id(ID_ge); + auto new_expr = expr; + new_expr.id(ID_ge); // swap operands - expr.op0().swap(expr.op1()); - simplify_inequality_no_constant(expr); - return false; + new_expr.op0().swap(new_expr.op1()); + new_expr = simplify_inequality_no_constant(new_expr); + return std::move(new_expr); } // now we only have >=, = @@ -1568,11 +1542,8 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr) // syntactically equal? - if(operands.front()==operands.back()) - { - expr=true_exprt(); - return false; - } + if(expr.op0() == expr.op1()) + return true_exprt(); // try constants @@ -1620,8 +1591,7 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr) if(ok) { - expr = make_boolean_expr(result); - return false; + return make_boolean_expr(result); } } @@ -1629,22 +1599,24 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr) // On bit-vectors, this is only sound on '='. if(expr.id()==ID_equal) { - if(!eliminate_common_addends(expr.op0(), expr.op1())) + auto new_expr = expr; + if(!eliminate_common_addends(new_expr.op0(), new_expr.op1())) { // remove zeros - simplify_node(expr.op0()); - simplify_node(expr.op1()); - expr = simplify_inequality(expr); // recursive call - return false; + simplify_node(new_expr.op0()); + simplify_node(new_expr.op1()); + new_expr = simplify_inequality(new_expr); // recursive call + return std::move(new_expr); } } - return true; + return unchanged(expr); } /// \par expr: an inequality where the RHS is a constant /// and the LHS is not -bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr) { // the constant is always on the RHS PRECONDITION(expr.op1().is_constant()); @@ -1652,10 +1624,11 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) if(expr.op0().id()==ID_if && expr.op0().operands().size()==3) { 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()); - expr = simplify_if(if_expr); - return false; + if_expr.true_case() = + simplify_inequality_rhs_is_constant(if_expr.true_case()); + if_expr.false_case() = + simplify_inequality_rhs_is_constant(if_expr.false_case()); + return changed(simplify_if(if_expr)); } // do we deal with pointers? @@ -1663,11 +1636,12 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) { if(expr.id()==ID_notequal) { - expr.id(ID_equal); - simplify_inequality_rhs_is_constant(expr); - expr = boolean_negate(expr); - simplify_node(expr); - return false; + auto new_expr = expr; + new_expr.id(ID_equal); + new_expr = simplify_inequality_rhs_is_constant(new_expr); + new_expr = boolean_negate(new_expr); + simplify_node(new_expr); + return std::move(new_expr); } // very special case for pointers @@ -1687,8 +1661,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) expr.op0().op0().id() == ID_index || expr.op0().op0().id() == ID_string_constant) { - expr=false_exprt(); - return false; + return false_exprt(); } } else if(expr.op0().id()==ID_typecast && @@ -1704,8 +1677,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) expr.op0().op0().op0().id() == ID_index || expr.op0().op0().op0().id() == ID_string_constant) { - expr=false_exprt(); - return false; + return false_exprt(); } } else if(expr.op0().id()==ID_typecast && @@ -1717,18 +1689,18 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) // (type)ptr == NULL -> ptr == NULL // note that 'ptr' may be an integer exprt op=expr.op0().op0(); - expr.op0().swap(op); - if(expr.op0().type().id()!=ID_pointer) - expr.op1()=from_integer(0, expr.op0().type()); + auto new_expr = expr; + new_expr.op0().swap(op); + if(new_expr.op0().type().id() != ID_pointer) + new_expr.op1() = from_integer(0, new_expr.op0().type()); else - expr.op1().type()=expr.op0().type(); - expr = simplify_inequality(expr); // do again! - return false; + new_expr.op1().type() = new_expr.op0().type(); + return changed(simplify_inequality(new_expr)); // do again! } } // all we are doing with pointers - return true; + return unchanged(expr); } // is it a separation predicate? @@ -1740,9 +1712,10 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) if(expr.id()==ID_equal || expr.id()==ID_notequal) { mp_integer constant=0; - bool changed=false; + bool op_changed = false; + auto new_expr = expr; - Forall_operands(it, expr.op0()) + Forall_operands(it, new_expr.op0()) { if(it->is_constant()) { @@ -1751,21 +1724,21 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) { constant+=i; *it=from_integer(0, it->type()); - changed=true; + op_changed = true; } } } - if(changed) + if(op_changed) { // adjust the constant on the RHS - mp_integer i = numeric_cast_v(to_constant_expr(expr.op1())); + mp_integer i = + numeric_cast_v(to_constant_expr(new_expr.op1())); i-=constant; - expr.op1()=from_integer(i, expr.op1().type()); + new_expr.op1() = from_integer(i, new_expr.op1().type()); - expr.op0() = simplify_plus(to_plus_expr(expr.op0())); - expr = simplify_inequality(expr); - return false; + new_expr.op0() = simplify_plus(to_plus_expr(new_expr.op0())); + return changed(simplify_inequality(new_expr)); } } } @@ -1791,8 +1764,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) exprt result=expr; result.op0()=expr.op0().op0(); result.op1()=const_val_converted.to_expr(); - expr.swap(result); - return false; + return std::move(result); } } #endif @@ -1805,11 +1777,11 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) expr.op0().type().id()==ID_unsignedbv) { // zero is always smaller or equal something unsigned - expr=true_exprt(); - return false; + return true_exprt(); } - exprt &operand=expr.op0(); + auto new_expr = expr; + exprt &operand = new_expr.op0(); if(expr.id()==ID_equal) { @@ -1817,11 +1789,13 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) if(operand.id()==ID_unary_minus) { if(operand.operands().size()!=1) - return true; + return unchanged(expr); + exprt tmp; tmp.swap(operand.op0()); operand.swap(tmp); - return false; + + return std::move(new_expr); } else if(operand.id()==ID_plus) { @@ -1841,8 +1815,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) tmp.operands().resize(2); tmp.op0().swap(operand.op0()); tmp.op1().swap(operand.op1().op0()); - expr.swap(tmp); - return false; + return std::move(tmp); } } } @@ -1857,15 +1830,13 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) // we re-write (TYPE)boolean == 0 -> !boolean if(expr.op1().is_zero() && expr.id()==ID_equal) { - expr = boolean_negate(expr.op0().op0()); - return false; + return boolean_negate(expr.op0().op0()); } // we re-write (TYPE)boolean != 0 -> boolean if(expr.op1().is_zero() && expr.id()==ID_notequal) { - expr=expr.op0().op0(); - return false; + return expr.op0().op0(); } } @@ -1879,11 +1850,12 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) if(expr.id()==ID_notequal) { - expr.id(ID_equal); - simplify_inequality_rhs_is_constant(expr); - expr = boolean_negate(expr); - simplify_node(expr); - return false; + auto new_expr = expr; + new_expr.id(ID_equal); + new_expr = simplify_inequality_rhs_is_constant(new_expr); + new_expr = boolean_negate(new_expr); + simplify_node(new_expr); + return std::move(new_expr); } else if(expr.id()==ID_gt) { @@ -1891,23 +1863,23 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) if(i==max) { - expr=false_exprt(); - return false; + return false_exprt(); } - expr.id(ID_ge); + auto new_expr = expr; + new_expr.id(ID_ge); ++i; - expr.op1()=from_integer(i, expr.op1().type()); - simplify_inequality_rhs_is_constant(expr); - return false; + new_expr.op1() = from_integer(i, new_expr.op1().type()); + return changed(simplify_inequality_rhs_is_constant(new_expr)); } else if(expr.id()==ID_lt) { - expr.id(ID_ge); - simplify_inequality_rhs_is_constant(expr); - expr = boolean_negate(expr); - simplify_node(expr); - return false; + auto new_expr = expr; + new_expr.id(ID_ge); + new_expr = simplify_inequality_rhs_is_constant(new_expr); + new_expr = boolean_negate(new_expr); + simplify_node(new_expr); + return std::move(new_expr); } else if(expr.id()==ID_le) { @@ -1915,19 +1887,19 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr) if(i==max) { - expr=true_exprt(); - return false; + return true_exprt(); } - expr.id(ID_ge); + auto new_expr = expr; + new_expr.id(ID_ge); ++i; - expr.op1()=from_integer(i, expr.op1().type()); - simplify_inequality_rhs_is_constant(expr); - expr = boolean_negate(expr); - simplify_node(expr); - return false; + new_expr.op1() = from_integer(i, new_expr.op1().type()); + new_expr = simplify_inequality_rhs_is_constant(new_expr); + new_expr = boolean_negate(new_expr); + simplify_node(new_expr); + return std::move(new_expr); } } #endif - return true; + return unchanged(expr); } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 2dc11ff6a34..a59eda81b5c 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -434,7 +434,8 @@ simplify_exprt::simplify_pointer_offset(const exprt &expr) return unchanged(expr); } -bool simplify_exprt::simplify_inequality_address_of(exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_inequality_address_of(const exprt &expr) { PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal); PRECONDITION(expr.type().id() == ID_bool); @@ -457,9 +458,9 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr) INVARIANT(tmp1.id() == ID_address_of, "id must be ID_address_of"); if(tmp0.operands().size()!=1) - return true; + return unchanged(expr); if(tmp1.operands().size()!=1) - return true; + return unchanged(expr); if(tmp0.op0().id()==ID_symbol && tmp1.op0().id()==ID_symbol) @@ -467,9 +468,7 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr) bool equal = to_symbol_expr(tmp0.op0()).get_identifier() == to_symbol_expr(tmp1.op0()).get_identifier(); - expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal); - - return false; + return make_boolean_expr(expr.id() == ID_equal ? equal : !equal); } else if( tmp0.op0().id() == ID_dynamic_object && @@ -478,23 +477,20 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr) bool equal = to_dynamic_object_expr(tmp0.op0()).get_instance() == to_dynamic_object_expr(tmp1.op0()).get_instance(); - expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal); - - return false; + return make_boolean_expr(expr.id() == ID_equal ? equal : !equal); } else if( (tmp0.op0().id() == ID_symbol && tmp1.op0().id() == ID_dynamic_object) || (tmp0.op0().id() == ID_dynamic_object && tmp1.op0().id() == ID_symbol)) { - expr = make_boolean_expr(expr.id() != ID_equal); - - return false; + return make_boolean_expr(expr.id() != ID_equal); } - return true; + return unchanged(expr); } -bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_inequality_pointer_object(const exprt &expr) { PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal); PRECONDITION(expr.type().id() == ID_bool); @@ -515,12 +511,12 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) (op.op0().id() != ID_symbol && op.op0().id() != ID_dynamic_object && op.op0().id() != ID_string_constant)) { - return true; + return unchanged(expr); } } else if(op.id() != ID_constant || !op.is_zero()) { - return true; + return unchanged(expr); } if(new_inequality_ops.empty()) @@ -533,9 +529,11 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) } } - expr.operands() = std::move(new_inequality_ops); - expr = simplify_inequality(expr); - return false; + auto new_expr = expr; + + new_expr.operands() = std::move(new_inequality_ops); + + return changed(simplify_inequality(new_expr)); } simplify_exprt::resultt<> From db75bb77750611307eacf34e660ec2329caab4d7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 13:28:50 +0100 Subject: [PATCH 07/18] type simplify_sign This improves memory safety. --- src/util/simplify_expr.cpp | 15 ++++++--------- src/util/simplify_expr_class.h | 3 ++- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index c8f8c6a73fc..bc0648abbc8 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -103,24 +103,21 @@ simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr) return unchanged(expr); } -simplify_exprt::resultt<> simplify_exprt::simplify_sign(const exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - - if(expr.op0().is_constant()) + if(expr.op().is_constant()) { - const typet &type = expr.op0().type(); + const typet &type = expr.op().type(); if(type.id()==ID_floatbv) { - ieee_floatt value(to_constant_expr(expr.op0())); + ieee_floatt value(to_constant_expr(expr.op())); return make_boolean_expr(value.get_sign()); } else if(type.id()==ID_signedbv || type.id()==ID_unsignedbv) { - const auto value = numeric_cast(expr.op0()); + const auto value = numeric_cast(expr.op()); if(value.has_value()) { return make_boolean_expr(*value >= 0); @@ -2389,7 +2386,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_sign) { - r = simplify_sign(expr); + r = simplify_sign(to_sign_expr(expr)); } else if(expr.id() == ID_popcount) { diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 7f916065e35..8b50a0f703e 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -50,6 +50,7 @@ class namespacet; class plus_exprt; class popcount_exprt; class refined_string_exprt; +class sign_exprt; class tvt; class typecast_exprt; class unary_exprt; @@ -175,7 +176,7 @@ class simplify_exprt NODISCARD resultt<> simplify_isnan(const unary_exprt &); NODISCARD resultt<> simplify_isnormal(const unary_exprt &); NODISCARD resultt<> simplify_abs(const abs_exprt &); - NODISCARD resultt<> simplify_sign(const exprt &); + NODISCARD resultt<> simplify_sign(const sign_exprt &); NODISCARD resultt<> simplify_popcount(const popcount_exprt &); NODISCARD resultt<> simplify_complex(const exprt &); From b42d47d914136309ea52c6798d0a675ba75c0509 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 13:31:23 +0100 Subject: [PATCH 08/18] type simplify_extractbit This improves memory safety. --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_class.h | 3 ++- src/util/simplify_expr_int.cpp | 15 ++++++--------- 3 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index bc0648abbc8..83e5058f9a1 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2349,7 +2349,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_extractbit) { - r = simplify_extractbit(expr); + r = simplify_extractbit(to_extractbit_expr(expr)); } else if(expr.id()==ID_concatenation) { diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 8b50a0f703e..42ac9a01396 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -36,6 +36,7 @@ class byte_update_exprt; class dereference_exprt; class div_exprt; class exprt; +class extractbit_exprt; class extractbits_exprt; class floatbv_typecast_exprt; class function_application_exprt; @@ -130,7 +131,7 @@ class simplify_exprt // These below all return 'true' if the simplification wasn't applicable. // If false is returned, the expression has changed. NODISCARD resultt<> simplify_typecast(const typecast_exprt &); - NODISCARD resultt<> simplify_extractbit(const exprt &); + NODISCARD resultt<> simplify_extractbit(const extractbit_exprt &); NODISCARD resultt<> simplify_extractbits(const extractbits_exprt &); NODISCARD resultt<> simplify_concatenation(const exprt &); NODISCARD resultt<> simplify_mult(const mult_exprt &); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index fea2db0c0e0..70d547f428c 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -771,20 +771,17 @@ simplify_exprt::resultt<> simplify_exprt::simplify_bitwise(const exprt &expr) return std::move(new_expr); } -simplify_exprt::resultt<> simplify_exprt::simplify_extractbit(const exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_extractbit(const extractbit_exprt &expr) { - PRECONDITION(expr.id() == ID_extractbit); - const auto &extractbit_expr = to_extractbit_expr(expr); - - const typet &src_type = extractbit_expr.src().type(); + const typet &src_type = expr.src().type(); if(!is_bitvector_type(src_type)) return unchanged(expr); const std::size_t src_bit_width = to_bitvector_type(src_type).get_width(); - const auto index_converted_to_int = - numeric_cast(extractbit_expr.index()); + const auto index_converted_to_int = numeric_cast(expr.index()); if( !index_converted_to_int.has_value() || *index_converted_to_int < 0 || *index_converted_to_int >= src_bit_width) @@ -792,11 +789,11 @@ simplify_exprt::resultt<> simplify_exprt::simplify_extractbit(const exprt &expr) return unchanged(expr); } - if(!extractbit_expr.src().is_constant()) + if(!expr.src().is_constant()) return unchanged(expr); const bool bit = get_bvrep_bit( - to_constant_expr(extractbit_expr.src()).get_value(), + to_constant_expr(expr.src()).get_value(), src_bit_width, numeric_cast_v(*index_converted_to_int)); From 866acc9a0a9d7fae9ee51a8fbf43086af496e594 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 13:34:44 +0100 Subject: [PATCH 09/18] type simplify_bitnot This improves memory safety. --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_class.h | 3 ++- src/util/simplify_expr_int.cpp | 10 +++------- 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 83e5058f9a1..a518239e321 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2278,7 +2278,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_bitnot) { - r = simplify_bitnot(expr); + r = simplify_bitnot(to_bitnot_expr(expr)); } else if(expr.id()==ID_bitand || expr.id()==ID_bitor || diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 42ac9a01396..66f5409e9ba 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -30,6 +30,7 @@ class abs_exprt; class address_of_exprt; class array_exprt; class binary_relation_exprt; +class bitnot_exprt; class bswap_exprt; class byte_extract_exprt; class byte_update_exprt; @@ -146,7 +147,7 @@ class simplify_exprt NODISCARD resultt<> simplify_bitwise(const exprt &); bool simplify_if_preorder(if_exprt &expr); NODISCARD resultt<> simplify_if(const if_exprt &); - NODISCARD resultt<> simplify_bitnot(const exprt &); + NODISCARD resultt<> simplify_bitnot(const bitnot_exprt &); NODISCARD resultt<> simplify_not(const exprt &); NODISCARD resultt<> simplify_boolean(const exprt &); NODISCARD resultt<> simplify_inequality(const exprt &); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 70d547f428c..246adeb8694 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1182,14 +1182,10 @@ simplify_exprt::simplify_unary_minus(const exprt &expr) return unchanged(expr); } -simplify_exprt::resultt<> simplify_exprt::simplify_bitnot(const exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_bitnot(const bitnot_exprt &expr) { - const exprt::operandst &operands = expr.operands(); - - if(operands.size()!=1) - return unchanged(expr); - - const exprt &op = operands.front(); + const exprt &op = expr.op(); const auto &type = expr.type(); From d061aaa1892f7924c62c6cc04ad79ba4f873533a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 13:36:18 +0100 Subject: [PATCH 10/18] type simplify_not This improves memory safety. --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_boolean.cpp | 7 ++----- src/util/simplify_expr_class.h | 3 ++- 3 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index a518239e321..09b31c4215e 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2327,7 +2327,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_not) { - r = simplify_not(expr); + r = simplify_not(to_not_expr(expr)); } else if(expr.id()==ID_implies || expr.id()==ID_or || expr.id()==ID_xor || diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 5bcf4678e68..03d54e1d2c1 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -164,12 +164,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) return unchanged(expr); } -simplify_exprt::resultt<> simplify_exprt::simplify_not(const exprt &expr) +simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - - const exprt &op = expr.op0(); + const exprt &op = expr.op(); if(expr.type().id()!=ID_bool || op.type().id()!=ID_bool) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 66f5409e9ba..d4fbcbe9ee4 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -49,6 +49,7 @@ class minus_exprt; class mod_exprt; class mult_exprt; class namespacet; +class not_exprt; class plus_exprt; class popcount_exprt; class refined_string_exprt; @@ -148,7 +149,7 @@ class simplify_exprt bool simplify_if_preorder(if_exprt &expr); NODISCARD resultt<> simplify_if(const if_exprt &); NODISCARD resultt<> simplify_bitnot(const bitnot_exprt &); - NODISCARD resultt<> simplify_not(const exprt &); + NODISCARD resultt<> simplify_not(const not_exprt &); NODISCARD resultt<> simplify_boolean(const exprt &); NODISCARD resultt<> simplify_inequality(const exprt &); NODISCARD resultt<> From 1d532960ef94ec2d14470d55d471de206d672bc5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 13:44:17 +0100 Subject: [PATCH 11/18] type simplify_index This improves memory safety. --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_array.cpp | 29 ++++++++++++++--------------- src/util/simplify_expr_class.h | 2 +- 3 files changed, 16 insertions(+), 17 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 09b31c4215e..9c66d36844a 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2232,7 +2232,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_index) { - r = simplify_index(expr); + r = simplify_index(to_index_expr(expr)); } else if(expr.id()==ID_member) { diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp index 949aae389e5..67c10c854cb 100644 --- a/src/util/simplify_expr_array.cpp +++ b/src/util/simplify_expr_array.cpp @@ -15,16 +15,17 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_expr.h" #include "string_constant.h" -simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_index(const index_exprt &expr) { bool no_change = true; // copy - auto index_expr = to_index_expr(expr); + auto new_expr = expr; // references - auto &index = index_expr.index(); - auto &array = index_expr.array(); + auto &index = new_expr.index(); + auto &array = new_expr.array(); // extra arithmetic optimizations @@ -35,16 +36,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) index.op0().operands().size()==2 && index.op0().op1()==index.op1()) { - exprt tmp=index.op0().op0(); - index = tmp; + index = index.op0().op0(); no_change = false; } else if(index.op0().id()==ID_mult && index.op0().operands().size()==2 && index.op0().op0()==index.op1()) { - exprt tmp=index.op0().op1(); - index = tmp; + index = index.op0().op1(); no_change = false; } } @@ -85,8 +84,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) exprt equality_expr = simplify_inequality(equal_exprt(index, rhs_casted)); - exprt new_index_expr = simplify_index(index_exprt( - with_expr.old(), index, index_expr.type())); // recursive call + exprt new_index_expr = simplify_index( + index_exprt(with_expr.old(), index, new_expr.type())); // recursive call if(equality_expr.is_true()) { @@ -98,7 +97,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) } if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr); - return simplify_if(if_expr).expr; + return changed(simplify_if(if_expr)); } } else if( @@ -138,7 +137,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) // terminating zero? const char v = (*i == value.size()) ? 0 : value[numeric_cast_v(*i)]; - return from_integer(v, index_expr.type()); + return from_integer(v, new_expr.type()); } } else if(array.id()==ID_array_of) @@ -198,14 +197,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr) index_exprt idx_false=to_index_expr(expr); idx_false.array()=if_expr.false_case(); - index_expr.array() = if_expr.true_case(); + new_expr.array() = if_expr.true_case(); - exprt result = if_exprt(cond, index_expr, idx_false, expr.type()); + exprt result = if_exprt(cond, new_expr, idx_false, expr.type()); return changed(simplify_rec(result)); } if(no_change) return unchanged(expr); else - return std::move(index_expr); + return std::move(new_expr); } diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index d4fbcbe9ee4..ab49c8ef685 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -157,7 +157,7 @@ class simplify_exprt NODISCARD resultt<> simplify_lambda(const exprt &); NODISCARD resultt<> simplify_with(const exprt &); NODISCARD resultt<> simplify_update(const exprt &); - NODISCARD resultt<> simplify_index(const exprt &); + NODISCARD resultt<> simplify_index(const index_exprt &); NODISCARD resultt<> simplify_member(const exprt &); NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &); NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &); From 7fe45614b701787998cd9063ab7360cfb83b105d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 13:47:21 +0100 Subject: [PATCH 12/18] type simplify_member This improves memory safety. --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_class.h | 2 +- src/util/simplify_expr_struct.cpp | 18 ++++++++---------- 3 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 9c66d36844a..cf5136b80db 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2236,7 +2236,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_member) { - r = simplify_member(expr); + r = simplify_member(to_member_expr(expr)); } else if(expr.id()==ID_byte_update_little_endian || expr.id()==ID_byte_update_big_endian) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index ab49c8ef685..226e4600000 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -158,7 +158,7 @@ class simplify_exprt NODISCARD resultt<> simplify_with(const exprt &); NODISCARD resultt<> simplify_update(const exprt &); NODISCARD resultt<> simplify_index(const index_exprt &); - NODISCARD resultt<> simplify_member(const exprt &); + NODISCARD resultt<> simplify_member(const member_exprt &); NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &); NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &); NODISCARD resultt<> simplify_pointer_object(const exprt &); diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index ca7b94313b7..4e19c95b93a 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -15,15 +15,13 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_offset_size.h" #include "std_expr.h" -simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_member(const member_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - const irep_idt &component_name= to_member_expr(expr).get_component_name(); - const exprt &op = expr.op0(); + const exprt &op = expr.compound(); const typet &op_type=ns.follow(op.type()); if(op.id()==ID_with) @@ -60,9 +58,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) DATA_INVARIANT(new_operands.size() == 1, "post-condition of loop"); auto new_member_expr = expr; - new_member_expr.op0() = new_operands.front(); + new_member_expr.struct_op() = new_operands.front(); // do this recursively - return simplify_member(new_member_expr); + return changed(simplify_member(new_member_expr)); } else if(op_type.id()==ID_union) { @@ -104,7 +102,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) { // UPDATE(s, .m1, v).m2 -> s.m2 auto new_expr = expr; - new_expr.op0() = update_expr.old(); + new_expr.struct_op() = update_expr.old(); // do this recursively return changed(simplify_rec(new_expr)); @@ -211,8 +209,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_member(const exprt &expr) if(op_type == op.op0().type()) { auto new_expr = expr; - new_expr.op0() = op.op0(); - return simplify_member(new_expr); + new_expr.struct_op() = op.op0(); + return changed(simplify_member(new_expr)); } // Try to translate into an equivalent member (perhaps nested) of the type From fddeaf9cf1ce1c92a5378acec767f49bd27ae4f4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 13:51:54 +0100 Subject: [PATCH 13/18] type simplify_unary_minus This improves memory safety. --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_class.h | 3 ++- src/util/simplify_expr_int.cpp | 23 +++++++++-------------- 3 files changed, 12 insertions(+), 16 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index cf5136b80db..4963fd7e6ad 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2319,7 +2319,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_unary_minus) { - r = simplify_unary_minus(expr); + r = simplify_unary_minus(to_unary_minus_expr(expr)); } else if(expr.id()==ID_unary_plus) { diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 226e4600000..e70d8d285cb 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -57,6 +57,7 @@ class sign_exprt; class tvt; class typecast_exprt; class unary_exprt; +class unary_minus_exprt; #define forall_value_list(it, value_list) \ for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \ @@ -169,7 +170,7 @@ class simplify_exprt NODISCARD resultt<> simplify_same_object(const exprt &); NODISCARD resultt<> simplify_good_pointer(const exprt &); NODISCARD resultt<> simplify_object(const exprt &); - NODISCARD resultt<> simplify_unary_minus(const exprt &); + NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &); NODISCARD resultt<> simplify_unary_plus(const exprt &); NODISCARD resultt<> simplify_dereference(const dereference_exprt &); NODISCARD resultt<> simplify_address_of(const address_of_exprt &); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 246adeb8694..ee2b874342e 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1118,15 +1118,12 @@ simplify_exprt::resultt<> simplify_exprt::simplify_unary_plus(const exprt &expr) } simplify_exprt::resultt<> -simplify_exprt::simplify_unary_minus(const exprt &expr) +simplify_exprt::simplify_unary_minus(const unary_minus_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - if(!is_number(expr.type())) return unchanged(expr); - const exprt &operand = expr.op0(); + const exprt &operand = expr.op(); if(expr.type()!=operand.type()) return unchanged(expr); @@ -1134,23 +1131,21 @@ simplify_exprt::simplify_unary_minus(const exprt &expr) if(operand.id()==ID_unary_minus) { // cancel out "-(-x)" to "x" - if(operand.operands().size()!=1) - return unchanged(expr); - - if(!is_number(operand.op0().type())) + if(!is_number(to_unary_minus_expr(operand).op().type())) return unchanged(expr); - return expr.op0().op0(); + return to_unary_minus_expr(operand).op(); } else if(operand.id()==ID_constant) { const irep_idt &type_id=expr.type().id(); + const auto &constant_expr = to_constant_expr(operand); if(type_id==ID_integer || type_id==ID_signedbv || type_id==ID_unsignedbv) { - const auto int_value = numeric_cast(expr.op0()); + const auto int_value = numeric_cast(constant_expr); if(!int_value.has_value()) return unchanged(expr); @@ -1160,20 +1155,20 @@ simplify_exprt::simplify_unary_minus(const exprt &expr) else if(type_id==ID_rational) { rationalt r; - if(to_rational(expr.op0(), r)) + if(to_rational(constant_expr, r)) return unchanged(expr); return from_rational(-r); } else if(type_id==ID_fixedbv) { - fixedbvt f(to_constant_expr(expr.op0())); + fixedbvt f(constant_expr); f.negate(); return f.to_expr(); } else if(type_id==ID_floatbv) { - ieee_floatt f(to_constant_expr(expr.op0())); + ieee_floatt f(constant_expr); f.negate(); return f.to_expr(); } From be1f6fa7dd2d553bd26b541770174d36d1a9b23e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 7 Jul 2019 14:00:56 +0100 Subject: [PATCH 14/18] simplifier: type remaining methods for unary expressions This improves memory safety. --- src/util/simplify_expr.cpp | 15 ++++++------ src/util/simplify_expr_class.h | 16 ++++++------- src/util/simplify_expr_int.cpp | 8 +++---- src/util/simplify_expr_pointer.cpp | 38 +++++++++++------------------- 4 files changed, 33 insertions(+), 44 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 4963fd7e6ad..405c1fc0b98 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2136,7 +2136,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) return unchanged(expr); } -simplify_exprt::resultt<> simplify_exprt::simplify_complex(const exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_complex(const unary_exprt &expr) { if(expr.id() == ID_complex_real) { @@ -2250,7 +2251,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_pointer_object) { - r = simplify_pointer_object(expr); + r = simplify_pointer_object(to_unary_expr(expr)); } else if(expr.id() == ID_is_dynamic_object) { @@ -2262,11 +2263,11 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_object_size) { - r = simplify_object_size(expr); + r = simplify_object_size(to_unary_expr(expr)); } else if(expr.id()==ID_good_pointer) { - r = simplify_good_pointer(expr); + r = simplify_good_pointer(to_unary_expr(expr)); } else if(expr.id()==ID_div) { @@ -2323,7 +2324,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_unary_plus) { - r = simplify_unary_plus(expr); + r = simplify_unary_plus(to_unary_expr(expr)); } else if(expr.id()==ID_not) { @@ -2345,7 +2346,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_pointer_offset) { - r = simplify_pointer_offset(expr); + r = simplify_pointer_offset(to_unary_expr(expr)); } else if(expr.id()==ID_extractbit) { @@ -2398,7 +2399,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag) { - r = simplify_complex(expr); + r = simplify_complex(to_unary_expr(expr)); } if(r.has_changed()) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index e70d8d285cb..446aaf71fdd 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -162,19 +162,19 @@ class simplify_exprt NODISCARD resultt<> simplify_member(const member_exprt &); NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &); NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &); - NODISCARD resultt<> simplify_pointer_object(const exprt &); - NODISCARD resultt<> simplify_object_size(const exprt &); - NODISCARD resultt<> simplify_dynamic_size(const exprt &); + NODISCARD resultt<> simplify_pointer_object(const unary_exprt &); + NODISCARD resultt<> simplify_object_size(const unary_exprt &); + NODISCARD resultt<> simplify_dynamic_size(const unary_exprt &); NODISCARD resultt<> simplify_is_dynamic_object(const exprt &expr); NODISCARD resultt<> simplify_is_invalid_pointer(const exprt &expr); - NODISCARD resultt<> simplify_same_object(const exprt &); - NODISCARD resultt<> simplify_good_pointer(const exprt &); + NODISCARD resultt<> simplify_same_object(const unary_exprt &); + NODISCARD resultt<> simplify_good_pointer(const unary_exprt &); NODISCARD resultt<> simplify_object(const exprt &); NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &); - NODISCARD resultt<> simplify_unary_plus(const exprt &); + NODISCARD resultt<> simplify_unary_plus(const unary_exprt &); NODISCARD resultt<> simplify_dereference(const dereference_exprt &); NODISCARD resultt<> simplify_address_of(const address_of_exprt &); - NODISCARD resultt<> simplify_pointer_offset(const exprt &); + NODISCARD resultt<> simplify_pointer_offset(const unary_exprt &); NODISCARD resultt<> simplify_bswap(const bswap_exprt &); NODISCARD resultt<> simplify_isinf(const unary_exprt &); NODISCARD resultt<> simplify_isnan(const unary_exprt &); @@ -182,7 +182,7 @@ class simplify_exprt NODISCARD resultt<> simplify_abs(const abs_exprt &); NODISCARD resultt<> simplify_sign(const sign_exprt &); NODISCARD resultt<> simplify_popcount(const popcount_exprt &); - NODISCARD resultt<> simplify_complex(const exprt &); + NODISCARD resultt<> simplify_complex(const unary_exprt &); /// Attempt to simplify mathematical function applications if we have /// enough information to do so. Currently focused on constant comparisons. diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index ee2b874342e..3d41cba8ebe 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1108,13 +1108,11 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) return unchanged(expr); } -simplify_exprt::resultt<> simplify_exprt::simplify_unary_plus(const exprt &expr) +simplify_exprt::resultt<> +simplify_exprt::simplify_unary_plus(const unary_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - // simply remove, this is always 'nop' - return expr.op0(); + return expr.op(); } simplify_exprt::resultt<> diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index a59eda81b5c..a9bf5919bcc 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -244,18 +244,17 @@ simplify_exprt::simplify_address_of(const address_of_exprt &expr) } simplify_exprt::resultt<> -simplify_exprt::simplify_pointer_offset(const exprt &expr) +simplify_exprt::simplify_pointer_offset(const unary_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - - const exprt &ptr = expr.op0(); + const exprt &ptr = expr.op(); if(ptr.id()==ID_if && ptr.operands().size()==3) { 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()); + if_expr.true_case() = + simplify_pointer_offset(to_unary_expr(if_expr.true_case())); + if_expr.false_case() = + simplify_pointer_offset(to_unary_expr(if_expr.false_case())); return changed(simplify_if(if_expr)); } @@ -284,7 +283,7 @@ simplify_exprt::simplify_pointer_offset(const exprt &expr) // Cast from pointer to pointer. // This just passes through, remove typecast. auto new_expr = expr; - new_expr.op0() = ptr.op0(); + new_expr.op() = ptr.op0(); simplify_node(new_expr); // recursive call return new_expr; @@ -537,12 +536,9 @@ simplify_exprt::simplify_inequality_pointer_object(const exprt &expr) } simplify_exprt::resultt<> -simplify_exprt::simplify_pointer_object(const exprt &expr) +simplify_exprt::simplify_pointer_object(const unary_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - - const exprt &op = expr.op0(); + const exprt &op = expr.op(); auto op_result = simplify_object(op); @@ -564,7 +560,7 @@ simplify_exprt::simplify_pointer_object(const exprt &expr) if(op_result.has_changed()) { auto new_expr = expr; - new_expr.op0() = op_result; + new_expr.op() = op_result; return std::move(new_expr); } else @@ -714,14 +710,11 @@ tvt simplify_exprt::objects_equal_address_of(const exprt &a, const exprt &b) } simplify_exprt::resultt<> -simplify_exprt::simplify_object_size(const exprt &expr) +simplify_exprt::simplify_object_size(const unary_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - auto new_expr = expr; bool no_change = true; - exprt &op = new_expr.op0(); + exprt &op = new_expr.op(); auto op_result = simplify_object(op); if(op_result.has_changed()) @@ -766,13 +759,10 @@ simplify_exprt::simplify_object_size(const exprt &expr) } simplify_exprt::resultt<> -simplify_exprt::simplify_good_pointer(const exprt &expr) +simplify_exprt::simplify_good_pointer(const unary_exprt &expr) { - if(expr.operands().size()!=1) - return unchanged(expr); - // we expand the definition - exprt def=good_pointer_def(expr.op0(), ns); + exprt def = good_pointer_def(expr.op(), ns); // recursive call simplify_node(def); From 488e4ef113344a12d90a49505d971ae5e323cc2d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 13 Jul 2019 06:34:04 -0400 Subject: [PATCH 15/18] type simplify_concatenation This improves type safety. --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_class.h | 3 ++- src/util/simplify_expr_int.cpp | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 405c1fc0b98..919431020d1 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2354,7 +2354,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_concatenation) { - r = simplify_concatenation(expr); + r = simplify_concatenation(to_concatenation_expr(expr)); } else if(expr.id()==ID_extractbits) { diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 446aaf71fdd..c10a11218e7 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -34,6 +34,7 @@ class bitnot_exprt; class bswap_exprt; class byte_extract_exprt; class byte_update_exprt; +class concatenation_exprt; class dereference_exprt; class div_exprt; class exprt; @@ -136,7 +137,7 @@ class simplify_exprt NODISCARD resultt<> simplify_typecast(const typecast_exprt &); NODISCARD resultt<> simplify_extractbit(const extractbit_exprt &); NODISCARD resultt<> simplify_extractbits(const extractbits_exprt &); - NODISCARD resultt<> simplify_concatenation(const exprt &); + NODISCARD resultt<> simplify_concatenation(const concatenation_exprt &); NODISCARD resultt<> simplify_mult(const mult_exprt &); NODISCARD resultt<> simplify_div(const div_exprt &); NODISCARD resultt<> simplify_mod(const mod_exprt &); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 3d41cba8ebe..a1cd0270b91 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -801,7 +801,7 @@ simplify_exprt::simplify_extractbit(const extractbit_exprt &expr) } simplify_exprt::resultt<> -simplify_exprt::simplify_concatenation(const exprt &expr) +simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) { bool no_change = true; From 2099dfef2c6a9d84314b2f01ff8c0741db6e60f5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 13 Jul 2019 06:36:29 -0400 Subject: [PATCH 16/18] type simplify_unary_plus This improves type safety. --- src/util/simplify_expr.cpp | 2 +- src/util/simplify_expr_class.h | 3 ++- src/util/simplify_expr_int.cpp | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 919431020d1..7d81fef9756 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2324,7 +2324,7 @@ bool simplify_exprt::simplify_node(exprt &expr) } else if(expr.id()==ID_unary_plus) { - r = simplify_unary_plus(to_unary_expr(expr)); + r = simplify_unary_plus(to_unary_plus_expr(expr)); } else if(expr.id()==ID_not) { diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index c10a11218e7..fabeef6114c 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -59,6 +59,7 @@ class tvt; class typecast_exprt; class unary_exprt; class unary_minus_exprt; +class unary_plus_exprt; #define forall_value_list(it, value_list) \ for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \ @@ -172,7 +173,7 @@ class simplify_exprt NODISCARD resultt<> simplify_good_pointer(const unary_exprt &); NODISCARD resultt<> simplify_object(const exprt &); NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &); - NODISCARD resultt<> simplify_unary_plus(const unary_exprt &); + NODISCARD resultt<> simplify_unary_plus(const unary_plus_exprt &); NODISCARD resultt<> simplify_dereference(const dereference_exprt &); NODISCARD resultt<> simplify_address_of(const address_of_exprt &); NODISCARD resultt<> simplify_pointer_offset(const unary_exprt &); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index a1cd0270b91..cd4aed6d928 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1109,7 +1109,7 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) } simplify_exprt::resultt<> -simplify_exprt::simplify_unary_plus(const unary_exprt &expr) +simplify_exprt::simplify_unary_plus(const unary_plus_exprt &expr) { // simply remove, this is always 'nop' return expr.op(); From 16e18d22e9c69b581ec8cf75df66dd93c34c0a43 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 13 Jul 2019 06:38:41 -0400 Subject: [PATCH 17/18] removed unneeded call to simplify_node in simplify_boolean Follow-up from comment in #4872. The call is a no-op. --- src/util/simplify_expr_boolean.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 03d54e1d2c1..74eead1c515 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -40,7 +40,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) auto new_expr = expr; new_expr.id(ID_or); new_expr.op0() = boolean_negate(new_expr.op0()); - simplify_node(new_expr.op0()); simplify_node(new_expr); return std::move(new_expr); } From 412754c2f861d905195417ab72e9e27bb252c93c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 13 Jul 2019 06:42:29 -0400 Subject: [PATCH 18/18] improved typing in simplify_boolean This improves type safety. --- src/util/simplify_expr_boolean.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 74eead1c515..35f30f7d528 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -27,17 +27,18 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) if(expr.id()==ID_implies) { + const auto &implies_expr = to_implies_expr(expr); + if( - expr.operands().size() != 2 || - expr.operands().front().type().id() != ID_bool || - expr.operands().back().type().id() != ID_bool) + implies_expr.op0().type().id() != ID_bool || + implies_expr.op1().type().id() != ID_bool) { return unchanged(expr); } // turn a => b into !a || b - auto new_expr = expr; + binary_exprt new_expr = implies_expr; new_expr.id(ID_or); new_expr.op0() = boolean_negate(new_expr.op0()); simplify_node(new_expr);