From 0be79d6fcccac8a9c735e84badaf67c4be4a8c6e Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Thu, 1 Aug 2024 16:29:15 -0400
Subject: [PATCH] char and ascii_char contracts (#48)

Add contracts for `char_try_from_u32`, `from_u32_unchecked`,
`from_u8_unchecked`, `from_u8`, and `as_ascii`.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 library/core/src/ascii/ascii_char.rs | 26 ++++++++++++++++++++++++++
 library/core/src/char/convert.rs     | 18 ++++++++++++++++++
 library/core/src/char/methods.rs     | 27 +++++++++++++++++++++++++++
 3 files changed, 71 insertions(+)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 34a05ac38884d..4d81eae9ccb83 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -3,9 +3,13 @@
 //! suggestions from rustc if you get anything slightly wrong in here, and overall
 //! helps with clarity as we're also referring to `char` intentionally in here.
 
+use safety::{ensures, requires};
 use crate::fmt::{self, Write};
 use crate::mem::transmute;
 
+#[cfg(kani)]
+use crate::kani;
+
 /// One of the 128 Unicode characters from U+0000 through U+007F,
 /// often known as the [ASCII] subset.
 ///
@@ -449,6 +453,7 @@ impl AsciiChar {
     /// or returns `None` if it's too large.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
+    #[ensures(|result| (b <= 127) == (result.is_some() && result.unwrap() as u8 == b))]
     pub const fn from_u8(b: u8) -> Option<Self> {
         if b <= 127 {
             // SAFETY: Just checked that `b` is in-range
@@ -466,6 +471,8 @@ impl AsciiChar {
     /// `b` must be in `0..=127`, or else this is UB.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
+    #[requires(b <= 127)]
+    #[ensures(|result| *result as u8 == b)]
     pub const unsafe fn from_u8_unchecked(b: u8) -> Self {
         // SAFETY: Our safety precondition is that `b` is in-range.
         unsafe { transmute(b) }
@@ -616,3 +623,22 @@ impl fmt::Debug for AsciiChar {
         f.write_char('\'')
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+    use AsciiChar;
+
+    #[kani::proof_for_contract(AsciiChar::from_u8)]
+    fn check_from_u8() {
+        let b: u8 = kani::any();
+        AsciiChar::from_u8(b);
+    }
+
+    #[kani::proof_for_contract(AsciiChar::from_u8_unchecked)]
+    fn check_from_u8_unchecked() {
+        let b: u8 = kani::any();
+        unsafe { AsciiChar::from_u8_unchecked(b) };
+    }
+}
diff --git a/library/core/src/char/convert.rs b/library/core/src/char/convert.rs
index f0c2636307fcf..698c85fcd1301 100644
--- a/library/core/src/char/convert.rs
+++ b/library/core/src/char/convert.rs
@@ -1,5 +1,6 @@
 //! Character conversions.
 
+use safety::{requires, ensures};
 use crate::char::TryFromCharError;
 use crate::error::Error;
 use crate::fmt;
@@ -7,6 +8,9 @@ use crate::mem::transmute;
 use crate::str::FromStr;
 use crate::ub_checks::assert_unsafe_precondition;
 
+#[cfg(kani)]
+use crate::kani;
+
 /// Converts a `u32` to a `char`. See [`char::from_u32`].
 #[must_use]
 #[inline]
@@ -21,6 +25,8 @@ pub(super) const fn from_u32(i: u32) -> Option<char> {
 /// Converts a `u32` to a `char`, ignoring validity. See [`char::from_u32_unchecked`].
 #[inline]
 #[must_use]
+#[requires(char_try_from_u32(i).is_ok())]
+#[ensures(|result| *result as u32 == i)]
 pub(super) const unsafe fn from_u32_unchecked(i: u32) -> char {
     // SAFETY: the caller must guarantee that `i` is a valid char value.
     unsafe {
@@ -290,3 +296,15 @@ pub(super) const fn from_digit(num: u32, radix: u32) -> Option<char> {
         None
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(from_u32_unchecked)]
+    fn check_from_u32_unchecked() {
+        let i: u32 = kani::any();
+        unsafe { from_u32_unchecked(i) };
+    }
+}
diff --git a/library/core/src/char/methods.rs b/library/core/src/char/methods.rs
index 4186565c131ed..21451b082d863 100644
--- a/library/core/src/char/methods.rs
+++ b/library/core/src/char/methods.rs
@@ -5,6 +5,9 @@ use crate::str::from_utf8_unchecked_mut;
 use crate::unicode::printable::is_printable;
 use crate::unicode::{self, conversions};
 
+#[cfg(kani)]
+use crate::kani;
+
 use super::*;
 
 impl char {
@@ -1836,3 +1839,27 @@ pub fn encode_utf16_raw(mut code: u32, dst: &mut [u16]) -> &mut [u16] {
         }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+    use safety::ensures;
+
+    #[ensures(|result| c.is_ascii() == (result.is_some() && (result.unwrap() as u8 as char == *c)))]
+    fn as_ascii_clone(c: &char) -> Option<ascii::Char> {
+        c.as_ascii()
+    }
+
+    #[kani::proof_for_contract(as_ascii_clone)]
+    fn check_as_ascii_ascii_char() {
+        let ascii: char = kani::any_where(|c : &char| c.is_ascii());
+        as_ascii_clone(&ascii);
+    }
+
+    #[kani::proof_for_contract(as_ascii_clone)]
+    fn check_as_ascii_non_ascii_char() {
+        let non_ascii: char = kani::any_where(|c: &char| !c.is_ascii());
+        as_ascii_clone(&non_ascii);
+    }
+}