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..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 @@ -95,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 @@ -260,6 +261,12 @@ 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 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() +} 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; + } +}