[TS] Reachability prototype (#308)

Author: CaelmBleidd

usvm-ts/src/main/kotlin/org/usvm/api/targets/ReachabilityObserver.kt

@@ -0,0 +1,38 @@
+package org.usvm.api.targets
+
+import org.usvm.machine.state.TsState
+import org.usvm.statistics.UMachineObserver
+
+class ReachabilityObserver : UMachineObserver<TsState> {
+    override fun onState(parent: TsState, forks: Sequence<TsState>) {
+        parent
+            .targets
+            .filter { it is TsReachabilityTarget }
+            .forEach { target ->
+                if (target.location == parent.pathNode.parent?.statement) {
+                    target.propagate(parent)
+                }
+            }
+
+        forks.forEach { fork ->
+            fork
+                .targets
+                .filter { it is TsReachabilityTarget }
+                .forEach { target ->
+                    if (target.location == fork.pathNode.parent?.statement) {
+                        target.propagate(fork)
+                    }
+                }
+        }
+    }
+
+    override fun onStateTerminated(state: TsState, stateReachable: Boolean) {
+        state.targets
+            .filter { it is TsReachabilityTarget }
+            .forEach { target ->
+                if (target.location == state.pathNode.statement) {
+                    target.propagate(state)
+                }
+            }
+    }
+}

usvm-ts/src/main/kotlin/org/usvm/api/targets/TsTarget.kt

@@ -3,4 +3,10 @@ package org.usvm.api.targets
 import org.jacodb.ets.model.EtsStmt
 import org.usvm.targets.UTarget
 
-class TsTarget : UTarget<EtsStmt, TsTarget>()
+open class TsTarget(location: EtsStmt?) : UTarget<EtsStmt, TsTarget>(location)
+
+sealed class TsReachabilityTarget(override val location: EtsStmt) : TsTarget(location) {
+    class InitialPoint(location: EtsStmt) : TsReachabilityTarget(location)
+    class IntermediatePoint(location: EtsStmt) : TsReachabilityTarget(location)
+    class FinalPoint(location: EtsStmt) : TsReachabilityTarget(location)
+}

usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt

@@ -0,0 +1,66 @@
+package org.usvm.checkers
+
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.usvm.PathSelectionStrategy
+import org.usvm.UMachineOptions
+import org.usvm.api.targets.ReachabilityObserver
+import org.usvm.api.targets.TsReachabilityTarget
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.util.getResourcePath
+import kotlin.test.Test
+import kotlin.time.Duration.Companion.seconds
+
+class ReachabilityChecker {
+    val scene = run {
+        val name = "ReachabilityChecker.ts"
+        val path = getResourcePath("/checkers/$name")
+        val file = loadEtsFileAutoConvert(path)
+        EtsScene(listOf(file))
+    }
+    val options = UMachineOptions(
+        stopOnTargetsReached = true,
+        pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
+        timeout = 15000000.seconds
+    )
+    val tsOptions = TsOptions()
+
+    @Test
+    fun runReachabilityCheck() {
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "simpleFunction" }
+
+        val initialPoint = method.cfg.stmts.first { "if (" in it.toString() }
+        val initialTarget = TsReachabilityTarget.InitialPoint(initialPoint)
+
+        val intermediatePoint = method.cfg.stmts.filter { "if (" in it.toString() }[1]
+        val intermediateTarget = TsReachabilityTarget.IntermediatePoint(intermediatePoint).also {
+            initialTarget.addChild((it))
+        }
+        val finalPoint = method.cfg.stmts.first { "return" in it.toString() }
+        TsReachabilityTarget.FinalPoint(finalPoint).also {
+            intermediateTarget.addChild(it)
+        }
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        require(results.size == 1) { "Expected exactly one result, but got ${results.size}" }
+    }
+
+    @Test
+    fun runReachabilityCheckForFirstInstruction() {
+        val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "simpleFunction" }
+
+        val initialPoint = method.cfg.stmts.first()
+        val initialTarget = TsReachabilityTarget.InitialPoint(initialPoint)
+
+        val results = machine.analyze(listOf(method), listOf(initialTarget))
+        require(results.isEmpty()) { "Expected no analysis results, but got ${results.size}" }
+        require(initialTarget.isRemoved) { "Expected initial target to be removed, but it was not" }
+    }
+}

usvm-ts/src/test/resources/checkers/ReachabilityChecker.ts

@@ -0,0 +1,14 @@
+class ReachabilityChecker {
+    // A target for this function will be 'if(x) -> if (y > 14) -> return 1'
+    simpleFunction(x: boolean, y: number): number {
+        if (x) {
+            if (y > 14) {
+                return 1;
+            } else {
+                return 2;
+            }
+        } else {
+            return 3;
+        }
+    }
+}