From 5c2571a7377825e576da0e9bf3ed248a1636d6ef Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:09:54 +0300 Subject: [PATCH 1/5] [TS] Construct instances from runtime constructor values --- .../kotlin/org/usvm/machine/expr/ReadField.kt | 24 +- .../org/usvm/machine/expr/TsExprResolver.kt | 53 +++- .../org/usvm/samples/types/RuntimeNewTest.kt | 231 ++++++++++++++++++ .../resources/samples/types/RuntimeNew.ts | 113 +++++++++ 4 files changed, 414 insertions(+), 7 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt create mode 100644 usvm-ts/src/test/resources/samples/types/RuntimeNew.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index fd27d6f2c5..8c33197cae 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -2,17 +2,22 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import mu.KotlinLogging +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsStaticFieldRef +import org.jacodb.ets.model.EtsUnionType import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.api.typeStreamOf +import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.ensureStaticsInitialized import org.usvm.machine.types.EtsAuxiliaryType import org.usvm.machine.types.mkFakeValue +import org.usvm.types.singleOrNull import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult import org.usvm.util.createFakeField @@ -80,7 +85,24 @@ fun TsContext.readField( is TsResolutionResult.Unique -> typeToSort(etsField.property.type) - is TsResolutionResult.Ambiguous -> unresolvedSort + is TsResolutionResult.Ambiguous -> { + // Dynamic `new` retains a union result type even after allocating a specific class. + // Keep the existing any-typed field representation for unrelated objects. + val runtimeType = if (instanceLocal?.type is EtsUnionType && isAllocatedConcreteHeapRef(instance)) { + scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() } + } else { + null + } + val runtimeClass = (runtimeType as? EtsClassType)?.let { type -> + scene.projectAndSdkClasses.singleOrNull { it.signature == type.signature } + } + val runtimeFields = runtimeClass?.let { clazz -> + val ancestors = hierarchy.getAncestors(clazz) + etsField.properties.filter { it.declaringClass in ancestors } + } + + runtimeFields?.singleOrNull()?.let { typeToSort(it.type) } ?: unresolvedSort + } } scope.doWithState { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 9f94f38c80..587d56614f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -958,8 +958,8 @@ class TsExprResolver( private fun resolveInstanceofConstructor(checkValue: EtsEntity): EtsClassType? = with(ctx) { val constructor = resolve(checkValue) ?: return null - if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwInstanceofTypeError() - if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwInstanceofTypeError() + if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwTypeError() + if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwTypeError() if (constructor.sort != addressSort || constructor.isFakeObject()) { throw UnsupportedOperationException("Unresolved instanceof RHS callability is not modeled") @@ -967,7 +967,7 @@ class TsExprResolver( val constructorRef = constructor as? UConcreteHeapRef ?: throw UnsupportedOperationException("Symbolic instanceof constructor identity is not modeled") - if (getStringConstantValue(constructorRef) != null) return throwInstanceofTypeError() + if (getStringConstantValue(constructorRef) != null) return throwTypeError() val signature = classConstructorSignature(constructorRef) ?: return resolveNonConstructorInstanceofRight(constructorRef) @@ -994,7 +994,7 @@ class TsExprResolver( null } val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull() - if (objectType == EtsStringType) return throwInstanceofTypeError() + if (objectType == EtsStringType) return throwTypeError() val objectClass = (objectType as? EtsClassType)?.let { type -> scene.projectClasses.singleOrNull { it.signature == type.signature } @@ -1009,13 +1009,13 @@ class TsExprResolver( } val isFunction = scope.calcOnState { associatedFunction[ref] != null } - if (ordinaryObject && !hasComputedMember && !isFunction) return throwInstanceofTypeError() + if (ordinaryObject && !hasComputedMember && !isFunction) return throwTypeError() } throw UnsupportedOperationException("Unknown instanceof constructor value: $ref") } - private fun throwInstanceofTypeError(): Nothing? { + private fun throwTypeError(): Nothing? { scope.doWithState { val exception = memory.allocConcrete(TS_TYPE_ERROR_TYPE) methodResult = TsMethodResult.TsException(exception, TS_TYPE_ERROR_TYPE) @@ -1181,6 +1181,8 @@ class TsExprResolver( // region OTHER override fun visit(expr: EtsNewExpr): UExpr? = with(ctx) { + expr.constructorValue?.let { return@with constructRuntimeClass(it) } + // Try to resolve the concrete type if possible. // Otherwise, create an object with UnclearRefType val resolvedType = if (expr.type.isResolved()) { @@ -1206,6 +1208,45 @@ class TsExprResolver( scope.calcOnState { memory.allocConcrete(resolvedType) } } + private fun constructRuntimeClass(constructorValue: EtsValue): UExpr? = with(ctx) { + val constructor = resolve(constructorValue) ?: return@with null + if (constructor.sort == fp64Sort || constructor.sort == boolSort) return@with throwTypeError() + if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return@with throwTypeError() + + if (constructor.sort != addressSort || constructor.isFakeObject()) { + throw UnsupportedOperationException("Unresolved new constructor callability is not modeled") + } + + val constructorRef = constructor as? UConcreteHeapRef + ?: throw UnsupportedOperationException("Symbolic new constructor identity is not modeled") + if (getStringConstantValue(constructorRef) != null) return@with throwTypeError() + + val signature = classConstructorSignature(constructorRef) + ?: return@with resolveNonConstructorNew(constructorRef) + val clazz = scene.projectClasses.singleOrNull { it.signature == signature } + ?: throw UnsupportedOperationException("Unknown new project class: $signature") + + scope.calcOnState { memory.allocConcrete(clazz.type) } + } + + private fun resolveNonConstructorNew(ref: UConcreteHeapRef): Nothing? = with(ctx) { + val objectTypes = if (isAllocatedConcreteHeapRef(ref)) { + scope.calcOnState { memory.typeStreamOf(ref).take(n = 2) } + } else { + null + } + val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull() + val objectClass = (objectType as? EtsClassType)?.let { type -> + scene.projectClasses.singleOrNull { it.signature == type.signature } + } + val isOrdinaryInstance = objectClass?.category == EtsClassCategory.CLASS || + objectClass?.category == EtsClassCategory.OBJECT + val isFunction = scope.calcOnState { associatedFunction[ref] != null } + if (isOrdinaryInstance && !isFunction) return@with throwTypeError() + + throw UnsupportedOperationException("Unknown new constructor value: $ref") + } + override fun visit(expr: EtsNewArrayExpr): UExpr? = with(ctx) { val arrayType = expr.type diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt new file mode 100644 index 0000000000..0126695d23 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt @@ -0,0 +1,231 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import java.nio.file.Path +import java.util.concurrent.TimeUnit +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class RuntimeNewTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/types/RuntimeNew.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `conditional constructor call selects class and executes its constructor`() { + for (methodName in listOf("dynamicCall", "inlineConditional", "localAlias")) { + val method = getMethod(methodName = methodName, className = "RuntimeNew") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = assertIs(test.before.parameters.single()).value + val actual = assertIs(test.returnValue).number + assertEquals(if (input) 1.0 else 0.0, actual, "$methodName($input)") + input to actual + } + assertEquals(setOf(false, true), cases.map { it.first }.toSet(), methodName) + + replay(cases.map { (input, actual) -> + "if (new RuntimeNew().$methodName($input) !== ${actual.toInt()}) " + + "throw Error('$methodName($input)');" + }) + } + } + + @Test + fun `constructor identity is captured before an argument changes its binding`() { + assertSingleNumberResult(methodName = "sideEffectingArgument", expected = 1.0) + + replay(listOf( + "if (new RuntimeNew().sideEffectingArgument() !== 1) throw Error('constructor snapshot');" + )) + } + + @Test + fun `field read uses the selected class when a constructor union has common property names`() { + val numberMethod = getMethod(methodName = "valueFromEither", className = "RuntimeNew") + val numberOutcome = analyze("valueFromEither") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, numberOutcome.stopReason) + assertTrue(numberOutcome.unsupportedPaths.isEmpty(), "${numberOutcome.unsupportedPaths}") + val numberCases = numberOutcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(numberMethod, state) + val input = assertIs(test.before.parameters.single()).value + assertEquals(7.0, assertIs(test.returnValue).number) + input + } + assertEquals(setOf(false, true), numberCases.toSet()) + + val sortMethod = getMethod(methodName = "fieldSortByRuntimeClass", className = "RuntimeNew") + val sortOutcome = analyze("fieldSortByRuntimeClass") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, sortOutcome.stopReason) + assertTrue(sortOutcome.unsupportedPaths.isEmpty(), "${sortOutcome.unsupportedPaths}") + val sortCases = sortOutcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(sortMethod, state) + val input = assertIs(test.before.parameters.single()).value + assertTrue(assertIs(test.returnValue).value) + input + } + assertEquals(setOf(false, true), sortCases.toSet()) + + replay(numberCases.map { input -> + "if (new RuntimeNew().valueFromEither($input) !== 7) throw Error('field number $input');" + } + sortCases.map { input -> + "if (new RuntimeNew().fieldSortByRuntimeClass($input) !== true) throw Error('field sort $input');" + }) + } + + @Test + fun `selected constructor executes exactly once`() { + val method = getMethod(methodName = "constructorCalledOnce", className = "RuntimeNew") + val outcome = analyze("constructorCalledOnce") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = assertIs(test.before.parameters.single()).value + assertTrue(assertIs(test.returnValue).value) + input + } + assertEquals(setOf(false, true), cases.toSet()) + + replay(cases.map { input -> + "if (new RuntimeNew().constructorCalledOnce($input) !== true) throw Error('ctor count $input');" + }) + } + + @Test + fun `direct construction still executes the constructor`() { + assertSingleNumberResult(methodName = "direct", expected = 1.0) + + replay(listOf( + "if (new RuntimeNew().direct() !== 1) throw Error('direct construction');" + )) + } + + @Test + fun `known non constructor throws TypeError`() { + val outcome = analyze("nonConstructable") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> + val exception = assertIs(state.methodResult) + assertEquals("TypeError", exception.type.typeName) + } + + replay(listOf( + "let threwTypeError = false; try { new RuntimeNew().nonConstructable(); } " + + "catch (error) { threwTypeError = error instanceof TypeError; } " + + "if (!threwTypeError) throw Error('non constructor');" + )) + } + + @Test + fun `unmodeled constructor identity is explicitly unsupported`() { + val method = getMethod(methodName = "symbolicConstructor", className = "RuntimeNew") + val outcome = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "${outcome.unsupportedPaths}") + + val unknownOutcome = analyze("unknownConstructor") + assertEquals(TsAnalysisStopReason.EXHAUSTED, unknownOutcome.stopReason) + assertTrue(unknownOutcome.states.isEmpty()) + assertTrue(unknownOutcome.unsupportedPaths.any { "new constructor" in it }, + "${unknownOutcome.unsupportedPaths}") + } + + @Test + fun `known object instance throws TypeError instead of allocating`() { + val outcome = analyze("nonConstructableObject") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> + val exception = assertIs(state.methodResult) + assertEquals("TypeError", exception.type.typeName) + } + + replay(listOf( + "let threwTypeError = false; try { new RuntimeNew().nonConstructableObject(); } " + + "catch (error) { threwTypeError = error instanceof TypeError; } " + + "if (!threwTypeError) throw Error('object constructor');" + )) + } + + private fun assertSingleNumberResult(methodName: String, expected: Double) { + val method = getMethod(methodName = methodName, className = "RuntimeNew") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(expected, assertIs(test.returnValue).number) + } + } + + private fun analyze(methodName: String) = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(getMethod(methodName = methodName, className = "RuntimeNew"))) + } + + private fun replay(assertions: List) { + val script = directory.resolve("runtime-new.ts") + val output = directory.resolve("runtime-new.out") + script.writeText(buildString { + appendLine(getResourcePath(tsPath).readText()) + assertions.forEach(::appendLine) + }) + + val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + + assertTrue(process.waitFor(30, TimeUnit.SECONDS), "Node replay timed out") + assertEquals(0, process.exitValue(), output.readText()) + } + + private val machineOptions = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = 30.seconds, + ) +} diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeNew.ts b/usvm-ts/src/test/resources/samples/types/RuntimeNew.ts new file mode 100644 index 0000000000..67fe9f6daf --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeNew.ts @@ -0,0 +1,113 @@ +class NewA { + value: number; + + constructor(value: number) { + this.value = value; + } +} + +class NewB { + value: number; + + constructor(value: number) { + this.value = value; + } +} + +class NewText { + value: string; + + constructor(_value: number) { + this.value = "seven"; + } +} + +class ConstructorCounter { + count: number; + + constructor() { + this.count = 0; + } +} + +class CountA { + constructor(counter: ConstructorCounter) { + counter.count = counter.count + 1; + } +} + +class CountB { + constructor(counter: ConstructorCounter) { + counter.count = counter.count + 1; + } +} + +class RuntimeNew { + choose(useA: boolean): typeof NewA | typeof NewB { + return useA ? NewA : NewB; + } + + dynamicCall(useA: boolean): number { + const value = new (this.choose(useA))(7); + return value instanceof NewA && value.value === 7 ? 1 : 0; + } + + inlineConditional(useA: boolean): number { + const value = new (useA ? NewA : NewB)(7); + return value instanceof NewA && value.value === 7 ? 1 : 0; + } + + localAlias(useA: boolean): number { + const selected = this.choose(useA); + const alias = selected; + const value = new alias(7); + return value instanceof NewA && value.value === 7 ? 1 : 0; + } + + valueFromEither(useA: boolean): number { + const value = new (this.choose(useA))(7); + return value.value; + } + + fieldSortByRuntimeClass(useNumber: boolean): boolean { + const value = new (useNumber ? NewA : NewText)(7); + return useNumber ? value.value === 7 : value.value === "seven"; + } + + constructorCalledOnce(useA: boolean): boolean { + const counter = new ConstructorCounter(); + const value = new (useA ? CountA : CountB)(counter); + return counter.count === 1 && (value instanceof CountA) === useA; + } + + sideEffectingArgument(): number { + let selected: typeof NewA | typeof NewB = NewA; + const value = new selected((selected = NewB, 7)); + return value instanceof NewA && (value as NewA).value === 7 && selected === NewB ? 1 : 0; + } + + direct(): number { + const value = new NewA(7); + return value instanceof NewA && value.value === 7 ? 1 : 0; + } + + nonConstructable(): number { + const selected: any = 42; + const value = new selected(); + return value instanceof NewA ? 1 : 0; + } + + nonConstructableObject(): number { + const selected: any = new NewA(7); + const value = new selected(); + return value instanceof NewA ? 1 : 0; + } + + symbolicConstructor(selected: typeof NewA): number { + return new selected(7).value; + } + + unknownConstructor(selected: any): number { + return new selected(7).value; + } +} From b3e61ba0f2fb5317df21bd47dbe23d0e824bdfc7 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:47:56 +0300 Subject: [PATCH 2/5] [TS] Keep runtime constructor field writes consistent with reads --- .../kotlin/org/usvm/machine/expr/ReadField.kt | 30 ++---- .../org/usvm/machine/expr/RuntimeFieldSort.kt | 37 +++++++ .../org/usvm/machine/expr/WriteField.kt | 44 +++++++-- .../org/usvm/samples/types/RuntimeNewTest.kt | 99 +++++++++++++++++++ .../resources/samples/types/RuntimeNew.ts | 33 +++++++ 5 files changed, 211 insertions(+), 32 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/RuntimeFieldSort.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 8c33197cae..ef899c880f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -2,22 +2,17 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import mu.KotlinLogging -import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsStaticFieldRef -import org.jacodb.ets.model.EtsUnionType import org.usvm.UExpr import org.usvm.UHeapRef -import org.usvm.api.typeStreamOf -import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.ensureStaticsInitialized import org.usvm.machine.types.EtsAuxiliaryType import org.usvm.machine.types.mkFakeValue -import org.usvm.types.singleOrNull import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult import org.usvm.util.createFakeField @@ -85,24 +80,13 @@ fun TsContext.readField( is TsResolutionResult.Unique -> typeToSort(etsField.property.type) - is TsResolutionResult.Ambiguous -> { - // Dynamic `new` retains a union result type even after allocating a specific class. - // Keep the existing any-typed field representation for unrelated objects. - val runtimeType = if (instanceLocal?.type is EtsUnionType && isAllocatedConcreteHeapRef(instance)) { - scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() } - } else { - null - } - val runtimeClass = (runtimeType as? EtsClassType)?.let { type -> - scene.projectAndSdkClasses.singleOrNull { it.signature == type.signature } - } - val runtimeFields = runtimeClass?.let { clazz -> - val ancestors = hierarchy.getAncestors(clazz) - etsField.properties.filter { it.declaringClass in ancestors } - } - - runtimeFields?.singleOrNull()?.let { typeToSort(it.type) } ?: unresolvedSort - } + is TsResolutionResult.Ambiguous -> resolveAmbiguousFieldSort( + scope = scope, + instanceLocal = instanceLocal, + instance = instance, + fields = etsField.properties, + hierarchy = hierarchy, + ) } scope.doWithState { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RuntimeFieldSort.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RuntimeFieldSort.kt new file mode 100644 index 0000000000..f2815465c7 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/RuntimeFieldSort.kt @@ -0,0 +1,37 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsField +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsUnionType +import org.usvm.UHeapRef +import org.usvm.USort +import org.usvm.api.typeStreamOf +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.types.singleOrNull +import org.usvm.util.EtsHierarchy + +internal fun TsContext.resolveAmbiguousFieldSort( + scope: TsStepScope, + instanceLocal: EtsLocal?, + instance: UHeapRef, + fields: List, + hierarchy: EtsHierarchy, +): USort { + // A dynamic constructor leaves the local union-typed after allocating one concrete class. + // Keep the existing representation for other ambiguous and any-typed fields. + if (instanceLocal?.type !is EtsUnionType || !isAllocatedConcreteHeapRef(instance)) { + return unresolvedSort + } + + val runtimeType = scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() } + val runtimeClass = (runtimeType as? EtsClassType)?.let { type -> + scene.projectAndSdkClasses.singleOrNull { it.signature == type.signature } + } ?: return unresolvedSort + + val ancestors = hierarchy.getAncestors(runtimeClass) + val runtimeField = fields.singleOrNull { it.declaringClass in ancestors } ?: return unresolvedSort + return typeToSort(runtimeField.type) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 2a465cc790..cb755be301 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -3,11 +3,9 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsLocal -import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStaticFieldRef import org.usvm.UExpr import org.usvm.UHeapRef @@ -153,7 +151,34 @@ fun TsContext.assignToInstanceField( val sort = when (etsField) { is TsResolutionResult.Empty -> unresolvedSort is TsResolutionResult.Unique -> typeToSort(etsField.property.type) - is TsResolutionResult.Ambiguous -> unresolvedSort + is TsResolutionResult.Ambiguous -> resolveAmbiguousFieldSort( + scope = scope, + instanceLocal = instanceLocal, + instance = unwrappedInstance, + fields = etsField.properties, + hierarchy = hierarchy, + ) + } + + if (sort !is TsUnresolvedSort && expr.isFakeObject()) { + val fakeType = scope.calcOnState { expr.getFakeType(scope) } + val compatibleType = when (sort) { + boolSort -> fakeType.boolTypeExpr + fp64Sort -> fakeType.fpTypeExpr + addressSort -> fakeType.refTypeExpr + else -> error("Unsupported field sort: $sort") + } + + scope.fork( + compatibleType, + blockOnFalseState = { + terminateAsUnsupported(reason = "Assignment changes runtime sort of field '${field.name}'") + }, + ) ?: return + } + + if (sort !is TsUnresolvedSort && expr.sort != sort && !expr.isFakeObject()) { + throw UnsupportedOperationException("Assignment changes runtime sort of field '${field.name}'") } // If the field type is unknown, we create a fake object for the expr and assign it. @@ -168,26 +193,27 @@ fun TsContext.assignToInstanceField( val lValue = mkFieldLValue(sort, unwrappedInstance, field) if (lValue.sort != expr.sort) { if (expr.isFakeObject()) { - val lhvType = instanceLocal.type - val value = when (lhvType) { - is EtsBooleanType -> { + val value = when (sort) { + boolSort -> { pathConstraints += expr.getFakeType(scope).boolTypeExpr expr.extractBool(scope) } - is EtsNumberType -> { + fp64Sort -> { pathConstraints += expr.getFakeType(scope).fpTypeExpr expr.extractFp(scope) } - else -> { + addressSort -> { pathConstraints += expr.getFakeType(scope).refTypeExpr expr.extractRef(scope) } + + else -> error("Unsupported field sort: $sort") } memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr) } else { - TODO("Support enums fields") + error("Incompatible field value should have been marked unsupported") } } else { memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt index 0126695d23..120936d080 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt @@ -101,6 +101,105 @@ class RuntimeNewTest : TsMethodTestRunner() { }) } + @Test + fun `field writes and aliases use the selected class`() { + for (methodName in listOf("writeToEither", "writeThroughAlias")) { + val method = getMethod(methodName = methodName, className = "RuntimeNew") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = assertIs(test.before.parameters.single()).value + val actual = assertIs(test.returnValue).number + val expected = if (methodName == "writeToEither") 5.0 else 11.0 + assertEquals(expected, actual, "$methodName($input)") + input to actual + } + assertEquals(setOf(false, true), cases.map { it.first }.toSet(), methodName) + + replay(cases.map { (input, actual) -> + "if (new RuntimeNew().$methodName($input) !== ${actual.toInt()}) " + + "throw Error('$methodName($input)');" + }) + } + } + + @Test + fun `field writes respect the selected runtime field sort`() { + val methodName = "writeFieldWithDifferentRuntimeSort" + val method = getMethod(methodName = methodName, className = "RuntimeNew") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = assertIs(test.before.parameters.single()).value + assertTrue(assertIs(test.returnValue).value) + input + } + assertEquals(setOf(false, true), cases.toSet()) + + replay(cases.map { input -> + "if (new RuntimeNew().$methodName($input) !== true) throw Error('$methodName($input)');" + }) + } + + @Test + fun `runtime field sort change is reported as unsupported`() { + val methodName = "writeIncompatibleRuntimeField" + val method = getMethod(methodName = methodName, className = "RuntimeNew") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.any { "Assignment changes runtime sort" in it }, + "${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = assertIs(test.before.parameters.single()).value + assertTrue(assertIs(test.returnValue).value) + input + } + assertEquals(setOf(false), cases.toSet()) + + replay(listOf( + "if (new RuntimeNew().$methodName(false) !== true) throw Error('supported field sort');", + "if (new RuntimeNew().$methodName(true) !== true) throw Error('unsupported field sort');", + )) + } + + @Test + fun `incompatible alternatives of a union field value are reported as unsupported`() { + val methodName = "writePossiblyIncompatibleRuntimeField" + val method = getMethod(methodName = methodName, className = "RuntimeNew") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.any { "Assignment changes runtime sort" in it }, + "${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = test.before.parameters.map { assertIs(it).value } + assertEquals(2, input.size) + assertTrue(assertIs(test.returnValue).value) + input + } + assertEquals(setOf(listOf(true, false), listOf(false, true)), cases.toSet()) + + replay(listOf( + "if (new RuntimeNew().$methodName(true, false) !== true) throw Error('numeric field');", + "if (new RuntimeNew().$methodName(false, true) !== true) throw Error('string field');", + "if (new RuntimeNew().$methodName(true, true) !== true) throw Error('numeric type change');", + "if (new RuntimeNew().$methodName(false, false) !== true) throw Error('string type change');", + )) + } + @Test fun `selected constructor executes exactly once`() { val method = getMethod(methodName = "constructorCalledOnce", className = "RuntimeNew") diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeNew.ts b/usvm-ts/src/test/resources/samples/types/RuntimeNew.ts index 67fe9f6daf..1b8bddf01c 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeNew.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeNew.ts @@ -1,5 +1,6 @@ class NewA { value: number; + onlyA: number = 1; constructor(value: number) { this.value = value; @@ -8,6 +9,7 @@ class NewA { class NewB { value: number; + onlyB: number = 2; constructor(value: number) { this.value = value; @@ -74,6 +76,37 @@ class RuntimeNew { return useNumber ? value.value === 7 : value.value === "seven"; } + writeToEither(useA: boolean): number { + const value = new (useA ? NewA : NewB)(7); + value.value = 5; + return value.value; + } + + writeThroughAlias(useA: boolean): number { + const value = new (useA ? NewA : NewB)(7); + const alias = value; + alias.value = 11; + return value.value; + } + + writeFieldWithDifferentRuntimeSort(useNumber: boolean): boolean { + const value = new (useNumber ? NewA : NewText)(7); + value.value = useNumber ? 9 : "nine"; + return useNumber ? value.value === 9 : value.value === "nine"; + } + + writeIncompatibleRuntimeField(useNumber: boolean): boolean { + const value = new (useNumber ? NewA : NewText)(7); + value.value = "changed"; + return value.value === "changed"; + } + + writePossiblyIncompatibleRuntimeField(useNumber: boolean, writeString: boolean): boolean { + const value = new (useNumber ? NewA : NewText)(7); + value.value = writeString ? "changed" : 9; + return writeString ? value.value === "changed" : value.value === 9; + } + constructorCalledOnce(useA: boolean): boolean { const counter = new ConstructorCounter(); const value = new (useA ? CountA : CountB)(counter); From 0c824bef82bfcf5b57503c3210d982b557b9b2d3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 07:09:34 +0300 Subject: [PATCH 3/5] [TS] Remove redundant field-write checks --- .../org/usvm/machine/expr/WriteField.kt | 29 +++++-------------- 1 file changed, 7 insertions(+), 22 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index cb755be301..cdbb946188 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -192,29 +192,14 @@ fun TsContext.assignToInstanceField( } else { val lValue = mkFieldLValue(sort, unwrappedInstance, field) if (lValue.sort != expr.sort) { - if (expr.isFakeObject()) { - val value = when (sort) { - boolSort -> { - pathConstraints += expr.getFakeType(scope).boolTypeExpr - expr.extractBool(scope) - } - - fp64Sort -> { - pathConstraints += expr.getFakeType(scope).fpTypeExpr - expr.extractFp(scope) - } - - addressSort -> { - pathConstraints += expr.getFakeType(scope).refTypeExpr - expr.extractRef(scope) - } - - else -> error("Unsupported field sort: $sort") - } - memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr) - } else { - error("Incompatible field value should have been marked unsupported") + check(expr.isFakeObject()) + val value = when (sort) { + boolSort -> expr.extractBool(scope) + fp64Sort -> expr.extractFp(scope) + addressSort -> expr.extractRef(scope) + else -> error("Unsupported field sort: $sort") } + memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr) } else { memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) } From eb345a8400681c902150079fa46d1578f66aac38 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 08:52:43 +0300 Subject: [PATCH 4/5] [TS] Reuse shared Node replay for runtime new tests --- .../org/usvm/samples/types/RuntimeNewTest.kt | 22 ++++++++----------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt index 120936d080..cecc9014e4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt @@ -12,11 +12,10 @@ import org.usvm.machine.TsOptions import org.usvm.machine.state.TsMethodResult import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay import org.usvm.util.getResourcePath import java.nio.file.Path -import java.util.concurrent.TimeUnit import kotlin.io.path.readText -import kotlin.io.path.writeText import kotlin.test.assertEquals import kotlin.test.assertIs import kotlin.test.assertTrue @@ -306,20 +305,17 @@ class RuntimeNewTest : TsMethodTestRunner() { } private fun replay(assertions: List) { - val script = directory.resolve("runtime-new.ts") - val output = directory.resolve("runtime-new.out") - script.writeText(buildString { + val source = buildString { appendLine(getResourcePath(tsPath).readText()) assertions.forEach(::appendLine) - }) - - val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) - .redirectErrorStream(true) - .redirectOutput(output.toFile()) - .start() + } - assertTrue(process.waitFor(30, TimeUnit.SECONDS), "Node replay timed out") - assertEquals(0, process.exitValue(), output.readText()) + assertNodeReplay( + source = source, + directory = directory, + name = "runtime-new", + timeoutMessage = "Node replay timed out", + ) } private val machineOptions = UMachineOptions( From acb1283d458d979a775dee8818d7ec5d1a29ba0f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 01:23:26 +0300 Subject: [PATCH 5/5] [TS] Check runtime constructor results through discoverProperties --- .../org/usvm/samples/types/RuntimeNewTest.kt | 59 ++++++++++++++++++- 1 file changed, 58 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt index cecc9014e4..b0ac85bb8f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt @@ -33,6 +33,14 @@ class RuntimeNewTest : TsMethodTestRunner() { fun `conditional constructor call selects class and executes its constructor`() { for (methodName in listOf("dynamicCall", "inlineConditional", "localAlias")) { val method = getMethod(methodName = methodName, className = "RuntimeNew") + + discoverProperties( + method = method, + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 0.0 }, + invariants = arrayOf({ input, result -> result.number == (if (input.value) 1.0 else 0.0) }), + ) + val outcome = analyze(methodName) assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) @@ -66,6 +74,16 @@ class RuntimeNewTest : TsMethodTestRunner() { @Test fun `field read uses the selected class when a constructor union has common property names`() { val numberMethod = getMethod(methodName = "valueFromEither", className = "RuntimeNew") + + withOptions(options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL, stopOnCoverage = 0)) { + discoverProperties( + method = numberMethod, + { input, result -> input.value && result.number == 7.0 }, + { input, result -> !input.value && result.number == 7.0 }, + invariants = arrayOf({ _, result -> result.number == 7.0 }), + ) + } + val numberOutcome = analyze("valueFromEither") assertEquals(TsAnalysisStopReason.EXHAUSTED, numberOutcome.stopReason) @@ -80,6 +98,14 @@ class RuntimeNewTest : TsMethodTestRunner() { assertEquals(setOf(false, true), numberCases.toSet()) val sortMethod = getMethod(methodName = "fieldSortByRuntimeClass", className = "RuntimeNew") + + discoverProperties( + method = sortMethod, + { input, result -> input.value && result.value }, + { input, result -> !input.value && result.value }, + invariants = arrayOf({ _, result -> result.value }), + ) + val sortOutcome = analyze("fieldSortByRuntimeClass") assertEquals(TsAnalysisStopReason.EXHAUSTED, sortOutcome.stopReason) @@ -104,6 +130,15 @@ class RuntimeNewTest : TsMethodTestRunner() { fun `field writes and aliases use the selected class`() { for (methodName in listOf("writeToEither", "writeThroughAlias")) { val method = getMethod(methodName = methodName, className = "RuntimeNew") + val expected = if (methodName == "writeToEither") 5.0 else 11.0 + + discoverProperties( + method = method, + { input, result -> input.value && result.number == expected }, + { input, result -> !input.value && result.number == expected }, + invariants = arrayOf({ _, result -> result.number == expected }), + ) + val outcome = analyze(methodName) assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) @@ -113,7 +148,6 @@ class RuntimeNewTest : TsMethodTestRunner() { val test = TsTestResolver().resolve(method, state) val input = assertIs(test.before.parameters.single()).value val actual = assertIs(test.returnValue).number - val expected = if (methodName == "writeToEither") 5.0 else 11.0 assertEquals(expected, actual, "$methodName($input)") input to actual } @@ -130,6 +164,14 @@ class RuntimeNewTest : TsMethodTestRunner() { fun `field writes respect the selected runtime field sort`() { val methodName = "writeFieldWithDifferentRuntimeSort" val method = getMethod(methodName = methodName, className = "RuntimeNew") + + discoverProperties( + method = method, + { input, result -> input.value && result.value }, + { input, result -> !input.value && result.value }, + invariants = arrayOf({ _, result -> result.value }), + ) + val outcome = analyze(methodName) assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -202,6 +244,14 @@ class RuntimeNewTest : TsMethodTestRunner() { @Test fun `selected constructor executes exactly once`() { val method = getMethod(methodName = "constructorCalledOnce", className = "RuntimeNew") + + discoverProperties( + method = method, + { input, result -> input.value && result.value }, + { input, result -> !input.value && result.value }, + invariants = arrayOf({ _, result -> result.value }), + ) + val outcome = analyze("constructorCalledOnce") assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -288,6 +338,13 @@ class RuntimeNewTest : TsMethodTestRunner() { private fun assertSingleNumberResult(methodName: String, expected: Double) { val method = getMethod(methodName = methodName, className = "RuntimeNew") + + discoverProperties( + method = method, + { result -> result.number == expected }, + invariants = arrayOf({ result -> result.number == expected }), + ) + val outcome = analyze(methodName) assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)