Simplify detector

Author: CaelmBleidd

usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt

@@ -9,44 +9,41 @@ import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsState
 import org.usvm.statistics.UMachineObserver
 
+data class UncoveredIfSuccessors(val ifStmt: EtsIfStmt, val successors: Set<EtsStmt>)
+
 class UnreachableCodeDetector : TsInterpreterObserver, UMachineObserver<TsState> {
-    private val uncoveredIfSuccessors = hashMapOf<EtsMethod, MutableSet<EtsStmt>>()
-    private val allIfSuccessors = hashMapOf<EtsMethod, MutableSet<EtsStmt>>()
-    private val visitedIfStmt = hashMapOf<EtsMethod, MutableSet<EtsIfStmt>>()
-
-    lateinit var result: Map<EtsMethod, Set<Pair<EtsIfStmt, Set<EtsStmt>>>>
-
-    override fun onStatePeeked(state: TsState) {
-        val method = state.currentStatement.method
-        if (method !in allIfSuccessors) {
-            val ifSuccessors = method.cfg.stmts
-                .filter { it is EtsIfStmt }
-                .flatMapTo(hashSetOf()) { method.cfg.successors(it) }
-            allIfSuccessors[method] = ifSuccessors
-            uncoveredIfSuccessors[method] = ifSuccessors.toHashSet()
-        }
-    }
+    private val uncoveredSuccessorsOfVisitedIfStmts = hashMapOf<EtsMethod, MutableMap<EtsIfStmt, MutableSet<EtsStmt>>>()
+    lateinit var result: Map<EtsMethod, List<UncoveredIfSuccessors>>
 
     override fun onIfStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, scope: TsStepScope) {
-        visitedIfStmt.getOrPut(stmt.method) { hashSetOf() }.add(stmt)
+        val ifStmts = uncoveredSuccessorsOfVisitedIfStmts.getOrPut(stmt.method) { mutableMapOf() }
+        // We've already added its successors in the map
+        if (stmt in ifStmts) return
+
+        val successors = stmt.method.cfg.successors(stmt)
+        ifStmts[stmt] = successors.toMutableSet()
     }
 
     override fun onState(parent: TsState, forks: Sequence<TsState>) {
-        if (parent.pathNode.parent?.statement !is EtsIfStmt) return
+        val previousStatement = parent.pathNode.parent?.statement
+        if (previousStatement !is EtsIfStmt) return
+
+        val method = parent.currentStatement.method
+        val remainingUncoveredIfSuccessors = uncoveredSuccessorsOfVisitedIfStmts.getValue(method)
+        val remainingSuccessorsForCurrentIf = remainingUncoveredIfSuccessors[previousStatement]
+            ?: return // No uncovered successors for this if statement
 
-        val currentIfSuccessors = uncoveredIfSuccessors.getValue(parent.currentStatement.method)
-        currentIfSuccessors -= parent.currentStatement
-        forks.forEach { currentIfSuccessors -= it.currentStatement }
+        remainingSuccessorsForCurrentIf -= parent.currentStatement
+        forks.forEach { remainingSuccessorsForCurrentIf -= it.currentStatement }
     }
 
     override fun onMachineStopped() {
-        result = uncoveredIfSuccessors.mapNotNull { (method, values) ->
-            val visitedIfs = visitedIfStmt[method] ?: return@mapNotNull null
-            val grouped = values.groupBy { method.cfg.predecessors(it).single() }
-                .map { it.key as EtsIfStmt to it.value.toSet() }
-                .filter { it.first in visitedIfs }
-                .toSet()
-            method to grouped
-        }.toMap()
+        result = uncoveredSuccessorsOfVisitedIfStmts
+            .mapNotNull { (method, uncoveredIfSuccessors) ->
+                uncoveredIfSuccessors
+                    .filter { it.value.isNotEmpty() }
+                    .takeIf { it.isNotEmpty() }
+                    ?.let { method to it.map { UncoveredIfSuccessors(it.key, it.value) } }
+            }.toMap()
     }
 }

usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt

@@ -4,7 +4,6 @@ import org.jacodb.ets.base.EtsAssignStmt
 import org.jacodb.ets.base.EtsIfStmt
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
-import org.jacodb.ets.utils.loadEtsProjectFromIR
 import org.junit.jupiter.api.Test
 import org.usvm.UMachineOptions
 import org.usvm.api.checkers.UnreachableCodeDetector
@@ -52,7 +51,7 @@ class UnreachableCodeDetectorTest {
         machine.analyze(methods)
 
         val results = observer.result.values.singleOrNull() ?: error("No results found")
-        check(results.single().second.single() is EtsAssignStmt)
+        check(results.single().successors.single() is EtsAssignStmt)
     }
 
     @Test
@@ -73,6 +72,6 @@ class UnreachableCodeDetectorTest {
 
         val relatedBranch = results.single { it.key.name == methodName }
         val stmts = relatedBranch.value.single()
-        check(stmts.second.single() is EtsIfStmt)
+        check(stmts.successors.single() is EtsIfStmt)
     }
 }