Some more fixes

UnitTestBot · CaelmBleidd · May 29, 2025 · May 29, 2025 · May 30, 2025 · May 30, 2025
commit f85ef55aa4bd325788a8fba6dd8bf5418a9d56c3
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -6,8 +6,10 @@ import org.jacodb.ets.model.EtsAliasType
 import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanType
+import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsRawType
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStringType
@@ -73,7 +75,20 @@ class TsContext(
         is EtsAnyType -> unresolvedSort
         is EtsUnknownType -> unresolvedSort
         is EtsAliasType -> typeToSort(type.originalType)
-        else -> TODO("${type::class.simpleName} is not yet supported: $type")
+        is EtsGenericType -> {
+            if (type.constraint == null && type.defaultType == null) {
+                unresolvedSort
+            } else {
+                TODO("Not yet implemented")
+            }
+        }
+        else -> {
+            if (type is EtsRawType && type.kind == "EnumValueType") {
+                unresolvedSort
+            } else {
+                TODO("${type::class.simpleName} is not yet supported: $type")
+            }
+        }
     }
 
     fun arrayDescriptorOf(type: EtsArrayType): EtsType {

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -8,6 +8,7 @@ import org.usvm.CoverageZone
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
+import org.usvm.UPathSelector
 import org.usvm.api.targets.TsTarget
 import org.usvm.machine.interpreter.TsInterpreter
 import org.usvm.machine.state.TsMethodResult
@@ -26,6 +27,7 @@ import org.usvm.statistics.collectors.TargetsReachedStatesCollector
 import org.usvm.statistics.constraints.SoftConstraintsObserver
 import org.usvm.statistics.distances.CfgStatisticsImpl
 import org.usvm.statistics.distances.PlainCallGraphStatistics
+import org.usvm.stopstrategies.StopStrategy
 import org.usvm.stopstrategies.createStopStrategy
 import org.usvm.util.humanReadableSignature
 import kotlin.time.Duration.Companion.seconds
@@ -72,15 +74,39 @@ class TsMachine(
 
         val timeStatistics = TimeStatistics<EtsMethod, TsState>()
 
-        val pathSelector = createPathSelector(
-            initialStates = initialStates,
-            options = options,
-            applicationGraph = graph,
-            timeStatistics = timeStatistics,
-            coverageStatisticsFactory = { coverageStatistics },
-            cfgStatisticsFactory = { cfgStatistics },
-            callGraphStatisticsFactory = { callGraphStatistics },
-        )
+        val pathSelector = object : UPathSelector<TsState> {
+            val internalSelector = createPathSelector(
+                initialStates = initialStates,
+                options = options,
+                applicationGraph = graph,
+                timeStatistics = timeStatistics,
+                coverageStatisticsFactory = { coverageStatistics },
+                cfgStatisticsFactory = { cfgStatistics },
+                callGraphStatisticsFactory = { callGraphStatistics }
+            )
+
+            override fun isEmpty(): Boolean {
+                return internalSelector.isEmpty()
+            }
+
+            override fun peek(): TsState {
+                return internalSelector.peek()
+            }
+
+            override fun remove(state: TsState) {
+                logger.warn { "Selector size -1" }
+                return internalSelector.remove(state)
+            }
+
+            override fun add(states: Collection<TsState>) {
+                logger.warn { "Selector size +1" }
+                return internalSelector.add(states)
+            }
+
+            override fun update(state: TsState) {
+                return internalSelector.update(state)
+            }
+        }
 
         val statesCollector =
             when (options.stateCollectionStrategy) {
@@ -101,14 +127,30 @@ class TsMachine(
 
         val stepsStatistics = StepsStatistics<EtsMethod, TsState>()
 
-        val stopStrategy = createStopStrategy(
-            options,
-            targets,
-            timeStatisticsFactory = { timeStatistics },
-            stepsStatisticsFactory = { stepsStatistics },
-            coverageStatisticsFactory = { coverageStatistics },
-            getCollectedStatesCount = { statesCollector.collectedStates.size }
-        )
+        val stopStrategy = object : StopStrategy {
+            val strategy = createStopStrategy(
+                options,
+                targets,
+                timeStatisticsFactory =
+                    { timeStatistics },
+                stepsStatisticsFactory =
+                    { stepsStatistics },
+                coverageStatisticsFactory =
+                    { coverageStatistics },
+                getCollectedStatesCount =
+                    { statesCollector.collectedStates.size }
+            )
+
+            override fun shouldStop(): Boolean {
+                val result = strategy.shouldStop()
+
+                if (result) {
+                    logger.warn { "Stop strategy finished execution $strategy" }
+                }
+
+                return result
+            }
+        }
 
         observers.add(timeStatistics)
         observers.add(stepsStatistics)
@@ -127,6 +169,16 @@ class TsMachine(
             )
         }
 
+        val endReasonObserver = object : UMachineObserver<TsState> {
+            override fun onStateTerminated(state: TsState, stateReachable: Boolean) {
+                logger.warn {
+                    "State is terminated on ${state.currentStatement} in the method ${state.currentStatement.method}"
+                }
+            }
+        }
+
+        observers += endReasonObserver
+
         run(
             interpreter,
             pathSelector,

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -54,6 +54,7 @@ import org.jacodb.ets.model.EtsPostIncExpr
 import org.jacodb.ets.model.EtsPreDecExpr
 import org.jacodb.ets.model.EtsPreIncExpr
 import org.jacodb.ets.model.EtsPtrCallExpr
+import org.jacodb.ets.model.EtsRawType
 import org.jacodb.ets.model.EtsRemExpr
 import org.jacodb.ets.model.EtsRightShiftExpr
 import org.jacodb.ets.model.EtsStaticCallExpr
@@ -476,10 +477,6 @@ class TsExprResolver(
         }
 
         // TODO write tests
-        if (expr.callee.name == "push") {
-            let {}
-        }
-
         if (expr.callee.name == "push" && expr.instance.type is EtsArrayType) {
             return scope.calcOnState {
                 val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
@@ -805,6 +802,7 @@ class TsExprResolver(
             is EtsPropertyResolution.Ambiguous -> unresolvedSort
         }
 
+        // TODO
         // Если мы записали что-то в объект в виде bool, а потом считали это из поля bool | null, то здесь будет unresolvedSort,
         // мы проигнорируем что уже туда писали и считаем не оттуда
 
@@ -827,6 +825,26 @@ class TsExprResolver(
                         lValuesToAllocatedFakeObjects += refLValue to it
                     }
                 }
+
+                // TODO ambiguous enum fields resolution
+                if (etsField is EtsPropertyResolution.Unique) {
+                    val fieldType = etsField.property.type
+                    if (fieldType is EtsRawType && fieldType.kind == "EnumValueType") {
+                        val fakeType = fakeRef.getFakeType(scope)
+                        pathConstraints += ctx.mkOr(
+                            fakeType.fpTypeExpr,
+                            fakeType.refTypeExpr
+                        )
+
+                        // val supertype = TODO()
+                        // TODO add enum type as a constraint
+                        // pathConstraints += memory.types.evalIsSubtype(
+                        //     ref,
+                        //     TODO()
+                        // )
+                    }
+                }
+
                 memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
 
                 fakeRef

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
@@ -134,9 +134,7 @@ class TsInterpreter(
                 val s = e.stackTrace[0]
                 "Exception .(${s.fileName}:${s.lineNumber}): $e}"
             }
-
-            // Kill the state causing error
-            scope.assert(ctx.falseExpr)
+            // todo are exceptional states properly removed?
         }
 
         return scope.stepResult()
@@ -206,12 +204,14 @@ class TsInterpreter(
             concreteMethods += methods
         }
 
+        val limitedConcreteMethods = concreteMethods.take(5)
+
         logger.info {
-            "Preparing to fork on ${concreteMethods.size} methods: ${
-                concreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
+            "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
+                limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
             }"
         }
-        val conditionsWithBlocks = concreteMethods.map { method ->
+        val conditionsWithBlocks = limitedConcreteMethods.map { method ->
             val concreteCall = stmt.toConcrete(method)
             val block = { state: TsState -> state.newStmt(concreteCall) }
             val type = requireNotNull(method.enclosingClass).type
@@ -531,6 +531,7 @@ class TsInterpreter(
 
                                 memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr)
                             } else {
+                                // probably it is a enum, check for it
                                 error("TODO")
                             }
                         } else {

diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -6,7 +6,7 @@ import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.utils.getDeclaredLocals
 import org.jacodb.ets.utils.getLocals
-import org.jacodb.ets.utils.loadEtsProjectFromIR
+import org.jacodb.ets.utils.loadEtsProjectAutoConvert
 import org.junit.jupiter.api.condition.EnabledIf
 import org.usvm.api.TsTestValue
 import org.usvm.machine.TsMachine
@@ -21,7 +21,7 @@ import kotlin.test.Test
 class RunOnPhotosProject : TsMethodTestRunner() {
 
     companion object {
-        private const val PROJECT_PATH = "/projects/Demo_Photos/etsir/entry"
+        private const val PROJECT_PATH = "/projects/Demo_Photos/source/entry"
         private const val SDK_PATH = "/sdk/ohos/etsir"
 
         @JvmStatic
@@ -34,7 +34,7 @@ class RunOnPhotosProject : TsMethodTestRunner() {
         val projectPath = getResourcePath(PROJECT_PATH)
         val sdkPath = getResourcePathOrNull(SDK_PATH)
             ?: error("Could not load SDK from resources '$SDK_PATH'. Try running './gradlew generateSdkIR' to generate it.")
-        loadEtsProjectFromIR(projectPath, sdkPath)
+        loadEtsProjectAutoConvert(projectPath, sdkPath)
     }
 
     @Test

diff --git a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt
@@ -259,4 +259,5 @@ data class UMachineOptions(
      * Limit loop iterations.
      * */
     val loopIterationLimit: Int? = null,
+    // TODO fork limit
-    // TODO fork limit
+    /**
+     * Limit the number of forks that can be created. If null, no limit is applied.
+     */
+    val forkLimit: Int? = null,
-    // TODO fork limit
+    /**
+     * Limit the number of forks that can be created. If null, no limit is applied.
+     */
+    val forkLimit: Int? = null,
 )