Write witnesses from the trace via witnesscreator

.github/workflows/gradle.yml

@@ -6,9 +6,9 @@ on:
   workflow_dispatch:
 
 env:
-  SVCOMP_VENV_DIR_NAME: .venv_ubuntu_24_04_1__x86_64
-  WITNESS_CREATOR_VERSION: v0.1.1
-  WITNESS_CREATOR_SHA256: 8fc8810237c99bf7d709bdb8692142695e407b5681e818fcfe8b45f9c598d814
+  # Python of the SV-COMP execution environment (SV-COMP 2027: Ubuntu 26.04).
+  SVCOMP_PYTHON_VERSION: '3.14'
+  SVCOMP_BASE_IMAGE: docker.io/ubuntu:26.04
 
 jobs:
   build:
@@ -85,23 +85,6 @@ jobs:
         mkdir -p libs/java-library-path
         cp "${RUNNER_TEMP}/release-jars/build/svcomp-runtime/java-smt-latest.jar" \
           libs/java-library-path/java-smt-latest.jar
-    - name: Download WitnessCreator runtime
-      run: |
-        version="${WITNESS_CREATOR_VERSION}"
-        zip_name="witness-creator-${version#v}.zip"
-        zip_path="${RUNNER_TEMP}/${zip_name}"
-        runtime_dir="${RUNNER_TEMP}/witness-creator-runtime"
-
-        curl --fail --location --retry 3 \
-          --output "${zip_path}" \
-          "https://github.com/SWAT-project/WitnessCreator/releases/download/${version}/${zip_name}"
-        echo "${WITNESS_CREATOR_SHA256}  ${zip_path}" | sha256sum --check -
-
-        mkdir -p "${runtime_dir}"
-        unzip -q "${zip_path}" -d "${runtime_dir}"
-        test -f "${runtime_dir}/WitnessCreator/build/libs/WitnessCreator.jar"
-        test -f "${runtime_dir}/WitnessCreator/witnesses/default_violation.st"
-        test -f "${runtime_dir}/WitnessCreator/witnesses/witness.st"
     - name: Determine release channel
       id: meta
       run: |
@@ -148,24 +131,19 @@ jobs:
         } >> "${GITHUB_OUTPUT}"
     - name: Build SV-COMP Python runtime
       env:
-        VENV_DIR: ${{ runner.temp }}/svcomp-runtime/${{ env.SVCOMP_VENV_DIR_NAME }}
-      run: |
-        mkdir -p "$(dirname "${VENV_DIR}")"
-        /usr/bin/python3 -m venv --copies "${VENV_DIR}"
-        "${VENV_DIR}/bin/python3" -m pip install --no-deps -r scripts/svcomp-package/requirements.txt
-        "${VENV_DIR}/bin/python3" -m pip check
-        "${VENV_DIR}/bin/python3" -m pip freeze --all > "${VENV_DIR}/requirements.freeze.txt"
-        "${VENV_DIR}/bin/python3" -c "import fastapi, pydantic, z3"
+        SWAT_SVCOMP_PYTHON_VERSION: ${{ env.SVCOMP_PYTHON_VERSION }}
+      run: scripts/build-svcomp-python-runtime.sh "${RUNNER_TEMP}/svcomp-python"
     - name: Pack SV-COMP ZIP
       env:
         SWAT_SVCOMP_VERSION: ${{ steps.meta.outputs.version }}
         SWAT_SVCOMP_ARTIFACT_DIR: ${{ runner.temp }}/release-jars
-        SWAT_SVCOMP_RUNTIME_DIR: ${{ runner.temp }}/svcomp-runtime
-        SWAT_SVCOMP_WITNESS_CREATOR_DIR: ${{ runner.temp }}/witness-creator-runtime/WitnessCreator
+        SWAT_SVCOMP_PYTHON_DIR: ${{ runner.temp }}/svcomp-python
         SWAT_SVCOMP_COMMIT: ${{ github.sha }}
         SWAT_SVCOMP_REF: ${{ github.ref_name }}
         SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }}
       run: scripts/package-svcomp.sh
+    - name: Check SV-COMP ZIP in competition base image
+      run: scripts/check-svcomp-package.sh "build/distributions/${{ steps.meta.outputs.zip-name }}" "${SVCOMP_BASE_IMAGE}"
     - name: Upload SV-COMP ZIP artifact
       uses: actions/upload-artifact@v4
       with:

.gitignore

@@ -29,6 +29,8 @@ targets/sv-comp/wit4java/
 /.vscode/
 **/smt_files/
 **/witness/
+# ... but not the witness packages of the executor sources
+!symbolic-executor/src/**/witness/
 **/sv-comp/results/
 **/analysis/
 !targets/sv-comp/scripts/lib/analysis

scripts/build-svcomp-python-runtime.sh

@@ -0,0 +1,86 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Builds the Python dependency directory that ships in the SV-COMP archive as
+# libs/python/. The archive runs SymbolicExplorer with the competition
+# machine's system python3 and puts this directory first on PYTHONPATH, so no
+# virtual environment (and no absolute interpreter path) is baked into the ZIP.
+#
+# Wheels are resolved for the *target* interpreter, not the one running pip,
+# so this works on any build host (e.g. an ubuntu-24.04 CI runner building for
+# the Ubuntu 26.04 / Python 3.14 competition image).
+#
+# Usage: scripts/build-svcomp-python-runtime.sh <output-dir>
+#
+# Environment:
+#   SWAT_SVCOMP_PYTHON_VERSION  target CPython "major.minor" (default: 3.14,
+#                               the python3 of Ubuntu 26.04 / SV-COMP 2027)
+#   SWAT_SVCOMP_PIP             pip command to use (default: "python3 -m pip")
+#   SWAT_SVCOMP_WITNESSCREATOR  replaces the pinned witnesscreator requirement
+#                               (git tag) with a local source directory or
+#                               wheel, for builds against an unreleased version
+
+ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+REQUIREMENTS="${ROOT_DIR}/scripts/svcomp-package/requirements.txt"
+PY_VERSION="${SWAT_SVCOMP_PYTHON_VERSION:-3.14}"
+PIP_CMD="${SWAT_SVCOMP_PIP:-python3 -m pip}"
+OUT_DIR="${1:?usage: $0 <output-dir>}"
+
+[[ "$PY_VERSION" =~ ^3\.[0-9]+$ ]] || { echo "error: invalid SWAT_SVCOMP_PYTHON_VERSION: ${PY_VERSION}" >&2; exit 1; }
+PY_TAG="cp${PY_VERSION/./}"
+
+if [[ -e "$OUT_DIR" ]] && [[ -n "$(ls -A "$OUT_DIR")" ]]; then
+  echo "error: output directory is not empty: ${OUT_DIR}" >&2
+  exit 1
+fi
+mkdir -p "$OUT_DIR"
+
+# witnesscreator (pure Python, stdlib only) is pinned to a git tag and built from
+# source below; everything else comes as wheels for the target interpreter.
+WHEEL_REQUIREMENTS="$(mktemp "${TMPDIR:-/tmp}/swat-svcomp-requirements.XXXXXX")"
+trap 'rm -f "$WHEEL_REQUIREMENTS"' EXIT
+grep -v '^witnesscreator' "$REQUIREMENTS" > "$WHEEL_REQUIREMENTS"
+WITNESSCREATOR_REQ="${SWAT_SVCOMP_WITNESSCREATOR:-$(grep '^witnesscreator' "$REQUIREMENTS")}"
+[[ -n "$WITNESSCREATOR_REQ" ]] || { echo "error: no witnesscreator requirement in ${REQUIREMENTS}" >&2; exit 1; }
+
+# --no-deps: requirements.txt is a complete, pinned closure.
+# --only-binary: never compile on the build host (would target the wrong ABI).
+# shellcheck disable=SC2086
+$PIP_CMD install \
+  --disable-pip-version-check \
+  --no-cache-dir \
+  --no-compile \
+  --no-deps \
+  --only-binary=:all: \
+  --implementation cp \
+  --python-version "$PY_VERSION" \
+  --abi "$PY_TAG" \
+  --abi abi3 \
+  --abi none \
+  --platform manylinux_2_17_x86_64 \
+  --platform manylinux2014_x86_64 \
+  --platform manylinux_2_28_x86_64 \
+  --platform manylinux_2_34_x86_64 \
+  --platform any \
+  --target "$OUT_DIR" \
+  -r "$WHEEL_REQUIREMENTS"
+
+# Pure-Python package: built on the host, valid for any CPython >= 3.10.
+# shellcheck disable=SC2086
+$PIP_CMD install \
+  --disable-pip-version-check \
+  --no-cache-dir \
+  --no-compile \
+  --no-deps \
+  --target "$OUT_DIR" \
+  "$WITNESSCREATOR_REQ"
+
+# Console-script wrappers carry the build host's interpreter path; unused.
+rm -rf "${OUT_DIR}/bin"
+find "$OUT_DIR" -name '__pycache__' -type d -prune -exec rm -rf {} +
+
+# Non-hidden marker (BenchExec skips hidden files when collecting tool files).
+echo "$PY_VERSION" > "${OUT_DIR}/PYTHON_VERSION"
+cp "$REQUIREMENTS" "${OUT_DIR}/requirements.txt"
+
+echo "Python runtime for CPython ${PY_VERSION} written to: ${OUT_DIR}"

scripts/check-svcomp-package.sh

@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Checks an SV-COMP ZIP built by scripts/package-svcomp.sh against the archive
+# requirements (single top-level directory, LICENSE, README, smoketest.sh,
+# one-line --version) and runs it in a bare competition base image with only
+# the fm-tools required_ubuntu_packages installed, like `fm-weck smoke-test`.
+#
+# Usage: scripts/check-svcomp-package.sh <zip> [base-image]
+# Requires docker. Default base image: docker.io/ubuntu:26.04 (SV-COMP 2027).
+
+ZIP_PATH="$(realpath "${1:?usage: $0 <zip> [base-image]}")"
+BASE_IMAGE="${2:-docker.io/ubuntu:26.04}"
+# Keep in sync with required_ubuntu_packages in fm-tools data/swat.yml.
+UBUNTU_PACKAGES="python3 openjdk-17-jdk-headless"
+
+fail() {
+  echo "error: $*" >&2
+  exit 1
+}
+
+echo "ZIP: ${ZIP_PATH} ($(stat -c %s "$ZIP_PATH") bytes)"
+
+top_dirs="$(unzip -Z1 "$ZIP_PATH" | cut -d/ -f1 | sort -u)"
+[[ "$(wc -l <<< "$top_dirs")" -eq 1 ]] || fail "ZIP must have a single top-level directory, found: ${top_dirs//$'\n'/ }"
+
+check_dir="$(mktemp -d "${TMPDIR:-/tmp}/swat-svcomp-check.XXXXXX")"
+unzip -q "$ZIP_PATH" -d "$check_dir"
+tool_dir="${check_dir}/${top_dirs}"
+for f in LICENSE README.md smoketest.sh run-swat.sh libs/python/PYTHON_VERSION; do
+  [[ -f "${tool_dir}/${f}" ]] || fail "missing ${f} in archive root ${top_dirs}/"
+done
+[[ -x "${tool_dir}/run-swat.sh" && -x "${tool_dir}/smoketest.sh" ]] || fail "run-swat.sh and smoketest.sh must be executable"
+
+echo "Running checks in ${BASE_IMAGE} (packages: ${UBUNTU_PACKAGES})"
+docker run --rm -v "${tool_dir}:/tool" -w /tool -e UBUNTU_PACKAGES="$UBUNTU_PACKAGES" "$BASE_IMAGE" bash -euc '
+  apt-get update -qq
+  DEBIAN_FRONTEND=noninteractive apt-get install -y -qq --no-install-recommends $UBUNTU_PACKAGES > /dev/null
+  echo "python3: $(python3 --version)"
+  echo "java: $(java -version 2>&1 | head -n 1)"
+  PYTHONPATH=libs/python python3 -c "import fastapi, pydantic, uvicorn, requests, yaml, z3, witnesscreator; print(\"z3:\", z3.get_version_string())"
+  version="$(./run-swat.sh --version)"
+  echo "version: ${version}"
+  [ -n "$version" ] && [ "$(printf "%s\n" "$version" | wc -l)" -eq 1 ] || { echo "error: --version must print one non-empty line" >&2; exit 1; }
+  [ "$(./run-swat.sh -v)" = "$version" ] || { echo "error: -v and --version differ" >&2; exit 1; }
+  ./smoketest.sh > smoketest.out 2>&1 || { cat smoketest.out; exit 1; }
+  echo "smoketest stdout: $(wc -c < smoketest.out) bytes"
+  [ -f witness/witness.yml ] && [ -f witness/witness.graphml ] || { echo "error: smoketest left no witness/witness.yml + witness.graphml" >&2; exit 1; }
+  tail -n 1 smoketest.out
+'
+echo "SV-COMP package check passed."

scripts/package-svcomp.sh

@@ -10,18 +10,10 @@ set -euo pipefail
 #
 # - symbolic-executor/lib/symbolic-executor.jar
 #
-# Set SWAT_SVCOMP_WITNESS_CREATOR_DIR to the extracted WitnessCreator runtime
-# root from https://github.com/SWAT-project/WitnessCreator. The root must
-# contain:
-#
-# - build/libs/WitnessCreator.jar
-# - witnesses/default_violation.st
-# - witnesses/witness.st
-#
-# Set SWAT_SVCOMP_RUNTIME_DIR to a runtime package root that contains the
-# pinned SV-COMP Python environment:
-#
-# - .venv_ubuntu_24_04_1__x86_64/
+# Set SWAT_SVCOMP_PYTHON_DIR to the Python dependency directory produced by
+# scripts/build-svcomp-python-runtime.sh (it includes the witnesscreator
+# package that writes the witnesses). It is shipped as libs/python/ and used
+# with the competition machine's system python3 (no bundled venv).
 #
 # Z3 and JavaSMT are taken from the vendored files in this repository.
 #
@@ -38,19 +30,13 @@ PACKAGE_DIR="${WORK_DIR}/${PACKAGE_NAME}"
 DIST_DIR="${ROOT_DIR}/build/distributions"
 SUPPORT_DIR="${ROOT_DIR}/scripts/svcomp-package"
 ARTIFACT_DIR="$(cd "${SWAT_SVCOMP_ARTIFACT_DIR:-$ROOT_DIR}" && pwd)"
-RUNTIME_DIR="${SWAT_SVCOMP_RUNTIME_DIR:-${SWAT_SVCOMP_REFERENCE_DIR:-}}"
-WITNESS_CREATOR_DIR="${SWAT_SVCOMP_WITNESS_CREATOR_DIR:-}"
-VENV_DIR_NAME="${SWAT_SVCOMP_VENV_DIR_NAME:-.venv_ubuntu_24_04_1__x86_64}"
+PYTHON_DIR="${SWAT_SVCOMP_PYTHON_DIR:-}"
 LINUX_Z3_DIST="z3-4.15.4-x64-glibc-2.39"
 LINUX_Z3_ZIP="${ROOT_DIR}/libs/${LINUX_Z3_DIST}.zip"
 JAVA_SMT_JAR="${ROOT_DIR}/libs/java-library-path/java-smt-latest.jar"
 
-if [[ -n "$RUNTIME_DIR" ]]; then
-  RUNTIME_DIR="$(cd "$RUNTIME_DIR" && pwd)"
-fi
-
-if [[ -n "$WITNESS_CREATOR_DIR" ]]; then
-  WITNESS_CREATOR_DIR="$(cd "$WITNESS_CREATOR_DIR" && pwd)"
+if [[ -n "$PYTHON_DIR" ]]; then
+  PYTHON_DIR="$(cd "$PYTHON_DIR" && pwd)"
 fi
 
 fail() {
@@ -143,12 +129,6 @@ copy_artifact_file "$EXECUTOR_JAR" "$PACKAGE_DIR/symbolic-executor/lib/symbolic-
 
 copy_tree_files symbolic-explorer "$PACKAGE_DIR/symbolic-explorer"
 
-[[ -n "$WITNESS_CREATOR_DIR" ]] || fail "SWAT_SVCOMP_WITNESS_CREATOR_DIR must point to the extracted WitnessCreator runtime root"
-[[ -f "$WITNESS_CREATOR_DIR/build/libs/WitnessCreator.jar" ]] || fail "missing WitnessCreator JAR: ${WITNESS_CREATOR_DIR}/build/libs/WitnessCreator.jar"
-[[ -f "$WITNESS_CREATOR_DIR/witnesses/default_violation.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/default_violation.st"
-[[ -f "$WITNESS_CREATOR_DIR/witnesses/witness.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/witness.st"
-copy_artifact_tree "$WITNESS_CREATOR_DIR" "$PACKAGE_DIR/WitnessCreator"
-
 install_z3_runtime_file z3 0755
 install_z3_runtime_file libz3.so
 install_z3_runtime_file libz3java.so
@@ -159,8 +139,10 @@ copy_artifact_file "$JAVA_SMT_JAR" "$PACKAGE_DIR/libs/java-library-path/java-smt
 
 copy_tree_files "$SUPPORT_DIR/smoketest" "$PACKAGE_DIR/smoketest"
 
-[[ -n "$RUNTIME_DIR" ]] || fail "SWAT_SVCOMP_RUNTIME_DIR must point to a runtime package root containing ${VENV_DIR_NAME}"
-copy_artifact_tree "${RUNTIME_DIR}/${VENV_DIR_NAME}" "${PACKAGE_DIR}/${VENV_DIR_NAME}"
+[[ -n "$PYTHON_DIR" ]] || fail "SWAT_SVCOMP_PYTHON_DIR must point to the output of scripts/build-svcomp-python-runtime.sh"
+[[ -f "$PYTHON_DIR/PYTHON_VERSION" ]] || fail "missing ${PYTHON_DIR}/PYTHON_VERSION; build it with scripts/build-svcomp-python-runtime.sh"
+[[ -d "$PYTHON_DIR/witnesscreator" ]] || fail "missing witnesscreator package in ${PYTHON_DIR}; build it with scripts/build-svcomp-python-runtime.sh"
+copy_artifact_tree "$PYTHON_DIR" "${PACKAGE_DIR}/libs/python"
 
 mkdir -p "$DIST_DIR"
 ZIP_PATH="${DIST_DIR}/${PACKAGE_NAME}.zip"

scripts/svcomp-package/README.md

@@ -4,13 +4,21 @@ This archive contains a runnable SWAT package for SV-COMP style Java verificatio
 
 Important entry points:
 
-- `run-swat.sh`: verifier entry point used by BenchExec.
+- `run-swat.sh`: verifier entry point used by BenchExec (`run-swat.sh --version`
+  or `-v` prints the version).
 - `compile-target.sh`: helper used by `run_swat.py` to compile Java benchmark sources.
-- `smoketest.sh`: runs SWAT on two bundled smoke-test targets.
+- `smoketest.sh`: runs SWAT on the bundled smoke-test target.
 - `sv-comp.cfg`: SWAT configuration for SV-COMP mode.
 
-The package expects Java 17 and the bundled `.venv_ubuntu_24_04_1__x86_64`
-Python environment. `run-swat.sh` intentionally uses only that environment.
+Requirements (SV-COMP 2027 environment, Ubuntu 26.04): `python3` (3.14) and
+Java 17 (`openjdk-17-jdk-headless`, which also provides `javac`).
+
+All Python dependencies are bundled in `libs/python/` and are used with the
+system `python3`; no virtual environment is needed. They are built for the
+Python version recorded in `libs/python/PYTHON_VERSION`, and `run-swat.sh`
+refuses to start with a different one. Set `SWAT_PYTHON` to use another
+interpreter of that version. The full tool log of the last run is in `out.log`;
+stdout is truncated if it would exceed SV-COMP's output limit.
 
 Example:
 

scripts/svcomp-package/requirements.txt

@@ -1,19 +1,21 @@
+annotated-doc==0.0.4
 annotated-types==0.7.0
-anyio==4.6.2.post1
-boto==2.49.0
-certifi==2025.11.12
+anyio==4.12.1
+certifi==2026.1.4
 charset-normalizer==3.4.4
-click==8.1.7
-fastapi==0.115.5
-h11==0.14.0
-idna==3.10
-pydantic==2.10.0
-pydantic_core==2.27.0
-PyYAML==6.0.2
+click==8.3.1
+fastapi==0.128.0
+h11==0.16.0
+idna==3.11
+pydantic==2.12.5
+pydantic_core==2.41.5
+PyYAML==6.0.3
 requests==2.32.5
 sniffio==1.3.1
-starlette==0.41.3
-typing_extensions==4.12.2
-urllib3==2.5.0
-uvicorn==0.32.1
+starlette==0.50.0
+typing-inspection==0.4.2
+typing_extensions==4.15.0
+urllib3==2.6.3
+uvicorn==0.40.0
+witnesscreator @ git+https://github.com/SWAT-project/WitnessCreator@v1.0.0
 z3-solver==4.15.4.0