Upgrade Rust toolchain to nightly-2025-12-04

.github/workflows/kani.yml

@@ -60,6 +60,13 @@ jobs:
 
   perf:
     runs-on: ubuntu-24.04
+    # The full perf suite runs in ~45 min (matching main): most cases finish in
+    # seconds; the heaviest, s2n-quic-core, runs 34 harnesses in ~1500s. The
+    # per-test guardrail in scripts/kani-perf.sh (2400s) sits above that. The
+    # 180-min step timeout leaves ample headroom over that realistic runtime,
+    # and the job timeout sits above (step timeout) x (max_attempts) so a retry
+    # can still land.
+    timeout-minutes: 380
     permissions:
       contents: read
     steps:
@@ -72,7 +79,14 @@ jobs:
           os: ubuntu-24.04
 
       - name: Execute Kani performance tests
-        run: ./scripts/kani-perf.sh
+        # Retry on infra-driven failures (spot preemption / runner shutdown).
+        # The script itself bounds per-test wall time, so functional regressions
+        # surface as normal test failures and are not retried indefinitely.
+        uses: nick-fields/retry@v3
+        with:
+          timeout_minutes: 180
+          max_attempts: 2
+          command: ./scripts/kani-perf.sh
         env:
           RUST_TEST_THREADS: 1
 

kani-compiler/src/kani_middle/reachability.rs

@@ -32,13 +32,14 @@ use rustc_public::mir::{
 use rustc_public::rustc_internal;
 use rustc_public::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
 use rustc_public::{CrateDef, ItemKind};
+#[cfg(debug_assertions)]
 use rustc_session::config::OutputType;
+use std::collections::{HashMap, HashSet};
 use std::fmt::{Display, Formatter};
-use std::{
-    collections::{HashMap, HashSet},
-    fs::File,
-    io::{BufWriter, Write},
-};
+#[cfg(debug_assertions)]
+use std::fs::File;
+#[cfg(debug_assertions)]
+use std::io::{BufWriter, Write};
 
 use crate::kani_middle::coercion;
 use crate::kani_middle::coercion::CoercionBase;
@@ -580,6 +581,7 @@ impl CallGraph {
 
     /// Print the graph in DOT format to a file.
     /// See <https://graphviz.org/doc/info/lang.html> for more information.
+    #[cfg(debug_assertions)]
     fn dump_dot(&self, tcx: TyCtxt, initial: Option<MonoItem>) -> std::io::Result<()> {
         if let Ok(target) = std::env::var("KANI_REACH_DEBUG") {
             debug!(?target, "dump_dot");
@@ -608,6 +610,7 @@ impl CallGraph {
     }
 
     /// Write all notes to the given writer.
+    #[cfg(debug_assertions)]
     fn dump_all<W: Write>(&self, writer: &mut W) -> std::io::Result<()> {
         tracing::info!(nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_all");
         for node in &self.nodes {
@@ -621,6 +624,7 @@ impl CallGraph {
     }
 
     /// Write all notes that may have led to the discovery of the given target.
+    #[cfg(debug_assertions)]
     fn dump_reason<W: Write>(&self, writer: &mut W, target: &str) -> std::io::Result<()> {
         let mut queue: Vec<Node> =
             self.nodes.iter().filter(|item| item.to_string().contains(target)).cloned().collect();

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-12-03"
+channel = "nightly-2025-12-04"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

scripts/kani-fmt.sh

@@ -30,7 +30,13 @@ cargo fmt ${check_flag} || error=1
 # Check test source files.
 TESTS=("tests" "docs/src/tutorial")
 # Add ignore patterns for code we don't want to format.
-IGNORE=("*/perf/s2n-quic/*")
+# `*/perf/s2n-quic/*` excludes the upstream submodule.
+# `*/perf/overlays/*` excludes the overlay sources (see
+# `tests/perf/overlays/README.md`): these are partial copies of submodule
+# files staged for `cp -r` by `scripts/kani-perf.sh`, and they can reference
+# `mod` declarations whose siblings only exist in the submodule, so rustfmt
+# cannot standalone-parse them.
+IGNORE=("*/perf/s2n-quic/*" "*/perf/overlays/*")
 
 # Arguments for the find command for excluding the IGNORE paths
 IGNORE_ARGS=()

scripts/kani-perf.sh

@@ -26,8 +26,21 @@ done
 
 suite="perf"
 mode="cargo-kani-test"
-echo "Check compiletest suite=$suite mode=$mode"
-cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast
+# Bound each test's wall time so a runaway case (e.g. an OOM-prone harness)
+# fails as a normal test failure with output, instead of triggering an
+# unattributable runner OOM-kill / shutdown signal in CI.
+# The cap is a guardrail against runaway/OOM, not a tight performance bound,
+# so it must sit above the slowest legitimate test. The whole-crate s2n-quic
+# tests run many heavy harnesses back-to-back; s2n-quic-core (34 harnesses,
+# e.g. sync::spsc::alloc_test ~375s and inet::checksum::differential ~135s)
+# takes ~1500s on CI. It passes cap-free on main, whose full suite is ~2650s,
+# and this branch's suite matches that, so this is not a regression. Default
+# 2400s (40 min) clears s2n-quic-core with margin while the realistic suite
+# runtime (~45 min) stays well within the workflow step timeout.
+# Override via KANI_PERF_TEST_TIMEOUT.
+timeout_secs="${KANI_PERF_TEST_TIMEOUT:-2400}"
+echo "Check compiletest suite=$suite mode=$mode timeout=${timeout_secs}s"
+cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast --timeout "$timeout_secs"
 exit_code=$?
 
 echo "Cleaning up..."

tests/kani/Iterator/chunks_exact_split_at.rs

@@ -0,0 +1,79 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Minimal reproducer / regression test for a CBMC symbolic-execution
+//! constant-propagation limitation exposed by rust-lang/rust#146436
+//! ("Slice iter cleanup", first shipped in nightly-2025-12-04).
+//!
+//! After #146436, `ChunksExact::next` decides `Some`/`None` via
+//! `self.v.split_at_checked(chunk_size).and_then(..)` -- i.e. through the
+//! niche-encoded discriminant of `Option<(&[T], &[T])>`, which is the payload
+//! reference's null-ness. When the slice's data pointer has been turned into a
+//! symbolic null-select `(cond ? &obj : NULL)` by an upstream *symbolic-index*
+//! `split_at` (whose `None` case is niche-encoded as a null pointer), CBMC's
+//! symex can no longer fold that discriminant to a constant. The
+//! `chunks_exact` loop then unwinds to the `--unwind` bound instead of its true
+//! (concrete) trip count, blowing up symex/SAT.
+//!
+//! All three harnesses verify successfully -- the property is unchanged. The
+//! point of the reproducer is the encoding *cost*: `poisoned_chunks_exact`
+//! produces a much larger SAT instance than `control_clean` for the same-sized
+//! concrete chunking work. If the underlying CBMC issue is fixed (or the
+//! toolchain reverts the niche interaction), `poisoned_chunks_exact` bounds at
+//! its true trip count again and the cost collapses back to the control's.
+
+// Clean pointer (no symbolic-index split): the chunking loop bounds at its
+// true trip count.
+#[kani::proof]
+#[kani::unwind(9)]
+fn control_clean() {
+    let chunks: [u8; 4] = kani::any();
+    let mut sum = 0u64;
+    for c in chunks.chunks_exact(2) {
+        sum = sum.wrapping_add(c[0] as u64);
+    }
+    kani::cover!(sum != 999);
+}
+
+// A symbolic-index `split_at` poisons the slice's data pointer into a
+// `(cond ? base : NULL)` select; `chunks_exact` (which decides Some/None via
+// `split_at_checked(..).and_then(..)`) then over-unwinds even though `chunks`
+// has a concrete length of 4.
+#[kani::proof]
+#[kani::unwind(9)]
+fn poisoned_chunks_exact() {
+    let arr: [u8; 16] = kani::any();
+    let idx: usize = kani::any();
+    kani::assume(idx <= 16);
+    let (a, _) = arr.split_at(idx);
+    if a.len() >= 4 {
+        let chunks = &a[..4]; // concrete length 4, but a poisoned data pointer
+        let mut sum = 0u64;
+        for c in chunks.chunks_exact(2) {
+            sum = sum.wrapping_add(c[0] as u64);
+        }
+        kani::cover!(sum != 999);
+    }
+}
+
+// Negative control: the same poisoned slice fed to a direct `split_at_checked`
+// loop (no `and_then` closure updating a captured `&mut`) is NOT affected -- it
+// bounds normally. This shows both ingredients (the poisoned pointer *and*
+// `chunks_exact`'s `and_then` form) are required to trigger the blow-up.
+#[kani::proof]
+#[kani::unwind(9)]
+fn poisoned_split_at_checked() {
+    let arr: [u8; 16] = kani::any();
+    let idx: usize = kani::any();
+    kani::assume(idx <= 16);
+    let (a, _) = arr.split_at(idx);
+    if a.len() >= 4 {
+        let mut v = &a[..4];
+        let mut c = 0u64;
+        while let Some((_h, t)) = v.split_at_checked(2) {
+            v = t;
+            c += 1;
+        }
+        kani::cover!(c != 999);
+    }
+}