Additional tests

Author: CaelmBleidd

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

@@ -162,8 +162,33 @@ class TsInterpreter(
                 is TsMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
                 is TsMethodResult.TsException -> error("Exceptions must be processed earlier")
             }
+
+            if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) {
+                scope.doWithState {
+                    with(ctx) {
+                        val resultSort = typeToSort(it.method.returnType)
+                        val resultValue = when (resultSort) {
+                            is UAddressSort -> makeSymbolicRefUntyped()
+                            is TsUnresolvedSort -> {
+                                mkFakeValue(
+                                    scope,
+                                    makeSymbolicPrimitive(ctx.boolSort),
+                                    makeSymbolicPrimitive(ctx.fp64Sort),
+                                    makeSymbolicRefUntyped()
+                                )
+                            }
+
+                            else -> makeSymbolicPrimitive(resultSort)
+                        }
+                        this@doWithState.methodResult = TsMethodResult.Success.MockedCall(it.method, resultValue)
+                    }
+                }
+                return
+            }
+
         } ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
 
+
         val expr = exprResolver.resolve(stmt.rhv) ?: return
 
         check(expr.sort != unresolvedSort) {

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

@@ -1,5 +1,7 @@
 package org.usvm.samples.checkers
 
+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
@@ -20,11 +22,11 @@ class UnreachableCodeDetectorTest {
         )
         EtsScene(listOf(file))
     }
+    val options = UMachineOptions()
+    val tsOptions = TsOptions(interproceduralAnalysis = false)
 
     @Test
     fun testUnreachableCode() {
-        val options = UMachineOptions()
-        val tsOptions = TsOptions(interproceduralAnalysis = false)
         val observer = UnreachableCodeDetector()
         val machine = TsMachine(scene, options, tsOptions, observer, observer)
         val methods = scene.projectClasses
@@ -38,4 +40,39 @@ class UnreachableCodeDetectorTest {
 
         check(uncoveredStatements != null) { "Uncovered statements are incorrect, results are $uncoveredStatements" }
     }
+
+    @Test
+    fun testUnreachableCodeWithMockedCallsInside() {
+        val observer = UnreachableCodeDetector()
+        val tsOptions = TsOptions(interproceduralAnalysis = false)
+        val machine = TsMachine(scene, options, tsOptions, observer, observer)
+        val methods = scene.projectClasses
+            .flatMap { it.methods }
+            .filter { it.name == "unreachableCodeWithCallsInside" }
+        machine.analyze(methods)
+
+        val results = observer.result.values.singleOrNull() ?: error("No results found")
+        check(results.single().second.single() is EtsAssignStmt)
+    }
+
+    @Test
+    fun testUnreachableCodeCallsInside() {
+        val observer = UnreachableCodeDetector()
+        val tsOptions = TsOptions(interproceduralAnalysis = true)
+        val machine = TsMachine(scene, options, tsOptions, observer, observer)
+        val methodName = "unreachableCodeWithCallsInside"
+        val methods = scene.projectClasses
+            .flatMap { it.methods }
+            .filter { it.name == methodName }
+
+        machine.analyze(methods)
+
+        val results = observer.result.entries
+
+        check(results.size == 2)
+
+        val relatedBranch = results.single { it.key.name == methodName }
+        val stmts = relatedBranch.value.single()
+        check(stmts.second.single() is EtsIfStmt)
+    }
 }

usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts

@@ -10,4 +10,17 @@ class UnreachableCode {
             return 2
         }
     }
+
+    unreachableCodeWithCallsInside(value: number): number {
+        anotherValue = this.simpleUnreachableBranch(value)
+        if (anotherValue > 2) {
+            if (anotherValue < 1) {
+                return -1 // Unreachable code
+            } else {
+                return 1 // Unreachable if we execute simpleUnreachableBranch call and reachable otherwise
+            }
+        }
+
+        return
+    }
 }