diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 994aed3..65c9273 100644 --- a/.github/workflows/gradle.yml +++ b/.github/workflows/gradle.yml @@ -6,8 +6,9 @@ on: workflow_dispatch: env: - SVCOMP_REFERENCE_URL: https://zenodo.org/api/records/17748741/files/swat-verify.zip/content - SVCOMP_REFERENCE_MD5: 8c776d19ac33ecf5c1c7441d16cc18a6 + SVCOMP_VENV_DIR_NAME: .venv_ubuntu_24_04_1__x86_64 + WITNESS_CREATOR_VERSION: v0.1.1 + WITNESS_CREATOR_SHA256: 8fc8810237c99bf7d709bdb8692142695e407b5681e818fcfe8b45f9c598d814 jobs: build: @@ -27,31 +28,51 @@ jobs: run: ./gradlew copyNativeLibs - name: Build run: ./gradlew --no-daemon build -x test - - name: Build WitnessCreator JAR - run: ./gradlew --no-daemon :targets:sv-comp:WitnessCreator:shadowJar + - name: Collect JavaSMT JAR + run: | + java_smt_dir="${HOME}/.gradle/caches/modules-2/files-2.1/org.sosy-lab/java-smt" + if [[ ! -d "$java_smt_dir" ]]; then + echo "JavaSMT Gradle cache directory not found: $java_smt_dir" >&2 + exit 1 + fi + + java_smt_jar="$(find "$java_smt_dir" -type f -name 'java-smt-*.jar' ! -name '*-sources.jar' ! -name '*-javadoc.jar' | sort | tail -n 1)" + if [[ -z "$java_smt_jar" ]]; then + echo "JavaSMT JAR not found in Gradle cache: $java_smt_dir" >&2 + exit 1 + fi + + mkdir -p build/svcomp-runtime + cp "$java_smt_jar" build/svcomp-runtime/java-smt-latest.jar - name: Upload JARs - if: github.event_name != 'pull_request' uses: actions/upload-artifact@v4 with: name: release-jars-${{ github.sha }} path: | symbolic-executor/lib/symbolic-executor.jar - targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar + build/svcomp-runtime/java-smt-latest.jar if-no-files-found: error retention-days: 1 package: needs: build if: >- + github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch' || (github.event_name == 'push' && ( github.ref == 'refs/heads/main' || github.ref == 'refs/heads/dev' || startsWith(github.ref, 'refs/tags/') )) - runs-on: ubuntu-latest + runs-on: ubuntu-24.04 permissions: - contents: write + contents: read + outputs: + channel: ${{ steps.meta.outputs.channel }} + zip-name: ${{ steps.meta.outputs.zip-name }} + rolling: ${{ steps.meta.outputs.rolling }} + prerelease: ${{ steps.meta.outputs.prerelease }} + artifact-name: ${{ steps.meta.outputs.artifact-name }} steps: - uses: actions/checkout@v5 - name: Download JARs @@ -59,6 +80,28 @@ jobs: with: name: release-jars-${{ github.sha }} path: ${{ runner.temp }}/release-jars + - name: Install JavaSMT packaging artifact + run: | + mkdir -p libs/java-library-path + cp "${RUNNER_TEMP}/release-jars/build/svcomp-runtime/java-smt-latest.jar" \ + libs/java-library-path/java-smt-latest.jar + - name: Download WitnessCreator runtime + run: | + version="${WITNESS_CREATOR_VERSION}" + zip_name="witness-creator-${version#v}.zip" + zip_path="${RUNNER_TEMP}/${zip_name}" + runtime_dir="${RUNNER_TEMP}/witness-creator-runtime" + + curl --fail --location --retry 3 \ + --output "${zip_path}" \ + "https://github.com/SWAT-project/WitnessCreator/releases/download/${version}/${zip_name}" + echo "${WITNESS_CREATOR_SHA256} ${zip_path}" | sha256sum --check - + + mkdir -p "${runtime_dir}" + unzip -q "${zip_path}" -d "${runtime_dir}" + test -f "${runtime_dir}/WitnessCreator/build/libs/WitnessCreator.jar" + test -f "${runtime_dir}/WitnessCreator/witnesses/default_violation.st" + test -f "${runtime_dir}/WitnessCreator/witnesses/witness.st" - name: Determine release channel id: meta run: | @@ -98,20 +141,27 @@ jobs: echo "channel=${channel}" echo "version=${version}" echo "zip-name=${zip_name}" + echo "artifact-name=swat-svcomp-${version}" echo "release=${release}" echo "rolling=${rolling}" echo "prerelease=${prerelease}" } >> "${GITHUB_OUTPUT}" - - name: Download SV-COMP reference runtime + - name: Build SV-COMP Python runtime + env: + VENV_DIR: ${{ runner.temp }}/svcomp-runtime/${{ env.SVCOMP_VENV_DIR_NAME }} run: | - curl --fail --location --retry 3 --output "${RUNNER_TEMP}/swat-verify.zip" "${SVCOMP_REFERENCE_URL}" - echo "${SVCOMP_REFERENCE_MD5} ${RUNNER_TEMP}/swat-verify.zip" | md5sum --check - - unzip -q "${RUNNER_TEMP}/swat-verify.zip" -d "${RUNNER_TEMP}/swat-reference" + mkdir -p "$(dirname "${VENV_DIR}")" + /usr/bin/python3 -m venv --copies "${VENV_DIR}" + "${VENV_DIR}/bin/python3" -m pip install --no-deps -r scripts/svcomp-package/requirements.txt + "${VENV_DIR}/bin/python3" -m pip check + "${VENV_DIR}/bin/python3" -m pip freeze --all > "${VENV_DIR}/requirements.freeze.txt" + "${VENV_DIR}/bin/python3" -c "import fastapi, pydantic, z3" - name: Pack SV-COMP ZIP env: SWAT_SVCOMP_VERSION: ${{ steps.meta.outputs.version }} SWAT_SVCOMP_ARTIFACT_DIR: ${{ runner.temp }}/release-jars - SWAT_SVCOMP_REFERENCE_DIR: ${{ runner.temp }}/swat-reference/swat-verify + SWAT_SVCOMP_RUNTIME_DIR: ${{ runner.temp }}/svcomp-runtime + SWAT_SVCOMP_WITNESS_CREATOR_DIR: ${{ runner.temp }}/witness-creator-runtime/WitnessCreator SWAT_SVCOMP_COMMIT: ${{ github.sha }} SWAT_SVCOMP_REF: ${{ github.ref_name }} SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }} @@ -119,19 +169,37 @@ jobs: - name: Upload SV-COMP ZIP artifact uses: actions/upload-artifact@v4 with: - name: swat-svcomp-${{ steps.meta.outputs.version }} + name: ${{ steps.meta.outputs.artifact-name }} path: build/distributions/${{ steps.meta.outputs.zip-name }} if-no-files-found: error + + publish-release: + needs: package + if: >- + github.event_name == 'push' && ( + github.ref == 'refs/heads/main' || + github.ref == 'refs/heads/dev' || + startsWith(github.ref, 'refs/tags/') + ) + runs-on: ubuntu-latest + permissions: + contents: write + steps: + - name: Download SV-COMP ZIP artifact + uses: actions/download-artifact@v4 + with: + name: ${{ needs.package.outputs.artifact-name }} + path: ${{ runner.temp }}/svcomp-package - name: Publish release - if: steps.meta.outputs.release == 'true' env: GH_TOKEN: ${{ github.token }} - CHANNEL: ${{ steps.meta.outputs.channel }} - ZIP_NAME: ${{ steps.meta.outputs.zip-name }} - ROLLING: ${{ steps.meta.outputs.rolling }} - PRERELEASE: ${{ steps.meta.outputs.prerelease }} + GH_REPO: ${{ github.repository }} + CHANNEL: ${{ needs.package.outputs.channel }} + ZIP_NAME: ${{ needs.package.outputs.zip-name }} + ROLLING: ${{ needs.package.outputs.rolling }} + PRERELEASE: ${{ needs.package.outputs.prerelease }} run: | - zip_path="build/distributions/${ZIP_NAME}" + zip_path="${RUNNER_TEMP}/svcomp-package/${ZIP_NAME}" notes="$(printf 'Automated SWAT SV-COMP package.\n\nRef: %s\nCommit: %s\nRun: %s/%s/actions/runs/%s\n' \ "$GITHUB_REF_NAME" "$GITHUB_SHA" "$GITHUB_SERVER_URL" "$GITHUB_REPOSITORY" "$GITHUB_RUN_ID")" @@ -221,4 +289,4 @@ jobs: java-version: '17' distribution: 'temurin' - name: Generate and submit dependency graph - uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 \ No newline at end of file + uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh index ee8ad2a..c3a5e78 100755 --- a/scripts/package-svcomp.sh +++ b/scripts/package-svcomp.sh @@ -9,15 +9,21 @@ set -euo pipefail # else. The artifact root must contain: # # - symbolic-executor/lib/symbolic-executor.jar -# - targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar # -# Set SWAT_SVCOMP_REFERENCE_DIR to the extracted Zenodo reference package root -# from https://zenodo.org/records/17748741. The reference root is used for the -# pinned SV-COMP Python environment and JavaSMT compatibility JAR: +# Set SWAT_SVCOMP_WITNESS_CREATOR_DIR to the extracted WitnessCreator runtime +# root from https://github.com/SWAT-project/WitnessCreator. The root must +# contain: +# +# - build/libs/WitnessCreator.jar +# - witnesses/default_violation.st +# - witnesses/witness.st +# +# Set SWAT_SVCOMP_RUNTIME_DIR to a runtime package root that contains the +# pinned SV-COMP Python environment: # # - .venv_ubuntu_24_04_1__x86_64/ # -# Z3 is taken from the vendored Linux distribution ZIP in this repository. +# Z3 and JavaSMT are taken from the vendored files in this repository. # ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" cd "$ROOT_DIR" @@ -32,13 +38,19 @@ PACKAGE_DIR="${WORK_DIR}/${PACKAGE_NAME}" DIST_DIR="${ROOT_DIR}/build/distributions" SUPPORT_DIR="${ROOT_DIR}/scripts/svcomp-package" ARTIFACT_DIR="$(cd "${SWAT_SVCOMP_ARTIFACT_DIR:-$ROOT_DIR}" && pwd)" -REFERENCE_DIR="${SWAT_SVCOMP_REFERENCE_DIR:-}" +RUNTIME_DIR="${SWAT_SVCOMP_RUNTIME_DIR:-${SWAT_SVCOMP_REFERENCE_DIR:-}}" +WITNESS_CREATOR_DIR="${SWAT_SVCOMP_WITNESS_CREATOR_DIR:-}" VENV_DIR_NAME="${SWAT_SVCOMP_VENV_DIR_NAME:-.venv_ubuntu_24_04_1__x86_64}" LINUX_Z3_DIST="z3-4.15.4-x64-glibc-2.39" LINUX_Z3_ZIP="${ROOT_DIR}/libs/${LINUX_Z3_DIST}.zip" +JAVA_SMT_JAR="${ROOT_DIR}/libs/java-library-path/java-smt-latest.jar" -if [[ -n "$REFERENCE_DIR" ]]; then - REFERENCE_DIR="$(cd "$REFERENCE_DIR" && pwd)" +if [[ -n "$RUNTIME_DIR" ]]; then + RUNTIME_DIR="$(cd "$RUNTIME_DIR" && pwd)" +fi + +if [[ -n "$WITNESS_CREATOR_DIR" ]]; then + WITNESS_CREATOR_DIR="$(cd "$WITNESS_CREATOR_DIR" && pwd)" fi fail() { @@ -46,22 +58,6 @@ fail() { exit 1 } -artifact_file() { - local rel="$1" - local path="${ARTIFACT_DIR}/${rel}" - [[ -f "$path" ]] || fail "missing built artifact file: ${path}" - printf '%s\n' "$path" -} - -reference_file() { - local rel="$1" - [[ -n "$REFERENCE_DIR" ]] || fail "SWAT_SVCOMP_REFERENCE_DIR is required for ${rel}" - - local path="${REFERENCE_DIR}/${rel}" - [[ -f "$path" ]] || fail "missing Zenodo reference file: ${path}" - printf '%s\n' "$path" -} - first_artifact_file() { local path for rel in "$@"; do @@ -137,6 +133,7 @@ install -m 0755 "$SUPPORT_DIR/run-swat.sh" "$PACKAGE_DIR/run-swat.sh" install -m 0755 "$SUPPORT_DIR/compile-target.sh" "$PACKAGE_DIR/compile-target.sh" install -m 0755 "$SUPPORT_DIR/smoketest.sh" "$PACKAGE_DIR/smoketest.sh" install -m 0755 "$SUPPORT_DIR/run_swat.py" "$PACKAGE_DIR/run_swat.py" +install -m 0644 "$SUPPORT_DIR/requirements.txt" "$PACKAGE_DIR/requirements.txt" install -m 0644 targets/sv-comp/sv-comp.cfg "$PACKAGE_DIR/sv-comp.cfg" EXECUTOR_JAR="$(first_artifact_file \ @@ -146,24 +143,24 @@ copy_artifact_file "$EXECUTOR_JAR" "$PACKAGE_DIR/symbolic-executor/lib/symbolic- copy_tree_files symbolic-explorer "$PACKAGE_DIR/symbolic-explorer" -WITNESS_CREATOR_JAR="$(artifact_file targets/sv-comp/WitnessCreator/build/libs/WitnessCreator.jar)" -copy_artifact_file "$WITNESS_CREATOR_JAR" "$PACKAGE_DIR/WitnessCreator/build/libs/WitnessCreator.jar" -mkdir -p "$PACKAGE_DIR/WitnessCreator/witnesses" -install -m 0644 targets/sv-comp/WitnessCreator/witnesses/default_violation.st "$PACKAGE_DIR/WitnessCreator/witnesses/default_violation.st" -install -m 0644 targets/sv-comp/WitnessCreator/witnesses/witness.st "$PACKAGE_DIR/WitnessCreator/witnesses/witness.st" +[[ -n "$WITNESS_CREATOR_DIR" ]] || fail "SWAT_SVCOMP_WITNESS_CREATOR_DIR must point to the extracted WitnessCreator runtime root" +[[ -f "$WITNESS_CREATOR_DIR/build/libs/WitnessCreator.jar" ]] || fail "missing WitnessCreator JAR: ${WITNESS_CREATOR_DIR}/build/libs/WitnessCreator.jar" +[[ -f "$WITNESS_CREATOR_DIR/witnesses/default_violation.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/default_violation.st" +[[ -f "$WITNESS_CREATOR_DIR/witnesses/witness.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/witness.st" +copy_artifact_tree "$WITNESS_CREATOR_DIR" "$PACKAGE_DIR/WitnessCreator" install_z3_runtime_file z3 0755 install_z3_runtime_file libz3.so install_z3_runtime_file libz3java.so install_z3_runtime_file com.microsoft.z3.jar install_z3_runtime_file libz3.a -JAVA_SMT_JAR="$(reference_file libs/java-library-path/java-smt-latest.jar)" +[[ -f "$JAVA_SMT_JAR" ]] || fail "missing JavaSMT JAR: ${JAVA_SMT_JAR}" copy_artifact_file "$JAVA_SMT_JAR" "$PACKAGE_DIR/libs/java-library-path/java-smt-latest.jar" copy_tree_files "$SUPPORT_DIR/smoketest" "$PACKAGE_DIR/smoketest" -[[ -n "$REFERENCE_DIR" ]] || fail "SWAT_SVCOMP_REFERENCE_DIR must point to the extracted Zenodo package root for ${VENV_DIR_NAME}" -copy_artifact_tree "${REFERENCE_DIR}/${VENV_DIR_NAME}" "${PACKAGE_DIR}/${VENV_DIR_NAME}" +[[ -n "$RUNTIME_DIR" ]] || fail "SWAT_SVCOMP_RUNTIME_DIR must point to a runtime package root containing ${VENV_DIR_NAME}" +copy_artifact_tree "${RUNTIME_DIR}/${VENV_DIR_NAME}" "${PACKAGE_DIR}/${VENV_DIR_NAME}" mkdir -p "$DIST_DIR" ZIP_PATH="${DIST_DIR}/${PACKAGE_NAME}.zip" diff --git a/scripts/svcomp-package/requirements.txt b/scripts/svcomp-package/requirements.txt new file mode 100644 index 0000000..5c32b0a --- /dev/null +++ b/scripts/svcomp-package/requirements.txt @@ -0,0 +1,19 @@ +annotated-types==0.7.0 +anyio==4.6.2.post1 +boto==2.49.0 +certifi==2025.11.12 +charset-normalizer==3.4.4 +click==8.1.7 +fastapi==0.115.5 +h11==0.14.0 +idna==3.10 +pydantic==2.10.0 +pydantic_core==2.27.0 +PyYAML==6.0.2 +requests==2.32.5 +sniffio==1.3.1 +starlette==0.41.3 +typing_extensions==4.12.2 +urllib3==2.5.0 +uvicorn==0.32.1 +z3-solver==4.15.4.0 diff --git a/scripts/svcomp-package/run-swat.sh b/scripts/svcomp-package/run-swat.sh index fc21ac2..424a318 100755 --- a/scripts/svcomp-package/run-swat.sh +++ b/scripts/svcomp-package/run-swat.sh @@ -60,7 +60,13 @@ done SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -source "$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/activate" +VENV_PYTHON="$SCRIPT_DIR/.venv_ubuntu_24_04_1__x86_64/bin/python3" + +if [ ! -x "$VENV_PYTHON" ]; then + echo "Error: Python runtime not found at $VENV_PYTHON" + exit 1 +fi + echo "Running SWAT with arguments: $@" -python3 -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1 -cat out.log \ No newline at end of file +"$VENV_PYTHON" -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1 +cat out.log diff --git a/settings.gradle b/settings.gradle index defcd23..2f822f5 100644 --- a/settings.gradle +++ b/settings.gradle @@ -6,7 +6,6 @@ rootProject.name = "SWAT" include 'symbolic-executor' include 'annotations' -include 'targets:sv-comp:WitnessCreator' include 'targets:instruction-tests:IFXX' include 'targets:instruction-tests:I2X' @@ -83,4 +82,4 @@ dependencyResolutionManagement { include 'targets:applications:modelmapper-test-app' findProject(':targets:applications:modelmapper-test-app')?.name = 'modelmapper-test-app' include 'targets:applications:reflection-test-app' -findProject(':targets:applications:reflection-test-app')?.name = 'reflection-test-app' \ No newline at end of file +findProject(':targets:applications:reflection-test-app')?.name = 'reflection-test-app' diff --git a/targets/sv-comp/WitnessCreator/build.gradle b/targets/sv-comp/WitnessCreator/build.gradle deleted file mode 100755 index 78e0867..0000000 --- a/targets/sv-comp/WitnessCreator/build.gradle +++ /dev/null @@ -1,44 +0,0 @@ -buildscript { - repositories { - gradlePluginPortal() - } - dependencies { - classpath 'com.github.johnrengelman:shadow:8.1.1' - } -} - -plugins { - id 'java' - id 'com.github.johnrengelman.shadow' version '8.1.1' -} - -group = 'org.example' -version = '1.0-SNAPSHOT' - -apply plugin: 'com.github.johnrengelman.shadow' -apply plugin: 'java' - -shadowJar { - archiveBaseName.set('WitnessCreator') - archiveClassifier.set('') - archiveVersion.set('') -} - -repositories { - mavenCentral() -} - -dependencies { - - implementation 'org.antlr:ST4:4.3.4' - -} - - -jar { - manifest { - attributes( - 'Main-Class': 'App' - ) - } -} \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/src/main/java/App.java b/targets/sv-comp/WitnessCreator/src/main/java/App.java deleted file mode 100755 index 37f7d43..0000000 --- a/targets/sv-comp/WitnessCreator/src/main/java/App.java +++ /dev/null @@ -1,180 +0,0 @@ -import java.io.BufferedReader; -import java.io.IOException; -import java.io.InputStream; -import java.io.InputStreamReader; -import java.nio.file.Files; -import java.nio.file.Paths; -import java.util.ArrayList; -import java.util.Base64; -import java.util.LinkedList; -import java.util.List; - -import org.stringtemplate.v4.ST; -import org.stringtemplate.v4.STGroup; -import org.stringtemplate.v4.STRawGroupDir; - -import witness.WitnessAssumption; -import witness.WitnessEdge; -import witness.WitnessNode; - -public class App { - - public static void main(String[] args) { - - - String path = args[1]; - System.out.println("source path: " + path); - - List witness = new LinkedList<>(); - if(args[0].trim().length() == 0) { - System.out.println("No witness record, assuming default assertion violation"); - (new App()).saveDefaultviolationWitness(path); - } else { - String param = new String(Base64.getDecoder().decode(args[0])); - String[] lines = param.split("\n"); - for (String line : lines) { - line = line.substring(line.indexOf("[WITNESS]") + 10).trim(); - // decode line base64 - byte[] decodedBytes = Base64.getDecoder().decode(line); - line = new String(decodedBytes); - - String[] parts = line.split("@@@"); - if (parts.length != 4) { - System.out.println("Received line:" + line); - throw new RuntimeException("Invalid witness line: " + line); - } - - String value = parts[0].trim(); - int lineNumber = Integer.parseInt(parts[1].trim()); // account for 0-based line numbers - String className = parts[2].trim(); - String description = parts[3].trim(); - - // Escape XML special characters in scope to avoid XML parse errors - // (e.g., contains angle brackets that break XML parsing) - String scope = "L" + className + ";." + description; - scope = scope.replace("&", "&").replace("<", "<").replace(">", ">"); - witness.add(new WitnessAssumption(value, className + ".java", scope, lineNumber)); - } - (new App()).checkAndSaveWitness(path, witness); - } - } - - - - private void saveDefaultviolationWitness(String path){ - STGroup group = new STRawGroupDir("witnesses", '$','$'); - ST st = group.getInstanceOf("default_violation"); - String result = st.render(); - try { - System.out.println("Writing default violation witness to file: " + path + "/" + "witness.graphml"); - Files.write(Paths.get(path + "/" + "witness.graphml"), result.getBytes()); - } catch (IOException e) { - System.err.println("Error writing witness to file: " + e.getMessage()); - } - } - private void checkAndSaveWitness(String path, List witness) { - - - List nodes = new ArrayList<>(); - List edges = new ArrayList<>(); - - int nodeId = 0; - WitnessNode initNode = new WitnessNode(nodeId++); - nodes.add(initNode); - initNode.addData("entry", "true"); - WitnessNode curNode = initNode; - - for (WitnessAssumption wa : witness) { - String loc = getLineOfCode(path, wa.getClazz(), wa.getLine()); - String assumption = computeAssumption(loc, wa); - - WitnessNode prevNode = curNode; - curNode = new WitnessNode(nodeId++); - nodes.add(curNode); - WitnessEdge edge = new WitnessEdge(prevNode, wa, assumption, curNode); - edges.add(edge); - } - - curNode.addData("violation", "true"); - - STGroup group = new STRawGroupDir("witnesses", '$','$'); - ST st = group.getInstanceOf("witness"); - st.add("nodes", nodes); - st.add("edges", edges); - String result = st.render(); - try { - System.out.println("Writing violation witness to file: " + path + "/" + "witness.graphml"); - Files.write(Paths.get(path + "/" + "witness.graphml"), result.getBytes()); - } catch (IOException e) { - System.out.println("Error writing witness to file: " + e.getMessage()); - } - } - - private String getLineOfCode(String path, String filename, int line) { - String absolutePath = path + "/" + filename; - try { - // Open absolutePath as a stream - InputStream is = Files.newInputStream(Paths.get(absolutePath)); - if (is == null) { - System.out.println("Could not find file: " + absolutePath); - return null; - } - BufferedReader res = new BufferedReader(new InputStreamReader(is)); - String loc = ""; - for (int i = 0; i 0 && lineOfCode.charAt(idx - 1) == '=') { - // This is a comparison like "if (pos == ..." - no variable assignment - return wa.getValue(); - } - lineOfCode = lineOfCode.substring(0, idx).trim(); - String[] parts = lineOfCode.split(" "); - String id = parts[parts.length-1].trim(); - - // For string types, always use .equals() format with properly quoted value - if (isStringType) { - String value = wa.getValue(); - // Add quotes around the value if not already present - if (!value.startsWith("\"")) { - // Escape any quotes and backslashes within the string value - value = value.replace("\\", "\\\\").replace("\"", "\\\""); - value = "\"" + value + "\""; - } - return id + ".equals(" + value + ")"; - } - - // For primitive types, use assignment format - return id + " = " + wa.getValue(); - } - -} \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java deleted file mode 100755 index d841c67..0000000 --- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessAssumption.java +++ /dev/null @@ -1,33 +0,0 @@ -package witness; - -public class WitnessAssumption { - - private String scope; - private String value; - private final String clazz; - private final int line; - - public WitnessAssumption(String value, String clazz, String scope, int line) { - this.scope = scope; - this.value = value; - this.clazz = clazz; - this.line = line; - } - - public String getScope() { - return scope; - } - - public String getValue() { - return value; - } - - public String getClazz() { - return clazz; - } - - public int getLine() { - return line; - } - -} diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java deleted file mode 100755 index 47fc961..0000000 --- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessEdge.java +++ /dev/null @@ -1,35 +0,0 @@ -package witness; - -public class WitnessEdge { - - private final WitnessNode source; - - private final WitnessNode dest; - - private final WitnessAssumption witness; - - private final String assumption; - - public WitnessEdge(WitnessNode source, WitnessAssumption witness, String assumption, WitnessNode dest) { - this.source = source; - this.dest = dest; - this.witness = witness; - this.assumption = assumption; - } - - public WitnessNode getSource() { - return source; - } - - public WitnessNode getDest() { - return dest; - } - - public WitnessAssumption getWitness() { - return witness; - } - - public String getAssumption() { - return assumption; - } -} \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java b/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java deleted file mode 100755 index 8ccc62e..0000000 --- a/targets/sv-comp/WitnessCreator/src/main/java/witness/WitnessNode.java +++ /dev/null @@ -1,29 +0,0 @@ -package witness; - -import java.util.HashMap; -import java.util.Map; - -public class WitnessNode { - - private final int id; - - private final Map data; - - public WitnessNode(int id) { - this.id = id; - this.data = new HashMap<>(); - } - - public int getId() { - return id; - } - - public Map getData() { - return data; - } - - public void addData(String key, String value) { - this.data.put(key, value); - } - -} \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/witness.graphml b/targets/sv-comp/WitnessCreator/witness.graphml deleted file mode 100644 index 99e9ee6..0000000 --- a/targets/sv-comp/WitnessCreator/witness.graphml +++ /dev/null @@ -1,134 +0,0 @@ - - - - <command-line> - - - - - false - - - false - - - false - - - false - - - false - - - 0 - - - 0 - - - - - - - - - - - - - - - - - violation_witness - SWAT - - - - - true - - - - - - - - - - - - - - - - - - - true - - - - - Main.java - 12 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 13 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 14 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 15 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 16 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 17 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 18 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 19 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - Main.java - 20 - 0 - true - java::LMain;.main([Ljava/lang/String;)V - - - - \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/witnesses/default_violation.st b/targets/sv-comp/WitnessCreator/witnesses/default_violation.st deleted file mode 100755 index 81cb4a6..0000000 --- a/targets/sv-comp/WitnessCreator/witnesses/default_violation.st +++ /dev/null @@ -1,56 +0,0 @@ - - - - <command-line> - - - - - false - - - false - - - false - - - false - - - false - - - 0 - - - 0 - - - - - - - - - - - - - - - - - violation_witness - SWAT - - - - true true - - - \ No newline at end of file diff --git a/targets/sv-comp/WitnessCreator/witnesses/witness.st b/targets/sv-comp/WitnessCreator/witnesses/witness.st deleted file mode 100755 index 6e7e57a..0000000 --- a/targets/sv-comp/WitnessCreator/witnesses/witness.st +++ /dev/null @@ -1,70 +0,0 @@ - - - - <command-line> - - - - - false - - - false - - - false - - - false - - - false - - - 0 - - - 0 - - - - - - - - - - - - - - - - - violation_witness - SWAT - - - - $nodes:{ n | - - $n.data.keys:{k | - $n.data.(k)$ }$ - - }$ - - $edges:{ e | - - $e.witness.clazz$ - $e.witness.line$ - 0 - $e.assumption$ - java::$e.witness.scope$ - }$ - - - \ No newline at end of file