Fix symtab json file removal and reduce regression scope (#2447)

This fixes a regression introduced in #2439 when write symtab json is enabled. We still need to take that into consideration and remove them if needed. This change also simplifies the write symtab json regression to avoid the out of disk space issue we've been seeing since #2439.
model-checking · May 17, 2023 · 3d05d3f · 3d05d3f
1 parent 2df67e3
commit 3d05d3f
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 19 deletions.
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
@@ -45,12 +45,14 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani
-        run: cargo build-dev
+        run: cargo build-dev -- --features write_json_symtab
+
+      - name: Run tests
+        run: |
+          cargo run -p compiletest --quiet -- --suite kani --mode kani --quiet --no-fail-fast
+          cargo run -p compiletest --quiet -- --suite expected --mode expected --quiet --no-fail-fast
+          cargo run -p compiletest --quiet -- --suite cargo-kani --mode cargo-kani --quiet --no-fail-fast
 
-      - name: Execute Kani regression
-        env:
-          KANI_ENABLE_WRITE_JSON_SYMTAB: 1
-        run: ./scripts/kani-regression.sh
 
   benchcomp-tests:
     runs-on: ubuntu-20.04

diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
@@ -129,12 +129,12 @@ impl Project {
                 let goto = Artifact::try_new(&goto_path, Goto)?;
 
                 // All other harness artifacts that may have been generated as part of the build.
-                artifacts.extend([TypeMap, VTableRestriction, PrettyNameMap].iter().filter_map(
-                    |typ| {
+                artifacts.extend(
+                    [SymTab, TypeMap, VTableRestriction, PrettyNameMap].iter().filter_map(|typ| {
                         let artifact = Artifact::try_from(&symtab_out, *typ).ok()?;
                         Some(artifact)
-                    },
-                ));
+                    }),
+                );
                 artifacts.push(symtab_out);
                 artifacts.push(goto);
             }

diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
@@ -27,11 +27,7 @@ check_kissat_version.sh
 ${SCRIPT_DIR}/kani-fmt.sh --check
 
 # Build all packages in the workspace
-if [[ "" != "${KANI_ENABLE_WRITE_JSON_SYMTAB-}" ]]; then
-  cargo build-dev -- --features write_json_symtab
-else
-  cargo build-dev
-fi
+cargo build-dev
 
 # Unit tests
 cargo test -p cprover_bindings
@@ -69,11 +65,8 @@ for testp in "${TESTS[@]}"; do
       --quiet --no-fail-fast
 done
 
-# Don't run std regression if using JSON symtab to avoid OOM issues.
-if [[ -z "${KANI_ENABLE_WRITE_JSON_SYMTAB-}" ]]; then
-    # Check codegen for the standard library
-    time "$SCRIPT_DIR"/std-lib-regression.sh
-fi
+# Check codegen for the standard library
+time "$SCRIPT_DIR"/std-lib-regression.sh
 
 # We rarely benefit from re-using build artifacts in the firecracker test,
 # and we often end up with incompatible leftover artifacts: