From 54acfc3e165c2dced434412e8b1cda49f5dc2906 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 16:35:51 +0300 Subject: [PATCH 1/3] [TS] Dispatch function values stored in object fields --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 9 +- .../usvm/machine/interpreter/TsInterpreter.kt | 34 +++++- .../reachability/StoredFunctionCallTest.kt | 104 ++++++++++++++++++ .../reachability/StoredFunctionCall.ts | 55 +++++++++ 4 files changed, 200 insertions(+), 2 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/reachability/StoredFunctionCallTest.kt create mode 100644 usvm-ts/src/test/resources/reachability/StoredFunctionCall.ts 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 5c5d344b3b..c5e36549ef 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -59,6 +59,7 @@ class TsMachine( observer: TsInterpreterObserver? = null, unknownCallDispatcher: TsUnknownCallDispatcher? = null, unknownCallModels: TsUnknownCallModelCatalog? = null, + private val initialStateConfigurator: (TsState) -> Unit = {}, ) : UMachine() { private val resolvedUnknownCallModels = when { unknownCallDispatcher != null -> null @@ -111,7 +112,13 @@ class TsMachine( targets: List = emptyList(), ): TsAnalysisResult { val initialStates = mutableMapOf() - methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } + methods.forEach { method -> + initialStates[method] = interpreter.getInitialState( + method = method, + targets = targets, + configure = initialStateConfigurator, + ) + } val methodsToTrackCoverage = when (options.coverageZone) { 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 423f5dde71..5d0b396bb8 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 @@ -196,6 +196,32 @@ class TsInterpreter( val concreteMethods: MutableList = mutableListOf() if (isAllocatedConcreteHeapRef(receiver)) { + val field = mkFieldLValue(addressSort, receiver, callee.name) + val functionRef = scope.calcOnState { memory.read(field) } + val function = if (isAllocatedConcreteHeapRef(functionRef)) { + scope.calcOnState { associatedFunction[functionRef] } + } else { + null + } + + if (function != null) { + val resolvedArgs = buildList { + function.closure?.let(::add) + addAll(stmt.args) + } + val concreteCall = TsConcreteMethodCallStmt( + callee = function.method, + call = stmt.call, + resolvedReceiver = functionRef, + instance = function.thisInstance ?: receiver, + args = resolvedArgs, + returnSite = stmt.returnSite, + ) + + scope.doWithState { newStmt(concreteCall) } + return + } + val type = scope.calcOnState { memory.typeStreamOf(receiver) }.single() if (type is EtsClassType) { val classes = graph.hierarchy.classesForType(type) @@ -712,7 +738,11 @@ class TsInterpreter( unknownCallDispatcher = unknownCallDispatcher, ) - fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { + fun getInitialState( + method: EtsMethod, + targets: List, + configure: (TsState) -> Unit = {}, + ): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -802,6 +832,8 @@ class TsInterpreter( } } + configure(state) + val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/StoredFunctionCallTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/StoredFunctionCallTest.kt new file mode 100644 index 0000000000..fd91cd0741 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/StoredFunctionCallTest.kt @@ -0,0 +1,104 @@ +package org.usvm.reachability + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import org.usvm.util.mkRegisterStackLValue +import org.usvm.util.type +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class StoredFunctionCallTest { + private val file = loadEtsFileAutoConvert(getResourcePath("/reachability/StoredFunctionCall.ts")) + private val scene = EtsScene(listOf(file)) + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + timeout = 5.seconds, + solverTimeout = 1.seconds, + solverType = SolverType.YICES, + exceptionsPropagation = true, + stepsFromLastCovered = 10_000L, + ) + + @Test + fun `constructor callback stored in a field can return`() { + val method = scene.projectClasses.flatMap { it.methods }.single { it.name == "exercise" } + + val machine = TsMachine(scene = scene, options = options, tsOptions = TsOptions()) + val results = machine.analyze(listOf(method)) + + assertTrue(results.isNotEmpty(), "Expected a completed path through the stored callback") + } + + @Test + fun `regular function stored in a field receives its call receiver`() { + assertEquals(setOf(5.0), numberResults("regularFunction")) + } + + @Test + fun `subclass can call a function stored in an inherited field`() { + val method = scene.projectClasses.flatMap { it.methods }.single { it.name == "inheritedField" } + val derived = scene.projectClasses.single { it.name == "DerivedStoredFunctionCall" } + val parameterSlot = 1 + val states = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + initialStateConfigurator = { state -> + with(state.ctx) { + val receiver = state.memory.allocConcrete(derived.type) + state.memory.write( + mkRegisterStackLValue(sort = addressSort, idx = parameterSlot), + receiver.asExpr(addressSort), + guard = trueExpr, + ) + state.saveSortForLocal(idx = parameterSlot, sort = addressSort) + } + }, + ).use { machine -> machine.analyze(listOf(method)) } + + assertTrue(states.isNotEmpty(), "Expected a completed path through the inherited callback") + val values = states.map { state -> + val result = TsTestResolver().resolve(method, state).returnValue + assertIs(result).number + }.toSet() + assertEquals(setOf(7.0), values) + } + + @Test + fun `symbolic object field can select both branches`() { + val method = scene.projectClasses.flatMap { it.methods }.single { it.name == "inspect" } + val returns = method.cfg.stmts.filterIsInstance() + + val machine = TsMachine(scene = scene, options = options, tsOptions = TsOptions()) + val results = machine.analyze(listOf(method)) + val reached = results.flatMap { it.pathNode.allStatements }.toSet() + + assertTrue(returns.size >= 2 && returns.all { it in reached }, "Expected both object-field branches") + } + + private fun numberResults(methodName: String): Set { + val method = scene.projectClasses.flatMap { it.methods }.single { it.name == methodName } + val states = TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + machine.analyze(listOf(method)) + } + + assertTrue(states.isNotEmpty(), "Expected a completed path through $methodName") + return states.map { state -> + val result = TsTestResolver().resolve(method, state).returnValue + assertIs(result).number + }.toSet() + } +} diff --git a/usvm-ts/src/test/resources/reachability/StoredFunctionCall.ts b/usvm-ts/src/test/resources/reachability/StoredFunctionCall.ts new file mode 100644 index 0000000000..872135f7e2 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/StoredFunctionCall.ts @@ -0,0 +1,55 @@ +// @ts-nocheck + +class StoredFunctionCall { + private callback: (value: number) => number; + private offset: number = 4; + + constructor() { + this.callback = (value: number) => value + 1; + } + + call(value: number): number { + return this.callback(value); + } + + static exercise(value: number): number { + const subject = new StoredFunctionCall(); + return subject.call(value); + } + + static regularFunction(): number { + const subject = new StoredFunctionCall(); + subject.callback = function (value: number): number { + return this.offset + value; + }; + return subject.call(1); + } + + static inheritedField(subject: DerivedStoredFunctionCall): number { + subject.callback = () => 7; + return subject.call(); + } + + static inspect(input: InputRecord): number { + if (input.score > 10) return 1; + return 0; + } +} + +class InputRecord { + score: number = 0; +} + +class BaseStoredFunctionCall { + callback: () => number; + + constructor() { + this.callback = () => 7; + } +} + +class DerivedStoredFunctionCall extends BaseStoredFunctionCall { + call(): number { + return this.callback(); + } +} From e5723b5e948291246a132fac9ebf32269ca5c1d5 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 16:58:17 +0300 Subject: [PATCH 2/3] [TS] Align stored function tests with sample runner --- .../reachability/StoredFunctionCallTest.kt | 104 ------------------ .../usvm/samples/lang/StoredFunctionCall.kt | 74 +++++++++++++ .../lang}/StoredFunctionCall.ts | 13 +-- 3 files changed, 76 insertions(+), 115 deletions(-) delete mode 100644 usvm-ts/src/test/kotlin/org/usvm/reachability/StoredFunctionCallTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt rename usvm-ts/src/test/resources/{reachability => samples/lang}/StoredFunctionCall.ts (80%) diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/StoredFunctionCallTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/StoredFunctionCallTest.kt deleted file mode 100644 index fd91cd0741..0000000000 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/StoredFunctionCallTest.kt +++ /dev/null @@ -1,104 +0,0 @@ -package org.usvm.reachability - -import io.ksmt.utils.asExpr -import org.jacodb.ets.model.EtsReturnStmt -import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.utils.loadEtsFileAutoConvert -import org.usvm.PathSelectionStrategy -import org.usvm.SolverType -import org.usvm.UMachineOptions -import org.usvm.api.TsTestValue -import org.usvm.machine.TsMachine -import org.usvm.machine.TsOptions -import org.usvm.util.TsTestResolver -import org.usvm.util.getResourcePath -import org.usvm.util.mkRegisterStackLValue -import org.usvm.util.type -import kotlin.test.Test -import kotlin.test.assertEquals -import kotlin.test.assertIs -import kotlin.test.assertTrue -import kotlin.time.Duration.Companion.seconds - -class StoredFunctionCallTest { - private val file = loadEtsFileAutoConvert(getResourcePath("/reachability/StoredFunctionCall.ts")) - private val scene = EtsScene(listOf(file)) - private val options = UMachineOptions( - pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), - timeout = 5.seconds, - solverTimeout = 1.seconds, - solverType = SolverType.YICES, - exceptionsPropagation = true, - stepsFromLastCovered = 10_000L, - ) - - @Test - fun `constructor callback stored in a field can return`() { - val method = scene.projectClasses.flatMap { it.methods }.single { it.name == "exercise" } - - val machine = TsMachine(scene = scene, options = options, tsOptions = TsOptions()) - val results = machine.analyze(listOf(method)) - - assertTrue(results.isNotEmpty(), "Expected a completed path through the stored callback") - } - - @Test - fun `regular function stored in a field receives its call receiver`() { - assertEquals(setOf(5.0), numberResults("regularFunction")) - } - - @Test - fun `subclass can call a function stored in an inherited field`() { - val method = scene.projectClasses.flatMap { it.methods }.single { it.name == "inheritedField" } - val derived = scene.projectClasses.single { it.name == "DerivedStoredFunctionCall" } - val parameterSlot = 1 - val states = TsMachine( - scene = scene, - options = options, - tsOptions = TsOptions(), - initialStateConfigurator = { state -> - with(state.ctx) { - val receiver = state.memory.allocConcrete(derived.type) - state.memory.write( - mkRegisterStackLValue(sort = addressSort, idx = parameterSlot), - receiver.asExpr(addressSort), - guard = trueExpr, - ) - state.saveSortForLocal(idx = parameterSlot, sort = addressSort) - } - }, - ).use { machine -> machine.analyze(listOf(method)) } - - assertTrue(states.isNotEmpty(), "Expected a completed path through the inherited callback") - val values = states.map { state -> - val result = TsTestResolver().resolve(method, state).returnValue - assertIs(result).number - }.toSet() - assertEquals(setOf(7.0), values) - } - - @Test - fun `symbolic object field can select both branches`() { - val method = scene.projectClasses.flatMap { it.methods }.single { it.name == "inspect" } - val returns = method.cfg.stmts.filterIsInstance() - - val machine = TsMachine(scene = scene, options = options, tsOptions = TsOptions()) - val results = machine.analyze(listOf(method)) - val reached = results.flatMap { it.pathNode.allStatements }.toSet() - - assertTrue(returns.size >= 2 && returns.all { it in reached }, "Expected both object-field branches") - } - - private fun numberResults(methodName: String): Set { - val method = scene.projectClasses.flatMap { it.methods }.single { it.name == methodName } - val states = TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> - machine.analyze(listOf(method)) - } - - assertTrue(states.isNotEmpty(), "Expected a completed path through $methodName") - return states.map { state -> - val result = TsTestResolver().resolve(method, state).returnValue - assertIs(result).number - }.toSet() - } -} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt new file mode 100644 index 0000000000..77f95b2064 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt @@ -0,0 +1,74 @@ +package org.usvm.samples.lang + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene +import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.eq +import org.usvm.util.mkRegisterStackLValue +import org.usvm.util.type +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs + +class StoredFunctionCall : TsMethodTestRunner() { + private val tsPath = "/samples/lang/StoredFunctionCall.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `test callback stored in constructor`() { + val method = getMethod("constructorCallback") + + discoverProperties( + method = method, + { result -> result eq 2 }, + invariants = arrayOf({ result -> result eq 2 }), + ) + } + + @Test + fun `test regular function uses call receiver`() { + val method = getMethod("regularFunction") + + discoverProperties( + method = method, + { result -> result eq 5 }, + invariants = arrayOf({ result -> result eq 5 }), + ) + } + + @Test + fun `test callback field inherited from base class`() { + val method = getMethod("inheritedField") + val derived = scene.projectClasses.single { it.name == "DerivedStoredFunctionCall" } + val parameterSlot = 1 + val machine = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + initialStateConfigurator = { state -> + with(state.ctx) { + val receiver = state.memory.allocConcrete(derived.type) + state.memory.write( + mkRegisterStackLValue(sort = addressSort, idx = parameterSlot), + receiver.asExpr(addressSort), + guard = trueExpr, + ) + state.saveSortForLocal(idx = parameterSlot, sort = addressSort) + } + }, + ) + + val states = machine.use { it.analyze(listOf(method)) } + val results = states.map { state -> + val result = TsTestResolver().resolve(method, state).returnValue + assertIs(result).number + }.toSet() + + assertEquals(setOf(7.0), results) + } +} diff --git a/usvm-ts/src/test/resources/reachability/StoredFunctionCall.ts b/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts similarity index 80% rename from usvm-ts/src/test/resources/reachability/StoredFunctionCall.ts rename to usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts index 872135f7e2..ef404e9536 100644 --- a/usvm-ts/src/test/resources/reachability/StoredFunctionCall.ts +++ b/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts @@ -12,9 +12,9 @@ class StoredFunctionCall { return this.callback(value); } - static exercise(value: number): number { + static constructorCallback(): number { const subject = new StoredFunctionCall(); - return subject.call(value); + return subject.call(1); } static regularFunction(): number { @@ -29,15 +29,6 @@ class StoredFunctionCall { subject.callback = () => 7; return subject.call(); } - - static inspect(input: InputRecord): number { - if (input.score > 10) return 1; - return 0; - } -} - -class InputRecord { - score: number = 0; } class BaseStoredFunctionCall { From 00cbfabcd609ea8da9afc46f18d3b225b4b0008f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 18:04:51 +0300 Subject: [PATCH 3/3] [TS] Remove synthetic initial state from callback tests --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 9 +---- .../usvm/machine/interpreter/TsInterpreter.kt | 8 +--- .../usvm/samples/lang/StoredFunctionCall.kt | 39 ------------------- .../samples/lang/StoredFunctionCall.ts | 19 --------- 4 files changed, 2 insertions(+), 73 deletions(-) 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 c5e36549ef..5c5d344b3b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -59,7 +59,6 @@ class TsMachine( observer: TsInterpreterObserver? = null, unknownCallDispatcher: TsUnknownCallDispatcher? = null, unknownCallModels: TsUnknownCallModelCatalog? = null, - private val initialStateConfigurator: (TsState) -> Unit = {}, ) : UMachine() { private val resolvedUnknownCallModels = when { unknownCallDispatcher != null -> null @@ -112,13 +111,7 @@ class TsMachine( targets: List = emptyList(), ): TsAnalysisResult { val initialStates = mutableMapOf() - methods.forEach { method -> - initialStates[method] = interpreter.getInitialState( - method = method, - targets = targets, - configure = initialStateConfigurator, - ) - } + methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } val methodsToTrackCoverage = when (options.coverageZone) { 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 5d0b396bb8..f5ea96ef7a 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 @@ -738,11 +738,7 @@ class TsInterpreter( unknownCallDispatcher = unknownCallDispatcher, ) - fun getInitialState( - method: EtsMethod, - targets: List, - configure: (TsState) -> Unit = {}, - ): TsState = with(ctx) { + fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -832,8 +828,6 @@ class TsInterpreter( } } - configure(state) - val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt index 77f95b2064..077d0e844a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt @@ -1,18 +1,10 @@ package org.usvm.samples.lang -import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsScene import org.usvm.api.TsTestValue -import org.usvm.machine.TsMachine -import org.usvm.machine.TsOptions import org.usvm.util.TsMethodTestRunner -import org.usvm.util.TsTestResolver import org.usvm.util.eq -import org.usvm.util.mkRegisterStackLValue -import org.usvm.util.type import kotlin.test.Test -import kotlin.test.assertEquals -import kotlin.test.assertIs class StoredFunctionCall : TsMethodTestRunner() { private val tsPath = "/samples/lang/StoredFunctionCall.ts" @@ -40,35 +32,4 @@ class StoredFunctionCall : TsMethodTestRunner() { invariants = arrayOf({ result -> result eq 5 }), ) } - - @Test - fun `test callback field inherited from base class`() { - val method = getMethod("inheritedField") - val derived = scene.projectClasses.single { it.name == "DerivedStoredFunctionCall" } - val parameterSlot = 1 - val machine = TsMachine( - scene = scene, - options = options, - tsOptions = TsOptions(), - initialStateConfigurator = { state -> - with(state.ctx) { - val receiver = state.memory.allocConcrete(derived.type) - state.memory.write( - mkRegisterStackLValue(sort = addressSort, idx = parameterSlot), - receiver.asExpr(addressSort), - guard = trueExpr, - ) - state.saveSortForLocal(idx = parameterSlot, sort = addressSort) - } - }, - ) - - val states = machine.use { it.analyze(listOf(method)) } - val results = states.map { state -> - val result = TsTestResolver().resolve(method, state).returnValue - assertIs(result).number - }.toSet() - - assertEquals(setOf(7.0), results) - } } diff --git a/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts b/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts index ef404e9536..b1ad133a1b 100644 --- a/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts +++ b/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts @@ -24,23 +24,4 @@ class StoredFunctionCall { }; return subject.call(1); } - - static inheritedField(subject: DerivedStoredFunctionCall): number { - subject.callback = () => 7; - return subject.call(); - } -} - -class BaseStoredFunctionCall { - callback: () => number; - - constructor() { - this.callback = () => 7; - } -} - -class DerivedStoredFunctionCall extends BaseStoredFunctionCall { - call(): number { - return this.callback(); - } }