Deprecate any_raw and Invariant (rust-lang#1415)

* Add perf tests for kani::any() implementations

Also change script to use release build instead of regular build.

* Deprecate any_raw and Invariant

Basically invariant type was only safe for T that had no invalid
value independent on its binary values. All other types had some sort of
UB involved. Thus, deprecate this for now.

Note that we will likely want the Invariant type reintroduced one day,
but we might need to either change its form or ensure that `any_raw()`
at least respect `primitives` and `std` type invariants to avoid users
having to explicitly check for any potential UB (which in itself is UB).

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Author: celinval

Cargo.toml

@@ -55,4 +55,6 @@ exclude = [
   "tests/kani-dependency-test/dependency3",
   # cargo kani tests should also have their own workspace
   "tests/cargo-kani",
+  "tests/perf",
+  "tests/cargo-ui",
 ]

kani-driver/src/call_cbmc.rs

@@ -54,6 +54,7 @@ impl KaniSession {
                 // the best possible fix is port to rust instead of using python, or getting more
                 // feedback than just exit status (or using a particular magic exit code?)
             }
+            // TODO: We should print this even the verification fails but not if it crashes.
             println!("Verification Time: {}s", elapsed);
         }
 

library/kani/src/arbitrary.rs

@@ -1,39 +1,102 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! This module introduces the Arbitrary trait as well as implementation for the Invariant trait.
-use crate::{any_raw, assume, Invariant};
+//! This module introduces the Arbitrary trait as well as implementation for primitive types and
+//! other std containers.
+use std::num::*;
 
 /// This trait should be used to generate symbolic variables that represent any valid value of
 /// its type.
 pub trait Arbitrary {
     fn any() -> Self;
 }
 
-impl<T> Arbitrary for T
-where
-    T: Invariant,
-{
-    default fn any() -> Self {
-        let value = unsafe { any_raw::<T>() };
-        assume(value.is_valid());
-        value
+/// The given type can be represented by an unconstrained symbolic value of size_of::<T>.
+macro_rules! trivial_arbitrary {
+    ( $type: ty ) => {
+        impl Arbitrary for $type {
+            #[inline(always)]
+            fn any() -> Self {
+                unsafe { crate::any_raw_internal::<$type>() }
+            }
+        }
+    };
+}
+
+trivial_arbitrary!(u8);
+trivial_arbitrary!(u16);
+trivial_arbitrary!(u32);
+trivial_arbitrary!(u64);
+trivial_arbitrary!(u128);
+trivial_arbitrary!(usize);
+
+trivial_arbitrary!(i8);
+trivial_arbitrary!(i16);
+trivial_arbitrary!(i32);
+trivial_arbitrary!(i64);
+trivial_arbitrary!(i128);
+trivial_arbitrary!(isize);
+
+// We do not constraint floating points values per type spec. Users must add assumptions to their
+// verification code if they want to eliminate NaN, infinite, or subnormal.
+trivial_arbitrary!(f32);
+trivial_arbitrary!(f64);
+
+trivial_arbitrary!(());
+
+impl Arbitrary for bool {
+    #[inline(always)]
+    fn any() -> Self {
+        let byte = u8::any();
+        byte == 0
+    }
+}
+
+/// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF]
+/// Ref: <https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html>
+impl Arbitrary for char {
+    #[inline(always)]
+    fn any() -> Self {
+        // Generate an arbitrary u32 and constrain it to make it a valid representation of char.
+        let val = u32::any();
+        crate::assume(val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val));
+        unsafe { char::from_u32_unchecked(val) }
     }
 }
 
+macro_rules! nonzero_arbitrary {
+    ( $type: ty, $base: ty ) => {
+        impl Arbitrary for $type {
+            #[inline(always)]
+            fn any() -> Self {
+                let val = <$base>::any();
+                crate::assume(val != 0);
+                unsafe { <$type>::new_unchecked(val) }
+            }
+        }
+    };
+}
+
+nonzero_arbitrary!(NonZeroU8, u8);
+nonzero_arbitrary!(NonZeroU16, u16);
+nonzero_arbitrary!(NonZeroU32, u32);
+nonzero_arbitrary!(NonZeroU64, u64);
+nonzero_arbitrary!(NonZeroU128, u128);
+nonzero_arbitrary!(NonZeroUsize, usize);
+
+nonzero_arbitrary!(NonZeroI8, i8);
+nonzero_arbitrary!(NonZeroI16, i16);
+nonzero_arbitrary!(NonZeroI32, i32);
+nonzero_arbitrary!(NonZeroI64, i64);
+nonzero_arbitrary!(NonZeroI128, i128);
+nonzero_arbitrary!(NonZeroIsize, isize);
+
 impl<T, const N: usize> Arbitrary for [T; N]
 where
     T: Arbitrary,
 {
     fn any() -> Self {
-        // The "correct way" would be to MaybeUninit but there is performance penalty.
-        let mut data: [T; N] = unsafe { crate::any_raw() };
-
-        for elem in &mut data[..] {
-            *elem = T::any();
-        }
-
-        data
+        [(); N].map(|_| T::any())
     }
 }
 

library/kani/src/invariant.rs

@@ -1,8 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! This module introduces the Invariant trait as well as implementation for commonly used types.
-use std::num::*;
+//! This module introduces the Invariant trait.
+
+use crate::Arbitrary;
 
 /// Types that implement a check to ensure its value is valid and safe to be used. See
 /// <https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html> for examples of valid values.
@@ -14,84 +15,33 @@ use std::num::*;
 ///
 /// This trait is unsafe since &self might represent an invalid value. The `is_valid()` function
 /// must return `true` if and only if the invariant of its type is held.
+///
+/// # Deprecation
+///
+/// We have decided to deprecate this trait in favor of using `Arbitrary` for now. The main
+/// benefit of using Invariant was to avoid calling `kani::any_raw()` followed by `kani::assume()`.
+/// However, `kani::any_raw()` today cannot guarantee the rust type validity invariants, which
+/// could lead to UB in our analysis.
+#[deprecated(
+    since = "0.8.0",
+    note = "With `kani::Invariant`, Kani cannot guarantee that the type respects the language \
+    type invariants which may trigger UB. Use `kani::Arbitrary` instead."
+)]
 pub unsafe trait Invariant {
     /// Check if `&self` holds a valid value that respect the type invariant.
     /// This function must return `true` if and only if `&self` is valid.
     fn is_valid(&self) -> bool;
 }
 
-macro_rules! empty_invariant {
-    ( $type: ty ) => {
-        unsafe impl Invariant for $type {
-            #[inline(always)]
-            fn is_valid(&self) -> bool {
-                true
-            }
-        }
-    };
-}
-
-empty_invariant!(u8);
-empty_invariant!(u16);
-empty_invariant!(u32);
-empty_invariant!(u64);
-empty_invariant!(u128);
-empty_invariant!(usize);
-
-empty_invariant!(i8);
-empty_invariant!(i16);
-empty_invariant!(i32);
-empty_invariant!(i64);
-empty_invariant!(i128);
-empty_invariant!(isize);
-
-// We do not constraint floating points values per type spec. Users must add assumptions to their
-// verification code if they want to eliminate NaN, infinite, or subnormal.
-empty_invariant!(f32);
-empty_invariant!(f64);
-
-empty_invariant!(());
-
-unsafe impl Invariant for bool {
-    #[inline(always)]
-    fn is_valid(&self) -> bool {
-        let byte = u8::from(*self);
-        byte == 0 || byte == 1
-    }
-}
-
-/// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF]
-/// Ref: <https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html>
-unsafe impl Invariant for char {
-    #[inline(always)]
-    fn is_valid(&self) -> bool {
-        // Kani translates char into i32.
-        let val = *self as i32;
-        val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val)
+// We cannot apply #[deprecated] to trait impl so add this to ignore the deprecation warnings.
+#[allow(deprecated)]
+impl<T> Arbitrary for T
+where
+    T: Invariant,
+{
+    default fn any() -> Self {
+        let value = unsafe { crate::any_raw_internal::<T>() };
+        crate::assume(value.is_valid());
+        value
     }
 }
-
-macro_rules! nonzero_invariant {
-    ( $type: ty ) => {
-        unsafe impl Invariant for $type {
-            #[inline(always)]
-            fn is_valid(&self) -> bool {
-                self.get() != 0
-            }
-        }
-    };
-}
-
-nonzero_invariant!(NonZeroU8);
-nonzero_invariant!(NonZeroU16);
-nonzero_invariant!(NonZeroU32);
-nonzero_invariant!(NonZeroU64);
-nonzero_invariant!(NonZeroU128);
-nonzero_invariant!(NonZeroUsize);
-
-nonzero_invariant!(NonZeroI8);
-nonzero_invariant!(NonZeroI16);
-nonzero_invariant!(NonZeroI32);
-nonzero_invariant!(NonZeroI64);
-nonzero_invariant!(NonZeroI128);
-nonzero_invariant!(NonZeroIsize);

library/kani/src/lib.rs

@@ -11,6 +11,7 @@ pub mod vec;
 
 pub use arbitrary::Arbitrary;
 pub use futures::block_on;
+#[allow(deprecated)]
 pub use invariant::Invariant;
 
 /// Creates an assumption that will be valid after this statement run. Note that the assumption
@@ -76,38 +77,32 @@ pub fn any<T: Arbitrary>() -> T {
 
 /// This function creates an unconstrained value of type `T`. This may result in an invalid value.
 ///
-/// # Example:
-///
-/// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
-/// under all possible values of char, including invalid ones that are greater than char::MAX.
-///
-/// ```rust
-/// let inputA = unsafe { kani::any_raw::<char>() };
-/// fn_under_verification(inputA);
-/// ```
-///
 /// # Safety
 ///
 /// This function is unsafe and it may represent invalid `T` values which can lead to many
-/// undesirable undefined behaviors. Users must validate that the symbolic variable respects
-/// the type invariant as well as any other constraint relevant to their usage. E.g.:
+/// undesirable undefined behaviors. Users must guarantee that an unconstrained symbolic value
+/// for type T only represents valid values.
 ///
-/// ```rust
-/// let c = unsafe { kani::any_raw::char() };
-/// kani::assume(char::from_u32(c as u32).is_ok());
-/// ```
+/// # Deprecation
 ///
-#[rustc_diagnostic_item = "KaniAnyRaw"]
+/// We have decided to deprecate this function due to the fact that its result can be the source
+/// of undefined behavior.
 #[inline(never)]
+#[deprecated(
+    since = "0.8.0",
+    note = "This function may return symbolic values that don't respects the language type invariants."
+)]
+#[doc(hidden)]
 pub unsafe fn any_raw<T>() -> T {
-    unimplemented!("Kani any_raw")
+    any_raw_internal()
 }
 
-/// This function has been split into a safe and unsafe functions: `kani::any` and `kani::any_raw`.
-#[deprecated]
+/// This function will replace `any_raw` that has been deprecated and it should only be used
+/// internally when we can guarantee that it will not trigger any undefined behavior.
+#[rustc_diagnostic_item = "KaniAnyRaw"]
 #[inline(never)]
-pub fn nondet<T: Arbitrary>() -> T {
-    any::<T>()
+pub(crate) unsafe fn any_raw_internal<T>() -> T {
+    unimplemented!("Kani any_raw")
 }
 
 /// Function used in tests for cases where the condition is not always true.
@@ -123,6 +118,7 @@ pub fn expect_fail(_cond: bool, _message: &'static str) {}
 /// overrides, but not the other way around.
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniPanic"]
+#[doc(hidden)]
 pub fn panic(message: &'static str) -> ! {
     panic!("{}", message)
 }

library/kani/src/slice.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::{any, any_raw, assume, Arbitrary};
+use crate::{any, any_raw_internal, assume, Arbitrary};
 use std::alloc::{alloc, dealloc, Layout};
 use std::ops::{Deref, DerefMut};
 
@@ -39,8 +39,7 @@ fn any_range<const LENGTH: usize>() -> (usize, usize) {
 /// between `0..=MAX_SLICE_LENGTH` and with non-deterministic content.  This is
 /// useful in situations where one wants to verify that all slices with any
 /// content and with a length up to `MAX_SLICE_LENGTH` satisfy a certain
-/// property. Use `any_slice` or `any_raw_slice` to create an instance of this
-/// struct.
+/// property. Use `any_slice` to create an instance of this struct.
 ///
 /// # Example:
 ///
@@ -79,13 +78,17 @@ impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
         any_slice
     }
 
+    #[deprecated(
+        since = "0.8.0",
+        note = "This function may return symbolic values that don't respects the language type invariants."
+    )]
     fn new_raw() -> Self {
         let any_slice = AnySlice::<T, MAX_SLICE_LENGTH>::alloc_slice();
         unsafe {
             let mut i = 0;
             // See note on `MAX_SLICE_LENGTH` in `new` method above
             while i < any_slice.slice_len && i < MAX_SLICE_LENGTH {
-                *any_slice.ptr.add(i) = any_raw();
+                *any_slice.ptr.add(i) = any_raw_internal();
                 i += 1;
             }
         }
@@ -151,8 +154,18 @@ where
 
 /// # Safety
 ///
-/// TODO: Safety of any_raw_slice is a complex matter. See
-/// https://github.com/model-checking/kani/issues/1394
+/// Users must guarantee that an unconstrained symbolic value for type T only represents valid
+/// values.
+///
+/// # Deprecated
+///
+/// This has been deprecated due to its limited value and high risk of generating undefined
+/// behavior.
+#[allow(deprecated)]
+#[deprecated(
+    since = "0.8.0",
+    note = "This function may return symbolic values that don't respects the language type invariants."
+)]
 pub unsafe fn any_raw_slice<T, const MAX_SLICE_LENGTH: usize>() -> AnySlice<T, MAX_SLICE_LENGTH> {
     AnySlice::<T, MAX_SLICE_LENGTH>::new_raw()
 }