diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 65c9273f..0ce97bd5 100644 --- a/.github/workflows/gradle.yml +++ b/.github/workflows/gradle.yml @@ -51,6 +51,10 @@ jobs: path: | symbolic-executor/lib/symbolic-executor.jar build/svcomp-runtime/java-smt-latest.jar + libs/java-library-path/com.microsoft.z3.jar + libs/java-library-path/libz3.so + libs/java-library-path/libz3java.so + libs/java-library-path/libz3.a if-no-files-found: error retention-days: 1 @@ -85,6 +89,11 @@ jobs: 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 + cp "${RUNNER_TEMP}/release-jars/libs/java-library-path/com.microsoft.z3.jar" \ + "${RUNNER_TEMP}/release-jars/libs/java-library-path/libz3.so" \ + "${RUNNER_TEMP}/release-jars/libs/java-library-path/libz3java.so" \ + "${RUNNER_TEMP}/release-jars/libs/java-library-path/libz3.a" \ + libs/java-library-path/ - name: Download WitnessCreator runtime run: | version="${WITNESS_CREATOR_VERSION}" diff --git a/build.gradle b/build.gradle index 9dfa1969..ac8ef03a 100644 --- a/build.gradle +++ b/build.gradle @@ -4,56 +4,82 @@ plugins { id 'com.diffplug.spotless' version '6.9.0' } -tasks.register('copyNativeLibs', Copy) { // copies correct native z3 files to libs/ - def osArchMap = [ - 'windows-x64': 'z3-4.15.4-x64-win', - 'windows-x86': 'z3-4.15.4-x86-win', - 'osx-x64' : 'z3-4.15.4-x64-osx-13.7.6', - 'osx-arm64' : 'z3-4.15.4-arm64-osx-13.7.6', - 'linux-x64' : 'z3-4.15.4-x64-glibc-2.39', - 'linux-arm64': 'z3-4.15.4-arm64-glibc-2.34' - ] - - def os = OperatingSystem.current() - println("Operating system: $os") - - def arch = System.getProperty("os.arch") // Use Java system property to get architecture - println("Architecture: $arch") - - - def osKey = '' - switch (os) { - case OperatingSystem.LINUX: - osKey = arch == "aarch64" ? "linux-arm64" : "linux-x64" - break; - case OperatingSystem.MAC_OS: - osKey = arch == "aarch64" ? "osx-arm64" : "osx-x64" - break; - case OperatingSystem.WINDOWS: - osKey = arch == "x86" ? "windows-x86" : "windows-x64" - break; - } - println("Operating system key: $osKey") - if (!osKey) { - throw new GradleException("Unsupported operating system or architecture.") - } +ext { + z3Version = libs.versions.z3.get() + z3NativeDir = layout.projectDirectory.dir('libs/java-library-path') +} + +def z3Platform() { + def os = OperatingSystem.current() + def arch = System.getProperty('os.arch').toLowerCase(Locale.ROOT) + def z3Arch = arch in ['aarch64', 'arm64'] ? 'arm64' : 'x64' + + if (os.isLinux()) { + def libc = z3Arch == 'arm64' ? 'glibc-2.34' : 'glibc-2.39' + return [distribution: "z3-${z3Version}-${z3Arch}-${libc}"] + } + if (os.isMacOsX()) { + return [distribution: "z3-${z3Version}-${z3Arch}-osx-13.7.6"] + } + if (os.isWindows()) { + def windowsArch = arch in ['x86', 'i386'] ? 'x86' : z3Arch + return [distribution: "z3-${z3Version}-${windowsArch}-win"] + } + + throw new GradleException("Unsupported operating system for Z3 native libraries: ${os}") +} + +configurations { + cfgExtractor +} + +dependencies { + cfgExtractor 'de.uzl.its:cfg-extractor:1.0-SNAPSHOT' +} + +def z3Platform = z3Platform() +def z3Archive = layout.buildDirectory.file("z3/${z3Platform.distribution}.zip") +def z3DownloadUrl = "https://github.com/Z3Prover/z3/releases/download/z3-${z3Version}/${z3Platform.distribution}.zip" - def z3Zip = file("libs/${osArchMap[osKey]}.zip") - if (!z3Zip.exists()) { - throw new GradleException("Z3 distribution zip file not found at ${z3Zip.path}") +tasks.register('downloadZ3Distribution') { + description = 'Downloads the official Z3 distribution for the current platform.' + inputs.property 'url', z3DownloadUrl + outputs.file z3Archive + + doLast { + def archive = z3Archive.get().asFile + def temporaryArchive = new File(archive.parentFile, "${archive.name}.part") + archive.parentFile.mkdirs() + + new URL(z3DownloadUrl).withInputStream { input -> + temporaryArchive.withOutputStream { output -> output << input } } - from zipTree(z3Zip) - into 'libs/java-library-path' - include "${osArchMap[osKey]}/bin/z3*" - include "${osArchMap[osKey]}/bin/libz3.*" - include "${osArchMap[osKey]}/bin/libz3java.*" - include "${osArchMap[osKey]}/bin/com.microsoft.z3.jar" - eachFile { FileCopyDetails fcp -> - fcp.relativePath = new RelativePath(true, fcp.name) - } - includeEmptyDirs false + java.nio.file.Files.move( + temporaryArchive.toPath(), + archive.toPath(), + java.nio.file.StandardCopyOption.REPLACE_EXISTING + ) + } +} + +tasks.register('copyNativeLibs', Sync) { + description = 'Fetches the Z3 Java bindings and native libraries.' + dependsOn tasks.named('downloadZ3Distribution') + inputs.property 'runtimeLayoutVersion', 2 + into z3NativeDir + duplicatesStrategy = DuplicatesStrategy.EXCLUDE + + from({ zipTree(z3Archive.get().asFile) }) { + include "${z3Platform.distribution}/bin/libz3.*" + include "${z3Platform.distribution}/bin/libz3java.*" + include "${z3Platform.distribution}/bin/com.microsoft.z3.jar" + eachFile { details -> + details.relativePath = new RelativePath(true, details.name) + } + includeEmptyDirs = false } +} tasks.register('downloadJacoco') { description = 'Downloads JaCoCo agent jar for coverage collection' def jacocoVersion = '0.8.13' @@ -85,14 +111,6 @@ tasks.register('downloadJacoco') { } } -configurations { - cfgExtractor -} - -dependencies { - cfgExtractor 'de.uzl.its:cfg-extractor:1.0-SNAPSHOT' -} - tasks.register('downloadCfgExtractor', Copy) { description = 'Downloads cfg-extractor fat JAR from GitHub Packages' from configurations.cfgExtractor diff --git a/docker/Dockerfile b/docker/Dockerfile index 2a0cde6b..b9a51b77 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -2,7 +2,7 @@ FROM gradle:8.13.0-jdk17 # Install Python and other tools RUN apt-get update && \ - apt-get install -y python3 python3-pip python3-venv findutils unzip ant + apt-get install -y python3 python3-pip python3-venv findutils unzip # Set working dir WORKDIR /app @@ -10,10 +10,7 @@ WORKDIR /app # Copy project source COPY . . -RUN chmod +x ./scripts/build-javasmt.sh -RUN ./scripts/build-javasmt.sh - -# Copy native Z3 libs via Gradle task (assumes they go to /app/libs/java-library-path) +# Fetch native Z3 libs via Gradle task RUN gradle copyNativeLibs # Build Java code (skip tests) @@ -24,4 +21,4 @@ RUN gradle clean build -x test RUN cp /app/libs/java-library-path/libz3*.so /usr/lib/ # Set Z3 JAR in CLASSPATH so it's visible to javaagent (NO JVM FLAGS NEEDED) -ENV CLASSPATH=/app/libs/java-library-path/com.microsoft.z3.jar \ No newline at end of file +ENV CLASSPATH=/app/libs/java-library-path/com.microsoft.z3.jar diff --git a/libs/z3-4.15.4-arm64-glibc-2.34.zip b/libs/z3-4.15.4-arm64-glibc-2.34.zip deleted file mode 100644 index 1155d780..00000000 Binary files a/libs/z3-4.15.4-arm64-glibc-2.34.zip and /dev/null differ diff --git a/libs/z3-4.15.4-arm64-osx-13.7.6.zip b/libs/z3-4.15.4-arm64-osx-13.7.6.zip deleted file mode 100644 index a2b3c985..00000000 Binary files a/libs/z3-4.15.4-arm64-osx-13.7.6.zip and /dev/null differ diff --git a/libs/z3-4.15.4-x64-glibc-2.39.zip b/libs/z3-4.15.4-x64-glibc-2.39.zip deleted file mode 100644 index f5031b51..00000000 Binary files a/libs/z3-4.15.4-x64-glibc-2.39.zip and /dev/null differ diff --git a/libs/z3-4.15.4-x64-osx-13.7.6.zip b/libs/z3-4.15.4-x64-osx-13.7.6.zip deleted file mode 100644 index 4043cf30..00000000 Binary files a/libs/z3-4.15.4-x64-osx-13.7.6.zip and /dev/null differ diff --git a/libs/z3-4.15.4-x64-win.zip b/libs/z3-4.15.4-x64-win.zip deleted file mode 100644 index 98b7e3a0..00000000 Binary files a/libs/z3-4.15.4-x64-win.zip and /dev/null differ diff --git a/libs/z3-4.15.4-x86-win.zip b/libs/z3-4.15.4-x86-win.zip deleted file mode 100644 index 38419c52..00000000 Binary files a/libs/z3-4.15.4-x86-win.zip and /dev/null differ diff --git a/scripts/package-svcomp.sh b/scripts/package-svcomp.sh index c3a5e788..d979e24b 100755 --- a/scripts/package-svcomp.sh +++ b/scripts/package-svcomp.sh @@ -23,7 +23,7 @@ set -euo pipefail # # - .venv_ubuntu_24_04_1__x86_64/ # -# Z3 and JavaSMT are taken from the vendored files in this repository. +# Z3 and JavaSMT are taken from the runtime files prepared by CI. # ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" cd "$ROOT_DIR" @@ -41,8 +41,6 @@ ARTIFACT_DIR="$(cd "${SWAT_SVCOMP_ARTIFACT_DIR:-$ROOT_DIR}" && pwd)" 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 "$RUNTIME_DIR" ]]; then @@ -106,12 +104,11 @@ copy_artifact_tree() { install_z3_runtime_file() { local name="$1" local mode="${2:-0644}" + local src="${ROOT_DIR}/libs/java-library-path/${name}" local dest="${PACKAGE_DIR}/libs/java-library-path/${name}" - [[ -f "$LINUX_Z3_ZIP" ]] || fail "missing vendored Linux Z3 distribution: ${LINUX_Z3_ZIP}" - mkdir -p "$(dirname "$dest")" - unzip -p "$LINUX_Z3_ZIP" "${LINUX_Z3_DIST}/bin/${name}" > "$dest" - chmod "$mode" "$dest" + [[ -f "$src" ]] || fail "missing prepared Z3 runtime file: ${src}" + copy_artifact_file "$src" "$dest" "$mode" } echo "Packaging repository files from: ${ROOT_DIR}" @@ -149,7 +146,6 @@ copy_tree_files symbolic-explorer "$PACKAGE_DIR/symbolic-explorer" [[ -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 diff --git a/settings.gradle b/settings.gradle index 430c6ddb..4b863500 100644 --- a/settings.gradle +++ b/settings.gradle @@ -61,12 +61,14 @@ dependencyResolutionManagement { versionCatalogs { libs { version('asm','9.6') + version('z3', '4.15.4') library('asm-core', 'org.ow2.asm','asm').versionRef('asm') library('asm-commons', 'org.ow2.asm','asm-commons').versionRef('asm') library('asm-util', 'org.ow2.asm','asm-util').versionRef('asm') library('asm-tree', 'org.ow2.asm','asm-tree').versionRef('asm') library('jackson-databind', 'com.fasterxml.jackson.core:jackson-databind:2.14.1') library('java-smt', 'org.sosy-lab:java-smt:6.0.0') + library('javasmt-solver-z3', 'org.sosy-lab', 'javasmt-solver-z3').versionRef('z3') library('spock-core', 'org.spockframework:spock-core:2.2-groovy-4.0') library('mockito-core', 'org.mockito:mockito-core:3.12.4') library('logback-classic', 'ch.qos.logback:logback-classic:1.5.3') diff --git a/symbolic-executor/build.gradle b/symbolic-executor/build.gradle index 94841476..58ebb835 100644 --- a/symbolic-executor/build.gradle +++ b/symbolic-executor/build.gradle @@ -38,8 +38,7 @@ dependencies { implementation libs.bundles.asm implementation libs.jackson.databind implementation libs.java.smt - - implementation rootProject.fileTree(dir: 'libs/java-library-path', include: ['*.jar']) // loads com.microsoft.z3 and java-smt + implementation libs.javasmt.solver.z3 testImplementation libs.spock.core testImplementation libs.jackson.databind @@ -47,7 +46,20 @@ dependencies { } test { - systemProperty "java.library.path", "../libs/java-library-path" + dependsOn rootProject.tasks.named('copyNativeLibs') + def z3NativePath = rootProject.z3NativeDir.asFile.absolutePath + def currentOs = org.gradle.internal.os.OperatingSystem.current() + systemProperty "java.library.path", z3NativePath + if (currentOs.isLinux()) { + def existingPath = System.getenv('LD_LIBRARY_PATH') + environment "LD_LIBRARY_PATH", existingPath ? "${z3NativePath}${File.pathSeparator}${existingPath}" : z3NativePath + } else if (currentOs.isMacOsX()) { + def existingPath = System.getenv('DYLD_LIBRARY_PATH') + environment "DYLD_LIBRARY_PATH", existingPath ? "${z3NativePath}${File.pathSeparator}${existingPath}" : z3NativePath + } else if (currentOs.isWindows()) { + def existingPath = System.getenv('PATH') + environment "PATH", existingPath ? "${z3NativePath}${File.pathSeparator}${existingPath}" : z3NativePath + } // Surface SWAT errors as exceptions instead of halting the test JVM systemProperty "exitOnError", "false"