From 60ca88bb4934151acef6c948fedbdf9b331650d8 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 20 Mar 2025 15:28:23 +0300 Subject: [PATCH 01/15] Add observer implementation --- .../org/usvm/machine/TsInterpreterObserver.kt | 25 ++++++++++++++++++ .../usvm/machine/interpreter/TsInterpreter.kt | 26 +++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt 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..cf0a5cec05 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -0,0 +1,25 @@ +package org.usvm.machine + +import org.jacodb.ets.base.EtsAssignStmt +import org.jacodb.ets.base.EtsCallExpr +import org.jacodb.ets.base.EtsGotoStmt +import org.jacodb.ets.base.EtsIfStmt +import org.jacodb.ets.base.EtsReturnStmt +import org.jacodb.ets.base.EtsSwitchStmt +import org.jacodb.ets.base.EtsThrowStmt +import org.usvm.machine.expr.TsSimpleValueResolver +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.statistics.UInterpreterObserver + +@Suppress("unused") +class TsInterpreterObserver : UInterpreterObserver { + fun onAssignStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsAssignStmt, stepScope: TsStepScope) {} + // TODO on entry point + fun onCallWithUnresolvedArguments(simpleValueResolver: TsSimpleValueResolver, stmt: EtsCallExpr, stepScope: TsStepScope) {} + // TODO onCallWithResolvedArguments + fun onIfStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, stepScope: TsStepScope) {} + fun onReturnStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsReturnStmt, stepScope: TsStepScope) {} + fun onThrowStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsThrowStmt, stepScope: TsStepScope) {} + fun onGotoStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsGotoStmt, stepScope: TsStepScope) {} + fun onSwitchStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsSwitchStmt, stepScope: TsStepScope) {} +} \ No newline at end of file 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..c212c852ba 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,7 @@ 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.utils.callExpr import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsParameterRef @@ -28,6 +29,7 @@ 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.expr.TsExprResolver import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.state.TsMethodResult @@ -52,6 +54,7 @@ typealias TsStepScope = StepScope class TsInterpreter( private val ctx: TsContext, private val applicationGraph: TsApplicationGraph, + private val observer: TsInterpreterObserver? = null, ) : UInterpreter() { private val forkBlackList: UForkBlackList = UForkBlackList.createDefault() @@ -93,6 +96,9 @@ class TsInterpreter( private fun visitIfStmt(scope: TsStepScope, stmt: EtsIfStmt) { val exprResolver = exprResolverWithScope(scope) + + observer?.onIfStatement(exprResolver.simpleValueResolver, stmt, scope) + val expr = exprResolver.resolve(stmt.condition) ?: return val boolExpr = if (expr.sort == ctx.boolSort) { @@ -115,6 +121,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 +134,22 @@ 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") + } + } ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) + val expr = exprResolver.resolve(stmt.rhv) ?: return check(expr.sort != unresolvedSort) { @@ -232,6 +256,8 @@ class TsInterpreter( 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() } From c6cba2c0d17d1c82b170fb7407f8d5b245933f7b Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 25 Mar 2025 16:15:02 +0300 Subject: [PATCH 02/15] Add detector --- .../api/checkers/UnreachableCodeDetector.kt | 52 +++++++++++++++++++ .../org/usvm/machine/TsInterpreterObserver.kt | 18 ++++--- .../main/kotlin/org/usvm/machine/TsMachine.kt | 6 ++- .../main/kotlin/org/usvm/machine/TsOptions.kt | 5 ++ .../org/usvm/machine/expr/TsExprResolver.kt | 2 +- .../usvm/machine/interpreter/TsInterpreter.kt | 43 +++++++++++++-- .../org/usvm/machine/state/TsMethodResult.kt | 29 ++++++++--- .../org/usvm/machine/state/TsStateUtils.kt | 2 +- .../checkers/UnreachableCodeDetector.kt | 36 +++++++++++++ .../org/usvm/util/TsMethodTestRunner.kt | 4 +- .../samples/checkers/UnreachableCode.ts | 13 +++++ 11 files changed, 187 insertions(+), 23 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt create mode 100644 usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts 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..556a471823 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt @@ -0,0 +1,52 @@ +package org.usvm.api.checkers + +import org.jacodb.ets.base.EtsIfStmt +import org.jacodb.ets.base.EtsStmt +import org.jacodb.ets.model.EtsMethod +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 + +class UnreachableCodeDetector : TsInterpreterObserver, UMachineObserver { + private val uncoveredIfSuccessors = hashMapOf>() + private val allIfSuccessors = hashMapOf>() + private val visitedIfStmt = hashMapOf>() + + lateinit var result: Map>>> + + 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() + } + } + + override fun onIfStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, scope: TsStepScope) { + visitedIfStmt.getOrPut(stmt.method) { hashSetOf() }.add(stmt) + } + + override fun onState(parent: TsState, forks: Sequence) { + if (parent.pathNode.parent?.statement !is EtsIfStmt) return + + val currentIfSuccessors = uncoveredIfSuccessors.getValue(parent.currentStatement.method) + currentIfSuccessors -= parent.currentStatement + forks.forEach { currentIfSuccessors -= it.currentStatement } + } + + override fun onMachineStopped() { + result = uncoveredIfSuccessors.map { (method, values) -> + val visitedIfs = visitedIfStmt.getValue(method) + val values = values.groupBy { method.cfg.predecessors(it).single() } + .map { it.key as EtsIfStmt to it.value.toSet() } + .filter { it.first in visitedIfs } + .toSet() + method to values + }.toMap() + } +} \ No newline at end of file diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index cf0a5cec05..a46d733fb1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -7,19 +7,21 @@ import org.jacodb.ets.base.EtsIfStmt import org.jacodb.ets.base.EtsReturnStmt import org.jacodb.ets.base.EtsSwitchStmt import org.jacodb.ets.base.EtsThrowStmt +import org.usvm.UBoolExpr import org.usvm.machine.expr.TsSimpleValueResolver import org.usvm.machine.interpreter.TsStepScope import org.usvm.statistics.UInterpreterObserver @Suppress("unused") -class TsInterpreterObserver : UInterpreterObserver { - fun onAssignStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsAssignStmt, stepScope: TsStepScope) {} +interface TsInterpreterObserver : UInterpreterObserver { + fun onAssignStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsAssignStmt, scope: TsStepScope) {} // TODO on entry point - fun onCallWithUnresolvedArguments(simpleValueResolver: TsSimpleValueResolver, stmt: EtsCallExpr, stepScope: TsStepScope) {} + fun onCallWithUnresolvedArguments(simpleValueResolver: TsSimpleValueResolver, stmt: EtsCallExpr, scope: TsStepScope) {} // TODO onCallWithResolvedArguments - fun onIfStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, stepScope: TsStepScope) {} - fun onReturnStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsReturnStmt, stepScope: TsStepScope) {} - fun onThrowStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsThrowStmt, stepScope: TsStepScope) {} - fun onGotoStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsGotoStmt, stepScope: TsStepScope) {} - fun onSwitchStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsSwitchStmt, stepScope: TsStepScope) {} + fun onIfStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, scope: TsStepScope) {} + fun onIfStatementWithResolvedCondition(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, condition: UBoolExpr, scope: TsStepScope) {} + fun onReturnStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsReturnStmt, scope: TsStepScope) {} + fun onThrowStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsThrowStmt, scope: TsStepScope) {} + fun onGotoStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsGotoStmt, scope: TsStepScope) {} + fun onSwitchStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsSwitchStmt, scope: TsStepScope) {} } \ No newline at end of file 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..7038c30230 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..7c6ee93084 --- /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 = false +) \ No newline at end of file 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 c212c852ba..24dbfd678f 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 @@ -23,14 +23,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 @@ -39,6 +44,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 @@ -54,6 +60,7 @@ typealias TsStepScope = StepScope class TsInterpreter( private val ctx: TsContext, private val applicationGraph: TsApplicationGraph, + private val tsOptions: TsOptions, private val observer: TsInterpreterObserver? = null, ) : UInterpreter() { @@ -97,7 +104,8 @@ class TsInterpreter( private fun visitIfStmt(scope: TsStepScope, stmt: EtsIfStmt) { val exprResolver = exprResolverWithScope(scope) - observer?.onIfStatement(exprResolver.simpleValueResolver, stmt, scope) + val simpleValueResolver = exprResolver.simpleValueResolver + observer?.onIfStatement(simpleValueResolver, stmt, scope) val expr = exprResolver.resolve(stmt.condition) ?: return @@ -107,6 +115,8 @@ class TsInterpreter( ctx.mkTruthyExpr(expr, scope) } + observer?.onIfStatementWithResolvedCondition(simpleValueResolver, stmt, boolExpr, scope) + val (posStmt, negStmt) = applicationGraph.successors(stmt).take(2).toList() scope.forkWithBlackList( @@ -246,11 +256,36 @@ class TsInterpreter( private fun visitCallStmt(scope: TsStepScope, stmt: EtsCallStmt) { val exprResolver = exprResolverWithScope(scope) - exprResolver.resolve(stmt.expr) ?: return + if (tsOptions.interproceduralAnalysis) { + exprResolver.resolve(stmt.expr) ?: return + + scope.doWithState { + val nextStmt = stmt.nextStmt ?: return@doWithState + newStmt(nextStmt) + } + + return + } + + // intraprocedural analysis scope.doWithState { - val nextStmt = stmt.nextStmt ?: return@doWithState - newStmt(nextStmt) + with(ctx) { + val resultSort = typeToSort(stmt.expr.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(stmt.expr.method, resultValue) + } } } 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..8b5f24db52 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,27 @@ 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..f4e7db6e76 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt @@ -0,0 +1,36 @@ +package org.usvm.samples.checkers + +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 +import kotlin.test.assertTrue + + +class UnreachableCodeDetectorTest { + @Test + fun testUnreachableCode() { + 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) + val observer = UnreachableCodeDetector() + val machine = TsMachine(scene, options, tsOptions, observer, observer) + val methods = scene.projectClasses.flatMap { it.methods }.filter { it.name == "simpleUnreachableBranch" } + val results = machine.analyze(methods) + + check(results.isNotEmpty()) + } +} \ No newline at end of file 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..a4e291a09e --- /dev/null +++ b/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts @@ -0,0 +1,13 @@ +class UnreachableCode { + simpleUnreachableBranch(value: number): number { + if (value > 4) { + if (value < 2) { + return -1 + } else { + return 1 + } + } else { + return 2 + } + } +} \ No newline at end of file From 3fccf0691c84b629799c66bc3db4a8223cfbbcaf Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 25 Mar 2025 17:29:37 +0300 Subject: [PATCH 03/15] Fix tests --- usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt | 2 +- .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index 7c6ee93084..a5cf2f452d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -1,5 +1,5 @@ package org.usvm.machine data class TsOptions( - val interproceduralAnalysis: Boolean = false + val interproceduralAnalysis: Boolean = true ) \ No newline at end of file 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 24dbfd678f..7d8b7fe8e9 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 @@ -257,6 +257,13 @@ class TsInterpreter( private fun visitCallStmt(scope: TsStepScope, stmt: EtsCallStmt) { val exprResolver = exprResolverWithScope(scope) + scope.doWithState { + if (methodResult is TsMethodResult.Success) { + newStmt(applicationGraph.successors(stmt).single()) + methodResult = TsMethodResult.NoCall + } + } + if (tsOptions.interproceduralAnalysis) { exprResolver.resolve(stmt.expr) ?: return From a18c572c5ded4fb3aa11e4b4cf351c3ff6c7b445 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 26 Mar 2025 17:31:05 +0300 Subject: [PATCH 04/15] Format --- .../main/kotlin/org/usvm/machine/TsInterpreterObserver.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt | 4 ++-- .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 1 + .../main/kotlin/org/usvm/machine/state/TsMethodResult.kt | 3 +-- .../org/usvm/samples/checkers/UnreachableCodeDetector.kt | 6 ++---- 6 files changed, 8 insertions(+), 10 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index a46d733fb1..daccb017a1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -24,4 +24,4 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onThrowStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsThrowStmt, scope: TsStepScope) {} fun onGotoStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsGotoStmt, scope: TsStepScope) {} fun onSwitchStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsSwitchStmt, scope: TsStepScope) {} -} \ No newline at end of file +} 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 7038c30230..d62c26945f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -30,7 +30,7 @@ class TsMachine( private val options: UMachineOptions, private val tsOptions: TsOptions, private val machineObserver: UMachineObserver? = null, - observer: TsInterpreterObserver? = null + observer: TsInterpreterObserver? = null, ) : UMachine() { private val typeSystem = TsTypeSystem(typeOperationsTimeout = 1.seconds, project) private val components = TsComponents(typeSystem, options) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index a5cf2f452d..cb2d36d91b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -1,5 +1,5 @@ package org.usvm.machine data class TsOptions( - val interproceduralAnalysis: Boolean = true -) \ No newline at end of file + val interproceduralAnalysis: Boolean = true, +) 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 7d8b7fe8e9..0fd4cae66c 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 @@ -289,6 +289,7 @@ class TsInterpreter( makeSymbolicRefUntyped() ) } + else -> makeSymbolicPrimitive(resultSort) } methodResult = TsMethodResult.Success.MockedCall(stmt.expr.method, resultValue) 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 8b5f24db52..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 @@ -16,9 +16,9 @@ sealed interface TsMethodResult { */ object NoCall : TsMethodResult - sealed class Success(val value: UExpr) : TsMethodResult { abstract fun methodSignature(): EtsMethodSignature + /** * A [method] successfully returned a [value]. */ @@ -37,7 +37,6 @@ sealed interface TsMethodResult { } } - /** * A method threw an exception with [type] type. */ 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 index f4e7db6e76..6d94c7e6da 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt @@ -8,13 +8,11 @@ import org.usvm.api.checkers.UnreachableCodeDetector import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.getResourcePath -import kotlin.test.assertTrue - class UnreachableCodeDetectorTest { @Test fun testUnreachableCode() { - val scene = run { + val scene = run { val name = "UnreachableCode.ts" val path = getResourcePath("/samples/checkers/$name") val file = loadEtsFileAutoConvert( @@ -33,4 +31,4 @@ class UnreachableCodeDetectorTest { check(results.isNotEmpty()) } -} \ No newline at end of file +} From c66537e8f3922102e6419284ffd5557baf9334c7 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 26 Mar 2025 17:43:38 +0300 Subject: [PATCH 05/15] Fix --- .../org/usvm/api/checkers/UnreachableCodeDetector.kt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 index 556a471823..31f42d4515 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt @@ -40,13 +40,13 @@ class UnreachableCodeDetector : TsInterpreterObserver, UMachineObserver } override fun onMachineStopped() { - result = uncoveredIfSuccessors.map { (method, values) -> - val visitedIfs = visitedIfStmt.getValue(method) - val values = values.groupBy { method.cfg.predecessors(it).single() } + 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 values + method to grouped }.toMap() } -} \ No newline at end of file +} From 93bd9e05883e9e8e0b2e8465bf72b682f1eca5a1 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 26 Mar 2025 17:44:43 +0300 Subject: [PATCH 06/15] Run on real project, filter out methods with empty cfg --- .../checkers/UnreachableCodeDetector.kt | 29 +++++++++++-------- 1 file changed, 17 insertions(+), 12 deletions(-) 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 index 6d94c7e6da..6221d0eecc 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt @@ -1,7 +1,6 @@ package org.usvm.samples.checkers -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 @@ -12,21 +11,27 @@ import org.usvm.util.getResourcePath class UnreachableCodeDetectorTest { @Test fun testUnreachableCode() { - val scene = run { - val name = "UnreachableCode.ts" - val path = getResourcePath("/samples/checkers/$name") - val file = loadEtsFileAutoConvert( - path, - useArkAnalyzerTypeInference = 1 - ) - EtsScene(listOf(file)) - } + // val scene = run { + // val name = "UnreachableCode.ts" + // val path = getResourcePath("/samples/checkers/$name") + // val file = loadEtsFileAutoConvert( + // path, + // useArkAnalyzerTypeInference = 1 + // ) + // EtsScene(listOf(file)) + // } + + val path = getResourcePath("/projects/Demo_Calc/etsir") + val scene = loadEtsProjectFromIR(path, null) val options = UMachineOptions() val tsOptions = TsOptions(interproceduralAnalysis = false) val observer = UnreachableCodeDetector() val machine = TsMachine(scene, options, tsOptions, observer, observer) - val methods = scene.projectClasses.flatMap { it.methods }.filter { it.name == "simpleUnreachableBranch" } + val methods = scene.projectClasses + .flatMap { it.methods } + .filterNot { it.cfg.stmts.isEmpty() } + //.filter { it.name == "simpleUnreachableBranch" } val results = machine.analyze(methods) check(results.isNotEmpty()) From 026d98082eae297f4a5212387f058ee0aa8bb9e0 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 16 Apr 2025 12:32:18 +0300 Subject: [PATCH 07/15] Fix tests --- .../checkers/UnreachableCodeDetector.kt | 23 +++++++++---------- 1 file changed, 11 insertions(+), 12 deletions(-) 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 index 6221d0eecc..ba226fbe40 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt @@ -1,5 +1,7 @@ package org.usvm.samples.checkers +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 @@ -11,18 +13,15 @@ import org.usvm.util.getResourcePath class UnreachableCodeDetectorTest { @Test fun testUnreachableCode() { - // val scene = run { - // val name = "UnreachableCode.ts" - // val path = getResourcePath("/samples/checkers/$name") - // val file = loadEtsFileAutoConvert( - // path, - // useArkAnalyzerTypeInference = 1 - // ) - // EtsScene(listOf(file)) - // } - - val path = getResourcePath("/projects/Demo_Calc/etsir") - val scene = loadEtsProjectFromIR(path, null) + 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) From 6c80308046f89eefaefcff3420a8827f961aed9a Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 16 Apr 2025 13:12:37 +0300 Subject: [PATCH 08/15] Tests update --- .../checkers/UnreachableCodeDetector.kt | 29 ++++++++++--------- 1 file changed, 16 insertions(+), 13 deletions(-) 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 index ba226fbe40..15278cba04 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt @@ -11,18 +11,18 @@ 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)) + } + @Test fun testUnreachableCode() { - 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) val observer = UnreachableCodeDetector() @@ -30,9 +30,12 @@ class UnreachableCodeDetectorTest { val methods = scene.projectClasses .flatMap { it.methods } .filterNot { it.cfg.stmts.isEmpty() } - //.filter { it.name == "simpleUnreachableBranch" } - val results = machine.analyze(methods) + .filter { it.name == "simpleUnreachableBranch" } + machine.analyze(methods) + + val uncoveredResults = observer.result.values.singleOrNull() ?: error("No results found") + val uncoveredStatements = uncoveredResults.singleOrNull() - check(results.isNotEmpty()) + check(uncoveredStatements != null) { "Uncovered statements are incorrect, results are $uncoveredStatements" } } } From 051c0abce2b5c673449f407253485f78e40cc535 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 16 Apr 2025 17:34:50 +0300 Subject: [PATCH 09/15] Additional tests --- .../usvm/machine/interpreter/TsInterpreter.kt | 25 +++++++++++ .../checkers/UnreachableCodeDetector.kt | 41 ++++++++++++++++++- .../samples/checkers/UnreachableCode.ts | 13 ++++++ 3 files changed, 77 insertions(+), 2 deletions(-) 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 0fd4cae66c..0ec745c0e1 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 @@ -158,8 +158,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) { 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 index 15278cba04..d1c1891827 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt +++ b/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) + } } diff --git a/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts b/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts index a4e291a09e..debbf83ffd 100644 --- a/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts +++ b/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 + } } \ No newline at end of file From fa86cb95d4e6c03f0e15f79ec157e23467c2b29a Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 16 Apr 2025 17:44:06 +0300 Subject: [PATCH 10/15] Extract mock method --- .../usvm/machine/interpreter/TsInterpreter.kt | 63 ++++++++----------- 1 file changed, 25 insertions(+), 38 deletions(-) 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 0ec745c0e1..0340376817 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,7 @@ 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 @@ -160,25 +161,7 @@ class TsInterpreter( } 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) - } - } + mockMethodCall(scope, it.method) return } @@ -301,25 +284,7 @@ class TsInterpreter( } // intraprocedural analysis - scope.doWithState { - with(ctx) { - val resultSort = typeToSort(stmt.expr.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(stmt.expr.method, resultValue) - } - } + mockMethodCall(scope, stmt.method.signature) } private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) { @@ -401,6 +366,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() From 3191cad9191dbaae612009c126aff128c52702f1 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Wed, 16 Apr 2025 18:22:41 +0300 Subject: [PATCH 11/15] Simplify detector --- .../api/checkers/UnreachableCodeDetector.kt | 55 +++++++++---------- .../checkers/UnreachableCodeDetector.kt | 5 +- 2 files changed, 28 insertions(+), 32 deletions(-) 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 index 31f42d4515..d78de9f1fc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt +++ b/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) + class UnreachableCodeDetector : TsInterpreterObserver, UMachineObserver { - private val uncoveredIfSuccessors = hashMapOf>() - private val allIfSuccessors = hashMapOf>() - private val visitedIfStmt = hashMapOf>() - - lateinit var result: Map>>> - - 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>>() + lateinit var result: Map> 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) { - 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() } } 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 index d1c1891827..31cf388549 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt +++ b/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) } } From fc89ae644a571e51fe36c01319695e693d702a22 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 17 Apr 2025 11:42:25 +0300 Subject: [PATCH 12/15] Style fixes --- .../api/checkers/UnreachableCodeDetector.kt | 2 +- .../org/usvm/machine/TsInterpreterObserver.kt | 74 +++++++++++++++++-- .../usvm/machine/interpreter/TsInterpreter.kt | 1 - 3 files changed, 67 insertions(+), 10 deletions(-) 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 index d78de9f1fc..07697b5b8e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt @@ -43,7 +43,7 @@ class UnreachableCodeDetector : TsInterpreterObserver, UMachineObserver uncoveredIfSuccessors .filter { it.value.isNotEmpty() } .takeIf { it.isNotEmpty() } - ?.let { method to it.map { UncoveredIfSuccessors(it.key, it.value) } } + ?.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 index daccb017a1..5be311dac1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -14,14 +14,72 @@ import org.usvm.statistics.UInterpreterObserver @Suppress("unused") interface TsInterpreterObserver : UInterpreterObserver { - fun onAssignStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsAssignStmt, scope: TsStepScope) {} + fun onAssignStatement( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsAssignStmt, + scope: TsStepScope + ) { + // default empty implementation + } + // TODO on entry point - fun onCallWithUnresolvedArguments(simpleValueResolver: TsSimpleValueResolver, stmt: EtsCallExpr, scope: TsStepScope) {} + + fun onCallWithUnresolvedArguments( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsCallExpr, + scope: TsStepScope + ) { + // default empty implementation + } + // TODO onCallWithResolvedArguments - fun onIfStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, scope: TsStepScope) {} - fun onIfStatementWithResolvedCondition(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, condition: UBoolExpr, scope: TsStepScope) {} - fun onReturnStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsReturnStmt, scope: TsStepScope) {} - fun onThrowStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsThrowStmt, scope: TsStepScope) {} - fun onGotoStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsGotoStmt, scope: TsStepScope) {} - fun onSwitchStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsSwitchStmt, scope: TsStepScope) {} + + 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 + } + + fun onGotoStatement( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsGotoStmt, + scope: TsStepScope + ) { + // default empty implementation + } + + fun onSwitchStatement( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsSwitchStmt, + scope: TsStepScope + ) { + // default empty implementation + } } 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 0340376817..7c34130c56 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 @@ -164,7 +164,6 @@ class TsInterpreter( mockMethodCall(scope, it.method) return } - } ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) From ca99356768e7d063837783064e4d711d16995b3d Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 17 Apr 2025 11:45:58 +0300 Subject: [PATCH 13/15] Comma fixes --- .../org/usvm/machine/TsInterpreterObserver.kt | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index 5be311dac1..5d87627e5a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -17,7 +17,7 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onAssignStatement( simpleValueResolver: TsSimpleValueResolver, stmt: EtsAssignStmt, - scope: TsStepScope + scope: TsStepScope, ) { // default empty implementation } @@ -27,7 +27,7 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onCallWithUnresolvedArguments( simpleValueResolver: TsSimpleValueResolver, stmt: EtsCallExpr, - scope: TsStepScope + scope: TsStepScope, ) { // default empty implementation } @@ -37,7 +37,7 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onIfStatement( simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, - scope: TsStepScope + scope: TsStepScope, ) { // default empty implementation } @@ -46,7 +46,7 @@ interface TsInterpreterObserver : UInterpreterObserver { simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, condition: UBoolExpr, - scope: TsStepScope + scope: TsStepScope, ) { // default empty implementation } @@ -54,7 +54,7 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onReturnStatement( simpleValueResolver: TsSimpleValueResolver, stmt: EtsReturnStmt, - scope: TsStepScope + scope: TsStepScope, ) { // default empty implementation } @@ -62,7 +62,7 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onThrowStatement( simpleValueResolver: TsSimpleValueResolver, stmt: EtsThrowStmt, - scope: TsStepScope + scope: TsStepScope, ) { // default empty implementation } @@ -70,7 +70,7 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onGotoStatement( simpleValueResolver: TsSimpleValueResolver, stmt: EtsGotoStmt, - scope: TsStepScope + scope: TsStepScope, ) { // default empty implementation } @@ -78,7 +78,7 @@ interface TsInterpreterObserver : UInterpreterObserver { fun onSwitchStatement( simpleValueResolver: TsSimpleValueResolver, stmt: EtsSwitchStmt, - scope: TsStepScope + scope: TsStepScope, ) { // default empty implementation } From 558e0d9ec1ef41ff9532a3bc3b56e083bd1266f1 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 17 Apr 2025 17:21:29 +0300 Subject: [PATCH 14/15] Rebase fixes --- .../api/checkers/UnreachableCodeDetector.kt | 6 ++-- .../org/usvm/machine/TsInterpreterObserver.kt | 28 ++++--------------- .../checkers/UnreachableCodeDetector.kt | 4 +-- .../samples/checkers/UnreachableCode.ts | 2 +- 4 files changed, 12 insertions(+), 28 deletions(-) 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 index 07697b5b8e..b65e385010 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/checkers/UnreachableCodeDetector.kt @@ -1,13 +1,15 @@ package org.usvm.api.checkers -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsStmt +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) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index 5d87627e5a..43203c52ca 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -1,12 +1,10 @@ package org.usvm.machine -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsCallExpr -import org.jacodb.ets.base.EtsGotoStmt -import org.jacodb.ets.base.EtsIfStmt -import org.jacodb.ets.base.EtsReturnStmt -import org.jacodb.ets.base.EtsSwitchStmt -import org.jacodb.ets.base.EtsThrowStmt +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 @@ -66,20 +64,4 @@ interface TsInterpreterObserver : UInterpreterObserver { ) { // default empty implementation } - - fun onGotoStatement( - simpleValueResolver: TsSimpleValueResolver, - stmt: EtsGotoStmt, - scope: TsStepScope, - ) { - // default empty implementation - } - - fun onSwitchStatement( - simpleValueResolver: TsSimpleValueResolver, - stmt: EtsSwitchStmt, - scope: TsStepScope, - ) { - // default empty implementation - } } 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 index 31cf388549..fdbabb3c0c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt @@ -1,7 +1,7 @@ package org.usvm.samples.checkers -import org.jacodb.ets.base.EtsAssignStmt -import org.jacodb.ets.base.EtsIfStmt +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.junit.jupiter.api.Test diff --git a/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts b/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts index debbf83ffd..ae8c630171 100644 --- a/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts +++ b/usvm-ts/src/test/resources/samples/checkers/UnreachableCode.ts @@ -23,4 +23,4 @@ class UnreachableCode { return } -} \ No newline at end of file +} From b8e8cdfa1b626d463d14003ec54c0714955c9870 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Thu, 17 Apr 2025 17:29:44 +0300 Subject: [PATCH 15/15] Rebase fixes --- .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 2 +- .../org/usvm/samples/checkers/UnreachableCodeDetector.kt | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) 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 7c34130c56..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 @@ -161,7 +161,7 @@ class TsInterpreter( } if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) { - mockMethodCall(scope, it.method) + mockMethodCall(scope, it.callee) return } } ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope) 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 index fdbabb3c0c..8d805dfbef 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/checkers/UnreachableCodeDetector.kt @@ -1,7 +1,8 @@ package org.usvm.samples.checkers import org.jacodb.ets.model.EtsAssignStmt -import org.jacodb.ets.model.EtsIfStmt +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 @@ -72,6 +73,8 @@ class UnreachableCodeDetectorTest { val relatedBranch = results.single { it.key.name == methodName } val stmts = relatedBranch.value.single() - check(stmts.successors.single() is EtsIfStmt) + 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) } }