Skip to content

Commit 7cba5a5

Browse files
DamtevDamtev
committed
WIP numeric fixes, solver factory
1 parent 0142583 commit 7cba5a5

File tree

9 files changed

+112
-30
lines changed

9 files changed

+112
-30
lines changed

‎usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -925,18 +925,20 @@ class UNumericConstraints<Sort : UBvSort> private constructor(
925925
bias: KBitVecValue<Sort>,
926926
bound: KBitVecValue<Sort>,
927927
): BoundsConstraint<Sort> {
928-
val currentValue = concreteLowerBounds[bias]?.value
929-
if (currentValue != null && currentValue.signedGreaterOrEqual(bound)) return this
930-
return modifyConcreteLowerBounds(bias, ValueConstraint(bound, isPrimary = false))
928+
val current = concreteLowerBounds[bias]
929+
if (current != null && current.value.signedGreaterOrEqual(bound)) return this
930+
val isPrimary = current?.isPrimary ?: false
931+
return modifyConcreteLowerBounds(bias, ValueConstraint(bound, isPrimary))
931932
}
932933

933934
private fun BoundsConstraint<Sort>.refineUpperBound(
934935
bias: KBitVecValue<Sort>,
935936
bound: KBitVecValue<Sort>,
936937
): BoundsConstraint<Sort> {
937-
val currentValue = concreteUpperBounds[bias]?.value
938-
if (currentValue != null && currentValue.signedLessOrEqual(bound)) return this
939-
return modifyConcreteUpperBounds(bias, ValueConstraint(bound, isPrimary = false))
938+
val current = concreteUpperBounds[bias]
939+
if (current != null && current.value.signedLessOrEqual(bound)) return this
940+
val isPrimary = current?.isPrimary ?: false
941+
return modifyConcreteUpperBounds(bias, ValueConstraint(bound, isPrimary))
940942
}
941943

942944
private fun BoundsConstraint<Sort>.updateConcreteLowerBound(

‎usvm-core/src/test/kotlin/org/usvm/constraints/NumericConstraintsTests.kt

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,25 @@ class NumericConstraintsTests {
9898
solver.checkConstraints(0)
9999
}
100100

101+
@Test
102+
fun testConcreteBoundsSimplification(): Unit = with(ctx) {
103+
KZ3Solver(ctx).use { solver ->
104+
bvSort = ctx.mkBvSort(sizeBits = 4u)
105+
constraints = UNumericConstraints(ctx, bvSort)
106+
val x by bvSort
107+
108+
val zero = mkBv(0, bvSort)
109+
val four = mkBv(4, bvSort)
110+
val xMinusOne = mkBvAddExpr(x, mkBv(-1, bvSort))
111+
112+
addConstraint(mkBvSignedLessOrEqualExpr(zero, x))
113+
addConstraint(mkBvSignedLessOrEqualExpr(x, four))
114+
addConstraint(mkBvSignedLessOrEqualExpr(zero, xMinusOne))
115+
116+
solver.checkConstraints(0)
117+
}
118+
}
119+
101120
@Test
102121
fun testEvalInterval(): Unit = with(ctx) {
103122
bvSort = ctx.mkBvSort(sizeBits = 32u)

‎usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt

Lines changed: 56 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
package org.usvm.machine
22

33
import io.ksmt.KContext
4+
import io.ksmt.solver.KSolver
5+
import io.ksmt.solver.KSolverConfiguration
46
import io.ksmt.solver.runner.KSolverRunnerManager
57
import io.ksmt.solver.yices.KYicesSolver
68
import io.ksmt.solver.yices.KYicesSolverConfiguration
@@ -18,33 +20,27 @@ import org.usvm.solver.UTypeSolver
1820

1921
class JcComponents(
2022
private val typeSystem: JcTypeSystem,
23+
// TODO group all parameters below to the one class
2124
private val solverType: SolverType,
2225
override val useSolverForForks: Boolean,
26+
private val runSolverInAnotherProcess: Boolean,
2327
) : UComponents<JcType, USizeSort> {
2428
private val closeableResources = mutableListOf<AutoCloseable>()
25-
private val solverManager: KSolverRunnerManager = KSolverRunnerManager()
26-
27-
init {
28-
solverManager.registerSolver(YicesWithSymFpu::class, KYicesSolverUniversalConfiguration::class)
29-
}
3029

3130
override fun <Context : UContext<USizeSort>> mkSolver(ctx: Context): USolverBase<JcType> {
3231
val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx)
3332

34-
val smtSolver = when (solverType) {
35-
// Yices with Fp support via SymFpu
36-
SolverType.YICES -> solverManager.createSolver(ctx, YicesWithSymFpu::class)
37-
SolverType.Z3 -> solverManager.createSolver(ctx, KZ3Solver::class)
38-
}
33+
val solverFactory = SolverFactory.mkFactory(runSolverInAnotherProcess)
34+
val smtSolver = solverFactory.mkSolver(ctx, solverType)
3935
val typeSolver = UTypeSolver(typeSystem)
4036
closeableResources += smtSolver
37+
closeableResources += solverFactory
4138

4239
return USolverBase(ctx, smtSolver, typeSolver, translator, decoder)
4340
}
4441

4542
fun close() {
4643
closeableResources.forEach(AutoCloseable::close)
47-
solverManager.close()
4844
}
4945

5046
override fun mkTypeSystem(ctx: UContext<USizeSort>): JcTypeSystem {
@@ -54,5 +50,54 @@ class JcComponents(
5450
override fun <Context : UContext<USizeSort>> mkSizeExprProvider(ctx: Context): USizeExprProvider<USizeSort> =
5551
UBv32SizeExprProvider(ctx)
5652

53+
}
54+
55+
interface SolverFactory : AutoCloseable {
56+
fun <Context : UContext<USizeSort>> mkSolver(
57+
ctx: Context,
58+
solverType: SolverType
59+
): KSolver<out KSolverConfiguration>
60+
61+
companion object {
62+
fun mkFactory(runSolverInAnotherProcess: Boolean): SolverFactory =
63+
if (runSolverInAnotherProcess) AnotherProcessSolverFactory() else SameProcessSolverFactory
64+
}
65+
}
66+
67+
private object SameProcessSolverFactory : SolverFactory {
68+
override fun <Context : UContext<USizeSort>> mkSolver(
69+
ctx: Context,
70+
solverType: SolverType
71+
): KSolver<out KSolverConfiguration> = when (solverType) {
72+
// Yices with Fp support via SymFpu
73+
SolverType.YICES -> KSymFpuSolver(KYicesSolver(ctx), ctx)
74+
SolverType.Z3 -> KZ3Solver(ctx)
75+
}
76+
77+
override fun close() {
78+
// Do nothing
79+
}
80+
}
81+
82+
private class AnotherProcessSolverFactory : SolverFactory {
83+
private val solverManager: KSolverRunnerManager = KSolverRunnerManager()
84+
85+
init {
86+
solverManager.registerSolver(YicesWithSymFpu::class, KYicesSolverUniversalConfiguration::class)
87+
}
88+
89+
override fun <Context : UContext<USizeSort>> mkSolver(
90+
ctx: Context,
91+
solverType: SolverType
92+
): KSolver<out KSolverConfiguration> = when (solverType) {
93+
// Yices with Fp support via SymFpu
94+
SolverType.YICES -> solverManager.createSolver(ctx, YicesWithSymFpu::class)
95+
SolverType.Z3 -> solverManager.createSolver(ctx, KZ3Solver::class)
96+
}
97+
98+
override fun close() {
99+
solverManager.close()
100+
}
101+
57102
class YicesWithSymFpu(ctx: KContext): KSymFpuSolver<KYicesSolverConfiguration>(KYicesSolver(ctx), ctx)
58103
}

‎usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ import org.usvm.StateCollectionStrategy
1010
import org.usvm.UMachine
1111
import org.usvm.UMachineOptions
1212
import org.usvm.api.targets.JcTarget
13-
import org.usvm.applySoftConstraints
1413
import org.usvm.forkblacklists.TargetsReachableForkBlackList
1514
import org.usvm.forkblacklists.UForkBlackList
1615
import org.usvm.machine.interpreter.JcInterpreter
@@ -45,7 +44,12 @@ class JcMachine(
4544
private val applicationGraph = JcApplicationGraph(cp)
4645

4746
private val typeSystem = JcTypeSystem(cp)
48-
private val components = JcComponents(typeSystem, options.solverType, options.useSolverForForks)
47+
private val components = JcComponents(
48+
typeSystem,
49+
options.solverType,
50+
options.useSolverForForks,
51+
options.runSolverInAnotherProcess
52+
)
4953
private val ctx = JcContext(cp, components)
5054

5155
private val interpreter = JcInterpreter(ctx, applicationGraph, interpreterObserver)

‎usvm-jvm/src/samples/java/org/usvm/samples/arrays/PrimitiveArrays.java

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,10 @@ public byte charArray(char[] a, char x) {
5959
}
6060
a[0] = 5;
6161
a[1] = x;
62-
if (a[0] + a[1] > 20) {
62+
63+
// Note that the sum of two chars has the int type
64+
int sum = a[0] + a[1];
65+
if (sum > 20) {
6366
return 1;
6467
}
6568
return 0;

‎usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/PrimitiveArraysTest.kt

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ package org.usvm.samples.arrays
22

33

44
import org.junit.jupiter.api.Disabled
5+
import org.junit.jupiter.api.RepeatedTest
56
import org.junit.jupiter.api.Test
67
import org.usvm.samples.JavaMethodTestRunner
78
import org.usvm.test.util.checkers.eq
@@ -68,8 +69,8 @@ internal class PrimitiveArraysTest : JavaMethodTestRunner() {
6869
ignoreNumberOfAnalysisResults,
6970
{ _, a, _, r -> a == null && r.isException<NullPointerException>() },
7071
{ _, a, _, r -> a != null && a.size != 2 && r.getOrNull() == (-1).toByte() },
71-
{ _, a, x, r -> a != null && a.size == 2 && x + 5 <= 20.toChar() && r.getOrNull() == 0.toByte() },
72-
{ _, a, x, r -> a != null && a.size == 2 && x + 5 > 20.toChar() && r.getOrNull() == 1.toByte() }
72+
{ _, a, x, r -> a != null && a.size == 2 && x.code + 5 <= 20 && r.getOrNull() == 0.toByte() },
73+
{ _, a, x, r -> a != null && a.size == 2 && x.code + 5 > 20 && r.getOrNull() == 1.toByte() }
7374
)
7475
}
7576

‎usvm-jvm/src/test/kotlin/org/usvm/samples/functions/TestSimple.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ class TestSimple : JavaMethodTestRunner() {
2222
checkDiscoveredProperties(
2323
Simple::calcTwoFunctions,
2424
ignoreNumberOfAnalysisResults,
25-
{ _, x, y, r -> r == 0 && y > 0 && x * x + y < 0 },
25+
{ _, x, y, r -> r == 0 && y >= 0 && x * x + y < 0 },
2626
{ _, x, y, r -> r == 1 && !(y > 0 && x * x + y < 0) },
2727
)
2828
}

‎usvm-jvm/src/test/kotlin/org/usvm/samples/types/CastExamplesTest.kt

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package org.usvm.samples.types
22

33
import org.junit.jupiter.api.Test
4+
import org.usvm.SolverType
45
import org.usvm.samples.JavaMethodTestRunner
56
import org.usvm.test.util.checkers.eq
67

@@ -53,13 +54,16 @@ internal class CastExamplesTest : JavaMethodTestRunner() {
5354

5455
@Test
5556
fun testFloatToInt() {
56-
checkDiscoveredProperties(
57-
CastExamples::floatToInt,
58-
eq(3),
59-
{ _, x, r -> x < 0 && x.toInt() < 0 && r == 1 },
60-
{ _, x, r -> x < 0 && x.toInt() >= 0 && r == 2 },
61-
{ _, x, r -> !(x < 0) && r == 3 },
62-
)
57+
// TODO remove after fixing Z3 model detach in ksmt
58+
withOptions(options.copy(solverType = SolverType.YICES)) {
59+
checkDiscoveredProperties(
60+
CastExamples::floatToInt,
61+
eq(3),
62+
{ _, x, r -> x < 0 && x.toInt() < 0 && r == 1 },
63+
{ _, x, r -> x < 0 && x.toInt() >= 0 && r == 2 },
64+
{ _, x, r -> !(x < 0) && r == 3 },
65+
)
66+
}
6367
}
6468

6569
@Test

‎usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,10 @@ data class UMachineOptions(
181181
* Whether we use a solver on symbolic branching to fork only with satisfiable states or keep all states.
182182
*/
183183
val useSolverForForks: Boolean = true,
184+
/**
185+
* Whether we should run solver in another process or not.
186+
*/
187+
val runSolverInAnotherProcess: Boolean = false,
184188
/**
185189
* Whether we should try to apply soft constraints for symbolic values.
186190
*/

0 commit comments

Comments
 (0)