TS interpreter observer (#268)

CaelmBleidd · web-flow · commit f5462e677789 · 2025-04-17T17:44:31.000+03:00
diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt b/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt
@@ -0,0 +1,51 @@
+package org.usvm.api.checkers
+
+import org.jacodb.ets.model.EtsIfStmt
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsStmt
+import org.usvm.machine.TsInterpreterObserver
+import org.usvm.machine.expr.TsSimpleValueResolver
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsState
+import org.usvm.statistics.UMachineObserver
+import kotlin.collections.filter
+import kotlin.collections.isNotEmpty
+
+data class UncoveredIfSuccessors(val ifStmt: EtsIfStmt, val successors: Set<EtsStmt>)
+
+class UnreachableCodeDetector : TsInterpreterObserver, UMachineObserver<TsState> {
+    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) {
+        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>) {
+        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
+
+        remainingSuccessorsForCurrentIf -= parent.currentStatement
+        forks.forEach { remainingSuccessorsForCurrentIf -= it.currentStatement }
+    }
+
+    override fun onMachineStopped() {
+        result = uncoveredSuccessorsOfVisitedIfStmts
+            .mapNotNull { (method, uncoveredIfSuccessors) ->
+                uncoveredIfSuccessors
+                    .filter { it.value.isNotEmpty() }
+                    .takeIf { it.isNotEmpty() }
+                    ?.let { ifSucc -> method to ifSucc.map { UncoveredIfSuccessors(it.key, it.value) } }
+            }.toMap()
+    }
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt
@@ -0,0 +1,67 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsAssignStmt
+import org.jacodb.ets.model.EtsCallExpr
+import org.jacodb.ets.model.EtsIfStmt
+import org.jacodb.ets.model.EtsReturnStmt
+import org.jacodb.ets.model.EtsThrowStmt
+import org.usvm.UBoolExpr
+import org.usvm.machine.expr.TsSimpleValueResolver
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.statistics.UInterpreterObserver
+
+@Suppress("unused")
+interface TsInterpreterObserver : UInterpreterObserver {
+    fun onAssignStatement(
+        simpleValueResolver: TsSimpleValueResolver,
+        stmt: EtsAssignStmt,
+        scope: TsStepScope,
+    ) {
+        // default empty implementation
+    }
+
+    // TODO on entry point
+
+    fun onCallWithUnresolvedArguments(
+        simpleValueResolver: TsSimpleValueResolver,
+        stmt: EtsCallExpr,
+        scope: TsStepScope,
+    ) {
+        // default empty implementation
+    }
+
+    // TODO onCallWithResolvedArguments
+
+    fun onIfStatement(
+        simpleValueResolver: TsSimpleValueResolver,
+        stmt: EtsIfStmt,
+        scope: TsStepScope,
+    ) {
+        // default empty implementation
+    }
+
+    fun onIfStatementWithResolvedCondition(
+        simpleValueResolver: TsSimpleValueResolver,
+        stmt: EtsIfStmt,
+        condition: UBoolExpr,
+        scope: TsStepScope,
+    ) {
+        // default empty implementation
+    }
+
+    fun onReturnStatement(
+        simpleValueResolver: TsSimpleValueResolver,
+        stmt: EtsReturnStmt,
+        scope: TsStepScope,
+    ) {
+        // default empty implementation
+    }
+
+    fun onThrowStatement(
+        simpleValueResolver: TsSimpleValueResolver,
+        stmt: EtsThrowStmt,
+        scope: TsStepScope,
+    ) {
+        // default empty implementation
+    }
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -28,12 +28,15 @@ import kotlin.time.Duration.Companion.seconds
 class TsMachine(
     private val project: EtsScene,
     private val options: UMachineOptions,
+    private val tsOptions: TsOptions,
+    private val machineObserver: UMachineObserver<TsState>? = null,
+    observer: TsInterpreterObserver? = null,
 ) : UMachine<TsState>() {
     private val typeSystem = TsTypeSystem(typeOperationsTimeout = 1.seconds, project)
     private val components = TsComponents(typeSystem, options)
     private val ctx = TsContext(project, components)
     private val applicationGraph = TsApplicationGraph(project)
-    private val interpreter = TsInterpreter(ctx, applicationGraph)
+    private val interpreter = TsInterpreter(ctx, applicationGraph, tsOptions, observer)
     private val cfgStatistics = CfgStatisticsImpl(applicationGraph)
 
     fun analyze(
@@ -98,6 +101,7 @@ class TsMachine(
 
         observers.add(timeStatistics)
         observers.add(stepsStatistics)
+        machineObserver?.let { observers.add(it) }
 
         run(
             interpreter,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt
@@ -0,0 +1,5 @@
+package org.usvm.machine
+
+data class TsOptions(
+    val interproceduralAnalysis: Boolean = true,
+)
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
@@ -696,7 +696,7 @@ class TsExprResolver(
                 scope.doWithState {
                     // TODO: Handle static initializer result
                     val result = methodResult
-                    if (result is TsMethodResult.Success && result.method == initializer) {
+                    if (result is TsMethodResult.Success && result.methodSignature() == initializer.signature) {
                         methodResult = TsMethodResult.NoCall
                     }
                 }
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
@@ -9,6 +9,8 @@ import org.jacodb.ets.model.EtsIfStmt
 import org.jacodb.ets.model.EtsInstanceFieldRef
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.utils.callExpr
 import org.jacodb.ets.model.EtsNopStmt
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsParameterRef
@@ -22,13 +24,19 @@ import org.jacodb.ets.model.EtsValue
 import org.jacodb.ets.utils.getDeclaredLocals
 import org.usvm.StepResult
 import org.usvm.StepScope
+import org.usvm.UAddressSort
 import org.usvm.UInterpreter
+import org.usvm.api.makeSymbolicPrimitive
+import org.usvm.api.makeSymbolicRefUntyped
 import org.usvm.api.targets.TsTarget
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.forkblacklists.UForkBlackList
 import org.usvm.machine.TsApplicationGraph
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsInterpreterObserver
+import org.usvm.machine.TsOptions
 import org.usvm.machine.expr.TsExprResolver
+import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.expr.mkTruthyExpr
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
@@ -37,6 +45,7 @@ import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.parametersWithThisCount
 import org.usvm.machine.state.returnValue
+import org.usvm.machine.types.mkFakeValue
 import org.usvm.sizeSort
 import org.usvm.targets.UTargetsSet
 import org.usvm.util.mkArrayIndexLValue
@@ -52,6 +61,8 @@ typealias TsStepScope = StepScope<TsState, EtsType, EtsStmt, TsContext>
 class TsInterpreter(
     private val ctx: TsContext,
     private val applicationGraph: TsApplicationGraph,
+    private val tsOptions: TsOptions,
+    private val observer: TsInterpreterObserver? = null,
 ) : UInterpreter<TsState>() {
 
     private val forkBlackList: UForkBlackList<TsState, EtsStmt> = UForkBlackList.createDefault()
@@ -93,6 +104,10 @@ class TsInterpreter(
 
     private fun visitIfStmt(scope: TsStepScope, stmt: EtsIfStmt) {
         val exprResolver = exprResolverWithScope(scope)
+
+        val simpleValueResolver = exprResolver.simpleValueResolver
+        observer?.onIfStatement(simpleValueResolver, stmt, scope)
+
         val expr = exprResolver.resolve(stmt.condition) ?: return
 
         val boolExpr = if (expr.sort == ctx.boolSort) {
@@ -101,6 +116,8 @@ class TsInterpreter(
             ctx.mkTruthyExpr(expr, scope)
         }
 
+        observer?.onIfStatementWithResolvedCondition(simpleValueResolver, stmt, boolExpr, scope)
+
         val (posStmt, negStmt) = applicationGraph.successors(stmt).take(2).toList()
 
         scope.forkWithBlackList(
@@ -115,6 +132,8 @@ class TsInterpreter(
     private fun visitReturnStmt(scope: TsStepScope, stmt: EtsReturnStmt) {
         val exprResolver = exprResolverWithScope(scope)
 
+        observer?.onReturnStatement(exprResolver.simpleValueResolver, stmt, scope)
+
         val valueToReturn = stmt.returnValue
             ?.let { exprResolver.resolve(it) ?: return }
             ?: ctx.mkUndefinedValue()
@@ -126,6 +145,28 @@ class TsInterpreter(
 
     private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) = with(ctx) {
         val exprResolver = exprResolverWithScope(scope)
+
+        stmt.callExpr?.let {
+            val methodResult = scope.calcOnState { methodResult }
+
+            when (methodResult) {
+                is TsMethodResult.NoCall -> observer?.onCallWithUnresolvedArguments(
+                    exprResolver.simpleValueResolver,
+                    it,
+                    scope
+                )
+
+                is TsMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
+                is TsMethodResult.TsException -> error("Exceptions must be processed earlier")
+            }
+
+            if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) {
+                mockMethodCall(scope, it.callee)
+                return
+            }
+        } ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
+
+
         val expr = exprResolver.resolve(stmt.rhv) ?: return
 
         check(expr.sort != unresolvedSort) {
@@ -222,16 +263,33 @@ class TsInterpreter(
 
     private fun visitCallStmt(scope: TsStepScope, stmt: EtsCallStmt) {
         val exprResolver = exprResolverWithScope(scope)
-        exprResolver.resolve(stmt.expr) ?: return
 
         scope.doWithState {
-            val nextStmt = stmt.nextStmt ?: return@doWithState
-            newStmt(nextStmt)
+            if (methodResult is TsMethodResult.Success) {
+                newStmt(applicationGraph.successors(stmt).single())
+                methodResult = TsMethodResult.NoCall
+            }
         }
+
+        if (tsOptions.interproceduralAnalysis) {
+            exprResolver.resolve(stmt.expr) ?: return
+
+            scope.doWithState {
+                val nextStmt = stmt.nextStmt ?: return@doWithState
+                newStmt(nextStmt)
+            }
+
+            return
+        }
+
+        // intraprocedural analysis
+        mockMethodCall(scope, stmt.method.signature)
     }
 
     private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) {
         // TODO do not forget to pop the sorts call stack in the state
+        val exprResolver = exprResolverWithScope(scope)
+        observer?.onThrowStatement(exprResolver.simpleValueResolver, stmt, scope)
         TODO()
     }
 
@@ -307,6 +365,28 @@ class TsInterpreter(
         return state
     }
 
+    private fun mockMethodCall(scope: TsStepScope, method: EtsMethodSignature) {
+        scope.doWithState {
+            with(ctx) {
+                val resultSort = typeToSort(method.returnType)
+                val resultValue = when (resultSort) {
+                    is UAddressSort -> makeSymbolicRefUntyped()
+                    is TsUnresolvedSort -> {
+                        mkFakeValue(
+                            scope,
+                            makeSymbolicPrimitive(ctx.boolSort),
+                            makeSymbolicPrimitive(ctx.fp64Sort),
+                            makeSymbolicRefUntyped()
+                        )
+                    }
+
+                    else -> makeSymbolicPrimitive(resultSort)
+                }
+                methodResult = TsMethodResult.Success.MockedCall(method, resultValue)
+            }
+        }
+    }
+
     // TODO: expand with interpreter implementation
     private val EtsStmt.nextStmt: EtsStmt?
         get() = applicationGraph.successors(this).firstOrNull()
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt
@@ -1,6 +1,7 @@
 package org.usvm.machine.state
 
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsMethodSignature
 import org.jacodb.ets.model.EtsType
 import org.usvm.UExpr
 import org.usvm.UHeapRef
@@ -15,13 +16,26 @@ sealed interface TsMethodResult {
      */
     object NoCall : TsMethodResult
 
-    /**
-     * A [method] successfully returned a [value].
-     */
-    class Success(
-        val method: EtsMethod,
-        val value: UExpr<out USort>,
-    ) : TsMethodResult
+    sealed class Success(val value: UExpr<out USort>) : TsMethodResult {
+        abstract fun methodSignature(): EtsMethodSignature
+
+        /**
+         * A [method] successfully returned a [value].
+         */
+        class RegularCall(
+            val method: EtsMethod,
+            value: UExpr<out USort>,
+        ) : Success(value) {
+            override fun methodSignature(): EtsMethodSignature = method.signature
+        }
+
+        class MockedCall(
+            val methodSignature: EtsMethodSignature,
+            value: UExpr<out USort>,
+        ) : Success(value) {
+            override fun methodSignature(): EtsMethodSignature = methodSignature
+        }
+    }
 
     /**
      * A method threw an exception with [type] type.
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt
@@ -20,7 +20,7 @@ fun TsState.returnValue(valueToReturn: UExpr<out USort>) {
         popLocalToSortStack()
     }
 
-    methodResult = TsMethodResult.Success(returnFromMethod, valueToReturn)
+    methodResult = TsMethodResult.Success.RegularCall(returnFromMethod, valueToReturn)
 
     if (returnSite != null) {
         newStmt(returnSite)
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
diff --git a/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts b/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts

Original file line number	Diff line number	Diff line change
`@@ -696,7 +696,7 @@ class TsExprResolver(`
`696`	`696`	`scope.doWithState {`
`697`	`697`	`// TODO: Handle static initializer result`
`698`	`698`	`val result = methodResult`
`699`		`- if (result is TsMethodResult.Success && result.method == initializer) {`
	`699`	`+ if (result is TsMethodResult.Success && result.methodSignature() == initializer.signature) {`
`700`	`700`	`methodResult = TsMethodResult.NoCall`
`701`	`701`	`}`
`702`	`702`	`}`
Original file line number	Diff line number	Diff line change
`@@ -20,7 +20,7 @@ fun TsState.returnValue(valueToReturn: UExpr<out USort>) {`
`20`	`20`	`popLocalToSortStack()`
`21`	`21`	`}`
`22`	`22`
`23`		`- methodResult = TsMethodResult.Success(returnFromMethod, valueToReturn)`
	`23`	`+ methodResult = TsMethodResult.Success.RegularCall(returnFromMethod, valueToReturn)`
`24`	`24`
`25`	`25`	`if (returnSite != null) {`
`26`	`26`	`newStmt(returnSite)`