Add Arbitrary implementation for std::ascii::EscapeDefault

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

tests/kani/ascii_escape_default.rs

@@ -0,0 +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 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();
+
+    // 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]);
+}

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,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 ' '

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