From ea4b124ca86b9f08237f419f919419cb9fbd40cb Mon Sep 17 00:00:00 2001 From: Simon Dierl Date: Fri, 20 Sep 2024 16:35:44 +0200 Subject: [PATCH] Migrate to turnkey-support and turnkey-gradle-plugin; introduce various refactorings and support JPMS modules. --- .github/dependabot.yml | 22 +- .github/workflows/ci.yml | 112 +++ .github/workflows/test.yml | 156 ---- AUTHORS.md | 22 +- README.md | 125 ++-- build.gradle.kts | 682 +++++++++++------- buildSrc/build.gradle.kts | 31 +- buildSrc/settings.gradle.kts | 22 +- .../kotlin/tools/aqua/InstallNameToolTask.kt | 149 ---- .../main/kotlin/tools/aqua/NativeRewriter.kt | 49 -- buildSrc/src/main/kotlin/tools/aqua/Tests.kt | 35 - buildSrc/src/main/kotlin/tools/aqua/Utils.kt | 24 - .../src/main/kotlin/tools/aqua/Versions.kt | 31 - .../main/kotlin/tools/aqua/Z3Distribution.kt | 68 -- .../main/kotlin/tools/aqua/Z3GeneratorTask.kt | 71 +- config/license/Apache-2.0-cstyle | 18 + config/license/Apache-2.0-hashmark | 16 + config/license/CC-BY-4.0-xmlstyle | 12 + config/pmd.xml | 71 ++ contrib/license-header.java | 14 - contrib/license-header.kt | 14 - contrib/license-header.yml | 14 - gradle/gradle-daemon-jvm.properties | 2 + gradle/libs.versions.toml | 35 +- gradle/wrapper/gradle-wrapper.jar | Bin 43453 -> 43583 bytes gradle/wrapper/gradle-wrapper.properties | 2 +- gradlew | 7 +- gradlew.bat | 2 + settings.gradle.kts | 31 +- src/main/java/com/microsoft/z3/Z3Loader.java | 254 ------- src/main/java/module-info.java | 4 +- .../aqua/turnkey/z3/ShutdownHookTest.java | 86 +++ .../turnkey/z3/SolverInteractionTest.java | 111 +++ .../tools/aqua/turnkey/z3/Z3LoaderTest.java | 38 + .../aqua/z3turnkey/ShutdownHookTest.java | 93 --- .../aqua/z3turnkey/SolverInteractionTest.java | 96 --- .../tools/aqua/z3turnkey/Z3LoaderTest.java | 38 - 37 files changed, 1121 insertions(+), 1436 deletions(-) create mode 100644 .github/workflows/ci.yml delete mode 100644 .github/workflows/test.yml delete mode 100644 buildSrc/src/main/kotlin/tools/aqua/InstallNameToolTask.kt delete mode 100644 buildSrc/src/main/kotlin/tools/aqua/NativeRewriter.kt delete mode 100644 buildSrc/src/main/kotlin/tools/aqua/Tests.kt delete mode 100644 buildSrc/src/main/kotlin/tools/aqua/Utils.kt delete mode 100644 buildSrc/src/main/kotlin/tools/aqua/Versions.kt delete mode 100644 buildSrc/src/main/kotlin/tools/aqua/Z3Distribution.kt create mode 100644 config/license/Apache-2.0-cstyle create mode 100644 config/license/Apache-2.0-hashmark create mode 100644 config/license/CC-BY-4.0-xmlstyle create mode 100644 config/pmd.xml delete mode 100644 contrib/license-header.java delete mode 100644 contrib/license-header.kt delete mode 100644 contrib/license-header.yml create mode 100644 gradle/gradle-daemon-jvm.properties delete mode 100644 src/main/java/com/microsoft/z3/Z3Loader.java create mode 100644 src/test/java/tools/aqua/turnkey/z3/ShutdownHookTest.java create mode 100644 src/test/java/tools/aqua/turnkey/z3/SolverInteractionTest.java create mode 100644 src/test/java/tools/aqua/turnkey/z3/Z3LoaderTest.java delete mode 100644 src/test/java/tools/aqua/z3turnkey/ShutdownHookTest.java delete mode 100644 src/test/java/tools/aqua/z3turnkey/SolverInteractionTest.java delete mode 100644 src/test/java/tools/aqua/z3turnkey/Z3LoaderTest.java diff --git a/.github/dependabot.yml b/.github/dependabot.yml index 474106c..d2e39b1 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -1,16 +1,18 @@ +# SPDX-License-Identifier: Apache-2.0 # -# Copyright 2019-2024 The Z3-TurnKey Authors -# SPDX-License-Identifier: ISC +# Copyright 2019-2024 The TurnKey Authors # -# Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby -# granted, provided that the above copyright notice and this permission notice appear in all copies. +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at # -# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL -# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, -# INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN -# AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR -# PERFORMANCE OF THIS SOFTWARE. +# http://www.apache.org/licenses/LICENSE-2.0 # +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. version: 2 updates: @@ -21,4 +23,4 @@ updates: - package-ecosystem: github-actions directory: / schedule: - interval: daily \ No newline at end of file + interval: daily diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..980456e --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,112 @@ +# SPDX-License-Identifier: Apache-2.0 +# +# Copyright 2019-2024 The TurnKey Authors +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +name: CI/CD + +on: + push: + branches: + - main + pull_request: + branches: + - main + workflow_dispatch: + +permissions: + contents: write + +jobs: + build-local: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-java@v4 + with: + distribution: temurin + java-version: 17 + - uses: gradle/actions/setup-gradle@v4 + - run: | + ./gradlew build testRunner versionFile + cp build/z3.version build/libs/z3-turnkey-*-test-runner.jar . + - uses: actions/upload-artifact@v4 + with: + name: test-runner + path: | + z3-turnkey-*-test-runner.jar + z3.version + + test: + strategy: + matrix: + os: [macos-latest, ubuntu-latest, windows-latest] + java-package: [liberica, microsoft, temurin, zulu] + java-version: [8, 11, 17, 21] + architecture: [x64] + exclude: + - java-package: microsoft + java-version: 8 + fail-fast: false # Ensure we get all failures on all affected platforms + + name: JUnit Test on ${{ matrix.os }} and ${{ matrix.java-package }} version ${{ matrix.java-version }} for ${{ matrix.architecture }} + needs: build-local + runs-on: ${{ matrix.os }} + steps: + - uses: actions/download-artifact@v4 + with: + name: test-runner + + - uses: actions/setup-java@v4 + with: + distribution: ${{ matrix.java-package }} + java-version: ${{ matrix.java-version }} + architecture: ${{ matrix.architecture }} + + - shell: bash + run: | + z3version="$(cat z3.version)" + prefix="" + if ! command -v arch &> /dev/null; then + case "${{ matrix.architecture }}" in + "aarch64") prefix="arch -arm64";; + "x64") prefix="arch -x86_64";; + *) echo "unknown architecture ${{ matrix.architecture }}"; exit 1;; + esac + fi + module_options="" + if [ "${{ matrix.java-version }}" -gt 8 ]; then + module_options="--add-opens java.base/java.io=ALL-UNNAMED" + fi + ${prefix} java ${module_options} \ + -DexpectedZ3Version="${z3version}" \ + -jar z3-turnkey-*-test-runner.jar \ + execute --fail-if-no-tests \ + --select-package tools.aqua.turnkey.z3 \ + --reports-dir test-results + - uses: mikepenz/action-junit-report@v4 + if: always() + with: + require_tests: true + report_paths: "test-results/*.xml" + + dependency-submission: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-java@v4 + with: + distribution: temurin + java-version: 17 + - uses: gradle/actions/dependency-submission@v4 diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml deleted file mode 100644 index 9172c37..0000000 --- a/.github/workflows/test.yml +++ /dev/null @@ -1,156 +0,0 @@ -# -# Copyright 2019-2024 The Z3-TurnKey Authors -# SPDX-License-Identifier: ISC -# -# Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby -# granted, provided that the above copyright notice and this permission notice appear in all copies. -# -# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL -# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, -# INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN -# AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR -# PERFORMANCE OF THIS SOFTWARE. -# - -name: License Check and Multi-Platform Test - -on: - push: - branches: - - main - pull_request: - branches: - - main - workflow_dispatch: - -env: - JDK_VERSION: 17 - -jobs: - safety-check: - name: Check for modified Gradle - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v4 - - - name: Validate Gradle artifacts - uses: gradle/actions/wrapper-validation@v3 - - spotless: - name: Run Spotless - needs: safety-check - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v4 - - - name: Set up JDK - uses: actions/setup-java@v4 - with: - distribution: temurin - java-version: ${{ env.JDK_VERSION }} - - - name: Set up Gradle - uses: gradle/actions/setup-gradle@v3 - with: - dependency-graph: generate-and-submit - - - name: Run Spotless checks - run: ./gradlew spotlessCheck - - test-runner: - name: Build JUnit Test Runner - needs: safety-check - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v4 - - - name: Set up JDK - uses: actions/setup-java@v4 - with: - distribution: temurin - java-version: ${{ env.JDK_VERSION }} - - - name: Set up Gradle - uses: gradle/actions/setup-gradle@v3 - with: - dependency-graph: generate-and-submit - - - name: Identify install_name_tool name - shell: bash - run: | - cd /usr/bin - tools=( llvm-install-name-tool-* ) - echo "ORG_GRADLE_PROJECT_install_name_tool=${tools[-1]}" >> "${GITHUB_ENV}" - - - name: Build Test Runner Jar - run: | - ./gradlew testRunner versionFile - cp build/z3.version build/libs/z3-turnkey-*-test-runner.jar . - - - name: Upload Test Runner Jar - uses: actions/upload-artifact@v4 - with: - name: test-runner - path: | - z3-turnkey-*-test-runner.jar - z3.version - - test: - strategy: - matrix: - os: [ macos-latest, ubuntu-latest, windows-latest ] - java-package: [ liberica, microsoft, temurin, zulu ] - java-version: [ 8, 11, 17, 21 ] - architecture: [ x64 ] - exclude: - - java-package: microsoft - java-version: 8 - fail-fast: false # Ensure we get all failures on all affected platforms - - name: JUnit Test on ${{ matrix.os }} and ${{ matrix.java-package }} version ${{ matrix.java-version }} for ${{ matrix.architecture }} - needs: test-runner - runs-on: ${{ matrix.os }} - steps: - - name: Download Test Runner Jar - uses: actions/download-artifact@v4 - with: - name: test-runner - - - name: Set up JDK - uses: actions/setup-java@v4 - with: - distribution: ${{ matrix.java-package }} - java-version: ${{ matrix.java-version }} - architecture: ${{ matrix.architecture }} - - - name: Run tests - shell: bash - run: | - z3version="$(cat z3.version)" - prefix="" - if ! command -v arch &> /dev/null; then - case "${{ matrix.architecture }}" in - "aarch64") prefix="arch -arm64";; - "x64") prefix="arch -x86_64";; - *) echo "unknown architecture ${{ matrix.architecture }}"; exit 1;; - esac - fi - module_options="" - if [ "${{ matrix.java-version }}" -gt 8 ]; then - module_options="--add-opens java.base/java.io=ALL-UNNAMED" - fi - ${prefix} java ${module_options} \ - -DexpectedZ3Version="${z3version}" \ - -jar z3-turnkey-*-test-runner.jar \ - execute --fail-if-no-tests \ - --select-package tools.aqua.z3turnkey \ - --reports-dir test-results - - name: Publish Test Report - uses: mikepenz/action-junit-report@v4 - if: always() - with: - require_tests: true - report_paths: 'test-results/*.xml' diff --git a/AUTHORS.md b/AUTHORS.md index bb61b6b..1f13a2a 100644 --- a/AUTHORS.md +++ b/AUTHORS.md @@ -1,8 +1,20 @@ -### The Z3-TurnKey Authors + + +# The TurnKey Authors + +The project is maintained by [AQUA Group](https://aqua.engineering/) at TU Dortmund University. + +## Active Contributors + +- [Simon Dierl](mailto:simon.dierl@tu-dortmund.de) +- [Malte Mues](mailto:mail.mues@gmail.com) diff --git a/README.md b/README.md index 47173cb..86dd135 100644 --- a/README.md +++ b/README.md @@ -1,96 +1,67 @@ -[![GitHub Workflow Status](https://img.shields.io/github/actions/workflow/status/tudo-aqua/z3-turnkey/test.yml?branch=master)](https://github.com/tudo-aqua/z3-turnkey/actions) -[![JavaDoc](https://javadoc.io/badge2/tools.aqua/z3-turnkey/javadoc.svg)](https://javadoc.io/doc/tools.aqua/z3-turnkey) -[![Maven Central](https://img.shields.io/maven-central/v/tools.aqua/z3-turnkey?logo=apache-maven)](https://search.maven.org/artifact/tools.aqua/z3-turnkey) -### The Z3-TurnKey Distribution - -[The Z3 Theorem Prover](https://github.com/Z3Prover/z3/) is a widely used SMT solver that is written in C and C++. The -authors provide a Java API, however, it is not trivial to set up in a Java project. This project aims to solve this -issue. - -#### Why? - -The Z3 API is hard-coded to load its libraries from the OS's library directory (e.g., `/usr/lib`, `/usr/local/lib`, -etc. on Linux). These directories should not be writable by normal users. The expected workflow to use Z3 from Java -would therefore require installing a matching version of the Z3 native libraries as an administrator before using the -Java bindings. + -#### How? - -This project consists of two parts: -1. a Java loader, `Z3Loader`, that handles runtime unpacking and linking of the native support libraries, and -2. a build system that create a JAR from the official Z3 distributions that - 1. contains all native support libraries built by the Z3 project, - 2. replaces the hard-coded system library loader with `Z3Loader` by rewriting the Z3 source code, - 3. fixes the OS X library's search path to a relative one, and - 3. bundles all of the required files. -Also, JavaDoc and source JARs are generated for ease of use. - -#### Building +[![GitHub Workflow Status](https://img.shields.io/github/actions/workflow/status/tudo-aqua/z3-turnkey/ci.yml?logo=githubactions&logoColor=white)](https://github.com/tudo-aqua/z3-turnkey/actions) +[![JavaDoc](https://javadoc.io/badge2/tools.aqua/z3-turnkey/javadoc.svg)](https://javadoc.io/doc/tools.aqua/z3-turnkey) +[![Maven Central](https://img.shields.io/maven-central/v/tools.aqua/z3-turnkey?logo=apache-maven)](https://search.maven.org/artifact/tools.aqua/z3-turnkey) -The project is built using [Gradle](https://gradle.org/). In addition to Java 11 or higher, building requires Python 3, -an `install_name_tool` for OS X and a GPG signature key. +# The Z3-TurnKey Distribution -The project can be built and tested on the current platform using: -> ./gradlew assemble integrationTest +[The Z3 Theorem Prover](https://github.com/Z3Prover/z3/) is a widely used SMT solver that is written +in C and C++. The authors provide a Java API, however, it expects the user to install native +libraries for their platform. This precludes easy usage of the solver as, e.g., a Maven dependency. -##### Python 3 +This project packages the Z3 Java API and native libraries for all supported platforms as a +[TurnKey bundle](https://github.com/tudo-aqua/turnkey-support). At runtime, the correct library for +the platform is extracted and automatically loaded. The libraries themselves are modified to support +this paradigm. -Python 3 can be acquired as follows: -- Windows users can use the [official installer](https://www.python.org/downloads/windows/). When using the - [Chocolatey package manager](https://chocolatey.org/), Python can be installed using - > choco install python -- OS X users can use the [official installer](https://www.python.org/downloads/mac-osx/). When using the - [Homebrew package manager](https://brew.sh/), Python can be installer using - > brew install python -- Linux users should install the Python package provided by their distribution. Most likely, it is already present. +At the moment, platform support is as follows: -Python 3 is discovered by the build script using [https://github.com/xvik/gradle-use-python-plugin]. +| Operating System | x86 | AMD64 | AARCH64 | +| ---------------- | :-: | :---: | :-----: | +| Linux | | ✓ | | +| macOS | | ✓ | ✓ | +| Windows | ✓ | ✓ | | -##### `install_name_tool` +## Usage -An `install_name_tool` can be acquired as follows: -- Windows users will need to experiment with Cygwin/MinGW or Docker. -- OS X already ships an `install_name_tool`. -- Linux users can use the version shipped by LLVM. +The library can be included as a regular Maven dependency from the Maven Central repository. See the +page for your version of choice [there](https://search.maven.org/artifact/tools.aqua/z3-turnkey) for +configuration snippets for most build tools. -The `install_name_tool` binary is discovered as follows: -1. If the project parameter `install_name_tool` is set, its value is used. -2. Else, `install_name_tool` is tried and used if it exists. This should be the case on OS X. -3. Else, `llvm-install-name-tool` is tried and used if it exists. This should be the case on other OSes with LLVM - installed. -4. Else, the build fails. +## Building -Without an `install_name_tool`, a build can be created by setting the parameter to the `true` application. However, the -resulting artifact *will not work on OS X*! -> ./gradlew -Pinstall_name_tool=true assemble integrationTest +Building the library requires multiple native tools to be installed that can not be installed using +Gradle: -##### Signing +- For library rewriting, see the tools required by the + [turnkey-gradle-plugin](https://github.com/tudo-aqua/turnkey-gradle-plugin). +- Additionally, Python 3 is required for a code generation step and localized by the + [gradle-use-python-plugin](https://github.com/xvik/gradle-use-python-plugin). -Normally, Gradle will enforce a GPG signature on the artifacts. By setting the project parameter `skip-signing`, -enforcement is disabled: -> ./gradlew -Pskip-signing assemble +## Java and JPMS Support -##### Releasing +The library requires Java 8. It can be used as a Java module on Java 9+ via the multi-release JAR +mechanism as the `tools.aqua.turnkey.z3` module. -This project uses the `maven-pubish` plugin in combination with the `Gradle Nexus Publish Plugin`. -To publis and autoclose a version, run `./gradlew publishToSonatype closeAndReleaseSonatypeStagingRepository` -as one command. Due to [WIP in the Gradle Nexus Publish Plugin](https://github.com/gradle-nexus/publish-plugin/issues/19) this has to be run in conjunction for now. +## License -#### License +Z3 is licensed under the [MIT License](https://opensource.org/licenses/MIT). Two dependencies are +introduced: the TurnKey support library is licensed under the +[ISC License](https://opensource.org/licenses/ISC) and the JSpecify annotation library used by it is +licensed under the [Apache Licence, Version 2.0](https://www.apache.org/licenses/LICENSE-2.0). -Z3 is licensed under the [MIT License](https://github.com/Z3Prover/z3/blob/master/LICENSE.txt). The support files in -this project are licensed under the [ISC License](https://opensource.org/licenses/ISC). +Tests and other non-runtime code are licensed under the +[Apache Licence, Version 2.0](https://www.apache.org/licenses/LICENSE-2.0). Standalone documentation +is licensed under the +[Creative Commons Attribution 4.0 International License](https://creativecommons.org/licenses/by/4.0/). diff --git a/build.gradle.kts b/build.gradle.kts index 6baaa09..5aff8d4 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -1,26 +1,40 @@ /* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC + * SPDX-License-Identifier: Apache-2.0 * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. + * Copyright 2019-2024 The TurnKey Authors * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. */ -import com.diffplug.gradle.spotless.FormatExtension +import com.diffplug.gradle.spotless.JavaExtension import com.diffplug.gradle.spotless.KotlinExtension import com.diffplug.gradle.spotless.KotlinGradleExtension -import com.github.benmanes.gradle.versions.updates.DependencyUpdatesTask +import com.diffplug.gradle.spotless.SpotlessTask +import com.github.gradle.node.variant.computeNodeDir +import com.github.gradle.node.variant.computeNodeExec +import com.github.javaparser.StaticJavaParser.parseClassOrInterfaceType +import com.github.javaparser.ast.NodeList +import com.github.javaparser.ast.body.InitializerDeclaration +import com.github.javaparser.ast.expr.ClassExpr +import com.github.javaparser.ast.expr.MethodCallExpr +import com.github.javaparser.ast.expr.MethodReferenceExpr +import com.github.javaparser.ast.expr.StringLiteralExpr +import com.github.javaparser.ast.stmt.BlockStmt +import com.github.javaparser.ast.stmt.ExpressionStmt +import com.github.spotbugs.snom.Effort.MAX import de.undercouch.gradle.tasks.download.Download -import org.glavo.mic.tasks.CompileModuleInfo import org.gradle.api.file.DuplicatesStrategy.EXCLUDE import org.gradle.api.plugins.BasePlugin.BUILD_GROUP -import org.gradle.api.publish.plugins.PublishingPlugin.PUBLISH_TASK_GROUP import org.gradle.api.tasks.testing.logging.TestLogEvent.FAILED import org.gradle.api.tasks.testing.logging.TestLogEvent.PASSED import org.gradle.api.tasks.testing.logging.TestLogEvent.SKIPPED @@ -31,77 +45,182 @@ import org.gradle.jvm.toolchain.JvmVendorSpec.BELLSOFT import org.gradle.jvm.toolchain.JvmVendorSpec.GRAAL_VM import org.gradle.jvm.toolchain.JvmVendorSpec.MICROSOFT import org.gradle.language.base.plugins.LifecycleBasePlugin.VERIFICATION_GROUP -import tools.aqua.InstallNameToolTask -import tools.aqua.NativeRewriter -import tools.aqua.OfficialZ3Distribution -import tools.aqua.TestToolchain -import tools.aqua.Z3GeneratorTask -import tools.aqua.Z3_PACKAGE -import tools.aqua.Z3_PACKAGE_PATH -import tools.aqua.isStable -import tools.aqua.isUnstable +import tools.aqua.* +import tools.aqua.turnkey.plugin.* plugins { `java-library` `maven-publish` + pmd signing alias(libs.plugins.download) alias(libs.plugins.moduleInfo) alias(libs.plugins.nexusPublish) + alias(libs.plugins.node) + alias(libs.plugins.spotbugs) alias(libs.plugins.spotless) alias(libs.plugins.taskTree) + alias(libs.plugins.turnkey) alias(libs.plugins.versions) } group = "tools.aqua" val z3Version = "4.13.0" -val turnkeyVersion = "" - -version = "$z3Version$turnkeyVersion" +val turnkeyVersion = "1" -val z3Distributions = - listOf( - OfficialZ3Distribution("MacOSAArch64", "arm64-osx-11.0", "osx", "aarch64", "dylib"), - OfficialZ3Distribution("MacOSAmd64", "x64-osx-11.7.10", "osx", "amd64", "dylib"), - OfficialZ3Distribution("LinuxAmd64", "x64-glibc-2.31", "linux", "amd64", "so"), - OfficialZ3Distribution("WinAmd64", "x64-win", "windows", "amd64", "dll"), - OfficialZ3Distribution("WinX86", "x86-win", "windows", "x86", "dll"), - ) +version = if (turnkeyVersion.isNotBlank()) "$z3Version.$turnkeyVersion" else z3Version val testToolchains = - listOf(8, 11, 17, 21).map { TestToolchain("EclipseTemurin$it", it, ADOPTIUM) } + - listOf(8, 11, 17, 21).map { TestToolchain("AzulZulu$it", it, AZUL) } + - listOf(8, 11, 17, 21).map { TestToolchain("BellsoftLiberica$it", it, BELLSOFT) } + - listOf(8, 11, 17, 21).map { TestToolchain("GraalVM$it", it, GRAAL_VM) } + - listOf(11, 17, 21).map { TestToolchain("MicrosoftOpenJDK$it", it, MICROSOFT) } + listOf(8, 11, 17, 21).map { Triple("EclipseTemurin$it", it, ADOPTIUM) } + + listOf(8, 11, 17, 21).map { Triple("AzulZulu$it", it, AZUL) } + + listOf(8, 11, 17, 21).map { Triple("BellsoftLiberica$it", it, BELLSOFT) } + + listOf(8, 11, 17, 21).map { Triple("GraalVM$it", it, GRAAL_VM) } + + listOf(11, 17, 21).map { Triple("MicrosoftOpenJDK$it", it, MICROSOFT) } + +repositories { mavenCentral() } + +val testJar by configurations.registering { extendsFrom(configurations.testRuntimeClasspath.get()) } + +dependencies { + implementation(libs.turnkey) + + testImplementation(libs.assertj) + testImplementation(libs.junit.jupiter) + testRuntimeOnly(libs.junit.launcher) + testJar(libs.junit.console) +} + +val versionFile by + tasks.registering { + doLast { layout.buildDirectory.file("z3.version").get().asFile.writeText(z3Version) } + } + +node { + download = true + workDir = layout.buildDirectory.dir("nodejs") +} + +fun isNonStable(version: String): Boolean { + val stableKeyword = listOf("RELEASE", "FINAL", "GA").any { version.uppercase().contains(it) } + val regex = "^[0-9,.v-]+(-r)?$".toRegex() + val isStable = stableKeyword || regex.matches(version) + return isStable.not() +} + +tasks.dependencyUpdates { + gradleReleaseChannel = "current" + revision = "release" + rejectVersionIf { isNonStable(candidate.version) && !isNonStable(currentVersion) } +} + +pmd { + isConsoleOutput = true + toolVersion = libs.pmd.get().version!! + ruleSetConfig = resources.text.fromFile("config/pmd.xml") +} -val downloadZ3Source by +tasks.pmdMain { enabled = false } + +spotbugs { effort = MAX } + +tasks.spotbugsMain { enabled = false } + +spotless { + format("javaTest", JavaExtension::class.java) { + target(sourceSets.test.get().java.filter { it.extension == "java" }) + licenseHeaderFile(project.file("config/license/Apache-2.0-cstyle")).updateYearWithLatest(true) + googleJavaFormat() + } + kotlinGradle { + licenseHeaderFile( + file("config/license/Apache-2.0-cstyle"), + "(import |@file|plugins |dependencyResolutionManagement|rootProject.name)") + .updateYearWithLatest(true) + ktfmt() + } + format("kotlinBuildSrc", KotlinExtension::class.java) { + target("buildSrc/src/*/kotlin/**/*.kt") + licenseHeaderFile( + file("config/license/Apache-2.0-cstyle"), + ) + .updateYearWithLatest(true) + ktfmt() + } + format("kotlinGradleBuildSrc", KotlinGradleExtension::class.java) { + target("buildSrc/*.gradle.kts") + licenseHeaderFile( + file("config/license/Apache-2.0-cstyle"), + "(import |@file|plugins |dependencyResolutionManagement|rootProject.name)") + .updateYearWithLatest(true) + ktfmt() + } + format("markdown") { + target("*.md") + licenseHeaderFile(project.file("config/license/CC-BY-4.0-xmlstyle"), """#+|\[!\[""") + .updateYearWithLatest(true) + prettier() + .npmInstallCache() + .nodeExecutable(computeNodeExec(node, computeNodeDir(node)).get()) + .config(mapOf("parser" to "markdown", "printWidth" to 100, "proseWrap" to "always")) + } + yaml { + target("config/**/*.yml", ".github/**/*.yml", "CITATION.cff") + licenseHeaderFile(project.file("config/license/Apache-2.0-hashmark"), "[A-Za-z-]+:") + .updateYearWithLatest(true) + prettier() + .npmInstallCache() + .nodeExecutable(computeNodeExec(node, computeNodeDir(node)).get()) + .config(mapOf("parser" to "yaml", "printWidth" to 100)) + } + format("toml") { + target("gradle/libs.versions.toml") + licenseHeaderFile(project.file("config/license/Apache-2.0-hashmark"), """\[[A-Za-z-]+]""") + .updateYearWithLatest(true) + prettier(mapOf("prettier-plugin-toml" to libs.versions.prettier.toml.get())) + .npmInstallCache() + .nodeExecutable(computeNodeExec(node, computeNodeDir(node)).get()) + .config( + mapOf( + "plugins" to listOf("prettier-plugin-toml"), + "parser" to "toml", + "alignComments" to false, + "printWidth" to 100, + )) + } +} + +tasks.withType().configureEach { dependsOn(tasks.npmSetup) } + +// Z3 Source Code + +val downloadSource by tasks.registering(Download::class) { - description = "Download the Z3 source archive." + description = "Download the Z3 source distribution." - src("https://github.com/Z3Prover/z3/archive/z3-$z3Version/z3-$z3Version.zip") - dest(layout.buildDirectory.file("source-archive/z3-$z3Version.zip")) + src("https://github.com/Z3Prover/z3/archive/refs/tags/z3-$z3Version.zip") + dest(layout.buildDirectory.file("download/source.zip")) overwrite(false) quiet(true) } -val extractZ3Source by +val extractSource by tasks.registering(Copy::class) { - description = "Extract the Z3 source archive." + description = "Extract the Z3 source distribution." - from(zipTree(downloadZ3Source.map { it.dest })) - into(layout.buildDirectory.dir("unpacked-source")) + from(zipTree(downloadSource.map { it.dest })) + + into(layout.buildDirectory.dir("unpacked/source")) } val copyNonGeneratedSources by tasks.registering(Copy::class) { description = "Copy the non-generated Z3 Java sources to the correct directory structure." - from(extractZ3Source.map { it.destinationDir.resolve("z3-z3-$z3Version/src/api/java") }) + from(extractSource.map { it.destinationDir.resolve("z3-z3-$z3Version/src/api/java") }) include("**/*.java") - eachFile { path = "$Z3_PACKAGE_PATH/$path" } + eachFile { path = "com/microsoft/z3/$path" } into(layout.buildDirectory.dir("non-generated-sources")) } @@ -110,90 +229,225 @@ val mkConstsFiles by tasks.registering(Z3GeneratorTask::class) { description = "Generate the Java source for Z3 enumerations." - sourceDir = layout.dir(extractZ3Source.map { it.destinationDir.resolve("z3-z3-$z3Version") }) + sourceDir = layout.dir(extractSource.map { it.destinationDir.resolve("z3-z3-$z3Version") }) scriptName = "mk_consts_files" - realOutputPackage = "$Z3_PACKAGE.enumerations" - outputDir = layout.buildDirectory.dir("generated-enumerations") + realOutputPackage = "com.microsoft.z3.enumerations" + outputDir = layout.buildDirectory.dir("generated/enumerations") } val updateAPI by tasks.registering(Z3GeneratorTask::class) { description = "Generate the Java source for the Z3 native binding." - sourceDir = layout.dir(extractZ3Source.map { it.destinationDir.resolve("z3-z3-$z3Version") }) + sourceDir = layout.dir(extractSource.map { it.destinationDir.resolve("z3-z3-$z3Version") }) scriptName = "update_api" requiresJavaInput = true - realOutputPackage = Z3_PACKAGE - outputDir = layout.buildDirectory.dir("generated-native") + outputDir = layout.buildDirectory.dir("generated/native") } val rewriteNativeJava by - tasks.registering(Copy::class) { + tasks.registering(JavaRewriteTask::class) { description = "Rewrite the Z3 native binding to use the new unpack-and-link code." - from(updateAPI.flatMap { it.outputDir }) - include("$Z3_PACKAGE_PATH/Native.java") - filter(NativeRewriter::class) - into(layout.buildDirectory.dir("rewritten-native")) + inputDirectory = updateAPI.flatMap { it.outputDir } + inputFile = "com/microsoft/z3/Native.java" + + rewrite { compilationUnit -> + val nativeClass = compilationUnit.types.single { it.name.id == "Native" } + val staticInitializer = + nativeClass.members + .filterIsInstance() + .first(InitializerDeclaration::isStatic) + staticInitializer.body = + BlockStmt( + NodeList( + ExpressionStmt( + MethodCallExpr( + "tools.aqua.turnkey.support.TurnKey.load", + StringLiteralExpr("com/microsoft/z3"), + MethodReferenceExpr( + ClassExpr(parseClassOrInterfaceType("com.microsoft.z3.Native")), + NodeList(), + "getResourceAsStream")), + ))) + } + + outputDirectory = layout.buildDirectory.dir("generated/rewritten-native") } -val copyNativeLibs = - z3Distributions.map { z3 -> - val download = - tasks.register("downloadZ3Binary${z3.nameInTasks}", Download::class) { - description = "Download the Z3 binary distribution for ${z3.nameInTasks}." +// Linux AMD64 - src(z3.downloadURL(z3Version)) - dest(layout.buildDirectory.file("binary-archives/z3${z3.nameInTasks}.zip")) - overwrite(false) - quiet(true) - } +val downloadLinuxAMD64 by + tasks.registering(Download::class) { + description = "Download the Z3 binary distribution for Linux AMD64." - val extract = - tasks.register("extractZ3Binary${z3.nameInTasks}", Copy::class) { - description = "Extract the Z3 binary distribution for ${z3.nameInTasks}." + src( + "https://github.com/Z3Prover/z3/releases/download/z3-$z3Version/z3-$z3Version-x64-glibc-2.31.zip") + dest(layout.buildDirectory.file("download/linux-amd64.zip")) + overwrite(false) + quiet(true) + } - from(zipTree(download.map { it.dest })) - include( - "${z3.libraryPath(z3Version)}/libz3.${z3.libraryExtension}", - "${z3.libraryPath(z3Version)}/libz3java.${z3.libraryExtension}") - eachFile { path = name } +val extractLinuxAMD64 by + tasks.registering(Copy::class) { + description = "Extract libraries from the Z3 binary distribution for Linux AMD64." - into(layout.buildDirectory.dir("unpacked-binaries/z3${z3.nameInTasks}")) - } + from(zipTree(downloadLinuxAMD64.map { it.dest })) + include("*/bin/*.so") + eachFile { path = name } - val java = - if (z3.needsInstallNameTool) { - tasks - .register("fixZ3JavaSearchPath${z3.nameInTasks}", InstallNameToolTask::class) { - description = - "Fix the search path for the Z3Java native library for ${z3.nameInTasks}." - - sourceFile = - layout.file( - extract.map { - it.destinationDir.resolve("libz3java.${z3.libraryExtension}") - }) - installNameToolName = project.properties["install_name_tool"]?.toString() - libraryChanges.put( - "libz3.${z3.libraryExtension}", "@loader_path/libz3.${z3.libraryExtension}") - outputDirectory = layout.buildDirectory.dir("fixed-binaries/z3${z3.nameInTasks}") - } - .flatMap { it.outputDirectory.asFile } - } else { - extract.map { it.destinationDir } - } + into(layout.buildDirectory.dir("unpacked/linux-amd64")) + } - tasks.register("copyNativeLibraries${z3.nameInTasks}", Copy::class) { - description = - "Copy the Z3 native libraries for ${z3.nameInTasks} to the correct directory layout." +val turnkeyLinuxAMD64 by + tasks.registering(ELFTurnKeyTask::class) { + description = "Run the TurnKey packager for Linux AMD64" + dependsOn(extractLinuxAMD64) - from( - extract.map { it.destinationDir.resolve("libz3.${z3.libraryExtension}") }, - java.map { it.resolve("libz3java.${z3.libraryExtension}") }) - eachFile { path = "native/${z3.operatingSystem}-${z3.cpuArchitecture}/$path" } - into(layout.buildDirectory.dir("native-libs/z3${z3.nameInTasks}")) - } + libraries.from(fileTree(extractLinuxAMD64.map { it.destinationDir })).filter { it.isFile } + rootLibraryNames.add("libz3java.so") + targetDirectory = layout.buildDirectory.dir("turnkey/linux-amd64") + targetSubPath = "com/microsoft/z3/linux/amd64" + } + +// macOS AARCH64 + +val downloadMacOSAARCH64 by + tasks.registering(Download::class) { + description = "Download the Z3 binary distribution for macOS AARCH64." + + src( + "https://github.com/Z3Prover/z3/releases/download/z3-$z3Version/z3-$z3Version-arm64-osx-11.0.zip") + dest(layout.buildDirectory.file("download/macos-aarch64.zip")) + overwrite(false) + quiet(true) + } + +val extractMacOSAARCH64 by + tasks.registering(Copy::class) { + description = "Extract libraries from the Z3 binary distribution for macOS AARCH64." + + from(zipTree(downloadMacOSAARCH64.map { it.dest })) + include("*/bin/*.dylib") + eachFile { path = name } + + into(layout.buildDirectory.dir("unpacked/macos-aarch64")) + } + +val turnkeyMacOSAARCH64 by + tasks.registering(MachOTurnKeyTask::class) { + description = "Run the TurnKey packager for macOS AARCH64" + dependsOn(extractMacOSAARCH64) + + libraries.from(fileTree(extractMacOSAARCH64.map { it.destinationDir })).filter { it.isFile } + rootLibraryNames.add("libz3java.dylib") + targetDirectory = layout.buildDirectory.dir("turnkey/macos-aarch64") + targetSubPath = "com/microsoft/z3/osx/aarch64" + } + +// macOS AMD64 + +val downloadMacOSAMD64 by + tasks.registering(Download::class) { + description = "Download the Z3 binary distribution for macOS AMD64." + + src( + "https://github.com/Z3Prover/z3/releases/download/z3-$z3Version/z3-$z3Version-x64-osx-11.7.10.zip") + dest(layout.buildDirectory.file("download/macos-amd64.zip")) + overwrite(false) + quiet(true) + } + +val extractMacOSAMD64 by + tasks.registering(Copy::class) { + description = "Extract libraries from the Z3 binary distribution for macOS AMD64." + + from(zipTree(downloadMacOSAMD64.map { it.dest })) + include("*/bin/*.dylib") + eachFile { path = name } + + into(layout.buildDirectory.dir("unpacked/macos-amd64")) + } + +val turnkeyMacOSAMD64 by + tasks.registering(MachOTurnKeyTask::class) { + description = "Run the TurnKey packager for macOS AMD64" + dependsOn(extractMacOSAMD64) + + libraries.from(fileTree(extractMacOSAMD64.map { it.destinationDir })).filter { it.isFile } + rootLibraryNames.add("libz3java.dylib") + targetDirectory = layout.buildDirectory.dir("turnkey/macos-amd64") + targetSubPath = "com/microsoft/z3/osx/amd64" + } + +// Windows AMD64 + +val downloadWindowsAMD64 by + tasks.registering(Download::class) { + description = "Download the Z3 binary distribution for Windows AMD64." + + src( + "https://github.com/Z3Prover/z3/releases/download/z3-$z3Version/z3-$z3Version-x64-win.zip") + dest(layout.buildDirectory.file("download/windows-amd64.zip")) + overwrite(false) + quiet(true) + } + +val extractWindowsAMD64 by + tasks.registering(Copy::class) { + description = "Extract libraries from the Z3 binary distribution for Windows AMD64." + + from(zipTree(downloadWindowsAMD64.map { it.dest })) + include("*/bin/*.dll") + eachFile { path = name } + + into(layout.buildDirectory.dir("unpacked/windows-amd64")) + } + +val turnkeyWindowsAMD64 by + tasks.registering(COFFTurnKeyTask::class) { + description = "Run the TurnKey packager for Windows AMD64" + dependsOn(extractWindowsAMD64) + + libraries.from(fileTree(extractWindowsAMD64.map { it.destinationDir })).filter { it.isFile } + rootLibraryNames.add("libz3java.dll") + targetDirectory = layout.buildDirectory.dir("turnkey/windows-amd64") + targetSubPath = "com/microsoft/z3/windows/amd64" + } + +// Windows x86 + +val downloadWindowsX86 by + tasks.registering(Download::class) { + description = "Download the Z3 binary distribution for Windows x86." + + src( + "https://github.com/Z3Prover/z3/releases/download/z3-$z3Version/z3-$z3Version-x86-win.zip") + dest(layout.buildDirectory.file("download/windows-x86.zip")) + overwrite(false) + quiet(true) + } + +val extractWindowsX86 by + tasks.registering(Copy::class) { + description = "Extract libraries from the Z3 binary distribution for Windows x86." + + from(zipTree(downloadWindowsX86.map { it.dest })) + include("*/bin/*.dll") + eachFile { path = name } + + into(layout.buildDirectory.dir("unpacked/windows-x86")) + } + +val turnkeyWindowsX86 by + tasks.registering(COFFTurnKeyTask::class) { + description = "Run the TurnKey packager for Windows x86" + dependsOn(extractWindowsX86) + + libraries.from(fileTree(extractWindowsX86.map { it.destinationDir })).filter { it.isFile } + rootLibraryNames.add("libz3java.dll") + targetDirectory = layout.buildDirectory.dir("turnkey/windows-x86") + targetSubPath = "com/microsoft/z3/windows/x86" } sourceSets { @@ -202,187 +456,131 @@ sourceSets { srcDirs( copyNonGeneratedSources.map { it.destinationDir }, mkConstsFiles.flatMap { it.outputDir }, - rewriteNativeJava.map { it.destinationDir }) + rewriteNativeJava.flatMap { it.outputDirectory }) } resources { - copyNativeLibs.forEach { copyNative -> srcDir(copyNative.map { it.destinationDir }) } + srcDir(turnkeyLinuxAMD64.flatMap { it.targetDirectory }) + srcDir(turnkeyMacOSAARCH64.flatMap { it.targetDirectory }) + srcDir(turnkeyMacOSAMD64.flatMap { it.targetDirectory }) + srcDir(turnkeyWindowsAMD64.flatMap { it.targetDirectory }) + srcDir(turnkeyWindowsX86.flatMap { it.targetDirectory }) } } } -repositories { mavenCentral() } - -val testJar by configurations.registering { extendsFrom(configurations.testRuntimeClasspath.get()) } - -dependencies { - testImplementation(libs.junit.jupiter) - testJar(libs.junit.console) -} +val sourcesJar by + tasks.registering(Jar::class) { + group = BUILD_GROUP + from(sourceSets.main.map { it.allJava }, extractSource.map { it.destinationDir }) + archiveClassifier = DocsType.SOURCES + } -tasks { - val sourcesJar by - registering(Jar::class) { - group = BUILD_GROUP - from(sourceSets.main.map { it.allJava }, extractZ3Source.map { it.destinationDir }) - archiveClassifier = DocsType.SOURCES - } - assemble { dependsOn(sourcesJar) } -} +tasks.assemble { dependsOn(sourcesJar) } java { - toolchain { - languageVersion = JavaLanguageVersion.of(8) - vendor = ADOPTIUM - } + toolchain { languageVersion = JavaLanguageVersion.of(8) } + modularity.inferModulePath = false withJavadocJar() withSourcesJar() } -tasks { - val versionFile by registering { - doLast { layout.buildDirectory.file("z3.version").get().asFile.writeText(z3Version) } - } - - named("dependencyUpdates") { - gradleReleaseChannel = "current" - rejectVersionIf { candidate.version.isUnstable && currentVersion.isStable } - } - - javadoc { exclude("module-info.java") } - - named("compileModuleInfo") { - targetFile = layout.buildDirectory.file("classes/META-INF/versions/9") - } - - val platformTests = - testToolchains.map { (name, jvmVersion, jvmVendor) -> - register("testOn$name") { - group = VERIFICATION_GROUP - javaLauncher = - project.javaToolchains.launcherFor { - languageVersion = jvmVersion - vendor = jvmVendor - } - useJUnitPlatform() - systemProperty("expectedZ3Version", z3Version) - if (jvmVersion.asInt() > 8) { - jvmArgs("--add-opens", "java.base/java.io=ALL-UNNAMED") - } - forkEvery = 1 // for hook tests - testLogging { events(FAILED, STANDARD_ERROR, SKIPPED, PASSED) } +val test by testing.suites.existing(JvmTestSuite::class) +val platformTests = + testToolchains.map { (name, jvmVersion, jvmVendor) -> + tasks.register("testOn$name") { + group = VERIFICATION_GROUP + javaLauncher = + project.javaToolchains.launcherFor { + languageVersion = JavaLanguageVersion.of(jvmVersion) + vendor = jvmVendor + } + useJUnitPlatform() + testClassesDirs = files(test.map { it.sources.output.classesDirs }) + classpath = files(test.map { it.sources.runtimeClasspath }) + systemProperty("expectedZ3Version", z3Version) + if (jvmVersion > 8) { + jvmArgs("--add-opens", "java.base/java.io=ALL-UNNAMED") } + forkEvery = 1 // for hook tests + testLogging { events(FAILED, STANDARD_ERROR, SKIPPED, PASSED) } } + } - test { - dependsOn(*platformTests.toTypedArray()) - exclude("*") - } - - val testRunner by - registering(Jar::class) { - group = BUILD_GROUP +tasks.test { + dependsOn(*platformTests.toTypedArray()) + exclude("*") +} - destinationDirectory = layout.buildDirectory.dir("libs") - archiveClassifier = "test-runner" +tasks.javadoc { + // we are using a Java 8 toolchain, so javadoc does not know about modules + exclude("module-info.java") + (options as? StandardJavadocDocletOptions)?.apply { + // disable doclint -- the Z3 JavaDoc contains invalid HTML5. + addBooleanOption("Xdoclint:none", true) + links("https://docs.oracle.com/javase/8/docs/api/") + } +} - from( - compileJava.map { it.destinationDirectory }, - sourceSets.main.map { it.resources.sourceDirectories }, - compileTestJava.map { it.destinationDirectory }, - sourceSets.test.map { it.resources.sourceDirectories }, - testJar.map { cp -> cp.files.map { if (it.isDirectory()) it else zipTree(it) } }, - ) - duplicatesStrategy = EXCLUDE - manifest { attributes["Main-Class"] = "org.junit.platform.console.ConsoleLauncher" } - } +tasks.compileModuleInfo { + moduleVersion = version.toString() + targetFile = layout.buildDirectory.file("mic/META-INF/versions/9/module-info.class") +} - javadoc { - (options as? StandardJavadocDocletOptions)?.apply { - // disable doclint -- the Z3 JavaDoc contains invalid HTML5. - addBooleanOption("Xdoclint:none", true) - links("https://docs.oracle.com/javase/8/docs/api/") - } - } +tasks.jar { + from(layout.buildDirectory.dir("mic")) + manifest { attributes("Multi-Release" to "True") } } -spotless { - java { - target("src/*/java/**/*.java") // do not reformat Z3! - licenseHeaderFile(file("contrib/license-header.java")).also { it.updateYearWithLatest(true) } - googleJavaFormat() - } - kotlinGradle { - licenseHeaderFile( - file("contrib/license-header.kt"), - "(import |@file|plugins |dependencyResolutionManagement|rootProject.name)") - .also { it.updateYearWithLatest(true) } - ktfmt() - } - format("kotlinBuildSrc", KotlinExtension::class.java) { - target("buildSrc/src/*/kotlin/**/*.kt") - licenseHeaderFile( - file("contrib/license-header.kt"), - ) - .also { it.updateYearWithLatest(true) } - ktfmt() - } - format("kotlinGradleBuildSrc", KotlinGradleExtension::class.java) { - target("buildSrc/*.gradle.kts", "buildSrc/src/*/kotlin/**/*.gradle.kts") - licenseHeaderFile( - file("contrib/license-header.kt"), - "(import |@file|plugins |dependencyResolutionManagement|rootProject.name)") - .also { it.updateYearWithLatest(true) } - ktfmt() - } - format("github", FormatExtension::class.java) { - target(".github/**/*.yml") - licenseHeaderFile(file("contrib/license-header.yml"), "[a-z]+:").also { - it.updateYearWithLatest(true) +val testRunner by + tasks.registering(Jar::class) { + group = BUILD_GROUP + + destinationDirectory = layout.buildDirectory.dir("libs") + archiveClassifier = "test-runner" + + from( + tasks.compileJava.map { it.destinationDirectory }, + sourceSets.main.map { it.resources.sourceDirectories }, + tasks.compileTestJava.map { it.destinationDirectory }, + sourceSets.test.map { it.resources.sourceDirectories }, + testJar.map { cp -> cp.files.map { if (it.isDirectory) it else zipTree(it) } }, + ) + duplicatesStrategy = EXCLUDE + manifest { attributes("Main-Class" to "org.junit.platform.console.ConsoleLauncher") } } - } -} -publishing { - publications { - create("maven") { +val maven by + publishing.publications.register("maven") { from(components["java"]) + artifactId = "z3-turnkey" pom { name = "Z3-TurnKey" - description = - "A self-unpacking, standalone Z3 distribution that ships all required native support " + - "code and automatically unpacks it at runtime." + description = "TurnKey artifact for Z3" url = "https://github.com/tudo-aqua/z3-turnkey" licenses { license { name = "The MIT License" url = "https://opensource.org/licenses/MIT" } - license { - name = "ISC License" - url = "https://opensource.org/licenses/ISC" - } } developers { developer { name = "Simon Dierl" email = "simon.dierl@cs.tu-dortmund.de" - organization = "TU Dortmund University" } } scm { connection = "scm:git:git://github.com:tudo-aqua/z3-turnkey.git" developerConnection = "scm:git:ssh://git@github.com:tudo-aqua/z3-turnkey.git" - url = "https://github.com/tudo-aqua/z3-turnkey/tree/master" + url = "https://github.com/tudo-aqua/z3-turnkey/tree/main" } } } - } -} signing { - setRequired { gradle.taskGraph.allTasks.any { it.group == PUBLISH_TASK_GROUP } } + setRequired { gradle.taskGraph.allTasks.any { it is PublishToMavenRepository } } useGpgCmd() - sign(publishing.publications["maven"]) + sign(maven) } nexusPublishing { this.repositories { sonatype() } } diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts index 4724ff2..7e6ddd3 100644 --- a/buildSrc/build.gradle.kts +++ b/buildSrc/build.gradle.kts @@ -1,27 +1,26 @@ /* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC + * SPDX-License-Identifier: Apache-2.0 * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. + * Copyright 2019-2024 The TurnKey Authors * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. */ -plugins { embeddedKotlin("jvm") } +plugins { `kotlin-dsl-base` } repositories { gradlePluginPortal() mavenCentral() } -dependencies { - implementation(libs.commons.io) - implementation(libs.gradle.usePython) - implementation(libs.javaparser) - compileOnly(gradleKotlinDsl()) -} +dependencies { implementation(libs.gradle.usePython) } diff --git a/buildSrc/settings.gradle.kts b/buildSrc/settings.gradle.kts index 5d8503b..2c4732b 100644 --- a/buildSrc/settings.gradle.kts +++ b/buildSrc/settings.gradle.kts @@ -1,15 +1,19 @@ /* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC + * SPDX-License-Identifier: Apache-2.0 * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. + * Copyright 2019-2024 The TurnKey Authors * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. */ dependencyResolutionManagement { diff --git a/buildSrc/src/main/kotlin/tools/aqua/InstallNameToolTask.kt b/buildSrc/src/main/kotlin/tools/aqua/InstallNameToolTask.kt deleted file mode 100644 index a7521f6..0000000 --- a/buildSrc/src/main/kotlin/tools/aqua/InstallNameToolTask.kt +++ /dev/null @@ -1,149 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua - -import java.io.StringWriter -import javax.inject.Inject -import org.apache.commons.io.output.NullOutputStream -import org.apache.commons.io.output.WriterOutputStream -import org.gradle.api.DefaultTask -import org.gradle.api.GradleException -import org.gradle.api.file.DirectoryProperty -import org.gradle.api.file.RegularFileProperty -import org.gradle.api.internal.file.FileOperations -import org.gradle.api.provider.ListProperty -import org.gradle.api.provider.MapProperty -import org.gradle.api.provider.Property -import org.gradle.api.tasks.Input -import org.gradle.api.tasks.InputFile -import org.gradle.api.tasks.Optional -import org.gradle.api.tasks.OutputDirectory -import org.gradle.api.tasks.TaskAction -import org.gradle.process.ExecOperations -import org.gradle.process.internal.ExecException - -/** - * Runs `install_name_tool`, the library linkage update tool for MacOS. - * - * @param exec interface for starting processes. - * @param fs interface for file system operations. - */ -abstract class InstallNameToolTask -@Inject -constructor(private val exec: ExecOperations, private val fs: FileOperations) : DefaultTask() { - - /** The file to modify. */ - @get:InputFile abstract val sourceFile: RegularFileProperty - - /** - * The `install_name_tool` to use. Can be used to override the binary name or provide a full path. - * If absent, a heuristic is used. - */ - @get:Input @get:Optional abstract val installNameToolName: Property - - /** Update the library's internal ID. Optional. */ - @get:Input @get:Optional abstract val idChange: Property - - /** Update the library's linkage by repacing keys with values. Optional. */ - @get:Input @get:Optional abstract val libraryChanges: MapProperty - - /** Update the library's RPATH by repacing keys with values. Optional. */ - @get:Input @get:Optional abstract val rpathChanges: MapProperty - - /** Extend the library's RPATH with the given values. Optional. */ - @get:Input @get:Optional abstract val rpathAdditions: ListProperty - - /** Remove the given values from the library's RPATH. Optional. */ - @get:Input @get:Optional abstract val rpathRemovals: ListProperty - - /** The directory the transformed library is written to. */ - @get:OutputDirectory abstract val outputDirectory: DirectoryProperty - - /** - * Run the `install_name_tool` with the given configuration and store the result in the defined - * output directory. - */ - @TaskAction - fun runInstallNameTool() { - val installNameTool = installNameToolName.orNull ?: findInstallNameTool() - - val idChangeCmd = idChange.orNull?.let { listOf("-id", it) } ?: emptyList() - val libraryChangeCmd = - libraryChanges.orNull?.let { it.flatMap { (old, new) -> listOf("-change", old, new) } } - ?: emptyList() - val rpathChangeCmd = - rpathChanges.orNull?.let { it.flatMap { (old, new) -> listOf("-rpath", old, new) } } - ?: emptyList() - val rpathAddCmd = - rpathAdditions.orNull?.let { it.flatMap { new -> listOf("-add_rpath", new) } } - ?: emptyList() - val rpathDelCmd = - rpathRemovals.orNull?.let { it.flatMap { old -> listOf("-delete_rpath", old) } } - ?: emptyList() - - fs.copy { - it.from(sourceFile) - it.into(outputDirectory) - } - - val copiedFile = outputDirectory.file(sourceFile.get().asFile.name).get().asFile.absolutePath - - val stdOut = StringWriter() - val stdErr = StringWriter() - try { - exec.exec { - it.commandLine = - listOf(installNameTool) + - idChangeCmd + - libraryChangeCmd + - rpathChangeCmd + - rpathAddCmd + - rpathDelCmd + - copiedFile - it.standardOutput = WriterOutputStream.builder().setWriter(stdOut).get() - it.errorOutput = WriterOutputStream.builder().setWriter(stdErr).get() - } - } finally { - if (stdOut.buffer.isNotBlank()) logger.info("install_name_tool output: {}", stdOut) - if (stdErr.buffer.isNotBlank()) logger.error("install_name_tool error: {}", stdErr) - } - } - - /** - * Try to find an installed `install_name_tool` on the system. - * - * @return the name of the found tool. - * @throws GradleException if no tool was found. - */ - private fun findInstallNameTool(): String { - listOf("install_name_tool", "llvm-install-name-tool").forEach { candidate -> - try { - exec.exec { - it.commandLine = listOf(candidate) - it.isIgnoreExitValue = true - it.standardOutput = NullOutputStream.INSTANCE - it.errorOutput = NullOutputStream.INSTANCE - } - logger.info("install_name_tool search: $candidate accepted") - return candidate - } catch (e: ExecException) { - logger.info("install_name_tool search: $candidate rejected", e) - // try the next one - } - } - - throw GradleException("No install_name_tool defined or found on the search path") - } -} diff --git a/buildSrc/src/main/kotlin/tools/aqua/NativeRewriter.kt b/buildSrc/src/main/kotlin/tools/aqua/NativeRewriter.kt deleted file mode 100644 index 8f4a9b5..0000000 --- a/buildSrc/src/main/kotlin/tools/aqua/NativeRewriter.kt +++ /dev/null @@ -1,49 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua - -import com.github.javaparser.JavaParser -import com.github.javaparser.ast.NodeList -import com.github.javaparser.ast.body.InitializerDeclaration -import com.github.javaparser.ast.expr.MethodCallExpr -import com.github.javaparser.ast.stmt.BlockStmt -import com.github.javaparser.ast.stmt.ExpressionStmt -import java.io.FilterReader -import java.io.Reader -import java.io.StringReader - -/** A rewriter that can be used to fix Z3's `Native.java` to hook into out `Z3Loader`. */ -class NativeRewriter(input: Reader) : FilterReader(rewriteNative(input)) - -private fun rewriteNative(source: Reader): Reader { - val parse = JavaParser().parse(source) - - val compilationUnit = parse.result.orElseThrow(::NoSuchElementException) - val nativeClass = compilationUnit.types.single { it.name.id == "Native" } - val staticInitializer = - nativeClass.members - .filterIsInstance(InitializerDeclaration::class.java) - .first(InitializerDeclaration::isStatic) - staticInitializer.body = BlockStmt(NodeList(ExpressionStmt(MethodCallExpr("Z3Loader.loadZ3")))) - - compilationUnit.toString() - - return object : StringReader(compilationUnit.toString()) { - override fun close() { - super.close() - source.close() - } - } -} diff --git a/buildSrc/src/main/kotlin/tools/aqua/Tests.kt b/buildSrc/src/main/kotlin/tools/aqua/Tests.kt deleted file mode 100644 index 3dcad40..0000000 --- a/buildSrc/src/main/kotlin/tools/aqua/Tests.kt +++ /dev/null @@ -1,35 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua - -import org.gradle.jvm.toolchain.JavaLanguageVersion -import org.gradle.jvm.toolchain.JvmVendorSpec - -/** A toolchain to run tests on. */ -data class TestToolchain( - /** The gradle-style name for the test, in CamelCase. */ - val name: String, - /** The JVM version to run on. */ - val version: JavaLanguageVersion, - /** The JVM provider to use. */ - val vendor: JvmVendorSpec, -) { - /** Simplified constructzor that accepts a JVM version as a number. */ - constructor( - name: String, - version: Int, - vendor: JvmVendorSpec - ) : this(name, JavaLanguageVersion.of(version), vendor) -} diff --git a/buildSrc/src/main/kotlin/tools/aqua/Utils.kt b/buildSrc/src/main/kotlin/tools/aqua/Utils.kt deleted file mode 100644 index 6ef0f04..0000000 --- a/buildSrc/src/main/kotlin/tools/aqua/Utils.kt +++ /dev/null @@ -1,24 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua - -/** Transform a Java package name into the corresponding file path. */ -fun String.packagePath(): String = replace(".", "/") - -/** The Z3 root package. */ -const val Z3_PACKAGE: String = "com.microsoft.z3" - -/** The Z3 root package's path. */ -val Z3_PACKAGE_PATH: String = Z3_PACKAGE.packagePath() diff --git a/buildSrc/src/main/kotlin/tools/aqua/Versions.kt b/buildSrc/src/main/kotlin/tools/aqua/Versions.kt deleted file mode 100644 index 632d837..0000000 --- a/buildSrc/src/main/kotlin/tools/aqua/Versions.kt +++ /dev/null @@ -1,31 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua - -import java.util.Locale.ROOT - -/** Keywords that indicate a stable version, independent of other version elements. */ -private val stableKeyword = listOf("RELEASE", "FINAL", "GA") - -/** A regular expression recognizing "usual" stable versions. */ -private val regex = "^[0-9,.v-]+(-r)?$".toRegex() - -/** Checks if this string appears to represent a stable version. */ -val String.isStable: Boolean - get() = stableKeyword.any { uppercase(ROOT).contains(it) } || regex.matches(this) - -/** Checks if this string does not appear to represent a stable version. */ -val String.isUnstable: Boolean - get() = isStable.not() diff --git a/buildSrc/src/main/kotlin/tools/aqua/Z3Distribution.kt b/buildSrc/src/main/kotlin/tools/aqua/Z3Distribution.kt deleted file mode 100644 index 83881da..0000000 --- a/buildSrc/src/main/kotlin/tools/aqua/Z3Distribution.kt +++ /dev/null @@ -1,68 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua - -import java.net.URL - -/** Metadata for a downloadable Z3 distribution. */ -interface Z3Distribution { - /** The CamelCase name to use in derived Gradle tasks. */ - val nameInTasks: String - /** The URL used to download the distribution for version [version]. */ - fun downloadURL(version: String): URL - /** The path to the library files inside the artifact for version [version]. */ - fun libraryPath(version: String): String - /** The operating system's canonical name. */ - val operatingSystem: String - /** The CPU architecture's canonical name. */ - val cpuArchitecture: String - /** The file name extension used by the Z3 libraries. */ - val libraryExtension: String - /** True if `install_name_tool` must be used to repair the linkage. */ - val needsInstallNameTool: Boolean -} - -/** Self-built Z3 distribution. */ -data class SelfBuiltZ3Distribution( - override val nameInTasks: String, - val downloadName: String, - override val operatingSystem: String, - override val cpuArchitecture: String, - override val libraryExtension: String -) : Z3Distribution { - override fun downloadURL(version: String): URL = - URL("https://github.com/tudo-aqua/z3-builds/releases/download/$version/z3-$downloadName.zip") - - override fun libraryPath(version: String): String = "z3/build" - - override val needsInstallNameTool: Boolean = false -} - -/** Z3-built Z3 distribution. */ -data class OfficialZ3Distribution( - override val nameInTasks: String, - val downloadName: String, - override val operatingSystem: String, - override val cpuArchitecture: String, - override val libraryExtension: String -) : Z3Distribution { - override fun downloadURL(version: String): URL = - URL( - "https://github.com/Z3Prover/z3/releases/download/z3-$version/z3-$version-$downloadName.zip") - - override fun libraryPath(version: String): String = "z3-$version-$downloadName/bin" - - override val needsInstallNameTool: Boolean = operatingSystem == "osx" -} diff --git a/buildSrc/src/main/kotlin/tools/aqua/Z3GeneratorTask.kt b/buildSrc/src/main/kotlin/tools/aqua/Z3GeneratorTask.kt index ae550cb..7505223 100644 --- a/buildSrc/src/main/kotlin/tools/aqua/Z3GeneratorTask.kt +++ b/buildSrc/src/main/kotlin/tools/aqua/Z3GeneratorTask.kt @@ -1,34 +1,36 @@ /* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC + * SPDX-License-Identifier: Apache-2.0 * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. + * Copyright 2019-2024 The TurnKey Authors * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. */ package tools.aqua -import javax.inject.Inject +import kotlin.io.path.createDirectories import org.gradle.api.DefaultTask import org.gradle.api.file.DirectoryProperty -import org.gradle.api.model.ObjectFactory import org.gradle.api.provider.Property import org.gradle.api.tasks.Input import org.gradle.api.tasks.InputDirectory import org.gradle.api.tasks.OutputDirectory import org.gradle.api.tasks.TaskAction -import org.gradle.kotlin.dsl.property import ru.vyarus.gradle.plugin.python.cmd.Python import ru.vyarus.gradle.plugin.python.cmd.env.SimpleEnvironment /** Run the Z3 code generator scripts. */ -abstract class Z3GeneratorTask @Inject constructor(objects: ObjectFactory) : DefaultTask() { +abstract class Z3GeneratorTask : DefaultTask() { /** The Z3 source checkout root. */ @get:InputDirectory abstract val sourceDir: DirectoryProperty @@ -36,35 +38,53 @@ abstract class Z3GeneratorTask @Inject constructor(objects: ObjectFactory) : Def /** The name of the script to run, without the `.py` suffix. */ @get:Input abstract val scriptName: Property - /** Controls if the script requires the path to the Java API sources. */ - @get:Input - val requiresJavaInput: Property = objects.property().convention(false) + /** The name of the Java package to target for generation. Defaults to `com.microsoft.z3`. */ + @get:Input abstract val targetOutputPackage: Property + + init { + @Suppress("LeakingThis") targetOutputPackage.convention("com.microsoft.z3") + } + + /** Controls if the script requires the path to the Java API sources. Defaults to `false`. */ + @get:Input abstract val requiresJavaInput: Property + + init { + @Suppress("LeakingThis") requiresJavaInput.convention(false) + } /** - * The generated files' package. The scripts do not generate a correct hierarchy by themselves. + * The generated files' actual package. That can not be derived from the output files. Defaults to + * [targetOutputPackage]. */ @get:Input abstract val realOutputPackage: Property + init { + @Suppress("LeakingThis") realOutputPackage.convention(targetOutputPackage) + } + /** The output base directory (i.e., the relative resource root). */ @get:OutputDirectory abstract val outputDir: DirectoryProperty + /** Transform a Java package name into the corresponding file path. */ + private fun String.packagePath(): String = replace(".", "/") + /** Run the generator script according to the configuration. */ @TaskAction fun runGenerator() { val script = scriptName.flatMap { sourceDir.file("scripts/$it.py") } - val packageOutputDir = outputDir.dir(Z3_PACKAGE_PATH) + val packageOutputDir = outputDir.dir(targetOutputPackage.get().packagePath()) val baseOptions = listOf( "--java-package-name", - Z3_PACKAGE, + targetOutputPackage.get(), "--java-output-dir", packageOutputDir.get().toString()) val javaInputOptions = if (requiresJavaInput.get()) listOf("--java-input-dir", sourceDir.dir("src/api/java").get().toString()) - else emptyList() + else emptyList() val headers = sourceDir @@ -72,14 +92,19 @@ abstract class Z3GeneratorTask @Inject constructor(objects: ObjectFactory) : Def .get() .asFileTree .matching { - it.include("z3*.h") - it.exclude("*v1*") + include("z3*.h") + exclude("*v1*") } .map { it.toString() } val generatorOptions = baseOptions + javaInputOptions + headers - outputDir.dir(realOutputPackage.map { it.packagePath() }).get().asFile.mkdirs() + outputDir + .dir(realOutputPackage.map { it.packagePath() }) + .get() + .asFile + .toPath() + .createDirectories() Python(SimpleEnvironment(project)) .exec((listOf("-B", script.get()) + generatorOptions).toTypedArray()) diff --git a/config/license/Apache-2.0-cstyle b/config/license/Apache-2.0-cstyle new file mode 100644 index 0000000..2819bd0 --- /dev/null +++ b/config/license/Apache-2.0-cstyle @@ -0,0 +1,18 @@ +/* + * SPDX-License-Identifier: Apache-2.0 + * + * Copyright 2019-$YEAR The TurnKey Authors + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + diff --git a/config/license/Apache-2.0-hashmark b/config/license/Apache-2.0-hashmark new file mode 100644 index 0000000..3248a27 --- /dev/null +++ b/config/license/Apache-2.0-hashmark @@ -0,0 +1,16 @@ +# SPDX-License-Identifier: Apache-2.0 +# +# Copyright 2019-$YEAR The TurnKey Authors +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + diff --git a/config/license/CC-BY-4.0-xmlstyle b/config/license/CC-BY-4.0-xmlstyle new file mode 100644 index 0000000..ecababb --- /dev/null +++ b/config/license/CC-BY-4.0-xmlstyle @@ -0,0 +1,12 @@ + + diff --git a/config/pmd.xml b/config/pmd.xml new file mode 100644 index 0000000..298ba53 --- /dev/null +++ b/config/pmd.xml @@ -0,0 +1,71 @@ + + + + Common ruleset + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/contrib/license-header.java b/contrib/license-header.java deleted file mode 100644 index 7553467..0000000 --- a/contrib/license-header.java +++ /dev/null @@ -1,14 +0,0 @@ -/* - * Copyright 2019-$YEAR The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - diff --git a/contrib/license-header.kt b/contrib/license-header.kt deleted file mode 100644 index 7553467..0000000 --- a/contrib/license-header.kt +++ /dev/null @@ -1,14 +0,0 @@ -/* - * Copyright 2019-$YEAR The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - diff --git a/contrib/license-header.yml b/contrib/license-header.yml deleted file mode 100644 index 25e7aff..0000000 --- a/contrib/license-header.yml +++ /dev/null @@ -1,14 +0,0 @@ -# -# Copyright 2019-$YEAR The Z3-TurnKey Authors -# SPDX-License-Identifier: ISC -# -# Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby -# granted, provided that the above copyright notice and this permission notice appear in all copies. -# -# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL -# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, -# INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN -# AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR -# PERFORMANCE OF THIS SOFTWARE. -# - diff --git a/gradle/gradle-daemon-jvm.properties b/gradle/gradle-daemon-jvm.properties new file mode 100644 index 0000000..858feb7 --- /dev/null +++ b/gradle/gradle-daemon-jvm.properties @@ -0,0 +1,2 @@ +#This file is generated by updateDaemonJvm +toolchainVersion=17 diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 0c1116a..06a4e2e 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -1,16 +1,41 @@ +# SPDX-License-Identifier: Apache-2.0 +# +# Copyright 2019-2024 The TurnKey Authors +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +[versions] + +prettier-toml = "2.0.1" + [plugins] download = { id = "de.undercouch.download", version = "5.6.0" } moduleInfo = { id = "org.glavo.compile-module-info-plugin", version = "2.0" } nexusPublish = { id = "io.github.gradle-nexus.publish-plugin", version = "2.0.0" } +node = { id = "com.github.node-gradle.node", version = "7.0.2" } +spotbugs = { id = "com.github.spotbugs", version = "6.0.22" } spotless = { id = "com.diffplug.spotless", version = "6.25.0" } -taskTree = { id = "com.dorongold.task-tree", version = "3.0.0" } +taskTree = { id = "com.dorongold.task-tree", version = "4.0.0" } +turnkey = { id = "tools.aqua.turnkey", version = "1.0.0" } versions = { id = "com.github.ben-manes.versions", version = "0.51.0" } [libraries] -commons-io = { group = "commons-io", name = "commons-io", version = "2.16.1" } +assertj = { group = "org.assertj", name = "assertj-core", version = "3.26.3" } gradle-usePython = { group = "ru.vyarus", name = "gradle-use-python-plugin", version = "4.0.0" } -javaparser = { group = "com.github.javaparser", name = "javaparser-core", version = "3.25.10" } -junit-console = { group = "org.junit.platform", name = "junit-platform-console", version = "1.10.2" } -junit-jupiter = { group = "org.junit.jupiter", name = "junit-jupiter", version = "5.10.2" } +junit-console = { group = "org.junit.platform", name = "junit-platform-console", version = "1.11.0" } +junit-jupiter = { group = "org.junit.jupiter", name = "junit-jupiter", version = "5.11.0" } +junit-launcher = { group = "org.junit.platform", name = "junit-platform-launcher", version = "1.11.0" } +pmd = { group = "net.sourceforge.pmd", name = "pmd", version = "7.5.0" } +turnkey = { group = "tools.aqua", name = "turnkey-support", version = "1.0.0" } diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar index e6441136f3d4ba8a0da8d277868979cfbc8ad796..a4b76b9530d66f5e68d973ea569d8e19de379189 100644 GIT binary patch delta 12612 zcmY+pRa6|n(lttO3GVLh?(Xh3xVuAe26uONcL=V5;I6?T_zdn2`Oi5I_gl9gx~lft zRjVKRp?B~8Wyrx5$mS3|py!Njy{0Wt4i%@s8v88pK z6fPNA45)|*9+*w5kcg$o)}2g}%JfXe6l9ig4T8ia3Hlw#3f^fAKW63%<~GZJd-0YA z9YjleCs~#Y?V+`#nr+49hhsr$K$k!lg}AZDw@>2j=f7t~5IW6#K|lAX7|^N}lJ)I!km`nrwx> z))1Es16__aXGVzQM0EC8xH+O!nqTFBg9Ci{NwRK*CP<6s`Gq(~#lqb(zOlh6ZDBK* zr$|NDj^s6VanrKa+QC;5>twePaexqRI%RO~OY075y?NN90I|f^(P# zF=b>fZ73b5JzD`#GC3lTQ_B3lMeBWgQUGYnFw*HQC}^z{$6G4j(n4y-pRxPT(d2Wgb%vCH(?+t&Pj z)QM`zc`U`+<~D+9E{4Uj2kc#*6eZMU$4Oj6QMfA^K!rbl`iBix=2sPrs7j@aqIrE zTaZJ2M09>rp$mgyUZ!r2$UK{+DGqgl`n;*qFF~M(r#eh`T{MO?2&j?xgr8FU$u3-` zhRDc_I23LL4)K&xg$^&l-W=!Jp-P(_Ie07q>Je;QLxi8LaEc%;WIacJD_T69egF?7 z;I_Sg_!+qrur8$Hq4grigaiVF>U7uWJ@Hkd&%kmFnQN-P^fq0gB1|uRt!U#X;DnlV zo?yHWTw7g5B;#xxY`adhi4yZn@f(7-Xa(J6S=#d@&rlFw!qfvholE>MEb|VWn^g}G zMSrK&zQ^vDId&ojL!{%{o7?s{7;{+u%L{|tar(gp?Uxq3p?xAysB>0E$eG#$tvkk9 z2Q2gEP17{U6@UD*v({5MP-CTZfvWMItVjb4c;i~WLq&{?Q1(koX&vt7+$z}10{^Id z{KDjGi0JpD7@;~odF__0m|p;5rIrHidOP9^mwKe#-&JX-X@acc)06G{LO1Wu)#gvZ za~y9(fhA%UwkDOVU1LBJ`0ROE z4&)dJKK%mG@+CIm?+wt9f~@xIMr8}UH*K1j| z0pppo{7gv3v{URwxVMeg>Ps!L5IKxm zjac2egjgb0vH5i75$s|sY_RYec#>faqJk|AGgV;v=^%BM(^p{p;(^SVt-88G9f!q; z>p}9E4^f0=01S2pQBE4}9YqE%TV)*hlU^8k9{&=K76+*Ax^r=AkBb%OCP^P2nm0Ri z;D-|Zk?gGeU<12ti2CnPVNA(Pb)02+r|&yTWW-OJO7 zNLb0pps6aN?A~NJp5kj{{IOlf!5KWMleV@-hYLift)D>-7K+tgs=7Ake}oBnIy-y1 z(Hn@Hjw=_(x>dO5ysQsrnE%A*bk0K<-j{1Yqz@#n#jOL^AzCr#wR|WYzqk6i7v)Lf zkXdKxzuu20aP{Tbg$(+9&oh7cd(Uoqqf<#ujb$q4sZ~gxFbQfS zS)kNklyL*{2AELgjZ(LBu*>S(oH5AaJ;YiB@;l@=O%F6B?oanzoYRM^fQ9-<~^=3$H0g^JPMLQo@SZ@QuNvy)tyJ)LSj`+()#fy?{aV4Yg^7dlQ7AQM^3GLCR2dAFR zJjtfKiVqF`l-H_fz0HD|9g>)pOxn}k!vdZ=DO!7Sikm{Z%P6BrRkBS6W?ZB5W&7rT z@uYpf@M@a!z7H&o@-yrcCL^Ff3e7p3T`R9p?@o-acXmbTSa0>ZANzCSgovsd%;i$| zVus`not!oL#(W`L-!9w0jdaECaG4hk{V7IOs676ZquZH~0TX5hDq|)x z6T497l|E?f4)LA>j=S8}b$0LS=I4h|hUFJYJODT8Li@#6kF$k0)@*l{RnM1HQ%?VT ze-Pqlc!~t(oumVC*?5fwR;P6u{tHaZ~*LlD;B)4f? z?lpWfa2P@)g57flVl83Ej%P`2)gGyaPjhvD(%i~{`2b>#3!+y&` z!2nuwHMFA-zUY}f1^0B8<`N)Gr=A4TS@b1qykmd0Pq{?r)+1^^+D(=xasb^Tf!oK9 zBLL+*p6M_#ufgLzgq1zcSwZsZnQWFLC3`Yxdg-2=*tT`J9nrfYt)RF)YryBf8_gW{ zvKbB+oZLehfT)S#<|y1)E0hW^?+AnqPXq9Hu;v3dsMGdr{SVyF63;K<8VcgI#~}1i zLYSBL0K;RTT(;>2x=*!1Di9w0mwr;`CN}kM65|Ay{~z}_^JKOsRaN<~#9O^iiW<5P zYN7r~HV!#Nz~IZU`P>1Xe%4f~K}KcF#X&5kO*G}-)74S*tQ8CietdPcA1Yl;S=Mr# z`#MYY!{s^uo=jn7;k6O%(}fN+*0cWMpt~#n9DR<3NyU?+3D^AgI}S)Cu-Tljg`VY} zX1=fq$?8$DtOeGxE6f8lbS_6Q3C4+LDTO$}_IpM$Xv<|QSC%+Oll^q$y`7o@jD{dp zNDl|&X)r7wETa-#h*d`KXntxI(Y{vLha{$0i7@G8xx^m=c<{lJ9?p-i!^W{%j7-oo z0W^SzZ^(Wkyz*We{lEn%Yhu-ycUOHtrRiVJL4~&S91*D0MrLu}Q>v-Mc?GcWfpyz% zX|UvcN@krFO#@v|CtYM}g|=L3%aMo$E5<@CM%c*;?u>LOTz00@+dt1{yg1y=$h+{|D17U}$*^fE^H&8b431EUE z<9tv0V_#%#&1N#j7AKCj!tTK@J%oFW*ESW<(#Gl#Xs%v<@AitI?s92nLzm<)w3Wkkom1f$gcdUi%g_*jofy&}N#luL<$GVIe{iQkQ)sIHVy zBgItnPBFamrv6Kb{eE($Q(f`ZPeW!Hm%Y@F*OF1sKB{Yy|C>WEv_mfvv-N-jh)B-5 z4a!1WcT@9a+hGaBrc~sz=>G?Q!*Zp^JFRUvBMyNR1;`)j$RhH$6gEyVKhd$&K-CFT zXaWC-Y=fyOnqT84iMn9o5oLEOI(_3fk!W^8-74|q1QhQ|CmT0i=b;6Z3u?E{p7V{? z;f#Q-33!L+4&QQcZ~GAqu$NS{M;u%`+#9=7^Oa5PKvCCCWNG_~l(CidS!+xr-*gg{ z$UQ`_1tLT_9jB=Hckkwu>G{s0b0F4bnR7GibmHo?>TR&<3?D;5Fb#gd8*wYa$$~ar z7epl1qM)L{kwiNjQk}?)CFpNTd?0wAOUZ|gC{Ub|c-7h~+Rm(JbdoRe!RNVBQi!M8 z+~U6E2X&KSA*T6KJvsqwqZl#1&==Dm(#b^&VAKQ>7ygv*Fyr;)q9*^F@dCTg2g!w~ z%hg)UXAUyIpIbLXJv1nZX+a_C)BOH2hUim|>=JHCRf(!dtTidb&*~I!JrfRe+PO>w z@ox$G2a3i9d_N9J=|2$y2m-P&#PTNwe!oLBZFs;z|F5kXvBDn<)WwE0E3$ow=zg3R zK(9;sf0t;VEV3@gAg7jRtnj%-6O@!Hvg*;XcUAw}!=2*aErvB(eQIm(-UGmq^J=XN zTqJo$Y|WKo^HlBF3BXJrA#}7ZLg=r*w`I*~Ix`o&2k8^(0mt8Rp=A>F`&gehhp@Jy z^e^#B2!~$LvNCKugg)8)-G%&THdk~kfextilegP9?#C#()F59U$&eo(h|5>ceo*Em z{PEE79T$YP|Kr7K`WBHbtQwyxFkCl6xX&+oUf90B5xoi3_5KHHCyEE*oPbOQkfMz& z6^hT8_NXd2iWk{q9IKae1{_7hMPH8I7_BMtVOM4 z6jm?E0QJOn$qrgsJ`9w##GB9?G})-GXSQo6(tYS(Q0-Ct$co?Zzl0?NHsDRron?;_ zZZgQg)%XW>P?8_&zoGuF(>Och2kEJXsu1_X&~w87x!b z>~h!a>e7{`p@+#hXF88wI*JeWRZ;J4ev4<}HWf|Z;(7$E!S5l9wzBHFe>^I{2`a;a)QnAwa2xv1e(bq$<}!8o^ofGvYpk7dBR+`*%iE;hUY5 zaHF}OjGO9r*{%lmcK^uFiTHgoUD`^9Nx@~;Bg!V* zuuJ&ti{DQiq7RyJAR94wem{}cPK1J(Yxnn_{=>?USqz-~&QXRStS^s-7TksZ$AEI! z#og36s3JGtGU{CnDHRFtipFqvrE*gw7_K@NN0h+ItTq@4fqN!HeQU1y7*X?9+IfZT4Vxebpt z%#VzgdDK~-&+=Z*#>=n#XUhNvBZp3=Cr41jMqwJkHLf3L7Vm~V#GgJ(Jpii~PmJ#s zA7Ft!{xD@z>9DUb4JbiUBdNEcU4BO$651iN*mp*f)HbRRM`Cx5cR?5IfEcU{IZWwf zz(M6CDv)>xa3x}K6%tP^i15P1&&DOLK=k~+jNR$UK3frSl+|PjSC-dBItvD~LL! z>_g(YYdO4k(5EbPOw+v+;G7~jYm>F@Ai|o`gs%F)F8tDz$dl7Q%aCe|v|$UkAul_R zNlA-beBX^IJU?kgS`E$it7nF4DaI!SJAGq)2P&Few(-|tp z?K+%D3e4{pfkayrcbm0ftu6Ol2ZzdKM+4i!hNP3NRL`EvvZJ3yvNr2MV%igZ4kj``Qrdb_OI$7jWP z;l0DYf&0(-*QcP5zrP`HVznW+SbH63Qx$7_9~NjRNg7eKqI!UJ=XH`g^=t8GiFTu( z?2L{JKEu%jJx&XjNzU(*!ZNmL1@RlJA0G$2_LrAb_7lmjil(GSlSM zwTes`m+3R;3#N~Xg#9owh3ycXV8@ZlaY_16kpPFA={721b~URO4HD3sp%fmkZM}k) zZB0#)kP=RkNB~R-MCk8aljG_bagt4vIb~8)BV%(b8_;)&Kf9GX+%O_cNG|(D$!3&D zL(I8}*LqN5NntipFlN13=`D>6!{D@CFMBH0kW3=HccJV+xW~|$qeFR5i-2{X+iWMu zI2$gepQ)H_B%ip_BlWOQ*|pErXs|4ir{IHccgaIJ84irE{?+$KDABXr&f`jB^V-c% z$$u`uU1YB^{<+UN2cNg#7&0bz@yF?5>j|;)5&IV3wIQp58X#OE-M^$HdyvL|Um5t? zhZlAG!Mz%XkUe3t471JM*Yur}o30vzu6RN7gJyNcf!IItsDO730mcJ*O!~V``y5=3 zNJGp34DZ}wd1H6V`Uuy%es>BiO_aE-S8jzir#$& zyk)@2a5tP$@g%jW^b^JGdo)X@Q%sE`^lDQmY9m%uDFpPX`w9%=yQ+nneMm#OaXcD` z9}{tn5A2b2z9783vL2_jSao?uxJhWJoq%47*RafM4o0@gY(p)F>qT4^XM5GLzV#6j zC+HoGhAne7o_w{WUo(B++z7lU3Y0k1rYv9|TSv0vR-Du(5=VakbbelgZTeDn+a_Wv zq_j-^+Qz1WAl;Zg>ahX|CERbX1V%B!hTKN?M}fGoA07M(WU&NfT&TmN`P@56U2 z^)vLDs|Ln~0iTtn-?KTeQl@T&bskJFuTUS!m+$CS9vnd}8(UMO|Kv6TCfGN9NUu&4 zL{)GTxPq>fwsJ~aU=4Qhuq8*RzDsP(LZh$BHezq&9gK$IS<|DYbm})$QTGCS6T;Dr zEkLct!b+#<1r9OKG@P!f1wm8>=Nz!7OzJm!g<+`?N3;YaA3(P@EL=(sTaRMDD!c8=-XN^4BXp(eVkj$NmEMYPP>YJ4bJ3yUud z<3BeJAJ$6z^TuywnfH5lv#$lgwraNw{IV=tIznPH1DT`v-5yS=!)J<}xxl}uZf9azA2A97Haf!;<3y01hlw?dWNEv@TLi1s-mO4vmIT%O_42nS z$VRWrs9NngqRRkWAnWkn%`Rw@?wH|)7XL`EL5EZu$qyJW31&CB^T_)qwIv!{;E_6 zo-9XAryQRlk-O0>o#-SZO>|6OYq;}<*>Wu1AsVRiXY4f8qb;+sItv3AyS!4Ry+q}) zA!pAB|BmC;=RIOk^^vlsEH(!Q!7_1FK~ZB2err*o!+b(r=m1b?$6d!%zmN+69LXnT z&gRmM+n_R-F@sT*IYv0_mGPvur!u`iWbQO7SqiGFLeY&yga zf`lM&B74FA2C?N@8_z652fjhBEoDUKbP8hL{0{HAF%qDo7)o3=3rg#6)T7%%5^wl% z9R0*S*<~>nzYOdQk2l`9h#t+gJy_xujw6xjV(8S<_DbVg61&pT%Hi42l%D73G?adn znB%UdNM0p}lEF-P2%TAMam2zpQev71e>a$$%i+r~b+D9G9pF|oY_*(-u*89oKsXLY+UIbqq)MQ%(GYS{(*n_S_*RN$*~`zUtab%0aKwhx znc)Yo?{xq1sJCgQD)TeTci1ucvbez9q=A72H(-SB18Kl&6^vHV8^i!p@>iF!DIw17 z+8Q)TNisB7>pwyww4y)yJx*wX6SJO78eLBC-ar1+k$Z9fy;wBD|3kzI{<+l*>PSY^ z_?nLOZaeWbU@C3hfK?X;Di*8CHCPkx2qco6(ZyJdqSzp^TJ_5Lpa0UP{Gy+!b0Lr% z@xYxSjUKoY6L#>$qx~KD$-0=|OF7zhVP~ntMgEALYPIfhj@+ z!;JJ7te>CcovruwHsJH6Lta$nm|%^C@=V-rmhU{+I~0(|XHQ9jt@L7pb{gx#{4r!) zg($FyFTslcgu(~6lYr$nW?)%*l#VJ=R-jxK(x=t1bWlu(nL66T#qj%3aZ@uVhy}Co zDU_q61DD5FqqJ*#c|(M5tV)XBN?Ac^12*q)VN4yKPJ|#==S_`_QD9|0ls!`2)SwuHDRA_OfXQDq3%qW&MZB}Z!=k-9xqev8jHz(H z{^D@cIB~QiK>~wa)A&^Ll^Wi6QgCzU;iv-BHsLBs zH7=jN%|>0S`SjP%M&AF1PNVDp_FZ?2Bm@7`DC&v(pYrw!!yD#4 z6+<=HS0Ln6MhoKxF<%~H`y20{vf#pxh=;j{zY381gvAFekgG|>G1zo8$&az{V=;JR zy_puF4$L$?EMhT?;TpQoR*j16ll`#AS4e96C}yp_aGKkBe?1H|k_;gG-~Xorc<;lI zkB}fB{$c-D2mGA&{rm<*@F5)c3X+6??g~XoEwuzSuch0D@W~P5(2I8v8F$c2$Vw51 zP#YLSBDqtWW^EYBl^QYHF+MA7am6f4DOhwnJM=W9$uvMOsZ%_~?)2C#wb?CkI$7{K zEi)=#|5pFvg^){zK5kpBLjB2kZ+$ZB|L=W|aNwyyb(gC2l7bcpx{E-H@)q6@D6N^xh`{1E%ItF2$eeB_SjI@b2WgTpS1thwg&n`jiIzw^TtXUyB{00($GIq>vbj|}bav}}Q_~wp3>k8!E@hVC;OMUTu|= zAy#vXH*GrUHu7^cNZWe1>y;2(51js9wbu+R3Aa*(wzH9+X0dIsf&gc_x|_LP z>~CF^?(~U}+l~ehe|i>?4eo!xkq&Lk+RR-1duNP#o~>@1x)s&i&u zRaYL@+D&_M|JLI6fHbEr_`U;HgPTh#E3?sB)A$*gqyBgg*ql|a-m*TX5rACbWKCE6 zdeQ`v8m6>g^ugv`p|HY^#1QZrGGUj0^HVDc@{?Q0yhalbBEV{+|HzC^-{&e{5K%z9 z6Bxtnfu1!@Mp+Q&*&~;FOg&*Vm<@4b;{FG0-!UUXX!|)1w}op!B_|7_s~d(+=9Gba zKp8`LaB4D(H=cGcspJ_TjYaOwMb=sGn^gtUVhK!UI~2KKYEE-NC}F>+BEY7IVvy%KRvm00tg!Q`y=er}wpEetX}K@;}(}{s9AzV#q2@ zBy7}->|N?13POrs`;U?(qAG(I$~Gt+Rgw%aNZ_0fs_utVvRJT-7z4!@x36v@=NBX=IqkK{#Kg0w48de@?#Yb4M(Svj5=T+<ONr8-oh7l?Cji@+erqur zFhZ=9|Lk=$`c}v4u`)-!!UI=!9Jo@h&7p4RlS#u! zZ7-prn75JkV?VjptX;@$#`U`{vB!=Z?V`T*FBF>J?vsML7e6@2GbUteMFfX-TUu{2 zLNIG*;dV)8GV8gAgEf#)X3A>p3^CRka1v?~8x^anBhQ=L=LsOl=&pcOYHo98m##ye z34MtGCDK!`ptl?taGMr5q{!zVc? zG00e){TV?`YA9eB;(lA3lXI?RrB4BYQGk?vOmTIUJED=(`_*gtn2DB-t4WW54as*W zb2kD-lWX>lb$+W!VFakki>B^Vc+u$?NLF>)!U%b@Y}gYJ>m2H=^x0=nsE0TF^Yu0h ztgH8-o1%+jCk(+&`|)tTfEVHq0cMeFa{Uz)X$;fCq%Y=SOWML6bYfeP8j5hktL`KK z(18`XrUn&WN9PtFxh&dX`y~YBsmdhi7Kw%tKzM%^VEhdD<_XkulW-x=JN6OPbFI4@ zzDDRN+f=@{0h*MswwOqG6gJ?{NuHx(y-|FUGsxyZ*x0~$MW(eY>vqq4Fh#t7uzw=- zKB?|!0N~!h^AMdLa)oR!Ca#HZ9&Zf)ghuO<^RN)4twRlygHnQG(BE{cDc5E}OF4;xss6gYyV~EcJvJkX)xNWb=@yw!uq0v-sf^rvkp-;?DPWK@*SEw|V;IH=7 zfQqEV_>DjOPT~8X*J|H8=&RnzK4~S7ML~nLX^%s-Vqc^aWy7N$y57qciZGcqy#=zU zs8hcHiI=D$+RB{|62{ohCTiaML6FI4Uhzo5D{Jik@poCs0w7F)*w}F4r0sJ~#u-72 z5bK=ANt=M$Dh5NKnxGsg9NRR?WD-x|FhTwBjd zD<-K>44DB~i%frJOfnzh1R>PRY34kw!6~p3M$JLaD1r@`=h)~Ngks-(gdXh^Q?BTP zZ^Zj5w1AwtuR2$~E7s9iZdF}z%pv1em^V2rM{1tLUY@-+Sc0(9jA|iZWml1;v13=U zHf?y@#mb--7z6$ue>`qjhE~brk$AY-RG90~5wcBbDReXR2)pKg{L>;H(DI`U!MLNQ zY9rFJP@ZQ}jlcMh%WSCo%vf+nd0Gmd*F%KMIe>slCUh)8Ma|;M_I+v#;|ueg9oLg; zq2HtZX%&#F7vdpNlkX?}(C7dGC^y#NB#m4%69RzTNrk%4ol~hSI%>2r6B|*ZkW(*P z;u#s;+faHo{tfy+1L^RzWDi*^JR0iY(zJDB36y_QJ+|E-2x+cY z!V8uLNktH~q>WQZuY!Ap66WP|E!0PA1jK~)^8oJVGbspJs6QL!!-5Qm7 zHYI|_`Actg?vDzdg5{86w@GS$G6ANzff7->6i5pB$T4O}`fZ_;{217Om0gN5zTr12 z5mW{hCzCE-QubjxN$TAE-XgI-8dTY@OZmq`y+y_>dk*(qXF0{nam|q@~i}Utp*k{yurq(DW54hkDT4bbg z=_etM?Nf5W^o-HEu9_?&xEqPg^P^mTxLH8n%u$!mWvFG|{&)jtnU&6|5-`~eaNz0%D1BDo`{ zS1N5(KW5v^2eLdd_%`uaRndF@h0Uo6=M|8?b~KbOLZk{HXEnGmtgZXf2inI*1r%n! zQ3&%RI4r{f&dwW~HwH0Ked9b!k6{>_19H z_Ai>5IChDMY(FfMyG%;30?SQ{iV9KyGru62+Y)~qSQ91}b~}w<&*}R&1c#$O`H@~c z5)2S_eXx}M#N{MuGeQS9@#UJB@;W_j50b}jIhxMPloEFQZdvwxiU^RYycTzgK)-vl3LT&$L8~@68$C8~5_U{cR$E#w*x65(qw&eoL@>%ZHvj zWnEMlSh*(o&oy|J7eJ5OD`ssy%F?*Vp?`Cq;FShyl{ZoKCG5g{y}>usznni#8ki(i zO{w@n{iAj1_ooX@+s*!uW60WcH~*bNOT6z%0jVML5};wVrQp~`Uss_{cO2oud_nNA8^B$?07fJ6?iI)Q zuo9G)O-z)DqstrBqf>B%S05hf-wep0@$BFHKSrkZ{za3D)yVzRz)2{wf8(Wp+xyAM z$rtyx$gi3A=V~V!`Q3;BM0$>*VVtxEM|xDL^gew7ydy3Q6YzD&THRz*q33Ms_D;M- zbCx1Ft#UNB)V3bf`~{ImI72OTp^|bF8?G8#FRj+Biy8ET5#rA3sd|0FR@U(LAJ%w8 zS1%n8Z=Amhw)92rIsof=YVWF4jw&F*j1LG@-`+cR0-~2LqXRH8(Ccne{y#MCPncF64U`0uO zWmi$dlii~1D0rLR{qc|_2M!C$t8^=G7xQY)9!#Y331A|>N)EhmyVdLWL9I3YLJ`7? zZmpqUJB>Ni9oiL)^1IK1UoMyhWE{$9M2M6Xi zPKk7GpMsA6vjZbU7~i+u|J6Nk|Ci!Y3UMUT2|`M;JsNQACdJ%ooo9Yt{?A+0hMpxi znEa~~sxC>rKrU6bd=WRb;%wsH>A#j4{({&1GYSNR57Gama(3)2A;SM>qop}l>Jk2* zn1+C$fIxuwzg3mCU#SOqb-wOCb6mBcYlA5+mt<&_J~sBxc(GQtBFINUO~Mr7<-uu($>P HJ4oML2Lo<@i8BwbL^1~GkG`E7C$SEa_ zF^}Ea+#Je`Xy6;#D0FPnSrR%Y!QGA~NA^{oWmW8C<3dr{x6wWQ{4+bzemqV5W$i5~ z=J0jXZ>uZb>DT@0Ks?4QJ{`z?8JWl3$y;2pj#$XP*pv$>$g(z43{YH9KmmR6<#sIn zA`#=0#sgycaBQ^&}Xba!|KaZ8~b30v~nLt z9%#gz_*=~KD{3t^X~l>480*}PhKN=??g`RV|4Ud{Gyyl187MJ}r(#e+H$GEdI+p1s zq_25h;fV)$EPK%Dw-(G=f`yHB-_tttsC!?k7*#!|4a>`Ahj8nm?&n>NRs%jkZW^3-0P_yMP5&*6a26{MRj1&TPF zyE#|c)5uUHzMWx=rMKpuPih*V=S;W3MzIZTw2uTbr}8`p2bm+Z6Sa%vvWAWSf4H)p(+ zSQ8;EvUa#wqWV+9vmIio(%7wukK2SwjUS8Yl%Rq%=~PU)2$Tvm6`1!r3H@U#_|bB0 zmlT1PS3wPB(b&^+@YY7Y$n4l3mV3-X0$>z|gZp6O*Lhzn&?Gad2ZCF;+#95-Y?#y+ z?*l@Yf=a4w{Px=o!N|3~_XKfk&G;fN>Ps&dp2FpA~qD=0~=!NOS@B#XAKKkND>Y{4>rqxrViKD7;?>j8`R` z&G)3FN|dfsxnaI^!d1G%=>AbTTxZWo;n-DLrQ!sj=f~VAOe5zhGS(dgx|!ls62fbX zV@<7Ck^!}R=`Swr?(7w1rY6Nmq~sfXJ?TiKJLn=&SQdEt9$@0 zA+h1Wbwbri0s-stc8yVq;mRa6@kEf8^KXUz&jcic!+avDvvJFa>k0ioWug=T3oPw; zyj4it&0@>_*uI@2=^+T7sL1_!^aJW@Xfo8aC#3^WtQC7fET8b9C} z*u^ue6Ojn z7@(eskJ2+cNnH9~VyfIh<-|7!je~vGy*odz(sk-u$~SrYF3glruZ*W`{sqnS+9=;Z zh{D@MSG91%lr&ua8%$sJF%y1I<|e;EdfJykY8#D$Hc_81n5`$7;1N|b0tvvPLzSg& zn7!5x?T*@rQUKcUhTIjV(rw*5oQYlm5DbEO?60#mohHfbR$3_x#+PZoYi@Vd4`#YgKyTd^!4n{fN~WZDY61sAOm6 zl!d^i*a01QxpWM9Pcl?&{RgO}uq%ErOk5WpECvnfEh!*YP&1Sl)uTN4hg??Vqs~i5 zYsfufz3?{TtwuBN=`0~Qg1PlWH#OGG$ zLLWU17$v``)CE1cds_7kj8mJ{-+l8{DS|zAQ&3|qpOY=!J|kXUhXue9|H>4gqk|n) z-i34GmxLFj8asb3D#D&=ya*a5`C<=o?G;Ev^LV%;l#nH#O=7Nh@z1Do>j6Q;I5S2P zhg|AZbC&|c7}uSJt57s2IK#rSWuararn-02dkptTjo*R{c5o(bWV}_k3BBnKcE|6l zrHl&ezUyw^DmaMdDFVn<8ZY=7_{u{uW&*F<7Al6};lD(u;SB=RpIwI)PTyL=e25h* zGi{lRT}snjbMK~IUx|EGonH+w;iC2Ws)x>=5_{5$m?K z5(*1jMn%u0V1Y%m@`YS3kskt~`1p(rA4uk;Cs!w^KL$w>MH)+cP6|XKr4FfHIATJH z!EGAK4N>1yFR`-zW|w%ByRe#=&kA&#WyUldDGpt!wf-8SFWiSi!5QZL+l7*CE?u!NW1T$<1rdLJ9y3u{_zvHaM?#Rm4 zFk}^1!ffcrB|XK3gsO-s=wr*sUe&^$yN|KxrA)uW00Gu60%pw_+DcUjW`oW<35OC8 zq2{j8SgC}W$?10pvFU83(SL$%C?Kctu3*cs0aa%q!fjn1%xD*Jrm!F3HGR9-C{b?- zHp(cL;ezXMpL@0-1v0DMWddSDNZ5h?q50cOZyVi#bU3&PWE=(hpVn|M4_KYG5h9LffKNRsfhr^=SYiKg?#r&HNMi2@cd4aYL9lw(5_IvQJ zcB*DD()hUSAD^PdA0y|QrVnqwgI@pUXZXjHq3lG2OU&7sPOxxU$Y3&ytj6Qb=2#cC z;{d-{k|xI*bu+Vy&N+}{i(+1me!M;nshY_*&ZQLTGG*xNw#{RpI`3^eGfHck+*38NRgiGahkFethtVY=czJs#)VVc{T65rhU#3Vf?X)8f0)X{w!J3J{z|Sq|%?)nA+zo?$>L9@o`Kc|*7sJo4UjIqu0Ir~S5k^vEH};6K?-dZ0h*m%-1L zf!VC%YbM1~sZOG5zu&Sh>R;(md*_)kGHP)<;OA44W?y53PI%{&@MEN}9TOiqu+1a3AGetBr$c)Ao3OX>iGxmA;^^_alwS818r4Pn&uYe^;z6dh z)68T|AN=hjNdGpF7n>y+RTAZc9&opTXf zqWfK_dUv=mW{p_vN>|(cIkd(+Jy}qnK{IW%X*3!l`^H~FbAHwof+vLZ0C2ZXN1$v7 zgN&R9c8IO`fkR{6U%ERq8FN<1DQYbAN0-pH7EfcA{A&nhT!Be>jj>J!bNRw4NF|}! z1c70_#fkk!VQ!q1h2ff@`yDyrI1`np>*e#D4-Z~*!T^8#o*$V~!8bWQaie?P@KGBb z8rXc!YDL!$3ZgZZ%;-%~0Kn<+d+{xJ$stQbtN8GWV?MCJvzPU|(E(1z;rFw{&6vy) z3*@y%7Tx8rH-p$boS>bLyod?OKRE8v`QSBvGfY6f}_{Zo1q85xoyOF16n~yHx2W ziydUoYLkJmzq|n&2S(O!ZmLdP1(o1Jsq88cX)x3V-BK5eF&0e_0G!5?U7&3KN0`mc zH&Lt)q8!d_VgzxyL^(@xrbp2y)Hmr^V48));RSfE=*Ly0uh9!$3dv-vMZr2URf@l5zdwLjGZB zugY>7_fd_vbV*Qv1?H~>Z%RD%nEeFSI$n$$Lrpc6g>i4+XdBB!%zM$Bhrz5Swzyg? z$~I~n@~-wTBY3-T&pr+|gC+OHDoR?I(eLWa{Z#Rsh>lc~%u0!&R|s0pA*w<7QZ}{i z*AFr~0F3y~f$MGh_HDL7J_1?SxKL}fWIk!$G}`^{)xh*dZ5kK>xGL9>V`WZZg_ z)^Vm)EQK`yfh5KiR(vb&aHvhich z_5o+{d~0+4BEBqYJXyXBIEb1UgVDs;a!N2$9WA>CbfrWryqT25)S4E4)QXBd*3jN} z?phkAt`1rKW?xoLzEm!*IfkH|P>BtECVr0l8-IGk_`UjE#IWkUGqvyS+dMrCnFl<7RCgSMX^qn|Ld_4iYRldO zY&cHhv)GDo8nKvKwAbfyLR%t?9gG?R7~PSD#4D-;?F&!kV59O}neYut5AGbKwy-(U zqyBi=&Mgj|VIo>$u!DHM`R7O?W8-idbePuxiJMH``6c_5L-chKd}=rGC5Gfrc{f!* zWFEBm?l@_b7kzY7%1RQQbG5V<4=ZlkZ%sF74Q|mKOc7Ak7dP2#quiGcZ0_J%7Q?j{ zv9{WFw;n5G-Mn%r#0R;{jLt{yy}9J6rQ(>X9pJ`7Xy?Zv z=lNit#qXaq?CnElK^zF~sG}U5oCpR0T>FH=ZX}Prju$);?;VOhFH8L3I><9P_A|C+ z{;>~dk%9rrq(snjsEm}oUz2FQ21MCG*e?g)?{!&|eg7PX@I+Q0!hL6C7ZVY|g2E>i zr!Ri2@OfEu$)d52+>+cpgh6Z;cLYCZ&EMR0i<^~4&wEu_bdo;y^6}+U2GIQgW$|Od z_jg{O=pU>0-H$P-EOlWyQy#W0r@@_uT}Lg+!d5NxMii7aT1=|qm6BRaWOf{Pws54v zTu=}LR!V(JzI07>QR;;px0+zq=(s+XH-0~rVbmGp8<)7G+Jf)UYs<$Dd>-K+4}CsD zS}KYLmkbRvjwBO3PB%2@j(vOpm)!JABH_E7X^f#V-bzifSaKtE)|QrczC1$sC<<*Y z$hY*3E10fYk`2W09gM_U<2>+r^+ro$Bqh-O7uSa)cfPE_<#^O) zF+5V;-8LaCLKdIh3UB@idQZL`0Vx8`OE#6*1<;8(zi&E7MWB1S%~HAm%axyIHN2vd zA(pJGm_PraB0Aat3~?obWBs?iSc*NhM!{-l_WNCx4@F7I?)5&oI|z{o@JKd1HZ}zf*#}JjK3$ z-;3V*WJZvUcKvSOBH4c7C{fl8oRw8-vfgKQjNiR|KhQ%k6hWNEke(k8w-Ro| z7Y3)FsY-?7%;VT64vRM)l0%&HI~BXkSAOV#F3Bf#|3QLZM%6C{paqLTb3MU-_)`{R zRdfVQ)uX90VCa3ja$8m;cdtxQ*(tNjIfVb%#TCJWeH?o4RY#LWpyZBJHR| z6G-!4W5O^Z8U}e5GfZ!_M{B``ve{r0Z#CXV0x@~X#Pc;}{{ClY_uw^=wWurj0RKnoFzeY` z;gS!PCLCo*c}-hLc?C&wv&>P1hH75=p#;D3{Q8UZ0ctX!b)_@Ur=WCMEuz>pTs$@s z#7bIutL9Pm2FDb~d+H}uBI#pu6R}T{nzpz9U0XLb9lu@=9bTY&PEyFwhHHtXFX~6C zrcg|qqTk(|MIM%KQ<@j=DOjt|V)+8K26wE_CBNnZTg+Z+s}AU|jp6CFoIptG1{J*# z7Ne~l;ba*=bSwAMQ|Vq#fW~+je4PXA91YFzBubNF?ovIOw-$C-8=Ehed{lGD0}(Id zRe4sh8L>&T%{>8o))he}eE;5_ zxoXk3wX?MyNl-xF!q1d$G?=wp^`@09(jU&X zOqZIBI#dN`2PJNdATR3ivtub|nO$dulSaP|e4)WXF1YAGN1pDQIbIjXFG!oC85Mt; zW$eteoL{y^5t4TMRwP$jNPjZFpGsWnGe=jMMqKtcZm9Y9PFZLi*1p@qoKKub^T@2+ zk$@*KYdQ?Z`}<%4ALwk*Yc{(WTf@#u;as(fvE^9{Gk)lWbJP*SjttWofV0s?AB({~l zZI1hZVWFT~W-T?nfMMcnCS4-#6H-MU7H$KxD;yaM46K4Kc@~Q>xzB+QnD_I`b_l3m zo9pRx46b!p?a^&zCDwygqqV3epjs(s0NQI6ARA1n!Yy-qduipxQ& zUAlqRpNjBS+y-ZheD(!R;F}&^V_}b_gqH%tVZ5%%ziO7k^w=es+wZtK^i*vmrWNLMs{oWu_CIov|s1raZiS)>38>pYu;i+-t zI_DiNe6aA4KTZ2P09qPj(0~K4nUq^0+f(2$g`229zkG4jLzRvJUWE0oF1XHL4t3UN zDH466G56sy9hTZoAJB!C3;@F;ONxEk5u6Mv%zdo}Rq`=* zw1n7MOhfNSV48TS989ArIcj`C%Gk8~93~u>)!Yt2b4ZriKj9x2d`H2HQNJ=I>hkDlcZn zqRj>!;oRMTIOu zx|Zfsu~v76T{z7AC(jxj^c@tnJHZtGPsq$DE!8kqvkDx5W?KUJPL+!Ffpwfa+|5z5 zKPCiOPqZZrAG;2%OH0T$W|`C@C*!Z`@Wkop{CTjB&Tk`+{XPnt`ND`Haz;xV`H^RS zyXYtw@WlqTvToi;=mq1<-|IQ(gcOpU%)b#_46|IuWL#4$oYLbqwuk6=Q@xZaJSKVF zZcHs~ZBl;&lF3=+nK; zF`4gSCeZXlwmC_t4I`#PUNQ*)Uv&oGxMALip|sxv^lyVV73tKI7)+QY5=tEMas{vTD-BaTJ^*Y6gq~PU;F5X!sxqiq$iFCo+Uv7m%1w((=e}Vf*=dtds|6 zbX}91!G?C*KG03eHoN}RZS9DJxa&8YwNCT8?JxMXyZqZr13NA|GB{+vG`08C{V(yy zf*Lw$+tYSU_+dI`3n{bMrPdDb`A=Mkg!O=k>1|*3MC8j~- zXL79J4E=U^H=iBLTeHE_OKzE&dws8RNynsSJ!d;`zK?P92U{f)xvD7VQVosrXZrL+ z6lMVdD1YgL;%(1cq{#bS6yXmp|DS@nax#AqqlZhtUQdh<^2vr5`EpAO

LGYq)sa(w9^3-f}NHy=GR4v%t2YZly3m1G@5y`xBh_HGrD%f z>;|Ty?9FiJAc&UVD(StT4I` zfVQwxhE9bXE6r2mKO8Ag7{L^jCyqQb0QqKDPE=RAgqn8q1O^>(z7h5kE(6va%QqRZ zkIOmp(})rLSS(2{=C12e&@!W2=Jel-^_R``0xHO^+t!(oXbcv5yhD4g*$t_F)_5Dl zSVCgesW%;DtYPCFs{G;GX_o?1J3;QQPPv)rWw;>} zJ&KwnUqwNXloNXlK_+pNDfI~hON#SokVJb&ilg8d7^NWo2ZQymCqQMnjfi>ePibjr z-Z@q!?RGN$Mj}Nk){X_vaj6?Mj$>ACR*z|6MsXy3VZ^PFn@yHkPo(>m(iWepn8SC@ z>D2;R4m+gDRZ=SIX!b+CP(qE=JDIUkn=D$aUu+Ihn9-+k1LS3PreQg0N5eWIG@x${nC3v^7caS>1!PKNAY9J z#}E}Q9w#SP>(GY7Hbj&z4$Li6o5taBO|4+F`yS9zq*LJ<38wy4I>HA9(&GYrk4dLajKGww))BWli6Ln1A^Lda@N~p+snkb9C z@OthI+<##vp8!HVQT4Wk(=@zQ{OvZ$EKWS73+JHb)eYLGD-cqi6^|vd$<+IHuc?Nq zW7JertT~3))4?J|28n$I@nAD0c1%9C&IVhEZX~mUsf{efyS(XNG%ch;!N~d7S(Ri7 zb&=BuON95aVA&kLn6&MVU|x}xPMp7xwWxNU1wS+F6#y}1@^wQZB*(&ecT?RnQcI}Y z2*z!^!D?gDUhc@;M^OpLs4mq>C&p{}OWVv<)S9KMars@0JQ{c_ScGsFo3BJ)Irg++ zAWwypJdTO-_{Uh8m(Z!3KL7K{ZZzKHj;{M8I$mV>k znTM?sa0);^=X^cglL`uC+^J)M7nEa$w=VwFULg~%DJllw+7dJAj3{qnP5i3@wr7%y zjXp?Wl2%Th=my&3u?Q$RV6N5tzKMSPTsc#J+-cDDp~qFB6bL2C8AS7Y3PKtVhdhl) zIaLqH5+OnWPWSt(lQCgkN8lczc-V%_iZ{>#1%Z$N*>lu#S;0MZ$T2Y8Kg!U;hAZj> z6S#%$DQ_`Ic%Zr@?}GgjRXg@qTj^17n`65oJ@Wj0u1X8&+UVd|Xs?J+i_^GZ94m6= zUc96~Q`OJvlKB_Lr15*Yw_PUPEr?f?H&00b^-W%26mD)(n(rGGNfK9~2h=C>p-7BZ zFd&*&Msdu{w~(eyFOglwCPH^Rb}O(N7LtS+nnEwDx*pGD?|&9Si~M43a+*L(b0$5A zv`T`(G3xO;I_sx;FwTP21ZlfDpz zOo?}Vlgf~fo{YWm@n_JyD*frOg{XsvBA~|Tn4V6hu>Gd>89-rblfVJUaGvj6X%NZ} z$tFF9sx=4_$*c~G`9iPLGh@=sV+O{D2-t*K@J7H=`V+oVt}8?04WwU3h1BgS!f%1P zFak-T#7`TtLcR=Yz>g0R!ZQrH!YiZOQN=_V-UyncN1Rc18?KY?#O`v#JK+pq0K$~H z3D@v9DZF42R)b9#BBX{^$DOMlJ!g)Gc za{o-1e%F6NvgKq9tC8pV+9S$;9*zNv{J*)n&dmf~anP1)4~N%~h#c(=B#3*KgzhCKhFdgDoWi2IDog{RVyzK|Y`rCUs3T~pJMmdZJy4?b z&s5G=zhf**(t7Y^oC_mcTsE-{^}wiaoUu&?kojLKs>SJPxjcP>{a5CbXCx92AcBE) zHtqP}LjZ{W>PH?Tu(E0X=%{PBMW@F_?#7b&#!^q`<-5$ur+-q6 z{dn=(^UZw6*3-XM_(=@<1_*i&XM4=0t5u!gm6 z{UlmNGPKgO_;e;q9|#esq~Sq`<}%d{+sRmhvsA{5i*91=tub>OZZ%)xUA#4q$dDyy z1`w4%?OPLg3JeZb#cqSMO?*Xn%|-FCcuH2i2fn_{IFusub6;NQdN|7TD1N?%E8*g? z$apAt@cEe!I%jB=*q$p_3=t_5R0ph%{qaq+QDg!c99Y!Xa!&oDZOeis_ot)gNXr{l zdY$|So2Qed2Y7KMNBrS^E169kG%h<+z{Z_p_;shB!uY)>yAVcK=&!bg`lVg)4T1|7 z0}7FpfydVH4F87K@c!nEG+WGKm{Ouo)Slpl;#qcEIQ0zdMfLA#;dBxYw;p;KoVv6| z3_D5&7rJdG12CnDSvZUW?$UC6^UVSW^|vw|o-_4bz)(w5(3AiVhpeT(|=f#x_}E?s#qHZF#xA6AF_ujl$G z-jHD%q(d2}v2PhXx&6YWps~m(^+RXl91Q#xRRJBhjKl$FG4bk);|ag;ieUZ&!Ii3$ z(iGz1+0m7#g5>ASldBbNZL=ZHh=tmmJt$!71; zIML2GhEz1pg@1rQN(M^_691wAGkJ@Pga_05WuQ6! zG5RkGY2^`@(H~pp7&Ga+Pwh3L!Njj!-rc;^bTIfo5hP@H##1X8xUZJckrx>id`bAd3QUx9GuomqBYZ!uN1-&o zvTxC?;p8vL67&fW8fw(YOqt>L@bdLrEF*3OgYe$4n4{ zEB40LiU#6-0@5jdN`0w}N0qi@c0~oT2FP z)LNk&a82my?jv(tQpiMi$TK_L@lub#lsM$R{Dk?Ya@%%%huZkct~tSWM714c!45k}-ZLVA-bVM`>|_ZBbW_m-7| z3U%xrAhi}n?T(2F{_n4EZ10inkIFl#y09?7$uwBoJgqY8vylwev)fDOn;>0R!aEnV zBz%j0Mqpx~EZU3q@%+oV7;}|vt7$~ou@faEIq{p?FY$XXg&6*K)b_LP=}gi9`Bij3 zN`zEo|B6*|-;>S`rNa^BKRDbDAk>X#MsR`EvL>6bqU@SaDDs z8>bu@3YdRaWs*Te@G-UHjU%F~kTHw5(0PVJ+pwh#ha2u;DB+UMo@A5UYIl#5rtBV- zGX_hIpw}3C@H*Us(Cc-d#-gNrG#w$(9+S=GxO>3SR`SE2fHZ2KrDc#_C^$jI>Y}#; zMwY=R6@+dWi~0RXw(c@3GZ&%~9K(q&ee0Zw;pwL`E_tZak-#8^_b)Dpyi73^he?xV zXJ08&wh5-M&}qy4f7!D&=E)puDD(Nmg1d_(j`4LvxM5x_huNg-pGG%9rYqO6mImyJ@}*3Y>^3OvcnTG%EV1) zq_Ap?Z!Iw__7#D=pOWnQN$gB!Mr0!9yx|g<4icJh{cFOu3B8}&RiYm+Mb;VEK``LK zL(NcpcTiGieOIssSjr?ob}^``nNf&UcJhXyncO9m{6gD$kqSD`S69(aF8dkWz5>!9 zBLe4Sib7Hs2x_L2Ls6Ish$MGVKrGt5+_2zCyP1byaCg3upo+-I}R4&$m)8 zQ7|jc1Z^VWggpuQj*cP;>Zo9LS!VSzrqmZczaf;u`d0J(f%Z9r%An@s!e>n9%y=n!IZ_tVGu{Jmsbp}Fk%HJIU?a+-~bjfLTuH|JExA8EROowzr zqW9{YyZhR0a4clRK>1I4Ncx&WER~{iE;F^$T7K%X@3PGOA%6#Z%p3TS^&M;Dnjw@i z^o!$9nhcsmcHcY4?4j9+ofL_CWsZ4Hcch(rjsGfGD(nsH>w}^ERqGnz%iGj0j{g}h z7wMkJ-2Z2~eS>2!i}0~B63i;>SyFJU2+>VCS^AxaDOx%g6-t0eM^P<3+*z`ztvOqrG3)&#$K?& z_Y0wbWID47@cU`E1A6A&!`aZk0ZE@z-h#l1NqX2#`$Uev2gepW`rf8*!=rD5&;Jb{ zl08rU>dPo=K%-1Ao1~G-@4ve~y5#9E8x;TE0k5d^TC(=Zc>mwjW^c=+U-<9}b0ku~}gj z3sbW>R2M6DR!g#NUP;nxo>)@7*=RP{U18SDop6b2&PHce^&h97@xx3t+VK+!keE#} z;(Uf&89as9k8{$nkLbuB!-d7TP`_VJpL^Xs8OKB~ri$YUbW8fch64}7|0EWoT(TRj{ z*GT<7Y<7DsrCi79ZsM)z#c(!nNOGySOCkY1fAuQOq12&iUVC!a`#O;dBLf=d?&4*B zI~LgAO7E0qxK(uRTM;IgJ}+z^gD+bi-6I!3x{r9`l~%8TRP%UE0V8E*Sz>Nl1NVG<<7(wDHZ+HcOkQm$O&k+vyx)y)x{Pz!U8hS$*m zByc0h6BUI*BOpuL==P+H|Hx%`>7!W+1H!l9vi&)`V zyn2o9{z=lc+VX*!Vh~SF=)L}Z40XeG>LF6cP^b+R$NxSeUqbK^Q*UTalKzP8X%{9@RSCXm_NhF>{=S2 zi}ezam_^P`S!!-cyEW9y7DBbK93roz@Raccy*v}?mKXScU9E_4g;hBU7}zSofAFda zKYEe?{{I54 diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index b82aa23..0aaefbc 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,6 +1,6 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.10.1-bin.zip networkTimeout=10000 validateDistributionUrl=true zipStoreBase=GRADLE_USER_HOME diff --git a/gradlew b/gradlew index 1aa94a4..f5feea6 100755 --- a/gradlew +++ b/gradlew @@ -15,6 +15,8 @@ # See the License for the specific language governing permissions and # limitations under the License. # +# SPDX-License-Identifier: Apache-2.0 +# ############################################################################## # @@ -55,7 +57,7 @@ # Darwin, MinGW, and NonStop. # # (3) This script is generated from the Groovy template -# https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt +# https://github.com/gradle/gradle/blob/HEAD/platforms/jvm/plugins-application/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt # within the Gradle project. # # You can find Gradle at https://github.com/gradle/gradle/. @@ -84,7 +86,8 @@ done # shellcheck disable=SC2034 APP_BASE_NAME=${0##*/} # Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036) -APP_HOME=$( cd "${APP_HOME:-./}" > /dev/null && pwd -P ) || exit +APP_HOME=$( cd -P "${APP_HOME:-./}" > /dev/null && printf '%s +' "$PWD" ) || exit # Use the maximum available, or set MAX_FD != -1 to use that value. MAX_FD=maximum diff --git a/gradlew.bat b/gradlew.bat index 7101f8e..9b42019 100644 --- a/gradlew.bat +++ b/gradlew.bat @@ -13,6 +13,8 @@ @rem See the License for the specific language governing permissions and @rem limitations under the License. @rem +@rem SPDX-License-Identifier: Apache-2.0 +@rem @if "%DEBUG%"=="" @echo off @rem ########################################################################## diff --git a/settings.gradle.kts b/settings.gradle.kts index 42bc68c..22ca675 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -1,21 +1,32 @@ /* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC + * SPDX-License-Identifier: Apache-2.0 * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. + * Copyright 2019-2024 The TurnKey Authors * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. */ rootProject.name = "z3-turnkey" +pluginManagement { + repositories { + gradlePluginPortal() + mavenCentral() + } +} + plugins { - id("com.gradle.develocity") version "3.17.1" + id("com.gradle.develocity") version "3.18.1" id("org.gradle.toolchains.foojay-resolver-convention") version "0.8.0" } diff --git a/src/main/java/com/microsoft/z3/Z3Loader.java b/src/main/java/com/microsoft/z3/Z3Loader.java deleted file mode 100644 index 2b3e774..0000000 --- a/src/main/java/com/microsoft/z3/Z3Loader.java +++ /dev/null @@ -1,254 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package com.microsoft.z3; - -import static java.lang.System.getProperty; -import static java.nio.file.Files.createTempDirectory; -import static java.nio.file.Files.newOutputStream; - -import java.io.IOException; -import java.io.InputStream; -import java.io.OutputStream; -import java.nio.file.Path; - -/** - * Handles automatic unpacking and loading for the Z3 native libraries. The Z3 code is rewritten to - * invoke this class automatically. It should not be called manually. - */ -final class Z3Loader { - - /** This class should not be constructed. */ - private Z3Loader() { - throw new AssertionError(); - } - - /** - * Execute the unpack-and-load algorithm. In essence, this does - * - *

    - *
  1. Identify the current OS and CPU architecture the JVM runs on. - *
  2. Check if matching native libraries are present. If not, abort. - *
  3. Unpack the native libraries to a temporary directory and schedule the resulting files for - * deletion on JVM exit. - *
  4. Load the native libraries. - *
- * - * Loading is performed during the first Z3 operation that uses native code. A loading error will - * be thrown during the same operation; otherwise, Z3 should be in a usable state. - * - * @throws UnsatisfiedLinkError if the current platform is not supported. - * @throws UnsatisfiedLinkError if library unpacking or linking fails. - * @throws IllegalStateException if the Z3 library distribution is incomplete, indicating a - * packaging error. - */ - static void loadZ3() { - final OperatingSystem os = OperatingSystem.identify(); - final CPUArchitecture cpu = CPUArchitecture.identify(); - final Class clazz = Z3Loader.class; - - final InputStream libZ3 = clazz.getResourceAsStream(getLibraryPath(os, cpu, "z3")); - final InputStream libZ3Java = clazz.getResourceAsStream(getLibraryPath(os, cpu, "z3java")); - assertLibrariesFound(libZ3, libZ3Java, os, cpu); - - final Path libZ3Out; - final Path libZ3JavaOut; - try { - final Path libraryDir = createTempDirectory("z3-turnkey"); - libraryDir.toFile().deleteOnExit(); // deletion is LIFO, so add the directory first - - libZ3Out = libraryDir.resolve(getLibraryName(os, "z3")); - libZ3Out.toFile().deleteOnExit(); - - libZ3JavaOut = libraryDir.resolve(getLibraryName(os, "z3java")); - libZ3JavaOut.toFile().deleteOnExit(); - - unpackLibrary(libZ3, libZ3Out); - unpackLibrary(libZ3Java, libZ3JavaOut); - } catch (IOException e) { - throw new LinkageError("Could not unpack native libraries", e); - } - - System.load(libZ3Out.toAbsolutePath().toString()); - System.load(libZ3JavaOut.toAbsolutePath().toString()); - } - - /** Supported operating systems. */ - private enum OperatingSystem { - /** Mac OS. */ - OS_X("osx", "dylib"), - /** Linux. */ - LINUX("linux", "so"), - /** Microsoft Windows. */ - WINDOWS("windows", "dll"); - - /** The directory name used for the OS's libraries. */ - final String name; - - /** The file name extension for dynamic libraries defined by the OS. */ - final String libraryExtension; - - /** - * Construct a new enum entry. - * - * @param name the {@link #name}. - * @param libraryExtension the {@link #libraryExtension}. - */ - OperatingSystem(final String name, final String libraryExtension) { - this.name = name; - this.libraryExtension = libraryExtension; - } - - /** - * Identify the current operating system. This uses the {@code os.name} system property. - * - * @return the current operating system. - * @throws UnsatisfiedLinkError if the current operating system is not known, i.e., unsupported. - */ - static OperatingSystem identify() { - final String osName = getProperty("os.name"); - if (osName.startsWith("Darwin") || osName.startsWith("Mac")) return OS_X; - else if (osName.startsWith("Linux")) return LINUX; - else if (osName.startsWith("Windows")) return WINDOWS; - else throw new UnsatisfiedLinkError("Unsupported operating system: " + osName); - } - } - - /** Supported CPU architectures. */ - private enum CPUArchitecture { - /** Intel/AMD 32 bit. */ - X86("x86"), - /** Intel/AMD 64 bit. */ - AMD64("amd64"), - /** ARMv8 64 bit. */ - AARCH64("aarch64"); - - /** The directory name used for the OS's libraries. */ - final String name; - - /** - * Construct a new enum entry. - * - * @param name the {@link #name}. - */ - CPUArchitecture(final String name) { - this.name = name; - } - - /** - * Identify the CPU architecture used by the JVM. For a 32-bit JVM running on a 64-bit CPU, this - * will identify a 32-bit CPU. Since the JVM needs lo link against same-architecture libraries, - * this is the desired behavior. This uses the {@code os.arch} system property. - * - * @return the current CPU architecture. - * @throws UnsatisfiedLinkError if the current architecture is not known, i.e., unsupported. - */ - static CPUArchitecture identify() { - final String osArch = getProperty("os.arch"); - switch (osArch) { - case "i386": - case "i686": - return X86; - case "amd64": - case "x86_64": - return AMD64; - case "aarch64": - return AARCH64; - default: - throw new UnsatisfiedLinkError("Unsupported CPU architecture: " + osArch); - } - } - } - - /** - * Get the expected library file's location for the given OS, CPU architecture and library name. - * - * @param os the operating system. - * @param cpu the CPU architecture. - * @param library the library name. - * @return the expected location of the library for the OS-architecture-combination. - */ - private static String getLibraryPath( - final OperatingSystem os, final CPUArchitecture cpu, final String library) { - return "/native/" + os.name + "-" + cpu.name + "/" + getLibraryName(os, library); - } - - /** - * Get the expected library file's location for the given OS and library name. - * - * @param os the operating system. - * @return the expected name of the library for the OS. - */ - private static String getLibraryName(final OperatingSystem os, final String library) { - return "lib" + library + "." + os.libraryExtension; - } - - /** - * Ensure that all required Z3 libraries are present. - * - * @param libZ3 the input stream for {@code libz3} or {@code null}, if not found. - * @param libZ3Java the input stream for {@code libz3java} or {@code null}, if not found. - * @param os the current operating system, used in exception messages. - * @param cpu the current CPU architecture, used in exception messages. - * @throws UnsatisfiedLinkError if no library could be found. - * @throws IllegalStateException if only one library is missing. - */ - private static void assertLibrariesFound( - final InputStream libZ3, - final InputStream libZ3Java, - final OperatingSystem os, - final CPUArchitecture cpu) { - if (libZ3 == null && libZ3Java == null) { - throw new UnsatisfiedLinkError("No native libraries present for " + os + " on " + cpu); - } - if (libZ3 == null) { - throw new IllegalStateException( - "Z3 native library is missing from the distribution. This is a packaging error."); - } - if (libZ3Java == null) { - throw new IllegalStateException( - "Z3 native java support library is missing from the distribution. This is a packaging error."); - } - } - - /** - * Copy a library to a destination path and closes the input stream. - * - * @param lib the input stream for the library, must not be {@code null}. - * @param destination the destination path for the library. - * @throws IOException if the copy operation fails. - */ - private static void unpackLibrary(InputStream lib, Path destination) throws IOException { - try (OutputStream out = newOutputStream(destination)) { - copy(lib, out); - } - lib.close(); - } - - /** - * Copy an input stream to an output stream. This functionality is provided by the standard - * library on Java 9+; unfortunately, we target Java 8. - * - * @param in the input stream. - * @param out the output stream. - * @throws IOException if the read or write operation fails. The stream may be partially written. - */ - private static void copy(final InputStream in, final OutputStream out) throws IOException { - final byte[] buffer = new byte[1 << 13]; - int read; - while ((read = in.read(buffer, 0, buffer.length)) >= 0) { - out.write(buffer, 0, read); - } - } -} diff --git a/src/main/java/module-info.java b/src/main/java/module-info.java index 79a592e..360156e 100644 --- a/src/main/java/module-info.java +++ b/src/main/java/module-info.java @@ -1,4 +1,6 @@ -module com.microsoft.z3 { +module tools.aqua.turnkey.z3 { + requires tools.aqua.turnkey.support; + exports com.microsoft.z3; exports com.microsoft.z3.enumerations; } diff --git a/src/test/java/tools/aqua/turnkey/z3/ShutdownHookTest.java b/src/test/java/tools/aqua/turnkey/z3/ShutdownHookTest.java new file mode 100644 index 0000000..6e80b3d --- /dev/null +++ b/src/test/java/tools/aqua/turnkey/z3/ShutdownHookTest.java @@ -0,0 +1,86 @@ +/* + * SPDX-License-Identifier: Apache-2.0 + * + * Copyright 2019-2024 The TurnKey Authors + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package tools.aqua.turnkey.z3; + +import static java.util.Arrays.asList; +import static java.util.Objects.requireNonNull; +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assumptions.assumeThat; +import static org.assertj.core.api.Assumptions.assumeThatThrownBy; + +import com.microsoft.z3.Native; +import java.lang.reflect.Field; +import java.nio.file.Paths; +import java.util.Collection; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import org.junit.jupiter.api.Test; + +/** Test that the loader library schedules the unpacked Z3 native libraries for deletion. */ +class ShutdownHookTest { + + /** The library names to look out for. */ + private static final List LIBRARY_NAMES = asList("z3", "z3java"); + + private static String getFileBaseName(final String file) { + final String fileName = requireNonNull(Paths.get(file).getFileName()).toString(); + final int fileNameDot = fileName.indexOf('.'); + return (fileNameDot == -1) ? fileName : fileName.substring(0, fileNameDot); + } + + private static String getLibraryBaseName(final String library) { + final String name = getFileBaseName(library); + return name.startsWith("lib") ? name.substring("lib".length()) : name; + } + + /** + * Reflectively obtain the list of deletion-schedules files and verify that files starting with + * {@code name.} for {@code name} in {@link #LIBRARY_NAMES} are scheduled for deletion on JVM exit + * after Z3 has been invoked. + * + * @throws ClassNotFoundException on reflection error. + * @throws NoSuchFieldException on reflection error. + * @throws IllegalAccessException on reflection error. + */ + @Test + void testShutdownHookGeneration() + throws ClassNotFoundException, NoSuchFieldException, IllegalAccessException { + + final Class deleteOnExitHook = Class.forName("java.io.DeleteOnExitHook"); + final Field files = deleteOnExitHook.getDeclaredField("files"); + assumeThatThrownBy(() -> files.setAccessible(true)).doesNotThrowAnyException(); + + @SuppressWarnings("unchecked") + final Set before = new HashSet<>((Collection) files.get(null)); + + assumeThat(before) + .map(ShutdownHookTest::getLibraryBaseName) + .doesNotContainAnyElementsOf(LIBRARY_NAMES); + + Native.getFullVersion(); + + @SuppressWarnings("unchecked") + final Set after = new HashSet<>((Collection) files.get(null)); + final Set newFiles = new HashSet<>(after); + newFiles.removeAll(before); + + assertThat(newFiles).map(ShutdownHookTest::getLibraryBaseName).containsAll(LIBRARY_NAMES); + } +} diff --git a/src/test/java/tools/aqua/turnkey/z3/SolverInteractionTest.java b/src/test/java/tools/aqua/turnkey/z3/SolverInteractionTest.java new file mode 100644 index 0000000..0541f79 --- /dev/null +++ b/src/test/java/tools/aqua/turnkey/z3/SolverInteractionTest.java @@ -0,0 +1,111 @@ +/* + * SPDX-License-Identifier: Apache-2.0 + * + * Copyright 2019-2024 The TurnKey Authors + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package tools.aqua.turnkey.z3; + +import static com.microsoft.z3.Status.SATISFIABLE; +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.InstanceOfAssertFactories.BOOLEAN; + +import com.microsoft.z3.ArithExpr; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.BoolSort; +import com.microsoft.z3.CharSort; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import com.microsoft.z3.IntExpr; +import com.microsoft.z3.Model; +import com.microsoft.z3.RealExpr; +import com.microsoft.z3.RealSort; +import com.microsoft.z3.SeqExpr; +import com.microsoft.z3.Solver; +import org.junit.jupiter.api.Test; + +/** Test more complicated solver interactions that require the entire ecosystem to be loaded. */ +class SolverInteractionTest { + + /** Check the satisfiability of a simple comparison. */ + @Test + void testSimpleSolving() { + try (Context ctx = new Context()) { + final Solver solver = ctx.mkSolver(); + + final IntExpr x = ctx.mkIntConst("x"); + final IntExpr c = ctx.mkInt(15); + final BoolExpr b = ctx.mkGt(x, c); + assertThat(solver.check(b)).isEqualTo(SATISFIABLE); + + final Model m = solver.getModel(); + final Expr evaluated = m.evaluate(b, true); + assertThat(evaluated).extracting(Expr::isTrue, BOOLEAN).isTrue(); + } + } + + /** Check the satisfiability of two floating-point expressions. */ + @Test + void testArithmeticSolving() { + try (Context ctx = new Context()) { + final IntExpr x = ctx.mkIntConst("x"); + final RealExpr xReal = ctx.mkInt2Real(x); + + final RealExpr y = ctx.mkRealConst("y"); + + final RealExpr three = ctx.mkReal(3); + final RealExpr minusTwo = ctx.mkReal(-2); + final RealExpr twoThirds = ctx.mkReal(2, 3); + + final ArithExpr threeY = ctx.mkMul(three, y); + final ArithExpr yOverX = ctx.mkDiv(y, xReal); + + final BoolExpr xGreaterEqualThreeY = ctx.mkGe(xReal, threeY); + final BoolExpr xLessEqualY = ctx.mkLe(xReal, y); + final BoolExpr minusTwoLessX = ctx.mkLt(minusTwo, xReal); + + final BoolExpr assumptions = ctx.mkAnd(xGreaterEqualThreeY, xLessEqualY, minusTwoLessX); + + final Solver solver = ctx.mkSolver(); + solver.add(assumptions); + + solver.push(); + final BoolExpr differenceLessEqualTwoThirds = ctx.mkLe(yOverX, twoThirds); + assertThat(solver.check(differenceLessEqualTwoThirds)).isEqualTo(SATISFIABLE); + solver.pop(); + + solver.push(); + final BoolExpr differenceIsTwoThirds = ctx.mkEq(yOverX, twoThirds); + assertThat(solver.check(differenceIsTwoThirds)).isEqualTo(SATISFIABLE); + solver.pop(); + } + } + + /** Check that expression concatenation operates correctly. */ + @Test + void testConcat() { + try (Context ctx = new Context()) { + final Solver solver = ctx.mkSolver(); + + final SeqExpr x = ctx.mkString("x"); + final SeqExpr y = ctx.mkString("y"); + final SeqExpr xPlusY = ctx.mkConcat(x, y); + final SeqExpr xy = ctx.mkString("xy"); + + final BoolExpr b = ctx.mkEq(xPlusY, xy); + assertThat(solver.check(b)).isEqualTo(SATISFIABLE); + } + } +} diff --git a/src/test/java/tools/aqua/turnkey/z3/Z3LoaderTest.java b/src/test/java/tools/aqua/turnkey/z3/Z3LoaderTest.java new file mode 100644 index 0000000..b0d3a87 --- /dev/null +++ b/src/test/java/tools/aqua/turnkey/z3/Z3LoaderTest.java @@ -0,0 +1,38 @@ +/* + * SPDX-License-Identifier: Apache-2.0 + * + * Copyright 2019-2024 The TurnKey Authors + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package tools.aqua.turnkey.z3; + +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assumptions.assumeThat; + +import com.microsoft.z3.Native; +import org.junit.jupiter.api.Test; + +/** Test that Z3 native methods can successfully be invoked. */ +class Z3LoaderTest { + + /** Invoke the {@link Native#getFullVersion} method from Z3. */ + @Test + void testLoading() { + final String expectedVersion = System.getProperty("expectedZ3Version"); + assumeThat(expectedVersion).isNotNull(); + + assertThat(Native.getFullVersion()).contains(expectedVersion); + } +} diff --git a/src/test/java/tools/aqua/z3turnkey/ShutdownHookTest.java b/src/test/java/tools/aqua/z3turnkey/ShutdownHookTest.java deleted file mode 100644 index 51b8261..0000000 --- a/src/test/java/tools/aqua/z3turnkey/ShutdownHookTest.java +++ /dev/null @@ -1,93 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua.z3turnkey; - -import static org.junit.jupiter.api.Assertions.assertTrue; - -import com.microsoft.z3.Native; -import java.io.File; -import java.lang.reflect.Field; -import java.util.Collection; -import java.util.HashSet; -import java.util.Set; -import org.junit.jupiter.api.Test; -import org.opentest4j.TestAbortedException; - -/** Test that the loader library schedules the unpacked Z3 native libraries for deletion. */ -public class ShutdownHookTest { - - /** - * Reflectively obtain the list of deletion-schedules files and verify that files containing - * {@code z3} and {@code z3java} or {@code libz3} and {@code libz3java} are scheduled for deletion - * on JVM exit after Z3 has been invoked. - * - * @throws ClassNotFoundException on reflection error. - * @throws NoSuchFieldException on reflection error. - * @throws IllegalAccessException on reflection error. - */ - @Test - public void testShutdownHookGeneration() - throws ClassNotFoundException, NoSuchFieldException, IllegalAccessException { - final Class deleteOnExitHook = Class.forName("java.io.DeleteOnExitHook"); - final Field files = deleteOnExitHook.getDeclaredField("files"); - try { - files.setAccessible(true); - } catch (Exception e) { - throw new TestAbortedException("Could not reflectively access hook", e); - } - - @SuppressWarnings("unchecked") - final Set before = new HashSet<>((Collection) files.get(null)); - - Native.getFullVersion(); - - @SuppressWarnings("unchecked") - final Set after = new HashSet<>((Collection) files.get(null)); - HashSet newFiles = new HashSet<>(after); - newFiles.removeAll(before); - - assertTrue( - newFiles.stream() - .anyMatch( - file -> { - String name = new File(file).getName(); - return name.startsWith("z3.") || name.startsWith("libz3."); - }), - "Z3 library not scheduled for deletion " - + "(before = " - + before - + ", after = " - + after - + ", new = " - + newFiles - + ")"); - - assertTrue( - newFiles.stream() - .anyMatch( - file -> { - String name = new File(file).getName(); - return name.startsWith("z3java.") || name.startsWith("libz3java."); - }), - "Z3 java support library not scheduled for deletion " - + "(before = " - + before - + ", after = " - + after - + ", new = " - + newFiles - + ")"); - } -} diff --git a/src/test/java/tools/aqua/z3turnkey/SolverInteractionTest.java b/src/test/java/tools/aqua/z3turnkey/SolverInteractionTest.java deleted file mode 100644 index 1221008..0000000 --- a/src/test/java/tools/aqua/z3turnkey/SolverInteractionTest.java +++ /dev/null @@ -1,96 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua.z3turnkey; - -import static com.microsoft.z3.Status.SATISFIABLE; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertTrue; - -import com.microsoft.z3.*; -import org.junit.jupiter.api.Test; - -/** - * Test more complicated solver interactions that require both the libz3java and the libz3 to be - * loaded correctly. - */ -public class SolverInteractionTest { - - /** Check the satisfiability of two floating-point expression. */ - @Test - @SuppressWarnings("unchecked") - public void testArithmeticSolving() { - try (Context ctx = new Context()) { - IntExpr x = ctx.mkIntConst("x"); - RealExpr xReal = ctx.mkInt2Real(x); - RealExpr y = ctx.mkRealConst("y"); - RealExpr three = ctx.mkReal(3); - RealExpr neg2 = ctx.mkReal(-2); - RealExpr two_thirds = ctx.mkReal(2, 3); - ArithExpr three_y = ctx.mkMul(three, y); - ArithExpr y_over_x = ctx.mkDiv(y, xReal); - BoolExpr x_geq_3y = ctx.mkGe(xReal, three_y); - BoolExpr x_leq_y = ctx.mkLe(xReal, y); - BoolExpr neg1_lt_x = ctx.mkLt(neg2, xReal); - BoolExpr assumptions = ctx.mkAnd(x_geq_3y, x_leq_y, neg1_lt_x); - - Solver solver = ctx.mkSolver(); - solver.add(assumptions); - - solver.push(); - BoolExpr diff_leq_two_thirds = ctx.mkLe(y_over_x, two_thirds); - assertEquals(SATISFIABLE, solver.check(diff_leq_two_thirds)); - solver.pop(); - - solver.push(); - BoolExpr diff_is_two_thirds = ctx.mkEq(y_over_x, two_thirds); - solver.add(diff_is_two_thirds); - assertEquals(SATISFIABLE, solver.check()); - solver.pop(); - } - } - - /** Check the satisfiability of a simple comparison. */ - @Test - public void testSimpleSolving() { - try (Context ctx = new Context()) { - Solver solver = ctx.mkSolver(); - - IntExpr x = ctx.mkIntConst("x"); - IntExpr c = ctx.mkInt(15); - BoolExpr b = ctx.mkGt(x, c); - assertEquals(SATISFIABLE, solver.check(b)); - - Model m = solver.getModel(); - Expr evaluated = m.evaluate(b, true); - assertTrue(evaluated.isTrue(), "The model should evaluate"); - } - } - - /** Check that expression concatenation operates correctly. */ - @Test - public void testConcat() { - try (Context ctx = new Context()) { - Solver solver = ctx.mkSolver(); - - SeqExpr x = ctx.mkString("x"); - SeqExpr y = ctx.mkString("y"); - SeqExpr xPlusY = ctx.mkConcat(x, y); - SeqExpr xy = ctx.mkString("xy"); - - BoolExpr b = ctx.mkEq(xPlusY, xy); - assertEquals(SATISFIABLE, solver.check(b)); - } - } -} diff --git a/src/test/java/tools/aqua/z3turnkey/Z3LoaderTest.java b/src/test/java/tools/aqua/z3turnkey/Z3LoaderTest.java deleted file mode 100644 index 0d04083..0000000 --- a/src/test/java/tools/aqua/z3turnkey/Z3LoaderTest.java +++ /dev/null @@ -1,38 +0,0 @@ -/* - * Copyright 2019-2024 The Z3-TurnKey Authors - * SPDX-License-Identifier: ISC - * - * Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby - * granted, provided that the above copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, - * INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN - * AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR - * PERFORMANCE OF THIS SOFTWARE. - */ - -package tools.aqua.z3turnkey; - -import static org.junit.jupiter.api.Assertions.assertTrue; - -import com.microsoft.z3.Native; -import org.junit.jupiter.api.Test; -import org.opentest4j.TestAbortedException; - -/** Test that Z3 native methods can successfully be invoked. */ -public class Z3LoaderTest { - - /** Invoke the {@link Native#getFullVersion} method from Z3. */ - @Test - public void testLoading() { - String version = Native.getFullVersion(); - String expectedVersion = System.getProperty("expectedZ3Version"); - if (expectedVersion == null) { - throw new TestAbortedException("Z3 version not passed as property"); - } - assertTrue( - version.contains(expectedVersion), - "The loaded lib should report the expected version '" + expectedVersion + "'"); - } -}