From 17c1b3393d49d210765e60ee4595c71cc2ca49cb Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 23:41:48 +0300 Subject: [PATCH 1/2] [TS] Stop unsupported accessor and method-value storage access --- .../machine/expr/DeclaredMemberBoundary.kt | 35 ++++++ .../kotlin/org/usvm/machine/expr/ReadField.kt | 3 + .../org/usvm/machine/expr/WriteField.kt | 3 + .../samples/types/DeclaredMemberReadsTest.kt | 101 ++++++++++++++++++ .../samples/types/DeclaredMemberReads.ts | 41 +++++++ 5 files changed, 183 insertions(+) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt create mode 100644 usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt new file mode 100644 index 0000000000..7cec4f6d58 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt @@ -0,0 +1,35 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsUnclearRefType +import org.usvm.UHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.util.EtsHierarchy +import org.usvm.util.arrayStorageType +import org.usvm.util.getAllFields +import org.usvm.util.hasStringName + +/** EtsIR currently represents accessors and ordinary prototype methods with the same method metadata. */ +internal fun TsContext.ensureSupportedDeclaredMemberAccess( + scope: TsStepScope, + instance: UHeapRef, + local: EtsLocal, + fieldName: String, + hierarchy: EtsHierarchy, +) { + val runtimeType = scope.calcOnState { arrayStorageType(instance, local.type) } + if (runtimeType !is EtsClassType && runtimeType !is EtsUnclearRefType) return + + val owners = hierarchy.classesForType(runtimeType) + val requiresPrototypeMember = owners.any { owner -> + val hasDataField = owner.getAllFields(hierarchy).any { !it.isStatic && it.hasStringName(fieldName) } + !hasDataField && hierarchy.nearestInstanceMethod(owner, methodName = fieldName) != null + } + if (requiresPrototypeMember) { + throw UnsupportedOperationException( + "Declared class member '$fieldName' needs accessor or method-value semantics", + ) + } +} 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 1a94e3d6b8..5c0284b727 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 @@ -165,6 +165,9 @@ private fun TsContext.resolveDeclaredField( // A literal's own declarations, rather than scene-wide same-name fields, determine its initial storage. val objectClass = objectLiteralClass(scope, instance, hierarchy) val wasWritten = scope.calcOnState { (instance to field.name) in writtenConcreteFields } + if (local != null && objectClass == null) { + ensureSupportedDeclaredMemberAccess(scope, instance, local, field.name, hierarchy) + } if (objectClass != null && !wasWritten && !objectClass.hasOwnProperty(field.name)) { scope.ensureMissingPropertyHasNoPrototype(instance, objectClass, field.name) return mkUndefinedValue() 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 76c60cdea2..41f511b33c 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 @@ -237,6 +237,9 @@ fun TsContext.assignToInstanceField( if (wroteModeledErrorField) return Unit val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy) + if (objectLiteralClass == null) { + ensureSupportedDeclaredMemberAccess(scope, unwrappedInstance, instanceLocal, field.name, hierarchy) + } // An object literal can acquire a new own property after creation. Requiring its // allocation type to declare the field would reject that valid JavaScript write. diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt new file mode 100644 index 0000000000..9ae3ed9b13 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt @@ -0,0 +1,101 @@ +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.SolverType +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.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class DeclaredMemberReadsTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val sourcePath = "/samples/types/DeclaredMemberReads.ts" + + override val scene: EtsScene = loadScene(sourcePath) + + @Test + fun `getter and method value reads stop with an explicit limitation`() { + val unsupported = listOf( + "getter", "inheritedGetter", "methodValue", "inheritedMethodValue", "methodWrite", "getterWrite", + ) + for (name in unsupported) { + val method = getMethod(name, className = "DeclaredMemberReads") + val result = TsMachine( + scene = scene, + options = UMachineOptions( + solverType = SolverType.YICES, + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = 20.seconds, + ), + tsOptions = TsOptions(), + ).use { it.analyzeWithMetadata(methods = listOf(method)) } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason, name) + assertTrue(result.states.isEmpty(), name) + assertFalse(result.engineFailed, name) + val hasMemberLimitation = result.unsupportedPaths.any { "accessor or method-value semantics" in it } + assertTrue(hasMemberLimitation, "$name: ${result.unsupportedPaths}") + } + } + + @Test + fun `direct calls own data and own writes retain their values`() { + val expected = mapOf( + "directCall" to 5.0, + "inheritedCall" to 5.0, + "ownData" to 7.0, + "ownWrite" to 9.0, + "callableData" to 11.0, + ) + + for ((name, value) in expected) { + discoverProperties( + method = getMethod(name, className = "DeclaredMemberReads"), + { result -> result.number == value }, + invariants = arrayOf({ result -> result.number == value }), + ) + } + } + + @Test + fun `native replay distinguishes accessors method values and own data`() { + assertNodeReplay( + source = getResourcePath(sourcePath).readText() + "\n" + """ + const subject = new DeclaredMemberReads(); + for (const name of ['getter', 'inheritedGetter']) { + if (subject[name]() !== 3) throw Error(name); + } + for (const name of ['methodValue', 'inheritedMethodValue']) { + if (subject[name]() !== 'function') throw Error(name); + } + const expected = { directCall: 5, inheritedCall: 5, ownData: 7, ownWrite: 9, callableData: 11 }; + for (const [name, value] of Object.entries(expected)) { + if (subject[name]() !== value) throw Error(name); + } + if (subject.methodWrite() !== 9) throw Error('methodWrite'); + let getterWriteThrows = false; + try { subject.getterWrite(); } catch (error) { getterWriteThrows = error instanceof TypeError; } + if (!getterWriteThrows) throw Error('getter assignment must throw in a class method'); + """.trimIndent(), + directory = directory, + name = "declared-member-reads", + timeoutMessage = "Declared member native replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts b/usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts new file mode 100644 index 0000000000..8833c04219 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts @@ -0,0 +1,41 @@ +class PrototypeMembers { + get value(): number { return 3; } + method(): number { return 5; } +} + +class InheritedMembers extends PrototypeMembers {} + +class OwnData extends PrototypeMembers { + method: any = 7; +} + +class CallableData { + value = 1; + callback = (value: number): number => value + 1; +} + +export class DeclaredMemberReads { + getter(): number { return new PrototypeMembers().value; } + inheritedGetter(): number { return new InheritedMembers().value; } + methodValue(): string { return typeof new PrototypeMembers().method; } + inheritedMethodValue(): string { return typeof new InheritedMembers().method; } + directCall(): number { return new PrototypeMembers().method(); } + inheritedCall(): number { return new InheritedMembers().method(); } + ownData(): number { return new OwnData().method; } + ownWrite(): number { + const instance = new CallableData(); + instance.value = 9; + return instance.value; + } + methodWrite(): number { + const instance: any = new PrototypeMembers(); + instance.method = 9; + return instance.method; + } + getterWrite(): number { + const instance: any = new PrototypeMembers(); + instance.value = 9; + return instance.value; + } + callableData(): number { return new CallableData().callback(10); } +} From 371a4659321831999ecacb4835c90785b0a23af6 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 23:55:53 +0300 Subject: [PATCH 2/2] [TS] Preserve method overwrites with unambiguous ordinary signatures --- .../machine/expr/DeclaredMemberBoundary.kt | 20 ++++++++++++++++++- .../org/usvm/machine/expr/WriteField.kt | 9 ++++++++- .../samples/types/DeclaredMemberReadsTest.kt | 9 +++++++-- .../samples/types/DeclaredMemberReads.ts | 19 ++++++++++++++++++ 4 files changed, 53 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt index 7cec4f6d58..23b4d5c4c6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt @@ -1,7 +1,11 @@ package org.usvm.machine.expr +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnclearRefType import org.usvm.UHeapRef import org.usvm.machine.TsContext @@ -18,6 +22,7 @@ internal fun TsContext.ensureSupportedDeclaredMemberAccess( local: EtsLocal, fieldName: String, hierarchy: EtsHierarchy, + isWrite: Boolean = false, ) { val runtimeType = scope.calcOnState { arrayStorageType(instance, local.type) } if (runtimeType !is EtsClassType && runtimeType !is EtsUnclearRefType) return @@ -25,7 +30,9 @@ internal fun TsContext.ensureSupportedDeclaredMemberAccess( val owners = hierarchy.classesForType(runtimeType) val requiresPrototypeMember = owners.any { owner -> val hasDataField = owner.getAllFields(hierarchy).any { !it.isStatic && it.hasStringName(fieldName) } - !hasDataField && hierarchy.nearestInstanceMethod(owner, methodName = fieldName) != null + val method = hierarchy.nearestInstanceMethod(owner, methodName = fieldName) + val writesOrdinaryMethod = isWrite && method?.hasOrdinaryMethodSignature() == true + !hasDataField && method != null && !writesOrdinaryMethod } if (requiresPrototypeMember) { throw UnsupportedOperationException( @@ -33,3 +40,14 @@ internal fun TsContext.ensureSupportedDeclaredMemberAccess( ) } } + +private fun EtsMethod.hasOrdinaryMethodSignature(): Boolean { + // A TypeScript getter has no parameters; a setter has one parameter and returns void. + val returnsPrimitiveValue = returnType == EtsBooleanType || returnType == EtsNumberType || + returnType == EtsStringType + return when (parameters.size) { + 0 -> false + 1 -> returnsPrimitiveValue + else -> true + } +} 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 41f511b33c..ddec7e07da 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 @@ -238,7 +238,14 @@ fun TsContext.assignToInstanceField( val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy) if (objectLiteralClass == null) { - ensureSupportedDeclaredMemberAccess(scope, unwrappedInstance, instanceLocal, field.name, hierarchy) + ensureSupportedDeclaredMemberAccess( + scope = scope, + instance = unwrappedInstance, + local = instanceLocal, + fieldName = field.name, + hierarchy = hierarchy, + isWrite = true, + ) } // An object literal can acquire a new own property after creation. Requiring its diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt index 9ae3ed9b13..5413675a2d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt @@ -31,7 +31,8 @@ class DeclaredMemberReadsTest : TsMethodTestRunner() { @Test fun `getter and method value reads stop with an explicit limitation`() { val unsupported = listOf( - "getter", "inheritedGetter", "methodValue", "inheritedMethodValue", "methodWrite", "getterWrite", + "getter", "inheritedGetter", "methodValue", "inheritedMethodValue", + "methodWrite", "getterWrite", "setterWrite", ) for (name in unsupported) { val method = getMethod(name, className = "DeclaredMemberReads") @@ -62,6 +63,7 @@ class DeclaredMemberReadsTest : TsMethodTestRunner() { "ownData" to 7.0, "ownWrite" to 9.0, "callableData" to 11.0, + "capturedArgumentWrite" to 5.0, ) for ((name, value) in expected) { @@ -84,7 +86,10 @@ class DeclaredMemberReadsTest : TsMethodTestRunner() { for (const name of ['methodValue', 'inheritedMethodValue']) { if (subject[name]() !== 'function') throw Error(name); } - const expected = { directCall: 5, inheritedCall: 5, ownData: 7, ownWrite: 9, callableData: 11 }; + const expected = { + directCall: 5, inheritedCall: 5, ownData: 7, ownWrite: 9, callableData: 11, + capturedArgumentWrite: 5, setterWrite: 9, + }; for (const [name, value] of Object.entries(expected)) { if (subject[name]() !== value) throw Error(name); } diff --git a/usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts b/usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts index 8833c04219..deff1602aa 100644 --- a/usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts +++ b/usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts @@ -14,6 +14,16 @@ class CallableData { callback = (value: number): number => value + 1; } +class SetterMember { + stored = 0; + set value(value: number) { this.stored = value; } +} + +class WritableMethod { + method(ignored: number): number { return 5; } + replace(): number { this.method = () => 9; return 0; } +} + export class DeclaredMemberReads { getter(): number { return new PrototypeMembers().value; } inheritedGetter(): number { return new InheritedMembers().value; } @@ -37,5 +47,14 @@ export class DeclaredMemberReads { instance.value = 9; return instance.value; } + setterWrite(): number { + const instance = new SetterMember(); + instance.value = 9; + return instance.stored; + } + capturedArgumentWrite(): number { + const instance = new WritableMethod(); + return instance.method(instance.replace()); + } callableData(): number { return new CallableData().callback(10); } }