Respect callee strictness for indexed string writes

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 = "55a0990fa1"
+    const val jacodb = "23199c1843"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

usvm-ts/UNKNOWN_CALL_MODELS.md

@@ -251,8 +251,13 @@ normalization depends on `ts.math.floor`; case conversion needs only the two cod
 String indexing accepts canonical integral numeric positions and canonical numeric string keys. It returns one
 UTF-16 code unit in range and `undefined` out of range, for fractions, or for non-finite numeric positions. Numeric
 property-key conversion preserves symbolic numbers internally until the string property read; general object
-properties still require concrete converted keys. String index writes and other unmodeled String properties
-remain unsupported.
+properties still require concrete converted keys. Primitive String property writes preserve string contents and
+length. The executing method's lexical `isStrictMode` metadata controls the failed write: strict code produces a
+runtime `TypeError`, while sloppy code ignores the write. The assignment expression still yields its right-hand
+value in sloppy mode, and right-hand side effects or exceptions occur before the write in either mode. This
+applies to indexed, named, compound, and update assignments. Callers do not override the callee's strictness.
+Legacy EtsIR without strictness metadata reports these writes as unsupported instead of guessing a mode.
+Other unmodeled String property reads remain unsupported.
 
 Typed symbolic String parameters initialize bounded backing storage, so model guards accept symbolic receivers
 and search strings with known backing, as well as constructed strings. `charAt` accepts symbolic positions, and

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

@@ -3,6 +3,8 @@ package org.usvm.machine
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsFileSignature
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.TsState
 
 private val runtimeFile = EtsFileSignature(
     projectName = "usvm.ts.runtime",
@@ -15,3 +17,8 @@ private val typeErrorSignature = EtsClassSignature(
 
 /** Type identity of terminal JavaScript TypeError exceptions produced by the interpreter. */
 internal val TS_TYPE_ERROR_TYPE = EtsClassType(typeErrorSignature)
+
+internal fun TsState.throwTypeError() {
+    val exception = memory.allocConcrete(TS_TYPE_ERROR_TYPE)
+    methodResult = TsMethodResult.TsException(exception, TS_TYPE_ERROR_TYPE)
+}

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

@@ -273,6 +273,18 @@ fun TsContext.mkNumericExpr(
         return boolToFp(expr.asExpr(boolSort))
     }
 
+    if (expr is UIteExpr<*>) {
+        val trueNumber = mkNumericExpr(expr.trueBranch, scope)
+        val falseNumber = mkNumericExpr(expr.falseBranch, scope)
+
+        return mkIte(expr.condition, trueNumber, falseNumber)
+    }
+
+    val codeUnitNumber = singleCodeUnitToNumber(scope = scope, string = expr.asExpr(addressSort))
+    if (codeUnitNumber != null) {
+        return codeUnitNumber
+    }
+
     // TODO: ToPrimitive, then ToNumber again
     // TODO: probably we need to implement Object (Ref/Fake) -> Number conversion here directly, without ToPrimitive
 

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

@@ -29,7 +29,23 @@ internal fun TsExprResolver.handlePropertyRef(value: EtsPropertyRef): UExpr<*>?
     }
 }
 
-internal fun TsExprResolver.handleAssignToProperty(value: EtsPropertyRef, expr: UExpr<*>): Unit? {
+internal fun TsExprResolver.handleAssignToProperty(value: EtsPropertyRef, expr: UExpr<*>): Unit? = with(ctx) {
+    val receiver = resolve(value.instance) ?: return null
+    val rawReference = if (receiver.isFakeObject()) {
+        scope.assert(receiver.getFakeType(scope).refTypeExpr) ?: return null
+        receiver.extractRef(scope)
+    } else {
+        receiver.asExpr(addressSort)
+    }
+
+    checkUndefinedOrNullPropertyRead(scope, rawReference, propertyName = "[]") ?: return null
+    val reference = resolveHeapRef(scope, rawReference) ?: return null
+    val storageType = scope.calcOnState { arrayStorageType(reference, value.instance.type) }
+    if (storageType == EtsStringType) {
+        resolve(value.key) ?: return null
+        return handleStringPropertyWrite()
+    }
+
     val normalized = normalizePropertyRef(value, isRead = false) ?: return null
 
     return when (normalized) {

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

@@ -0,0 +1,57 @@
+package org.usvm.machine.expr
+
+import io.ksmt.sort.KFp64Sort
+import io.ksmt.utils.cast
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.machine.TsContext
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.util.mkStringBackingElementLValue
+import org.usvm.util.stringCharacters
+import org.usvm.util.stringLength
+
+private val singleCodeUnitWhitespace = listOf(
+    '\t', '\n', '\u000b', '\u000c', '\r', ' ', '\u00a0', '\u1680',
+    '\u2028', '\u2029', '\u202f', '\u205f', '\u3000', '\ufeff',
+) + ('\u2000'..'\u200a')
+
+/** ToNumber for the zero- or one-code-unit Strings produced by indexing and charAt. */
+internal fun TsContext.singleCodeUnitToNumber(scope: TsStepScope, string: UHeapRef): UExpr<KFp64Sort>? {
+    val lengthBound = scope.calcOnState { boundedStringBackingRefs[string] } ?: return null
+    if (lengthBound !in 0..1) {
+        return null
+    }
+
+    val (length, codeUnit) = scope.calcOnState {
+        val characters = stringCharacters(string)
+        val character = mkStringBackingElementLValue(ref = characters, index = mkBv(0))
+
+        stringLength(string) to memory.read(character)
+    }
+    val firstDigit = mkBv('0'.code, bv16Sort)
+    val lastDigit = mkBv('9'.code, bv16Sort)
+    val isDigit = mkAnd(
+        mkBvUnsignedGreaterOrEqualExpr(codeUnit, firstDigit),
+        mkBvUnsignedLessOrEqualExpr(codeUnit, lastDigit),
+    )
+    val digit = mkBvSubExpr(codeUnit, firstDigit)
+    val digitNumber = mkBvToFpExpr(
+        sort = fp64Sort,
+        roundingMode = fpRoundingModeSortDefaultValue(),
+        value = digit.cast(),
+        signed = false,
+    )
+    val whitespaceGuards = singleCodeUnitWhitespace.map { character ->
+        val whitespace = mkBv(character.code, bv16Sort)
+
+        mkEq(codeUnit, whitespace)
+    }
+    val isWhitespace = mkOr(whitespaceGuards)
+    val zero = mkFp64(0.0)
+    val nonDigitNumber = mkIte(isWhitespace, zero, mkFp64NaN())
+    val nonEmptyNumber = mkIte(isDigit, digitNumber, nonDigitNumber)
+    val emptyLength = mkBv(0)
+    val isEmpty = mkEq(length, emptyLength)
+
+    return mkIte(isEmpty, zero, nonEmptyNumber)
+}

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

@@ -111,7 +111,6 @@ import org.usvm.dataflow.ts.infer.tryGetKnownType
 import org.usvm.dataflow.ts.util.type
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.isTrue
-import org.usvm.machine.TS_TYPE_ERROR_TYPE
 import org.usvm.machine.TsConcreteMethodCallStmt
 import org.usvm.machine.TsContext
 import org.usvm.machine.TsInterpreterObserver
@@ -136,6 +135,7 @@ import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.lastStmt
 import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
+import org.usvm.machine.throwTypeError
 import org.usvm.machine.types.EtsNominalType
 import org.usvm.machine.types.iteWriteIntoFakeObject
 import org.usvm.sizeSort
@@ -1291,8 +1291,7 @@ class TsExprResolver(
 
     private fun throwTypeError(): Nothing? {
         scope.doWithState {
-            val exception = memory.allocConcrete(TS_TYPE_ERROR_TYPE)
-            methodResult = TsMethodResult.TsException(exception, TS_TYPE_ERROR_TYPE)
+            this.throwTypeError()
         }
 
         return null

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

@@ -59,7 +59,7 @@ internal fun TsExprResolver.handleAssignToArrayIndex(
     val resolvedIndex = resolve(lhv.index) ?: return null
     val storageType = scope.calcOnState { arrayStorageType(array, lhv.array.type) }
     if (storageType == EtsStringType) {
-        throw UnsupportedOperationException("Writes to string indexes are not modeled")
+        return handleStringPropertyWrite()
     }
 
     val propertyName = concreteStringValue(resolvedIndex)

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

@@ -8,6 +8,7 @@ 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.EtsStringType
 import org.jacodb.ets.model.EtsType
 import org.usvm.UExpr
 import org.usvm.UHeapRef
@@ -88,7 +89,12 @@ internal fun TsExprResolver.handleAssignToInstanceField(
     val instance = resolveHeapRef(scope, rawInstance) ?: return null
     if (!ensureSupportedArrayPrototypeAccess(instance, field.name)) return null
 
-    val arrayType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } as? EtsArrayType
+    val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) }
+    if (storageType == EtsStringType) {
+        return handleStringPropertyWrite()
+    }
+
+    val arrayType = storageType as? EtsArrayType
     if (field.name == "length" && arrayType != null) {
         return assignToArrayLength(
             scope = scope,

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

@@ -0,0 +1,18 @@
+package org.usvm.machine.expr
+
+import org.usvm.machine.throwTypeError
+
+/** Primitive strings are immutable; assignment values and effects were already evaluated by the interpreter. */
+internal fun TsExprResolver.handleStringPropertyWrite(): Unit? {
+    val strictMode = scope.calcOnState { lastEnteredMethod.isStrictMode }
+        ?: throw UnsupportedOperationException("String property writes require lexical strictness metadata")
+    if (!strictMode) {
+        return Unit
+    }
+
+    scope.doWithState {
+        throwTypeError()
+    }
+
+    return null
+}