diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 138dd91..65c9273 100644 --- a/.github/workflows/gradle.yml +++ b/.github/workflows/gradle.yml @@ -3,6 +3,12 @@ name: Java CI with Gradle on: push: pull_request: + workflow_dispatch: + +env: + SVCOMP_VENV_DIR_NAME: .venv_ubuntu_24_04_1__x86_64 + WITNESS_CREATOR_VERSION: v0.1.1 + WITNESS_CREATOR_SHA256: 8fc8810237c99bf7d709bdb8692142695e407b5681e818fcfe8b45f9c598d814 jobs: build: @@ -18,8 +24,209 @@ jobs: distribution: 'temurin' - name: Setup Gradle uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 + - name: Prepare Solver Dependencies + run: ./gradlew copyNativeLibs - name: Build - run: ./gradlew build -x test + run: ./gradlew --no-daemon build -x test + - name: Collect JavaSMT JAR + run: | + java_smt_dir="${HOME}/.gradle/caches/modules-2/files-2.1/org.sosy-lab/java-smt" + if [[ ! -d "$java_smt_dir" ]]; then + echo "JavaSMT Gradle cache directory not found: $java_smt_dir" >&2 + exit 1 + fi + + java_smt_jar="$(find "$java_smt_dir" -type f -name 'java-smt-*.jar' ! -name '*-sources.jar' ! -name '*-javadoc.jar' | sort | tail -n 1)" + if [[ -z "$java_smt_jar" ]]; then + echo "JavaSMT JAR not found in Gradle cache: $java_smt_dir" >&2 + exit 1 + fi + + mkdir -p build/svcomp-runtime + cp "$java_smt_jar" build/svcomp-runtime/java-smt-latest.jar + - name: Upload JARs + uses: actions/upload-artifact@v4 + with: + name: release-jars-${{ github.sha }} + path: | + symbolic-executor/lib/symbolic-executor.jar + build/svcomp-runtime/java-smt-latest.jar + if-no-files-found: error + retention-days: 1 + + package: + needs: build + if: >- + github.event_name == 'pull_request' || + github.event_name == 'workflow_dispatch' || + (github.event_name == 'push' && ( + github.ref == 'refs/heads/main' || + github.ref == 'refs/heads/dev' || + startsWith(github.ref, 'refs/tags/') + )) + runs-on: ubuntu-24.04 + permissions: + contents: read + outputs: + channel: ${{ steps.meta.outputs.channel }} + zip-name: ${{ steps.meta.outputs.zip-name }} + rolling: ${{ steps.meta.outputs.rolling }} + prerelease: ${{ steps.meta.outputs.prerelease }} + artifact-name: ${{ steps.meta.outputs.artifact-name }} + steps: + - uses: actions/checkout@v5 + - name: Download JARs + uses: actions/download-artifact@v4 + with: + name: release-jars-${{ github.sha }} + path: ${{ runner.temp }}/release-jars + - name: Install JavaSMT packaging artifact + run: | + 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: | + ref_type="${GITHUB_REF_TYPE}" + ref_name="${GITHUB_REF_NAME}" + sha_short="${GITHUB_SHA::7}" + + channel="" # release/tag name; empty -> build artifact only, no release + release="false" + rolling="false" # rolling channels move their tag to the current commit + prerelease="false" + + if [[ "$ref_type" == "tag" ]]; then + channel="$ref_name" + release="true" + elif [[ "$ref_name" == "main" ]]; then + channel="latest" + release="true" + rolling="true" + elif [[ "$ref_name" == "dev" ]]; then + channel="latest-dev" + release="true" + rolling="true" + prerelease="true" + fi + + # Channel-stable asset name gives the nightly cron a fixed download URL; + # the exact commit is recorded in the release notes and BUILD_INFO.txt. + if [[ -n "$channel" ]]; then + version="$channel" + else + version="$sha_short" + fi + zip_name="swat-svcomp-${version}.zip" + + { + echo "channel=${channel}" + echo "version=${version}" + echo "zip-name=${zip_name}" + echo "artifact-name=swat-svcomp-${version}" + echo "release=${release}" + echo "rolling=${rolling}" + echo "prerelease=${prerelease}" + } >> "${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" + - name: Pack SV-COMP ZIP + env: + SWAT_SVCOMP_VERSION: ${{ steps.meta.outputs.version }} + SWAT_SVCOMP_ARTIFACT_DIR: ${{ runner.temp }}/release-jars + SWAT_SVCOMP_RUNTIME_DIR: ${{ runner.temp }}/svcomp-runtime + SWAT_SVCOMP_WITNESS_CREATOR_DIR: ${{ runner.temp }}/witness-creator-runtime/WitnessCreator + SWAT_SVCOMP_COMMIT: ${{ github.sha }} + SWAT_SVCOMP_REF: ${{ github.ref_name }} + SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }} + run: scripts/package-svcomp.sh + - name: Upload SV-COMP ZIP artifact + uses: actions/upload-artifact@v4 + with: + name: ${{ steps.meta.outputs.artifact-name }} + path: build/distributions/${{ steps.meta.outputs.zip-name }} + if-no-files-found: error + + publish-release: + needs: package + if: >- + github.event_name == 'push' && ( + github.ref == 'refs/heads/main' || + github.ref == 'refs/heads/dev' || + startsWith(github.ref, 'refs/tags/') + ) + runs-on: ubuntu-latest + permissions: + contents: write + steps: + - name: Download SV-COMP ZIP artifact + uses: actions/download-artifact@v4 + with: + name: ${{ needs.package.outputs.artifact-name }} + path: ${{ runner.temp }}/svcomp-package + - name: Publish release + env: + GH_TOKEN: ${{ github.token }} + GH_REPO: ${{ github.repository }} + CHANNEL: ${{ needs.package.outputs.channel }} + ZIP_NAME: ${{ needs.package.outputs.zip-name }} + ROLLING: ${{ needs.package.outputs.rolling }} + PRERELEASE: ${{ needs.package.outputs.prerelease }} + run: | + zip_path="${RUNNER_TEMP}/svcomp-package/${ZIP_NAME}" + notes="$(printf 'Automated SWAT SV-COMP package.\n\nRef: %s\nCommit: %s\nRun: %s/%s/actions/runs/%s\n' \ + "$GITHUB_REF_NAME" "$GITHUB_SHA" "$GITHUB_SERVER_URL" "$GITHUB_REPOSITORY" "$GITHUB_RUN_ID")" + + prerelease_flag=() + [[ "$PRERELEASE" == "true" ]] && prerelease_flag=(--prerelease) + + if [[ "$ROLLING" == "true" ]]; then + # Refresh the rolling channel: drop the old release + tag, then recreate + # it at the current commit so the tag always tracks the channel head. + # Uses the default GITHUB_TOKEN, so the new tag does not retrigger CI. + gh release delete "$CHANNEL" --yes --cleanup-tag 2>/dev/null || true + gh release create "$CHANNEL" "$zip_path" \ + --target "$GITHUB_SHA" \ + --title "SWAT ${CHANNEL} (${GITHUB_SHA::7})" \ + --notes "$notes" \ + "${prerelease_flag[@]}" + else + # Permanent, version-tagged release (the tag already points at this commit). + if gh release view "$CHANNEL" >/dev/null 2>&1; then + gh release upload "$CHANNEL" "$zip_path" --clobber + else + gh release create "$CHANNEL" "$zip_path" \ + --title "SWAT ${CHANNEL}" \ + --notes "$notes" \ + "${prerelease_flag[@]}" + fi + fi test: needs: build diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh new file mode 100755 index 0000000..c3a5e78 --- /dev/null +++ b/scripts/package-svcomp.sh @@ -0,0 +1,177 @@ +#!/usr/bin/env bash +set -euo pipefail + +# This script packages artifacts that were already produced by CI. It must not +# invoke Gradle, create virtual environments, or download dependencies. +# +# Generated files are expected in the repository checkout after the CI build. +# Set SWAT_SVCOMP_ARTIFACT_DIR only if those generated files live somewhere +# else. The artifact root must contain: +# +# - symbolic-executor/lib/symbolic-executor.jar +# +# Set SWAT_SVCOMP_WITNESS_CREATOR_DIR to the extracted WitnessCreator runtime +# root from https://github.com/SWAT-project/WitnessCreator. The root must +# contain: +# +# - build/libs/WitnessCreator.jar +# - witnesses/default_violation.st +# - witnesses/witness.st +# +# Set SWAT_SVCOMP_RUNTIME_DIR to a runtime package root that contains the +# pinned SV-COMP Python environment: +# +# - .venv_ubuntu_24_04_1__x86_64/ +# +# Z3 and JavaSMT are taken from the vendored files in this repository. +# +ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$ROOT_DIR" + +VERSION="${SWAT_SVCOMP_VERSION:-$(git rev-parse --short HEAD)}" +COMMIT="${SWAT_SVCOMP_COMMIT:-$(git rev-parse HEAD 2>/dev/null || echo unknown)}" +REF="${SWAT_SVCOMP_REF:-$(git rev-parse --abbrev-ref HEAD 2>/dev/null || echo unknown)}" +CHANNEL="${SWAT_SVCOMP_CHANNEL:-}" +PACKAGE_NAME="swat-svcomp-${VERSION}" +WORK_DIR="$(mktemp -d "${TMPDIR:-/tmp}/swat-svcomp-package.XXXXXX")" +PACKAGE_DIR="${WORK_DIR}/${PACKAGE_NAME}" +DIST_DIR="${ROOT_DIR}/build/distributions" +SUPPORT_DIR="${ROOT_DIR}/scripts/svcomp-package" +ARTIFACT_DIR="$(cd "${SWAT_SVCOMP_ARTIFACT_DIR:-$ROOT_DIR}" && pwd)" +RUNTIME_DIR="${SWAT_SVCOMP_RUNTIME_DIR:-${SWAT_SVCOMP_REFERENCE_DIR:-}}" +WITNESS_CREATOR_DIR="${SWAT_SVCOMP_WITNESS_CREATOR_DIR:-}" +VENV_DIR_NAME="${SWAT_SVCOMP_VENV_DIR_NAME:-.venv_ubuntu_24_04_1__x86_64}" +LINUX_Z3_DIST="z3-4.15.4-x64-glibc-2.39" +LINUX_Z3_ZIP="${ROOT_DIR}/libs/${LINUX_Z3_DIST}.zip" +JAVA_SMT_JAR="${ROOT_DIR}/libs/java-library-path/java-smt-latest.jar" + +if [[ -n "$RUNTIME_DIR" ]]; then + RUNTIME_DIR="$(cd "$RUNTIME_DIR" && pwd)" +fi + +if [[ -n "$WITNESS_CREATOR_DIR" ]]; then + WITNESS_CREATOR_DIR="$(cd "$WITNESS_CREATOR_DIR" && pwd)" +fi + +fail() { + echo "error: $*" >&2 + exit 1 +} + +first_artifact_file() { + local path + for rel in "$@"; do + path="${ARTIFACT_DIR}/${rel}" + if [[ -f "$path" ]]; then + printf '%s\n' "$path" + return 0 + fi + done + fail "missing built artifact file; checked: $*" +} + +copy_tree_files() { + local src="$1" + local dest="$2" + mkdir -p "$dest" + find "$src" -type f \ + ! -path '*/__pycache__/*' \ + ! -path '*/.venv/*' \ + ! -name '*.pyc' \ + ! -name '*.pyo' \ + ! -name '*.iml' \ + -print0 | while IFS= read -r -d '' file; do + local rel="${file#"$src"/}" + mkdir -p "$dest/$(dirname "$rel")" + cp "$file" "$dest/$rel" + done +} + +copy_artifact_file() { + local src="$1" + local dest="$2" + local mode="${3:-0644}" + mkdir -p "$(dirname "$dest")" + install -m "$mode" "$src" "$dest" +} + +copy_artifact_tree() { + local src="$1" + local dest="$2" + [[ -d "$src" ]] || fail "missing artifact directory: ${src}" + mkdir -p "$(dirname "$dest")" + cp -a "$src" "$dest" +} + +install_z3_runtime_file() { + local name="$1" + local mode="${2:-0644}" + local dest="${PACKAGE_DIR}/libs/java-library-path/${name}" + + [[ -f "$LINUX_Z3_ZIP" ]] || fail "missing vendored Linux Z3 distribution: ${LINUX_Z3_ZIP}" + mkdir -p "$(dirname "$dest")" + unzip -p "$LINUX_Z3_ZIP" "${LINUX_Z3_DIST}/bin/${name}" > "$dest" + chmod "$mode" "$dest" +} + +echo "Packaging repository files from: ${ROOT_DIR}" +echo "Packaging built artifacts from: ${ARTIFACT_DIR}" + +echo "Creating package staging directory: ${PACKAGE_DIR}" +mkdir -p "$PACKAGE_DIR" +{ + echo "version=${VERSION}" + echo "channel=${CHANNEL}" + echo "ref=${REF}" + echo "commit=${COMMIT}" +} > "$PACKAGE_DIR/BUILD_INFO.txt" + +install -m 0644 LICENSE "$PACKAGE_DIR/LICENSE" +install -m 0644 Third-Party-Licenses.html "$PACKAGE_DIR/Third-Party-Licenses.html" +install -m 0644 "$SUPPORT_DIR/README.md" "$PACKAGE_DIR/README.md" +install -m 0755 "$SUPPORT_DIR/run-swat.sh" "$PACKAGE_DIR/run-swat.sh" +install -m 0755 "$SUPPORT_DIR/compile-target.sh" "$PACKAGE_DIR/compile-target.sh" +install -m 0755 "$SUPPORT_DIR/smoketest.sh" "$PACKAGE_DIR/smoketest.sh" +install -m 0755 "$SUPPORT_DIR/run_swat.py" "$PACKAGE_DIR/run_swat.py" +install -m 0644 "$SUPPORT_DIR/requirements.txt" "$PACKAGE_DIR/requirements.txt" +install -m 0644 targets/sv-comp/sv-comp.cfg "$PACKAGE_DIR/sv-comp.cfg" + +EXECUTOR_JAR="$(first_artifact_file \ + symbolic-executor/lib/symbolic-executor.jar \ + symbolic-executor/build/libs/symbolic-executor-all.jar)" +copy_artifact_file "$EXECUTOR_JAR" "$PACKAGE_DIR/symbolic-executor/lib/symbolic-executor.jar" + +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 +install_z3_runtime_file com.microsoft.z3.jar +install_z3_runtime_file libz3.a +[[ -f "$JAVA_SMT_JAR" ]] || fail "missing JavaSMT JAR: ${JAVA_SMT_JAR}" +copy_artifact_file "$JAVA_SMT_JAR" "$PACKAGE_DIR/libs/java-library-path/java-smt-latest.jar" + +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}" + +mkdir -p "$DIST_DIR" +ZIP_PATH="${DIST_DIR}/${PACKAGE_NAME}.zip" +ZIP_TMP="${WORK_DIR}/${PACKAGE_NAME}.zip" + +echo "Creating ZIP: ${ZIP_PATH}" +( + cd "$WORK_DIR" + zip -qr "$ZIP_TMP" "$PACKAGE_NAME" +) +cp "$ZIP_TMP" "$ZIP_PATH" + +echo "Package created at: ${ZIP_PATH}" +echo "Staging directory left at: ${PACKAGE_DIR}" diff --git a/scripts/svcomp-package/README.md b/scripts/svcomp-package/README.md new file mode 100644 index 0000000..46852fd --- /dev/null +++ b/scripts/svcomp-package/README.md @@ -0,0 +1,19 @@ +# SWAT SV-COMP Package + +This archive contains a runnable SWAT package for SV-COMP style Java verification tasks. + +Important entry points: + +- `run-swat.sh`: verifier entry point used by BenchExec. +- `compile-target.sh`: helper used by `run_swat.py` to compile Java benchmark sources. +- `smoketest.sh`: runs SWAT on two bundled smoke-test targets. +- `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. + +Example: + +```sh +./run-swat.sh ../../sv-benchmarks/java/properties/valid-assert.prp smoketest/common smoketest +``` diff --git a/scripts/svcomp-package/compile-target.sh b/scripts/svcomp-package/compile-target.sh new file mode 100755 index 0000000..5d2e5ff --- /dev/null +++ b/scripts/svcomp-package/compile-target.sh @@ -0,0 +1,35 @@ +#!/bin/bash + +# Check if at least two arguments are provided +if [ "$#" -lt 2 ]; then + echo "Usage: $0 ... " + exit 1 +fi + +# Check if the fourth argument ends with 'rbtree' and swap if true +if [[ "${4}" == *rbtree ]]; then + temp=$3 + set -- "${@:1:2}" "$4" "$temp" "${@:5}" +fi + +# print all params +shift # Remove the first argument (property file) + +# Extract the target file (last argument) +target_directory="${!#}" # Get the last argument + +# Construct the classpath using all remaining arguments except the last one +classpath=$(IFS=:; echo "${*:1:$#-1}/") + +build_directory="$target_directory/build" + +#echo $target_directory $classpath $build_directory +# Create the build directory if it doesn't exist +mkdir -p "$build_directory" + +# Use find to get all .java files recursively from the target directory +java_files=$(find "$target_directory" -name "*.java") + +echo "javac -source 1.8 -target 1.8 -cp \"$classpath\" -d \"$build_directory\" $java_files" +# Compile all the found .java files +javac -source 1.8 -target 1.8 -cp "$classpath" -d "$build_directory" $java_files \ No newline at end of file diff --git a/scripts/svcomp-package/requirements.txt b/scripts/svcomp-package/requirements.txt new file mode 100644 index 0000000..5c32b0a --- /dev/null +++ b/scripts/svcomp-package/requirements.txt @@ -0,0 +1,19 @@ +annotated-types==0.7.0 +anyio==4.6.2.post1 +boto==2.49.0 +certifi==2025.11.12 +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 +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 +z3-solver==4.15.4.0 diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh new file mode 100755 index 0000000..424a318 --- /dev/null +++ b/scripts/svcomp-package/run-swat.sh @@ -0,0 +1,72 @@ +#!/bin/bash + + +# Check if the '-v' argument is among the arguments, indicating that the user wants to see the version +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 + fi +done + +# get last argument +last_path="${@: -1}" + +# get second last argument +second_last_path="${*: -2:1}" + +# check if there is a Main.java in last_path +if [ -f "$second_last_path/Main.java" ]; then + # switch the last two arguments + 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 + + +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" + exit 1 +fi + +echo "Running SWAT with arguments: $@" +"$VENV_PYTHON" -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1 +cat out.log diff --git a/scripts/svcomp-package/run_swat.py b/scripts/svcomp-package/run_swat.py new file mode 100755 index 0000000..6b88333 --- /dev/null +++ b/scripts/svcomp-package/run_swat.py @@ -0,0 +1,239 @@ +from contextlib import contextmanager +import logging, os, enum, subprocess, sys, base64, uuid + +import concurrent.futures, json, datetime +from typing import List, Optional + +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') + + +class ExecutionStatus(enum.Enum): + SUCCESS = "success" + ERROR = "error" + TIMEOUT = "timeout" + +class Verdict(enum.Enum): + VIOLATION = "== ERROR" + SAFE = "== OK" + UNKNOWN = "== DONT-KNOW" + NO_SYMBOLIC_VARS = "== NON-SYMBOLIC" + +@contextmanager +def pushd(dirname): + """Context manager to temporarily change the working directory.""" + original_dir = os.getcwd() + logger.info(f"Changing directory to: {dirname}") + os.chdir(dirname) + try: + yield + finally: + os.chdir(original_dir) + +def determine_result(output: List[str], property_file: str) -> Verdict: + """Parse the verdict for a specific property from the output.""" + verdict = None + for line in output: + if f"[VERDICT {property_file}]" in line: + if "== OK" in line: + verdict = Verdict.SAFE + break + elif "== ERROR" in line: + verdict = Verdict.VIOLATION + break + elif "== DONT-KNOW" in line: + verdict = Verdict.UNKNOWN + break + return verdict + + + + + + +def run_command_with_timeout(cmd: list[str], timeout: int | None = None) -> tuple[ExecutionStatus, list[str]]: + """Executes the given command and returns output from both STDOUT and STDERR. + + timeout=None (the default) imposes no internal cutoff so SWAT can use the full + SV-COMP time budget; benchexec enforces the wall/CPU limit externally. + """ + + logger.info(f'[TARGET EXECUTION]: Running command: {cmd}') + output = [] + with subprocess.Popen( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + universal_newlines=True, + bufsize=1 + ) as proc: + try: + # 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() + output = [str(e)] + return ExecutionStatus.ERROR, output + [str(e)] + + + + + +def generate_command(args, property_file: str): + config_file = 'sv-comp.cfg' + + agent_path = os.path.join(SCRIPT_DIR, 'symbolic-executor', 'lib', 'symbolic-executor.jar') + config_path = os.path.join(SCRIPT_DIR, config_file) + 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'), + "-prp", property_file, + "--agent", agent_path, + "--config", config_path, + "-z3", library_path, + "--logdir", logging_dir, + "--mode", "sv-comp", + '--port', "8000", + "--classpath"] + print("CP args: " + str(args)) + for arg in args[1:]: + print("CP arg: " + arg) + print("CP arg path: " + os.path.join(SCRIPT_DIR, arg)) + base_command.append(os.path.join(SCRIPT_DIR, arg)) + return base_command + + +def copy_target(target_dir): + # generate random target tmp name + local_target_dir = f"target_{uuid.uuid4()}" + + os.system(f'rm -rf {local_target_dir} && cp -r {target_dir} {local_target_dir}') + print(f"Target copied from {target_dir} to: {local_target_dir}") + return local_target_dir + +def compile_target(args, local_target_dir): + cmd = [ + 'bash', + f'compile-target.sh', + ] + args[-1] = local_target_dir # overwrite target dir + cmd = cmd + args + print(cmd) + _, output = run_command_with_timeout(cmd) + log_output(output) + + +def extract_last_round(out, marker="============================== ROUND"): + + return "\n ".join(out).split(marker)[-1] + + +def extract_markers(out, marker): + res = [] + for line in out.split("\n"): + print(line) + if marker in line: + 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) + _, output = run_command_with_timeout(cmd) + print("WITNESS CREATED") + print(output) + +def log_output(output: List[str]): + for line in output: + logger.info(line.strip()) + +if __name__ == "__main__": + logger.info("Running SWAT Wrapper...") + + # Look for property file in arguments + # SV-COMP framework passes the .prp file directly as first argument + property_file = None + for arg in sys.argv[1:]: + if arg.endswith('.prp'): + property_file = os.path.basename(arg) + logger.info(f"Found property file in arguments: {property_file}") + break + + if property_file is None: + logger.error(f"ERROR: No .prp file found in arguments.") + logger.error(f"Arguments: {sys.argv}") + exit(1) + + logger.info(f"Using property file: {property_file}") + + target_dir = sys.argv[-1] + cmd = generate_command(sys.argv[1:], property_file) + local_target_dir = copy_target(target_dir) + compile_target(sys.argv[1:], local_target_dir) + + path = local_target_dir + log_dir = f'{path}/logs' + + cmd[-1] = os.path.join(SCRIPT_DIR, local_target_dir, 'build') #f"{local_target_dir}/build" + #delete the dir if it exists + if os.path.exists(log_dir): + os.system(f'rm -rf {log_dir}') + os.makedirs(log_dir) + with pushd(path): + execution_status, output = run_command_with_timeout(cmd) + log_output(output) + print(f"Execution status: {execution_status}") + if execution_status == ExecutionStatus.TIMEOUT or execution_status == ExecutionStatus.ERROR: + print(f'Error: {output}') + exit(1) + + + 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)) + 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') + 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}") + 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 new file mode 100755 index 0000000..95fb8c0 --- /dev/null +++ b/scripts/svcomp-package/smoketest.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +cd "$(dirname "$0")" +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!" + exit 1 +fi + diff --git a/scripts/svcomp-package/smoketest/Main.java b/scripts/svcomp-package/smoketest/Main.java new file mode 100644 index 0000000..7362ba8 --- /dev/null +++ b/scripts/svcomp-package/smoketest/Main.java @@ -0,0 +1,10 @@ +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + public static void main(String[] args) { + // Fetch inputs using Verifier.nondet* methods + int i = Verifier.nondetInt(); + + assert i != 42; + } +} diff --git a/scripts/svcomp-package/smoketest/common/Verifier.java b/scripts/svcomp-package/smoketest/common/Verifier.java new file mode 100644 index 0000000..7fd2399 --- /dev/null +++ b/scripts/svcomp-package/smoketest/common/Verifier.java @@ -0,0 +1,60 @@ +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://github.com/sosy-lab/sv-benchmarks +// +// SPDX-FileCopyrightText: Contributed by Peter Schrammel +// SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.sv_benchmarks; + +import java.util.Random; + +public final class Verifier { + public static void assume(boolean condition) { + if (!condition) { + Runtime.getRuntime().halt(1); + } + } + + public static boolean nondetBoolean() { + return new Random().nextBoolean(); + } + + public static byte nondetByte() { + return (byte) (new Random().nextInt()); + } + + public static char nondetChar() { + return (char) (new Random().nextInt()); + } + + public static short nondetShort() { + return (short) (new Random().nextInt()); + } + + public static int nondetInt() { + return new Random().nextInt(); + } + + public static long nondetLong() { + return new Random().nextLong(); + } + + public static float nondetFloat() { + return new Random().nextFloat(); + } + + public static double nondetDouble() { + return new Random().nextDouble(); + } + + public static String nondetString() { + Random random = new Random(); + int size = random.nextInt(); + assume(size >= 0); + byte[] bytes = new byte[size]; + random.nextBytes(bytes); + return new String(bytes); + } +} diff --git a/settings.gradle b/settings.gradle index defcd23..2f822f5 100644 --- a/settings.gradle +++ b/settings.gradle @@ -6,7 +6,6 @@ rootProject.name = "SWAT" include 'symbolic-executor' include 'annotations' -include 'targets:sv-comp:WitnessCreator' include 'targets:instruction-tests:IFXX' include 'targets:instruction-tests:I2X' @@ -83,4 +82,4 @@ dependencyResolutionManagement { include 'targets:applications:modelmapper-test-app' findProject(':targets:applications:modelmapper-test-app')?.name = 'modelmapper-test-app' include 'targets:applications:reflection-test-app' -findProject(':targets:applications:reflection-test-app')?.name = 'reflection-test-app' \ No newline at end of file +findProject(':targets:applications:reflection-test-app')?.name = 'reflection-test-app' diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java index 8cf11a6..a716713 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/Frame.java @@ -21,15 +21,20 @@ public class Frame { /** Number of words that are returned on invoke method end */ public final int nReturnWords; /** The symbolic version of Javas locals */ - @Getter private final ArrayList> locals = new ArrayList<>(8); + @Getter + private final ArrayList> locals = new ArrayList<>(8); /** The symbolic version of Javas operand stack */ - @Getter private final ArrayList> operandStack = new ArrayList<>(8); + @Getter + private final ArrayList> operandStack = new ArrayList<>(8); /** The return value of the symbolic stack frame */ - @Getter private Value ret; + @Getter + private Value ret; /** The class name of the method that is invoked */ - @Getter private final String className; + @Getter + private final String className; /** The method name of the method that is invoked */ - @Getter private final String methodName; + @Getter + private final String methodName; /** * Constructor for Frame @@ -249,14 +254,19 @@ public void printStack() throws NoThreadContextException { // purposes. Logger stateLogger = ThreadHandler.getShadowStateLogger(id); - int cnt = 3; + int cnt = 4; for (int i = operandStack.size() - 1; i >= 0; i--) { stateLogger.info("[{}]: {}", operandStack.size() - i, operandStack.get(i)); - if(--cnt == 0) break; + if (--cnt == 0) + break; } int remaining = operandStack.size() - 4; - if (remaining >= 0) stateLogger.info("... ({} more)", remaining); + if (remaining > 0) + stateLogger.info("... ({} more)", remaining); + + // stateLogger.info("LOCALS: {}", locals); } + /** * Override of the default toString method for printing the Current symbolic stack frame and * locals diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java index ebba905..24f8d59 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java @@ -69,6 +69,7 @@ public BooleanFormula IF_ACMPNE(ObjectValue o2) { return super.IF_ACMPNE(o2); } } + /** * Compares if two references are identical * @@ -91,10 +92,10 @@ public Object getConcrete() { } public String MAKE_SYMBOLIC(String prefixOrIdx) { - if (prefixOrIdx.matches("-?\\d+")){ + if (prefixOrIdx.matches("-?\\d+")) { // We assume a constructed idx was passed as it is a number initSymbolic(symbolicPrefix, prefixOrIdx); - } else if (prefixOrIdx.matches(".*-?\\d+")){ + } else if (prefixOrIdx.matches(".*-?\\d+")) { // Its a list which already has prefix and idx initSymbolicWithoutIdx(prefixOrIdx); } else { @@ -110,6 +111,7 @@ public String MAKE_SYMBOLIC() { formula = smgr.makeVariable(name); return name; } + /** * Turns this IntValue into a symbolic variable * @@ -146,7 +148,8 @@ public BooleanFormula getBounds(boolean upper) { * implemented or void should be returned */ @Override - public Value invokeMethod(String name, Type[] desc, Value[] args) throws NotImplementedException, ValueConversionException { + public Value invokeMethod(String name, Type[] desc, Value[] args) + throws NotImplementedException, ValueConversionException { return switch (name) { case "" -> invokeInit(args, desc); case "charAt" -> invokeCharAt(args, desc); @@ -215,7 +218,7 @@ public BooleanFormula getBounds(boolean upper) { * @return The resulting Value or PlaceHolder::instance */ private Value invokeInit(Value[] args, Type[] desc) { - if(args.length == 1 && args[0] instanceof StringValue s) { + if (args.length == 1 && args[0] instanceof StringValue s) { this.concrete = s.concrete; this.formula = s.formula; } @@ -236,7 +239,8 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeCharAt(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + private Value invokeCharAt(Value[] args, Type[] desc) + throws NotImplementedException, ValueConversionException { if (args.length == 1) { IntValue index = args[0].asIntValue(); char result = concrete.charAt(index.concrete); @@ -502,8 +506,7 @@ public BooleanFormula getBounds(boolean upper) { BooleanFormula constraints = uf.createEqualsIgnoreCaseConstraints( this.formula, rhs.formula, this.concrete, rhs.concrete, - this.isSymbolic(), rhs.isSymbolic() - ); + this.isSymbolic(), rhs.isSymbolic()); ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).addConstraint(constraints); // also carry the concrete result for concolic steering @@ -516,7 +519,6 @@ public BooleanFormula getBounds(boolean upper) { } } - /** * Invocation handling for the String instance method Formatted(). @@ -566,8 +568,8 @@ public BooleanFormula getBounds(boolean upper) { CharArrayValue dst = args[2].asObjectValue().asArrayValue().asCharArrayValue(); IntValue dstBegin = args[3].asIntValue(); for (int idx = srcBegin.concrete; idx < srcEnd.concrete; idx++) { - Value[] charAtArgs = new Value[] {new IntValue(context, idx)}; - Type[] charAtDesc = new Type[] {Type.INT_TYPE}; + Value[] charAtArgs = new Value[] { new IntValue(context, idx) }; + Type[] charAtDesc = new Type[] { Type.INT_TYPE }; dst.storeElement( new IntValue(context, dstBegin.concrete + idx), (CharValue) invokeCharAt(charAtArgs, charAtDesc)); @@ -624,7 +626,8 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeIndexOf(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + private Value invokeIndexOf(Value[] args, Type[] desc) + throws NotImplementedException, ValueConversionException { if (args.length == 1) { return switch (desc[0].getDescriptor()) { case "I" -> invokeIndexOf(args[0].asIntValue()); @@ -823,7 +826,8 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeReplace(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + private Value invokeReplace(Value[] args, Type[] desc) + throws NotImplementedException, ValueConversionException { if (args.length == 2) { return switch (desc[0].getDescriptor()) { case "C" -> invokeReplace(args[0].asCharValue(), args[1].asCharValue()); @@ -836,17 +840,20 @@ public BooleanFormula getBounds(boolean upper) { } private Value invokeReplace(ObjectValue target, ObjectValue replacement) { - if (target instanceof StringValue s1 && replacement instanceof StringValue s2) { + if (target instanceof StringValue oldString && replacement instanceof StringValue newString) { // ToDo (Nils): This is the correct implementation. However replaceAll is currently not // supported by Z3 /* - this.formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula); + formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula); */ - this.concrete = this.concrete.replace(s1.concrete, s2.concrete); + + var newConcrete = this.concrete.replace(oldString.concrete, newString.concrete); + var newFormula = this.formula; for (int i = 0; i < REPLACE_COUNT; i++) { - this.formula = smgr.replace(this.formula, s1.formula, s2.formula); + newFormula = smgr.replace(newFormula, oldString.formula, newString.formula); } - return this; + + return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN); } else { return PlaceHolder.instance; } @@ -858,16 +865,17 @@ public BooleanFormula getBounds(boolean upper) { // ToDo (Nils): This is the correct implementation. However replaceAll is currently not // supported by Z3 // See: https://git.its.uni-luebeck.de/research-projects/pet-hmr/knife-fuzzer/-/issues/54 - /* - this.formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula); + formula = smgr.replaceAll(this.formula, oldString.formula, newString.formula); */ - this.concrete = this.concrete.replace(oldString.concrete, newString.concrete); + + var newConcrete = this.concrete.replace(oldString.concrete, newString.concrete); + var newFormula = this.formula; for (int i = 0; i < REPLACE_COUNT; i++) { - this.formula = smgr.replace(this.formula, oldString.formula, newString.formula); + newFormula = smgr.replace(newFormula, oldString.formula, newString.formula); } - // ToDo: A new string is created as we need a new address, should the entire object be recreated above? - return new StringValue(context, this.concrete, this.formula, ObjectValue.ADDRESS_UNKNOWN); + + return new StringValue(context, newConcrete, newFormula, ObjectValue.ADDRESS_UNKNOWN); } /** @@ -941,7 +949,8 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeStartsWith(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + private Value invokeStartsWith(Value[] args, Type[] desc) + throws NotImplementedException, ValueConversionException { if (args.length == 1) { return invokeStartsWith(args[0].asStringValue()); } else if (args.length == 2) { @@ -1053,7 +1062,8 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeSubstring(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + private Value invokeSubstring(Value[] args, Type[] desc) + throws NotImplementedException, ValueConversionException { if (args.length == 1) { return invokeSubstring(args[0].asIntValue()); } else if (args.length == 2) { @@ -1091,14 +1101,14 @@ public BooleanFormula getBounds(boolean upper) { * the Value in args is of the same type. * @return The resulting Value or PlaceHolder::instance */ - private Value invokeToCharArray(Value[] args, Type[] desc) throws NotImplementedException, ValueConversionException { + private Value invokeToCharArray(Value[] args, Type[] desc) + throws NotImplementedException, ValueConversionException { if (!concrete.isEmpty()) { - CharArrayValue dst = - new CharArrayValue(context, new IntValue(context, concrete.length()), -1); + CharArrayValue dst = new CharArrayValue(context, new IntValue(context, concrete.length()), -1); for (int idx = 0; idx < concrete.length(); idx++) { - Value[] charAtArgs = new Value[] {new IntValue(context, idx)}; - Type[] charAtDesc = new Type[] {Type.INT_TYPE}; + Value[] charAtArgs = new Value[] { new IntValue(context, idx) }; + Type[] charAtDesc = new Type[] { Type.INT_TYPE }; dst.storeElement( new IntValue(context, idx), (CharValue) invokeCharAt(charAtArgs, charAtDesc)); @@ -1232,7 +1242,7 @@ public ImmutableSet getSymbolicVariables() { } @Override - public String getSymPrefix(){ + public String getSymPrefix() { return symbolicPrefix; } @@ -1242,11 +1252,10 @@ public String toString() { String concreteString = null != concrete ? concrete : ""; if (formulaString.length() > Config.instance().getLoggingFormulaLength()) { - formulaString = - formulaString.substring(0, Config.instance().getLoggingFormulaLength()) + "..."; + formulaString = formulaString.substring(0, Config.instance().getLoggingFormulaLength()) + "..."; } - return "StringValue[" + this.internalID +"]; @" + return "StringValue[" + this.internalID + "]; @" + Integer.toHexString(address) + " (" + concreteString diff --git a/symbolic-explorer/data/BinaryExecutionTree/Tree.py b/symbolic-explorer/data/BinaryExecutionTree/Tree.py index 6636395..ad6c2b0 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Tree.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Tree.py @@ -8,7 +8,7 @@ import log logger = log.get_logger() -#import pygraphviz as pgv +# import pygraphviz as pgv class Tree: """ @@ -130,8 +130,10 @@ def add_recursive(self, parent: Optional[Node], node: Optional[Union[Node, Leaf] return Node(parent, trace, inputs, ufs) if len(trace) > 0 else Leaf(parent, inputs, ufs) return node + + +# VISUALIZATIONS def get_constraint_label(self, parent: Node, node: Union[Node, Leaf]): - return None """Get the constraint label for an edge.""" if isinstance(node, Leaf): return "" @@ -140,7 +142,6 @@ def get_constraint_label(self, parent: Node, node: Union[Node, Leaf]): return "" def add_to_dot(self, node: Optional[Union[Node, Leaf]], graph, parent: Optional[Node] = None): - return None """Recursively add nodes and edges to the DOT graph.""" if node is not None: graph.add_node(node.gid, label=str(node.gid) + ':' + str(node.id)) @@ -153,11 +154,10 @@ def add_to_dot(self, node: Optional[Union[Node, Leaf]], graph, parent: Optional[ self.add_to_dot(node.branched, graph, node) self.add_to_dot(node.skipped, graph, node) -# def plot_tree(self, idx): -# return None -# """Plot the tree using Graphviz and save to a file.""" -# #log.info(self.to_string()) -# G = pgv.AGraph(directed=True, strict=True, rankdir='TB') -# self.add_to_dot(self.root, G) -# G.layout(prog="dot") -# G.draw(f"tree_{idx}.png") + def plot_tree(self, idx): + """Plot the tree using Graphviz and save to a file.""" + #log.info(self.to_string()) + G = pgv.AGraph(directed=True, strict=True, rankdir='TB') + self.add_to_dot(self.root, G) + G.layout(prog="dot") + G.draw(f"tree_{idx}.png") diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a0081e8..19ea7b3 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -222,6 +222,9 @@ def run_testcase(self, java_path, agentpath: str, configpath: str, z3path, port, logger.info(f'[STATUS] {status}') next_step: Action = self.determine_next_step(status, output) + # Visualize DB tree + # print("Plotting DB Tree...", flush=True) + # Database.instance().get_tree(0).plot_tree(round_idx) round_idx += 1 if next_step == Action.REPORTVERDICT: @@ -258,7 +261,7 @@ def retrieve_solution(self): continue branch_found = True #logger.info(f'[SYMBOLIC EXPLORATION] Solving for branch {branch.id}') - sat, sol = StrategyService.solve_branch(branch) + sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None) if sat == SATResult.SAT: logger.info(f'[SYMBOLIC EXPLORATION] Found solution for branch {branch.id} {"skipped" if branch.skipped is None else "branched"}') diff --git a/symbolic-explorer/solver/SolverHandler.py b/symbolic-explorer/solver/SolverHandler.py index dd9a0ee..471f0f8 100755 --- a/symbolic-explorer/solver/SolverHandler.py +++ b/symbolic-explorer/solver/SolverHandler.py @@ -358,7 +358,7 @@ def write_optimizer_to_file(optimizer: Optimize, output_dir: str = "smt_files") return filepath @staticmethod - def solve(node: Any, path_constraints: list) -> Tuple[SATResult, Dict[str, Any]]: + def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000) -> Tuple[SATResult, Dict[str, Any]]: """ Solve for the given node and path constraints using ConstraintCache (modern approach). @@ -391,6 +391,8 @@ def solve(node: Any, path_constraints: list) -> Tuple[SATResult, Dict[str, Any]] for i, path_constraint_str in enumerate(path_constraints): path_cached = cache.get_smt_constraint(path_constraint_str, source=f"path_{i}") all_exprs.extend(path_cached['exprs']) + + # logger.debug(f"[SOLVER] all_exprs: {all_exprs}") # Create solver with shared context from cache @@ -432,7 +434,8 @@ def solve(node: Any, path_constraints: list) -> Tuple[SATResult, Dict[str, Any]] except Exception as e: logger.warning(f"[SOLVER] Failed to save SMT formula: {e}") - solver.set("timeout", 60 * 1000) + if timeout_ms is not None: + solver.set("timeout", timeout_ms) t_start = time.time() res = solver.check() t_check = time.time() - t_start diff --git a/symbolic-explorer/strategy/StrategyService.py b/symbolic-explorer/strategy/StrategyService.py index 5d97d72..56f3924 100755 --- a/symbolic-explorer/strategy/StrategyService.py +++ b/symbolic-explorer/strategy/StrategyService.py @@ -82,7 +82,7 @@ def collect_uf_definitions(node: Node) -> list(): return uf_definitions @staticmethod - def solve_branch(possible_branch: Node, endpoint_id=None): + def solve_branch(possible_branch: Node, endpoint_id=None, solver_timeout_ms: int | None = 60 * 1000): db = Database.instance() path_constraints = StrategyService.collect_path_constrains(possible_branch) @@ -93,7 +93,7 @@ def solve_branch(possible_branch: Node, endpoint_id=None): inputs = possible_branch.inputs - sat, sol = Z3Handler.solve(possible_branch, path_constraints) + sat, sol = Z3Handler.solve(possible_branch, path_constraints, timeout_ms=solver_timeout_ms) if sat == SATResult.SAT: db.add_solution(branch_id=possible_branch.gid, sol=sol, inputs=inputs, endpoint_id=endpoint_id) diff --git a/symbolic-explorer/svcomp/SVCompHandler.py b/symbolic-explorer/svcomp/SVCompHandler.py index 7922fb1..a14c9ae 100755 --- a/symbolic-explorer/svcomp/SVCompHandler.py +++ b/symbolic-explorer/svcomp/SVCompHandler.py @@ -192,7 +192,7 @@ def retrieve_solution(self): if not StrategyService.is_symbolic_branch(branch): continue branch_found = True - sat, sol = StrategyService.solve_branch(branch) + sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None) if sat == SATResult.SAT: symbolic_vars = branch.inputs diff --git a/targets/sv-comp/WitnessCreator/build.gradle b/targets/sv-comp/WitnessCreator/build.gradle deleted file mode 100755 index 78e0867..0000000 --- a/targets/sv-comp/WitnessCreator/build.gradle +++ /dev/null @@ -1,44 +0,0 @@ -buildscript { - repositories { - gradlePluginPortal() - } - dependencies { - classpath 'com.github.johnrengelman:shadow:8.1.1' - } -} - -plugins { - id 'java' - id 'com.github.johnrengelman.shadow' version '8.1.1' -} - -group = 'org.example' -version = '1.0-SNAPSHOT' - -apply plugin: 'com.github.johnrengelman.shadow' -apply plugin: 'java' - -shadowJar { - archiveBaseName.set('WitnessCreator') - archiveClassifier.set('') - archiveVersion.set('') -} - -repositories { - mavenCentral() -} - -dependencies { - - implementation 'org.antlr:ST4:4.3.4' - -} - - -jar { - manifest { - attributes( - 'Main-Class': 'App' - ) - } -} \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/src/main/java/App.java b/targets/sv-comp/WitnessCreator/src/main/java/App.java deleted file mode 100755 index 37f7d43..0000000 --- a/targets/sv-comp/WitnessCreator/src/main/java/App.java +++ /dev/null @@ -1,180 +0,0 @@ -import java.io.BufferedReader; -import java.io.IOException; -import java.io.InputStream; -import java.io.InputStreamReader; -import java.nio.file.Files; -import java.nio.file.Paths; -import java.util.ArrayList; -import java.util.Base64; -import java.util.LinkedList; -import java.util.List; - -import org.stringtemplate.v4.ST; -import org.stringtemplate.v4.STGroup; -import org.stringtemplate.v4.STRawGroupDir; - -import witness.WitnessAssumption; -import witness.WitnessEdge; -import witness.WitnessNode; - -public class App { - - public static void main(String[] args) { - - - String path = args[1]; - System.out.println("source path: " + path); - - List witness = new LinkedList<>(); - if(args[0].trim().length() == 0) { - System.out.println("No witness record, assuming default assertion violation"); - (new App()).saveDefaultviolationWitness(path); - } else { - String param = new String(Base64.getDecoder().decode(args[0])); - String[] lines = param.split("\n"); - for (String line : lines) { - line = line.substring(line.indexOf("[WITNESS]") + 10).trim(); - // decode line base64 - byte[] decodedBytes = Base64.getDecoder().decode(line); - line = new String(decodedBytes); - - String[] parts = line.split("@@@"); - if (parts.length != 4) { - System.out.println("Received line:" + line); - throw new RuntimeException("Invalid witness line: " + line); - } - - String value = parts[0].trim(); - int lineNumber = Integer.parseInt(parts[1].trim()); // account for 0-based line numbers - String className = parts[2].trim(); - String description = parts[3].trim(); - - // Escape XML special characters in scope to avoid XML parse errors - // (e.g., contains angle brackets that break XML parsing) - String scope = "L" + className + ";." + description; - scope = scope.replace("&", "&").replace("<", "<").replace(">", ">"); - witness.add(new WitnessAssumption(value, className + ".java", scope, lineNumber)); - } - (new App()).checkAndSaveWitness(path, witness); - } - } - - - - private void saveDefaultviolationWitness(String path){ - STGroup group = new STRawGroupDir("witnesses", '$','$'); - ST st = group.getInstanceOf("default_violation"); - String result = st.render(); - try { - System.out.println("Writing default violation witness to file: " + path + "/" + "witness.graphml"); - Files.write(Paths.get(path + "/" + "witness.graphml"), result.getBytes()); - } catch (IOException e) { - System.err.println("Error writing witness to file: " + e.getMessage()); - } - } - private void checkAndSaveWitness(String path, List witness) { - - - List nodes = new ArrayList<>(); - List edges = new ArrayList<>(); - - int nodeId = 0; - WitnessNode initNode = new WitnessNode(nodeId++); - nodes.add(initNode); - initNode.addData("entry", "true"); - WitnessNode curNode = initNode; - - for (WitnessAssumption wa : witness) { - String loc = getLineOfCode(path, wa.getClazz(), wa.getLine()); - String assumption = computeAssumption(loc, wa); - - WitnessNode prevNode = curNode; - curNode = new WitnessNode(nodeId++); - nodes.add(curNode); - WitnessEdge edge = new WitnessEdge(prevNode, wa, assumption, curNode); - edges.add(edge); - } - - curNode.addData("violation", "true"); - - STGroup group = new STRawGroupDir("witnesses", '$','$'); - ST st = group.getInstanceOf("witness"); - st.add("nodes", nodes); - st.add("edges", edges); - String result = st.render(); - try { - System.out.println("Writing violation witness to file: " + path + "/" + "witness.graphml"); - Files.write(Paths.get(path + "/" + "witness.graphml"), result.getBytes()); - } catch (IOException e) { - System.out.println("Error writing witness to file: " + e.getMessage()); - } - } - - private String getLineOfCode(String path, String filename, int line) { - String absolutePath = path + "/" + filename; - try { - // Open absolutePath as a stream - InputStream is = Files.newInputStream(Paths.get(absolutePath)); - if (is == null) { - System.out.println("Could not find file: " + absolutePath); - return null; - } - BufferedReader res = new BufferedReader(new InputStreamReader(is)); - String loc = ""; - for (int i = 0; i 0 && lineOfCode.charAt(idx - 1) == '=') { - // This is a comparison like "if (pos == ..." - no variable assignment - return wa.getValue(); - } - lineOfCode = lineOfCode.substring(0, idx).trim(); - String[] parts = lineOfCode.split(" "); - String id = parts[parts.length-1].trim(); - - // For string types, always use .equals() format with properly quoted value - if (isStringType) { - String value = wa.getValue(); - // Add quotes around the value if not already present - if (!value.startsWith("\"")) { - // Escape any quotes and backslashes within the string value - value = value.replace("\\", "\\\\").replace("\"", "\\\""); - value = "\"" + value + "\""; - } - return id + ".equals(" + value + ")"; - } - - // For primitive types, use assignment format - return id + " = " + wa.getValue(); - } - -} \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java deleted file mode 100755 index d841c67..0000000 --- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java +++ /dev/null @@ -1,33 +0,0 @@ -package witness; - -public class WitnessAssumption { - - private String scope; - private String value; - private final String clazz; - private final int line; - - public WitnessAssumption(String value, String clazz, String scope, int line) { - this.scope = scope; - this.value = value; - this.clazz = clazz; - this.line = line; - } - - public String getScope() { - return scope; - } - - public String getValue() { - return value; - } - - public String getClazz() { - return clazz; - } - - public int getLine() { - return line; - } - -} diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java deleted file mode 100755 index 47fc961..0000000 --- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java +++ /dev/null @@ -1,35 +0,0 @@ -package witness; - -public class WitnessEdge { - - private final WitnessNode source; - - private final WitnessNode dest; - - private final WitnessAssumption witness; - - private final String assumption; - - public WitnessEdge(WitnessNode source, WitnessAssumption witness, String assumption, WitnessNode dest) { - this.source = source; - this.dest = dest; - this.witness = witness; - this.assumption = assumption; - } - - public WitnessNode getSource() { - return source; - } - - public WitnessNode getDest() { - return dest; - } - - public WitnessAssumption getWitness() { - return witness; - } - - public String getAssumption() { - return assumption; - } -} \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java deleted file mode 100755 index 8ccc62e..0000000 --- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java +++ /dev/null @@ -1,29 +0,0 @@ -package witness; - -import java.util.HashMap; -import java.util.Map; - -public class WitnessNode { - - private final int id; - - private final Map data; - - public WitnessNode(int id) { - this.id = id; - this.data = new HashMap<>(); - } - - public int getId() { - return id; - } - - public Map getData() { - return data; - } - - public void addData(String key, String value) { - this.data.put(key, value); - } - -} \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/witness.graphml b/targets/sv-comp/WitnessCreator/witness.graphml deleted file mode 100644 index 99e9ee6..0000000 --- a/targets/sv-comp/WitnessCreator/witness.graphml +++ /dev/null @@ -1,134 +0,0 @@ - - - - <command-line> - - - - - false - - - false - - - false - - - false - - - false - - - 0 - - - 0 - - - - - - - - - - - - - - - - - violation_witness - SWAT - - - - - true - - - - - - - - - - - - - - - - - - - true - - - - - Main.java - 12 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 13 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 14 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 15 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 16 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 17 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 18 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 19 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 20 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - - - \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/witnesses/default_violation.st b/targets/sv-comp/WitnessCreator/witnesses/default_violation.st deleted file mode 100755 index 81cb4a6..0000000 --- a/targets/sv-comp/WitnessCreator/witnesses/default_violation.st +++ /dev/null @@ -1,56 +0,0 @@ - - - - <command-line> - - - - - false - - - false - - - false - - - false - - - false - - - 0 - - - 0 - - - - - - - - - - - - - - - - - violation_witness - SWAT - - - - true true - - - \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/witnesses/witness.st b/targets/sv-comp/WitnessCreator/witnesses/witness.st deleted file mode 100755 index 6e7e57a..0000000 --- a/targets/sv-comp/WitnessCreator/witnesses/witness.st +++ /dev/null @@ -1,70 +0,0 @@ - - - - <command-line> - - - - - false - - - false - - - false - - - false - - - false - - - 0 - - - 0 - - - - - - - - - - - - - - - - - violation_witness - SWAT - - - - $nodes:{ n | - - $n.data.keys:{k | - $n.data.(k)$ }$ - - }$ - - $edges:{ e | - - $e.witness.clazz$ - $e.witness.line$ - 0 - $e.assumption$ - java::$e.witness.scope$ - }$ - - - \ No newline at end of file diff --git a/targets/sv-comp/scripts/commands/test.py b/targets/sv-comp/scripts/commands/test.py index a40e526..54e748b 100644 --- a/targets/sv-comp/scripts/commands/test.py +++ b/targets/sv-comp/scripts/commands/test.py @@ -107,7 +107,7 @@ def run_tests(ctx, mode, workers, benchmark_dir, config_file, categories, target click.echo(f"Filtered to {len(ver_tasks)} test cases for categories: {[c.value for c in selected_categories]}") # Generate commands - if mode == 'single' and target is None: + if mode == 'single': # Use default target from original script config = 'swat-debug.cfg' else: