Add ensureSat

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<out T>
@@ -149,7 +150,7 @@ open class USolverBase<Type>(
     }
 
     fun emptyModel(): UModelBase<Type> =
-        (check(UPathConstraints(ctx, ctx.defaultOwnership)) as USatResult<UModelBase<Type>>).model
+        check(UPathConstraints(ctx, ctx.defaultOwnership)).ensureSat().model
 
     override fun close() {
         smtSolver.close()

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 <T> USolverResult<T>.ensureSat(): USatResult<T> {
+    check(this is USatResult) { "Expected SAT result, but got $this" }
+    return this
+}

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)

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<UModelBase<TestType>>).model
+        val model = solver.check(pc).ensureSat().model
         val concreteRef = assertIs<UConcreteHeapRef>(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<UModelBase<TestType>>).model
+        val model = solver.check(pc).ensureSat().model
         val concreteRef = assertIs<UConcreteHeapRef>(model.eval(ref))
         val types = model.typeStreamOf(concreteRef)
         types.take100AndAssertEqualsToSetOf(derived1A, derivedMulti, derivedMultiInterfaces)

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<JcType>()
 
-        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)

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<EtsType>()
-        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)