Split rmc::nondet into safe and unsafe functions(#607)

library/rmc/src/arbitrary.rs

@@ -0,0 +1,22 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// 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 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,
+{
+    fn any() -> Self {
+        let value = unsafe { any_raw::<T>() };
+        assume(value.is_valid());
+        value
+    }
+}

library/rmc/src/invariant.rs

@@ -0,0 +1,130 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// 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::*;
+
+/// 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.
+///
+/// Implementations of Invariant traits must ensure that the current bit values of the given type
+/// is valid and that all its invariants hold.
+///
+/// # Safety
+///
+/// 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.
+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 {
+        // RMC translates char into i32.
+        let val = *self as i32;
+        val <= 0xD7FF || (val >= 0xE000 && val <= 0x10FFFF)
+    }
+}
+
+unsafe impl<T: Invariant, const N: usize> Invariant for [T; N] {
+    fn is_valid(&self) -> bool {
+        self.iter().all(|e| e.is_valid())
+    }
+}
+
+unsafe impl<T> Invariant for Option<T>
+where
+    T: Invariant,
+{
+    #[inline(always)]
+    fn is_valid(&self) -> bool {
+        if let Some(v) = self { v.is_valid() } else { matches!(*self, None) }
+    }
+}
+
+unsafe impl<T, E> Invariant for Result<T, E>
+where
+    T: Invariant,
+    E: Invariant,
+{
+    #[inline(always)]
+    fn is_valid(&self) -> bool {
+        if let Ok(v) = self {
+            v.is_valid()
+        } else if let Err(e) = self {
+            e.is_valid()
+        } else {
+            false
+        }
+    }
+}
+
+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/rmc/src/lib.rs

@@ -2,8 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 #![feature(rustc_attrs)] // Used for rustc_diagnostic_item.
 
+pub mod arbitrary;
+pub mod invariant;
 pub mod slice;
 
+pub use arbitrary::Arbitrary;
+pub use invariant::Invariant;
+
 /// Creates an assumption that will be valid after this statement run. Note that the assumption
 /// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the
 /// program will exit successfully.
@@ -13,7 +18,7 @@ pub mod slice;
 /// The code snippet below should never panic.
 ///
 /// ```rust
-/// let i : i32 = rmc::nondet();
+/// let i : i32 = rmc::any();
 /// rmc::assume(i > 10);
 /// if i < 0 {
 ///   panic!("This will never panic");
@@ -23,30 +28,69 @@ pub mod slice;
 /// The following code may panic though:
 ///
 /// ```rust
-/// let i : i32 = rmc::nondet();
+/// let i : i32 = rmc::any();
 /// assert!(i < 0, "This may panic and verification should fail.");
 /// rmc::assume(i > 10);
 /// ```
 #[inline(never)]
 #[rustc_diagnostic_item = "RmcAssume"]
 pub fn assume(_cond: bool) {}
 
-/// This creates an unconstrained value of type `T`. You can assign the return value of this
+/// This creates an symbolic *valid* value of type `T`. You can assign the return value of this
 /// function to a variable that you want to make symbolic.
 ///
 /// # Example:
 ///
 /// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
-/// under all possible i32 input values.
+/// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero.
 ///
 /// ```rust
-/// let inputA = rmc::nondet::<i32>();
+/// let inputA = rmc::any::<std::num::NonZeroU8>();
 /// fn_under_verification(inputA);
 /// ```
+///
+/// Note: This is a safe construct and can only be used with types that implement the `Arbitrary`
+/// trait. The Arbitrary trait is used to build a symbolic value that represents all possible
+/// valid values for type `T`.
+#[inline(always)]
+pub fn any<T: Arbitrary>() -> T {
+    T::any()
+}
+
+/// 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 { rmc::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.:
+///
+/// ```rust
+/// let c = unsafe { rmc::any_raw::char() };
+/// rmc::assume(char::from_u32(c as u32).is_ok());
+/// ```
+///
+#[rustc_diagnostic_item = "RmcAnyRaw"]
+#[inline(never)]
+pub unsafe fn any_raw<T>() -> T {
+    unimplemented!("RMC any_raw")
+}
+
+/// This function has been split into a safe and unsafe functions: `rmc::any` and `rmc::any_raw`.
+#[deprecated]
 #[inline(never)]
-#[rustc_diagnostic_item = "RmcNonDet"]
-pub fn nondet<T>() -> T {
-    unimplemented!("RMC nondet")
+pub fn nondet<T: Arbitrary>() -> T {
+    any::<T>()
 }
 
 /// Function used in tests for cases where the condition is not always true.

library/rmc/src/slice.rs

@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::{assume, nondet};
+use crate::{any, any_raw, assume};
 use core::ops::{Deref, DerefMut};
 
 /// Given an array `arr` of length `LENGTH`, this function returns a **valid**
@@ -12,23 +12,23 @@ use core::ops::{Deref, DerefMut};
 ///
 /// ```rust
 /// let arr = [1, 2, 3];
-/// let slice = rmc::slice::nondet_slice_of_array(&arr);
+/// let slice = rmc::slice::any_slice_of_array(&arr);
 /// foo(slice); // where foo is a function that takes a slice and verifies a property about it
 /// ```
-pub fn nondet_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
-    let (from, to) = nondet_range::<LENGTH>();
+pub fn any_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
+    let (from, to) = any_range::<LENGTH>();
     &arr[from..to]
 }
 
 /// A mutable version of the previous function
-pub fn nondet_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) -> &mut [T] {
-    let (from, to) = nondet_range::<LENGTH>();
+pub fn any_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) -> &mut [T] {
+    let (from, to) = any_range::<LENGTH>();
     &mut arr[from..to]
 }
 
-fn nondet_range<const LENGTH: usize>() -> (usize, usize) {
-    let from: usize = nondet();
-    let to: usize = nondet();
+fn any_range<const LENGTH: usize>() -> (usize, usize) {
+    let from: usize = any();
+    let to: usize = any();
     assume(to <= LENGTH);
     assume(from <= to);
     (from, to)
@@ -38,12 +38,12 @@ fn nondet_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 `nondet_slice` to create an instance of this struct.
+/// property. Use `any_slice` to create an instance of this struct.
 ///
 /// # Example:
 ///
 /// ```rust
-/// let slice: rmc::slice::NonDetSlice<u8, 5> = rmc::slice::nondet_slice();
+/// let slice: rmc::slice::NonDetSlice<u8, 5> = rmc::slice::any_slice();
 /// foo(&slice); // where foo is a function that takes a slice and verifies a property about it
 /// ```
 pub struct NonDetSlice<T, const MAX_SLICE_LENGTH: usize> {
@@ -53,8 +53,8 @@ pub struct NonDetSlice<T, const MAX_SLICE_LENGTH: usize> {
 
 impl<T, const MAX_SLICE_LENGTH: usize> NonDetSlice<T, MAX_SLICE_LENGTH> {
     fn new() -> Self {
-        let arr: [T; MAX_SLICE_LENGTH] = nondet();
-        let slice_len: usize = nondet();
+        let arr: [T; MAX_SLICE_LENGTH] = unsafe { any_raw() };
+        let slice_len: usize = any();
         assume(slice_len <= MAX_SLICE_LENGTH);
         Self { arr, slice_len }
     }
@@ -82,6 +82,6 @@ impl<T, const MAX_SLICE_LENGTH: usize> DerefMut for NonDetSlice<T, MAX_SLICE_LEN
     }
 }
 
-pub fn nondet_slice<T, const MAX_SLICE_LENGTH: usize>() -> NonDetSlice<T, MAX_SLICE_LENGTH> {
+pub fn any_slice<T, const MAX_SLICE_LENGTH: usize>() -> NonDetSlice<T, MAX_SLICE_LENGTH> {
     NonDetSlice::<T, MAX_SLICE_LENGTH>::new()
 }

rmc-docs/src/tutorial-first-steps.md

@@ -71,7 +71,7 @@ The second command opens that report in your default browser (on mac, on linux d
 From this report, we can find the trace of the failure and filter through it to find the relevant line (at present time, an unfortunate amount of generated code is present in the trace):
 
 ```
-let x: u32 = rmc::nondet();
+let x: u32 = rmc::any();
 x = 1023u
 ```
 

rmc-docs/src/tutorial-kinds-of-failure.md

@@ -101,26 +101,26 @@ Having run `rmc --visualize` and clicked on one of the failures to see a trace,
 
 To navigate this trace to find the information you need, we recommend searching for things you expect to be somewhere in the trace:
 
-1. Search the document for `rmc::nondet` or `variable_of_interest =` such as `size =`.
+1. Search the document for `rmc::any` or `variable_of_interest =` such as `size =`.
 We can use this to find out what example values lead to a problem.
-In this case, where we just have a couple of `rmc::nondet` values in our proof harness, we can learn a lot just by seeing what these are.
+In this case, where we just have a couple of `rmc::any` values in our proof harness, we can learn a lot just by seeing what these are.
 In this trace we find (and the values you get may be different):
 
 ```
 Step 23: Function main, File tests/bounds-check.rs, Line 43
-let size: usize = rmc::nondet();
+let size: usize = rmc::any();
 size = 0ul
 
 Step 27: Function main, File tests/bounds-check.rs, Line 45
-let index: usize = rmc::nondet();
+let index: usize = rmc::any();
 index = 0ul
 
 Step 36: Function main, File tests/bounds-check.rs, Line 43
-let size: usize = rmc::nondet();
+let size: usize = rmc::any();
 size = 2464ul
 
 Step 39: Function main, File tests/bounds-check.rs, Line 45
-let index: usize = rmc::nondet();
+let index: usize = rmc::any();
 index = 2463ul
 ```
 

rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs

@@ -34,9 +34,9 @@ mod tests {
 #[cfg(rmc)]
 #[no_mangle]
 fn main() {
-    let size: usize = rmc::nondet();
+    let size: usize = rmc::any();
     rmc::assume(size < 4096);
-    let index: usize = rmc::nondet();
+    let index: usize = rmc::any();
     let array: Vec<u32> = vec![0; size];
     get_wrapped(index, &array);
 }

rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs

@@ -12,8 +12,8 @@ fn find_midpoint(low: u32, high: u32) -> u32 {
 #[cfg(rmc)]
 #[no_mangle]
 fn main() {
-    let a: u32 = rmc::nondet();
-    let b: u32 = rmc::nondet();
+    let a: u32 = rmc::any();
+    let b: u32 = rmc::any();
     find_midpoint(a, b);
 }
 // ANCHOR_END: rmc