fix(explorer): fall back to concrete trace values in annotation Targe… #119
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Java CI with Gradle | |
| on: | |
| push: | |
| pull_request: | |
| workflow_dispatch: | |
| env: | |
| SVCOMP_REFERENCE_URL: https://zenodo.org/api/records/17748741/files/swat-verify.zip/content | |
| SVCOMP_REFERENCE_MD5: 8c776d19ac33ecf5c1c7441d16cc18a6 | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Set up JDK 17 | |
| uses: actions/setup-java@v4 | |
| with: | |
| java-version: '17' | |
| distribution: 'temurin' | |
| - name: Setup Gradle | |
| uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 | |
| - name: Prepare Solver Dependencies | |
| 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: 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 | |
| if-no-files-found: error | |
| retention-days: 1 | |
| package: | |
| needs: build | |
| if: >- | |
| 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 | |
| permissions: | |
| contents: write | |
| 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: Determine release channel | |
| id: meta | |
| run: | | |
| ref_type="${GITHUB_REF_TYPE}" | |
| ref_name="${GITHUB_REF_NAME}" | |
| sha_short="${GITHUB_SHA::7}" | |
| channel="" # release/tag name; empty -> build artifact only, no release | |
| release="false" | |
| rolling="false" # rolling channels move their tag to the current commit | |
| prerelease="false" | |
| if [[ "$ref_type" == "tag" ]]; then | |
| channel="$ref_name" | |
| release="true" | |
| elif [[ "$ref_name" == "main" ]]; then | |
| channel="latest" | |
| release="true" | |
| rolling="true" | |
| elif [[ "$ref_name" == "dev" ]]; then | |
| channel="latest-dev" | |
| release="true" | |
| rolling="true" | |
| prerelease="true" | |
| fi | |
| # Channel-stable asset name gives the nightly cron a fixed download URL; | |
| # the exact commit is recorded in the release notes and BUILD_INFO.txt. | |
| if [[ -n "$channel" ]]; then | |
| version="$channel" | |
| else | |
| version="$sha_short" | |
| fi | |
| zip_name="swat-svcomp-${version}.zip" | |
| { | |
| echo "channel=${channel}" | |
| echo "version=${version}" | |
| echo "zip-name=${zip_name}" | |
| echo "release=${release}" | |
| echo "rolling=${rolling}" | |
| echo "prerelease=${prerelease}" | |
| } >> "${GITHUB_OUTPUT}" | |
| - name: Download SV-COMP reference runtime | |
| 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" | |
| - 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_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 }} | |
| path: build/distributions/${{ steps.meta.outputs.zip-name }} | |
| if-no-files-found: error | |
| - 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 }} | |
| run: | | |
| zip_path="build/distributions/${ZIP_NAME}" | |
| notes="$(printf 'Automated SWAT SV-COMP package.\n\nRef: %s\nCommit: %s\nRun: %s/%s/actions/runs/%s\n' \ | |
| "$GITHUB_REF_NAME" "$GITHUB_SHA" "$GITHUB_SERVER_URL" "$GITHUB_REPOSITORY" "$GITHUB_RUN_ID")" | |
| prerelease_flag=() | |
| [[ "$PRERELEASE" == "true" ]] && prerelease_flag=(--prerelease) | |
| if [[ "$ROLLING" == "true" ]]; then | |
| # Refresh the rolling channel: drop the old release + tag, then recreate | |
| # it at the current commit so the tag always tracks the channel head. | |
| # Uses the default GITHUB_TOKEN, so the new tag does not retrigger CI. | |
| gh release delete "$CHANNEL" --yes --cleanup-tag 2>/dev/null || true | |
| gh release create "$CHANNEL" "$zip_path" \ | |
| --target "$GITHUB_SHA" \ | |
| --title "SWAT ${CHANNEL} (${GITHUB_SHA::7})" \ | |
| --notes "$notes" \ | |
| "${prerelease_flag[@]}" | |
| else | |
| # Permanent, version-tagged release (the tag already points at this commit). | |
| if gh release view "$CHANNEL" >/dev/null 2>&1; then | |
| gh release upload "$CHANNEL" "$zip_path" --clobber | |
| else | |
| gh release create "$CHANNEL" "$zip_path" \ | |
| --title "SWAT ${CHANNEL}" \ | |
| --notes "$notes" \ | |
| "${prerelease_flag[@]}" | |
| fi | |
| fi | |
| test: | |
| needs: build | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Set up JDK 17 | |
| uses: actions/setup-java@v4 | |
| with: | |
| java-version: '17' | |
| distribution: 'temurin' | |
| - name: Setup Gradle | |
| uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 | |
| - name: Copy Z3 | |
| run: ./gradlew copyNativeLibs | |
| - name: Test | |
| run: ./gradlew test | |
| - name: Upload test reports | |
| if: failure() | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: test-reports | |
| path: symbolic-executor/build/reports/tests | |
| javadoc: | |
| needs: build | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Set up JDK 17 | |
| uses: actions/setup-java@v4 | |
| with: | |
| java-version: '17' | |
| distribution: 'temurin' | |
| - name: Setup Gradle | |
| uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 | |
| - name: Generate Javadoc | |
| run: ./gradlew :symbolic-executor:javadoc | |
| - name: Upload Javadoc | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: javadoc | |
| path: symbolic-executor/build/docs/javadoc | |
| dependency-submission: | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: write | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Set up JDK 17 | |
| uses: actions/setup-java@v4 | |
| with: | |
| java-version: '17' | |
| distribution: 'temurin' | |
| - name: Generate and submit dependency graph | |
| uses: gradle/actions/dependency-submission@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4 |