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 new file mode 100644 index 0000000000..b65e385010 --- /dev/null +++ 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) + +class UnreachableCodeDetector : TsInterpreterObserver, UMachineObserver { + private val uncoveredSuccessorsOfVisitedIfStmts = hashMapOf>>() + lateinit var result: Map> + + 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) { + 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 new file mode 100644 index 0000000000..43203c52ca --- /dev/null +++ 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 index 972f346c6e..d62c26945f 100644 --- 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? = null, + observer: TsInterpreterObserver? = null, ) : UMachine() { 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 new file mode 100644 index 0000000000..cb2d36d91b --- /dev/null +++ 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 index 8b5e813e0d..d130a6e5c0 100644 --- 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 index fe60350ab7..564ec7b46f 100644 --- 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 class TsInterpreter( private val ctx: TsContext, private val applicationGraph: TsApplicationGraph, + private val tsOptions: TsOptions, + private val observer: TsInterpreterObserver? = null, ) : UInterpreter() { private val forkBlackList: UForkBlackList = 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 index 844ed9963b..1bd8f7acb3 100644 --- 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, - ) : TsMethodResult + sealed class Success(val value: UExpr) : TsMethodResult { + abstract fun methodSignature(): EtsMethodSignature + + /** + * A [method] successfully returned a [value]. + */ + class RegularCall( + val method: EtsMethod, + value: UExpr, + ) : Success(value) { + override fun methodSignature(): EtsMethodSignature = method.signature + } + + class MockedCall( + val methodSignature: EtsMethodSignature, + value: UExpr, + ) : 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 index 13f199cffc..e706047b5f 100644 --- 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) { 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 new file mode 100644 index 0000000000..8d805dfbef --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt @@ -0,0 +1,80 @@ +package org.usvm.samples.checkers + +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsLtExpr +import org.jacodb.ets.model.EtsNumberConstant +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.UMachineOptions +import org.usvm.api.checkers.UnreachableCodeDetector +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath + +class UnreachableCodeDetectorTest { + val scene = run { + val name = "UnreachableCode.ts" + val path = getResourcePath("/samples/checkers/$name") + val file = loadEtsFileAutoConvert( + path, + useArkAnalyzerTypeInference = 1 + ) + EtsScene(listOf(file)) + } + val options = UMachineOptions() + val tsOptions = TsOptions(interproceduralAnalysis = false) + + @Test + fun testUnreachableCode() { + val observer = UnreachableCodeDetector() + val machine = TsMachine(scene, options, tsOptions, observer, observer) + val methods = scene.projectClasses + .flatMap { it.methods } + .filterNot { it.cfg.stmts.isEmpty() } + .filter { it.name == "simpleUnreachableBranch" } + machine.analyze(methods) + + val uncoveredResults = observer.result.values.singleOrNull() ?: error("No results found") + val uncoveredStatements = uncoveredResults.singleOrNull() + + 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().successors.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() + val assignment = stmts.successors.single() as? EtsAssignStmt ?: error("Expected EtsAssignStmt") + val rhv = assignment.rhv as? EtsLtExpr ?: error("Expected EtsLtExpr") + check((rhv.right as EtsNumberConstant).value == 1.0) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index 7b1c9a2bca..449e548a61 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -24,6 +24,7 @@ import org.usvm.api.TsMethodCoverage import org.usvm.api.TsTest import org.usvm.api.TsValue import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions import org.usvm.test.util.TestRunner import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import kotlin.reflect.KClass @@ -215,7 +216,8 @@ abstract class TsMethodTestRunner : TestRunner List = { method, options -> - TsMachine(scene, options).use { machine -> + val tsMachineOptions = TsOptions() + TsMachine(scene, options, tsMachineOptions).use { machine -> val states = machine.analyze(listOf(method)) states.map { state -> val resolver = TsTestResolver() diff --git a/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts b/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts new file mode 100644 index 0000000000..ae8c630171 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts @@ -0,0 +1,26 @@ +class UnreachableCode { + simpleUnreachableBranch(value: number): number { + if (value > 4) { + if (value < 2) { + return -1 + } else { + return 1 + } + } else { + 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 + } +}