[TS] Fixes in TS interpreter for real projects

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

@@ -249,7 +249,7 @@ fun TsContext.checkReadingInRange(
     )
 }
 
-fun TsContext.checkLengthBounds(
+fun TsContext.ensureLengthBounds(
     scope: TsStepScope,
     length: UExpr<TsSizeSort>,
     maxLength: Int,

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

@@ -1,6 +1,7 @@
 package org.usvm.machine.expr
 
 import io.ksmt.utils.asExpr
+import mu.KotlinLogging
 import org.jacodb.ets.model.EtsArrayAccess
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanType
@@ -20,18 +21,30 @@ import org.usvm.types.first
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
 
+private val logger = KotlinLogging.logger {}
+
 internal fun TsExprResolver.handleArrayAccess(
     value: EtsArrayAccess,
 ): UExpr<*>? = with(ctx) {
     // Resolve the array.
-    val array = resolve(value.array) ?: return null
-    check(array.sort == addressSort) {
-        "Expected address sort for array, got: ${array.sort}"
+    val array = run {
+        val resolved = resolve(value.array) ?: return null
+        if (resolved.isFakeObject()) {
+            scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: run {
+                logger.warn { "UNSAT after ensuring fake object is ref-typed" }
+                return null
+            }
+            resolved.extractRef(scope)
+        } else {
+            check(resolved.sort == addressSort) {
+                "Expected address sort for array, got: ${resolved.sort}"
+            }
+            resolved.asExpr(addressSort)
+        }
     }
-    val arrayRef = array.asExpr(addressSort)
 
     // Check for undefined or null array access.
-    checkUndefinedOrNullPropertyRead(scope, arrayRef, propertyName = "[]") ?: return null
+    checkUndefinedOrNullPropertyRead(scope, array, propertyName = "[]") ?: return null
 
     // Resolve the index.
     val resolvedIndex = resolve(value.index) ?: return null
@@ -49,8 +62,8 @@ internal fun TsExprResolver.handleArrayAccess(
     ).asExpr(sizeSort)
 
     // Determine the array type.
-    val arrayType = if (isAllocatedConcreteHeapRef(arrayRef)) {
-        scope.calcOnState { memory.typeStreamOf(arrayRef).first() }
+    val arrayType = if (isAllocatedConcreteHeapRef(array)) {
+        scope.calcOnState { memory.typeStreamOf(array).first() }
     } else {
         value.array.type
     }
@@ -59,7 +72,7 @@ internal fun TsExprResolver.handleArrayAccess(
     }
 
     // Read the array element.
-    readArray(scope, arrayRef, bvIndex, arrayType)
+    readArray(scope, array, bvIndex, arrayType)
 }
 
 fun TsContext.readArray(
@@ -103,7 +116,11 @@ fun TsContext.readArray(
             index = index,
             type = arrayType,
         )
-        return scope.calcOnState { memory.read(lValue) }
+        val fake = scope.calcOnState { memory.read(lValue) }
+        check(fake.isFakeObject()) {
+            "Expected fake object in concrete array with unresolved element type, got: $fake"
+        }
+        return fake
     }
 
     // If the element type is unresolved, we need to create a fake object

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

@@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr
 import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsUnknownType
 import org.usvm.UExpr
 import org.usvm.UHeapRef
@@ -30,6 +31,11 @@ fun TsContext.readLengthProperty(
             EtsArrayType(EtsUnknownType, dimensions = 1)
         }
 
+        is EtsStringType -> {
+            // Strings are treated as arrays of characters (represented as strings).
+            EtsArrayType(EtsStringType, dimensions = 1)
+        }
+
         else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type")
     }
 
@@ -53,7 +59,7 @@ fun TsContext.readArrayLength(
     }
 
     // Check that the length is within the allowed bounds.
-    checkLengthBounds(scope, length, maxArraySize) ?: return null
+    ensureLengthBounds(scope, length, maxArraySize) ?: return null
 
     // Convert the length to fp64.
     return mkBvToFpExpr(

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

@@ -1160,13 +1160,24 @@ class TsSimpleValueResolver(
         }
 
         if (local.name.startsWith(ANONYMOUS_METHOD_PREFIX)) {
+            val currentMethod = scope.calcOnState { lastEnteredMethod }
             val sig = EtsMethodSignature(
-                enclosingClass = EtsClassSignature.UNKNOWN,
+                enclosingClass = currentMethod.signature.enclosingClass,
                 name = local.name,
                 parameters = emptyList(),
                 returnType = EtsUnknownType,
             )
             val methods = ctx.resolveEtsMethods(sig)
+            if (methods.isEmpty()) {
+                logger.error { "Cannot resolve anonymous method for local: $local" }
+                scope.assert(ctx.mkFalse())
+                return null
+            }
+            if (methods.size > 1) {
+                logger.error { "Multiple methods found for anonymous method local: $local" }
+                scope.assert(ctx.mkFalse())
+                return null
+            }
             val method = methods.single()
             val ref = scope.calcOnState { getMethodRef(method) }
             return ref

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

@@ -1,5 +1,6 @@
 package org.usvm.util
 
+import mu.KotlinLogging
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsField
@@ -12,6 +13,8 @@ import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
 import org.usvm.machine.TsContext
 
+private val logger = KotlinLogging.logger {}
+
 fun TsContext.resolveEtsField(
     instance: EtsLocal?,
     field: EtsFieldSignature,
@@ -68,10 +71,12 @@ private fun tryGetSingleField(
         val clazz = classes.single()
         val fields = clazz.getAllFields(hierarchy).filter { it.name == fieldName }
         if (fields.isEmpty()) {
-            error("No field with name '$fieldName' in class '${clazz.name}'")
+            // logger.warn { "No field with name '$fieldName' in class '${clazz.name}'" }
+            return null
         }
         if (fields.size > 1) {
-            error("Multiple fields with name '$fieldName' in class '${clazz.name}': $fields")
+            logger.warn { "Multiple fields with name '$fieldName' in class '${clazz.name}': $fields" }
+            return null
         }
         return fields.single()
     }

usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt

@@ -0,0 +1,28 @@
+package org.usvm.samples.lang
+
+import org.jacodb.ets.model.EtsScene
+import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.RepeatedTest
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.eq
+
+class Optional : TsMethodTestRunner() {
+    private val tsPath = "/samples/lang/Optional.ts"
+
+    override val scene: EtsScene = loadScene(tsPath)
+
+    @Disabled("Input union types are not supported yet")
+    @RepeatedTest(10, failureThreshold = 1)
+    fun `test nullableArgument`() {
+        val method = getMethod("nullableArgument")
+        discoverProperties<TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { x, r -> (r eq 0) && (x is TsTestValue.TsUndefined) },
+            { x, r -> (r eq 0) && (x is TsTestValue.TsNull) },
+            { x, r -> (r eq 1) && (x is TsTestValue.TsNumber) && (x eq 1) },
+            { x, r -> (r eq 2) && (x is TsTestValue.TsNumber) && (x eq 2) },
+            { x, r -> (r eq 10) && (x is TsTestValue.TsNumber) },
+        )
+    }
+}

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

@@ -0,0 +1,16 @@
+// @ts-nocheck
+// noinspection JSUnusedGlobalSymbols
+
+class Optional {
+    nullableArgument(x: number | null): number {
+        let value: number = 42;
+        if (x === undefined) return 0;
+        if (x !== null) {
+            if (x === 1) return x; // 1
+            value = x;
+            if (x === 2) return value; // 2
+            return 10;
+        }
+        return 0;
+    }
+}