diff --git a/README.md b/README.md index 9c31b6717..beb367019 100644 --- a/README.md +++ b/README.md @@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features: * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml) -[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.4) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.5) [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core) ## Get started @@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/): ```kotlin // core -implementation("io.ksmt:ksmt-core:0.6.4") +implementation("io.ksmt:ksmt-core:0.6.5") // z3 solver -implementation("io.ksmt:ksmt-z3:0.6.4") +implementation("io.ksmt:ksmt-z3:0.6.5") ``` Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts index ddbee4c1a..fe9bf4972 100644 --- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts +++ b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts @@ -11,7 +11,7 @@ plugins { } group = "io.ksmt" -version = "0.6.4" +version = "0.6.5" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index df95b2959..38069f783 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -34,7 +34,7 @@ repositories { ```kotlin dependencies { // core - implementation("io.ksmt:ksmt-core:0.6.4") + implementation("io.ksmt:ksmt-core:0.6.5") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.6.4") + implementation("io.ksmt:ksmt-z3:0.6.5") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.6.4") + implementation("io.ksmt:ksmt-bitwuzla:0.6.5") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index 18c7bbad2..ba99896e4 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -9,11 +9,11 @@ repositories { dependencies { // core - implementation("io.ksmt:ksmt-core:0.6.4") + implementation("io.ksmt:ksmt-core:0.6.5") // z3 solver - implementation("io.ksmt:ksmt-z3:0.6.4") + implementation("io.ksmt:ksmt-z3:0.6.5") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.6.4") + implementation("io.ksmt:ksmt-runner:0.6.5") } java { diff --git a/ksmt-z3/dist/README.md b/ksmt-z3/dist/README.md new file mode 100644 index 000000000..b19119f50 --- /dev/null +++ b/ksmt-z3/dist/README.md @@ -0,0 +1,116 @@ +# Z3 native libraries for linux-x86-64 + +`z3-native-linux-x86-64-.zip` contains `libz3.so` and `libz3java.so` (at the archive root) +and is consumed by `ksmt-z3-native` as a `flatDir` dependency. + +Unlike every other platform, these libraries are **not** taken from the +[Z3 GitHub release](https://github.com/Z3Prover/z3/releases). The released `x64-glibc-*` package is +built against a recent glibc (2.39 for Z3 5.0.0) and does not run on older distributions, including +the `ubuntu-22.04` CI runner. Instead, we build Z3 ourselves against an old glibc and link the C++ +runtime statically. + +Every other platform (`x64-win`, `x64-osx-*`, `arm64-osx-*`, `arm64-glibc-*`) is downloaded from the +Z3 release by `mkZ3ReleaseDownloadTask`, so only linux-x86-64 needs the procedure below. + +## Building + +The build runs in an AlmaLinux 8 container: it provides glibc 2.28 (older than any supported +distribution) together with a C++20 capable toolchain, which Z3 requires since 5.0.0 +(it uses `` and ``, so GCC 13+ is a hard requirement). + +```bash +Z3_VERSION=5.0.0 + +# Z3 sources +curl -sL -o z3.tar.gz "https://github.com/Z3Prover/z3/archive/refs/tags/z3-$Z3_VERSION.tar.gz" +tar xzf z3.tar.gz # -> z3-z3-$Z3_VERSION + +docker run --rm -v "$PWD:/work" -e "Z3_VERSION=$Z3_VERSION" \ + -e "HOST_UID=$(id -u)" -e "HOST_GID=$(id -g)" almalinux:8 bash /work/build-z3-linux-x86-64.sh + +cd z3-linux-dist && zip -X -9 "../z3-native-linux-x86-64-$Z3_VERSION.zip" libz3.so libz3java.so +``` + +with `build-z3-linux-x86-64.sh`: + +```bash +#!/bin/bash +set -euo pipefail + +dnf -y install --setopt=install_weak_deps=False \ + gcc-toolset-14 cmake make java-17-openjdk-devel python3 + +source /opt/rh/gcc-toolset-14/enable +export JAVA_HOME=$(dirname $(dirname $(readlink -f $(which javac)))) + +cd "/work/z3-z3-$Z3_VERSION" + +# The CMake build gives libz3 a versioned SONAME (e.g. libz3.so.5.0) and makes libz3java +# depend on that name, but the distribution ships a flat libz3.so. Drop VERSION/SOVERSION +# to keep the SONAME equal to the file name. +python3 - <<'EOF' +p = 'src/CMakeLists.txt' +s = open(p).read() +patched = s.replace(""" VERSION ${Z3_VERSION} + SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR})""", " POSITION_INDEPENDENT_CODE ON)") +assert patched != s, "SOVERSION patch did not apply" +open(p, 'w').write(patched) +EOF + +cmake -S . -B build-linux \ + -DCMAKE_BUILD_TYPE=Release \ + -DZ3_BUILD_JAVA_BINDINGS=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_EXECUTABLE=FALSE \ + -DZ3_BUILD_TEST_EXECUTABLES=FALSE \ + -DZ3_INCLUDE_GIT_HASH=FALSE \ + -DZ3_INCLUDE_GIT_DESCRIBE=FALSE \ + -DCMAKE_SHARED_LINKER_FLAGS="-static-libstdc++ -static-libgcc -Wl,--exclude-libs,ALL" \ + -DCMAKE_EXE_LINKER_FLAGS="-static-libstdc++ -static-libgcc -Wl,--exclude-libs,ALL" + +cmake --build build-linux --target libz3 z3java -j "$(nproc)" + +mkdir -p /work/z3-linux-dist +cp build-linux/libz3.so build-linux/libz3java.so /work/z3-linux-dist/ +chown -R "$HOST_UID:$HOST_GID" /work/z3-linux-dist "/work/z3-z3-$Z3_VERSION" +``` + +### Why these linker flags + +* `-static-libstdc++ -static-libgcc` — the resulting libraries must not depend on the libstdc++ + of the machine that runs ksmt. +* `-Wl,--exclude-libs,ALL` — **required**. Without it the statically linked libstdc++ symbols stay + in the dynamic symbol table (~4500 exported `std::` symbols). They then interpose on the + libstdc++ used by the Bitwuzla / cvc5 / Yices native libraries loaded into the same JVM, + which crashes the JVM with a SIGSEGV inside `libz3.so`. + +## Verifying the result + +Run these checks before committing a new archive — a mistake here produces libraries that either +crash at runtime or silently keep the previous Z3 version. + +```bash +cd z3-linux-dist + +# 1. The version is the one we intended to build +strings -a libz3.so | grep -m1 -E '^[0-9]+\.[0-9]+\.[0-9]+\.[0-9]+$' + +# 2. No dependency on the system C++ runtime (expect 0) +objdump -T libz3.so libz3java.so | grep -c GLIBCXX + +# 3. Old glibc is enough (expect something well below the oldest supported distribution) +objdump -T libz3.so libz3java.so | grep -o 'GLIBC_[0-9.]*' | sort -uV | tail -1 + +# 4. The static C++ runtime is not exported (expect ~90, not ~4500) +nm -D --defined-only -C libz3.so | grep -c 'std::' + +# 5. SONAMEs match the file names, and libz3java depends on plain libz3.so +objdump -p libz3.so | grep -E 'SONAME|NEEDED' +objdump -p libz3java.so | grep -E 'SONAME|NEEDED' +``` + +For Z3 5.0.0 this gives: version `5.0.0.0`, `0` GLIBCXX references, max `GLIBC_2.26`, +`91` exported `std::` symbols, `SONAME libz3.so` / `SONAME libz3java.so`. + +Finally run the tests, including `:ksmt-test:test`, which loads several solvers into a single JVM +and is what catches the symbol interposition problem described above. diff --git a/ksmt-z3/dist/z3-native-linux-x86-64-4.15.3.zip b/ksmt-z3/dist/z3-native-linux-x86-64-5.0.0.zip similarity index 60% rename from ksmt-z3/dist/z3-native-linux-x86-64-4.15.3.zip rename to ksmt-z3/dist/z3-native-linux-x86-64-5.0.0.zip index 053de40c5..bd511e9dc 100644 Binary files a/ksmt-z3/dist/z3-native-linux-x86-64-4.15.3.zip and b/ksmt-z3/dist/z3-native-linux-x86-64-5.0.0.zip differ diff --git a/ksmt-z3/ksmt-z3-core/build.gradle.kts b/ksmt-z3/ksmt-z3-core/build.gradle.kts index be73b3e15..38b0ea3a5 100644 --- a/ksmt-z3/ksmt-z3-core/build.gradle.kts +++ b/ksmt-z3/ksmt-z3-core/build.gradle.kts @@ -9,7 +9,7 @@ repositories { mavenCentral() } -val z3Version = "4.15.3" +val z3Version = "5.0.0" val z3JavaJar by lazy { mkZ3ReleaseDownloadTask(z3Version, "x64-win", listOf("**/com.microsoft.z3.jar")) } diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/com/microsoft/z3/Util.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/com/microsoft/z3/Util.kt index 363f990bd..0f5fd85c4 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/com/microsoft/z3/Util.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/com/microsoft/z3/Util.kt @@ -1,5 +1,6 @@ package com.microsoft.z3 +import com.microsoft.z3.Native.BoolPtr import com.microsoft.z3.Native.IntPtr import com.microsoft.z3.Native.LongPtr import com.microsoft.z3.enumerations.Z3_error_code @@ -30,9 +31,9 @@ fun fpExponentInt64OrNull(ctx: Long, expr: Long, biased: Boolean): Long? { } fun fpSignOrNull(ctx: Long, expr: Long): Boolean? { - val result = IntPtr() + val result = BoolPtr() if (!Native.fpaGetNumeralSign(ctx, expr, result)) return null - return result.value != 0 + return result.value } @Suppress("LongParameterList") diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Model.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Model.kt index 6ac92b804..e96b4c1cb 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Model.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Model.kt @@ -13,6 +13,8 @@ import io.ksmt.KContext import io.ksmt.decl.KDecl import io.ksmt.expr.KExpr import io.ksmt.expr.KUninterpretedSortValue +import io.ksmt.expr.rewrite.simplify.castRealValue +import io.ksmt.expr.rewrite.simplify.toRealValue import io.ksmt.solver.KModel import io.ksmt.solver.model.KFuncInterp import io.ksmt.solver.model.KFuncInterpEntryVarsFree @@ -20,6 +22,7 @@ import io.ksmt.solver.model.KFuncInterpEntryWithVars import io.ksmt.solver.model.KFuncInterpVarsFree import io.ksmt.solver.model.KFuncInterpWithVars import io.ksmt.solver.model.KModelImpl +import io.ksmt.sort.KArithSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort import io.ksmt.utils.mkFreshConst @@ -92,7 +95,26 @@ open class KZ3Model( z3Ctx.releaseTemporaryAst(z3Result) - return result + return result.castToSort(expr.sort) + } + + /** + * Z3 may assign an arith sort to an expression which differs from the sort ksmt uses. + * For example, `(^ a b)` is Real sorted in Z3 even when both `a` and `b` are Int sorted, + * while in ksmt this expression is Int sorted. + * Because of this, the value we get from a Z3 model may have an unexpected arith sort. + * + * Cast such values back to the sort of the evaluated expression to keep [eval] sort preserving. + * The cast is performed in the same way as in the ksmt expression simplifier + * (see [castRealValue]) and therefore the value we produce here is consistent + * with the value produced by a detached model. + * */ + private fun KExpr.castToSort(sort: T): KExpr { + if (this.sort == sort || sort !is KArithSort) return this + + val value = uncheckedCast<_, KExpr>().toRealValue() ?: return this + + return ctx.castRealValue(value, sort).uncheckedCast() } override fun interpretation(decl: KDecl): KFuncInterp? = diff --git a/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/ModelEvalSortTest.kt b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/ModelEvalSortTest.kt new file mode 100644 index 000000000..320e821e4 --- /dev/null +++ b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/ModelEvalSortTest.kt @@ -0,0 +1,37 @@ +package io.ksmt.solver.z3 + +import io.ksmt.KContext +import io.ksmt.solver.KSolverStatus +import kotlin.test.Test +import kotlin.test.assertEquals + +/** + * Z3 assigns the Real sort to `(^ a b)` even when both `a` and `b` are Int sorted, + * while in ksmt such an expression is Int sorted. + * Because of this, a model value of an Int sorted expression may be a Real numeral. + * */ +class ModelEvalSortTest { + private val ctx = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY) + + @Test + fun testIntPowerModelValueSort() = with(ctx) { + KZ3Solver(this).use { solver -> + val base = mkConst("base", intSort) + val power = mkConst("power", intSort) + val expr = mkArithPowerNoSimplify(base, power) + + solver.assert(base eq 2.expr) + solver.assert(power eq 2.expr) + + assertEquals(KSolverStatus.SAT, solver.check()) + + val model = solver.model() + val value = model.eval(expr) + val detachedValue = model.detach().eval(expr) + + assertEquals(intSort, value.sort) + assertEquals(4.expr, value) + assertEquals(detachedValue, value) + } + } +} diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts index 89306c80d..c11bfeeb7 100644 --- a/ksmt-z3/ksmt-z3-native/build.gradle.kts +++ b/ksmt-z3/ksmt-z3-native/build.gradle.kts @@ -21,7 +21,7 @@ val `mac-arm` by sourceSets.creating val `windows-arm` by sourceSets.creating val `linux-arm` by sourceSets.creating -val z3Version = "4.15.3" +val z3Version = "5.0.0" val winDllPath = listOf("**/vcruntime140.dll", "**/vcruntime140_1.dll", "**/libz3.dll", "**/libz3java.dll") val linuxSoPath = listOf("**/libz3.so", "**/libz3java.so") @@ -30,9 +30,9 @@ val macDylibPath = listOf("**/libz3.dylib", "**/libz3java.dylib") val z3Binaries = listOf( Triple(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", winDllPath), null), Triple(`linux-x64`, null, z3NativeLinuxX64), - Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-13.7.6", macDylibPath), null), - Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-13.7.6", macDylibPath), null), - Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.34", linuxSoPath), null), + Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-13.3", macDylibPath), null), + Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-13.3", macDylibPath), null), + Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.38", linuxSoPath), null), ) z3Binaries.forEach { it.first.compileClasspath = compileConfig }