From 36e4f390510309156251fa40c9d8200ae58020a9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Nov 2021 21:34:23 -0800 Subject: [PATCH 1/9] Mark rmc::nondet as unsafe (#607) The return value of rmc::nondet doesn't respect the invariant of a type. Until we have a better way to create symbolic variables, users must enforce the type invariant in their proof harness before using the value returned. --- library/rmc/src/lib.rs | 8 ++++---- .../kinds-of-failure/tests/bounds-check.rs | 4 ++-- .../tests/overflow-quicksort.rs | 4 ++-- .../kinds-of-failure/tests/overflow.rs | 4 ++-- .../src/tutorial/loops-unwinding/src/lib.rs | 2 +- .../src/tutorial/rmc-first-steps/src/lib.rs | 2 +- .../rmc-first-steps/tests/final-form.rs | 4 ++-- src/test/benchmarks/Vector/append.rs | 4 ++-- src/test/benchmarks/Vector/insert.rs | 6 +++--- src/test/benchmarks/Vector/push.rs | 2 +- src/test/benchmarks/Vector/push_and_pop.rs | 4 ++-- src/test/benchmarks/Vector/remove.rs | 4 ++-- src/test/benchmarks/Vector/shrink_and_clear.rs | 10 +++++----- src/test/cargo-rmc/dependencies/src/lib.rs | 2 +- .../cargo-rmc/simple-config-toml/src/lib.rs | 4 ++-- src/test/cargo-rmc/simple-extern/src/lib.rs | 2 +- src/test/cargo-rmc/simple-lib/src/lib.rs | 4 ++-- src/test/expected/closure/main.rs | 2 +- src/test/expected/closure3/main.rs | 2 +- src/test/expected/comp/main.rs | 4 ++-- src/test/expected/dynamic-error-trait/main.rs | 2 +- src/test/expected/nondet/main.rs | 2 +- src/test/expected/one-assert/test.rs | 3 ++- src/test/expected/unwind_tip/main.rs | 2 +- src/test/expected/vecdq/main.rs | 4 ++-- .../micro-http-parsed-request/ignore-main.rs | 2 +- .../virtio-balloon-compact/ignore-main.rs | 4 ++-- .../firecracker/virtio-block-parse/main.rs | 14 +++++++------- src/test/prusti/Binary_search.rs | 2 +- src/test/rmc/ArithEqualOperators/main.rs | 4 ++-- src/test/rmc/ArithOperators/main.rs | 2 +- src/test/rmc/Assume/main.rs | 2 +- src/test/rmc/Assume/main_fail.rs | 2 +- src/test/rmc/BinOp_Offset/main_fail.rs | 4 ++-- src/test/rmc/BitwiseArithOperators/bool.rs | 4 ++-- src/test/rmc/BitwiseArithOperators/main.rs | 4 ++-- src/test/rmc/BitwiseEqualOperators/main.rs | 4 ++-- src/test/rmc/Bool-BoolOperators/main.rs | 2 +- src/test/rmc/Cast/from_be_bytes.rs | 16 ++++++++-------- src/test/rmc/DynTrait/drop_boxed_dyn.rs | 2 +- src/test/rmc/DynTrait/main.rs | 2 +- src/test/rmc/DynTrait/main_fail.rs | 2 +- src/test/rmc/EQ-NE/main.rs | 2 +- src/test/rmc/Enum/result3.rs | 4 ++-- src/test/rmc/FloatingPoint/main.rs | 2 +- .../rmc/FunctionAbstractions/mem_replace.rs | 4 ++-- src/test/rmc/FunctionAbstractions/mem_swap.rs | 4 ++-- src/test/rmc/FunctionCall_Ret-NoParam/main.rs | 10 +++++----- src/test/rmc/FunctionCall_Ret-Param/main.rs | 2 +- src/test/rmc/IfElseifElse_NonReturning/main.rs | 2 +- src/test/rmc/IfElseifElse_Returning/main.rs | 4 ++-- src/test/rmc/LT-GT-LE-GE/main.rs | 2 +- src/test/rmc/LoopLoop_NonReturning/main.rs | 2 +- .../main_no_unwind_asserts.rs | 2 +- src/test/rmc/LoopWhile_NonReturning/main.rs | 2 +- .../main_no_unwind_asserts.rs | 2 +- src/test/rmc/Never/never_return.rs | 2 +- src/test/rmc/NondetVectors/bytes.rs | 18 +++++++++--------- src/test/rmc/NondetVectors/fixme_main.rs | 6 +++--- src/test/rmc/Pointers_OtherTypes/main.rs | 2 +- src/test/rmc/SaturatingIntrinsics/add_128.rs | 4 ++-- src/test/rmc/SaturatingIntrinsics/main.rs | 4 ++-- src/test/rmc/Scopes_NonReturning/main.rs | 2 +- src/test/rmc/Scopes_Returning/main.rs | 4 ++-- src/test/rmc/i32-Unary-/main.rs | 2 +- src/test/serial/serial.rs | 12 ++++++------ src/test/serial/serial2.rs | 6 +++--- src/test/serial/serial_spec.rs | 6 +++--- src/test/smack/basic/arith_assume.rs | 4 ++-- src/test/smack/basic/arith_assume2.rs | 4 ++-- src/test/smack/basic/arith_assume3.rs | 4 ++-- src/test/smack/functions/closure.rs | 2 +- src/test/smack/functions/closure_fail.rs | 2 +- src/test/smack/functions/double.rs | 2 +- src/test/smack/functions/double_fail.rs | 2 +- src/test/smack/generics/generic_function.rs | 10 +++++----- src/test/smack/generics/generic_function1.rs | 10 +++++----- src/test/smack/generics/generic_function2.rs | 10 +++++----- src/test/smack/generics/generic_function3.rs | 10 +++++----- src/test/smack/generics/generic_function4.rs | 10 +++++----- src/test/smack/generics/generic_function5.rs | 10 +++++----- src/test/smack/loops/gauss_sum_nondet.rs | 2 +- src/test/smack/loops/gauss_sum_nondet_fail.rs | 2 +- src/test/smack/loops/iterator.rs | 2 +- src/test/smack/loops/iterator_fail.rs | 2 +- src/test/smack/structures/option.rs | 4 ++-- src/test/smack/structures/option_fail.rs | 4 ++-- src/test/smack/structures/point.rs | 8 ++++---- src/test/smack/structures/point_fail.rs | 8 ++++---- src/test/stub-tests/HashSet/concrete.rs | 6 +++--- src/test/stub-tests/HashSet/ignore-nondet.rs | 6 +++--- 91 files changed, 200 insertions(+), 199 deletions(-) diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs index 4c7acf68f766..67e1381404ba 100644 --- a/library/rmc/src/lib.rs +++ b/library/rmc/src/lib.rs @@ -13,7 +13,7 @@ pub mod slice; /// The code snippet below should never panic. /// /// ```rust -/// let i : i32 = rmc::nondet(); +/// let i : i32 = unsafe { rmc::nondet() }; /// rmc::assume(i > 10); /// if i < 0 { /// panic!("This will never panic"); @@ -23,7 +23,7 @@ pub mod slice; /// The following code may panic though: /// /// ```rust -/// let i : i32 = rmc::nondet(); +/// let i : i32 = unsafe { rmc::nondet() }; /// assert!(i < 0, "This may panic and verification should fail."); /// rmc::assume(i > 10); /// ``` @@ -40,12 +40,12 @@ pub fn assume(_cond: bool) {} /// under all possible i32 input values. /// /// ```rust -/// let inputA = rmc::nondet::(); +/// let inputA = unsafe { rmc::nondet::() }; /// fn_under_verification(inputA); /// ``` #[inline(never)] #[rustc_diagnostic_item = "RmcNonDet"] -pub fn nondet() -> T { +pub unsafe fn nondet() -> T { unimplemented!("RMC nondet") } 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..cbd61a8e8702 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 = unsafe { rmc::nondet() }; rmc::assume(size < 4096); - let index: usize = rmc::nondet(); + let index: usize = unsafe { rmc::nondet() }; 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..0f3c1dc32145 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 = unsafe { rmc::nondet() }; + let b: u32 = unsafe { rmc::nondet() }; 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..e8d3a0f2a535 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 = unsafe { rmc::nondet() }; + let b: u32 = unsafe { rmc::nondet() }; 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..1e844da1f7dd 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 = unsafe { rmc::nondet() }; 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..8a7c6a9ddd87 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 = unsafe { rmc::nondet() }; 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..7b3a667711fb 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 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; let y = estimate_size(x); } diff --git a/src/test/benchmarks/Vector/append.rs b/src/test/benchmarks/Vector/append.rs index 8d6b70d4c4e3..6d05512f7f02 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(unsafe { rmc::nondet() }); } let mut v2: Vec = Vec::with_capacity(times); for i in 0..times { - v2.push(rmc::nondet()); + v2.push(unsafe { rmc::nondet() }); } 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..79e02e7f9b12 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(unsafe { rmc::nondet() }); } - let sentinel = rmc::nondet(); + let sentinel = unsafe { rmc::nondet() }; v.push(sentinel); - v.insert(v.len()/2, rmc::nondet()); + v.insert(v.len()/2, unsafe { rmc::nondet() }); assert!(v.pop() == Some(sentinel)); } diff --git a/src/test/benchmarks/Vector/push.rs b/src/test/benchmarks/Vector/push.rs index 880914b4b8b8..d69b2370f431 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(unsafe { rmc::nondet() }); } } diff --git a/src/test/benchmarks/Vector/push_and_pop.rs b/src/test/benchmarks/Vector/push_and_pop.rs index 5a5a941facff..357dbe1222aa 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(unsafe { rmc::nondet() }); } 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(unsafe { rmc::nondet() }); } 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..736d3e51a757 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(unsafe { rmc::nondet() }); } - let sentinel = rmc::nondet(); + let sentinel = unsafe { rmc::nondet() }; 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..d060422b0ad3 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(unsafe { rmc::nondet() }); } assert!(v.len() == times); // Here, Vecs with grow() internally - let i: usize = rmc::nondet(); + let i: usize = unsafe { rmc::nondet() }; 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(unsafe { rmc::nondet() }); } // Drop all elements in the Vec v.clear(); // Add some more new elements for i in 0..times { - v.push(rmc::nondet()); + v.push(unsafe { rmc::nondet() }); } // Assert! - let sentinel = rmc::nondet(); + let sentinel = unsafe { rmc::nondet() }; 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..12124928f820 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 = unsafe { rmc::nondet::() }; 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..cc27a0114345 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 = unsafe { rmc::nondet() }; + let b: u64 = unsafe { rmc::nondet() }; 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..bd11980717f2 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 = unsafe { rmc::nondet() }; 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..cc27a0114345 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 = unsafe { rmc::nondet() }; + let b: u64 = unsafe { rmc::nondet() }; 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..35ebe8deec77 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 = unsafe { rmc::nondet() }; 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..38f81746a2a7 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 = unsafe { rmc::nondet() }; 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..5ec03133bf18 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 = unsafe { rmc::nondet() }; + let b = unsafe { rmc::nondet() }; 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..0807d223b841 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 unsafe { rmc::nondet() } { 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..6de5a71b79c6 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 = unsafe { rmc::nondet() }; 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/test.rs b/src/test/expected/one-assert/test.rs index 144392c29dbf..f19c854a6bd2 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 = unsafe { rmc::nondet() }; 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..35d8a8d8d723 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 = unsafe { rmc::nondet() }; if a < 1024 { loop { diff --git a/src/test/expected/vecdq/main.rs b/src/test/expected/vecdq/main.rs index 0e7d7f7ed3df..4afe1a45ebf3 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 = unsafe { rmc::nondet() }; + let y = unsafe { rmc::nondet() }; 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..30f51f217e7a 100644 --- a/src/test/firecracker/micro-http-parsed-request/ignore-main.rs +++ b/src/test/firecracker/micro-http-parsed-request/ignore-main.rs @@ -24,7 +24,7 @@ fn fix(n: u32) { } fn main() { - let n: u32 = rmc::nondet(); + let n: u32 = unsafe { rmc::nondet() }; 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..cc0155bb2660 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] = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; 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..9ff60d85452d 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -23,7 +23,7 @@ pub struct GuestMemoryMmap {} impl GuestMemoryMmap { fn checked_offset(&self, base: GuestAddress, offset: usize) -> Option { let mut retval = None; - if rmc::nondet() { + if unsafe { rmc::nondet() } { if let Some(sum) = base.0.checked_add(offset as u64) { retval = Some(GuestAddress(sum)) } @@ -42,15 +42,15 @@ impl GuestMemoryMmap { if let Some(prev_addr) = TRACK_READ_OBJ { assert!(prev_addr.0 != addr.0); } - if rmc::nondet() && TRACK_READ_OBJ.is_none() { + if unsafe { rmc::nondet() && TRACK_READ_OBJ.is_none() } { TRACK_READ_OBJ = Some(addr); } } - rmc::nondet() + unsafe { rmc::nondet() } } fn read_obj_request_header(&self, addr: GuestAddress) -> Result { - rmc::nondet() + unsafe { rmc::nondet() } } } @@ -317,12 +317,12 @@ fn is_nonzero_pow2(x: u16) -> bool { fn main() { let mem = GuestMemoryMmap {}; - let queue_size: u16 = rmc::nondet(); + let queue_size: u16 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; + let desc_table = GuestAddress(unsafe { rmc::nondet::() } & 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..db0b1273f65a 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 = unsafe { rmc::nondet() }; 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..74c9ab33e33d 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 = unsafe { rmc::nondet() }; a /= 2; - let mut b: u32 = rmc::nondet(); + let mut b: u32 = unsafe { rmc::nondet() }; 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..713059a3d0c0 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 = unsafe { rmc::nondet() }; 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..fc8bb71cf2a5 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 = unsafe { unsafe { rmc::nondet() } }; 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..66b9ea64a58b 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 = unsafe { rmc::nondet() }; 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..431a13481813 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] = [[unsafe { rmc::nondet::() }]]; + table[0][unsafe { rmc::nondet::() }]; // EXPCECTED FAIL } fn main() { diff --git a/src/test/rmc/BitwiseArithOperators/bool.rs b/src/test/rmc/BitwiseArithOperators/bool.rs index f5311d95898b..9771934e77ef 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 = unsafe { rmc::nondet() }; + let b: bool = unsafe { rmc::nondet() }; 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..7c2b749daf83 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 = unsafe { rmc::nondet() }; + let b: u32 = unsafe { rmc::nondet() }; 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..d4cc4c69c47c 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 = unsafe { rmc::nondet() }; a %= 8; - let mut b: u32 = rmc::nondet(); + let mut b: u32 = unsafe { rmc::nondet() }; 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..011bb86e576b 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 = unsafe { rmc::nondet() }; 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..e3a4bbb08a90 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(), + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, ]; 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..d64d938aa493 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 unsafe { rmc::nondet() } { 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..34e02a7b5619 100644 --- a/src/test/rmc/DynTrait/main.rs +++ b/src/test/rmc/DynTrait/main.rs @@ -34,7 +34,7 @@ fn random_animal(random_number: i64) -> Box { } fn main() { - let random_number = rmc::nondet(); + let random_number = unsafe { rmc::nondet() }; 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..e1d6e3620080 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 = unsafe { rmc::nondet() }; 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..5024f1d649a4 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 = unsafe { rmc::nondet() }; 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..da7c7e9ffec1 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::nondet() }; 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 unsafe { rmc::nondet() } { 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..af9ab222da00 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 = unsafe { rmc::nondet() }; 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..821a6b92ab7f 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 = unsafe { rmc::nondet::() }; + let mut var2 = unsafe { rmc::nondet::() }; 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..f74f494c10c2 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 = unsafe { rmc::nondet::() }; + let mut var2 = unsafe { rmc::nondet::() }; 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..58fe54c0ee6b 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 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; 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..57d2687a2164 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 = unsafe { rmc::nondet() }; 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..76eea0a91ab6 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 = unsafe { rmc::nondet() }; 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..fb25bcc0cbef 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 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; let d = if c > 100 { c diff --git a/src/test/rmc/LT-GT-LE-GE/main.rs b/src/test/rmc/LT-GT-LE-GE/main.rs index b29d66d9520a..a201e5b6c1a0 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 = unsafe { rmc::nondet() }; 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..db150f3548bf 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 = unsafe { rmc::nondet() }; 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..31009aed705f 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 = unsafe { rmc::nondet() }; if a < 1024 { loop { diff --git a/src/test/rmc/LoopWhile_NonReturning/main.rs b/src/test/rmc/LoopWhile_NonReturning/main.rs index 85dc4bc2772d..25ab9276b8a5 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 = unsafe { rmc::nondet() }; 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..f88062ac1558 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 = unsafe { rmc::nondet() }; 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..df7ba852a994 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 = unsafe { rmc::nondet::() }; if var > 0 { err(); } diff --git a/src/test/rmc/NondetVectors/bytes.rs b/src/test/rmc/NondetVectors/bytes.rs index ac819897ccd5..8458071e540b 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(), + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, + unsafe { rmc::nondet() }, ]; 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 = unsafe { rmc::nondet() }; 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..9d67e6ab236a 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 = unsafe { rmc::nondet() }; if !(len <= FIFO_SIZE) { return; } let _buf1: Vec = vec![0u8; len]; //< this works - let elt: u8 = rmc::nondet(); + let elt: u8 = unsafe { rmc::nondet() }; let _buf2: Vec = vec![elt; len]; //< this fails: "memset destination region writeable" - let idx: usize = rmc::nondet(); + let idx: usize = unsafe { rmc::nondet() }; 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..5e8e2f3cbe25 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 = unsafe { rmc::nondet() }; 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..3987da8c947c 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 = unsafe { rmc::nondet() }; + let w: u128 = unsafe { rmc::nondet() }; intrinsics::saturating_add(v, w); } diff --git a/src/test/rmc/SaturatingIntrinsics/main.rs b/src/test/rmc/SaturatingIntrinsics/main.rs index 31fa51b78d45..176170932a1a 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 = unsafe { rmc::nondet() }; + let w: $ty = unsafe { rmc::nondet() }; 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..63afc266da27 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 = unsafe { rmc::nondet() }; 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..fa1ecff49ac7 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 = unsafe { rmc::nondet() }; let e = { let f: u32; @@ -32,7 +32,7 @@ fn main() { }; assert!(e == d || e == 10); - let g: u32 = rmc::nondet(); + let g: u32 = unsafe { rmc::nondet() }; 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..a90d6f20fdf6 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 = unsafe { rmc::nondet() }; if -100000 < a && a < 100000 { let b = -a; diff --git a/src/test/serial/serial.rs b/src/test/serial/serial.rs index 230ce94db0ca..0d82779672a4 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 = unsafe { rmc::nondet() }; + let b: u8 = unsafe { rmc::nondet() }; + let c: u8 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; + // let b: u8 = unsafe { rmc::nondet() }; + // let c: u8 = unsafe { rmc::nondet() }; // // 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..e04d69e9b91a 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 = unsafe { rmc::nondet() }; + let b: u8 = unsafe { rmc::nondet() }; + let c: u8 = unsafe { rmc::nondet() }; // 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..1d0a8f5bcc28 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 = unsafe { rmc::nondet() }; + let b: u8 = unsafe { rmc::nondet() }; + let c: u8 = unsafe { rmc::nondet() }; 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..bd95af5d20d7 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 = unsafe { rmc::nondet() }; + let b = unsafe { rmc::nondet() }; 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..bd95af5d20d7 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 = unsafe { rmc::nondet() }; + let b = unsafe { rmc::nondet() }; 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..97b80765cb85 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 = unsafe { rmc::nondet() }; + let b = unsafe { rmc::nondet() }; 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..938d43c8918b 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 = unsafe { rmc::nondet() }; 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..8d4a6e8e2915 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 = unsafe { rmc::nondet() }; 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..2911ef890496 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 = unsafe { rmc::nondet() }; 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..1019256e089f 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 = unsafe { rmc::nondet() }; 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..8a49533a0d21 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 = unsafe { rmc::nondet() }; + let y2 = unsafe { rmc::nondet() }; + let x3 = unsafe { rmc::nondet() }; + let y3 = unsafe { rmc::nondet() }; + let z3 = unsafe { rmc::nondet() }; 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..eb620a3ffb82 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 = unsafe { rmc::nondet() }; + let y2 = unsafe { rmc::nondet() }; + let x3 = unsafe { rmc::nondet() }; + let y3 = unsafe { rmc::nondet() }; + let z3 = unsafe { rmc::nondet() }; 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..f3a56a806c28 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 = unsafe { rmc::nondet() }; + let y2 = unsafe { rmc::nondet() }; + let x3 = unsafe { rmc::nondet() }; + let y3 = unsafe { rmc::nondet() }; + let z3 = unsafe { rmc::nondet() }; 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..31e5e3d27995 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 = unsafe { rmc::nondet() }; + let y2 = unsafe { rmc::nondet() }; + let x3 = unsafe { rmc::nondet() }; + let y3 = unsafe { rmc::nondet() }; + let z3 = unsafe { rmc::nondet() }; 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..53038d2fb003 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 = unsafe { rmc::nondet() }; + let y2 = unsafe { rmc::nondet() }; + let x3 = unsafe { rmc::nondet() }; + let y3 = unsafe { rmc::nondet() }; + let z3 = unsafe { rmc::nondet() }; 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..1747aa0a9747 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 = unsafe { rmc::nondet() }; + let y2 = unsafe { rmc::nondet() }; + let x3 = unsafe { rmc::nondet() }; + let y3 = unsafe { rmc::nondet() }; + let z3 = unsafe { rmc::nondet() }; 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..0b0e589236dc 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 = unsafe { rmc::nondet() }; 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..af8f7b9a8eed 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 = unsafe { rmc::nondet() }; 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..42cf6770369a 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 = unsafe { rmc::nondet() }; 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..9ed0eed906e8 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 = unsafe { rmc::nondet() }; 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..460e3c927f79 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 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; 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..d7412cdacb59 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 = unsafe { rmc::nondet() }; 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 = unsafe { rmc::nondet() }; 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..dc69ac475e16 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 = unsafe { rmc::nondet() }; + let x = unsafe { rmc::nondet() }; + let y = unsafe { rmc::nondet() }; + let z = unsafe { rmc::nondet() }; 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..d17ff1a3b08e 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 = unsafe { rmc::nondet() }; + let x = unsafe { rmc::nondet() }; + let y = unsafe { rmc::nondet() }; + let z = unsafe { rmc::nondet() }; 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..cc25fed89485 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 = unsafe { rmc::nondet() }; + // let b: u16 = unsafe { rmc::nondet() }; + // let c: u16 = unsafe { rmc::nondet() }; // 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..111f0533312a 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 = unsafe { rmc::nondet() }; + let b: u16 = unsafe { rmc::nondet() }; + let c: u16 = unsafe { rmc::nondet() }; rmc::assume(a != b); rmc::assume(a != c); rmc::assume(b != c); From ad41274712d155b98685baafbe24b0e9577a0163 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Nov 2021 21:40:59 -0800 Subject: [PATCH 2/9] Introduce rmc::any and rmc::any_raw We decided to replace the old method rmc::nondet because its behavior wasn't clear. For some types it would respect the type invariants but not for others. Additionally, there was no way for the user to specify how to create safe non-deterministic values. --- library/rmc/src/invariants.rs | 113 ++++++++++++++++++ library/rmc/src/lib.rs | 32 ++++- rmc-docs/src/tutorial-first-steps.md | 2 +- rmc-docs/src/tutorial-kinds-of-failure.md | 12 +- .../kinds-of-failure/tests/bounds-check.rs | 4 +- .../tests/overflow-quicksort.rs | 4 +- .../kinds-of-failure/tests/overflow.rs | 4 +- .../src/tutorial/loops-unwinding/src/lib.rs | 2 +- .../src/tutorial/rmc-first-steps/src/lib.rs | 2 +- .../rmc-first-steps/tests/final-form.rs | 4 +- src/test/benchmarks/Vector/append.rs | 4 +- src/test/benchmarks/Vector/insert.rs | 6 +- src/test/benchmarks/Vector/push.rs | 2 +- src/test/benchmarks/Vector/push_and_pop.rs | 4 +- src/test/benchmarks/Vector/remove.rs | 4 +- .../benchmarks/Vector/shrink_and_clear.rs | 10 +- src/test/cargo-rmc/dependencies/src/lib.rs | 2 +- .../cargo-rmc/simple-config-toml/src/lib.rs | 4 +- src/test/cargo-rmc/simple-extern/src/lib.rs | 2 +- src/test/cargo-rmc/simple-lib/src/lib.rs | 4 +- src/test/expected/closure/main.rs | 2 +- src/test/expected/closure3/main.rs | 2 +- src/test/expected/comp/main.rs | 4 +- src/test/expected/dynamic-error-trait/main.rs | 2 +- src/test/expected/nondet/main.rs | 2 +- src/test/expected/one-assert/expected | 2 +- src/test/expected/one-assert/test.rs | 2 +- src/test/expected/unwind_tip/main.rs | 2 +- src/test/expected/vecdq/main.rs | 4 +- .../micro-http-parsed-request/ignore-main.rs | 8 +- .../virtio-balloon-compact/ignore-main.rs | 4 +- .../firecracker/virtio-block-parse/main.rs | 16 +-- src/test/prusti/Binary_search.rs | 2 +- src/test/rmc/ArithEqualOperators/main.rs | 4 +- src/test/rmc/ArithOperators/main.rs | 2 +- src/test/rmc/Assume/main.rs | 2 +- src/test/rmc/Assume/main_fail.rs | 2 +- src/test/rmc/BinOp_Offset/main_fail.rs | 4 +- src/test/rmc/BitwiseArithOperators/bool.rs | 4 +- src/test/rmc/BitwiseArithOperators/main.rs | 4 +- src/test/rmc/BitwiseEqualOperators/main.rs | 4 +- src/test/rmc/Bool-BoolOperators/main.rs | 2 +- src/test/rmc/Cast/from_be_bytes.rs | 16 +-- src/test/rmc/DynTrait/drop_boxed_dyn.rs | 2 +- src/test/rmc/DynTrait/main.rs | 9 +- src/test/rmc/DynTrait/main_fail.rs | 2 +- src/test/rmc/EQ-NE/main.rs | 2 +- src/test/rmc/Enum/result3.rs | 4 +- src/test/rmc/FloatingPoint/main.rs | 2 +- .../rmc/FunctionAbstractions/mem_replace.rs | 4 +- src/test/rmc/FunctionAbstractions/mem_swap.rs | 4 +- src/test/rmc/FunctionCall_Ret-NoParam/main.rs | 10 +- src/test/rmc/FunctionCall_Ret-Param/main.rs | 2 +- .../rmc/IfElseifElse_NonReturning/main.rs | 2 +- src/test/rmc/IfElseifElse_Returning/main.rs | 4 +- src/test/rmc/LT-GT-LE-GE/main.rs | 2 +- src/test/rmc/LoopLoop_NonReturning/main.rs | 2 +- .../main_no_unwind_asserts.rs | 2 +- src/test/rmc/LoopWhile_NonReturning/main.rs | 2 +- .../main_no_unwind_asserts.rs | 2 +- src/test/rmc/Never/never_return.rs | 2 +- src/test/rmc/NondetVectors/bytes.rs | 18 +-- src/test/rmc/NondetVectors/fixme_main.rs | 6 +- src/test/rmc/Pointers_OtherTypes/main.rs | 2 +- src/test/rmc/SaturatingIntrinsics/add_128.rs | 4 +- src/test/rmc/SaturatingIntrinsics/main.rs | 4 +- src/test/rmc/Scopes_NonReturning/main.rs | 2 +- src/test/rmc/Scopes_Returning/main.rs | 4 +- src/test/rmc/i32-Unary-/main.rs | 2 +- src/test/serial/serial.rs | 12 +- src/test/serial/serial2.rs | 6 +- src/test/serial/serial_spec.rs | 6 +- src/test/smack/basic/arith_assume.rs | 4 +- src/test/smack/basic/arith_assume2.rs | 4 +- src/test/smack/basic/arith_assume3.rs | 4 +- src/test/smack/functions/closure.rs | 2 +- src/test/smack/functions/closure_fail.rs | 2 +- src/test/smack/functions/double.rs | 2 +- src/test/smack/functions/double_fail.rs | 2 +- src/test/smack/generics/generic_function.rs | 10 +- src/test/smack/generics/generic_function1.rs | 10 +- src/test/smack/generics/generic_function2.rs | 10 +- src/test/smack/generics/generic_function3.rs | 10 +- src/test/smack/generics/generic_function4.rs | 10 +- src/test/smack/generics/generic_function5.rs | 10 +- src/test/smack/loops/gauss_sum_nondet.rs | 2 +- src/test/smack/loops/gauss_sum_nondet_fail.rs | 2 +- src/test/smack/loops/iterator.rs | 2 +- src/test/smack/loops/iterator_fail.rs | 2 +- src/test/smack/structures/option.rs | 4 +- src/test/smack/structures/option_fail.rs | 4 +- src/test/smack/structures/point.rs | 8 +- src/test/smack/structures/point_fail.rs | 8 +- src/test/stub-tests/HashSet/concrete.rs | 6 +- src/test/stub-tests/HashSet/ignore-nondet.rs | 6 +- 95 files changed, 349 insertions(+), 217 deletions(-) create mode 100644 library/rmc/src/invariants.rs diff --git a/library/rmc/src/invariants.rs b/library/rmc/src/invariants.rs new file mode 100644 index 000000000000..22d700f8ea39 --- /dev/null +++ b/library/rmc/src/invariants.rs @@ -0,0 +1,113 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// This module introduces the Invariant trait and as well as implementation for commonly used types. + +/// 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. +pub trait Invariant { + fn is_valid(&self) -> bool; +} + +impl Invariant for bool { + #[inline(always)] + fn is_valid(&self) -> bool { + let byte = u8::from(*self); + byte == 0 || byte == 1 + } +} + +impl Invariant for u8 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for u16 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for u32 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for u64 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for u128 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for usize { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for i8 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for i16 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for i32 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for i64 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for i128 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +impl Invariant for isize { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +/// Verifies that: +/// - a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] +/// Ref: https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html +impl Invariant for char { + #[inline(always)] + fn is_valid(&self) -> bool { + let val = *self as u32; + val <= 0xD7FF || (val >= 0xE000 && val <= 0x10FFFF) + } +} diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs index 67e1381404ba..c247495a7b15 100644 --- a/library/rmc/src/lib.rs +++ b/library/rmc/src/lib.rs @@ -3,6 +3,9 @@ #![feature(rustc_attrs)] // Used for rustc_diagnostic_item. pub mod slice; +mod invariants; + +use invariants::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 @@ -31,7 +34,7 @@ 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: @@ -40,12 +43,33 @@ pub fn assume(_cond: bool) {} /// under all possible i32 input values. /// /// ```rust -/// let inputA = unsafe { 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 `Invariant` +/// trait. The invariant trait is used to constraint the result to ensure the value is valid. +#[inline(always)] +pub fn any() -> T { + let value = unsafe { any_raw::() }; + assume(value.is_valid()); + value +} + +/// 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 = rmc::any_raw::(); /// fn_under_verification(inputA); /// ``` -#[inline(never)] #[rustc_diagnostic_item = "RmcNonDet"] -pub unsafe fn nondet() -> T { +#[inline(never)] +pub unsafe fn any_raw() -> T { unimplemented!("RMC nondet") } 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 cbd61a8e8702..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 = unsafe { rmc::nondet() }; + let size: usize = rmc::any(); rmc::assume(size < 4096); - let index: usize = unsafe { 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 0f3c1dc32145..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 = unsafe { rmc::nondet() }; - let b: u32 = unsafe { 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 e8d3a0f2a535..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 = unsafe { rmc::nondet() }; - let b: u32 = unsafe { 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 1e844da1f7dd..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 = unsafe { 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 8a7c6a9ddd87..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 = unsafe { 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 7b3a667711fb..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 = unsafe { 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 = unsafe { rmc::nondet() }; + let x: u32 = rmc::any(); let y = estimate_size(x); } diff --git a/src/test/benchmarks/Vector/append.rs b/src/test/benchmarks/Vector/append.rs index 6d05512f7f02..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(unsafe { rmc::nondet() }); + v.push(rmc::any()); } let mut v2: Vec = Vec::with_capacity(times); for i in 0..times { - v2.push(unsafe { 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 79e02e7f9b12..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(unsafe { rmc::nondet() }); + v.push(rmc::any()); } - let sentinel = unsafe { rmc::nondet() }; + let sentinel = rmc::any(); v.push(sentinel); - v.insert(v.len()/2, unsafe { 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 d69b2370f431..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(unsafe { 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 357dbe1222aa..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(unsafe { 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(unsafe { 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 736d3e51a757..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(unsafe { rmc::nondet() }); + v.push(rmc::any()); } - let sentinel = unsafe { 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 d060422b0ad3..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(unsafe { rmc::nondet() }); + v.push(rmc::any()); } assert!(v.len() == times); // Here, Vecs with grow() internally - let i: usize = unsafe { 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(unsafe { 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(unsafe { rmc::nondet() }); + v.push(rmc::any()); } // Assert! - let sentinel = unsafe { 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 12124928f820..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 = unsafe { 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 cc27a0114345..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 = unsafe { rmc::nondet() }; - let b: u64 = unsafe { 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 bd11980717f2..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 = unsafe { 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 cc27a0114345..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 = unsafe { rmc::nondet() }; - let b: u64 = unsafe { 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 35ebe8deec77..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 = unsafe { 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 38f81746a2a7..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 = unsafe { 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 5ec03133bf18..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 = unsafe { rmc::nondet() }; - let b = unsafe { 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 0807d223b841..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 unsafe { 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 6de5a71b79c6..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 = unsafe { 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 f19c854a6bd2..9b55d093c869 100644 --- a/src/test/expected/one-assert/test.rs +++ b/src/test/expected/one-assert/test.rs @@ -5,7 +5,7 @@ // compile-flags: --crate-type lib #[no_mangle] pub fn check_assert() { - let x: u8 = unsafe { 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 35d8a8d8d723..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 = unsafe { 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 4afe1a45ebf3..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 = unsafe { rmc::nondet() }; - let y = unsafe { 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 30f51f217e7a..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 = unsafe { 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 cc0155bb2660..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] = unsafe { 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 = unsafe { 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 9ff60d85452d..738fc4ba6484 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -23,7 +23,7 @@ pub struct GuestMemoryMmap {} impl GuestMemoryMmap { fn checked_offset(&self, base: GuestAddress, offset: usize) -> Option { let mut retval = None; - if unsafe { rmc::nondet() } { + if rmc::any() { if let Some(sum) = base.0.checked_add(offset as u64) { retval = Some(GuestAddress(sum)) } @@ -31,7 +31,7 @@ impl GuestMemoryMmap { unsafe { if retval.is_none() && !TRACK_CHECKED_OFFSET_NONE { TRACK_CHECKED_OFFSET_NONE = true; - } + } } return retval; } @@ -42,15 +42,15 @@ impl GuestMemoryMmap { if let Some(prev_addr) = TRACK_READ_OBJ { assert!(prev_addr.0 != addr.0); } - if unsafe { rmc::nondet() && TRACK_READ_OBJ.is_none() } { + if rmc::any() && TRACK_READ_OBJ.is_none() { TRACK_READ_OBJ = Some(addr); } } - unsafe { rmc::nondet() } + unsafe { rmc::any_raw() } } fn read_obj_request_header(&self, addr: GuestAddress) -> Result { - unsafe { rmc::nondet() } + unsafe { rmc::any_raw() } } } @@ -317,12 +317,12 @@ fn is_nonzero_pow2(x: u16) -> bool { fn main() { let mem = GuestMemoryMmap {}; - let queue_size: u16 = unsafe { rmc::nondet() }; + let queue_size: u16 = rmc::any(); if !is_nonzero_pow2(queue_size) { return; } - let index: u16 = unsafe { rmc::nondet() }; - let desc_table = GuestAddress(unsafe { 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 db0b1273f65a..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 = unsafe { 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 74c9ab33e33d..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 = unsafe { rmc::nondet() }; + let mut a: u32 = rmc::any(); a /= 2; - let mut b: u32 = unsafe { 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 713059a3d0c0..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 = unsafe { 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 fc8bb71cf2a5..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 = unsafe { unsafe { 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 66b9ea64a58b..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 = unsafe { 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 431a13481813..7840f141b5e9 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] = [[unsafe { rmc::nondet::() }]]; - table[0][unsafe { rmc::nondet::() }]; // EXPCECTED FAIL + let table: [[u64; 1]; 1] = [[rmc::any::()]]; + table[0][rmc::any::()]; // EXPCECTED FAIL } fn main() { diff --git a/src/test/rmc/BitwiseArithOperators/bool.rs b/src/test/rmc/BitwiseArithOperators/bool.rs index 9771934e77ef..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 = unsafe { rmc::nondet() }; - let b: bool = unsafe { 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 7c2b749daf83..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 = unsafe { rmc::nondet() }; - let b: u32 = unsafe { 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 d4cc4c69c47c..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 = unsafe { rmc::nondet() }; + let mut a: u32 = rmc::any(); a %= 8; - let mut b: u32 = unsafe { 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 011bb86e576b..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 = unsafe { 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 e3a4bbb08a90..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![ - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { 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 d64d938aa493..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 unsafe { 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 34e02a7b5619..17c46da445c4 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,10 +29,10 @@ fn random_animal(random_number: i64) -> Box { } fn main() { - let random_number = unsafe { rmc::nondet() }; + let random_number = rmc::any(); let animal = random_animal(random_number); let s = animal.noise(); - if random_number < 5 { + if (random_number < 5) { assert!(s == 1); } else { assert!(s == 2); diff --git a/src/test/rmc/DynTrait/main_fail.rs b/src/test/rmc/DynTrait/main_fail.rs index e1d6e3620080..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 = unsafe { 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 5024f1d649a4..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 = unsafe { 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 da7c7e9ffec1..f6a28391df84 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 = unsafe { rmc::nondet() }; + let input: Result = unsafe { rmc::any_raw() }; let x = foo(&input); assert!(x == 3 || input != Err(Unit::Unit)); - let input: Result = if unsafe { rmc::nondet() } { Ok(0) } else { Err(Unit::Unit) }; + let input: Result = if unsafe { rmc::any_raw() } { 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 af9ab222da00..8237aa76c7a7 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 = unsafe { rmc::nondet() }; + let a: $ty = unsafe { rmc::any_raw() }; 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 821a6b92ab7f..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 = unsafe { rmc::nondet::() }; - let mut var2 = unsafe { 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 f74f494c10c2..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 = unsafe { rmc::nondet::() }; - let mut var2 = unsafe { 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 58fe54c0ee6b..372e205434b9 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 = unsafe { 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 = unsafe { 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 = unsafe { 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 = unsafe { 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 = unsafe { rmc::nondet() }; + let x: f64 = unsafe { rmc::any_raw() }; 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 57d2687a2164..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 = unsafe { 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 76eea0a91ab6..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 = unsafe { 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 fb25bcc0cbef..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 = unsafe { 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 = unsafe { rmc::nondet() }; + let c: u32 = rmc::any(); let d = if c > 100 { c diff --git a/src/test/rmc/LT-GT-LE-GE/main.rs b/src/test/rmc/LT-GT-LE-GE/main.rs index a201e5b6c1a0..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 = unsafe { 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 db150f3548bf..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 = unsafe { 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 31009aed705f..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 = unsafe { 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 25ab9276b8a5..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 = unsafe { 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 f88062ac1558..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 = unsafe { 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 df7ba852a994..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 = unsafe { rmc::nondet::() }; + let var = rmc::any::(); if var > 0 { err(); } diff --git a/src/test/rmc/NondetVectors/bytes.rs b/src/test/rmc/NondetVectors/bytes.rs index 8458071e540b..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![ - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { rmc::nondet() }, - unsafe { 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 = unsafe { 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 9d67e6ab236a..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 = unsafe { rmc::nondet() }; + let len: usize = rmc::any(); if !(len <= FIFO_SIZE) { return; } let _buf1: Vec = vec![0u8; len]; //< this works - let elt: u8 = unsafe { rmc::nondet() }; + let elt: u8 = rmc::any(); let _buf2: Vec = vec![elt; len]; //< this fails: "memset destination region writeable" - let idx: usize = unsafe { 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 5e8e2f3cbe25..30e3caa76099 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 = unsafe { rmc::nondet() }; + let mut a: f32 = unsafe { rmc::any_raw() }; 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 3987da8c947c..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 = unsafe { rmc::nondet() }; - let w: u128 = unsafe { 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 176170932a1a..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 = unsafe { rmc::nondet() }; - let w: $ty = unsafe { 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 63afc266da27..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 = unsafe { 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 fa1ecff49ac7..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 = unsafe { 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 = unsafe { 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 a90d6f20fdf6..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 = unsafe { 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 0d82779672a4..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 = unsafe { rmc::nondet() }; - let b: u8 = unsafe { rmc::nondet() }; - let c: u8 = unsafe { 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 = unsafe { rmc::nondet() }; - // let b: u8 = unsafe { rmc::nondet() }; - // let c: u8 = unsafe { 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 e04d69e9b91a..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 = unsafe { rmc::nondet() }; - let b: u8 = unsafe { rmc::nondet() }; - let c: u8 = unsafe { 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 1d0a8f5bcc28..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 = unsafe { rmc::nondet() }; - let b: u8 = unsafe { rmc::nondet() }; - let c: u8 = unsafe { 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 bd95af5d20d7..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 = unsafe { rmc::nondet() }; - let b = unsafe { 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 bd95af5d20d7..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 = unsafe { rmc::nondet() }; - let b = unsafe { 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 97b80765cb85..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 = unsafe { rmc::nondet() }; - let b = unsafe { 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 938d43c8918b..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 = unsafe { 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 8d4a6e8e2915..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 = unsafe { 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 2911ef890496..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 = unsafe { 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 1019256e089f..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 = unsafe { 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 8a49533a0d21..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 = unsafe { rmc::nondet() }; - let y2 = unsafe { rmc::nondet() }; - let x3 = unsafe { rmc::nondet() }; - let y3 = unsafe { rmc::nondet() }; - let z3 = unsafe { 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 eb620a3ffb82..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 = unsafe { rmc::nondet() }; - let y2 = unsafe { rmc::nondet() }; - let x3 = unsafe { rmc::nondet() }; - let y3 = unsafe { rmc::nondet() }; - let z3 = unsafe { 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 f3a56a806c28..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 = unsafe { rmc::nondet() }; - let y2 = unsafe { rmc::nondet() }; - let x3 = unsafe { rmc::nondet() }; - let y3 = unsafe { rmc::nondet() }; - let z3 = unsafe { 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 31e5e3d27995..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 = unsafe { rmc::nondet() }; - let y2 = unsafe { rmc::nondet() }; - let x3 = unsafe { rmc::nondet() }; - let y3 = unsafe { rmc::nondet() }; - let z3 = unsafe { 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 53038d2fb003..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 = unsafe { rmc::nondet() }; - let y2 = unsafe { rmc::nondet() }; - let x3 = unsafe { rmc::nondet() }; - let y3 = unsafe { rmc::nondet() }; - let z3 = unsafe { 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 1747aa0a9747..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 = unsafe { rmc::nondet() }; - let y2 = unsafe { rmc::nondet() }; - let x3 = unsafe { rmc::nondet() }; - let y3 = unsafe { rmc::nondet() }; - let z3 = unsafe { 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 0b0e589236dc..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 = unsafe { 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 af8f7b9a8eed..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 = unsafe { 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 42cf6770369a..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 = unsafe { 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 9ed0eed906e8..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 = unsafe { 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 460e3c927f79..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 = unsafe { 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 = unsafe { 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 d7412cdacb59..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 = unsafe { 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 = unsafe { 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 dc69ac475e16..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 = unsafe { rmc::nondet() }; - let x = unsafe { rmc::nondet() }; - let y = unsafe { rmc::nondet() }; - let z = unsafe { 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 d17ff1a3b08e..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 = unsafe { rmc::nondet() }; - let x = unsafe { rmc::nondet() }; - let y = unsafe { rmc::nondet() }; - let z = unsafe { 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 cc25fed89485..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 = unsafe { rmc::nondet() }; - // let b: u16 = unsafe { rmc::nondet() }; - // let c: u16 = unsafe { 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 111f0533312a..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 = unsafe { rmc::nondet() }; - let b: u16 = unsafe { rmc::nondet() }; - let c: u16 = unsafe { 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); From 16e7ba06bf93d62df346248bd2f327f62c081039 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Nov 2021 22:43:07 -0800 Subject: [PATCH 3/9] Add any / any_raw to replace nondet. Users will be able to control how RMC generate symbolic values to their variables. - `rmc::any::()` will provide a safe way to generate values that respect any invariant specified to type T (Given by the implementation of Invariant type.) - `rmc::any_raw::()` will provide any bitvalue possible for the memory layout of the type. This is an unsafe method and users must ensure correctness after this call. Note: I still need to add tests to the implementations of Invariant we provide. --- .../src/codegen/assumptions.rs | 594 ------------------ compiler/rustc_codegen_rmc/src/codegen/mod.rs | 1 - .../rustc_codegen_rmc/src/overrides/hooks.rs | 9 +- .../rmc/src/{invariants.rs => invariant.rs} | 60 +- library/rmc/src/lib.rs | 17 +- library/rmc/src/slice.rs | 28 +- .../firecracker/virtio-block-parse/main.rs | 16 +- src/test/rmc/Invariants/enum.rs | 67 ++ src/test/rmc/Invariants/enum_raw_fail.rs | 35 ++ src/test/rmc/NondetSlices/test1.rs | 2 +- src/test/rmc/NondetSlices/test2.rs | 2 +- src/test/rmc/TypeInvariant/char.rs_ignore | 9 + src/test/rmc/TypeInvariant/char_fail.rs | 8 + 13 files changed, 208 insertions(+), 640 deletions(-) delete mode 100644 compiler/rustc_codegen_rmc/src/codegen/assumptions.rs rename library/rmc/src/{invariants.rs => invariant.rs} (61%) create mode 100644 src/test/rmc/Invariants/enum.rs create mode 100644 src/test/rmc/Invariants/enum_raw_fail.rs create mode 100644 src/test/rmc/TypeInvariant/char.rs_ignore create mode 100644 src/test/rmc/TypeInvariant/char_fail.rs diff --git a/compiler/rustc_codegen_rmc/src/codegen/assumptions.rs b/compiler/rustc_codegen_rmc/src/codegen/assumptions.rs deleted file mode 100644 index 6383160d0ca3..000000000000 --- a/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/compiler/rustc_codegen_rmc/src/codegen/mod.rs b/compiler/rustc_codegen_rmc/src/codegen/mod.rs index 643bb9de3cb0..c2106961df5a 100644 --- a/compiler/rustc_codegen_rmc/src/codegen/mod.rs +++ b/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/compiler/rustc_codegen_rmc/src/overrides/hooks.rs b/compiler/rustc_codegen_rmc/src/overrides/hooks.rs index 2b08c842ffeb..56fb79a8f3f1 100644 --- a/compiler/rustc_codegen_rmc/src/overrides/hooks.rs +++ b/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/library/rmc/src/invariants.rs b/library/rmc/src/invariant.rs similarity index 61% rename from library/rmc/src/invariants.rs rename to library/rmc/src/invariant.rs index 22d700f8ea39..1a5d26d4fecb 100644 --- a/library/rmc/src/invariants.rs +++ b/library/rmc/src/invariant.rs @@ -5,11 +5,14 @@ /// 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. -pub trait Invariant { +/// +/// Implementations of Invariant traits must ensure that the current bit values of the given type +/// is valid and that all its invariants hold. +pub unsafe trait Invariant { fn is_valid(&self) -> bool; } -impl Invariant for bool { +unsafe impl Invariant for bool { #[inline(always)] fn is_valid(&self) -> bool { let byte = u8::from(*self); @@ -17,84 +20,84 @@ impl Invariant for bool { } } -impl Invariant for u8 { +unsafe impl Invariant for u8 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for u16 { +unsafe impl Invariant for u16 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for u32 { +unsafe impl Invariant for u32 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for u64 { +unsafe impl Invariant for u64 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for u128 { +unsafe impl Invariant for u128 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for usize { +unsafe impl Invariant for usize { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for i8 { +unsafe impl Invariant for i8 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for i16 { +unsafe impl Invariant for i16 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for i32 { +unsafe impl Invariant for i32 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for i64 { +unsafe impl Invariant for i64 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for i128 { +unsafe impl Invariant for i128 { #[inline(always)] fn is_valid(&self) -> bool { true } } -impl Invariant for isize { +unsafe impl Invariant for isize { #[inline(always)] fn is_valid(&self) -> bool { true @@ -104,10 +107,37 @@ impl Invariant for isize { /// Verifies that: /// - a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] /// Ref: https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html -impl Invariant for char { +unsafe impl Invariant for char { #[inline(always)] fn is_valid(&self) -> bool { let val = *self as u32; val <= 0xD7FF || (val >= 0xE000 && val <= 0x10FFFF) } } + +unsafe impl Invariant for Option +where + T: Invariant, +{ + #[inline(always)] + fn is_valid(&self) -> bool { + match self { + None => true, + Some(value) => value.is_valid(), + } + } +} + +unsafe impl Invariant for Result +where + T: Invariant, + E: Invariant, +{ + #[inline(always)] + fn is_valid(&self) -> bool { + match self { + Ok(v) => v.is_valid(), + Err(e) => e.is_valid(), + } + } +} diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs index c247495a7b15..b8ed47cecb28 100644 --- a/library/rmc/src/lib.rs +++ b/library/rmc/src/lib.rs @@ -2,10 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(rustc_attrs)] // Used for rustc_diagnostic_item. +pub mod invariant; pub mod slice; -mod invariants; -use invariants::Invariant; +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 @@ -64,13 +64,20 @@ pub fn any() -> T { /// under all possible values of char, including invalid ones that are greater than char::MAX. /// /// ```rust -/// let inputA = rmc::any_raw::(); +/// let inputA = unsafe { rmc::any_raw::() }; /// fn_under_verification(inputA); /// ``` -#[rustc_diagnostic_item = "RmcNonDet"] +#[rustc_diagnostic_item = "RmcAnyRaw"] #[inline(never)] pub unsafe fn any_raw() -> T { - unimplemented!("RMC nondet") + unimplemented!("RMC any_raw") +} + +/// This function has been split into a safe and unsafe functions: `rmc::any` and `rmc::any_raw`. +#[deprecated] +#[inline(never)] +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/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index 738fc4ba6484..1ec33252f0d4 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -12,6 +12,10 @@ 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); @@ -46,11 +50,19 @@ impl GuestMemoryMmap { TRACK_READ_OBJ = Some(addr); } } - unsafe { rmc::any_raw() } + if rmc::any() { + unsafe { Ok(rmc::any_raw::()) } + } else { + Err(rmc::any::()) + } } fn read_obj_request_header(&self, addr: GuestAddress) -> Result { - unsafe { rmc::any_raw() } + if rmc::any() { + unsafe { Ok(rmc::any_raw::()) } + } else { + unsafe { Err(rmc::any_raw::()) } + } } } diff --git a/src/test/rmc/Invariants/enum.rs b/src/test/rmc/Invariants/enum.rs new file mode 100644 index 000000000000..fe6d20232077 --- /dev/null +++ b/src/test/rmc/Invariants/enum.rs @@ -0,0 +1,67 @@ +// 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 { + let val = *self as $repr; + val == $v1 || val == $v2 || val == $v3 + } + } + + 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..725b52383190 --- /dev/null +++ b/src/test/rmc/Invariants/enum_raw_fail.rs @@ -0,0 +1,35 @@ +// 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. + 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/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/TypeInvariant/char.rs_ignore b/src/test/rmc/TypeInvariant/char.rs_ignore new file mode 100644 index 000000000000..65f4207dafb4 --- /dev/null +++ b/src/test/rmc/TypeInvariant/char.rs_ignore @@ -0,0 +1,9 @@ +// 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/TypeInvariant/char_fail.rs b/src/test/rmc/TypeInvariant/char_fail.rs new file mode 100644 index 000000000000..7ba97c603f82 --- /dev/null +++ b/src/test/rmc/TypeInvariant/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"); +} From 460dd98fb51ecdb0e6a1e7444692935e39e5fd1e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 4 Jan 2022 13:05:13 -0800 Subject: [PATCH 4/9] Added tests and fixed a few things in the Invariant impl --- library/rmc/src/invariant.rs | 35 +++++++++++++---- library/rmc/src/lib.rs | 4 +- src/test/rmc/Invariants/bool.rs | 13 +++++++ src/test/rmc/Invariants/bool_raw_fail.rs | 14 +++++++ src/test/rmc/Invariants/enum.rs | 3 +- src/test/rmc/Invariants/float.rs | 23 +++++++++++ src/test/rmc/Invariants/integer.rs | 30 +++++++++++++++ src/test/rmc/Invariants/option.rs | 26 +++++++++++++ src/test/rmc/Invariants/option_raw_fail.rs | 26 +++++++++++++ src/test/rmc/Invariants/result.rs | 39 +++++++++++++++++++ src/test/rmc/Invariants/result_raw_fail.rs | 44 ++++++++++++++++++++++ 11 files changed, 245 insertions(+), 12 deletions(-) create mode 100644 src/test/rmc/Invariants/bool.rs create mode 100644 src/test/rmc/Invariants/bool_raw_fail.rs create mode 100644 src/test/rmc/Invariants/float.rs create mode 100644 src/test/rmc/Invariants/integer.rs create mode 100644 src/test/rmc/Invariants/option.rs create mode 100644 src/test/rmc/Invariants/option_raw_fail.rs create mode 100644 src/test/rmc/Invariants/result.rs create mode 100644 src/test/rmc/Invariants/result_raw_fail.rs diff --git a/library/rmc/src/invariant.rs b/library/rmc/src/invariant.rs index 1a5d26d4fecb..9d5f2d77f53d 100644 --- a/library/rmc/src/invariant.rs +++ b/library/rmc/src/invariant.rs @@ -97,6 +97,24 @@ unsafe impl Invariant for i128 { } } +/// 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. +unsafe impl Invariant for f32 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + +/// 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. +unsafe impl Invariant for f64 { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } +} + unsafe impl Invariant for isize { #[inline(always)] fn is_valid(&self) -> bool { @@ -110,7 +128,8 @@ unsafe impl Invariant for isize { unsafe impl Invariant for char { #[inline(always)] fn is_valid(&self) -> bool { - let val = *self as u32; + // RMC translates char into i32. + let val = *self as i32; val <= 0xD7FF || (val >= 0xE000 && val <= 0x10FFFF) } } @@ -121,10 +140,7 @@ where { #[inline(always)] fn is_valid(&self) -> bool { - match self { - None => true, - Some(value) => value.is_valid(), - } + if let Some(v) = self { v.is_valid() } else { matches!(*self, None) } } } @@ -135,9 +151,12 @@ where { #[inline(always)] fn is_valid(&self) -> bool { - match self { - Ok(v) => v.is_valid(), - Err(e) => e.is_valid(), + if let Ok(v) = self { + v.is_valid() + } else if let Err(e) = self { + e.is_valid() + } else { + false } } } diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs index b8ed47cecb28..bfd32f83e778 100644 --- a/library/rmc/src/lib.rs +++ b/library/rmc/src/lib.rs @@ -16,7 +16,7 @@ pub use invariant::Invariant; /// The code snippet below should never panic. /// /// ```rust -/// let i : i32 = unsafe { rmc::nondet() }; +/// let i : i32 = rmc::any(); /// rmc::assume(i > 10); /// if i < 0 { /// panic!("This will never panic"); @@ -26,7 +26,7 @@ pub use invariant::Invariant; /// The following code may panic though: /// /// ```rust -/// let i : i32 = unsafe { rmc::nondet() }; +/// let i : i32 = rmc::any(); /// assert!(i < 0, "This may panic and verification should fail."); /// rmc::assume(i > 10); /// ``` 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..30960e768ee3 --- /dev/null +++ b/src/test/rmc/Invariants/bool_raw_fail.rs @@ -0,0 +1,14 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-verify-fail +// 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/enum.rs b/src/test/rmc/Invariants/enum.rs index fe6d20232077..4cad4ca7e43e 100644 --- a/src/test/rmc/Invariants/enum.rs +++ b/src/test/rmc/Invariants/enum.rs @@ -28,8 +28,7 @@ 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 { - let val = *self as $repr; - val == $v1 || val == $v2 || val == $v3 + matches!(*self, $enum_type::Variant1 | $enum_type::Variant2 | $enum_type::Variant3) } } diff --git a/src/test/rmc/Invariants/float.rs b/src/test/rmc/Invariants/float.rs new file mode 100644 index 000000000000..e236fc108f6e --- /dev/null +++ b/src/test/rmc/Invariants/float.rs @@ -0,0 +1,23 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-verify-fail +// 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..fdd25ccec14a --- /dev/null +++ b/src/test/rmc/Invariants/integer.rs @@ -0,0 +1,30 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-verify-fail +// 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/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..0ad523e0359a --- /dev/null +++ b/src/test/rmc/Invariants/option_raw_fail.rs @@ -0,0 +1,26 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-verify-fail +// 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..1599d33cf0c4 --- /dev/null +++ b/src/test/rmc/Invariants/result_raw_fail.rs @@ -0,0 +1,44 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-verify-fail +// 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."); + } +} From ca85f7e56f696d453f1fc9bdbb80df0326532212 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 4 Jan 2022 17:31:02 -0800 Subject: [PATCH 5/9] Apply suggestions from code review Some typos Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- library/rmc/src/invariant.rs | 5 ++--- library/rmc/src/lib.rs | 2 +- src/test/rmc/BinOp_Offset/main_fail.rs | 2 +- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/library/rmc/src/invariant.rs b/library/rmc/src/invariant.rs index 9d5f2d77f53d..2986faa9e2c8 100644 --- a/library/rmc/src/invariant.rs +++ b/library/rmc/src/invariant.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -/// This module introduces the Invariant trait and as well as implementation for commonly used types. +/// This module introduces the Invariant trait as well as implementation for commonly used types. /// 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. @@ -122,8 +122,7 @@ unsafe impl Invariant for isize { } } -/// Verifies that: -/// - a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] +/// 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)] diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs index bfd32f83e778..6a463c1c9b6c 100644 --- a/library/rmc/src/lib.rs +++ b/library/rmc/src/lib.rs @@ -48,7 +48,7 @@ pub fn assume(_cond: bool) {} /// ``` /// /// Note: This is a safe construct and can only be used with types that implement the `Invariant` -/// trait. The invariant trait is used to constraint the result to ensure the value is valid. +/// trait. The invariant trait is used to constrain the result to ensure the value is valid. #[inline(always)] pub fn any() -> T { let value = unsafe { any_raw::() }; diff --git a/src/test/rmc/BinOp_Offset/main_fail.rs b/src/test/rmc/BinOp_Offset/main_fail.rs index 7840f141b5e9..87bc66666aaa 100644 --- a/src/test/rmc/BinOp_Offset/main_fail.rs +++ b/src/test/rmc/BinOp_Offset/main_fail.rs @@ -5,7 +5,7 @@ pub fn test_offset_in_double_array() { //let table: Vec> = Vec::with_capacity(1); let table: [[u64; 1]; 1] = [[rmc::any::()]]; - table[0][rmc::any::()]; // EXPCECTED FAIL + table[0][rmc::any::()]; // EXPECTED FAIL } fn main() { From 93581031aa3552578813552eab461d0d1fcf54fe Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 5 Jan 2022 12:42:32 -0800 Subject: [PATCH 6/9] Address a few comments --- library/rmc/src/invariant.rs | 134 +++++------------- src/test/rmc/DynTrait/main.rs | 2 +- src/test/rmc/FloatingPoint/main.rs | 2 +- src/test/rmc/Invariants/array.rs | 15 ++ src/test/rmc/Invariants/array_raw_fail.rs | 15 ++ src/test/rmc/Invariants/bool_raw_fail.rs | 1 - .../char.rs_ignore => Invariants/char.rs} | 1 - .../char_fail.rs | 0 src/test/rmc/Invariants/option_raw_fail.rs | 1 - src/test/rmc/Invariants/result_raw_fail.rs | 1 - src/test/rmc/Pointers_OtherTypes/main.rs | 2 +- 11 files changed, 68 insertions(+), 106 deletions(-) create mode 100644 src/test/rmc/Invariants/array.rs create mode 100644 src/test/rmc/Invariants/array_raw_fail.rs rename src/test/rmc/{TypeInvariant/char.rs_ignore => Invariants/char.rs} (99%) rename src/test/rmc/{TypeInvariant => Invariants}/char_fail.rs (100%) diff --git a/library/rmc/src/invariant.rs b/library/rmc/src/invariant.rs index 2986faa9e2c8..c24673b66407 100644 --- a/library/rmc/src/invariant.rs +++ b/library/rmc/src/invariant.rs @@ -12,113 +12,43 @@ pub unsafe trait Invariant { fn is_valid(&self) -> bool; } -unsafe impl Invariant for bool { - #[inline(always)] - fn is_valid(&self) -> bool { - let byte = u8::from(*self); - byte == 0 || byte == 1 - } -} - -unsafe impl Invariant for u8 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} - -unsafe impl Invariant for u16 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} - -unsafe impl Invariant for u32 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} - -unsafe impl Invariant for u64 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} - -unsafe impl Invariant for u128 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} - -unsafe impl Invariant for usize { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} - -unsafe impl Invariant for i8 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } +macro_rules! empty_invariant { + ( $type: ty ) => { + unsafe impl Invariant for $type { + #[inline(always)] + fn is_valid(&self) -> bool { + true + } + } + }; } -unsafe impl Invariant for i16 { - #[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); -unsafe impl Invariant for i32 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} +empty_invariant!(i8); +empty_invariant!(i16); +empty_invariant!(i32); +empty_invariant!(i64); +empty_invariant!(i128); +empty_invariant!(isize); -unsafe impl Invariant for i64 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} +// 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); -unsafe impl Invariant for i128 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} - -/// 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. -unsafe impl Invariant for f32 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} - -/// 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. -unsafe impl Invariant for f64 { - #[inline(always)] - fn is_valid(&self) -> bool { - true - } -} +empty_invariant!(()); -unsafe impl Invariant for isize { +unsafe impl Invariant for bool { #[inline(always)] fn is_valid(&self) -> bool { - true + let byte = u8::from(*self); + byte == 0 || byte == 1 } } @@ -133,6 +63,12 @@ unsafe impl Invariant for char { } } +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, diff --git a/src/test/rmc/DynTrait/main.rs b/src/test/rmc/DynTrait/main.rs index 17c46da445c4..29eae7e29481 100644 --- a/src/test/rmc/DynTrait/main.rs +++ b/src/test/rmc/DynTrait/main.rs @@ -32,7 +32,7 @@ fn main() { let random_number = rmc::any(); let animal = random_animal(random_number); let s = animal.noise(); - if (random_number < 5) { + if random_number < 5 { assert!(s == 1); } else { assert!(s == 2); diff --git a/src/test/rmc/FloatingPoint/main.rs b/src/test/rmc/FloatingPoint/main.rs index 8237aa76c7a7..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 = unsafe { rmc::any_raw() }; + let a: $ty = rmc::any(); let b = a / 2.0; if a < 0.0 { 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_raw_fail.rs b/src/test/rmc/Invariants/bool_raw_fail.rs index 30960e768ee3..7de1aa63d90b 100644 --- a/src/test/rmc/Invariants/bool_raw_fail.rs +++ b/src/test/rmc/Invariants/bool_raw_fail.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// rmc-verify-fail // Ensure that rmc::any_raw:: may generate invalid booleans. fn main() { diff --git a/src/test/rmc/TypeInvariant/char.rs_ignore b/src/test/rmc/Invariants/char.rs similarity index 99% rename from src/test/rmc/TypeInvariant/char.rs_ignore rename to src/test/rmc/Invariants/char.rs index 65f4207dafb4..0483846c8c5e 100644 --- a/src/test/rmc/TypeInvariant/char.rs_ignore +++ b/src/test/rmc/Invariants/char.rs @@ -6,4 +6,3 @@ pub fn main() { let c: char = rmc::any(); assert!(c <= char::MAX); } - diff --git a/src/test/rmc/TypeInvariant/char_fail.rs b/src/test/rmc/Invariants/char_fail.rs similarity index 100% rename from src/test/rmc/TypeInvariant/char_fail.rs rename to src/test/rmc/Invariants/char_fail.rs diff --git a/src/test/rmc/Invariants/option_raw_fail.rs b/src/test/rmc/Invariants/option_raw_fail.rs index 0ad523e0359a..2ad74d45d818 100644 --- a/src/test/rmc/Invariants/option_raw_fail.rs +++ b/src/test/rmc/Invariants/option_raw_fail.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// rmc-verify-fail // Ensure that rmc::any_raw will generate unsconstrainted values for Option. extern crate rmc; diff --git a/src/test/rmc/Invariants/result_raw_fail.rs b/src/test/rmc/Invariants/result_raw_fail.rs index 1599d33cf0c4..d7f30fdbd910 100644 --- a/src/test/rmc/Invariants/result_raw_fail.rs +++ b/src/test/rmc/Invariants/result_raw_fail.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// rmc-verify-fail // Ensure that rmc::any_raw will generate unsconstrainted values for Result. extern crate rmc; diff --git a/src/test/rmc/Pointers_OtherTypes/main.rs b/src/test/rmc/Pointers_OtherTypes/main.rs index 30e3caa76099..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 = unsafe { rmc::any_raw() }; + let mut a: f32 = rmc::any(); let b = a; div_by_two(&mut a); // NaN From 2d9cc0a218a9b80f127480239b9db764e7177707 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 5 Jan 2022 13:58:53 -0800 Subject: [PATCH 7/9] Add support to NonZero* types --- library/rmc/src/invariant.rs | 26 ++++++++++++++++++++ src/test/rmc/Invariants/float.rs | 1 - src/test/rmc/Invariants/integer.rs | 1 - src/test/rmc/Invariants/nonzero.rs | 39 ++++++++++++++++++++++++++++++ 4 files changed, 65 insertions(+), 2 deletions(-) create mode 100644 src/test/rmc/Invariants/nonzero.rs diff --git a/library/rmc/src/invariant.rs b/library/rmc/src/invariant.rs index c24673b66407..425dfc40c983 100644 --- a/library/rmc/src/invariant.rs +++ b/library/rmc/src/invariant.rs @@ -2,6 +2,7 @@ // 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. @@ -95,3 +96,28 @@ where } } } + +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/src/test/rmc/Invariants/float.rs b/src/test/rmc/Invariants/float.rs index e236fc108f6e..14c805ff2654 100644 --- a/src/test/rmc/Invariants/float.rs +++ b/src/test/rmc/Invariants/float.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// rmc-verify-fail // Ensure that rmc::any and rmc::any_raw can be used with integers. macro_rules! test { diff --git a/src/test/rmc/Invariants/integer.rs b/src/test/rmc/Invariants/integer.rs index fdd25ccec14a..2278cf2dd4a6 100644 --- a/src/test/rmc/Invariants/integer.rs +++ b/src/test/rmc/Invariants/integer.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// rmc-verify-fail // Ensure that rmc::any and rmc::any_raw can be used with integers. macro_rules! test { 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); +} From 2277f3418747af068c4683fa47b162631a2acace Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 6 Jan 2022 22:00:51 -0800 Subject: [PATCH 8/9] Update tests per PR comments. --- .../firecracker/virtio-block-parse/main.rs | 52 ++++++++++++++----- src/test/rmc/Enum/result3.rs | 2 +- src/test/rmc/FunctionCall_Ret-NoParam/main.rs | 2 +- src/test/rmc/Invariants/enum_raw_fail.rs | 4 ++ 4 files changed, 45 insertions(+), 15 deletions(-) diff --git a/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index 1ec33252f0d4..6c727dd3b3d8 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -13,12 +13,20 @@ macro_rules! error { struct MyError {} unsafe impl rmc::Invariant for MyError { - fn is_valid(&self) -> bool { true } + 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; @@ -35,12 +43,12 @@ impl GuestMemoryMmap { unsafe { if retval.is_none() && !TRACK_CHECKED_OFFSET_NONE { TRACK_CHECKED_OFFSET_NONE = true; - } + } } 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 { @@ -50,19 +58,11 @@ impl GuestMemoryMmap { TRACK_READ_OBJ = Some(addr); } } - if rmc::any() { - unsafe { Ok(rmc::any_raw::()) } - } else { - Err(rmc::any::()) - } + if rmc::any() { Ok(rmc::any::()) } else { Err(rmc::any::()) } } fn read_obj_request_header(&self, addr: GuestAddress) -> Result { - if rmc::any() { - unsafe { Ok(rmc::any_raw::()) } - } else { - unsafe { Err(rmc::any_raw::()) } - } + if rmc::any() { Ok(rmc::any::()) } else { Err(rmc::any::()) } } } @@ -79,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, @@ -187,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 } @@ -241,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, diff --git a/src/test/rmc/Enum/result3.rs b/src/test/rmc/Enum/result3.rs index f6a28391df84..b61c66bcc08c 100644 --- a/src/test/rmc/Enum/result3.rs +++ b/src/test/rmc/Enum/result3.rs @@ -14,7 +14,7 @@ fn main() { let input: Result = unsafe { rmc::any_raw() }; let x = foo(&input); assert!(x == 3 || input != Err(Unit::Unit)); - let input: Result = if unsafe { rmc::any_raw() } { 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/FunctionCall_Ret-NoParam/main.rs b/src/test/rmc/FunctionCall_Ret-NoParam/main.rs index 372e205434b9..6850b707495c 100644 --- a/src/test/rmc/FunctionCall_Ret-NoParam/main.rs +++ b/src/test/rmc/FunctionCall_Ret-NoParam/main.rs @@ -45,7 +45,7 @@ fn return_f32() -> f32 { } } fn return_f64() -> f64 { - let x: f64 = unsafe { rmc::any_raw() }; + let x: f64 = rmc::any(); if x <= 10.0 && x >= -10.0 { return x; } else { diff --git a/src/test/rmc/Invariants/enum_raw_fail.rs b/src/test/rmc/Invariants/enum_raw_fail.rs index 725b52383190..89920c94f13f 100644 --- a/src/test/rmc/Invariants/enum_raw_fail.rs +++ b/src/test/rmc/Invariants/enum_raw_fail.rs @@ -15,6 +15,10 @@ enum Basic { 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; From 502c84ef22e311062a53057e6c71840fd226c79d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 7 Jan 2022 14:28:09 -0800 Subject: [PATCH 9/9] Add Arbitrary trait --- library/rmc/src/arbitrary.rs | 22 ++++++++++++++++++++++ library/rmc/src/invariant.rs | 9 ++++++++- library/rmc/src/lib.rs | 31 ++++++++++++++++++++++--------- 3 files changed, 52 insertions(+), 10 deletions(-) create mode 100644 library/rmc/src/arbitrary.rs 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 index 425dfc40c983..0437c8ee19bc 100644 --- a/library/rmc/src/invariant.rs +++ b/library/rmc/src/invariant.rs @@ -1,7 +1,7 @@ // 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. +//! 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 @@ -9,7 +9,14 @@ use std::num::*; /// /// 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; } diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs index 6a463c1c9b6c..3a91fc7e3f55 100644 --- a/library/rmc/src/lib.rs +++ b/library/rmc/src/lib.rs @@ -2,9 +2,11 @@ // 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 @@ -40,20 +42,19 @@ pub fn assume(_cond: bool) {} /// # 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::any::(); +/// let inputA = rmc::any::(); /// fn_under_verification(inputA); /// ``` /// -/// Note: This is a safe construct and can only be used with types that implement the `Invariant` -/// trait. The invariant trait is used to constrain the result to ensure the value is valid. +/// 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 { - let value = unsafe { any_raw::() }; - assume(value.is_valid()); - value +pub fn any() -> T { + T::any() } /// This function creates an unconstrained value of type `T`. This may result in an invalid value. @@ -67,6 +68,18 @@ pub fn any() -> T { /// 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 { @@ -76,7 +89,7 @@ pub unsafe fn any_raw() -> T { /// This function has been split into a safe and unsafe functions: `rmc::any` and `rmc::any_raw`. #[deprecated] #[inline(never)] -pub fn nondet() -> T { +pub fn nondet() -> T { any::() }