Move gotoc tests under run-make to their own test suite. (rust-lang#217)

* Move expected tests out of run-make tests.

* Skip copyright check for `*expected` and `.gitignore` files.

* Fix typos.

* Readd code to add scripts directory to path.

* Factor out duplicated code.

Author: bdalrhm

.github/workflows/copyright.yml

@@ -15,7 +15,7 @@ jobs:
       - name: Get paths for files added
         id: git-diff
         run: |
-          files=$(git diff --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | xargs)
+          files=$(git diff --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -v -E '(expected|gitignore)$' | xargs)
           echo "::set-output name=paths::$files"
 
       - name: Execute copyright check

scripts/rmc-regression.sh

@@ -9,8 +9,6 @@ set -o pipefail
 set -o nounset
 
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
-RUST_DIR=$SCRIPT_DIR/..
-export RMC_RUSTC=`find $RUST_DIR/build -name "rustc" -print | grep stage1`
 export PATH=$SCRIPT_DIR:$PATH
 EXTRA_X_PY_BUILD_ARGS="${EXTRA_X_PY_BUILD_ARGS:-}"
 
@@ -21,10 +19,6 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 # Formatting check
 ./x.py fmt --check
 
-# Standalone rmc tests and cargo tests
-pushd $RUST_DIR
+# Standalone rmc tests, expected tests, and cargo tests
 ./x.py build -i --stage 1 library/std ${EXTRA_X_PY_BUILD_ARGS}
-./x.py test -i --stage 1 cbmc firecracker prusti smack cargo-rmc
-
-# run-make tests
-./x.py test -i --stage 1 src/test/run-make --test-args gotoc
+./x.py test -i --stage 1 cbmc firecracker prusti smack expected cargo-rmc

src/bootstrap/builder.rs

@@ -469,6 +469,7 @@ impl<'a> Builder<'a> {
                 test::Serial,
                 test::SMACK,
                 test::CargoRMC,
+                test::Expected,
                 // Run run-make last, since these won't pass without make on Windows
                 test::RunMake,
             ),

src/bootstrap/test.rs

@@ -1212,6 +1212,8 @@ default_test!(SMACK { path: "src/test/smack", mode: "rmc", suite: "smack" });
 
 default_test!(CargoRMC { path: "src/test/cargo-rmc", mode: "cargo-rmc", suite: "cargo-rmc" });
 
+default_test!(Expected { path: "src/test/expected", mode: "expected", suite: "expected" });
+
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
 struct Compiletest {
     compiler: Compiler,

src/test/run-make/gotoc-allocation/expected renamed to src/test/expected/allocation/expected

@@ -3,7 +3,7 @@ array 'y'.0 upper bound in y.0[var_12]: SUCCESS
 array 'y'.0 upper bound in y.0[var_16]: FAILURE
 array 'x'.0 upper bound in x.0[var_3]: SUCCESS
 array 'x'.0 upper bound in x.0[var_5]: SUCCESS
-line 11 assertion failed: y[0] == 1: SUCCESS
-line 12 assertion failed: y[1] == 2: SUCCESS
-line 13 index out of bounds: the length is move _17 but the index is _16: FAILURE
-line 13 assertion failed: y[z] == 3: FAILURE
+line 12 assertion failed: y[0] == 1: SUCCESS
+line 13 assertion failed: y[1] == 2: SUCCESS
+line 14 index out of bounds: the length is move _17 but the index is _16: FAILURE
+line 14 assertion failed: y[z] == 3: FAILURE

src/test/run-make/gotoc-allocation/main.rs renamed to src/test/expected/allocation/main.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// cbmc-flags: --bounds-check
 fn foo(x: [i32; 5]) -> [i32; 2] {
     [x[0], x[1]]
 }

src/test/run-make/gotoc-array/expected renamed to src/test/expected/array/expected

@@ -0,0 +1,7 @@
+resume instruction: SUCCESS
+line 22 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
+line 22 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
+line 22 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
+line 27 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
+line 27 assertion failed: original_num + 12 == num: SUCCESS
+line 27 arithmetic overflow on signed + in var_18 + 12: SUCCESS

src/test/run-make/gotoc-array/main.rs renamed to src/test/expected/array/main.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// cbmc-flags: --signed-overflow-check
 fn call_with_one<F>(mut some_closure: F) -> ()
     where
         F: FnMut(i64, i64) -> (),

src/test/run-make/gotoc-assert-eq/expected renamed to src/test/expected/assert-eq/expected

@@ -0,0 +1,6 @@
+line 28 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
+line 28 arithmetic overflow on unsigned + in self->len + 1: SUCCESS
+line 58 assertion failed: a.is_some(): FAILURE
+line 59 assertion failed: a.is_none(): FAILURE
+line 61 assertion failed: b.is_some(): SUCCESS
+line 62 assertion failed: b.is_none(): FAILURE

src/test/run-make/gotoc-assert-eq/main.rs renamed to src/test/expected/assert-eq/main.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// cbmc-flags: --unsigned-overflow-check
 use std::collections::HashMap;
 use std::hash::Hash;
 use std::collections::hash_map::RandomState;