From 71d18232d2d5feab7fbd1af0de1bdb6aa9ab44ef Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Jun 2026 10:10:57 +0000 Subject: [PATCH] goto-symex: keep composite quantifier bound variables as symbols Field sensitivity decomposes struct- and array-typed symbols into struct/array expressions built from per-field SSA symbols. When this is applied to the bound variable of a forall/exists quantifier, the bound variable is turned into a non-symbol expression, violating the invariant that quantifier bound variables must be symbols (validate_expr in mathematical_expr.h: "quantified variable shall be a symbol"). As a result, any quantifier with a struct- or array-typed bound variable triggered an invariant violation, in both the assertion (forall) and the assumption (exists) code paths. Restrict field sensitivity to the body of a quantifier: - field_sensitivityt::apply now descends only into the body (operand 1) of a quantifier, leaving the bound variables (operand 0) untouched. This covers the assertion path, where the quantifier is field-sensitised by clean_expr before rewrite_quantifiers removes it. - goto_symex_statet::rename renames the bound-variable symbols individually via the symbol path (which assigns L2 indices but does not apply field sensitivity) and renames the body normally. This covers the assumption path, where renaming happens before rewrite_quantifiers and was decomposing the binding via field sensitivity. The body is still renamed with field sensitivity so that references to program variables remain connected to their SSA values. Co-authored-by: Kiro --- .../exists_unsat.c | 16 ++++++++++++ .../exists_unsat.desc | 12 +++++++++ .../cbmc/Quantifiers-array-bound-var/main.c | 14 ++++++++++ .../Quantifiers-array-bound-var/refuted.c | 13 ++++++++++ .../Quantifiers-array-bound-var/refuted.desc | 11 ++++++++ .../Quantifiers-array-bound-var/test.desc | 11 ++++++++ .../Quantifiers-struct-bound-var/exists.c | 20 ++++++++++++++ .../Quantifiers-struct-bound-var/exists.desc | 10 +++++++ .../exists_unsat.c | 22 ++++++++++++++++ .../exists_unsat.desc | 13 ++++++++++ .../cbmc/Quantifiers-struct-bound-var/main.c | 20 ++++++++++++++ .../Quantifiers-struct-bound-var/refuted.c | 19 ++++++++++++++ .../Quantifiers-struct-bound-var/refuted.desc | 11 ++++++++ .../Quantifiers-struct-bound-var/test.desc | 12 +++++++++ src/goto-symex/field_sensitivity.cpp | 17 ++++++++++++ src/goto-symex/goto_symex_state.cpp | 26 +++++++++++++++++++ 16 files changed, 247 insertions(+) create mode 100644 regression/cbmc/Quantifiers-array-bound-var/exists_unsat.c create mode 100644 regression/cbmc/Quantifiers-array-bound-var/exists_unsat.desc create mode 100644 regression/cbmc/Quantifiers-array-bound-var/main.c create mode 100644 regression/cbmc/Quantifiers-array-bound-var/refuted.c create mode 100644 regression/cbmc/Quantifiers-array-bound-var/refuted.desc create mode 100644 regression/cbmc/Quantifiers-array-bound-var/test.desc create mode 100644 regression/cbmc/Quantifiers-struct-bound-var/exists.c create mode 100644 regression/cbmc/Quantifiers-struct-bound-var/exists.desc create mode 100644 regression/cbmc/Quantifiers-struct-bound-var/exists_unsat.c create mode 100644 regression/cbmc/Quantifiers-struct-bound-var/exists_unsat.desc create mode 100644 regression/cbmc/Quantifiers-struct-bound-var/main.c create mode 100644 regression/cbmc/Quantifiers-struct-bound-var/refuted.c create mode 100644 regression/cbmc/Quantifiers-struct-bound-var/refuted.desc create mode 100644 regression/cbmc/Quantifiers-struct-bound-var/test.desc 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();