diff --git a/library/rmc/src/arbitrary.rs b/library/rmc/src/arbitrary.rs new file mode 100644 index 000000000000..b98d6c8272c1 --- /dev/null +++ b/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 Arbitrary for T +where + T: Invariant, +{ + fn any() -> Self { + let value = unsafe { any_raw::() }; + assume(value.is_valid()); + value + } +} diff --git a/library/rmc/src/invariant.rs b/library/rmc/src/invariant.rs new file mode 100644 index 000000000000..0437c8ee19bc --- /dev/null +++ b/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 Invariant for [T; N] { + fn is_valid(&self) -> bool { + self.iter().all(|e| e.is_valid()) + } +} + +unsafe impl Invariant for Option +where + T: Invariant, +{ + #[inline(always)] + fn is_valid(&self) -> bool { + if let Some(v) = self { v.is_valid() } else { matches!(*self, None) } + } +} + +unsafe impl Invariant for Result +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); diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs index 4c7acf68f766..3a91fc7e3f55 100644 --- a/library/rmc/src/lib.rs +++ b/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,7 +28,7 @@ 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); /// ``` @@ -31,22 +36,61 @@ pub mod slice; #[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::(); +/// let inputA = rmc::any::(); /// 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 { + 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::() }; +/// 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 { + 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 { - unimplemented!("RMC nondet") +pub fn nondet() -> T { + any::() } /// Function used in tests for cases where the condition is not always true. diff --git a/library/rmc/src/slice.rs b/library/rmc/src/slice.rs index bd7aa1aecfc3..c6141cab278d 100644 --- a/library/rmc/src/slice.rs +++ b/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(arr: &[T; LENGTH]) -> &[T] { - let (from, to) = nondet_range::(); +pub fn any_slice_of_array(arr: &[T; LENGTH]) -> &[T] { + let (from, to) = any_range::(); &arr[from..to] } /// A mutable version of the previous function -pub fn nondet_slice_of_array_mut(arr: &mut [T; LENGTH]) -> &mut [T] { - let (from, to) = nondet_range::(); +pub fn any_slice_of_array_mut(arr: &mut [T; LENGTH]) -> &mut [T] { + let (from, to) = any_range::(); &mut arr[from..to] } -fn nondet_range() -> (usize, usize) { - let from: usize = nondet(); - let to: usize = nondet(); +fn any_range() -> (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() -> (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 = rmc::slice::nondet_slice(); +/// let slice: rmc::slice::NonDetSlice = rmc::slice::any_slice(); /// foo(&slice); // where foo is a function that takes a slice and verifies a property about it /// ``` pub struct NonDetSlice { @@ -53,8 +53,8 @@ pub struct NonDetSlice { impl NonDetSlice { 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 DerefMut for NonDetSlice() -> NonDetSlice { +pub fn any_slice() -> NonDetSlice { NonDetSlice::::new() } diff --git a/rmc-docs/src/tutorial-first-steps.md b/rmc-docs/src/tutorial-first-steps.md index 567b33e78580..8244d6d5ee0f 100644 --- a/rmc-docs/src/tutorial-first-steps.md +++ b/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 ``` diff --git a/rmc-docs/src/tutorial-kinds-of-failure.md b/rmc-docs/src/tutorial-kinds-of-failure.md index 6215469ff7d7..805e0b0350dd 100644 --- a/rmc-docs/src/tutorial-kinds-of-failure.md +++ b/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 ``` diff --git a/rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs b/rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs index 9ec80f040fa4..942b1fc2af98 100644 --- a/rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs +++ b/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 = vec![0; size]; get_wrapped(index, &array); } diff --git a/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs b/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs index 2542810a788b..55d596dd6de2 100644 --- a/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs +++ b/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 diff --git a/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs b/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs index ae754004d16a..99ceab01e848 100644 --- a/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs +++ b/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs @@ -27,8 +27,8 @@ mod tests { #[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(); simple_addition(a, b); } // ANCHOR_END: rmc diff --git a/rmc-docs/src/tutorial/loops-unwinding/src/lib.rs b/rmc-docs/src/tutorial/loops-unwinding/src/lib.rs index cc1d210bf860..49bfa094ec92 100644 --- a/rmc-docs/src/tutorial/loops-unwinding/src/lib.rs +++ b/rmc-docs/src/tutorial/loops-unwinding/src/lib.rs @@ -23,7 +23,7 @@ fn main() { const LIMIT: usize = 10; let mut buffer: [u8; LIMIT] = [1; LIMIT]; - let length = rmc::nondet(); + let length = rmc::any(); rmc::assume(length <= LIMIT); initialize_prefix(length, &mut buffer); diff --git a/rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs b/rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs index 4894b8c423cb..a11351b80c2c 100644 --- a/rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs +++ b/rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs @@ -51,7 +51,7 @@ mod tests { #[cfg(rmc)] #[no_mangle] fn main() { - let x: u32 = rmc::nondet(); + let x: u32 = rmc::any(); estimate_size(x); } // ANCHOR_END: rmc diff --git a/rmc-docs/src/tutorial/rmc-first-steps/tests/final-form.rs b/rmc-docs/src/tutorial/rmc-first-steps/tests/final-form.rs index 89bba37c6f53..a28fece655e1 100644 --- a/rmc-docs/src/tutorial/rmc-first-steps/tests/final-form.rs +++ b/rmc-docs/src/tutorial/rmc-first-steps/tests/final-form.rs @@ -52,7 +52,7 @@ mod tests { #[cfg(rmc)] #[no_mangle] fn main() { - let x: u32 = rmc::nondet(); + let x: u32 = rmc::any(); rmc::assume(x < 4096); let y = estimate_size(x); assert!(y < 10); @@ -62,6 +62,6 @@ fn main() { #[cfg(rmc)] #[no_mangle] fn failing_main() { - let x: u32 = rmc::nondet(); + let x: u32 = rmc::any(); let y = estimate_size(x); } diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/assumptions.rs b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/assumptions.rs deleted file mode 100644 index 6383160d0ca3..000000000000 --- a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/assumptions.rs +++ /dev/null @@ -1,594 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! this module defines functions which impose data invariant on generated data types. - -use crate::GotocCtx; -use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; -use cbmc::NO_PRETTY_NAME; -use rustc_middle::mir::interpret::{ConstValue, Scalar}; -use rustc_middle::ty; -use rustc_middle::ty::layout::LayoutOf; -use rustc_middle::ty::Ty; -use rustc_middle::ty::{IntTy, UintTy}; -use rustc_target::abi::{FieldsShape, Primitive, Size, TagEncoding, Variants}; - -fn fold_invariants_gen Expr>(mut iv: Vec, dfl: Expr, comb: F) -> Expr { - let mut res: Option = None; - while !iv.is_empty() { - let e = iv.remove(0); - if let Some(r) = res { - res = Some(comb(r, e)); - } else { - res = Some(e); - } - } - res.unwrap_or(dfl) -} - -fn fold_invariants(iv: Vec) -> Expr { - fold_invariants_gen(iv, Expr::bool_true(), |a, b| a.and(b)) -} - -fn fold_invariants_or(iv: Vec) -> Expr { - fold_invariants_gen(iv, Expr::bool_false(), |a, b| a.or(b)) -} - -impl<'tcx> GotocCtx<'tcx> { - fn invariant_name(&mut self, t: Ty<'tcx>) -> String { - let ty_name = self.ty_mangled_name(t); - let fname = format!("{}:invariant", ty_name); - fname - } - - fn bound_ty_above_and_below( - &mut self, - fname: String, - t: Ty<'tcx>, - below: i32, - above: i32, - ) -> Option { - self.ensure(&fname, |ctx, _| { - ctx.codegen_assumption_genfunc(&fname, t, |_tcx, ptr, body| { - let exp = ptr - .clone() - .dereference() - .ge(Expr::int_constant(below, Type::signed_int(32))) - .and(ptr.dereference().le(Expr::int_constant(above, Type::signed_int(32)))) - .ret(Location::none()); - body.push(exp) - }) - }); - self.find_function(&fname) - } - - fn bound_true_false(&mut self, fname: String, t: Ty<'tcx>) -> Option { - self.ensure(&fname, |ctx, _| { - ctx.codegen_assumption_genfunc(&fname, t, |_tcx, ptr, body| { - let exp = ptr - .clone() - .dereference() - .eq(Expr::c_true()) - .or(ptr.dereference().eq(Expr::c_false())) - .ret(Location::none()); - body.push(exp) - }) - }); - self.find_function(&fname) - } - /// return an option of an expression representing a function assuming the data invariant of the type t - /// - /// for a type t, this function generates - /// bool t:invariant(t *x); - pub fn codegen_assumption(&mut self, t: Ty<'tcx>) -> Option { - let fname = self.invariant_name(t); - match t.kind() { - ty::Bool => self.bound_true_false(fname, t), - ty::Int(_) | ty::Uint(_) | ty::Float(_) => None, - ty::Char => { - //Char is an i32, but has invalid values. This means that rust can do a niche optimization for - // Option. Make sure we never generate a value above char::MAX https://doc.rust-lang.org/beta/std/char/constant.MAX.html - self.bound_ty_above_and_below(fname, t, 0, '\u{10ffff}' as i32) - } - ty::Adt(def, subst) => { - if def.is_union() { - None - } - // - else if def.is_struct() { - let variant = &def.variants.raw[0]; - self.ensure(&fname, |ctx, _| { - ctx.codegen_assumption_struct(&fname, t, variant, subst) - }); - self.find_function(&fname) - } else { - // is enum - if def.variants.is_empty() { - None - } else { - self.ensure(&fname, |ctx, _| { - ctx.codegen_assumption_enum(&fname, t, def, subst) - }); - self.find_function(&fname) - } - } - } - ty::Foreign(_) => unreachable!("cannot generate assumptions for foreign types"), - ty::Array(et, c) => { - self.ensure(&fname, |ctx, _| ctx.codegen_assumption_array(&fname, t, et, c)); - self.find_function(&fname) - } - ty::Str | ty::Slice(_) => unreachable!("should be handled by Ref or RawPtr"), - ty::RawPtr(rt) => self.codegen_assumption_ref_ptr(&fname, t, rt.ty, false), - ty::Ref(_, rt, _) => self.codegen_assumption_ref_ptr(&fname, t, rt, true), - ty::FnDef(_, _) | ty::FnPtr(_) => None, - ty::Dynamic(_, _) => unreachable!(), - ty::Closure(_, _) => None, - ty::Generator(_, _, _) => unimplemented!(), - ty::GeneratorWitness(_) => unimplemented!(), - ty::Never => None, - ty::Tuple(ts) => { - if ts.is_empty() { - None - } else { - self.ensure(&fname, |ctx, _| ctx.codegen_assumption_tuple(&fname, t, ts)); - self.find_function(&fname) - } - } - ty::Projection(_) | ty::Opaque(_, _) => { - let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), t); - self.codegen_assumption(normalized) - } - ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"), - ty::Placeholder(_) | ty::Infer(_) | ty::Error(_) => { - unreachable!("remnants of type checking") - } - } - } - - /// * fname - function name - /// * t - type of a reference - /// * rt - type of the referenced term - /// * is_ref - whether we are handling references or pointers - fn codegen_assumption_ref_ptr( - &mut self, - fname: &str, - t: Ty<'tcx>, - rt: Ty<'tcx>, - is_ref: bool, - ) -> Option { - match rt.kind() { - ty::Slice(e) => { - let ef = self.codegen_assumption(e); - if ef.is_none() && !is_ref { - None - } else { - self.ensure(&fname, |ctx, _| { - ctx.codegen_assumption_ref_ptr_slice(fname, t, ef, is_ref) - }); - self.find_function(fname) - } - } - ty::Str => { - if !is_ref { - None - } else { - self.ensure(&fname, |ctx, _| { - ctx.codegen_assumption_ref_ptr_slice(fname, t, None, is_ref) - }); - self.find_function(fname) - } - } - ty::Dynamic(_, _) => None, - ty::Projection(_) | ty::Opaque(_, _) => { - let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), t); - self.codegen_assumption_ref_ptr(fname, t, normalized, is_ref) - } - _ => { - let ef = self.codegen_assumption(rt); - if ef.is_none() && !is_ref { - None - } else { - self.ensure(&fname, |ctx, _| { - ctx.codegen_assumption_ref_ptr_thin(fname, t, ef, is_ref) - }); - self.find_function(fname) - } - } - } - } - - /// * fname - function name - /// * t - type of a reference to a slice - /// * e - type of an element in the slice - /// * f - invariant function for each element - /// * is_ref - whether we are handling references or pointers - fn codegen_assumption_ref_ptr_slice( - &mut self, - fname: &str, - t: Ty<'tcx>, - f: Option, - is_ref: bool, - ) -> Symbol { - self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| { - let sl = ptr.dereference(); - let data = sl.clone().member("data", &tcx.symbol_table); - let len = sl.member("len", &tcx.symbol_table); - let mut invariants = vec![]; - if is_ref { - invariants.push(data.clone().is_nonnull()); - } - if let Some(f) = f { - //CHECKME: why is this 2? - let idx = tcx.gen_function_local_variable(2, &fname, Type::size_t()).to_expr(); - body.push(Stmt::decl(idx.clone(), Some(Type::size_t().zero()), Location::none())); - let lbody = Stmt::block( - vec![ - data.clone() - .is_nonnull() - .implies(f.call(vec![data.plus(idx.clone())])) - .not() - .if_then_else( - Expr::bool_false().ret(Location::none()), - None, - Location::none(), - ), - ], - Location::none(), - ); - body.push(Stmt::for_loop( - Stmt::skip(Location::none()), - idx.clone().lt(len), - idx.postincr().as_stmt(Location::none()), - lbody, - Location::none(), - )); - } - body.push(fold_invariants(invariants).ret(Location::none())); - }) - } - - /// * fname - function name - /// * t - type of the reference - /// * f - invariant function for the referenced element - /// * is_ref - whether we are handling references or pointers - fn codegen_assumption_ref_ptr_thin( - &mut self, - fname: &str, - t: Ty<'tcx>, - f: Option, - is_ref: bool, - ) -> Symbol { - self.codegen_assumption_genfunc(fname, t, |_, ptr, body| { - let x = ptr.dereference(); - let mut invarints = vec![]; - if is_ref { - invarints.push(x.clone().is_nonnull()); - } - if let Some(f) = f { - invarints.push(x.clone().is_nonnull().implies(f.call(vec![x]))); - } - body.push(fold_invariants(invarints).ret(Location::none())); - }) - } - - fn codegen_assumption_struct_invariant( - &mut self, - ptr: Expr, - variant: &ty::VariantDef, - subst: ty::subst::SubstsRef<'tcx>, - ) -> Vec { - let mut invariants = vec![]; - for fd in &variant.fields { - let t = fd.ty(self.tcx, subst); - if let Some(f) = self.codegen_assumption(t) { - let fp = ptr - .clone() - .dereference() - .member(&fd.ident.name.to_string(), &self.symbol_table) - .address_of(); - let assumption = f.call(vec![fp]); - invariants.push(assumption); - } - } - invariants - } - - /// collect invariant for each field - fn codegen_assumption_struct( - &mut self, - fname: &str, - t: Ty<'tcx>, - variant: &'tcx ty::VariantDef, - subst: ty::subst::SubstsRef<'tcx>, - ) -> Symbol { - self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| { - let invariants = tcx.codegen_assumption_struct_invariant(ptr, variant, subst); - body.push(fold_invariants(invariants).ret(Location::none())); - }) - } - - fn codegen_assumption_enum( - &mut self, - fname: &str, - t: Ty<'tcx>, - def: &'tcx ty::AdtDef, - subst: ty::subst::SubstsRef<'tcx>, - ) -> Symbol { - match def.variants.len() { - 0 => unreachable!(), - 1 => self.codegen_assumption_enum_single_variant(fname, t, &def.variants.raw[0], subst), - _ => { - let layout = self.layout_of(t); - match &layout.variants { - Variants::Single { .. } => unreachable!(), - Variants::Multiple { tag_encoding, .. } => match tag_encoding { - TagEncoding::Direct => { - self.codegen_assumption_enum_direct(fname, t, def, subst) - } - TagEncoding::Niche { .. } => { - self.codegen_assumption_enum_niche(fname, t, def, subst) - } - }, - } - } - } - } - - fn codegen_assumption_enum_single_variant( - &mut self, - fname: &str, - t: Ty<'tcx>, - variant: &ty::VariantDef, - subst: ty::subst::SubstsRef<'tcx>, - ) -> Symbol { - self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| { - let invariants = tcx.codegen_assumption_struct_invariant(ptr, variant, subst); - body.push(fold_invariants(invariants).ret(Location::none())); - }) - } - - fn codegen_assumption_enum_niche( - &mut self, - fname: &str, - t: Ty<'tcx>, - def: &'tcx ty::AdtDef, - subst: ty::subst::SubstsRef<'tcx>, - ) -> Symbol { - let layout = self.layout_of(t); - let (tag, dataful_variant, niche_variants, niche_start) = match &layout.variants { - Variants::Single { .. } => unreachable!(), - Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { - TagEncoding::Direct => unreachable!(), - TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { - (tag, dataful_variant, niche_variants, niche_start) - } - }, - }; - let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => offsets[0].bytes_usize(), - _ => unreachable!("niche encoding must have arbitrary fields"), - }; - let discr_ty = self.codegen_enum_discr_typ(t); - let discr_ty = self.codegen_ty(discr_ty); - let variant = &def.variants[*dataful_variant]; - self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| { - let discr = tcx.codegen_get_niche(ptr.clone().dereference(), offset, discr_ty.clone()); - let mut invariants = vec![]; - for (idx, _) in def.variants.iter_enumerated() { - if idx != *dataful_variant { - let niche_value = idx.as_u32() - niche_variants.start().as_u32(); - let niche_value = (niche_value as u128).wrapping_add(*niche_start); - let value = if niche_value == 0 && tag.value == Primitive::Pointer { - discr_ty.null() - } else { - Expr::int_constant(niche_value, discr_ty.clone()) - }; - invariants.push(discr.clone().eq(value)); - } - } - - let data_invar = tcx.codegen_assumption_struct_invariant(ptr, variant, subst); - invariants.push(fold_invariants(data_invar)); - body.push(fold_invariants_or(invariants).ret(Location::none())); - }) - } - - /// see comments in the body - fn codegen_assumption_enum_direct( - &mut self, - fname: &str, - t: Ty<'tcx>, - def: &'tcx ty::AdtDef, - subst: ty::subst::SubstsRef<'tcx>, - ) -> Symbol { - self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| { - // here we have enum - // - // we have a few invariants to assume. - // 1. the discriminant is within [0, def.variants.len()) - let discr_t = tcx.codegen_enum_discr_typ(t); - let isz = tcx.codegen_ty(discr_t); - let case = ptr.clone().dereference().member("case", &tcx.symbol_table); - let mut invariants = vec![]; - if def - .variants - .iter_enumerated() - .all(|(i, v)| v.discr == ty::VariantDiscr::Relative(i.as_u32())) - { - // ptr.case >= 0 - invariants.push(case.clone().ge(isz.zero())); - // ptr.case < def.variants.len() - invariants - .push(case.clone().lt(Expr::int_constant(def.variants.len(), isz.clone()))); - } else { - // if it's not the default case, we have to enumerate all possible values of - // discriminants. - let mut cases = vec![]; - let sz = match discr_t.kind() { - ty::Int(k) => match k { - IntTy::Isize => unreachable!(), - IntTy::I8 => 1, - IntTy::I16 => 2, - IntTy::I32 => 4, - IntTy::I64 => 8, - IntTy::I128 => 16, - }, - ty::Uint(k) => match k { - UintTy::Usize => unreachable!(), - UintTy::U8 => 1, - UintTy::U16 => 2, - UintTy::U32 => 4, - UintTy::U64 => 8, - UintTy::U128 => 16, - }, - _ => unreachable!(), - }; - for (_, discr) in def.discriminants(tcx.tcx) { - let val = (discr.val << (128 - 8 * sz)) >> (128 - 8 * sz); - let scalar = Scalar::from_uint(val, Size::from_bytes(sz)); - cases.push(case.clone().eq(tcx.codegen_const_value( - ConstValue::Scalar(scalar), - discr_t, - None, - ))); - } - invariants.push(fold_invariants_or(cases)); - } - - // 2. for each discriminant within the valid range, we check each field of each case - // e.g. - // enum Foo { - // C1(T1, T2), - // C2(T3, T4), - // } - // - // we assume - // ptr.case == 0 ==> T1:invariant(..) && T2:invariant(..) - // and - // ptr.case == 1 ==> T3:invariant(..) && T4:invariant(..) - for (i, variant) in def.variants.iter_enumerated() { - let idx = i.index(); - let variant_name = variant.ident.name.to_string(); - let var_struct = ptr - .clone() - .dereference() - .member("cases", &tcx.symbol_table) - .member(&variant_name, &tcx.symbol_table); - let mut case_invariants = vec![]; - for f in &variant.fields { - let ft = f.ty(tcx.tcx, subst); - if let Some(fi) = tcx.codegen_assumption(ft) { - let fname = f.ident.name.to_string(); - case_invariants.push(fi.call(vec![ - var_struct.clone().member(&fname, &tcx.symbol_table).address_of(), - ])); - } - } - - if !case_invariants.is_empty() { - invariants.push( - case.clone() - .eq(Expr::int_constant(idx, isz.clone())) - .implies(fold_invariants(case_invariants)), - ); - } - } - - body.push(fold_invariants(invariants).ret(Location::none())); - }) - } - - /// generates: - /// - /// bool t:invariant(t* ptr) { - /// for (int i; i < len; i++) { - /// if (!et:invariant(&ptr.0[i])) return false; - /// } - /// return true; - /// } - fn codegen_assumption_array( - &mut self, - fname: &str, - t: Ty<'tcx>, - et: Ty<'tcx>, - c: &'tcx ty::Const<'tcx>, - ) -> Symbol { - self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| { - if let Some(f) = tcx.codegen_assumption(et) { - let idx = tcx.gen_function_local_variable(2, &fname, Type::size_t()); - body.push(Stmt::decl(idx.to_expr(), Some(Type::size_t().zero()), Location::none())); - let idxe = idx.to_expr(); - let lbody = Stmt::block( - vec![ - f.call(vec![ - tcx.codegen_idx_array(ptr.clone().dereference(), idxe.clone()) - .address_of(), - ]) - .not() - .if_then_else( - Expr::bool_false().ret(Location::none()), - None, - Location::none(), - ), - ], - Location::none(), - ); - body.push(Stmt::for_loop( - Stmt::skip(Location::none()), - idxe.clone().lt(tcx.codegen_const(c, None)), - idxe.postincr().as_stmt(Location::none()), - lbody, - Location::none(), - )); - body.push(Expr::bool_true().ret(Location::none())); - } - }) - } - - /// the same as struct actually - fn codegen_assumption_tuple( - &mut self, - fname: &str, - t: Ty<'tcx>, - ts: ty::subst::SubstsRef<'tcx>, - ) -> Symbol { - self.codegen_assumption_genfunc(fname, t, |tcx, ptr, body| { - let mut invariants = vec![]; - for (i, t) in ts.iter().enumerate() { - let t = t.expect_ty(); - if let Some(f) = tcx.codegen_assumption(t) { - let field = ptr - .clone() - .dereference() - .member(&Self::tuple_fld_name(i), &tcx.symbol_table) // x->i - .address_of(); // &(x->i) - invariants.push(f.call(vec![field])); - } - } - body.push(fold_invariants(invariants).ret(Location::none())); - }) - } - - fn codegen_assumption_genfunc, Expr, &mut Vec) -> ()>( - &mut self, - fname: &str, - t: Ty<'tcx>, - f: F, - ) -> Symbol { - //TODO this is created all out of order! - let paramt = self.codegen_ty(t).to_pointer(); - let var = self.gen_function_local_variable(1, &fname, paramt); - let ptr = var.clone().to_expr(); - let mut stmts = vec![]; - //let mut body = Stmt::block(vec![]); - f(self, ptr, &mut stmts); - let body = Stmt::block(stmts, Location::none()); - Symbol::function( - fname, - Type::code(vec![var.to_function_parameter()], Type::bool()), - Some(body), - NO_PRETTY_NAME, - Location::none(), - ) - } -} diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/mod.rs b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/mod.rs index 643bb9de3cb0..c2106961df5a 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/mod.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/mod.rs @@ -4,7 +4,6 @@ //! This module does that actual translation of MIR constructs to goto constructs. //! Each subfile is named for the MIR construct it translates. -mod assumptions; mod block; mod function; mod intrinsic; diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs b/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs index 2b08c842ffeb..56fb79a8f3f1 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/overrides/hooks.rs @@ -153,10 +153,10 @@ impl<'tcx> GotocHook<'tcx> for Nondet { // Deprecate old __nondet since it doesn't match rust naming conventions. // Complete removal is tracked here: https://github.com/model-checking/rmc/issues/599 if instance_name_starts_with(tcx, instance, "__nondet") { - warn!("The function __nondet is deprecated. Use rmc::nondet instead"); + warn!("The function __nondet is deprecated. Use rmc::any instead"); return true; } - matches_function(tcx, instance, "RmcNonDet") + matches_function(tcx, instance, "RmcAnyRaw") } fn handle( @@ -180,11 +180,6 @@ impl<'tcx> GotocHook<'tcx> for Nondet { Stmt::block( vec![ pe.clone().assign(tcx.codegen_ty(pt).nondet(), loc.clone()), - // we should potentially generate an assumption - match tcx.codegen_assumption(pt) { - None => Stmt::skip(loc.clone()), - Some(f) => Stmt::assume(f.call(vec![pe.address_of()]), loc.clone()), - }, Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()), ], loc, diff --git a/src/test/benchmarks/Vector/append.rs b/src/test/benchmarks/Vector/append.rs index 8d6b70d4c4e3..8d9ea0e654a8 100644 --- a/src/test/benchmarks/Vector/append.rs +++ b/src/test/benchmarks/Vector/append.rs @@ -9,11 +9,11 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } let mut v2: Vec = Vec::with_capacity(times); for i in 0..times { - v2.push(rmc::nondet()); + v2.push(rmc::any()); } v.append(&mut v2); assert!(v.len() == times * 2); diff --git a/src/test/benchmarks/Vector/insert.rs b/src/test/benchmarks/Vector/insert.rs index f25a49a3c474..f8630594471e 100644 --- a/src/test/benchmarks/Vector/insert.rs +++ b/src/test/benchmarks/Vector/insert.rs @@ -9,11 +9,11 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } - let sentinel = rmc::nondet(); + let sentinel = rmc::any(); v.push(sentinel); - v.insert(v.len()/2, rmc::nondet()); + v.insert(v.len()/2, rmc::any()); assert!(v.pop() == Some(sentinel)); } diff --git a/src/test/benchmarks/Vector/push.rs b/src/test/benchmarks/Vector/push.rs index 880914b4b8b8..683a58d22b61 100644 --- a/src/test/benchmarks/Vector/push.rs +++ b/src/test/benchmarks/Vector/push.rs @@ -9,7 +9,7 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } } diff --git a/src/test/benchmarks/Vector/push_and_pop.rs b/src/test/benchmarks/Vector/push_and_pop.rs index 5a5a941facff..b11ffb4b3682 100644 --- a/src/test/benchmarks/Vector/push_and_pop.rs +++ b/src/test/benchmarks/Vector/push_and_pop.rs @@ -9,7 +9,7 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::new(); for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } assert!(v.len() == times); v.push(1); @@ -19,7 +19,7 @@ fn operate_on_vec(times: usize) { fn operate_on_vec_len(times: usize) { let mut v: Vec = Vec::new(); for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } assert!(v.len() == times); v.push(1); diff --git a/src/test/benchmarks/Vector/remove.rs b/src/test/benchmarks/Vector/remove.rs index 0f41df354534..aedb3068252a 100644 --- a/src/test/benchmarks/Vector/remove.rs +++ b/src/test/benchmarks/Vector/remove.rs @@ -9,9 +9,9 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } - let sentinel = rmc::nondet(); + let sentinel = rmc::any(); v.push(sentinel); // We remove elements to perform more memmoves. These are done to fill up // "holes" created due to elements removed from the middle of the Vec. diff --git a/src/test/benchmarks/Vector/shrink_and_clear.rs b/src/test/benchmarks/Vector/shrink_and_clear.rs index 3a492dcea4e7..6d559abf8180 100644 --- a/src/test/benchmarks/Vector/shrink_and_clear.rs +++ b/src/test/benchmarks/Vector/shrink_and_clear.rs @@ -9,11 +9,11 @@ fn operate_on_vec(times: usize) { // Create vector with known capacity let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } assert!(v.len() == times); // Here, Vecs with grow() internally - let i: usize = rmc::nondet(); + let i: usize = rmc::any(); rmc::assume(i >= 0 && i < v.len()); let saved = v[i]; // Completely shrink the array to remove additional allocations @@ -21,16 +21,16 @@ fn operate_on_vec(times: usize) { assert!(v[i] == saved); // Push some new elements to grow() again for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } // Drop all elements in the Vec v.clear(); // Add some more new elements for i in 0..times { - v.push(rmc::nondet()); + v.push(rmc::any()); } // Assert! - let sentinel = rmc::nondet(); + let sentinel = rmc::any(); v.push(sentinel); assert!(v.pop() == Some(sentinel)); } diff --git a/src/test/cargo-rmc/dependencies/src/lib.rs b/src/test/cargo-rmc/dependencies/src/lib.rs index fb672fe89428..534a08ae2153 100644 --- a/src/test/cargo-rmc/dependencies/src/lib.rs +++ b/src/test/cargo-rmc/dependencies/src/lib.rs @@ -3,7 +3,7 @@ #[no_mangle] pub fn check_dummy() { - let x = rmc::nondet::(); + let x = rmc::any::(); rmc::assume(x > 10); assert!(x > 2); } diff --git a/src/test/cargo-rmc/simple-config-toml/src/lib.rs b/src/test/cargo-rmc/simple-config-toml/src/lib.rs index ace3ddcd98a5..5a5a89e8f3f5 100644 --- a/src/test/cargo-rmc/simple-config-toml/src/lib.rs +++ b/src/test/cargo-rmc/simple-config-toml/src/lib.rs @@ -18,8 +18,8 @@ mod rmc_tests { #[allow(dead_code)] #[no_mangle] fn test_sum() { - let a: u64 = rmc::nondet(); - let b: u64 = rmc::nondet(); + let a: u64 = rmc::any(); + let b: u64 = rmc::any(); let p = Pair::new(a, b); assert!(p.sum() == a.wrapping_add(b)); } diff --git a/src/test/cargo-rmc/simple-extern/src/lib.rs b/src/test/cargo-rmc/simple-extern/src/lib.rs index 5448970f70cd..a04462b26c07 100644 --- a/src/test/cargo-rmc/simple-extern/src/lib.rs +++ b/src/test/cargo-rmc/simple-extern/src/lib.rs @@ -20,7 +20,7 @@ mod rmc_tests { #[allow(dead_code)] #[no_mangle] fn test_sum() { - let a: u32 = rmc::nondet(); + let a: u32 = rmc::any(); if a < 100 { unsafe { diff --git a/src/test/cargo-rmc/simple-lib/src/lib.rs b/src/test/cargo-rmc/simple-lib/src/lib.rs index ace3ddcd98a5..5a5a89e8f3f5 100644 --- a/src/test/cargo-rmc/simple-lib/src/lib.rs +++ b/src/test/cargo-rmc/simple-lib/src/lib.rs @@ -18,8 +18,8 @@ mod rmc_tests { #[allow(dead_code)] #[no_mangle] fn test_sum() { - let a: u64 = rmc::nondet(); - let b: u64 = rmc::nondet(); + let a: u64 = rmc::any(); + let b: u64 = rmc::any(); let p = Pair::new(a, b); assert!(p.sum() == a.wrapping_add(b)); } diff --git a/src/test/expected/closure/main.rs b/src/test/expected/closure/main.rs index 152b8b958e7b..87a755d99062 100644 --- a/src/test/expected/closure/main.rs +++ b/src/test/expected/closure/main.rs @@ -9,7 +9,7 @@ where } fn main() { - let mut num: i32 = rmc::nondet(); + let mut num: i32 = rmc::any(); let y = 2; if num <= std::i32::MAX - 100 { // avoid overflow diff --git a/src/test/expected/closure3/main.rs b/src/test/expected/closure3/main.rs index afb1fde1ccd6..88b34e70acf4 100644 --- a/src/test/expected/closure3/main.rs +++ b/src/test/expected/closure3/main.rs @@ -8,7 +8,7 @@ where } fn main() { - let num: i64 = rmc::nondet(); + let num: i64 = rmc::any(); if num <= std::i64::MAX - 100 { // avoid overflow let y = call_with_one(|x| x + num); diff --git a/src/test/expected/comp/main.rs b/src/test/expected/comp/main.rs index 472b49ef8088..8ac10a82f923 100644 --- a/src/test/expected/comp/main.rs +++ b/src/test/expected/comp/main.rs @@ -13,8 +13,8 @@ fn eq2(a: i32, b: i32) { } fn main() { - let a = rmc::nondet(); - let b = rmc::nondet(); + let a = rmc::any(); + let b = rmc::any(); if a > -400 && a < 100 && b < 200 && b > 0 { eq1(a, b); eq2(a, b); diff --git a/src/test/expected/dynamic-error-trait/main.rs b/src/test/expected/dynamic-error-trait/main.rs index 59b368f47e26..8765eeb409e5 100644 --- a/src/test/expected/dynamic-error-trait/main.rs +++ b/src/test/expected/dynamic-error-trait/main.rs @@ -14,7 +14,7 @@ pub struct MemoryMapping { impl MemoryMapping { pub fn new(size: usize) -> Result { - if rmc::nondet() { + if rmc::any() { let mm = MemoryMapping { addr: std::ptr::null_mut(), size: size }; Ok(mm) } else { diff --git a/src/test/expected/nondet/main.rs b/src/test/expected/nondet/main.rs index e3e10e0c3a36..64c353ec415e 100644 --- a/src/test/expected/nondet/main.rs +++ b/src/test/expected/nondet/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let x: i32 = rmc::nondet(); + let x: i32 = rmc::any(); if (x > -500 && x < 500) { // x * x - 2 * x + 1 == 4 -> x == -1 || x == 3 assert!(x * x - 2 * x + 1 != 4 || (x == -1 || x == 3)); diff --git a/src/test/expected/one-assert/expected b/src/test/expected/one-assert/expected index 6a4df0c7a65f..fe3626889661 100644 --- a/src/test/expected/one-assert/expected +++ b/src/test/expected/one-assert/expected @@ -1 +1 @@ -** 0 of 1 failed (1 iterations) +** 0 of 2 failed (1 iterations) diff --git a/src/test/expected/one-assert/test.rs b/src/test/expected/one-assert/test.rs index 144392c29dbf..9b55d093c869 100644 --- a/src/test/expected/one-assert/test.rs +++ b/src/test/expected/one-assert/test.rs @@ -1,10 +1,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + // rmc-flags: --function check_assert // compile-flags: --crate-type lib #[no_mangle] pub fn check_assert() { - let x: u8 = rmc::nondet(); + let x: u8 = rmc::any(); let y = x; assert!(x == y); } diff --git a/src/test/expected/unwind_tip/main.rs b/src/test/expected/unwind_tip/main.rs index 04bcef9c2d4a..241f52aa19db 100644 --- a/src/test/expected/unwind_tip/main.rs +++ b/src/test/expected/unwind_tip/main.rs @@ -11,7 +11,7 @@ // In this test, we check that RMC warns the user about unwinding failures // and makes a recommendation to fix the issue. fn main() { - let mut a: u32 = rmc::nondet(); + let mut a: u32 = rmc::any(); if a < 1024 { loop { diff --git a/src/test/expected/vecdq/main.rs b/src/test/expected/vecdq/main.rs index 0e7d7f7ed3df..f0ab4b8c6060 100644 --- a/src/test/expected/vecdq/main.rs +++ b/src/test/expected/vecdq/main.rs @@ -3,8 +3,8 @@ use std::collections::VecDeque; fn main() { - let x = rmc::nondet(); - let y = rmc::nondet(); + let x = rmc::any(); + let y = rmc::any(); let mut q: VecDeque = VecDeque::new(); q.push_back(x); q.push_back(y); diff --git a/src/test/firecracker/micro-http-parsed-request/ignore-main.rs b/src/test/firecracker/micro-http-parsed-request/ignore-main.rs index 943dd4de0b6a..f5462bc5094d 100644 --- a/src/test/firecracker/micro-http-parsed-request/ignore-main.rs +++ b/src/test/firecracker/micro-http-parsed-request/ignore-main.rs @@ -5,26 +5,26 @@ // Should return a nondet string of up to n characters // Currently RMC does not support strings -fn rmc::nondet_string(n: u32) -> String { +fn rmc::any_string(n: u32) -> String { unimplemented!() } // from 4e905f741 fn bug(n: u32) { - let request_uri: String = rmc::nondet_string(n); + let request_uri: String = rmc::any_string(n); let _path_tokens: Vec<&str> = request_uri[1..].split_terminator('/').collect(); // ^ slice of empty string panics } // from 22908c9fb fn fix(n: u32) { - let request_uri: String = rmc::nondet_string(n); + let request_uri: String = rmc::any_string(n); let _path_tokens: Vec<&str> = request_uri.trim_start_matches('/').split_terminator('/').collect(); } fn main() { - let n: u32 = rmc::nondet(); + let n: u32 = rmc::any(); bug(n); fix(n); } diff --git a/src/test/firecracker/virtio-balloon-compact/ignore-main.rs b/src/test/firecracker/virtio-balloon-compact/ignore-main.rs index b49da56798ed..c4638a05d4c1 100644 --- a/src/test/firecracker/virtio-balloon-compact/ignore-main.rs +++ b/src/test/firecracker/virtio-balloon-compact/ignore-main.rs @@ -56,7 +56,7 @@ fn expand(ranges: Vec<(u32, u32)>) -> Vec { fn main() { let mut input = vec![0; 2]; for i in 0..input.len() { - input[i] = rmc::nondet(); + input[i] = rmc::any(); if input[i] == u32::MAX { return; } @@ -67,7 +67,7 @@ fn main() { } assert!(output.len() <= input.len()); let expanded_output = expand(output); - let i: usize = rmc::nondet(); + let i: usize = rmc::any(); if i < expanded_output.len() { assert!(expanded_output[i] == input[i]); } diff --git a/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index 669866b59942..6c727dd3b3d8 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -12,9 +12,21 @@ macro_rules! error { struct MyError {} +unsafe impl rmc::Invariant for MyError { + fn is_valid(&self) -> bool { + true + } +} + #[derive(Default, Clone, Copy)] pub struct GuestAddress(pub u64); +unsafe impl rmc::Invariant for GuestAddress { + fn is_valid(&self) -> bool { + true + } +} + static mut TRACK_CHECKED_OFFSET_NONE: bool = false; static mut TRACK_READ_OBJ: Option = None; @@ -23,7 +35,7 @@ pub struct GuestMemoryMmap {} impl GuestMemoryMmap { fn checked_offset(&self, base: GuestAddress, offset: usize) -> Option { let mut retval = None; - if rmc::nondet() { + if rmc::any() { if let Some(sum) = base.0.checked_add(offset as u64) { retval = Some(GuestAddress(sum)) } @@ -36,21 +48,21 @@ impl GuestMemoryMmap { return retval; } - fn read_obj(&self, addr: GuestAddress) -> Result { + fn read_obj(&self, addr: GuestAddress) -> Result { // This assertion means that no descriptor is read more than once unsafe { if let Some(prev_addr) = TRACK_READ_OBJ { assert!(prev_addr.0 != addr.0); } - if rmc::nondet() && TRACK_READ_OBJ.is_none() { + if rmc::any() && TRACK_READ_OBJ.is_none() { TRACK_READ_OBJ = Some(addr); } } - rmc::nondet() + if rmc::any() { Ok(rmc::any::()) } else { Err(rmc::any::()) } } fn read_obj_request_header(&self, addr: GuestAddress) -> Result { - rmc::nondet() + if rmc::any() { Ok(rmc::any::()) } else { Err(rmc::any::()) } } } @@ -67,6 +79,12 @@ struct Descriptor { next: u16, } +unsafe impl rmc::Invariant for Descriptor { + fn is_valid(&self) -> bool { + true + } +} + /// A virtio descriptor chain. pub struct DescriptorChain<'a> { desc_table: GuestAddress, @@ -175,6 +193,12 @@ pub struct RequestHeader { sector: u64, } +unsafe impl rmc::Invariant for RequestHeader { + fn is_valid(&self) -> bool { + true + } +} + impl RequestHeader { pub fn new(request_type: u32, sector: u64) -> RequestHeader { RequestHeader { request_type, _reserved: 0, sector } @@ -229,6 +253,20 @@ pub enum Error { UnexpectedWriteOnlyDescriptor, } +unsafe impl rmc::Invariant for Error { + fn is_valid(&self) -> bool { + matches!( + *self, + Error::DescriptorChainTooShort + | Error::DescriptorLengthTooSmall + | Error::GuestMemory + | Error::InvalidOffset + | Error::UnexpectedReadOnlyDescriptor + | Error::UnexpectedWriteOnlyDescriptor + ) + } +} + pub struct Request { pub request_type: RequestType, pub data_len: u32, @@ -317,12 +355,12 @@ fn is_nonzero_pow2(x: u16) -> bool { fn main() { let mem = GuestMemoryMmap {}; - let queue_size: u16 = rmc::nondet(); + let queue_size: u16 = rmc::any(); if !is_nonzero_pow2(queue_size) { return; } - let index: u16 = rmc::nondet(); - let desc_table = GuestAddress(rmc::nondet::() & 0xffff_ffff_ffff_fff0); + let index: u16 = rmc::any(); + let desc_table = GuestAddress(rmc::any::() & 0xffff_ffff_ffff_fff0); let desc = DescriptorChain::checked_new(&mem, desc_table, queue_size, index); match desc { Some(x) => { diff --git a/src/test/prusti/Binary_search.rs b/src/test/prusti/Binary_search.rs index ae1f8ff8823d..4f17cd894e2f 100644 --- a/src/test/prusti/Binary_search.rs +++ b/src/test/prusti/Binary_search.rs @@ -49,7 +49,7 @@ fn get() -> [i32; 11] { fn main() { let x = get(); - let y = rmc::nondet(); + let y = rmc::any(); if 1 <= y && y <= 11 { assert!(binary_search_wrong(&x, &y) == Some(y as usize - 1)); // this fails diff --git a/src/test/rmc/ArithEqualOperators/main.rs b/src/test/rmc/ArithEqualOperators/main.rs index 3b8fa3798a68..3ccdc428eb5f 100644 --- a/src/test/rmc/ArithEqualOperators/main.rs +++ b/src/test/rmc/ArithEqualOperators/main.rs @@ -1,9 +1,9 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let mut a: u32 = rmc::nondet(); + let mut a: u32 = rmc::any(); a /= 2; - let mut b: u32 = rmc::nondet(); + let mut b: u32 = rmc::any(); b /= 2; let c = b; b += a; diff --git a/src/test/rmc/ArithOperators/main.rs b/src/test/rmc/ArithOperators/main.rs index ba611f96b44b..c18e94984023 100644 --- a/src/test/rmc/ArithOperators/main.rs +++ b/src/test/rmc/ArithOperators/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let a: u32 = rmc::nondet(); + let a: u32 = rmc::any(); assert!(a / 2 <= a); assert!(a / 2 * 2 >= a / 2); assert!(a / 2 + 5 + 1 > a / 2 + 5); diff --git a/src/test/rmc/Assume/main.rs b/src/test/rmc/Assume/main.rs index 2e4b91c45431..2f11194b4c38 100644 --- a/src/test/rmc/Assume/main.rs +++ b/src/test/rmc/Assume/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let i: i32 = rmc::nondet(); + let i: i32 = rmc::any(); rmc::assume(i < 10); assert!(i < 20); } diff --git a/src/test/rmc/Assume/main_fail.rs b/src/test/rmc/Assume/main_fail.rs index 709500cd9ba1..50024ce30f5a 100644 --- a/src/test/rmc/Assume/main_fail.rs +++ b/src/test/rmc/Assume/main_fail.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let i: i32 = rmc::nondet(); + let i: i32 = rmc::any(); rmc::assume(i < 10); rmc::expect_fail(i > 20, "Blocked by assumption above."); } diff --git a/src/test/rmc/BinOp_Offset/main_fail.rs b/src/test/rmc/BinOp_Offset/main_fail.rs index 0d99d452f218..87bc66666aaa 100644 --- a/src/test/rmc/BinOp_Offset/main_fail.rs +++ b/src/test/rmc/BinOp_Offset/main_fail.rs @@ -4,8 +4,8 @@ pub fn test_offset_in_double_array() { //let table: Vec> = Vec::with_capacity(1); - let table: [[u64; 1]; 1] = [[rmc::nondet::()]]; - table[0][rmc::nondet::()]; // EXPECTED FAIL + let table: [[u64; 1]; 1] = [[rmc::any::()]]; + table[0][rmc::any::()]; // EXPECTED FAIL } fn main() { diff --git a/src/test/rmc/BitwiseArithOperators/bool.rs b/src/test/rmc/BitwiseArithOperators/bool.rs index f5311d95898b..95ed6e1f6570 100644 --- a/src/test/rmc/BitwiseArithOperators/bool.rs +++ b/src/test/rmc/BitwiseArithOperators/bool.rs @@ -1,8 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let a: bool = rmc::nondet(); - let b: bool = rmc::nondet(); + let a: bool = rmc::any(); + let b: bool = rmc::any(); let c = a ^ b; assert!((a == b && !c) || (a != b && c)); } diff --git a/src/test/rmc/BitwiseArithOperators/main.rs b/src/test/rmc/BitwiseArithOperators/main.rs index 6288a8f881c9..45e2cdd79a4a 100644 --- a/src/test/rmc/BitwiseArithOperators/main.rs +++ b/src/test/rmc/BitwiseArithOperators/main.rs @@ -7,8 +7,8 @@ fn main() { assert!(!8 ^ !0 == 8); let x = 1; - let a: u32 = rmc::nondet(); - let b: u32 = rmc::nondet(); + let a: u32 = rmc::any(); + let b: u32 = rmc::any(); if a < 100000 && b < 100000 { let c = a + b; if c & x == x { diff --git a/src/test/rmc/BitwiseEqualOperators/main.rs b/src/test/rmc/BitwiseEqualOperators/main.rs index 7319e235d0a8..33b4332d3aa0 100644 --- a/src/test/rmc/BitwiseEqualOperators/main.rs +++ b/src/test/rmc/BitwiseEqualOperators/main.rs @@ -12,10 +12,10 @@ fn main() { x &= 15; assert!(x == 2); - let mut a: u32 = rmc::nondet(); + let mut a: u32 = rmc::any(); a %= 8; - let mut b: u32 = rmc::nondet(); + let mut b: u32 = rmc::any(); b %= 8; let mut c = a; diff --git a/src/test/rmc/Bool-BoolOperators/main.rs b/src/test/rmc/Bool-BoolOperators/main.rs index ba1cf37a5c93..c9665011d186 100644 --- a/src/test/rmc/Bool-BoolOperators/main.rs +++ b/src/test/rmc/Bool-BoolOperators/main.rs @@ -12,6 +12,6 @@ fn main() { assert!(d && true); assert!(!b && d); - let e: bool = rmc::nondet(); + let e: bool = rmc::any(); assert!(e || !e); } diff --git a/src/test/rmc/Cast/from_be_bytes.rs b/src/test/rmc/Cast/from_be_bytes.rs index 8d5f4c5bb4f4..e76d13fe47d7 100644 --- a/src/test/rmc/Cast/from_be_bytes.rs +++ b/src/test/rmc/Cast/from_be_bytes.rs @@ -3,14 +3,14 @@ use std::convert::TryInto; fn main() { let input: &[u8] = &vec![ - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), ]; let buffer = input.as_ref(); let bytes: [u8; 8] = buffer.try_into().unwrap(); diff --git a/src/test/rmc/DynTrait/drop_boxed_dyn.rs b/src/test/rmc/DynTrait/drop_boxed_dyn.rs index 7046ef5f9914..97a150506ec1 100644 --- a/src/test/rmc/DynTrait/drop_boxed_dyn.rs +++ b/src/test/rmc/DynTrait/drop_boxed_dyn.rs @@ -36,7 +36,7 @@ impl Drop for Concrete2 { fn main() { { let x: Box; - if rmc::nondet() { + if rmc::any() { x = Box::new(Concrete1 {}); } else { x = Box::new(Concrete2 {}); diff --git a/src/test/rmc/DynTrait/main.rs b/src/test/rmc/DynTrait/main.rs index 82ccba691131..29eae7e29481 100644 --- a/src/test/rmc/DynTrait/main.rs +++ b/src/test/rmc/DynTrait/main.rs @@ -9,11 +9,6 @@ trait Animal { fn noise(&self) -> i32; } -trait Other { - // Instance method signature - fn noise(&self) -> i32; -} - // Implement the `Animal` trait for `Sheep`. impl Animal for Sheep { fn noise(&self) -> i32 { @@ -34,7 +29,7 @@ fn random_animal(random_number: i64) -> Box { } fn main() { - let random_number = rmc::nondet(); + let random_number = rmc::any(); let animal = random_animal(random_number); let s = animal.noise(); if random_number < 5 { diff --git a/src/test/rmc/DynTrait/main_fail.rs b/src/test/rmc/DynTrait/main_fail.rs index 1e918c50d81a..a98a7cbe1b69 100644 --- a/src/test/rmc/DynTrait/main_fail.rs +++ b/src/test/rmc/DynTrait/main_fail.rs @@ -29,7 +29,7 @@ fn random_animal(random_number: i64) -> Box { } fn main() { - let random_number = rmc::nondet(); + let random_number = rmc::any(); let animal = random_animal(random_number); let s = animal.noise(); if (random_number < 5) { diff --git a/src/test/rmc/EQ-NE/main.rs b/src/test/rmc/EQ-NE/main.rs index 5849086dff9c..c77bf3659bc4 100644 --- a/src/test/rmc/EQ-NE/main.rs +++ b/src/test/rmc/EQ-NE/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let x: u32 = rmc::nondet(); + let x: u32 = rmc::any(); if x < u32::MAX >> 1 { let y = x * 2; diff --git a/src/test/rmc/Enum/result3.rs b/src/test/rmc/Enum/result3.rs index 5531362420b7..b61c66bcc08c 100644 --- a/src/test/rmc/Enum/result3.rs +++ b/src/test/rmc/Enum/result3.rs @@ -11,10 +11,10 @@ fn foo(input: &Result) -> u32 { } fn main() { - let input: Result = rmc::nondet(); + let input: Result = unsafe { rmc::any_raw() }; let x = foo(&input); assert!(x == 3 || input != Err(Unit::Unit)); - let input: Result = if rmc::nondet() { Ok(0) } else { Err(Unit::Unit) }; + let input: Result = if rmc::any() { Ok(0) } else { Err(Unit::Unit) }; let x = foo(&input); assert!(x != 3 || input == Err(Unit::Unit)); assert!(x != 0 || input == Ok(0)); diff --git a/src/test/rmc/FloatingPoint/main.rs b/src/test/rmc/FloatingPoint/main.rs index 589a2642f1b3..d44659956cd9 100644 --- a/src/test/rmc/FloatingPoint/main.rs +++ b/src/test/rmc/FloatingPoint/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT macro_rules! test_floats { ($ty:ty) => { - let a: $ty = rmc::nondet(); + let a: $ty = rmc::any(); let b = a / 2.0; if a < 0.0 { diff --git a/src/test/rmc/FunctionAbstractions/mem_replace.rs b/src/test/rmc/FunctionAbstractions/mem_replace.rs index 32ba619da356..d2e071c5f17e 100644 --- a/src/test/rmc/FunctionAbstractions/mem_replace.rs +++ b/src/test/rmc/FunctionAbstractions/mem_replace.rs @@ -4,8 +4,8 @@ use std::mem; fn main() { - let mut var1 = rmc::nondet::(); - let mut var2 = rmc::nondet::(); + let mut var1 = rmc::any::(); + let mut var2 = rmc::any::(); let old_var1 = var1; unsafe { assert_eq!(mem::replace(&mut var1, var2), old_var1); diff --git a/src/test/rmc/FunctionAbstractions/mem_swap.rs b/src/test/rmc/FunctionAbstractions/mem_swap.rs index 7517cbcfb28d..069f51d8b708 100644 --- a/src/test/rmc/FunctionAbstractions/mem_swap.rs +++ b/src/test/rmc/FunctionAbstractions/mem_swap.rs @@ -4,8 +4,8 @@ use std::mem; fn main() { - let mut var1 = rmc::nondet::(); - let mut var2 = rmc::nondet::(); + let mut var1 = rmc::any::(); + let mut var2 = rmc::any::(); let old_var1 = var1; let old_var2 = var2; unsafe { diff --git a/src/test/rmc/FunctionCall_Ret-NoParam/main.rs b/src/test/rmc/FunctionCall_Ret-NoParam/main.rs index fb2df43cb4a0..6850b707495c 100644 --- a/src/test/rmc/FunctionCall_Ret-NoParam/main.rs +++ b/src/test/rmc/FunctionCall_Ret-NoParam/main.rs @@ -10,7 +10,7 @@ fn main() { assert!(return_f64() < 11.0 && return_f64() > -11.0); } fn return_u32() -> u32 { - let x: u32 = rmc::nondet(); + let x: u32 = rmc::any(); if x < 10 { return x; @@ -19,7 +19,7 @@ fn return_u32() -> u32 { } } fn return_u64() -> u64 { - let x: u64 = rmc::nondet(); + let x: u64 = rmc::any(); if x > 100 { return x; @@ -28,7 +28,7 @@ fn return_u64() -> u64 { } } fn return_bool() -> bool { - let x: bool = rmc::nondet(); + let x: bool = rmc::any(); if x { return x; } else { @@ -37,7 +37,7 @@ fn return_bool() -> bool { } fn return_f32() -> f32 { let x = 10.0; - let y: bool = rmc::nondet(); + let y: bool = rmc::any(); if y { return x / 2.0; } else { @@ -45,7 +45,7 @@ fn return_f32() -> f32 { } } fn return_f64() -> f64 { - let x: f64 = rmc::nondet(); + let x: f64 = rmc::any(); if x <= 10.0 && x >= -10.0 { return x; } else { diff --git a/src/test/rmc/FunctionCall_Ret-Param/main.rs b/src/test/rmc/FunctionCall_Ret-Param/main.rs index 57c0e14b8515..7540bf16b540 100644 --- a/src/test/rmc/FunctionCall_Ret-Param/main.rs +++ b/src/test/rmc/FunctionCall_Ret-Param/main.rs @@ -9,7 +9,7 @@ // a nondet. variable) fn main() { - let x: u32 = rmc::nondet(); + let x: u32 = rmc::any(); let pi = 3.14159265359; let x_iters = leibniz_pi(x); diff --git a/src/test/rmc/IfElseifElse_NonReturning/main.rs b/src/test/rmc/IfElseifElse_NonReturning/main.rs index 0b90b631978e..99a428156a4d 100644 --- a/src/test/rmc/IfElseifElse_NonReturning/main.rs +++ b/src/test/rmc/IfElseifElse_NonReturning/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let a: u32 = rmc::nondet(); + let a: u32 = rmc::any(); if a % 3 == 0 { assert!(a != 4); diff --git a/src/test/rmc/IfElseifElse_Returning/main.rs b/src/test/rmc/IfElseifElse_Returning/main.rs index c3cb9e62fc44..16a8ff42eb96 100644 --- a/src/test/rmc/IfElseifElse_Returning/main.rs +++ b/src/test/rmc/IfElseifElse_Returning/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let a: u32 = rmc::nondet(); + let a: u32 = rmc::any(); let b = if a % 3 == 0 { assert!(a != 5); @@ -16,7 +16,7 @@ fn main() { assert!(b < 3); - let c: u32 = rmc::nondet(); + let c: u32 = rmc::any(); let d = if c > 100 { c diff --git a/src/test/rmc/Invariants/array.rs b/src/test/rmc/Invariants/array.rs new file mode 100644 index 000000000000..3eff0a25f0d6 --- /dev/null +++ b/src/test/rmc/Invariants/array.rs @@ -0,0 +1,15 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-flags: --unwind 3 +// Check that the Invariant implementation for array respect the underlying types invariant. + +extern crate rmc; + +use rmc::Invariant; + +fn main() { + let arr: [char; 2] = rmc::any(); + assert!(arr[0].is_valid()); + assert!(arr[1].is_valid()); +} diff --git a/src/test/rmc/Invariants/array_raw_fail.rs b/src/test/rmc/Invariants/array_raw_fail.rs new file mode 100644 index 000000000000..62b7e2541e5f --- /dev/null +++ b/src/test/rmc/Invariants/array_raw_fail.rs @@ -0,0 +1,15 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-flags: --unwind 3 +// Check that any_raw for arrays do not respect the elements invariants. + +extern crate rmc; + +use rmc::Invariant; + +fn main() { + let arr_raw: [char; 2] = unsafe { rmc::any_raw() }; + rmc::expect_fail(arr_raw[0].is_valid(), "Should fail"); + rmc::expect_fail(arr_raw[1].is_valid(), "Should fail"); +} diff --git a/src/test/rmc/Invariants/bool.rs b/src/test/rmc/Invariants/bool.rs new file mode 100644 index 000000000000..26bf3f669928 --- /dev/null +++ b/src/test/rmc/Invariants/bool.rs @@ -0,0 +1,13 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that rmc::any:: generates only valid booleans. + +fn main() { + let b: bool = rmc::any(); + match b { + true => assert!(b as u8 == 1), + false => assert!(b as u8 == 0), + } + assert!(matches!(b, true | false)); +} diff --git a/src/test/rmc/Invariants/bool_raw_fail.rs b/src/test/rmc/Invariants/bool_raw_fail.rs new file mode 100644 index 000000000000..7de1aa63d90b --- /dev/null +++ b/src/test/rmc/Invariants/bool_raw_fail.rs @@ -0,0 +1,13 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that rmc::any_raw:: may generate invalid booleans. + +fn main() { + let b: bool = unsafe { rmc::any_raw() }; + assert!(matches!(b, true | false), "Rust converts any non-zero value to true"); + match b { + true => rmc::expect_fail(b as u8 == 1, "This can be any non-zero value"), + false => assert!(b as u8 == 0), + } +} diff --git a/src/test/rmc/Invariants/char.rs b/src/test/rmc/Invariants/char.rs new file mode 100644 index 000000000000..0483846c8c5e --- /dev/null +++ b/src/test/rmc/Invariants/char.rs @@ -0,0 +1,8 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that rmc::any respect the char::MAX limit. +pub fn main() { + let c: char = rmc::any(); + assert!(c <= char::MAX); +} diff --git a/src/test/rmc/Invariants/char_fail.rs b/src/test/rmc/Invariants/char_fail.rs new file mode 100644 index 000000000000..7ba97c603f82 --- /dev/null +++ b/src/test/rmc/Invariants/char_fail.rs @@ -0,0 +1,8 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that rmc::any_raw may generate invalid char. +pub fn main() { + let c: char = unsafe { rmc::any_raw() }; + rmc::expect_fail(c <= char::MAX, "rmc::any_raw() may generate invalid values"); +} diff --git a/src/test/rmc/Invariants/enum.rs b/src/test/rmc/Invariants/enum.rs new file mode 100644 index 000000000000..4cad4ca7e43e --- /dev/null +++ b/src/test/rmc/Invariants/enum.rs @@ -0,0 +1,66 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Check that we correctly generate invariants for enums. + +#[derive(Copy, Clone)] +enum Basic { + Variant1, + Variant2, + Variant3, +} + +#[derive(Copy, Clone)] +enum Continuous { + Variant1 = 10, + Variant2, + Variant3, +} + +#[derive(Copy, Clone)] +enum Random { + Variant1 = -10, + Variant2 = 100, + Variant3 = 0, +} + +macro_rules! check_enum { + ( $fn_name:ident, $repr:ty, $enum_type:ident, $v1:literal, $v2:literal, $v3:literal ) => { + unsafe impl rmc::Invariant for $enum_type { + fn is_valid(&self) -> bool { + matches!(*self, $enum_type::Variant1 | $enum_type::Variant2 | $enum_type::Variant3) + } + } + + fn $fn_name() { + let e = rmc::any::<$enum_type>(); + match e { + $enum_type::Variant1 => { + let val = e as $repr; + assert!(val == $v1); + return; + } + $enum_type::Variant2 => { + let val = e as $repr; + assert!(val == $v2); + return; + } + $enum_type::Variant3 => { + let val = e as $repr; + assert!(val == $v3); + return; + } + } + } + }; +} + +check_enum!(check_basic, u8, Basic, 0, 1, 2); +check_enum!(check_continuous, u8, Continuous, 10, 11, 12); +check_enum!(check_random, i8, Random, -10, 100, 0); + +fn main() { + check_basic(); + check_continuous(); + check_random(); +} diff --git a/src/test/rmc/Invariants/enum_raw_fail.rs b/src/test/rmc/Invariants/enum_raw_fail.rs new file mode 100644 index 000000000000..89920c94f13f --- /dev/null +++ b/src/test/rmc/Invariants/enum_raw_fail.rs @@ -0,0 +1,39 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-verify-fail +// Check that rmc::raw_any for enums will generate invalid enums. +// This code should fail due to unreachable code being reached. + +#[derive(Copy, Clone)] +enum Basic { + Variant1, + Variant2, + Variant3, +} + +fn main() { + let e = unsafe { rmc::any_raw::() }; + // This enum can be invalid and this code may actually not match any of the options below. + rmc::expect_fail( + matches!(e, Basic::Variant1 | Basic::Variant2 | Basic::Variant3), + "Invalid enum variant", + ); + match e { + Basic::Variant1 => { + let val = e as u8; + assert!(val == 0); + return; + } + Basic::Variant2 => { + let val = e as u8; + assert!(val == 1); + return; + } + Basic::Variant3 => { + let val = e as u8; + assert!(val == 2); + return; + } + } +} diff --git a/src/test/rmc/Invariants/float.rs b/src/test/rmc/Invariants/float.rs new file mode 100644 index 000000000000..14c805ff2654 --- /dev/null +++ b/src/test/rmc/Invariants/float.rs @@ -0,0 +1,22 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that rmc::any and rmc::any_raw can be used with integers. + +macro_rules! test { + ( $type: ty ) => {{ + let v1 = rmc::any::<$type>(); + let v2 = unsafe { rmc::any_raw::<$type>() }; + rmc::expect_fail(v1 == v2, "This may not be true"); + rmc::expect_fail(v1 != v2, "This may also not be true"); + rmc::expect_fail(!v1.is_nan(), "NaN should be valid float"); + rmc::expect_fail(!v1.is_subnormal(), "Subnormal should be valid float"); + rmc::expect_fail(!v1.is_normal(), "Normal should be valid float"); + rmc::expect_fail(v1.is_finite(), "Non-finite numbers are valid float"); + }}; +} + +fn main() { + test!(f32); + test!(f64); +} diff --git a/src/test/rmc/Invariants/integer.rs b/src/test/rmc/Invariants/integer.rs new file mode 100644 index 000000000000..2278cf2dd4a6 --- /dev/null +++ b/src/test/rmc/Invariants/integer.rs @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that rmc::any and rmc::any_raw can be used with integers. + +macro_rules! test { + ( $type: ty ) => {{ + let v1 = rmc::any::<$type>(); + let v2 = unsafe { rmc::any_raw::<$type>() }; + rmc::expect_fail(v1 == v2, "This may not be true"); + rmc::expect_fail(v1 != v2, "This may also not be true"); + }}; +} + +fn main() { + test!(i8); + test!(i16); + test!(i32); + test!(i64); + test!(i128); + test!(isize); + + test!(u8); + test!(u16); + test!(u32); + test!(u64); + test!(u128); + test!(usize); +} diff --git a/src/test/rmc/Invariants/nonzero.rs b/src/test/rmc/Invariants/nonzero.rs new file mode 100644 index 000000000000..f830d108dd25 --- /dev/null +++ b/src/test/rmc/Invariants/nonzero.rs @@ -0,0 +1,39 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that rmc::any behaves correcty with NonZero types. This also shows how using the unsafe +// kind can generate UB. + +use std::num::*; + +macro_rules! test { + ( $type: ty ) => {{ + let v1 = rmc::any::<$type>(); + assert!(v1.get() != 0, "Any should not generate value zero"); + + let option = Some(v1); + assert!(option.is_some(), "Niche optimization works well."); + + let v2 = unsafe { rmc::any_raw::<$type>() }; + rmc::expect_fail(v2.get() != 0, "Any raw may generate invalid value."); + + let option = Some(v2); + rmc::expect_fail(option.is_some(), "Yep. This can happen due to niche optimization"); + }}; +} + +fn main() { + test!(NonZeroI8); + test!(NonZeroI16); + test!(NonZeroI32); + test!(NonZeroI64); + test!(NonZeroI128); + test!(NonZeroIsize); + + test!(NonZeroU8); + test!(NonZeroU16); + test!(NonZeroU32); + test!(NonZeroU64); + test!(NonZeroU128); + test!(NonZeroUsize); +} diff --git a/src/test/rmc/Invariants/option.rs b/src/test/rmc/Invariants/option.rs new file mode 100644 index 000000000000..92f2cfe487b2 --- /dev/null +++ b/src/test/rmc/Invariants/option.rs @@ -0,0 +1,26 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Check that the Invariant implementation for Option respect underlying types invariant. + +extern crate rmc; + +use rmc::Invariant; + +struct MyType { + pub val: char, +} + +unsafe impl rmc::Invariant for MyType { + fn is_valid(&self) -> bool { + self.val.is_valid() + } +} + +fn main() { + let option: Option = rmc::any(); + match option { + Some(v) => assert!(v.is_valid() && v.val <= char::MAX), + None => (), + } +} diff --git a/src/test/rmc/Invariants/option_raw_fail.rs b/src/test/rmc/Invariants/option_raw_fail.rs new file mode 100644 index 000000000000..2ad74d45d818 --- /dev/null +++ b/src/test/rmc/Invariants/option_raw_fail.rs @@ -0,0 +1,25 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that rmc::any_raw will generate unsconstrainted values for Option. + +extern crate rmc; + +use rmc::Invariant; + +struct MyType { + pub val: char, +} + +unsafe impl rmc::Invariant for MyType { + fn is_valid(&self) -> bool { + self.val.is_valid() + } +} + +fn main() { + let option: Option = unsafe { rmc::any_raw() }; + if let Some(ref v) = option { + rmc::expect_fail(v.is_valid(), "No guarantee about the underlying value"); + } +} diff --git a/src/test/rmc/Invariants/result.rs b/src/test/rmc/Invariants/result.rs new file mode 100644 index 000000000000..f71b18b92650 --- /dev/null +++ b/src/test/rmc/Invariants/result.rs @@ -0,0 +1,39 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Check that the Invariant implementation for Result respect underlying types invariant. + +extern crate rmc; + +use rmc::Invariant; + +#[derive(PartialEq)] +enum Error { + Error1, + Error2, +} + +struct MyType { + pub val: i32, + pub is_negative: bool, +} + +unsafe impl rmc::Invariant for MyType { + fn is_valid(&self) -> bool { + (self.is_negative && self.val < 0) || (!self.is_negative && self.val >= 0) + } +} + +unsafe impl rmc::Invariant for Error { + fn is_valid(&self) -> bool { + matches!(*self, Error::Error1 | Error::Error2) + } +} + +fn main() { + let result: Result = rmc::any(); + match result { + Ok(v) => assert!(v.is_valid()), + Err(e) => assert!(e.is_valid()), + } +} diff --git a/src/test/rmc/Invariants/result_raw_fail.rs b/src/test/rmc/Invariants/result_raw_fail.rs new file mode 100644 index 000000000000..d7f30fdbd910 --- /dev/null +++ b/src/test/rmc/Invariants/result_raw_fail.rs @@ -0,0 +1,43 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that rmc::any_raw will generate unsconstrainted values for Result. + +extern crate rmc; + +use rmc::Invariant; + +#[derive(PartialEq)] +enum Error { + Error1, + Error2, +} + +struct MyType { + pub val: i32, + pub is_negative: bool, +} + +unsafe impl rmc::Invariant for MyType { + fn is_valid(&self) -> bool { + (self.is_negative && self.val < 0) || (!self.is_negative && self.val >= 0) + } +} + +unsafe impl rmc::Invariant for Error { + fn is_valid(&self) -> bool { + matches!(*self, Error::Error1 | Error::Error2) + } +} + +fn main() { + let result: Result = unsafe { rmc::any_raw() }; + if let Ok(ref v) = result { + rmc::expect_fail(v.is_valid(), "No guarantee about the underlying value"); + } + if let Err(e) = result { + rmc::expect_fail(e.is_valid(), "No guarantee about the underlying error"); + } else { + rmc::expect_fail(false, "This is also reachable since the enum is unconstrained."); + } +} diff --git a/src/test/rmc/LT-GT-LE-GE/main.rs b/src/test/rmc/LT-GT-LE-GE/main.rs index b29d66d9520a..157d916883de 100644 --- a/src/test/rmc/LT-GT-LE-GE/main.rs +++ b/src/test/rmc/LT-GT-LE-GE/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let a: u32 = rmc::nondet(); + let a: u32 = rmc::any(); let b = a / 2; assert!(b <= a); let c = b * 2; diff --git a/src/test/rmc/LoopLoop_NonReturning/main.rs b/src/test/rmc/LoopLoop_NonReturning/main.rs index 76591cfa43b1..7c4c63c3b583 100644 --- a/src/test/rmc/LoopLoop_NonReturning/main.rs +++ b/src/test/rmc/LoopLoop_NonReturning/main.rs @@ -4,7 +4,7 @@ // cbmc-flags: --unwind 10 fn main() { - let mut a: u32 = rmc::nondet(); + let mut a: u32 = rmc::any(); if a < 1024 { loop { diff --git a/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs b/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs index 9b1a725767ab..7d666156742b 100644 --- a/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs +++ b/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs @@ -22,7 +22,7 @@ // ** 0 of 1 failed (1 iterations) // VERIFICATION SUCCESSFUL fn main() { - let mut a: u32 = rmc::nondet(); + let mut a: u32 = rmc::any(); if a < 1024 { loop { diff --git a/src/test/rmc/LoopWhile_NonReturning/main.rs b/src/test/rmc/LoopWhile_NonReturning/main.rs index 85dc4bc2772d..be6696e0f991 100644 --- a/src/test/rmc/LoopWhile_NonReturning/main.rs +++ b/src/test/rmc/LoopWhile_NonReturning/main.rs @@ -4,7 +4,7 @@ // cbmc-flags: --unwind 11 fn main() { - let mut a: u32 = rmc::nondet(); + let mut a: u32 = rmc::any(); if a < 1024 { while a > 0 { diff --git a/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs b/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs index 37a6be42b67c..667fb44d2551 100644 --- a/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs +++ b/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs @@ -23,7 +23,7 @@ // ** 0 of 1 failed (1 iterations) // VERIFICATION SUCCESSFUL fn main() { - let mut a: u32 = rmc::nondet(); + let mut a: u32 = rmc::any(); if a < 1024 { while a > 0 { diff --git a/src/test/rmc/Never/never_return.rs b/src/test/rmc/Never/never_return.rs index 5bd1be309eb7..7653e4b4dd88 100644 --- a/src/test/rmc/Never/never_return.rs +++ b/src/test/rmc/Never/never_return.rs @@ -12,7 +12,7 @@ pub fn err() -> ! { // Give an empty main to make rustc happy. #[no_mangle] fn main() { - let var = rmc::nondet::(); + let var = rmc::any::(); if var > 0 { err(); } diff --git a/src/test/rmc/NondetSlices/test1.rs b/src/test/rmc/NondetSlices/test1.rs index c072c9661a08..3158dff4848a 100644 --- a/src/test/rmc/NondetSlices/test1.rs +++ b/src/test/rmc/NondetSlices/test1.rs @@ -19,6 +19,6 @@ fn main() { let arr = [1, 2, 3]; // The slice returned can be any of the following: // {[], [1], [2], [3], [1, 2], [2, 3], [1, 2, 3]} - let slice = rmc::slice::nondet_slice_of_array(&arr); + let slice = rmc::slice::any_slice_of_array(&arr); check(slice); } diff --git a/src/test/rmc/NondetSlices/test2.rs b/src/test/rmc/NondetSlices/test2.rs index bb58f1b6e91d..3d49aa0406fb 100644 --- a/src/test/rmc/NondetSlices/test2.rs +++ b/src/test/rmc/NondetSlices/test2.rs @@ -9,6 +9,6 @@ fn check(s: &[u8]) { fn main() { // returns a slice of length between 0 and 5 with non-det content - let slice: rmc::slice::NonDetSlice = rmc::slice::nondet_slice(); + let slice: rmc::slice::NonDetSlice = rmc::slice::any_slice(); check(&slice); } diff --git a/src/test/rmc/NondetVectors/bytes.rs b/src/test/rmc/NondetVectors/bytes.rs index ac819897ccd5..f06f6ccefc8b 100644 --- a/src/test/rmc/NondetVectors/bytes.rs +++ b/src/test/rmc/NondetVectors/bytes.rs @@ -4,19 +4,19 @@ use std::convert::TryInto; fn main() { let input: &[u8] = &vec![ - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), - rmc::nondet(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), + rmc::any(), ]; let buffer = input.as_ref(); let bytes: [u8; 8] = buffer.try_into().unwrap(); let value = u64::from_be_bytes(bytes); - let idx: usize = rmc::nondet(); + let idx: usize = rmc::any(); if idx < 8 { assert!(u64::to_be_bytes(value)[idx] == input[idx]); } diff --git a/src/test/rmc/NondetVectors/fixme_main.rs b/src/test/rmc/NondetVectors/fixme_main.rs index 889d1131098b..62e8f4ec2343 100644 --- a/src/test/rmc/NondetVectors/fixme_main.rs +++ b/src/test/rmc/NondetVectors/fixme_main.rs @@ -2,14 +2,14 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT const FIFO_SIZE: usize = 2; fn main() { - let len: usize = rmc::nondet(); + let len: usize = rmc::any(); if !(len <= FIFO_SIZE) { return; } let _buf1: Vec = vec![0u8; len]; //< this works - let elt: u8 = rmc::nondet(); + let elt: u8 = rmc::any(); let _buf2: Vec = vec![elt; len]; //< this fails: "memset destination region writeable" - let idx: usize = rmc::nondet(); + let idx: usize = rmc::any(); if idx < len { assert!(_buf1[idx] == 0u8); assert!(_buf2[idx] == elt); diff --git a/src/test/rmc/Pointers_OtherTypes/main.rs b/src/test/rmc/Pointers_OtherTypes/main.rs index be5c183d0e25..975d4f23ef93 100644 --- a/src/test/rmc/Pointers_OtherTypes/main.rs +++ b/src/test/rmc/Pointers_OtherTypes/main.rs @@ -21,7 +21,7 @@ fn main() { make_true(&mut z); assert!(z); - let mut a: f32 = rmc::nondet(); + let mut a: f32 = rmc::any(); let b = a; div_by_two(&mut a); // NaN diff --git a/src/test/rmc/SaturatingIntrinsics/add_128.rs b/src/test/rmc/SaturatingIntrinsics/add_128.rs index 66e9f2848a5d..afb788139a08 100644 --- a/src/test/rmc/SaturatingIntrinsics/add_128.rs +++ b/src/test/rmc/SaturatingIntrinsics/add_128.rs @@ -6,7 +6,7 @@ use std::intrinsics; fn main() { - let v: u128 = rmc::nondet(); - let w: u128 = rmc::nondet(); + let v: u128 = rmc::any(); + let w: u128 = rmc::any(); intrinsics::saturating_add(v, w); } diff --git a/src/test/rmc/SaturatingIntrinsics/main.rs b/src/test/rmc/SaturatingIntrinsics/main.rs index 31fa51b78d45..2f6e2c27a2ae 100644 --- a/src/test/rmc/SaturatingIntrinsics/main.rs +++ b/src/test/rmc/SaturatingIntrinsics/main.rs @@ -5,8 +5,8 @@ use std::intrinsics; macro_rules! test_saturating_intrinsics { ($ty:ty) => { - let v: $ty = rmc::nondet(); - let w: $ty = rmc::nondet(); + let v: $ty = rmc::any(); + let w: $ty = rmc::any(); let result = intrinsics::saturating_add(v, w); match (0 <= v, 0 <= w) { (true, true) => { diff --git a/src/test/rmc/Scopes_NonReturning/main.rs b/src/test/rmc/Scopes_NonReturning/main.rs index b2dbb0cb0d57..6e28579cdaa4 100644 --- a/src/test/rmc/Scopes_NonReturning/main.rs +++ b/src/test/rmc/Scopes_NonReturning/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let a: u32 = rmc::nondet(); + let a: u32 = rmc::any(); let b = a / 2; let c = a / 2; { diff --git a/src/test/rmc/Scopes_Returning/main.rs b/src/test/rmc/Scopes_Returning/main.rs index d0de28d81371..a1ff082f1e11 100644 --- a/src/test/rmc/Scopes_Returning/main.rs +++ b/src/test/rmc/Scopes_Returning/main.rs @@ -18,7 +18,7 @@ fn main() { }; assert!(c == 10); - let d: u32 = rmc::nondet(); + let d: u32 = rmc::any(); let e = { let f: u32; @@ -32,7 +32,7 @@ fn main() { }; assert!(e == d || e == 10); - let g: u32 = rmc::nondet(); + let g: u32 = rmc::any(); let h = { if g < 10 { g } else { 10 } }; diff --git a/src/test/rmc/i32-Unary-/main.rs b/src/test/rmc/i32-Unary-/main.rs index 0fb94edd4261..5ac5d0e27dc7 100644 --- a/src/test/rmc/i32-Unary-/main.rs +++ b/src/test/rmc/i32-Unary-/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let a: i32 = rmc::nondet(); + let a: i32 = rmc::any(); if -100000 < a && a < 100000 { let b = -a; diff --git a/src/test/serial/serial.rs b/src/test/serial/serial.rs index 230ce94db0ca..545a928c1a76 100644 --- a/src/test/serial/serial.rs +++ b/src/test/serial/serial.rs @@ -326,9 +326,9 @@ fn main() { { // test_serial_modem() let mut serial = Serial::new_sink(EventFd {}); - let a: u8 = rmc::nondet(); - let b: u8 = rmc::nondet(); - let c: u8 = rmc::nondet(); + let a: u8 = rmc::any(); + let b: u8 = rmc::any(); + let c: u8 = rmc::any(); serial.write(MCR as u64, &[MCR_LOOP_BIT as u8]); serial.write(DATA as u64, &[a]); @@ -352,9 +352,9 @@ fn main() { // // test_serial_data_len() // const LEN: usize = 1; // let mut serial = Serial::new_out(EventFd {}, OutWrapper::new()); - // let a: u8 = rmc::nondet(); - // let b: u8 = rmc::nondet(); - // let c: u8 = rmc::nondet(); + // let a: u8 = rmc::any(); + // let b: u8 = rmc::any(); + // let c: u8 = rmc::any(); // // let missed_writes_before = METRICS.uart.missed_write_count.count(); // // Trying to write data of length different than the one that we initialized the device with diff --git a/src/test/serial/serial2.rs b/src/test/serial/serial2.rs index f05d9f7ca4d2..b35aee1b580b 100644 --- a/src/test/serial/serial2.rs +++ b/src/test/serial/serial2.rs @@ -327,9 +327,9 @@ fn main() { // test_serial_data_len() const LEN: usize = 1; let mut serial = Serial::new_out(EventFd {}, OutWrapper::new()); - let a: u8 = rmc::nondet(); - let b: u8 = rmc::nondet(); - let c: u8 = rmc::nondet(); + let a: u8 = rmc::any(); + let b: u8 = rmc::any(); + let c: u8 = rmc::any(); // let missed_writes_before = METRICS.uart.missed_write_count.count(); // Trying to write data of length different than the one that we initialized the device with diff --git a/src/test/serial/serial_spec.rs b/src/test/serial/serial_spec.rs index a63a2630d791..6f176275f596 100644 --- a/src/test/serial/serial_spec.rs +++ b/src/test/serial/serial_spec.rs @@ -467,9 +467,9 @@ impl Serial { fn main() { { let mut serial = Serial::new_sink(EventFd {}); - let a: u8 = rmc::nondet(); - let b: u8 = rmc::nondet(); - let c: u8 = rmc::nondet(); + let a: u8 = rmc::any(); + let b: u8 = rmc::any(); + let c: u8 = rmc::any(); serial.write(MCR as u64, &[MCR_LOOP_BIT as u8]); serial.write(DATA as u64, &[a]); diff --git a/src/test/smack/basic/arith_assume.rs b/src/test/smack/basic/arith_assume.rs index 2abacaccb6b1..47874c91d631 100644 --- a/src/test/smack/basic/arith_assume.rs +++ b/src/test/smack/basic/arith_assume.rs @@ -3,8 +3,8 @@ // @expect verified pub fn main() { - let a = rmc::nondet(); - let b = rmc::nondet(); + let a = rmc::any(); + let b = rmc::any(); if 4 < a && a < 8 { // a in [5,7] if 5 < b && b < 9 { diff --git a/src/test/smack/basic/arith_assume2.rs b/src/test/smack/basic/arith_assume2.rs index 2abacaccb6b1..47874c91d631 100644 --- a/src/test/smack/basic/arith_assume2.rs +++ b/src/test/smack/basic/arith_assume2.rs @@ -3,8 +3,8 @@ // @expect verified pub fn main() { - let a = rmc::nondet(); - let b = rmc::nondet(); + let a = rmc::any(); + let b = rmc::any(); if 4 < a && a < 8 { // a in [5,7] if 5 < b && b < 9 { diff --git a/src/test/smack/basic/arith_assume3.rs b/src/test/smack/basic/arith_assume3.rs index c63397ddc794..8b0aef9865e2 100644 --- a/src/test/smack/basic/arith_assume3.rs +++ b/src/test/smack/basic/arith_assume3.rs @@ -4,8 +4,8 @@ // rmc-verify-fail pub fn main() { - let a = rmc::nondet(); - let b = rmc::nondet(); + let a = rmc::any(); + let b = rmc::any(); if 4 < a && a < 8 { // a in [5,7] if 5 < b && b < 9 { diff --git a/src/test/smack/functions/closure.rs b/src/test/smack/functions/closure.rs index ab7c2870603f..f384fbc796bc 100644 --- a/src/test/smack/functions/closure.rs +++ b/src/test/smack/functions/closure.rs @@ -11,7 +11,7 @@ where } pub fn main() { - let mut num: i32 = rmc::nondet(); + let mut num: i32 = rmc::any(); if num <= std::i32::MAX - 10 { let original_num = num; { diff --git a/src/test/smack/functions/closure_fail.rs b/src/test/smack/functions/closure_fail.rs index 371b0ba83343..2b0918456dc6 100644 --- a/src/test/smack/functions/closure_fail.rs +++ b/src/test/smack/functions/closure_fail.rs @@ -12,7 +12,7 @@ where } pub fn main() { - let mut num: i32 = rmc::nondet(); + let mut num: i32 = rmc::any(); if num <= std::i32::MAX - 10 { let original_num = num; { diff --git a/src/test/smack/functions/double.rs b/src/test/smack/functions/double.rs index ed030d8b7b7e..cfafee4c2152 100644 --- a/src/test/smack/functions/double.rs +++ b/src/test/smack/functions/double.rs @@ -7,7 +7,7 @@ fn double(a: u32) -> u32 { } pub fn main() { - let a = rmc::nondet(); + let a = rmc::any(); if a <= std::u32::MAX / 2 { let b = double(a); assert!(b == 2 * a); diff --git a/src/test/smack/functions/double_fail.rs b/src/test/smack/functions/double_fail.rs index 668b04f08596..4f45cd62350c 100644 --- a/src/test/smack/functions/double_fail.rs +++ b/src/test/smack/functions/double_fail.rs @@ -8,7 +8,7 @@ fn double(a: u32) -> u32 { } pub fn main() { - let a = rmc::nondet(); + let a = rmc::any(); if a <= std::u32::MAX / 2 { // avoid overflow let b = double(a); diff --git a/src/test/smack/generics/generic_function.rs b/src/test/smack/generics/generic_function.rs index ee8059692979..a0969ca4e777 100644 --- a/src/test/smack/generics/generic_function.rs +++ b/src/test/smack/generics/generic_function.rs @@ -34,11 +34,11 @@ fn swapem>(s: U) -> U { } pub fn main() { - let x2 = rmc::nondet(); - let y2 = rmc::nondet(); - let x3 = rmc::nondet(); - let y3 = rmc::nondet(); - let z3 = rmc::nondet(); + let x2 = rmc::any(); + let y2 = rmc::any(); + let x3 = rmc::any(); + let y3 = rmc::any(); + let z3 = rmc::any(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function1.rs b/src/test/smack/generics/generic_function1.rs index eb39959a66c5..d43d4468ac0f 100644 --- a/src/test/smack/generics/generic_function1.rs +++ b/src/test/smack/generics/generic_function1.rs @@ -35,11 +35,11 @@ fn swapem>(s: U) -> U { } pub fn main() { - let x2 = rmc::nondet(); - let y2 = rmc::nondet(); - let x3 = rmc::nondet(); - let y3 = rmc::nondet(); - let z3 = rmc::nondet(); + let x2 = rmc::any(); + let y2 = rmc::any(); + let x3 = rmc::any(); + let y3 = rmc::any(); + let z3 = rmc::any(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function2.rs b/src/test/smack/generics/generic_function2.rs index 4ccb6b6582c6..aae67ad1ead0 100644 --- a/src/test/smack/generics/generic_function2.rs +++ b/src/test/smack/generics/generic_function2.rs @@ -35,11 +35,11 @@ fn swapem>(s: U) -> U { } pub fn main() { - let x2 = rmc::nondet(); - let y2 = rmc::nondet(); - let x3 = rmc::nondet(); - let y3 = rmc::nondet(); - let z3 = rmc::nondet(); + let x2 = rmc::any(); + let y2 = rmc::any(); + let x3 = rmc::any(); + let y3 = rmc::any(); + let z3 = rmc::any(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function3.rs b/src/test/smack/generics/generic_function3.rs index 4065966e0495..347aae041ff4 100644 --- a/src/test/smack/generics/generic_function3.rs +++ b/src/test/smack/generics/generic_function3.rs @@ -35,11 +35,11 @@ fn swapem>(s: U) -> U { } pub fn main() { - let x2 = rmc::nondet(); - let y2 = rmc::nondet(); - let x3 = rmc::nondet(); - let y3 = rmc::nondet(); - let z3 = rmc::nondet(); + let x2 = rmc::any(); + let y2 = rmc::any(); + let x3 = rmc::any(); + let y3 = rmc::any(); + let z3 = rmc::any(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function4.rs b/src/test/smack/generics/generic_function4.rs index c655cab54d6b..9e4be6c051d1 100644 --- a/src/test/smack/generics/generic_function4.rs +++ b/src/test/smack/generics/generic_function4.rs @@ -35,11 +35,11 @@ fn swapem>(s: U) -> U { } pub fn main() { - let x2 = rmc::nondet(); - let y2 = rmc::nondet(); - let x3 = rmc::nondet(); - let y3 = rmc::nondet(); - let z3 = rmc::nondet(); + let x2 = rmc::any(); + let y2 = rmc::any(); + let x3 = rmc::any(); + let y3 = rmc::any(); + let z3 = rmc::any(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function5.rs b/src/test/smack/generics/generic_function5.rs index 081c67e4cd81..233761844319 100644 --- a/src/test/smack/generics/generic_function5.rs +++ b/src/test/smack/generics/generic_function5.rs @@ -35,11 +35,11 @@ fn swapem>(s: U) -> U { } pub fn main() { - let x2 = rmc::nondet(); - let y2 = rmc::nondet(); - let x3 = rmc::nondet(); - let y3 = rmc::nondet(); - let z3 = rmc::nondet(); + let x2 = rmc::any(); + let y2 = rmc::any(); + let x3 = rmc::any(); + let y3 = rmc::any(); + let z3 = rmc::any(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/loops/gauss_sum_nondet.rs b/src/test/smack/loops/gauss_sum_nondet.rs index 006ec6f50df3..f40bb9bdbe66 100644 --- a/src/test/smack/loops/gauss_sum_nondet.rs +++ b/src/test/smack/loops/gauss_sum_nondet.rs @@ -6,7 +6,7 @@ pub fn main() { let mut sum = 0; - let b: u64 = rmc::nondet(); + let b: u64 = rmc::any(); if b < 5 && b > 1 { for i in 0..b { sum += i; diff --git a/src/test/smack/loops/gauss_sum_nondet_fail.rs b/src/test/smack/loops/gauss_sum_nondet_fail.rs index 216665b15fdc..72036b250894 100644 --- a/src/test/smack/loops/gauss_sum_nondet_fail.rs +++ b/src/test/smack/loops/gauss_sum_nondet_fail.rs @@ -7,7 +7,7 @@ pub fn main() { let mut sum = 0; - let b: u64 = rmc::nondet(); + let b: u64 = rmc::any(); if b < 5 && b > 1 { for i in 0..b { sum += i; diff --git a/src/test/smack/loops/iterator.rs b/src/test/smack/loops/iterator.rs index 387f81e4bcc5..8602b423bb96 100644 --- a/src/test/smack/loops/iterator.rs +++ b/src/test/smack/loops/iterator.rs @@ -15,7 +15,7 @@ fn fac(n: u64) -> u64 { pub fn main() { let mut a = 1; - let n = rmc::nondet(); + let n = rmc::any(); if n < 5 { for i in 1..n + 1 as u64 { a *= i; diff --git a/src/test/smack/loops/iterator_fail.rs b/src/test/smack/loops/iterator_fail.rs index 08fc810a53a4..b170fad1768c 100644 --- a/src/test/smack/loops/iterator_fail.rs +++ b/src/test/smack/loops/iterator_fail.rs @@ -15,7 +15,7 @@ fn fac(n: u64) -> u64 { pub fn main() { let mut a = 1; - let n = rmc::nondet(); + let n = rmc::any(); if n < 5 { for i in 1..n + 1 as u64 { a *= i; diff --git a/src/test/smack/structures/option.rs b/src/test/smack/structures/option.rs index 9a2ad11f39a4..4cd88c4cca83 100644 --- a/src/test/smack/structures/option.rs +++ b/src/test/smack/structures/option.rs @@ -7,7 +7,7 @@ fn safe_div(x: u32, y: u32) -> Option { } pub fn main() { - let x = rmc::nondet(); + let x = rmc::any(); if x > 0 && x <= 200 { // avoid overflow let a = safe_div(2 * x, x); @@ -15,7 +15,7 @@ pub fn main() { Some(c) => assert!(c == 2), None => assert!(false), }; - let y = rmc::nondet(); + let y = rmc::any(); if y > 0 { let b = safe_div(x, y); match b { diff --git a/src/test/smack/structures/option_fail.rs b/src/test/smack/structures/option_fail.rs index 1d204297aaa8..82b7b3eee97a 100644 --- a/src/test/smack/structures/option_fail.rs +++ b/src/test/smack/structures/option_fail.rs @@ -8,7 +8,7 @@ fn safe_div(x: u32, y: u32) -> Option { } pub fn main() { - let x = rmc::nondet(); + let x = rmc::any(); if x > 0 && x <= 100 { // avoid overflow let a = safe_div(2 * x, x); @@ -16,7 +16,7 @@ pub fn main() { Some(c) => assert!(c == 2), None => assert!(false), }; - let y = rmc::nondet(); + let y = rmc::any(); let b = safe_div(x, y); match b { Some(c) => assert!(c == x / y), diff --git a/src/test/smack/structures/point.rs b/src/test/smack/structures/point.rs index 1306df3d52d9..e92c090dd89d 100644 --- a/src/test/smack/structures/point.rs +++ b/src/test/smack/structures/point.rs @@ -37,10 +37,10 @@ impl AddAssign for Point { } pub fn main() { - let w = rmc::nondet(); - let x = rmc::nondet(); - let y = rmc::nondet(); - let z = rmc::nondet(); + let w = rmc::any(); + let x = rmc::any(); + let y = rmc::any(); + let z = rmc::any(); if w <= std::u64::MAX / 2 // avoid overflow && x <= std::u64::MAX / 2 // avoid overflow diff --git a/src/test/smack/structures/point_fail.rs b/src/test/smack/structures/point_fail.rs index 97204dc8d54d..4103c11220e2 100644 --- a/src/test/smack/structures/point_fail.rs +++ b/src/test/smack/structures/point_fail.rs @@ -38,10 +38,10 @@ impl AddAssign for Point { } pub fn main() { - let w = rmc::nondet(); - let x = rmc::nondet(); - let y = rmc::nondet(); - let z = rmc::nondet(); + let w = rmc::any(); + let x = rmc::any(); + let y = rmc::any(); + let z = rmc::any(); if w <= std::u64::MAX / 2 // avoid overflow && x <= std::u64::MAX / 2 // avoid overflow diff --git a/src/test/stub-tests/HashSet/concrete.rs b/src/test/stub-tests/HashSet/concrete.rs index b1000efb767a..6e92f345b9d0 100644 --- a/src/test/stub-tests/HashSet/concrete.rs +++ b/src/test/stub-tests/HashSet/concrete.rs @@ -8,9 +8,9 @@ fn main() { // TODO: This test should ideally work with nondeterminstic values but for // for the moment it does not. // - // let a: u16 = rmc::nondet(); - // let b: u16 = rmc::nondet(); - // let c: u16 = rmc::nondet(); + // let a: u16 = rmc::any(); + // let b: u16 = rmc::any(); + // let c: u16 = rmc::any(); // rmc::assume(a != b); // rmc::assume(a != c); // rmc::assume(b != c); diff --git a/src/test/stub-tests/HashSet/ignore-nondet.rs b/src/test/stub-tests/HashSet/ignore-nondet.rs index b2a6ec7faebd..6291620c7792 100644 --- a/src/test/stub-tests/HashSet/ignore-nondet.rs +++ b/src/test/stub-tests/HashSet/ignore-nondet.rs @@ -7,9 +7,9 @@ fn main() { // TODO: This test should ideally work with nondeterminstic values but for // for the moment it does not. - let a: u16 = rmc::nondet(); - let b: u16 = rmc::nondet(); - let c: u16 = rmc::nondet(); + let a: u16 = rmc::any(); + let b: u16 = rmc::any(); + let c: u16 = rmc::any(); rmc::assume(a != b); rmc::assume(a != c); rmc::assume(b != c);