From 67eb9cabe53d13a7d17b27bd78e00f378104ae50 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 24 Nov 2023 20:10:24 +0100 Subject: build: package Z3 solver native libraries --- z3/build.gradle.kts | 9 ++ z3/buildSrc/build.gradle.kts | 18 +++ z3/buildSrc/settings.gradle.kts | 13 ++ .../tools/refinery/z3/gradle/ClassFilePatcher.java | 48 +++++++ .../refinery/z3/gradle/java-library.gradle.kts | 75 ++++++++++ z3/docker/.gitignore | 5 + z3/docker/README.md | 14 ++ z3/docker/build_in_docker.sh | 21 +++ z3/docker/cross_build.sh | 16 +++ z3/gradle.properties | 9 ++ z3/gradle/libs.versions.toml | 15 ++ z3/settings.gradle.kts | 22 +++ .../solver-darwin-aarch64/build.gradle.kts | 36 +++++ .../solver-darwin-x86-64/build.gradle.kts | 36 +++++ .../solver-linux-aarch64/build.gradle.kts | 14 ++ .../main/resources/z3java-linux-aarch64/libz3.so | Bin 0 -> 29479296 bytes .../z3java-linux-aarch64/libz3.so.license | 6 + .../resources/z3java-linux-aarch64/libz3java.so | Bin 0 -> 295952 bytes .../z3java-linux-aarch64/libz3java.so.license | 6 + .../solver-linux-x86-64/build.gradle.kts | 36 +++++ .../solver-win32-x86-64/build.gradle.kts | 38 +++++ z3/subprojects/solver/build.gradle.kts | 107 ++++++++++++++ .../java/tools/refinery/z3/Z3SolverLoader.java | 154 +++++++++++++++++++++ .../java/tools/refinery/z3/Z3SolverLoaderTest.java | 30 ++++ 24 files changed, 728 insertions(+) create mode 100644 z3/build.gradle.kts create mode 100644 z3/buildSrc/build.gradle.kts create mode 100644 z3/buildSrc/settings.gradle.kts create mode 100644 z3/buildSrc/src/main/java/tools/refinery/z3/gradle/ClassFilePatcher.java create mode 100644 z3/buildSrc/src/main/kotlin/tools/refinery/z3/gradle/java-library.gradle.kts create mode 100644 z3/docker/.gitignore create mode 100644 z3/docker/README.md create mode 100755 z3/docker/build_in_docker.sh create mode 100755 z3/docker/cross_build.sh create mode 100644 z3/gradle.properties create mode 100644 z3/gradle/libs.versions.toml create mode 100644 z3/settings.gradle.kts create mode 100644 z3/subprojects/solver-darwin-aarch64/build.gradle.kts create mode 100644 z3/subprojects/solver-darwin-x86-64/build.gradle.kts create mode 100644 z3/subprojects/solver-linux-aarch64/build.gradle.kts create mode 100755 z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so create mode 100644 z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license create mode 100755 z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so create mode 100644 z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license create mode 100644 z3/subprojects/solver-linux-x86-64/build.gradle.kts create mode 100644 z3/subprojects/solver-win32-x86-64/build.gradle.kts create mode 100644 z3/subprojects/solver/build.gradle.kts create mode 100644 z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java create mode 100644 z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java (limited to 'z3') diff --git a/z3/build.gradle.kts b/z3/build.gradle.kts new file mode 100644 index 00000000..74ee6bc8 --- /dev/null +++ b/z3/build.gradle.kts @@ -0,0 +1,9 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +plugins { + alias(libs.plugins.versions) +} diff --git a/z3/buildSrc/build.gradle.kts b/z3/buildSrc/build.gradle.kts new file mode 100644 index 00000000..adc19562 --- /dev/null +++ b/z3/buildSrc/build.gradle.kts @@ -0,0 +1,18 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +plugins { + `kotlin-dsl` + alias(libs.plugins.versions) +} + +repositories { + mavenCentral() +} + +dependencies { + implementation(libs.asm) +} diff --git a/z3/buildSrc/settings.gradle.kts b/z3/buildSrc/settings.gradle.kts new file mode 100644 index 00000000..095ab24c --- /dev/null +++ b/z3/buildSrc/settings.gradle.kts @@ -0,0 +1,13 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +dependencyResolutionManagement { + versionCatalogs { + create("libs") { + from(files("../gradle/libs.versions.toml")) + } + } +} diff --git a/z3/buildSrc/src/main/java/tools/refinery/z3/gradle/ClassFilePatcher.java b/z3/buildSrc/src/main/java/tools/refinery/z3/gradle/ClassFilePatcher.java new file mode 100644 index 00000000..5ac56005 --- /dev/null +++ b/z3/buildSrc/src/main/java/tools/refinery/z3/gradle/ClassFilePatcher.java @@ -0,0 +1,48 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ +package tools.refinery.z3.gradle; + +import org.objectweb.asm.*; + +import java.io.File; +import java.io.FileInputStream; +import java.io.FileOutputStream; +import java.io.IOException; + +public final class ClassFilePatcher { + private ClassFilePatcher() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static void removeClassInitializer(File classFile) throws IOException { + byte[] resultBytes; + try (var fileReader = new FileInputStream(classFile)) { + var classReader = new ClassReader(fileReader); + var classWriter = new ClassWriter(classReader, 0); + var classVisitor = new Visitor(classWriter); + classReader.accept(classVisitor, 0); + resultBytes = classWriter.toByteArray(); + } + try (var fileWriter = new FileOutputStream(classFile)) { + fileWriter.write(resultBytes); + } + } + + private static class Visitor extends ClassVisitor { + protected Visitor(ClassVisitor classVisitor) { + super(Opcodes.ASM9, classVisitor); + } + + @Override + public MethodVisitor visitMethod(int access, String name, String descriptor, String signature, + String[] exceptions) { + if (name.equals("")) { + return null; + } + return super.visitMethod(access, name, descriptor, signature, exceptions); + } + } +} diff --git a/z3/buildSrc/src/main/kotlin/tools/refinery/z3/gradle/java-library.gradle.kts b/z3/buildSrc/src/main/kotlin/tools/refinery/z3/gradle/java-library.gradle.kts new file mode 100644 index 00000000..75d64a6f --- /dev/null +++ b/z3/buildSrc/src/main/kotlin/tools/refinery/z3/gradle/java-library.gradle.kts @@ -0,0 +1,75 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ +package tools.refinery.z3.gradle + +plugins { + `java-library` + `maven-publish` +} + +java { + toolchain { + languageVersion.set(JavaLanguageVersion.of(21)) + } +} + +repositories { + mavenCentral() + + // Configuration based on https://stackoverflow.com/a/34327202 to pretend that GitHub is an Ivy repository + // in order to take advantage of Gradle dependency caching. + val github = ivy { + setUrl("https://github.com") + patternLayout { + artifact("/[organisation]/[module]/releases/download/[module]-[revision]/[classifier].[ext]") + artifact("/[organisation]/[module]/archive/refs/tags/[module]-[revision].[ext]") + } + metadataSources { + artifact() + } + } + + exclusiveContent { + forRepositories(github) + filter { + includeGroup("Z3Prover") + } + } +} + +val z3: Provider by configurations.registering { + isCanBeConsumed = false + isCanBeResolved = true +} + +tasks { + jar { + manifest { + attributes( + "Bundle-SymbolicName" to "${project.group}.${project.name}", + "Bundle-Version" to project.version + ) + } + } +} + +publishing.publications { + register("mavenJava") { + from(components["java"]) + pom { + licenses { + license { + name = "MIT License" + url = "https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt" + } + license { + name = "The Apache License, Version 2.0" + url = "http://www.apache.org/licenses/LICENSE-2.0.txt" + } + } + } + } +} diff --git a/z3/docker/.gitignore b/z3/docker/.gitignore new file mode 100644 index 00000000..d5b53f81 --- /dev/null +++ b/z3/docker/.gitignore @@ -0,0 +1,5 @@ +# SPDX-FileCopyrightText: 2023 The Refinery Authors +# +# SPDX-License-Identifier: CC0-1.0 + +out/ diff --git a/z3/docker/README.md b/z3/docker/README.md new file mode 100644 index 00000000..d979fd5e --- /dev/null +++ b/z3/docker/README.md @@ -0,0 +1,14 @@ + + +# Scripts for cross-building Z3 for linux-aarch64 + +We intentionally build in Ubuntu Focal to avoid a dependency on glibc 2.35. +See https://github.com/Z3Prover/z3/issues/6572 for details. + +This should not be necessary once Z3 4.12.3 is released, as now Z3 nighly +includes linux-aarch64 builds. +See https://github.com/Z3Prover/z3/issues/6835 for details. diff --git a/z3/docker/build_in_docker.sh b/z3/docker/build_in_docker.sh new file mode 100755 index 00000000..cd28bd32 --- /dev/null +++ b/z3/docker/build_in_docker.sh @@ -0,0 +1,21 @@ +#!/usr/bin/env bash + +# SPDX-FileCopyrightText: 2023 The Refinery Authors +# +# SPDX-License-Identifier: Apache-2.0 + +set -euo pipefail + +z3_version="$1" +target_uid="$2" +target_gid="$3" + +apt-get update +apt-get install -y python3 make gcc-aarch64-linux-gnu g++-aarch64-linux-gnu unzip +wget "https://github.com/Z3Prover/z3/archive/refs/tags/z3-${z3_version}.zip" +unzip "z3-${z3_version}.zip" +cd "z3-z3-${z3_version}" +CXX=aarch64-linux-gnu-g++ CC=aarch64-linux-gnu-gcc python3 scripts/mk_unix_dist.py -f --nodotnet --arch=arm64 +cp --preserve=all "./dist/z3-${z3_version}-arm64-glibc-2.31/bin"/*.so /data/out/ +chown "${target_uid}:${target_gid}" /data/out/* + diff --git a/z3/docker/cross_build.sh b/z3/docker/cross_build.sh new file mode 100755 index 00000000..fe5edd2f --- /dev/null +++ b/z3/docker/cross_build.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +# SPDX-FileCopyrightText: 2023 The Refinery Authors +# +# SPDX-License-Identifier: Apache-2.0 + +set -euo pipefail + +z3_version="$(grep '^version=' ../gradle.properties | cut -d'=' -f2)" + +rm -rf out +mkdir out +docker run --platform linux/amd64 --rm -it -v "${PWD}:/data" --entrypoint /bin/bash docker.io/eclipse-temurin:17-jdk-focal /data/build_in_docker.sh "${z3_version}" "$(id -u)" "$(id -g)" +rm -rf ../subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/* +cp ./out/* ../subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/ + diff --git a/z3/gradle.properties b/z3/gradle.properties new file mode 100644 index 00000000..3ef49dc6 --- /dev/null +++ b/z3/gradle.properties @@ -0,0 +1,9 @@ +# SPDX-FileCopyrightText: 2023 The Refinery Authors +# +# SPDX-License-Identifier: Apache-2.0 + +file.encoding=UTF-8 +group=tools.refinery.z3 +org.gradle.configuration-cache=false +org.gradle.parallel=true +version=4.12.2 diff --git a/z3/gradle/libs.versions.toml b/z3/gradle/libs.versions.toml new file mode 100644 index 00000000..88cf8083 --- /dev/null +++ b/z3/gradle/libs.versions.toml @@ -0,0 +1,15 @@ +# SPDX-FileCopyrightText: 2023 The Refinery Authors +# +# SPDX-License-Identifier: Apache-2.0 + +[versions] +junit = "5.10.1" + +[libraries] +asm = { group = "org.ow2.asm", name = "asm", version = "9.6" } +jna = { group = "net.java.dev.jna", name = "jna", version = "5.13.0" } +junit-api = { group = "org.junit.jupiter", name = "junit-jupiter-api", version.ref = "junit" } +junit-engine = { group = "org.junit.jupiter", name = "junit-jupiter-engine", version.ref = "junit" } + +[plugins] +versions = { id = "com.github.ben-manes.versions", version = "0.50.0" } diff --git a/z3/settings.gradle.kts b/z3/settings.gradle.kts new file mode 100644 index 00000000..a857f5ce --- /dev/null +++ b/z3/settings.gradle.kts @@ -0,0 +1,22 @@ +/* + * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +rootProject.name = "refinery-z3" + +include( + "solver", + "solver-darwin-aarch64", + "solver-darwin-x86-64", + "solver-linux-aarch64", + "solver-linux-x86-64", + "solver-win32-x86-64", +) + +for (project in rootProject.children) { + val projectName = project.name + project.name = "${rootProject.name}-$projectName" + project.projectDir = file("subprojects/$projectName") +} diff --git a/z3/subprojects/solver-darwin-aarch64/build.gradle.kts b/z3/subprojects/solver-darwin-aarch64/build.gradle.kts new file mode 100644 index 00000000..21c9739c --- /dev/null +++ b/z3/subprojects/solver-darwin-aarch64/build.gradle.kts @@ -0,0 +1,36 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +plugins { + id("tools.refinery.z3.gradle.java-library") +} + +val classifier = "z3-${version}-arm64-osx-11.0" +val library = "z3java-darwin-aarch64" + +dependencies { + z3("Z3Prover:z3:${version}:${classifier}@zip") +} + +val extractZ3Libs by tasks.registering(Sync::class) { + dependsOn(configurations.z3) + from({ + val zipFile = configurations.z3.map { it.singleFile } + zipTree(zipFile).matching { + include("${classifier}/bin/*.so") + includeEmptyDirs = false + } + }) + eachFile { + val pathInBin = relativePath.segments.drop(2).toTypedArray() + relativePath = RelativePath(true, library, *pathInBin) + } + into(layout.buildDirectory.dir("z3-extracted")) +} + +sourceSets.main { + resources.srcDir(extractZ3Libs) +} diff --git a/z3/subprojects/solver-darwin-x86-64/build.gradle.kts b/z3/subprojects/solver-darwin-x86-64/build.gradle.kts new file mode 100644 index 00000000..75e59267 --- /dev/null +++ b/z3/subprojects/solver-darwin-x86-64/build.gradle.kts @@ -0,0 +1,36 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +plugins { + id("tools.refinery.z3.gradle.java-library") +} + +val classifier = "z3-${version}-x64-osx-10.16" +val library = "z3java-darwin-x86-64" + +dependencies { + z3("Z3Prover:z3:${version}:${classifier}@zip") +} + +val extractZ3Libs by tasks.registering(Sync::class) { + dependsOn(configurations.z3) + from({ + val zipFile = configurations.z3.map { it.singleFile } + zipTree(zipFile).matching { + include("${classifier}/bin/*.so") + includeEmptyDirs = false + } + }) + eachFile { + val pathInBin = relativePath.segments.drop(2).toTypedArray() + relativePath = RelativePath(true, library, *pathInBin) + } + into(layout.buildDirectory.dir("z3-extracted")) +} + +sourceSets.main { + resources.srcDir(extractZ3Libs) +} diff --git a/z3/subprojects/solver-linux-aarch64/build.gradle.kts b/z3/subprojects/solver-linux-aarch64/build.gradle.kts new file mode 100644 index 00000000..a8e7e259 --- /dev/null +++ b/z3/subprojects/solver-linux-aarch64/build.gradle.kts @@ -0,0 +1,14 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +plugins { + id("tools.refinery.z3.gradle.java-library") +} + +tasks.jar { + // License information is redundant here, since it already gets added to the POM. + exclude("**/*.license") +} diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so new file mode 100755 index 00000000..f7013e4f Binary files /dev/null and b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so differ diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license new file mode 100644 index 00000000..6f1e5a96 --- /dev/null +++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license @@ -0,0 +1,6 @@ +Copyright (c) Microsoft Corporations + +SPDX-License-Identifier: MIT + +This file was created from the Z3 4.12.2 release sources using the +z3/docker/cross_build.sh script in this repository. diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so new file mode 100755 index 00000000..e37c7cdb Binary files /dev/null and b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so differ diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license new file mode 100644 index 00000000..6f1e5a96 --- /dev/null +++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license @@ -0,0 +1,6 @@ +Copyright (c) Microsoft Corporations + +SPDX-License-Identifier: MIT + +This file was created from the Z3 4.12.2 release sources using the +z3/docker/cross_build.sh script in this repository. diff --git a/z3/subprojects/solver-linux-x86-64/build.gradle.kts b/z3/subprojects/solver-linux-x86-64/build.gradle.kts new file mode 100644 index 00000000..89c737b6 --- /dev/null +++ b/z3/subprojects/solver-linux-x86-64/build.gradle.kts @@ -0,0 +1,36 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +plugins { + id("tools.refinery.z3.gradle.java-library") +} + +val classifier = "z3-${version}-x64-glibc-2.31" +val library = "z3java-linux-x86-64" + +dependencies { + z3("Z3Prover:z3:${version}:${classifier}@zip") +} + +val extractZ3Libs by tasks.registering(Sync::class) { + dependsOn(configurations.z3) + from({ + val zipFile = configurations.z3.map { it.singleFile } + zipTree(zipFile).matching { + include("${classifier}/bin/*.so") + includeEmptyDirs = false + } + }) + eachFile { + val pathInBin = relativePath.segments.drop(2).toTypedArray() + relativePath = RelativePath(true, library, *pathInBin) + } + into(layout.buildDirectory.dir("z3-extracted")) +} + +sourceSets.main { + resources.srcDir(extractZ3Libs) +} diff --git a/z3/subprojects/solver-win32-x86-64/build.gradle.kts b/z3/subprojects/solver-win32-x86-64/build.gradle.kts new file mode 100644 index 00000000..c5fa0421 --- /dev/null +++ b/z3/subprojects/solver-win32-x86-64/build.gradle.kts @@ -0,0 +1,38 @@ +/* + * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +plugins { + id("tools.refinery.z3.gradle.java-library") +} + +val classifier = "z3-${version}-x64-win" +val library = "z3java-win32-x86-64" + +dependencies { + z3("Z3Prover:z3:${version}:${classifier}@zip") +} + +val extractZ3Libs by tasks.registering(Sync::class) { + dependsOn(configurations.z3) + from({ + val zipFile = configurations.z3.map { it.singleFile } + zipTree(zipFile).matching { + include("${classifier}/bin/*.dll") + // Do not include .NET assembly. + exclude("${classifier}/bin/Microsoft.Z3.dll") + includeEmptyDirs = false + } + }) + eachFile { + val pathInBin = relativePath.segments.drop(2).toTypedArray() + relativePath = RelativePath(true, library, *pathInBin) + } + into(layout.buildDirectory.dir("z3-extracted")) +} + +sourceSets.main { + resources.srcDir(extractZ3Libs) +} diff --git a/z3/subprojects/solver/build.gradle.kts b/z3/subprojects/solver/build.gradle.kts new file mode 100644 index 00000000..7e898b3e --- /dev/null +++ b/z3/subprojects/solver/build.gradle.kts @@ -0,0 +1,107 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ + +import tools.refinery.z3.gradle.ClassFilePatcher + +plugins { + id("tools.refinery.z3.gradle.java-library") +} + +val classifier = "z3-${version}-x64-glibc-2.31" +val extractedClassesDir = layout.buildDirectory.dir("z3-extracted") +val extractedSourcesDir = layout.buildDirectory.dir("z3-sources") + +java { + withJavadocJar() + withSourcesJar() +} + +val z3Source: Configuration by configurations.creating { + isCanBeConsumed = false + isCanBeResolved = true +} + +val extractZ3Jar by tasks.registering(Sync::class) { + dependsOn(configurations.z3) + from({ + val zipFile = configurations.z3.map { it.singleFile } + val jarFile = zipTree(zipFile).matching { + include("${classifier}/bin/com.microsoft.z3.jar") + }.singleFile + zipTree(jarFile).matching { + exclude("META-INF/MANIFEST.MF") + includeEmptyDirs = false + } + }) + into(extractedClassesDir) + doLast { + // The class initializer off {@see com.microsoft.z3.Native} will try to load the Z3 native libraries + // from the system default library path unless the {@code z3.skipLibraryLoad} system property is set. + // Since we don't control the library path or system properties, we remove the class initializer entirely. + val nativeClassFile = extractedClassesDir.get().file("com/microsoft/z3/Native.class").asFile + ClassFilePatcher.removeClassInitializer(nativeClassFile) + } +} + +val extractZ3Source by tasks.registering(Sync::class) { + dependsOn(z3Source) + from({ + val zipFile = z3Source.singleFile + zipTree(zipFile).matching { + include("z3-z3-${version}/src/api/java/**/*") + includeEmptyDirs = false + } + }) + eachFile { + val pathInBin = relativePath.segments.drop(4).toTypedArray() + relativePath = RelativePath(true, "com", "microsoft", "z3", *pathInBin) + } + into(extractedSourcesDir) +} + +tasks.jar { + // Add class files to our jar manually. + from(extractZ3Jar) +} + +tasks.test { + useJUnitPlatform() +} + +tasks.named("sourcesJar") { + from(extractZ3Source) +} + +tasks.named("javadoc") { + source(sourceSets.main.map { it.allJava }) + source(fileTree(extractedSourcesDir) { + builtBy(extractZ3Source) + include("**/*.java") + }) + options { + this as StandardJavadocDocletOptions + addBooleanOption("Xdoclint:none", true) + // {@code -Xmaxwarns 0} will print all warnings, so we must keep at least one. + addStringOption("Xmaxwarns", "1") + quiet() + } +} + +dependencies { + z3("Z3Prover:z3:${version}:${classifier}@zip") + z3Source("Z3Prover:z3:${version}@zip") + // This dependency doesn't get added to Maven metadata, so we have to add the class files to our jar manually. + api(files(extractZ3Jar)) + implementation(libs.jna) + implementation(project(":refinery-z3-solver-darwin-aarch64")) + implementation(project(":refinery-z3-solver-darwin-x86-64")) + implementation(project(":refinery-z3-solver-linux-aarch64")) + implementation(project(":refinery-z3-solver-linux-x86-64")) + implementation(project(":refinery-z3-solver-win32-x86-64")) + testImplementation(libs.junit.api) + testRuntimeOnly(libs.junit.engine) + testRuntimeOnly("org.junit.platform:junit-platform-launcher") +} diff --git a/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java b/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java new file mode 100644 index 00000000..84f99540 --- /dev/null +++ b/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java @@ -0,0 +1,154 @@ +/* + * Copyright 2010-2022 Google LLC + * Copyright 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + * + * This file is based on + * https://github.com/google/or-tools/blob/f3d1d5f6a67356ec38a7fd2ab607624eea8ad3a6/ortools/java/com/google/ortools/Loader.java + * We adapted the loader logic to extract the JNI libraries of Z3 and the corresponding dependencies instead of the + * Google OR-Tools JNI libraries. + */ +package tools.refinery.z3; + +import com.sun.jna.Platform; + +import java.io.IOException; +import java.net.URI; +import java.net.URISyntaxException; +import java.nio.file.*; +import java.nio.file.attribute.BasicFileAttributes; +import java.util.Map; + +public final class Z3SolverLoader { + private static final String JNI_LIBRARY_NAME = "z3java"; + private static final String SOLVER_LIBRARY_NAME = "z3"; + + private static boolean loaded; + + private Z3SolverLoader() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static synchronized void loadNativeLibraries() { + if (loaded) { + return; + } + try { + System.loadLibrary(getOsSpecificLibraryName(JNI_LIBRARY_NAME)); + loaded = true; + return; + } catch (UnsatisfiedLinkError e) { + // Continue, we'll have to extract the libraries from the classpath. + } + try { + extractAndLoad(); + loaded = true; + } catch (IOException e) { + throw new IllegalStateException("Could not extract and load " + JNI_LIBRARY_NAME, e); + } + } + + private static void extractAndLoad() throws IOException { + var resourceName = JNI_LIBRARY_NAME + "-" + Platform.RESOURCE_PREFIX; + var resource = Z3SolverLoader.class.getClassLoader().getResource(resourceName); + if (resource == null) { + throw new IllegalStateException("Resource %s was not found".formatted(resourceName)); + } + URI resourceUri; + try { + resourceUri = resource.toURI(); + } catch (URISyntaxException e) { + throw new IllegalStateException("Invalid resource URI: " + resource); + } + FileSystem fileSystem = null; + boolean newFileSystem = false; + Path extractedPath; + try { + try { + fileSystem = FileSystems.newFileSystem(resourceUri, Map.of()); + newFileSystem = true; + } catch (FileSystemAlreadyExistsException e) { + fileSystem = FileSystems.getFileSystem(resourceUri); + } + var resourcePath = fileSystem.provider().getPath(resourceUri); + if (fileSystem.equals(FileSystems.getDefault())) { + extractedPath = resourcePath; + } else { + extractedPath = extract(resourcePath); + } + } finally { + if (newFileSystem) { + fileSystem.close(); + } + } + // We can't rely on RPATH, so we load libraries in reverse dependency order manually. + try { + loadFromPath(extractedPath, SOLVER_LIBRARY_NAME); + } catch (UnsatisfiedLinkError e) { + if (Platform.isWindows()) { + // Try again with our packaged msvcp140 if the system one is missing. + loadFromPathExactName(extractedPath, "vcruntime140.dll"); + loadFromPathExactName(extractedPath, "vcruntime140_1.dll"); + loadFromPathExactName(extractedPath, "msvcp140.dll"); + loadFromPath(extractedPath, SOLVER_LIBRARY_NAME); + } else { + throw e; + } + } + loadFromPath(extractedPath, JNI_LIBRARY_NAME); + } + + private static Path extract(Path resourcePath) throws IOException { + var tempDir = Files.createTempDirectory(JNI_LIBRARY_NAME).toAbsolutePath(); + tempDir.toFile().deleteOnExit(); + Files.walkFileTree(resourcePath, new SimpleFileVisitor<>() { + @Override + public FileVisitResult preVisitDirectory(Path dir, BasicFileAttributes attrs) throws IOException { + var result = super.preVisitDirectory(dir, attrs); + var targetPath = getTargetPath(dir, resourcePath, tempDir); + if (!Files.exists(targetPath)) { + Files.createDirectory(targetPath); + targetPath.toFile().deleteOnExit(); + } + return result; + } + + @Override + public FileVisitResult visitFile(Path file, BasicFileAttributes attrs) throws IOException { + var result = super.visitFile(file, attrs); + var targetPath = getTargetPath(file, resourcePath, tempDir); + Files.copy(file, targetPath); + targetPath.toFile().deleteOnExit(); + return result; + } + }); + return tempDir; + } + + private static Path getTargetPath(Path sourcePath, Path resourcePath, Path tempDir) { + var targetPath = tempDir.resolve(resourcePath.relativize(sourcePath).toString()).normalize(); + if (!targetPath.startsWith(tempDir)) { + throw new IllegalStateException("Target path '%s' for '%s' is outside '%s'" + .formatted(targetPath, sourcePath, tempDir)); + } + return targetPath; + } + + private static String getOsSpecificLibraryName(String libraryName) { + var osSpecificLibraryNamePrefix = Platform.isWindows() ? "lib" : ""; + return osSpecificLibraryNamePrefix + libraryName; + } + + private static void loadFromPath(Path extractedPath, String libraryName) { + var osSpecificLibraryName = getOsSpecificLibraryName(libraryName); + loadFromPathExactName(extractedPath, System.mapLibraryName(osSpecificLibraryName)); + } + + private static void loadFromPathExactName(Path extractedPath, String exactName) { + var library = extractedPath.resolve(exactName) + .toAbsolutePath() + .toString(); + System.load(library); + } +} diff --git a/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java b/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java new file mode 100644 index 00000000..df3139cc --- /dev/null +++ b/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java @@ -0,0 +1,30 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: Apache-2.0 + */ +package tools.refinery.z3; + +import com.microsoft.z3.*; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertDoesNotThrow; +import static org.junit.jupiter.api.Assertions.assertEquals; + +class Z3SolverLoaderTest { + @Test + void testLoad() { + assertDoesNotThrow(Z3SolverLoader::loadNativeLibraries); + try (var context = new Context()) { + var solver = context.mkSolver(); + var a = context.mkConst("a", context.getIntSort()); + var b = context.mkConst("b", context.getIntSort()); + solver.add(context.mkEq(a, context.mkInt(3))); + solver.add(context.mkEq(b, context.mkMul(context.mkInt(2), a))); + assertEquals(Status.SATISFIABLE, solver.check()); + var model = solver.getModel(); + var bValue = (IntNum) model.getConstInterp(b); + assertEquals(6, bValue.getInt()); + } + } +} -- cgit v1.2.3-54-g00ecf