[TS] Extend reachability analysis test suite

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

@@ -1,5 +1,6 @@
 package org.usvm.machine.expr
 
+import io.ksmt.expr.KFpRoundingMode
 import io.ksmt.utils.asExpr
 import mu.KotlinLogging
 import org.jacodb.ets.model.EtsArrayType
@@ -76,6 +77,13 @@
         }
     }
 
+    // Handle `Math` method calls
+    if (expr.instance.name == "Math") {
+        if (expr.callee.name == "floor") {
+            return from(handleMathFloor(expr))
+        }
+    }
+
     val instance = scope.calcOnState { resolve(expr.instance)?.asExpr(addressSort) }
         ?: return TsExprApproximationResult.ResolveFailure
 
@@ -255,6 +263,27 @@
     promise
 }
 
+private fun TsExprResolver.handleMathFloor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
+    check(expr.args.size == 1) {
+        "Math.floor() should have exactly one argument, but got ${expr.args.size}"
+    }
+    val arg = resolve(expr.args.single()) ?: return null
+
+    when (arg.sort) {
+        fp64Sort -> mkFpRoundToIntegralExpr(
+            roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative),
+            value = arg.asExpr(fp64Sort),
+        )
+
+        sizeSort -> arg.asExpr(sizeSort)
+
+        else -> {
+            logger.warn { "Unsupported argument sort for Math.floor(): ${arg.sort}" }
+            null
+        }
+    }
+}
+
 /**
  * Handles the `Array.push(...items)` method call.
  * Appends the specified `items` to the end of the array.

usvm-ts/src/test/kotlin/org/usvm/reachability/AsyncReachabilityTest.kt

@@ -0,0 +1,296 @@
+package org.usvm.reachability
+
+import org.jacodb.ets.model.EtsIfStmt
+import org.jacodb.ets.model.EtsReturnStmt
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.Disabled
+import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
+import org.usvm.UMachineOptions
+import org.usvm.api.targets.ReachabilityObserver
+import org.usvm.api.targets.TsReachabilityTarget
+import org.usvm.api.targets.TsTarget
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.util.getResourcePath
+import kotlin.test.Test
+import kotlin.test.assertTrue
+import kotlin.time.Duration
+
+/**
+ * Tests for asynchronous programming reachability scenarios.
+ * Verifies reachability analysis through async patterns and error handling.
+ */
+class AsyncReachabilityTest {
+
+    private val scene = run {
+        val path = "/reachability/AsyncReachability.ts"
+        val res = getResourcePath(path)
+        val file = loadEtsFileAutoConvert(res)
+        EtsScene(listOf(file))
+    }
+
+    private val options = UMachineOptions(
+        pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
+        exceptionsPropagation = true,
+        stopOnTargetsReached = true,
+        timeout = Duration.INFINITE,
+        stepsFromLastCovered = 3500L,
+        solverType = SolverType.YICES,
+        solverTimeout = Duration.INFINITE,
+        typeOperationsTimeout = Duration.INFINITE,
+    )
+
+    private val tsOptions = TsOptions()
+
+    @Test
+    fun testAsyncAwaitReachable() {
+        // Test reachability through async function logic:
+        //   const result = delay * 2 -> if (result > 50) -> if (result < 100) -> return 1
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "asyncAwaitReachable" }
+
+        val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
+        var target: TsTarget = initialTarget
+
+        // if (result > 50)
+        val minCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(minCheck))
+
+        // if (result < 100)
+        val maxCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(maxCheck))
+
+        // return 1
+        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
+        target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result for async/await reachability"
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached when delay * 2 is between 50-100"
+        )
+    }
+
+    @Test
+    fun testPromiseChainReachable() {
+        // Test reachability through Promise chain:
+        //   const doubled = value * 2 -> if (doubled === 20) -> return Promise.resolve(1)
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "promiseChainReachable" }
+
+        val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
+        var target: TsTarget = initialTarget
+
+        // if (doubled === 20)
+        val doubledCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(doubledCheck))
+
+        // return Promise.resolve(1)
+        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
+        target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result for Promise chain reachability"
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached when input value is 10"
+        )
+    }
+
+    @Disabled("No ::map method")
+    @Test
+    fun testPromiseAllReachable() {
+        // Test reachability through Promise.all pattern:
+        //   const results = values.map(v => v * 2) -> if (results.length === 3) -> if (results[1] === 40) -> return 1
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "promiseAllReachable" }
+
+        val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
+        var target: TsTarget = initialTarget
+
+        // if (results.length === 3)
+        val lengthCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(lengthCheck))
+
+        // if (results[1] === 40)
+        val valueCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(valueCheck))
+
+        // return 1
+        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
+        target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result for Promise.all reachability"
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached when values[1] is 20 (doubled to 40)"
+        )
+    }
+
+    @Disabled("Function types are not supported in EtsHierarchy")
+    @Test
+    fun testCallbackReachable() {
+        // Test reachability through callback pattern:
+        //   const processed = value + 10 -> if (processed > 25) -> callback(processed) -> return 1
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "callbackReachable" }
+
+        val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
+        var target: TsTarget = initialTarget
+
+        // if (processed > 25)
+        val processedCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(processedCheck))
+
+        // return 1
+        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
+        target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result for callback reachability"
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached when value > 15 (processed > 25)"
+        )
+    }
+
+    @Test
+    fun testErrorHandlingReachable() {
+        // Test reachability through try-catch error handling:
+        //   try { if (shouldThrow) throw Error -> return 1 } catch { return -1 }
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "errorHandlingReachable" }
+
+        val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
+        var target: TsTarget = initialTarget
+
+        // if (shouldThrow)
+        val throwCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(throwCheck))
+
+        // Both return paths should be reachable
+        val returnStmts = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()
+        returnStmts.forEach { returnStmt ->
+            target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
+        }
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result for error handling reachability"
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmts.any { it in reachedStatements },
+            "Expected at least one return statement to be reached in try-catch"
+        )
+    }
+
+    @Test
+    fun testConditionalAsyncReachable() {
+        // Test reachability through conditional async pattern:
+        //   if (useSync) result = value * 2 else result = value + 10 -> if (result === 20) -> return 1
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "conditionalAsyncReachable" }
+
+        val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
+        var target: TsTarget = initialTarget
+
+        // if (useSync)
+        val useSyncCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(useSyncCheck))
+
+        // if (result === 20)
+        val resultCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck))
+
+        // return 1
+        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
+        target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result for conditional async reachability"
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached through conditional branches"
+        )
+    }
+
+    @Test
+    fun testPromiseCreationReachable() {
+        // Test reachability through Promise creation logic:
+        //   if (shouldResolve) -> if (value > 5) -> return 1
+        //   else -> if (value < 0) -> return -1
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "promiseCreationReachable" }
+
+        val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
+        var target: TsTarget = initialTarget
+
+        // if (shouldResolve)
+        val shouldResolveCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(shouldResolveCheck))
+
+        // Multiple return paths
+        val returnStmts = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()
+        returnStmts.forEach { returnStmt ->
+            target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
+        }
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result for Promise creation reachability"
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmts.any { it in reachedStatements },
+            "Expected at least one return statement to be reached in Promise creation"
+        )
+    }
+}

usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt

@@ -4,6 +4,7 @@ import org.jacodb.ets.model.EtsIfStmt
 import org.jacodb.ets.model.EtsReturnStmt
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.Disabled
 import org.usvm.PathSelectionStrategy
 import org.usvm.SolverType
 import org.usvm.UMachineOptions
@@ -95,7 +96,7 @@ class ComplexReachabilityTest {
         target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf))
 
         // return 1
-        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
+        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[1]
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
@@ -147,6 +148,7 @@ class ComplexReachabilityTest {
         )
     }
 
+    @Disabled("Multiple methods ::process")
     @Test
     fun testConditionalObjectReachable() {
         // Test reachability with conditional object creation and polymorphic method calls
@@ -167,7 +169,7 @@ class ComplexReachabilityTest {
         target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf))
 
         // return 1
-        val return1 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
+        val return1 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[2]
         target.addChild(TsReachabilityTarget.FinalPoint(return1))
 
         // return 2

usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt

@@ -161,7 +161,7 @@ class FunctionCallReachabilityTest {
         target = target.addChild(TsReachabilityTarget.IntermediatePoint(check))
 
         // return 1
-        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
+        val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[1]
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))