diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 5a970e1..d2930b5 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -10,42 +10,69 @@ on: workflow_dispatch: jobs: - build: + test: runs-on: ubuntu-latest permissions: contents: read + strategy: + fail-fast: false + matrix: + python-version: ['3.10', '3.13', '3.14'] steps: - uses: actions/checkout@v5 - - name: Set up JDK 17 - uses: actions/setup-java@v4 + - uses: actions/setup-python@v5 with: - java-version: '17' - distribution: 'temurin' + python-version: ${{ matrix.python-version }} - - name: Setup Gradle - uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 + - name: Install + run: python -m pip install --upgrade pip && python -m pip install -e '.[test]' - - name: Build release artifact + - name: Install WitnessLint run: | - version="${GITHUB_REF_NAME#v}" - if [[ "$GITHUB_REF_TYPE" != "tag" ]]; then - version="ci-${GITHUB_SHA::7}" - fi - ./gradlew --no-daemon -PwitnessCreatorVersion="$version" clean build + git clone --depth 1 https://gitlab.com/sosy-lab/benchmarking/sv-witnesses.git "$RUNNER_TEMP/sv-witnesses" + python -m pip install -r "$RUNNER_TEMP/sv-witnesses/linter/requirements.txt" + echo "WITNESSLINT=python $RUNNER_TEMP/sv-witnesses/linter/witnesslinter.py" >> "$GITHUB_ENV" + + - name: Test (unit, golden, WitnessLint on generated witnesses) + run: python -m pytest -v -rs + + - name: Smoke-test the command line + run: | + witnesscreator --version + python -m witnesscreator --help > /dev/null + + build: + needs: test + runs-on: ubuntu-latest + permissions: + contents: read + steps: + - uses: actions/checkout@v5 + + - uses: actions/setup-python@v5 + with: + python-version: '3.14' - - name: Create checksum + - name: Build wheel, sdist and zipapp run: | - cd build/distributions - sha256sum witness-creator-*.zip > SHA256SUMS + python -m pip install --upgrade pip build + python -m build + python tools/build_pyz.py dist/witnesscreator.pyz + python dist/witnesscreator.pyz --version + python -m pip install dist/witnesscreator-*.whl + witnesscreator --version + cd dist && sha256sum witnesscreator-* > SHA256SUMS && cat SHA256SUMS - name: Upload CI artifact uses: actions/upload-artifact@v4 with: - name: witness-creator-${{ github.sha }} + name: witnesscreator-${{ github.sha }} path: | - build/distributions/witness-creator-*.zip - build/distributions/SHA256SUMS + dist/witnesscreator-*.whl + dist/witnesscreator-*.tar.gz + dist/witnesscreator.pyz + dist/SHA256SUMS if-no-files-found: error release: @@ -60,7 +87,7 @@ jobs: - name: Download CI artifact uses: actions/download-artifact@v4 with: - name: witness-creator-${{ github.sha }} + name: witnesscreator-${{ github.sha }} path: dist - name: Publish GitHub release @@ -68,13 +95,14 @@ jobs: GH_TOKEN: ${{ github.token }} run: | tag="${GITHUB_REF_NAME}" - notes="$(printf 'Automated WitnessCreator release.\n\nCommit: %s\nRun: %s/%s/actions/runs/%s\n' \ - "$GITHUB_SHA" "$GITHUB_SERVER_URL" "$GITHUB_REPOSITORY" "$GITHUB_RUN_ID")" + notes="$(printf 'Automated WitnessCreator release.\n\nInstall: pip install git+https://github.com/%s@%s\n\nCommit: %s\nRun: %s/%s/actions/runs/%s\n' \ + "$GITHUB_REPOSITORY" "$tag" "$GITHUB_SHA" "$GITHUB_SERVER_URL" "$GITHUB_REPOSITORY" "$GITHUB_RUN_ID")" + files=(dist/witnesscreator-*.whl dist/witnesscreator-*.tar.gz dist/witnesscreator.pyz dist/SHA256SUMS) if gh release view "$tag" >/dev/null 2>&1; then - gh release upload "$tag" dist/witness-creator-*.zip dist/SHA256SUMS --clobber + gh release upload "$tag" "${files[@]}" --clobber else - gh release create "$tag" dist/witness-creator-*.zip dist/SHA256SUMS \ + gh release create "$tag" "${files[@]}" \ --verify-tag \ --title "WitnessCreator ${tag}" \ --notes "$notes" diff --git a/.gitignore b/.gitignore index 8642f23..5772f43 100644 --- a/.gitignore +++ b/.gitignore @@ -1,8 +1,18 @@ -.gradle/ +__pycache__/ +*.py[cod] +*.egg-info/ +.eggs/ build/ -out/ -*.class +dist/ +*.pyz +.pytest_cache/ +.venv/ +venv/ *.log .DS_Store -*.iml .idea/ +*.iml +# leftovers of the Java build +.gradle/ +out/ +*.class diff --git a/MANIFEST.in b/MANIFEST.in new file mode 100644 index 0000000..bc8afda --- /dev/null +++ b/MANIFEST.in @@ -0,0 +1,3 @@ +recursive-include tests * +recursive-include tools *.py +global-exclude __pycache__ *.py[cod] diff --git a/README.md b/README.md index bc9cd54..b842b3c 100644 --- a/README.md +++ b/README.md @@ -1,26 +1,159 @@ # WitnessCreator -WitnessCreator creates SV-COMP GraphML violation witnesses from SWAT witness -markers. +WitnessCreator creates SV-COMP violation witnesses for Java programs: -## Build +- `witness.yml` in the [YAML witness format 2.3](https://gitlab.com/sosy-lab/benchmarking/sv-witnesses) + (required for Java in SV-COMP 2027): one `violation_sequence` with a `function_return` + waypoint per `Verifier.nondet*()` value (`\result == ` at the closing + parenthesis of the call) and a final `target` waypoint at the violating statement; +- `witness.graphml` in the legacy GraphML format, for validators such as wit4java that + still consume it. + +It is a pure-Python package (Python >= 3.10, no runtime dependencies) with a library API, +a command line interface and a single-file `witnesscreator.pyz`. It is used by +[SWAT](https://github.com/SWAT-project/SWAT) but does not depend on it: any tool that knows +the values its `Verifier.nondet*()` calls returned and where the violation happened can use it. + +## Installation ```sh -./gradlew --no-daemon clean build +pip install git+https://github.com/SWAT-project/WitnessCreator@v1.0.0 ``` -The release archive is written to `build/distributions/` and contains the -runtime layout expected by SWAT: +or download `witnesscreator--py3-none-any.whl` / `witnesscreator.pyz` from the +[releases](https://github.com/SWAT-project/WitnessCreator/releases). The `.pyz` needs nothing +but a Python interpreter: `python3 witnesscreator.pyz ...`. + +## Library + +```python +from witnesscreator import Task, Location, NondetReturn, Frame, Violation, write_witnesses + +task = Task( + input_files=["../common/", "Main.java"], # as given to the verifier; directories are expanded to *.java + property_file="valid-assert.prp", # its content becomes metadata.task.specification + producer_name="MyVerifier", producer_version="1.0", + base_dir=None, # resolve relative paths against this directory (default: cwd) +) -```text -WitnessCreator/ - build/libs/WitnessCreator.jar - witnesses/default_violation.st - witnesses/witness.st +values = [ + NondetReturn( + function="nondetInt", # Verifier method name + type="int", # boolean|byte|short|char|int|long|float|double|String + value="42", # decimal; char = code point; float/double as Java's toString + # (NaN, Infinity, -Infinity, -0.0); String = the raw string + location=Location(class_name="pkg.Main", source_file="Main.java", line=12, call_index=0), + # or Location(file_name="Main.java", line=12, column=27) when file and column are already known + ), +] + +violation = Violation( + throwable="java.lang.AssertionError", + frames=[Frame(class_name="pkg.Main", source_file="Main.java", line=17)], # innermost first +) # or None if unknown + +paths = write_witnesses(task, values, violation, out_dir="output", formats=("yaml", "graphml")) +# {'yaml': PosixPath('output/witness.yml'), 'graphml': PosixPath('output/witness.graphml')} ``` +- `call_index` is the 0-based index of the call among the `nondet*` calls on that source + line (left to right, which is Java's evaluation order). The column of the waypoint is the + closing parenthesis of that call; calls inside comments and string literals are ignored. +- The target is the innermost stack frame that lies in the task sources (frames of `java.`, + `javax.`, `jdk.`, `sun.` and `de.uzl.its.swat.` are skipped, the package of a class must match + the file's path or `package` declaration). Its column is the `assert` of a failed assertion, + the `throw` of an explicit throw, or the first token of the statement. +- `write_witnesses` never raises for bad data: problems are logged on the `witnesscreator` + logger, each format is written independently and only the formats actually written are + returned. Without a target a warning is logged and the witness has no `target` waypoint. +- `render_yaml(task, values, violation)` and `render_graphml(...)` return the documents as strings. + +Values can also be exchanged through an event file (JSON lines, see below): +`dump_events(values, violation, producer_name, producer_version)` writes it, +`read_events(path)` reads it. + +## Command line + +`witnesscreator` (console script), `python -m witnesscreator` and `python3 witnesscreator.pyz` +are equivalent. Exit status is 0 once a witness was written, 1 if nothing could be written +and 2 for usage errors. Progress and warnings go to stderr. + +### Event file + +```sh +witnesscreator events --events run.jsonl --property valid-assert.prp \ + --input ../common/ --input Main.java --out-dir witness \ + [--format yaml|graphml|both] [--producer-name N] [--producer-version V] [--base-dir DIR] +``` + +`run.jsonl` holds one JSON object per line, the serialization of the objects above: + +```json +{"kind": "header", "schema": "witnesscreator-events", "version": 1, "producer": {"name": "MyVerifier", "version": "1.0"}} +{"kind": "nondet_return", "function": "nondetInt", "type": "int", "value": "42", "location": {"class_name": "pkg.Main", "source_file": "Main.java", "line": 12, "call_index": 0}, "bits": null} +{"kind": "violation", "throwable": "java.lang.AssertionError", "frames": [{"class_name": "pkg.Main", "source_file": "Main.java", "line": 17}]} +``` + +The `producer` of the header is optional and overridden by `--producer-name` / +`--producer-version`. Unknown or malformed lines are skipped with a warning. + +### Legacy markers (SWAT output lines) + +```sh +witnesscreator legacy [] [--markers-file FILE] --input ../common/ --input Main.java \ + --property valid-assert.prp --out-dir witness [--format ...] [--producer-name N] [--producer-version V] +``` + +reads the `[WITNESS]` / `[WITNESS_TARGET]` markers SWAT printed, either as the base64 of the +output lines (as SWAT passed them to the Java tool) or from a file holding the lines (plain +text or base64). Both marker payload forms are accepted: +`value@@@line@@@class@@@methodDesc@@@callIndex@@@typeDesc@@@sourceFile` and the old +`value@@@line@@@class@@@methodDesc`. The producer defaults to `SWAT` / `unknown`. + +The Java tool's command line keeps working unchanged (`witnesscreator` replaces +`java -jar WitnessCreator.jar`): + +```sh +witnesscreator [] [--input PATH]... [--property FILE.prp] [--out DIR] [--producer-version V] +``` + +`` is both the (only) input and the default output directory; an empty `` +yields the default violation witness without waypoints. + +## Development + +```sh +pip install -e '.[test]' +python -m pytest # unit, golden and CLI tests +WITNESSLINT="python /path/to/sv-witnesses/linter/witnesslinter.py" python -m pytest # also lint the generated witnesses +python -m build # wheel + sdist in dist/ +python tools/build_pyz.py # dist/witnesscreator.pyz +``` + +The golden tests run on copies of SV-COMP tasks in `tests/fixtures/` (see the README there); +generated witnesses are parsed with PyYAML / ElementTree and, when WitnessLint is available +(`$WITNESSLINT` or the CI setup), checked with it. + ## Release -Push a version tag such as `v0.1.0`. The CI workflow builds -`witness-creator-.zip`, uploads it as a CI artifact, and attaches it to -the GitHub release for that tag together with `SHA256SUMS`. +Push a version tag such as `v1.0.0`. The CI workflow runs the tests on Python 3.10, 3.13 +and 3.14, builds the wheel, the sdist and `witnesscreator.pyz`, and attaches them together +with `SHA256SUMS` to the GitHub release for that tag. + +## Migrating from the Java version (0.x) + +Version 1.0 replaces the Java/Gradle implementation; there is no jar and no +`witnesses/*.st` template directory any more. + +- Replace `java -jar build/libs/WitnessCreator.jar ARGS` by `witnesscreator ARGS` (or + `python3 witnesscreator.pyz ARGS`); the arguments are unchanged. The tool no longer needs to + run from a particular working directory. +- Output files and their names (`witness.yml`, `witness.graphml`) are unchanged. Differences in + content: GraphML assumptions are now `\result = ;` / `\result.equals("...");` instead + of a variable name guessed from the source line, all GraphML text is XML-escaped, and the + graph carries `sourcecodelang` and `specification`. Strings and chars escape every + non-ASCII character (`\uXXXX`) in Java literals, YAML scalars are plain ASCII. +- Target resolution is stricter: a stack frame only becomes the target when its package + matches the file (path or `package` declaration); JDK and SWAT frames are skipped. +- Progress messages are written to stderr (logging) instead of stdout. +- Prefer the library API or the event file over the markers for new integrations. diff --git a/build.gradle b/build.gradle deleted file mode 100644 index 0429df6..0000000 --- a/build.gradle +++ /dev/null @@ -1,65 +0,0 @@ -plugins { - id 'application' - id 'com.github.johnrengelman.shadow' version '8.1.1' -} - -group = 'de.uzl.its.swat' -version = providers.gradleProperty('witnessCreatorVersion') - .orElse('0.1.0-SNAPSHOT') - .get() - -repositories { - mavenCentral() -} - -dependencies { - implementation 'org.antlr:ST4:4.3.4' -} - -java { - toolchain { - languageVersion = JavaLanguageVersion.of(17) - } -} - -application { - mainClass = 'App' -} - -jar { - manifest { - attributes('Main-Class': application.mainClass.get()) - } -} - -shadowJar { - archiveBaseName.set('WitnessCreator') - archiveClassifier.set('') - archiveVersion.set('') -} - -def shadowJarTask = tasks.named('shadowJar') - -tasks.register('svcompDistributionZip', Zip) { - dependsOn shadowJarTask - - archiveBaseName.set('witness-creator') - archiveVersion.set(project.version.toString()) - destinationDirectory.set(layout.buildDirectory.dir('distributions')) - - into('WitnessCreator/build/libs') { - from(shadowJarTask.flatMap { it.archiveFile }) - rename { 'WitnessCreator.jar' } - } - - into('WitnessCreator/witnesses') { - from('witnesses') { - include '*.st' - } - } -} - -build { - dependsOn shadowJar - dependsOn svcompDistributionZip -} diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar deleted file mode 100644 index 7f93135..0000000 Binary files a/gradle/wrapper/gradle-wrapper.jar and /dev/null differ diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties deleted file mode 100644 index 3fa8f86..0000000 --- a/gradle/wrapper/gradle-wrapper.properties +++ /dev/null @@ -1,7 +0,0 @@ -distributionBase=GRADLE_USER_HOME -distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip -networkTimeout=10000 -validateDistributionUrl=true -zipStoreBase=GRADLE_USER_HOME -zipStorePath=wrapper/dists diff --git a/gradlew b/gradlew deleted file mode 100755 index 0adc8e1..0000000 --- a/gradlew +++ /dev/null @@ -1,249 +0,0 @@ -#!/bin/sh - -# -# Copyright © 2015-2021 the original authors. -# -# Licensed under the Apache License, Version 2.0 (the "License"); -# you may not use this file except in compliance with the License. -# You may obtain a copy of the License at -# -# https://www.apache.org/licenses/LICENSE-2.0 -# -# Unless required by applicable law or agreed to in writing, software -# distributed under the License is distributed on an "AS IS" BASIS, -# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -# See the License for the specific language governing permissions and -# limitations under the License. -# - -############################################################################## -# -# Gradle start up script for POSIX generated by Gradle. -# -# Important for running: -# -# (1) You need a POSIX-compliant shell to run this script. If your /bin/sh is -# noncompliant, but you have some other compliant shell such as ksh or -# bash, then to run this script, type that shell name before the whole -# command line, like: -# -# ksh Gradle -# -# Busybox and similar reduced shells will NOT work, because this script -# requires all of these POSIX shell features: -# * functions; -# * expansions «$var», «${var}», «${var:-default}», «${var+SET}», -# «${var#prefix}», «${var%suffix}», and «$( cmd )»; -# * compound commands having a testable exit status, especially «case»; -# * various built-in commands including «command», «set», and «ulimit». -# -# Important for patching: -# -# (2) This script targets any POSIX shell, so it avoids extensions provided -# by Bash, Ksh, etc; in particular arrays are avoided. -# -# The "traditional" practice of packing multiple parameters into a -# space-separated string is a well documented source of bugs and security -# problems, so this is (mostly) avoided, by progressively accumulating -# options in "$@", and eventually passing that to Java. -# -# Where the inherited environment variables (DEFAULT_JVM_OPTS, JAVA_OPTS, -# and GRADLE_OPTS) rely on word-splitting, this is performed explicitly; -# see the in-line comments for details. -# -# There are tweaks for specific operating systems such as AIX, CygWin, -# Darwin, MinGW, and NonStop. -# -# (3) This script is generated from the Groovy template -# https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt -# within the Gradle project. -# -# You can find Gradle at https://github.com/gradle/gradle/. -# -############################################################################## - -# Attempt to set APP_HOME - -# Resolve links: $0 may be a link -app_path=$0 - -# Need this for daisy-chained symlinks. -while - APP_HOME=${app_path%"${app_path##*/}"} # leaves a trailing /; empty if no leading path - [ -h "$app_path" ] -do - ls=$( ls -ld "$app_path" ) - link=${ls#*' -> '} - case $link in #( - /*) app_path=$link ;; #( - *) app_path=$APP_HOME$link ;; - esac -done - -# This is normally unused -# shellcheck disable=SC2034 -APP_BASE_NAME=${0##*/} -# Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036) -APP_HOME=$( cd "${APP_HOME:-./}" > /dev/null && pwd -P ) || exit - -# Use the maximum available, or set MAX_FD != -1 to use that value. -MAX_FD=maximum - -warn () { - echo "$*" -} >&2 - -die () { - echo - echo "$*" - echo - exit 1 -} >&2 - -# OS specific support (must be 'true' or 'false'). -cygwin=false -msys=false -darwin=false -nonstop=false -case "$( uname )" in #( - CYGWIN* ) cygwin=true ;; #( - Darwin* ) darwin=true ;; #( - MSYS* | MINGW* ) msys=true ;; #( - NONSTOP* ) nonstop=true ;; -esac - -CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar - - -# Determine the Java command to use to start the JVM. -if [ -n "$JAVA_HOME" ] ; then - if [ -x "$JAVA_HOME/jre/sh/java" ] ; then - # IBM's JDK on AIX uses strange locations for the executables - JAVACMD=$JAVA_HOME/jre/sh/java - else - JAVACMD=$JAVA_HOME/bin/java - fi - if [ ! -x "$JAVACMD" ] ; then - die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME - -Please set the JAVA_HOME variable in your environment to match the -location of your Java installation." - fi -else - JAVACMD=java - if ! command -v java >/dev/null 2>&1 - then - die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. - -Please set the JAVA_HOME variable in your environment to match the -location of your Java installation." - fi -fi - -# Increase the maximum file descriptors if we can. -if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then - case $MAX_FD in #( - max*) - # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked. - # shellcheck disable=SC3045 - MAX_FD=$( ulimit -H -n ) || - warn "Could not query maximum file descriptor limit" - esac - case $MAX_FD in #( - '' | soft) :;; #( - *) - # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked. - # shellcheck disable=SC3045 - ulimit -n "$MAX_FD" || - warn "Could not set maximum file descriptor limit to $MAX_FD" - esac -fi - -# Collect all arguments for the java command, stacking in reverse order: -# * args from the command line -# * the main class name -# * -classpath -# * -D...appname settings -# * --module-path (only if needed) -# * DEFAULT_JVM_OPTS, JAVA_OPTS, and GRADLE_OPTS environment variables. - -# For Cygwin or MSYS, switch paths to Windows format before running java -if "$cygwin" || "$msys" ; then - APP_HOME=$( cygpath --path --mixed "$APP_HOME" ) - CLASSPATH=$( cygpath --path --mixed "$CLASSPATH" ) - - JAVACMD=$( cygpath --unix "$JAVACMD" ) - - # Now convert the arguments - kludge to limit ourselves to /bin/sh - for arg do - if - case $arg in #( - -*) false ;; # don't mess with options #( - /?*) t=${arg#/} t=/${t%%/*} # looks like a POSIX filepath - [ -e "$t" ] ;; #( - *) false ;; - esac - then - arg=$( cygpath --path --ignore --mixed "$arg" ) - fi - # Roll the args list around exactly as many times as the number of - # args, so each arg winds up back in the position where it started, but - # possibly modified. - # - # NB: a `for` loop captures its iteration list before it begins, so - # changing the positional parameters here affects neither the number of - # iterations, nor the values presented in `arg`. - shift # remove old arg - set -- "$@" "$arg" # push replacement arg - done -fi - - -# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. -DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"' - -# Collect all arguments for the java command; -# * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of -# shell script including quotes and variable substitutions, so put them in -# double quotes to make sure that they get re-expanded; and -# * put everything else in single quotes, so that it's not re-expanded. - -set -- \ - "-Dorg.gradle.appname=$APP_BASE_NAME" \ - -classpath "$CLASSPATH" \ - org.gradle.wrapper.GradleWrapperMain \ - "$@" - -# Stop when "xargs" is not available. -if ! command -v xargs >/dev/null 2>&1 -then - die "xargs is not available" -fi - -# Use "xargs" to parse quoted args. -# -# With -n1 it outputs one arg per line, with the quotes and backslashes removed. -# -# In Bash we could simply go: -# -# readarray ARGS < <( xargs -n1 <<<"$var" ) && -# set -- "${ARGS[@]}" "$@" -# -# but POSIX shell has neither arrays nor command substitution, so instead we -# post-process each arg (as a line of input to sed) to backslash-escape any -# character that might be a shell metacharacter, then use eval to reverse -# that process (while maintaining the separation between arguments), and wrap -# the whole thing up as a single "set" statement. -# -# This will of course break if any of these variables contains a newline or -# an unmatched quote. -# - -eval "set -- $( - printf '%s\n' "$DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS" | - xargs -n1 | - sed ' s~[^-[:alnum:]+,./:=@_]~\\&~g; ' | - tr '\n' ' ' - )" '"$@"' - -exec "$JAVACMD" "$@" diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..ef473de --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,51 @@ +[build-system] +requires = ["setuptools>=68"] +build-backend = "setuptools.build_meta" + +[project] +name = "witnesscreator" +dynamic = ["version"] +description = "SV-COMP violation witnesses for Java: YAML format 2.3 and legacy GraphML" +readme = "README.md" +license = { file = "LICENSE" } +requires-python = ">=3.10" +authors = [{ name = "Nils Loose" }] +keywords = ["sv-comp", "witness", "java", "verification"] +classifiers = [ + "Development Status :: 5 - Production/Stable", + "Intended Audience :: Science/Research", + "License :: OSI Approved :: BSD License", + "Operating System :: OS Independent", + "Programming Language :: Python :: 3", + "Programming Language :: Python :: 3 :: Only", + "Programming Language :: Python :: 3.10", + "Programming Language :: Python :: 3.11", + "Programming Language :: Python :: 3.12", + "Programming Language :: Python :: 3.13", + "Programming Language :: Python :: 3.14", + "Topic :: Software Development :: Testing", +] +dependencies = [] + +[project.optional-dependencies] +test = ["pytest>=7", "PyYAML>=6"] + +[project.scripts] +witnesscreator = "witnesscreator.cli:main" + +[project.urls] +Homepage = "https://github.com/SWAT-project/WitnessCreator" +Issues = "https://github.com/SWAT-project/WitnessCreator/issues" + +[tool.setuptools] +package-dir = { "" = "src" } + +[tool.setuptools.packages.find] +where = ["src"] + +[tool.setuptools.dynamic] +version = { attr = "witnesscreator._version.__version__" } + +[tool.pytest.ini_options] +testpaths = ["tests"] +addopts = "-ra" diff --git a/settings.gradle b/settings.gradle deleted file mode 100644 index efe09d0..0000000 --- a/settings.gradle +++ /dev/null @@ -1,8 +0,0 @@ -pluginManagement { - repositories { - gradlePluginPortal() - mavenCentral() - } -} - -rootProject.name = 'WitnessCreator' diff --git a/src/main/java/App.java b/src/main/java/App.java deleted file mode 100755 index 37f7d43..0000000 --- a/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/src/main/java/witness/WitnessAssumption.java b/src/main/java/witness/WitnessAssumption.java deleted file mode 100644 index 83fea6c..0000000 --- a/src/main/java/witness/WitnessAssumption.java +++ /dev/null @@ -1,31 +0,0 @@ -package witness; - -public class WitnessAssumption { - private final String value; - private final String clazz; - private final String scope; - private final int line; - - public WitnessAssumption(String value, String clazz, String scope, int line) { - this.value = value; - this.clazz = clazz; - this.scope = scope; - 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/src/main/java/witness/WitnessEdge.java b/src/main/java/witness/WitnessEdge.java deleted file mode 100644 index 18a4fb6..0000000 --- a/src/main/java/witness/WitnessEdge.java +++ /dev/null @@ -1,31 +0,0 @@ -package witness; - -public class WitnessEdge { - private final WitnessNode source; - private final WitnessAssumption witness; - private final String assumption; - private final WitnessNode dest; - - public WitnessEdge(WitnessNode source, WitnessAssumption witness, String assumption, WitnessNode dest) { - this.source = source; - this.witness = witness; - this.assumption = assumption; - this.dest = dest; - } - - public WitnessNode getSource() { - return source; - } - - public WitnessNode getDest() { - return dest; - } - - public WitnessAssumption getWitness() { - return witness; - } - - public String getAssumption() { - return assumption; - } -} diff --git a/src/main/java/witness/WitnessNode.java b/src/main/java/witness/WitnessNode.java deleted file mode 100644 index 5e74e65..0000000 --- a/src/main/java/witness/WitnessNode.java +++ /dev/null @@ -1,25 +0,0 @@ -package witness; - -import java.util.LinkedHashMap; -import java.util.Map; - -public class WitnessNode { - private final int id; - private final Map data = new LinkedHashMap<>(); - - public WitnessNode(int id) { - this.id = id; - } - - public int getId() { - return id; - } - - public Map getData() { - return data; - } - - public void addData(String key, String value) { - data.put(key, value); - } -} diff --git a/src/witnesscreator/__init__.py b/src/witnesscreator/__init__.py new file mode 100644 index 0000000..fe8f234 --- /dev/null +++ b/src/witnesscreator/__init__.py @@ -0,0 +1,36 @@ +"""witnesscreator: SV-COMP violation witnesses for Java. + +>>> from witnesscreator import Task, Location, NondetReturn, Frame, Violation, write_witnesses +>>> task = Task(input_files=["../common/", "Main.java"], property_file="valid-assert.prp", +... producer_name="MyVerifier", producer_version="1.0") +>>> values = [NondetReturn("nondetInt", "int", "42", +... Location(class_name="Main", source_file="Main.java", line=12, call_index=0))] +>>> violation = Violation("java.lang.AssertionError", [Frame("Main", "Main.java", 17)]) +>>> write_witnesses(task, values, violation, out_dir="output") # doctest: +SKIP +{'yaml': PosixPath('output/witness.yml'), 'graphml': PosixPath('output/witness.graphml')} +""" + +from ._version import __version__ +from .events import dump_events, parse_events, read_events +from .markers import parse_marker_lines, parse_markers +from .model import JAVA_TYPES, Frame, Location, NondetReturn, Task, Violation +from .witness import FORMATS, render_graphml, render_yaml, write_witnesses + +__all__ = [ + "__version__", + "JAVA_TYPES", + "FORMATS", + "Task", + "Location", + "NondetReturn", + "Frame", + "Violation", + "write_witnesses", + "render_yaml", + "render_graphml", + "parse_markers", + "parse_marker_lines", + "read_events", + "parse_events", + "dump_events", +] diff --git a/src/witnesscreator/__main__.py b/src/witnesscreator/__main__.py new file mode 100644 index 0000000..dd8a8c9 --- /dev/null +++ b/src/witnesscreator/__main__.py @@ -0,0 +1,5 @@ +import sys + +from .cli import main + +sys.exit(main()) diff --git a/src/witnesscreator/_version.py b/src/witnesscreator/_version.py new file mode 100644 index 0000000..5becc17 --- /dev/null +++ b/src/witnesscreator/_version.py @@ -0,0 +1 @@ +__version__ = "1.0.0" diff --git a/src/witnesscreator/cli.py b/src/witnesscreator/cli.py new file mode 100644 index 0000000..6394ff4 --- /dev/null +++ b/src/witnesscreator/cli.py @@ -0,0 +1,164 @@ +"""Command line interface. + +:: + + witnesscreator events --events E.jsonl --property P.prp --input PATH... --out-dir D + [--format yaml|graphml|both] [--producer-name N] [--producer-version V] + witnesscreator legacy [ []] [--markers-file F] --input PATH... --property P.prp + --out-dir D [--format ...] [--producer-name N] [--producer-version V] + witnesscreator [] [--input PATH]... [--property P.prp] [--out D] + [--producer-version V] (the Java WitnessCreator's command line) + +Exit status 0 once a witness was written, 1 if nothing could be written, 2 for usage errors. +""" + +from __future__ import annotations + +import argparse +import logging +import sys +from pathlib import Path +from typing import List, Optional, Sequence + +from ._version import __version__ +from .events import read_events +from .markers import parse_markers +from .model import Task +from .witness import FORMATS, write_witnesses + +log = logging.getLogger("witnesscreator") + +SUBCOMMANDS = ("events", "legacy") +LEGACY_PRODUCER = "SWAT" + + +def _formats(choice: str) -> Sequence[str]: + return FORMATS if choice == "both" else (choice,) + + +def _add_common(p: argparse.ArgumentParser, producer_name: Optional[str], producer_version: Optional[str]) -> None: + p.add_argument("--input", action="append", default=[], metavar="PATH", + help="input file or directory of the task, exactly as given to the verifier (repeatable)") + p.add_argument("--property", metavar="FILE.prp", help="the property file; its content becomes the specification") + p.add_argument("--out-dir", "--out", dest="out_dir", metavar="DIR", help="where witness.yml / witness.graphml are written") + p.add_argument("--format", choices=("yaml", "graphml", "both"), default="both", help="which witness formats to write (default: both)") + p.add_argument("--producer-name", default=producer_name, metavar="NAME", + help=f"metadata.producer.name (default: {producer_name or 'the event file header, else witnesscreator'})") + p.add_argument("--producer-version", default=producer_version, metavar="VERSION", + help=f"metadata.producer.version (default: {producer_version or 'the event file header, else the witnesscreator version'})") + p.add_argument("--base-dir", metavar="DIR", help="resolve relative input and property paths against this directory") + + +def build_parser() -> argparse.ArgumentParser: + parser = argparse.ArgumentParser( + prog="witnesscreator", + description="Creates SV-COMP violation witnesses for Java (YAML format 2.3 and legacy GraphML).", + ) + parser.add_argument("--version", action="version", version=f"witnesscreator {__version__}") + parser.add_argument("-v", "--verbose", action="store_true", help="debug output") + parser.add_argument("-q", "--quiet", action="store_true", help="only warnings and errors") + sub = parser.add_subparsers(dest="command", metavar="COMMAND") + + events = sub.add_parser("events", help="create witnesses from an event file (JSON lines)") + events.add_argument("--events", required=True, metavar="FILE.jsonl", help="the event file") + _add_common(events, None, None) + + legacy = sub.add_parser( + "legacy", + help="create witnesses from SWAT's [WITNESS] / [WITNESS_TARGET] marker lines", + description="The markers are given base64-encoded on the command line (as SWAT printed them) " + "or as a file of marker lines. The positional is both an input and the default " + "output directory, like the Java WitnessCreator's.", + ) + legacy.add_argument("markers", nargs="?", default=None, metavar="BASE64", + help="base64 of the output lines carrying the markers (empty for the default violation witness)") + legacy.add_argument("dir", nargs="?", default=None, metavar="DIR", help="legacy: the task directory, also the output directory") + legacy.add_argument("--markers-file", metavar="FILE", help="file with the marker lines (plain text or base64)") + _add_common(legacy, LEGACY_PRODUCER, "unknown") + return parser + + +def _configure_logging(verbose: bool, quiet: bool) -> None: + level = logging.DEBUG if verbose else logging.WARNING if quiet else logging.INFO + handler = logging.StreamHandler(sys.stderr) + handler.setFormatter(logging.Formatter("%(levelname)s: %(message)s")) + logger = logging.getLogger("witnesscreator") + logger.handlers = [handler] + logger.setLevel(level) + logger.propagate = False + + +def _normalize_argv(argv: List[str]) -> List[str]: + """The Java command line (`` [] [--input ...]``) becomes ``legacy ...``.""" + if not argv: + return argv + first = argv[0] + if first in SUBCOMMANDS or first in ("-h", "--help", "--version"): + return argv + if first in ("-v", "--verbose", "-q", "--quiet") and len(argv) > 1 and argv[1] in SUBCOMMANDS: + return argv + return ["legacy"] + argv + + +def run_events(args: argparse.Namespace) -> int: + try: + ev = read_events(args.events) + except OSError as e: + log.error("Could not read event file %s: %s", args.events, e) + ev = None + values = ev.values if ev else [] + violation = ev.violation if ev else None + task = Task( + input_files=list(args.input), + property_file=args.property, + producer_name=args.producer_name or (ev.producer_name if ev else None) or "witnesscreator", + producer_version=args.producer_version or (ev.producer_version if ev else None) or __version__, + base_dir=args.base_dir, + ) + written = write_witnesses(task, values, violation, args.out_dir or ".", _formats(args.format)) + return 0 if written else 1 + + +def run_legacy(args: argparse.Namespace) -> int: + text = "" + if args.markers_file: + try: + text = Path(args.markers_file).read_text(encoding="utf-8", errors="replace") + except OSError as e: + log.error("Could not read markers file %s: %s", args.markers_file, e) + if args.markers: + text = (text + "\n" + args.markers) if text.strip() else args.markers + values, violation = parse_markers(text) + + inputs = list(args.input) + if not inputs and args.dir: + inputs.append(args.dir) + out_dir = args.out_dir or args.dir or "." + task = Task( + input_files=inputs, + property_file=args.property, + producer_name=args.producer_name or LEGACY_PRODUCER, + producer_version=args.producer_version or "unknown", + base_dir=args.base_dir, + ) + log.info("inputs: %s", inputs) + log.info("output directory: %s", out_dir) + written = write_witnesses(task, values, violation, out_dir, _formats(args.format)) + return 0 if written else 1 + + +def main(argv: Optional[Sequence[str]] = None) -> int: + argv = list(sys.argv[1:] if argv is None else argv) + parser = build_parser() + args = parser.parse_args(_normalize_argv(argv)) + _configure_logging(args.verbose, args.quiet) + if args.command == "events": + return run_events(args) + if args.command == "legacy": + return run_legacy(args) + parser.print_usage(sys.stderr) + return 2 + + +if __name__ == "__main__": # pragma: no cover + sys.exit(main()) diff --git a/src/witnesscreator/columns.py b/src/witnesscreator/columns.py new file mode 100644 index 0000000..a85546c --- /dev/null +++ b/src/witnesscreator/columns.py @@ -0,0 +1,126 @@ +"""Column heuristics over Java source lines. + +Columns are 1-based and count every character (a tab is one column), as the +witness format defines them. The heuristics work on lines whose comments and +string/char literals were blanked out by :func:`mask_non_code`, so a ``nondet(`` +inside a comment or a ``)`` inside a string does not confuse them. +""" + +from __future__ import annotations + +import re +from typing import Optional + +NONDET_CALL = re.compile(r"\bnondet[A-Za-z0-9_]*\s*\(") +ASSERT_KEYWORD = re.compile(r"\bassert\b") +THROW_KEYWORD = re.compile(r"\bthrow\b") + + +def _blank(s: str) -> str: + return "".join(ch if ch in "\r\n" else " " for ch in s) + + +def mask_non_code(text: str) -> str: + """Replaces comments and string/char literals by spaces, keeping every position. + + Line breaks are kept so that line numbers and columns of the result equal those + of the input. Text blocks (``\"\"\"``) and block comments may span lines. + """ + out = [] + i, n = 0, len(text) + while i < n: + c = text[i] + nxt = text[i + 1] if i + 1 < n else "" + if c == "/" and nxt == "/": + j = i + while j < n and text[j] not in "\r\n": + j += 1 + out.append(" " * (j - i)) + i = j + elif c == "/" and nxt == "*": + j = text.find("*/", i + 2) + j = n if j < 0 else j + 2 + out.append(_blank(text[i:j])) + i = j + elif c == '"' and text.startswith('"""', i): + j = text.find('"""', i + 3) + j = n if j < 0 else j + 3 + out.append(_blank(text[i:j])) + i = j + elif c in "\"'": + j = i + 1 + while j < n and text[j] != c and text[j] not in "\r\n": + if text[j] == "\\": + j += 1 + j += 1 + if j < n and text[j] == c: + j += 1 + out.append(_blank(text[i:j])) + i = j + else: + out.append(c) + i += 1 + return "".join(out) + + +def nondet_call_column(line: str, call_index: int) -> Optional[int]: + """The column of the closing parenthesis of the ``call_index``-th ``nondet*(`` call. + + ``line`` should be a masked line (see :func:`mask_non_code`). ``None`` if the + line has no such call or its parentheses are unbalanced. + """ + if line is None or call_index is None or call_index < 0: + return None + matches = list(NONDET_CALL.finditer(line)) + if call_index >= len(matches): + return None + open_paren = matches[call_index].end() - 1 + depth = 0 + for i in range(open_paren, len(line)): + ch = line[i] + if ch == "(": + depth += 1 + elif ch == ")": + depth -= 1 + if depth == 0: + return i + 1 + return None + + +def _is_java_identifier_part(ch: str) -> bool: + return ch.isalnum() or ch in "_$" + + +def _skip_whitespace(line: str, i: int) -> int: + while i < len(line) and line[i].isspace(): + i += 1 + return i + + +def statement_column(line: str, assertion: bool) -> Optional[int]: + """The column of the first character of the violating statement on the line. + + The ``assert`` of a failed assertion, the ``throw`` of an explicit throw, + otherwise the first token that is not a brace or an ``else``. ``line`` should + be a masked line (see :func:`mask_non_code`). + """ + if line is None: + return None + if assertion: + m = ASSERT_KEYWORD.search(line) + if m: + return m.start() + 1 + m = THROW_KEYWORD.search(line) + if m: + return m.start() + 1 + i = _skip_whitespace(line, 0) + while i < len(line): + if line[i] in "{}": + i = _skip_whitespace(line, i + 1) + elif line.startswith("else", i) and ( + i + 4 == len(line) or not _is_java_identifier_part(line[i + 4]) + ): + i = _skip_whitespace(line, i + 4) + else: + break + return i + 1 if i < len(line) else None diff --git a/src/witnesscreator/events.py b/src/witnesscreator/events.py new file mode 100644 index 0000000..bb68911 --- /dev/null +++ b/src/witnesscreator/events.py @@ -0,0 +1,166 @@ +"""The event file: JSON lines carrying the model objects. + +:: + + {"kind": "header", "schema": "witnesscreator-events", "version": 1, "producer": {"name": "SWAT", "version": "svcomp27"}} + {"kind": "nondet_return", "function": "nondetInt", "type": "int", "value": "42", "location": {...}, "bits": null} + {"kind": "violation", "throwable": "java.lang.AssertionError", "frames": [{"class_name": "Main", "source_file": "Main.java", "line": 17}]} + +The ``producer`` of the header is optional. Unknown lines are skipped with a +warning; a later ``violation`` line replaces an earlier one. +""" + +from __future__ import annotations + +import json +import logging +from dataclasses import asdict, dataclass, field +from pathlib import Path +from typing import Any, Dict, Iterable, List, Optional, Union + +from .model import Frame, Location, NondetReturn, Violation + +log = logging.getLogger("witnesscreator") + +SCHEMA = "witnesscreator-events" +VERSION = 1 + + +def header_dict(producer_name: Optional[str] = None, producer_version: Optional[str] = None) -> Dict[str, Any]: + header: Dict[str, Any] = {"kind": "header", "schema": SCHEMA, "version": VERSION} + if producer_name is not None or producer_version is not None: + header["producer"] = {"name": producer_name, "version": producer_version} + return header + + +def nondet_return_to_dict(nr: NondetReturn) -> Dict[str, Any]: + d: Dict[str, Any] = {"kind": "nondet_return"} + d.update(asdict(nr)) + return d + + +def violation_to_dict(v: Violation) -> Dict[str, Any]: + d: Dict[str, Any] = {"kind": "violation"} + d.update(asdict(v)) + return d + + +def _int(value: Any, default: int) -> int: + try: + return int(value) + except (TypeError, ValueError): + return default + + +def _opt_str(value: Any) -> Optional[str]: + return None if value is None else str(value) + + +def location_from_dict(d: Any) -> Location: + if not isinstance(d, dict): + return Location() + column = d.get("column") + return Location( + class_name=_opt_str(d.get("class_name")), + source_file=_opt_str(d.get("source_file")), + line=_int(d.get("line"), 0), + call_index=_int(d.get("call_index"), 0), + file_name=_opt_str(d.get("file_name")), + column=None if column is None else _int(column, 0) or None, + method=_opt_str(d.get("method")), + ) + + +def nondet_return_from_dict(d: Dict[str, Any]) -> NondetReturn: + value = d.get("value") + return NondetReturn( + function=_opt_str(d.get("function")), + type=_opt_str(d.get("type")), + value="" if value is None else (value if isinstance(value, str) else json.dumps(value)), + location=location_from_dict(d.get("location")), + bits=_opt_str(d.get("bits")), + ) + + +def frame_from_dict(d: Any) -> Optional[Frame]: + if not isinstance(d, dict): + return None + return Frame(str(d.get("class_name") or ""), _opt_str(d.get("source_file")), _int(d.get("line"), -1)) + + +def violation_from_dict(d: Dict[str, Any]) -> Violation: + frames = [f for f in (frame_from_dict(x) for x in (d.get("frames") or [])) if f is not None] + return Violation(str(d.get("throwable") or "unknown"), frames) + + +@dataclass +class EventFile: + header: Dict[str, Any] = field(default_factory=dict) + values: List[NondetReturn] = field(default_factory=list) + violation: Optional[Violation] = None + + @property + def producer_name(self) -> Optional[str]: + p = self.header.get("producer") + return _opt_str(p.get("name")) if isinstance(p, dict) else None + + @property + def producer_version(self) -> Optional[str]: + p = self.header.get("producer") + return _opt_str(p.get("version")) if isinstance(p, dict) else None + + +def parse_events(lines: Iterable[str]) -> EventFile: + """Parses event lines leniently: bad lines are logged and skipped.""" + ev = EventFile() + for number, raw in enumerate(lines, 1): + line = raw.strip() + if not line: + continue + try: + d = json.loads(line) + except ValueError as e: + log.warning("Skipping event line %d (%s): %s", number, e, line[:120]) + continue + if not isinstance(d, dict): + log.warning("Skipping event line %d: not an object", number) + continue + kind = d.get("kind") + try: + if kind == "header": + if d.get("schema") != SCHEMA: + log.warning("Unexpected event schema %r (expected %r)", d.get("schema"), SCHEMA) + if _int(d.get("version"), VERSION) > VERSION: + log.warning("Event file version %s is newer than %s", d.get("version"), VERSION) + ev.header = d + elif kind == "nondet_return": + ev.values.append(nondet_return_from_dict(d)) + elif kind == "violation": + if ev.violation is not None: + log.info("Event line %d replaces an earlier violation", number) + ev.violation = violation_from_dict(d) + else: + log.warning("Skipping event line %d of unknown kind %r", number, kind) + except Exception as e: # noqa: BLE001 + log.warning("Skipping event line %d (%s)", number, e) + return ev + + +def read_events(path: Union[str, Path]) -> EventFile: + with open(path, "r", encoding="utf-8", errors="replace") as fh: + return parse_events(fh) + + +def dump_events( + values: Iterable[NondetReturn], + violation: Optional[Violation], + producer_name: Optional[str] = None, + producer_version: Optional[str] = None, +) -> str: + """The event file text for the given objects (header first).""" + out = [json.dumps(header_dict(producer_name, producer_version))] + for nr in values: + out.append(json.dumps(nondet_return_to_dict(nr))) + if violation is not None: + out.append(json.dumps(violation_to_dict(violation))) + return "\n".join(out) + "\n" diff --git a/src/witnesscreator/graphml_writer.py b/src/witnesscreator/graphml_writer.py new file mode 100644 index 0000000..7dbcc77 --- /dev/null +++ b/src/witnesscreator/graphml_writer.py @@ -0,0 +1,122 @@ +"""Emitter for the legacy GraphML violation witness (format 1.0), as wit4java consumes it.""" + +from __future__ import annotations + +from dataclasses import dataclass +from typing import List, Optional + +_XML_ESCAPES = {"&": "&", "<": "<", ">": ">", '"': """} + + +def _xml_char_ok(c: int) -> bool: + return c in (0x9, 0xA, 0xD) or 0x20 <= c <= 0xD7FF or 0xE000 <= c <= 0xFFFD or 0x10000 <= c <= 0x10FFFF + + +def xml_escape(s: str) -> str: + """Escapes markup characters; characters XML 1.0 cannot carry become ``\\uXXXX``.""" + out = [] + for ch in str(s): + esc = _XML_ESCAPES.get(ch) + if esc is not None: + out.append(esc) + elif _xml_char_ok(ord(ch)): + out.append(ch) + else: + out.append(f"\\u{ord(ch):04x}") + return "".join(out) + + +@dataclass +class Assumption: + """One edge of the witness automaton: a value a ``nondet*`` call returned.""" + + origin_file: str + line: int + text: str + scope: str + + +_HEADER = """ + + + <command-line> + + + + + false + + + false + + + false + + + false + + + false + + + 0 + + + 0 + + + + + + + + + + + + + + + + + violation_witness + Java +""" + + +def render_graphml(producer: str, specification: Optional[str], assumptions: List[Assumption]) -> str: + """The witness automaton: a chain of edges, one per assumption, ending in the violation node. + + Without assumptions the automaton is the single entry node that is also the + violation node (the "default violation"). + """ + out = [_HEADER] + out.append(f" {xml_escape(producer)}\n") + if specification: + out.append(f" {xml_escape(specification)}\n") + out.append(' \n') + if not assumptions: + out.append(' \n') + out.append(' true\n') + out.append(' true\n') + out.append(" \n") + else: + last = len(assumptions) + for i in range(last + 1): + out.append(f' \n') + if i == 0: + out.append(' true\n') + if i == last: + out.append(' true\n') + out.append(" \n") + for i, a in enumerate(assumptions): + out.append(f' \n') + out.append(f' {xml_escape(a.origin_file)}\n') + out.append(f' {int(a.line)}\n') + out.append(' 0\n') + out.append(f' {xml_escape(a.text)}\n') + out.append(f' {xml_escape(a.scope)}\n') + out.append(" \n") + out.append(" \n") + out.append("\n") + return "".join(out) diff --git a/src/witnesscreator/literals.py b/src/witnesscreator/literals.py new file mode 100644 index 0000000..c9930a5 --- /dev/null +++ b/src/witnesscreator/literals.py @@ -0,0 +1,209 @@ +"""Rendering of recorded values as Java literals and ``java_expression`` constraints.""" + +from __future__ import annotations + +import re +import struct +from decimal import Decimal, InvalidOperation +from typing import Optional + +from .model import normalize_type + +RESULT = "\\result" + +_INT_RE = re.compile(r"^[+-]?\d+$") +_INT_MIN, _INT_MAX = -(2**31), 2**31 - 1 + +_JAVA_ESCAPES = { + '"': '\\"', + "\\": "\\\\", + "\n": "\\n", + "\r": "\\r", + "\t": "\\t", + "\b": "\\b", + "\f": "\\f", +} + +_CHAR_ESCAPES = { + 0x27: "'\\''", + 0x5C: "'\\\\'", + 0x0A: "'\\n'", + 0x0D: "'\\r'", + 0x09: "'\\t'", + 0x08: "'\\b'", + 0x0C: "'\\f'", +} + + +def result_constraint(value: str, type_name: Optional[str]) -> str: + """The ``java_expression`` satisfied exactly when the call returned ``value``. + + ``type_name`` is a Java type name (``int``, ``String``, ...) or a JVM descriptor + (``I``, ``Ljava/lang/String;``); ``None`` selects the legacy rendering that only + looks at the value (integers and booleans compare with ``==``, everything else is + a string). + """ + value = "" if value is None else str(value) + t = normalize_type(type_name) + if t is None: + return _legacy_constraint(value) + if t == "boolean": + return f"{RESULT} == {'true' if value.strip() == 'true' else 'false'}" + if t in ("byte", "short", "int"): + return f"{RESULT} == {value.strip()}" + if t == "long": + return f"{RESULT} == {long_literal(value)}" + if t == "char": + return f"{RESULT} == {char_literal(value)}" + if t == "float": + return floating_constraint(value, True) + if t == "double": + return floating_constraint(value, False) + return f"{RESULT}.equals({string_literal(value)})" + + +def _legacy_constraint(value: str) -> str: + v = value.strip() + if _INT_RE.match(v) or v in ("true", "false"): + return f"{RESULT} == {v}" + return f"{RESULT}.equals({string_literal(value)})" + + +def long_literal(value: str) -> str: + """``L`` suffix only when the value does not fit into an ``int``.""" + v = value.strip() + try: + n = int(v) + except ValueError: + return v + if _INT_MIN <= n <= _INT_MAX: + return v + return f"{v}L" + + +def char_literal(code_point) -> str: + """Char values are recorded as their code point; renders the Java char literal.""" + try: + c = int(str(code_point).strip()) + except ValueError: + return str(code_point) + if c < 0 or c > 0xFFFF: + return str(code_point) + if c in _CHAR_ESCAPES: + return _CHAR_ESCAPES[c] + if 0x20 <= c < 0x7F: + return f"'{chr(c)}'" + return f"'\\u{c:04x}'" + + +def string_literal(value: str) -> str: + """A Java string literal: every character outside printable ASCII is escaped. + + Characters outside the Basic Multilingual Plane are written as surrogate pairs, + which is how Java sees them. + """ + out = ['"'] + for ch in value: + esc = _JAVA_ESCAPES.get(ch) + if esc is not None: + out.append(esc) + continue + c = ord(ch) + if 0x20 <= c < 0x7F: + out.append(ch) + elif c > 0xFFFF: + c -= 0x10000 + out.append(f"\\u{0xD800 + (c >> 10):04x}\\u{0xDC00 + (c & 0x3FF):04x}") + else: + out.append(f"\\u{c:04x}") + out.append('"') + return "".join(out) + + +def plain_decimal(value: str) -> str: + """``1.0E10`` -> ``10000000000``, ``-0.0`` stays ``-0.0``; unparsable values are kept.""" + v = value.strip() + if v.endswith(("f", "F", "d", "D")) and not v.lower().endswith("infinity"): + v = v[:-1] + negative = v.startswith("-") + body = v[1:] if negative else v + try: + body = format(Decimal(body), "f") + except (InvalidOperation, ValueError): + return v + if body.startswith("-"): # Decimal("-0") style input after sign removal cannot happen, be safe + body = body[1:] + return f"-{body}" if negative else body + + +def floating_constraint(value: str, is_float: bool) -> str: + box = "Float" if is_float else "Double" + v = value.strip() + if v == "NaN": + return f"{box}.isNaN({RESULT})" + if v == "Infinity": + return f"{RESULT} == {box}.POSITIVE_INFINITY" + if v == "-Infinity": + return f"{RESULT} == {box}.NEGATIVE_INFINITY" + literal = plain_decimal(v) + if "." not in literal: + literal += ".0" + return f"{RESULT} == {literal}{'f' if is_float else ''}" + + +def value_from_bits(bits: str, type_name: Optional[str]) -> Optional[str]: + """The Java ``toString`` form of a float/double given its IEEE bits (``0x3dcccccd``).""" + t = normalize_type(type_name) + if t not in ("float", "double"): + return None + try: + n = int(str(bits).strip(), 0) + except ValueError: + return None + try: + if t == "float": + f = struct.unpack(">f", struct.pack(">I", n & 0xFFFFFFFF))[0] + else: + f = struct.unpack(">d", struct.pack(">Q", n & 0xFFFFFFFFFFFFFFFF))[0] + except struct.error: + return None + if f != f: + return "NaN" + if f in (float("inf"), float("-inf")): + return "Infinity" if f > 0 else "-Infinity" + if f == 0.0: + return "-0.0" if str(f).startswith("-") else "0.0" + return repr(f) + + +def graphml_assumption_value(value: str, type_name: Optional[str]) -> str: + """The right-hand side of a GraphML assumption, as wit4java's harness parses it. + + Primitives are plain decimal values that ``Integer.parseInt``/``Float.parseFloat`` + accept (chars as their code point, no ``L``/``f`` suffixes); strings become + ``.equals("")``. + """ + value = "" if value is None else str(value) + t = normalize_type(type_name) + if t is None: + v = value.strip() + if _INT_RE.match(v) or v in ("true", "false"): + return v + return f".equals({string_literal(value)})" + if t == "String": + return f".equals({string_literal(value)})" + if t == "boolean": + return "true" if value.strip() == "true" else "false" + if t == "char": + v = value.strip() + if _INT_RE.match(v): + return v + if len(v) == 1: + return str(ord(v)) + return v + if t in ("float", "double"): + v = value.strip() + if v in ("NaN", "Infinity", "-Infinity"): + return v + return plain_decimal(v) + return value.strip() diff --git a/src/witnesscreator/markers.py b/src/witnesscreator/markers.py new file mode 100644 index 0000000..a0c60d5 --- /dev/null +++ b/src/witnesscreator/markers.py @@ -0,0 +1,152 @@ +"""The legacy ``[WITNESS]`` / ``[WITNESS_TARGET]`` marker lines SWAT printed. + +Each marker is followed by the base64 of its payload: + +* ``[WITNESS]``: ``value@@@line@@@class@@@methodDesc@@@callIndex@@@typeDesc@@@sourceFile`` + (the 4-field form ``value@@@line@@@class@@@methodDesc`` is still accepted); + because a String value may contain the separator, fields are parsed from the end; +* ``[WITNESS_TARGET]``: ``throwable@@@class@@file@@line;class@@file@@line;...`` + (innermost frame first). +""" + +from __future__ import annotations + +import base64 +import binascii +import logging +import re +from typing import Iterable, List, Optional, Tuple + +from .model import Frame, Location, NondetReturn, Violation, normalize_type + +log = logging.getLogger("witnesscreator") + +VALUE_MARKER = "[WITNESS]" +TARGET_MARKER = "[WITNESS_TARGET]" +SEPARATOR = "@@@" +TYPE_DESCRIPTORS = {"Z", "B", "C", "S", "I", "J", "F", "D", "Ljava/lang/String;"} + +_B64_JUNK = re.compile(r"[^A-Za-z0-9+/=_-]") + + +def decode_base64(text: str) -> str: + """Decodes base64 (standard or URL-safe, padding optional) to UTF-8 text.""" + s = _B64_JUNK.sub("", str(text).strip()).replace("-", "+").replace("_", "/") + s += "=" * (-len(s) % 4) + try: + raw = base64.b64decode(s, validate=False) + except (binascii.Error, ValueError) as e: + raise ValueError(f"invalid base64: {e}") from e + return raw.decode("utf-8", errors="replace") + + +def _is_int(s: str) -> bool: + try: + int(s.strip()) + return True + except ValueError: + return False + + +def function_for_type(type_name: Optional[str]) -> Optional[str]: + t = normalize_type(type_name) + if t is None: + return None + return "nondet" + t[0].upper() + t[1:] + + +def parse_value_marker(payload: str) -> NondetReturn: + """Parses the payload of a ``[WITNESS]`` marker (7- or 4-field form).""" + parts = payload.split(SEPARATOR) + n = len(parts) + if n >= 7 and parts[n - 2].strip() in TYPE_DESCRIPTORS and _is_int(parts[n - 3]) and _is_int(parts[n - 6]): + type_desc = parts[n - 2].strip() + return NondetReturn( + function=function_for_type(type_desc), + type=normalize_type(type_desc), + value=SEPARATOR.join(parts[: n - 6]), + location=Location( + class_name=parts[n - 5].strip(), + source_file=parts[n - 1].strip() or None, + line=int(parts[n - 6].strip()), + call_index=int(parts[n - 3].strip()), + method=parts[n - 4].strip() or None, + ), + ) + if n >= 4 and _is_int(parts[n - 3]): + return NondetReturn( + function=None, + type=None, + value=SEPARATOR.join(parts[: n - 3]), + location=Location( + class_name=parts[n - 2].strip(), + source_file=None, + line=int(parts[n - 3].strip()), + call_index=0, + method=parts[n - 1].strip() or None, + ), + ) + raise ValueError(f"invalid witness marker: {payload!r}") + + +def parse_target_marker(payload: str) -> Violation: + """Parses the payload of a ``[WITNESS_TARGET]`` marker.""" + idx = payload.find(SEPARATOR) + if idx < 0: + raise ValueError(f"invalid witness target marker: {payload!r}") + throwable = payload[:idx].strip() + frames: List[Frame] = [] + rest = payload[idx + len(SEPARATOR) :].strip() + if rest: + for frame in rest.split(";"): + fields = frame.split("@@") + if len(fields) != 3: + continue + try: + line = int(fields[2].strip()) + except ValueError: + line = -1 + frames.append(Frame(fields[0].strip(), fields[1].strip() or None, line)) + return Violation(throwable, frames) + + +def parse_marker_lines(lines: Iterable[str]) -> Tuple[List[NondetReturn], Optional[Violation]]: + """Extracts the values and the (last) target from output lines carrying markers. + + Lines without a marker are ignored, so the whole output of a run may be passed. + Undecodable markers are logged and skipped. + """ + values: List[NondetReturn] = [] + violation: Optional[Violation] = None + for raw in lines: + line = str(raw) + idx = line.find(TARGET_MARKER) + if idx >= 0: + try: + violation = parse_target_marker(decode_base64(line[idx + len(TARGET_MARKER) :])) + except ValueError as e: + log.warning("Ignoring bad target marker (%s): %s", e, line.strip()) + continue + idx = line.find(VALUE_MARKER) + if idx >= 0: + try: + values.append(parse_value_marker(decode_base64(line[idx + len(VALUE_MARKER) :]))) + except ValueError as e: + log.warning("Ignoring bad witness marker (%s): %s", e, line.strip()) + return values, violation + + +def parse_markers(text: str) -> Tuple[List[NondetReturn], Optional[Violation]]: + """Like :func:`parse_marker_lines` for a block of text, which may itself be base64.""" + if text is None: + return [], None + if VALUE_MARKER not in text and TARGET_MARKER not in text and text.strip(): + try: + decoded = decode_base64(text) + except ValueError: + decoded = "" + if VALUE_MARKER in decoded or TARGET_MARKER in decoded: + text = decoded + elif decoded.strip(): + log.warning("No witness markers found in the (decoded) input") + return parse_marker_lines(text.splitlines()) diff --git a/src/witnesscreator/model.py b/src/witnesscreator/model.py new file mode 100644 index 0000000..82c4557 --- /dev/null +++ b/src/witnesscreator/model.py @@ -0,0 +1,125 @@ +"""The data model shared by the library, the event file and the command line. + +Every object is a plain dataclass; ``write_witnesses`` never mutates them. +""" + +from __future__ import annotations + +from dataclasses import dataclass, field +from pathlib import Path +from typing import Optional, Sequence, Union + +from ._version import __version__ + +#: Java types of ``Verifier.nondet*()`` results, as spelled in :attr:`NondetReturn.type`. +JAVA_TYPES = ("boolean", "byte", "short", "char", "int", "long", "float", "double", "String") + +_DESCRIPTOR_TO_TYPE = { + "Z": "boolean", + "B": "byte", + "S": "short", + "C": "char", + "I": "int", + "J": "long", + "F": "float", + "D": "double", + "Ljava/lang/String;": "String", + "java.lang.String": "String", + "java/lang/String": "String", + "string": "String", +} + + +def normalize_type(type_name: Optional[str]) -> Optional[str]: + """Maps a Java type name or JVM descriptor to one of :data:`JAVA_TYPES`. + + Returns ``None`` for an unknown or missing type, which selects the legacy + rendering that only looks at the value. + """ + if type_name is None: + return None + t = str(type_name).strip() + if t in JAVA_TYPES: + return t + return _DESCRIPTOR_TO_TYPE.get(t) + + +@dataclass +class Location: + """Where a ``Verifier.nondet*()`` call happened. + + Two forms are accepted: + + * ``Location(class_name="pkg.Main", source_file="Main.java", line=12, call_index=0)``: + the call site is resolved to one of the task's source files and the column is + derived from the source text; + * ``Location(file_name="Main.java", line=12, column=27)``: the producer already + knows the file (one of the task's input files) and, optionally, the column. + + ``method`` optionally names the calling method (``main([Ljava/lang/String;)V``); + it only appears in the GraphML ``assumption.scope``. + """ + + class_name: Optional[str] = None + source_file: Optional[str] = None + line: int = 0 + call_index: int = 0 + file_name: Optional[str] = None + column: Optional[int] = None + method: Optional[str] = None + + +@dataclass +class NondetReturn: + """One value returned by a ``Verifier.nondet*()`` call. + + ``value`` is the string form of the value: integers in decimal, ``char`` as its + code point in decimal, ``boolean`` as ``true``/``false``, ``float``/``double`` as + Java's ``Float.toString``/``Double.toString`` (``NaN``, ``Infinity``, + ``-Infinity``, ``-0.0`` included) and ``String`` as the raw, unescaped string. + """ + + function: Optional[str] + type: Optional[str] + value: str + location: Location + bits: Optional[str] = None + + +@dataclass +class Frame: + """A stack frame of the uncaught throwable, as ``StackTraceElement`` reports it.""" + + class_name: str + source_file: Optional[str] = None + line: int = -1 + + +@dataclass +class Violation: + """The uncaught throwable that ended the violating run, innermost frame first.""" + + throwable: str + frames: list = field(default_factory=list) + + @property + def is_assertion_error(self) -> bool: + return self.throwable == "java.lang.AssertionError" + + +@dataclass +class Task: + """The verification task the witness belongs to. + + ``input_files`` are the files or directories exactly as given to the verifier; + directories are expanded to the ``.java`` files they contain. ``property_file`` + is the ``.prp`` file whose content becomes the witness' specification. + Relative input paths are resolved against ``base_dir`` (default: the current + working directory) but written to the witness as given. + """ + + input_files: Sequence[str] = field(default_factory=list) + property_file: Union[str, Path, None] = None + producer_name: str = "witnesscreator" + producer_version: str = __version__ + base_dir: Union[str, Path, None] = None diff --git a/src/witnesscreator/sources.py b/src/witnesscreator/sources.py new file mode 100644 index 0000000..bf20b18 --- /dev/null +++ b/src/witnesscreator/sources.py @@ -0,0 +1,263 @@ +"""The Java source files of a verification task and the lookup of classes in them.""" + +from __future__ import annotations + +import hashlib +import logging +import os +import re +from pathlib import Path +from typing import Callable, Iterable, List, Optional, Union + +from .columns import mask_non_code + +log = logging.getLogger("witnesscreator") + +_LINE_BREAK = re.compile(r"\r\n|\r|\n") +_PACKAGE_DECL = re.compile(r"^\s*package\s+([A-Za-z_$][\w$]*(?:\s*\.\s*[A-Za-z_$][\w$]*)*)\s*;", re.MULTILINE) +_UNSET = object() + + +def to_slashes(s: str) -> str: + return str(s).replace("\\", "/") + + +def strip_trailing_slash(s: str) -> str: + r = to_slashes(s) + while len(r) > 1 and r.endswith("/"): + r = r[:-1] + return r + + +def split_lines(text: str) -> List[str]: + """Splits on ``\\n``, ``\\r\\n`` and ``\\r`` only (like ``Files.readAllLines``).""" + if text == "": + return [] + lines = _LINE_BREAK.split(text) + if lines and lines[-1] == "": + lines.pop() + return lines + + +class InputFile: + """One ``.java`` file of the task.""" + + def __init__(self, display_path: str, path: Path, relative_path: str): + #: The path as written into the witness: the input as given plus the relative path. + self.display_path = display_path + #: Where the file is read from. + self.path = path + #: Path relative to the input root it was found in, ``/``-separated. + self.relative_path = relative_path + self._lines: Optional[List[str]] = None + self._masked: Optional[List[str]] = None + self._sha256: Optional[str] = None + self._package = _UNSET + + @property + def file_name(self) -> str: + return self.path.name + + def _read(self) -> str: + try: + return self.path.read_bytes().decode("utf-8", errors="replace") + except OSError as e: + log.warning("Could not read %s: %s", self.path, e) + return "" + + @property + def lines(self) -> List[str]: + if self._lines is None: + self._lines = split_lines(self._read()) + return self._lines + + @property + def masked_lines(self) -> List[str]: + """The lines with comments and string/char literals blanked out.""" + if self._masked is None: + self._masked = split_lines(mask_non_code("\n".join(self.lines) + "\n")) + while len(self._masked) < len(self.lines): + self._masked.append("") + return self._masked + + @property + def package(self) -> Optional[str]: + """The declared package (``""`` for the default package), ``None`` if unreadable.""" + if self._package is _UNSET: + if not self.lines: + self._package = None + else: + m = _PACKAGE_DECL.search("\n".join(self.masked_lines)) + self._package = m.group(1) if m else "" + return self._package + + def line(self, number: int) -> Optional[str]: + """The 1-based line, or ``None`` if the file does not have it.""" + if number < 1 or number > len(self.lines): + return None + return self.lines[number - 1] + + def masked_line(self, number: int) -> Optional[str]: + if number < 1 or number > len(self.lines): + return None + return self.masked_lines[number - 1] + + @property + def sha256(self) -> str: + if self._sha256 is None: + try: + self._sha256 = hashlib.sha256(self.path.read_bytes()).hexdigest() + except OSError as e: + log.warning("Could not hash %s: %s", self.path, e) + self._sha256 = "" + return self._sha256 + + def __repr__(self) -> str: + return f"InputFile({self.display_path!r})" + + +class SourceFiles: + """The ``.java`` files of the task, in the order of the inputs.""" + + def __init__(self, files: List[InputFile]): + self.files = list(files) + + def __len__(self) -> int: + return len(self.files) + + def __iter__(self): + return iter(self.files) + + @classmethod + def collect(cls, inputs: Iterable[str], base_dir: Union[str, Path, None] = None) -> "SourceFiles": + """Collects the ``.java`` files of the inputs (files or directories, searched recursively). + + A file reachable through several inputs is listed once. Relative inputs are + resolved against ``base_dir`` but displayed as given. + """ + base = Path(base_dir) if base_dir is not None else None + files: List[InputFile] = [] + seen = set() + for given in inputs: + given = str(given) + if given == "": + continue + root = Path(given) + if base is not None and not root.is_absolute(): + root = base / root + try: + if root.is_dir(): + prefix = strip_trailing_slash(given) + found = [] + for dirpath, dirnames, filenames in os.walk(root): + dirnames.sort() + for name in filenames: + if name.endswith(".java"): + found.append(Path(dirpath) / name) + found.sort(key=lambda p: to_slashes(str(p))) + for p in found: + key = os.path.normpath(os.path.abspath(p)) + if key in seen: + continue + seen.add(key) + rel = to_slashes(str(p.relative_to(root))) + files.append(InputFile(f"{prefix}/{rel}", p, rel)) + elif root.is_file(): + if not root.name.endswith(".java"): + log.info("Ignoring input that is not a Java source: %s", given) + continue + key = os.path.normpath(os.path.abspath(root)) + if key in seen: + continue + seen.add(key) + files.append(InputFile(to_slashes(given), root, root.name)) + else: + log.warning("Ignoring missing input: %s", given) + except OSError as e: + log.warning("Could not read input %s: %s", given, e) + return cls(files) + + def _find(self, predicate: Callable[[InputFile], bool]) -> Optional[InputFile]: + for f in self.files: + if predicate(f): + return f + return None + + def resolve( + self, class_name: str, source_file_name: Optional[str], allow_name_only: bool = True + ) -> Optional[InputFile]: + """Finds the source file of a class. + + ``class_name`` may be JVM internal (``pkg/Outer$Inner``) or dotted + (``pkg.Outer$Inner``); ``source_file_name`` is the class' ``SourceFile`` + attribute, if known. + + Candidates are the files of the expected name; a candidate whose ``package`` + declaration contradicts the class' package is never taken. Among the rest, + the file whose path inside its input matches the package path wins (exact + match first, then as a suffix). A file whose package declaration matches is + accepted regardless of its path; a file whose declaration could not be read + only with ``allow_name_only``. + """ + internal = str(class_name).replace(".", "/") + slash = internal.rfind("/") + pkg_dir = "" if slash < 0 else internal[:slash] + package = pkg_dir.replace("/", ".") + simple = internal if slash < 0 else internal[slash + 1 :] + dollar = simple.find("$") + outer = simple if dollar < 0 else simple[:dollar] + + names: List[str] = [] + if source_file_name: + names.append(to_slashes(source_file_name).rsplit("/", 1)[-1]) + if f"{outer}.java" not in names: + names.append(f"{outer}.java") + + for name in names: + candidates = [f for f in self.files if f.file_name == name and f.package in (package, None)] + if not candidates: + continue + rel = name if not pkg_dir else f"{pkg_dir}/{name}" + for f in candidates: + if f.relative_path == rel: + return f + for f in candidates: + if f.relative_path.endswith("/" + rel): + return f + for f in candidates: + if f.package == package: + return f + if allow_name_only: + return candidates[0] + return None + + def resolve_file_name(self, file_name: str) -> Optional[InputFile]: + """Finds an input file by the path a producer wrote (as given, relative, or by name).""" + name = to_slashes(file_name) + while name.startswith("./"): + name = name[2:] + if not name: + return None + for pred in ( + lambda f: f.display_path == name, + lambda f: f.relative_path == name, + lambda f: f.display_path.endswith("/" + name), + lambda f: f.relative_path.endswith("/" + name), + lambda f: f.file_name == name.rsplit("/", 1)[-1], + ): + match = self._find(pred) + if match is not None: + return match + return None + + +def fallback_file_name(class_name: str, source_file: Optional[str]) -> str: + """The file a class should live in when it was not found among the inputs.""" + internal = str(class_name).replace(".", "/") + slash = internal.rfind("/") + pkg_dir = "" if slash < 0 else internal[: slash + 1] + if source_file: + return pkg_dir + to_slashes(source_file).rsplit("/", 1)[-1] + simple = internal[slash + 1 :] + dollar = simple.find("$") + return pkg_dir + (simple if dollar < 0 else simple[:dollar]) + ".java" diff --git a/src/witnesscreator/witness.py b/src/witnesscreator/witness.py new file mode 100644 index 0000000..7470b8b --- /dev/null +++ b/src/witnesscreator/witness.py @@ -0,0 +1,283 @@ +"""Turns a task, the recorded values and the violation into witness documents.""" + +from __future__ import annotations + +import logging +import uuid +from dataclasses import dataclass, field +from datetime import datetime, timezone +from pathlib import Path +from typing import Dict, Iterable, List, Optional, Sequence, Tuple, Union + +from .columns import nondet_call_column, statement_column +from .graphml_writer import Assumption, render_graphml as _render_graphml +from .literals import graphml_assumption_value, result_constraint, value_from_bits +from .model import Location, NondetReturn, Task, Violation +from .sources import InputFile, SourceFiles, fallback_file_name, to_slashes +from .yaml_writer import Metadata, Waypoint, render_yaml as _render_yaml + +log = logging.getLogger("witnesscreator") + +DEFAULT_SPECIFICATION = "CHECK( init(Main.main()), LTL(G assert) )" +FORMATS = ("yaml", "graphml") +FILE_NAMES = {"yaml": "witness.yml", "graphml": "witness.graphml"} + +#: Stack frames of these packages never are the target: the violating statement is +#: the innermost frame of the task sources that called into them. +SKIPPED_FRAME_PREFIXES = ("java.", "javax.", "jdk.", "sun.", "de.uzl.its.swat.") + + +@dataclass +class BuiltWitness: + """Everything the writers need, computed once for all formats.""" + + metadata: Metadata + waypoints: List[Waypoint] = field(default_factory=list) + assumptions: List[Assumption] = field(default_factory=list) + target: Optional[Waypoint] = None + + @property + def has_target(self) -> bool: + return self.target is not None + + +def read_specification(property_file: Union[str, Path, None], base_dir: Union[str, Path, None] = None) -> str: + """The content of the property file; the default specification if it cannot be read.""" + if property_file is None or str(property_file) == "": + log.warning("No property file given, assuming specification: %s", DEFAULT_SPECIFICATION) + return DEFAULT_SPECIFICATION + path = Path(property_file) + if base_dir is not None and not path.is_absolute(): + path = Path(base_dir) / path + try: + spec = path.read_bytes().decode("utf-8", errors="replace").strip() + except OSError as e: + log.warning("Could not read property file %s: %s", property_file, e) + spec = "" + if spec: + return spec + log.warning("Assuming specification: %s", DEFAULT_SPECIFICATION) + return DEFAULT_SPECIFICATION + + +def _scope(class_name: Optional[str], method: Optional[str], file_name: Optional[str]) -> str: + if class_name: + internal = str(class_name).replace(".", "/") + elif file_name: + internal = to_slashes(file_name).rsplit("/", 1)[-1] + if internal.endswith(".java"): + internal = internal[: -len(".java")] + else: + internal = "" + scope = f"java::L{internal};" + if method: + scope += f".{method}" + return scope + + +class _Builder: + def __init__(self, task: Task, sources: SourceFiles): + self.task = task + self.sources = sources + + def value(self, nr: NondetReturn) -> Tuple[Optional[Waypoint], Optional[Assumption]]: + loc = nr.location if nr.location is not None else Location() + value = nr.value + if (value is None or value == "") and nr.bits: + derived = value_from_bits(nr.bits, nr.type) + if derived is not None: + value = derived + value = "" if value is None else str(value) + try: + line = int(loc.line) + except (TypeError, ValueError): + line = 0 + if line < 1: + log.warning("Ignoring value %r without a valid line: %s", value, loc) + return None, None + + found: Optional[InputFile] = None + if loc.file_name: + found = self.sources.resolve_file_name(loc.file_name) + display = found.display_path if found else to_slashes(loc.file_name) + origin = found.relative_path if found else to_slashes(loc.file_name) + if found is None: + log.warning("%s is not among the input files, using it as given", loc.file_name) + elif loc.class_name: + found = self.sources.resolve(loc.class_name, loc.source_file, allow_name_only=True) + if found is not None: + display = found.display_path + origin = found.relative_path + else: + display = origin = fallback_file_name(loc.class_name, loc.source_file) + log.warning("Could not find the source of %s, using %s", loc.class_name, display) + else: + log.warning("Ignoring value %r without a file or class: %s", value, loc) + return None, None + + column = loc.column + if column is not None: + try: + column = int(column) + except (TypeError, ValueError): + column = None + if column is not None and column < 1: + column = None + if column is None and found is not None: + code = found.masked_line(line) + column = nondet_call_column(code, loc.call_index) if code is not None else None + if column is None: + log.warning( + "Could not locate nondet call %s in %s:%s (%r)", + loc.call_index, display, line, found.line(line), + ) + + constraint = result_constraint(value, nr.type) + waypoint = Waypoint.function_return(constraint, display, line, column) + scope = _scope(loc.class_name, loc.method, display) + rhs = graphml_assumption_value(value, nr.type) + text = f"\\result{rhs};" if rhs.startswith(".equals(") else f"\\result = {rhs};" + return waypoint, Assumption(origin, line, text, scope) + + def target(self, violation: Violation) -> Optional[Waypoint]: + for frame in violation.frames or []: + try: + line = int(frame.line) + except (TypeError, ValueError): + continue + if line < 1: + continue + class_name = str(frame.class_name or "").replace("/", ".") + if not class_name or class_name.startswith(SKIPPED_FRAME_PREFIXES): + continue + found = self.sources.resolve(class_name, frame.source_file, allow_name_only=False) + if found is None: + continue + code = found.masked_line(line) + if code is None: + log.warning("Frame %s:%s is outside of %s", class_name, line, found.path) + continue + column = statement_column(code, violation.is_assertion_error) + return Waypoint.target(found.display_path, line, column) + return None + + +def build_witness(task: Task, values: Iterable[NondetReturn], violation: Optional[Violation]) -> BuiltWitness: + """Resolves locations and renders constraints; never raises for bad values.""" + sources = SourceFiles.collect(task.input_files or [], task.base_dir) + specification = read_specification(task.property_file, task.base_dir) + metadata = Metadata( + uuid=str(uuid.uuid4()), + creation_time=datetime.now(timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ"), + producer_name=str(task.producer_name), + producer_version=str(task.producer_version), + specification=specification, + input_files=[(f.display_path, f.sha256) for f in sources], + ) + built = BuiltWitness(metadata) + builder = _Builder(task, sources) + + for nr in values or []: + try: + waypoint, assumption = builder.value(nr) + except Exception as e: # noqa: BLE001 - a bad value must not lose the witness + log.error("Ignoring value %r: %s", nr, e) + continue + if waypoint is not None: + built.waypoints.append(waypoint) + if assumption is not None: + built.assumptions.append(assumption) + if not built.waypoints: + log.info("No witness values recorded, assuming default violation") + + if violation is not None: + try: + built.target = builder.target(violation) + except Exception as e: # noqa: BLE001 + log.error("Could not resolve the target of %r: %s", violation, e) + if built.target is None: + log.warning( + "No stack frame of %s lies in the task sources, the witness has no target waypoint: %s", + violation.throwable, violation.frames, + ) + else: + built.waypoints.append(built.target) + else: + log.warning("No violation recorded, the witness has no target waypoint") + + for wp in built.waypoints: + log.info("Waypoint: %s", wp) + return built + + +def render_yaml(task: Task, values: Iterable[NondetReturn], violation: Optional[Violation]) -> str: + """The YAML (format 2.3) witness as a string.""" + built = build_witness(task, values, violation) + return _render_yaml(built.metadata, built.waypoints) + + +def render_graphml(task: Task, values: Iterable[NondetReturn], violation: Optional[Violation]) -> str: + """The legacy GraphML witness as a string.""" + built = build_witness(task, values, violation) + return _render_graphml(built.metadata.producer_name, built.metadata.specification, built.assumptions) + + +def _render(built: BuiltWitness, fmt: str) -> str: + if fmt == "yaml": + return _render_yaml(built.metadata, built.waypoints) + if fmt == "graphml": + return _render_graphml(built.metadata.producer_name, built.metadata.specification, built.assumptions) + raise ValueError(f"unknown witness format: {fmt}") + + +def write_witnesses( + task: Task, + values: Iterable[NondetReturn], + violation: Optional[Violation], + out_dir: Union[str, Path] = "output", + formats: Sequence[str] = FORMATS, +) -> Dict[str, Path]: + """Writes ``witness.yml`` and/or ``witness.graphml`` into ``out_dir``. + + Never raises for bad data: problems are logged (logger ``witnesscreator``) and + each format is written independently. Returns the files actually written, by + format. + """ + written: Dict[str, Path] = {} + wanted = [f for f in (formats or ()) if f in FORMATS] + for f in formats or (): + if f not in FORMATS: + log.error("Unknown witness format %r (known: %s)", f, ", ".join(FORMATS)) + if not wanted: + return written + + values = list(values or []) + try: + built = build_witness(task, values, violation) + except Exception as e: # noqa: BLE001 - last line of defence + log.error("Could not build the witness, writing a witness without waypoints: %s", e) + metadata = Metadata( + uuid=str(uuid.uuid4()), + creation_time=datetime.now(timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ"), + producer_name=str(getattr(task, "producer_name", "unknown")), + producer_version=str(getattr(task, "producer_version", "unknown")), + specification=DEFAULT_SPECIFICATION, + input_files=[], + ) + built = BuiltWitness(metadata) + + out = Path(out_dir) + try: + out.mkdir(parents=True, exist_ok=True) + except OSError as e: + log.error("Could not create output directory %s: %s", out, e) + for fmt in wanted: + path = out / FILE_NAMES[fmt] + try: + text = _render(built, fmt) + log.info("Writing violation witness to file: %s", path) + path.write_text(text, encoding="utf-8", newline="\n") + written[fmt] = path + except Exception as e: # noqa: BLE001 + log.error("Could not write %s witness to %s: %s", fmt, path, e) + return written diff --git a/src/witnesscreator/yaml_writer.py b/src/witnesscreator/yaml_writer.py new file mode 100644 index 0000000..226ed94 --- /dev/null +++ b/src/witnesscreator/yaml_writer.py @@ -0,0 +1,126 @@ +"""Hand-written emitter for violation witnesses in the YAML format, version 2.3.""" + +from __future__ import annotations + +from dataclasses import dataclass +from typing import List, Optional, Sequence, Tuple + +FORMAT_VERSION = "2.3" + +_YAML_ESCAPES = { + '"': '\\"', + "\\": "\\\\", + "\n": "\\n", + "\r": "\\r", + "\t": "\\t", + "\x85": "\\N", + "
": "\\L", + "
": "\\P", +} + + +def yaml_quote(s: str) -> str: + """Renders a YAML double-quoted scalar. + + Everything outside printable ASCII is escaped (``\\uXXXX``, ``\\UXXXXXXXX`` for + characters beyond the BMP), so the output is plain ASCII that every YAML parser + decodes to the same string, including control characters and lone surrogates. + """ + out = ['"'] + for ch in str(s): + esc = _YAML_ESCAPES.get(ch) + if esc is not None: + out.append(esc) + continue + c = ord(ch) + if 0x20 <= c < 0x7F: + out.append(ch) + elif c > 0xFFFF: + out.append(f"\\U{c:08x}") + else: + out.append(f"\\u{c:04x}") + out.append('"') + return "".join(out) + + +@dataclass +class Waypoint: + """A ``follow`` waypoint of the single violation sequence.""" + + type: str + constraint: Optional[str] + file_name: str + line: int + column: Optional[int] = None + + @classmethod + def function_return(cls, constraint: str, file_name: str, line: int, column: Optional[int]): + return cls("function_return", constraint, file_name, line, column) + + @classmethod + def target(cls, file_name: str, line: int, column: Optional[int]): + return cls("target", None, file_name, line, column) + + def __str__(self) -> str: + s = f"{self.type} @ {self.file_name}:{self.line}" + if self.column is not None: + s += f":{self.column}" + if self.constraint is not None: + s += f" [{self.constraint}]" + return s + + +@dataclass +class Metadata: + uuid: str + creation_time: str + producer_name: str + producer_version: str + specification: str + input_files: Sequence[Tuple[str, str]] # (display path, sha256) + + +def render_yaml(metadata: Metadata, waypoints: List[Waypoint]) -> str: + """The witness document: one ``violation_sequence`` entry, one segment per waypoint.""" + q = yaml_quote + out = [] + out.append('- entry_type: "violation_sequence"\n') + out.append(" metadata:\n") + out.append(f" format_version: {q(FORMAT_VERSION)}\n") + out.append(f" uuid: {q(metadata.uuid)}\n") + out.append(f" creation_time: {q(metadata.creation_time)}\n") + out.append(" producer:\n") + out.append(f" name: {q(metadata.producer_name)}\n") + out.append(f" version: {q(metadata.producer_version)}\n") + out.append(" task:\n") + if not metadata.input_files: + out.append(" input_files: []\n") + out.append(" input_file_hashes: {}\n") + else: + out.append(" input_files:\n") + for path, _ in metadata.input_files: + out.append(f" - {q(path)}\n") + out.append(" input_file_hashes:\n") + for path, sha in metadata.input_files: + out.append(f" {q(path)}: {q(sha)}\n") + out.append(f" specification: {q(metadata.specification)}\n") + out.append(' language: "Java"\n') + if not waypoints: + out.append(" content: []\n") + return "".join(out) + out.append(" content:\n") + for wp in waypoints: + out.append(" - segment:\n") + out.append(" - waypoint:\n") + out.append(f" type: {q(wp.type)}\n") + out.append(' action: "follow"\n') + if wp.constraint is not None: + out.append(" constraint:\n") + out.append(f" value: {q(wp.constraint)}\n") + out.append(' format: "java_expression"\n') + out.append(" location:\n") + out.append(f" file_name: {q(wp.file_name)}\n") + out.append(f" line: {int(wp.line)}\n") + if wp.column is not None: + out.append(f" column: {int(wp.column)}\n") + return "".join(out) diff --git a/tests/conftest.py b/tests/conftest.py new file mode 100644 index 0000000..ee04bc0 --- /dev/null +++ b/tests/conftest.py @@ -0,0 +1,122 @@ +import os +import shutil +import subprocess +import sys +import xml.etree.ElementTree as ET +from pathlib import Path + +import pytest +import yaml + +FIXTURES = Path(__file__).resolve().parent / "fixtures" +GRAPHML_NS = "{http://graphml.graphdrawing.org/xmlns}" + +# WitnessLint: a command prefix in $WITNESSLINT (e.g. "python3 /path/lint/witnesslinter.py"), +# or the developer's local installation. +_LOCAL_LINT = Path("/home/nils/dev/sv-comp-validators") +_LOCAL_LINT_CMD = [str(_LOCAL_LINT / "venv/bin/python"), str(_LOCAL_LINT / "witnesslint-2.3/lint/witnesslinter.py")] + + +def witnesslint_command(): + env = os.environ.get("WITNESSLINT") + if env: + return env.split() + if all(Path(p).exists() for p in _LOCAL_LINT_CMD): + return _LOCAL_LINT_CMD + return None + + +@pytest.fixture(scope="session") +def fixtures(): + return FIXTURES + + +@pytest.fixture +def witnesslint(): + """Runs WitnessLint on a YAML witness; skips the test when the linter is unavailable.""" + cmd = witnesslint_command() + if cmd is None: + pytest.skip("WitnessLint not available (set $WITNESSLINT)") + + def run(witness: Path, *programs: Path) -> str: + p = subprocess.run( + cmd + ["--expectViolationWitness", "--expectedWitnessVersion", "2", "--witness", str(witness)] + + [str(x) for x in programs], + capture_output=True, text=True, timeout=300, + ) + out = p.stdout + p.stderr + assert p.returncode == 0 and "finished with exit code 0" in out, out + return out + + return run + + +def load_yaml(path: Path): + """Parses the witness with PyYAML and checks the basic 2.3 structure.""" + doc = yaml.safe_load(path.read_text(encoding="utf-8")) + assert isinstance(doc, list) and len(doc) == 1 + entry = doc[0] + assert entry["entry_type"] == "violation_sequence" + md = entry["metadata"] + assert md["format_version"] == "2.3" + assert md["task"]["language"] == "Java" + assert "data_model" not in md["task"] + assert set(md["task"]["input_file_hashes"]) == set(md["task"]["input_files"]) + for seg in entry["content"]: + wps = seg["segment"] + assert len(wps) == 1 + wp = wps[0]["waypoint"] + assert wp["action"] == "follow" + assert wp["location"]["line"] >= 1 + assert wp["location"]["file_name"] in md["task"]["input_files"], wp + if "column" in wp["location"]: + assert wp["location"]["column"] >= 1 + if wp["type"] == "function_return": + assert wp["constraint"]["format"] == "java_expression" + else: + assert wp["type"] == "target" and "constraint" not in wp + return entry + + +def waypoints(entry): + return [seg["segment"][0]["waypoint"] for seg in entry["content"]] + + +def assert_single_final_target(entry): + """Exactly one target waypoint, and it is the last segment (WitnessLint does not check this).""" + wps = waypoints(entry) + targets = [i for i, wp in enumerate(wps) if wp["type"] == "target"] + assert targets == [len(wps) - 1], [wp["type"] for wp in wps] + + +def load_graphml(path: Path): + root = ET.parse(path).getroot() + graph = root.find(GRAPHML_NS + "graph") + data = {d.get("key"): d.text for d in graph.findall(GRAPHML_NS + "data")} + nodes = {n.get("id"): {d.get("key"): d.text for d in n.findall(GRAPHML_NS + "data")} for n in graph.findall(GRAPHML_NS + "node")} + edges = [] + for e in graph.findall(GRAPHML_NS + "edge"): + d = {x.get("key"): x.text for x in e.findall(GRAPHML_NS + "data")} + d["source"], d["target"] = e.get("source"), e.get("target") + edges.append(d) + return data, nodes, edges + + +def cli(*args, cwd=None): + """Runs the command line interface in a subprocess.""" + return subprocess.run( + [sys.executable, "-m", "witnesscreator", *map(str, args)], + capture_output=True, text=True, cwd=cwd, + ) + + +@pytest.fixture +def task_dir(tmp_path): + """A copy of a fixture task directory (so tests may write next to it).""" + + def copy(name: str) -> Path: + dst = tmp_path / Path(name).name + shutil.copytree(FIXTURES / name, dst) + return dst + + return copy diff --git a/tests/fixtures/MinePump/spec1-5_product25/Actions.java b/tests/fixtures/MinePump/spec1-5_product25/Actions.java new file mode 100644 index 0000000..0aa65e8 --- /dev/null +++ b/tests/fixtures/MinePump/spec1-5_product25/Actions.java @@ -0,0 +1,140 @@ +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +// +// SPDX-FileCopyrightText: 2011-2013 Alexander von Rhein, University of Passau +// SPDX-FileCopyrightText: 2011-2021 The SV-Benchmarks Community +// +// SPDX-License-Identifier: Apache-2.0 + +import MinePumpSystem.Environment; +import MinePumpSystem.MinePump; + +public class Actions { + + Environment env; + MinePump p; + + boolean methAndRunningLastTime = false; + boolean switchedOnBeforeTS = false; + + Actions() { + env = new Environment(); + p = new MinePump(env); + } + + void waterRise() { + env.waterRise(); + } + + void methaneChange() { + env.changeMethaneLevel(); + } + + void stopSystem() { + if (p.isSystemActive()) p.stopSystem(); + } + + void startSystem() { + if (!p.isSystemActive()) p.startSystem(); + } + + void timeShift() { + + if (p.isSystemActive()) Specification5_1(); + + p.timeShift(); + + if (p.isSystemActive()) { + Specification1(); + Specification2(); + Specification3(); + Specification4(); + Specification5_2(); + } + } + + String getSystemState() { + return p.toString(); + } + + // Specification 1 methan is Critical and pumping leads to Error + void Specification1() { + + Environment e = p.getEnv(); + + boolean b1 = e.isMethaneLevelCritical(); + boolean b2 = p.isPumpRunning(); + + if (b1 && b2) { + assert false; + } + } + + // Specification 2: When the pump is running, and there is methane, then it is + // in switched off at most 1 timesteps. + void Specification2() { + + Environment e = p.getEnv(); + + boolean b1 = e.isMethaneLevelCritical(); + boolean b2 = p.isPumpRunning(); + + if (b1 && b2) { + if (methAndRunningLastTime) { + assert false; + } else { + methAndRunningLastTime = true; + } + } else { + methAndRunningLastTime = false; + } + } + + // Specification 3: When the water is high and there is no methane, then the + // pump is on. + void Specification3() { + + Environment e = p.getEnv(); + + boolean b1 = e.isMethaneLevelCritical(); + boolean b2 = p.isPumpRunning(); + boolean b3 = e.getWaterLevel() == Environment.WaterLevelEnum.high; + + if (!b1 && b3 && !b2) { + assert false; + } + } + + // Specification 4: the pump is never on when the water level is low + void Specification4() { + + Environment e = p.getEnv(); + + boolean b2 = p.isPumpRunning(); + boolean b3 = e.getWaterLevel() == Environment.WaterLevelEnum.low; + + if (b3 && b2) { + assert false; + } + } + + // Specification 5: The Pump is never switched on when the water is below the + // highWater sensor. + void Specification5_1() { + switchedOnBeforeTS = p.isPumpRunning(); + } + + // Specification 5: The Pump is never switched on when the water is below the + // highWater sensor. + void Specification5_2() { + + Environment e = p.getEnv(); + + boolean b1 = p.isPumpRunning(); + boolean b2 = e.getWaterLevel() != Environment.WaterLevelEnum.high; + + if ((b2) && (b1 && !switchedOnBeforeTS)) { + assert false; + } + } +} diff --git a/tests/fixtures/MinePump/spec1-5_product25/Main.java b/tests/fixtures/MinePump/spec1-5_product25/Main.java new file mode 100644 index 0000000..7fce6cf --- /dev/null +++ b/tests/fixtures/MinePump/spec1-5_product25/Main.java @@ -0,0 +1,57 @@ +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +// +// SPDX-FileCopyrightText: 2011-2013 Alexander von Rhein, University of Passau +// SPDX-FileCopyrightText: 2011-2021 The SV-Benchmarks Community +// +// SPDX-License-Identifier: Apache-2.0 + +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + + private static int cleanupTimeShifts = 2; + + public static void main(String[] args) { + randomSequenceOfActions(3); + } + + public static boolean getBoolean() { + return Verifier.nondetBoolean(); + } + + public static void randomSequenceOfActions(int maxLength) { + Actions a = new Actions(); + + int counter = 0; + while (counter < maxLength) { + counter++; + + boolean action1 = getBoolean(); + boolean action2 = getBoolean(); + boolean action3 = getBoolean(); + boolean action4 = false; + if (!action3) action4 = getBoolean(); + + if (action1) { + a.waterRise(); + } + + if (action2) { + a.methaneChange(); + } + + if (action3) { + a.startSystem(); + } else if (action4) { + a.stopSystem(); + } + + a.timeShift(); + } + + for (counter = 0; counter < cleanupTimeShifts; counter++) { + a.timeShift(); + } + } +} diff --git a/tests/fixtures/MinePump/spec1-5_product25/MinePumpSystem/Environment.java b/tests/fixtures/MinePump/spec1-5_product25/MinePumpSystem/Environment.java new file mode 100644 index 0000000..ca33523 --- /dev/null +++ b/tests/fixtures/MinePump/spec1-5_product25/MinePumpSystem/Environment.java @@ -0,0 +1,65 @@ +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +// +// SPDX-FileCopyrightText: 2011-2013 Alexander von Rhein, University of Passau +// SPDX-FileCopyrightText: 2011-2021 The SV-Benchmarks Community +// +// SPDX-License-Identifier: Apache-2.0 + +package MinePumpSystem; + +public class Environment { + + public enum WaterLevelEnum { + low, + normal, + high + } + + private WaterLevelEnum waterLevel = WaterLevelEnum.normal; + + private boolean methaneLevelCritical = false; + + void lowerWaterLevel() { + switch (waterLevel) { + case high: + waterLevel = WaterLevelEnum.normal; + break; + case normal: + waterLevel = WaterLevelEnum.low; + break; + } + } + + public void waterRise() { + switch (waterLevel) { + case low: + waterLevel = WaterLevelEnum.normal; + break; + case normal: + waterLevel = WaterLevelEnum.high; + break; + } + } + + public void changeMethaneLevel() { + methaneLevelCritical = !methaneLevelCritical; + } + + public boolean isMethaneLevelCritical() { + return methaneLevelCritical; + } + + @Override + public String toString() { + return "Env(Water:" + waterLevel + ",Meth:" + (methaneLevelCritical ? "CRIT" : "OK") + ")"; + } + + public WaterLevelEnum getWaterLevel() { + return waterLevel; + } + + boolean isLowWaterSensorDry() { + return waterLevel == WaterLevelEnum.low; + } +} diff --git a/tests/fixtures/MinePump/spec1-5_product25/MinePumpSystem/MinePump.java b/tests/fixtures/MinePump/spec1-5_product25/MinePumpSystem/MinePump.java new file mode 100644 index 0000000..087f984 --- /dev/null +++ b/tests/fixtures/MinePump/spec1-5_product25/MinePumpSystem/MinePump.java @@ -0,0 +1,92 @@ +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +// +// SPDX-FileCopyrightText: 2011-2013 Alexander von Rhein, University of Passau +// SPDX-FileCopyrightText: 2011-2021 The SV-Benchmarks Community +// +// SPDX-License-Identifier: Apache-2.0 + +package MinePumpSystem; + +public class MinePump { + + boolean pumpRunning = false; + + boolean systemActive = true; + + Environment env; + + public MinePump(Environment env) { + super(); + this.env = env; + } + + public void timeShift() { + if (pumpRunning) env.lowerWaterLevel(); + if (systemActive) processEnvironment(); + } + + private void processEnvironment__wrappee__base() {} + + public void processEnvironment() { + if (pumpRunning && isLowWaterLevel()) { + deactivatePump(); + } else { + processEnvironment__wrappee__base(); + } + } + + private void activatePump__wrappee__lowWaterSensor() { + pumpRunning = true; + } + + void activatePump() { + if (!isMethaneAlarm()) { + activatePump__wrappee__lowWaterSensor(); + } else { + // System.out.println("Pump not activated due to methane alarm"); + } + } + + public boolean isPumpRunning() { + return pumpRunning; + } + + void deactivatePump() { + pumpRunning = false; + } + + boolean isMethaneAlarm() { + return env.isMethaneLevelCritical(); + } + + @Override + public String toString() { + return "Pump(System:" + + (systemActive ? "On" : "Off") + + ",Pump:" + + (pumpRunning ? "On" : "Off") + + ") " + + env.toString(); + } + + public Environment getEnv() { + return env; + } + + boolean isLowWaterLevel() { + return !env.isLowWaterSensorDry(); + } + + public void stopSystem() { + // feature not present + } + + public void startSystem() { + // feature not present + } + + public boolean isSystemActive() { + return systemActive; + } +} diff --git a/tests/fixtures/README.md b/tests/fixtures/README.md new file mode 100644 index 0000000..915ac08 --- /dev/null +++ b/tests/fixtures/README.md @@ -0,0 +1,14 @@ +# Test fixtures + +Small verification tasks used by the golden tests. They are copies of files from +the [SV-Benchmarks](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks) and +[sv-witnesses](https://gitlab.com/sosy-lab/benchmarking/sv-witnesses) repositories +and keep their original license headers: + +| Directory | Origin | License | +|---|---|---| +| `common/`, `properties/`, `MinePump/` | sv-benchmarks `java/` | Apache-2.0 (SPDX headers in the files) | +| `jbmc-regression/` | sv-benchmarks `java/jbmc-regression` | 4-clause BSD, see `jbmc-regression/LICENSE` | +| `jdart-regression/` | sv-benchmarks `java/jdart-regression` | MIT, see `jdart-regression/LICENSE-MIT` | +| `sv-witnesses/` | sv-witnesses `examples/java` (the GDart example witness and its task) | Apache-2.0, see `sv-witnesses/LICENSE.Apache-2.0.txt` | +| `synthetic/` | written for these tests | same license as this repository | diff --git a/tests/fixtures/common/org/sosy_lab/sv_benchmarks/Verifier.java b/tests/fixtures/common/org/sosy_lab/sv_benchmarks/Verifier.java new file mode 100644 index 0000000..8769f84 --- /dev/null +++ b/tests/fixtures/common/org/sosy_lab/sv_benchmarks/Verifier.java @@ -0,0 +1,101 @@ +// 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-2025 The SV-Benchmarks Community +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.sv_benchmarks; + +import java.util.Random; + +/** + * This class provides an interface between the benchmarks and the verification tools for + * + *
    + *
  • defining assumptions + *
  • generating nondeterministic values + *
+ * + * The verification semantics of the methods is defined in the method documentations below. The + * bodies of the methods are only approximate to allow execution, but do NOT define the verification + * semantics. + * + *

Also see java/README.md + */ +public final class Verifier { + /** + * Assume that the given condition holds true. Any execution that does not satisfy the condition + * cannot proceed. + * + * @param condition The assumption + */ + public static void assume(boolean condition) { + if (!condition) { + Runtime.getRuntime().halt(1); + } + } + + /** @return A nondeterministically chosen Boolean value (true or false) */ + public static boolean nondetBoolean() { + return new Random().nextBoolean(); + } + + /** @return A nondeterministicly chosen 8-bit signed integer value */ + public static byte nondetByte() { + return (byte) (new Random().nextInt()); + } + + /** @return A nondeterministicly chosen 16-bit unsigned integer value */ + public static char nondetChar() { + return (char) (new Random().nextInt()); + } + + /** @return A nondeterministicly chosen 16-bit signed integer value */ + public static short nondetShort() { + return (short) (new Random().nextInt()); + } + + /** @return A nondeterministicly chosen 32-bit signed integer value */ + public static int nondetInt() { + return new Random().nextInt(); + } + + /** @return A nondeterministicly chosen 64-bit signed integer value */ + public static long nondetLong() { + return new Random().nextLong(); + } + + /** @return A nondeterministicly chosen 32-bit IEEE 754 single-precision floating point value */ + public static float nondetFloat() { + return new Random().nextFloat(); + } + + /** @return A nondeterministicly chosen 64-bit IEEE 754 double-precision floating point value */ + public static double nondetDouble() { + return new Random().nextDouble(); + } + + /** + * @return A non-null character string of nondeterministically chosen length (in range + * [0,2147483647]) and consisting of nondeterministically chosen characters. + */ + 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); + } + + /** + * @return An object of given type chosen by the given factory implementation. + * @implnote For nondeterministic choice, the factory implementation must use the nondet methods + * above. + */ + public static T nondetObject(Class type, ObjectFactory factory) { + return factory.createObject(); + } +} diff --git a/tests/fixtures/jbmc-regression/LICENSE b/tests/fixtures/jbmc-regression/LICENSE new file mode 100644 index 0000000..50673cf --- /dev/null +++ b/tests/fixtures/jbmc-regression/LICENSE @@ -0,0 +1,39 @@ +(C) 2001-2016, Daniel Kroening, Edmund Clarke, +Computer Science Department, University of Oxford +Computer Science Department, Carnegie Mellon University + +All rights reserved. Redistribution and use in source and binary forms, with +or without modification, are permitted provided that the following +conditions are met: + + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + 2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + 3. All advertising materials mentioning features or use of this software + must display the following acknowledgement: + + This product includes software developed by Daniel Kroening, + Edmund Clarke, + Computer Science Department, University of Oxford + Computer Science Department, Carnegie Mellon University + + 4. Neither the name of the University nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE +LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR +CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF +SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS +INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN +CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. diff --git a/tests/fixtures/jbmc-regression/StringValueOf08/Main.java b/tests/fixtures/jbmc-regression/StringValueOf08/Main.java new file mode 100644 index 0000000..3bb0344 --- /dev/null +++ b/tests/fixtures/jbmc-regression/StringValueOf08/Main.java @@ -0,0 +1,18 @@ +/* + * Origin of the benchmark: + * license: 4-clause BSD (see /java/jbmc-regression/LICENSE) + * repo: https://github.com/diffblue/cbmc.git + * branch: develop + * directory: regression/jbmc-strings/StringValueOf08 + * The benchmark was taken from the repo: 24 January 2018 + */ +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + public static void main(String[] args) { + String arg = Verifier.nondetString(); + float floatValue = Float.parseFloat(arg); + String tmp = String.valueOf(floatValue); + assert tmp.equals("2.50"); + } +} diff --git a/tests/fixtures/jbmc-regression/exceptions16/Main.java b/tests/fixtures/jbmc-regression/exceptions16/Main.java new file mode 100644 index 0000000..87aa147 --- /dev/null +++ b/tests/fixtures/jbmc-regression/exceptions16/Main.java @@ -0,0 +1,32 @@ +/* + * Origin of the benchmark: + * license: 4-clause BSD (see /java/jbmc-regression/LICENSE) + * repo: https://github.com/diffblue/cbmc.git + * branch: develop + * directory: regression/cbmc-java/exceptions16 + * The benchmark was taken from the repo: 24 January 2018 + */ +import org.sosy_lab.sv_benchmarks.Verifier; + +class A extends RuntimeException {} + +class B extends A {} + +class C extends B {} + +public class Main { + public static void main(String[] args) { + int x = Verifier.nondetInt(); + try { + x++; + } catch (A exc) { + assert false; + } + + try { + throw new B(); + } catch (B exc) { + assert false; + } + } +} diff --git a/tests/fixtures/jbmc-regression/return2/Main.java b/tests/fixtures/jbmc-regression/return2/Main.java new file mode 100644 index 0000000..e6c7a8b --- /dev/null +++ b/tests/fixtures/jbmc-regression/return2/Main.java @@ -0,0 +1,17 @@ +/* + * Origin of the benchmark: + * license: 4-clause BSD (see /java/jbmc-regression/LICENSE) + * repo: https://github.com/diffblue/cbmc.git + * branch: develop + * directory: regression/cbmc-java/return2 + * The benchmark was taken from the repo: 24 January 2018 + */ +import org.sosy_lab.sv_benchmarks.Verifier; + +class Main { + public static void main(String[] args) { + int v1 = Verifier.nondetInt(); + int v2 = Verifier.nondetInt(); + assert v1 == v2; // should be able to fail + } +} diff --git a/tests/fixtures/jdart-regression/LICENSE-MIT b/tests/fixtures/jdart-regression/LICENSE-MIT new file mode 100644 index 0000000..8c2aebe --- /dev/null +++ b/tests/fixtures/jdart-regression/LICENSE-MIT @@ -0,0 +1,21 @@ +The MIT License (MIT) + +Copyright (c) 2020 TU Dortmund, Falk Howar and Malte Mues + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/tests/fixtures/jdart-regression/float/Main.java b/tests/fixtures/jdart-regression/float/Main.java new file mode 100644 index 0000000..80783f3 --- /dev/null +++ b/tests/fixtures/jdart-regression/float/Main.java @@ -0,0 +1,16 @@ +/* + * Contributed to SV-COMP by Falk Howar + * License: MIT (see /java/jdart-regression/LICENSE-MIT) + * + */ + +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + + public static void main(String[] args) { + float a = Verifier.nondetFloat(); + float b = Verifier.nondetFloat(); + assert (a + b != a || b == 0.0); + } +} diff --git a/tests/fixtures/properties/no-runtime-exception.prp b/tests/fixtures/properties/no-runtime-exception.prp new file mode 100644 index 0000000..55b5c59 --- /dev/null +++ b/tests/fixtures/properties/no-runtime-exception.prp @@ -0,0 +1 @@ +CHECK(init(Main.main()), LTL(G ! uncaught(java.lang.RuntimeException))) diff --git a/tests/fixtures/properties/no-runtime-exception.prp.license b/tests/fixtures/properties/no-runtime-exception.prp.license new file mode 100644 index 0000000..b76c19f --- /dev/null +++ b/tests/fixtures/properties/no-runtime-exception.prp.license @@ -0,0 +1,6 @@ +This file is part of the SV-Benchmarks collection of verification tasks: +https://github.com/sosy-lab/sv-benchmarks + +SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community + +SPDX-License-Identifier: Apache-2.0 diff --git a/tests/fixtures/properties/valid-assert.prp b/tests/fixtures/properties/valid-assert.prp new file mode 100644 index 0000000..a9d5a52 --- /dev/null +++ b/tests/fixtures/properties/valid-assert.prp @@ -0,0 +1 @@ +CHECK( init(Main.main()), LTL(G assert) ) diff --git a/tests/fixtures/properties/valid-assert.prp.license b/tests/fixtures/properties/valid-assert.prp.license new file mode 100644 index 0000000..5a43e6b --- /dev/null +++ b/tests/fixtures/properties/valid-assert.prp.license @@ -0,0 +1,6 @@ +This file is part of the SV-Benchmarks collection of verification tasks: +https://github.com/sosy-lab/sv-benchmarks + +SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community + +SPDX-License-Identifier: Apache-2.0 \ No newline at end of file diff --git a/tests/fixtures/sv-witnesses/ExDarko_false.witness-2.3.yml b/tests/fixtures/sv-witnesses/ExDarko_false.witness-2.3.yml new file mode 100644 index 0000000..3633213 --- /dev/null +++ b/tests/fixtures/sv-witnesses/ExDarko_false.witness-2.3.yml @@ -0,0 +1,55 @@ +# This file is part of the SV-Witnesses repository as regression test: +# https://gitlab.com/sosy-lab/benchmarking/sv-witnesses +# +# SPDX-FileCopyrightText: 2026 The SV-Witnesses Community +# +# SPDX-License-Identifier: Apache-2.0 +--- +- entry_type: "violation_sequence" + metadata: + creation_time: "2026-09-08T17:36:11Z" + format_version: "2.3" + producer: + name: "GDart" + version: "VERSION_PLACEHOLDER" + task: + input_file_hashes: + ./java/common/org/sosy_lab/sv_benchmarks/Verifier.java: "d544c9e74f86b4ed8e692b7b7bcb00ec3901e19f5b0d4740b49e5c3c672031ba" + ./java/jpf-regression/ExDarko_false/Main.java: "44faed0b4c09127009615aa7c0699fb1acda5235fdcd1bbcbea867661d450d82" + input_files: + - "./java/common/org/sosy_lab/sv_benchmarks/Verifier.java" + - "./java/jpf-regression/ExDarko_false/Main.java" + language: "Java" + specification: "CHECK( init(Main.main()), LTL(G assert) )" + uuid: "be742527-8e82-4418-9ba2-6cbb857e25a7" + content: + - segment: + - waypoint: + type: "function_return" + action: "follow" + constraint: + value: "\\result == 0" + format: "java_expression" + location: + file_name: "./java/jpf-regression/ExDarko_false/Main.java" + line: 34 + column: 43 + - segment: + - waypoint: + type: "function_return" + action: "follow" + constraint: + value: "\\result == 0" + format: "java_expression" + location: + file_name: "./java/jpf-regression/ExDarko_false/Main.java" + line: 35 + column: 41 + - segment: + - waypoint: + type: "target" + action: "follow" + location: + file_name: "./java/jpf-regression/ExDarko_false/Main.java" + line: 48 + column: 12 diff --git a/tests/fixtures/sv-witnesses/LICENSE.Apache-2.0.txt b/tests/fixtures/sv-witnesses/LICENSE.Apache-2.0.txt new file mode 100644 index 0000000..4ed90b9 --- /dev/null +++ b/tests/fixtures/sv-witnesses/LICENSE.Apache-2.0.txt @@ -0,0 +1,208 @@ +Apache License + +Version 2.0, January 2004 + +http://www.apache.org/licenses/ TERMS AND CONDITIONS FOR USE, REPRODUCTION, +AND DISTRIBUTION + + 1. Definitions. + + + +"License" shall mean the terms and conditions for use, reproduction, and distribution +as defined by Sections 1 through 9 of this document. + + + +"Licensor" shall mean the copyright owner or entity authorized by the copyright +owner that is granting the License. + + + +"Legal Entity" shall mean the union of the acting entity and all other entities +that control, are controlled by, or are under common control with that entity. +For the purposes of this definition, "control" means (i) the power, direct +or indirect, to cause the direction or management of such entity, whether +by contract or otherwise, or (ii) ownership of fifty percent (50%) or more +of the outstanding shares, or (iii) beneficial ownership of such entity. + + + +"You" (or "Your") shall mean an individual or Legal Entity exercising permissions +granted by this License. + + + +"Source" form shall mean the preferred form for making modifications, including +but not limited to software source code, documentation source, and configuration +files. + + + +"Object" form shall mean any form resulting from mechanical transformation +or translation of a Source form, including but not limited to compiled object +code, generated documentation, and conversions to other media types. + + + +"Work" shall mean the work of authorship, whether in Source or Object form, +made available under the License, as indicated by a copyright notice that +is included in or attached to the work (an example is provided in the Appendix +below). + + + +"Derivative Works" shall mean any work, whether in Source or Object form, +that is based on (or derived from) the Work and for which the editorial revisions, +annotations, elaborations, or other modifications represent, as a whole, an +original work of authorship. For the purposes of this License, Derivative +Works shall not include works that remain separable from, or merely link (or +bind by name) to the interfaces of, the Work and Derivative Works thereof. + + + +"Contribution" shall mean any work of authorship, including the original version +of the Work and any modifications or additions to that Work or Derivative +Works thereof, that is intentionally submitted to Licensor for inclusion in +the Work by the copyright owner or by an individual or Legal Entity authorized +to submit on behalf of the copyright owner. For the purposes of this definition, +"submitted" means any form of electronic, verbal, or written communication +sent to the Licensor or its representatives, including but not limited to +communication on electronic mailing lists, source code control systems, and +issue tracking systems that are managed by, or on behalf of, the Licensor +for the purpose of discussing and improving the Work, but excluding communication +that is conspicuously marked or otherwise designated in writing by the copyright +owner as "Not a Contribution." + + + +"Contributor" shall mean Licensor and any individual or Legal Entity on behalf +of whom a Contribution has been received by Licensor and subsequently incorporated +within the Work. + +2. Grant of Copyright License. Subject to the terms and conditions of this +License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, +no-charge, royalty-free, irrevocable copyright license to reproduce, prepare +Derivative Works of, publicly display, publicly perform, sublicense, and distribute +the Work and such Derivative Works in Source or Object form. + +3. Grant of Patent License. Subject to the terms and conditions of this License, +each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, +no-charge, royalty-free, irrevocable (except as stated in this section) patent +license to make, have made, use, offer to sell, sell, import, and otherwise +transfer the Work, where such license applies only to those patent claims +licensable by such Contributor that are necessarily infringed by their Contribution(s) +alone or by combination of their Contribution(s) with the Work to which such +Contribution(s) was submitted. If You institute patent litigation against +any entity (including a cross-claim or counterclaim in a lawsuit) alleging +that the Work or a Contribution incorporated within the Work constitutes direct +or contributory patent infringement, then any patent licenses granted to You +under this License for that Work shall terminate as of the date such litigation +is filed. + +4. Redistribution. You may reproduce and distribute copies of the Work or +Derivative Works thereof in any medium, with or without modifications, and +in Source or Object form, provided that You meet the following conditions: + +(a) You must give any other recipients of the Work or Derivative Works a copy +of this License; and + +(b) You must cause any modified files to carry prominent notices stating that +You changed the files; and + +(c) You must retain, in the Source form of any Derivative Works that You distribute, +all copyright, patent, trademark, and attribution notices from the Source +form of the Work, excluding those notices that do not pertain to any part +of the Derivative Works; and + +(d) If the Work includes a "NOTICE" text file as part of its distribution, +then any Derivative Works that You distribute must include a readable copy +of the attribution notices contained within such NOTICE file, excluding those +notices that do not pertain to any part of the Derivative Works, in at least +one of the following places: within a NOTICE text file distributed as part +of the Derivative Works; within the Source form or documentation, if provided +along with the Derivative Works; or, within a display generated by the Derivative +Works, if and wherever such third-party notices normally appear. The contents +of the NOTICE file are for informational purposes only and do not modify the +License. You may add Your own attribution notices within Derivative Works +that You distribute, alongside or as an addendum to the NOTICE text from the +Work, provided that such additional attribution notices cannot be construed +as modifying the License. + +You may add Your own copyright statement to Your modifications and may provide +additional or different license terms and conditions for use, reproduction, +or distribution of Your modifications, or for any such Derivative Works as +a whole, provided Your use, reproduction, and distribution of the Work otherwise +complies with the conditions stated in this License. + +5. Submission of Contributions. Unless You explicitly state otherwise, any +Contribution intentionally submitted for inclusion in the Work by You to the +Licensor shall be under the terms and conditions of this License, without +any additional terms or conditions. Notwithstanding the above, nothing herein +shall supersede or modify the terms of any separate license agreement you +may have executed with Licensor regarding such Contributions. + +6. Trademarks. This License does not grant permission to use the trade names, +trademarks, service marks, or product names of the Licensor, except as required +for reasonable and customary use in describing the origin of the Work and +reproducing the content of the NOTICE file. + +7. Disclaimer of Warranty. Unless required by applicable law or agreed to +in writing, Licensor provides the Work (and each Contributor provides its +Contributions) on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +KIND, either express or implied, including, without limitation, any warranties +or conditions of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR +A PARTICULAR PURPOSE. You are solely responsible for determining the appropriateness +of using or redistributing the Work and assume any risks associated with Your +exercise of permissions under this License. + +8. Limitation of Liability. In no event and under no legal theory, whether +in tort (including negligence), contract, or otherwise, unless required by +applicable law (such as deliberate and grossly negligent acts) or agreed to +in writing, shall any Contributor be liable to You for damages, including +any direct, indirect, special, incidental, or consequential damages of any +character arising as a result of this License or out of the use or inability +to use the Work (including but not limited to damages for loss of goodwill, +work stoppage, computer failure or malfunction, or any and all other commercial +damages or losses), even if such Contributor has been advised of the possibility +of such damages. + +9. Accepting Warranty or Additional Liability. While redistributing the Work +or Derivative Works thereof, You may choose to offer, and charge a fee for, +acceptance of support, warranty, indemnity, or other liability obligations +and/or rights consistent with this License. However, in accepting such obligations, +You may act only on Your own behalf and on Your sole responsibility, not on +behalf of any other Contributor, and only if You agree to indemnify, defend, +and hold each Contributor harmless for any liability incurred by, or claims +asserted against, such Contributor by reason of your accepting any such warranty +or additional liability. END OF TERMS AND CONDITIONS + +APPENDIX: How to apply the Apache License to your work. + +To apply the Apache License to your work, attach the following boilerplate +notice, with the fields enclosed by brackets "[]" replaced with your own identifying +information. (Don't include the brackets!) The text should be enclosed in +the appropriate comment syntax for the file format. We also recommend that +a file or class name and description of purpose be included on the same "printed +page" as the copyright notice for easier identification within third-party +archives. + +Copyright [yyyy] [name of copyright owner] + +Licensed under the Apache License, Version 2.0 (the "License"); + +you may not use this file except in compliance with the License. + +You may obtain a copy of the License at + +http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software + +distributed under the License is distributed on an "AS IS" BASIS, + +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + +See the License for the specific language governing permissions and + +limitations under the License. diff --git a/tests/fixtures/sv-witnesses/java/common/org/sosy_lab/sv_benchmarks/Verifier.java b/tests/fixtures/sv-witnesses/java/common/org/sosy_lab/sv_benchmarks/Verifier.java new file mode 100644 index 0000000..e0ff042 --- /dev/null +++ b/tests/fixtures/sv-witnesses/java/common/org/sosy_lab/sv_benchmarks/Verifier.java @@ -0,0 +1,92 @@ +// 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-2025 The SV-Benchmarks Community +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.sv_benchmarks; + +import java.util.Random; + +/** + * This class provides an interface between the benchmarks and the verification tools for + * + *

    + *
  • defining assumptions + *
  • generating nondeterministic values + *
+ * + * The verification semantics of the methods is defined in the method documentations below. The + * bodies of the methods are only approximate to allow execution, but do NOT define the verification + * semantics. + * + *

Also see java/README.md + */ +public final class Verifier { + /** + * Assume that the given condition holds true. Any execution that does not satisfy the condition + * cannot proceed. + * + * @param condition The assumption + */ + public static void assume(boolean condition) { + if (!condition) { + Runtime.getRuntime().halt(1); + } + } + + /** @return A nondeterministically chosen Boolean value (true or false) */ + public static boolean nondetBoolean() { + return new Random().nextBoolean(); + } + + /** @return A nondeterministicly chosen 8-bit signed integer value */ + public static byte nondetByte() { + return (byte) (new Random().nextInt()); + } + + /** @return A nondeterministicly chosen 16-bit unsigned integer value */ + public static char nondetChar() { + return (char) (new Random().nextInt()); + } + + /** @return A nondeterministicly chosen 16-bit signed integer value */ + public static short nondetShort() { + return (short) (new Random().nextInt()); + } + + /** @return A nondeterministicly chosen 32-bit signed integer value */ + public static int nondetInt() { + return new Random().nextInt(); + } + + /** @return A nondeterministicly chosen 64-bit signed integer value */ + public static long nondetLong() { + return new Random().nextLong(); + } + + /** @return A nondeterministicly chosen 32-bit IEEE 754 single-precision floating point value */ + public static float nondetFloat() { + return new Random().nextFloat(); + } + + /** @return A nondeterministicly chosen 64-bit IEEE 754 double-precision floating point value */ + public static double nondetDouble() { + return new Random().nextDouble(); + } + + /** + * @return A non-null character string of nondeterministically chosen length (in range + * [0,2147483647]) and consisting of nondeterministically chosen characters. + */ + 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/tests/fixtures/sv-witnesses/java/jpf-regression/ExDarko_false/Main.java b/tests/fixtures/sv-witnesses/java/jpf-regression/ExDarko_false/Main.java new file mode 100644 index 0000000..d07247a --- /dev/null +++ b/tests/fixtures/sv-witnesses/java/jpf-regression/ExDarko_false/Main.java @@ -0,0 +1,76 @@ +/* + * Origin of the benchmark: + * repo: https://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc + * branch: updated-spf + * root directory: src/tests/gov/nasa/jpf/symbc + * The benchmark was taken from the repo: 24 January 2018 + */ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * Symbolic Pathfinder (jpf-symbc) is licensed under the Apache License, + * Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + * SPDX-FileCopyrightText: Copyright (C) 2014, United States Government, as represented by the Administrator of the National Aeronautics and Space Administration. All rights reserved. + * SPDX-License-Identifier: Apache-2.0 + */ + +// package gov.nasa.jpf.symbc; +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + + public static void main(String[] args) { + new Main().unboxed(Verifier.nondetInt(), 2); + new Main().boxed(Verifier.nondetInt(), 2); + new Main().customBoxed(Verifier.nondetInt(), 2); + } + + private void unboxed(int i, int j) { + if (i == j) { + System.out.println("HIT"); + } + } + + private void boxed(int i, int j) { + if (new Integer(i).equals(new Integer(j))) { + System.out.println("HIT"); + } else assert false; + } + + private void customBoxed(int i, int j) { + if (new MyInteger(i).equals(new MyInteger(j))) { + System.out.println("HIT"); + } + } +} + +class MyInteger { + int value; + + public MyInteger(int value) { + this.value = value; + } + + @Override + public boolean equals(Object obj) { + if (obj == this) { + return true; + } + if (!(obj instanceof MyInteger)) { + return false; + } + MyInteger other = (MyInteger) obj; + return this.value == other.value; + } +} diff --git a/tests/fixtures/synthetic/Main.java b/tests/fixtures/synthetic/Main.java new file mode 100644 index 0000000..319d5e2 --- /dev/null +++ b/tests/fixtures/synthetic/Main.java @@ -0,0 +1,31 @@ +import org.sosy_lab.sv_benchmarks.Verifier; +import pkg.Helper; + +public class Main { + static class Inner { + int pick() { + // Verifier.nondetInt() in a comment + String s = "Verifier.nondetInt()"; // and in a string literal + return Verifier.nondetInt() + Verifier.nondetInt(); // two calls, one line + } + } + + public static void main(String[] args) { + char c = Verifier.nondetChar(); + double d = Verifier.nondetDouble(); + float f = Verifier.nondetFloat(); + long l = Verifier.nondetLong(); + String s = Verifier.nondetString(); + int sum = new Inner().pick(); + if (Helper.check(sum) && Companion.flag() && s.length() > 0) { + throw new IllegalStateException("boom"); + } + assert false; + } +} + +class Companion { + static boolean flag() { + return Verifier.nondetBoolean(); + } +} diff --git a/tests/fixtures/synthetic/pkg/Helper.java b/tests/fixtures/synthetic/pkg/Helper.java new file mode 100644 index 0000000..42d0216 --- /dev/null +++ b/tests/fixtures/synthetic/pkg/Helper.java @@ -0,0 +1,9 @@ +package pkg; + +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Helper { + public static boolean check(int x) { + return x > Verifier.nondetInt(); + } +} diff --git a/tests/test_cli.py b/tests/test_cli.py new file mode 100644 index 0000000..344d0b0 --- /dev/null +++ b/tests/test_cli.py @@ -0,0 +1,212 @@ +import base64 +import shutil + +import yaml + +from conftest import cli, load_graphml, load_yaml, waypoints +from witnesscreator import Frame, Location, NondetReturn, Violation, dump_events +from witnesscreator.cli import main + + +def b64(s: str) -> str: + return base64.b64encode(s.encode()).decode() + + +def marker(kind: str, payload: str) -> str: + return f"prefix {kind} {b64(payload)}" + + +def write_task(dir_): + dir_.mkdir(parents=True, exist_ok=True) + (dir_ / "Main.java").write_text( + "import org.sosy_lab.sv_benchmarks.Verifier;\n" + "public class Main {\n" + " public static void main(String[] args) {\n" + " int x = Verifier.nondetInt();\n" + " String s = Verifier.nondetString();\n" + " if (x == 3 && s.equals(\"a\\\"b\")) {\n" + " assert false;\n" + " }\n" + " }\n" + "}\n" + ) + prp = dir_.parent / "valid-assert.prp" + prp.write_text("CHECK( init(Main.main()), LTL(G assert) )\n") + return prp + + +MARKERS = "\n".join([ + marker("[WITNESS]", "3@@@4@@@Main@@@main([Ljava/lang/String;)V@@@0@@@I@@@Main.java"), + marker("[WITNESS]", "a\"b@@@5@@@Main@@@main([Ljava/lang/String;)V@@@0@@@Ljava/lang/String;@@@Main.java"), + marker("[WITNESS_TARGET]", "java.lang.AssertionError@@@Main@@Main.java@@7"), +]) + + +def check_witness(out, task): + entry = load_yaml(out / "witness.yml") + wps = waypoints(entry) + assert [wp["type"] for wp in wps] == ["function_return", "function_return", "target"] + assert wps[0]["constraint"]["value"] == "\\result == 3" + assert wps[0]["location"] == {"file_name": f"{task}/Main.java", "line": 4, "column": 32} + assert wps[1]["constraint"]["value"] == '\\result.equals("a\\"b")' + assert wps[1]["location"]["column"] == 38 + assert wps[2]["location"] == {"file_name": f"{task}/Main.java", "line": 7, "column": 7} + _, nodes, edges = load_graphml(out / "witness.graphml") + assert [e["assumption"] for e in edges] == ["\\result = 3;", '\\result.equals("a\\"b");'] + assert edges[0]["assumption.scope"] == "java::LMain;.main([Ljava/lang/String;)V" + assert edges[0]["originfile"] == "Main.java" + assert nodes["n2"] == {"violation": "true"} + + +def test_java_compatible_command_line(tmp_path): + task = tmp_path / "task" + prp = write_task(task) + out = tmp_path / "out" + p = cli(b64(MARKERS), "--input", task, "--property", prp, "--out", out, "--producer-version", "test") + assert p.returncode == 0, p.stderr + entry = load_yaml(out / "witness.yml") + assert entry["metadata"]["producer"] == {"name": "SWAT", "version": "test"} + assert entry["metadata"]["task"]["specification"] == "CHECK( init(Main.main()), LTL(G assert) )" + check_witness(out, task) + assert "Writing violation witness" in p.stderr + + +def test_legacy_positional_dir(tmp_path): + task = tmp_path / "task" + write_task(task) + assert main([b64(MARKERS), str(task)]) == 0 + check_witness(task, task) + entry = load_yaml(task / "witness.yml") + assert entry["metadata"]["producer"] == {"name": "SWAT", "version": "unknown"} + assert entry["metadata"]["task"]["specification"] == "CHECK( init(Main.main()), LTL(G assert) )" + + +def test_legacy_subcommand_with_markers_file(tmp_path): + task = tmp_path / "task" + prp = write_task(task) + markers = tmp_path / "markers.txt" + markers.write_text(MARKERS + "\n") + out = tmp_path / "out" + assert main(["legacy", "--markers-file", str(markers), "--input", str(task), "--property", str(prp), + "--out-dir", str(out), "--producer-name", "Other", "--producer-version", "1"]) == 0 + check_witness(out, task) + assert load_yaml(out / "witness.yml")["metadata"]["producer"] == {"name": "Other", "version": "1"} + # the file may hold the base64 blob as well + markers.write_text(b64(MARKERS)) + out2 = tmp_path / "out2" + assert main(["legacy", "--markers-file", str(markers), "--input", str(task), "--out-dir", str(out2), "--format", "yaml"]) == 0 + assert (out2 / "witness.yml").exists() and not (out2 / "witness.graphml").exists() + + +def test_legacy_empty_markers_write_default_violation(tmp_path): + task = tmp_path / "task" + write_task(task) + out = tmp_path / "out" + p = cli("", "--input", task, "--out", out) + assert p.returncode == 0, p.stderr + entry = load_yaml(out / "witness.yml") + assert entry["content"] == [] + _, nodes, edges = load_graphml(out / "witness.graphml") + assert nodes["n0"] == {"entry": "true", "violation": "true"} and edges == [] + # a target alone yields a single final target segment + p = cli(b64(marker("[WITNESS_TARGET]", "java.lang.AssertionError@@@Main@@Main.java@@7")), "--input", task, "--out", out) + assert p.returncode == 0 + wps = waypoints(load_yaml(out / "witness.yml")) + assert len(wps) == 1 and wps[0]["type"] == "target" and wps[0]["location"]["column"] == 7 + + +def test_legacy_four_field_markers(tmp_path): + (tmp_path / "Main.java").write_text("class Main {\n int x = Verifier.nondetInt();\n}\n") + markers = marker("[WITNESS]", "1@@@2@@@Main@@@()V") + assert main([b64(markers), str(tmp_path)]) == 0 + wps = waypoints(load_yaml(tmp_path / "witness.yml")) + assert wps[0]["constraint"]["value"] == "\\result == 1" + assert wps[0]["location"]["line"] == 2 and wps[0]["location"]["column"] == 30 + text = (tmp_path / "witness.graphml").read_text() + assert "<init>" in text + _, _, edges = load_graphml(tmp_path / "witness.graphml") + assert edges[0]["assumption.scope"] == "java::LMain;.()V" + + +def test_events_command(tmp_path): + task = tmp_path / "task" + prp = write_task(task) + values = [ + NondetReturn("nondetInt", "int", "3", Location(class_name="Main", source_file="Main.java", line=4, call_index=0, method="main([Ljava/lang/String;)V")), + NondetReturn("nondetString", "String", 'a"b', Location(file_name=f"{task}/Main.java", line=5, column=38)), + ] + violation = Violation("java.lang.AssertionError", [Frame("Main", "Main.java", 7)]) + events = tmp_path / "events.jsonl" + events.write_text(dump_events(values, violation, "SWAT", "svcomp27")) + out = tmp_path / "out" + p = cli("events", "--events", events, "--property", prp, "--input", task, "--out-dir", out) + assert p.returncode == 0, p.stderr + entry = load_yaml(out / "witness.yml") + assert entry["metadata"]["producer"] == {"name": "SWAT", "version": "svcomp27"} + wps = waypoints(entry) + assert wps[0]["location"]["column"] == 32 and wps[1]["location"]["column"] == 38 + assert wps[2]["type"] == "target" + _, _, edges = load_graphml(out / "witness.graphml") + assert edges[0]["assumption.scope"] == "java::LMain;.main([Ljava/lang/String;)V" + assert edges[1]["assumption.scope"] == "java::LMain;" + # command line overrides the header + p = cli("events", "--events", events, "--property", prp, "--input", task, "--out-dir", out, + "--producer-name", "X", "--producer-version", "Y", "--format", "graphml") + assert p.returncode == 0 + data, _, _ = load_graphml(out / "witness.graphml") + assert data["producer"] == "X" + + +def test_events_missing_file_still_writes(tmp_path): + task = tmp_path / "task" + write_task(task) + out = tmp_path / "out" + p = cli("events", "--events", tmp_path / "nope.jsonl", "--input", task, "--out-dir", out) + assert p.returncode == 0 + assert "Could not read event file" in p.stderr + assert load_yaml(out / "witness.yml")["content"] == [] + assert "No property file given" in p.stderr + + +def test_usage_errors(tmp_path): + assert cli().returncode == 2 + assert cli("events").returncode == 2 + assert cli("legacy", "--format", "xml").returncode == 2 + p = cli("--version") + assert p.returncode == 0 and "witnesscreator" in p.stdout + assert cli("--help").returncode == 0 + assert cli("legacy", "--help").returncode == 0 + + +def test_nothing_written_is_exit_1(tmp_path): + blocker = tmp_path / "file" + blocker.write_text("not a directory") + p = cli("", "--out", blocker / "out") + assert p.returncode == 1 + assert "Could not" in p.stderr + + +def test_quiet_and_verbose(tmp_path): + task = tmp_path / "task" + write_task(task) + p = cli("-q", "legacy", b64(MARKERS), str(task)) + assert p.returncode == 0 and "INFO" not in p.stderr + p = cli("-v", "legacy", b64(MARKERS), str(task)) + assert p.returncode == 0 and "INFO" in p.stderr + + +def test_pyz_build_and_run(tmp_path): + import subprocess + import sys + from pathlib import Path + + tool = Path(__file__).resolve().parent.parent / "tools" / "build_pyz.py" + pyz = tmp_path / "witnesscreator.pyz" + assert subprocess.run([sys.executable, str(tool), str(pyz)], capture_output=True).returncode == 0 + task = tmp_path / "task" + write_task(task) + p = subprocess.run([sys.executable, str(pyz), b64(MARKERS), str(task)], capture_output=True, text=True) + assert p.returncode == 0, p.stderr + check_witness(task, task) + p = subprocess.run([sys.executable, str(pyz), "--version"], capture_output=True, text=True) + assert p.stdout.startswith("witnesscreator ") diff --git a/tests/test_e2e.py b/tests/test_e2e.py new file mode 100644 index 0000000..eb023c8 --- /dev/null +++ b/tests/test_e2e.py @@ -0,0 +1,319 @@ +"""Golden end-to-end tests on real SV-COMP tasks (see fixtures/README.md).""" + +import logging + +import pytest +import yaml + +from conftest import FIXTURES, assert_single_final_target, load_graphml, load_yaml, waypoints +from witnesscreator import Frame, Location, NondetReturn, Task, Violation, parse_markers, write_witnesses +from witnesscreator import witness as witness_module + +COMMON = FIXTURES / "common" +PROPS = FIXTURES / "properties" +VALID_ASSERT = PROPS / "valid-assert.prp" +NO_RUNTIME_EXCEPTION = PROPS / "no-runtime-exception.prp" + + +def task_for(task_dir, prp=VALID_ASSERT, **kw): + return Task(input_files=[str(COMMON), str(task_dir)], property_file=str(prp), + producer_name="test", producer_version="0", **kw) + + +def write(task, values, violation, out, **kw): + paths = write_witnesses(task, values, violation, out, **kw) + assert set(paths) == {"yaml", "graphml"} + assert paths["yaml"].read_text(encoding="utf-8").isascii() + return load_yaml(paths["yaml"]), load_graphml(paths["graphml"]) + + +def test_gdart_example_matches_official_witness(tmp_path, witnesslint): + """The sv-witnesses example (produced by GDart) for jpf-regression/ExDarko_false.""" + base = FIXTURES / "sv-witnesses" + inputs = ["./java/common/org/sosy_lab/sv_benchmarks/Verifier.java", "./java/jpf-regression/ExDarko_false/Main.java"] + task = Task(input_files=inputs, property_file=str(VALID_ASSERT), producer_name="GDart", + producer_version="VERSION_PLACEHOLDER", base_dir=base) + main = Location(class_name="Main", source_file="Main.java", line=34, call_index=0) + values = [ + NondetReturn("nondetInt", "int", "0", main), + NondetReturn("nondetInt", "int", "0", Location(class_name="Main", source_file="Main.java", line=35, call_index=0)), + ] + violation = Violation("java.lang.AssertionError", [Frame("Main", "Main.java", 48), Frame("Main", "Main.java", 35)]) + paths = write_witnesses(task, values, violation, tmp_path) + ours = load_yaml(paths["yaml"]) + official = yaml.safe_load((base / "ExDarko_false.witness-2.3.yml").read_text(encoding="utf-8"))[0] + assert ours["content"] == official["content"] + assert ours["metadata"]["task"] == official["metadata"]["task"] + assert ours["metadata"]["producer"] == official["metadata"]["producer"] + assert_single_final_target(ours) + witnesslint(paths["yaml"], base / "java" / "common", base / "java" / "jpf-regression" / "ExDarko_false") + + +def test_return2_from_markers(tmp_path, witnesslint): + """jbmc-regression/return2 with the markers SWAT printed for it.""" + task_dir = FIXTURES / "jbmc-regression" / "return2" + values, violation = parse_markers( + "[WITNESS] LTFAQEAxM0BAQE1haW5AQEBtYWluKFtMamF2YS9sYW5nL1N0cmluZzspVkBAQDBAQEBJQEBATWFpbi5qYXZh\n" + "[WITNESS] MEBAQDE0QEBATWFpbkBAQG1haW4oW0xqYXZhL2xhbmcvU3RyaW5nOylWQEBAMEBAQElAQEBNYWluLmphdmE=\n" + "[WITNESS_TARGET] amF2YS5sYW5nLkFzc2VydGlvbkVycm9yQEBATWFpbkBATWFpbi5qYXZhQEAxNQ==\n" + ) + entry, (data, nodes, edges) = write(task_for(task_dir), values, violation, tmp_path) + md = entry["metadata"]["task"] + assert md["input_files"] == [f"{COMMON}/org/sosy_lab/sv_benchmarks/Verifier.java", f"{task_dir}/Main.java"] + assert md["specification"] == "CHECK( init(Main.main()), LTL(G assert) )" + wps = waypoints(entry) + assert [(wp["type"], wp["location"]["line"], wp["location"]["column"]) for wp in wps] == [ + ("function_return", 13, 33), ("function_return", 14, 33), ("target", 15, 5)] + assert [wp["constraint"]["value"] for wp in wps[:2]] == ["\\result == -1", "\\result == 0"] + assert_single_final_target(entry) + assert data["producer"] == "test" and data["sourcecodelang"] == "Java" + assert [(e["originfile"], e["startline"], e["assumption"], e["assumption.scope"]) for e in edges] == [ + ("Main.java", "13", "\\result = -1;", "java::LMain;.main([Ljava/lang/String;)V"), + ("Main.java", "14", "\\result = 0;", "java::LMain;.main([Ljava/lang/String;)V"), + ] + assert nodes["n0"] == {"entry": "true"} and nodes["n2"] == {"violation": "true"} + witnesslint(tmp_path / "witness.yml", COMMON, task_dir) + + +def test_float_special_values(tmp_path, witnesslint): + """jdart-regression/float: NaN, infinities and negative zero.""" + task_dir = FIXTURES / "jdart-regression" / "float" + loc = lambda line: Location(class_name="Main", source_file="Main.java", line=line, call_index=0, method="main([Ljava/lang/String;)V") + values = [ + NondetReturn("nondetFloat", "float", "-Infinity", loc(12)), + NondetReturn("nondetFloat", "float", "NaN", loc(13)), + NondetReturn("nondetFloat", "float", "-0.0", loc(12)), + NondetReturn("nondetFloat", "float", "Infinity", loc(13)), + NondetReturn("nondetFloat", "float", "1.0E10", loc(12)), + NondetReturn("nondetFloat", "F", "-0.0012512209359556437", loc(13)), + NondetReturn("nondetFloat", "float", "", loc(12), bits="0x3dcccccd"), + ] + violation = Violation("java.lang.AssertionError", [Frame("Main", "Main.java", 14)]) + entry, (_, _, edges) = write(task_for(task_dir), values, violation, tmp_path) + wps = waypoints(entry) + assert [wp["constraint"]["value"] for wp in wps[:-1]] == [ + "\\result == Float.NEGATIVE_INFINITY", "Float.isNaN(\\result)", "\\result == -0.0f", + "\\result == Float.POSITIVE_INFINITY", "\\result == 10000000000.0f", "\\result == -0.0012512209359556437f", + "\\result == 0.10000000149011612f", + ] + assert all(wp["location"]["column"] == 36 for wp in wps[:-1]) + assert wps[-1]["location"] == {"file_name": f"{task_dir}/Main.java", "line": 14, "column": 5} + assert [e["assumption"] for e in edges] == [ + "\\result = -Infinity;", "\\result = NaN;", "\\result = -0.0;", "\\result = Infinity;", + "\\result = 10000000000;", "\\result = -0.0012512209359556437;", "\\result = 0.10000000149011612;", + ] + assert_single_final_target(entry) + witnesslint(tmp_path / "witness.yml", COMMON, task_dir) + + +def test_string_value_and_runtime_exception_thrown_in_jdk(tmp_path, witnesslint): + """jbmc-regression/StringValueOf08: the NumberFormatException is thrown inside the JDK, + the target is the innermost frame of the task sources.""" + task_dir = FIXTURES / "jbmc-regression" / "StringValueOf08" + values = [NondetReturn("nondetString", "String", "fixed", Location(class_name="Main", source_file="Main.java", line=13, call_index=0))] + violation = Violation("java.lang.NumberFormatException", [ + Frame("jdk.internal.math.FloatingDecimal", "FloatingDecimal.java", 2054), + Frame("jdk.internal.math.FloatingDecimal", "FloatingDecimal.java", 122), + Frame("java.lang.Float", "Float.java", 476), + Frame("Main", "Main.java", 14), + ]) + entry, (_, _, edges) = write(task_for(task_dir, NO_RUNTIME_EXCEPTION), values, violation, tmp_path) + assert entry["metadata"]["task"]["specification"] == "CHECK(init(Main.main()), LTL(G ! uncaught(java.lang.RuntimeException)))" + wps = waypoints(entry) + assert wps[0]["constraint"]["value"] == '\\result.equals("fixed")' + assert wps[0]["location"]["column"] == 40 + assert wps[1] == {"type": "target", "action": "follow", "location": {"file_name": f"{task_dir}/Main.java", "line": 14, "column": 5}} + assert edges[0]["assumption"] == '\\result.equals("fixed");' + assert_single_final_target(entry) + witnesslint(tmp_path / "witness.yml", COMMON, task_dir) + + +def test_multi_file_task_with_package(tmp_path, witnesslint): + """MinePump/spec1-5_product25: several files, a package directory, the assertion fails in Actions.java.""" + task_dir = FIXTURES / "MinePump" / "spec1-5_product25" + loc = Location(class_name="Main", source_file="Main.java", line=20, call_index=0, method="getBoolean()Z") + values = [NondetReturn("nondetBoolean", "boolean", v, loc) for v in ("false", "true", "false")] + violation = Violation("java.lang.AssertionError", [ + Frame("Actions", "Actions.java", 104), Frame("Actions", "Actions.java", 50), Frame("Main", "Main.java", 50), Frame("Main", "Main.java", 16)]) + entry, (_, _, edges) = write(task_for(task_dir), values, violation, tmp_path) + files = entry["metadata"]["task"]["input_files"] + assert files == [ + f"{COMMON}/org/sosy_lab/sv_benchmarks/Verifier.java", + f"{task_dir}/Actions.java", f"{task_dir}/Main.java", + f"{task_dir}/MinePumpSystem/Environment.java", f"{task_dir}/MinePumpSystem/MinePump.java", + ] + wps = waypoints(entry) + assert [wp["constraint"]["value"] for wp in wps[:3]] == ["\\result == false", "\\result == true", "\\result == false"] + assert all(wp["location"] == {"file_name": f"{task_dir}/Main.java", "line": 20, "column": 35} for wp in wps[:3]) + assert wps[3]["location"] == {"file_name": f"{task_dir}/Actions.java", "line": 104, "column": 7} + assert_single_final_target(entry) + assert edges[0]["assumption.scope"] == "java::LMain;.getBoolean()Z" + witnesslint(tmp_path / "witness.yml", COMMON, task_dir) + + # a frame in the package directory resolves through the package path + violation = Violation("java.lang.RuntimeException", [Frame("MinePumpSystem.MinePump", "MinePump.java", 30)]) + entry, _ = write(task_for(task_dir), [], violation, tmp_path) + assert waypoints(entry)[0]["location"]["file_name"] == f"{task_dir}/MinePumpSystem/MinePump.java" + # ... and not when the package does not match + violation = Violation("java.lang.RuntimeException", [Frame("other.MinePump", "MinePump.java", 30)]) + entry, _ = write(task_for(task_dir), [], violation, tmp_path) + assert entry["content"] == [] + + +def test_explicit_throw_target(tmp_path): + task_dir = FIXTURES / "jbmc-regression" / "exceptions16" + values = [NondetReturn("nondetInt", "int", "7", Location(class_name="Main", source_file="Main.java", line=19, call_index=0))] + violation = Violation("B", [Frame("Main", "Main.java", 27)]) + entry, _ = write(task_for(task_dir), values, violation, tmp_path) + wps = waypoints(entry) + assert wps[0]["location"]["column"] == 32 + assert wps[1]["location"] == {"file_name": f"{task_dir}/Main.java", "line": 27, "column": 7} + + +def test_inner_class_same_line_calls_unicode_and_package(tmp_path, witnesslint): + task_dir = FIXTURES / "synthetic" + main = lambda line, idx=0, cls="Main", src="Main.java": Location(class_name=cls, source_file=src, line=line, call_index=idx) + values = [ + NondetReturn("nondetChar", "char", "39", main(14)), + NondetReturn("nondetDouble", "double", "1.0E-5", main(15)), + NondetReturn("nondetFloat", "float", "0.1", main(16)), + NondetReturn("nondetLong", "long", "-9223372036854775808", main(17)), + NondetReturn("nondetString", "String", "a\"b<ä&\U0001F600\x00\n", main(18)), + NondetReturn("nondetInt", "int", "1", main(9, 0, "Main$Inner")), + NondetReturn("nondetInt", "int", "2", main(9, 1, "Main$Inner")), + NondetReturn("nondetInt", "int", "2", main(9, 2, "Main$Inner")), # no third call on the line + NondetReturn("nondetInt", "int", "3", main(7, 0, "pkg.Helper", "Helper.java")), + NondetReturn("nondetBoolean", "boolean", "true", main(29, 0, "Companion")), + ] + violation = Violation("java.lang.IllegalStateException", [Frame("Main", "Main.java", 21)]) + entry, (_, _, edges) = write(task_for(task_dir), values, violation, tmp_path) + wps = waypoints(entry) + main_java, helper_java = f"{task_dir}/Main.java", f"{task_dir}/pkg/Helper.java" + assert [(wp["constraint"]["value"], wp["location"]["file_name"], wp["location"]["line"], wp["location"].get("column")) for wp in wps[:-1]] == [ + ("\\result == '\\''", main_java, 14, 34), + ("\\result == 0.000010", main_java, 15, 38), + ("\\result == 0.1f", main_java, 16, 36), + ("\\result == -9223372036854775808L", main_java, 17, 34), + ('\\result.equals("a\\"b<\\u00e4&\\ud83d\\ude00\\u0000\\n")', main_java, 18, 38), + ("\\result == 1", main_java, 9, 33), + ("\\result == 2", main_java, 9, 56), + ("\\result == 2", main_java, 9, None), + ("\\result == 3", helper_java, 7, 35), + ("\\result == true", main_java, 29, 35), + ] + assert wps[-1] == {"type": "target", "action": "follow", "location": {"file_name": main_java, "line": 21, "column": 7}} + assert_single_final_target(entry) + assert edges[4]["assumption"] == '\\result.equals("a\\"b<\\u00e4&\\ud83d\\ude00\\u0000\\n");' + assert edges[5]["assumption.scope"] == "java::LMain$Inner;" + assert edges[8]["originfile"] == "pkg/Helper.java" and edges[8]["assumption.scope"] == "java::Lpkg/Helper;" + assert edges[0]["assumption"] == "\\result = 39;" + witnesslint(tmp_path / "witness.yml", COMMON, task_dir) + + +def test_file_name_locations(tmp_path, caplog): + task_dir = FIXTURES / "synthetic" + values = [ + NondetReturn("nondetChar", "char", "97", Location(file_name=f"{task_dir}/Main.java", line=14, column=34)), + NondetReturn("nondetDouble", "double", "1.5", Location(file_name="Main.java", line=15)), + NondetReturn("nondetInt", "int", "3", Location(file_name="pkg/Helper.java", line=7, column=0)), + ] + entry, (_, _, edges) = write(task_for(task_dir), values, None, tmp_path) + wps = waypoints(entry) + assert [(wp["location"]["file_name"], wp["location"].get("column")) for wp in wps] == [ + (f"{task_dir}/Main.java", 34), (f"{task_dir}/Main.java", 38), (f"{task_dir}/pkg/Helper.java", 35)] + assert [e["assumption.scope"] for e in edges] == ["java::LMain;", "java::LMain;", "java::LHelper;"] + assert [e["originfile"] for e in edges] == ["Main.java", "Main.java", "pkg/Helper.java"] + # a file that is not among the inputs is written as given, with a warning + values = [NondetReturn("nondetInt", "int", "4", Location(file_name="Elsewhere.java", line=1, column=2))] + with caplog.at_level(logging.WARNING, logger="witnesscreator"): + text = witness_module.render_yaml(task_for(task_dir), values, None) + assert "Elsewhere.java is not among the input files" in caplog.text + wp = yaml.safe_load(text)[0]["content"][0]["segment"][0]["waypoint"] + assert wp["location"] == {"file_name": "Elsewhere.java", "line": 1, "column": 2} + + +def test_no_target_warns_but_writes(tmp_path, caplog, witnesslint): + task_dir = FIXTURES / "jbmc-regression" / "return2" + values = [NondetReturn("nondetInt", "int", "1", Location(class_name="Main", source_file="Main.java", line=13))] + with caplog.at_level(logging.WARNING, logger="witnesscreator"): + entry, _ = write(task_for(task_dir), values, None, tmp_path) + assert [wp["type"] for wp in waypoints(entry)] == ["function_return"] + assert "no target waypoint" in caplog.text + witnesslint(tmp_path / "witness.yml", COMMON, task_dir) + + # all frames outside the task sources (JDK, SWAT's own classes, wrong line, unknown class) + caplog.clear() + violation = Violation("java.lang.ArithmeticException", [ + Frame("java.lang.Integer", "Integer.java", 1), Frame("de.uzl.its.swat.Main", "Main.java", 13), + Frame("Main", "Main.java", 0), Frame("Main", "Main.java", 999), Frame("Nope", "Nope.java", 3), Frame("", None, 3)]) + with caplog.at_level(logging.WARNING, logger="witnesscreator"): + entry, _ = write(task_for(task_dir), values, violation, tmp_path) + assert [wp["type"] for wp in waypoints(entry)] == ["function_return"] + assert "No stack frame of java.lang.ArithmeticException lies in the task sources" in caplog.text + + +def test_unresolvable_value_location_falls_back_to_package_path(tmp_path, caplog): + task_dir = FIXTURES / "jbmc-regression" / "return2" + values = [NondetReturn("nondetInt", "int", "1", Location(class_name="securibench/micro/basic/Basic4", source_file="Basic4.java", line=29, method="doGet()V"))] + with caplog.at_level(logging.WARNING, logger="witnesscreator"): + text = witness_module.render_yaml(task_for(task_dir), values, None) + assert "Could not find the source of securibench/micro/basic/Basic4" in caplog.text + doc = yaml.safe_load(text)[0] + wp = doc["content"][0]["segment"][0]["waypoint"] + assert wp["location"] == {"file_name": "securibench/micro/basic/Basic4.java", "line": 29} + assert wp["constraint"]["value"] == "\\result == 1" + + +def test_never_crashes_on_garbage(tmp_path, caplog): + task = Task(input_files=[str(tmp_path / "missing"), "", str(FIXTURES / "synthetic")], property_file=str(tmp_path / "no.prp")) + values = [ + NondetReturn(None, None, None, None), + NondetReturn("x", "weird", "v", Location(line="x")), + NondetReturn("x", "int", "1", Location(class_name="Main", line=-4)), + NondetReturn("x", "int", "1", Location(line=3)), + NondetReturn("x", "int", object(), Location(class_name="Main", source_file="Main.java", line=14, call_index=None, column="?")), + "not even a value", + ] + violation = Violation(None, [None, "junk", Frame(None, None, None), Frame("Main", "Main.java", "x")]) + with caplog.at_level(logging.WARNING, logger="witnesscreator"): + paths = write_witnesses(task, values, violation, tmp_path) + assert set(paths) == {"yaml", "graphml"} + entry = load_yaml(paths["yaml"]) + assert entry["metadata"]["task"]["specification"] == witness_module.DEFAULT_SPECIFICATION + assert len(entry["content"]) == 1 # the one value with a usable location + load_graphml(paths["graphml"]) + assert "Ignoring missing input" in caplog.text + assert "Could not read property file" in caplog.text + + +def test_formats_are_written_independently(tmp_path, monkeypatch): + task_dir = FIXTURES / "jbmc-regression" / "return2" + + def boom(*args, **kwargs): + raise RuntimeError("graphml writer broken") + + monkeypatch.setattr(witness_module, "_render_graphml", boom) + paths = write_witnesses(task_for(task_dir), [], None, tmp_path) + assert set(paths) == {"yaml"} + assert write_witnesses(task_for(task_dir), [], None, tmp_path, formats=("yaml",)) == {"yaml": tmp_path / "witness.yml"} + assert write_witnesses(task_for(task_dir), [], None, tmp_path, formats=("xml",)) == {} + assert write_witnesses(task_for(task_dir), [], None, tmp_path, formats=()) == {} + + +def test_render_functions_and_relative_inputs(tmp_path): + task = Task(input_files=["../common/", "return2/Main.java"], property_file="../properties/valid-assert.prp", + base_dir=FIXTURES / "jbmc-regression") + values = [NondetReturn("nondetInt", "int", "1", Location(class_name="Main", source_file="Main.java", line=13))] + doc = yaml.safe_load(witness_module.render_yaml(task, values, None))[0] + assert doc["metadata"]["task"]["input_files"] == ["../common/org/sosy_lab/sv_benchmarks/Verifier.java", "return2/Main.java"] + assert doc["metadata"]["producer"]["name"] == "witnesscreator" + assert doc["content"][0]["segment"][0]["waypoint"]["location"]["file_name"] == "return2/Main.java" + assert "Main.java" in witness_module.render_graphml(task, values, None) + + +@pytest.mark.parametrize("name", ["jbmc-regression/return2", "jdart-regression/float", "MinePump/spec1-5_product25", "synthetic"]) +def test_default_violation_lints(tmp_path, witnesslint, name): + task_dir = FIXTURES / name + paths = write_witnesses(task_for(task_dir), [], None, tmp_path) + assert load_yaml(paths["yaml"])["content"] == [] + witnesslint(paths["yaml"], COMMON, task_dir) diff --git a/tests/test_escaping.py b/tests/test_escaping.py new file mode 100644 index 0000000..721da06 --- /dev/null +++ b/tests/test_escaping.py @@ -0,0 +1,102 @@ +import xml.etree.ElementTree as ET + +import pytest +import yaml + +from witnesscreator.graphml_writer import Assumption, render_graphml, xml_escape +from witnesscreator.yaml_writer import Metadata, Waypoint, render_yaml, yaml_quote + + +@pytest.mark.parametrize( + "s", + [ + "", + "plain", + 'quote " and backslash \\', + "\\result == 3", + "tab\tnewline\ncr\r", + "\x00\x01\x1f\x7f", + "\x85\xa0

", + "ä€", + "\U0001F600 emoji", + "￾￿", + "\ud800 lone surrogate", + "a: b # not a comment", + "- not a list", + ], +) +def test_yaml_quote_round_trips_through_pyyaml(s): + quoted = yaml_quote(s) + assert quoted.isascii() + assert yaml.safe_load(quoted) == s + assert yaml.safe_load(f"k: {quoted}\n") == {"k": s} + + +def test_yaml_quote_escapes(): + assert yaml_quote('\\result.equals("a\\"b")') == '"\\\\result.equals(\\"a\\\\\\"b\\")"' + assert yaml_quote("ä") == '"\\u00e4"' + assert yaml_quote("\U0001F600") == '"\\U0001f600"' + assert yaml_quote("\n\t\r") == '"\\n\\t\\r"' + + +def test_yaml_document_structure(): + md = Metadata("u", "2026-01-01T00:00:00Z", "P", "v", 'CHECK( init(Main.main()), LTL(G assert) )', [("a/Main.java", "0" * 64)]) + text = render_yaml(md, [Waypoint.function_return('\\result.equals("x")', "a/Main.java", 3, 7), Waypoint.target("a/Main.java", 4, None)]) + doc = yaml.safe_load(text) + entry = doc[0] + assert entry["metadata"]["uuid"] == "u" + assert entry["metadata"]["task"]["input_file_hashes"] == {"a/Main.java": "0" * 64} + assert entry["metadata"]["task"]["specification"] == "CHECK( init(Main.main()), LTL(G assert) )" + wps = [s["segment"][0]["waypoint"] for s in entry["content"]] + assert wps[0]["constraint"] == {"value": '\\result.equals("x")', "format": "java_expression"} + assert wps[0]["location"] == {"file_name": "a/Main.java", "line": 3, "column": 7} + assert wps[1] == {"type": "target", "action": "follow", "location": {"file_name": "a/Main.java", "line": 4}} + assert yaml.safe_load(render_yaml(md, []))[0]["content"] == [] + empty = Metadata("u", "t", "P", "v", "spec", []) + assert yaml.safe_load(render_yaml(empty, []))[0]["metadata"]["task"]["input_files"] == [] + + +@pytest.mark.parametrize( + "s, expected", + [ + ("a < b & c > d \"q\"", "a < b & c > d "q""), + ("", "<init>"), + ("\x00\x01\x0b", "\\u0000\\u0001\\u000b"), + ("\t\n ok", "\t\n ok"), + ("￾", "\\ufffe"), + ("ä", "ä"), + ], +) +def test_xml_escape(s, expected): + assert xml_escape(s) == expected + + +def test_graphml_escapes_all_text_and_parses(): + text = render_graphml( + "P & Co", "CHECK( )", + [Assumption("pkg/

.java", 3, '\\result.equals("");', "java::Lpkg/Main;.()V")], + ) + root = ET.fromstring(text) + ns = "{http://graphml.graphdrawing.org/xmlns}" + graph = root.find(ns + "graph") + data = {d.get("key"): d.text for d in graph.findall(ns + "data")} + assert data["producer"] == "P & Co" + assert data["specification"] == "CHECK( )" + assert data["sourcecodelang"] == "Java" + edge = graph.find(ns + "edge") + ed = {d.get("key"): d.text for d in edge.findall(ns + "data")} + assert ed["originfile"] == "pkg/
.java" + assert ed["assumption"] == '\\result.equals("");' + assert ed["assumption.scope"] == "java::Lpkg/Main;.()V" + nodes = {n.get("id"): {d.get("key"): d.text for d in n.findall(ns + "data")} for n in graph.findall(ns + "node")} + assert nodes["n0"] == {"entry": "true"} + assert nodes["n1"] == {"violation": "true"} + assert "sink" in nodes + + +def test_graphml_default_violation(): + root = ET.fromstring(render_graphml("P", None, [])) + ns = "{http://graphml.graphdrawing.org/xmlns}" + nodes = {n.get("id"): {d.get("key"): d.text for d in n.findall(ns + "data")} for n in root.iter(ns + "node")} + assert nodes["n0"] == {"entry": "true", "violation": "true"} + assert not list(root.iter(ns + "edge")) diff --git a/tests/test_events.py b/tests/test_events.py new file mode 100644 index 0000000..7fcaf06 --- /dev/null +++ b/tests/test_events.py @@ -0,0 +1,62 @@ +import json + +from witnesscreator import Frame, Location, NondetReturn, Violation, dump_events, parse_events, read_events +from witnesscreator.events import nondet_return_from_dict, nondet_return_to_dict, violation_to_dict + + +def test_round_trip(tmp_path): + values = [ + NondetReturn("nondetInt", "int", "42", Location(class_name="pkg.Main", source_file="Main.java", line=12, call_index=1)), + NondetReturn("nondetString", "String", "a\"b\nä", Location(file_name="Main.java", line=13, column=27), bits=None), + NondetReturn("nondetFloat", "float", "0.1", Location(class_name="Main", line=14), bits="0x3dcccccd"), + ] + violation = Violation("java.lang.AssertionError", [Frame("pkg.Main", "Main.java", 17), Frame("java.lang.Thread", None, -1)]) + text = dump_events(values, violation, "SWAT", "svcomp27") + lines = text.splitlines() + header = json.loads(lines[0]) + assert header == {"kind": "header", "schema": "witnesscreator-events", "version": 1, "producer": {"name": "SWAT", "version": "svcomp27"}} + assert json.loads(lines[1])["kind"] == "nondet_return" + assert json.loads(lines[1])["location"]["class_name"] == "pkg.Main" + assert json.loads(lines[-1])["kind"] == "violation" + + path = tmp_path / "events.jsonl" + path.write_text(text, encoding="utf-8") + ev = read_events(path) + assert ev.producer_name == "SWAT" and ev.producer_version == "svcomp27" + assert ev.values == values + assert ev.violation == violation + + +def test_dict_forms(): + nr = NondetReturn("nondetInt", "int", "1", Location(line=3)) + d = nondet_return_to_dict(nr) + assert d["kind"] == "nondet_return" and d["bits"] is None and d["location"]["line"] == 3 + assert nondet_return_from_dict(d) == nr + v = violation_to_dict(Violation("x", [])) + assert v == {"kind": "violation", "throwable": "x", "frames": []} + + +def test_lenient_parsing(): + lines = [ + "", + "not json", + "[1, 2]", + '{"kind": "header", "schema": "other", "version": 99}', + '{"kind": "nondet_return", "type": "int", "value": 7, "location": {"line": "4", "call_index": null, "column": 0}}', + '{"kind": "nondet_return", "value": "x"}', + '{"kind": "violation", "throwable": "A", "frames": [{"class_name": "Main", "line": "x"}, "junk"]}', + '{"kind": "violation", "throwable": "B", "frames": null}', + '{"kind": "mystery"}', + ] + ev = parse_events(lines) + assert ev.header["version"] == 99 + assert ev.producer_name is None + assert len(ev.values) == 2 + assert ev.values[0].value == "7" and ev.values[0].location.line == 4 + assert ev.values[0].location.call_index == 0 and ev.values[0].location.column is None + assert ev.values[1].location == Location() + assert ev.violation.throwable == "B" and ev.violation.frames == [] + + +def test_header_without_producer(): + assert json.loads(dump_events([], None).splitlines()[0]) == {"kind": "header", "schema": "witnesscreator-events", "version": 1} diff --git a/tests/test_literals.py b/tests/test_literals.py new file mode 100644 index 0000000..b904d4a --- /dev/null +++ b/tests/test_literals.py @@ -0,0 +1,141 @@ +import pytest + +from witnesscreator.literals import ( + char_literal, + graphml_assumption_value, + plain_decimal, + result_constraint, + string_literal, + value_from_bits, +) +from witnesscreator.model import normalize_type + + +def test_integral_types(): + assert result_constraint("5", "int") == "\\result == 5" + assert result_constraint("-5", "I") == "\\result == -5" + assert result_constraint("-128", "byte") == "\\result == -128" + assert result_constraint("32767", "S") == "\\result == 32767" + assert result_constraint("-2147483648", "int") == "\\result == -2147483648" + + +def test_longs_get_suffix_only_outside_int_range(): + assert result_constraint("5", "long") == "\\result == 5" + assert result_constraint("2147483647", "J") == "\\result == 2147483647" + assert result_constraint("2147483648", "J") == "\\result == 2147483648L" + assert result_constraint("5000000000", "long") == "\\result == 5000000000L" + assert result_constraint("-9223372036854775808", "long") == "\\result == -9223372036854775808L" + assert result_constraint("garbage", "long") == "\\result == garbage" + + +def test_booleans(): + assert result_constraint("true", "boolean") == "\\result == true" + assert result_constraint("false", "Z") == "\\result == false" + assert result_constraint("maybe", "boolean") == "\\result == false" + + +def test_chars_are_java_literals(): + assert result_constraint("97", "char") == "\\result == 'a'" + assert result_constraint("39", "C") == "\\result == '\\''" + assert result_constraint("92", "C") == "\\result == '\\\\'" + assert result_constraint("10", "C") == "\\result == '\\n'" + assert result_constraint("0", "C") == "\\result == '\\u0000'" + assert result_constraint("228", "C") == "\\result == '\\u00e4'" + assert result_constraint("65535", "C") == "\\result == '\\uffff'" + assert result_constraint("127", "C") == "\\result == '\\u007f'" + assert char_literal("x") == "x" + assert char_literal("70000") == "70000" + + +def test_floating_point(): + assert result_constraint("1.5", "float") == "\\result == 1.5f" + assert result_constraint("-0.000002022784", "F") == "\\result == -0.000002022784f" + assert result_constraint("1.0E10", "F") == "\\result == 10000000000.0f" + assert result_constraint("1.0E-5", "D") == "\\result == 0.000010" + assert result_constraint("0.1", "double") == "\\result == 0.1" + assert result_constraint("-0.0", "D") == "\\result == -0.0" + assert result_constraint("-0.0", "F") == "\\result == -0.0f" + assert result_constraint("10000000000", "D") == "\\result == 10000000000.0" + assert result_constraint("NaN", "float") == "Float.isNaN(\\result)" + assert result_constraint("NaN", "D") == "Double.isNaN(\\result)" + assert result_constraint("Infinity", "double") == "\\result == Double.POSITIVE_INFINITY" + assert result_constraint("-Infinity", "float") == "\\result == Float.NEGATIVE_INFINITY" + assert result_constraint("1.5f", "F") == "\\result == 1.5f" + assert result_constraint("nonsense", "D") == "\\result == nonsense.0" + + +def test_plain_decimal(): + assert plain_decimal("1.0E10") == "10000000000" + assert plain_decimal("-1.0E-3") == "-0.0010" + assert plain_decimal("-0.0") == "-0.0" + assert plain_decimal("1E3") == "1000" + assert plain_decimal("x") == "x" + + +def test_strings(): + assert result_constraint("abc", "String") == '\\result.equals("abc")' + assert result_constraint("", "Ljava/lang/String;") == '\\result.equals("")' + assert result_constraint('a"b\\c\nd\te', "String") == '\\result.equals("a\\"b\\\\c\\nd\\te")' + assert result_constraint("\u0001x\u007f", "String") == '\\result.equals("\\u0001x\\u007f")' + assert result_constraint("\r\b\f", "String") == '\\result.equals("\\r\\b\\f")' + + +def test_string_literal_escapes_everything_non_ascii(): + assert string_literal("ä€") == '"\\u00e4\\u20ac"' + # outside the BMP: a surrogate pair, as Java sees it + assert string_literal("\U0001F600") == '"\\ud83d\\ude00"' + # a lone surrogate (e.g. from surrogateescape decoding) is representable too + assert string_literal("\ud800") == '"\\ud800"' + assert string_literal("\x00\x1f\x85
") == '"\\u0000\\u001f\\u0085\\u2028"' + + +def test_legacy_markers_without_type(): + assert result_constraint("42", None) == "\\result == 42" + assert result_constraint("-7", None) == "\\result == -7" + assert result_constraint("true", None) == "\\result == true" + assert result_constraint("hi", None) == '\\result.equals("hi")' + assert result_constraint("1.5", "unknown-type") == '\\result.equals("1.5")' + + +def test_normalize_type(): + assert normalize_type("I") == "int" + assert normalize_type("int") == "int" + assert normalize_type("Ljava/lang/String;") == "String" + assert normalize_type("java.lang.String") == "String" + assert normalize_type(None) is None + assert normalize_type("Object") is None + + +def test_value_from_bits(): + assert value_from_bits("0x3dcccccd", "float") == "0.10000000149011612" + assert value_from_bits("0x3ff0000000000000", "double") == "1.0" + assert value_from_bits("0x7fc00000", "float") == "NaN" + assert value_from_bits("0x7f800000", "float") == "Infinity" + assert value_from_bits("0xfff0000000000000", "double") == "-Infinity" + assert value_from_bits("0x80000000", "float") == "-0.0" + assert value_from_bits("0x1", "int") is None + assert value_from_bits("zz", "float") is None + assert result_constraint(value_from_bits("0x3dcccccd", "float"), "float") == "\\result == 0.10000000149011612f" + + +@pytest.mark.parametrize( + "value, type_, expected", + [ + ("5", "int", "5"), + ("5000000000", "long", "5000000000"), + ("true", "boolean", "true"), + ("97", "char", "97"), + ("a", "char", "97"), + ("1.5", "float", "1.5"), + ("1.0E10", "double", "10000000000"), + ("-0.0", "double", "-0.0"), + ("NaN", "float", "NaN"), + ("-Infinity", "double", "-Infinity"), + ("a\"b", "String", '.equals("a\\"b")'), + ("ä", "String", '.equals("\\u00e4")'), + ("42", None, "42"), + ("x", None, '.equals("x")'), + ], +) +def test_graphml_assumption_value(value, type_, expected): + assert graphml_assumption_value(value, type_) == expected diff --git a/tests/test_locations.py b/tests/test_locations.py new file mode 100644 index 0000000..11eed7f --- /dev/null +++ b/tests/test_locations.py @@ -0,0 +1,173 @@ +import pytest + +from witnesscreator.columns import mask_non_code, nondet_call_column, statement_column +from witnesscreator.sources import SourceFiles, fallback_file_name, split_lines + + +def test_column_of_closing_parenthesis(): + line = " Boolean input_1_0 = Verifier.nondetBoolean();" + assert nondet_call_column(line, 0) == 48 + assert nondet_call_column(line, 1) is None + two = " if (!chunked && Verifier.nondetInt() > 0 && Verifier.nondetInt() != 0) {" + c0, c1 = nondet_call_column(two, 0), nondet_call_column(two, 1) + assert two[c0 - 1] == ")" and two[c1 - 1] == ")" and c0 < c1 + assert nondet_call_column("x = Verifier.nondetInt ( );", 0) == 26 + assert nondet_call_column("no call here", 0) is None + assert nondet_call_column("Verifier.nondetInt(", 0) is None + assert nondet_call_column("x = nondetInt(f(1, (2)));", 0) == 24 + assert nondet_call_column("", 0) is None + assert nondet_call_column(None, 0) is None + assert nondet_call_column("Verifier.nondetInt()", -1) is None + + +def test_nondet_call_needs_word_boundary(): + assert nondet_call_column("x = mynondetInt();", 0) is None + assert nondet_call_column("x = my_nondetInt();", 0) is None + assert nondet_call_column("x = Verifier.nondetInt();", 0) == 24 + assert nondet_call_column("x = nondet();", 0) == 12 + + +def test_calls_in_comments_and_strings_are_ignored(): + line = mask_non_code('String s = "nondetInt()"; int x = Verifier.nondetInt(); // nondetInt()') + assert nondet_call_column(line, 0) == 54 + assert nondet_call_column(line, 1) is None + line = mask_non_code('int x = Verifier.nondetInt(/* ) */);') + assert nondet_call_column(line, 0) == 35 + line = mask_non_code("char c = ')'; int x = Verifier.nondetInt();") + assert nondet_call_column(line, 0) == 42 + + +def test_mask_non_code_keeps_positions(): + src = 'a = "x\\"y"; // c\nb = \'"\'; /* multi\nline */ c = 1;\nd = """t\nb""" + 2;\n' + masked = mask_non_code(src) + assert len(masked) == len(src) + assert masked.count("\n") == src.count("\n") + assert masked.splitlines() == ["a = ; ", "b = ; ", " c = 1;", "d = ", " + 2;"] + # unterminated constructs do not raise + assert len(mask_non_code('x = "unterminated')) == len('x = "unterminated') + assert len(mask_non_code("/* never closed")) == len("/* never closed") + assert mask_non_code("") == "" + + +def test_column_of_violating_statement(): + assert statement_column(" } else assert false;", True) == 12 + assert statement_column(" assert !(output_1 == 1);", True) == 5 + assert statement_column(" assert !(output_1 == 1);", False) == 5 + assert statement_column(" } throw new RuntimeException();", False) == 7 + assert statement_column(" int x = a / b;", False) == 5 + assert statement_column(" } else { int x = a / b; }", False) == 14 + assert statement_column("\t\t\tx = elsewhere / 0;", False) == 4 # a tab is one column + assert statement_column(" }", False) is None + assert statement_column("", False) is None + assert statement_column(None, False) is None + assert statement_column(" elsewhere = 1;", False) == 5 + assert statement_column(" x.throws();", False) == 3 + assert statement_column(" if (b) throw new Error();", True) == 10 + # the keyword inside a string or comment does not count once masked + assert statement_column(mask_non_code(' s = "assert"; assert x;'), True) == 17 + assert statement_column(mask_non_code(" } // assert here"), True) is None + + +def test_split_lines_only_on_line_breaks(): + assert split_lines("a\nb\r\nc\rd") == ["a", "b", "c", "d"] + assert split_lines("a\n") == ["a"] + assert split_lines("") == [] + assert split_lines("a\x0cb
c\n") == ["a\x0cb
c"] + + +@pytest.fixture +def tree(tmp_path): + task = tmp_path / "task" + (task / "pkg").mkdir(parents=True) + (task / "Main.java").write_text("class Main {}\nclass Helper {}\n") + (task / "pkg" / "Foo.java").write_text("package pkg;\nclass Foo {}\n") + (task / "notes.txt").write_text("ignored") + common = tmp_path / "common" + (common / "org" / "sosy_lab" / "sv_benchmarks").mkdir(parents=True) + (common / "org" / "sosy_lab" / "sv_benchmarks" / "Verifier.java").write_text("package org.sosy_lab.sv_benchmarks;\n") + return tmp_path, task, common + + +def test_collect_lists_inputs_as_given(tree): + tmp, task, common = tree + files = SourceFiles.collect([str(common) + "/", str(task)]) + assert [f.display_path for f in files] == [ + f"{common}/org/sosy_lab/sv_benchmarks/Verifier.java", + f"{task}/Main.java", + f"{task}/pkg/Foo.java", + ] + assert [f.relative_path for f in files] == ["org/sosy_lab/sv_benchmarks/Verifier.java", "Main.java", "pkg/Foo.java"] + assert len(files.files[0].sha256) == 64 + # a file reachable through several inputs is listed once + nested = SourceFiles.collect([str(task / "pkg"), str(task), str(task / "pkg" / "Foo.java")]) + assert [f.display_path for f in nested] == [f"{task}/pkg/Foo.java", f"{task}/Main.java"] + # relative inputs are resolved against base_dir but displayed as given + rel = SourceFiles.collect(["../common/", "Main.java"], base_dir=task) + assert [f.display_path for f in rel] == ["../common/org/sosy_lab/sv_benchmarks/Verifier.java", "Main.java"] + assert rel.files[1].path.exists() + # missing and non-java inputs are ignored + assert len(SourceFiles.collect([str(tmp / "missing"), str(task / "notes.txt"), ""])) == 0 + assert len(SourceFiles.collect([str(task / "notes.txt")])) == 0 + + +def test_resolve_classes(tree): + _, task, common = tree + files = SourceFiles.collect([str(common), str(task)]) + assert files.resolve("Main", "Main.java").relative_path == "Main.java" + assert files.resolve("Main$1", None).relative_path == "Main.java" + assert files.resolve("Helper", "Main.java").relative_path == "Main.java" + assert files.resolve("pkg/Foo", "Foo.java").relative_path == "pkg/Foo.java" + assert files.resolve("pkg.Foo$Inner", "").relative_path == "pkg/Foo.java" + assert files.resolve("org.sosy_lab.sv_benchmarks.Verifier", "Verifier.java").relative_path == "org/sosy_lab/sv_benchmarks/Verifier.java" + assert files.resolve("Missing", "") is None + # a file whose package declaration contradicts the class is never taken + assert files.resolve("other.Foo", "Foo.java", allow_name_only=True) is None + assert files.resolve("other.Main", None, allow_name_only=True) is None + assert files.resolve("Foo", None, allow_name_only=True) is None # Foo lives in pkg/ + # a file without a readable package declaration only resolves by name when allowed + (task / "Empty.java").write_text("") + files = SourceFiles.collect([str(common), str(task)]) + assert files.resolve("some.pkg.Empty", None, allow_name_only=True).relative_path == "Empty.java" + assert files.resolve("some.pkg.Empty", None, allow_name_only=False) is None + # a matching declaration is accepted whatever the path (e.g. sources below an src/ dir) + (task / "src").mkdir() + (task / "src" / "Bar.java").write_text("/* c */ package pkg; class Bar {}\n") + files = SourceFiles.collect([str(task)]) + assert files.resolve("pkg.Bar", "Bar.java", allow_name_only=False).relative_path == "src/Bar.java" + assert files.resolve("Bar", "Bar.java", allow_name_only=True) is None + # the package path may be a suffix of the file's path (input root above the package root) + outer = SourceFiles.collect([str(task.parent)]) + assert outer.resolve("pkg.Foo", "Foo.java", allow_name_only=False).relative_path == "task/pkg/Foo.java" + assert outer.resolve("Main", "Main.java", allow_name_only=False).relative_path == "task/Main.java" + + +def test_resolve_file_name(tree): + _, task, common = tree + files = SourceFiles.collect([str(common), str(task)]) + assert files.resolve_file_name(f"{task}/pkg/Foo.java").relative_path == "pkg/Foo.java" + assert files.resolve_file_name("pkg/Foo.java").relative_path == "pkg/Foo.java" + assert files.resolve_file_name("./Foo.java").relative_path == "pkg/Foo.java" + assert files.resolve_file_name("Verifier.java").relative_path == "org/sosy_lab/sv_benchmarks/Verifier.java" + assert files.resolve_file_name("Nope.java") is None + assert files.resolve_file_name("") is None + + +def test_lines_and_masking(tree): + _, task, _ = tree + files = SourceFiles.collect([str(task)]) + main = files.resolve("Main", None) + assert main.line(1) == "class Main {}" + assert main.line(2) == "class Helper {}" + assert main.line(3) is None + assert main.line(0) is None + assert main.masked_line(1) == "class Main {}" + assert main.masked_line(9) is None + assert main.package == "" + assert files.resolve("pkg.Foo", None).package == "pkg" + + +def test_fallback_file_name(): + assert fallback_file_name("pkg.Main$1", "Main.java") == "pkg/Main.java" + assert fallback_file_name("pkg/Main$1", None) == "pkg/Main.java" + assert fallback_file_name("Main", "") == "Main.java" + assert fallback_file_name("a.b.Outer$Inner$2", None) == "a/b/Outer.java" diff --git a/tests/test_markers.py b/tests/test_markers.py new file mode 100644 index 0000000..8c4d54e --- /dev/null +++ b/tests/test_markers.py @@ -0,0 +1,123 @@ +import base64 + +import pytest + +from witnesscreator.markers import ( + decode_base64, + parse_marker_lines, + parse_markers, + parse_target_marker, + parse_value_marker, +) + + +def b64(s: str) -> str: + return base64.b64encode(s.encode()).decode() + + +def test_parses_current_format(): + m = parse_value_marker("5@@@13@@@pkg/Main$1@@@main([Ljava/lang/String;)V@@@2@@@I@@@Main.java") + assert m.value == "5" + assert m.type == "int" + assert m.function == "nondetInt" + assert m.location.line == 13 + assert m.location.class_name == "pkg/Main$1" + assert m.location.method == "main([Ljava/lang/String;)V" + assert m.location.call_index == 2 + assert m.location.source_file == "Main.java" + + +def test_string_values_may_contain_the_separator(): + m = parse_value_marker("a@@@b@@@7@@@Main@@@main()V@@@0@@@Ljava/lang/String;@@@Main.java") + assert m.value == "a@@@b" + assert m.type == "String" + assert m.function == "nondetString" + assert m.location.line == 7 + legacy = parse_value_marker("a@@@b@@@7@@@Main@@@main()V") + assert legacy.value == "a@@@b" + assert legacy.location.line == 7 + + +def test_parses_legacy_format(): + m = parse_value_marker("true@@@13@@@Main@@@main([Ljava/lang/String;)V") + assert m.value == "true" + assert m.type is None + assert m.function is None + assert m.location.line == 13 + assert m.location.class_name == "Main" + assert m.location.call_index == 0 + assert m.location.source_file is None + + +def test_empty_source_file_and_types(): + m = parse_value_marker("97@@@3@@@Main@@@m()V@@@0@@@C@@@") + assert m.type == "char" and m.location.source_file is None + m = parse_value_marker("1.5@@@3@@@Main@@@m()V@@@0@@@F@@@Main.java") + assert m.type == "float" and m.function == "nondetFloat" + + +def test_rejects_garbage(): + with pytest.raises(ValueError): + parse_value_marker("nonsense") + with pytest.raises(ValueError): + parse_value_marker("a@@@b@@@c@@@d") # line is not a number + with pytest.raises(ValueError): + parse_target_marker("no separator") + + +def test_parses_target(): + t = parse_target_marker( + "java.lang.AssertionError@@@Main@@Main.java@@23;pkg.Helper$Inner@@Helper.java@@5;java.lang.Thread@@@@-1" + ) + assert t.is_assertion_error + assert len(t.frames) == 3 + assert t.frames[0].class_name == "Main" + assert t.frames[0].source_file == "Main.java" + assert t.frames[0].line == 23 + assert t.frames[2].source_file is None + assert t.frames[2].line == -1 + assert parse_target_marker("java.lang.RuntimeException@@@").frames == [] + assert parse_target_marker("x@@@bad;Main@@Main.java@@notanumber").frames[0].line == -1 + + +def test_marker_lines_from_log_output(): + lines = [ + "2026-10-15 10:20:02 [INFO] [SWAT] --> [WITNESS] " + b64("3@@@4@@@Main@@@main([Ljava/lang/String;)V@@@0@@@I@@@Main.java"), + "unrelated line", + "[WITNESS] not-base64!!", + "[WITNESS_TARGET] " + b64("java.lang.AssertionError@@@Main@@Main.java@@7"), + "[WITNESS] " + b64("a\"b@@@5@@@Main@@@main([Ljava/lang/String;)V@@@0@@@Ljava/lang/String;@@@Main.java"), + ] + values, violation = parse_marker_lines(lines) + assert [v.value for v in values] == ["3", 'a"b'] + assert violation.throwable == "java.lang.AssertionError" + assert violation.frames[0].line == 7 + + +def test_last_target_wins(): + lines = [ + "[WITNESS_TARGET] " + b64("java.lang.AssertionError@@@Main@@Main.java@@7"), + "[WITNESS_TARGET] " + b64("java.lang.RuntimeException@@@Main@@Main.java@@9"), + ] + _, violation = parse_marker_lines(lines) + assert violation.throwable == "java.lang.RuntimeException" + + +def test_parse_markers_accepts_base64_blob_and_plain_text(): + plain = "[WITNESS] " + b64("1@@@2@@@Main@@@()V") + "\n[WITNESS_TARGET] " + b64("java.lang.AssertionError@@@Main@@Main.java@@3") + for text in (plain, b64(plain), " " + b64(plain) + "\n"): + values, violation = parse_markers(text) + assert len(values) == 1 and violation is not None + assert parse_markers("") == ([], None) + assert parse_markers(" ") == ([], None) + assert parse_markers("not markers at all") == ([], None) + assert parse_markers(None) == ([], None) + + +def test_decode_base64_is_lenient(): + assert decode_base64(b64("abc")) == "abc" + assert decode_base64("YWJj") == "abc" + assert decode_base64("YWJjZA") == "abcd" # missing padding + assert decode_base64("YW Jj\n") == "abc" # whitespace + assert decode_base64(base64.urlsafe_b64encode(b"\xfb\xff").decode()) == "��" # url-safe, bad utf-8 replaced + assert decode_base64("!!!") == "" # nothing but junk decodes to nothing diff --git a/tools/build_pyz.py b/tools/build_pyz.py new file mode 100644 index 0000000..25eada6 --- /dev/null +++ b/tools/build_pyz.py @@ -0,0 +1,35 @@ +#!/usr/bin/env python3 +"""Builds the single-file ``witnesscreator.pyz`` (a zipapp, stdlib only). + +usage: tools/build_pyz.py [OUTPUT] (default: dist/witnesscreator.pyz) +""" + +import shutil +import sys +import tempfile +import zipapp +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +PACKAGE = ROOT / "src" / "witnesscreator" + + +def main() -> int: + target = Path(sys.argv[1]) if len(sys.argv) > 1 else ROOT / "dist" / "witnesscreator.pyz" + target.parent.mkdir(parents=True, exist_ok=True) + with tempfile.TemporaryDirectory() as tmp: + staging = Path(tmp) / "app" + shutil.copytree(PACKAGE, staging / "witnesscreator", ignore=shutil.ignore_patterns("__pycache__", "*.pyc")) + zipapp.create_archive( + staging, + target=target, + interpreter="/usr/bin/env python3", + main="witnesscreator.cli:main", + compressed=True, + ) + print(target) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/witnesses/default_violation.st b/witnesses/default_violation.st deleted file mode 100755 index 81cb4a6..0000000 --- a/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/witnesses/witness.st b/witnesses/witness.st deleted file mode 100755 index 6e7e57a..0000000 --- a/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