From e5bd1d8efb933e2ef4a5d5a4377a545d00a31b39 Mon Sep 17 00:00:00 2001 From: Aryan Arun Date: Sun, 6 Sep 2026 17:25:47 -0700 Subject: [PATCH 1/2] 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/2] 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]); }