[TS] Stop unsupported accessor and method-value storage access

usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeclaredMemberBoundary.kt

@@ -0,0 +1,53 @@
+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
+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,
+    isWrite: Boolean = false,
+) {
+    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) }
+        val method = hierarchy.nearestInstanceMethod(owner, methodName = fieldName)
+        val writesOrdinaryMethod = isWrite && method?.hasOrdinaryMethodSignature() == true
+        !hasDataField && method != null && !writesOrdinaryMethod
+    }
+    if (requiresPrototypeMember) {
+        throw UnsupportedOperationException(
+            "Declared class member '$fieldName' needs accessor or method-value semantics",
+        )
+    }
+}
+
+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
+    }
+}

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()

usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt

@@ -237,6 +237,16 @@ fun TsContext.assignToInstanceField(
     if (wroteModeledErrorField) return Unit
 
     val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy)
+    if (objectLiteralClass == null) {
+        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
     // allocation type to declare the field would reject that valid JavaScript write.

usvm-ts/src/test/kotlin/org/usvm/samples/types/DeclaredMemberReadsTest.kt

@@ -0,0 +1,106 @@
+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", "setterWrite",
+        )
+        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,
+            "capturedArgumentWrite" to 5.0,
+        )
+
+        for ((name, value) in expected) {
+            discoverProperties<TsTestValue.TsNumber>(
+                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,
+                    capturedArgumentWrite: 5, setterWrite: 9,
+                };
+                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",
+        )
+    }
+}

usvm-ts/src/test/resources/samples/types/DeclaredMemberReads.ts

@@ -0,0 +1,60 @@
+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;
+}
+
+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; }
+    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;
+    }
+    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); }
+}