CI: run the Cranelift verifier.

.github/workflows/main.yml

@@ -189,6 +189,7 @@ jobs:
       run-dwarf: ${{ steps.calculate.outputs.run-dwarf }}
       platform-checks: ${{ steps.calculate.outputs.platform-checks }}
       test-gc-zeal: ${{ steps.calculate.outputs.test-gc-zeal }}
+      run-isle-veri: ${{ steps.calculate.outputs.run-isle-veri }}
     steps:
     - uses: actions/checkout@v6
     - id: calculate
@@ -245,6 +246,15 @@ jobs:
           if grep -q gc names.log; then
             echo test-gc-zeal=true >> $GITHUB_OUTPUT
           fi
+          # Run the ISLE verifier for PRs that touch the ISLE toolchain
+          # (cranelift/isle) or any ISLE source file (*.isle); `prtest:full`
+          # is handled by run_full below.
+          if grep -q cranelift/isle names.log; then
+            echo run-isle-veri=true >> $GITHUB_OUTPUT
+          fi
+          if grep -qE '\.isle$' names.log; then
+            echo run-isle-veri=true >> $GITHUB_OUTPUT
+          fi
         fi
         matrix="$(node ./ci/build-test-matrix.js ./commits.log ./names.log $run_full)"
         echo "test-matrix={\"include\":$(echo $matrix)}" >> $GITHUB_OUTPUT
@@ -263,6 +273,7 @@ jobs:
             echo preview1-adapter=true >> $GITHUB_OUTPUT
             echo run-dwarf=true >> $GITHUB_OUTPUT
             echo platform-checks=true >> $GITHUB_OUTPUT
+            echo run-isle-veri=true >> $GITHUB_OUTPUT
         fi
 
   # Build all documentation of Wasmtime, including the C API documentation,
@@ -1363,20 +1374,74 @@ jobs:
     - run: ${{ matrix.script }}
       if: ${{ matrix.script }}
 
-  # Check the ISLE verifier builds/runs (without invoking the SMT solver, for now).
-  isle_veri_basic_check:
+  # Run the full ISLE verifier (see cranelift/isle/veri/) incrementally on top
+  # of a shared SMT query cache. Cache misses are solved with cvc5/z3, so this
+  # is fast when the cache is warm and can take a long time when it is cold.
+  #
+  # The cache is a named entry in the actions cache, keyed by a hash of the
+  # ISLE sources and the ISLE toolchain (see `hashFiles` in the cache key).
+  # Caches saved by merge-queue runs are stored in the default branch's
+  # cache scope and are visible to every PR and future merge-queue run, so
+  # each distinct ISLE state gets exactly one immutable entry on `main`, and
+  # no branch ever needs to "update" an existing entry: a new ISLE state is
+  # a new key. PR runs read those entries and, when their ISLE state is new,
+  # save an entry scoped to their own merge ref, so repeated runs of the
+  # same PR verify incrementally on top of their previous run's cache.
+  #
+  # The rebuilt cache is also uploaded as the `isle-veri-cache` run
+  # artifact; the `publish-artifacts.yml` workflow publishes it as the
+  # `isle-veri-cache.tar.gz` asset on the rolling `dev` release so local
+  # users can download it with `cranelift/isle/veri/setup/download-cache.sh`.
+  # That asset is a convenience snapshot for humans; CI itself only uses the
+  # named cache above.
+  isle_veri_full_check:
     needs: determine
-    if: needs.determine.outputs.run-full
-    name: ISLE verifier basic check
+    if: needs.determine.outputs.run-isle-veri
+    name: ISLE verifier full check
     runs-on: ubuntu-latest
+    # Runs can be cold and take a long time; most will not take this long.
+    timeout-minutes: 360
     steps:
     - uses: actions/checkout@v6
       with:
         submodules: true
     - uses: ./.github/actions/install-rust
-    - run: cargo run -p cranelift-isle-veri --bin veri -- --config cranelift/isle/veri/configs/aarch64-fast.args --skip-solver
-    - run: cargo run -p cranelift-isle-veri --bin veri -- --name x64 --rule iadd_base_case_32_or_64_lea --skip-solver
-    - run: cargo run -p cranelift-isle-veri --bin veri -- --name opt --only-root simplify --default-excludes --skip-solver
+    - uses: ./.github/actions/apt-get-install
+      with:
+        packages: wget unzip
+    - name: Install SMT solvers (cvc5, z3)
+      run: |
+        solver_dir="$HOME/.cache/smt-solvers"
+        mkdir -p "${solver_dir}/bin"
+        ./cranelift/isle/veri/setup/install-cvc5.sh -i "${solver_dir}"
+        ./cranelift/isle/veri/setup/install-z3.sh -b "${solver_dir}/bin"
+    - name: Add solvers to PATH
+      run: echo "$HOME/.cache/smt-solvers/bin" >> "${GITHUB_PATH}"
+    - name: Restore and save verifier cache
+      uses: actions/cache@v5
+      with:
+        path: cranelift/isle/veri/cache
+        # Bump `v1` if the cache format changes. `hashFiles` covers the ISLE
+        # sources and the ISLE toolchain itself by hashing the paths and
+        # contents of all matching files.
+        key: isle-veri-cache-v1-${{ hashFiles('cranelift/isle/**/*.rs', 'cranelift/codegen/**/*.isle') }}
+        restore-keys: |
+          isle-veri-cache-v1-
+    - name: Verify and rebuild cache
+      env:
+        # Per-SMT-query timeout, in seconds (see the `--timeout` option in
+        # cranelift/isle/veri/veri/src/bin/veri.rs).
+        ISLE_VERI_TIMEOUT: "120"
+      run: |
+        mkdir -p cranelift/isle/veri/cache
+        ./cranelift/isle/veri/verify.sh rebuild-cache aarch64-fast opt-fast x64-iadd-base-case
+    - name: Package rebuilt cache
+      run: tar czf isle-veri-cache.tar.gz -C cranelift/isle/veri cache
+    - name: Upload cache tarball as run artifact
+      uses: actions/upload-artifact@v6
+      with:
+        name: isle-veri-cache
+        path: isle-veri-cache.tar.gz
 
   # Perform release builds of `wasmtime` and `libwasmtime.so`. Builds a variety
   # of platforms and architectures and then uploads the release artifacts to
@@ -1487,7 +1552,7 @@ jobs:
       - verify-publish
       - determine
       - miri
-      - isle_veri_basic_check
+      - isle_veri_full_check
       - build-preview1-component-adapter
       - build-preview1-component-adapter-provider
       - test-min-platform-example

.gitignore

@@ -36,3 +36,5 @@ miri-wast/
 report/
 # Local SMT query cache for the ISLE verifier (see cranelift/isle/veri/verify.sh).
 cranelift/isle/veri/cache/
+# Staging directory used by `verify.sh rebuild-cache` before it swaps in.
+cranelift/isle/veri/cache.rebuild/

ci/merge-artifacts.sh

@@ -52,3 +52,8 @@ done
 
 # Copy over remaining source tarball into the dist folder
 mv -t dist bins-*/*.tar.*
+
+# Also move the ISLE verifier's SMT query cache, if present, into `dist/`.
+if [ -f isle-veri-cache/isle-veri-cache.tar.gz ]; then
+  mv isle-veri-cache/isle-veri-cache.tar.gz dist/
+fi

cranelift/isle/veri/README.md

@@ -38,6 +38,38 @@ Alternatively, on Linux or MacOS you can install from Github release with:
 
 If you use this method, ensure that `<install_path>/bin` is on your `$PATH`.
 
+## Sharing the cache with CI
+
+To keep local runs fast, CI maintains a shared copy of the verifier's SMT
+query cache in the GitHub Actions cache under keys of the form
+`isle-veri-cache-v1-<hash>`, where `<hash>` is derived from the ISLE sources
+and toolchain. Runs in the merge queue save entries in the default branch's
+cache scope, so every subsequent PR restores the most recent entry and
+verifies incrementally on top of it.
+
+The current cache is also published as the `isle-veri-cache.tar.gz` asset on
+the rolling
+[`dev` release](https://github.com/bytecodealliance/wasmtime/releases/tag/dev)
+for local use: the "ISLE verifier full check" job in the CI workflow
+([`.github/workflows/main.yml`](../../.github/workflows/main.yml)) uploads the
+rebuilt cache as a run artifact, and the
+[`publish-artifacts.yml`](../../.github/workflows/publish-artifacts.yml)
+workflow publishes it to the `dev` release when the run lands on `main`. The
+job runs on full CI and, on pull requests, when the PR touches the ISLE
+sources (`cranelift/codegen/**/*.isle`) or the ISLE toolchain
+(`cranelift/isle`), or a commit message contains `prtest:full`.
+
+To start a local session from the cache CI is currently using, run:
+
+```
+./cranelift/isle/veri/setup/download-cache.sh
+```
+
+This downloads the latest asset from the `dev` release and installs it as
+`cranelift/isle/veri/cache`. You can then verify incrementally on top of it
+with `./cranelift/isle/veri/verify.sh` (and check full cache coverage with
+`verify.sh cache-only`).
+
 ## Configuration files
 
 Rather than configuring arguments on the command line, you can store
@@ -52,7 +84,7 @@ Blank lines and anything following a `#` (whole-line or trailing comments) are i
 The arguments from the file are applied *before* any passed on the command line, so the command line always takes precedence (for example, you can reuse a config but override its `--timeout`).
 Multi-valued arguments such as `--filter` accumulate, while single-valued arguments (like `--name`) take their last value.
 
-Three example configurations live in [`configs/`](configs):
+Five example configurations live in [`configs/`](configs):
 
 | File                              | Equivalent to                                                       |
 | --------------------------------- | ------------------------------------------------------------------- |

cranelift/isle/veri/setup/download-cache.sh

@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+#
+# Download the latest ISLE verifier SMT query cache from the `dev` release on
+# github.com/bytecodealliance/wasmtime and install it as
+# cranelift/isle/veri/cache, so a local run of verify.sh starts from the same
+# state CI is currently using.
+#
+# The `dev` release asset is refreshed by the `publish-artifacts.yml`
+# workflow from the "ISLE verifier full check" CI job's artifact (see
+# .github/workflows/main.yml).
+#
+# Usage:
+#   ./cranelift/isle/veri/setup/download-cache.sh
+#
+# Requires: curl, tar.
+# Optionally set GH_TOKEN to avoid GitHub API rate limits (unauthenticated
+# requests are limited to 60/hour per IP).
+
+set -euo pipefail
+
+repo="bytecodealliance/wasmtime"
+release="dev"
+asset="isle-veri-cache.tar.gz"
+cache_dir="cranelift/isle/veri/cache"
+
+cd "$(git rev-parse --show-toplevel)"
+
+if [ -n "${GH_TOKEN:-}" ]; then
+    curl_args=(-fsSL -H "Authorization: Bearer ${GH_TOKEN}")
+else
+    curl_args=(-fsSL)
+fi
+
+json=$(curl "${curl_args[@]}" \
+    "https://api.github.com/repos/${repo}/releases/tags/${release}")
+
+# Extract the browser_download_url of our asset from the release JSON.
+url=$(printf '%s\n' "$json" \
+    | { grep -o "\"browser_download_url\"[[:space:]]*:[[:space:]]*\"[^\"]*/${asset}\"" || true; } \
+    | sed 's/.*"browser_download_url"[[:space:]]*:[[:space:]]*"//; s/"$//')
+if [ -z "$url" ]; then
+    echo "ERROR: asset '${asset}' not found on release '${release}' of ${repo}" >&2
+    exit 1
+fi
+
+tmp=$(mktemp -d)
+trap 'rm -rf "$tmp"' EXIT
+curl -fL --progress-bar -o "${tmp}/${asset}" "$url"
+
+rm -rf "$cache_dir"
+tar xzf "${tmp}/${asset}" -C cranelift/isle/veri
+echo "Installed verifier cache to ${cache_dir}/"
+echo "You can now run ./cranelift/isle/veri/verify.sh (or cache-only / rebuild-cache)."

cranelift/isle/veri/verify.sh

@@ -2,12 +2,16 @@
 #
 # Driver for VeriISLE verification with the SMT query cache.
 #
-# The cache lives locally at cranelift/isle/veri/cache (gitignored). Sharing
-# the cache across runs in CI (via artifacts) is planned separately; for now
-# these modes manage a local cache only.
+# The cache lives locally at cranelift/isle/veri/cache (gitignored). CI
+# (the isle_veri_full_check job in .github/workflows/main.yml) verifies on
+# top of the shared entry in the GitHub Actions cache (keyed by a hash of
+# the ISLE sources and toolchain) and also uploads the rebuilt cache as a
+# run artifact, which the publish-artifacts.yml workflow publishes as
+# isle-veri-cache.tar.gz on the `dev` release when the run lands on main,
+# for local use. Local users can download it with setup/download-cache.sh.
 #
 # Usage:
-#   ./cranelift/isle/veri/verify.sh [MODE]
+#   ./cranelift/isle/veri/verify.sh [MODE] [CONFIG ...]
 #
 # Modes:
 #   cache-only     Verify purely from the local cache, in read-only, enforcing
@@ -25,16 +29,30 @@
 #                  Serves cached results where possible and invokes the solver
 #                  on misses, writing new entries back to the cache.
 #
+# CONFIG names (without the .args suffix) optionally select the
+# configurations to run from cranelift/isle/veri/configs/; the default is
+# CONFIGS below.
+
 set -euo pipefail
 cd "$(git rev-parse --show-toplevel)"
 
 MODE="${1:-local}"
+shift || true
 
 CACHE_DIR="cranelift/isle/veri/cache"
+# The default set of configurations to verify.
 CONFIGS=(
     cranelift/isle/veri/configs/aarch64.args
     cranelift/isle/veri/configs/x64-iadd-base-case.args
 )
+# CI passes its own list (see the isle_veri_full_check job in
+# .github/workflows/main.yml).
+if [ $# -gt 0 ]; then
+    CONFIGS=()
+    for name in "$@"; do
+        CONFIGS+=("cranelift/isle/veri/configs/${name}.args")
+    done
+fi
 
 # Run the verifier for every configuration, forwarding the given cache flags.
 run_all() {
@@ -94,8 +112,9 @@ local | "")
     ;;
 
 *)
-    echo "usage: $0 [cache-only | rebuild-cache]" >&2
+    echo "usage: $0 [cache-only | rebuild-cache] [CONFIG ...]" >&2
     echo "       (no argument runs a local, in-place read-write verification)" >&2
+    echo "       (CONFIG names are .args files in cranelift/isle/veri/configs/)" >&2
     exit 1
     ;;
 esac