From 69e363409fa0f289070a65188e259dad79208abc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 05:41:03 +0530 Subject: [PATCH 1/4] ci: Check --version, the counterexample, JSON, and clang++ rejecting a failure in the smoke test. --- .github/workflows/cppverify-smoke.sh | 56 ++++++++++++++++++++++++---- 1 file changed, 48 insertions(+), 8 deletions(-) diff --git a/.github/workflows/cppverify-smoke.sh b/.github/workflows/cppverify-smoke.sh index fa965767a5..2d81b8869d 100755 --- a/.github/workflows/cppverify-smoke.sh +++ b/.github/workflows/cppverify-smoke.sh @@ -1,10 +1,18 @@ #!/usr/bin/env bash -# Verifies a correct and an incorrect program with the cpp-verify and clang++ -# in the directory $1, and compiles the correct one with contracts verified. +# Checks the cpp-verify and clang++ in the directory $1: what --version +# reports, a correct program verified and compiled with its contracts +# verified, and an incorrect one rejected by both, with its counterexample in +# text and in JSON. set -euo pipefail BIN="$1" WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + +fail() { + echo "error: $1" >&2 + exit 1 +} cat > "$WORK/good.cpp" <<'EOF' #include @@ -32,18 +40,50 @@ int twice(int x) } EOF -"$BIN/cpp-verify" --version +"$BIN/cpp-verify" --version | tee "$WORK/version.txt" +grep -Eq '^cpp-verify [0-9]+\.[0-9]+\.[0-9]+' "$WORK/version.txt" || + fail "--version does not start with cpp-verify's version" +grep -Eq '^ based on LLVM [0-9]+\.[0-9]+\.[0-9]+' "$WORK/version.txt" || + fail "--version names no LLVM release" +grep -Eq '^ z3 +[0-9]+\.[0-9]+\.[0-9]+ +built in' "$WORK/version.txt" || + fail "--version names no built-in Z3" "$BIN/cpp-verify" "$WORK/good.cpp" | tee "$WORK/good.txt" -grep -q "Verified: abs_value" "$WORK/good.txt" +grep -q "Verified: abs_value" "$WORK/good.txt" || + fail "the correct program did not verify" if "$BIN/cpp-verify" "$WORK/bad.cpp" > "$WORK/bad.txt" 2>&1; then cat "$WORK/bad.txt" - echo "error: the incorrect program verified" >&2 - exit 1 + fail "the incorrect program verified" fi cat "$WORK/bad.txt" -grep -q "verification failed: twice" "$WORK/bad.txt" +grep -q "verification failed: twice" "$WORK/bad.txt" || + fail "the incorrect program's failure is missing" +grep -Eq "counterexample: x( \[[^]]*\])* = " "$WORK/bad.txt" || + fail "the incorrect program's counterexample is missing" + +if "$BIN/cpp-verify" --diagnostics-format=json "$WORK/bad.cpp" \ + > "$WORK/bad.json" 2> /dev/null; then + fail "the incorrect program verified with --diagnostics-format=json" +fi +cat "$WORK/bad.json" +grep -q '"function":"twice"' "$WORK/bad.json" && + grep -q '"status":"failed"' "$WORK/bad.json" && + grep -q '"name":"x"' "$WORK/bad.json" || + fail "the incorrect program's JSON record is missing" + +"$BIN/clang++" -std=c++17 -fverify-contracts -c "$WORK/good.cpp" \ + -o "$WORK/good.o" +test -s "$WORK/good.o" || fail "clang++ wrote no object for the correct program" + +if "$BIN/clang++" -std=c++17 -fverify-contracts -c "$WORK/bad.cpp" \ + -o "$WORK/bad.o" > "$WORK/bad-clang.txt" 2>&1; then + cat "$WORK/bad-clang.txt" + fail "clang++ -fverify-contracts compiled the incorrect program" +fi +cat "$WORK/bad-clang.txt" +grep -q "error: verification failed: twice" "$WORK/bad-clang.txt" || + fail "clang++ did not report the incorrect program's failure" +test ! -e "$WORK/bad.o" || fail "clang++ wrote an object for the incorrect program" -"$BIN/clang++" -std=c++17 -fverify-contracts -c "$WORK/good.cpp" -o "$WORK/good.o" echo "smoke test passed" From d1228f0ff1b64810a31534cda22d75adde4d8562 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 05:41:03 +0530 Subject: [PATCH 2/4] ci: Refuse a release whose --version names no LLVM release. --- .github/workflows/cppverify-release.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/cppverify-release.yml b/.github/workflows/cppverify-release.yml index 8b931973ee..4850a5bd41 100644 --- a/.github/workflows/cppverify-release.yml +++ b/.github/workflows/cppverify-release.yml @@ -85,6 +85,10 @@ jobs: *) echo "error: the tag $TAG does not match '$first'" >&2; exit 1 ;; esac llvm="$(dist/cpp-verify/bin/cpp-verify --version | sed -n 's/^ based on LLVM \([0-9.]*\).*/\1/p')" + if [ -z "$llvm" ]; then + echo "error: --version names no LLVM release" >&2 + exit 1 + fi name="cpp-verify-$version-llvm$llvm-${{ matrix.platform }}" series="$(echo "$version" | cut -d. -f1,2)" mv dist/cpp-verify "dist/$name" From 1da8533026da5347cbd299143ece841094a1fd96 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 10:35:30 +0530 Subject: [PATCH 3/4] ci: Find x anywhere in the smoke test's counterexample, as main lists result first. --- .github/workflows/cppverify-smoke.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/cppverify-smoke.sh b/.github/workflows/cppverify-smoke.sh index 2d81b8869d..955836f35f 100755 --- a/.github/workflows/cppverify-smoke.sh +++ b/.github/workflows/cppverify-smoke.sh @@ -59,7 +59,7 @@ fi cat "$WORK/bad.txt" grep -q "verification failed: twice" "$WORK/bad.txt" || fail "the incorrect program's failure is missing" -grep -Eq "counterexample: x( \[[^]]*\])* = " "$WORK/bad.txt" || +grep -Eq "counterexample: (.*, )?x( \[[^]]*\])* = " "$WORK/bad.txt" || fail "the incorrect program's counterexample is missing" if "$BIN/cpp-verify" --diagnostics-format=json "$WORK/bad.cpp" \ From 1b19e4443c21eb0ec34e5cfb4123ee42f4928eb1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 11:34:47 +0530 Subject: [PATCH 4/4] ci: Install the pinned Lean from its GitHub release, as releases.lean-lang.org refuses connections. --- .github/workflows/cppverify-ci.yml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/.github/workflows/cppverify-ci.yml b/.github/workflows/cppverify-ci.yml index d8959b2302..b8a0f8eae1 100644 --- a/.github/workflows/cppverify-ci.yml +++ b/.github/workflows/cppverify-ci.yml @@ -61,14 +61,22 @@ jobs: - name: Install build tools, cvc5, and Lean run: | + set -o pipefail sudo apt-get update - sudo apt-get install -y ninja-build ccache + sudo apt-get install -y ninja-build ccache zstd curl -sSfL -o "$RUNNER_TEMP/cvc5.zip" \ "https://github.com/cvc5/cvc5/releases/download/cvc5-${{ matrix.cvc5 }}/${{ matrix.cvc5-archive }}" unzip -q "$RUNNER_TEMP/cvc5.zip" -d "$RUNNER_TEMP/cvc5" dirname "$(find "$RUNNER_TEMP/cvc5" -name cvc5 -type f)" >> "$GITHUB_PATH" curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ - | sh -s -- -y --default-toolchain "$LEAN_TOOLCHAIN" + | sh -s -- -y --default-toolchain none + # From its GitHub release: elan's own source, releases.lean-lang.org, may be down. + version="${LEAN_TOOLCHAIN##*:v}" + toolchain="$HOME/.elan/toolchains/leanprover--lean4---v$version" + mkdir -p "$toolchain" + curl -sSfL "https://github.com/leanprover/lean4/releases/download/v$version/lean-$version-linux.tar.zst" \ + | tar --zstd -x --strip-components=1 -C "$toolchain" + "$HOME/.elan/bin/elan" default "$LEAN_TOOLCHAIN" echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - uses: actions/cache/restore@v4