From e343ec10bb16495ae8bae85229a7612e3470de1b Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Thu, 15 Oct 2026 10:24:17 +0000 Subject: [PATCH 1/7] build: make SV-COMP archive run on Ubuntu 26.04 (SV-COMP 2027) The svcomp26 archive bundled a venv built on Ubuntu 24.04 whose interpreter points at /usr/bin/python3.12; on Ubuntu 26.04 (Python 3.14) the explorer dies with "No module named 'encodings'". Instead of a venv, ship the pinned Python dependencies as plain packages in libs/python/ and run with the system python3 plus PYTHONPATH. libs/ is already in the BenchExec tool-info REQUIRED_PATHS, so no benchexec change is needed. - scripts/build-svcomp-python-runtime.sh: resolves wheels for the target CPython (default 3.14) with pip --target/--python-version, so it runs on any build host (CI stays on ubuntu-24.04). - requirements.txt: bump to versions with cp314 wheels (pydantic_core 2.27.0 has none), matching symbolic-explorer/requirements.txt; drop unused boto. - run-swat.sh: accept --version as well as -v; check the interpreter matches libs/python/PYTHON_VERSION; cap stdout below SV-COMP's 2 MB limit (head + verdict lines + tail, full log kept in out.log). - run_swat.py: launch SymbolicExplorer with sys.executable. - scripts/check-svcomp-package.sh + CI step: verify archive layout and run --version and smoketest.sh in docker.io/ubuntu:26.04 with only the fm-tools required_ubuntu_packages installed. Refs #48 Co-Authored-By: Claude Opus 5.5 --- .github/workflows/gradle.yml | 20 ++++---- scripts/build-svcomp-python-runtime.sh | 65 +++++++++++++++++++++++++ scripts/check-svcomp-package.sh | 50 +++++++++++++++++++ scripts/package-svcomp.sh | 19 ++++---- scripts/svcomp-package/README.md | 16 ++++-- scripts/svcomp-package/requirements.txt | 29 +++++------ scripts/svcomp-package/run-swat.sh | 53 ++++++++++++++------ scripts/svcomp-package/run_swat.py | 5 +- 8 files changed, 200 insertions(+), 57 deletions(-) create mode 100755 scripts/build-svcomp-python-runtime.sh create mode 100755 scripts/check-svcomp-package.sh diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 65c9273f..215ab991 100644 --- a/.github/workflows/gradle.yml +++ b/.github/workflows/gradle.yml @@ -6,7 +6,11 @@ on: workflow_dispatch: env: - SVCOMP_VENV_DIR_NAME: .venv_ubuntu_24_04_1__x86_64 + # 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 + # WitnessCreator release bundled in the SV-COMP ZIP (release tag + SHA-256 of + # its witness-creator-.zip asset); a new release only changes these two. WITNESS_CREATOR_VERSION: v0.1.1 WITNESS_CREATOR_SHA256: 8fc8810237c99bf7d709bdb8692142695e407b5681e818fcfe8b45f9c598d814 @@ -148,24 +152,20 @@ 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_PYTHON_DIR: ${{ runner.temp }}/svcomp-python SWAT_SVCOMP_WITNESS_CREATOR_DIR: ${{ runner.temp }}/witness-creator-runtime/WitnessCreator 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: diff --git a/scripts/build-svcomp-python-runtime.sh b/scripts/build-svcomp-python-runtime.sh new file mode 100755 index 00000000..ae69143a --- /dev/null +++ b/scripts/build-svcomp-python-runtime.sh @@ -0,0 +1,65 @@ +#!/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 +# +# 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") + +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 }" + +[[ "$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" + +# --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 "$REQUIREMENTS" + +# 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}" diff --git a/scripts/check-svcomp-package.sh b/scripts/check-svcomp-package.sh new file mode 100755 index 00000000..010ae441 --- /dev/null +++ b/scripts/check-svcomp-package.sh @@ -0,0 +1,50 @@ +#!/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 [base-image] +# Requires docker. Default base image: docker.io/ubuntu:26.04 (SV-COMP 2027). + +ZIP_PATH="$(realpath "${1:?usage: $0 [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; 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" + tail -n 1 smoketest.out +' +echo "SV-COMP package check passed." diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh index c3a5e788..b804bd1d 100755 --- a/scripts/package-svcomp.sh +++ b/scripts/package-svcomp.sh @@ -18,10 +18,9 @@ set -euo pipefail # - 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 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,15 +37,14 @@ 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:-}}" +PYTHON_DIR="${SWAT_SVCOMP_PYTHON_DIR:-}" WITNESS_CREATOR_DIR="${SWAT_SVCOMP_WITNESS_CREATOR_DIR:-}" -VENV_DIR_NAME="${SWAT_SVCOMP_VENV_DIR_NAME:-.venv_ubuntu_24_04_1__x86_64}" 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)" +if [[ -n "$PYTHON_DIR" ]]; then + PYTHON_DIR="$(cd "$PYTHON_DIR" && pwd)" fi if [[ -n "$WITNESS_CREATOR_DIR" ]]; then @@ -159,8 +157,9 @@ 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" +copy_artifact_tree "$PYTHON_DIR" "${PACKAGE_DIR}/libs/python" mkdir -p "$DIST_DIR" ZIP_PATH="${DIST_DIR}/${PACKAGE_NAME}.zip" diff --git a/scripts/svcomp-package/README.md b/scripts/svcomp-package/README.md index 46852fdf..bf7fc7e2 100644 --- a/scripts/svcomp-package/README.md +++ b/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: diff --git a/scripts/svcomp-package/requirements.txt b/scripts/svcomp-package/requirements.txt index 5c32b0a4..df7d3303 100644 --- a/scripts/svcomp-package/requirements.txt +++ b/scripts/svcomp-package/requirements.txt @@ -1,19 +1,20 @@ +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 z3-solver==4.15.4.0 diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh index 424a3188..beb6c10c 100755 --- a/scripts/svcomp-package/run-swat.sh +++ b/scripts/svcomp-package/run-swat.sh @@ -1,17 +1,13 @@ #!/bin/bash +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -# Check if the '-v' argument is among the arguments, indicating that the user wants to see the version +# '-v' is what the BenchExec tool-info module passes; '--version' is the +# SV-COMP archive convention. Both print a single version line. for arg in "$@" do - # Check if '-v' is among the arguments - if [ "$arg" == "-v" ]; then - # Execute the Java command with base dir of this script - pushd "$(dirname "$0")" > /dev/null - java -cp ./symbolic-executor/lib/symbolic-executor.jar de.uzl.its.swat.Version - popd > /dev/null - # Exit with status 0 - exit 0 + if [ "$arg" == "-v" ] || [ "$arg" == "--version" ]; then + exec java -cp "$SCRIPT_DIR/symbolic-executor/lib/symbolic-executor.jar" de.uzl.its.swat.Version fi done @@ -59,14 +55,39 @@ done # fi -SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -VENV_PYTHON="$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/python3" - -if [ ! -x "$VENV_PYTHON" ]; then - echo "Error: Python runtime not found at $VENV_PYTHON" +# Python dependencies are shipped in libs/python (built for one CPython +# minor version, recorded in libs/python/PYTHON_VERSION) and used with the +# system python3. Override the interpreter with SWAT_PYTHON if needed. +PYTHON="${SWAT_PYTHON:-python3}" +PYTHON_LIBS="$SCRIPT_DIR/libs/python" +expected_py="$(cat "$PYTHON_LIBS/PYTHON_VERSION" 2>/dev/null)" +actual_py="$("$PYTHON" -c 'import sys; print("%d.%d" % sys.version_info[:2])' 2>/dev/null)" +if [ -z "$expected_py" ]; then + echo "Error: Python dependencies not found at $PYTHON_LIBS" exit 1 fi +if [ "$actual_py" != "$expected_py" ]; then + echo "Error: SWAT's Python dependencies were built for Python $expected_py, but '$PYTHON' is '${actual_py:-not runnable}'" + exit 1 +fi +export PYTHONPATH="$PYTHON_LIBS${PYTHONPATH:+:$PYTHONPATH}" +export PYTHONNOUSERSITE=1 echo "Running SWAT with arguments: $@" -"$VENV_PYTHON" -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1 -cat out.log +"$PYTHON" -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1 + +# SV-COMP requires tool output below 2 MB. Long explorations can log far more, +# so past the cap print the head, every verdict line, and the tail (which holds +# the final verdict and witness). The full log stays in out.log. +MAX_STDOUT_BYTES=$((1536 * 1024)) +log_size="$(stat -c %s out.log)" +if [ "$log_size" -le "$MAX_STDOUT_BYTES" ]; then + cat out.log +else + head -c $((256 * 1024)) out.log + echo + echo "[run-swat.sh] output truncated: ${log_size} bytes total; verdict lines and tail follow" + grep -F '[VERDICT ' out.log | head -n 200 | cut -c1-500 + echo "[run-swat.sh] ... tail ..." + tail -c $((1024 * 1024)) out.log +fi diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py index 6b883330..bd8fc6f3 100755 --- a/scripts/svcomp-package/run_swat.py +++ b/scripts/svcomp-package/run_swat.py @@ -101,9 +101,8 @@ def generate_command(args, property_file: str): library_path = os.path.join(SCRIPT_DIR, 'libs', 'java-library-path') logging_dir = os.path.join(SCRIPT_DIR, 'logs') - python3_path = os.path.join(SCRIPT_DIR, '.venv_ubuntu_24_04_1__x86_64/bin/python3') - - base_command = [ python3_path, "-u", os.path.join(SCRIPT_DIR, 'symbolic-explorer', 'SymbolicExplorer.py'), + # Same interpreter (and PYTHONPATH, via the inherited environment) as run-swat.sh set up. + base_command = [ sys.executable, "-u", os.path.join(SCRIPT_DIR, 'symbolic-explorer', 'SymbolicExplorer.py'), "-prp", property_file, "--agent", agent_path, "--config", config_path, From 737f96e97ab59b19cb5c77ccf9ca6cfc33fff864 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Thu, 15 Oct 2026 10:38:00 +0000 Subject: [PATCH 2/7] Emit YAML violation witnesses (format 2.3) for SV-COMP 2027 SV-COMP 2027 requires Java violation witnesses in the YAML format (version 2.3); WitnessCreator writes them from the executor's witness markers. This supplies what the markers were missing: - [WITNESS] markers now carry the index of the nondet call on its source line (per class, bytecode order = evaluation order), the JVM type descriptor of the value and the class' SourceFile attribute, so WitnessCreator can place the function_return waypoint at the closing parenthesis of the right call, render a typed Java literal and find the file of non-public or inner classes. - A new [WITNESS_TARGET] marker with the uncaught throwable and its stack trace is emitted by Witness.recordTarget, which the surrounding try/catch of main now calls instead of printStackTrace (the trace is still printed). WitnessCreator derives the target waypoint from the innermost frame inside the task sources. - Negative zero is recorded as -0.0 (BigDecimal has no sign for zero). - Harness (lib/witness.py) and competition wrapper (run_swat.py) pass both markers, the task's input paths and the property file to WitnessCreator (--input/--property/--out); sources are no longer copied around. Optional WitnessLint via SWAT_WITNESSLINT. - The package smoketest requires witness.yml with a target waypoint. Requires WitnessCreator >= the YAML-capable release (feat/yaml-witness-2.3); the CI pin WITNESS_CREATOR_VERSION/SHA256 must be bumped with it. Co-Authored-By: Claude Opus 5.5 --- .gitignore | 1 + scripts/svcomp-package/run-swat.sh | 32 +--- scripts/svcomp-package/run_swat.py | 71 +++++--- scripts/svcomp-package/smoketest.sh | 16 +- .../instrument/svcomp/SVCompClassAdapter.java | 22 ++- .../svcomp/SVCompMethodAdapter.java | 25 ++- .../SurroundingTryCatchMethodAdapter.java | 7 +- .../java/de/uzl/its/swat/witness/Witness.java | 167 ++++++++++++++---- targets/sv-comp/scripts/README.md | 6 + targets/sv-comp/scripts/lib/witness.py | 83 +++++---- 10 files changed, 301 insertions(+), 129 deletions(-) diff --git a/.gitignore b/.gitignore index 57b3d545..9c44923f 100644 --- a/.gitignore +++ b/.gitignore @@ -24,6 +24,7 @@ targets/applications/openhospital/oh_build/restler_working_dir/Compile targets/applications/openhospital/oh_build/restler_working_dir/RestlerResults targets/sv-comp/sv-benchmarks/ targets/sv-comp/wit4java/ +targets/sv-comp/WitnessCreator/ **/__pycache__ **/.venv/* /.vscode/ diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh index 424a3188..62a17e10 100755 --- a/scripts/svcomp-package/run-swat.sh +++ b/scripts/svcomp-package/run-swat.sh @@ -27,37 +27,7 @@ if [ -f "$second_last_path/Main.java" ]; then set -- "${@:1:$(($#-2))}" "$last_path" "$second_last_path" fi -# Loop through all provided paths and copy Java files preserving directory structure -for path in "$@"; do - if [ -d "$path" ]; then - # Find all Java files and preserve relative directory structure - find "$path" -type f -name "*.java" | while read src; do - rel_path="${src#$path/}" - dst_dir="./WitnessCreator/$(dirname "$rel_path")" - mkdir -p "$dst_dir" - cp "$src" "$dst_dir/" - done - echo "Java files from $path copied successfully to ./WitnessCreator/" - elif [ -f "$path" ] && [[ "$path" == *.java ]]; then - # If the argument is a single Java file, copy it - cp "$path" ./WitnessCreator/ - echo "File $path copied successfully to ./WitnessCreator/" - fi -done - -# # copy Main.java for Witness creation -# last_path="${@: -1}" -# file_to_copy="${last_path}/Main.java" -# -# # Check if the file exists -# if [ -f "$file_to_copy" ]; then -# # Copy the Main.java file to the current directory -# cp "$file_to_copy" ./WitnessCreator/. -# echo "File copied successfully to ./WitnessCreator/" -# else -# echo "Error: File not found." -# fi - +# The witness is created by run_swat.py directly from the given input paths. SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" VENV_PYTHON="$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/python3" diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py index 6b883330..8d36dca0 100755 --- a/scripts/svcomp-package/run_swat.py +++ b/scripts/svcomp-package/run_swat.py @@ -7,7 +7,11 @@ logging.basicConfig(level=logging.INFO) logger = logging.getLogger(__name__) SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__)) -WITNESS_PATH = os.path.join(SCRIPT_DIR, 'WitnessCreator/build/libs/WitnessCreator.jar') +ORIGINAL_CWD = os.getcwd() +WITNESS_DIR = os.path.join(SCRIPT_DIR, 'WitnessCreator') +WITNESS_PATH = os.path.join(WITNESS_DIR, 'build/libs/WitnessCreator.jar') +# Output lines carrying witness information: nondet values and the violating location +WITNESS_MARKERS = ('[WITNESS]', '[WITNESS_TARGET]') class ExecutionStatus(enum.Enum): @@ -145,30 +149,50 @@ def extract_last_round(out, marker="============================== ROUND"): return "\n ".join(out).split(marker)[-1] -def extract_markers(out, marker): +def extract_markers(out, markers): + if isinstance(markers, str): + markers = (markers,) res = [] for line in out.split("\n"): print(line) - if marker in line: + if any(marker in line for marker in markers): res.append(line) return res -def generate_witness(witness): - witness_dir = os.path.join(SCRIPT_DIR, 'WitnessCreator/') - with pushd(witness_dir): - # base64 encode the string - enc = base64.b64encode(witness.encode()) - cmd = [ - 'java', - '-jar', - WITNESS_PATH, - enc, - witness_dir - ] - print(cmd) +def swat_version(): + """The package version from BUILD_INFO.txt, written by scripts/package-svcomp.sh.""" + try: + with open(os.path.join(SCRIPT_DIR, 'BUILD_INFO.txt')) as f: + for line in f: + if line.startswith('version='): + return line[len('version='):].strip() + except OSError: + pass + return 'unknown' + +def generate_witness(witness, property_path, input_paths): + """Create witness.yml (format 2.3) and witness.graphml in the WitnessCreator directory. + + `property_path` and `input_paths` are the verifier's arguments as given by BenchExec; + they are resolved against the original working directory and end up in the witness. + """ + enc = base64.b64encode(witness.encode()).decode() + cmd = [ + 'java', + '-jar', + WITNESS_PATH, + enc, + '--out', WITNESS_DIR, + '--property', property_path, + '--producer-version', swat_version(), + ] + for path in input_paths: + cmd.extend(['--input', path]) + print(cmd) + with pushd(ORIGINAL_CWD): _, output = run_command_with_timeout(cmd) - print("WITNESS CREATED") - print(output) + print("WITNESS CREATED") + log_output(output) def log_output(output: List[str]): for line in output: @@ -180,9 +204,11 @@ def log_output(output: List[str]): # Look for property file in arguments # SV-COMP framework passes the .prp file directly as first argument property_file = None + property_path = None for arg in sys.argv[1:]: if arg.endswith('.prp'): property_file = os.path.basename(arg) + property_path = arg logger.info(f"Found property file in arguments: {property_file}") break @@ -193,6 +219,9 @@ def log_output(output: List[str]): logger.info(f"Using property file: {property_file}") + # The task's input files/directories, as given (everything but the property file) + input_paths = [arg for arg in sys.argv[1:] if arg != property_path] + target_dir = sys.argv[-1] cmd = generate_command(sys.argv[1:], property_file) local_target_dir = copy_target(target_dir) @@ -218,12 +247,12 @@ def log_output(output: List[str]): out = extract_last_round(output) verdict = extract_markers(out, f'[VERDICT {property_file}]') if "== ERROR" in str(verdict): - witnesses = extract_markers(out, '[WITNESS]') - generate_witness("\n".join(witnesses)) + witnesses = extract_markers(out, WITNESS_MARKERS) + generate_witness("\n".join(witnesses), property_path, input_paths) print(f'Witnesses:\n {witnesses}') # Print the generated witness file contents for validation on benchmark server - witness_file_path = os.path.join(SCRIPT_DIR, 'WitnessCreator', 'witness.graphml') + witness_file_path = os.path.join(WITNESS_DIR, 'witness.yml') if os.path.exists(witness_file_path): print("\n" + "="*80) print("WITNESS FILE CONTENTS:") diff --git a/scripts/svcomp-package/smoketest.sh b/scripts/svcomp-package/smoketest.sh index 95fb8c05..e816d1d0 100755 --- a/scripts/svcomp-package/smoketest.sh +++ b/scripts/svcomp-package/smoketest.sh @@ -1,12 +1,18 @@ #!/bin/bash cd "$(dirname "$0")" +rm -f WitnessCreator/witness.yml WitnessCreator/witness.graphml output="$("bash" "run-swat.sh" "../../sv-benchmarks/java/properties/valid-assert.prp" "smoketest/common" "smoketest")" -if echo "$output" | grep -q "\[VERDICT valid-assert.prp\] == ERROR"; then - echo "Smoketest passed!" - exit 0 -else - echo "Smoketest failed!" +if ! echo "$output" | grep -q "\[VERDICT valid-assert.prp\] == ERROR"; then + echo "Smoketest failed: no violation verdict!" exit 1 fi +# The violation must come with a YAML witness (format 2.3) for the smoketest target +if ! grep -q 'entry_type: "violation_sequence"' WitnessCreator/witness.yml 2>/dev/null \ + || ! grep -q 'type: "target"' WitnessCreator/witness.yml; then + echo "Smoketest failed: no violation witness with a target waypoint in WitnessCreator/witness.yml!" + exit 1 +fi +echo "Smoketest passed!" +exit 0 diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java index 8ed69119..798cac83 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompClassAdapter.java @@ -1,6 +1,8 @@ package de.uzl.its.swat.instrument.svcomp; import de.uzl.its.swat.common.Util; +import java.util.HashMap; +import java.util.Map; import org.objectweb.asm.ClassVisitor; import org.objectweb.asm.MethodVisitor; import org.objectweb.asm.Opcodes; @@ -15,6 +17,15 @@ public class SVCompClassAdapter extends ClassVisitor { private final String cname; + /** + * Number of nondet calls seen so far per source line of this class. Shared by all method + * adapters so that the witness can tell apart several nondet calls on one line. + */ + private final Map nondetCallsPerLine = new HashMap<>(); + + /** The source file name of the class (SourceFile attribute), empty if unknown. */ + private String sourceFile = ""; + /** * Constructor that calls the super from the default ClassVisitor * @@ -25,6 +36,14 @@ public SVCompClassAdapter(ClassVisitor cv, String cname) { this.cname = cname; } + @Override + public void visitSource(String source, String debug) { + if (source != null) { + sourceFile = source; + } + super.visitSource(source, debug); + } + /** * Visits a method of the class. This method must return a new MethodVisitor instance (or null) * each time it is called, i.e., it should not return a previously returned visitor. Addition: @@ -55,7 +74,8 @@ public MethodVisitor visitMethod( if (!cname.equals("org/sosy_lab/sv_benchmarks/Verifier")) { SVCompTransformer.getPrintBox().addMsg("Method: " + name); - return new SVCompMethodAdapter(access, mv, cname, name, desc); + return new SVCompMethodAdapter( + access, mv, cname, name, desc, sourceFile, nondetCallsPerLine); } return mv; } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java index df2a3877..c7082ae1 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java @@ -3,6 +3,7 @@ import de.uzl.its.swat.instrument.InternalTransformerType; import de.uzl.its.swat.instrument.Intrinsics; import de.uzl.its.swat.instrument.Transformer; +import java.util.Map; import org.objectweb.asm.Label; import org.objectweb.asm.MethodVisitor; import org.objectweb.asm.Opcodes; @@ -16,6 +17,8 @@ public class SVCompMethodAdapter extends LocalVariablesSorter { private final String cname; private final String name; private final String desc; + private final String sourceFile; + private final Map nondetCallsPerLine; int lineNumber = 0; /** @@ -24,14 +27,25 @@ public class SVCompMethodAdapter extends LocalVariablesSorter { * @param mv Parent MethodVisitor * @param name The method name * @param desc A string description of the parameters of the method + * @param sourceFile The source file name of the class (empty if unknown) + * @param nondetCallsPerLine Per-class counter of nondet calls per source line (shared between + * the methods of the class) */ public SVCompMethodAdapter( - int access, MethodVisitor mv, String cname, String name, String desc) { + int access, + MethodVisitor mv, + String cname, + String name, + String desc, + String sourceFile, + Map nondetCallsPerLine) { super(Opcodes.ASM9, access, desc, mv); identifier = cname + "/" + name; this.desc = desc; this.cname = cname; this.name = name; + this.sourceFile = sourceFile; + this.nondetCallsPerLine = nondetCallsPerLine; } @Override @@ -58,6 +72,9 @@ public void visitMethodInsn( String retType = descriptor.split("\\)")[1]; long nextId = Verifier.getNextId(); + // Index of this call among the nondet calls on the same source line (bytecode order + // follows the left-to-right evaluation order); lets the witness locate the call. + int callIndex = nondetCallsPerLine.merge(lineNumber, 1, Integer::sum) - 1; SVCompTransformer.getPrintBox().setContentPresent(true); SVCompTransformer.getPrintBox() .addMsg(" => Found " + name + " in line " + lineNumber); @@ -72,11 +89,15 @@ public void visitMethodInsn( mv.visitLdcInsn(lineNumber); mv.visitLdcInsn(cname); mv.visitLdcInsn(this.name + this.desc); + mv.visitLdcInsn(callIndex); + mv.visitLdcInsn(sourceFile); mv.visitMethodInsn( Opcodes.INVOKESTATIC, "de/uzl/its/swat/witness/Witness", "recordValue", - "(" + descriptor.substring(2) + "ILjava/lang/String;Ljava/lang/String;)V", + "(" + + descriptor.substring(2) + + "ILjava/lang/String;Ljava/lang/String;ILjava/lang/String;)V", false); mv.visitLdcInsn(nextId); SVCompTransformer.getPrintBox().addMsg(" => Adding Witness recording"); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java index bc59a3f2..5d74772a 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/symbolicwrapper/SurroundingTryCatchMethodAdapter.java @@ -67,8 +67,13 @@ private void addEndOfSurrounding() { visitInsn(Opcodes.DUP); + // Prints the stack trace and records the violating location for the witness visitMethodInsn( - Opcodes.INVOKEVIRTUAL, "java/lang/Throwable", "printStackTrace", "()V", false); + Opcodes.INVOKESTATIC, + "de/uzl/its/swat/witness/Witness", + "recordTarget", + "(Ljava/lang/Throwable;)V", + false); // Duplicate exception for instanceof check visitInsn(Opcodes.DUP); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java index 10e1e79d..db5262fc 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java @@ -3,75 +3,172 @@ import java.math.BigDecimal; import java.util.Base64; +/** + * Emits the witness markers that WitnessCreator turns into an SV-COMP violation witness. + * + *

Two kinds of markers are printed to stdout: + * + *

    + *
  • {@code [WITNESS] } for every value returned by a {@code Verifier.nondet*()} call. + * The payload is {@code + * value@@@line@@@className@@@methodDesc@@@callIndex@@@typeDesc@@@sourceFile}, where {@code + * callIndex} is the (0-based) index of the call among the nondet calls on the same source + * line of the class (bytecode order, which follows the left-to-right evaluation order), + * {@code typeDesc} is the JVM descriptor of the returned type and {@code sourceFile} the + * SourceFile attribute of the class (empty if unknown). + *
  • {@code [WITNESS_TARGET] } once for the uncaught throwable that ends the run. The + * payload is {@code throwableClass@@@frame;frame;...} with frames encoded as {@code + * className@@fileName@@line}, innermost first. + *
+ */ public class Witness { - public static void recordValue(boolean value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; + private static final String SEPARATOR = "@@@"; + private static final int MAX_TARGET_FRAMES = 64; + + private static void record( + String value, + String typeDesc, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { + String witness = + value + + SEPARATOR + + lineNumber + + SEPARATOR + + cname + + SEPARATOR + + desc + + SEPARATOR + + callIndex + + SEPARATOR + + typeDesc + + SEPARATOR + + sourceFile; String enc = Base64.getEncoder().encodeToString(witness.getBytes()); System.out.println("[WITNESS] " + enc); } - public static void recordValue(byte value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + boolean value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { + record(String.valueOf(value), "Z", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(char value, int lineNumber, String cname, String desc) { - int encVal = Integer.valueOf(value); - String witness = encVal + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + byte value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { + record(String.valueOf(value), "B", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(short value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + char value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { + // Chars are transported as their (unsigned) code point, WitnessCreator renders the literal + record(String.valueOf((int) value), "C", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(int value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + short value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { + record(String.valueOf(value), "S", lineNumber, cname, desc, callIndex, sourceFile); + } + + public static void recordValue( + int value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { + record(String.valueOf(value), "I", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(float value, int lineNumber, String cname, String desc) { + public static void recordValue( + float value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { // Use BigDecimal to avoid scientific notation (e.g., -2.022784E-6) // but handle special values (NaN, Infinity) which BigDecimal doesn't support String valueStr; if (Float.isNaN(value) || Float.isInfinite(value)) { valueStr = Float.toString(value); + } else if (value == 0.0f && 1.0f / value < 0.0f) { + valueStr = "-0.0"; // BigDecimal has no negative zero } else { valueStr = BigDecimal.valueOf(value).toPlainString(); } - String witness = valueStr + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + record(valueStr, "F", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(long value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + long value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { + record(String.valueOf(value), "J", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(double value, int lineNumber, String cname, String desc) { + public static void recordValue( + double value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { // Use BigDecimal to avoid scientific notation (e.g., 1.23E-10) // but handle special values (NaN, Infinity) which BigDecimal doesn't support String valueStr; if (Double.isNaN(value) || Double.isInfinite(value)) { valueStr = Double.toString(value); + } else if (value == 0.0 && 1.0 / value < 0.0) { + valueStr = "-0.0"; // BigDecimal has no negative zero } else { valueStr = BigDecimal.valueOf(value).toPlainString(); } - String witness = valueStr + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + record(valueStr, "D", lineNumber, cname, desc, callIndex, sourceFile); } - public static void recordValue(String value, int lineNumber, String cname, String desc) { - String witness = value + "@@@" + lineNumber + "@@@" + cname + "@@@" + desc; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + public static void recordValue( + String value, + int lineNumber, + String cname, + String desc, + int callIndex, + String sourceFile) { + record( + String.valueOf(value), + "Ljava/lang/String;", + lineNumber, + cname, + desc, + callIndex, + sourceFile); + } + + /** + * Records the throwable that escaped the entry method and prints its stack trace. The stack + * trace locates the violating statement for the witness' target waypoint. + * + * @param throwable the uncaught throwable + */ + public static void recordTarget(Throwable throwable) { + throwable.printStackTrace(); + StringBuilder sb = new StringBuilder(throwable.getClass().getName()).append(SEPARATOR); + StackTraceElement[] frames = throwable.getStackTrace(); + for (int i = 0; i < frames.length && i < MAX_TARGET_FRAMES; i++) { + if (i > 0) sb.append(';'); + StackTraceElement frame = frames[i]; + sb.append(frame.getClassName()) + .append("@@") + .append(frame.getFileName() == null ? "" : frame.getFileName()) + .append("@@") + .append(frame.getLineNumber()); + } + String enc = Base64.getEncoder().encodeToString(sb.toString().getBytes()); + System.out.println("[WITNESS_TARGET] " + enc); } } diff --git a/targets/sv-comp/scripts/README.md b/targets/sv-comp/scripts/README.md index 22ce37c6..2b53be54 100644 --- a/targets/sv-comp/scripts/README.md +++ b/targets/sv-comp/scripts/README.md @@ -61,6 +61,12 @@ scripts/ ./svcomp setup all ``` +Witnesses of violation results are written by WitnessCreator (expected at +`../WitnessCreator/{build/libs/WitnessCreator.jar,witnesses/}`) to the testcase's +`logs/witness/` as `witness.yml` (YAML format 2.3) and `witness.graphml` (legacy, validated with +wit4java). To additionally lint the YAML witness, point `SWAT_WITNESSLINT` at a WitnessLint +command, e.g. `SWAT_WITNESSLINT="/path/venv/bin/python /path/witnesslint/witnesslinter.py"`. + ### Test Commands ```bash diff --git a/targets/sv-comp/scripts/lib/witness.py b/targets/sv-comp/scripts/lib/witness.py index 16fd26c4..97d9d2ce 100644 --- a/targets/sv-comp/scripts/lib/witness.py +++ b/targets/sv-comp/scripts/lib/witness.py @@ -3,7 +3,7 @@ import os import enum import logging -import shutil +import shlex import subprocess import time from typing import List, Optional, Tuple @@ -14,6 +14,11 @@ SCRIPT_DIR = Path(__file__).resolve().parent.parent # Now in lib/, so go up one more level WITNESS_CREATION_PATH = (SCRIPT_DIR.parent / 'WitnessCreator' / 'build' / 'libs' / 'WitnessCreator.jar') WITNESS_VALIDATION_PATH = (SCRIPT_DIR.parent / 'wit4java' / 'bin' / 'wit4java') +# Output lines carrying witness information: nondet values and the violating location +WITNESS_MARKERS = ("[WITNESS]", "[WITNESS_TARGET]") +# Optional: command prefix of WitnessLint (e.g. "/path/venv/bin/python /path/witnesslinter.py"); +# when set, the YAML witness is linted after creation. Proper validator setup is tracked in #47. +WITNESSLINT_ENV = 'SWAT_WITNESSLINT' class ExecutionStatus(enum.Enum): SUCCESS = "success" @@ -38,26 +43,43 @@ def generate_and_validate_witness(ver_task: VerificationTask, output: List[str]) } out = extract_last_round(output) - witnesses = extract_markers(out, "[WITNESS]") + witnesses = extract_markers(out, WITNESS_MARKERS) if not witnesses: logger.debug("No witnesses found in output") return None, 0.0, 0.0 - witness_dir = assemble_files(info) + witness_dir = Path(info['log_dir']) / 'witness' + witness_dir.mkdir(parents=True, exist_ok=True) logger.info("Generating witness files") generation_start = time.perf_counter() - generate_witness(witness_dir, "\n".join(witnesses)) + generate_witness(witness_dir, "\n".join(witnesses), input_dirs(info), property_file(ver_task)) generation_time = time.perf_counter() - generation_start logger.info("Validating witness") validation_start = time.perf_counter() + lint_witness(witness_dir / 'witness.yml', input_dirs(info)) validation_result = validate_witness(info) validation_time = time.perf_counter() - validation_start return validation_result, generation_time, validation_time +def input_dirs(info: dict) -> List[str]: + """The task's source directories (classpath entries that are directories).""" + try: + classpath_index = info['command'].index('--classpath') + classpath_entries = info['command'][classpath_index + 1:] + except ValueError: + classpath_entries = [] + return [folder for folder in classpath_entries if Path(folder).is_dir()] + + +def property_file(ver_task: VerificationTask) -> Path: + """The property file of the task, e.g. sv-benchmarks/java/properties/valid-assert.prp.""" + return ver_task['file_path'].parent.parent / 'properties' / ver_task['category'].value + + def log_output(output: List[str]): for line in output: logger.info(line.strip()) @@ -115,15 +137,18 @@ def extract_last_round(out: List[str], marker: str = "========================== -def extract_markers(out: str, marker: str) -> List[str]: +def extract_markers(out: str, markers) -> List[str]: + if isinstance(markers, str): + markers = (markers,) res: List[str] = [] for line in out.split("\n"): logger.debug(line) - if marker in line: + if any(marker in line for marker in markers): res.append(line) return res -def generate_witness(witness_dir: str, witness: str) -> None: +def generate_witness(witness_dir: Path, witness: str, inputs: List[str], prp: Path) -> None: + """Create witness.yml (format 2.3) and witness.graphml in `witness_dir` from the marker lines.""" with pushd(str(SCRIPT_DIR.parent / 'WitnessCreator')): # base64 encode the string enc = base64.b64encode(witness.encode()).decode() @@ -132,13 +157,30 @@ def generate_witness(witness_dir: str, witness: str) -> None: '-jar', str(WITNESS_CREATION_PATH), enc, - str(witness_dir) + '--out', str(witness_dir), + '--property', str(prp), + '--producer-version', 'local', ] + for folder in inputs: + cmd.extend(['--input', folder]) logger.info(f"Running witness creator: {cmd}") _, output = run_command_with_timeout(cmd) logger.info("Witness created") log_output(output) +def lint_witness(witness_file: Path, inputs: List[str]) -> Optional[bool]: + """Run WitnessLint on the YAML witness if SWAT_WITNESSLINT is set; True iff the witness is well-formed.""" + linter = os.environ.get(WITNESSLINT_ENV) + if not linter or not witness_file.exists(): + return None + cmd = shlex.split(linter) + ['--expectViolationWitness', '--expectedWitnessVersion', '2', + '--witness', str(witness_file)] + inputs + status, output = run_command_with_timeout(cmd) + log_output(output) + ok = status == ExecutionStatus.SUCCESS and any('finished with exit code 0' in line for line in output) + logger.info(f"WitnessLint: {'well-formed' if ok else 'FAULTY'} ({witness_file})") + return ok + def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[ExecutionStatus, list[str]]: """Executes the given command and returns output from both STDOUT and STDERR.""" @@ -172,28 +214,3 @@ def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[Execut return ExecutionStatus.ERROR, output + [str(e)] -def assemble_files(info: dict) -> str: - witness_dir = Path(info['log_dir']) / 'witness' - witness_dir.mkdir(parents=True, exist_ok=True) - - try: - classpath_index = info['command'].index('--classpath') - classpath_entries = info['command'][classpath_index + 1:] - except ValueError: - classpath_entries = [] - - for folder in classpath_entries: - folder_path = Path(folder) - if not folder_path.exists(): - continue - for src in folder_path.rglob('*.java'): - # Preserve relative path structure (package directories) for WitnessCreator - rel_path = src.relative_to(folder_path) - dst = witness_dir / rel_path - dst.parent.mkdir(parents=True, exist_ok=True) - logger.info(f"Copying {src} to {dst}") - shutil.copy(str(src), str(dst)) - - return str(witness_dir) - - \ No newline at end of file From 7430bef59da11b1d4945bae7f09a1f84f2b45fde Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Thu, 15 Oct 2026 13:34:33 +0000 Subject: [PATCH 3/7] Ship witness data in the trace instead of stdout markers The SV-COMP violation witness is built from two things the executor knows: the values returned by Verifier.nondet*() calls (with where each call is) and the throwable that escaped main (with where it was thrown). Until now both were printed as base64 [WITNESS]/[WITNESS_TARGET] markers to stdout and scraped by the driver. They now travel in the TraceDTO: - TraceDTO.nondetReturns: one NondetReturnDTO per nondet call with the Verifier function, the Java type, the value in its witness string form (integers decimal, char as code point, float/double via Java's Float/Double.toString plus the exact IEEE bits, boolean, raw String), the class, its SourceFile attribute, the line and the call index on that line (bytecode = evaluation order; computed by the SV-COMP adapters as before). - TraceDTO.violation: the throwable class and its stack frames innermost first, without JDK/SWAT frames, capped at 32; recorded by Witness.recordTarget from the surrounding try/catch of main (which still prints the stack trace the explorer derives the verdict from). Witness is now a static recorder (one JVM per execution); DTOBuilder attaches its data to every trace. The instrumentation records only the supported Verifier types, so an unsupported nondet (e.g. nondetObject) no longer breaks at the recording call. Tests: WitnessSpec (L0, value rendering and frame filtering) runs with the suite; SvcompWitnessAgentSpec forks a JVM with the agent in solver.mode=PRINT on a small SV-COMP target and checks the trace. It needs the built jar and runs via the new agentTest Gradle task (excluded from test). .gitignore no longer hides the executor's witness packages. Co-Authored-By: Claude Opus 5.5 --- .gitignore | 3 +- symbolic-executor/build.gradle | 20 +- .../svcomp/SVCompMethodAdapter.java | 44 +-- .../its/swat/symbolic/trace/DTOBuilder.java | 3 +- .../its/swat/symbolic/trace/dto/FrameDTO.java | 38 +++ .../symbolic/trace/dto/NondetReturnDTO.java | 101 +++++++ .../its/swat/symbolic/trace/dto/TraceDTO.java | 12 +- .../swat/symbolic/trace/dto/ViolationDTO.java | 37 +++ .../java/de/uzl/its/swat/witness/Witness.java | 259 +++++++++--------- .../witness/SvcompWitnessAgentSpec.groovy | 108 ++++++++ .../uzl/its/swat/witness/WitnessSpec.groovy | 144 ++++++++++ .../test/resources/targets/svcomp/Main.java | 21 ++ .../org/sosy_lab/sv_benchmarks/Verifier.java | 46 ++++ 13 files changed, 690 insertions(+), 146 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/FrameDTO.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/ViolationDTO.java create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy create mode 100644 symbolic-executor/src/test/resources/targets/svcomp/Main.java create mode 100644 symbolic-executor/src/test/resources/targets/svcomp/org/sosy_lab/sv_benchmarks/Verifier.java diff --git a/.gitignore b/.gitignore index 9c44923f..486a104a 100644 --- a/.gitignore +++ b/.gitignore @@ -24,12 +24,13 @@ targets/applications/openhospital/oh_build/restler_working_dir/Compile targets/applications/openhospital/oh_build/restler_working_dir/RestlerResults targets/sv-comp/sv-benchmarks/ targets/sv-comp/wit4java/ -targets/sv-comp/WitnessCreator/ **/__pycache__ **/.venv/* /.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 diff --git a/symbolic-executor/build.gradle b/symbolic-executor/build.gradle index 94841476..3abdf970 100644 --- a/symbolic-executor/build.gradle +++ b/symbolic-executor/build.gradle @@ -50,10 +50,12 @@ test { systemProperty "java.library.path", "../libs/java-library-path" // Surface SWAT errors as exceptions instead of halting the test JVM systemProperty "exitOnError", "false" - + useJUnitPlatform { excludeTags "slow" // skip @Tag("slow") tests } + // Forked-agent specs need the built agent jar; they run via agentTest + exclude '**/*AgentSpec*' testLogging { // Show events for passed, skipped, and failed tests @@ -63,6 +65,22 @@ test { } } +// Forked-agent tests: run a small target with the real agent (solver.mode=PRINT) and check the +// TraceDTO printed to stdout. Needs the agent jar in lib/, hence the copyJar dependency. +tasks.register('agentTest', Test) { + dependsOn copyJar + description = 'Runs the *AgentSpec tests against the built agent jar' + group = 'verification' + useJUnitPlatform() + filter { + includeTestsMatching '*AgentSpec' + } + testLogging { + events "passed", "failed", "skipped" + showStandardStreams = false + } +} + tasks.register('testFull', Test) { systemProperty "java.library.path", "../libs/java-library-path" // Surface SWAT errors as exceptions instead of halting the test JVM diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java index c7082ae1..60c60d32 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java @@ -4,6 +4,7 @@ import de.uzl.its.swat.instrument.Intrinsics; import de.uzl.its.swat.instrument.Transformer; import java.util.Map; +import java.util.Set; import org.objectweb.asm.Label; import org.objectweb.asm.MethodVisitor; import org.objectweb.asm.Opcodes; @@ -20,6 +21,10 @@ public class SVCompMethodAdapter extends LocalVariablesSorter { private final String sourceFile; private final Map nondetCallsPerLine; + /** Return type descriptors of the nondet methods whose values are recorded for the witness. */ + private static final Set WITNESS_VALUE_TYPES = + Set.of("Z", "B", "S", "C", "I", "J", "F", "D", "Ljava/lang/String;"); + int lineNumber = 0; /** * Constructor that calls the super from the default MethodVisitor @@ -81,26 +86,29 @@ public void visitMethodInsn( SVCompTransformer.getPrintBox().addMsg(" => Assigning ID: " + nextId); mv.visitLdcInsn(nextId); mv.visitMethodInsn(opcode, newOwner, name, newDescriptor, isInterface); - if (retType.equals("D") || retType.equals("J")) { - visitInsn(Opcodes.DUP2); - } else { - visitInsn(Opcodes.DUP); + if (WITNESS_VALUE_TYPES.contains(retType)) { + // Record the returned value with the call location for the witness (trace data) + if (retType.equals("D") || retType.equals("J")) { + visitInsn(Opcodes.DUP2); + } else { + visitInsn(Opcodes.DUP); + } + mv.visitLdcInsn(name); + mv.visitLdcInsn(cname); + mv.visitLdcInsn(sourceFile); + mv.visitLdcInsn(lineNumber); + mv.visitLdcInsn(callIndex); + mv.visitMethodInsn( + Opcodes.INVOKESTATIC, + "de/uzl/its/swat/witness/Witness", + "recordValue", + "(" + + retType + + "Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;II)V", + false); + SVCompTransformer.getPrintBox().addMsg(" => Adding Witness recording"); } - mv.visitLdcInsn(lineNumber); - mv.visitLdcInsn(cname); - mv.visitLdcInsn(this.name + this.desc); - mv.visitLdcInsn(callIndex); - mv.visitLdcInsn(sourceFile); - mv.visitMethodInsn( - Opcodes.INVOKESTATIC, - "de/uzl/its/swat/witness/Witness", - "recordValue", - "(" - + descriptor.substring(2) - + "ILjava/lang/String;Ljava/lang/String;ILjava/lang/String;)V", - false); mv.visitLdcInsn(nextId); - SVCompTransformer.getPrintBox().addMsg(" => Adding Witness recording"); /* if (descriptor.equals("()D") || descriptor.equals("()J")) { visitInsn(Opcodes.DUP2); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index e1156b95..454c3232 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -16,6 +16,7 @@ import de.uzl.its.swat.coverage.InstrCoverage; import de.uzl.its.swat.symbolic.trace.dto.*; import de.uzl.its.swat.thread.ThreadHandler; +import de.uzl.its.swat.witness.Witness; import java.util.ArrayList; import java.util.HashSet; import java.util.List; @@ -134,7 +135,7 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage trace.add(new BranchDTO(se.getIid(), se.getInst())); } } - return new TraceDTO(inputs, trace, ufs, buildMissingInvocations(statsStorage), symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange()); + return new TraceDTO(inputs, trace, ufs, buildMissingInvocations(statsStorage), Witness.getNondetReturns(), Witness.getViolation(), symbolicTrace.isSymbolicContextLoss(), symbolicPrecisionLoss, symbolicTrace.isReferenceSemanticChange()); } protected static String encodeCoverage(InstrCoverage instrCoverage) throws JsonProcessingException { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/FrameDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/FrameDTO.java new file mode 100644 index 00000000..57f9572c --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/FrameDTO.java @@ -0,0 +1,38 @@ +package de.uzl.its.swat.symbolic.trace.dto; + +/** One stack frame of the throwable that ended the execution (see {@link ViolationDTO}). */ +public class FrameDTO { + // The declaring class of the frame (dotted name) + private String className; + // The source file of the frame, empty if unknown + private String sourceFile; + // The source line of the frame, -1 if unknown + private int line; + + public FrameDTO(String className, String sourceFile, int line) { + this.className = className; + this.sourceFile = sourceFile; + this.line = line; + } + + /** Private default constructor for serialization */ + @SuppressWarnings("unused") + private FrameDTO() {} + + public String getClassName() { + return className; + } + + public String getSourceFile() { + return sourceFile; + } + + public int getLine() { + return line; + } + + @Override + public String toString() { + return className + "(" + sourceFile + ":" + line + ")"; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java new file mode 100644 index 00000000..607d72e4 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java @@ -0,0 +1,101 @@ +package de.uzl.its.swat.symbolic.trace.dto; + +/** + * A value returned by a {@code Verifier.nondet*()} call together with the location of the call. + * The explorer turns the sequence of these into the {@code function_return} waypoints of an + * SV-COMP violation witness. + */ +public class NondetReturnDTO { + // The Verifier method name, e.g. nondetInt + private String function; + // The Java type of the value: boolean|byte|short|char|int|long|float|double|String + private String type; + // The value in its witness string form: integers decimal, char as its code point, float/double + // as Java's Float/Double.toString, boolean true/false, String the raw string. + private String value; + // Exact IEEE-754 bits of a float/double value as 0x-prefixed hex, null for other types + private String bits; + // The class containing the call (dotted name) + private String className; + // The SourceFile attribute of that class, empty if unknown + private String sourceFile; + // The source line of the call + private int line; + // 0-based index among the nondet calls on that source line of that class (evaluation order) + private int callIndex; + + public NondetReturnDTO( + String function, + String type, + String value, + String bits, + String className, + String sourceFile, + int line, + int callIndex) { + this.function = function; + this.type = type; + this.value = value; + this.bits = bits; + this.className = className; + this.sourceFile = sourceFile; + this.line = line; + this.callIndex = callIndex; + } + + /** Private default constructor for serialization */ + @SuppressWarnings("unused") + private NondetReturnDTO() {} + + public String getFunction() { + return function; + } + + public String getType() { + return type; + } + + public String getValue() { + return value; + } + + public String getBits() { + return bits; + } + + public String getClassName() { + return className; + } + + public String getSourceFile() { + return sourceFile; + } + + public int getLine() { + return line; + } + + public int getCallIndex() { + return callIndex; + } + + @Override + public String toString() { + return "NondetReturnDTO{" + + function + + " -> " + + type + + " " + + value + + (bits == null ? "" : " (" + bits + ")") + + " at " + + className + + "(" + + sourceFile + + ":" + + line + + ")#" + + callIndex + + '}'; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java index 75eaf698..e4d3bfa2 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java @@ -17,6 +17,14 @@ public class TraceDTO { @SuppressWarnings("unused") private ArrayList missingInvocations; + // The values returned by Verifier.nondet*() calls with their call locations (witness data) + @SuppressWarnings("unused") + private ArrayList nondetReturns; + + // The throwable that escaped the entry method, null if the execution ended normally + @SuppressWarnings("unused") + private ViolationDTO violation; + @SuppressWarnings("unused") private boolean symbolicContextLoss = false; @SuppressWarnings("unused") @@ -24,11 +32,13 @@ public class TraceDTO { @SuppressWarnings("unused") private boolean referenceSemanticChange = false; - public TraceDTO(ArrayList inputs, ArrayList trace, ArrayList ufs, ArrayList missingInvocations, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) { + public TraceDTO(ArrayList inputs, ArrayList trace, ArrayList ufs, ArrayList missingInvocations, ArrayList nondetReturns, ViolationDTO violation, boolean symbolicContextLoss, boolean symbolicPrecisionLoss, boolean referenceSemanticChange) { this.trace = trace; this.inputs = inputs; this.ufs = ufs; this.missingInvocations = missingInvocations; + this.nondetReturns = nondetReturns; + this.violation = violation; this.symbolicContextLoss = symbolicContextLoss; this.symbolicPrecisionLoss = symbolicPrecisionLoss; this.referenceSemanticChange = referenceSemanticChange; diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/ViolationDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/ViolationDTO.java new file mode 100644 index 00000000..f9afd782 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/ViolationDTO.java @@ -0,0 +1,37 @@ +package de.uzl.its.swat.symbolic.trace.dto; + +import java.util.List; + +/** + * The throwable that escaped the entry method, recorded by the surrounding try/catch of main. The + * explorer derives the target waypoint of a violation witness from the innermost frame that lies + * in the task sources. + */ +public class ViolationDTO { + // The class name of the throwable, e.g. java.lang.AssertionError + private String throwable; + // The stack frames, innermost first; JDK and SWAT frames are left out + private List frames; + + public ViolationDTO(String throwable, List frames) { + this.throwable = throwable; + this.frames = frames; + } + + /** Private default constructor for serialization */ + @SuppressWarnings("unused") + private ViolationDTO() {} + + public String getThrowable() { + return throwable; + } + + public List getFrames() { + return frames; + } + + @Override + public String toString() { + return "ViolationDTO{" + throwable + " " + frames + '}'; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java index db5262fc..3c675ea6 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java @@ -1,174 +1,185 @@ package de.uzl.its.swat.witness; -import java.math.BigDecimal; -import java.util.Base64; +import de.uzl.its.swat.symbolic.trace.dto.FrameDTO; +import de.uzl.its.swat.symbolic.trace.dto.NondetReturnDTO; +import de.uzl.its.swat.symbolic.trace.dto.ViolationDTO; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; /** - * Emits the witness markers that WitnessCreator turns into an SV-COMP violation witness. - * - *

Two kinds of markers are printed to stdout: + * Records the data an SV-COMP violation witness is built from. The data travels to the explorer as + * part of the trace ({@code TraceDTO.nondetReturns} and {@code TraceDTO.violation}); nothing is + * printed for it. * *

    - *
  • {@code [WITNESS] } for every value returned by a {@code Verifier.nondet*()} call. - * The payload is {@code - * value@@@line@@@className@@@methodDesc@@@callIndex@@@typeDesc@@@sourceFile}, where {@code - * callIndex} is the (0-based) index of the call among the nondet calls on the same source - * line of the class (bytecode order, which follows the left-to-right evaluation order), - * {@code typeDesc} is the JVM descriptor of the returned type and {@code sourceFile} the - * SourceFile attribute of the class (empty if unknown). - *
  • {@code [WITNESS_TARGET] } once for the uncaught throwable that ends the run. The - * payload is {@code throwableClass@@@frame;frame;...} with frames encoded as {@code - * className@@fileName@@line}, innermost first. + *
  • {@link #recordValue} is invoked by the SV-COMP instrumentation right after every {@code + * Verifier.nondet*()} call with the returned value and the location of the call: the class, + * its SourceFile attribute, the line and the index of the call among the nondet calls on that + * line (bytecode order, which follows the left-to-right evaluation order). + *
  • {@link #recordTarget} is invoked by the surrounding try/catch of the entry method with the + * throwable that escaped it; its stack trace locates the violating statement. *
+ * + *

The state is static: every execution of the target runs in its own JVM, and the recording + * calls may happen before a thread context exists (e.g. in static initializers). */ -public class Witness { - private static final String SEPARATOR = "@@@"; - private static final int MAX_TARGET_FRAMES = 64; +public final class Witness { + /** Upper bound on the recorded stack frames of the violation (after dropping JDK/SWAT frames). */ + static final int MAX_FRAMES = 32; + + /** Class name prefixes of frames that cannot be the violating statement of the task. */ + private static final String[] SKIPPED_FRAME_PREFIXES = { + "java.", "javax.", "jdk.", "sun.", "com.sun.", "de.uzl.its.swat.", "shadow.swat." + }; + + private static final List nondetReturns = + Collections.synchronizedList(new ArrayList<>()); + private static volatile ViolationDTO violation = null; + + private Witness() {} private static void record( + String function, + String type, String value, - String typeDesc, - int lineNumber, + String bits, String cname, - String desc, - int callIndex, - String sourceFile) { - String witness = - value - + SEPARATOR - + lineNumber - + SEPARATOR - + cname - + SEPARATOR - + desc - + SEPARATOR - + callIndex - + SEPARATOR - + typeDesc - + SEPARATOR - + sourceFile; - String enc = Base64.getEncoder().encodeToString(witness.getBytes()); - System.out.println("[WITNESS] " + enc); + String sourceFile, + int line, + int callIndex) { + nondetReturns.add( + new NondetReturnDTO( + function, + type, + value, + bits, + cname.replace('/', '.'), + sourceFile == null ? "" : sourceFile, + line, + callIndex)); } public static void recordValue( - boolean value, - int lineNumber, - String cname, - String desc, - int callIndex, - String sourceFile) { - record(String.valueOf(value), "Z", lineNumber, cname, desc, callIndex, sourceFile); + boolean value, String function, String cname, String sourceFile, int line, int callIndex) { + record(function, "boolean", String.valueOf(value), null, cname, sourceFile, line, callIndex); } public static void recordValue( - byte value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { - record(String.valueOf(value), "B", lineNumber, cname, desc, callIndex, sourceFile); + byte value, String function, String cname, String sourceFile, int line, int callIndex) { + record(function, "byte", String.valueOf(value), null, cname, sourceFile, line, callIndex); } public static void recordValue( - char value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { - // Chars are transported as their (unsigned) code point, WitnessCreator renders the literal - record(String.valueOf((int) value), "C", lineNumber, cname, desc, callIndex, sourceFile); + short value, String function, String cname, String sourceFile, int line, int callIndex) { + record(function, "short", String.valueOf(value), null, cname, sourceFile, line, callIndex); } public static void recordValue( - short value, - int lineNumber, - String cname, - String desc, - int callIndex, - String sourceFile) { - record(String.valueOf(value), "S", lineNumber, cname, desc, callIndex, sourceFile); + char value, String function, String cname, String sourceFile, int line, int callIndex) { + // Chars travel as their (unsigned) code point; the witness renders the literal + record(function, "char", String.valueOf((int) value), null, cname, sourceFile, line, callIndex); } public static void recordValue( - int value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { - record(String.valueOf(value), "I", lineNumber, cname, desc, callIndex, sourceFile); + int value, String function, String cname, String sourceFile, int line, int callIndex) { + record(function, "int", String.valueOf(value), null, cname, sourceFile, line, callIndex); } public static void recordValue( - float value, - int lineNumber, - String cname, - String desc, - int callIndex, - String sourceFile) { - // Use BigDecimal to avoid scientific notation (e.g., -2.022784E-6) - // but handle special values (NaN, Infinity) which BigDecimal doesn't support - String valueStr; - if (Float.isNaN(value) || Float.isInfinite(value)) { - valueStr = Float.toString(value); - } else if (value == 0.0f && 1.0f / value < 0.0f) { - valueStr = "-0.0"; // BigDecimal has no negative zero - } else { - valueStr = BigDecimal.valueOf(value).toPlainString(); - } - record(valueStr, "F", lineNumber, cname, desc, callIndex, sourceFile); + long value, String function, String cname, String sourceFile, int line, int callIndex) { + record(function, "long", String.valueOf(value), null, cname, sourceFile, line, callIndex); } public static void recordValue( - long value, int lineNumber, String cname, String desc, int callIndex, String sourceFile) { - record(String.valueOf(value), "J", lineNumber, cname, desc, callIndex, sourceFile); + float value, String function, String cname, String sourceFile, int line, int callIndex) { + // Float.toString is exact enough to round-trip (incl. NaN, Infinity, -0.0); the raw bits + // let the witness reproduce the value bit for bit. + record( + function, + "float", + Float.toString(value), + "0x" + Integer.toHexString(Float.floatToRawIntBits(value)), + cname, + sourceFile, + line, + callIndex); } public static void recordValue( - double value, - int lineNumber, - String cname, - String desc, - int callIndex, - String sourceFile) { - // Use BigDecimal to avoid scientific notation (e.g., 1.23E-10) - // but handle special values (NaN, Infinity) which BigDecimal doesn't support - String valueStr; - if (Double.isNaN(value) || Double.isInfinite(value)) { - valueStr = Double.toString(value); - } else if (value == 0.0 && 1.0 / value < 0.0) { - valueStr = "-0.0"; // BigDecimal has no negative zero - } else { - valueStr = BigDecimal.valueOf(value).toPlainString(); - } - record(valueStr, "D", lineNumber, cname, desc, callIndex, sourceFile); + double value, String function, String cname, String sourceFile, int line, int callIndex) { + record( + function, + "double", + Double.toString(value), + "0x" + Long.toHexString(Double.doubleToRawLongBits(value)), + cname, + sourceFile, + line, + callIndex); } public static void recordValue( - String value, - int lineNumber, - String cname, - String desc, - int callIndex, - String sourceFile) { - record( - String.valueOf(value), - "Ljava/lang/String;", - lineNumber, - cname, - desc, - callIndex, - sourceFile); + String value, String function, String cname, String sourceFile, int line, int callIndex) { + record(function, "String", value == null ? "" : value, null, cname, sourceFile, line, callIndex); } /** - * Records the throwable that escaped the entry method and prints its stack trace. The stack - * trace locates the violating statement for the witness' target waypoint. + * Records the throwable that escaped the entry method and prints its stack trace (the explorer + * derives the verdict from that output). The frames locate the violating statement for the + * witness' target waypoint. * * @param throwable the uncaught throwable */ public static void recordTarget(Throwable throwable) { throwable.printStackTrace(); - StringBuilder sb = new StringBuilder(throwable.getClass().getName()).append(SEPARATOR); - StackTraceElement[] frames = throwable.getStackTrace(); - for (int i = 0; i < frames.length && i < MAX_TARGET_FRAMES; i++) { - if (i > 0) sb.append(';'); - StackTraceElement frame = frames[i]; - sb.append(frame.getClassName()) - .append("@@") - .append(frame.getFileName() == null ? "" : frame.getFileName()) - .append("@@") - .append(frame.getLineNumber()); + violation = describe(throwable); + } + + /** + * Builds the violation entry for a throwable: its class name and its stack frames, innermost + * first, without the JDK and SWAT frames (which cannot be the violating statement), capped at + * {@link #MAX_FRAMES}. + * + * @param throwable the throwable + * @return the violation entry + */ + public static ViolationDTO describe(Throwable throwable) { + List frames = new ArrayList<>(); + for (StackTraceElement frame : throwable.getStackTrace()) { + if (frames.size() >= MAX_FRAMES) break; + if (isSkipped(frame.getClassName())) continue; + frames.add( + new FrameDTO( + frame.getClassName(), + frame.getFileName() == null ? "" : frame.getFileName(), + frame.getLineNumber())); } - String enc = Base64.getEncoder().encodeToString(sb.toString().getBytes()); - System.out.println("[WITNESS_TARGET] " + enc); + return new ViolationDTO(throwable.getClass().getName(), frames); + } + + private static boolean isSkipped(String className) { + for (String prefix : SKIPPED_FRAME_PREFIXES) { + if (className.startsWith(prefix)) return true; + } + return false; + } + + /** The recorded nondet return values in execution order (a copy). */ + public static ArrayList getNondetReturns() { + synchronized (nondetReturns) { + return new ArrayList<>(nondetReturns); + } + } + + /** The recorded violation, or null if no throwable escaped the entry method (yet). */ + public static ViolationDTO getViolation() { + return violation; + } + + /** Clears the recorded data (for tests; a target execution never needs this). */ + public static void reset() { + nondetReturns.clear(); + violation = null; } } diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy new file mode 100644 index 00000000..ba2a337c --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy @@ -0,0 +1,108 @@ +package de.uzl.its.swat.witness + +import com.fasterxml.jackson.databind.ObjectMapper +import spock.lang.Shared +import spock.lang.Specification + +import javax.tools.ToolProvider +import java.nio.file.Files +import java.nio.file.Path +import java.util.concurrent.TimeUnit + +/** + * L2 (forked agent): the SV-COMP instrumentation records the witness data in the trace. A tiny + * SV-COMP style target is compiled and run with the agent in {@code solver.mode=PRINT}; the + * {@code TraceDTO} JSON printed to stdout must carry the nondet returns with their call locations + * and the violation with its frames. Runs via the {@code agentTest} Gradle task (needs the agent + * jar from {@code copyJar}). + */ +class SvcompWitnessAgentSpec extends Specification { + + static final Path AGENT_JAR = Path.of("lib", "symbolic-executor.jar").toAbsolutePath() + static final Path NATIVE_LIBS = Path.of("..", "libs", "java-library-path").toAbsolutePath() + static final Path TARGET_SOURCES = Path.of("src", "test", "resources", "targets", "svcomp").toAbsolutePath() + + @Shared Path classes + @Shared Map trace + @Shared String output + + def setupSpec() { + assert Files.isRegularFile(AGENT_JAR): "agent jar missing, run copyJar first: ${AGENT_JAR}" + classes = Files.createTempDirectory("swat-witness-agent-spec") + compile(classes) + output = run(classes, ["-Dswat.input.I_0=3", "-Dswat.input.I_1=4"]) + trace = parseTrace(output) + } + + def cleanupSpec() { + classes?.toFile()?.deleteDir() + } + + def "the trace carries every nondet return with its call location"() { + expect: + trace.nondetReturns.size() == 4 + trace.nondetReturns*.function == ["nondetInt", "nondetInt", "nondetDouble", "nondetString"] + trace.nondetReturns*.type == ["int", "int", "double", "String"] + trace.nondetReturns*.value == ["3", "4", "0.0", "fixed"] + trace.nondetReturns*.className == ["Main"] * 4 + trace.nondetReturns*.sourceFile == ["Main.java"] * 4 + trace.nondetReturns*.line == [14, 14, 15, 16] + trace.nondetReturns*.callIndex == [0, 1, 0, 0] + trace.nondetReturns[2].bits == "0x0" + trace.nondetReturns[0].bits == null + } + + def "the trace carries the violation with the frames of the task innermost first"() { + expect: + trace.violation != null + trace.violation.throwable == "java.lang.AssertionError" + trace.violation.frames*.className == ["Main", "Main"] + trace.violation.frames*.sourceFile == ["Main.java", "Main.java"] + trace.violation.frames*.line == [9, 18] + } + + def "the inputs of the trace still correspond to the nondet returns"() { + expect: + trace.inputs.size() == 4 + trace.inputs*.name.findAll { it.startsWith("I_") }.size() == 2 + } + + def "nothing is printed for the witness besides the trace"() { + expect: + !output.contains("[WITNESS]") + !output.contains("[WITNESS_TARGET]") + } + + private static void compile(Path outDir) { + def sources = Files.walk(TARGET_SOURCES).filter { it.toString().endsWith(".java") }.collect { it.toString() } + def args = ["-source", "1.8", "-target", "1.8", "-g", "-d", outDir.toString()] + sources + def err = new ByteArrayOutputStream() + int rc = ToolProvider.getSystemJavaCompiler().run(null, null, err, args as String[]) + assert rc == 0: "javac failed: ${err}" + } + + private static String run(Path classes, List inputs) { + def java = Path.of(System.getProperty("java.home"), "bin", "java").toString() + def cmd = [java, + "-javaagent:${AGENT_JAR}".toString(), + "-Djava.library.path=${NATIVE_LIBS}".toString(), + "-Dconfig.path=/nonexistent/swat.cfg", + "-Dinstrumentation.transformer=SV_COMP", + "-Dsolver.mode=PRINT", + "-DexitOnError=false", + "-DlogShadowStateToConsole=false"] + inputs + + ["-cp", classes.toString(), "-ea", "Main"] + def proc = new ProcessBuilder(cmd).directory(classes.toFile()).redirectErrorStream(true).start() + def out = proc.inputStream.text + assert proc.waitFor(5, TimeUnit.MINUTES): "target did not finish:\n${out}" + return out + } + + /** The TraceDTO is the single pretty-printed JSON object whose braces start at column 0. */ + private static Map parseTrace(String out) { + int start = out.indexOf("\n{\n") + int end = out.indexOf("\n}\n", start) + assert start >= 0 && end > start: "no trace JSON in output:\n${out}" + return new ObjectMapper().readValue(out.substring(start + 1, end + 2), Map) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy new file mode 100644 index 00000000..c7987f0a --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy @@ -0,0 +1,144 @@ +package de.uzl.its.swat.witness + +import de.uzl.its.swat.symbolic.trace.dto.NondetReturnDTO +import de.uzl.its.swat.symbolic.trace.dto.ViolationDTO +import spock.lang.Specification + +/** + * L0: the witness recorder renders nondet return values and the violation's stack frames in the + * form the witness library expects (see the witnesscreator API contract). + */ +class WitnessSpec extends Specification { + + def setup() { + Witness.reset() + } + + def cleanup() { + Witness.reset() + } + + def "a nondet return value is recorded with its call location"() { + when: + Witness.recordValue(42, "nondetInt", "pkg/Main", "Main.java", 12, 1) + List recorded = Witness.getNondetReturns() + + then: + recorded.size() == 1 + with(recorded[0]) { + function == "nondetInt" + type == "int" + value == "42" + bits == null + className == "pkg.Main" + sourceFile == "Main.java" + line == 12 + callIndex == 1 + } + } + + def "values are rendered in their witness string form (#type #description)"() { + when: + Witness.recordValue(*args) + NondetReturnDTO recorded = Witness.getNondetReturns()[0] + + then: + recorded.type == type + recorded.value == expectedValue + recorded.bits == expectedBits + + where: + description | args | type | expectedValue | expectedBits + "true" | [true, "nondetBoolean", "Main", "Main.java", 1, 0] | "boolean" | "true" | null + "negative" | [(byte) -5, "nondetByte", "Main", "Main.java", 1, 0] | "byte" | "-5" | null + "min" | [Short.MIN_VALUE, "nondetShort", "Main", "Main.java", 1, 0] | "short" | "-32768" | null + "code point" | [(char) 'A', "nondetChar", "Main", "Main.java", 1, 0] | "char" | "65" | null + "high code" | [(char) 0xFFFF, "nondetChar", "Main", "Main.java", 1, 0] | "char" | "65535" | null + "min" | [Integer.MIN_VALUE, "nondetInt", "Main", "Main.java", 1, 0] | "int" | "-2147483648" | null + "max" | [Long.MAX_VALUE, "nondetLong", "Main", "Main.java", 1, 0] | "long" | "9223372036854775807" | null + "plain" | [0.1f, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "0.1" | "0x3dcccccd" + "small" | [-2.022784E-6f, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "-2.022784E-6" | "0x" + Integer.toHexString(Float.floatToRawIntBits(-2.022784E-6f)) + "negative zero" | [-0.0f, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "-0.0" | "0x80000000" + "NaN" | [Float.NaN, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "NaN" | "0x7fc00000" + "infinity" | [Float.NEGATIVE_INFINITY, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "-Infinity" | "0xff800000" + "plain" | [1.23E-10d, "nondetDouble", "Main", "Main.java", 1, 0] | "double" | "1.23E-10" | "0x" + Long.toHexString(Double.doubleToRawLongBits(1.23E-10d)) + "negative zero" | [-0.0d, "nondetDouble", "Main", "Main.java", 1, 0] | "double" | "-0.0" | "0x8000000000000000" + "infinity" | [Double.POSITIVE_INFINITY, "nondetDouble", "Main", "Main.java", 1, 0] | "double" | "Infinity" | "0x7ff0000000000000" + "raw" | ["a \"quoted\"\\n", "nondetString", "Main", "Main.java", 1, 0] | "String" | "a \"quoted\"\\n" | null + "null" | [(String) null, "nondetString", "Main", "Main.java", 1, 0] | "String" | "" | null + } + + def "float and double strings round-trip to the recorded value"() { + when: + Witness.recordValue(f, "nondetFloat", "Main", "Main.java", 1, 0) + Witness.recordValue(d, "nondetDouble", "Main", "Main.java", 1, 0) + def recorded = Witness.getNondetReturns() + + then: + Float.floatToRawIntBits(Float.parseFloat(recorded[0].value)) == Float.floatToRawIntBits(f) + Double.doubleToRawLongBits(Double.parseDouble(recorded[1].value)) == Double.doubleToRawLongBits(d) + + where: + f << [0.33333334f, Float.MIN_VALUE, 16777217.0f, -3.4028235E38f] + d << [0.3333333333333333d, Double.MIN_VALUE, 9007199254740993.0d, 1.7976931348623157E308d] + } + + def "nondet returns keep their execution order"() { + when: + Witness.recordValue(1, "nondetInt", "Main", "Main.java", 5, 0) + Witness.recordValue(2, "nondetInt", "Main", "Main.java", 5, 1) + Witness.recordValue(3L, "nondetLong", "Main", "Main.java", 6, 0) + + then: + Witness.getNondetReturns()*.value == ["1", "2", "3"] + Witness.getNondetReturns()*.callIndex == [0, 1, 0] + } + + def "the violation records the throwable and its frames innermost first without JDK and SWAT frames"() { + given: + def throwable = new AssertionError("boom") + throwable.setStackTrace([ + new StackTraceElement("java.lang.Integer", "parseInt", "Integer.java", 652), + new StackTraceElement("de.uzl.its.swat.instrument.Intrinsics", "init", "Intrinsics.java", 1), + new StackTraceElement("pkg.Helper", "check", "Helper.java", 20), + new StackTraceElement("jdk.internal.reflect.NativeMethodAccessorImpl", "invoke0", null, -2), + new StackTraceElement("Main", "main", "Main.java", 8), + ] as StackTraceElement[]) + + when: + ViolationDTO violation = Witness.describe(throwable) + + then: + violation.throwable == "java.lang.AssertionError" + violation.frames*.className == ["pkg.Helper", "Main"] + violation.frames*.sourceFile == ["Helper.java", "Main.java"] + violation.frames*.line == [20, 8] + } + + def "the violation frames are capped"() { + given: + def throwable = new RuntimeException() + throwable.setStackTrace((1..(Witness.MAX_FRAMES + 10)).collect { + new StackTraceElement("pkg.Rec", "rec", "Rec.java", it) + } as StackTraceElement[]) + + expect: + Witness.describe(throwable).frames.size() == Witness.MAX_FRAMES + Witness.describe(throwable).frames[0].line == 1 + } + + def "an unknown source file is recorded as empty"() { + given: + def throwable = new RuntimeException() + throwable.setStackTrace([new StackTraceElement("Main", "main", null, -1)] as StackTraceElement[]) + + expect: + Witness.describe(throwable).frames[0].sourceFile == "" + Witness.describe(throwable).frames[0].line == -1 + } + + def "no violation is recorded until a throwable escapes"() { + expect: + Witness.getViolation() == null + } +} diff --git a/symbolic-executor/src/test/resources/targets/svcomp/Main.java b/symbolic-executor/src/test/resources/targets/svcomp/Main.java new file mode 100644 index 00000000..0356b322 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/svcomp/Main.java @@ -0,0 +1,21 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +/** + * SV-COMP style target for the agent test of the witness data in the trace: nondet calls of + * several types, two of them on one line, and an assertion that fails in a helper method. + */ +public class Main { + static int check(int a, int b) { + assert a + b != 7 : "witness target"; + return a + b; + } + + public static void main(String[] args) { + int a = Verifier.nondetInt(), b = Verifier.nondetInt(); + double d = Verifier.nondetDouble(); + String s = Verifier.nondetString(); + if (d < 0.5 && s.length() > 3) { + check(a, b); + } + } +} diff --git a/symbolic-executor/src/test/resources/targets/svcomp/org/sosy_lab/sv_benchmarks/Verifier.java b/symbolic-executor/src/test/resources/targets/svcomp/org/sosy_lab/sv_benchmarks/Verifier.java new file mode 100644 index 00000000..2dcbc9ac --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/svcomp/org/sosy_lab/sv_benchmarks/Verifier.java @@ -0,0 +1,46 @@ +package org.sosy_lab.sv_benchmarks; + +/** Minimal stand-in for the sv-benchmarks Verifier; the SV-COMP transformer redirects the calls. */ +public final class Verifier { + public static void assume(boolean condition) { + if (!condition) { + Runtime.getRuntime().halt(1); + } + } + + public static boolean nondetBoolean() { + return false; + } + + public static byte nondetByte() { + return 0; + } + + public static char nondetChar() { + return 0; + } + + public static short nondetShort() { + return 0; + } + + public static int nondetInt() { + return 0; + } + + public static long nondetLong() { + return 0; + } + + public static float nondetFloat() { + return 0; + } + + public static double nondetDouble() { + return 0; + } + + public static String nondetString() { + return ""; + } +} From feaa35921745e793cfa812cfb84fd2775ff01ead Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Thu, 15 Oct 2026 13:34:33 +0000 Subject: [PATCH 4/7] Write SV-COMP violation witnesses from the trace via witnesscreator In SV-COMP mode the explorer now writes witness.yml (format 2.3) and witness.graphml itself, from the trace of the round that produced the VIOLATION verdict, using the witnesscreator package (github.com/SWAT-project/WitnessCreator, pinned in requirements.txt). No stdout parsing for witnesses anymore. - ConstraintRequest carries nondetReturns and violation; the Database keeps the witness data of the latest trace per endpoint. The driver clears it before every round, so only a trace of the violating execution can provide it. - New arguments: --witness-dir (default: witness, relative to the working directory), --witness-input (the task's input files as given to the verifier), --witness-property, --witness-base-dir and --producer-version. - svcomp/WitnessWriter.py maps the trace data onto the witnesscreator API (Task, NondetReturn/Location, Violation/Frame, write_witnesses) and catches everything: the witness is written after the verdict line and can neither break nor delay it. Its time is recorded as witness generation time. - Verdict downgrades are unchanged; a witness is only written for a final VIOLATION. Co-Authored-By: Claude Opus 5.5 --- symbolic-explorer/SymbolicExplorer.py | 11 ++ .../constraint/ConstraintController.py | 6 +- .../constraint/ConstraintService.py | 18 ++- symbolic-explorer/data/Database.py | 23 +++- symbolic-explorer/driver/SVCompDriver.py | 23 ++++ .../parse/DataTransferObjects.py | 34 ++++++ symbolic-explorer/requirements.txt | 1 + symbolic-explorer/svcomp/WitnessWriter.py | 103 ++++++++++++++++++ 8 files changed, 213 insertions(+), 6 deletions(-) create mode 100644 symbolic-explorer/svcomp/WitnessWriter.py diff --git a/symbolic-explorer/SymbolicExplorer.py b/symbolic-explorer/SymbolicExplorer.py index c2bdf135..4cdd428d 100755 --- a/symbolic-explorer/SymbolicExplorer.py +++ b/symbolic-explorer/SymbolicExplorer.py @@ -132,6 +132,17 @@ def init_args(parser: argparse.ArgumentParser): parser.add_argument("--optimize", action="store_true", help="Enable Z3 optimizer to minimize variable values (slower but may produce simpler solutions)", default=False) parser.add_argument("--log-smt-formulas", action="store_true", help="Log SMT formulas and models to disk for debugging", default=False) + # SV-COMP witness arguments: the explorer writes the violation witness from the trace of the + # violating execution (needs the task's input files and property file as given to the verifier) + parser.add_argument("--witness-dir", default="witness", + help="Directory for witness.yml/witness.graphml, relative to the working directory (sv-comp mode)") + parser.add_argument("--witness-input", nargs='+', default=[], + help="The task's input files/directories exactly as given to the verifier") + parser.add_argument("--witness-property", help="Path to the property file of the task") + parser.add_argument("--witness-base-dir", + help="Directory relative witness input paths are resolved against (default: the working directory)") + parser.add_argument("--producer-version", default="unknown", help="Producer version recorded in the witness") + # HTTP-specific arguments parser.add_argument("--host", help="HTTP target host", default="localhost") parser.add_argument("--http-port", help="HTTP target port", type=int, default=8080) diff --git a/symbolic-explorer/constraint/ConstraintController.py b/symbolic-explorer/constraint/ConstraintController.py index 7b205a09..666c6cd8 100755 --- a/symbolic-explorer/constraint/ConstraintController.py +++ b/symbolic-explorer/constraint/ConstraintController.py @@ -42,6 +42,8 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str symbolicContextLoss = request.symbolicContextLoss symbolicPrecisionLoss = request.symbolicPrecisionLoss referenceSemanticChange = request.referenceSemanticChange + nondetReturns = request.nondetReturns + violation = request.violation # Start a new thread to add constraints thread = threading.Thread(target=ConstraintService.add_constraints, kwargs={ @@ -53,7 +55,9 @@ def post(request: ConstraintRequest, endpointID: str = Query(...), traceID: str 'missing_invocations': missingInvocations, 'symbolic_context_loss': symbolicContextLoss, 'symbolic_precision_loss': symbolicPrecisionLoss, - 'reference_semantic_change': referenceSemanticChange}) + 'reference_semantic_change': referenceSemanticChange, + 'nondet_returns': nondetReturns, + 'violation': violation}) thread.start() thread.join() # To ensure trace is added in SV-Comp mode # Return a response indicating that the request has been accepted diff --git a/symbolic-explorer/constraint/ConstraintService.py b/symbolic-explorer/constraint/ConstraintService.py index 14cee249..20fc8b5a 100755 --- a/symbolic-explorer/constraint/ConstraintService.py +++ b/symbolic-explorer/constraint/ConstraintService.py @@ -1,10 +1,10 @@ -from typing import List +from typing import List, Optional from data.Database import Database from parse.TraceParser import Parser from data.trace.Input import Input from data.trace.UF import UF -from parse.DataTransferObjects import TraceItem, InputItem, UFItem, InvocationItem +from parse.DataTransferObjects import TraceItem, InputItem, UFItem, InvocationItem, NondetReturnItem, ViolationItem from data.trace.Special import Special from data.trace.Branch import Branch @@ -24,7 +24,9 @@ class ConstraintService: def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inputs: List[InputItem], ufs: List[UFItem], symbolic_context_loss: bool, symbolic_precision_loss: bool, reference_semantic_change: bool = False, - missing_invocations: List[InvocationItem] = None): + missing_invocations: List[InvocationItem] = None, + nondet_returns: List[NondetReturnItem] = None, + violation: Optional[ViolationItem] = None): """ Adds constraints to the database. @@ -42,6 +44,8 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp symbolic_precision_loss (bool): A flag indicating whether the symbolic precision was lost (UFs introduced). reference_semantic_change (bool): A flag indicating whether reference equality semantics changed. missing_invocations (list): Methods that could not be modelled symbolically during this trace. + nondet_returns (list): The values returned by Verifier.nondet*() calls with their call locations. + violation (ViolationItem): The throwable that escaped the entry method, if any. Returns: None: The result is the side effect of adding data to the database. @@ -55,6 +59,12 @@ def add_constraints(endpoint_id: str, trace_id: str, trace: List[TraceItem], inp # Flatten the missing-invocation DTOs into plain dicts so the Database/Tree stay decoupled # from the pydantic request models. missing_invocations_data = [item.model_dump() for item in (missing_invocations or [])] + # The witness data of this execution (plain dicts as well); the Database keeps the latest. + witness_data = { + 'trace_id': trace_id, + 'nondet_returns': [item.model_dump() for item in (nondet_returns or [])], + 'violation': violation.model_dump() if violation is not None else None, + } # Adding the trace and inputs to the database for the specified endpoint. - Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change, missing_invocations_data) + Database.instance().add_trace(endpoint_id, trace_id, trace_parsed, inputs_parsed, ufs_parsed, symbolic_context_loss, symbolic_precision_loss, reference_semantic_change, missing_invocations_data, witness_data) logger.info(f'[CONSTRAINT SERVICE] Added trace {trace_id} to endpoint {endpoint_id}') diff --git a/symbolic-explorer/data/Database.py b/symbolic-explorer/data/Database.py index 489190bc..9b7b8af9 100755 --- a/symbolic-explorer/data/Database.py +++ b/symbolic-explorer/data/Database.py @@ -42,6 +42,8 @@ def __init__(self): self.instr_coverage = {'total_executed': {}, 'total_instr_count': 0, 'endpoints': {}} self.branch_coverage = {'total_executed': {}, 'total_branch_instr_count': 0} self.violations = {} + # Witness data (nondet returns, uncaught throwable) of the latest trace per endpoint + self.witness_data = {} self.optimize_solutions = False # Whether to use Z3 Optimize() to minimize values self.log_smt_formulas = False # Whether to log SMT formulas and models to disk for debugging @@ -61,6 +63,7 @@ def reset(self): self.instr_coverage = {'total_executed': {}, 'total_instr_count': 0, 'endpoints': {}} self.branch_coverage = {'total_executed': {}, 'total_branch_instr_count': 0} self.violations = {} + self.witness_data = {} lock.release() @@ -114,13 +117,16 @@ def get_endpoints(self): def add_trace(self, endpoint_id: Union[str, int], trace_id: str, trace: list[Branch | Special], inputs: List[Input], ufs: List[UF], symbolic_context_loss: bool, symbolic_precision_loss: bool, - reference_semantic_change: bool = False, missing_invocations: list = None): + reference_semantic_change: bool = False, missing_invocations: list = None, + witness_data: dict = None): endpoint_id = str(endpoint_id) lock.acquire() self._add_endpoint(endpoint_id) self.traces.append(trace) + if witness_data is not None: + self.witness_data[endpoint_id] = witness_data self.tree[endpoint_id].add(trace, inputs, ufs) self.tree[endpoint_id].record_inputs(inputs) self.tree[endpoint_id].record_ufs(ufs) @@ -150,6 +156,21 @@ def get_tree(self, endpoint_id: Union[str, int]) -> Tree: lock.release() return ret + def get_witness_data(self, endpoint_id: Union[str, int]) -> dict | None: + """The witness data of the latest trace of the endpoint (None if no trace arrived since the last clear).""" + endpoint_id = str(endpoint_id) + lock.acquire() + ret = copy.deepcopy(self.witness_data.get(endpoint_id)) + lock.release() + return ret + + def clear_witness_data(self, endpoint_id: Union[str, int]): + """Forgets the witness data of the endpoint, so that only a trace of the next execution can provide it.""" + endpoint_id = str(endpoint_id) + lock.acquire() + self.witness_data.pop(endpoint_id, None) + lock.release() + def record_uncaught_exception(self, endpoint_id: Union[str, int]): endpoint_id = str(endpoint_id) lock.acquire() diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index d3d75756..eae64fd7 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -18,6 +18,7 @@ from enum import Enum from svcomp.SymbolicStorage import SymbolicStorage from svcomp.TestcaseStats import write_testcase_stats +from svcomp.WitnessWriter import write_violation_witness from timing.TimingManager import TimingManager @@ -197,6 +198,9 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, logger.info(f'[SVCOMP] {"="*30} ROUND ({round_idx:03}) {"="*30}') logger.info(f'[SVCOMP] {"="*73}') + # Only a trace of this round may provide the witness data of the violating execution + Database.instance().clear_witness_data(ENDPOINT_ID) + # Build the java command to run DSE command: List[str] = self.build_command(javaagent=agentpath, config=configpath, Z3_DIR=z3path, port=port, cp=cp, java_path=java_path) @@ -327,6 +331,10 @@ def run(self): verdict = Verdict.SAFE verdict_logger.info(f'[VERDICT {self.verification_category.value}] {verdict.value}') + # The witness is written after the verdict and never affects it + if verdict == Verdict.VIOLATION: + self.write_witness() + # Stop total timing (don't print summary here - execution.py will print complete summary with witness timing) TimingManager.instance().stop_total_timer() @@ -343,6 +351,21 @@ def run(self): self.kill_current_process() + def write_witness(self): + """Writes witness.yml/witness.graphml for the VIOLATION verdict from the trace of the violating round.""" + input_files = getattr(self.args, 'witness_input', None) or [] + property_file = getattr(self.args, 'witness_property', None) + if not input_files or not property_file: + logger.warning('[WITNESS] No task input files/property file given (--witness-input/--witness-property), no witness is written') + return + write_violation_witness( + Database.instance().get_witness_data(ENDPOINT_ID), + input_files=input_files, + property_file=property_file, + out_dir=getattr(self.args, 'witness_dir', None) or 'witness', + producer_version=getattr(self.args, 'producer_version', None) or 'unknown', + base_dir=getattr(self.args, 'witness_base_dir', None) or None) + def kill_current_process(self): pid = os.getpid() os.kill(pid, signal.SIGTERM) # Send termination signal diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index 4d46be72..eeb9a386 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -37,11 +37,45 @@ class InvocationItem(BaseModel): count: int +class NondetReturnItem(BaseModel): + """A value returned by a ``Verifier.nondet*()`` call and the location of the call. + + ``value`` is the witness string form (integers decimal, char as code point, float/double as + Java's ``Float/Double.toString``, boolean ``true``/``false``, String raw); ``bits`` carries the + exact IEEE-754 bits of a float/double as ``0x``-prefixed hex. ``callIndex`` is the 0-based + index among the nondet calls on that source line of that class, in evaluation order. + """ + function: str + type: str + value: str + bits: Optional[str] = None + className: str + sourceFile: str = "" + line: int + callIndex: int = 0 + + +class FrameItem(BaseModel): + """A stack frame of the throwable that escaped the entry method.""" + className: str + sourceFile: str = "" + line: int + + +class ViolationItem(BaseModel): + """The throwable that escaped the entry method, with its frames innermost first.""" + throwable: str + frames: List[FrameItem] = [] + + class ConstraintRequest(BaseModel): trace: List[TraceItem] inputs: List[InputItem] ufs: List[UFItem] missingInvocations: List[InvocationItem] = [] + # Witness data: the nondet return values of the execution and the uncaught throwable (if any) + nondetReturns: List[NondetReturnItem] = [] + violation: Optional[ViolationItem] = None symbolicContextLoss: bool symbolicPrecisionLoss: bool referenceSemanticChange: bool = False diff --git a/symbolic-explorer/requirements.txt b/symbolic-explorer/requirements.txt index fec927c0..0362c7cd 100644 --- a/symbolic-explorer/requirements.txt +++ b/symbolic-explorer/requirements.txt @@ -18,4 +18,5 @@ 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 diff --git a/symbolic-explorer/svcomp/WitnessWriter.py b/symbolic-explorer/svcomp/WitnessWriter.py new file mode 100644 index 00000000..451913eb --- /dev/null +++ b/symbolic-explorer/svcomp/WitnessWriter.py @@ -0,0 +1,103 @@ +""" +Writes the SV-COMP violation witness of a testcase from the trace of the violating execution. + +The executor ships the witness data in the trace (``nondetReturns``: every value returned by a +``Verifier.nondet*()`` call with the location of the call; ``violation``: the throwable that escaped +the entry method with its stack frames). The Database keeps the data of the latest trace; when the +final verdict is VIOLATION the driver hands it to :func:`write_violation_witness`, which builds the +witness files with the ``witnesscreator`` package (``witness.yml`` in format 2.3 and the legacy +``witness.graphml``). + +Witness generation must never break or delay the verdict: everything here is caught and logged. +""" + +import time +from pathlib import Path +from typing import Dict, List, Optional + +import log +from timing.TimingManager import TimingManager + +logger = log.get_logger() + +# The witness formats written per violation; YAML (2.3) is what SV-COMP 2027 requires, GraphML is +# kept for validators that still read it (e.g. wit4java). +WITNESS_FORMATS = ("yaml", "graphml") +PRODUCER_NAME = "SWAT" + + +def write_violation_witness(witness_data: Optional[dict], input_files: List[str], property_file: str, + out_dir: str, producer_version: str, + base_dir: Optional[str] = None) -> Dict[str, Path]: + """ + Write the violation witness files for the trace data of the violating execution. + + Args: + witness_data: ``{'nondet_returns': [...], 'violation': {...} | None}`` as stored by the + Database for the latest trace, or None if no trace of the violating execution arrived. + input_files: The task's input files/directories exactly as given to the verifier. + property_file: Path to the property file of the task. + out_dir: Directory the witness files are written to (created if needed). + producer_version: The SWAT version recorded in the witness metadata. + base_dir: Directory relative input paths are resolved against (default: the working directory). + + Returns: + The written files per format (``{'yaml': Path, 'graphml': Path}``), empty if nothing was written. + Never raises. + """ + start = time.perf_counter() + try: + return _write(witness_data, input_files, property_file, out_dir, producer_version, base_dir) + except Exception: # noqa: BLE001 - the verdict must not depend on the witness + logger.exception('[WITNESS] Writing the violation witness failed') + return {} + finally: + TimingManager.instance().record_witness_generation_time(time.perf_counter() - start) + + +def _write(witness_data: Optional[dict], input_files: List[str], property_file: str, out_dir: str, + producer_version: str, base_dir: Optional[str]) -> Dict[str, Path]: + try: + from witnesscreator import Frame, Location, NondetReturn, Task, Violation, write_witnesses + except ImportError as e: + logger.error(f'[WITNESS] The witnesscreator package is not available, no witness is written: {e}') + return {} + + if witness_data is None: + logger.warning('[WITNESS] No trace of the violating execution arrived; the witness has no waypoints') + witness_data = {} + + values = [] + for nr in witness_data.get('nondet_returns') or []: + values.append(NondetReturn( + function=nr['function'], + type=nr['type'], + value=nr['value'], + location=Location(class_name=nr['className'], source_file=nr.get('sourceFile') or None, + line=nr['line'], call_index=nr.get('callIndex', 0)), + bits=nr.get('bits'), + )) + + violation = None + v = witness_data.get('violation') + if v is not None: + violation = Violation( + throwable=v['throwable'], + frames=[Frame(class_name=f['className'], source_file=f.get('sourceFile') or None, line=f['line']) + for f in v.get('frames') or []], + ) + else: + logger.warning('[WITNESS] No uncaught throwable recorded; the witness has no target waypoint') + + task = Task(input_files=list(input_files), property_file=property_file, + producer_name=PRODUCER_NAME, producer_version=producer_version, base_dir=base_dir) + + logger.info(f'[WITNESS] Writing witness ({len(values)} nondet values, ' + f'target: {violation.throwable if violation else "none"}) to {out_dir}') + paths = write_witnesses(task, values, violation, out_dir=out_dir, formats=WITNESS_FORMATS) + for fmt, path in paths.items(): + logger.info(f'[WITNESS] Written {fmt}: {path}') + missing = [fmt for fmt in WITNESS_FORMATS if fmt not in paths] + if missing: + logger.error(f'[WITNESS] Not written: {missing}') + return dict(paths) From 39188f86e7c47ccd35392f957ba6699e0167c918 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Thu, 15 Oct 2026 13:34:33 +0000 Subject: [PATCH 5/7] Package witnesscreator instead of the WitnessCreator jar The competition wrapper no longer runs WitnessCreator: run_swat.py passes the task's input paths, the property file and the version to the explorer (--witness-*), removes a stale witness/ directory before the run and prints witness/witness.yml after a violation verdict. BenchExec collects it via the **/witness.* result-files pattern. The witnesscreator package is pinned to the v1.0.0 tag in the package requirements and installed into libs/python by build-svcomp-python-runtime.sh (built from source as the one pure-Python requirement; SWAT_SVCOMP_WITNESSCREATOR points it at a local checkout or wheel for builds against an unreleased version). The WitnessCreator download, its templates and the WitnessCreator archive directory are gone from the workflow and package-svcomp.sh; the archive check imports witnesscreator and requires the smoketest to leave witness.yml and witness.graphml; the smoketest requires a target waypoint. The benchexec tool-info keeps listing WitnessCreator in REQUIRED_PATHS, which is fine as missing paths are ignored. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/gradle.yml | 22 ------- scripts/build-svcomp-python-runtime.sh | 23 ++++++- scripts/check-svcomp-package.sh | 3 +- scripts/package-svcomp.sh | 25 ++------ scripts/svcomp-package/requirements.txt | 1 + scripts/svcomp-package/run-swat.sh | 2 +- scripts/svcomp-package/run_swat.py | 80 ++++++++++--------------- scripts/svcomp-package/smoketest.sh | 11 ++-- 8 files changed, 67 insertions(+), 100 deletions(-) diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 215ab991..1c19075b 100644 --- a/.github/workflows/gradle.yml +++ b/.github/workflows/gradle.yml @@ -9,10 +9,6 @@ env: # 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 - # WitnessCreator release bundled in the SV-COMP ZIP (release tag + SHA-256 of - # its witness-creator-.zip asset); a new release only changes these two. - WITNESS_CREATOR_VERSION: v0.1.1 - WITNESS_CREATOR_SHA256: 8fc8810237c99bf7d709bdb8692142695e407b5681e818fcfe8b45f9c598d814 jobs: build: @@ -89,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: | @@ -159,7 +138,6 @@ jobs: SWAT_SVCOMP_VERSION: ${{ steps.meta.outputs.version }} SWAT_SVCOMP_ARTIFACT_DIR: ${{ runner.temp }}/release-jars SWAT_SVCOMP_PYTHON_DIR: ${{ runner.temp }}/svcomp-python - SWAT_SVCOMP_WITNESS_CREATOR_DIR: ${{ runner.temp }}/witness-creator-runtime/WitnessCreator SWAT_SVCOMP_COMMIT: ${{ github.sha }} SWAT_SVCOMP_REF: ${{ github.ref_name }} SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }} diff --git a/scripts/build-svcomp-python-runtime.sh b/scripts/build-svcomp-python-runtime.sh index ae69143a..eaf49a40 100755 --- a/scripts/build-svcomp-python-runtime.sh +++ b/scripts/build-svcomp-python-runtime.sh @@ -16,6 +16,9 @@ set -euo pipefail # 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" @@ -32,6 +35,14 @@ if [[ -e "$OUT_DIR" ]] && [[ -n "$(ls -A "$OUT_DIR")" ]]; then 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 @@ -52,7 +63,17 @@ $PIP_CMD install \ --platform manylinux_2_34_x86_64 \ --platform any \ --target "$OUT_DIR" \ - -r "$REQUIREMENTS" + -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" diff --git a/scripts/check-svcomp-package.sh b/scripts/check-svcomp-package.sh index 010ae441..129bbefb 100755 --- a/scripts/check-svcomp-package.sh +++ b/scripts/check-svcomp-package.sh @@ -38,13 +38,14 @@ docker run --rm -v "${tool_dir}:/tool" -w /tool -e UBUNTU_PACKAGES="$UBUNTU_PACK 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; print(\"z3:\", z3.get_version_string())" + 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." diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh index b804bd1d..edf95e5e 100755 --- a/scripts/package-svcomp.sh +++ b/scripts/package-svcomp.sh @@ -10,17 +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_PYTHON_DIR to the Python dependency directory produced by -# scripts/build-svcomp-python-runtime.sh. It is shipped as libs/python/ and -# used with the competition machine's system python3 (no bundled venv). +# 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,7 +31,6 @@ DIST_DIR="${ROOT_DIR}/build/distributions" SUPPORT_DIR="${ROOT_DIR}/scripts/svcomp-package" ARTIFACT_DIR="$(cd "${SWAT_SVCOMP_ARTIFACT_DIR:-$ROOT_DIR}" && pwd)" PYTHON_DIR="${SWAT_SVCOMP_PYTHON_DIR:-}" -WITNESS_CREATOR_DIR="${SWAT_SVCOMP_WITNESS_CREATOR_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" @@ -47,10 +39,6 @@ if [[ -n "$PYTHON_DIR" ]]; then PYTHON_DIR="$(cd "$PYTHON_DIR" && pwd)" fi -if [[ -n "$WITNESS_CREATOR_DIR" ]]; then - WITNESS_CREATOR_DIR="$(cd "$WITNESS_CREATOR_DIR" && pwd)" -fi - fail() { echo "error: $*" >&2 exit 1 @@ -141,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,6 +141,7 @@ copy_tree_files "$SUPPORT_DIR/smoketest" "$PACKAGE_DIR/smoketest" [[ -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" diff --git a/scripts/svcomp-package/requirements.txt b/scripts/svcomp-package/requirements.txt index df7d3303..b4eb8467 100644 --- a/scripts/svcomp-package/requirements.txt +++ b/scripts/svcomp-package/requirements.txt @@ -17,4 +17,5 @@ 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 diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh index e5d13f44..a10bb7b5 100755 --- a/scripts/svcomp-package/run-swat.sh +++ b/scripts/svcomp-package/run-swat.sh @@ -23,7 +23,7 @@ if [ -f "$second_last_path/Main.java" ]; then set -- "${@:1:$(($#-2))}" "$last_path" "$second_last_path" fi -# The witness is created by run_swat.py directly from the given input paths. +# The violation witness is written by the explorer to witness/ from the given input paths. # Python dependencies are shipped in libs/python (built for one CPython # minor version, recorded in libs/python/PYTHON_VERSION) and used with the diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py index a0ba996a..dbeda389 100755 --- a/scripts/svcomp-package/run_swat.py +++ b/scripts/svcomp-package/run_swat.py @@ -1,5 +1,5 @@ from contextlib import contextmanager -import logging, os, enum, subprocess, sys, base64, uuid +import logging, os, enum, shutil, subprocess, sys, uuid import concurrent.futures, json, datetime from typing import List, Optional @@ -8,10 +8,9 @@ logger = logging.getLogger(__name__) SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__)) ORIGINAL_CWD = os.getcwd() -WITNESS_DIR = os.path.join(SCRIPT_DIR, 'WitnessCreator') -WITNESS_PATH = os.path.join(WITNESS_DIR, 'build/libs/WitnessCreator.jar') -# Output lines carrying witness information: nondet values and the violating location -WITNESS_MARKERS = ('[WITNESS]', '[WITNESS_TARGET]') +# The explorer writes the violation witness (witness.yml, witness.graphml) here; BenchExec collects +# it via the `**/witness.*` result-files pattern of the benchmark definition. +WITNESS_DIR = os.path.join(SCRIPT_DIR, 'witness') class ExecutionStatus(enum.Enum): @@ -97,7 +96,9 @@ def run_command_with_timeout(cmd: list[str], timeout: int | None = None) -> tupl -def generate_command(args, property_file: str): +def generate_command(args, property_file: str, property_path: str, input_paths: List[str]): + """The explorer command; `property_path` and `input_paths` are the verifier's arguments as given + by BenchExec (relative to the original working directory) and end up in the witness.""" config_file = 'sv-comp.cfg' agent_path = os.path.join(SCRIPT_DIR, 'symbolic-executor', 'lib', 'symbolic-executor.jar') @@ -114,6 +115,11 @@ def generate_command(args, property_file: str): "--logdir", logging_dir, "--mode", "sv-comp", '--port', "8000", + "--witness-dir", WITNESS_DIR, + "--witness-property", property_path, + "--witness-base-dir", ORIGINAL_CWD, + "--producer-version", swat_version(), + "--witness-input", *input_paths, "--classpath"] print("CP args: " + str(args)) for arg in args[1:]: @@ -153,7 +159,6 @@ def extract_markers(out, markers): markers = (markers,) res = [] for line in out.split("\n"): - print(line) if any(marker in line for marker in markers): res.append(line) return res @@ -169,29 +174,20 @@ def swat_version(): pass return 'unknown' -def generate_witness(witness, property_path, input_paths): - """Create witness.yml (format 2.3) and witness.graphml in the WitnessCreator directory. - - `property_path` and `input_paths` are the verifier's arguments as given by BenchExec; - they are resolved against the original working directory and end up in the witness. - """ - enc = base64.b64encode(witness.encode()).decode() - cmd = [ - 'java', - '-jar', - WITNESS_PATH, - enc, - '--out', WITNESS_DIR, - '--property', property_path, - '--producer-version', swat_version(), - ] - for path in input_paths: - cmd.extend(['--input', path]) - print(cmd) - with pushd(ORIGINAL_CWD): - _, output = run_command_with_timeout(cmd) - print("WITNESS CREATED") - log_output(output) +def print_witness(): + """Print the witness file contents for validation on the benchmark server.""" + witness_file_path = os.path.join(WITNESS_DIR, 'witness.yml') + if os.path.exists(witness_file_path): + print("\n" + "="*80) + print("WITNESS FILE CONTENTS:") + print("="*80) + with open(witness_file_path, 'r') as f: + print(f.read()) + print("="*80) + print("END OF WITNESS FILE") + print("="*80 + "\n") + else: + print(f"WARNING: Witness file not found at {witness_file_path}") def log_output(output: List[str]): for line in output: @@ -222,7 +218,9 @@ def log_output(output: List[str]): input_paths = [arg for arg in sys.argv[1:] if arg != property_path] target_dir = sys.argv[-1] - cmd = generate_command(sys.argv[1:], property_file) + cmd = generate_command(sys.argv[1:], property_file, property_path, input_paths) + # Exactly one witness per run: drop whatever an earlier run left behind + shutil.rmtree(WITNESS_DIR, ignore_errors=True) local_target_dir = copy_target(target_dir) compile_target(sys.argv[1:], local_target_dir) @@ -246,22 +244,6 @@ def log_output(output: List[str]): out = extract_last_round(output) verdict = extract_markers(out, f'[VERDICT {property_file}]') if "== ERROR" in str(verdict): - witnesses = extract_markers(out, WITNESS_MARKERS) - generate_witness("\n".join(witnesses), property_path, input_paths) - print(f'Witnesses:\n {witnesses}') - - # Print the generated witness file contents for validation on benchmark server - witness_file_path = os.path.join(WITNESS_DIR, 'witness.yml') - if os.path.exists(witness_file_path): - print("\n" + "="*80) - print("WITNESS FILE CONTENTS:") - print("="*80) - with open(witness_file_path, 'r') as f: - witness_content = f.read() - print(witness_content) - print("="*80) - print("END OF WITNESS FILE") - print("="*80 + "\n") - else: - print(f"WARNING: Witness file not found at {witness_file_path}") + # The explorer wrote the witness from the trace of the violating execution + print_witness() print(f'Verdict:\n {verdict}') \ No newline at end of file diff --git a/scripts/svcomp-package/smoketest.sh b/scripts/svcomp-package/smoketest.sh index e816d1d0..22228fae 100755 --- a/scripts/svcomp-package/smoketest.sh +++ b/scripts/svcomp-package/smoketest.sh @@ -1,16 +1,17 @@ #!/bin/bash cd "$(dirname "$0")" -rm -f WitnessCreator/witness.yml WitnessCreator/witness.graphml +rm -rf witness output="$("bash" "run-swat.sh" "../../sv-benchmarks/java/properties/valid-assert.prp" "smoketest/common" "smoketest")" if ! echo "$output" | grep -q "\[VERDICT valid-assert.prp\] == ERROR"; then echo "Smoketest failed: no violation verdict!" exit 1 fi -# The violation must come with a YAML witness (format 2.3) for the smoketest target -if ! grep -q 'entry_type: "violation_sequence"' WitnessCreator/witness.yml 2>/dev/null \ - || ! grep -q 'type: "target"' WitnessCreator/witness.yml; then - echo "Smoketest failed: no violation witness with a target waypoint in WitnessCreator/witness.yml!" +# The violation must come with a YAML witness (format 2.3) with a target waypoint, written by +# the explorer to witness/witness.yml +if ! grep -q 'entry_type: "violation_sequence"' witness/witness.yml 2>/dev/null \ + || ! grep -q 'type: "target"' witness/witness.yml; then + echo "Smoketest failed: no violation witness with a target waypoint in witness/witness.yml!" exit 1 fi echo "Smoketest passed!" From be5ddca6e3f3c3abb56299e019cd216de9d35e3f Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Thu, 15 Oct 2026 13:34:33 +0000 Subject: [PATCH 6/7] Validate the explorer-written witnesses in the local harness The harness passes the task's input directories and property file to the explorer (--witness-*), which writes witness.yml and witness.graphml to the testcase's logs/witness/. lib/witness.py only validates them now: the YAML witness must have exactly one target waypoint (WitnessLint does not check that) and is linted when SWAT_WITNESSLINT names a WitnessLint command (--expectViolationWitness --expectedWitnessVersion 2); the GraphML witness is validated with wit4java as before. Generation time comes from the explorer's timing data. Co-Authored-By: Claude Opus 5.5 --- targets/sv-comp/scripts/README.md | 13 +- targets/sv-comp/scripts/lib/__init__.py | 4 +- targets/sv-comp/scripts/lib/command_gen.py | 17 ++- targets/sv-comp/scripts/lib/execution.py | 10 +- targets/sv-comp/scripts/lib/witness.py | 144 ++++++++++----------- 5 files changed, 97 insertions(+), 91 deletions(-) diff --git a/targets/sv-comp/scripts/README.md b/targets/sv-comp/scripts/README.md index 2b53be54..d8aeb5dd 100644 --- a/targets/sv-comp/scripts/README.md +++ b/targets/sv-comp/scripts/README.md @@ -61,11 +61,14 @@ scripts/ ./svcomp setup all ``` -Witnesses of violation results are written by WitnessCreator (expected at -`../WitnessCreator/{build/libs/WitnessCreator.jar,witnesses/}`) to the testcase's -`logs/witness/` as `witness.yml` (YAML format 2.3) and `witness.graphml` (legacy, validated with -wit4java). To additionally lint the YAML witness, point `SWAT_WITNESSLINT` at a WitnessLint -command, e.g. `SWAT_WITNESSLINT="/path/venv/bin/python /path/witnesslint/witnesslinter.py"`. +Witnesses of violation results are written by the Symbolic Explorer itself (from the trace of +the violating execution, via the `witnesscreator` package from `symbolic-explorer/requirements.txt`) +to the testcase's log directory as `witness/witness.yml` (YAML format 2.3) and +`witness/witness.graphml` (legacy). The harness only validates them: the YAML witness must have +exactly one `target` waypoint and, if `SWAT_WITNESSLINT` names a WitnessLint command +(e.g. `SWAT_WITNESSLINT="/path/venv/bin/python /path/witnesslint/witnesslinter.py"`), it is linted +with `--expectViolationWitness --expectedWitnessVersion 2`; the GraphML witness is validated with +wit4java (reported as `Validated:`). A proper validator setup is tracked in #47. ### Test Commands diff --git a/targets/sv-comp/scripts/lib/__init__.py b/targets/sv-comp/scripts/lib/__init__.py index 818811d0..b9a25c3c 100644 --- a/targets/sv-comp/scripts/lib/__init__.py +++ b/targets/sv-comp/scripts/lib/__init__.py @@ -17,7 +17,7 @@ check_port_availability, ExecutionStatus, ) -from .witness import generate_and_validate_witness +from .witness import validate_witness from .analysis.context_loss import main as analyze_context_loss from .comparison import compare_results from .utils import ci_print @@ -50,7 +50,7 @@ "check_port_availability", "ExecutionStatus", # Witness - "generate_and_validate_witness", + "validate_witness", # Analysis "analyze_context_loss", # Comparison diff --git a/targets/sv-comp/scripts/lib/command_gen.py b/targets/sv-comp/scripts/lib/command_gen.py index 9bf39f79..1f3a697f 100644 --- a/targets/sv-comp/scripts/lib/command_gen.py +++ b/targets/sv-comp/scripts/lib/command_gen.py @@ -49,14 +49,23 @@ def generate_command(ver_task: VerificationTask, logging_dir: Path, port: int=80 "-z3", str(library_path), "--logdir", str(logging_dir), "--mode", "sv-comp", - '--port', str(port), - "--classpath"] + '--port', str(port)] cp: list[str] = [] + inputs: list[str] = [] for input_file in ver_task['input_files']: - cp.append(str((test_case_dir / input_file).resolve())) + inputs.append(str((test_case_dir / input_file).resolve())) + cp.append(inputs[-1]) cp.append(str(BASE_PATH / 'libs' / 'java-library-path' / 'com.microsoft.z3.jar')) - return base_command + cp + + # The explorer writes the violation witness (witness.yml/witness.graphml) to /witness + # from the trace of the violating execution; it needs the task's input files and property file. + property_path = test_case_dir.parent / 'properties' / ver_task['category'].value + witness_args: list[str] = ["--witness-dir", "witness", + "--witness-property", str(property_path.resolve()), + "--producer-version", "local", + "--witness-input"] + inputs + return base_command + witness_args + ["--classpath"] + cp diff --git a/targets/sv-comp/scripts/lib/execution.py b/targets/sv-comp/scripts/lib/execution.py index db5c354e..d4f0d1f5 100644 --- a/targets/sv-comp/scripts/lib/execution.py +++ b/targets/sv-comp/scripts/lib/execution.py @@ -9,7 +9,7 @@ from .dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command from .utils import ci_print from .command_gen import extract_testcases, generate_commands, new_run_timestamp, run_dir as make_run_dir -from .witness import generate_and_validate_witness +from .witness import validate_witness from collections import Counter from pathlib import Path @@ -194,9 +194,10 @@ def target_execution(ver_task: VerificationTask, create_witness: bool = True) -> 'case': case } - # Generate and validate witness (with timing) + # Validate the witness the explorer wrote for the violation verdict (with timing); the + # generation time is taken from the explorer's timing data below. if 'violation' in case and create_witness: - validated, witness_generation_time, witness_validation_time = generate_and_validate_witness(ver_task, output) + validated, witness_validation_time = validate_witness(ver_task) elapsed_time = time.perf_counter() - start_time @@ -208,7 +209,8 @@ def target_execution(ver_task: VerificationTask, create_witness: bool = True) -> with open(timing_file, 'r') as f: timing_data = json.load(f) timing_breakdown = timing_data.get('aggregates', {}) - # Update witness timing from our measurements + # Add the witness validation time measured here (generation is timed by the explorer) + witness_generation_time = timing_breakdown.get('witness_generation', witness_generation_time) timing_breakdown['witness_generation'] = witness_generation_time timing_breakdown['witness_validation'] = witness_validation_time diff --git a/targets/sv-comp/scripts/lib/witness.py b/targets/sv-comp/scripts/lib/witness.py index 97d9d2ce..e1b538de 100644 --- a/targets/sv-comp/scripts/lib/witness.py +++ b/targets/sv-comp/scripts/lib/witness.py @@ -1,24 +1,33 @@ -import base64 +"""Validation of the witness files the Symbolic Explorer writes for violation verdicts. + +The explorer writes `witness.yml` (format 2.3) and `witness.graphml` to `/witness/` via the +`witnesscreator` package. This module only checks them: + +- YAML: WitnessLint, if `SWAT_WITNESSLINT` names a linter command (e.g. + `"/path/venv/bin/python /path/witnesslint/witnesslinter.py"`); WitnessLint does not check for a + target segment, so the number of `target` waypoints is checked here (exactly one is expected). +- GraphML: wit4java (the result is what `target_execution` reports as `validated`). + +A proper validator setup is tracked in #47. +""" from contextlib import contextmanager import os import enum import logging +import re import shlex import subprocess import time from typing import List, Optional, Tuple from pathlib import Path -from .dtypes import Verdict, ExpectedVerdict, VerificationCategory, VerificationTask, Command +from .dtypes import VerificationTask logger = logging.getLogger(__name__) SCRIPT_DIR = Path(__file__).resolve().parent.parent # Now in lib/, so go up one more level -WITNESS_CREATION_PATH = (SCRIPT_DIR.parent / 'WitnessCreator' / 'build' / 'libs' / 'WitnessCreator.jar') WITNESS_VALIDATION_PATH = (SCRIPT_DIR.parent / 'wit4java' / 'bin' / 'wit4java') -# Output lines carrying witness information: nondet values and the violating location -WITNESS_MARKERS = ("[WITNESS]", "[WITNESS_TARGET]") -# Optional: command prefix of WitnessLint (e.g. "/path/venv/bin/python /path/witnesslinter.py"); -# when set, the YAML witness is linted after creation. Proper validator setup is tracked in #47. WITNESSLINT_ENV = 'SWAT_WITNESSLINT' +WITNESS_DIR_NAME = 'witness' +TARGET_WAYPOINT = re.compile(r'^\s*type:\s*["\']?target["\']?\s*$') class ExecutionStatus(enum.Enum): SUCCESS = "success" @@ -26,43 +35,39 @@ class ExecutionStatus(enum.Enum): TIMEOUT = "timeout" +def witness_dir(ver_task: VerificationTask) -> Path: + """The directory the explorer writes the witness files of the task to.""" + command_dict = ver_task.get('command') or {} + return Path(str(command_dict.get('log_dir', SCRIPT_DIR))) / WITNESS_DIR_NAME -def generate_and_validate_witness(ver_task: VerificationTask, output: List[str]) -> Tuple[Optional[bool], float, float]: - """Extract witnesses from `output`, create witness files and validate them. - Returns tuple of (validation_result, generation_time, validation_time): - - validation_result: True/False on validation result or None if no witness was found - - generation_time: Time spent generating witness (seconds) - - validation_time: Time spent validating witness (seconds) +def validate_witness(ver_task: VerificationTask) -> Tuple[Optional[bool], float]: + """Check the witness files the explorer wrote for a violation verdict. + + Returns (validation_result, validation_time): + - validation_result: wit4java's verdict on witness.graphml (True/False), or None if no + witness was written + - validation_time: time spent validating (seconds) """ - # Build an `info` dict compatible with the legacy implementation command_dict = ver_task.get('command', {}) info = { 'command': command_dict.get('command', []), 'log_dir': str(command_dict.get('log_dir', SCRIPT_DIR)) } - - out = extract_last_round(output) - witnesses = extract_markers(out, WITNESS_MARKERS) - if not witnesses: - logger.debug("No witnesses found in output") - return None, 0.0, 0.0 - - witness_dir = Path(info['log_dir']) / 'witness' - witness_dir.mkdir(parents=True, exist_ok=True) - - logger.info("Generating witness files") - generation_start = time.perf_counter() - generate_witness(witness_dir, "\n".join(witnesses), input_dirs(info), property_file(ver_task)) - generation_time = time.perf_counter() - generation_start + directory = witness_dir(ver_task) + yaml_file = directory / 'witness.yml' + graphml_file = directory / 'witness.graphml' + if not yaml_file.exists() and not graphml_file.exists(): + logger.warning(f"No witness files found in {directory}") + return None, 0.0 logger.info("Validating witness") validation_start = time.perf_counter() - lint_witness(witness_dir / 'witness.yml', input_dirs(info)) - validation_result = validate_witness(info) + check_yaml_witness(yaml_file, input_dirs(info)) + validation_result = validate_graphml_witness(info, graphml_file) if graphml_file.exists() else None validation_time = time.perf_counter() - validation_start - return validation_result, generation_time, validation_time + return validation_result, validation_time def input_dirs(info: dict) -> List[str]: @@ -83,9 +88,10 @@ def property_file(ver_task: VerificationTask) -> Path: def log_output(output: List[str]): for line in output: logger.info(line.strip()) - -def validate_witness(info: dict) -> bool: - """Run the external witness validator and return True if witness is correct.""" + + +def validate_graphml_witness(info: dict, witness_file: Path) -> bool: + """Run wit4java on the GraphML witness and return True if it reports the witness as correct.""" cmd: List[str] = [str(WITNESS_VALIDATION_PATH), '--packages'] main_folder = '' @@ -106,7 +112,7 @@ def validate_witness(info: dict) -> bool: # ignore non-folders or missing paths continue - cmd.extend(['--witness', str(Path(info['log_dir']) / 'witness' / 'witness.graphml')]) + cmd.extend(['--witness', str(witness_file)]) if main_folder: cmd.append(main_folder) @@ -117,8 +123,8 @@ def validate_witness(info: dict) -> bool: if "wit4java: Witness Correct" in line: return True return False - - + + @contextmanager def pushd(dirname): """Context manager to temporarily change the working directory.""" @@ -131,42 +137,28 @@ def pushd(dirname): os.chdir(original_dir) +def count_target_waypoints(witness_file: Path) -> int: + """The number of `target` waypoints in a YAML witness (a violation witness needs exactly one).""" + with open(witness_file, encoding='utf-8') as f: + return sum(1 for line in f if TARGET_WAYPOINT.match(line)) + + +def check_yaml_witness(witness_file: Path, inputs: List[str]) -> Optional[bool]: + """Check the YAML witness: exactly one target waypoint, and WitnessLint if configured. + + Returns True iff all performed checks passed, False if one failed, None if there is no file. + """ + if not witness_file.exists(): + logger.warning(f"No YAML witness at {witness_file}") + return None + targets = count_target_waypoints(witness_file) + ok = targets == 1 + logger.info(f"YAML witness target waypoints: {targets} ({'ok' if ok else 'expected exactly one'}) ({witness_file})") + lint = lint_witness(witness_file, inputs) + if lint is False: + ok = False + return ok -def extract_last_round(out: List[str], marker: str = "============================== ROUND") -> str: - return "\n".join(out).split(marker)[-1] - - - -def extract_markers(out: str, markers) -> List[str]: - if isinstance(markers, str): - markers = (markers,) - res: List[str] = [] - for line in out.split("\n"): - logger.debug(line) - if any(marker in line for marker in markers): - res.append(line) - return res - -def generate_witness(witness_dir: Path, witness: str, inputs: List[str], prp: Path) -> None: - """Create witness.yml (format 2.3) and witness.graphml in `witness_dir` from the marker lines.""" - with pushd(str(SCRIPT_DIR.parent / 'WitnessCreator')): - # base64 encode the string - enc = base64.b64encode(witness.encode()).decode() - cmd = [ - 'java', - '-jar', - str(WITNESS_CREATION_PATH), - enc, - '--out', str(witness_dir), - '--property', str(prp), - '--producer-version', 'local', - ] - for folder in inputs: - cmd.extend(['--input', folder]) - logger.info(f"Running witness creator: {cmd}") - _, output = run_command_with_timeout(cmd) - logger.info("Witness created") - log_output(output) def lint_witness(witness_file: Path, inputs: List[str]) -> Optional[bool]: """Run WitnessLint on the YAML witness if SWAT_WITNESSLINT is set; True iff the witness is well-formed.""" @@ -197,16 +189,16 @@ def run_command_with_timeout(cmd: list[str], timeout: int = 180) -> tuple[Execut # Read output and wait for process to finish, with a timeout stdout, _ = proc.communicate(timeout=timeout) output = stdout.splitlines() - + return ExecutionStatus.SUCCESS, output - - + + except subprocess.TimeoutExpired: proc.kill() stdout, _ = proc.communicate() output = stdout.splitlines() return ExecutionStatus.TIMEOUT, output - + except Exception as e: logger.critical(f'[SVCOMP] Exception: {e}') proc.kill() From f18d36fed2fd2153f667db820b138b538b8d142b Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Thu, 15 Oct 2026 13:39:18 +0000 Subject: [PATCH 7/7] Record the calling method and send the trace on System.exit - NondetReturnDTO.method carries the calling method as name + descriptor (e.g. main([Ljava/lang/String;)V), passed through to witnesscreator's Location.method so the GraphML assumption scope stays java::L;. as before. - A target that ends the JVM with System.exit never reached the instrumented end of main, so its trace was lost: the explorer logged "Target did not explore branch ... as expected" and had to find the violation on another path. The Transformer's shutdown hook now calls Intrinsics.terminateOnShutdown, which sends (HTTP) or prints (PRINT) the traces of thread contexts still active at shutdown; executions that terminated normally have removed their context already. Trace encoding takes the thread id explicitly since the hook runs on another thread. Runtime.halt paths (SWAT errors, Verifier.assume) are unchanged. Co-Authored-By: Claude Opus 5.5 --- .../uzl/its/swat/instrument/Intrinsics.java | 42 ++++++++++++++++- .../uzl/its/swat/instrument/Transformer.java | 2 + .../svcomp/SVCompMethodAdapter.java | 3 +- .../its/swat/symbolic/trace/DTOBuilder.java | 10 ++-- .../symbolic/trace/SymbolicTraceHandler.java | 10 +++- .../symbolic/trace/dto/NondetReturnDTO.java | 10 ++++ .../de/uzl/its/swat/thread/ThreadHandler.java | 19 +++++++- .../java/de/uzl/its/swat/witness/Witness.java | 41 +++++++++------- .../witness/SvcompWitnessAgentSpec.groovy | 1 + .../uzl/its/swat/witness/WitnessSpec.groovy | 47 ++++++++++--------- .../parse/DataTransferObjects.py | 5 +- symbolic-explorer/svcomp/WitnessWriter.py | 3 +- 12 files changed, 142 insertions(+), 51 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java index 48061c8f..f280c9ba 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Intrinsics.java @@ -4,7 +4,9 @@ import com.sap.fontus.taintaware.unified.IASString; import de.uzl.its.swat.common.ErrorHandler; import de.uzl.its.swat.common.PrintBox; +import com.fasterxml.jackson.core.JsonProcessingException; import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.SWATAssert; import de.uzl.its.swat.common.exceptions.SWATException; import de.uzl.its.swat.common.exceptions.ThreadAlreadyDisabledException; @@ -138,7 +140,7 @@ public static void terminate() { break; case PRINT: if (!ThreadHandler.isThreadContextAborted(currentThread().getId())) { - System.out.println(ThreadHandler.getSymbolicVisitor(currentThread().getId()).getSymbolicTraceHandler().getTraceDTO(ThreadHandler.getStatsStorage(currentThread().getId()))); + printTrace(currentThread().getId()); } break; case NONE: @@ -162,6 +164,44 @@ public static void terminate() { } } + private static void printTrace(long threadId) throws NoThreadContextException, NotImplementedException, JsonProcessingException { + System.out.println(ThreadHandler.getSymbolicVisitor(threadId).getSymbolicTraceHandler().getTraceDTO(ThreadHandler.getStatsStorage(threadId), threadId)); + } + + /** + * Sends (HTTP) or prints (PRINT) the traces of target threads whose symbolic execution is still + * active when the JVM shuts down, i.e. the target ended the run abruptly (System.exit) before + * reaching the instrumented end of its entry method. Executions that terminated normally have + * removed their context already, so this is a no-op for them. Runs in the shutdown hook + * registered by the Transformer, hence on another thread than the target; errors are logged + * only. + */ + public static void terminateOnShutdown() { + for (long threadId : ThreadHandler.getActiveThreadContextIds()) { + try { + logger.warn( + "JVM shutdown with an active symbolic execution (thread {}), e.g. System.exit in the target: sending its trace", + threadId); + ThreadHandler.disableThreadContext(threadId); + if (ThreadHandler.isThreadContextAborted(threadId)) { + continue; + } + switch (config.getSolverMode()) { + case HTTP: + ThreadHandler.sendData(threadId); + break; + case PRINT: + printTrace(threadId); + break; + default: + break; + } + } catch (Throwable t) { + logger.error("Error sending the trace of thread {} on shutdown", threadId, t); + } + } + } + public static void retrieveAssignments() { PrintBox printBox = new PrintBox(60, "Retrieving assignments"); System.getProperties().forEach((key, value) -> { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java index 149e4855..bb29b91e 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java @@ -37,6 +37,8 @@ public abstract class Transformer implements ClassFileTransformer { static { // register the hook as early as possible Runtime.getRuntime().addShutdownHook(new Thread(() -> { + // A target that ends the JVM abruptly (System.exit) must not lose its trace + Intrinsics.terminateOnShutdown(); LoggerContext lc = (LoggerContext) LoggerFactory.getILoggerFactory(); // this will flush and close all appenders (including your buffered FileAppender) lc.stop(); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java index 60c60d32..e0471e47 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/svcomp/SVCompMethodAdapter.java @@ -95,6 +95,7 @@ public void visitMethodInsn( } mv.visitLdcInsn(name); mv.visitLdcInsn(cname); + mv.visitLdcInsn(this.name + this.desc); mv.visitLdcInsn(sourceFile); mv.visitLdcInsn(lineNumber); mv.visitLdcInsn(callIndex); @@ -104,7 +105,7 @@ public void visitMethodInsn( "recordValue", "(" + retType - + "Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;II)V", + + "Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;Ljava/lang/String;II)V", false); SVCompTransformer.getPrintBox().addMsg(" => Adding Witness recording"); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index 454c3232..c773811b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -36,10 +36,12 @@ class DTOBuilder { * Encodes the symbolic trace as a JSON string. * * @param symbolicTrace The symbolic trace to be encoded. + * @param statsStorage The per-execution statistics of the thread. + * @param threadId The thread whose solver context the formulas belong to. * @return The symbolic trace encoded as a JSON string. */ - protected static String encodeTrace(SymbolicTrace symbolicTrace, StatsStorage statsStorage) throws NoThreadContextException, JsonProcessingException, NotImplementedException { - return buildRequestBody(buildTraceDTO(symbolicTrace, statsStorage)); + protected static String encodeTrace(SymbolicTrace symbolicTrace, StatsStorage statsStorage, long threadId) throws NoThreadContextException, JsonProcessingException, NotImplementedException { + return buildRequestBody(buildTraceDTO(symbolicTrace, statsStorage, threadId)); } /** @@ -75,13 +77,13 @@ private static ArrayList buildMissingInvocations(StatsStorage sta * @return A {@link TraceDTO ConstraintDTO} that contains relevant all relevant information * to transfer symbolic traces */ - private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage statsStorage) throws NoThreadContextException, NotImplementedException { + private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage statsStorage, long threadId) throws NoThreadContextException, NotImplementedException { ArrayList inputs = new ArrayList<>(); ArrayList ufs = new ArrayList<>(); ArrayList trace = new ArrayList<>(); FormulaManager fmgr = - ThreadHandler.getSolverContext(currentThread().getId()).getFormulaManager(); + ThreadHandler.getSolverContext(threadId).getFormulaManager(); for (InputElement ie : symbolicTrace.getInputs()) { String lowerBound = String.valueOf(fmgr.dumpFormula(ie.getValue().getBounds(false))); String upperBound = String.valueOf(fmgr.dumpFormula(ie.getValue().getBounds(true))); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java index 02119155..539abc72 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java @@ -110,7 +110,15 @@ public List getConstraints() { * @return The symbolic trace encoded as a JSON string. */ public String getTraceDTO(StatsStorage statsStorage) throws NoThreadContextException, JsonProcessingException, NotImplementedException { - return DTOBuilder.encodeTrace(symbolicTrace, statsStorage); + return DTOBuilder.encodeTrace(symbolicTrace, statsStorage, Thread.currentThread().getId()); + } + + /** + * Encodes the trace with the solver context of the given thread, for callers running on + * another thread (the shutdown hook sending the trace of the target's main thread). + */ + public String getTraceDTO(StatsStorage statsStorage, long threadId) throws NoThreadContextException, JsonProcessingException, NotImplementedException { + return DTOBuilder.encodeTrace(symbolicTrace, statsStorage, threadId); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java index 607d72e4..aa7928e5 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/NondetReturnDTO.java @@ -17,6 +17,8 @@ public class NondetReturnDTO { private String bits; // The class containing the call (dotted name) private String className; + // The method containing the call as name + descriptor, e.g. main([Ljava/lang/String;)V + private String method; // The SourceFile attribute of that class, empty if unknown private String sourceFile; // The source line of the call @@ -30,6 +32,7 @@ public NondetReturnDTO( String value, String bits, String className, + String method, String sourceFile, int line, int callIndex) { @@ -38,6 +41,7 @@ public NondetReturnDTO( this.value = value; this.bits = bits; this.className = className; + this.method = method; this.sourceFile = sourceFile; this.line = line; this.callIndex = callIndex; @@ -67,6 +71,10 @@ public String getClassName() { return className; } + public String getMethod() { + return method; + } + public String getSourceFile() { return sourceFile; } @@ -90,6 +98,8 @@ public String toString() { + (bits == null ? "" : " (" + bits + ")") + " at " + className + + "." + + method + "(" + sourceFile + ":" diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java index 2ecdbac3..b83a3e8d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java @@ -17,7 +17,10 @@ import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.Value; +import java.util.ArrayList; import java.util.HashMap; +import java.util.List; +import java.util.Map; import java.util.concurrent.ThreadLocalRandom; import java.util.logging.LogRecord; import java.util.logging.SimpleFormatter; @@ -163,7 +166,7 @@ public static void sendData(long id) throws NoThreadContextException, JsonProces } if(!config.isCoverageOnly()) { ConstraintRequest.sendConstraints( - symbolicStateHandler.getTraceDTO(context.getStatsStorage()), endpointID, traceID); + symbolicStateHandler.getTraceDTO(context.getStatsStorage(), id), endpointID, traceID); } } else { @@ -175,6 +178,20 @@ public static int getThreadCount() { return threadContextHashMap.size(); } + /** + * The ids of the target threads whose symbolic execution has started and not been terminated + * (the context of the instrumentation itself, id -1, is left out). + */ + public static List getActiveThreadContextIds() { + List ids = new ArrayList<>(); + for (Map.Entry e : threadContextHashMap.entrySet()) { + if (e.getKey() != -1 && !e.getValue().isDisabled()) { + ids.add(e.getKey()); + } + } + return ids; + } + public static void removeSolverContext(long id) throws NoThreadContextException { ThreadContext context = threadContextHashMap.get(id); if (context != null) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java index 3c675ea6..5507f37f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/witness/Witness.java @@ -15,8 +15,9 @@ *

    *
  • {@link #recordValue} is invoked by the SV-COMP instrumentation right after every {@code * Verifier.nondet*()} call with the returned value and the location of the call: the class, - * its SourceFile attribute, the line and the index of the call among the nondet calls on that - * line (bytecode order, which follows the left-to-right evaluation order). + * the calling method (name + descriptor), the class' SourceFile attribute, the line and the + * index of the call among the nondet calls on that line (bytecode order, which follows the + * left-to-right evaluation order). *
  • {@link #recordTarget} is invoked by the surrounding try/catch of the entry method with the * throwable that escaped it; its stack trace locates the violating statement. *
@@ -45,6 +46,7 @@ private static void record( String value, String bits, String cname, + String method, String sourceFile, int line, int callIndex) { @@ -55,44 +57,45 @@ private static void record( value, bits, cname.replace('/', '.'), + method, sourceFile == null ? "" : sourceFile, line, callIndex)); } public static void recordValue( - boolean value, String function, String cname, String sourceFile, int line, int callIndex) { - record(function, "boolean", String.valueOf(value), null, cname, sourceFile, line, callIndex); + boolean value, String function, String cname, String method, String sourceFile, int line, int callIndex) { + record(function, "boolean", String.valueOf(value), null, cname, method, sourceFile, line, callIndex); } public static void recordValue( - byte value, String function, String cname, String sourceFile, int line, int callIndex) { - record(function, "byte", String.valueOf(value), null, cname, sourceFile, line, callIndex); + byte value, String function, String cname, String method, String sourceFile, int line, int callIndex) { + record(function, "byte", String.valueOf(value), null, cname, method, sourceFile, line, callIndex); } public static void recordValue( - short value, String function, String cname, String sourceFile, int line, int callIndex) { - record(function, "short", String.valueOf(value), null, cname, sourceFile, line, callIndex); + short value, String function, String cname, String method, String sourceFile, int line, int callIndex) { + record(function, "short", String.valueOf(value), null, cname, method, sourceFile, line, callIndex); } public static void recordValue( - char value, String function, String cname, String sourceFile, int line, int callIndex) { + char value, String function, String cname, String method, String sourceFile, int line, int callIndex) { // Chars travel as their (unsigned) code point; the witness renders the literal - record(function, "char", String.valueOf((int) value), null, cname, sourceFile, line, callIndex); + record(function, "char", String.valueOf((int) value), null, cname, method, sourceFile, line, callIndex); } public static void recordValue( - int value, String function, String cname, String sourceFile, int line, int callIndex) { - record(function, "int", String.valueOf(value), null, cname, sourceFile, line, callIndex); + int value, String function, String cname, String method, String sourceFile, int line, int callIndex) { + record(function, "int", String.valueOf(value), null, cname, method, sourceFile, line, callIndex); } public static void recordValue( - long value, String function, String cname, String sourceFile, int line, int callIndex) { - record(function, "long", String.valueOf(value), null, cname, sourceFile, line, callIndex); + long value, String function, String cname, String method, String sourceFile, int line, int callIndex) { + record(function, "long", String.valueOf(value), null, cname, method, sourceFile, line, callIndex); } public static void recordValue( - float value, String function, String cname, String sourceFile, int line, int callIndex) { + float value, String function, String cname, String method, String sourceFile, int line, int callIndex) { // Float.toString is exact enough to round-trip (incl. NaN, Infinity, -0.0); the raw bits // let the witness reproduce the value bit for bit. record( @@ -101,27 +104,29 @@ public static void recordValue( Float.toString(value), "0x" + Integer.toHexString(Float.floatToRawIntBits(value)), cname, + method, sourceFile, line, callIndex); } public static void recordValue( - double value, String function, String cname, String sourceFile, int line, int callIndex) { + double value, String function, String cname, String method, String sourceFile, int line, int callIndex) { record( function, "double", Double.toString(value), "0x" + Long.toHexString(Double.doubleToRawLongBits(value)), cname, + method, sourceFile, line, callIndex); } public static void recordValue( - String value, String function, String cname, String sourceFile, int line, int callIndex) { - record(function, "String", value == null ? "" : value, null, cname, sourceFile, line, callIndex); + String value, String function, String cname, String method, String sourceFile, int line, int callIndex) { + record(function, "String", value == null ? "" : value, null, cname, method, sourceFile, line, callIndex); } /** diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy index ba2a337c..2d47c4a4 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/SvcompWitnessAgentSpec.groovy @@ -45,6 +45,7 @@ class SvcompWitnessAgentSpec extends Specification { trace.nondetReturns*.type == ["int", "int", "double", "String"] trace.nondetReturns*.value == ["3", "4", "0.0", "fixed"] trace.nondetReturns*.className == ["Main"] * 4 + trace.nondetReturns*.method == ["main([Ljava/lang/String;)V"] * 4 trace.nondetReturns*.sourceFile == ["Main.java"] * 4 trace.nondetReturns*.line == [14, 14, 15, 16] trace.nondetReturns*.callIndex == [0, 1, 0, 0] diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy index c7987f0a..fc859254 100644 --- a/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/witness/WitnessSpec.groovy @@ -20,7 +20,7 @@ class WitnessSpec extends Specification { def "a nondet return value is recorded with its call location"() { when: - Witness.recordValue(42, "nondetInt", "pkg/Main", "Main.java", 12, 1) + Witness.recordValue(42, "nondetInt", "pkg/Main", "main([Ljava/lang/String;)V", "Main.java", 12, 1) List recorded = Witness.getNondetReturns() then: @@ -31,6 +31,7 @@ class WitnessSpec extends Specification { value == "42" bits == null className == "pkg.Main" + method == "main([Ljava/lang/String;)V" sourceFile == "Main.java" line == 12 callIndex == 1 @@ -49,29 +50,29 @@ class WitnessSpec extends Specification { where: description | args | type | expectedValue | expectedBits - "true" | [true, "nondetBoolean", "Main", "Main.java", 1, 0] | "boolean" | "true" | null - "negative" | [(byte) -5, "nondetByte", "Main", "Main.java", 1, 0] | "byte" | "-5" | null - "min" | [Short.MIN_VALUE, "nondetShort", "Main", "Main.java", 1, 0] | "short" | "-32768" | null - "code point" | [(char) 'A', "nondetChar", "Main", "Main.java", 1, 0] | "char" | "65" | null - "high code" | [(char) 0xFFFF, "nondetChar", "Main", "Main.java", 1, 0] | "char" | "65535" | null - "min" | [Integer.MIN_VALUE, "nondetInt", "Main", "Main.java", 1, 0] | "int" | "-2147483648" | null - "max" | [Long.MAX_VALUE, "nondetLong", "Main", "Main.java", 1, 0] | "long" | "9223372036854775807" | null - "plain" | [0.1f, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "0.1" | "0x3dcccccd" - "small" | [-2.022784E-6f, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "-2.022784E-6" | "0x" + Integer.toHexString(Float.floatToRawIntBits(-2.022784E-6f)) - "negative zero" | [-0.0f, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "-0.0" | "0x80000000" - "NaN" | [Float.NaN, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "NaN" | "0x7fc00000" - "infinity" | [Float.NEGATIVE_INFINITY, "nondetFloat", "Main", "Main.java", 1, 0] | "float" | "-Infinity" | "0xff800000" - "plain" | [1.23E-10d, "nondetDouble", "Main", "Main.java", 1, 0] | "double" | "1.23E-10" | "0x" + Long.toHexString(Double.doubleToRawLongBits(1.23E-10d)) - "negative zero" | [-0.0d, "nondetDouble", "Main", "Main.java", 1, 0] | "double" | "-0.0" | "0x8000000000000000" - "infinity" | [Double.POSITIVE_INFINITY, "nondetDouble", "Main", "Main.java", 1, 0] | "double" | "Infinity" | "0x7ff0000000000000" - "raw" | ["a \"quoted\"\\n", "nondetString", "Main", "Main.java", 1, 0] | "String" | "a \"quoted\"\\n" | null - "null" | [(String) null, "nondetString", "Main", "Main.java", 1, 0] | "String" | "" | null + "true" | [true, "nondetBoolean", "Main", "main()V", "Main.java", 1, 0] | "boolean" | "true" | null + "negative" | [(byte) -5, "nondetByte", "Main", "main()V", "Main.java", 1, 0] | "byte" | "-5" | null + "min" | [Short.MIN_VALUE, "nondetShort", "Main", "main()V", "Main.java", 1, 0] | "short" | "-32768" | null + "code point" | [(char) 'A', "nondetChar", "Main", "main()V", "Main.java", 1, 0] | "char" | "65" | null + "high code" | [(char) 0xFFFF, "nondetChar", "Main", "main()V", "Main.java", 1, 0] | "char" | "65535" | null + "min" | [Integer.MIN_VALUE, "nondetInt", "Main", "main()V", "Main.java", 1, 0] | "int" | "-2147483648" | null + "max" | [Long.MAX_VALUE, "nondetLong", "Main", "main()V", "Main.java", 1, 0] | "long" | "9223372036854775807" | null + "plain" | [0.1f, "nondetFloat", "Main", "main()V", "Main.java", 1, 0] | "float" | "0.1" | "0x3dcccccd" + "small" | [-2.022784E-6f, "nondetFloat", "Main", "main()V", "Main.java", 1, 0] | "float" | "-2.022784E-6" | "0x" + Integer.toHexString(Float.floatToRawIntBits(-2.022784E-6f)) + "negative zero" | [-0.0f, "nondetFloat", "Main", "main()V", "Main.java", 1, 0] | "float" | "-0.0" | "0x80000000" + "NaN" | [Float.NaN, "nondetFloat", "Main", "main()V", "Main.java", 1, 0] | "float" | "NaN" | "0x7fc00000" + "infinity" | [Float.NEGATIVE_INFINITY, "nondetFloat", "Main", "main()V", "Main.java", 1, 0] | "float" | "-Infinity" | "0xff800000" + "plain" | [1.23E-10d, "nondetDouble", "Main", "main()V", "Main.java", 1, 0] | "double" | "1.23E-10" | "0x" + Long.toHexString(Double.doubleToRawLongBits(1.23E-10d)) + "negative zero" | [-0.0d, "nondetDouble", "Main", "main()V", "Main.java", 1, 0] | "double" | "-0.0" | "0x8000000000000000" + "infinity" | [Double.POSITIVE_INFINITY, "nondetDouble", "Main", "main()V", "Main.java", 1, 0] | "double" | "Infinity" | "0x7ff0000000000000" + "raw" | ["a \"quoted\"\\n", "nondetString", "Main", "main()V", "Main.java", 1, 0] | "String" | "a \"quoted\"\\n" | null + "null" | [(String) null, "nondetString", "Main", "main()V", "Main.java", 1, 0] | "String" | "" | null } def "float and double strings round-trip to the recorded value"() { when: - Witness.recordValue(f, "nondetFloat", "Main", "Main.java", 1, 0) - Witness.recordValue(d, "nondetDouble", "Main", "Main.java", 1, 0) + Witness.recordValue(f, "nondetFloat", "Main", "main()V", "Main.java", 1, 0) + Witness.recordValue(d, "nondetDouble", "Main", "main()V", "Main.java", 1, 0) def recorded = Witness.getNondetReturns() then: @@ -85,9 +86,9 @@ class WitnessSpec extends Specification { def "nondet returns keep their execution order"() { when: - Witness.recordValue(1, "nondetInt", "Main", "Main.java", 5, 0) - Witness.recordValue(2, "nondetInt", "Main", "Main.java", 5, 1) - Witness.recordValue(3L, "nondetLong", "Main", "Main.java", 6, 0) + Witness.recordValue(1, "nondetInt", "Main", "main()V", "Main.java", 5, 0) + Witness.recordValue(2, "nondetInt", "Main", "main()V", "Main.java", 5, 1) + Witness.recordValue(3L, "nondetLong", "Main", "main()V", "Main.java", 6, 0) then: Witness.getNondetReturns()*.value == ["1", "2", "3"] diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index eeb9a386..03b6c94f 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -43,13 +43,16 @@ class NondetReturnItem(BaseModel): ``value`` is the witness string form (integers decimal, char as code point, float/double as Java's ``Float/Double.toString``, boolean ``true``/``false``, String raw); ``bits`` carries the exact IEEE-754 bits of a float/double as ``0x``-prefixed hex. ``callIndex`` is the 0-based - index among the nondet calls on that source line of that class, in evaluation order. + index among the nondet calls on that source line of that class, in evaluation order; + ``method`` is the calling method (name + descriptor). """ function: str type: str value: str bits: Optional[str] = None className: str + # The calling method as name + descriptor, e.g. main([Ljava/lang/String;)V + method: Optional[str] = None sourceFile: str = "" line: int callIndex: int = 0 diff --git a/symbolic-explorer/svcomp/WitnessWriter.py b/symbolic-explorer/svcomp/WitnessWriter.py index 451913eb..dad58141 100644 --- a/symbolic-explorer/svcomp/WitnessWriter.py +++ b/symbolic-explorer/svcomp/WitnessWriter.py @@ -74,7 +74,8 @@ def _write(witness_data: Optional[dict], input_files: List[str], property_file: type=nr['type'], value=nr['value'], location=Location(class_name=nr['className'], source_file=nr.get('sourceFile') or None, - line=nr['line'], call_index=nr.get('callIndex', 0)), + line=nr['line'], call_index=nr.get('callIndex', 0), + method=nr.get('method')), bits=nr.get('bits'), ))