Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
209 changes: 208 additions & 1 deletion .github/workflows/gradle.yml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,12 @@ name: Java CI with Gradle
on:
push:
pull_request:
workflow_dispatch:

env:
SVCOMP_VENV_DIR_NAME: .venv_ubuntu_24_04_1__x86_64
WITNESS_CREATOR_VERSION: v0.1.1
WITNESS_CREATOR_SHA256: 8fc8810237c99bf7d709bdb8692142695e407b5681e818fcfe8b45f9c598d814

jobs:
build:
Expand All @@ -18,8 +24,209 @@ jobs:
distribution: 'temurin'
- name: Setup Gradle
uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4
- name: Prepare Solver Dependencies
run: ./gradlew copyNativeLibs
- name: Build
run: ./gradlew build -x test
run: ./gradlew --no-daemon build -x test
- name: Collect JavaSMT JAR
run: |
java_smt_dir="${HOME}/.gradle/caches/modules-2/files-2.1/org.sosy-lab/java-smt"
if [[ ! -d "$java_smt_dir" ]]; then
echo "JavaSMT Gradle cache directory not found: $java_smt_dir" >&2
exit 1
fi

java_smt_jar="$(find "$java_smt_dir" -type f -name 'java-smt-*.jar' ! -name '*-sources.jar' ! -name '*-javadoc.jar' | sort | tail -n 1)"
if [[ -z "$java_smt_jar" ]]; then
echo "JavaSMT JAR not found in Gradle cache: $java_smt_dir" >&2
exit 1
fi

mkdir -p build/svcomp-runtime
cp "$java_smt_jar" build/svcomp-runtime/java-smt-latest.jar
- name: Upload JARs
uses: actions/upload-artifact@v4
with:
name: release-jars-${{ github.sha }}
path: |
symbolic-executor/lib/symbolic-executor.jar
build/svcomp-runtime/java-smt-latest.jar
if-no-files-found: error
retention-days: 1

package:
needs: build
if: >-
github.event_name == 'pull_request' ||
github.event_name == 'workflow_dispatch' ||
(github.event_name == 'push' && (
github.ref == 'refs/heads/main' ||
github.ref == 'refs/heads/dev' ||
startsWith(github.ref, 'refs/tags/')
))
runs-on: ubuntu-24.04
permissions:
contents: read
outputs:
channel: ${{ steps.meta.outputs.channel }}
zip-name: ${{ steps.meta.outputs.zip-name }}
rolling: ${{ steps.meta.outputs.rolling }}
prerelease: ${{ steps.meta.outputs.prerelease }}
artifact-name: ${{ steps.meta.outputs.artifact-name }}
steps:
- uses: actions/checkout@v5
- name: Download JARs
uses: actions/download-artifact@v4
with:
name: release-jars-${{ github.sha }}
path: ${{ runner.temp }}/release-jars
- name: Install JavaSMT packaging artifact
run: |
mkdir -p libs/java-library-path
cp "${RUNNER_TEMP}/release-jars/build/svcomp-runtime/java-smt-latest.jar" \
libs/java-library-path/java-smt-latest.jar
- name: Download WitnessCreator runtime
run: |
version="${WITNESS_CREATOR_VERSION}"
zip_name="witness-creator-${version#v}.zip"
zip_path="${RUNNER_TEMP}/${zip_name}"
runtime_dir="${RUNNER_TEMP}/witness-creator-runtime"

curl --fail --location --retry 3 \
--output "${zip_path}" \
"https://github.com/SWAT-project/WitnessCreator/releases/download/${version}/${zip_name}"
echo "${WITNESS_CREATOR_SHA256} ${zip_path}" | sha256sum --check -

mkdir -p "${runtime_dir}"
unzip -q "${zip_path}" -d "${runtime_dir}"
test -f "${runtime_dir}/WitnessCreator/build/libs/WitnessCreator.jar"
test -f "${runtime_dir}/WitnessCreator/witnesses/default_violation.st"
test -f "${runtime_dir}/WitnessCreator/witnesses/witness.st"
- name: Determine release channel
id: meta
run: |
ref_type="${GITHUB_REF_TYPE}"
ref_name="${GITHUB_REF_NAME}"
sha_short="${GITHUB_SHA::7}"

channel="" # release/tag name; empty -> build artifact only, no release
release="false"
rolling="false" # rolling channels move their tag to the current commit
prerelease="false"

if [[ "$ref_type" == "tag" ]]; then
channel="$ref_name"
release="true"
elif [[ "$ref_name" == "main" ]]; then
channel="latest"
release="true"
rolling="true"
elif [[ "$ref_name" == "dev" ]]; then
channel="latest-dev"
release="true"
rolling="true"
prerelease="true"
fi

# Channel-stable asset name gives the nightly cron a fixed download URL;
# the exact commit is recorded in the release notes and BUILD_INFO.txt.
if [[ -n "$channel" ]]; then
version="$channel"
else
version="$sha_short"
fi
zip_name="swat-svcomp-${version}.zip"

{
echo "channel=${channel}"
echo "version=${version}"
echo "zip-name=${zip_name}"
echo "artifact-name=swat-svcomp-${version}"
echo "release=${release}"
echo "rolling=${rolling}"
echo "prerelease=${prerelease}"
} >> "${GITHUB_OUTPUT}"
- name: Build SV-COMP Python runtime
env:
VENV_DIR: ${{ runner.temp }}/svcomp-runtime/${{ env.SVCOMP_VENV_DIR_NAME }}
run: |
mkdir -p "$(dirname "${VENV_DIR}")"
/usr/bin/python3 -m venv --copies "${VENV_DIR}"
"${VENV_DIR}/bin/python3" -m pip install --no-deps -r scripts/svcomp-package/requirements.txt
"${VENV_DIR}/bin/python3" -m pip check
"${VENV_DIR}/bin/python3" -m pip freeze --all > "${VENV_DIR}/requirements.freeze.txt"
"${VENV_DIR}/bin/python3" -c "import fastapi, pydantic, z3"
- name: Pack SV-COMP ZIP
env:
SWAT_SVCOMP_VERSION: ${{ steps.meta.outputs.version }}
SWAT_SVCOMP_ARTIFACT_DIR: ${{ runner.temp }}/release-jars
SWAT_SVCOMP_RUNTIME_DIR: ${{ runner.temp }}/svcomp-runtime
SWAT_SVCOMP_WITNESS_CREATOR_DIR: ${{ runner.temp }}/witness-creator-runtime/WitnessCreator
SWAT_SVCOMP_COMMIT: ${{ github.sha }}
SWAT_SVCOMP_REF: ${{ github.ref_name }}
SWAT_SVCOMP_CHANNEL: ${{ steps.meta.outputs.channel }}
run: scripts/package-svcomp.sh
- name: Upload SV-COMP ZIP artifact
uses: actions/upload-artifact@v4
with:
name: ${{ steps.meta.outputs.artifact-name }}
path: build/distributions/${{ steps.meta.outputs.zip-name }}
if-no-files-found: error

publish-release:
needs: package
if: >-
github.event_name == 'push' && (
github.ref == 'refs/heads/main' ||
github.ref == 'refs/heads/dev' ||
startsWith(github.ref, 'refs/tags/')
)
runs-on: ubuntu-latest
permissions:
contents: write
steps:
- name: Download SV-COMP ZIP artifact
uses: actions/download-artifact@v4
with:
name: ${{ needs.package.outputs.artifact-name }}
path: ${{ runner.temp }}/svcomp-package
- name: Publish release
env:
GH_TOKEN: ${{ github.token }}
GH_REPO: ${{ github.repository }}
CHANNEL: ${{ needs.package.outputs.channel }}
ZIP_NAME: ${{ needs.package.outputs.zip-name }}
ROLLING: ${{ needs.package.outputs.rolling }}
PRERELEASE: ${{ needs.package.outputs.prerelease }}
run: |
zip_path="${RUNNER_TEMP}/svcomp-package/${ZIP_NAME}"
notes="$(printf 'Automated SWAT SV-COMP package.\n\nRef: %s\nCommit: %s\nRun: %s/%s/actions/runs/%s\n' \
"$GITHUB_REF_NAME" "$GITHUB_SHA" "$GITHUB_SERVER_URL" "$GITHUB_REPOSITORY" "$GITHUB_RUN_ID")"

prerelease_flag=()
[[ "$PRERELEASE" == "true" ]] && prerelease_flag=(--prerelease)

if [[ "$ROLLING" == "true" ]]; then
# Refresh the rolling channel: drop the old release + tag, then recreate
# it at the current commit so the tag always tracks the channel head.
# Uses the default GITHUB_TOKEN, so the new tag does not retrigger CI.
gh release delete "$CHANNEL" --yes --cleanup-tag 2>/dev/null || true
gh release create "$CHANNEL" "$zip_path" \
--target "$GITHUB_SHA" \
--title "SWAT ${CHANNEL} (${GITHUB_SHA::7})" \
--notes "$notes" \
"${prerelease_flag[@]}"
else
# Permanent, version-tagged release (the tag already points at this commit).
if gh release view "$CHANNEL" >/dev/null 2>&1; then
gh release upload "$CHANNEL" "$zip_path" --clobber
else
gh release create "$CHANNEL" "$zip_path" \
--title "SWAT ${CHANNEL}" \
--notes "$notes" \
"${prerelease_flag[@]}"
fi
fi

test:
needs: build
Expand Down
Loading
Loading