Fail verification when the solver backend drops quantifiers

docs/src/reference/experimental/quantifiers.md

@@ -54,3 +54,9 @@ fn vec_assert_forall_harness() {
 
 We now assume that all quantified variables are of type `usize`. This means that the range specified in the quantifier must be compatible with `usize`.
  We plan to support other types in the future, but for now, ensure that your quantifiers use `usize` ranges.
+
+#### Solver Backend Support
+
+The default SAT-based solver backend only supports quantifiers with constant bounds. A quantifier whose bound is symbolic (not known at compile time) cannot be encoded and would be silently replaced with an unconstrained value, which is unsound: a `kani::assume` containing such a quantifier would not be enforced, and a `kani::assert` containing one could fail spuriously.
+
+To keep results sound, Kani reports verification as `FAILED` when the backend drops a quantifier, and directs you to an SMT solver backend that supports quantifiers. Use `#[kani::solver(z3)]` on the harness (or `--solver z3` on the command line) to verify these quantifiers.

kani-driver/src/call_cbmc.rs

@@ -210,6 +210,13 @@ pub struct VerificationResult {
     pub runtime: Duration,
     /// Whether concrete playback generated a test
     pub generated_concrete_test: bool,
+    /// The number of quantifier expressions CBMC's solver backend could not encode and
+    /// dropped (replaced with unconstrained values), c.f. CBMC's "warning: ignoring forall"
+    /// messages. A nonzero count makes the analysis unsound -- an `assume` containing such a
+    /// quantifier is not enforced (a successful result would be vacuous), and an `assert`
+    /// containing one may fail spuriously -- so it forces the verification to fail (see
+    /// `VerificationResult::from`).
+    pub ignored_quantifiers: usize,
     /// The coverage results
     pub coverage_results: Option<CoverageResults>,
     /// CBMC execution statistics extracted from messages
@@ -304,6 +311,7 @@ impl KaniSession {
                 results: Err(ExitStatus::Timeout),
                 runtime: start_time.elapsed(),
                 generated_concrete_test: false,
+                ignored_quantifiers: 0,
                 coverage_results: None,
                 cbmc_stats: None,
             })
@@ -469,6 +477,34 @@ impl KaniSession {
     }
 }
 
+/// Count CBMC messages reporting that a quantifier expression could not be encoded and was
+/// dropped. CBMC's SAT-based backends only support quantifiers with constant bounds; other
+/// quantifiers are replaced by unconstrained values, with only a low-visibility message
+/// (`prop_conv_solvert::ignoring`, printed as "warning: ignoring forall" followed by the
+/// pretty-printed expression).
+fn count_ignored_quantifiers(items: &[ParserItem]) -> usize {
+    items
+        .iter()
+        .filter(|item| {
+            matches!(item, ParserItem::Message { message_text, .. }
+                if message_text.starts_with("warning: ignoring forall")
+                    || message_text.starts_with("warning: ignoring exists"))
+        })
+        .count()
+}
+
+/// The error rendered when the solver backend dropped quantifier expressions.
+fn ignored_quantifiers_error(count: usize) -> String {
+    format!(
+        "error: the solver backend does not support quantifiers with non-constant bounds \
+and ignored {count} quantifier expression(s), replacing them with unconstrained values.\n\
+         Kani cannot soundly verify this harness: `kani::assume` calls containing such a \
+quantifier are NOT enforced (a successful result would not cover the intended property), and \
+`kani::assert` calls containing one may fail spuriously.\n\
+         Use an SMT solver backend that supports quantifiers, e.g. `#[kani::solver(z3)]`.\n"
+    )
+}
+
 impl VerificationResult {
     /// Computes a `VerificationResult` (kani-driver's notion of the result of a CBMC call) from a
     /// `VerificationOutput` (cbmc_output_parser's idea of CBMC results).
@@ -485,22 +521,32 @@ impl VerificationResult {
         collect_cbmc_stats: bool,
     ) -> VerificationResult {
         let runtime = start_time.elapsed();
+        let ignored_quantifiers = count_ignored_quantifiers(&output.processed_items);
         let (remaining_items, results) = extract_results(output.processed_items);
 
         // Only `--export-json` consumes these, and collecting them means running several regexes
         // over every message CBMC emitted, so skip the work entirely when nothing will read it.
         let cbmc_stats = if collect_cbmc_stats { merge_cbmc_stats(&remaining_items) } else { None };
 
         if let Some(results) = results {
-            let (status, failed_properties) =
+            let (mut status, mut failed_properties) =
                 verification_outcome_from_properties(&results, should_panic);
+            // A dropped quantifier makes the analysis unsound: a `kani::assume` containing one is
+            // silently not enforced, so a "successful" result may be vacuous. Kani must never
+            // report success in that case -- force a failure and (via the rendered error) direct
+            // the user to an SMT backend that supports quantifiers.
+            if ignored_quantifiers > 0 {
+                status = VerificationStatus::Failure;
+                failed_properties = FailedProperties::Error;
+            }
             let coverage_results = coverage_results_from_properties(&results);
             VerificationResult {
                 status,
                 failed_properties,
                 results: Ok(results),
                 runtime,
                 generated_concrete_test: false,
+                ignored_quantifiers,
                 coverage_results,
                 cbmc_stats,
             }
@@ -517,6 +563,7 @@ impl VerificationResult {
                 results: Err(exit_status),
                 runtime,
                 generated_concrete_test: false,
+                ignored_quantifiers,
                 coverage_results: None,
                 cbmc_stats,
             }
@@ -530,6 +577,7 @@ impl VerificationResult {
             results: Ok(vec![]),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
+            ignored_quantifiers: 0,
             coverage_results: None,
             cbmc_stats: None,
         }
@@ -545,6 +593,7 @@ impl VerificationResult {
             results: Err(ExitStatus::Other(42)),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
+            ignored_quantifiers: 0,
             coverage_results: None,
             cbmc_stats: None,
         }
@@ -569,6 +618,20 @@ impl VerificationResult {
                 } else {
                     format_result(results, status, should_panic, failed_properties, show_checks)
                 };
+                if self.ignored_quantifiers > 0 {
+                    let error = ignored_quantifiers_error(self.ignored_quantifiers);
+                    // Surface the soundness error immediately before the overall
+                    // `VERIFICATION:- ...` line, so it explains the forced failure. Fall back to
+                    // appending it (e.g. coverage output, which has no such line) if the marker
+                    // isn't present.
+                    match result.find("\nVERIFICATION:- ") {
+                        Some(pos) => result.insert_str(pos + 1, &error),
+                        None => {
+                            result.push('\n');
+                            result.push_str(&error);
+                        }
+                    }
+                }
                 writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
                 result
             }

kani-driver/src/frontend/tests/schema_utils_test.rs

@@ -134,6 +134,7 @@ fn test_create_verification_result_json() {
         results: Ok(properties),
         runtime: Duration::from_millis(120),
         generated_concrete_test: false,
+        ignored_quantifiers: 0,
         coverage_results: None,
         cbmc_stats: None,
     };
@@ -207,6 +208,7 @@ fn test_add_runner_results_to_json_real() {
         results: Err(ExitStatus::Other(42)),
         runtime: Duration::from_millis(120),
         generated_concrete_test: false,
+        ignored_quantifiers: 0,
         coverage_results: None,
         cbmc_stats: None,
     };

kani-driver/src/sarif.rs

@@ -326,6 +326,7 @@ mod tests {
             results: Err(ExitStatus::Timeout),
             runtime: Duration::from_secs(1),
             generated_concrete_test: false,
+            ignored_quantifiers: 0,
             coverage_results: None,
             cbmc_stats: None,
         }
@@ -340,6 +341,7 @@ mod tests {
             results: Ok(vec![failure_property()]),
             runtime: Duration::from_secs(1),
             generated_concrete_test: false,
+            ignored_quantifiers: 0,
             coverage_results: None,
             cbmc_stats: None,
         };

tests/expected/quantifiers/dropped_quantifier_error.expected

@@ -0,0 +1,4 @@
+error: the solver backend does not support quantifiers with non-constant bounds and ignored 1 quantifier expression(s), replacing them with unconstrained values.
+Kani cannot soundly verify this harness: `kani::assume` calls containing such a quantifier are NOT enforced (a successful result would not cover the intended property), and `kani::assert` calls containing one may fail spuriously.
+Use an SMT solver backend that supports quantifiers, e.g. `#[kani::solver(z3)]`.
+VERIFICATION:- FAILED

tests/expected/quantifiers/dropped_quantifier_error.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zquantifiers
+
+//! Test that Kani fails with a sound-analysis error when the solver backend
+//! drops a quantifier it cannot encode. CBMC's SAT-based backends only support
+//! quantifiers with constant bounds; a quantifier with a symbolic bound is
+//! replaced by an unconstrained value (CBMC prints only a low-visibility
+//! "warning: ignoring forall"). That silently vacuates `kani::assume`s: without
+//! intervention this harness would report SUCCESSFUL only because the final
+//! assertion does not depend on the (unenforced) assumption -- an unsound false
+//! negative. Kani must instead surface the error and force a failure.
+
+extern crate kani;
+
+#[kani::proof]
+fn vacuous_assume_warns() {
+    let len: usize = kani::any();
+    kani::assume(len >= 1 && len <= 100);
+    let layout = std::alloc::Layout::array::<u8>(len).unwrap();
+    let p = unsafe { std::alloc::alloc(layout) };
+    kani::assume(!p.is_null());
+    unsafe {
+        kani::assume(kani::forall!(|i in (0, len)| *p.wrapping_add(i) < 60));
+    }
+    assert!(len <= 100);
+}