[TS] Preserve lexical constructor and field initializer dispatch

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
@@ -78,9 +80,11 @@ 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.resolveDeclaredConstructor
+import org.usvm.util.resolveDeclaredInitialization
 import org.usvm.util.resolveEtsMethods
 import org.usvm.util.type
 
@@ -254,6 +258,31 @@ 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 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) {
+                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
+            }
+
+            scope.doWithState { newStmt(stmt.toConcrete(initializer)) }
+            return
+        }
+
         val concreteMethods: MutableList<EtsMethod> = mutableListOf()
 
         if (isAllocatedConcreteHeapRef(receiver)) {
@@ -287,12 +316,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)

usvm-ts/src/main/kotlin/org/usvm/util/DeclaredInitializationResolver.kt

@@ -0,0 +1,56 @@
+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,
+    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 = allocatedType ?: EtsClassType(callee.enclosingClass)
+    val methods = hierarchy.classesForType(ownerType)
+        .flatMap { owner -> owner.methods }
+        .filter { method -> method.name == callee.name }
+        .canonicalizeExecutableOverloads()
+
+    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<EtsStmt>()
+    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
+}

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<TsTestValue.TsNumber>(
+            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<TsTestValue.TsClass>(test.returnValue) }
+        results.forEach { result ->
+            val value = assertIs<TsTestValue.TsNumber>(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<TsTestValue.TsClass>(test.returnValue) }
+        results.forEach { result ->
+            val value = assertIs<TsTestValue.TsNumber>(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<TsUnknownCall>()
+        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.RECEIVER_CLASS_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",
+        )
+    }
 }

usvm-ts/src/test/resources/samples/lang/MissingSuperclassBase.d.ts

@@ -0,0 +1,3 @@
+declare class MissingSuperclassBase {
+    constructor();
+}

usvm-ts/src/test/resources/samples/lang/MissingSuperclassConstructor.ts

@@ -0,0 +1,7 @@
+/// <reference path="./MissingSuperclassBase.d.ts" />
+
+class MissingSuperclassConstructor extends MissingSuperclassBase {
+    constructor() {
+        super();
+    }
+}

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 {}