|
| 1 | +// Copyright Kani Contributors |
| 2 | +// SPDX-License-Identifier: Apache-2.0 OR MIT |
| 3 | + |
| 4 | +//! Minimal reproducer / regression test for a CBMC symbolic-execution |
| 5 | +//! constant-propagation limitation exposed by rust-lang/rust#146436 |
| 6 | +//! ("Slice iter cleanup", first shipped in nightly-2025-12-04). |
| 7 | +//! |
| 8 | +//! After #146436, `ChunksExact::next` decides `Some`/`None` via |
| 9 | +//! `self.v.split_at_checked(chunk_size).and_then(..)` -- i.e. through the |
| 10 | +//! niche-encoded discriminant of `Option<(&[T], &[T])>`, which is the payload |
| 11 | +//! reference's null-ness. When the slice's data pointer has been turned into a |
| 12 | +//! symbolic null-select `(cond ? &obj : NULL)` by an upstream *symbolic-index* |
| 13 | +//! `split_at` (whose `None` case is niche-encoded as a null pointer), CBMC's |
| 14 | +//! symex can no longer fold that discriminant to a constant. The |
| 15 | +//! `chunks_exact` loop then unwinds to the `--unwind` bound instead of its true |
| 16 | +//! (concrete) trip count, blowing up symex/SAT. |
| 17 | +//! |
| 18 | +//! All three harnesses verify successfully -- the property is unchanged. The |
| 19 | +//! point of the reproducer is the encoding *cost*: `poisoned_chunks_exact` |
| 20 | +//! produces a much larger SAT instance than `control_clean` for the same-sized |
| 21 | +//! concrete chunking work. If the underlying CBMC issue is fixed (or the |
| 22 | +//! toolchain reverts the niche interaction), `poisoned_chunks_exact` bounds at |
| 23 | +//! its true trip count again and the cost collapses back to the control's. |
| 24 | +
|
| 25 | +// Clean pointer (no symbolic-index split): the chunking loop bounds at its |
| 26 | +// true trip count. |
| 27 | +#[kani::proof] |
| 28 | +#[kani::unwind(9)] |
| 29 | +fn control_clean() { |
| 30 | + let chunks: [u8; 4] = kani::any(); |
| 31 | + let mut sum = 0u64; |
| 32 | + for c in chunks.chunks_exact(2) { |
| 33 | + sum = sum.wrapping_add(c[0] as u64); |
| 34 | + } |
| 35 | + kani::cover!(sum != 999); |
| 36 | +} |
| 37 | + |
| 38 | +// A symbolic-index `split_at` poisons the slice's data pointer into a |
| 39 | +// `(cond ? base : NULL)` select; `chunks_exact` (which decides Some/None via |
| 40 | +// `split_at_checked(..).and_then(..)`) then over-unwinds even though `chunks` |
| 41 | +// has a concrete length of 4. |
| 42 | +#[kani::proof] |
| 43 | +#[kani::unwind(9)] |
| 44 | +fn poisoned_chunks_exact() { |
| 45 | + let arr: [u8; 16] = kani::any(); |
| 46 | + let idx: usize = kani::any(); |
| 47 | + kani::assume(idx <= 16); |
| 48 | + let (a, _) = arr.split_at(idx); |
| 49 | + if a.len() >= 4 { |
| 50 | + let chunks = &a[..4]; // concrete length 4, but a poisoned data pointer |
| 51 | + let mut sum = 0u64; |
| 52 | + for c in chunks.chunks_exact(2) { |
| 53 | + sum = sum.wrapping_add(c[0] as u64); |
| 54 | + } |
| 55 | + kani::cover!(sum != 999); |
| 56 | + } |
| 57 | +} |
| 58 | + |
| 59 | +// Negative control: the same poisoned slice fed to a direct `split_at_checked` |
| 60 | +// loop (no `and_then` closure updating a captured `&mut`) is NOT affected -- it |
| 61 | +// bounds normally. This shows both ingredients (the poisoned pointer *and* |
| 62 | +// `chunks_exact`'s `and_then` form) are required to trigger the blow-up. |
| 63 | +#[kani::proof] |
| 64 | +#[kani::unwind(9)] |
| 65 | +fn poisoned_split_at_checked() { |
| 66 | + let arr: [u8; 16] = kani::any(); |
| 67 | + let idx: usize = kani::any(); |
| 68 | + kani::assume(idx <= 16); |
| 69 | + let (a, _) = arr.split_at(idx); |
| 70 | + if a.len() >= 4 { |
| 71 | + let mut v = &a[..4]; |
| 72 | + let mut c = 0u64; |
| 73 | + while let Some((_h, t)) = v.split_at_checked(2) { |
| 74 | + v = t; |
| 75 | + c += 1; |
| 76 | + } |
| 77 | + kani::cover!(c != 999); |
| 78 | + } |
| 79 | +} |
0 commit comments