From 91b842e19eb58e83a51976cc27e968c65dbe7c7c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Mar 2024 14:04:43 +0000 Subject: [PATCH 1/2] Eager quantifier elimination: support empty ranges conjunction(...) and disjunction(...) helper functions produce the appropriate result for empty operand sequences. --- regression/cbmc/Quantifiers-invalid-var-range/test.desc | 6 ++---- src/solvers/flattening/boolbv_quantifier.cpp | 3 --- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc index 5ca881d80d9..53977132489 100644 --- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc +++ b/regression/cbmc/Quantifiers-invalid-var-range/test.desc @@ -1,13 +1,11 @@ -KNOWNBUG broken-smt-backend +CORE no-new-smt main.c ^\*\* Results:$ -^\*\* 0 of 1 failed +^\*\* 0 of \d+ failed ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -- -This produces the expected verification result, but actually ignores some -quantifiers. diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 5ca7c77b243..edd13fbf17e 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -210,9 +210,6 @@ static std::optional eager_quantifier_instantiation( mp_integer lb = numeric_cast_v(min_i.value()); mp_integer ub = numeric_cast_v(max_i.value()); - if(lb > ub) - return {}; - auto expr_simplified = quantifier_exprt(expr.id(), expr.variables(), where_simplified); From 9be48ee5f48dc038b011160010fbb73c212f841f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Feb 2024 16:03:46 +0000 Subject: [PATCH 2/2] Quantifier instantiation via simplistic E-matching Use E-matching on index expressions to instantiate quantifiers when eager instantiation (aka enumerative instantiation) cannot be applied. --- doc/cprover-manual/cbmc-assertions.md | 7 +- .../no-upper-bound.c | 20 +++ .../no-upper-bound.desc | 11 ++ regression/cbmc/Quantifiers-type/test.desc | 9 +- .../main.c | 102 +++++++++++++ .../test.desc | 14 ++ .../cbmc/Quantifiers-unbounded-array/main.c | 41 ++++++ .../Quantifiers-unbounded-array/test.desc | 8 ++ src/solvers/flattening/boolbv_quantifier.cpp | 136 +++++++++++++++++- 9 files changed, 329 insertions(+), 19 deletions(-) create mode 100644 regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.c create mode 100644 regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.desc create mode 100644 regression/cbmc/Quantifiers-unbounded-array-overflow/main.c create mode 100644 regression/cbmc/Quantifiers-unbounded-array-overflow/test.desc create mode 100644 regression/cbmc/Quantifiers-unbounded-array/main.c create mode 100644 regression/cbmc/Quantifiers-unbounded-array/test.desc diff --git a/doc/cprover-manual/cbmc-assertions.md b/doc/cprover-manual/cbmc-assertions.md index 8fc8395d377..7ea680434a3 100644 --- a/doc/cprover-manual/cbmc-assertions.md +++ b/doc/cprover-manual/cbmc-assertions.md @@ -82,12 +82,7 @@ int foo(int a, int b) { } ``` -A future release of CPROVER will support using these pre and -postconditions to create a function contract, which can be used for -modular verification. - - -Future CPROVER releases will support explicit quantifiers with a syntax +CPROVER supports explicit quantifiers with a syntax that resembles Spec\#: ```C diff --git a/regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.c b/regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.c new file mode 100644 index 00000000000..b881ee7bf64 --- /dev/null +++ b/regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.c @@ -0,0 +1,20 @@ +int main() +{ + int a[2][2]; + + __CPROVER_assume(__CPROVER_forall { + unsigned i; + __CPROVER_forall + { + unsigned j; + a[i % 2][j % 2] == (i % 2) + (j % 2) + } + }); + + assert(a[0][0] == 0); + assert(a[0][1] == 1); + assert(a[1][0] == 1); + assert(a[1][1] == 2); + + return 0; +} diff --git a/regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.desc b/regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.desc new file mode 100644 index 00000000000..fe26160a3fc --- /dev/null +++ b/regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.desc @@ -0,0 +1,11 @@ +CORE broken-cprover-smt-backend no-new-smt +no-upper-bound.c +--max-field-sensitivity-array-size 0 +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +E-matching does not yet handle array expressions (which field sensitivity +produces for small fixed-size arrays), so we disable field sensitivity. diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index 2281b9ab7a3..a600caa79b7 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/regression/cbmc/Quantifiers-type/test.desc @@ -1,14 +1,11 @@ -KNOWNBUG broken-smt-backend +CORE broken-smt-backend no-new-smt main.c ^\*\* Results:$ -^\[main.assertion.1\] line 12 assertion tmp_if_expr(\$\d+)?: FAILURE$ -^\*\* 1 of 1 failed +^\[main.assertion.1\] line 10 assertion a\[(\(signed (long )*int\))?0\] == 10 && a\[(\(signed (long )*int\))?1\] == 10: FAILURE$ +^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring --- -This produces the expected verification result, but actually ignores some -quantifiers. diff --git a/regression/cbmc/Quantifiers-unbounded-array-overflow/main.c b/regression/cbmc/Quantifiers-unbounded-array-overflow/main.c new file mode 100644 index 00000000000..e618e43a437 --- /dev/null +++ b/regression/cbmc/Quantifiers-unbounded-array-overflow/main.c @@ -0,0 +1,102 @@ +#include +#include +#include +#include + +size_t nondet_size_t(); + +#if UINT_MAX < SIZE_MAX +# define SMALLER_TYPE int +#else +# define SMALLER_TYPE short +#endif + +// The model has an overflow, falsified instantly with SAT, +// takes forever with z3 because of the quantifiers +int main() +{ + size_t size = nondet_size_t(); + __CPROVER_assume(0 < size); + __CPROVER_assume(size <= __CPROVER_max_malloc_size / sizeof(SMALLER_TYPE)); + // we remove this assumption, which in turn allows to cause an integer + // overflow in the loop body when computing i*2, because we would end up + // comparing i*2, which does not overflow on size_t, to the overflowed + // (wrap-around) value when i*2 was assigned to the int-typed array element + // __CPROVER_assume(size < INT_MAX / 2); + size_t nof_bytes = size * sizeof(SMALLER_TYPE); + SMALLER_TYPE *arr = malloc(nof_bytes); + __CPROVER_assume(arr); + __CPROVER_array_set(arr, 0); + + // None of this should overflow because initially arr[j] == 0 for all j + + // the original loop + // size_t i = 0; + // while (i < size) + // __CPROVER_loop_invariant(i <= size) + // __CPROVER_loop_invariant(__CPROVER_forall {size_t j; !(j < i) || (arr[j] == j * 2) }) + // __CPROVER_loop_invariant(__CPROVER_forall {size_t j; !(i <= j && j < size) || (arr[j] == 0) }) + // { + // arr[i] = arr[i] + 2 * i; + // i += 1; + // } + + size_t i = 0; + + // check base case + assert(i <= size); + assert(__CPROVER_forall { + size_t j; + !(j < i) || (arr[j] == j * 2) + }); + assert(__CPROVER_forall { + size_t j; + !(i <= j && j < size) || (arr[j] == 0) + }); + + // jump to a nondet state + i = nondet_size_t(); + __CPROVER_havoc_object(arr); + + // assume loop invariant + __CPROVER_assume(i <= size); + __CPROVER_assume(i <= size); + __CPROVER_assume(__CPROVER_forall { + size_t j; + !(j < i) || (arr[j] == j * 2) + }); + __CPROVER_assume(__CPROVER_forall { + size_t j; + !(i <= j && j < size) || (arr[j] == 0) + }); + + size_t old_i = i; + if(i < size) + { + arr[i] = arr[i] + i * 2; + i += 1; + + // check loop invariant post loop step + assert(i <= size); + assert(__CPROVER_forall { + size_t j; + !(j < i) || (arr[j] == j * 2) + }); + assert(__CPROVER_forall { + size_t j; + !(i <= j && j < size) || (arr[j] == 0) + }); + __CPROVER_assume(0); // stop progress + } + + // check that the loop invariant holds post loop + assert(__CPROVER_forall { + size_t j; + !(j < i) || (arr[j] == j * 2) + }); + + assert(__CPROVER_forall { + size_t j; + !(i <= j && j < size) || (arr[j] == 0) + }); +} diff --git a/regression/cbmc/Quantifiers-unbounded-array-overflow/test.desc b/regression/cbmc/Quantifiers-unbounded-array-overflow/test.desc new file mode 100644 index 00000000000..ec92a6c89ca --- /dev/null +++ b/regression/cbmc/Quantifiers-unbounded-array-overflow/test.desc @@ -0,0 +1,14 @@ +CORE thorough-z3-smt-backend broken-cprover-smt-backend no-new-smt +main.c +--no-standard-checks +^\[main.assertion.5\] line 81 assertion __CPROVER_forall \{ size_t j; !\(j < i\) \|\| \(arr\[j\] == j \* 2\) \}: FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Uses --no-standard-checks to contain verification time with MiniSat; with +CaDiCaL this completes in under 5 seconds either way. Takes an unknown amount of +time (has never been run to completition) when using Z3. diff --git a/regression/cbmc/Quantifiers-unbounded-array/main.c b/regression/cbmc/Quantifiers-unbounded-array/main.c new file mode 100644 index 00000000000..017b58c8282 --- /dev/null +++ b/regression/cbmc/Quantifiers-unbounded-array/main.c @@ -0,0 +1,41 @@ +#include +#include +#include + +size_t nondet_size_t(); + +int main() +{ + size_t size = nondet_size_t(); + __CPROVER_assume(0 < size); + + // avoids overflows in the loop body on i * 2 + __CPROVER_assume(size < INT_MAX / 2); + size_t nof_bytes = size * sizeof(int); + int *arr = malloc(nof_bytes); + __CPROVER_assume(arr); + __CPROVER_array_set(arr, 0); + + // jump to a nondet state + size_t i = nondet_size_t(); + __CPROVER_assume(i < size); + __CPROVER_havoc_object(arr); + + // assume loop invariant + __CPROVER_assume(__CPROVER_forall { + size_t j; + !(j < i) || (arr[j] == j * 2) + }); + __CPROVER_assume(__CPROVER_forall { + size_t j; + !(i <= j && j < size) || (arr[j] == 0) + }); + + arr[i] = arr[i] + i * 2; + i += 1; + + assert(__CPROVER_forall { + size_t j; + !(i <= j && j < size) || (arr[j] == 0) + }); +} diff --git a/regression/cbmc/Quantifiers-unbounded-array/test.desc b/regression/cbmc/Quantifiers-unbounded-array/test.desc new file mode 100644 index 00000000000..d6cf44082c0 --- /dev/null +++ b/regression/cbmc/Quantifiers-unbounded-array/test.desc @@ -0,0 +1,8 @@ +CORE broken-cprover-smt-backend no-new-smt +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index edd13fbf17e..17e56e46881 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -6,12 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include "boolbv.h" - #include #include #include #include +#include + +#include "boolbv.h" /// A method to detect equivalence between experts that can contain typecast static bool expr_eq(const exprt &expr1, const exprt &expr2) @@ -280,12 +281,133 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src) return quantifier_list.back().l; } +/// Eliminate the quantifier in \p q_expr via E-matching in \p context_map. +/// \return Quantifier-free expression, if quantifier elimination was +/// successful, else nullopt. +static std::optional instantiate_one_quantifier( + const quantifier_exprt &q_expr, + const std::unordered_map &context_map) +{ + if(q_expr.variables().size() > 1) + { + // Rewrite Qx,y.P(x,y) as Qy.Qx.P(x,y), just like + // eager_quantifier_instantiation does. + auto new_variables = q_expr.variables(); + new_variables.pop_back(); + quantifier_exprt new_expression{ + q_expr.id(), + q_expr.variables().back(), + quantifier_exprt{q_expr.id(), new_variables, q_expr.where()}}; + return instantiate_one_quantifier(new_expression, context_map); + } + + // find the contexts in which the bound variable is used + const irep_idt &bound_variable_id = q_expr.symbol().get_identifier(); + bool required_context = false; + std::unordered_set index_contexts; + auto context_finder = + [&bound_variable_id, &required_context, &index_contexts](const exprt &e) + { + if(auto symbol_expr = expr_try_dynamic_cast(e)) + { + required_context |= bound_variable_id == symbol_expr->get_identifier(); + } + else if(required_context) + { + if(auto index_expr = expr_try_dynamic_cast(e)) + { + index_contexts.insert(*index_expr); + required_context = false; + } + } + }; + q_expr.where().visit_post(context_finder); + // make sure we found some context for instantiation + if(index_contexts.empty()) + return {}; + + // match the contexts against expressions that we have cached + std::unordered_set instantiation_candidates; + for(const auto &cache_entry : context_map) + { + // consider re-organizing the cache to use expression ids at the top level + if(auto index_expr = expr_try_dynamic_cast(cache_entry.first)) + { + for(const auto &index_context : index_contexts) + { + if( + auto ssa_context = + expr_try_dynamic_cast(index_context.array())) + { + if( + auto ssa_array = + expr_try_dynamic_cast(index_expr->array())) + { + if( + ssa_context->get_l1_object_identifier() == + ssa_array->get_l1_object_identifier()) + { + instantiation_candidates.insert(index_expr->index()); + break; + } + } + } + else if(index_expr->array() == index_context.array()) + { + instantiation_candidates.insert(index_expr->index()); + break; + } + } + } + } + + if(instantiation_candidates.empty()) + return {}; + + exprt::operandst instantiations; + instantiations.reserve(instantiation_candidates.size()); + for(const auto &e : instantiation_candidates) + { + exprt::operandst values{ + {typecast_exprt::conditional_cast(e, q_expr.symbol().type())}}; + instantiations.push_back(q_expr.instantiate(values)); + } + + if(q_expr.id() == ID_exists) + return disjunction(instantiations); + else + return conjunction(instantiations); +} + void boolbvt::finish_eager_conversion_quantifiers() { - if(quantifier_list.empty()) - return; + // Nested quantifiers may yield additional entries in quantifier_list via + // convert. + while(!quantifier_list.empty()) + { + std::list remaining_quantifiers; + std::swap(quantifier_list, remaining_quantifiers); + std::list> instantiations; + + for(const auto &q : remaining_quantifiers) + { + instantiations.push_back( + instantiate_one_quantifier(to_quantifier_expr(q.expr), bv_cache)); + } + + auto instantiations_it = instantiations.begin(); + for(const auto &q : remaining_quantifiers) + { + if(!instantiations_it->has_value()) + { + conversion_failed(q.expr); + ++instantiations_it; + continue; + } - // we do not yet have any elaborate post-processing - for(const auto &q : quantifier_list) - conversion_failed(q.expr); + literalt result_lit = convert(**instantiations_it); + prop.l_set_to_true(prop.lequal(q.l, result_lit)); + ++instantiations_it; + } + } }