S8: a smoke test that checks more, and Lean from its GitHub release in CI

.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

.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"

.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 <cstdint>
@@ -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"