diff --git a/regression/cbmc/Quantifiers-array-bound-var/exists_unsat.c b/regression/cbmc/Quantifiers-array-bound-var/exists_unsat.c new file mode 100644 index 00000000000..5e41c0e6be9 --- /dev/null +++ b/regression/cbmc/Quantifiers-array-bound-var/exists_unsat.c @@ -0,0 +1,16 @@ +int main() +{ + // Exercises the exists/assumption code path with an array-typed bound + // variable (renaming runs before quantifier rewriting). The quantifier is + // unsatisfiable (no array has a[0] < a[1] and a[1] < a[0]), so the + // assumption blocks every path and the assertion is vacuously unreachable; a + // dropped or mis-encoded array-typed bound variable would make it reachable + // and fail. + // clang-format off + __CPROVER_assume(__CPROVER_exists { int a[3]; a[0] < a[1] && a[1] < a[0] }); + // clang-format on + + __CPROVER_assert(0, "unreachable: exists-assumption is unsatisfiable"); + + return 0; +} diff --git a/regression/cbmc/Quantifiers-array-bound-var/exists_unsat.desc b/regression/cbmc/Quantifiers-array-bound-var/exists_unsat.desc new file mode 100644 index 00000000000..02c69e46a29 --- /dev/null +++ b/regression/cbmc/Quantifiers-array-bound-var/exists_unsat.desc @@ -0,0 +1,12 @@ +CORE +exists_unsat.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +Exercises the exists/assumption code path with an array-typed bound variable: +the quantifier is unsatisfiable, so the assumption blocks all paths and the +assertion is vacuously unreachable. A dropped or mis-encoded bound variable +would make the assertion reachable and fail. diff --git a/regression/cbmc/Quantifiers-array-bound-var/main.c b/regression/cbmc/Quantifiers-array-bound-var/main.c new file mode 100644 index 00000000000..6038c31e9eb --- /dev/null +++ b/regression/cbmc/Quantifiers-array-bound-var/main.c @@ -0,0 +1,14 @@ +int main() +{ + // A universal quantifier with an array-typed bound variable. Like + // struct-typed bound variables, an array-typed bound variable must remain a + // symbol rather than being decomposed into an array expression by field + // sensitivity. + // clang-format off + __CPROVER_assert( + __CPROVER_forall { int a[3]; a[0] - a[0] == 0 }, + "holds for every array-typed bound variable"); + // clang-format on + + return 0; +} diff --git a/regression/cbmc/Quantifiers-array-bound-var/refuted.c b/regression/cbmc/Quantifiers-array-bound-var/refuted.c new file mode 100644 index 00000000000..f5379693bee --- /dev/null +++ b/regression/cbmc/Quantifiers-array-bound-var/refuted.c @@ -0,0 +1,13 @@ +int main() +{ + // The body does not hold for every array (e.g. a[0] != a[1]), so + // verification must fail. This confirms the array-typed quantifier body is + // genuinely evaluated rather than the quantifier being silently dropped. + // clang-format off + __CPROVER_assert( + __CPROVER_forall { int a[3]; a[0] == a[1] }, + "does not hold for every array-typed bound variable"); + // clang-format on + + return 0; +} diff --git a/regression/cbmc/Quantifiers-array-bound-var/refuted.desc b/regression/cbmc/Quantifiers-array-bound-var/refuted.desc new file mode 100644 index 00000000000..13f5793e2d8 --- /dev/null +++ b/regression/cbmc/Quantifiers-array-bound-var/refuted.desc @@ -0,0 +1,11 @@ +CORE +refuted.c + +^\[main\.assertion\.\d+\] .* does not hold for every array-typed bound variable: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +Confirms the array-typed quantifier body is genuinely evaluated: a property +that does not hold for all arrays must be refuted. diff --git a/regression/cbmc/Quantifiers-array-bound-var/test.desc b/regression/cbmc/Quantifiers-array-bound-var/test.desc new file mode 100644 index 00000000000..e720b2d4242 --- /dev/null +++ b/regression/cbmc/Quantifiers-array-bound-var/test.desc @@ -0,0 +1,11 @@ +CORE +main.c + +^\[main\.assertion\.\d+\] .* holds for every array-typed bound variable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +This tests that an array-typed quantifier bound variable does not trigger an +invariant violation ("quantified variable shall be a symbol"). diff --git a/regression/cbmc/Quantifiers-struct-bound-var/exists.c b/regression/cbmc/Quantifiers-struct-bound-var/exists.c new file mode 100644 index 00000000000..d553ee91b39 --- /dev/null +++ b/regression/cbmc/Quantifiers-struct-bound-var/exists.c @@ -0,0 +1,20 @@ +struct point +{ + int x; + int y; +}; + +int main() +{ + // An existential quantifier with a struct-typed bound variable exercises the + // assumption (exists) code path, where renaming happens before quantifier + // rewriting. The struct-typed bound variable must remain a symbol rather than + // being decomposed by field sensitivity during renaming. + // clang-format off + __CPROVER_assume(__CPROVER_exists { struct point p; p.x > p.y }); + // clang-format on + + __CPROVER_assert(1 == 1, "reachable after exists-assumption"); + + return 0; +} diff --git a/regression/cbmc/Quantifiers-struct-bound-var/exists.desc b/regression/cbmc/Quantifiers-struct-bound-var/exists.desc new file mode 100644 index 00000000000..cb4396772e0 --- /dev/null +++ b/regression/cbmc/Quantifiers-struct-bound-var/exists.desc @@ -0,0 +1,10 @@ +CORE +exists.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +Exercises the exists/assumption code path with a struct-typed bound variable, +where renaming runs before quantifier rewriting. diff --git a/regression/cbmc/Quantifiers-struct-bound-var/exists_unsat.c b/regression/cbmc/Quantifiers-struct-bound-var/exists_unsat.c new file mode 100644 index 00000000000..65b03063db2 --- /dev/null +++ b/regression/cbmc/Quantifiers-struct-bound-var/exists_unsat.c @@ -0,0 +1,22 @@ +struct point +{ + int x; + int y; +}; + +int main() +{ + // Discriminating companion to exists.c on the exists/assumption path: this + // existential quantifier is unsatisfiable (no struct point p has p.x < p.y + // and p.y < p.x), so the assumption blocks every path and the assertion + // below is vacuously unreachable. If the struct-typed bound variable were + // dropped or the exists mis-encoded during renaming, the assumption would no + // longer block and the assertion would be reachable and fail. + // clang-format off + __CPROVER_assume(__CPROVER_exists { struct point p; p.x < p.y && p.y < p.x }); + // clang-format on + + __CPROVER_assert(0, "unreachable: exists-assumption is unsatisfiable"); + + return 0; +} diff --git a/regression/cbmc/Quantifiers-struct-bound-var/exists_unsat.desc b/regression/cbmc/Quantifiers-struct-bound-var/exists_unsat.desc new file mode 100644 index 00000000000..7f9c95979c9 --- /dev/null +++ b/regression/cbmc/Quantifiers-struct-bound-var/exists_unsat.desc @@ -0,0 +1,13 @@ +CORE +exists_unsat.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +Discriminating companion to exists.c on the exists/assumption path: the +existential quantifier is unsatisfiable -- no struct point has p.x < p.y and +p.y < p.x -- so the assumption blocks all paths and the assertion is vacuously +unreachable. A dropped or mis-encoded bound variable would make the assertion +reachable and fail. diff --git a/regression/cbmc/Quantifiers-struct-bound-var/main.c b/regression/cbmc/Quantifiers-struct-bound-var/main.c new file mode 100644 index 00000000000..93b7b6794d6 --- /dev/null +++ b/regression/cbmc/Quantifiers-struct-bound-var/main.c @@ -0,0 +1,20 @@ +struct point +{ + int x; + int y; +}; + +int main() +{ + // A universal quantifier with a struct-typed bound variable exercises the + // assertion (forall) code path, where quantifier rewriting happens before + // renaming. The struct-typed bound variable must remain a symbol rather than + // being decomposed into a struct expression by field sensitivity. + // clang-format off + __CPROVER_assert( + __CPROVER_forall { struct point p; p.x - p.x == 0 }, + "holds for every struct-typed bound variable"); + // clang-format on + + return 0; +} diff --git a/regression/cbmc/Quantifiers-struct-bound-var/refuted.c b/regression/cbmc/Quantifiers-struct-bound-var/refuted.c new file mode 100644 index 00000000000..e33718f825b --- /dev/null +++ b/regression/cbmc/Quantifiers-struct-bound-var/refuted.c @@ -0,0 +1,19 @@ +struct point +{ + int x; + int y; +}; + +int main() +{ + // The body does not hold for every struct point (e.g. x != y), so + // verification must fail. This confirms that the quantifier body is genuinely + // evaluated rather than the quantifier being silently dropped. + // clang-format off + __CPROVER_assert( + __CPROVER_forall { struct point p; p.x == p.y }, + "does not hold for every struct-typed bound variable"); + // clang-format on + + return 0; +} diff --git a/regression/cbmc/Quantifiers-struct-bound-var/refuted.desc b/regression/cbmc/Quantifiers-struct-bound-var/refuted.desc new file mode 100644 index 00000000000..15582b0870b --- /dev/null +++ b/regression/cbmc/Quantifiers-struct-bound-var/refuted.desc @@ -0,0 +1,11 @@ +CORE +refuted.c + +^\[main\.assertion\.\d+\] .* does not hold for every struct-typed bound variable: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +Confirms the struct-typed quantifier body is genuinely evaluated: a property +that does not hold for all struct points must be refuted. diff --git a/regression/cbmc/Quantifiers-struct-bound-var/test.desc b/regression/cbmc/Quantifiers-struct-bound-var/test.desc new file mode 100644 index 00000000000..3f92fd41f75 --- /dev/null +++ b/regression/cbmc/Quantifiers-struct-bound-var/test.desc @@ -0,0 +1,12 @@ +CORE +main.c + +^\[main\.assertion\.\d+\] .* holds for every struct-typed bound variable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +This tests that a struct-typed quantifier bound variable does not trigger an +invariant violation ("quantified variable shall be a symbol"). Field +sensitivity must not decompose the bound-variable symbol of a quantifier. diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 9c657af5678..f0ab957297c 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -11,6 +11,7 @@ Author: Michael Tautschnig #include #include #include +#include #include #include "goto_symex_state.h" @@ -157,6 +158,22 @@ exprt field_sensitivityt::apply( exprt expr, bool write) const { + if(expr.id() == ID_forall || expr.id() == ID_exists) + { + // Only apply field sensitivity to the body of a quantifier, never to its + // bound variables: decomposing a struct- or array-typed bound-variable + // symbol into a non-symbol expression would violate the invariant that + // quantifier bound variables are symbols. We handle only the forall/exists + // quantifiers produced by __CPROVER_forall/__CPROVER_exists; the other + // binding_exprts (lambda_exprt, array_comprehension_exprt) are not produced + // on the symex paths that reach field sensitivity (e.g. an + // array_comprehension_exprt originates from byte-operator lowering), so + // they are out of scope here. + auto &quantifier = to_quantifier_expr(expr); + quantifier.where() = apply(ns, state, std::move(quantifier.where()), write); + return expr; + } + if(expr.id() != ID_address_of) { Forall_operands(it, expr) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index d5e597a0925..c53d6750364 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -250,6 +251,31 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) { rename(expr.type(), irep_idt(), ns); + // For quantifiers, rename the bound variables individually via the symbol + // path, which renames their L2 indices but does not apply field + // sensitivity. Renaming the whole binding (operand 0) would apply field + // sensitivity to it and decompose struct- or array-typed bound-variable + // symbols into non-symbol expressions, violating the invariant that + // quantifier bound variables are symbols. The body is renamed normally + // (with field sensitivity) so that references to program variables remain + // connected to their SSA values. + // + // The loop handles an arbitrary number of bound variables, but downstream + // rewrite_quantifiers (symex_main.cpp) only supports a single one + // (quant_expr.symbol() asserts variables().size() == 1), so in practice + // this is single-iteration. The renamed bound variable stays a symbol (the + // symbol path returns an ssa_exprt, which is a symbol_exprt). + if(expr.id() == ID_forall || expr.id() == ID_exists) + { + auto &quantifier = to_quantifier_expr(expr); + for(auto &bound_variable : quantifier.variables()) + bound_variable = + to_symbol_expr(rename(std::move(bound_variable), ns).get()); + quantifier.where() = + rename(std::move(quantifier.where()), ns).get(); + return renamedt{std::move(expr)}; + } + // do this recursively Forall_operands(it, expr) *it = rename(std::move(*it), ns).get();