diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt index b0f50aca0c..3607a9120b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt +++ b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt @@ -11,6 +11,7 @@ import org.usvm.isFalse import org.usvm.isTrue import org.usvm.model.UModelBase import org.usvm.model.UModelDecoder +import org.usvm.utils.ensureSat import kotlin.time.Duration sealed interface USolverResult @@ -149,7 +150,7 @@ open class USolverBase( } fun emptyModel(): UModelBase = - (check(UPathConstraints(ctx, ctx.defaultOwnership)) as USatResult>).model + check(UPathConstraints(ctx, ctx.defaultOwnership)).ensureSat().model override fun close() { smtSolver.close() diff --git a/usvm-core/src/main/kotlin/org/usvm/utils/ResultUtils.kt b/usvm-core/src/main/kotlin/org/usvm/utils/ResultUtils.kt new file mode 100644 index 0000000000..42968a4fd0 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/utils/ResultUtils.kt @@ -0,0 +1,9 @@ +package org.usvm.utils + +import org.usvm.solver.USatResult +import org.usvm.solver.USolverResult + +fun USolverResult.ensureSat(): USatResult { + check(this is USatResult) { "Expected SAT result, but got $this" } + return this +} diff --git a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt index 603b3205a1..1fd671d90d 100644 --- a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt @@ -21,6 +21,7 @@ import org.usvm.memory.UReadOnlyMemory import org.usvm.model.ULazyModelDecoder import org.usvm.sizeSort import org.usvm.types.single.SingleTypeSystem +import org.usvm.utils.ensureSat import kotlin.test.assertSame import kotlin.time.Duration.Companion.INFINITE @@ -65,7 +66,7 @@ open class SoftConstraintsTest { pc += expr val softConstraints = softConstraintsProvider.makeSoftConstraints(pc) - val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult + val result = solver.checkWithSoftConstraints(pc, softConstraints).ensureSat() val model = result.model val fstRegisterValue = model.eval(fstRegister) @@ -99,7 +100,7 @@ open class SoftConstraintsTest { USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, timeout = INFINITE) val softConstraints = softConstraintsProvider.makeSoftConstraints(pc) - val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult + val result = solver.checkWithSoftConstraints(pc, softConstraints).ensureSat() val model = result.model verify(exactly = 1) { @@ -144,7 +145,7 @@ open class SoftConstraintsTest { pc += (inputRef eq nullRef).not() val softConstraints = softConstraintsProvider.makeSoftConstraints(pc) - val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult + val result = solver.checkWithSoftConstraints(pc, softConstraints).ensureSat() val model = result.model val value = model.eval(mkInputArrayLengthReading(region, inputRef)) @@ -164,7 +165,7 @@ open class SoftConstraintsTest { pc += (inputRef eq nullRef).not() val softConstraints = softConstraintsProvider.makeSoftConstraints(pc) - val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult + val result = solver.checkWithSoftConstraints(pc, softConstraints).ensureSat() val model = result.model val value = model.eval(mkInputArrayLengthReading(region, inputRef)) @@ -182,7 +183,7 @@ open class SoftConstraintsTest { pc += expression val softConstraints = softConstraintsProvider.makeSoftConstraints(pc) - val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult + val result = solver.checkWithSoftConstraints(pc, softConstraints).ensureSat() val model = result.model model.eval(expression) diff --git a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt index ba6acb47f9..57ffb11bfa 100644 --- a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt @@ -51,6 +51,7 @@ import org.usvm.types.system.interfaceBC1 import org.usvm.types.system.interfaceBC2 import org.usvm.types.system.testTypeSystem import org.usvm.types.system.top +import org.usvm.utils.ensureSat import kotlin.test.assertEquals import kotlin.test.assertIs import kotlin.test.assertNotEquals @@ -92,7 +93,7 @@ class TypeSolverTest { val ref = mkRegisterReading(0, addressSort) pc += mkIsSubtypeExpr(ref, base1) pc += mkHeapRefEq(ref, nullRef).not() - val model = (solver.check(pc) as USatResult>).model + val model = solver.check(pc).ensureSat().model val concreteRef = assertIs(model.eval(ref)) val types = model.typeStreamOf(concreteRef) types.take100AndAssertEqualsToSetOf(base1, derived1A, derived1B) @@ -103,7 +104,7 @@ class TypeSolverTest { val ref = mkRegisterReading(0, addressSort) pc += mkIsSubtypeExpr(ref, interface1) pc += mkHeapRefEq(ref, nullRef).not() - val model = (solver.check(pc) as USatResult>).model + val model = solver.check(pc).ensureSat().model val concreteRef = assertIs(model.eval(ref)) val types = model.typeStreamOf(concreteRef) types.take100AndAssertEqualsToSetOf(derived1A, derivedMulti, derivedMultiInterfaces) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt index 396c791c33..f84135736a 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt @@ -74,12 +74,12 @@ import org.usvm.machine.state.throwExceptionAndDropStackFrame import org.usvm.machine.state.throwExceptionWithoutStackFrameDrop import org.usvm.memory.ULValue import org.usvm.memory.URegisterStackLValue -import org.usvm.solver.USatResult import org.usvm.targets.UTargetsSet import org.usvm.types.singleOrNull import org.usvm.util.name import org.usvm.util.outerClassInstanceField import org.usvm.util.write +import org.usvm.utils.ensureSat import org.usvm.utils.logAssertFailure import org.usvm.utils.onStateDeath @@ -140,7 +140,7 @@ class JcInterpreter( val solver = ctx.solver() - val model = (solver.check(state.pathConstraints) as USatResult).model + val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) val entrypointInst = JcMethodEntrypointInst(method, entrypointArguments) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt index 10b3652eb8..c380714d47 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TSInterpreter.kt @@ -35,8 +35,8 @@ import org.usvm.machine.state.newStmt import org.usvm.machine.state.parametersWithThisCount import org.usvm.machine.state.returnValue import org.usvm.memory.URegisterStackLValue -import org.usvm.solver.USatResult import org.usvm.targets.UTargetsSet +import org.usvm.utils.ensureSat private val logger = KotlinLogging.logger {} @@ -199,7 +199,7 @@ class TSInterpreter( ) val solver = ctx.solver() - val model = (solver.check(state.pathConstraints) as USatResult).model + val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) state.callStack.push(method, returnSite = null)