Skip to content

Commit 88927a9

Browse files
CaelmBleiddCaelmBleidd
authored
Replace z3 jar files with KSMT dependency (#1941)
1 parent e3e6428 commit 88927a9

File tree

20 files changed

+173
-189
lines changed

20 files changed

+173
-189
lines changed

‎build.gradle.kts

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,7 @@ allprojects {
132132

133133
repositories {
134134
mavenCentral()
135+
maven("https://jitpack.io")
135136
maven("https://s01.oss.sonatype.org/content/repositories/orgunittestbotsoot-1004/")
136137
maven("https://plugins.gradle.org/m2")
137138
maven("https://www.jetbrains.com/intellij-repository/releases")

‎gradle.properties

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,7 @@ junit5Version=5.8.0-RC1
2626
junit4Version=4.13.2
2727
junit4PlatformVersion=1.9.0
2828
mockitoVersion=3.5.13
29-
z3Version=4.8.9.1
30-
z3JavaApiVersion=4.8.9
29+
ksmtVersion=0.4.3
3130
sootVersion=4.4.0-FORK-2
3231
kotlinVersion=1.8.0
3332
log4j2Version=2.13.3
@@ -63,7 +62,6 @@ testNgVersion=7.6.0
6362
mockitoInlineVersion=4.0.0
6463
kamlVersion = 0.51.0
6564
jacksonVersion = 2.12.3
66-
javasmtSolverZ3Version=4.8.9-sosy1
6765
slf4jVersion=1.7.36
6866
eclipseAetherVersion=1.1.0
6967
mavenWagonVersion=3.5.1

‎utbot-framework-test/build.gradle

Lines changed: 2 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -10,16 +10,6 @@ tasks.withType(JavaCompile) {
1010
targetCompatibility = JavaVersion.VERSION_17
1111
}
1212

13-
repositories {
14-
flatDir {
15-
dirs 'dist'
16-
}
17-
}
18-
19-
configurations {
20-
z3native
21-
}
22-
2313
dependencies {
2414
api project(':utbot-framework-api')
2515
testImplementation project(':utbot-testing')
@@ -39,7 +29,6 @@ dependencies {
3929

4030
implementation group: 'com.charleskorn.kaml', name: 'kaml', version: kamlVersion
4131
implementation group: 'com.fasterxml.jackson.module', name: 'jackson-module-kotlin', version: jacksonVersion
42-
implementation group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: javasmtSolverZ3Version
4332
implementation group: 'com.github.curious-odd-man', name: 'rgxgen', version: rgxgenVersion
4433
implementation group: 'org.apache.logging.log4j', name: 'log4j-slf4j-impl', version: log4j2Version
4534
implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlinLoggingVersion
@@ -66,12 +55,10 @@ dependencies {
6655
testImplementation group: 'org.mockito', name: 'mockito-inline', version: mockitoInlineVersion
6756
testImplementation group: 'org.apache.logging.log4j', name: 'log4j-core', version: log4j2Version
6857

69-
z3native group: 'com.microsoft.z3', name: 'z3-native-win64', version: z3Version, ext: 'zip'
70-
z3native group: 'com.microsoft.z3', name: 'z3-native-linux64', version: z3Version, ext: 'zip'
71-
z3native group: 'com.microsoft.z3', name: 'z3-native-osx', version: z3Version, ext: 'zip'
58+
implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-core', version: ksmtVersion
59+
implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-z3', version: ksmtVersion
7260
}
7361

74-
7562
test {
7663
if (System.getProperty('DEBUG', 'false') == 'true') {
7764
jvmArgs '-Xdebug', '-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=9009'

‎utbot-framework-test/src/test/kotlin/org/utbot/examples/math/OverflowAsErrorTest.kt

Lines changed: 16 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import org.utbot.framework.plugin.api.CodegenLanguage
88
import org.utbot.testcheckers.eq
99
import org.utbot.testcheckers.withSolverTimeoutInMillis
1010
import org.utbot.testcheckers.withTreatingOverflowAsError
11-
import org.utbot.testing.AtLeast
11+
import org.utbot.testing.DoNotCalculate
1212
import org.utbot.testing.Compilation
1313
import org.utbot.testing.UtValueTestCaseChecker
1414
import org.utbot.testing.ignoreExecutionsNumber
@@ -32,12 +32,23 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
3232
checkWithException(
3333
OverflowExamples::intOverflow,
3434
eq(5),
35-
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow
36-
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow (2nd '*')
35+
{ x, _, r ->
36+
val overflowOccurred = kotlin.runCatching {
37+
Math.multiplyExact(x, x)
38+
}.isFailure
39+
overflowOccurred && r.isException<OverflowDetectionError>()
40+
}, // through overflow
41+
{ x, _, r ->
42+
val twoMul = Math.multiplyExact(x, x)
43+
val overflowOccurred = kotlin.runCatching {
44+
Math.multiplyExact(twoMul, x)
45+
}.isFailure
46+
overflowOccurred && r.isException<OverflowDetectionError>()
47+
}, // through overflow (2nd '*')
3748
{ x, _, r -> x * x * x >= 0 && x >= 0 && r.getOrNull() == 0 },
3849
{ x, y, r -> x * x * x > 0 && x > 0 && y == 10 && r.getOrNull() == 1 },
3950
{ x, y, r -> x * x * x > 0 && x > 0 && y != 10 && r.getOrNull() == 0 },
40-
coverage = AtLeast(90),
51+
coverage = DoNotCalculate
4152
)
4253
}
4354
}
@@ -258,7 +269,7 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
258269
}
259270
}
260271

261-
// Generated Kotlin code does not compile, so disabled for now
272+
// Generated Kotlin code does not compile, so disabled for now
262273
@Test
263274
@Disabled
264275
fun testQuickSort() {

‎utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionForTests.kt

Lines changed: 29 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -5,19 +5,19 @@ package com.microsoft.z3
55
import kotlin.reflect.KProperty
66

77

8-
operator fun ArithExpr.plus(other: ArithExpr): ArithExpr = context.mkAdd(this, other)
9-
operator fun ArithExpr.plus(other: Int): ArithExpr = this + context.mkInt(other)
8+
operator fun ArithExpr<*>.plus(other: ArithExpr<*>): ArithExpr<*> = context.mkAdd(this, other)
9+
operator fun ArithExpr<*>.plus(other: Int): ArithExpr<*> = this + context.mkInt(other)
1010

11-
operator fun ArithExpr.minus(other: ArithExpr): ArithExpr = context.mkSub(this, other)
12-
operator fun ArithExpr.minus(other: Int): ArithExpr = this - context.mkInt(other)
11+
operator fun ArithExpr<*>.minus(other: ArithExpr<*>): ArithExpr<*> = context.mkSub(this, other)
12+
operator fun ArithExpr<*>.minus(other: Int): ArithExpr<*> = this - context.mkInt(other)
1313

14-
operator fun ArithExpr.times(other: ArithExpr): ArithExpr = context.mkMul(this, other)
15-
operator fun ArithExpr.times(other: Int): ArithExpr = this * context.mkInt(other)
14+
operator fun ArithExpr<*>.times(other: ArithExpr<*>): ArithExpr<*> = context.mkMul(this, other)
15+
operator fun ArithExpr<*>.times(other: Int): ArithExpr<*> = this * context.mkInt(other)
1616

17-
infix fun Expr.`=`(other: Int): BoolExpr = this eq context.mkInt(other)
18-
infix fun Expr.`=`(other: Expr): BoolExpr = this eq other
19-
infix fun Expr.eq(other: Expr): BoolExpr = context.mkEq(this, other)
20-
infix fun Expr.`!=`(other: Expr): BoolExpr = context.mkNot(this `=` other)
17+
infix fun Expr<*>.`=`(other: Int): BoolExpr = this eq context.mkInt(other)
18+
infix fun Expr<*>.`=`(other: Expr<*>): BoolExpr = this eq other
19+
infix fun Expr<*>.eq(other: Expr<*>): BoolExpr = context.mkEq(this, other)
20+
infix fun Expr<*>.`!=`(other: Expr<*>): BoolExpr = context.mkNot(this `=` other)
2121
operator fun BoolExpr.not(): BoolExpr = context.mkNot(this)
2222

2323
infix fun BoolExpr.`⇒`(other: BoolExpr): BoolExpr = this implies other
@@ -27,20 +27,24 @@ infix fun BoolExpr.implies(other: BoolExpr): BoolExpr = context.mkImplies(this,
2727
infix fun BoolExpr.and(other: BoolExpr): BoolExpr = context.mkAnd(this, other)
2828
infix fun BoolExpr.or(other: BoolExpr): BoolExpr = context.mkOr(this, other)
2929

30-
infix fun ArithExpr.gt(other: ArithExpr): BoolExpr = context.mkGt(this, other)
31-
infix fun ArithExpr.gt(other: Int): BoolExpr = context.mkGt(this, context.mkInt(other))
30+
infix fun ArithExpr<*>.gt(other: ArithExpr<*>): BoolExpr = context.mkGt(this, other)
31+
infix fun ArithExpr<*>.gt(other: Int): BoolExpr = context.mkGt(this, context.mkInt(other))
3232

33-
infix fun ArithExpr.`=`(other: Int): BoolExpr = context.mkEq(this, context.mkInt(other))
33+
infix fun ArithExpr<*>.`=`(other: Int): BoolExpr = context.mkEq(this, context.mkInt(other))
3434

35-
operator fun ArrayExpr.get(index: IntExpr): Expr = context.mkSelect(this, index)
36-
operator fun ArrayExpr.get(index: Int): Expr = this[context.mkInt(index)]
37-
fun ArrayExpr.set(index: IntExpr, value: Expr): ArrayExpr = context.mkStore(this, index, value)
38-
fun ArrayExpr.set(index: Int, value: Expr): ArrayExpr = set(context.mkInt(index), value)
35+
operator fun ArrayExpr<*, *>.get(index: IntExpr): Expr<*> = context.mkSelect(this, index.cast())
36+
operator fun ArrayExpr<*, *>.get(index: Int): Expr<*> = this[context.mkInt(index)]
37+
fun ArrayExpr<*, *>.set(index: IntExpr, value: Expr<*>): ArrayExpr<*, *> = context.mkStore(this, index.cast(), value.cast())
38+
fun ArrayExpr<*, *>.set(index: Int, value: Expr<*>): ArrayExpr<*, *> = set(context.mkInt(index), value)
3939

40-
operator fun SeqExpr.plus(other: SeqExpr): SeqExpr = context.mkConcat(this, other)
41-
operator fun SeqExpr.plus(other: String): SeqExpr = context.mkConcat(context.mkString(other))
40+
operator fun SeqExpr<*>.plus(other: SeqExpr<*>): SeqExpr<*> = context.mkConcat(this, other.cast())
41+
operator fun SeqExpr<*>.plus(other: String): SeqExpr<*> = context.mkConcat(context.mkString(other))
4242

43-
infix fun SeqExpr.`=`(other: String): BoolExpr = context.mkEq(this, context.mkString(other))
43+
@Suppress("UNCHECKED_CAST")
44+
fun <T : Sort, R : Sort> Expr<T>.cast(): Expr<R> = this as Expr<R>
45+
46+
47+
infix fun SeqExpr<*>.`=`(other: String): BoolExpr = context.mkEq(this, context.mkString(other))
4448

4549
class Const<T>(private val ctx: Context, val produce: (Context, name: String) -> T) {
4650
operator fun getValue(thisRef: Nothing?, property: KProperty<*>): T = produce(ctx, property.name)
@@ -49,12 +53,12 @@ class Const<T>(private val ctx: Context, val produce: (Context, name: String) ->
4953
fun Context.declareInt() = Const(this) { ctx, name -> ctx.mkIntConst(name) }
5054
fun Context.declareBool() = Const(this) { ctx, name -> ctx.mkBoolConst(name) }
5155
fun Context.declareReal() = Const(this) { ctx, name -> ctx.mkRealConst(name) }
52-
fun Context.declareString() = Const(this) { ctx, name -> ctx.mkConst(name, stringSort) as SeqExpr }
53-
fun Context.declareList(sort: ListSort) = Const(this) { ctx, name -> ctx.mkConst(name, sort) }
56+
fun Context.declareString() = Const(this) { ctx, name -> ctx.mkConst(name, stringSort) as SeqExpr<*> }
57+
fun Context.declareList(sort: ListSort<*>) = Const(this) { ctx, name -> ctx.mkConst(name, sort) }
5458
fun Context.declareIntArray() = Const(this) { ctx, name -> ctx.mkArrayConst(name, intSort, intSort) }
5559

5660

57-
operator fun FuncDecl.invoke(vararg expr: Expr): Expr = context.mkApp(this, *expr)
61+
operator fun FuncDecl<*>.invoke(vararg expr: Expr<*>): Expr<*> = context.mkApp(this, *expr)
5862

59-
fun Model.eval(expr: Expr): Expr = this.eval(expr, true)
60-
fun Model.eval(vararg exprs: Expr): List<Expr> = exprs.map { this.eval(it, true) }
63+
fun Model.eval(expr: Expr<*>): Expr<*> = this.eval(expr, true)
64+
fun Model.eval(vararg exprs: Expr<*>): List<Expr<*>> = exprs.map { this.eval(it, true) }

‎utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionTest.kt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -99,8 +99,8 @@ class Z3ExtensionTest : Z3Initializer() {
9999

100100
val (aVal, bVal, cVal) = solver.model
101101
.eval(a, b, c)
102-
.filterIsInstance<SeqExpr>()
103-
.map(SeqExpr::getString)
102+
.filterIsInstance<SeqExpr<*>>()
103+
.map(SeqExpr<*>::getString)
104104
.also { list -> assertEquals(3, list.size) }
105105

106106
assertEquals("abcd", "$aVal$bVal")

‎utbot-framework/build.gradle

Lines changed: 2 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,3 @@
1-
repositories {
2-
flatDir {
3-
dirs 'dist'
4-
}
5-
}
6-
7-
configurations {
8-
z3native
9-
}
10-
111
dependencies {
122

133
api project(':utbot-fuzzers')
@@ -29,7 +19,6 @@ dependencies {
2919

3020
implementation group: 'com.charleskorn.kaml', name: 'kaml', version: kamlVersion
3121
implementation group: 'com.fasterxml.jackson.module', name: 'jackson-module-kotlin', version: jacksonVersion
32-
implementation group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: javasmtSolverZ3Version
3322
implementation group: 'com.github.curious-odd-man', name: 'rgxgen', version: rgxgenVersion
3423
implementation group: 'org.apache.logging.log4j', name: 'log4j-slf4j-impl', version: log4j2Version
3524
implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlinLoggingVersion
@@ -43,15 +32,6 @@ dependencies {
4332
implementation group: 'org.junit.jupiter', name: 'junit-jupiter-params', version: '5.8.1'
4433
implementation group: 'org.junit.jupiter', name: 'junit-jupiter-engine', version: '5.8.1'
4534

46-
z3native group: 'com.microsoft.z3', name: 'z3-native-win64', version: z3Version, ext: 'zip'
47-
z3native group: 'com.microsoft.z3', name: 'z3-native-linux64', version: z3Version, ext: 'zip'
48-
z3native group: 'com.microsoft.z3', name: 'z3-native-osx', version: z3Version, ext: 'zip'
49-
}
50-
51-
processResources {
52-
configurations.z3native.resolvedConfiguration.resolvedArtifacts.each { artifact ->
53-
from(zipTree(artifact.getFile())) {
54-
into "lib/x64"
55-
}
56-
}
35+
implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-core', version: ksmtVersion
36+
implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-z3', version: ksmtVersion
5737
}

‎utbot-framework/dist/z3-native-linux64-4.8.9.1.zip

-10.3 MB
Binary file not shown.

‎utbot-framework/dist/z3-native-osx-4.8.9.1.zip

-18 MB
Binary file not shown.

‎utbot-framework/dist/z3-native-win64-4.8.9.1.zip

-6.27 MB
Binary file not shown.

‎utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -932,7 +932,7 @@ data class UtMkTermArrayExpression(val array: UtArrayExpressionBase, val default
932932
override fun hashCode() = hashCode
933933
}
934934

935-
data class Z3Variable(val type: Type, val expr: Expr) {
935+
data class Z3Variable(val type: Type, val expr: Expr<*>) {
936936
private val hashCode = Objects.hash(type, expr)
937937

938938
override fun equals(other: Any?): Boolean {
@@ -950,6 +950,6 @@ data class Z3Variable(val type: Type, val expr: Expr) {
950950
override fun hashCode() = hashCode
951951
}
952952

953-
fun Expr.z3Variable(type: Type) = Z3Variable(type, this)
953+
fun Expr<*>.z3Variable(type: Type) = Z3Variable(type, this)
954954

955955
fun UtExpression.isInteger() = this.sort is UtBvSort

‎utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ class UtSolverStatusSAT(
4747

4848
private val evaluator: Z3EvaluatorVisitor = translator.evaluator(model)
4949

50-
fun eval(expression: UtExpression): Expr = evaluator.eval(expression)
50+
fun eval(expression: UtExpression): Expr<*> = evaluator.eval(expression)
5151

5252
fun concreteAddr(expression: UtAddrExpression): Address = eval(expression).intValue()
5353

@@ -65,7 +65,7 @@ class UtSolverStatusSAT(
6565
* - val arrayInterpretationFuncDecl: FuncDecl = mfd.parameters[[0]].funcDecl
6666
* - val interpretation: FuncInterp = z3Solver.model.getFuncInterp(arrayInterpretationFuncDecl)
6767
*/
68-
internal fun evalArrayDescriptor(mval: Expr, unsigned: Boolean, filter: (Int) -> Boolean): ArrayDescriptor {
68+
internal fun evalArrayDescriptor(mval: Expr<*>, unsigned: Boolean, filter: (Int) -> Boolean): ArrayDescriptor {
6969
var next = mval
7070
val stores = mutableMapOf<Int, Any>()
7171
var const: Any? = null
@@ -79,7 +79,7 @@ class UtSolverStatusSAT(
7979
next = next.args[0]
8080
}
8181
Z3_OP_UNINTERPRETED -> next = model.eval(next)
82-
Z3_OP_CONST_ARRAY -> const = if (next.args[0] is ArrayExpr) {
82+
Z3_OP_CONST_ARRAY -> const = if (next.args[0] is ArrayExpr<*, *>) {
8383
// if we have an array as const value, create a corresponding descriptor for it
8484
evalArrayDescriptor(next.args[0], unsigned, filter)
8585
} else {

‎utbot-framework/src/main/kotlin/org/utbot/engine/pc/Util.kt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
package org.utbot.engine.pc
2+
3+
import com.microsoft.z3.Expr
4+
import com.microsoft.z3.Sort
5+
6+
@Suppress("UNCHECKED_CAST")
7+
fun <T : Sort, R : Sort> Expr<T>.cast(): Expr<R> = this as Expr<R>

0 commit comments

Comments
 (0)