From 39cdc17e8ff0a8062a344782d0d9cf5b83c12592 Mon Sep 17 00:00:00 2001
From: zhaojieyou <zjyscu@gmail.com>
Date: Mon, 7 Sep 2026 03:28:45 -0700
Subject: [PATCH] Add Arbitrary impl for char EscapeUnicode

---
 library/kani/src/arbitrary.rs                 | 45 +++++++++++++++++++
 tests/kani/char_escape_unicode.rs             | 26 +++++++++++
 .../Cargo.toml                                | 10 +++++
 .../config.yml                                |  6 +++
 .../escape_unicode.expected                   |  1 +
 .../escape_unicode.sh                         | 10 +++++
 .../src/lib.rs                                |  8 ++++
 7 files changed, 106 insertions(+)
 create mode 100644 tests/kani/char_escape_unicode.rs
 create mode 100644 tests/script-based-pre/autoharness_char_escape_unicode/Cargo.toml
 create mode 100644 tests/script-based-pre/autoharness_char_escape_unicode/config.yml
 create mode 100644 tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.expected
 create mode 100755 tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.sh
 create mode 100644 tests/script-based-pre/autoharness_char_escape_unicode/src/lib.rs

diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index b5562cd0574..35e0bfcde9b 100644
--- a/library/kani/src/arbitrary.rs
+++ b/library/kani/src/arbitrary.rs
@@ -71,6 +71,51 @@ impl Arbitrary for std::time::Duration {
     }
 }
 
+impl Arbitrary for std::char::EscapeUnicode {
+    fn any() -> Self {
+        // Generate any state reachable by consuming a freshly constructed
+        // EscapeUnicode iterator from the front.
+        let mut escape = char::any().escape_unicode();
+        let len = escape.len();
+
+        let front = usize::from(u8::any());
+        crate::assume(front <= len);
+
+        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 front >= 5 {
+            let _ = escape.next();
+        }
+        if front >= 6 {
+            let _ = escape.next();
+        }
+        if front >= 7 {
+            let _ = escape.next();
+        }
+        if front >= 8 {
+            let _ = escape.next();
+        }
+        if front >= 9 {
+            let _ = escape.next();
+        }
+        if front >= 10 {
+            let _ = escape.next();
+        }
+
+        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/char_escape_unicode.rs b/tests/kani/char_escape_unicode.rs
new file mode 100644
index 00000000000..d60d46e7c47
--- /dev/null
+++ b/tests/kani/char_escape_unicode.rs
@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Ensure that `kani::any` can generate valid `std::char::EscapeUnicode` states.
+
+use std::char::EscapeUnicode;
+
+#[kani::proof]
+fn check_arbitrary_escape_unicode() {
+    let escape: EscapeUnicode = kani::any();
+    let count = escape.count();
+
+    assert!(count <= 10);
+
+    kani::cover!(count == 0);
+    kani::cover!(count == 1);
+    kani::cover!(count == 2);
+    kani::cover!(count == 3);
+    kani::cover!(count == 4);
+    kani::cover!(count == 5);
+    kani::cover!(count == 6);
+    kani::cover!(count == 7);
+    kani::cover!(count == 8);
+    kani::cover!(count == 9);
+    kani::cover!(count == 10);
+}
diff --git a/tests/script-based-pre/autoharness_char_escape_unicode/Cargo.toml b/tests/script-based-pre/autoharness_char_escape_unicode/Cargo.toml
new file mode 100644
index 00000000000..8450afe260e
--- /dev/null
+++ b/tests/script-based-pre/autoharness_char_escape_unicode/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "autoharness_char_escape_unicode"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/autoharness_char_escape_unicode/config.yml b/tests/script-based-pre/autoharness_char_escape_unicode/config.yml
new file mode 100644
index 00000000000..fe817c099f9
--- /dev/null
+++ b/tests/script-based-pre/autoharness_char_escape_unicode/config.yml
@@ -0,0 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+script: escape_unicode.sh
+expected: escape_unicode.expected
+exit_code: 0
diff --git a/tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.expected b/tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.expected
new file mode 100644
index 00000000000..5f75b0f0151
--- /dev/null
+++ b/tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.expected
@@ -0,0 +1 @@
+| autoharness_char_escape_unicode | consume_escape_unicode | #[kani::proof] | Success |
diff --git a/tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.sh b/tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.sh
new file mode 100755
index 00000000000..77db7d6f1bb
--- /dev/null
+++ b/tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.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_char_escape_unicode \| consume_escape_unicode .*Success' \
+    | tr -s ' '
diff --git a/tests/script-based-pre/autoharness_char_escape_unicode/src/lib.rs b/tests/script-based-pre/autoharness_char_escape_unicode/src/lib.rs
new file mode 100644
index 00000000000..2952f024ed8
--- /dev/null
+++ b/tests/script-based-pre/autoharness_char_escape_unicode/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_unicode(value: std::char::EscapeUnicode) -> usize {
+    value.count()
+}