From ff0b9f6139028528770790606e1dd4e758149f93 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 8 Jun 2023 11:51:15 +0100 Subject: [PATCH 1/4] Allow simplification of singleton interval. Before this change, an expression like `value >= 255 && value <= 255` would fail to be simplified to `value == 255` by the expression simplifier. While the simplification itself is useful, the *lack* of it was causing some misbehaviour in one of our backends (the old SMT one under `src/solvers/smt2`) because the lack of simplification resulted in less constraints being propagated to the solver, missing some assertions around the expression that was using `value` as the size of an array. --- src/util/simplify_expr_boolean.cpp | 99 ++++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index d7bbc229248..1c732468aaf 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -99,6 +99,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) bool no_change = true; bool may_be_reducible_to_interval = expr.id() == ID_or && expr.operands().size() > 2; + bool may_be_reducible_to_singleton_interval = + expr.id() == ID_and && expr.operands().size() == 2; exprt::operandst new_operands = expr.operands(); @@ -137,6 +139,103 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) } } + // NOLINTNEXTLINE(whitespace/line_length) + // This block reduces singleton intervals like (value >= 255 && value <= 255) + // to just (value == 255). We also need to be careful with the operands + // as some of them are erased in the previous step. We proceed only if + // no operands have been erased (i.e. the expression structure has been + // preserved by previous simplification rounds.) + if(may_be_reducible_to_singleton_interval && new_operands.size() == 2) + { + struct boundst + { + mp_integer lower; + mp_integer higher; + }; + boundst bounds; + bool structure_matched = false; + + // Before we do anything else, we need to "pattern match" against the + // expression and make sure that it has the structure we're looking for. + // The structure we're looking for is going to be + // (value >= 255 && !(value >= 256)) -- 255, 256 values indicative. + // (this is because previous simplification runs will have transformed + // the less_than_or_equal expression to a not(greater_than_or_equal) + // expression) + + // matching (value >= 255) + auto const match_first_operand = [&bounds](const exprt &op) -> bool { + if( + const auto ge_expr = + expr_try_dynamic_cast(op)) + { + // The construction of these expressions ensures that the RHS + // is constant, therefore if we don't have a constant, it's a + // different expression, so we bail. + if(!ge_expr->rhs().is_constant()) + return false; + if( + auto int_opt = + numeric_cast(to_constant_expr(ge_expr->rhs()))) + { + bounds.lower = *int_opt; + return true; + } + return false; + } + return false; + }; + + // matching !(value >= 256) + auto const match_second_operand = [&bounds](const exprt &op) -> bool { + if(const auto not_expr = expr_try_dynamic_cast(op)) + { + PRECONDITION(not_expr->operands().size() == 1); + if( + const auto ge_expr = + expr_try_dynamic_cast( + not_expr->op())) + { + // If the rhs() is not constant, it has a different structure + // (e.g. i >= j) + if(!ge_expr->rhs().is_constant()) + return false; + if( + auto int_opt = + numeric_cast(to_constant_expr(ge_expr->rhs()))) + { + bounds.higher = *int_opt - 1; + return true; + } + return false; + } + return false; + } + return false; + }; + + // We need to match both operands, at the particular sequence we expect. + structure_matched |= match_first_operand(new_operands[0]); + structure_matched &= match_second_operand(new_operands[1]); + + if(structure_matched && bounds.lower == bounds.higher) + { + // Go through the expression again and convert >= operand into == + for(const auto &op : new_operands) + { + if( + const auto ge_expr = + expr_try_dynamic_cast(op)) + { + equal_exprt new_expr{ge_expr->lhs(), ge_expr->rhs()}; + return changed(new_expr); + } + else + continue; + } + } + } + if(may_be_reducible_to_interval) { optionalt symbol_opt; From 8e82b4db01df48da897fe53d9bd3e31a739c7e65 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 13 Jun 2023 16:59:11 +0100 Subject: [PATCH 2/4] Fix recognition of quantifier bounds in case of previous simplification of singleton interval --- .../forall_in_exists.c | 2 +- src/solvers/flattening/boolbv_quantifier.cpp | 58 ++++++++++++------- 2 files changed, 39 insertions(+), 21 deletions(-) diff --git a/regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c b/regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c index 0f745817d63..dad8fe424c4 100644 --- a/regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c +++ b/regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c @@ -8,7 +8,7 @@ int main(int argc, char **argv) __CPROVER_assert( __CPROVER_exists { int z; (0 < z && z < 2) && - __CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == * i }}, + __CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == *i }}, "there exists a z between 0 and 2 so that for all o between 10 and 20, o > z and z = 1"); } // clang-format on diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 7110b85c116..71590bca107 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -50,13 +50,13 @@ get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr) } else if(quantifier_expr.id() == ID_and) { - /** - * The min variable - * is in the form of "var_expr >= constant". - */ + // The minimum variable can be of the form `var_expr >= constant`, or + // it can be of the form `var_expr == constant` (e.g. in the case where + // the interval that bounds the variable is a singleton interval (set + // with only one element)). for(auto &x : quantifier_expr.operands()) { - if(x.id()!=ID_ge) + if(x.id() != ID_ge && x.id() != ID_equal) continue; const auto &x_binary = to_binary_relation_expr(x); if(expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().is_constant()) @@ -106,24 +106,42 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr) } else { - /** - * The max variable - * is in the form of "!(var_expr >= constant)". - */ + // There are two potential forms we could come across here. The first one + // is `!(var_expr >= constant)` - identified by the first if branch - and + // the second is `var_expr == constant` - identified by the second else-if + // branch. The second form could be met if previous simplification has + // identified a singleton interval - see simplify_boolean_expr.cpp. for(auto &x : quantifier_expr.operands()) { - if(x.id()!=ID_not) - continue; - exprt y = to_not_expr(x).op(); - if(y.id()!=ID_ge) - continue; - const auto &y_binary = to_binary_relation_expr(y); - if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant()) + if(x.id() == ID_not) { - const constant_exprt &over_expr = to_constant_expr(y_binary.rhs()); - mp_integer over_i = numeric_cast_v(over_expr); - over_i-=1; - return from_integer(over_i, y_binary.rhs().type()); + exprt y = to_not_expr(x).op(); + if(y.id() != ID_ge) + continue; + const auto &y_binary = to_binary_relation_expr(y); + if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant()) + { + const constant_exprt &over_expr = to_constant_expr(y_binary.rhs()); + mp_integer over_i = numeric_cast_v(over_expr); + over_i -= 1; + return from_integer(over_i, y_binary.rhs().type()); + } + } + else if(x.id() == ID_equal) + { + const auto &y_binary = to_binary_relation_expr(x); + if(expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().is_constant()) + { + return to_constant_expr(y_binary.rhs()); + } + } + else + { + // If we are here, we came across a (simplified?) expression that was + // not anticipated - normally this would be a bug, but if you made + // changes to the simplifier (as an example), you would need to add an + // else-if branch that handles that type above. + continue; } } } From c5c8e62ade362601214bdb7e8bdef876e6353dab Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 14 Jun 2023 11:07:59 +0100 Subject: [PATCH 3/4] Add regression tests for simplification of singleton intervals --- .../negative_test.desc | 18 ++++++++++++++++++ .../positive_test.desc | 14 ++++++++++++++ .../singleton_interval_simp.c | 17 +++++++++++++++++ .../singleton_interval_simp_neg.c | 18 ++++++++++++++++++ 4 files changed, 67 insertions(+) create mode 100644 regression/cbmc/simplify_singleton_interval_7690/negative_test.desc create mode 100644 regression/cbmc/simplify_singleton_interval_7690/positive_test.desc create mode 100644 regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp.c create mode 100644 regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp_neg.c diff --git a/regression/cbmc/simplify_singleton_interval_7690/negative_test.desc b/regression/cbmc/simplify_singleton_interval_7690/negative_test.desc new file mode 100644 index 00000000000..141ab73c26d --- /dev/null +++ b/regression/cbmc/simplify_singleton_interval_7690/negative_test.desc @@ -0,0 +1,18 @@ +CORE +--trace +singleton_interval_simp_neg.c +^VERIFICATION FAILED$ +^\[main\.assertion\.1\] line \d expected failure: paths where x is unbounded explored: FAILURE$ +^\[main\.assertion\.2\] line \d+ expected failure: paths where 0 \<= x \<= 15 explored: FAILURE$ +^\[main\.assertion\.3\] line \d+ expected success: paths where x \<= 15 explored: SUCCESS$ +y=-6 \(11111111 11111111 11111111 11111010\) +x=14 \(00000000 00000000 00000000 00001110\) +y=34 \(00000000 00000000 00000000 00100010\) +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This tests the negative case of the simplification of the singleton interval +(i.e when the presented interval *is* the *not* the singleton interval - +the set of possible values that the bounded variable can take has cardinality +> 1). diff --git a/regression/cbmc/simplify_singleton_interval_7690/positive_test.desc b/regression/cbmc/simplify_singleton_interval_7690/positive_test.desc new file mode 100644 index 00000000000..4977415b9fc --- /dev/null +++ b/regression/cbmc/simplify_singleton_interval_7690/positive_test.desc @@ -0,0 +1,14 @@ +CORE +--trace +singleton_interval_simp.c +^VERIFICATION FAILED$ +^\[main\.assertion\.1\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$ +^\[main\.assertion\.2\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$ +x=15 \(00000000 00000000 00000000 00001111\) +y=35 \(00000000 00000000 00000000 00100011\) +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This tests the positive case of the simplification of the singleton interval +(i.e when the presented interval *is* the singleton interval) diff --git a/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp.c b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp.c new file mode 100644 index 00000000000..961c423dabd --- /dev/null +++ b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp.c @@ -0,0 +1,17 @@ +// Positive test for singleton interval simplification. +// Notice that the sequence of the inequalities in this +// expression is different to the one in +// `singleton_interval_in_assume_7690.c`. + +int main() +{ + int x; + __CPROVER_assume(x >= 15 && x <= 15); + int y = x + 20; + + __CPROVER_assert( + y != 35, "expected failure: only paths where x == 15 explored"); + __CPROVER_assert( + y == 34, "expected failure: only paths where x == 15 explored"); + return 0; +} diff --git a/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp_neg.c b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp_neg.c new file mode 100644 index 00000000000..98aa521031e --- /dev/null +++ b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp_neg.c @@ -0,0 +1,18 @@ +// Negative test for singleton interval simplification. + +int main() +{ + int x; + int y = x + 20; + + __CPROVER_assert( + y != -6, "expected failure: paths where x is unbounded explored"); + + __CPROVER_assume(x >= 0 && x <= 15); + __CPROVER_assert( + y != 34, "expected failure: paths where 0 <= x <= 15 explored"); + + int z = x + 20; + __CPROVER_assert(z != 36, "expected success: paths where x <= 15 explored"); + return 0; +} From de8b169f44dcbe3a57bd3d931b8175f124d45509 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 16 Jun 2023 10:56:14 +0100 Subject: [PATCH 4/4] Simplify handling of expression matching and clarify comment in else branch --- src/solvers/flattening/boolbv_quantifier.cpp | 8 +++---- src/util/simplify_expr_boolean.cpp | 25 +++++++------------- 2 files changed, 13 insertions(+), 20 deletions(-) diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 71590bca107..0887966fb2c 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -137,10 +137,10 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr) } else { - // If we are here, we came across a (simplified?) expression that was - // not anticipated - normally this would be a bug, but if you made - // changes to the simplifier (as an example), you would need to add an - // else-if branch that handles that type above. + // If you need special handling for a particular expression type (say, + // after changes to the simplifier) you need to make sure that you add + // an `else if` branch above, otherwise the expression will get skipped + // and the constraints will not propagate correctly. continue; } } diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 1c732468aaf..247979f8426 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -153,7 +153,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) mp_integer higher; }; boundst bounds; - bool structure_matched = false; // Before we do anything else, we need to "pattern match" against the // expression and make sure that it has the structure we're looking for. @@ -215,24 +214,18 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) }; // We need to match both operands, at the particular sequence we expect. - structure_matched |= match_first_operand(new_operands[0]); - structure_matched &= match_second_operand(new_operands[1]); + bool structure_matched = match_first_operand(new_operands[0]) && + match_second_operand(new_operands[1]); if(structure_matched && bounds.lower == bounds.higher) { - // Go through the expression again and convert >= operand into == - for(const auto &op : new_operands) - { - if( - const auto ge_expr = - expr_try_dynamic_cast(op)) - { - equal_exprt new_expr{ge_expr->lhs(), ge_expr->rhs()}; - return changed(new_expr); - } - else - continue; - } + // If we are here, we have matched the structure we expected, so we can + // make some reasonable assumptions about where certain info we need is + // located at. + const auto ge_expr = + expr_dynamic_cast(new_operands[0]); + equal_exprt new_expr{ge_expr.lhs(), ge_expr.rhs()}; + return changed(new_expr); } }