Add Arbitrary implementation for std::ascii::EscapeDefault

library/kani/src/arbitrary.rs

@@ -116,6 +116,52 @@ impl Arbitrary for std::char::EscapeUnicode {
     }
 }
 
+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);
+
+        // 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();
+        }
+        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

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

tests/expected/arbitrary/escape_default.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! 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;
+
+#[kani::proof]
+fn check_arbitrary_escape_default() {
+    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());
+
+    let count = remaining.iter().filter(|byte| byte.is_some()).count();
+
+    // 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], "front consumed");
+
+    // Observable back-consumed state: b"\\x00" -> b"\\x".
+    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], "front and back consumed");
+}

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)'] }

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

tests/script-based-pre/autoharness_ascii_escape_default/escape_default.expected

@@ -0,0 +1 @@
+| autoharness_ascii_escape_default | consume_escape_default | #[kani::proof] | Success |

tests/script-based-pre/autoharness_ascii_escape_default/escape_default.sh

@@ -0,0 +1,9 @@
+#!/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 ' '

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()
+}