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/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; +} diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 7110b85c116..0887966fb2c 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 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 d7bbc229248..247979f8426 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,96 @@ 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; + + // 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. + bool structure_matched = match_first_operand(new_operands[0]) && + match_second_operand(new_operands[1]); + + if(structure_matched && bounds.lower == bounds.higher) + { + // 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); + } + } + if(may_be_reducible_to_interval) { optionalt symbol_opt;