diff --git a/.github/workflows/build-and-run-tests.yml b/.github/workflows/build-and-run-tests.yml index 9df103bba..4063d5686 100644 --- a/.github/workflows/build-and-run-tests.yml +++ b/.github/workflows/build-and-run-tests.yml @@ -14,6 +14,9 @@ jobs: run_tests: name: Run tests strategy: + # Without this a failure on one platform cancels the others, and the + # cancellation is what gets reported, hiding the actual failure. + fail-fast: false matrix: os: [ ubuntu-22.04, windows-latest, macos-latest ] diff --git a/README.md b/README.md index beb367019..5d01a7b81 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.5) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.6) [![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.5") +implementation("io.ksmt:ksmt-core:0.6.6") // z3 solver -implementation("io.ksmt:ksmt-z3:0.6.5") +implementation("io.ksmt:ksmt-z3:0.6.6") ``` 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 fe9bf4972..fa3143a65 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.5" +version = "0.6.6" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 38069f783..3722a1fd7 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.5") + implementation("io.ksmt:ksmt-core:0.6.6") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.6.5") + implementation("io.ksmt:ksmt-z3:0.6.6") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.6.5") + implementation("io.ksmt:ksmt-bitwuzla:0.6.6") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index ba99896e4..c57a7f000 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.5") + implementation("io.ksmt:ksmt-core:0.6.6") // z3 solver - implementation("io.ksmt:ksmt-z3:0.6.5") + implementation("io.ksmt:ksmt-z3:0.6.6") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.6.5") + implementation("io.ksmt:ksmt-runner:0.6.6") } java { diff --git a/ksmt-cvc5/dist/build.md b/ksmt-cvc5/dist/build.md index b1cb663d0..29f0621d2 100644 --- a/ksmt-cvc5/dist/build.md +++ b/ksmt-cvc5/dist/build.md @@ -1,68 +1,165 @@ -### Build details +# cvc5 distribution for ksmt -Build is based on the cvc5 fork: https://github.com/Saloed/cvc5/tree/ksmt -This fork provides fixed Java API and buildscripts (`build_(linux|windows|mac).sh`) +`ksmt-cvc5-core` compiles against `cvc5-.jar` and `ksmt-cvc5-native` ships one +`cvc5-native--.zip` per platform, consumed as a `flatDir` dependency. +The libraries in each zip are loaded, in order, by the matching +`KCvc5NativeLibraryLoader*` in `ksmt-cvc5-native`. + +| Artifact | Contents | Origin | +| --- | --- | --- | +| `cvc5-.jar` | `io.github.cvc5.*` classes, no natives | built from the fork (see below) | +| `cvc5-native-linux-x86-64-.zip` | `libcvc5.so.1`, `libcvc5parser.so.1`, `libcvc5jni.so` | built from the fork | +| `cvc5-native-win-x86-64-.zip` | `libcvc5jni.dll` | official cvc5 release | +| `cvc5-native-osx-arm64-.zip` | `libcvc5jni.dylib` | official cvc5 release | + +The jar must always come from the same cvc5 patch release as the native libraries: +`Kind` constants are generated from the C++ headers and new kinds are inserted mid-list, +so `Kind` ordinals shift between releases. + +## The fork + +Build is based on the cvc5 fork , branch `ksmt-` +(`ksmt` for the 1.3.0-era builds). It is a two-commit patch series on top of the upstream +release tag, and is refreshed by rebasing those two commits onto the new tag: -We build cvc5 with the following configuration: ```shell -./configure.sh production --auto-download --ipo --no-static --no-cln --no-glpk --no-editline --cryptominisat --java-bindings +git rebase --onto cvc5- cvc5- ``` -To make our distribution portable we statically link cvc5 against `libgmp`. -#### Building on Windows -To produce Windows builds we use the same approach as in [`ksmt-bitwuzla`](../../ksmt-bitwuzla/dist/build.md). -Also, we use addition configuration flag: +**`disable library load`** — patches the Java API: + +* `AbstractPointer` and `IPointer` are made `public`. `KCvc5TermManager` uses + `AbstractPointer` as a generic bound and calls `getPointer()`/`deletePointer()` on it. +* `Context`'s global pointer registry is disabled (`TRACK_POINTERS = false`). Upstream + registers *every* `Term`/`Sort`/`Op` in a static map that is only drained by + `Context.deletePointers()`. ksmt manages cvc5 objects per solver via `KCvc5TermManager` + and never calls that JVM-global method, so the registry would retain every term ksmt + ever creates. +* cvc5 does not load its native libraries from its own static initializers. ksmt ships + the libraries in its own resource layout and loads them explicitly + (`KCvc5NativeLibraryLoader`). This is belt-and-braces: `KCvc5Solver` also sets + `-Dcvc5.skipLibraryLoad=true`, which upstream honours. + +**`Fix build`** — adds `build_(linux|windows|mac).sh` and cmake fixes: libpoly is linked +statically even for a shared cvc5 build, `CMAKE_AR` is honoured when cross-compiling, and +the macOS deployment target is pinned. + +## Building linux-x86-64 + +Built in an AlmaLinux 8 container, which provides a glibc (2.28) older than any supported +distribution together with a C++17 toolchain. Do **not** use the official Linux release +artifacts: they require glibc 2.33 and export ~1350 `std::` symbols, which interpose on +the C++ runtime of the other native solvers in the same JVM. + ```shell -./configure.sh ... --win64-native +docker run --rm -v "$PWD:/work" -e "HOST_UID=$(id -u)" -e "HOST_GID=$(id -g)" \ + -w /work almalinux:8 bash /work/cvc5/build_linux.sh + +cd linux-dist/dist +zip -X -9 "cvc5-native-linux-x86-64-.zip" libcvc5jni.so libcvc5parser.so.1 libcvc5.so.1 ``` -### Expected dynamic dependencies -To ensure that our distribution is portable, we verify that the produced binaries have no dependencies that might not be present on the user's machine. +with the fork checked out in `./cvc5`. See `build_linux.sh` in the fork for the full +recipe; the parts that matter are: + +* `./configure.sh production --auto-download --ipo --no-static --no-cln --no-glpk + --no-editline --java-bindings` +* `LDFLAGS="-static-libgcc -static-libstdc++ -Wl,--exclude-libs=ALL"`. The static linking + keeps the libraries independent of the host C++ runtime; `--exclude-libs=ALL` is + **required** to keep those statically linked symbols out of the dynamic symbol table, + otherwise they interpose on the libstdc++ used by the Bitwuzla / Z3 / Yices libraries + loaded into the same JVM and crash it with a SIGSEGV. +* GMP is built statically and separately, because for a shared cvc5 build cvc5 would + otherwise produce a shared GMP that we would have to ship as a fourth library. +* The jar is built with JDK 8 — ksmt targets Java 8. +* Since 1.3.4 `libcvc5.so.1` and `libcvc5parser.so.1` are symlinks to the fully versioned + files, so packaging must dereference them (`cp -L`). + +## Windows x64 and macOS arm64 + +Taken from the official [cvc5 release](https://github.com/cvc5/cvc5/releases). Since +cvc5 1.3.2 the `cvc5--java-api.jar` release assets contain a single, +self-contained JNI library under `cvc5-libs///` with libcvc5, libcvc5parser, +GMP and the C++ runtime all linked in, so no post-processing is needed: -#### Linux x64 ```shell -$ ldd libcvc5.so libcvc5jni.so -libcvc5.so: - linux-vdso.so.1 (0x00007ffe22381000) - libm.so.6 => /usr/lib/libm.so.6 (0x00007ff4c8bf4000) - libc.so.6 => /usr/lib/libc.so.6 (0x00007ff4c7619000) - /usr/lib64/ld-linux-x86-64.so.2 (0x00007ff4c8d0a000) -libcvc5jni.so: - linux-vdso.so.1 (0x00007ffccbbb5000) - libcvc5.so => not found - libc.so.6 => /usr/lib/libc.so.6 (0x00007fa594c19000) - libm.so.6 => /usr/lib/libm.so.6 (0x00007fa5961f3000) - /usr/lib64/ld-linux-x86-64.so.2 (0x00007fa596389000) +unzip -j "cvc5-Win64-x86_64-java-api.jar" "cvc5-libs/windows/x86_64/cvc5jni.dll" +zip -X -9 "cvc5-native-win-x86-64-.zip" libcvc5jni.dll # note: renamed + +unzip -j "cvc5-macOS-arm64-java-api.jar" "cvc5-libs/osx/aarch_64/libcvc5jni.dylib" +zip -X -9 "cvc5-native-osx-arm64-.zip" libcvc5jni.dylib ``` -#### Windows x64 + +Do **not** use the `-shared.zip` assets: their libraries reference each other through +`@rpath`/relative names, and on macOS they are ad-hoc code signed, so the install-name +rewriting the old fork-based build did would invalidate the signature. + +Note that the Windows library links the UCRT, so it requires Windows 10 or newer. + +## Verifying the result + +Run these before committing new archives. + ```shell -$ ldd libcvc5.dll libcvc5jni.dll -libcvc5.dll: - ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000) - KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000) - KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000) - msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000) - CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000) - bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000) -libcvc5jni.dll: - ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000) - KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000) - KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000) - msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000) - libcvc5.dll => not found - CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000) - bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000) +# The version is the one we intended to ship +strings -a libcvc5.so.1 | grep -m1 -E '^1\.[0-9]+\.[0-9]+$' + +# No dependency on the system C++ runtime (expect 0) +objdump -T libcvc5.so.1 libcvc5parser.so.1 libcvc5jni.so | grep -c GLIBCXX + +# Old glibc is enough +objdump -T libcvc5.so.1 libcvc5parser.so.1 libcvc5jni.so | grep -o 'GLIBC_[0-9.]*' | sort -uV | tail -1 + +# The static C++ runtime is not exported (expect a few hundred, not thousands) +nm -D --defined-only -C libcvc5.so.1 | grep -c 'std::' + +# The jar is Java 8 and carries no natives +unzip -l cvc5-.jar | grep -c cvc5-libs ``` -#### MacOS aarch64 + +For cvc5 1.3.4 this gives version `1.3.4`, `0` GLIBCXX references, max `GLIBC_2.25`, +`402`/`251`/`10` exported `std::` symbols, and `0` native entries in the jar. + +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. + +## Expected dynamic dependencies + +To ensure the distribution is portable, verify the produced binaries have no dependencies +that might not be present on the user's machine. + +### Linux x64 + ```shell -$ otool -L libcvc5.dylib libcvc5jni.dylib -libcvc5.dylib: - @rpath/libcvc5.dylib (compatibility version 0.0.0, current version 0.0.0) - /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0) - /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0) +$ objdump -p libcvc5.so.1 libcvc5parser.so.1 libcvc5jni.so | grep -E 'SONAME|NEEDED' +libcvc5.so.1: NEEDED libm.so.6, libc.so.6, ld-linux-x86-64.so.2 + SONAME libcvc5.so.1 +libcvc5parser.so.1: NEEDED libcvc5.so.1, libm.so.6, libc.so.6, ld-linux-x86-64.so.2 + SONAME libcvc5parser.so.1 +libcvc5jni.so: NEEDED libcvc5parser.so.1, libcvc5.so.1, libm.so.6, libc.so.6, ld-linux-x86-64.so.2 + SONAME libcvc5jni.so +``` + +### Windows x64 + +```shell +$ objdump -p libcvc5jni.dll | grep 'DLL Name' + DLL Name: api-ms-win-crt-{convert,environment,filesystem,heap,locale,math, + multibyte,private,runtime,stdio,string,time,utility}-l1-1-0.dll + DLL Name: KERNEL32.dll +``` + +No `libstdc++-6.dll`, `libgcc_s_seh-1.dll`, `libwinpthread-1.dll` and no sibling cvc5 DLL. + +### MacOS aarch64 + +```shell +$ otool -L libcvc5jni.dylib libcvc5jni.dylib: @rpath/libcvc5jni.dylib (compatibility version 0.0.0, current version 0.0.0) - @rpath/libcvc5.dylib (compatibility version 0.0.0, current version 0.0.0) - /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0) - /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0) + /usr/lib/libc++.1.dylib + /usr/lib/libSystem.B.dylib ``` + +Both dependencies are absolute system paths and there is no `LC_RPATH`, so the `@rpath` +install name is never resolved — ksmt loads the library by absolute path. diff --git a/ksmt-cvc5/dist/cvc5-1.3.0.jar b/ksmt-cvc5/dist/cvc5-1.3.0.jar deleted file mode 100644 index 6c33e7f6c..000000000 Binary files a/ksmt-cvc5/dist/cvc5-1.3.0.jar and /dev/null differ diff --git a/ksmt-cvc5/dist/cvc5-1.3.4.jar b/ksmt-cvc5/dist/cvc5-1.3.4.jar new file mode 100644 index 000000000..4883ea48f Binary files /dev/null and b/ksmt-cvc5/dist/cvc5-1.3.4.jar differ diff --git a/ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.0.zip b/ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.4.zip similarity index 55% rename from ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.0.zip rename to ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.4.zip index 5d4fe0a45..34839b999 100644 Binary files a/ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.0.zip and b/ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.4.zip differ diff --git a/ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.0.zip b/ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.4.zip similarity index 53% rename from ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.0.zip rename to ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.4.zip index 72a884aa6..683104359 100644 Binary files a/ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.0.zip and b/ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.4.zip differ diff --git a/ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.0.zip b/ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.4.zip similarity index 54% rename from ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.0.zip rename to ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.4.zip index c5264f908..b66d07246 100644 Binary files a/ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.0.zip and b/ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.4.zip differ diff --git a/ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts b/ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts index b70bebbd8..b950ef3d7 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts +++ b/ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts @@ -11,7 +11,7 @@ repositories { mavenCentral() } -val cvc5Version = "1.3.0" +val cvc5Version = "1.3.4" val cvc5Jar = distDir.resolve("cvc5-$cvc5Version.jar") dependencies { diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt index 1f34145a1..c79749d98 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt @@ -148,6 +148,7 @@ open class KCvc5ExprConverter( Kind.SQRT -> throw KSolverUnsupportedFeatureException("No direct mapping of sqrt on real in ksmt") Kind.POW -> convertNativePowExpr(expr) Kind.POW2 -> convertNativePowExpr(expr) + Kind.LOG2 -> throw KSolverUnsupportedFeatureException("No direct mapping of log2 on int in ksmt") Kind.INTS_MODULUS -> expr.convert(::mkIntMod) Kind.INTS_DIVISION -> expr.convert(::mkArithDiv) Kind.DIVISION -> expr.convert(::mkArithDiv) @@ -178,7 +179,8 @@ open class KCvc5ExprConverter( Kind.DIVISIBLE -> expr.convert { arExpr: KExpr -> mkIntMod(arExpr, expr.intDivisibleArg.expr) eq 0.expr } - Kind.IAND -> throw KSolverUnsupportedFeatureException( + Kind.IAND, + Kind.PIAND -> throw KSolverUnsupportedFeatureException( "No direct mapping in ksmt. btw int to bv is not supported in ksmt" ) diff --git a/ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts b/ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts index 2ff1fb872..2226f2b13 100644 --- a/ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts +++ b/ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts @@ -29,7 +29,7 @@ val cvc5Binaries = mapOf( cvc5Binaries.keys.forEach { it.compileClasspath = compileConfig } -val cvc5Version = "1.3.0" +val cvc5Version = "1.3.4" dependencies { compileConfig(project(":ksmt-cvc5:ksmt-cvc5-core")) diff --git a/ksmt-cvc5/ksmt-cvc5-native/src/mac-arm/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderMacArm.kt b/ksmt-cvc5/ksmt-cvc5-native/src/mac-arm/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderMacArm.kt index dd5e49c37..f1e50b761 100644 --- a/ksmt-cvc5/ksmt-cvc5-native/src/mac-arm/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderMacArm.kt +++ b/ksmt-cvc5/ksmt-cvc5-native/src/mac-arm/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderMacArm.kt @@ -14,9 +14,9 @@ class KCvc5NativeLibraryLoaderMacArm : } companion object { + // A single self-contained library: the cvc5 release build for this platform + // links libcvc5 and libcvc5parser into libcvc5jni. private val libraries = listOf( - "libcvc5.1", - "libcvc5parser.1", "libcvc5jni", ) } diff --git a/ksmt-cvc5/ksmt-cvc5-native/src/windows-x64/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderWindowsX64.kt b/ksmt-cvc5/ksmt-cvc5-native/src/windows-x64/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderWindowsX64.kt index 8f66e0dcd..92d4add0a 100644 --- a/ksmt-cvc5/ksmt-cvc5-native/src/windows-x64/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderWindowsX64.kt +++ b/ksmt-cvc5/ksmt-cvc5-native/src/windows-x64/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderWindowsX64.kt @@ -14,9 +14,9 @@ class KCvc5NativeLibraryLoaderWindowsX64 : } companion object { + // A single self-contained library: the cvc5 release build for this platform + // links libcvc5 and libcvc5parser into libcvc5jni. private val libraries = listOf( - "libcvc5", - "libcvc5parser", "libcvc5jni" ) } diff --git a/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/IncrementalApiTest.kt b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/IncrementalApiTest.kt index c615b8541..1d949feae 100644 --- a/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/IncrementalApiTest.kt +++ b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/IncrementalApiTest.kt @@ -1,5 +1,6 @@ package io.ksmt.solver.z3 +import com.microsoft.z3.Global import io.ksmt.KContext import io.ksmt.solver.KSolverStatus import io.ksmt.utils.mkConst @@ -82,8 +83,43 @@ class IncrementalApiTest { val query = mkUniversalQuantifier(queryBody, listOf(x.decl)) solver.assert(query) - val status = solver.checkWithAssumptions(emptyList(), timeout = 1.milliseconds) + val status = withZ3MemoryLimit(MEMORY_LIMIT_MB) { + solver.checkWithAssumptions(emptyList(), timeout = 1.milliseconds) + } assertEquals(KSolverStatus.UNKNOWN, status) - assertEquals("timeout", solver.reasonOfUnknown()) + + /** + * Normally Z3 reports the timeout. If it happens to reach the memory limit before + * its next timeout checkpoint it reports [Z3_OUT_OF_MEMORY_REASON] instead, which is + * an equally valid "gave up on the resource limit" outcome. + */ + val reason = solver.reasonOfUnknown() + assertTrue( + reason == TIMEOUT_REASON || reason == Z3_OUT_OF_MEMORY_REASON, + "Unexpected reason of unknown: $reason" + ) + } + + /** + * Z3 only checks the [timeout] parameter at its internal checkpoints. On this query it + * allocates memory far faster than it reaches one, so without a memory limit the check + * grows to tens of gigabytes and the test process gets killed by the OS. + * + * The limit is a global Z3 parameter because a solver parameter would not survive: + * every check replaces the solver parameters with the ones holding the timeout. + */ + private inline fun withZ3MemoryLimit(limitMb: Int, body: () -> T): T = try { + Global.setParameter(Z3_MAX_MEMORY, limitMb.toString()) + body() + } finally { + Global.setParameter(Z3_MAX_MEMORY, UNLIMITED_MEMORY) + } + + companion object { + private const val Z3_MAX_MEMORY = "memory_max_size" + private const val UNLIMITED_MEMORY = "0" + private const val MEMORY_LIMIT_MB = 2048 + private const val TIMEOUT_REASON = "timeout" + private const val Z3_OUT_OF_MEMORY_REASON = "out of memory" } }