Improve some regression tests and add some more. (rust-lang#154)

* Improve some regression tests and add some more.

* Add more assertions to a test.

* Revert changes to trait regressions.

* Add comments explaining dereferencing raw address test.

Author: bdalrhm

rust-tests/cbmc-reg/BitManipulation/Stable/fixme_main_fail.rs

@@ -10,7 +10,7 @@ fn main() {
     let num_leading = x.leading_zeros();
     let rotated_num = x.rotate_left(3);
 
-    assert!(num_trailing == 3);
+    assert!(num_trailing == 3); // fails because of https://github.com/model-checking/rmc/issues/26
     assert!(num_leading == 2);
     assert!(rotated_num == 0b1100_0001_u8);
 }

rust-tests/cbmc-reg/BitManipulation/Unstable/fixme_main_fail.rs

@@ -14,6 +14,7 @@ fn main() {
     let num_leading = ctlz(v8);
     let num_trailing_nz = unsafe { cttz_nonzero(v8) };
 
+    // fail because of https://github.com/model-checking/rmc/issues/26
     assert!(nttz8 == 3);
     assert!(nttz16 == 11);
     assert!(nttz32 == 27);

rust-tests/cbmc-reg/CodegenStatic/main.rs

@@ -2,5 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 static STATIC: [&str; 1] = ["FOO"];
 fn main() {
-    let _x = STATIC[0];
+    let x = STATIC[0];
+    let bytes = x.as_bytes();
+    assert!(bytes.len() == 3);
+    assert!(bytes[0] == b'F');
+    assert!(bytes[1] == b'O');
+    assert!(bytes[2] == b'O');
 }

rust-tests/cbmc-reg/Enum/result3.rs

@@ -0,0 +1,24 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[derive(Debug, PartialEq)]
+pub enum Unit {
+    Unit,
+}
+
+fn __nondet<T>() -> T {
+    unimplemented!()
+}
+
+fn foo(input: &Result<u32, Unit>) -> u32 {
+    if let Ok(num) = input { *num } else { 3 }
+}
+
+pub fn main() {
+    let input: Result<u32, Unit> = __nondet();
+    let x = foo(&input);
+    assert!(x == 3 || input != Err(Unit::Unit));
+    let input: Result<u32, Unit> = if __nondet() { Ok(0) } else { Err(Unit::Unit) };
+    let x = foo(&input);
+    assert!(x != 3 || input == Err(Unit::Unit));
+    assert!(x != 0 || input == Ok(0));
+}

rust-tests/cbmc-reg/ExactDiv/main.rs

@@ -6,7 +6,5 @@ fn main() {
     let a: u8 = 8;
     let b: u8 = 4;
     let i = unsafe { std::intrinsics::exact_div(a, b) };
+    assert!(i == 2);
 }
-
-//  let mut iter = "a".split_whitespace();
-//  iter.next();

rust-tests/cbmc-reg/FatPointers/boxslice1.rs

@@ -8,7 +8,7 @@ fn main() {
     // This vector of bytes is used to initialize a Box<[u8; 4]>
     let sparkle_heart_vec = vec![240, 159, 146, 150];
 
-    // This transformer produces a Box<[u8>]
+    // This transformer produces a Box<[u8]>
     let _sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
 
     // see boxslice2_fail.rs for an attempt to test sparkle_heart_str

rust-tests/cbmc-reg/FatPointers/boxslice2_fail.rs

@@ -8,7 +8,7 @@ fn main() {
     // This vector of bytes is used to initialize a Box<[u8; 4]>
     let sparkle_heart_vec = vec![240, 159, 146, 150];
 
-    // This transformer produces a Box<[u8>]
+    // This transformer produces a Box<[u8]>
     let sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
 
     // This match statement generates failures even though

rust-tests/cbmc-reg/FloatingPoint/main.rs

@@ -0,0 +1,34 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+fn __nondet<T>() -> T {
+    unimplemented!()
+}
+
+macro_rules! test_floats {
+    ($ty:ty) => {
+        let a: $ty = __nondet();
+        let b = a / 2.0;
+
+        if a < 0.0 {
+            assert!(a <= b);
+        } else if a >= 0.0 {
+            assert!(a >= b);
+        }
+
+        let c = b * 2.0;
+        // general/infinity            Close but not exact                    NAN
+        assert!(a == c || a - c < 0.00000001 || c - a < 0.00000001 || c * 0.0 != 0.0);
+
+        let d: $ty = 0.0;
+        assert!(d + 1.0 > 0.0);
+        assert!(d - 1.0 < 0.0);
+    };
+}
+
+fn main() {
+    assert!(1.1 == 1.1 * 1.0);
+    assert!(1.1 != 1.11 / 1.0);
+
+    test_floats!(f32);
+    test_floats!(f64);
+}

rust-tests/cbmc-reg/Pointers_Basic/fixme_from_raw_fail.rs

@@ -0,0 +1,12 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let address = 0x01234usize;
+    let ptr = address as *mut i32;
+    // pointers can only be dereferenced inside unsafe blocks
+    unsafe {
+        // dereferencing a random address in memory will probably crash the program
+        *ptr = 1; // rmc verification succeeds without generating any assertions
+    };
+}

rust-tests/cbmc-reg/SaturatingIntrinsics/main.rs

@@ -8,7 +8,7 @@ fn __nondet<T>() -> T {
 }
 
 macro_rules! test_saturating_intrinsics {
-    ($ty:tt) => {
+    ($ty:ty) => {
         let v: $ty = __nondet();
         let w: $ty = __nondet();
         let result = intrinsics::saturating_add(v, w);

rust-tests/cbmc-reg/Slice/main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+/// rmc main.rs -- --unwind 6 --unwinding-assertions
 fn main() {
     let name: &str = "hello";
+    assert!(name == "hello");
 }

rust-tests/cbmc-reg/Slice/slice_from_raw_fail.rs

@@ -0,0 +1,17 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+use std::slice;
+
+fn __nondet<T>() -> T {
+    unimplemented!()
+}
+
+// From Listing 19-7: Creating a slice from an arbitrary memory location. https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html
+fn main() {
+    let address = 0x01234usize;
+    let r = address as *mut i32;
+    let slice: &mut [i32] = unsafe { slice::from_raw_parts_mut(r, 10000) };
+    // the behavior is undefined when the slice is used
+    slice[9999] = 0; // verification succeeds
+    assert!(slice[9999] == 0); // verification succeeds
+}