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 cfb3207ef..a56559257 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.7" +version = project.findProperty("ksmtVersion")?.toString()?.takeIf { it.isNotBlank() } ?: "0.6.7" repositories { mavenCentral() diff --git a/jitpack.yml b/jitpack.yml new file mode 100644 index 000000000..99bcee790 --- /dev/null +++ b/jitpack.yml @@ -0,0 +1,4 @@ +jdk: + - openjdk17 +install: + - ./gradlew :ksmt-core:publishToMavenLocal :ksmt-bitwuzla:ksmt-bitwuzla-core:publishToMavenLocal ":ksmt-bitwuzla:ksmt-bitwuzla-native:publishMaven-linux-x64PublicationToMavenLocal" -PksmtVersion=$VERSION -x test -x dokkaJavadoc -Dorg.gradle.jvmargs=-Xmx1g diff --git a/ksmt-bitwuzla/dist/Dockerfile.bitwuzla-linux64 b/ksmt-bitwuzla/dist/Dockerfile.bitwuzla-linux64 new file mode 100644 index 000000000..bbf3dd095 --- /dev/null +++ b/ksmt-bitwuzla/dist/Dockerfile.bitwuzla-linux64 @@ -0,0 +1,59 @@ +ARG BASE_REGISTRY=docker.io + +FROM ${BASE_REGISTRY}/library/ubuntu:22.04@sha256:08ea48a03a3e78ebc7cd526e6a275053223aadd88bfc09cc49b06d5281525fde AS build + +ARG BITWUZLA_COMMIT=1230d80a5275ddf525da9c218c2bcd29c3130e49 +ARG BITWUZLA_SHA256=3639b4bb8c4e832514fe45456ac12c1e1a87af2d66f67518a82ab3014ac90b9b +ARG GMP_VERSION=6.3.0 +ARG GMP_SHA256=a3c2b80201b89e68616f4ad30bc66aee4927c3ce50e33929ca819d5c43538898 + +RUN apt-get update \ + && apt-get install -y --no-install-recommends \ + binutils build-essential ca-certificates cmake curl git m4 patch python3 unzip xz-utils zip \ + && rm -rf /var/lib/apt/lists/* + +WORKDIR /build + +RUN curl -fsSL -o gmp.tar.xz "https://ftp.gnu.org/gnu/gmp/gmp-${GMP_VERSION}.tar.xz" \ + && echo "${GMP_SHA256} gmp.tar.xz" | sha256sum -c - \ + && tar xf gmp.tar.xz \ + && cd "gmp-${GMP_VERSION}" \ + && ./configure --prefix=/build/deps --disable-shared --enable-static --with-pic --enable-fat --enable-cxx \ + && make -j"$(nproc)" \ + && make install + +RUN curl -fsSL -o bitwuzla.tar.gz "https://github.com/bitwuzla/bitwuzla/archive/${BITWUZLA_COMMIT}.tar.gz" \ + && echo "${BITWUZLA_SHA256} bitwuzla.tar.gz" | sha256sum -c - \ + && tar xzf bitwuzla.tar.gz \ + && mv "bitwuzla-${BITWUZLA_COMMIT}" bitwuzla + +COPY bitwuzla-gh31.patch /build/ +RUN cd bitwuzla && patch -p1 < /build/bitwuzla-gh31.patch + +RUN cd bitwuzla \ + && ./contrib/setup-cadical.sh \ + && ./contrib/setup-btor2tools.sh \ + && ./contrib/setup-symfpu.sh + +RUN cd bitwuzla \ + && LDFLAGS="-static-libstdc++ -static-libgcc" ./configure.sh production --shared --only-cadical --path /build/deps \ + && cd build \ + && make -j"$(nproc)" + +COPY bitwuzla-linux64-1.0.zip /build/original.zip +RUN mkdir original out \ + && unzip -q original.zip -d original \ + && lib=/build/bitwuzla/build/lib/libbitwuzla.so \ + && needed=$(objdump -p "$lib" | awk '/NEEDED/ { print $2 }' | grep -v '^ld-linux' | sort | tr '\n' ' ') \ + && [ "$needed" = "libc.so.6 libm.so.6 " ] \ + && ! nm -D --undefined-only "$lib" | grep -q -i gmp \ + && nm -D --undefined-only original/libbitwuzla_jni.so | awk '{ print $NF }' | grep -E '^(bzla|bitwuzla)_' | sort -u > needed.txt \ + && nm -D --defined-only "$lib" | awk '{ print $NF }' | sort -u > defined.txt \ + && missing=$(comm -23 needed.txt defined.txt) \ + && [ -z "$missing" ] \ + && cp "$lib" original/libbitwuzla.so \ + && (cd original && zip -q -X ../out/bitwuzla-linux64-1.0.zip libbitwuzla.so libbitwuzla_jni.so) \ + && sha256sum "$lib" | awk '{ print $1 }' > out/libbitwuzla.so.sha256 + +FROM scratch AS out +COPY --from=build /build/out/ / diff --git a/ksmt-bitwuzla/dist/bitwuzla-gh31.patch b/ksmt-bitwuzla/dist/bitwuzla-gh31.patch new file mode 100644 index 000000000..2a9a912dd --- /dev/null +++ b/ksmt-bitwuzla/dist/bitwuzla-gh31.patch @@ -0,0 +1,67 @@ +--- a/src/bzlabeta.c ++++ b/src/bzlabeta.c +@@ -460,12 +460,10 @@ + cache_beta_result(bzla, cache, real_cur->e[0], e[0], result); + break; + case BZLA_LAMBDA_NODE: +- /* function equalities and conditionals always expect a lambda +- * as argument */ +- if (cur_parent +- && (bzla_node_is_fun_eq(cur_parent) +- || (bzla_node_is_fun_cond(cur_parent) +- && !bzla_node_param_get_assigned_exp(real_cur->e[0])))) ++ /* a lambda whose parameter was not instantiated by this ++ * reduction (function equalities, conditionals, array updates) ++ * stays a lambda */ ++ if (!bzla_node_param_get_assigned_exp(real_cur->e[0])) + { + assert(bzla_node_is_param(e[1])); + result = bzla_exp_lambda(bzla, e[1], e[0]); +@@ -640,7 +638,7 @@ + else if (bzla_node_is_param(real_cur)) + { + next = bzla_node_param_get_assigned_exp(real_cur); +- assert(next); ++ if (!next) next = real_cur; + next = bzla_node_cond_invert(cur, next); + BZLA_PUSH_STACK(arg_stack, bzla_node_copy(bzla, next)); + continue; +@@ -710,9 +708,23 @@ + } + break; + case BZLA_LAMBDA_NODE: +- /* lambdas are always reduced to some term without e[1] */ +- assert(!bzla_node_real_addr(e[0])->parameterized); +- result = bzla_node_copy(bzla, e[0]); ++ /* a nested lambda whose parameter was not instantiated by this ++ * reduction (e.g. the array of an update) stays a lambda */ ++ if (!bzla_node_param_get_assigned_exp(real_cur->e[0])) ++ { ++ assert(bzla_node_is_param(e[1])); ++ result = bzla_exp_lambda(bzla, e[1], e[0]); ++ if (real_cur->is_array) result->is_array = 1; ++ if (bzla_node_lambda_get_static_rho(real_cur) ++ && !bzla_node_lambda_get_static_rho(result)) ++ bzla_node_lambda_set_static_rho( ++ result, bzla_node_lambda_copy_static_rho(bzla, real_cur)); ++ } ++ else ++ { ++ assert(!bzla_node_real_addr(e[0])->parameterized); ++ result = bzla_node_copy(bzla, e[0]); ++ } + break; + case BZLA_COND_NODE: + /* only condition rebuilt, evaluate and choose branch */ +@@ -779,7 +791,10 @@ + if (real_cur->parameterized || bzla_node_is_lambda(real_cur)) + BZLA_PUSH_STACK(reset, real_cur); + +- if (bzla_node_is_lambda(real_cur)) ++ /* only a lambda whose parameters were assigned above pushed its own ++ * entry on 'reset'; a rebuilt nested lambda has nothing to unwind */ ++ if (bzla_node_is_lambda(real_cur) ++ && bzla_node_param_get_assigned_exp(real_cur->e[0])) + { + bzla_beta_unassign_params(bzla, real_cur); + next = BZLA_POP_STACK(reset); diff --git a/ksmt-bitwuzla/dist/bitwuzla-linux64-1.0.zip b/ksmt-bitwuzla/dist/bitwuzla-linux64-1.0.zip index 527615c62..f6997edfd 100644 Binary files a/ksmt-bitwuzla/dist/bitwuzla-linux64-1.0.zip and b/ksmt-bitwuzla/dist/bitwuzla-linux64-1.0.zip differ diff --git a/ksmt-bitwuzla/dist/build-linux64.sh b/ksmt-bitwuzla/dist/build-linux64.sh new file mode 100755 index 000000000..6d685a2ae --- /dev/null +++ b/ksmt-bitwuzla/dist/build-linux64.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash +set -euo pipefail + +here=$(cd "$(dirname "$(readlink -f "$0")")" && pwd) +out=$(mktemp -d) + +docker build \ + --build-arg BASE_REGISTRY="${BASE_REGISTRY:-docker.io}" \ + --target out \ + --output "type=local,dest=$out" \ + -f "$here/Dockerfile.bitwuzla-linux64" \ + "$here" + +cp "$out/bitwuzla-linux64-1.0.zip" "$here/bitwuzla-linux64-1.0.zip" +echo "libbitwuzla.so sha256: $(cat "$out/libbitwuzla.so.sha256")" +rm -rf "$out" diff --git a/ksmt-bitwuzla/dist/build.md b/ksmt-bitwuzla/dist/build.md index 5be38b43d..447bf6e7d 100644 --- a/ksmt-bitwuzla/dist/build.md +++ b/ksmt-bitwuzla/dist/build.md @@ -8,6 +8,24 @@ To make our distribution portable we statically link Bitwuzla against `libgmp`. Jni bindings `bitwuzla_jni` are built without any tricks. +### Linux x64 rebuild with the beta-reduction fix + +`bitwuzla-linux64-1.0.zip` carries a `libbitwuzla.so` rebuilt from Bitwuzla commit `1230d80a5275ddf525da9c218c2bcd29c3130e49` with `bitwuzla-gh31.patch` applied. +The patch stops `beta_reduce` and `beta_reduce_partial_aux` in `src/bzlabeta.c` from replacing a lambda by its body when the lambda's parameter was not instantiated. +Without it an array `update` over such a lambda took a bitvector sort, and the next `bzla_node_create_apply` crashed in `bzla_sort_fun_get_codomain`. +The crash is reached from the fun solver's lemma loop, so no option avoids it. + +`Dockerfile.bitwuzla-linux64` reproduces the build: GMP 6.3.0 static with `--with-pic --enable-fat`, the pinned Bitwuzla tarball, the patch, the `contrib/setup-*.sh` dependencies, then `./configure.sh production --shared --only-cadical`. +It checks that the result needs only `libc.so.6` and `libm.so.6` and defines every `bzla_*` and `bitwuzla_*` symbol the unchanged `libbitwuzla_jni.so` imports, then repacks the zip. + +```shell +BASE_REGISTRY=mirror.gcr.io ./build-linux64.sh +``` + +`libbitwuzla_jni.so` in the zip is still the original binary. +The rebuilt `libbitwuzla.so` has sha256 `6b2ee8e5efed1af68f86474dfeff7c8f9685f3999472073ce201529fb4486252`. +It also lists `ld-linux-x86-64.so.2` as a dependency and needs glibc 2.33 or newer, because the build image is Ubuntu 22.04; the 2023 binary needed glibc 2.14. + ### Building on windows To produce Windows builds we use MSYS2 environment prepared as described [here](https://github.com/aytey/bitwuzla/blob/refreshed_windows_instructions/docs/building_on_windows.rst). Also, it is important to link statically with `libwinpthread`. diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt index 164ad78a8..f9425f560 100644 --- a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt +++ b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt @@ -15,6 +15,17 @@ import io.ksmt.expr.KConst import io.ksmt.expr.KEqExpr import io.ksmt.expr.KExpr import io.ksmt.expr.KFpRoundingMode +import io.ksmt.expr.KApp +import io.ksmt.expr.KArray2Lambda +import io.ksmt.expr.KArray2Store +import io.ksmt.expr.KArray3Lambda +import io.ksmt.expr.KArray3Store +import io.ksmt.expr.KArrayLambda +import io.ksmt.expr.KArrayLambdaBase +import io.ksmt.expr.KArrayNLambda +import io.ksmt.expr.KArrayNStore +import io.ksmt.expr.KArrayStore +import io.ksmt.expr.KArrayStoreBase import io.ksmt.expr.KInterpretedValue import io.ksmt.expr.KIteExpr import io.ksmt.expr.printer.ExpressionPrinter @@ -1186,6 +1197,11 @@ open class KBitwuzlaExprConverter( return@with expr.arg.uncheckedCast() } + val retypedArray = ArrayDomainRetyper(fromSort, toSort).retype(expr.arg) + if (retypedArray != null) { + return@with AdapterTermRewriter(ctx).apply(retypedArray).uncheckedCast() + } + val indices = toSort.domainSorts.map { mkFreshConst("i", it) } @@ -1216,6 +1232,135 @@ open class KBitwuzlaExprConverter( } } + private inner class ArrayDomainRetyper( + private val fromSort: KArraySortBase<*>, + private val toSort: KArraySortBase<*> + ) : KNonRecursiveTransformer(ctx) { + private val retypedIndices = hashMapOf, KDecl<*>>() + private var failed = false + + fun retype(array: KExpr<*>): KExpr<*>? { + val result = apply(array) + return if (failed || result.sort != toSort) null else result + } + + override fun exprTransformationRequired(expr: KExpr): Boolean = + expr !is KInterpretedValue && !expr.isAdapterTerm() + + private fun KExpr<*>.isAdapterTerm(): Boolean = + this is BoolToBv1AdapterExpr || + this is Bv1ToBoolAdapterExpr || + this is Bv32ToUninterpretedSortAdapterExpr || + this is ArrayAdapterExpr<*, *> + + override fun transformApp(expr: KApp): KExpr { + if (expr.sort == fromSort || expr.args.any { it.isRetypedIndex() }) failed = true + return expr + } + + override fun transform(expr: KEqExpr): KExpr = + transformExprAfterTransformed(expr, expr.lhs, expr.rhs) { lhs, rhs -> + retypedEquality(lhs, rhs) ?: retypedEquality(rhs, lhs) ?: run { + if (lhs.isRetypedIndex() || rhs.isRetypedIndex()) failed = true + ctx.mkEq(lhs, rhs) + } + } + + override fun , R : KSort> transform(expr: KArrayConst): KExpr = + if (expr.sort != fromSort) super.transform(expr) else retypedConstArray(expr) + + override fun transform(expr: KArrayStore): KExpr> = + if (expr.sort != fromSort) super.transform(expr) else retypedStore(expr) + + override fun transform( + expr: KArray2Store + ): KExpr> = + if (expr.sort != fromSort) super.transform(expr) else retypedStore(expr) + + override fun transform( + expr: KArray3Store + ): KExpr> = + if (expr.sort != fromSort) super.transform(expr) else retypedStore(expr) + + override fun transform(expr: KArrayNStore): KExpr> = + if (expr.sort != fromSort) super.transform(expr) else retypedStore(expr) + + override fun transform(expr: KArrayLambda): KExpr> = + if (expr.sort != fromSort) super.transform(expr) else retypedLambda(expr) + + override fun transform( + expr: KArray2Lambda + ): KExpr> = + if (expr.sort != fromSort) super.transform(expr) else retypedLambda(expr) + + override fun transform( + expr: KArray3Lambda + ): KExpr> = + if (expr.sort != fromSort) super.transform(expr) else retypedLambda(expr) + + override fun transform(expr: KArrayNLambda): KExpr> = + if (expr.sort != fromSort) super.transform(expr) else retypedLambda(expr) + + private fun retypedConstArray(expr: KArrayConst<*, *>): KExpr { + val array: KExpr = expr.uncheckedCast() + return transformExprAfterTransformed(array, expr.value) { value -> + val wellSortedValue: KExpr = value.convertToExpectedIfNeeded(toSort.range) + val arraySort: KArraySortBase = toSort.uncheckedCast() + ctx.mkArrayConst(arraySort, wellSortedValue).uncheckedCast() + }.uncheckedCast() + } + + private fun retypedStore(expr: KArrayStoreBase<*, *>): KExpr { + val store: KExpr = expr.uncheckedCast() + return transformExprAfterTransformed(store, expr.args) { args -> + val indices = args.subList(1, args.lastIndex) + if (indices.any { it !is KInterpretedValue<*> }) failed = true + val array: KExpr> = args.first().uncheckedCast() + with(ctx) { mkAnyArrayStore(array, indices, args.last()) }.uncheckedCast() + }.uncheckedCast() + } + + private fun retypedLambda(expr: KArrayLambdaBase<*, *>): KExpr { + val oldDecls = expr.indexVarDeclarations + if (oldDecls.size != toSort.domainSorts.size) failed = true + val newDecls = oldDecls.zip(toSort.domainSorts) { old, sort -> retypedIndexDecl(old, sort) } + + val lambda: KExpr = expr.uncheckedCast() + val body: KExpr = expr.body.uncheckedCast() + return transformExprAfterTransformed(lambda, body) { transformedBody -> + val wellSortedBody: KExpr = transformedBody.convertToExpectedIfNeeded(toSort.range) + with(ctx) { mkAnyArrayLambda(newDecls, wellSortedBody) }.uncheckedCast() + }.uncheckedCast() + } + + private fun retypedIndexDecl(old: KDecl<*>, sort: KSort): KDecl<*> = when { + old.sort == sort -> old + old.sort == ctx.bv32Sort && sort is KUninterpretedSort -> + retypedIndices.getOrPut(old) { ctx.mkFreshConstDecl(old.name, sort) } + else -> { + failed = true + old + } + } + + private fun retypedEquality(index: KExpr, other: KExpr): KExpr? { + val newIndex = retypedConst(index) ?: return null + val newOther: KExpr = when { + other is KBitVec32Value -> Bv32ToUninterpretedSortAdapterExpr(other, newIndex.sort) + else -> retypedConst(other) ?: return null + } + return ctx.mkEq(newIndex, newOther) + } + + private fun KExpr<*>.isRetypedIndex(): Boolean = this is KConst<*> && decl in retypedIndices + + private fun retypedConst(expr: KExpr<*>): KExpr? { + if (expr !is KConst<*>) return null + val newDecl = retypedIndices[expr.decl] ?: return null + return ctx.mkConstApp(newDecl).uncheckedCast() + } + } + inline fun BitwuzlaTerm.convertBv( op: (KExpr, KExpr) -> KExpr ) = convert { a0: KExpr, a1: KExpr -> diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/test/kotlin/io/ksmt/solver/bitwuzla/UninterpretedSortArrayModelTest.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/test/kotlin/io/ksmt/solver/bitwuzla/UninterpretedSortArrayModelTest.kt new file mode 100644 index 000000000..4fe58dd7d --- /dev/null +++ b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/test/kotlin/io/ksmt/solver/bitwuzla/UninterpretedSortArrayModelTest.kt @@ -0,0 +1,56 @@ +package io.ksmt.solver.bitwuzla + +import io.ksmt.KContext +import io.ksmt.solver.KSolverStatus +import kotlin.test.Test +import kotlin.test.assertEquals + +class UninterpretedSortArrayModelTest { + private val ctx = KContext() + private val solver = KBitwuzlaSolver(ctx) + + @Test + fun detachModelOfSelectedTwoIndexArrayOverUninterpretedSort(): Unit = with(ctx) { + val address = mkUninterpretedSort("Address") + val array = mkConst("input", mkArraySort(address, bv32Sort, bv8Sort)) + val a = mkConst("a", address) + val i = mkConst("i", bv32Sort) + val selected = array.select(a, i) + + solver.assert(selected eq mkBv(5.toByte())) + assertEquals(KSolverStatus.SAT, solver.check()) + + val model = solver.model().detach() + assertEquals(mkBv(5.toByte()), model.eval(selected)) + } + + @Test + fun detachModelOfEqualTwoIndexArraysOverUninterpretedSort(): Unit = with(ctx) { + val address = mkUninterpretedSort("Address") + val sort = mkArraySort(address, bv32Sort, bv8Sort) + val array = mkConst("input", sort) + val other = mkConst("other", sort) + + solver.assert(array eq other) + assertEquals(KSolverStatus.SAT, solver.check()) + + val model = solver.model().detach() + assertEquals(model.eval(array), model.eval(other)) + } + + @Test + fun detachModelOfStoredTwoIndexArrayOverUninterpretedSort(): Unit = with(ctx) { + val address = mkUninterpretedSort("Address") + val sort = mkArraySort(address, bv32Sort, bv8Sort) + val array = mkConst("input", sort) + val other = mkConst("other", sort) + val a = mkConst("a", address) + val i = mkConst("i", bv32Sort) + + solver.assert(array eq other.store(a, i, mkBv(7.toByte()))) + assertEquals(KSolverStatus.SAT, solver.check()) + + val model = solver.model().detach() + assertEquals(mkBv(7.toByte()), model.eval(array.select(a, i))) + } +}