From 5c5c5ecf684c090310950c7168f2d24286f58175 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 23:50:12 +0300 Subject: [PATCH 1/3] [TS] Preserve lexical constructor and field initializer dispatch --- .../usvm/machine/interpreter/TsInterpreter.kt | 25 +++-- .../usvm/util/DeclaredConstructorResolver.kt | 20 ---- .../util/DeclaredInitializationResolver.kt | 22 ++++ .../usvm/samples/lang/SuperConstructorCall.kt | 102 ++++++++++++++++++ .../samples/lang/MissingSuperclassBase.d.ts | 3 + .../lang/MissingSuperclassConstructor.ts | 7 ++ .../samples/lang/SuperConstructorCall.ts | 33 ++++++ 7 files changed, 185 insertions(+), 27 deletions(-) delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/DeclaredConstructorResolver.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt create mode 100644 usvm-ts/src/test/resources/samples/lang/MissingSuperclassBase.d.ts create mode 100644 usvm-ts/src/test/resources/samples/lang/MissingSuperclassConstructor.ts 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 1249e3c441..fc7cdae41b 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 @@ -28,8 +28,10 @@ import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsThrowStmt import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME import org.jacodb.ets.utils.callExpr import org.usvm.StepResult import org.usvm.StepScope @@ -80,7 +82,7 @@ import org.usvm.types.TypesResult import org.usvm.types.single import org.usvm.util.executableOverloadImplementation import org.usvm.util.mkFieldLValue -import org.usvm.util.resolveDeclaredConstructor +import org.usvm.util.resolveDeclaredInitialization import org.usvm.util.resolveEtsMethods import org.usvm.util.type @@ -254,6 +256,21 @@ class TsInterpreter( } val receiver = instance.asExpr(addressSort) + val isInitialization = callee.name == CONSTRUCTOR_NAME || callee.name == INSTANCE_INIT_METHOD_NAME + val usesDeclaredInitialization = !stmt.targetCaptured && isInitialization + if (usesDeclaredInitialization) { + // Construction and field initialization retain their lexical owner for symbolic entry receivers. + // Virtual lookup would select the derived initializer or recursively select its constructor. + val initializer = stmt.resolveDeclaredInitialization(graph.hierarchy) + if (initializer == null) { + unknownCallDispatcher.dispatch(scope, stmt, Reason.VIRTUAL_METHOD_NOT_FOUND, receiver) + return + } + + scope.doWithState { newStmt(stmt.toConcrete(initializer)) } + return + } + val concreteMethods: MutableList = mutableListOf() if (isAllocatedConcreteHeapRef(receiver)) { @@ -287,12 +304,6 @@ class TsInterpreter( return } - val constructor = stmt.resolveDeclaredConstructor(graph.hierarchy) - if (constructor != null) { - scope.doWithState { newStmt(stmt.toConcrete(constructor)) } - return - } - val type = scope.calcOnState { memory.typeStreamOf(receiver) }.single() if (type is EtsClassType) { val classes = graph.hierarchy.classesForType(type) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredConstructorResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredConstructorResolver.kt deleted file mode 100644 index 23e63e68dd..0000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredConstructorResolver.kt +++ /dev/null @@ -1,20 +0,0 @@ -package org.usvm.util - -import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.utils.CONSTRUCTOR_NAME -import org.usvm.machine.TsVirtualMethodCallStmt - -/** New and super calls use their declared owner; captured property calls retain virtual dispatch. */ -internal fun TsVirtualMethodCallStmt.resolveDeclaredConstructor(hierarchy: EtsHierarchy): EtsMethod? { - val callee = call.callee - if (targetCaptured || callee.name != CONSTRUCTOR_NAME) return null - - val ownerType = EtsClassType(callee.enclosingClass) - val constructors = hierarchy.classesForType(ownerType) - .flatMap { owner -> owner.methods } - .filter { method -> method.name == CONSTRUCTOR_NAME } - .canonicalizeExecutableOverloads() - - return constructors.singleOrNull() -} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt new file mode 100644 index 0000000000..4e89c6c95d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt @@ -0,0 +1,22 @@ +package org.usvm.util + +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME +import org.usvm.machine.TsVirtualMethodCallStmt + +/** Construction and instance initialization use their declared owner, including symbolic receivers. */ +internal fun TsVirtualMethodCallStmt.resolveDeclaredInitialization(hierarchy: EtsHierarchy): EtsMethod? { + val callee = call.callee + val isInitialization = callee.name == CONSTRUCTOR_NAME || callee.name == INSTANCE_INIT_METHOD_NAME + if (targetCaptured || !isInitialization) return null + + val ownerType = EtsClassType(callee.enclosingClass) + val methods = hierarchy.classesForType(ownerType) + .flatMap { owner -> owner.methods } + .filter { method -> method.name == callee.name } + .canonicalizeExecutableOverloads() + + return methods.singleOrNull() +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt index 63c9fd7e68..cdd7f2cbf9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt @@ -1,12 +1,30 @@ package org.usvm.samples.lang import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.io.TempDir import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.call.TsModelUnknownCallDispatcher +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModelCatalog import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay import org.usvm.util.eq +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds class SuperConstructorCall : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + override val scene: EtsScene = loadScene("/samples/lang/SuperConstructorCall.ts") @Test @@ -31,6 +49,17 @@ class SuperConstructorCall : TsMethodTestRunner() { ) } + @Test + fun `allocated receiver initializes every declared superclass in order`() { + val method = getMethod(methodName = "nestedSuper") + + discoverProperties( + method = method, + { result -> result eq 71 }, + invariants = arrayOf({ result -> result eq 71 }), + ) + } + @Test fun `ordinary constructor property remains callable`() { val method = getMethod("shadowedConstructorProperty") @@ -41,4 +70,77 @@ class SuperConstructorCall : TsMethodTestRunner() { invariants = arrayOf({ result -> result eq 17 }), ) } + + @Test + fun `symbolic entry receiver calls each superclass constructor once`() { + val method = getMethod(methodName = "constructor", className = "SymbolicConstructorChild") + val constructorOptions = options.copy(timeout = 5.seconds, stepsFromLastCovered = 200L) + + val tests = runner(method, constructorOptions) + + assertTrue(tests.isNotEmpty()) + val results = tests.map { test -> assertIs(test.returnValue) } + results.forEach { result -> + val value = assertIs(result.properties["value"]) + assertEquals(expected = 71.0, actual = value.number) + } + replayConstructor(className = "SymbolicConstructorChild", expectedValue = 71) + } + + @Test + fun `symbolic entry receiver forwards an implicit superclass constructor`() { + val method = getMethod(methodName = "constructor", className = "SymbolicImplicitConstructorChild") + val constructorOptions = options.copy(timeout = 5.seconds, stepsFromLastCovered = 200L) + + val tests = runner(method, constructorOptions) + + assertTrue(tests.isNotEmpty()) + val results = tests.map { test -> assertIs(test.returnValue) } + results.forEach { result -> + val value = assertIs(result.properties["value"]) + assertEquals(expected = 13.0, actual = value.number) + } + replayConstructor(className = "SymbolicImplicitConstructorChild", expectedValue = 13) + } + + @Test + fun `missing superclass constructor reaches the unknown call boundary once`() { + val missingBaseScene = loadScene("/samples/lang/MissingSuperclassConstructor.ts") + val missingBaseClass = missingBaseScene.projectClasses.single { it.name == "MissingSuperclassConstructor" } + val method = missingBaseClass.methods.single { it.name == "constructor" } + val calls = mutableListOf() + val fallback = TsModelUnknownCallDispatcher( + models = TsUnknownCallModelCatalog(models = emptyList()), + fallback = TsResidualCallPolicy.STOP_PATH, + ) + val constructorOptions = options.copy(timeout = 5.seconds, stepsFromLastCovered = 200L) + + TsMachine( + scene = missingBaseScene, + options = constructorOptions, + tsOptions = tsOptions, + unknownCallDispatcher = { scope, call -> + calls += call + fallback.dispatch(scope, call) + }, + ).use { machine -> + val states = machine.analyze(listOf(method)) + assertTrue(states.isEmpty()) + } + + assertEquals(TsUnknownCallFailureReason.VIRTUAL_METHOD_NOT_FOUND, calls.single().failureReason) + assertEquals(expected = "constructor", actual = calls.single().callee.name) + } + + private fun replayConstructor(className: String, expectedValue: Int) { + val source = getResourcePath("/samples/lang/SuperConstructorCall.ts").readText() + val script = source + "\nif (new $className().value !== $expectedValue) throw Error('constructor replay');" + + assertNodeReplay( + source = script, + directory = directory, + name = className, + timeoutMessage = "Constructor replay timed out for $className", + ) + } } diff --git a/usvm-ts/src/test/resources/samples/lang/MissingSuperclassBase.d.ts b/usvm-ts/src/test/resources/samples/lang/MissingSuperclassBase.d.ts new file mode 100644 index 0000000000..115b9dcdd4 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/MissingSuperclassBase.d.ts @@ -0,0 +1,3 @@ +declare class MissingSuperclassBase { + constructor(); +} diff --git a/usvm-ts/src/test/resources/samples/lang/MissingSuperclassConstructor.ts b/usvm-ts/src/test/resources/samples/lang/MissingSuperclassConstructor.ts new file mode 100644 index 0000000000..68bf2256b9 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/MissingSuperclassConstructor.ts @@ -0,0 +1,7 @@ +/// + +class MissingSuperclassConstructor extends MissingSuperclassBase { + constructor() { + super(); + } +} diff --git a/usvm-ts/src/test/resources/samples/lang/SuperConstructorCall.ts b/usvm-ts/src/test/resources/samples/lang/SuperConstructorCall.ts index 08bd06f65a..d37644eee5 100644 --- a/usvm-ts/src/test/resources/samples/lang/SuperConstructorCall.ts +++ b/usvm-ts/src/test/resources/samples/lang/SuperConstructorCall.ts @@ -11,6 +11,11 @@ class SuperConstructorCall { return subject.value; } + static nestedSuper(): number { + const subject = new SymbolicConstructorChild(); + return subject.value; + } + static shadowedConstructorProperty(): number { const subject = new ImplicitConstructorChild(); subject.constructor = () => subject.value + 10; @@ -34,3 +39,31 @@ class ExplicitConstructorChild extends ConstructorParent { this.value = this.value * 2; } } + +class SymbolicConstructorBase { + value: number = 1; + + constructor() { + this.value = this.value + 2; + } +} + +class SymbolicConstructorMiddle extends SymbolicConstructorBase { + middleValue: number = this.value * 3; + + constructor() { + super(); + this.value = this.middleValue + 4; + } +} + +class SymbolicConstructorChild extends SymbolicConstructorMiddle { + childValue: number = this.value * 5; + + constructor() { + super(); + this.value = this.childValue + 6; + } +} + +class SymbolicImplicitConstructorChild extends SymbolicConstructorMiddle {} From 4aebf63e557aeb347072861ff15e09a31a3f611c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 00:24:34 +0300 Subject: [PATCH 2/3] [TS] Retain constructors selected by dynamic new --- .../usvm/machine/interpreter/TsInterpreter.kt | 11 +++++- .../util/DeclaredInitializationResolver.kt | 38 ++++++++++++++++++- 2 files changed, 46 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 fc7cdae41b..b8416c8840 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 @@ -80,7 +80,9 @@ import org.usvm.machine.state.returnValue import org.usvm.sizeSort import org.usvm.types.TypesResult import org.usvm.types.single +import org.usvm.types.singleOrNull import org.usvm.util.executableOverloadImplementation +import org.usvm.util.hasConstructorAllocation import org.usvm.util.mkFieldLValue import org.usvm.util.resolveDeclaredInitialization import org.usvm.util.resolveEtsMethods @@ -261,7 +263,14 @@ class TsInterpreter( if (usesDeclaredInitialization) { // Construction and field initialization retain their lexical owner for symbolic entry receivers. // Virtual lookup would select the derived initializer or recursively select its constructor. - val initializer = stmt.resolveDeclaredInitialization(graph.hierarchy) + val isNewAllocation = stmt.hasConstructorAllocation(graph) + val allocatedType = if (isNewAllocation) { + // Dynamic new already selected its constructor before argument evaluation and allocation. + scope.calcOnState { memory.typeStreamOf(receiver).singleOrNull() } as? EtsClassType + } else { + null + } + val initializer = stmt.resolveDeclaredInitialization(graph.hierarchy, allocatedType) if (initializer == null) { unknownCallDispatcher.dispatch(scope, stmt, Reason.VIRTUAL_METHOD_NOT_FOUND, receiver) return diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt index 4e89c6c95d..092fbcd780 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt @@ -1,18 +1,26 @@ package org.usvm.util +import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNewExpr +import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME +import org.usvm.machine.TsGraph import org.usvm.machine.TsVirtualMethodCallStmt /** Construction and instance initialization use their declared owner, including symbolic receivers. */ -internal fun TsVirtualMethodCallStmt.resolveDeclaredInitialization(hierarchy: EtsHierarchy): EtsMethod? { +internal fun TsVirtualMethodCallStmt.resolveDeclaredInitialization( + hierarchy: EtsHierarchy, + allocatedType: EtsClassType?, +): EtsMethod? { val callee = call.callee val isInitialization = callee.name == CONSTRUCTOR_NAME || callee.name == INSTANCE_INIT_METHOD_NAME if (targetCaptured || !isInitialization) return null - val ownerType = EtsClassType(callee.enclosingClass) + val ownerType = allocatedType ?: EtsClassType(callee.enclosingClass) val methods = hierarchy.classesForType(ownerType) .flatMap { owner -> owner.methods } .filter { method -> method.name == callee.name } @@ -20,3 +28,29 @@ internal fun TsVirtualMethodCallStmt.resolveDeclaredInitialization(hierarchy: Et return methods.singleOrNull() } + +/** Argument temporaries can separate allocation and construction; every reaching definition must allocate. */ +internal fun TsVirtualMethodCallStmt.hasConstructorAllocation(graph: TsGraph): Boolean { + if (call.callee.name != CONSTRUCTOR_NAME) return false + + val pending = ArrayDeque(graph.predecessors(returnSite).toList()) + val visited = mutableSetOf() + var foundAllocation = false + while (pending.isNotEmpty()) { + val statement = pending.removeFirst() + if (!visited.add(statement)) continue + + val assignment = statement as? EtsAssignStmt + val local = assignment?.lhv as? EtsLocal + if (local?.name == call.instance.name) { + if (assignment.rhv !is EtsNewExpr) return false + foundAllocation = true + continue + } + + val predecessors = graph.predecessors(statement).toList() + if (predecessors.isEmpty()) return false + pending.addAll(predecessors) + } + return foundAllocation +} From 54c8079067fb7ab5bbd9e043ae5ab327338f02cc Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 00:41:57 +0300 Subject: [PATCH 3/3] [TS] Preserve missing constructor owner classification --- .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 5 ++++- .../kotlin/org/usvm/samples/lang/SuperConstructorCall.kt | 2 +- 2 files changed, 5 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 b8416c8840..b1a4805799 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 @@ -272,7 +272,10 @@ class TsInterpreter( } val initializer = stmt.resolveDeclaredInitialization(graph.hierarchy, allocatedType) if (initializer == null) { - unknownCallDispatcher.dispatch(scope, stmt, Reason.VIRTUAL_METHOD_NOT_FOUND, receiver) + val ownerType = allocatedType ?: EtsClassType(callee.enclosingClass) + val ownerIsMissing = graph.hierarchy.classesForType(ownerType).isEmpty() + val reason = if (ownerIsMissing) Reason.RECEIVER_CLASS_NOT_FOUND else Reason.VIRTUAL_METHOD_NOT_FOUND + unknownCallDispatcher.dispatch(scope, stmt, reason, receiver) return } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt index cdd7f2cbf9..382d10b0a8 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt @@ -128,7 +128,7 @@ class SuperConstructorCall : TsMethodTestRunner() { assertTrue(states.isEmpty()) } - assertEquals(TsUnknownCallFailureReason.VIRTUAL_METHOD_NOT_FOUND, calls.single().failureReason) + assertEquals(TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, calls.single().failureReason) assertEquals(expected = "constructor", actual = calls.single().callee.name) }