Mark performance regressions as ignored for now

and enable them to be executed as part of CBMC nightly
model-checking · Mar 8, 2023 · 4d3bed2 · 4d3bed2
1 parent 657ddda
commit 4d3bed2
Show file tree

Hide file tree

Showing 11 changed files with 17 additions and 14 deletions.
diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml
@@ -89,3 +89,8 @@ jobs:
       - name: Execute Kani performance tests
         working-directory: ./kani
         run: ./scripts/kani-perf.sh
+
+      - name: Execute Kani performance ignored tests
+        working-directory: ./kani
+        continue-on-error: true
+        run: cargo run -p compiletest -- --suite perf --mode cargo-kani-test ignore --ignored
diff --git a/tests/perf/btreeset/insert_same/Cargo.toml → ...rf/btreeset/ignore_insert_same/Cargo.toml b/tests/perf/btreeset/insert_same/Cargo.toml → ...rf/btreeset/ignore_insert_same/Cargo.toml
diff --git a/tests/perf/btreeset/insert_same/expected → ...perf/btreeset/ignore_insert_same/expected b/tests/perf/btreeset/insert_same/expected → ...perf/btreeset/ignore_insert_same/expected
diff --git a/tests/perf/btreeset/insert_same/src/main.rs → ...f/btreeset/ignore_insert_same/src/main.rs b/tests/perf/btreeset/insert_same/src/main.rs → ...f/btreeset/ignore_insert_same/src/main.rs
diff --git a/tests/perf/vec/string/Cargo.toml → tests/perf/vec/ignore_string/Cargo.toml b/tests/perf/vec/string/Cargo.toml → tests/perf/vec/ignore_string/Cargo.toml
diff --git a/tests/perf/vec/box_dyn/Cargo.toml → ...perf/vec/ignore_string/box_dyn/Cargo.toml b/tests/perf/vec/box_dyn/Cargo.toml → ...perf/vec/ignore_string/box_dyn/Cargo.toml
diff --git a/tests/perf/vec/box_dyn/expected → ...s/perf/vec/ignore_string/box_dyn/expected b/tests/perf/vec/box_dyn/expected → ...s/perf/vec/ignore_string/box_dyn/expected
diff --git a/tests/perf/vec/box_dyn/src/main.rs → ...erf/vec/ignore_string/box_dyn/src/main.rs b/tests/perf/vec/box_dyn/src/main.rs → ...erf/vec/ignore_string/box_dyn/src/main.rs
diff --git a/tests/perf/vec/string/expected → tests/perf/vec/ignore_string/expected b/tests/perf/vec/string/expected → tests/perf/vec/ignore_string/expected
diff --git a/tests/perf/vec/string/src/main.rs → tests/perf/vec/ignore_string/src/main.rs b/tests/perf/vec/string/src/main.rs → tests/perf/vec/ignore_string/src/main.rs
diff --git a/tools/compiletest/src/header.rs b/tools/compiletest/src/header.rs
@@ -180,21 +180,17 @@ pub fn make_test_description<R: Read>(
     path: &Path,
     src: R,
 ) -> test::TestDesc {
-    let mut ignore = false;
     let mut should_fail = false;
-    let mut ignore_message = None;
 
-    if config.mode == Mode::Kani || config.mode == Mode::Stub {
-        // If the path to the test contains "fixme" or "ignore", skip it.
-        let file_path = path.to_str().unwrap();
-        (ignore, ignore_message) = if file_path.contains("fixme") {
-            (true, Some("fixme test"))
-        } else if file_path.contains("ignore") {
-            (true, Some("ignore test"))
-        } else {
-            (false, None)
-        };
-    }
+    // If the path to the test contains "fixme" or "ignore", skip it.
+    let file_path = path.to_str().unwrap();
+    let (mut ignore, mut ignore_message) = if file_path.contains("fixme") {
+        (true, Some("fixme test"))
+    } else if file_path.contains("ignore") {
+        (true, Some("ignore test"))
+    } else {
+        (false, None)
+    };
 
     // The `KaniFixme` mode runs tests that are ignored in the `kani` suite
     if config.mode == Mode::KaniFixme {
@@ -207,8 +203,10 @@ pub fn make_test_description<R: Read>(
 
         // If the base name does NOT contain "fixme" or "ignore", we skip it.
         // All "fixme" tests are expected to fail
-        (ignore, ignore_message) = if base_name.contains("fixme") || base_name.contains("ignore") {
+        (ignore, ignore_message) = if base_name.contains("fixme") {
             (false, None)
+        } else if base_name.contains("ignore") {
+            (true, Some("ignore test"))
         } else {
             (true, Some("regular test"))
         };