Various fixes (#162)

* Various fixes * Rebuild z3-linux-x64 * Rollback cvc bv-reduction and/or fix as incorrect * Upgrade version to 0.5.25
UnitTestBot · Aug 16, 2024 · fdd016d · fdd016d
1 parent e294ff4
commit fdd016d
Show file tree

Hide file tree

Showing 12 changed files with 55 additions and 23 deletions.
diff --git 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.5.24)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.25)
 [![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.5.24")
+implementation("io.ksmt:ksmt-core:0.5.25")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.24")
+implementation("io.ksmt:ksmt-z3:0.5.25")
 ```
 
 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
@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.24"
+version = "0.5.25"
 
 repositories {
     mavenCentral()

diff --git a/docs/getting-started.md b/docs/getting-started.md
@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.24")    
+    implementation("io.ksmt:ksmt-core:0.5.25")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.24")
+    implementation("io.ksmt:ksmt-z3:0.5.25")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.24")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.25")
 }
 ```
 

diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.24")
+    implementation("io.ksmt:ksmt-core:0.5.25")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.24")
+    implementation("io.ksmt:ksmt-z3:0.5.25")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.24")
+    implementation("io.ksmt:ksmt-runner:0.5.25")
 }
 
 java {

diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvSimplificationRules.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvSimplificationRules.kt
@@ -12,6 +12,7 @@ import io.ksmt.expr.KBvNotExpr
 import io.ksmt.expr.KBvOrExpr
 import io.ksmt.expr.KBvShiftLeftExpr
 import io.ksmt.expr.KBvXorExpr
+import io.ksmt.expr.KBvZeroExtensionExpr
 import io.ksmt.expr.KExpr
 import io.ksmt.expr.KIteExpr
 import io.ksmt.sort.KBoolSort
@@ -826,15 +827,22 @@ inline fun <T : KBvSort> KContext.simplifyBvLogicalShiftRightExprLight(
     shift: KExpr<T>,
     cont: (KExpr<T>, KExpr<T>) -> KExpr<T>
 ): KExpr<T> {
+    val sizeBits = shift.sort.sizeBits
+
     if (shift is KBitVecValue<T>) {
         // (x >>> 0) ==> x
         if (shift.isBvZero()) {
             return lhs
         }
 
         // (x >>> shift), shift >= size ==> 0
-        if (shift.signedGreaterOrEqual(shift.sort.sizeBits.toInt())) {
-            return bvZero(shift.sort.sizeBits)
+        if (shift.signedGreaterOrEqual(sizeBits.toInt())) {
+            return bvZero(sizeBits)
+        }
+
+        // ((zero-ext x E) >>> shift), shift >= sizeOf(x) ==> 0
+        if (lhs is KBvZeroExtensionExpr && shift.signedGreaterOrEqual(lhs.value.sort.sizeBits.toInt())) {
+            return bvZero(sizeBits)
         }
 
         if (lhs is KBitVecValue<T>) {
@@ -844,7 +852,7 @@ inline fun <T : KBvSort> KContext.simplifyBvLogicalShiftRightExprLight(
 
     // (x >>> x) ==> 0
     if (lhs == shift) {
-        return bvZero(shift.sort.sizeBits)
+        return bvZero(sizeBits)
     }
 
     return cont(lhs, shift)

diff --git a/ksmt-core/src/test/kotlin/io/ksmt/BvSimplifyTest.kt b/ksmt-core/src/test/kotlin/io/ksmt/BvSimplifyTest.kt
@@ -121,6 +121,7 @@ class BvSimplifyTest: ExpressionSimplifyTest() {
                 bvValue(it.sizeBits, 3),
                 bvValue(it.sizeBits, BV_SIZE.toInt() + 5),
                 bvZero(it.sizeBits),
+                mkBvZeroExtensionExpr((it.sizeBits.toInt() - 3).coerceAtLeast(0), mkConst("b", mkBvSort(3u))),
                 mkConst("a", it)  // same as lhs
             )
         }

diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt
@@ -1215,11 +1215,17 @@ class KCvc5ExprInternalizer(
     private fun Term.mkFunctionApp(args: List<Term>): Term =
         tm.mkTerm(Kind.APPLY_UF, arrayOf(this) + args)
 
-    private fun mkAndTerm(args: List<Term>): Term =
-        if (args.size == 1) args.single() else tm.mkTerm(Kind.AND, args.toTypedArray())
+    private fun mkAndTerm(args: List<Term>): Term = when (args.size) {
+        0 -> tm.builder { mkTrue() }
+        1 -> args.single()
+        else -> tm.mkTerm(Kind.AND, args.toTypedArray())
+    }
 
-    private fun mkOrTerm(args: List<Term>): Term =
-        if (args.size == 1) args.single() else tm.mkTerm(Kind.OR, args.toTypedArray())
+    private fun mkOrTerm(args: List<Term>): Term = when (args.size) {
+        0 -> tm.builder { mkFalse() }
+        1 -> args.single()
+        else -> tm.mkTerm(Kind.OR, args.toTypedArray())
+    }
 
     private fun mkArraySelectTerm(array: Term, indices: List<Term>): Term =
         if (tm.termSort(array).isArray) {

diff --git a/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt b/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt
@@ -91,8 +91,14 @@ class TestWorkerProcess : ChildProcessBase<TestProtocolModel>() {
     }
 
     private fun convertAssertions(nativeAssertions: List<Long>): List<KExpr<KBoolSort>> {
-        val converter = KZ3ExprConverter(ctx, KZ3Context(ctx, z3Ctx))
-        return with(converter) { nativeAssertions.map { it.convertExpr() } }
+        val context = KZ3Context(ctx, z3Ctx)
+        return try {
+            val converter = KZ3ExprConverter(ctx, context)
+            with(converter) { nativeAssertions.map { it.convertExpr() } }
+        } finally {
+            // Don't close native context, only release native refs
+            context.releaseNativeMemory()
+        }
     }
 
     private fun internalizeAndConvertBitwuzla(assertions: List<KExpr<KBoolSort>>): List<KExpr<KBoolSort>> =

diff --git a/ksmt-z3/dist/z3-native-linux-x86-64-4.13.0.zip b/ksmt-z3/dist/z3-native-linux-x86-64-4.13.0.zip
diff --git a/...z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/ExpressionUninterpretedValuesTracker.kt b/...z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/ExpressionUninterpretedValuesTracker.kt
@@ -214,6 +214,13 @@ class ExpressionUninterpretedValuesTracker(val ctx: KContext, val z3Ctx: KZ3Cont
             }
         }
 
+        fun containsExpressionOnCurrentLevel(expr: KExpr<*>): Boolean {
+            // Was not initialized --> has no expressions
+            if (!initialized) return false
+
+            return expr in currentLevelExpressions
+        }
+
         fun addRegisteredValueToCurrentLevel(value: KUninterpretedSortValue) {
             val descriptor = tracker.registeredUninterpretedSortValues[value]
                 ?: error("Value $value was not registered")
@@ -250,7 +257,7 @@ class ExpressionUninterpretedValuesTracker(val ctx: KContext, val z3Ctx: KZ3Cont
             if (frameLevel < level) {
                 val levelFrame = getFrame(frameLevel)
                 // If expr is valid on its level we don't need to move it
-                return expr !in levelFrame.currentLevelExpressions
+                return !levelFrame.containsExpressionOnCurrentLevel(expr)
             }
             return super.exprTransformationRequired(expr)
         }

diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt
@@ -264,6 +264,12 @@ class KZ3Context(
         if (isClosed) return
         isClosed = true
 
+        releaseNativeMemory()
+
+        ctx.close()
+    }
+
+    fun releaseNativeMemory() {
         uninterpretedSortValueInterpreter.clear()
 
         uninterpretedSortValueDecls.keys.decRefAll()
@@ -289,8 +295,6 @@ class KZ3Context(
         z3Sorts.keys.decRefAll()
         sorts.clear()
         z3Sorts.clear()
-
-        ctx.close()
     }
 
     private fun LongSet.decRefAll() =

diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts
@@ -27,7 +27,7 @@ val macDylibPath = listOf("**/libz3.dylib", "**/libz3java.dylib")
 
 val z3Binaries = listOf(
     Triple(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", winDllPath), null),
-    Triple(`linux-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-glibc-2.31", linuxSoPath), null),
+    Triple(`linux-x64`, null, z3NativeLinuxX64),
     Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-11.7.10", macDylibPath), null),
     Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", macDylibPath), null),
     Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.35", linuxSoPath), null),