Skip to content

Commit be69bc3

Browse files
celinvalzhassan-awsadpaco-aws
authored and
tedinski
committed
Split rmc::nondet into safe and unsafe functions(rust-lang#607) (rust-lang#657)
* Introduce rmc::any and rmc::any_raw and deprecate rmc::nondet We decided to replace the old method rmc::nondet because its behavior wasn't clear. For some types it would respect the type invariants but not for others. Additionally, there was no way for the user to specify how to create safe non-deterministic values. Users will be able to control how RMC generate symbolic values to their variables. - `rmc::any::<T>()` will provide a safe way to generate values that respect any invariant specified to type T (Given by the implementation of Arbitrary trait.) - `rmc::any_raw::<T>()` will provide any possible bit value for the memory layout of the type. This is an unsafe method and users must ensure correctness after this call. Co-authored-by: Zyad Hassan <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>
1 parent 2c50840 commit be69bc3

File tree

117 files changed

+868
-838
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

117 files changed

+868
-838
lines changed

‎library/rmc/src/arbitrary.rs

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
//! This module introduces the Arbitrary trait as well as implementation for the Invariant trait.
5+
use crate::{any_raw, assume, Invariant};
6+
7+
/// This trait should be used to generate symbolic variables that represent any valid value of
8+
/// its type.
9+
pub trait Arbitrary {
10+
fn any() -> Self;
11+
}
12+
13+
impl<T> Arbitrary for T
14+
where
15+
T: Invariant,
16+
{
17+
fn any() -> Self {
18+
let value = unsafe { any_raw::<T>() };
19+
assume(value.is_valid());
20+
value
21+
}
22+
}

‎library/rmc/src/invariant.rs

+130
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
//! This module introduces the Invariant trait as well as implementation for commonly used types.
5+
use std::num::*;
6+
7+
/// Types that implement a check to ensure its value is valid and safe to be used. See
8+
/// https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html for examples of valid values.
9+
///
10+
/// Implementations of Invariant traits must ensure that the current bit values of the given type
11+
/// is valid and that all its invariants hold.
12+
///
13+
/// # Safety
14+
///
15+
/// This trait is unsafe since &self might represent an invalid value. The `is_valid()` function
16+
/// must return `true` if and only if the invariant of its type is held.
17+
pub unsafe trait Invariant {
18+
/// Check if `&self` holds a valid value that respect the type invariant.
19+
/// This function must return `true` if and only if `&self` is valid.
20+
fn is_valid(&self) -> bool;
21+
}
22+
23+
macro_rules! empty_invariant {
24+
( $type: ty ) => {
25+
unsafe impl Invariant for $type {
26+
#[inline(always)]
27+
fn is_valid(&self) -> bool {
28+
true
29+
}
30+
}
31+
};
32+
}
33+
34+
empty_invariant!(u8);
35+
empty_invariant!(u16);
36+
empty_invariant!(u32);
37+
empty_invariant!(u64);
38+
empty_invariant!(u128);
39+
empty_invariant!(usize);
40+
41+
empty_invariant!(i8);
42+
empty_invariant!(i16);
43+
empty_invariant!(i32);
44+
empty_invariant!(i64);
45+
empty_invariant!(i128);
46+
empty_invariant!(isize);
47+
48+
// We do not constraint floating points values per type spec. Users must add assumptions to their
49+
// verification code if they want to eliminate NaN, infinite, or subnormal.
50+
empty_invariant!(f32);
51+
empty_invariant!(f64);
52+
53+
empty_invariant!(());
54+
55+
unsafe impl Invariant for bool {
56+
#[inline(always)]
57+
fn is_valid(&self) -> bool {
58+
let byte = u8::from(*self);
59+
byte == 0 || byte == 1
60+
}
61+
}
62+
63+
/// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF]
64+
/// Ref: https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html
65+
unsafe impl Invariant for char {
66+
#[inline(always)]
67+
fn is_valid(&self) -> bool {
68+
// RMC translates char into i32.
69+
let val = *self as i32;
70+
val <= 0xD7FF || (val >= 0xE000 && val <= 0x10FFFF)
71+
}
72+
}
73+
74+
unsafe impl<T: Invariant, const N: usize> Invariant for [T; N] {
75+
fn is_valid(&self) -> bool {
76+
self.iter().all(|e| e.is_valid())
77+
}
78+
}
79+
80+
unsafe impl<T> Invariant for Option<T>
81+
where
82+
T: Invariant,
83+
{
84+
#[inline(always)]
85+
fn is_valid(&self) -> bool {
86+
if let Some(v) = self { v.is_valid() } else { matches!(*self, None) }
87+
}
88+
}
89+
90+
unsafe impl<T, E> Invariant for Result<T, E>
91+
where
92+
T: Invariant,
93+
E: Invariant,
94+
{
95+
#[inline(always)]
96+
fn is_valid(&self) -> bool {
97+
if let Ok(v) = self {
98+
v.is_valid()
99+
} else if let Err(e) = self {
100+
e.is_valid()
101+
} else {
102+
false
103+
}
104+
}
105+
}
106+
107+
macro_rules! nonzero_invariant {
108+
( $type: ty ) => {
109+
unsafe impl Invariant for $type {
110+
#[inline(always)]
111+
fn is_valid(&self) -> bool {
112+
self.get() != 0
113+
}
114+
}
115+
};
116+
}
117+
118+
nonzero_invariant!(NonZeroU8);
119+
nonzero_invariant!(NonZeroU16);
120+
nonzero_invariant!(NonZeroU32);
121+
nonzero_invariant!(NonZeroU64);
122+
nonzero_invariant!(NonZeroU128);
123+
nonzero_invariant!(NonZeroUsize);
124+
125+
nonzero_invariant!(NonZeroI8);
126+
nonzero_invariant!(NonZeroI16);
127+
nonzero_invariant!(NonZeroI32);
128+
nonzero_invariant!(NonZeroI64);
129+
nonzero_invariant!(NonZeroI128);
130+
nonzero_invariant!(NonZeroIsize);

‎library/rmc/src/lib.rs

+52-8
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,13 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
#![feature(rustc_attrs)] // Used for rustc_diagnostic_item.
44

5+
pub mod arbitrary;
6+
pub mod invariant;
57
pub mod slice;
68

9+
pub use arbitrary::Arbitrary;
10+
pub use invariant::Invariant;
11+
712
/// Creates an assumption that will be valid after this statement run. Note that the assumption
813
/// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the
914
/// program will exit successfully.
@@ -13,7 +18,7 @@ pub mod slice;
1318
/// The code snippet below should never panic.
1419
///
1520
/// ```rust
16-
/// let i : i32 = rmc::nondet();
21+
/// let i : i32 = rmc::any();
1722
/// rmc::assume(i > 10);
1823
/// if i < 0 {
1924
/// panic!("This will never panic");
@@ -23,30 +28,69 @@ pub mod slice;
2328
/// The following code may panic though:
2429
///
2530
/// ```rust
26-
/// let i : i32 = rmc::nondet();
31+
/// let i : i32 = rmc::any();
2732
/// assert!(i < 0, "This may panic and verification should fail.");
2833
/// rmc::assume(i > 10);
2934
/// ```
3035
#[inline(never)]
3136
#[rustc_diagnostic_item = "RmcAssume"]
3237
pub fn assume(_cond: bool) {}
3338

34-
/// This creates an unconstrained value of type `T`. You can assign the return value of this
39+
/// This creates an symbolic *valid* value of type `T`. You can assign the return value of this
3540
/// function to a variable that you want to make symbolic.
3641
///
3742
/// # Example:
3843
///
3944
/// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
40-
/// under all possible i32 input values.
45+
/// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero.
4146
///
4247
/// ```rust
43-
/// let inputA = rmc::nondet::<i32>();
48+
/// let inputA = rmc::any::<std::num::NonZeroU8>();
4449
/// fn_under_verification(inputA);
4550
/// ```
51+
///
52+
/// Note: This is a safe construct and can only be used with types that implement the `Arbitrary`
53+
/// trait. The Arbitrary trait is used to build a symbolic value that represents all possible
54+
/// valid values for type `T`.
55+
#[inline(always)]
56+
pub fn any<T: Arbitrary>() -> T {
57+
T::any()
58+
}
59+
60+
/// This function creates an unconstrained value of type `T`. This may result in an invalid value.
61+
///
62+
/// # Example:
63+
///
64+
/// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
65+
/// under all possible values of char, including invalid ones that are greater than char::MAX.
66+
///
67+
/// ```rust
68+
/// let inputA = unsafe { rmc::any_raw::<char>() };
69+
/// fn_under_verification(inputA);
70+
/// ```
71+
///
72+
/// # Safety
73+
///
74+
/// This function is unsafe and it may represent invalid `T` values which can lead to many
75+
/// undesirable undefined behaviors. Users must validate that the symbolic variable respects
76+
/// the type invariant as well as any other constraint relevant to their usage. E.g.:
77+
///
78+
/// ```rust
79+
/// let c = unsafe { rmc::any_raw::char() };
80+
/// rmc::assume(char::from_u32(c as u32).is_ok());
81+
/// ```
82+
///
83+
#[rustc_diagnostic_item = "RmcAnyRaw"]
84+
#[inline(never)]
85+
pub unsafe fn any_raw<T>() -> T {
86+
unimplemented!("RMC any_raw")
87+
}
88+
89+
/// This function has been split into a safe and unsafe functions: `rmc::any` and `rmc::any_raw`.
90+
#[deprecated]
4691
#[inline(never)]
47-
#[rustc_diagnostic_item = "RmcNonDet"]
48-
pub fn nondet<T>() -> T {
49-
unimplemented!("RMC nondet")
92+
pub fn nondet<T: Arbitrary>() -> T {
93+
any::<T>()
5094
}
5195

5296
/// Function used in tests for cases where the condition is not always true.

‎library/rmc/src/slice.rs

+14-14
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
use crate::{assume, nondet};
3+
use crate::{any, any_raw, assume};
44
use core::ops::{Deref, DerefMut};
55

66
/// Given an array `arr` of length `LENGTH`, this function returns a **valid**
@@ -12,23 +12,23 @@ use core::ops::{Deref, DerefMut};
1212
///
1313
/// ```rust
1414
/// let arr = [1, 2, 3];
15-
/// let slice = rmc::slice::nondet_slice_of_array(&arr);
15+
/// let slice = rmc::slice::any_slice_of_array(&arr);
1616
/// foo(slice); // where foo is a function that takes a slice and verifies a property about it
1717
/// ```
18-
pub fn nondet_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
19-
let (from, to) = nondet_range::<LENGTH>();
18+
pub fn any_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
19+
let (from, to) = any_range::<LENGTH>();
2020
&arr[from..to]
2121
}
2222

2323
/// A mutable version of the previous function
24-
pub fn nondet_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) -> &mut [T] {
25-
let (from, to) = nondet_range::<LENGTH>();
24+
pub fn any_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) -> &mut [T] {
25+
let (from, to) = any_range::<LENGTH>();
2626
&mut arr[from..to]
2727
}
2828

29-
fn nondet_range<const LENGTH: usize>() -> (usize, usize) {
30-
let from: usize = nondet();
31-
let to: usize = nondet();
29+
fn any_range<const LENGTH: usize>() -> (usize, usize) {
30+
let from: usize = any();
31+
let to: usize = any();
3232
assume(to <= LENGTH);
3333
assume(from <= to);
3434
(from, to)
@@ -38,12 +38,12 @@ fn nondet_range<const LENGTH: usize>() -> (usize, usize) {
3838
/// between `0..=MAX_SLICE_LENGTH` and with non-deterministic content. This is
3939
/// useful in situations where one wants to verify that all slices with any
4040
/// content and with a length up to `MAX_SLICE_LENGTH` satisfy a certain
41-
/// property. Use `nondet_slice` to create an instance of this struct.
41+
/// property. Use `any_slice` to create an instance of this struct.
4242
///
4343
/// # Example:
4444
///
4545
/// ```rust
46-
/// let slice: rmc::slice::NonDetSlice<u8, 5> = rmc::slice::nondet_slice();
46+
/// let slice: rmc::slice::NonDetSlice<u8, 5> = rmc::slice::any_slice();
4747
/// foo(&slice); // where foo is a function that takes a slice and verifies a property about it
4848
/// ```
4949
pub struct NonDetSlice<T, const MAX_SLICE_LENGTH: usize> {
@@ -53,8 +53,8 @@ pub struct NonDetSlice<T, const MAX_SLICE_LENGTH: usize> {
5353

5454
impl<T, const MAX_SLICE_LENGTH: usize> NonDetSlice<T, MAX_SLICE_LENGTH> {
5555
fn new() -> Self {
56-
let arr: [T; MAX_SLICE_LENGTH] = nondet();
57-
let slice_len: usize = nondet();
56+
let arr: [T; MAX_SLICE_LENGTH] = unsafe { any_raw() };
57+
let slice_len: usize = any();
5858
assume(slice_len <= MAX_SLICE_LENGTH);
5959
Self { arr, slice_len }
6060
}
@@ -82,6 +82,6 @@ impl<T, const MAX_SLICE_LENGTH: usize> DerefMut for NonDetSlice<T, MAX_SLICE_LEN
8282
}
8383
}
8484

85-
pub fn nondet_slice<T, const MAX_SLICE_LENGTH: usize>() -> NonDetSlice<T, MAX_SLICE_LENGTH> {
85+
pub fn any_slice<T, const MAX_SLICE_LENGTH: usize>() -> NonDetSlice<T, MAX_SLICE_LENGTH> {
8686
NonDetSlice::<T, MAX_SLICE_LENGTH>::new()
8787
}

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ The second command opens that report in your default browser (on mac, on linux d
7171
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):
7272

7373
```
74-
let x: u32 = rmc::nondet();
74+
let x: u32 = rmc::any();
7575
x = 1023u
7676
```
7777

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

+6-6
Original file line numberDiff line numberDiff line change
@@ -101,26 +101,26 @@ Having run `rmc --visualize` and clicked on one of the failures to see a trace,
101101

102102
To navigate this trace to find the information you need, we recommend searching for things you expect to be somewhere in the trace:
103103

104-
1. Search the document for `rmc::nondet` or `variable_of_interest =` such as `size =`.
104+
1. Search the document for `rmc::any` or `variable_of_interest =` such as `size =`.
105105
We can use this to find out what example values lead to a problem.
106-
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.
106+
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.
107107
In this trace we find (and the values you get may be different):
108108

109109
```
110110
Step 23: Function main, File tests/bounds-check.rs, Line 43
111-
let size: usize = rmc::nondet();
111+
let size: usize = rmc::any();
112112
size = 0ul
113113
114114
Step 27: Function main, File tests/bounds-check.rs, Line 45
115-
let index: usize = rmc::nondet();
115+
let index: usize = rmc::any();
116116
index = 0ul
117117
118118
Step 36: Function main, File tests/bounds-check.rs, Line 43
119-
let size: usize = rmc::nondet();
119+
let size: usize = rmc::any();
120120
size = 2464ul
121121
122122
Step 39: Function main, File tests/bounds-check.rs, Line 45
123-
let index: usize = rmc::nondet();
123+
let index: usize = rmc::any();
124124
index = 2463ul
125125
```
126126

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,9 @@ mod tests {
3434
#[cfg(rmc)]
3535
#[no_mangle]
3636
fn main() {
37-
let size: usize = rmc::nondet();
37+
let size: usize = rmc::any();
3838
rmc::assume(size < 4096);
39-
let index: usize = rmc::nondet();
39+
let index: usize = rmc::any();
4040
let array: Vec<u32> = vec![0; size];
4141
get_wrapped(index, &array);
4242
}

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ fn find_midpoint(low: u32, high: u32) -> u32 {
1212
#[cfg(rmc)]
1313
#[no_mangle]
1414
fn main() {
15-
let a: u32 = rmc::nondet();
16-
let b: u32 = rmc::nondet();
15+
let a: u32 = rmc::any();
16+
let b: u32 = rmc::any();
1717
find_midpoint(a, b);
1818
}
1919
// ANCHOR_END: rmc

0 commit comments

Comments
 (0)