Warn when quantifier range exceeds SAT solver threshold (#4579)

Emit a compile-time warning when an unbounded `forall!` or `exists!`
quantifier is detected. SAT solvers (the default backend) expand
quantifiers into one conjunction/disjunction per value in the range, so
unbounded ranges (`forall!(|i| ...)` which expands over all 2^64 `usize`
values) cause silent memory exhaustion or divergence with no diagnostic.

Contributes to #3273.

## Problem

Writing `forall!(|i| ...)` (unbounded, ranging over all `usize` values)
with the default SAT backend silently hangs or OOMs because CBMC expands
the quantifier into 2^64 terms. Users get no feedback about why
verification doesn't terminate.

## Solution

- **`warn_large_quantifier_range()`** in `hooks.rs`: At codegen time,
checks if both quantifier bounds are compile-time integer constants. If
the range exceeds `QUANTIFIER_RANGE_WARN_THRESHOLD` (1000), emits a
`span_warn` suggesting tighter bounds or an SMT solver. For unbounded
ranges (~2^64), uses a human-friendly message instead of the raw
integer.
- **`unwrap_to_constant()`**: Helper that unwraps typecasts and resolves
symbol references via the symbol table to extract integer constants from
bound expressions. Includes a depth limit (5) to guard against cycles.

### Known limitation

Bounded quantifiers (`forall!(|i in (0, 2000)| ...)`) use `let` bindings
in the macro expansion for type coercion, which hides the constant
values from codegen. The warning currently only fires for **unbounded**
quantifiers, which is the most dangerous case. Detecting large bounded
ranges would require constant propagation through local variables, a
potential follow-up improvement.

## Example warning

```
warning: `kani::forall` has an unbounded (~2^64) range; SAT solvers (the default
         backend) expand quantifiers over every value and may exhaust memory or
         diverge. Consider adding tighter bounds or using an SMT solver
         (`#[kani::solver(z3)]` or `--solver z3`).
  --> tests/expected/quantifiers/large_range_warning.rs:15:13
```

## Testing

- `large_range_warning.rs` — expected test with 3 harnesses:
- `check_unbounded_forall_warns`: unbounded `forall!(|i| ...)`, verifies
warning is emitted
- `check_unbounded_exists_warns`: unbounded `exists!(|i| ...)`, verifies
warning is emitted
- `check_small_forall_no_warn`: range of 10, verifies no warning
(absence of output is intentional)

---

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: feliperodri

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -957,6 +957,12 @@ fn handle_quantifier(
     let lower_bound = &fargs[0];
     let upper_bound = &fargs[1];
 
+    // Warn when quantifier range is large or unbounded, since SAT solvers
+    // (the default backend) expand quantifiers into conjunctions/disjunctions
+    // over every value in the range. For unbounded quantifiers over usize,
+    // this means 2^64 terms, which will exhaust memory or diverge silently.
+    warn_large_quantifier_range(gcx, lower_bound, upper_bound, span, &quantifier_kind);
+
     // Create a fresh quantified variable.
     let base_name = "kani_quantified_var".to_string();
     let mut counter = 0;
@@ -1121,6 +1127,86 @@ fn build_quantifier_predicate(
 /// Get the closure's function pointer expression for use in a function call.
 /// This is the fallback path when direct substitution cannot produce a
 /// side-effect-free predicate expression.
+/// Threshold above which a quantifier range is considered too large for SAT
+/// solvers. SAT-based backends expand quantifiers into one term per value in
+/// the range, so anything beyond this is likely to cause memory exhaustion or
+/// silent divergence. The value 1000 is chosen as a conservative default that
+/// covers most practical quantifier ranges while catching accidental unbounded
+/// or excessively large ranges.
+const QUANTIFIER_RANGE_WARN_THRESHOLD: u64 = 1000;
+
+/// Emit a compile-time warning when a quantifier's range is statically known
+/// to be large or unbounded. This catches the common mistake of writing
+/// `forall!(|i| ...)` (which expands over all 2^64 usize values) without
+/// selecting an SMT solver.
+///
+/// Only fires when **both** bounds resolve to compile-time integer constants.
+/// Bounded quantifiers (`forall!(|i in (lo, hi)| ...)`) use `let` bindings
+/// for type coercion, which hides the constants from codegen — so this
+/// currently only detects unbounded quantifiers in practice.
+fn warn_large_quantifier_range(
+    gcx: &GotocCtx,
+    lower_bound: &Expr,
+    upper_bound: &Expr,
+    span: Span,
+    quantifier_kind: &QuantifierKind,
+) {
+    let lo = unwrap_to_constant(gcx, lower_bound, 0);
+    let hi = unwrap_to_constant(gcx, upper_bound, 0);
+    if let (Some(lo), Some(hi)) = (lo, hi)
+        // If hi <= lo the range is empty/inverted; no expansion happens, so no warning needed.
+        && hi > lo
+    {
+        let range_size = &hi - &lo;
+        let threshold = num::BigInt::from(QUANTIFIER_RANGE_WARN_THRESHOLD);
+        if range_size > threshold {
+            let kind = match quantifier_kind {
+                QuantifierKind::ForAll => "forall",
+                QuantifierKind::Exists => "exists",
+            };
+            // usize::MAX - usize::MIN = u64::MAX - 1 on 64-bit targets; treat
+            // anything in this ballpark as effectively unbounded.
+            let near_max = num::BigInt::from(u64::MAX) - num::BigInt::from(1u64);
+            let size_str = if range_size >= near_max {
+                "unbounded (~2^64)".to_string()
+            } else {
+                format!("{range_size}")
+            };
+            let internal_span = rustc_internal::internal(gcx.tcx, span);
+            gcx.tcx.dcx().span_warn(
+                internal_span,
+                format!(
+                    "`kani::{kind}` has an {size_str} range; \
+                     SAT solvers (the default backend) expand quantifiers \
+                     over every value and may exhaust memory or diverge. \
+                     Consider adding tighter bounds or using an SMT solver \
+                     (`#[kani::solver(z3)]` or `--solver z3`)."
+                ),
+            );
+        }
+    }
+}
+
+/// Maximum recursion depth for `unwrap_to_constant` to guard against cycles.
+const MAX_UNWRAP_DEPTH: u8 = 5;
+
+/// Unwrap typecasts and symbol references to extract an integer constant.
+fn unwrap_to_constant(gcx: &GotocCtx, expr: &Expr, depth: u8) -> Option<num::BigInt> {
+    if depth > MAX_UNWRAP_DEPTH {
+        return None;
+    }
+    expr.int_constant_value().or_else(|| match expr.value() {
+        cbmc::goto_program::ExprValue::Typecast(inner) => unwrap_to_constant(gcx, inner, depth + 1),
+        cbmc::goto_program::ExprValue::Symbol { identifier } => {
+            gcx.symbol_table.lookup(*identifier).and_then(|sym| match &sym.value {
+                SymbolValues::Expr(init) => unwrap_to_constant(gcx, init, depth + 1),
+                _ => None,
+            })
+        }
+        _ => None,
+    })
+}
+
 fn find_closure_call_expr(instance: &Instance, gcx: &mut GotocCtx, loc: Location) -> Option<Expr> {
     for arg in instance.args().0.iter() {
         let arg_ty = arg.ty()?;

tests/expected/quantifiers/large_range_warning.expected

@@ -0,0 +1,2 @@
+`kani::forall` has an unbounded (~2^64) range; SAT solvers (the default backend) expand quantifiers over every value and may exhaust memory or diverge. Consider adding tighter bounds or using an SMT solver
+`kani::exists` has an unbounded (~2^64) range; SAT solvers (the default backend) expand quantifiers over every value and may exhaust memory or diverge. Consider adding tighter bounds or using an SMT solver

tests/expected/quantifiers/large_range_warning.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zquantifiers --solver z3
+
+//! Test that Kani emits a compile-time warning when a quantifier has a large
+//! statically-known range. Unbounded quantifiers (no explicit bounds) expand to
+//! usize::MIN..usize::MAX, which are visible as constants at codegen time.
+//! Bounded quantifiers use let bindings for type coercion, so their constants
+//! are not visible at codegen time — a known limitation.
+//!
+//! Note: We use --solver z3 so the harnesses actually verify (SAT would hang
+//! on unbounded ranges). The warning fires at codegen time regardless of solver.
+
+#[kani::proof]
+fn check_unbounded_forall_warns() {
+    // Unbounded quantifier expands to usize::MIN..usize::MAX: should warn
+    assert!(kani::forall!(|i| i < 10 || i >= 10));
+}
+
+#[kani::proof]
+fn check_unbounded_exists_warns() {
+    // Unbounded exists also warns
+    assert!(kani::exists!(|i| i == 42));
+}
+
+#[kani::proof]
+fn check_small_forall_no_warn() {
+    // Range of 10 < threshold: should NOT trigger warning.
+    // (No expected output for this harness — absence of warning is the test.)
+    assert!(kani::forall!(|i in (0, 10)| i < 10));
+}