diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 60886e5c49..e7f7c7423f 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/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" diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index d68e3f1e81..ee4c4de708 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt index 9a6d36d630..fb1a454544 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt +++ b/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) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index f0acfefe67..1335278ac1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt index b4bd5d567b..27fc66309d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt +++ b/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) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringCodeUnitConversion.kt new file mode 100644 index 0000000000..7705f4b459 --- /dev/null +++ b/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? { + 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) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index fa6523a116..8eff962178 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index 3bbe16de40..1e582d23c1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/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) 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 95a7cdb50b..82f8d2d61c 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 @@ -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, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteString.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteString.kt new file mode 100644 index 0000000000..77d3354fad --- /dev/null +++ b/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 +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexWriteTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexWriteTest.kt new file mode 100644 index 0000000000..5aa6b244e0 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringIndexWriteTest.kt @@ -0,0 +1,255 @@ +package org.usvm.machine + +import org.jacodb.ets.dto.EtsFileDto +import org.jacodb.ets.dto.toEtsFile +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.generateEtsIR +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class TsStringIndexWriteTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val strictSource = getResourcePath("/models/StringIndexWrites.ts") + private val sloppySource = getResourcePath("/models/StringIndexWritesSloppy.ts") + private val strictFile = loadEtsFileAutoConvert(strictSource, provider = EtsIrProvider.TS_FRONTEND) + private val sloppyFile = loadEtsFileAutoConvert(sloppySource, provider = EtsIrProvider.TS_FRONTEND) + override val scene = EtsScene(listOf(strictFile, sloppyFile)) + override val tsOptions = TsOptions(maxArraySize = 4) + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + val analysis = machine.analyzeWithOutcome(listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), "${method.name}: ${analysis.unsupportedPaths}") + analysis.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `strict symbolic writes throw after evaluating the right side and preserve the string`() { + discoverProperties( + method = method("strictCaught"), + { _, index, result -> index.number == 0.0 && result.number == 1.0 }, + { _, index, result -> index.number != 0.0 && result.number == 2.0 }, + invariants = arrayOf({ _, index, result -> result.number == if (index.number == 0.0) 1.0 else 2.0 }), + ) + } + + @Test + fun `strict writes fail for canonical invalid and length property keys`() { + discoverProperties( + method = method("strictKeys"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `a right side exception precedes the string write error`() { + discoverProperties( + method = method("rightSideThrows"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + + @Test + fun `sloppy symbolic writes ignore the assignment and preserve its value and effects`() { + discoverProperties( + method = method("sloppyWrite", sloppy = true), + { input, _, result -> input.value.isEmpty() && result.value }, + { input, _, result -> input.value.isNotEmpty() && result.value }, + invariants = arrayOf({ _, _, result -> result.value }), + ) + } + + @Test + fun `sloppy keys compound assignment and updates retain immutable string storage`() { + for (name in listOf("sloppyKeys", "sloppyCompound", "sloppyUpdates", "sloppyWhitespaceUpdate")) { + discoverProperties( + method = method(name, sloppy = true), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + } + + @Test + fun `symbolic string updates convert digits whitespace and other code units`() { + val whitespace = setOf( + '\t', '\n', '\u000b', '\u000c', '\r', ' ', '\u00a0', '\u1680', + '\u2028', '\u2029', '\u202f', '\u205f', '\u3000', '\ufeff', + ) + ('\u2000'..'\u200a') + + discoverProperties( + method = method("sloppySymbolicUpdate", sloppy = true), + { input, result -> input.value.length == 1 && input.value[0] in '0'..'9' && !result.number.isNaN() }, + { input, result -> input.value == " " && result.number == 0.0 }, + { _, result -> result.number.isNaN() }, + invariants = arrayOf({ input, result -> + val value = input.value + val expected = when { + value.length != 1 -> Double.NaN + value[0] in '0'..'9' -> value[0].digitToInt().toDouble() + value[0] in whitespace -> 0.0 + else -> Double.NaN + } + + result.number == expected || result.number.isNaN() && expected.isNaN() + }), + ) + } + + @Test + fun `source directives apply to functions and lexically nested calls`() { + val methodNames = listOf( + "ownStrict", + "inheritedStrict", + "strictCaller", + "sloppyCaller", + "inheritedArrow", + "classInScript", + ) + + for (name in methodNames) { + discoverProperties( + method = method(name, sloppy = true), + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `an uncaught strict write returns a TypeError object`() { + discoverProperties( + method = method("uncaught"), + { _, _, result -> assertIs(result.value).name == "TypeError" }, + ) + } + + @Test + fun `legacy string writes without lexical metadata report unsupported`() { + val source = directory.resolve("legacy-string-write.ts") + source.writeText("function legacy() { const target: any = 'abc'; target[0] = 'x'; return 1; }") + val output = generateEtsIR(source, isProject = false, timeout = null, provider = EtsIrProvider.TS_FRONTEND) + val dto = EtsFileDto.loadFromJson(output.readText()) + val legacyClasses = dto.classes.map { clazz -> + val legacyMethods = clazz.methods.map { it.copy(isStrictMode = null) } + clazz.copy(methods = legacyMethods) + } + val legacyDto = dto.copy(classes = legacyClasses) + val legacyFile = legacyDto.toEtsFile() + val legacyMethod = legacyFile.allClasses.flatMap { it.methods }.single { it.name == "legacy" } + val legacyScene = EtsScene(listOf(legacyFile)) + val machineOptions = options.copy(throwExceptionOnStepFailure = false) + + val analysis = TsMachine(scene = legacyScene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyzeWithOutcome(listOf(legacyMethod)) + } + + assertTrue(analysis.states.isEmpty()) + assertEquals(listOf("String property writes require lexical strictness metadata"), analysis.unsupportedPaths) + } + + @Test + fun `generated strict and sloppy write witnesses replay in JavaScript`() { + replay( + source = strictSource, + methodNames = listOf("strictCaught", "strictKeys", "rightSideThrows", "uncaught"), + sloppy = false, + ) + replay( + source = sloppySource, + methodNames = listOf( + "sloppyWrite", + "sloppyKeys", + "sloppyCompound", + "sloppyUpdates", + "sloppySymbolicUpdate", + "sloppyWhitespaceUpdate", + "ownStrict", + "inheritedStrict", + "strictCaller", + "sloppyCaller", + "inheritedArrow", + "classInScript", + ), + sloppy = true, + ) + } + + private fun replay(source: Path, methodNames: List, sloppy: Boolean) { + val script = buildString { + appendLine(source.readText()) + for (name in methodNames) { + for (test in runner(method(name, sloppy = sloppy), options)) { + val arguments = test.before.parameters.joinToString { value -> jsValue(value) } + val receiver = if (sloppy) "" else "new StringIndexWrites()." + val call = "$receiver$name($arguments)" + if (test.returnValue is TsTestValue.TsException.ObjectException) { + appendLine("{ let caught = false; try { $call; }") + appendLine("catch (error) { caught = error instanceof TypeError; }") + appendLine("if (!caught) throw Error('$name TypeError'); }") + } else { + val expected = jsValue(test.returnValue) + + appendLine("if (!Object.is($call, $expected)) throw Error('$name');") + } + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = if (sloppy) "string-writes-sloppy" else "string-writes-strict", + timeoutMessage = "String write replay timed out", + failureContext = script.take(1000), + ) + } + + private fun method(name: String, sloppy: Boolean = false): EtsMethod { + val file = if (sloppy) sloppyFile else strictFile + val className = if (sloppy) DEFAULT_ARK_CLASS_NAME else "StringIndexWrites" + + return file.allClasses.single { it.name == className }.methods.single { it.name == name } + } + + private fun jsValue(value: TsTestValue): String = when (value) { + is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsBoolean -> value.value.toString() + else -> assertIs(value).number.toString() + } +} diff --git a/usvm-ts/src/test/resources/models/StringIndexWrites.ts b/usvm-ts/src/test/resources/models/StringIndexWrites.ts new file mode 100644 index 0000000000..a9ed1def13 --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringIndexWrites.ts @@ -0,0 +1,54 @@ +export class StringIndexWrites { + strictCaught(value: string, index: number): number { + const before = value.charAt(0); + const beforeLength = value.length; + const target: any = value; + let effects = 0; + try { + target[index] = (effects++, "x"); + return -1; + } catch { + if (effects !== 1 || value.length !== beforeLength || value.charAt(0) !== before) { + return -2; + } + return index === 0 ? 1 : 2; + } + } + + strictKeys(): boolean { + let caught = 0; + const value: any = "abc"; + try { value["0"] = "x"; } catch { caught++; } + try { value["01"] = "x"; } catch { caught++; } + try { value[-1] = "x"; } catch { caught++; } + try { value[100] = "x"; } catch { caught++; } + try { value[0.5] = "x"; } catch { caught++; } + try { value[NaN] = "x"; } catch { caught++; } + try { value[Infinity] = "x"; } catch { caught++; } + try { value["length"] = 1; } catch { caught++; } + try { value["extra"] = "x"; } catch { caught++; } + const typedValue = "abc"; + try { typedValue.length = 1; } catch { caught++; } + return caught === 10 && value === "abc" && value[0] === "a" && typedValue.length === 3; + } + + rightSideThrows(): number { + const value: any = "abc"; + try { + value[0] = StringIndexWrites.fail(); + } catch (error) { + return error === 77 ? 1 : -1; + } + return -2; + } + + private static fail(): string { + throw 77; + } + + uncaught(value: string, index: number): string { + const target: any = value; + target[index] = "x"; + return value; + } +} diff --git a/usvm-ts/src/test/resources/models/StringIndexWritesSloppy.ts b/usvm-ts/src/test/resources/models/StringIndexWritesSloppy.ts new file mode 100644 index 0000000000..c53980a104 --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringIndexWritesSloppy.ts @@ -0,0 +1,124 @@ +function sloppyWrite(value: string, index: number): boolean { + const before = value.charAt(0); + const beforeLength = value.length; + const alias = value; + const target: any = value; + let effects = 0; + const assigned = (target[index] = (effects++, "x")); + return effects === 1 && assigned === "x" && value === alias && + value.length === beforeLength && value.charAt(0) === before; +} + +function sloppyKeys(): boolean { + const value: any = "abc"; + value["0"] = "x"; + value["01"] = "x"; + value[-1] = "x"; + value[100] = "x"; + value[0.5] = "x"; + value[NaN] = "x"; + value[Infinity] = "x"; + value["length"] = 1; + const extra = (value["extra"] = "x"); + const typedValue = "abc"; + typedValue.length = 1; + return value === "abc" && value.length === 3 && value[0] === "a" && extra === "x" && typedValue.length === 3; +} + +function sloppyUpdates(): boolean { + const value: any = "4"; + const oldValue = value[0]++; + const newValue = ++value[0]; + return oldValue === 4 && newValue === 5 && value[0] === "4"; +} + +function sloppyCompound(): boolean { + let value = "a"; + const assigned = (value[0] += "b"); + return assigned === "ab" && value[0] === "a"; +} + +function sloppySymbolicUpdate(value: string): number { + if (value.length !== 1) { + return NaN; + } + + const before = value.charAt(0); + const target: any = value; + const oldValue = target[0]++; + if (value.charAt(0) !== before) { + return Infinity; + } + + // Expose conversion witnesses through source branches rather than relying on one arbitrary solver model. + if (value === " ") { + return oldValue; + } + + if (oldValue === 7) { + return oldValue; + } + + return oldValue; +} + +function sloppyWhitespaceUpdate(): boolean { + const value: any = "\u00a0"; + const oldValue = value[0]++; + return oldValue === 0 && value[0] === "\u00a0"; +} + +function ownStrict(value: string): number { + "use strict"; + const target: any = value; + try { target[0] = "x"; } catch { return 1; } + return -1; +} + +function inheritedStrict(value: string): number { + "use strict"; + function nested(): number { + const target: any = value; + try { target[0] = "x"; } catch { return 1; } + return -1; + } + return nested(); +} + +// Strictness follows the callee's lexical source even when the caller uses the other mode. +function sloppyCallee(value: string): number { + const target: any = value; + target[0] = "x"; + return 1; +} + +function strictCaller(value: string): number { + "use strict"; + return sloppyCallee(value); +} + +function sloppyCaller(value: string): number { + return ownStrict(value); +} + +function inheritedArrow(value: string): number { + "use strict"; + const nested = () => { + const target: any = value; + try { target[0] = "x"; } catch { return 1; } + return -1; + }; + return nested(); +} + +class ScriptClass { + write(value: string): number { + const target: any = value; + try { target[0] = "x"; } catch { return 1; } + return -1; + } +} + +function classInScript(value: string): number { + return new ScriptClass().write(value); +}