Merge pull request #5625 from tautschnig/cleanup-vs-action

GitHub actions: Make all Windows checks consistent

Author: tautschnig

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

@@ -9,7 +9,7 @@ jobs:
     steps:
       - uses: actions/checkout@v2
         with:
-          submodules: true
+          submodules: recursive
       - name: Fetch dependencies
         env:
           # This is needed in addition to -yq to prevent apt-get from asking for
@@ -59,7 +59,7 @@ jobs:
     steps:
       - uses: actions/checkout@v2
         with:
-          submodules: true
+          submodules: recursive
       - name: Fetch dependencies
         env:
           # This is needed in addition to -yq to prevent apt-get from asking for
@@ -103,7 +103,7 @@ jobs:
     steps:
       - uses: actions/checkout@v2
         with:
-          submodules: true
+          submodules: recursive
       - name: Fetch dependencies
         run: brew install maven flex bison parallel ccache
       - name: Prepare ccache
@@ -143,7 +143,7 @@ jobs:
     steps:
       - uses: actions/checkout@v2
         with:
-          submodules: true
+          submodules: recursive
       - name: Fetch dependencies
         run: brew install cmake ninja maven flex bison ccache
       - name: Prepare ccache
@@ -175,36 +175,48 @@ jobs:
   check-vs-2019-build-and-test:
     runs-on: windows-2019
     env:
-      SCRIPT_DIR: .github/workflows/vs2019
+      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
     steps:
-      - name: Checkout the repository
-        uses: actions/checkout@v2
+      - uses: actions/checkout@v2
         with:
           submodules: recursive
-
-      - name: Install bison and flex
-        run: "${{env.SCRIPT_DIR}}\\install-bison.bat"
-
-      - name: Install z3
+      - name: Fetch dependencies
         run: |
-          Invoke-WebRequest "https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-win.zip" -OutFile z3.zip
-          Expand-Archive z3.zip
-          # We need Get-ChildItem.Name here because the path includes
-          # the z3 version number, which we expect to change.
-          echo "$(Get-Location)\z3\$((Get-ChildItem z3).Name)" >> $env:GITHUB_PATH
-
-      - name: Build cbmc
-        run: "${{env.SCRIPT_DIR}}\\build-cbmc.bat"
-
+          choco install winflexbison3
+          nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
+          echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
+      - name: Setup Visual Studio environment
+        uses: microsoft/[email protected]
+      - name: Prepare ccache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-msbuild-${{ github.ref }}-${{ github.sha }}
+          restore-keys: |
+            ${{ runner.os }}-msbuild-${{ github.ref }}
+            ${{ runner.os }}-msbuild
+      - name: ccache environment
+        run: |
+          echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
+          echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
+      - name: Configure with cmake
+        run: cmake -S . -B build
+      - name: Build Release
+        run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
+      - name: Print ccache stats
+        run: clcache -s
+      - uses: ilammy/[email protected]
       - name: Test cbmc
-        run: "${{env.SCRIPT_DIR}}\\run-tests.bat"
+        run: |
+          Set-Location build
+          ctest -V -L CORE -C Release . -j2
 
   check-clang-format:
     runs-on: ubuntu-20.04
     steps:
       - uses: actions/checkout@v2
         with:
-          submodules: true
+          submodules: recursive
           fetch-depth: 0
       - name: Fetch dependencies
         env:
@@ -224,7 +236,7 @@ jobs:
     steps:
       - uses: actions/checkout@v2
         with:
-          submodules: true
+          submodules: recursive
           fetch-depth: 0
       - name: Fetch dependencies
         env:
@@ -239,7 +251,6 @@ jobs:
           MERGE_BRANCH: ${{ github.ref }}
         run: ./.github/workflows/pull-request-check-cpplint.sh
 
-  # I just added this to check if my stuff is working on github actions
   windows-msi-package:
     runs-on: windows-2019
     env:
@@ -253,7 +264,8 @@ jobs:
           choco install winflexbison3
           nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
           echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
-      - uses: microsoft/[email protected]
+      - name: Setup Visual Studio environment
+        uses: microsoft/[email protected]
       - name: Prepare ccache
         uses: actions/cache@v2
         with:
@@ -267,14 +279,9 @@ jobs:
           echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
           echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
       - name: Configure with cmake
-        run: |
-          New-Item -ItemType Directory -Path build
-          Set-Location build
-          cmake ..
+        run: cmake -S . -B build
       - name: Build Release
-        run: |
-          Set-Location build
-          cmake --build . --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
+        run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
       - name: Print ccache stats
         run: clcache -s
       - name: Create packages

.github/workflows/release-packages.yaml

@@ -144,10 +144,10 @@ jobs:
           choco install winflexbison3
           nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
           echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
-      - uses: microsoft/[email protected]
-        name: Setup Visual Studio environment
+      - name: Setup Visual Studio environment
+        uses: microsoft/[email protected]
       - name: Setup code sign environment
-        run: | 
+        run: |
           echo "$(Split-Path -Path $(Get-ChildItem -Path ${env:ProgramFiles(x86)} -Recurse -Filter 'signtool.exe' | Where-Object FullName -like '*10.0.19041.0\x64\signtool.exe').FullName)" >> $env:GITHUB_PATH
           echo "pfxcert=$([string](Get-Location)+'\CodeSignCertificate.pfx')" >> $env:GITHUB_ENV
       - name: Prepare ccache
@@ -163,18 +163,15 @@ jobs:
           echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
           echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
       - name: Configure with cmake
-        run: |
-          New-Item -ItemType Directory -Path build
-          Set-Location build
-          cmake ..
+        run: cmake -S . -B build
       - name: Build Release
-        run: |
-          Set-Location build
-          cmake --build . --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
+        run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
       - name: Print ccache stats
         run: clcache -s
       - name: Create packages
         id: create_packages
+        # We need to get the path to cpack because fascinatingly,
+        # chocolatey also includes a command called "cpack" which takes precedence
         run: |
           Set-Location build
           $cpack = "$(Split-Path -Parent (Get-Command cmake).Source)\cpack.exe"

.github/workflows/vs2019/build-cbmc.bat

@@ -3,7 +3,7 @@
 JBMC_PATH=$1
 shift
 
-JQ_COMMAND=$1
+JQ_FILTER_FILE=$1
 shift
 
-$JBMC_PATH "$@" | jq -c "$JQ_COMMAND"
+$JBMC_PATH "$@" | jq -c -f $JQ_FILTER_FILE

.github/workflows/vs2019/install-bison.bat

@@ -0,0 +1 @@
+.[] | select(has("result")) | .result | .[] | select(has("trace")) | .trace | .[] | select(has("value")) | .value | select(.name == "pointer") | {has_data: has("data")}

.github/workflows/vs2019/run-tests.bat

@@ -1,6 +1,6 @@
 CORE
 test
-'.[] | select(has("result")) | .result | .[] | select(has("trace")) | .trace | .[] | select(has("value")) | .value | select(.name == "pointer") | {has_data: has("data")}' --json-ui --trace
+filter.jq --json-ui --trace
 ^EXIT=0$
 ^SIGNAL=0$
 \{"has_data":true\}

jbmc/regression/jbmc-json-ui/chain.sh

@@ -24,17 +24,11 @@ add_test_pl_profile(
     "CORE"
 )
 
+# solver appears on the PATH in Windows already
 if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
   set_property(
     TEST "cbmc-cprover-smt2-CORE"
     PROPERTY ENVIRONMENT
       "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
   )
-else()
-  string(REPLACE ";" "\\;" path_value "$ENV{PATH}")
-  set_property(
-    TEST "cbmc-cprover-smt2-CORE"
-    PROPERTY ENVIRONMENT
-      "PATH=${path_value}\;$<TARGET_FILE_DIR:smt2_solver>"
-  )
 endif()

jbmc/regression/jbmc-json-ui/pointer-simplification/filter.jq

@@ -11,49 +11,48 @@
 test_base_dir = os.path.abspath(os.path.join(this_script_dir, '..', 'cbmc'))
 
 # some tests in the cbmc suite don't work for the trace checks for one reason or another
-ExcludedTests = list(map(lambda s: os.path.join(test_base_dir, s), [
+ExcludedTests = list(map(lambda s: os.path.join(test_base_dir, s[0], s[1]), [
     # these tests expect input from stdin
-    'json-interface1/test_wrong_option.desc',
-    'json-interface1/test.desc',
-    'json-interface1/test_wrong_flag.desc',
-    'xml-interface1/test_wrong_option.desc',
-    'xml-interface1/test.desc',
-    'xml-interface1/test_wrong_flag.desc',
+    ['json-interface1', 'test_wrong_option.desc'],
+    ['json-interface1', 'test.desc'],
+    ['json-interface1', 'test_wrong_flag.desc'],
+    ['xml-interface1', 'test_wrong_option.desc'],
+    ['xml-interface1', 'test.desc'],
+    ['xml-interface1', 'test_wrong_flag.desc'],
     # these want --show-goto-functions instead of producing a trace
-    'destructors/compound_literal.desc',
-    'destructors/enter_lexical_block.desc',
-    'reachability-slice-interproc2/test.desc',
+    ['destructors', 'compound_literal.desc'],
+    ['destructors', 'enter_lexical_block.desc'],
+    ['reachability-slice-interproc2', 'test.desc'],
     # this one wants show-properties instead producing a trace
-    'show_properties1/test.desc',
+    ['show_properties1', 'test.desc'],
     # program-only instead of trace
-    'vla1/program-only.desc',
-    'Quantifiers-simplify/simplify_not_forall.desc',
-    # this one doesn't work for me locally at all
-    # 'integer-assignments1/test.desc',
+    ['vla1', 'program-only.desc'],
+    ['Quantifiers-simplify', 'simplify_not_forall.desc'],
     # these test for invalid command line handling
-    'bad_option/test_multiple.desc',
-    'bad_option/test.desc',
-    'unknown-argument-suggestion/test.desc',
+    ['bad_option', 'test_multiple.desc'],
+    ['bad_option', 'test.desc'],
+    ['unknown-argument-suggestion', 'test.desc'],
     # this one produces XML intermingled with main XML output when used with --xml-ui
-    'graphml_witness2/test.desc',
+    ['graphml_witness2', 'test.desc'],
     # produces intermingled XML on the command line
-    'coverage_report1/test.desc',
-    'coverage_report1/paths.desc',
-    'graphml_witness1/test.desc',
-    'switch8/program-only.desc',
+    ['coverage_report1', 'test.desc'],
+    ['coverage_report1', 'paths.desc'],
+    ['graphml_witness1', 'test.desc'],
+    ['switch8', 'program-only.desc'],
     # this uses json-ui (fails for a different reason actually, but should also
     #   fail because of command line incompatibility)
-    'json1/test.desc',
+    ['json1', 'test.desc'],
     # uses show-goto-functions
-    'reachability-slice/test.desc',
-    'reachability-slice/test2.desc',
-    'reachability-slice/test3.desc',
-    'reachability-slice-interproc/test.desc',
-    'unsigned1/test.desc',
-    'reachability-slice-interproc3/test.desc',
-    'sync_lock_release-1/symbol_per_type.desc',
-    # this test is marked broken-smt-backend and doesn't work for me locally
-    'integer-assignments1/test.desc'
+    ['reachability-slice', 'test.desc'],
+    ['reachability-slice', 'test2.desc'],
+    ['reachability-slice', 'test3.desc'],
+    ['reachability-slice-interproc', 'test.desc'],
+    ['unsigned1', 'test.desc'],
+    ['reachability-slice-interproc3', 'test.desc'],
+    ['sync_lock_release-1', 'symbol_per_type.desc'],
+    # this test is marked smt-backend, and would thus fail as we run tests with
+    # the SAT back-end only
+    ['integer-assignments1', 'test.desc']
 ]))
 
 # TODO maybe consider looking them up on PATH, but direct paths are