From e5bd1d8efb933e2ef4a5d5a4377a545d00a31b39 Mon Sep 17 00:00:00 2001 From: Aryan Arun Date: Sun, 6 Sep 2026 17:25:47 -0700 Subject: [PATCH 1/3] Add Arbitrary implementation for ascii EscapeDefault --- library/kani/src/arbitrary.rs | 43 +++++++++++++++++++ tests/kani/ascii_escape_default.rs | 20 +++++++++ .../Cargo.toml | 10 +++++ .../config.yml | 6 +++ .../escape_default.expected | 1 + .../escape_default.sh | 10 +++++ .../src/lib.rs | 8 ++++ 7 files changed, 98 insertions(+) create mode 100644 tests/kani/ascii_escape_default.rs create mode 100644 tests/script-based-pre/autoharness_ascii_escape_default/Cargo.toml create mode 100644 tests/script-based-pre/autoharness_ascii_escape_default/config.yml create mode 100644 tests/script-based-pre/autoharness_ascii_escape_default/escape_default.expected create mode 100755 tests/script-based-pre/autoharness_ascii_escape_default/escape_default.sh create mode 100644 tests/script-based-pre/autoharness_ascii_escape_default/src/lib.rs diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index b5562cd0574..66d6d545a81 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -71,6 +71,49 @@ impl Arbitrary for std::time::Duration { } } +impl Arbitrary for std::ascii::EscapeDefault { + fn any() -> Self { + // Generate any state reachable by consuming a freshly constructed + // EscapeDefault iterator from either end. + let mut escape = std::ascii::escape_default(u8::any()); + let len = escape.size_hint().0; + + let front = usize::from(u8::any()); + crate::assume(front <= len); + + let back = usize::from(u8::any()); + crate::assume(back <= len - front); + + if front >= 1 { + let _ = escape.next(); + } + if front >= 2 { + let _ = escape.next(); + } + if front >= 3 { + let _ = escape.next(); + } + if front >= 4 { + let _ = escape.next(); + } + + if back >= 1 { + let _ = escape.next_back(); + } + if back >= 2 { + let _ = escape.next_back(); + } + if back >= 3 { + let _ = escape.next_back(); + } + if back >= 4 { + let _ = escape.next_back(); + } + + escape + } +} + /// Generate a slice of *unbounded* nondeterministic length: a fresh allocation of /// nondeterministic size whose contents are nondeterministic, with element validity /// established by `slice_validity_assume` (a compiler hook that emits a quantified diff --git a/tests/kani/ascii_escape_default.rs b/tests/kani/ascii_escape_default.rs new file mode 100644 index 00000000000..b21034913f9 --- /dev/null +++ b/tests/kani/ascii_escape_default.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Ensure that kani::any can generate valid std::ascii::EscapeDefault states. + +use std::ascii::EscapeDefault; + +#[kani::proof] +fn check_arbitrary_escape_default() { + let escape: EscapeDefault = kani::any(); + let count = escape.count(); + + assert!(count <= 4); + + kani::cover!(count == 0); + kani::cover!(count == 1); + kani::cover!(count == 2); + kani::cover!(count == 3); + kani::cover!(count == 4); +} diff --git a/tests/script-based-pre/autoharness_ascii_escape_default/Cargo.toml b/tests/script-based-pre/autoharness_ascii_escape_default/Cargo.toml new file mode 100644 index 00000000000..636bd1b9957 --- /dev/null +++ b/tests/script-based-pre/autoharness_ascii_escape_default/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "autoharness_ascii_escape_default" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/autoharness_ascii_escape_default/config.yml b/tests/script-based-pre/autoharness_ascii_escape_default/config.yml new file mode 100644 index 00000000000..31d5fcb0e9c --- /dev/null +++ b/tests/script-based-pre/autoharness_ascii_escape_default/config.yml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +script: escape_default.sh +expected: escape_default.expected +exit_code: 0 diff --git a/tests/script-based-pre/autoharness_ascii_escape_default/escape_default.expected b/tests/script-based-pre/autoharness_ascii_escape_default/escape_default.expected new file mode 100644 index 00000000000..8a75b78c7c2 --- /dev/null +++ b/tests/script-based-pre/autoharness_ascii_escape_default/escape_default.expected @@ -0,0 +1 @@ +| autoharness_ascii_escape_default | consume_escape_default | #[kani::proof] | Success | diff --git a/tests/script-based-pre/autoharness_ascii_escape_default/escape_default.sh b/tests/script-based-pre/autoharness_ascii_escape_default/escape_default.sh new file mode 100755 index 00000000000..b86e9ed05f6 --- /dev/null +++ b/tests/script-based-pre/autoharness_ascii_escape_default/escape_default.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -euo pipefail + +cargo kani autoharness -Z autoharness --output-format=regular 2>&1 \ + | grep -E '^\| autoharness_ascii_escape_default \| consume_escape_default .*Success' \ + | tr -s ' ' diff --git a/tests/script-based-pre/autoharness_ascii_escape_default/src/lib.rs b/tests/script-based-pre/autoharness_ascii_escape_default/src/lib.rs new file mode 100644 index 00000000000..56b74b7152e --- /dev/null +++ b/tests/script-based-pre/autoharness_ascii_escape_default/src/lib.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#![allow(dead_code)] + +pub fn consume_escape_default(value: std::ascii::EscapeDefault) -> usize { + value.count() +} From fca69f564d05457859a76f570a939da4a7289cb1 Mon Sep 17 00:00:00 2001 From: Aryan Arun Date: Mon, 7 Sep 2026 23:06:25 -0700 Subject: [PATCH 2/3] Update Arbitrary implementation tests for std::ascii::EscapeDefault --- tests/kani/ascii_escape_default.rs | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/tests/kani/ascii_escape_default.rs b/tests/kani/ascii_escape_default.rs index b21034913f9..9f9e07b9a81 100644 --- a/tests/kani/ascii_escape_default.rs +++ b/tests/kani/ascii_escape_default.rs @@ -1,20 +1,34 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// + //! Ensure that kani::any can generate valid std::ascii::EscapeDefault states. use std::ascii::EscapeDefault; #[kani::proof] fn check_arbitrary_escape_default() { - let escape: EscapeDefault = kani::any(); - let count = escape.count(); + let mut escape: EscapeDefault = kani::any(); + + let remaining = [escape.next(), escape.next(), escape.next(), escape.next()]; + + // EscapeDefault yields at most four bytes. + assert!(escape.next().is_none()); - assert!(count <= 4); + let count = remaining.iter().filter(|byte| byte.is_some()).count(); + // Preserve the original remaining-length coverage. kani::cover!(count == 0); kani::cover!(count == 1); kani::cover!(count == 2); kani::cover!(count == 3); kani::cover!(count == 4); + + // Observable front-consumed state: b"\\x00" -> b"x00". + kani::cover!(remaining == [Some(b'x'), Some(b'0'), Some(b'0'), None]); + + // Observable back-consumed state: b"\\x00" -> b"\\x". + kani::cover!(remaining == [Some(b'\\'), Some(b'x'), None, None]); + + // Observable mixed front/back state: b"\\x00" -> b"x0". + kani::cover!(remaining == [Some(b'x'), Some(b'0'), None, None]); } From a60b9c91b65047065e2d61a8773f4e6c7858b430 Mon Sep 17 00:00:00 2001 From: acearyanarun Date: Mon, 28 Sep 2026 16:38:48 -0700 Subject: [PATCH 3/3] Move EscapeDefault Arbitrary test to expected suite and document unrolling Address review feedback on #4782: - Move tests/kani/ascii_escape_default.rs to tests/expected/arbitrary/escape_default.rs with an .expected file that requires all 8 cover properties to be satisfied, so unsatisfied covers (e.g. if next_back() generation is removed) fail the test. - Add a comment explaining that front/back consumption is unrolled to avoid requiring loop unwinding when generating an arbitrary value. --- library/kani/src/arbitrary.rs | 3 ++ .../arbitrary/escape_default.expected | 28 +++++++++++++++++++ .../arbitrary/escape_default.rs} | 23 +++++++-------- 3 files changed, 43 insertions(+), 11 deletions(-) create mode 100644 tests/expected/arbitrary/escape_default.expected rename tests/{kani/ascii_escape_default.rs => expected/arbitrary/escape_default.rs} (63%) diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 5ebdc777aa6..dc110a1578a 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -129,6 +129,9 @@ impl Arbitrary for std::ascii::EscapeDefault { let back = usize::from(u8::any()); crate::assume(back <= len - front); + // The front/back consumption below is unrolled by hand (EscapeDefault + // yields at most 4 bytes) rather than written as a loop, so generating + // an arbitrary value does not require loop unwinding during verification. if front >= 1 { let _ = escape.next(); } diff --git a/tests/expected/arbitrary/escape_default.expected b/tests/expected/arbitrary/escape_default.expected new file mode 100644 index 00000000000..81c6ebc9a95 --- /dev/null +++ b/tests/expected/arbitrary/escape_default.expected @@ -0,0 +1,28 @@ +Checking harness check_arbitrary_escape_default... + +Status: SATISFIED\ +Description: "0 bytes remaining" + +Status: SATISFIED\ +Description: "1 byte remaining" + +Status: SATISFIED\ +Description: "2 bytes remaining" + +Status: SATISFIED\ +Description: "3 bytes remaining" + +Status: SATISFIED\ +Description: "4 bytes remaining" + +Status: SATISFIED\ +Description: "front consumed" + +Status: SATISFIED\ +Description: "back consumed" + +Status: SATISFIED\ +Description: "front and back consumed" + +8 of 8 cover properties satisfied +1 successfully verified harnesses, 0 failures diff --git a/tests/kani/ascii_escape_default.rs b/tests/expected/arbitrary/escape_default.rs similarity index 63% rename from tests/kani/ascii_escape_default.rs rename to tests/expected/arbitrary/escape_default.rs index 9f9e07b9a81..c288704ccc6 100644 --- a/tests/kani/ascii_escape_default.rs +++ b/tests/expected/arbitrary/escape_default.rs @@ -1,7 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT - -//! Ensure that kani::any can generate valid std::ascii::EscapeDefault states. +// +//! Ensure that kani::any can generate valid std::ascii::EscapeDefault states, +//! including states consumed from the front, from the back, and from both ends. use std::ascii::EscapeDefault; @@ -16,19 +17,19 @@ fn check_arbitrary_escape_default() { let count = remaining.iter().filter(|byte| byte.is_some()).count(); - // Preserve the original remaining-length coverage. - kani::cover!(count == 0); - kani::cover!(count == 1); - kani::cover!(count == 2); - kani::cover!(count == 3); - kani::cover!(count == 4); + // Every remaining length from fully consumed to fully unconsumed is reachable. + kani::cover!(count == 0, "0 bytes remaining"); + kani::cover!(count == 1, "1 byte remaining"); + kani::cover!(count == 2, "2 bytes remaining"); + kani::cover!(count == 3, "3 bytes remaining"); + kani::cover!(count == 4, "4 bytes remaining"); // Observable front-consumed state: b"\\x00" -> b"x00". - kani::cover!(remaining == [Some(b'x'), Some(b'0'), Some(b'0'), None]); + kani::cover!(remaining == [Some(b'x'), Some(b'0'), Some(b'0'), None], "front consumed"); // Observable back-consumed state: b"\\x00" -> b"\\x". - kani::cover!(remaining == [Some(b'\\'), Some(b'x'), None, None]); + kani::cover!(remaining == [Some(b'\\'), Some(b'x'), None, None], "back consumed"); // Observable mixed front/back state: b"\\x00" -> b"x0". - kani::cover!(remaining == [Some(b'x'), Some(b'0'), None, None]); + kani::cover!(remaining == [Some(b'x'), Some(b'0'), None, None], "front and back consumed"); }