diff --git a/.github/workflows/cppverify-z3-gate.yml b/.github/workflows/cppverify-z3-gate.yml new file mode 100644 index 0000000000..4259dbfc9f --- /dev/null +++ b/.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/ diff --git a/clang/utils/cppverify-z3-gate/differential.py b/clang/utils/cppverify-z3-gate/differential.py new file mode 100755 index 0000000000..c78ee38902 --- /dev/null +++ b/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) diff --git a/clang/utils/cppverify-z3-gate/gate.sh b/clang/utils/cppverify-z3-gate/gate.sh new file mode 100755 index 0000000000..01d03559c4 --- /dev/null +++ b/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 diff --git a/clang/utils/cppverify-z3-gate/seqbench.py b/clang/utils/cppverify-z3-gate/seqbench.py new file mode 100755 index 0000000000..2b08c5d5bf --- /dev/null +++ b/clang/utils/cppverify-z3-gate/seqbench.py @@ -0,0 +1,512 @@ +"""The sequence benchmark of the Z3 gate (gate.sh): one abstract workload of +valid and false claims over sequences, written in several exact SMT-LIB +encodings, among them cpp-verify's own (NT) and the plain sequence theory (N). +It comes from the sequence-encoding study that chose cpp-verify's encoding. + +usage: seqbench.py OUT_DIR + +Semantics (cppverify::seq): finite sequences of integers; s[i] is 0 outside +[0, len); update outside [0, len) changes nothing; subrange(lo, hi) clamps lo +into [0, len] and hi into [lo, len]; == is element-wise equality. +""" +import itertools, os, sys + +# ---- abstract terms ------------------------------------------------------- +# ('svar',n) ('ivar',n) ('int',k) ('len',s) ('at',s,i) ('push',s,x) +# ('upd',s,i,x) ('cat',s,t) ('sub',s,lo,hi) ('empty',) ('unit',x) +# ('contains',s,x) ('seq=',a,b) ('=',a,b) ('<',a,b) ('<=',a,b) ('+',a,b) +# ('-',a,b) ('and',*) ('or',*) ('not',a) ('=>',a,b) ('forall',k,body) +# ('forallr',k,lo,hi,body) ('existsr',k,lo,hi,body) ('app',f,args) ('fn',f,args) +# 'app' is a recursive spec over sequences; 'fn' an uninterpreted Int function. + +def S(n): return ('svar', n) +def I(n): return ('ivar', n) +def K(k): return ('int', k) +def L(s): return ('len', s) +def At(s, i): return ('at', s, i) +def Push(s, x): return ('push', s, x) +def Upd(s, i, x): return ('upd', s, i, x) +def Cat(s, t): return ('cat', s, t) +def Sub(s, lo, hi): return ('sub', s, lo, hi) +def SEq(a, b): return ('seq=', a, b) +def Eq(a, b): return ('=', a, b) +def Lt(a, b): return ('<', a, b) +def Le(a, b): return ('<=', a, b) +def Add(a, b): return ('+', a, b) +def Minus(a, b): return ('-', a, b) +def And(*a): return ('and',) + a +def Or(*a): return ('or',) + a +def Not(a): return ('not', a) +def Imp(a, b): return ('=>', a, b) +def Forall(k, b): return ('forall', k, b) +def ForallR(k, lo, hi, b): return ('forallr', k, lo, hi, b) +def ExistsR(k, lo, hi, b): return ('existsr', k, lo, hi, b) +def App(f, *a): return ('app', f, a) +def Fn(f, *a): return ('fn', f, a) +def Contains(s, x): return ('contains', s, x) +EMPTY = ('empty',) + +def free_vars(t, acc, bound=()): + k = t[0] + if k == 'svar': acc.setdefault(t[1], 'seq') + elif k == 'ivar': + if t[1] not in bound: acc.setdefault(t[1], 'int') + elif k in ('forall',): + free_vars(t[2], acc, bound + (t[1],)) + elif k in ('forallr', 'existsr'): + free_vars(t[2], acc, bound); free_vars(t[3], acc, bound) + free_vars(t[4], acc, bound + (t[1],)) + elif k in ('app', 'fn'): + for a in t[2]: free_vars(a, acc, bound) + else: + for a in t[1:]: + if isinstance(a, tuple): free_vars(a, acc, bound) + +# ---- recursive specs (sequence parameter s, extra int params) ------------- +SPECS = { + # total(s) = total(s[0, len - 1]) + s[len - 1] + 'total': (['s'], [], lambda s: ('ite', Le(L(s), K(0)), K(0), + Add(App('total', Sub(s, K(0), Minus(L(s), K(1)))), At(s, Minus(L(s), K(1)))))), + # count(s, x) = occurrences of x + 'count': (['s'], ['x'], lambda s, x: ('ite', Le(L(s), K(0)), K(0), + Add(App('count', Sub(s, K(0), Minus(L(s), K(1))), x), + ('ite', Eq(At(s, Minus(L(s), K(1))), x), K(1), K(0))))), +} + +# ---- workloads -------------------------------------------------------------- +s, t, u = S('s'), S('t'), S('u') +x, i, j, k, n, lo, hi, a_, b_, c_, d_ = (I(v) for v in 'x i j k n lo hi a b c d'.split()) +def in_range(v, lo_, hi_): return And(Le(lo_, v), Lt(v, hi_)) +def sorted_(q): return ForallR('i1', K(0), L(q), ForallR('j1', I('i1'), L(q), Le(At(q, I('i1')), At(q, I('j1'))))) + +W = {} +def wl(name, hyps, ok, bad): + W[name] = (hyps, ok, bad) + +# W1 ground algebra +wl('g1_len_push', [], Eq(L(Push(s, x)), Add(L(s), K(1))), Eq(L(Push(s, x)), L(s))) +wl('g2_at_push', [], Eq(At(Push(s, x), L(s)), x), Eq(At(Push(s, x), Add(L(s), K(1))), x)) +wl('g3_at_upd', [in_range(i, K(0), L(s))], Eq(At(Upd(s, i, x), i), x), + Imp(Lt(Add(i, K(1)), L(s)), Eq(At(Upd(s, i, x), Add(i, K(1))), x))) +wl('g4_len_cat', [], Eq(L(Cat(s, t)), Add(L(s), L(t))), Eq(L(Cat(s, t)), L(s))) +wl('g5_len_sub', [Le(K(0), lo), Le(lo, hi), Le(hi, L(s))], Eq(L(Sub(s, lo, hi)), Minus(hi, lo)), + Eq(L(Sub(s, lo, hi)), hi)) +wl('g6_at_sub', [Le(K(0), lo), Le(lo, hi), Le(hi, L(s)), in_range(k, K(0), Minus(hi, lo))], + Eq(At(Sub(s, lo, hi), k), At(s, Add(lo, k))), Eq(At(Sub(s, lo, hi), k), At(s, k))) +# W2 sequence equalities +wl('e1_cat_assoc', [], SEq(Cat(Cat(s, t), u), Cat(s, Cat(t, u))), SEq(Cat(Cat(s, t), u), Cat(Cat(t, s), u))) +wl('e2_take_cat', [], SEq(Sub(Cat(s, t), K(0), L(s)), s), SEq(Sub(Cat(s, t), K(0), L(s)), t)) +wl('e3_drop_last_cat', [Lt(K(0), L(t))], + SEq(Sub(Cat(s, t), K(0), Minus(L(Cat(s, t)), K(1))), Cat(s, Sub(t, K(0), Minus(L(t), K(1))))), + SEq(Sub(Cat(s, t), K(0), Minus(L(Cat(s, t)), K(1))), Cat(s, Sub(t, K(1), L(t))))) +wl('e4_take_push', [], SEq(Sub(Push(s, x), K(0), L(s)), s), SEq(Sub(Push(s, x), K(1), Add(L(s), K(1))), s)) +wl('e5_upd_same', [in_range(i, K(0), L(s))], SEq(Upd(s, i, At(s, i)), s), SEq(Upd(s, i, Add(At(s, i), K(1))), s)) +wl('e6_sub_sub', [Le(K(0), a_), Le(a_, b_), Le(b_, L(s)), Le(K(0), c_), Le(c_, d_), Le(d_, Minus(b_, a_))], + SEq(Sub(Sub(s, a_, b_), c_, d_), Sub(s, Add(a_, c_), Add(a_, d_))), + Imp(Lt(K(0), a_), SEq(Sub(Sub(s, a_, b_), c_, d_), Sub(s, c_, d_)))) +wl('e7_ext', [Eq(L(s), L(t))], + Imp(ForallR('m', K(0), L(s), Eq(At(s, I('m')), At(t, I('m')))), SEq(s, t)), + SEq(s, t)) +wl('e8_split', [Le(K(0), k), Le(k, L(s))], SEq(s, Cat(Sub(s, K(0), k), Sub(s, k, L(s)))), + SEq(s, Cat(Sub(s, k, L(s)), Sub(s, K(0), k)))) +# W3 quantified element facts +wl('q1_inv_push', [Eq(L(s), n), Le(K(0), n), ForallR('m', K(0), n, Eq(At(s, I('m')), Fn('a', I('m'))))], + ForallR('m', K(0), Add(n, K(1)), Eq(At(Push(s, Fn('a', n)), I('m')), Fn('a', I('m')))), + ForallR('m', K(0), Add(n, K(1)), Eq(At(Push(s, Add(Fn('a', n), K(1))), I('m')), Fn('a', I('m'))))) +wl('q2_all_upd', [Forall('m', Le(K(0), At(s, I('m'))))], + Forall('m', Le(K(0), At(Upd(s, i, K(5)), I('m')))), + Imp(in_range(i, K(0), L(s)), Forall('m', Le(K(0), At(Upd(s, i, K(-5)), I('m')))))) +wl('q3_contains', [], ('iff', Contains(s, x), ExistsR('m', K(0), L(s), Eq(At(s, I('m')), x))), + Imp(Contains(s, x), Eq(At(s, K(0)), x))) +wl('q4_sorted_sub', [sorted_(s), Le(K(0), lo), Le(lo, hi), Le(hi, L(s))], sorted_(Sub(s, lo, hi)), + Imp(Le(K(2), L(s)), sorted_(Upd(s, K(0), Add(At(s, K(1)), K(1)))))) +# W4 recursive specs +wl('r1_total_push', [], Eq(App('total', Push(s, x)), Add(App('total', s), x)), + Eq(App('total', Push(s, x)), App('total', s))) +U = Sub(t, K(0), Minus(L(t), K(1))) +IH = Eq(App('total', Cat(s, U)), Add(App('total', s), App('total', U))) +HINT1 = SEq(Sub(Cat(s, t), K(0), Minus(L(Cat(s, t)), K(1))), Cat(s, U)) +HINT2 = Eq(At(Cat(s, t), Minus(L(Cat(s, t)), K(1))), At(t, Minus(L(t), K(1)))) +GOAL = Eq(App('total', Cat(s, t)), Add(App('total', s), App('total', t))) +BADG = Eq(App('total', Cat(s, t)), Add(Add(App('total', s), App('total', t)), K(1))) +wl('r2_concat_hinted', [Lt(K(0), L(t)), IH, HINT1, HINT2], GOAL, BADG) +wl('r3_concat_unhinted', [Lt(K(0), L(t)), IH], GOAL, BADG) +wl('r4_count_push', [], Eq(App('count', Push(s, x), x), Add(App('count', s, x), K(1))), + Eq(App('count', Push(s, Add(x, K(1))), x), Add(App('count', s, x), K(1)))) +# W5 scale: a chain of pushes +def chain(m): + hyps = [SEq(S('c0'), EMPTY)] + [SEq(S(f'c{q+1}'), Push(S(f'c{q}'), K(q))) for q in range(m)] + last = S(f'c{m}') + return hyps, Eq(At(last, K(m // 2)), K(m // 2)), Eq(At(last, K(m // 2)), K(m // 2 + 1)) +for m in (50, 200): + h, ok, bad = chain(m); wl(f'c{m}_push_chain', h, ok, bad) + +# ---- encoders ------------------------------------------------------------- +def clamp_lo(lo_, ln): return f"(ite (< {lo_} 0) 0 (ite (> {lo_} {ln}) {ln} {lo_}))" +def clamp_hi(hi_, lo2, ln): return f"(ite (< {hi_} {lo2}) {lo2} (ite (> {hi_} {ln}) {ln} {hi_}))" + +class Native: + """Z3/cvc5 sequences, as cpp-verify encodes them (seq_at recfun).""" + name = 'N' + def __init__(self, lemmas=False, inline_at=False, element=False, split=False): + self.lemmas = lemmas or element; self.inline_at = inline_at + self.element = element + self.split = split + self.extra = [] + if lemmas: self.name = 'NL' + if inline_at: self.name = 'Ni' + if element: self.name = 'NX' + ('i' if inline_at else '') + if split: self.name = ('NX' + ('i' if inline_at else '') if element else 'N') + 'S' + def sort(self): return "(Seq Int)" + def preamble(self): + out = [] + if not self.inline_at: + out.append("(define-fun-rec seq_at ((x (Seq Int)) (i Int)) Int (ite (and (<= 0 i) (< i (seq.len x))) (seq.nth x i) 0))") + if self.lemmas and self.inline_at: + at = lambda q, i: f"(ite (and (<= 0 {i}) (< {i} (seq.len {q}))) (seq.nth {q} {i}) 0)" + out.append(f"(assert (forall ((a (Seq Int)) (b (Seq Int)) (k Int)) (! (= {at('(seq.++ a b)', 'k')} (ite (< k (seq.len a)) {at('a', 'k')} {at('b', '(- k (seq.len a))')})) :pattern ((seq.nth (seq.++ a b) k)))))") + out.append(f"(assert (forall ((x Int) (k Int)) (! (= {at('(seq.unit x)', 'k')} (ite (= k 0) x 0)) :pattern ((seq.nth (seq.unit x) k)))))") + out.append(f"(assert (forall ((a (Seq Int)) (o Int) (n Int) (k Int)) (! (=> (and (<= 0 o) (<= 0 n) (<= (+ o n) (seq.len a))) (= {at('(seq.extract a o n)', 'k')} (ite (and (<= 0 k) (< k n)) {at('a', '(+ o k)')} 0))) :pattern ((seq.nth (seq.extract a o n) k)))))") + elif self.lemmas: + out.append("(assert (forall ((a (Seq Int)) (b (Seq Int)) (k Int)) (! (= (seq_at (seq.++ a b) k) (ite (< k (seq.len a)) (seq_at a k) (seq_at b (- k (seq.len a))))) :pattern ((seq_at (seq.++ a b) k)))))") + out.append("(assert (forall ((x Int) (k Int)) (! (= (seq_at (seq.unit x) k) (ite (= k 0) x 0)) :pattern ((seq_at (seq.unit x) k)))))") + out.append("(assert (forall ((a (Seq Int)) (o Int) (n Int) (k Int)) (! (=> (and (<= 0 o) (<= 0 n) (<= (+ o n) (seq.len a))) (= (seq_at (seq.extract a o n) k) (ite (and (<= 0 k) (< k n)) (seq_at a (+ o k)) 0))) :pattern ((seq_at (seq.extract a o n) k)))))") + return out + def var_facts(self, v): return [] + def e(self, t): + k = t[0]; E = self.e + if k == 'svar': return t[1] + if k == 'ivar': return t[1] + if k == 'int': return str(t[1]) if t[1] >= 0 else f"(- {-t[1]})" + if k == 'empty': return "(as seq.empty (Seq Int))" + if k == 'unit': return f"(seq.unit {E(t[1])})" + if k == 'len': return f"(seq.len {E(t[1])})" + if k == 'at': + q, ix = E(t[1]), E(t[2]) + if self.inline_at: return f"(ite (and (<= 0 {ix}) (< {ix} (seq.len {q}))) (seq.nth {q} {ix}) 0)" + return f"(seq_at {q} {ix})" + if k == 'push': return f"(seq.++ {E(t[1])} (seq.unit {E(t[2])}))" + if k == 'upd': + q, ix, v = E(t[1]), E(t[2]), E(t[3]) + return (f"(ite (and (<= 0 {ix}) (< {ix} (seq.len {q}))) (seq.++ (seq.extract {q} 0 {ix}) (seq.unit {v}) " + f"(seq.extract {q} (+ {ix} 1) (- (seq.len {q}) {ix} 1))) {q})") + if k == 'cat': return f"(seq.++ {E(t[1])} {E(t[2])})" + if k == 'sub': + q, l_, h_ = E(t[1]), E(t[2]), E(t[3]) + if t[2][0] == 'int' and t[2][1] >= 0: + self.split_fact(t[1], l_, f"(- {h_} {l_})") + return f"(seq.extract {q} {l_} (- {h_} {l_}))" + self.split_fact(t[1], l_, f"(- {h_} {l_})") + return f"(ite (< {l_} 0) (seq.extract {q} 0 {h_}) (seq.extract {q} {l_} (- {h_} {l_})))" + if k == 'contains': + q, v = E(t[1]), E(t[2]) + c = f"(seq.contains {q} (seq.unit {v}))" + if self.element: + self.extra.append(f"(assert (= {c} (exists ((ck Int)) (and (<= 0 ck) (< ck (seq.len {q})) (= {self.at(q, 'ck')} {v})))))") + return c + if k == 'seq=': + a, b = E(t[1]), E(t[2]) + if self.element: + self.extra.append(f"(assert (=> (and (= (seq.len {a}) (seq.len {b})) (forall ((ei Int)) (=> (and (<= 0 ei) (< ei (seq.len {a}))) (= {self.at(a, 'ei')} {self.at(b, 'ei')})))) (= {a} {b})))") + return f"(= {a} {b})" + return common(self, t) + def split_fact(self, src, i, n): + """extract(a ++ b, i, n) for i >= 0 lies in b, in a, or across both.""" + if not self.split: return + if src[0] == 'push': a, b = self.e(src[1]), f"(seq.unit {self.e(src[2])})" + elif src[0] == 'cat': a, b = self.e(src[1]), self.e(src[2]) + else: return + whole = f"(seq.extract (seq.++ {a} {b}) {i} {n})" + la = f"(seq.len {a})" + split = (f"(ite (>= {i} {la}) (seq.extract {b} (- {i} {la}) {n}) " + f"(ite (<= (+ {i} {n}) {la}) (seq.extract {a} {i} {n}) " + f"(seq.++ (seq.extract {a} {i} (- {la} {i})) (seq.extract {b} 0 (- {n} (- {la} {i}))))))") + self.extra.append(f"(assert (=> (<= 0 {i}) (= {whole} {split})))") + def at(self, q, ix): + if self.inline_at: return f"(ite (and (<= 0 {ix}) (< {ix} (seq.len {q}))) (seq.nth {q} {ix}) 0)" + return f"(seq_at {q} {ix})" + +class Terms(Native): + """cpp-verify's encoding: per-term index facts quantified over the index, + extract split facts, the contains bridge, extensionality for refuted + equalities, and update as its spec body.""" + name = 'NT' + def __init__(self): + super().__init__(split=True) + self.name = 'NT' + self.polarity = 1 + self.named = {} + def term_fact(self, term, element): + if '(ite' in term: + if term not in self.named: + c = f"nt_t{len(self.named)}" + self.named[term] = c + self.extra.append(f"(declare-const {c} (Seq Int))") + self.extra.append(f"(assert (= {c} {term}))") + pat = self.named[term] + else: + pat = term + self.extra.append(f"(assert (forall ((tk Int)) (! (= (seq_at {pat} tk) {element('tk')}) :pattern ((seq_at {pat} tk)) :qid fact!index)))") + def e(self, t): + k = t[0]; E = self.e + if k == 'push': + q, v = E(t[1]), E(t[2]) + term = f"(seq.++ {q} (seq.unit {v}))" + self.term_fact(term, lambda K: f"(ite (= {K} (seq.len {q})) {v} (seq_at {q} {K}))") + return term + if k == 'cat': + a, b = E(t[1]), E(t[2]) + term = f"(seq.++ {a} {b})" + self.term_fact(term, lambda K: f"(ite (< {K} (seq.len {a})) (seq_at {a} {K}) (seq_at {b} (- {K} (seq.len {a}))))") + return term + if k == 'sub': + term = super().e(t) + q, l_, h_ = E(t[1]), E(t[2]), E(t[3]) + ln = f"(seq.len {q})" + fr = clamp_lo(l_, ln); to = clamp_hi(h_, fr, ln) + self.term_fact(term, lambda K: f"(ite (and (<= 0 {K}) (< {K} (- {to} {fr}))) (seq_at {q} (+ {fr} {K})) 0)") + return term + if k == 'upd': + s_, i_, x_ = t[1], t[2], t[3] + body = ('ite', And(Le(K(0), i_), Lt(i_, L(s_))), + Cat(Push(Sub(s_, K(0), i_), x_), Sub(s_, Add(i_, K(1)), L(s_))), s_) + return E(body) + if k == 'contains': + q, v = E(t[1]), E(t[2]) + c = f"(seq.contains {q} (seq.unit {v}))" + w = f"nt_w{len(self.extra)}" + self.extra.append(f"(declare-const {w} Int)") + self.extra.append(f"(assert (=> {c} (and (<= 0 {w}) (< {w} (seq.len {q})) (= (seq_at {q} {w}) {v}))))") + self.extra.append(f"(assert (forall ((ck Int)) (! (=> (and (<= 0 ck) (< ck (seq.len {q})) (= (seq_at {q} ck) {v})) {c}) :pattern ((seq_at {q} ck)) :qid fact!contains)))") + return c + if k == 'seq=': + a, b = E(t[1]), E(t[2]) + if self.polarity < 0: + ext = f"(and (= (seq.len {a}) (seq.len {b})) (forall ((ei Int)) (! (=> (and (<= 0 ei) (< ei (seq.len {a}))) (= (seq_at {a} ei) (seq_at {b} ei))) :qid q)))" + return f"(or (= {a} {b}) {ext})" + return f"(= {a} {b})" + if k == 'not': + self.polarity = -self.polarity + r = f"(not {E(t[1])})" + self.polarity = -self.polarity + return r + if k == '=>': + self.polarity = -self.polarity + l = E(t[1]) + self.polarity = -self.polarity + return f"(=> {l} {E(t[2])})" + if k == 'forall': + return f"(forall (({t[1]} Int)) (! {E(t[2])} :qid q))" + if k == 'forallr': + return f"(forall (({t[1]} Int)) (! (=> (and (<= {E(t[2])} {t[1]}) (< {t[1]} {E(t[3])})) {E(t[4])}) :qid q))" + if k == 'existsr': + return f"(exists (({t[1]} Int)) (! (and (<= {E(t[2])} {t[1]}) (< {t[1]} {E(t[3])}) {E(t[4])}) :qid q))" + if k in ('iff', '=', 'ite'): + saved = self.polarity; self.polarity = 0 + r = common(self, t) if k != 'ite' else f"(ite {E(t[1])} {E(t[2])} {E(t[3])})" + self.polarity = saved + return r + return super().e(t) + +class Axioms: + """Dafny/Verus style: an uninterpreted ASeq sort with triggered axioms; == on + sequences is Seq.Equal (extensional), as Dafny translates source ==.""" + name = 'AX' + def sort(self): return "ASeq" + def preamble(self): + return """(declare-sort ASeq 0) +(declare-fun Len (ASeq) Int) +(declare-fun At (ASeq Int) Int) +(declare-fun Push (ASeq Int) ASeq) +(declare-fun Upd (ASeq Int Int) ASeq) +(declare-fun Cat (ASeq ASeq) ASeq) +(declare-fun Sub (ASeq Int Int) ASeq) +(declare-fun Unit (Int) ASeq) +(declare-fun Empty () ASeq) +(declare-fun Contains (ASeq Int) Bool) +(declare-fun Equal (ASeq ASeq) Bool) +(assert (forall ((s ASeq)) (! (<= 0 (Len s)) :pattern ((Len s))))) +(assert (= (Len Empty) 0)) +(assert (forall ((s ASeq)) (! (=> (= (Len s) 0) (= s Empty)) :pattern ((Len s))))) +(assert (forall ((s ASeq) (i Int)) (! (=> (or (< i 0) (<= (Len s) i)) (= (At s i) 0)) :pattern ((At s i))))) +(assert (forall ((s ASeq) (v Int)) (! (= (Len (Push s v)) (+ 1 (Len s))) :pattern ((Push s v))))) +(assert (forall ((s ASeq) (v Int) (i Int)) (! (= (At (Push s v) i) (ite (= i (Len s)) v (At s i))) :pattern ((At (Push s v) i))))) +(assert (forall ((v Int)) (! (and (= (Len (Unit v)) 1) (= (At (Unit v) 0) v)) :pattern ((Unit v))))) +(assert (forall ((s ASeq) (i Int) (v Int)) (! (= (Len (Upd s i v)) (Len s)) :pattern ((Upd s i v))))) +(assert (forall ((s ASeq) (i Int) (v Int) (j Int)) (! (= (At (Upd s i v) j) (ite (and (<= 0 i) (< i (Len s)) (= j i)) v (At s j))) :pattern ((At (Upd s i v) j))))) +(assert (forall ((a ASeq) (b ASeq)) (! (= (Len (Cat a b)) (+ (Len a) (Len b))) :pattern ((Cat a b))))) +(assert (forall ((a ASeq) (b ASeq) (k Int)) (! (= (At (Cat a b) k) (ite (< k (Len a)) (At a k) (At b (- k (Len a))))) :pattern ((At (Cat a b) k))))) +(define-fun lo2 ((s ASeq) (lo Int)) Int (ite (< lo 0) 0 (ite (> lo (Len s)) (Len s) lo))) +(define-fun hi2 ((s ASeq) (lo Int) (hi Int)) Int (ite (< hi (lo2 s lo)) (lo2 s lo) (ite (> hi (Len s)) (Len s) hi))) +(assert (forall ((s ASeq) (lo Int) (hi Int)) (! (= (Len (Sub s lo hi)) (- (hi2 s lo hi) (lo2 s lo))) :pattern ((Sub s lo hi))))) +(assert (forall ((s ASeq) (lo Int) (hi Int) (k Int)) (! (= (At (Sub s lo hi) k) (ite (and (<= 0 k) (< k (- (hi2 s lo hi) (lo2 s lo)))) (At s (+ (lo2 s lo) k)) 0)) :pattern ((At (Sub s lo hi) k))))) +(assert (forall ((s ASeq) (x Int)) (! (= (Contains s x) (exists ((k Int)) (! (and (<= 0 k) (< k (Len s)) (= (At s k) x)) :pattern ((At s k))))) :pattern ((Contains s x))))) +(assert (forall ((a ASeq) (b ASeq)) (! (= (Equal a b) (and (= (Len a) (Len b)) (forall ((j Int)) (! (=> (and (<= 0 j) (< j (Len a))) (= (At a j) (At b j))) :pattern ((At a j)) :pattern ((At b j)))))) :pattern ((Equal a b))))) +(assert (forall ((a ASeq) (b ASeq)) (! (=> (Equal a b) (= a b)) :pattern ((Equal a b))))) +(assert (forall ((a ASeq) (b ASeq)) (! (and (= (Sub (Cat a b) 0 (Len a)) a) (= (Sub (Cat a b) (Len a) (+ (Len a) (Len b))) b)) :pattern ((Cat a b)))))""".split('\n') + def var_facts(self, v): return [] + def e(self, t): + k = t[0]; E = self.e + if k == 'svar': return t[1] + if k in ('ivar',): return t[1] + if k == 'int': return str(t[1]) if t[1] >= 0 else f"(- {-t[1]})" + if k == 'empty': return "Empty" + if k == 'unit': return f"(Unit {E(t[1])})" + if k == 'len': return f"(Len {E(t[1])})" + if k == 'at': return f"(At {E(t[1])} {E(t[2])})" + if k == 'push': return f"(Push {E(t[1])} {E(t[2])})" + if k == 'upd': return f"(Upd {E(t[1])} {E(t[2])} {E(t[3])})" + if k == 'cat': return f"(Cat {E(t[1])} {E(t[2])})" + if k == 'sub': return f"(Sub {E(t[1])} {E(t[2])} {E(t[3])})" + if k == 'contains': return f"(Contains {E(t[1])} {E(t[2])})" + if k == 'seq=': return f"(Equal {E(t[1])} {E(t[2])})" + return common(self, t) + +class Arrays: + """(length, array) with the array 0 outside [0, length).""" + name = 'A' + def sort(self): return None + def preamble(self): return [] + def var_facts(self, v): + return [f"(>= l_{v} 0)", f"(forall ((i Int)) (=> (or (< i 0) (>= i l_{v})) (= (select a_{v} i) 0)))"] + def p(self, t): + """(len, array) strings of a sequence term.""" + k = t[0]; E = self.e; P = self.p + if k == 'svar': return (f"l_{t[1]}", f"a_{t[1]}") + if k == 'empty': return ("0", "((as const (Array Int Int)) 0)") + if k == 'unit': return ("1", f"(store ((as const (Array Int Int)) 0) 0 {E(t[1])})") + if k == 'push': + l, a = P(t[1]); return (f"(+ {l} 1)", f"(store {a} {l} {E(t[2])})") + if k == 'upd': + l, a = P(t[1]); ix, v = E(t[2]), E(t[3]) + return (l, f"(ite (and (<= 0 {ix}) (< {ix} {l})) (store {a} {ix} {v}) {a})") + if k == 'cat': + (l1, a1), (l2, a2) = P(t[1]), P(t[2]) + return (f"(+ {l1} {l2})", f"(lambda ((q Int)) (ite (< q {l1}) (select {a1} q) (select {a2} (- q {l1}))))") + if k == 'sub': + l, a = P(t[1]); lo_, hi_ = E(t[2]), E(t[3]) + l2 = clamp_lo(lo_, l); h2 = clamp_hi(hi_, l2, l) + return (f"(- {h2} {l2})", f"(lambda ((q Int)) (ite (and (<= 0 q) (< q (- {h2} {l2}))) (select {a} (+ {l2} q)) 0))") + if k == 'app_seq': raise NotImplementedError + raise ValueError(k) + def e(self, t): + k = t[0]; E = self.e; P = self.p + if k == 'ivar': return t[1] + if k == 'int': return str(t[1]) if t[1] >= 0 else f"(- {-t[1]})" + if k == 'len': return P(t[1])[0] + if k == 'at': return f"(select {P(t[1])[1]} {E(t[2])})" + if k == 'contains': + l, a = P(t[1]); return f"(exists ((q Int)) (and (<= 0 q) (< q {l}) (= (select {a} q) {E(t[2])})))" + if k == 'seq=': + (l1, a1), (l2, a2) = P(t[1]), P(t[2]); return f"(and (= {l1} {l2}) (= {a1} {a2}))" + if k == 'app': + args = [] + for arg in t[2]: + if arg[0] in ('svar', 'empty', 'unit', 'push', 'upd', 'cat', 'sub'): + l, a = P(arg); args += [l, a] + else: args.append(E(arg)) + return f"({t[1]} {' '.join(args)})" + return common(self, t) + +def common(enc, t): + k = t[0]; E = enc.e + if k in ('=', '<', '<=', '+', '-', '=>'): return f"({k} {E(t[1])} {E(t[2])})" + if k == 'iff': return f"(= {E(t[1])} {E(t[2])})" + if k in ('and', 'or'): return f"({k} {' '.join(E(a) for a in t[1:])})" + if k == 'not': return f"(not {E(t[1])})" + if k == 'ite': return f"(ite {E(t[1])} {E(t[2])} {E(t[3])})" + if k == 'forall': return f"(forall (({t[1]} Int)) {E(t[2])})" + if k == 'forallr': return f"(forall (({t[1]} Int)) (=> (and (<= {E(t[2])} {t[1]}) (< {t[1]} {E(t[3])})) {E(t[4])}))" + if k == 'existsr': return f"(exists (({t[1]} Int)) (and (<= {E(t[2])} {t[1]}) (< {t[1]} {E(t[3])}) {E(t[4])}))" + if k == 'fn': return f"({t[1]} {' '.join(E(a) for a in t[2])})" + if k == 'app': + return f"({t[1]} {' '.join(E(a) for a in t[2])})" + if k == 'ivar': return t[1] + raise ValueError(k) + +def spec_defs(enc, used): + out = [] + for f in sorted(used): + sparams, iparams, body = SPECS[f] + args = [S(p) for p in sparams] + [I(p) for p in iparams] + b = enc.e(body(*args)) + if isinstance(enc, Arrays): + ps = ' '.join(f"(l_{p} Int) (a_{p} (Array Int Int))" for p in sparams) + else: + ps = ' '.join(f"({p} {enc.sort()})" for p in sparams) + ps += ''.join(f" ({p} Int)" for p in iparams) + out.append(f"(define-fun-rec {f} ({ps}) Int {b})") + return out + +def used_specs(t, acc): + if not isinstance(t, tuple): return + if t[0] == 'app': + acc.add(t[1]) + for a in t[2]: used_specs(a, acc) + return + for a in t[1:]: + if isinstance(a, tuple): used_specs(a, acc) + +def emit(enc, name, hyps, goal, logic): + fv = {} + for h in hyps: free_vars(h, fv) + free_vars(goal, fv) + used = set() + for h in hyps + [goal]: used_specs(h, used) + for f in used: + sp, ip, body = SPECS[f] + used_specs(body(*([S(p) for p in sp] + [I(p) for p in ip])), used) + lines = [f"(set-logic {logic})"] + lines += enc.preamble() + fns = set() + def fnames(t): + if not isinstance(t, tuple): return + if t[0] == 'fn': fns.add((t[1], len(t[2]))) + for a in t[1:]: + if isinstance(a, tuple): fnames(a) + elif isinstance(a, (list,)): [fnames(b) for b in a] + if t[0] in ('fn', 'app'): + for b in t[2]: fnames(b) + for h in hyps + [goal]: fnames(h) + for f, ar in sorted(fns): lines.append(f"(declare-fun {f} ({' '.join(['Int'] * ar)}) Int)") + for v, srt in sorted(fv.items()): + if srt == 'seq': + if isinstance(enc, Arrays): + lines.append(f"(declare-const l_{v} Int)"); lines.append(f"(declare-const a_{v} (Array Int Int))") + lines += [f"(assert {f})" for f in enc.var_facts(v)] + else: + lines.append(f"(declare-const {v} {enc.sort()})") + else: + lines.append(f"(declare-const {v} Int)") + if hasattr(enc, 'extra'): enc.extra = [] + if hasattr(enc, 'named'): enc.named = {} + lines += spec_defs(enc, used) + for h in hyps: lines.append(f"(assert {enc.e(h)})") + if hasattr(enc, 'polarity'): enc.polarity = -1 + lines.append(f"(assert (not {enc.e(goal)}))") + if hasattr(enc, 'polarity'): enc.polarity = 1 + if hasattr(enc, 'extra'): lines += list(dict.fromkeys(enc.extra)) + lines.append("(check-sat)") + return '\n'.join(lines) + '\n' + +if __name__ == '__main__': + out = sys.argv[1] + os.makedirs(out, exist_ok=True) + encs = [Native(), Native(lemmas=True), Native(inline_at=True), Native(element=True), + Native(element=True, inline_at=True), Native(split=True), + Native(element=True, inline_at=True, split=True), Terms(), Axioms(), + Arrays()] + count = 0 + for wname, (hyps, ok, bad) in W.items(): + for verdict, goal in (('ok', ok), ('bad', bad)): + for enc in encs: + for solver, logic in (('z3', 'ALL'), ('cvc5', 'ALL')): + if solver == 'cvc5' and isinstance(enc, Arrays): + continue + try: + text = emit(enc, wname, hyps, goal, logic) + except NotImplementedError: + continue + open(os.path.join(out, f"{wname}.{verdict}.{enc.name}.{solver}.smt2"), 'w').write(text) + count += 1 + print(count, 'files') diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 8801739d90..ee56418ee5 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -3586,6 +3586,17 @@ fresh context, the API's or `z3`'s, the same assertions are `unknown` `.github/workflows/cppverify-fuzz.yml`; `suite/archive_fuzzer.test` runs it on archives of the test programs. - Instrumented coverage: `scripts/coverage-verify.sh` (region target on `clang/lib/Verify`). +- Z3 gate: `clang/utils/cppverify-z3-gate/gate.sh BASE CANDIDATE` compares + two builds that differ in their Z3. Stage 1 solves the sequence benchmark + (`seqbench.py`, from the sequence-encoding study) in the production + encoding (NT) and the plain sequence theory (N), and judges each claim as + the verifier decides it, by NT with one job and by NT or N with more, where + they race; stage 2 verifies every Verify test program with both at one job + (`differential.py`). Losing a proof or a certified failure, or a function + Verified by one and Failed by the other, fails the gate; gains and time + changes are reported. `.github/workflows/cppverify-z3-gate.yml` runs it + weekly for Z3's newest release. + - Sanitizers: `-DCPPVERIFY_SANITIZER="address;undefined"` builds `clangVerify` and `cpp-verify` with AddressSanitizer and UndefinedBehaviorSanitizer beside an uninstrumented LLVM, Clang, and Z3, diff --git a/third_party/README.md b/third_party/README.md index 2231fb31c8..2dd7e80b08 100644 --- a/third_party/README.md +++ b/third_party/README.md @@ -19,6 +19,18 @@ git submodule update --init third_party/z3 Z3 is built as a separate CMake project, so its internal `opt` component never clashes with LLVM's `opt` tool. +### Upgrading Z3 + +A Z3 release replaces the vendored one only through the gate in +`clang/utils/cppverify-z3-gate`: `gate.sh BASE CANDIDATE`, with a build of each, +solves the sequence benchmark with both Z3 binaries and verifies every Verify +test program with both, and fails when the candidate loses a proof or a +certified failure, or when a function is verified by one and refuted by the +other. `.github/workflows/cppverify-z3-gate.yml` runs it every Monday for Z3's +newest release, and by hand for any tag; `-DCPPVERIFY_Z3_SOURCE_DIR=PATH` +builds cpp-verify with another Z3 tree. Proof-cache keys contain the exact Z3 +version, so an upgrade starts every cache afresh. + ### Use system Z3 instead (optional) ```bash diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 773c07003b..85248a3fb6 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -1029,6 +1029,18 @@ misbehaves on an input its precondition admits, when a counterexample does not reproduce, or when two backends decide differently (:doc:`book/part-ii/ch17-backends-modular-calls`). +**Z3 releases pass a gate.** A Z3 release replaces the built-in one only when +cpp-verify built with it loses nothing that 4.13.4 decides: no proof of a +valid claim or model of a false one in the sequence benchmark, as the +verifier poses them, and no proof or certified failure of any Verify test +program, with no function Verified by one and Failed by the other +(``clang/utils/cppverify-z3-gate``). CI runs the gate every week for Z3's +newest release. 0.2 keeps Z3 4.13.4: 5.3.2, the newest, gains a proof in the +benchmark and loses none there, but on the test programs it loses two proofs +(``even_mod``, ``count_reverse``) and a certified failure +(``break_heap_wrong`` ends ``solver.timeout`` after 66 s instead of failing in +2 s), as 4.16.0 and 5.1.0 did. + **Sanitizers every night.** The verifier's own code is now built with AddressSanitizer and UndefinedBehaviorSanitizer (``-DCPPVERIFY_SANITIZER``), and every Verify test program runs through that build every night; a report