Differentiate between check, codegen, and verification errors. (rust-lang#353)

* Differentiate between check, codegen, and verification errors.

* Fix typo.

* Rename tests.

* Address concerns.

* Remove unnecessary code and fix typos.

Author: bdalrhm

src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs renamed to src/test/cbmc/Assert/UninitValid/fixme_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-verify-fail
+
 use std::mem::{self, MaybeUninit};
 
 fn main() {

src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs renamed to src/test/cbmc/Assert/ZeroValid/fixme_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-verify-fail
+
 // The function zeroed() calls assert_zero_valid to mark that it is only defined to assign an
 // all-zero bit pattern to a type T if this is a valid value. So the following is undefined.
 

src/test/cbmc/BinOp_Offset/main_fail.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 include!("../../rmc-prelude.rs");
 
 pub fn test_offset_in_double_array() {

src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs renamed to src/test/cbmc/BitManipulation/Stable/fixme_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-verify-fail
+
 fn main() {
     // Intrinsics implemented as integer primitives
     // https://doc.rust-lang.org/core/intrinsics/fn.cttz.html

src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs renamed to src/test/cbmc/BitManipulation/Unstable/fixme_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-verify-fail
+
 #![feature(core_intrinsics)]
 use std::intrinsics::{ctlz, cttz, cttz_nonzero};
 

src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs renamed to src/test/cbmc/Count/Unstable/Ctlz/bounds.rs

@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// rmc-verify-fail
 // cbmc-flags: --bounds-check
 
 #![feature(core_intrinsics)]

src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs renamed to src/test/cbmc/Count/Unstable/Cttz/bounds.rs

@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// rmc-verify-fail
 // cbmc-flags: --bounds-check
 
 #![feature(core_intrinsics)]

src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs

@@ -1,10 +1,11 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Check that we can codegen a boxed dyn closure and fail an inner assertion
 
 // This current verifies "successfully" because the closure is not actually
-// called in the resulting CotoC code.
+// called in the resulting GotoC code.
 // https://github.com/model-checking/rmc/issues/240
 
 include!("../../rmc-prelude.rs");

src/test/cbmc/DynTrait/boxed_trait_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Dynamic traits should work when used through a box
 // _fail test; all assertions inverted.

src/test/cbmc/DynTrait/different_crates_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // This test uses a trait defined in a different crate (the standard library)
 // and a test defined in the local crate. The goal is to test vtable resolution

src/test/cbmc/DynTrait/nested_boxes_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // This test checks the size and align fields for 3-deep nested trait pointers. The
 // outter 2 dynamic trait objects have fat pointers as their backing data.

src/test/cbmc/FatPointers/boxmuttrait_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 use std::io::{sink, Write};
 

src/test/cbmc/FatPointers/boxslice1.rs

@@ -11,5 +11,5 @@ fn main() {
     // 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
+    // see boxslice2.rs for an attempt to test sparkle_heart_str
 }

src/test/cbmc/FatPointers/boxslice2_fail.rs renamed to src/test/cbmc/FatPointers/boxslice2.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Casts boxed array to boxed slice (example taken from rust documentation)
 use std::str;

src/test/cbmc/FatPointers/boxtrait_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // This is handled by the box to box case of unsized pointers
 

src/test/cbmc/FatPointers/trait1_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Cast a concrete ref to a trait ref.
 

src/test/cbmc/FatPointers/trait2_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Cast a concrete ref to a trait raw pointer.
 

src/test/cbmc/FatPointers/trait3_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Cast a concrete ref to
 //   concrete raw pointer

src/test/cbmc/Intrinsics/abort_fail.rs renamed to src/test/cbmc/Intrinsics/abort.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 #![feature(core_intrinsics)]
 use std::intrinsics;
 fn main() {

src/test/cbmc/PointerOffset/Unstable/main_fail.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 #![feature(core_intrinsics)]
 use std::intrinsics::ptr_offset_from;
 

src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs renamed to src/test/cbmc/Pointers_Basic/fixme_from_raw.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 fn main() {
     let address = 0x01234usize;

src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs renamed to src/test/cbmc/Pointers_OutOfScopeFail/fixme_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-verify-fail
+
 fn main() {
     // declare pointer to integer
     let p_subscoped: *const u32;

src/test/cbmc/SIMD/Compare/main_fail.rs renamed to src/test/cbmc/SIMD/Compare/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-verify-fail
+
 #![feature(repr_simd, platform_intrinsics)]
 
 #[repr(simd)]

src/test/cbmc/Serde/main_fail.rs renamed to src/test/cbmc/Serde/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-check-fail
+
 // We currently assert(false) for reify function pointer.
 // So this codegens but fails model checking.
 

src/test/cbmc/SizeAndAlignOfDst/main_fail.rs

@@ -5,6 +5,7 @@
 // Arc<Mutex<dyn Subscriber>>.
 // This test still fails with a final coercion error for
 // DummySubscriber to dyn Subscriber.
+// rmc-verify-fail
 
 use std::sync::Arc;
 use std::sync::Mutex;

src/test/cbmc/Slice/drop_in_place_fail.rs renamed to src/test/cbmc/Slice/drop_in_place.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-check-fail
+
 #[allow(unconditional_recursion)]
 pub unsafe fn drop_in_place<T: ?Sized>(to_drop: *mut T) {
     // Code here does not matter - this is replaced by the

src/test/cbmc/Slice/pathbuf_fail.rs renamed to src/test/cbmc/Slice/pathbuf.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 use std::fs;
 use std::path::PathBuf;
 pub fn main() {

src/test/cbmc/Slice/slice_from_raw_fail.rs renamed to src/test/cbmc/Slice/slice_from_raw.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 use std::slice;
 
 include!("../../rmc-prelude.rs");

src/test/cbmc/VolatileIntrinsics/core_intrinsics.rs

@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-codegen-fail
+
+#![feature(core_intrinsics)]
+
+use std::intrinsics::*;
+
+pub fn main() {
+    let mut a: Box<u8> = Box::new(0);
+    unsafe {
+        let x = volatile_load(&*a);
+        assert!(x == *a);
+        volatile_store(&mut *a, 1);
+        assert!(*a == 1);
+        unaligned_volatile_store(&mut *a, 2);
+        assert!(*a == 2);
+        volatile_set_memory(&mut *a, 3, 1);
+        assert!(*a == 3);
+    }
+}

src/test/prusti/Binary_search_fail.rs renamed to src/test/prusti/Binary_search.rs

@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// rmc-verify-fail
 // cbmc-flags: --unwind 4
 
 use std::cmp::Ordering::*;
@@ -43,7 +43,7 @@ fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize> {
     None
 }
 
-include!("../../rmc-prelude.rs");
+include!("../rmc-prelude.rs");
 
 fn get() -> [i32; 11] {
     [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11]

src/test/smack/basic/add_fail.rs renamed to src/test/smack/basic/add.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;

src/test/smack/basic/arith_assume_fail.rs renamed to src/test/smack/basic/arith_assume3.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 include!("../../rmc-prelude.rs");
 

src/test/smack/basic/div_fail.rs renamed to src/test/smack/basic/div.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;

src/test/smack/basic/mod_fail.rs renamed to src/test/smack/basic/mod.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;

src/test/smack/basic/mul_fail.rs renamed to src/test/smack/basic/mul.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;

src/test/smack/basic/sub_fail.rs renamed to src/test/smack/basic/sub.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;

src/test/smack/functions/closure_fail.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting
 // @expect verified
+// rmc-verify-fail
 
 fn call_with_one<F>(mut some_closure: F) -> ()
 where

src/test/smack/functions/double_fail.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 fn double(a: u32) -> u32 {
     a * 2

src/test/smack/generics/generic_function_fail1.rs renamed to src/test/smack/generics/generic_function1.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,

src/test/smack/generics/generic_function_fail2.rs renamed to src/test/smack/generics/generic_function2.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,

src/test/smack/generics/generic_function_fail3.rs renamed to src/test/smack/generics/generic_function3.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,

src/test/smack/generics/generic_function_fail4.rs renamed to src/test/smack/generics/generic_function4.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect verified
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,

src/test/smack/generics/generic_function_fail5.rs renamed to src/test/smack/generics/generic_function5.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect verified
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,

src/test/smack/loops/gauss_sum_nondet.rs

@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting --unroll=4
 // @expect verified
-
 // cbmc-flags: --unwind 5
 
 include!("../../rmc-prelude.rs");

src/test/smack/loops/gauss_sum_nondet_fail.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting --unroll=10
 // @expect error
-
+// rmc-verify-fail
 // cbmc-flags: --unwind 5
 
 include!("../../rmc-prelude.rs");

src/test/smack/loops/iterator_fail.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting --unroll=10
 // @expect error
-
+// rmc-verify-fail
 // cbmc-flags: --unwind 5
 
 fn fac(n: u64) -> u64 {

src/test/smack/overflow/add_overflow_fail.rs renamed to src/test/smack/overflow/add_overflow.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --integer-overflow
 // @expect overflow
+// rmc-verify-fail
 
 pub fn get128() -> u8 {
     128