From db7292beb37da4c85135356a0984c92376bb052f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 06:54:19 +0300 Subject: [PATCH 1/2] [TS] Dispatch super constructors to their declared class --- .../usvm/machine/interpreter/TsInterpreter.kt | 16 +++++++ .../usvm/samples/lang/SuperConstructorCall.kt | 44 +++++++++++++++++++ .../samples/lang/SuperConstructorCall.ts | 36 +++++++++++++++ 3 files changed, 96 insertions(+) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt create mode 100644 usvm-ts/src/test/resources/samples/lang/SuperConstructorCall.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 0b5757cc7a..5c54935a77 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 @@ -33,6 +33,7 @@ import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType 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.callExpr @@ -260,6 +261,21 @@ class TsInterpreter( return } + // Constructor calls, including super(), target their declared owner rather than an override. + if (callee.name == CONSTRUCTOR_NAME) { + val ownerType = EtsClassType(callee.enclosingClass) + val constructors = graph.hierarchy.classesForType(ownerType) + .flatMap { owner -> owner.methods } + .filter { method -> method.name == CONSTRUCTOR_NAME } + .map { method -> method.executableOverloadImplementation() } + .distinct() + val constructor = constructors.singleOrNull() + 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/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt new file mode 100644 index 0000000000..63c9fd7e68 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SuperConstructorCall.kt @@ -0,0 +1,44 @@ +package org.usvm.samples.lang + +import org.jacodb.ets.model.EtsScene +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import kotlin.test.Test + +class SuperConstructorCall : TsMethodTestRunner() { + override val scene: EtsScene = loadScene("/samples/lang/SuperConstructorCall.ts") + + @Test + fun `implicit derived constructor calls the parent once`() { + val method = getMethod("implicitSuper") + + discoverProperties( + method = method, + { result -> result eq 7 }, + invariants = arrayOf({ result -> result eq 7 }), + ) + } + + @Test + fun `explicit super preserves arguments and derived receiver`() { + val method = getMethod("explicitSuper") + + discoverProperties( + method = method, + { result -> result eq 8 }, + invariants = arrayOf({ result -> result eq 8 }), + ) + } + + @Test + fun `ordinary constructor property remains callable`() { + val method = getMethod("shadowedConstructorProperty") + + discoverProperties( + method = method, + { result -> result eq 17 }, + invariants = arrayOf({ result -> result eq 17 }), + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/lang/SuperConstructorCall.ts b/usvm-ts/src/test/resources/samples/lang/SuperConstructorCall.ts new file mode 100644 index 0000000000..08bd06f65a --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/SuperConstructorCall.ts @@ -0,0 +1,36 @@ +// @ts-nocheck + +class SuperConstructorCall { + static implicitSuper(): number { + const subject = new ImplicitConstructorChild(); + return subject.value; + } + + static explicitSuper(): number { + const subject = new ExplicitConstructorChild(3); + return subject.value; + } + + static shadowedConstructorProperty(): number { + const subject = new ImplicitConstructorChild(); + subject.constructor = () => subject.value + 10; + return subject.constructor(); + } +} + +class ConstructorParent { + value: number; + + constructor(value: number = 7) { + this.value = value; + } +} + +class ImplicitConstructorChild extends ConstructorParent {} + +class ExplicitConstructorChild extends ConstructorParent { + constructor(value: number) { + super(value + 1); + this.value = this.value * 2; + } +} From 07176235ab347e0bb394f2305010ba67486d7967 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 06:58:18 +0300 Subject: [PATCH 2/2] [TS] Isolate declared constructor dispatch from property calls --- .../usvm/machine/interpreter/TsInterpreter.kt | 19 +++++------------- .../usvm/util/DeclaredConstructorResolver.kt | 20 +++++++++++++++++++ 2 files changed, 25 insertions(+), 14 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/DeclaredConstructorResolver.kt 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 5c54935a77..14a0159029 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 @@ -33,7 +33,6 @@ import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType 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.callExpr @@ -96,6 +95,7 @@ import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue +import org.usvm.util.resolveDeclaredConstructor import org.usvm.util.resolveEtsMethods import org.usvm.util.type import org.usvm.utils.ensureSat @@ -261,19 +261,10 @@ class TsInterpreter( return } - // Constructor calls, including super(), target their declared owner rather than an override. - if (callee.name == CONSTRUCTOR_NAME) { - val ownerType = EtsClassType(callee.enclosingClass) - val constructors = graph.hierarchy.classesForType(ownerType) - .flatMap { owner -> owner.methods } - .filter { method -> method.name == CONSTRUCTOR_NAME } - .map { method -> method.executableOverloadImplementation() } - .distinct() - val constructor = constructors.singleOrNull() - if (constructor != null) { - scope.doWithState { newStmt(stmt.toConcrete(constructor)) } - 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() diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredConstructorResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredConstructorResolver.kt new file mode 100644 index 0000000000..23e63e68dd --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/DeclaredConstructorResolver.kt @@ -0,0 +1,20 @@ +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() +}