Ci/sv comp zip

.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,38 +28,80 @@ 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
       uses: actions/download-artifact@v4
       with:
         name: release-jars-${{ github.sha }}
         path: ${{ runner.temp }}/release-jars
+    - name: Install JavaSMT packaging artifact
+      run: |
+        mkdir -p libs/java-library-path
+        cp "${RUNNER_TEMP}/release-jars/build/svcomp-runtime/java-smt-latest.jar" \
+          libs/java-library-path/java-smt-latest.jar
+    - name: Download WitnessCreator runtime
+      run: |
+        version="${WITNESS_CREATOR_VERSION}"
+        zip_name="witness-creator-${version#v}.zip"
+        zip_path="${RUNNER_TEMP}/${zip_name}"
+        runtime_dir="${RUNNER_TEMP}/witness-creator-runtime"
+
+        curl --fail --location --retry 3 \
+          --output "${zip_path}" \
+          "https://github.com/SWAT-project/WitnessCreator/releases/download/${version}/${zip_name}"
+        echo "${WITNESS_CREATOR_SHA256}  ${zip_path}" | sha256sum --check -
+
+        mkdir -p "${runtime_dir}"
+        unzip -q "${zip_path}" -d "${runtime_dir}"
+        test -f "${runtime_dir}/WitnessCreator/build/libs/WitnessCreator.jar"
+        test -f "${runtime_dir}/WitnessCreator/witnesses/default_violation.st"
+        test -f "${runtime_dir}/WitnessCreator/witnesses/witness.st"
     - name: Determine release channel
       id: meta
       run: |
@@ -98,40 +141,65 @@ 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 }}
       run: scripts/package-svcomp.sh
     - 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
+      uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4

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,36 +38,26 @@ 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() {
   echo "error: $*" >&2
   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"

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

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
+"$VENV_PYTHON" -u "$SCRIPT_DIR/run_swat.py" "$@" > out.log 2>&1
+cat out.log

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'
+findProject(':targets:applications:reflection-test-app')?.name = 'reflection-test-app'