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..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 @@ -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 = 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) 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..092fbcd780 --- /dev/null +++ b/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() + 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 +} 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..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 @@ -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.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", + ) + } } 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 {}