goto-symex: keep composite quantifier bound variables as symbols

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;
+}

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.

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;
+}

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;
+}

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.

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").

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;
+}

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.

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;
+}

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.

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;
+}

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;
+}

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.

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.

src/goto-symex/field_sensitivity.cpp

@@ -11,6 +11,7 @@ Author: Michael Tautschnig
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/mathematical_expr.h>
 #include <util/pointer_offset_size.h>
 
 #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)

src/goto-symex/goto_symex_state.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
+#include <util/mathematical_expr.h>
 #include <util/std_expr.h>
 
 #include <analyses/dirty.h>
@@ -250,6 +251,31 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
   {
     rename<level>(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<level>(std::move(bound_variable), ns).get());
+      quantifier.where() =
+        rename<level>(std::move(quantifier.where()), ns).get();
+      return renamedt<exprt, level>{std::move(expr)};
+    }
+
     // do this recursively
     Forall_operands(it, expr)
       *it = rename<level>(std::move(*it), ns).get();