Merge pull request #5958 from tautschnig/test-thorough

Run KNOWNBUG and THOROUGH regression tests in CI

Author: tautschnig

.github/workflows/pull-request-checks.yaml

@@ -170,6 +170,90 @@ jobs:
       - name: Run tests
         run: cd build; ctest . -V -L CORE -j2
 
+  check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
+      - name: Prepare ccache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-20.04-Release-${{ github.ref }}
+            ${{ runner.os }}-20.04-Release
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -H. -Bbuild -G Ninja
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j2
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run tests
+        run: |
+          cd build
+          ctest . -V -L KNOWNBUG -j2
+          export PATH=$PWD/bin:$PATH
+          cd ../regression/cbmc
+          sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
+          # the following test fails on some Unix systems
+          git checkout -- r_w_ok6
+          # the following tests fail on Windows only
+          git checkout -- memory_allocation1 printf1 union12 va_list3
+          ../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K
+
+  check-ubuntu-20_04-cmake-gcc-THOROUGH:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
+      - name: Prepare ccache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-20.04-Release-${{ github.ref }}
+            ${{ runner.os }}-20.04-Release
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -H. -Bbuild -G Ninja
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j2
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run tests
+        run: cd build; ctest . -V -L THOROUGH -j2
+
   check-macos-10_15-make-clang:
     runs-on: macos-10.15
     steps:

jbmc/regression/jbmc-strings/VerifStringLastIndexOf/Test.class

@@ -19,6 +19,8 @@ public int referenceLastIndexOf(String s, char ch, int fromIndex) {
   }
 
   public int check(String s, char ch, int fromIndex) {
+    if(s.length() <= fromIndex)
+      return -1;
     int reference = referenceLastIndexOf(s, ch, fromIndex);
     int jbmc_result = s.lastIndexOf(ch, fromIndex);
     assert(reference == jbmc_result);

jbmc/regression/jbmc-strings/VerifStringLastIndexOf/Test.java

@@ -1,7 +1,6 @@
 THOROUGH
 Test
---function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null
-^EXIT=10$
+--function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+VERIFICATION SUCCESSFUL
+^EXIT=0$
 ^SIGNAL=0$
-assertion at file Test.java line 32 .* SUCCESS$
-assertion at file Test.java line 34 .* FAILURE$

jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 test
---max-nondet-string-length 20
+--function test.main --max-nondet-string-length 20  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_format5/test.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test2
---max-nondet-string-length 1000 --function Test2.main
+--max-nondet-string-length 1000 --function Test2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string/test2.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test3
---max-nondet-string-length 1000 --function Test3.main
+--max-nondet-string-length 1000 --function Test3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string/test3.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test4
---max-nondet-string-length 1000 --function Test4.main
+--max-nondet-string-length 1000 --function Test4.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string/test4.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test_binary1
---max-nondet-string-length 1000 --function Test_binary1.main
+--max-nondet-string-length 1000 --function Test_binary1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test_binary2
---max-nondet-string-length 1000 --function Test_binary2.main
+--max-nondet-string-length 1000 --function Test_binary2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test_binary3
---max-nondet-string-length 1000 --function Test_binary3.main
+--max-nondet-string-length 1000 --function Test_binary3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc

@@ -1,6 +1,6 @@
 THOROUGH
 test
---max-nondet-string-length 1000 --function test.check
+--max-nondet-string-length 1000 --function test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* test.java line 8 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_value_of_float_4/test.desc

@@ -1,6 +1,6 @@
-THOROUGH
+KNOWNBUG
 test
---max-nondet-string-length 1000 --function test.check
+--max-nondet-string-length 1000 --function test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 6 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_value_of_float_5/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$
-^\[main.coverage.2\] file main.c line 11 function main block 2.*: SATISFIED$
+^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
 ^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$
 ^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$

regression/cbmc-cover/location15/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main\.assertion\.1\] assertion sizeof\(ull\) != sizeof\(unsigned int\) && pop4\(ull\) == __builtin_popcount\(ull\): FAILURE$
+\[main\.assertion\.\d+\] line 39 assertion sizeof\(ull\) != sizeof\(unsigned int\) && pop4\(ull\) == __builtin_popcount\(ull\): FAILURE$
 ^\*\* 1 of 3 failed
 --
 ^warning: ignoring

regression/cbmc/gcc_popcount2/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww000.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww000_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww000.c
 POWER ALL
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww000_POWER_ALL/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww000.c
 POWER OPC
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww000_POWER_OPC/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww000.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww000_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww001.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww001_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww001.c
 POWER OPC
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww001_POWER_OPC/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww001.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww001_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww002.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww002_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww002.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww002_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww003.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww003_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww003.c
 POWER ALL
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww003_POWER_ALL/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww003.c
 POWER OPC
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww003_POWER_OPC/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww003.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww003_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww004.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww004_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww004.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww004_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww005.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww005_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww005.c
 POWER ALL
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww005_POWER_ALL/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww005.c
 POWER OPC
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww005_POWER_OPC/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww005.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww005_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww006.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww006_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww006.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww006_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww007.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww007_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww007.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww007_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww009.c
 CAV11 SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww009_CAV11_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww009.c
 POWER ALL
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww009_POWER_ALL/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww009.c
 POWER OPC
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww009_POWER_OPC/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwdww009.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwdww009_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwsww000.c
 CAV11 ERROR
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwsww000_CAV11_ERROR/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 bclwsww000.c
 SC SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_bclwsww000_SC_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 iriw+addrs.c
 CAV11 SAFE
 ^EXIT=10$

regression/goto-instrument-wmm-core/ppc_iriw+addrs_CAV11_SAFE/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+KNOWNBUG
 iriw+addrs.c
 POWER OPC
 ^EXIT=10$