Added timeout for SMT and type solvers (#90)

usvm-core/src/main/kotlin/org/usvm/model/UTypeModel.kt

@@ -31,7 +31,8 @@ class UTypeModel<Type>(
 
                 val evaluatedTypeStream = typeStream(ref)
                 val typeStream = evaluatedTypeStream.filterBySupertype(supertype)
-                if (!typeStream.isEmpty) {
+                val isEmpty = typeStream.isEmpty ?: error("Invalid model containing wrong type stream $typeStream")
+                if (!isEmpty) {
                     typeStreamByAddr[ref.address] = typeStream
                     ref.ctx.trueExpr
                 } else {
@@ -54,7 +55,8 @@ class UTypeModel<Type>(
 
                 val evaluatedTypeStream = typeStream(ref)
                 val typeStream = evaluatedTypeStream.filterBySubtype(subtype)
-                if (!typeStream.isEmpty) {
+                val isEmpty = typeStream.isEmpty ?: error("Invalid model containing wrong type stream $typeStream")
+                if (!isEmpty) {
                     typeStreamByAddr[ref.address] = typeStream
                     ref.ctx.trueExpr
                 } else {

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 kotlin.time.Duration
 
 sealed interface USolverResult<out T>
 
@@ -32,6 +33,8 @@ open class USolverBase<Type>(
     protected val typeSolver: UTypeSolver<Type>,
     protected val translator: UExprTranslator<Type, *>,
     protected val decoder: UModelDecoder<UModelBase<Type>>,
+    // TODO this timeout must not exceed time budget for the MUT
+    private val timeout: Duration
 ) : USolver<UPathConstraints<Type>, UModelBase<Type>>(), AutoCloseable {
 
     override fun check(query: UPathConstraints<Type>): USolverResult<UModelBase<Type>> =
@@ -123,16 +126,16 @@ open class USolverBase<Type>(
     ): KSolverStatus {
         var status: KSolverStatus
         if (softConstraints.isNotEmpty()) {
-            status = smtSolver.checkWithAssumptions(softConstraints)
+            status = smtSolver.checkWithAssumptions(softConstraints, timeout)
 
             while (status == KSolverStatus.UNSAT) {
                 val unsatCore = smtSolver.unsatCore().toHashSet()
                 if (unsatCore.isEmpty()) break
                 softConstraints.removeAll { it in unsatCore }
-                status = smtSolver.checkWithAssumptions(softConstraints)
+                status = smtSolver.checkWithAssumptions(softConstraints, timeout)
             }
         } else {
-            status = smtSolver.check()
+            status = smtSolver.check(timeout)
         }
         return status
     }

usvm-core/src/main/kotlin/org/usvm/solver/TypeSolver.kt

@@ -109,7 +109,8 @@ class UTypeSolver<Type>(
         val allConcreteRefToType = concreteToRegionWithCluster.mapValues { (_, regionToCluster) ->
             val (region, cluster) = regionToCluster
             val typeStream = region.typeStream
-            if (typeStream.isEmpty) {
+            val isEmpty = typeStream.isEmpty ?: return UUnknownResult() // Timeout here may lead to an inconsistent model - avoid it
+            if (isEmpty) {
                 // the only way to reach here is when some of the clusters consists of a single reference
                 // because if the cluster is bigger, then we called region.isEmpty previously at least once
                 check(cluster.size == 1)

usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt

@@ -2,6 +2,12 @@ package org.usvm.types
 
 import org.usvm.algorithms.CachingSequence
 import org.usvm.algorithms.DfsIterator
+import org.usvm.types.TypesResult.Companion.toTypesResult
+import org.usvm.types.TypesResult.EmptyTypesResult
+import org.usvm.types.TypesResult.SuccessfulTypesResult
+import org.usvm.types.TypesResult.TypesResultWithExpiredTimeout
+import org.usvm.util.TimeoutException
+import org.usvm.util.timeLimitedIterator
 
 /**
  * A persistent type stream based on the [supportType]. Takes inheritors of the [supportType] and
@@ -21,7 +27,7 @@ class USupportTypeStream<Type> private constructor(
     private val supportType: Type,
     private val filtering: (Type) -> Boolean,
 ) : UTypeStream<Type> {
-    override fun filterBySupertype(type: Type): UTypeStream<Type> =
+    override fun filterBySupertype(type: Type): USupportTypeStream<Type> =
         when {
             // we update the [supportType]
             typeSystem.isSupertype(supportType, type) -> USupportTypeStream(
@@ -59,13 +65,13 @@ class USupportTypeStream<Type> private constructor(
             else -> withNewFiltering(type) { !typeSystem.isSupertype(type, it) }
         }
 
-    override fun filterByNotSubtype(type: Type): UTypeStream<Type> =
+    override fun filterByNotSubtype(type: Type): USupportTypeStream<Type> =
         when {
             typeSystem.isSupertype(type, supportType) && type != supportType -> this
             else -> withNewFiltering(type) { !typeSystem.isSupertype(it, type) }
         }
 
-    private fun withNewFiltering(type: Type, newFiltering: (Type) -> Boolean) =
+    private fun withNewFiltering(type: Type, newFiltering: (Type) -> Boolean): USupportTypeStream<Type> =
         USupportTypeStream(
             typeSystem,
             cachingSequence.filter(newFiltering),
@@ -78,17 +84,29 @@ class USupportTypeStream<Type> private constructor(
             filtering = { filtering(it) && newFiltering(it) }
         )
 
-    override fun take(n: Int): Set<Type> {
+    override fun take(n: Int): TypesResult<Type> {
         val set = cacheFromQueries.take(n).toMutableSet()
-        val iterator = cachingSequence.iterator()
-        while (set.size < n && iterator.hasNext()) {
-            set += iterator.next()
+        val iterator = cachingSequence.timeLimitedIterator(typeSystem.typeOperationsTimeout)
+
+        return try {
+            while (set.size < n && iterator.hasNext()) {
+                set += iterator.next()
+            }
+
+            set.toTypesResult(wasTimeoutExpired = false)
+        } catch (e: TimeoutException) {
+            set.toTypesResult(wasTimeoutExpired = true)
         }
-        return set
     }
 
-    override val isEmpty: Boolean
-        get() = take(1).isEmpty()
+    override val isEmpty: Boolean?
+        get() = take(1).let {
+            when (it) {
+                EmptyTypesResult -> true
+                is SuccessfulTypesResult -> it.isEmpty()
+                is TypesResultWithExpiredTimeout -> null
+            }
+        }
 
     override val commonSuperType: Type
         get() = supportType

usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt

@@ -21,7 +21,7 @@ class UTypeRegion<Type>(
      */
     private fun contradiction() = UTypeRegion(typeSystem, emptyTypeStream())
 
-    override val isEmpty: Boolean get() = typeStream.isEmpty
+    override val isEmpty: Boolean get() = typeStream.isEmpty ?: false // Timeout here means that this type region **may** be not empty
 
     private val <Type> UTypeRegion<Type>.size: Int
         get() = supertypes.size + notSupertypes.size + subtypes.size + notSubtypes.size

usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt

@@ -1,5 +1,9 @@
 package org.usvm.types
 
+import org.usvm.types.TypesResult.EmptyTypesResult
+import org.usvm.types.TypesResult.SuccessfulTypesResult
+import org.usvm.types.TypesResult.TypesResultWithExpiredTimeout
+
 /**
  * A base interface representing persistent type constraints and a function to collect
  * **instantiable** types satisfying them.
@@ -43,18 +47,45 @@ interface UTypeStream<Type> {
     fun filterByNotSubtype(type: Type): UTypeStream<Type>
 
     /**
-     * @return the collection of **instantiable** types satisfying accumulated type constraints.
+     * @return a [TypesResult] on the collection of **instantiable** types satisfying accumulated type constraints,
+     * according to the [UTypeSystem.typeOperationsTimeout]:
+     * * If there are no types satisfying constraints, returns [EmptyTypesResult];
+     * * If there are some types found and [UTypeSystem.typeOperationsTimeout] was not expired,
+     * returns [SuccessfulTypesResult];
+     * * If the [UTypeSystem.typeOperationsTimeout] was expired, returns [TypesResultWithExpiredTimeout] containing
+     * all types satisfying constraints that were collected before timeout expiration.
      */
-    fun take(n: Int): Collection<Type>
+    fun take(n: Int): TypesResult<Type>
 
-    val isEmpty: Boolean
+    /**
+     * @return whether this [UTypeStream] is empty according to [UTypeStream.take],
+     * or null if [UTypeSystem.typeOperationsTimeout] was expired.
+     */
+    val isEmpty: Boolean?
 
     /**
      * Stores a supertype that satisfies current type constraints and other satisfying types are inheritors of this type.
      */
     val commonSuperType: Type?
 }
 
+sealed interface TypesResult<out Type> {
+    object EmptyTypesResult : TypesResult<Nothing>, Collection<Nothing> by emptyList()
+
+    class SuccessfulTypesResult<Type>(
+        val types: Collection<Type>
+    ) : TypesResult<Type>, Collection<Type> by types
+
+    class TypesResultWithExpiredTimeout<Type>(
+        val collectedTypes: Collection<Type>
+    ) : TypesResult<Type>
+
+    companion object {
+        fun <Type> Collection<Type>.toTypesResult(wasTimeoutExpired: Boolean): TypesResult<Type> =
+            if (wasTimeoutExpired) TypesResultWithExpiredTimeout(this) else SuccessfulTypesResult(this)
+    }
+}
+
 /**
  * An empty type stream.
  */
@@ -67,7 +98,7 @@ object UEmptyTypeStream : UTypeStream<Nothing> {
 
     override fun filterByNotSubtype(type: Nothing): UTypeStream<Nothing> = this
 
-    override fun take(n: Int): Collection<Nothing> = emptyList()
+    override fun take(n: Int): EmptyTypesResult = EmptyTypesResult
 
     override val isEmpty: Boolean
         get() = true
@@ -79,14 +110,42 @@ object UEmptyTypeStream : UTypeStream<Nothing> {
 @Suppress("UNCHECKED_CAST")
 fun <Type> emptyTypeStream(): UTypeStream<Type> = UEmptyTypeStream as UTypeStream<Type>
 
-fun <Type> UTypeStream<Type>.first(): Type = take(1).first()
+fun <Type> UTypeStream<Type>.first(): Type = take(1).let {
+    when (it) {
+        EmptyTypesResult -> throw NoSuchElementException("Collection is empty.")
+        is SuccessfulTypesResult -> it.first()
+        is TypesResultWithExpiredTimeout -> it.collectedTypes.first()
+    }
+}
 
-fun <Type> UTypeStream<Type>.firstOrNull(): Type? = take(1).firstOrNull()
+fun <Type> UTypeStream<Type>.firstOrNull(): Type? = take(1).let {
+    when (it) {
+        EmptyTypesResult -> null
+        is SuccessfulTypesResult -> it.firstOrNull()
+        is TypesResultWithExpiredTimeout -> it.collectedTypes.firstOrNull()
+    }
+}
 
 // Note: we try to take at least two types to ensure that we don't have no more than one type.
-fun <Type> UTypeStream<Type>.single(): Type = take(2).single()
+fun <Type> UTypeStream<Type>.single(): Type = take(2).let {
+    when (it) {
+        EmptyTypesResult -> throw NoSuchElementException("Collection is empty.")
+        is SuccessfulTypesResult -> it.single()
+        is TypesResultWithExpiredTimeout ->
+            error(
+                "$this type stream has unknown number of types because of timeout exceeding, " +
+                        "already found types: ${it.collectedTypes}"
+            )
+    }
+}
 
-fun <Type> UTypeStream<Type>.singleOrNull(): Type? = take(2).singleOrNull()
+fun <Type> UTypeStream<Type>.singleOrNull(): Type? = take(2).let {
+    when (it) {
+        EmptyTypesResult -> null
+        is SuccessfulTypesResult -> it.singleOrNull()
+        is TypesResultWithExpiredTimeout -> null // Unknown number of types
+    }
+}
 
 /**
  * Consists of just one type [singleType].
@@ -123,7 +182,7 @@ class USingleTypeStream<Type>(
             this
         }
 
-    override fun take(n: Int) = listOf(singleType)
+    override fun take(n: Int): SuccessfulTypesResult<Type> = SuccessfulTypesResult(listOf(singleType))
 
     override val isEmpty: Boolean
         get() = false

usvm-core/src/main/kotlin/org/usvm/types/TypeSystem.kt

@@ -1,10 +1,17 @@
 package org.usvm.types
 
+import kotlin.time.Duration
+
 /**
  * A base interface, instantiated in target machines. Provides type information and [topTypeStream],
  * representing all possible types in the system.
  */
 interface UTypeSystem<Type> {
+    /**
+     * A timeout used for heavy operations with types.
+     */
+    // TODO this timeout must not exceed time budget for the MUT
+    val typeOperationsTimeout: Duration
 
     /**
      * @return true if [type] <: [supertype].

usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt

@@ -29,6 +29,7 @@ import org.usvm.targets.UTarget
 import org.usvm.targets.UTargetsSet
 import org.usvm.types.single.SingleTypeSystem
 import kotlin.test.assertEquals
+import kotlin.time.Duration.Companion.INFINITE
 
 abstract class SymbolicCollectionTestBase {
     lateinit var ctx: UContext<USizeSort>
@@ -49,7 +50,7 @@ abstract class SymbolicCollectionTestBase {
         val decoder = ULazyModelDecoder(translator)
         this.translator = translator
         val typeSolver = UTypeSolver(SingleTypeSystem)
-        uSolver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder)
+        uSolver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, timeout = INFINITE)
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
         every { components.mkStatesForkProvider() } answers { WithSolverStateForker }
 

usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt

@@ -38,6 +38,7 @@ import org.usvm.solver.UUnsatResult
 import org.usvm.types.single.SingleTypeSystem
 import kotlin.test.assertIs
 import kotlin.test.assertTrue
+import kotlin.time.Duration.Companion.INFINITE
 
 private typealias Type = SingleTypeSystem.SingleType
 
@@ -60,7 +61,7 @@ class ModelDecodingTest {
         val translator = UExprTranslator<Type, USizeSort>(ctx)
         val decoder = ULazyModelDecoder(translator)
         val typeSolver = UTypeSolver(SingleTypeSystem)
-        solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder)
+        solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, timeout = INFINITE)
 
         pc = UPathConstraints(ctx)
 

usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt

@@ -18,6 +18,7 @@ import org.usvm.model.ULazyModelDecoder
 import org.usvm.sizeSort
 import org.usvm.types.single.SingleTypeSystem
 import kotlin.test.assertSame
+import kotlin.time.Duration.Companion.INFINITE
 
 private typealias Type = SingleTypeSystem.SingleType
 
@@ -41,7 +42,7 @@ open class SoftConstraintsTest {
         decoder = ULazyModelDecoder(translator)
 
         val typeSolver = UTypeSolver(SingleTypeSystem)
-        solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder)
+        solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, timeout = INFINITE)
     }
 
     @Test
@@ -85,7 +86,7 @@ open class SoftConstraintsTest {
 
         val typeSolver = UTypeSolver<Type>(mockk())
         val solver: USolverBase<Type> =
-            USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder)
+            USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, timeout = INFINITE)
 
         val softConstraints = softConstraintsProvider.makeSoftConstraints(pc)
         val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult

usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt

@@ -52,6 +52,7 @@ import kotlin.test.assertEquals
 import kotlin.test.assertIs
 import kotlin.test.assertNotEquals
 import kotlin.test.assertTrue
+import kotlin.time.Duration.Companion.INFINITE
 
 class TypeSolverTest {
     private val typeSystem = testTypeSystem
@@ -65,7 +66,7 @@ class TypeSolverTest {
         val decoder = ULazyModelDecoder(translator)
 
         typeSolver = UTypeSolver(typeSystem)
-        solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder)
+        solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, timeout = INFINITE)
 
         every { components.mkSolver(ctx) } returns solver
         every { components.mkTypeSystem(ctx) } returns typeSystem
@@ -514,6 +515,7 @@ class TypeSolverTest {
     private fun <T> UTypeStream<T>.take100AndAssertEqualsToSetOf(vararg elements: T) {
         val set = elements.toSet()
         val result = take(100)
+        assertIs<TypesResult.SuccessfulTypesResult<T>>(result)
         assertEquals(set.size, result.size, result.toString())
         assertEquals(set, result.toSet())
     }