Adopt Z3 releases only through a gate in CI; keep 4.13.4 for 0.2

.github/workflows/cppverify-z3-gate.yml

@@ -0,0 +1,138 @@
+name: CppVerify Z3 gate
+
+# A Z3 release is adopted only through this gate
+# (clang/utils/cppverify-z3-gate): cpp-verify is built with the vendored Z3
+# and with the candidate, and gate.sh compares the two on the sequence
+# benchmark and on every Verify test program. Every Monday it tests Z3's
+# newest release; run it by hand for any tag.
+
+on:
+  schedule:
+    - cron: "23 5 * * 1"
+  # A change to the gate runs it.
+  pull_request:
+    branches: [main]
+    paths:
+      - .github/workflows/cppverify-z3-gate.yml
+      - clang/utils/cppverify-z3-gate/**
+  workflow_dispatch:
+    inputs:
+      z3_tag:
+        description: Z3 tag to test, such as z3-5.3.2 (default the newest release)
+        required: false
+
+permissions:
+  contents: read
+
+jobs:
+  candidate:
+    name: Choose the candidate
+    runs-on: ubuntu-24.04
+    outputs:
+      tag: ${{ steps.tag.outputs.tag }}
+    steps:
+      - id: tag
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REQUESTED: ${{ inputs.z3_tag }}
+        run: |
+          tag=${REQUESTED:-$(gh api repos/Z3Prover/z3/releases/latest --jq .tag_name)}
+          echo "tag=$tag" >> "$GITHUB_OUTPUT"
+          echo "candidate: $tag"
+
+  build:
+    name: Build (${{ matrix.role }})
+    needs: candidate
+    runs-on: ubuntu-24.04
+    timeout-minutes: 355
+    strategy:
+      matrix:
+        role: [base, candidate]
+    env:
+      CCACHE_DIR: ${{ github.workspace }}/.ccache
+      CCACHE_MAXSIZE: 4G
+      CCACHE_COMPRESS: "1"
+    steps:
+      - name: Free disk space
+        run: sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
+
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install build tools
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y ninja-build ccache
+
+      # The tag is Z3's to name, so the shell reads it as data.
+      - name: Fetch the candidate Z3
+        if: matrix.role == 'candidate'
+        env:
+          TAG: ${{ needs.candidate.outputs.tag }}
+        run: |
+          git clone --depth 1 --branch "$TAG" \
+            https://github.com/Z3Prover/z3.git "$RUNNER_TEMP/z3"
+          echo "Z3_SOURCE=-DCPPVERIFY_Z3_SOURCE_DIR=$RUNNER_TEMP/z3" >> "$GITHUB_ENV"
+
+      - uses: actions/cache/restore@v4
+        with:
+          path: .ccache
+          key: ccache-linux-z3gate-${{ matrix.role }}-${{ github.sha }}
+          restore-keys: ccache-linux-z3gate-${{ matrix.role }}-
+
+      - name: Configure
+        run: |
+          cmake -S llvm -B build -G Ninja \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DLLVM_ENABLE_PROJECTS=clang \
+            -DLLVM_TARGETS_TO_BUILD=Native \
+            -DCPPVERIFY_VENDOR_Z3=ON \
+            -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF \
+            -DLLVM_ENABLE_ASSERTIONS=OFF \
+            -DLLVM_CCACHE_BUILD=ON ${Z3_SOURCE:-}
+
+      - name: Build
+        run: ninja -C build cpp-verify
+
+      - uses: actions/cache/save@v4
+        if: always()
+        with:
+          path: .ccache
+          key: ccache-linux-z3gate-${{ matrix.role }}-${{ github.sha }}
+
+      - name: Package
+        run: |
+          build/bin/cpp-verify --version
+          tar -czf ${{ matrix.role }}.tar.gz build/bin/cpp-verify build/lib/clang \
+            build/cppverify-z3/install/bin/z3
+
+      - uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.role }}
+          path: ${{ matrix.role }}.tar.gz
+
+  gate:
+    name: Gate (${{ needs.candidate.outputs.tag }})
+    needs: [candidate, build]
+    runs-on: ubuntu-24.04
+    timeout-minutes: 355
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions/download-artifact@v4
+
+      - name: Unpack
+        run: |
+          for role in base candidate; do
+            mkdir -p "$role" && tar -xzf "$role/$role.tar.gz" -C "$role"
+          done
+
+      - name: Run the gate
+        run: clang/utils/cppverify-z3-gate/gate.sh base/build candidate/build results
+
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: gate-results
+          path: results/

clang/utils/cppverify-z3-gate/differential.py

@@ -0,0 +1,130 @@
+#!/usr/bin/env python3
+"""Verdict-and-time differential between two cpp-verify binaries.
+
+usage: differential.py BASE NEW OUT.jsonl [--parallel N] [-- extra cpp-verify args]
+
+Every .cpp file under clang/test/Verify (run from the repository root) is
+verified by both binaries with --diagnostics-format=json and CPPVERIFY_JOBS=1.
+A function's verdict is its status, reason, and qualifiers (vacuous,
+partial, trusts). The differential prints each function whose verdict
+changed, as one of:
+
+  LOST     a proof or certified failure of BASE that NEW does not give
+  FLIPPED  Verified in one and Failed in the other: a solver or the verifier
+           is wrong in one of them
+  GAINED   a proof or certified failure NEW gives and BASE does not
+  CHANGED  any other change
+
+and each file whose time changed by more than 2x and 5 s. It exits with 1
+when a verdict is LOST or FLIPPED."""
+import concurrent.futures
+import json
+import os
+import re
+import subprocess
+import sys
+import time
+
+args = sys.argv[1:]
+extra = []
+if "--" in args:
+    i = args.index("--")
+    extra = args[i + 1:]
+    args = args[:i]
+parallel = os.cpu_count() or 4
+if "--parallel" in args:
+    i = args.index("--parallel")
+    parallel = int(args[i + 1])
+    del args[i:i + 2]
+base, new, out_path = args
+files = subprocess.run(["git", "ls-files", "clang/test/Verify/*.cpp",
+                        "clang/test/Verify/**/*.cpp"],
+                       capture_output=True, text=True, check=True).stdout.split()
+files = [f for f in files if "/Inputs/" not in f]
+INPUTS = os.path.abspath("clang/test/Verify/suite/Inputs")
+
+
+def run(binary, path):
+    env = dict(os.environ, CPPVERIFY_JOBS="1")
+    start = time.monotonic()
+    try:
+        p = subprocess.run([binary, "--diagnostics-format=json", *extra, path,
+                            "--", "-std=c++17", "-I" + INPUTS],
+                           capture_output=True, text=True, timeout=1800, env=env)
+        out = p.stdout
+    except subprocess.TimeoutExpired:
+        out = ""
+    seconds = time.monotonic() - start
+    verdicts = {}
+    for line in out.splitlines():
+        try:
+            r = json.loads(line)
+        except ValueError:
+            continue
+        name = r.get("function")
+        status = r.get("status")
+        if not name or status not in ("verified", "failed", "unresolved",
+                                      "bounded-safe", "trusted"):
+            continue
+        verdict = {"status": status, "reason": r.get("reason"),
+                   "vacuous": bool(r.get("vacuous")),
+                   "partial": bool(r.get("partial")),
+                   "trusts": sorted(r.get("trusts") or [])}
+        verdicts.setdefault(name, []).append(verdict)
+    return {"verdicts": verdicts, "seconds": round(seconds, 2)}
+
+
+def decisive(verdict):
+    return verdict["status"] in ("verified", "failed")
+
+
+def compare(a, b):
+    """The changes between two runs of one file."""
+    changes = []
+    for name in sorted(set(a) | set(b)):
+        va, vb = a.get(name, []), b.get(name, [])
+        if va == vb:
+            continue
+        sa = {v["status"] for v in va}
+        sb = {v["status"] for v in vb}
+        if ("verified" in sa and "failed" in sb) or ("failed" in sa and "verified" in sb):
+            kind = "FLIPPED"
+        elif any(decisive(v) and v not in vb for v in va):
+            kind = "LOST"
+        elif any(decisive(v) and v not in va for v in vb):
+            kind = "GAINED"
+        else:
+            kind = "CHANGED"
+        changes.append((kind, name, va, vb))
+    return changes
+
+
+def job(path):
+    return path, run(base, path), run(new, path)
+
+
+counts = {"LOST": 0, "FLIPPED": 0, "GAINED": 0, "CHANGED": 0}
+slow = 0
+with open(out_path, "w") as out, \
+        concurrent.futures.ThreadPoolExecutor(parallel) as pool:
+    for path, a, b in pool.map(job, files):
+        out.write(json.dumps({"file": path, "base": a, "new": b}) + "\n")
+        for kind, name, va, vb in compare(a["verdicts"], b["verdicts"]):
+            counts[kind] += 1
+            print("%s %s %s" % (kind, path, name))
+            print("  base: %s" % json.dumps(va))
+            print("  new:  %s" % json.dumps(vb))
+        ta, tb = a["seconds"], b["seconds"]
+        if abs(tb - ta) > 5 and (tb > 2 * ta or ta > 2 * tb):
+            slow += 1
+            print("TIME %s base %.1f s new %.1f s" % (path, ta, tb))
+total_a = total_b = 0.0
+for line in open(out_path):
+    record = json.loads(line)
+    total_a += record["base"]["seconds"]
+    total_b += record["new"]["seconds"]
+print("%d files: %d lost, %d flipped, %d gained, %d changed, %d with a time "
+      "change; total %.0f s -> %.0f s"
+      % (len(files), counts["LOST"], counts["FLIPPED"], counts["GAINED"],
+         counts["CHANGED"], slow, total_a, total_b))
+sys.exit(1 if counts["LOST"] or counts["FLIPPED"] else 0)

clang/utils/cppverify-z3-gate/gate.sh

@@ -0,0 +1,80 @@
+#!/bin/bash
+# The gate a Z3 release passes before cpp-verify adopts it.
+#
+# usage: gate.sh BASE CANDIDATE [OUT]
+#
+# BASE and CANDIDATE are cpp-verify build directories, each with
+# bin/cpp-verify and the Z3 it is built with in cppverify-z3/install/bin/z3.
+# Run from the repository root. Results land in OUT (default: a fresh
+# temporary directory).
+#
+# Stage 1 solves the sequence benchmark (seqbench.py) with both Z3 binaries,
+# in cpp-verify's own encoding (NT) and in the plain sequence theory (N),
+# which a run with more than one job races beside it. A claim counts as the
+# verifier would decide it: by NT with one job, by NT or N with more. The
+# candidate fails when it loses a proof of a valid claim or a model of a false
+# one that the base has in either.
+#
+# Stage 2 verifies every Verify test program with both builds at one job
+# (differential.py) and fails when the candidate loses a proof or a certified
+# failure, or when a function is Verified in one and Failed in the other.
+set -u
+BASE=$1
+CAND=$2
+OUT=${OUT:-${3:-$(mktemp -d)}}
+JOBS=${JOBS:-$(nproc)}
+HERE=$(cd "$(dirname "$0")" && pwd)
+mkdir -p "$OUT/queries"
+status=0
+
+echo "== stage 1: the sequence benchmark"
+python3 "$HERE/seqbench.py" "$OUT/queries" > /dev/null
+solve() {  # solve Z3 FILE: prints "name,verdict"
+  local out
+  out=$(timeout 30 "$1" -T:20 "$2" 2>&1 | head -1 | tr -d '\r')
+  case "$out" in sat|unsat|unknown) ;; *) out=timeout ;; esac
+  echo "$(basename "$2" .smt2),$out"
+}
+export -f solve
+for role in base cand; do
+  z3=$BASE/cppverify-z3/install/bin/z3
+  [ $role = cand ] && z3=$CAND/cppverify-z3/install/bin/z3
+  "$z3" --version
+  ls "$OUT"/queries/*.N.z3.smt2 "$OUT"/queries/*.NT.z3.smt2 |
+    xargs -P "$JOBS" -I{} bash -c "solve '$z3' {}" | sort > "$OUT/stage1_$role.csv"
+done
+python3 - "$OUT" <<'EOF' || status=1
+import csv, sys
+out = sys.argv[1]
+def load(role):
+    return {row[0]: row[1] for row in csv.reader(open(f"{out}/stage1_{role}.csv"))}
+def decided(results, claim, encodings):
+    want = 'unsat' if '.ok' in claim else 'sat'
+    return any(results.get(f"{claim}.{e}.z3") == want for e in encodings)
+base, cand = load('base'), load('cand')
+claims = sorted({name.rsplit('.', 2)[0] for name in base})
+lost = []
+for jobs, encodings in (('one job', ('NT',)), ('more jobs', ('NT', 'N'))):
+    for role, results in (('base', base), ('cand', cand)):
+        proved = sum(decided(results, c, encodings) for c in claims if '.ok' in c)
+        models = sum(decided(results, c, encodings) for c in claims if '.bad' in c)
+        print(f"{jobs:9} {role}: {proved} proofs, {models} models")
+    for c in claims:
+        if decided(base, c, encodings) and not decided(cand, c, encodings):
+            lost.append((jobs, c))
+for jobs, c in lost:
+    print(f"LOST {c} ({jobs})")
+for c in claims:
+    if decided(cand, c, ('NT', 'N')) and not decided(base, c, ('NT', 'N')):
+        print(f"GAINED {c}")
+sys.exit(1 if lost else 0)
+EOF
+
+echo "== stage 2: every Verify test program"
+python3 "$HERE/differential.py" "$BASE/bin/cpp-verify" "$CAND/bin/cpp-verify" \
+  "$OUT/stage2.jsonl" --parallel "$JOBS" | tee "$OUT/stage2.txt"
+[ "${PIPESTATUS[0]}" = 0 ] || status=1
+
+echo "results in $OUT"
+if [ $status = 0 ]; then echo "gate: pass"; else echo "gate: FAIL"; fi
+exit $status