From ffc784aebc55ebbf82622d172dd52a7133b56b3f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Mar 2026 12:31:01 +0000 Subject: [PATCH 1/3] Upgrade cvc5 from 1.2.1 to 1.3.4 cvc5 1.3.4 (released 2026-05-07) is the latest patch on the 1.3 line. The previous pin (1.2.1) was the last of the 1.2.x line, so this bump skips 1.3.0/1.3.1/1.3.2/1.3.3. Notable user-visible changes from upstream release notes since 1.2.1: - 1.3.0: behavioural change -- distinct constraints are now handled lazily; this can shift solving times in either direction on adversarial inputs and is the most likely source of any future performance bisect to land on this commit. - 1.3.2: variable-elimination fix for quantified formulas with variable shadowing; arithmetic-solver updates. - 1.3.3: get-assertions no longer clears solving state; SyGuS fix for unconstrained queries; minor non-linear arithmetic strategy tweak. - 1.3.4: soundness fix in the --learned-rewrite preprocessing pass; SymFPU divider-encoding fix that closes upstream cvc5 issues #9505 / #11139 / #12335 (we already carry a marker for #11139 at regression/smt2_solver/fp-issues/cvc5-11139 -fma.smt2); parser fixes for indexed bit-vector operators of width >= 2^32; theory-combination fixes for arrays + non- linear arithmetic. cvc5 1.3.4 raises its build-time toolchain minimum (GCC >= 10 / Clang >= 12), but we only consume the prebuilt static binaries so this does not affect us. All five binary assets we depend on (Linux x86_64/arm64, macOS x86_64/arm64, Windows x86_64 static zips) are published on the cvc5-1.3.4 release. CI exercises the new binary via the cvc5 regression suites under regression/cbmc-incr-smt2/ and regression/cbmc-output-file/dump -smt-formula/ on every run. Co-authored-by: Kiro --- .github/workflows/coverage.yaml | 2 +- .github/workflows/pull-request-checks.yaml | 2 +- .github/workflows/release-packages.yaml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/coverage.yaml b/.github/workflows/coverage.yaml index 146f0be5080..ade803fb611 100644 --- a/.github/workflows/coverage.yaml +++ b/.github/workflows/coverage.yaml @@ -5,7 +5,7 @@ on: pull_request: branches: [ develop ] env: - cvc5-version: "1.2.1" + cvc5-version: "1.3.4" linux-vcpus: 4 windows-vcpus: 4 diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 40f51832aeb..8ff462a83b6 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -5,7 +5,7 @@ on: pull_request: branches: [ develop ] env: - cvc5-version: "1.2.1" + cvc5-version: "1.3.4" linux-vcpus: 4 windows-vcpus: 4 diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml index e412dc62464..f19276ae769 100644 --- a/.github/workflows/release-packages.yaml +++ b/.github/workflows/release-packages.yaml @@ -2,7 +2,7 @@ on: release: types: [created] env: - cvc5-version: "1.2.1" + cvc5-version: "1.3.4" name: Upload additional release assets jobs: From a7c26bae8807e9382b6f0b7195bfb1957b300e00 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 24 May 2026 22:43:59 +0000 Subject: [PATCH 2/3] CI: extract cvc5 / Z3 install steps into reusable composite actions The cvc5 download-and-install snippet was duplicated 14 times across .github/workflows/{pull-request-checks,coverage,release-packages}.yaml, with only the asset filename varying by runner platform. The Z3 download was duplicated twice in the two Windows jobs of pull-request-checks.yaml, hard-coded to z3-4.8.10 from 2021. With the inline form a future cvc5 bump touched 14 places verbatim and a Z3 bump touched 2 places verbatim. This commit introduces two composite actions: - .github/actions/install-cvc5 -- handles all five supported runner platforms (Linux x86_64/arm64, macOS x86_64/arm64, Windows x86_64) by dispatching on runner.os / runner.arch. The Linux/macOS branch uses bash + wget + unzip; the Windows branch uses pwsh + Invoke-WebRequest + Expand-Archive and appends to $env:GITHUB_PATH so the binary is discoverable in subsequent steps. Both branches verify the install with `cvc5 --version` (Windows uses an absolute path because the PATH update only takes effect from the next step onward). - .github/actions/install-z3 -- Windows-only (Linux installs Z3 via apt and macOS via brew, neither requires a separate version pin). Mirrors the cvc5 action's Windows branch. The 16 existing inline blocks (10 in pull-request-checks.yaml, 1 in coverage.yaml, 3 in release-packages.yaml, plus 2 Z3 blocks inside the Windows jobs of pull-request-checks.yaml) are replaced with `uses:` references that read the new env.cvc5-version / env.z3-version variables. A future bump is now one literal change per workflow (and pulls in any improvements to the install-cvc5 / install-z3 actions for free). The refactor is behaviour-preserving: - same upstream URL pattern for both binaries; - same install location (/usr/local/bin on Linux/macOS, C:\tools on Windows); - same PATH update strategy on Windows; - same `cvc5 --version` / `z3 --version` self-check. actionlint reports no new warnings introduced by this change (pre-existing save-always and shellcheck SC2086 warnings on unrelated steps are unchanged in count). Co-authored-by: Kiro --- .github/actions/install-cvc5/action.yaml | 55 +++++++++ .github/actions/install-z3/action.yaml | 43 +++++++ .github/workflows/coverage.yaml | 10 +- .github/workflows/pull-request-checks.yaml | 133 +++++++++------------ .github/workflows/release-packages.yaml | 30 ++--- 5 files changed, 171 insertions(+), 100 deletions(-) create mode 100644 .github/actions/install-cvc5/action.yaml create mode 100644 .github/actions/install-z3/action.yaml diff --git a/.github/actions/install-cvc5/action.yaml b/.github/actions/install-cvc5/action.yaml new file mode 100644 index 00000000000..a2c66ceea73 --- /dev/null +++ b/.github/actions/install-cvc5/action.yaml @@ -0,0 +1,55 @@ +name: 'Install cvc5' +description: | + Download and install a static cvc5 release binary, auto-detecting the + runner platform from runner.os and runner.arch. Supported runners: + Linux (x86_64, arm64), macOS (x86_64, arm64), Windows (x86_64). + + After this action runs, `cvc5` is on PATH for subsequent steps. Note + that on Windows the PATH update only takes effect from the *next* + step onward (a GitHub Actions limitation of $env:GITHUB_PATH); the + action verifies the binary in-place via its absolute path. + +inputs: + version: + description: 'cvc5 version (without the "cvc5-" tag prefix), e.g. 1.3.4' + required: true + +runs: + using: composite + steps: + - name: Install cvc5 (Linux / macOS) + if: runner.os != 'Windows' + shell: bash + run: | + set -euo pipefail + case "${{ runner.os }}-${{ runner.arch }}" in + Linux-X64) asset=cvc5-Linux-x86_64-static ;; + Linux-ARM64) asset=cvc5-Linux-arm64-static ;; + macOS-X64) asset=cvc5-macOS-x86_64-static ;; + macOS-ARM64) asset=cvc5-macOS-arm64-static ;; + *) + echo "::error ::install-cvc5 does not support ${{ runner.os }}-${{ runner.arch }}" + exit 1 + ;; + esac + url="https://github.com/cvc5/cvc5/releases/download/cvc5-${{ inputs.version }}/${asset}.zip" + wget --quiet "${url}" + unzip -j -d /usr/local/bin "${asset}.zip" "${asset}/bin/cvc5" + rm "${asset}.zip" + cvc5 --version + + - name: Install cvc5 (Windows) + if: runner.os == 'Windows' + shell: pwsh + run: | + $ErrorActionPreference = 'Stop' + $asset = 'cvc5-Win64-x86_64-static' + $url = "https://github.com/cvc5/cvc5/releases/download/cvc5-${{ inputs.version }}/$asset.zip" + Invoke-WebRequest -Uri $url -OutFile ".\$asset.zip" + New-Item -ItemType Directory -Force -Path 'C:\tools\cvc5' | Out-Null + Expand-Archive -LiteralPath ".\$asset.zip" -DestinationPath '.\cvc5-extract' -Force + Move-Item -Force ".\cvc5-extract\$asset\bin\cvc5.exe" 'C:\tools\cvc5\cvc5.exe' + Remove-Item -Recurse -Force '.\cvc5-extract' + Remove-Item ".\$asset.zip" + echo 'C:\tools\cvc5' >> $env:GITHUB_PATH + & 'C:\tools\cvc5\cvc5.exe' --version diff --git a/.github/actions/install-z3/action.yaml b/.github/actions/install-z3/action.yaml new file mode 100644 index 00000000000..8d725f1effd --- /dev/null +++ b/.github/actions/install-z3/action.yaml @@ -0,0 +1,43 @@ +name: 'Install Z3 (Windows)' +description: | + Download and install a Z3 release binary on a Windows runner. After + this action runs, `z3` is on PATH for subsequent steps (the PATH + update only takes effect from the next step onward; the action + verifies the binary in-place via its absolute path). + + Linux and macOS runners install Z3 via the system package manager + (apt / brew) elsewhere in the workflow; this action only covers + Windows, which has no comparable distribution channel and therefore + needs an explicit version pin. + +inputs: + version: + description: 'Z3 version, e.g. 4.8.10' + required: true + arch: + description: 'Architecture suffix used in the upstream asset name' + required: false + default: 'x64-win' + +runs: + using: composite + steps: + - name: Install Z3 (Windows) + if: runner.os == 'Windows' + shell: pwsh + run: | + $ErrorActionPreference = 'Stop' + $name = "z3-${{ inputs.version }}-${{ inputs.arch }}" + $url = "https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/$name.zip" + Invoke-WebRequest -Uri $url -OutFile '.\z3.zip' + Expand-Archive -LiteralPath '.\z3.zip' -DestinationPath 'C:\tools' -Force + Remove-Item '.\z3.zip' + echo "C:\tools\$name\bin" >> $env:GITHUB_PATH + & "C:\tools\$name\bin\z3.exe" --version + + - name: install-z3 is currently Windows-only + if: runner.os != 'Windows' + shell: bash + run: | + echo "::error ::install-z3 currently only supports Windows; install Z3 via apt (Linux) or brew (macOS) directly" + exit 1 diff --git a/.github/workflows/coverage.yaml b/.github/workflows/coverage.yaml index ade803fb611..e4a71b5b452 100644 --- a/.github/workflows/coverage.yaml +++ b/.github/workflows/coverage.yaml @@ -34,12 +34,10 @@ jobs: sudo apt-get install --no-install-recommends -y g++ gcc gdb binutils flex bison cmake maven jq libxml2-utils openjdk-11-jdk-headless lcov ccache z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 8ff462a83b6..9acda5bb1ed 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -6,6 +6,7 @@ on: branches: [ develop ] env: cvc5-version: "1.3.4" + z3-version: "4.8.10" linux-vcpus: 4 windows-vcpus: 4 @@ -27,12 +28,10 @@ jobs: sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -114,12 +113,10 @@ jobs: cpanm Thread::Pool::Simple - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -225,12 +222,10 @@ jobs: sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -304,12 +299,10 @@ jobs: cpanm Thread::Pool::Simple - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -371,12 +364,10 @@ jobs: sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -431,12 +422,10 @@ jobs: sudo ln -sf cpp-14 /usr/bin/cpp - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -478,12 +467,10 @@ jobs: sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-arm64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-arm64-static.zip cvc5-Linux-arm64-static/bin/cvc5 - rm cvc5-Linux-arm64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -532,12 +519,10 @@ jobs: sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils ccache doxygen z3 g++-multilib - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -662,12 +647,10 @@ jobs: brew install flex bison parallel ccache z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc5 binary and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-macOS-x86_64-static.zip cvc5-macOS-x86_64-static/bin/cvc5 - rm cvc5-macOS-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -716,12 +699,10 @@ jobs: run: brew install ninja maven flex bison ccache z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc5 binary and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS-arm64-static.zip - unzip -j -d /usr/local/bin cvc5-macOS-arm64-static.zip cvc5-macOS-arm64-static/bin/cvc5 - rm cvc5-macOS-arm64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -790,14 +771,14 @@ jobs: Require-Tool win_bison nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0 echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH - Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip - Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools - echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH - New-Item -ItemType directory "C:\tools\cvc5" - Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-x86_64-static.zip -OutFile .\cvc5-Win64-x86_64-static.zip - Expand-Archive -LiteralPath '.\cvc5-Win64-x86_64-static.Zip' - Move-Item -Path .\cvc5-Win64-x86_64-static\cvc5-Win64-x86_64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe - echo "c:\tools\cvc5;" >> $env:GITHUB_PATH + - name: Install Z3 + uses: ./.github/actions/install-z3 + with: + version: ${{ env.z3-version }} + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Confirm z3 solver is available and log the version installed run: z3 --version - name: Confirm cvc5 solver is available and log the version installed @@ -875,14 +856,14 @@ jobs: nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0 echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH echo "c:\Strawberry\" >> $env:GITHUB_PATH - Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip - Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools - echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH - New-Item -ItemType directory "C:\tools\cvc5" - Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-x86_64-static.zip -OutFile .\cvc5-Win64-x86_64-static.zip - Expand-Archive -LiteralPath '.\cvc5-Win64-x86_64-static.Zip' - Move-Item -Path .\cvc5-Win64-x86_64-static\cvc5-Win64-x86_64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe - echo "c:\tools\cvc5;" >> $env:GITHUB_PATH + - name: Install Z3 + uses: ./.github/actions/install-z3 + with: + version: ${{ env.z3-version }} + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Confirm z3 solver is available and log the version installed run: z3 --version - name: Confirm cvc5 solver is available and log the version installed diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml index f19276ae769..b5309cf5f61 100644 --- a/.github/workflows/release-packages.yaml +++ b/.github/workflows/release-packages.yaml @@ -20,12 +20,10 @@ jobs: sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -87,12 +85,10 @@ jobs: sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-arm64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-arm64-static.zip cvc5-Linux-arm64-static/bin/cvc5 - rm cvc5-Linux-arm64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: @@ -154,12 +150,10 @@ jobs: sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3 - name: Confirm z3 solver is available and log the version installed run: z3 --version - - name: Download cvc-5 from the releases page and make sure it can be deployed - run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 - rm cvc5-Linux-x86_64-static.zip - cvc5 --version + - name: Install cvc5 + uses: ./.github/actions/install-cvc5 + with: + version: ${{ env.cvc5-version }} - name: Prepare ccache uses: actions/cache@v5 with: From a46825dcd916dd4b0ad77d30d1a836b9517627b4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 24 May 2026 22:46:23 +0000 Subject: [PATCH 3/3] CI: verify SHA-256 of solver binaries downloaded in workflows Until now the install-cvc5 and install-z3 composite actions trusted whatever bytes were served by github.com for a given release tag. That works in practice -- and the tag-based URL is itself a strong hint of integrity -- but it does not catch: - upstream republishing a tag with different content (uncommon for cvc5 / Z3 releases, but observed elsewhere); - a transparent-proxy or mirror compromise on the runner; or - a typo in the version pin that happens to resolve to a different real artifact. This commit pins the expected SHA-256 of every supported (binary, version, platform) tuple inside the composite actions, computes the hash of the downloaded archive, and aborts the step on mismatch *before* unzipping or moving the binary onto PATH. The hashes are hard-coded in a small case statement next to the asset names, so the next bump is mechanically "version + 5 cvc5 hashes (1 z3 hash) in the same PR"; an unknown version is rejected with a pointer to the file to edit. Hashes for cvc5 1.3.4 were obtained from the upstream release API (.assets[].digest) and cross-checked against locally computed sha256sum of the same downloads: cvc5-Linux-x86_64-static.zip dcdbfada0ce493ee98259c0816e0daafc561c223aadb3af298c2968e73ea39c6 cvc5-Linux-arm64-static.zip 2a4c108367f20b0c8990abd6b9535a5d62e08908d471d4671c00734e408f85bc cvc5-macOS-x86_64-static.zip 5a7976affaf37dcf03ee44c3d0297c8e0ba08afd44ac832dab97400da726b852 cvc5-macOS-arm64-static.zip 3840aa53f6ee6fc357415dcfe291d7f5ffec6cfb1ccca6fef64120a0d2be4cb6 cvc5-Win64-x86_64-static.zip 279fe7e95810cfb62433fcfc2932f35325a665f32d3697ff33f75e31d5c6a179 The Z3 4.8.10 release predates the API .digest field, so the hash z3-4.8.10-x64-win.zip 688c8f96f4f89cb474de4ecd740c812c6e695318e4b50fd790722513285b2fcb was computed locally from the upstream artifact. Implementation notes: - On Linux/macOS the verification uses `sha256sum` if available and falls back to `shasum -a 256` (macOS does not ship sha256sum but does ship shasum). - On Windows the verification uses PowerShell's built-in Get-FileHash -Algorithm SHA256. - Inputs to the verification step are passed via `env:` rather than interpolated into the shell script, so an attacker-controlled version string cannot inject shell or PowerShell commands. - The hash table is the single source of truth for both the asset name and the hash, eliminating the previous risk of the two drifting apart. actionlint reports no new warnings introduced by this change. Co-authored-by: Kiro --- .github/actions/install-cvc5/action.yaml | 84 +++++++++++++++++++----- .github/actions/install-z3/action.yaml | 60 +++++++++++++---- 2 files changed, 113 insertions(+), 31 deletions(-) diff --git a/.github/actions/install-cvc5/action.yaml b/.github/actions/install-cvc5/action.yaml index a2c66ceea73..766af064ded 100644 --- a/.github/actions/install-cvc5/action.yaml +++ b/.github/actions/install-cvc5/action.yaml @@ -4,6 +4,14 @@ description: | runner platform from runner.os and runner.arch. Supported runners: Linux (x86_64, arm64), macOS (x86_64, arm64), Windows (x86_64). + Downloaded archives are verified against a hard-coded SHA-256 hash + table embedded in this action; an unknown (version, platform) pair + causes the step to fail. To support a new cvc5 version, append a + row to the case statement in the "Resolve cvc5 asset and hash" step + below. Hashes can be obtained from the GitHub release API: + curl -sL "https://api.github.com/repos/cvc5/cvc5/releases/tags/cvc5-" \ + | jq -r '.assets[] | select(.name | test("static\\.zip$")) | "\(.name) \(.digest)"' + After this action runs, `cvc5` is on PATH for subsequent steps. Note that on Windows the PATH update only takes effect from the *next* step onward (a GitHub Actions limitation of $env:GITHUB_PATH); the @@ -17,39 +25,81 @@ inputs: runs: using: composite steps: - - name: Install cvc5 (Linux / macOS) - if: runner.os != 'Windows' + - name: Resolve cvc5 asset and hash + id: meta shell: bash run: | set -euo pipefail - case "${{ runner.os }}-${{ runner.arch }}" in - Linux-X64) asset=cvc5-Linux-x86_64-static ;; - Linux-ARM64) asset=cvc5-Linux-arm64-static ;; - macOS-X64) asset=cvc5-macOS-x86_64-static ;; - macOS-ARM64) asset=cvc5-macOS-arm64-static ;; + case "${{ inputs.version }}-${{ runner.os }}-${{ runner.arch }}" in + 1.3.4-Linux-X64) + asset=cvc5-Linux-x86_64-static + sha256=dcdbfada0ce493ee98259c0816e0daafc561c223aadb3af298c2968e73ea39c6 ;; + 1.3.4-Linux-ARM64) + asset=cvc5-Linux-arm64-static + sha256=2a4c108367f20b0c8990abd6b9535a5d62e08908d471d4671c00734e408f85bc ;; + 1.3.4-macOS-X64) + asset=cvc5-macOS-x86_64-static + sha256=5a7976affaf37dcf03ee44c3d0297c8e0ba08afd44ac832dab97400da726b852 ;; + 1.3.4-macOS-ARM64) + asset=cvc5-macOS-arm64-static + sha256=3840aa53f6ee6fc357415dcfe291d7f5ffec6cfb1ccca6fef64120a0d2be4cb6 ;; + 1.3.4-Windows-X64) + asset=cvc5-Win64-x86_64-static + sha256=279fe7e95810cfb62433fcfc2932f35325a665f32d3697ff33f75e31d5c6a179 ;; *) - echo "::error ::install-cvc5 does not support ${{ runner.os }}-${{ runner.arch }}" + echo "::error ::install-cvc5 has no SHA-256 entry for cvc5 ${{ inputs.version }} on ${{ runner.os }}-${{ runner.arch }}; add a case to .github/actions/install-cvc5/action.yaml" exit 1 ;; esac - url="https://github.com/cvc5/cvc5/releases/download/cvc5-${{ inputs.version }}/${asset}.zip" + echo "asset=${asset}" >> "$GITHUB_OUTPUT" + echo "sha256=${sha256}" >> "$GITHUB_OUTPUT" + + - name: Install cvc5 (Linux / macOS) + if: runner.os != 'Windows' + shell: bash + env: + ASSET: ${{ steps.meta.outputs.asset }} + EXPECTED_SHA256: ${{ steps.meta.outputs.sha256 }} + VERSION: ${{ inputs.version }} + run: | + set -euo pipefail + url="https://github.com/cvc5/cvc5/releases/download/cvc5-${VERSION}/${ASSET}.zip" wget --quiet "${url}" - unzip -j -d /usr/local/bin "${asset}.zip" "${asset}/bin/cvc5" - rm "${asset}.zip" + if command -v sha256sum >/dev/null; then + actual=$(sha256sum "${ASSET}.zip" | cut -d' ' -f1) + else + actual=$(shasum -a 256 "${ASSET}.zip" | cut -d' ' -f1) + fi + if [ "${actual}" != "${EXPECTED_SHA256}" ]; then + echo "::error ::SHA-256 mismatch for ${ASSET}.zip" + echo " expected: ${EXPECTED_SHA256}" + echo " actual: ${actual}" + exit 1 + fi + unzip -j -d /usr/local/bin "${ASSET}.zip" "${ASSET}/bin/cvc5" + rm "${ASSET}.zip" cvc5 --version - name: Install cvc5 (Windows) if: runner.os == 'Windows' shell: pwsh + env: + ASSET: ${{ steps.meta.outputs.asset }} + EXPECTED_SHA256: ${{ steps.meta.outputs.sha256 }} + VERSION: ${{ inputs.version }} run: | $ErrorActionPreference = 'Stop' - $asset = 'cvc5-Win64-x86_64-static' - $url = "https://github.com/cvc5/cvc5/releases/download/cvc5-${{ inputs.version }}/$asset.zip" - Invoke-WebRequest -Uri $url -OutFile ".\$asset.zip" + $url = "https://github.com/cvc5/cvc5/releases/download/cvc5-$env:VERSION/$env:ASSET.zip" + Invoke-WebRequest -Uri $url -OutFile ".\$env:ASSET.zip" + $actual = (Get-FileHash -Algorithm SHA256 ".\$env:ASSET.zip").Hash.ToLower() + if ($actual -ne $env:EXPECTED_SHA256) { + Write-Error "SHA-256 mismatch for $env:ASSET.zip`n expected: $env:EXPECTED_SHA256`n actual: $actual" + exit 1 + } New-Item -ItemType Directory -Force -Path 'C:\tools\cvc5' | Out-Null - Expand-Archive -LiteralPath ".\$asset.zip" -DestinationPath '.\cvc5-extract' -Force - Move-Item -Force ".\cvc5-extract\$asset\bin\cvc5.exe" 'C:\tools\cvc5\cvc5.exe' + Expand-Archive -LiteralPath ".\$env:ASSET.zip" -DestinationPath '.\cvc5-extract' -Force + Move-Item -Force ".\cvc5-extract\$env:ASSET\bin\cvc5.exe" 'C:\tools\cvc5\cvc5.exe' Remove-Item -Recurse -Force '.\cvc5-extract' - Remove-Item ".\$asset.zip" + Remove-Item ".\$env:ASSET.zip" echo 'C:\tools\cvc5' >> $env:GITHUB_PATH & 'C:\tools\cvc5\cvc5.exe' --version diff --git a/.github/actions/install-z3/action.yaml b/.github/actions/install-z3/action.yaml index 8d725f1effd..8fd1f1a89c7 100644 --- a/.github/actions/install-z3/action.yaml +++ b/.github/actions/install-z3/action.yaml @@ -1,14 +1,21 @@ name: 'Install Z3 (Windows)' description: | - Download and install a Z3 release binary on a Windows runner. After - this action runs, `z3` is on PATH for subsequent steps (the PATH - update only takes effect from the next step onward; the action + Download and install a Z3 release binary on a Windows runner. + + Downloaded archives are verified against a hard-coded SHA-256 hash + table embedded in this action; an unknown (version, arch) pair + causes the step to fail. To support a new Z3 version, append a row + to the case statement in the "Resolve Z3 asset hash" step. Hashes + can be obtained by downloading the asset and running: + sha256sum z3--.zip + + After this action runs, `z3` is on PATH for subsequent steps (the + PATH update only takes effect from the next step onward; the action verifies the binary in-place via its absolute path). Linux and macOS runners install Z3 via the system package manager (apt / brew) elsewhere in the workflow; this action only covers - Windows, which has no comparable distribution channel and therefore - needs an explicit version pin. + Windows, which has no comparable distribution channel. inputs: version: @@ -22,22 +29,47 @@ inputs: runs: using: composite steps: + - name: install-z3 is currently Windows-only + if: runner.os != 'Windows' + shell: bash + run: | + echo "::error ::install-z3 currently only supports Windows; install Z3 via apt (Linux) or brew (macOS) directly" + exit 1 + + - name: Resolve Z3 asset hash + if: runner.os == 'Windows' + id: meta + shell: bash + run: | + set -euo pipefail + case "${{ inputs.version }}-${{ inputs.arch }}" in + 4.8.10-x64-win) + sha256=688c8f96f4f89cb474de4ecd740c812c6e695318e4b50fd790722513285b2fcb ;; + *) + echo "::error ::install-z3 has no SHA-256 entry for Z3 ${{ inputs.version }} (${{ inputs.arch }}); add a case to .github/actions/install-z3/action.yaml" + exit 1 + ;; + esac + echo "sha256=${sha256}" >> "$GITHUB_OUTPUT" + - name: Install Z3 (Windows) if: runner.os == 'Windows' shell: pwsh + env: + VERSION: ${{ inputs.version }} + ARCH: ${{ inputs.arch }} + EXPECTED_SHA256: ${{ steps.meta.outputs.sha256 }} run: | $ErrorActionPreference = 'Stop' - $name = "z3-${{ inputs.version }}-${{ inputs.arch }}" - $url = "https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/$name.zip" + $name = "z3-$env:VERSION-$env:ARCH" + $url = "https://github.com/Z3Prover/z3/releases/download/z3-$env:VERSION/$name.zip" Invoke-WebRequest -Uri $url -OutFile '.\z3.zip' + $actual = (Get-FileHash -Algorithm SHA256 '.\z3.zip').Hash.ToLower() + if ($actual -ne $env:EXPECTED_SHA256) { + Write-Error "SHA-256 mismatch for $name.zip`n expected: $env:EXPECTED_SHA256`n actual: $actual" + exit 1 + } Expand-Archive -LiteralPath '.\z3.zip' -DestinationPath 'C:\tools' -Force Remove-Item '.\z3.zip' echo "C:\tools\$name\bin" >> $env:GITHUB_PATH & "C:\tools\$name\bin\z3.exe" --version - - - name: install-z3 is currently Windows-only - if: runner.os != 'Windows' - shell: bash - run: | - echo "::error ::install-z3 currently only supports Windows; install Z3 via apt (Linux) or brew (macOS) directly" - exit 1