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/bitwuzla-linux64-1.0.zip b/ksmt-bitwuzla/dist/bitwuzla-linux64-1.0.zip index 527615c62..f5705840c 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.md b/ksmt-bitwuzla/dist/build.md index 5be38b43d..1020842a0 100644 --- a/ksmt-bitwuzla/dist/build.md +++ b/ksmt-bitwuzla/dist/build.md @@ -8,6 +8,22 @@ To make our distribution portable we statically link Bitwuzla against `libgmp`. Jni bindings `bitwuzla_jni` are built without any tricks. +### Linux x64 library from the Bitwuzla fork + +`libbitwuzla.so` in `bitwuzla-linux64-1.0.zip` is the release `1.0-ksmt.1` of the fork https://github.com/metametamoon/bitwuzla, built from its branch `c-api-1.0`. +That branch starts at Bitwuzla commit `1230d80a5275ddf525da9c218c2bcd29c3130e49`, the commit of the original binary, and adds fixes for lambdas reached through array updates in beta reduction and model generation, with tests. +The fork's `contrib/ksmt/build-linux64.sh` builds the library in Docker, with GMP, libstdc++ and libgcc linked statically, and its release workflow attaches the library to the tag's GitHub release. + +`fetch-linux64.sh` downloads the library of a release, checks its sha256 and that it defines every `bzla_*` and `bitwuzla_*` symbol the unchanged `libbitwuzla_jni.so` imports, and repacks the zip. + +```shell +./fetch-linux64.sh 1.0-ksmt.1 +``` + +`libbitwuzla_jni.so` in the zip is still the original binary. +The library of `1.0-ksmt.1` has sha256 `51d57475e5e19286496f48da6f62acb59d164c26c373c6b30707461532fdce49`. +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/dist/fetch-linux64.sh b/ksmt-bitwuzla/dist/fetch-linux64.sh new file mode 100755 index 000000000..aedd9de51 --- /dev/null +++ b/ksmt-bitwuzla/dist/fetch-linux64.sh @@ -0,0 +1,42 @@ +#!/usr/bin/env bash +set -euo pipefail + +tag=${1:?usage: fetch-linux64.sh } +here=$(cd "$(dirname "$(readlink -f "$0")")" && pwd) +url="https://github.com/metametamoon/bitwuzla/releases/download/$tag" +work=$(mktemp -d) +trap 'rm -rf "$work"' EXIT + +curl -fsSL -o "$work/libbitwuzla.so" "$url/libbitwuzla.so" +curl -fsSL -o "$work/libbitwuzla.so.sha256" "$url/libbitwuzla.so.sha256" +(cd "$work" && sha256sum -c --quiet libbitwuzla.so.sha256) + +python3 - "$here/bitwuzla-linux64-1.0.zip" "$work" <<'PY' +import sys, zipfile +with zipfile.ZipFile(sys.argv[1]) as z: + z.extract("libbitwuzla_jni.so", sys.argv[2]) +PY + +nm -D --undefined-only "$work/libbitwuzla_jni.so" | awk '{ print $NF }' | grep -E '^(bzla|bitwuzla)_' | sort -u > "$work/needed" +nm -D --defined-only "$work/libbitwuzla.so" | awk '{ print $NF }' | sort -u > "$work/defined" +missing=$(comm -23 "$work/needed" "$work/defined") +if [ -n "$missing" ]; then + echo "libbitwuzla.so lacks symbols that libbitwuzla_jni.so imports:" >&2 + echo "$missing" >&2 + exit 1 +fi + +python3 - "$work" "$here/bitwuzla-linux64-1.0.zip" <<'PY' +import os, sys, zipfile +work, target = sys.argv[1], sys.argv[2] +with zipfile.ZipFile(target + ".new", "w", zipfile.ZIP_DEFLATED) as z: + for name in ("libbitwuzla.so", "libbitwuzla_jni.so"): + info = zipfile.ZipInfo(name, date_time=(1980, 1, 1, 0, 0, 0)) + info.external_attr = 0o755 << 16 + info.compress_type = zipfile.ZIP_DEFLATED + with open(os.path.join(work, name), "rb") as f: + z.writestr(info, f.read()) +os.replace(target + ".new", target) +PY + +cut -d' ' -f1 "$work/libbitwuzla.so.sha256" 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))) + } +}