More fixes for real applications

buildSrc/src/main/kotlin/Dependencies.kt

@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "4ca8d08f1d"
+    const val jacodb = "77b83e4127"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

usvm-core/src/main/kotlin/org/usvm/StepScope.kt

@@ -29,7 +29,7 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
 ) {
     private val forkedStates = mutableListOf<T>()
 
-    private inline val alive: Boolean get() = stepScopeState != DEAD
+    private inline val alive: Boolean get() = stepScopeState != DEAD && !originalState.pathConstraints.isFalse
     private inline val canProcessFurtherOnCurrentStep: Boolean get() = stepScopeState == CAN_BE_PROCESSED
     private inline val ctx: Context get() = originalState.ctx
 

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -6,6 +6,8 @@ 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.EtsEnumValueType
+import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsRefType
@@ -52,7 +54,6 @@ class TsContext(
     val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 
-
     /**
      * In TS we treat undefined value as a null reference in other objects.
      * For real null represented in the language we create another reference.
@@ -74,17 +75,28 @@ 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")
+            }
+        }
+        is EtsEnumValueType -> unresolvedSort
+        else -> {
+            TODO("${type::class.simpleName} is not yet supported: $type")
+        }
     }
 
-    // TODO: for now, ALL descriptors for array are UNKNOWN
-    //  in order to make ALL reading/writing, including '.length' access consistent
-    //  and possible in cases when the array type is not known.
-    //  For example, when we access '.length' of some array, we do not care about its type,
-    //  but we HAVE TO use some type consistent with the type used when this array was created.
-    //  Note: Using UnknownType everywhere does not lead to any errors yet,
-    //  since we do not rely on array types in any way.
-    fun arrayDescriptorOf(type: EtsArrayType): EtsType = EtsUnknownType
+    fun arrayDescriptorOf(type: EtsArrayType): EtsType {
+        return when (type.elementType) {
+            is EtsBooleanType -> EtsArrayType(EtsBooleanType, dimensions = 1)
+            is EtsNumberType -> EtsArrayType(EtsNumberType, dimensions = 1)
+            is EtsArrayType -> TODO("Unsupported yet: $type")
+            is EtsUnionType -> EtsArrayType(type.elementType, dimensions = 1)
+            else -> EtsArrayType(EtsUnknownType, dimensions = 1)
+        }
+    }
 
     fun UConcreteHeapRef.getFakeType(memory: UReadOnlyMemory<*>): EtsFakeType {
         check(isFakeObject())

usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

@@ -23,8 +23,10 @@ import org.usvm.statistics.UMachineObserver
 import org.usvm.statistics.collectors.AllStatesCollector
 import org.usvm.statistics.collectors.CoveredNewStatesCollector
 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
@@ -78,7 +80,7 @@ class TsMachine(
             timeStatistics = timeStatistics,
             coverageStatisticsFactory = { coverageStatistics },
             cfgStatisticsFactory = { cfgStatistics },
-            callGraphStatisticsFactory = { callGraphStatistics },
+            callGraphStatisticsFactory = { callGraphStatistics }
         )
 
         val statesCollector =
@@ -94,16 +96,36 @@ class TsMachine(
         val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
         observers.add(statesCollector)
 
+        if (options.useSoftConstraints) {
+            observers.add(SoftConstraintsObserver())
+        }
+
         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)

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt

@@ -92,6 +92,20 @@ fun TsContext.mkNumericExpr(
     expr: UExpr<out USort>,
     scope: TsStepScope,
 ): UExpr<KFp64Sort> = scope.calcOnState {
+    if (expr.isFakeObject()) {
+        return@calcOnState scope.calcOnState {
+            val type = expr.getFakeType(scope)
+            mkIte(
+                condition = type.fpTypeExpr,
+                trueBranch = expr.extractFp(scope),
+                falseBranch = mkIte(
+                    condition = type.boolTypeExpr,
+                    trueBranch = mkNumericExpr(expr.extractBool(scope), scope),
+                    falseBranch = mkNumericExpr(expr.extractRef(scope), scope)
+                )
+            )
+        }
+    }
 
     // 7.1.4 ToNumber ( argument )
     //