Preserve runtime types and bounded fresh-string fallback semantics

buildSrc/src/main/kotlin/Dependencies.kt

@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "bcad76ffd7"
+    const val jacodb = "7596ae5834"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt

@@ -1,15 +1,30 @@
 package org.usvm.api
 
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsBooleanLiteralType
+import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsNullType
+import org.jacodb.ets.model.EtsNumberLiteralType
+import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsStringLiteralType
+import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUndefinedType
+import org.jacodb.ets.model.EtsUnionType
 import org.jacodb.ets.model.EtsVoidType
 import org.usvm.UAddressSort
+import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
+import org.usvm.machine.types.iteWriteIntoFakeObject
 import org.usvm.machine.types.mkFakeValue
+import org.usvm.sizeSort
+import org.usvm.util.mkStringBackingLValue
+import org.usvm.util.mkStringBackingLengthLValue
 
 fun mockMethodCall(
     scope: TsStepScope,
@@ -37,6 +52,15 @@ internal fun makeFreshUnknownCallResult(
     resultType: EtsType,
 ): UExpr<*> = scope.calcOnState {
     if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue()
+    val literal = makeLiteralResult(resultType)
+    if (literal != null) return@calcOnState literal
+    if (resultType == EtsStringType) return@calcOnState makeFreshBoundedString()
+    if (resultType is EtsUnionType) {
+        val variants = resultType.finiteLiteralVariants()
+        if (!variants.isNullOrEmpty()) {
+            return@calcOnState makeFiniteLiteralUnion(scope = scope, variants = variants)
+        }
+    }
 
     when (val sort = ctx.typeToSort(resultType)) {
         is UAddressSort -> makeSymbolicRefUntyped()
@@ -51,3 +75,74 @@ internal fun makeFreshUnknownCallResult(
         else -> makeSymbolicPrimitive(sort)
     }
 }
+
+private fun EtsType.finiteLiteralVariants(): List<EtsType>? {
+    return when (this) {
+        is EtsUnionType -> {
+            val variants = mutableListOf<EtsType>()
+            for (member in types) {
+                val memberVariants = member.finiteLiteralVariants() ?: return null
+                variants += memberVariants
+            }
+            variants.distinct()
+        }
+
+        is EtsStringLiteralType, is EtsNumberLiteralType, is EtsBooleanLiteralType,
+        EtsNullType, EtsUndefinedType,
+        -> listOf(this)
+
+        EtsBooleanType -> listOf(EtsBooleanLiteralType(value = false), EtsBooleanLiteralType(value = true))
+        else -> null
+    }
+}
+
+private fun TsState.makeLiteralResult(type: EtsType): UExpr<*>? = when (type) {
+    is EtsStringLiteralType -> mkInitializedStringConstant(type.value)
+    is EtsNumberLiteralType -> ctx.mkFp64(type.value)
+    is EtsBooleanLiteralType -> ctx.mkBool(type.value)
+    EtsNullType -> ctx.mkTsNullValue()
+    EtsUndefinedType -> ctx.mkUndefinedValue()
+    else -> null
+}
+
+private fun TsState.makeFiniteLiteralUnion(scope: TsStepScope, variants: List<EtsType>): UExpr<*> {
+    var result = requireNotNull(makeLiteralResult(variants.first()))
+    for (variant in variants.drop(1)) {
+        val selected = makeSymbolicPrimitive(ctx.boolSort)
+        val value = requireNotNull(makeLiteralResult(variant))
+        result = ctx.iteWriteIntoFakeObject(
+            scope = scope,
+            condition = selected,
+            trueBranchValue = value,
+            falseBranchValue = result,
+        )
+    }
+
+    return result
+}
+
+/** An opaque string still has a real bounded UTF-16 backing and cannot become an arbitrary object reference. */
+private fun TsState.makeFreshBoundedString(): UConcreteHeapRef = with(ctx) {
+    val string = memory.allocConcrete(EtsStringType)
+    val characters = memory.allocConcrete(EtsArrayType(elementType = EtsNumberType, dimensions = 1))
+    val length = makeSymbolicPrimitive(sizeSort)
+    val minimum = mkBv(0)
+    val maximum = mkBv(maxStringLength)
+    val lengthBounds = mkAnd(
+        mkBvSignedGreaterOrEqualExpr(length, minimum),
+        mkBvSignedLessOrEqualExpr(length, maximum),
+    )
+    pathConstraints += lengthBounds
+
+    memory.initializeArray(
+        arrayHeapRef = characters,
+        type = stringBackingArrayDescriptor,
+        sort = bv16Sort,
+        sizeSort = sizeSort,
+        contents = (0 until maxStringLength).asSequence().map { makeSymbolicPrimitive(bv16Sort) },
+    )
+    memory.write(mkStringBackingLengthLValue(characters), length, guard = trueExpr)
+    memory.write(mkStringBackingLValue(string), characters, guard = trueExpr)
+    boundedStringBackingRefs += string
+    string
+}

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -11,6 +11,7 @@ import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsEnumValueType
 import org.jacodb.ets.model.EtsGenericType
+import org.jacodb.ets.model.EtsIntersectionType
 import org.jacodb.ets.model.EtsLexicalEnvType
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
@@ -165,6 +166,13 @@ class TsContext(
         is EtsNullType -> addressSort
         is EtsUndefinedType -> addressSort
         is EtsUnionType -> unresolvedSort
+        is EtsIntersectionType -> {
+            val memberSorts = type.types.map(::typeToSort)
+            val commonSort = memberSorts.firstOrNull() ?: unresolvedSort
+            val hasCommonSort = memberSorts.all { it == commonSort }
+
+            if (hasCommonSort) commonSort else unresolvedSort
+        }
         is EtsRefType -> addressSort
         is EtsLexicalEnvType -> addressSort
         is EtsAnyType -> unresolvedSort

usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt

@@ -4,6 +4,7 @@ import org.jacodb.ets.model.EtsAssignStmt
 import org.jacodb.ets.model.EtsCallExpr
 import org.jacodb.ets.model.EtsIfStmt
 import org.jacodb.ets.model.EtsReturnStmt
+import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.model.EtsThrowStmt
 import org.usvm.UBoolExpr
 import org.usvm.machine.call.TsUnknownCallEvent
@@ -21,6 +22,11 @@ interface TsInterpreterObserver : UInterpreterObserver {
         // default empty implementation
     }
 
+    /** Reports a satisfiable path stopped at an explicit runtime modeling boundary. */
+    fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) {
+        // default empty implementation
+    }
+
     fun onAssignStatement(
         simpleValueResolver: TsSimpleValueResolver,
         stmt: EtsAssignStmt,
@@ -74,3 +80,23 @@ interface TsInterpreterObserver : UInterpreterObserver {
         // default empty implementation
     }
 }
+
+/** A feasible execution path stopped because the runtime model deliberately omits [reason]. */
+data class TsRuntimeFeatureLimitationEvent(
+    val statement: EtsStmt,
+    val reason: TsRuntimeFeatureLimitationReason,
+    val detail: String,
+)
+
+/** Stable identifiers for bounded runtime features reported by [TsRuntimeFeatureLimitationEvent]. */
+enum class TsRuntimeFeatureLimitationReason {
+    REGULAR_EXPRESSION_LITERAL,
+    FRONTEND_UNSUPPORTED_VALUE,
+    STRING_CONCAT_OPERAND_CONVERSION,
+    ARRAY_STORAGE_TYPE,
+    ARRAY_NAMED_PROPERTY_READ,
+    ARRAY_NAMED_PROPERTY_WRITE,
+    ARRAY_INDEX_GROWTH,
+    ARRAY_LENGTH_CAPACITY,
+    ARRAY_LENGTH_GROWTH,
+}

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

@@ -10,6 +10,7 @@ import org.jacodb.ets.model.EtsUnknownType
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsRuntimeFeatureLimitationReason
 import org.usvm.machine.TsSizeSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.types.mkFakeValue
@@ -58,7 +59,11 @@ internal fun TsExprResolver.handleArrayAccess(
         return resolveField(scope, value.array, array, field, hierarchy)
     }
     if (receiverType !is EtsArrayType) {
-        throw UnsupportedOperationException("Symbolic object property keys are not supported")
+        stopRuntimeFeatureLimitation(
+            reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE,
+            detail = "Indexed access requires supported storage: static=${value.array.type}, storage=$receiverType",
+        )
+        return null
     }
 
     check(resolvedIndex.sort == fp64Sort) {

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

@@ -2,7 +2,9 @@ package org.usvm.machine.expr
 
 import io.ksmt.utils.asExpr
 import mu.KotlinLogging
+import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsField
 import org.jacodb.ets.model.EtsFieldSignature
@@ -17,6 +19,7 @@ import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUnclearRefType
 import org.jacodb.ets.model.EtsUndefinedType
+import org.jacodb.ets.model.EtsUnknownType
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
@@ -85,11 +88,24 @@ internal fun TsExprResolver.handleInstanceFieldRef(
     val instance = resolveHeapRef(scope, rawInstance) ?: return null
 
     // Handle reading "length" property.
-    if (value.field.name == "length") {
-        val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) }
+    val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) }
+    val usesArrayLength = storageType is EtsArrayType || storageType == EtsStringType ||
+        storageType == EtsAnyType || storageType == EtsUnknownType
+    val nativeTypedArray = storageType is EtsClassType &&
+        storageType.signature.file == EtsClassSignature.UNKNOWN.file &&
+        storageType.signature.name in NATIVE_TYPED_ARRAY_NAMES
+    if (value.field.name == "length" && (usesArrayLength || nativeTypedArray)) {
         val isObjectProperty = storageType is EtsClassType || storageType is EtsUnclearRefType ||
             scope.calcOnState { trackedObjectProperties.any { it.instance == instance && it.name == "length" } }
-        if (!isObjectProperty) return readLengthProperty(scope, instanceLocal, instance, options.maxArraySize)
+        if (!isObjectProperty) {
+            return readLengthProperty(
+                scope = scope,
+                instanceLocal = instanceLocal,
+                instance = instance,
+                maxArraySize = options.maxArraySize,
+                onFeatureLimitation = ::reportRuntimeFeatureLimitation,
+            )
+        }
     }
 
     // Read the field.
@@ -424,3 +440,8 @@ fun TsContext.readStaticField(
     // Read the field.
     return resolveField(scope, null, instance, field, hierarchy)
 }
+
+private val NATIVE_TYPED_ARRAY_NAMES = setOf(
+    "Int8Array", "Uint8Array", "Uint8ClampedArray", "Int16Array", "Uint16Array",
+    "Int32Array", "Uint32Array", "Float32Array", "Float64Array", "BigInt64Array", "BigUint64Array",
+)

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

@@ -12,6 +12,7 @@ import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsRuntimeFeatureLimitationReason
 import org.usvm.machine.TsSizeSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.sizeSort
@@ -26,6 +27,7 @@ fun TsContext.readLengthProperty(
     instanceLocal: EtsLocal,
     instance: UHeapRef,
     maxArraySize: Int,
+    onFeatureLimitation: ((TsRuntimeFeatureLimitationReason, String) -> Unit)? = null,
 ): UExpr<*>? {
     // Determine the array type.
     val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) }
@@ -50,7 +52,13 @@ fun TsContext.readLengthProperty(
             )
         }
 
-        else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type")
+        else -> {
+            val reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE
+            val detail = "Length read requires supported array storage: static=${instanceLocal.type}, storage=$type"
+            onFeatureLimitation?.invoke(reason, detail)
+            scope.doWithState { terminateAsUnsupported(reason = "$reason: $detail") }
+            return null
+        }
     }
 
     // Read the length of the array.