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-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/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 5ca7c77b243..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) @@ -210,9 +211,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); @@ -283,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; + } + } }