From d6b239cebfd6040cd775f1180f8a6f9725b65f2a Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 00:47:37 +0300 Subject: [PATCH 1/8] Extract bounded Number.parseFloat model onto current sequence models --- .../call/intrinsic/TsNumberParseFloatModel.kt | 67 +++++++++++ .../usvm/machine/expr/CallApproximations.kt | 2 +- .../call/models/NumberParseFloatModels.ts | 104 ++++++++++++++++++ .../call/TsNumberParseFloatEtsIrTest.kt | 83 ++++++++++++++ .../resources/models/NumberParseFloatEtsIr.ts | 20 ++++ 5 files changed, 275 insertions(+), 1 deletion(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumberParseFloatModel.kt create mode 100644 usvm-ts/src/main/resources/org/usvm/machine/call/models/NumberParseFloatModels.ts create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt create mode 100644 usvm-ts/src/test/resources/models/NumberParseFloatEtsIr.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumberParseFloatModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumberParseFloatModel.kt new file mode 100644 index 0000000000..b6a7d3186a --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumberParseFloatModel.kt @@ -0,0 +1,67 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsStringType +import org.usvm.UConcreteHeapRef +import org.usvm.api.evalTypeEquals +import org.usvm.machine.call.TsEtsIrUnknownCallModel +import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard +import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.call.hasBuiltinGlobalOwner +import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +import org.usvm.util.mkStringBackingLValue +import org.usvm.util.mkStringBackingLengthLValue + +/** Decimal prefix parsing in source, with exact binary64 arithmetic on a guarded finite domain. */ +internal object TsNumberParseFloatModel : TsBuiltInUnknownCallModelFamily { + private const val MAX_INPUT_LENGTH = 32 + + override val models by lazy { + val model = TsEtsIrUnknownCallModel( + id = "ts.number.parseFloat", + target = TsUnknownCallTarget( + methodName = "parseFloat", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ), + artifact = loadBundledEtsIrUnknownCallModelArtifact( + resourceName = "/org/usvm/machine/call/models/NumberParseFloatModels.ts", + sourceFileName = "NumberParseFloatModels.ts", + entryPointClassName = "NumberParseFloatModels", + entryPointMethodName = "parseFloat", + ), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + val owner = call.receiver?.source + if (owner == null || !hasBuiltinGlobalOwner(owner, call.callee, expectedName = "Number")) { + null + } else { + call.arguments.firstOrNull()?.resolved?.let(::listOf) + } + }, + domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> + with(state.ctx) { + val argument = inputs.single() + if (argument.sort != addressSort) return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val input = argument.asExpr(addressSort) + val isStringConstant = input is UConcreteHeapRef && getStringConstantValue(input) != null + val hasBacking = input in state.boundedStringBackingRefs || isStringConstant + if (input.hasFakeValueBranch() || !hasBacking) { + return@TsEtsIrUnknownCallModelDomainGuard falseExpr + } + + val characters = state.memory.read(mkStringBackingLValue(input)) + val length = state.memory.read(mkStringBackingLengthLValue(characters)) + val isString = state.memory.types.evalTypeEquals(input, EtsStringType) + val isBounded = mkAnd( + mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), + mkBvSignedLessOrEqualExpr(length, mkBv(MAX_INPUT_LENGTH)), + ) + mkAnd(isString, isBounded) + } + }, + requiredModelIds = setOf("ts.string.charCodeAt"), + ) + listOf(model) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 4ad94a9251..32e7b31f5c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -65,7 +65,7 @@ internal fun TsExprResolver.tryApproximateGlobalInstanceCall( // Handle `Number` calls. if (hasBuiltinGlobalOwner(owner = expr.instance, callee = expr.callee, expectedName = "Number")) { when (expr.callee.name) { - "isFinite", "isInteger", "isSafeInteger" -> { + "isFinite", "isInteger", "isSafeInteger", "parseFloat" -> { return tryDispatchNumericBuiltin(expr) ?: TsExprApproximationResult.NoApproximation } diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/NumberParseFloatModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/NumberParseFloatModels.ts new file mode 100644 index 0000000000..70d1f26478 --- /dev/null +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/NumberParseFloatModels.ts @@ -0,0 +1,104 @@ +declare class NumberParseFloatPrimitives { + // Deliberately unmodeled: the residual policy handles decimals outside the exact domain. + static unsupportedDecimal(): number; +} + +export class NumberParseFloatModels { + static parseFloat(input: string): number { + const length = input.length; + let index = 0; + while (index < length && NumberParseFloatModels.isWhitespace( + input.charCodeAt(index))) index++; + + let negative = false; + if (index < length) { + const sign = input.charCodeAt(index); + if (sign === 43 || sign === 45) { + negative = sign === 45; + index++; + } + } + if (NumberParseFloatModels.isInfinity(input, index, length)) return negative ? -Infinity : Infinity; + + let coefficient = 0; + let significantDigits = 0; + let digits = 0; + let fractionalDigits = 0; + let point = false; + while (index < length) { + const code = input.charCodeAt(index); + if (code >= 48 && code <= 57) { + const digit = code - 48; + if (coefficient !== 0 || digit !== 0) significantDigits++; + // Keep all arithmetic exact; rejected long mantissas never produce an approximation. + if (significantDigits > 15) return NumberParseFloatPrimitives.unsupportedDecimal(); + coefficient = coefficient * 10 + digit; + digits++; + if (point) fractionalDigits++; + index++; + } else if (code === 46 && !point) { + point = true; + index++; + } else { + break; + } + } + if (digits === 0) return NaN; + + let exponent = 0; + if (index < length) { + const code = input.charCodeAt(index); + if (code === 69 || code === 101) { + index++; + let exponentNegative = false; + if (index < length) { + const sign = input.charCodeAt(index); + if (sign === 43 || sign === 45) { + exponentNegative = sign === 45; + index++; + } + } + // With no exponent digits this remains zero: parseFloat accepts the preceding prefix. + while (index < length) { + const digit = input.charCodeAt(index) - 48; + if (digit < 0 || digit > 9) break; + if (exponent < 1000) exponent = exponent * 10 + digit; + index++; + } + if (exponentNegative) exponent = -exponent; + } + } + if (coefficient === 0) return negative ? -0 : 0; + const scale = exponent - fractionalDigits; + if (scale < -22 || scale > 22) return NumberParseFloatPrimitives.unsupportedDecimal(); + + // Every integer coefficient and every power 10^k, k <= 22, is exactly representable. + // A single final multiply/divide therefore supplies the required binary64 rounding. + let power = 1; + let remaining = scale < 0 ? -scale : scale; + while (remaining > 0) { + power *= 10; + remaining--; + } + const result = scale < 0 ? coefficient / power : coefficient * power; + return negative ? -result : result; + } + + private static isInfinity(input: string, start: number, length: number): boolean { + if (start + 8 > length) return false; + return input.charCodeAt(start) === 73 && + input.charCodeAt(start + 1) === 110 && + input.charCodeAt(start + 2) === 102 && + input.charCodeAt(start + 3) === 105 && + input.charCodeAt(start + 4) === 110 && + input.charCodeAt(start + 5) === 105 && + input.charCodeAt(start + 6) === 116 && + input.charCodeAt(start + 7) === 121; + } + + private static isWhitespace(code: number): boolean { + return (code >= 9 && code <= 13) || code === 32 || code === 160 || code === 5760 || + (code >= 8192 && code <= 8202) || code === 8232 || code === 8233 || code === 8239 || + code === 8287 || code === 12288 || code === 65279; + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt new file mode 100644 index 0000000000..e9176f45cc --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt @@ -0,0 +1,83 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.assertTrue + +class TsNumberParseFloatEtsIrTest : TsMethodTestRunner() { + override val scene = EtsScene( + projectFiles = listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/NumberParseFloatEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + ), + ) + override val tsOptions = TsOptions( + unknownCallFallback = TsResidualCallPolicy.STOP_PATH, + unknownCallModelSelection = TsUnknownCallModelSelection.Only(setOf("ts.number.parseFloat")), + ) + + // This suite exercises the production model catalog instead of the compatibility-only runner. + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + machine.analyze(methods = listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @Test + fun `decimal prefix model preserves numeric results and ignored argument evaluation`() { + val expected = mapOf( + "decimalPrefix" to -1.25, + "exponentPrefix" to 50.0, + "incompleteExponent" to 12.0, + "hexadecimalPrefix" to 0.0, + "secondDecimalPoint" to 1.2, + "unicodeWhitespace" to Double.POSITIVE_INFINITY, + "negativeZero" to Double.NEGATIVE_INFINITY, + "notANumber" to Double.NaN, + "decimalRounding" to 0.100000000000001, + "ignoredArgument" to 13.0, + ) + + for ((methodName, expectedValue) in expected) { + discoverProperties( + method = getMethod(methodName = methodName, className = "NumberParseFloatEtsIr"), + { result -> result.number.toBits() == expectedValue.toBits() }, + invariants = arrayOf({ result -> result.number.toBits() == expectedValue.toBits() }), + ) + } + } + + @Test + fun `decimal outside the exact model domain stays residual`() { + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + val method = getMethod(methodName = "unsupportedMantissa", className = "NumberParseFloatEtsIr") + + val states = TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> + machine.analyze(methods = listOf(method)) + } + + assertTrue(states.isEmpty()) + val modelApplied = TsUnknownCallDecision.ModelApplied(modelId = "ts.number.parseFloat") + assertTrue(events.any { it.decision == modelApplied }) + assertTrue(events.any { it.outcome == TsUnknownCallOutcome.PATH_STOPPED }) + } +} diff --git a/usvm-ts/src/test/resources/models/NumberParseFloatEtsIr.ts b/usvm-ts/src/test/resources/models/NumberParseFloatEtsIr.ts new file mode 100644 index 0000000000..dc7dfdd1cb --- /dev/null +++ b/usvm-ts/src/test/resources/models/NumberParseFloatEtsIr.ts @@ -0,0 +1,20 @@ +// @ts-nocheck + +export class NumberParseFloatEtsIr { + decimalPrefix(): number { return Number.parseFloat(" -1.25rem"); } + exponentPrefix(): number { return Number.parseFloat(".5e+2px"); } + incompleteExponent(): number { return Number.parseFloat("12e-foo"); } + hexadecimalPrefix(): number { return Number.parseFloat("0x10"); } + secondDecimalPoint(): number { return Number.parseFloat("1.2.3"); } + unicodeWhitespace(): number { return Number.parseFloat("\uFEFFInfinity!"); } + negativeZero(): number { return 1 / Number.parseFloat("-0.0"); } + notANumber(): number { return Number.parseFloat("nope"); } + decimalRounding(): number { return Number.parseFloat("0.100000000000001"); } + unsupportedMantissa(): number { return Number.parseFloat("12345678901234567"); } + + ignoredArgument(): number { + let calls = 0; + const result = Number.parseFloat("12px", calls++); + return result + calls; + } +} From cff578b54d397a7fc6121e6e3d00b4d7045e0c4f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:18:48 +0300 Subject: [PATCH 2/8] Restore bounded join reduce and split models with source regressions --- usvm-ts/UNKNOWN_CALL_MODELS.md | 19 +- .../org/usvm/machine/TsInterpreterObserver.kt | 1 + .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 60 +++--- .../intrinsic/TsDenseArrayModelSupport.kt | 100 +++++++++ .../call/intrinsic/TsDenseArrayPrimitives.kt | 157 ++++++++++++++ .../call/intrinsic/TsErrorEtsIrModelFamily.kt | 30 ++- .../intrinsic/TsStringEtsIrModelFamily.kt | 79 +++++++ .../usvm/machine/expr/CallApproximations.kt | 3 +- .../usvm/machine/expr/ErrorModelStorage.kt | 10 +- .../kotlin/org/usvm/machine/state/TsState.kt | 1 + .../main/kotlin/org/usvm/util/ArrayStorage.kt | 11 + .../usvm/machine/call/models/ArrayModels.ts | 35 +++ .../usvm/machine/call/models/ErrorModels.ts | 6 + .../usvm/machine/call/models/StringModels.ts | 48 +++++ .../machine/call/TsGapModelsSourceTest.kt | 203 ++++++++++++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 9 + .../test/resources/models/GapModelSource.ts | 143 ++++++++++++ 17 files changed, 867 insertions(+), 48 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt create mode 100644 usvm-ts/src/test/resources/models/GapModelSource.ts diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 950a3d5af6..94b5e94ae1 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -71,13 +71,17 @@ The built-in catalog includes the following public APIs and their internal stora | `ts.array.pop` | TypeScript/EtsIR body | Zero-argument `pop` on a definitely one-dimensional array that also satisfies the symbolic runtime type guard. | | `ts.array.includes`, `ts.array.indexOf`, `ts.array.lastIndexOf` | TypeScript/EtsIR bodies | One-dimensional arrays and numeric positions, with the missing-slot exclusions below. | | `ts.array.push`, `ts.array.fill`, `ts.array.reverse`, `ts.array.unshift`, `ts.array.slice`, `ts.array.concat` | TypeScript/EtsIR bodies with storage growth/allocation primitives | One-dimensional arrays with length/result at most 16. Push/unshift accept up to three arguments; resolved-sort arrays require matching element sorts, while mixed arrays retain runtime value kinds. Concat accepts one same-type array. Except push and full-range `fill(value)`, these operations require a current dense-array proof. | +| `ts.array.join` | TypeScript/EtsIR body with a primitive element conversion | Dense arrays of at most 16 strings, booleans or nullish values, including runtime overrides in typed storage. Separator must be a string or omitted/undefined; numeric and object element coercion uses fallback. | +| `ts.array.reduce` | TypeScript/EtsIR body | Dense arrays of at most 16 elements and a known source callback. Preserves initial-value omission, accumulator/receiver aliases, captured variables, in-range writes and callback exceptions. Structural mutation uses fallback. | | `ts.string.charAt`, `ts.string.charCodeAt`, `ts.string.includes`, `ts.string.indexOf`, `ts.string.lastIndexOf`, `ts.string.startsWith`, `ts.string.endsWith` | TypeScript/EtsIR bodies | Strings in initialized UTF-16 storage, including symbolic code units and numeric positions. | | `ts.string.slice`, `ts.string.substring`, `ts.string.trim`, `ts.string.trimStart`, `ts.string.trimEnd` | TypeScript/EtsIR bodies | UTF-16 range copying; substring clamps/swaps bounds, and trim uses the ECMAScript whitespace set. | | `ts.string.replaceAll` | TypeScript/EtsIR body | String receiver, string search and string replacement; non-overlapping UTF-16 matches, empty search and ECMAScript dollar substitutions for a dollar sign, the match, its prefix and its suffix. RegExp, callbacks and argument coercions use fallback. | +| `ts.string.split` | TypeScript/EtsIR body with dense string-array allocation | String or omitted/undefined separator and numeric or omitted/undefined limit. Uses exact Uint32 limit conversion. Ordinary split accepts at most 15 input code units; omitted separators and zero limits also accept longer strings. | | `ts.string.toLowerCase`, `ts.string.toUpperCase` | TypeScript/EtsIR bodies | ASCII strings of at most 16 code units; other strings use residual fallback. | | `ts.math.abs`, `ts.math.ceil`, `ts.math.floor`, `ts.math.max`, `ts.math.min`, `ts.math.round`, `ts.math.sqrt`, `ts.math.trunc` | Kotlin FP primitives | Numeric arguments; dynamic coercions use fallback. | | `ts.number.isFinite`, `ts.number.isInteger`, `ts.number.isNaN`, `ts.number.isSafeInteger` | Kotlin FP/type primitives | Non-coercing Number predicates, including runtime-kind guards. | -| `ts.error.constructor` | TypeScript/EtsIR body | Genuine `new Error(message)` with one string argument; initializes `name` and `message`. Other arities, coercions, subclasses, `cause` and stack inspection are outside this model. | +| `ts.number.parseFloat` | TypeScript/EtsIR decimal-prefix parser | String input up to 32 code units; at most 15 significant digits and final decimal scale between -22 and 22. Longer mantissas/scales and argument coercion use fallback. | +| `ts.error.constructor`, `ts.typeError.constructor` | TypeScript/EtsIR bodies | Genuine `new Error(message)` / `new TypeError(message)` with one string argument; initializes `name` and `message`. Other arities, coercions, subclasses, `cause` and stack inspection are outside these models. | | `ts.date.*` (38 IDs) | TypeScript/EtsIR bodies | Numeric Date construction, `UTC`, fixed-clock `now`, getters, setters, `valueOf`, and source `toISOString`; see the Date boundary below. | Matching standard calls are assumed to refer to genuine builtins. Monkey patching and prototype replacement are @@ -98,9 +102,16 @@ model, including through an `any` alias. An unknown or non-array receiver does n the method is named `shift`. A definitely-array receiver with an unresolved element sort remains applicable and uses the fake-value representation described below. -Dense input proofs retain snapshots of the array length and element storage regions. A later write invalidates the -proof conservatively, including writes to another array sharing a region. Consequently, a chain of individually -modeled array methods can still use fallback after its first mutation or copy. +Dense input proofs retain the original receiver length and storage-region snapshots. Join, reduce, reverse and slice +use the receiver's unchanged length as their density check: supported index writes cannot create holes, and deletion +stops explicitly. In-range payload writes and allocations of other arrays therefore preserve this check. Other models +still require unchanged storage-region snapshots and may use fallback after a mutation or copy. Split records a new +dense proof for its returned string array, allowing ordinary compositions such as split/reverse/join. + +Reduce captures the initial length and passes the original array reference to every callback. It checks the dense +shape again after each callback; unsupported structural changes remain residual. Empty reduce without an initial +value throws a modeled TypeError. Join/reduce/split resolve only their meaningful argument prefix, while evaluation +of extra source arguments still happens through the regular interpreter and retains its side effects. ### Runtime limitations and experimental outcomes diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index d6cf60c6ee..3051e1f9de 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -99,6 +99,7 @@ enum class TsRuntimeFeatureLimitationReason { ARRAY_INDEX_GROWTH, ARRAY_ITERATOR_UNSUPPORTED, ARRAY_ELEMENT_KIND_WRITE, + ARRAY_ELEMENT_DELETE, ARRAY_LENGTH_CAPACITY, ARRAY_LENGTH_GROWTH, STRING_ITERATOR_UNSUPPORTED, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index ac1874c52a..0a148aa6bc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -8,7 +8,6 @@ import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsUnknownType -import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.api.initializeArray @@ -33,6 +32,7 @@ import org.usvm.machine.types.TsUnresolvedArrayKind import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.componentType +import org.usvm.util.hasDenseArrayShape import org.usvm.util.initializeArrayKind import org.usvm.util.isUnmodifiedDenseInputArray import org.usvm.util.mkArrayLengthLValue @@ -143,7 +143,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private val denseReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> val (array, arrayType) = state.concreteArray(call, inputs) ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr - if (!state.isUnmodifiedDenseInputArray(array, arrayType)) { + if (!state.hasDenseArrayShape(array, arrayType)) { return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr } @@ -330,6 +330,18 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { listOf( arrayConstructorModel, + sourceModel( + id = "ts.array.join", + methodName = "join", + inputAdapter = TsDenseArrayModelSupport.joinAdapter, + domainGuard = TsDenseArrayModelSupport.joinDomain, + ), + sourceModel( + id = "ts.array.reduce", + methodName = "reduce", + inputAdapter = TsDenseArrayModelSupport.reduceAdapter, + domainGuard = TsDenseArrayModelSupport.denseReceiverDomain, + ), sourceModel( id = "ts.array.pop", methodName = "pop", @@ -385,6 +397,16 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { methodName = "concat", domainGuard = concatDomain, ), + primitiveModel( + methodName = "elementString", + arity = 1, + implementation = TsDenseArrayPrimitives::elementString, + ), + primitiveModel( + methodName = "requireDense", + arity = 1, + implementation = TsDenseArrayPrimitives::requireDense, + ), primitiveModel( methodName = "grow", arity = 2, @@ -422,6 +444,11 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { domainGuard = domainGuard, inputAdapter = inputAdapter, requiredModelIds = buildSet { + if (methodName == "join") add("ts.array.primitive.elementString") + if (methodName == "reduce") { + add("ts.array.primitive.requireDense") + add("ts.typeError.constructor") + } if (methodName in setOf("indexOf", "includes", "lastIndexOf", "fill", "reverse", "slice")) { add(MATH_FLOOR_MODEL_ID) } @@ -445,35 +472,6 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { return artifact.copy(entryPoint = entryPoint) } - private fun TsState.concreteArray( - call: TsUnknownCall, - inputs: List>, - ): Pair? { - val receiver = inputs.firstOrNull() as? UConcreteHeapRef ?: return null - if (with(ctx) { receiver.hasFakeValueBranch() }) return null - - val staticType = call.receiver?.source?.type ?: return null - val arrayType = arrayStorageType(receiver, staticType) as? EtsArrayType ?: return null - if (arrayType.dimensions != 1) return null - - return receiver to arrayType - } - - private fun TsState.boundedArrayGuard( - array: UConcreteHeapRef, - arrayType: EtsArrayType, - maximumLength: Int, - ): UBoolExpr = with(ctx) { - val length = memory.read(mkArrayLengthLValue(array, arrayType)) - val minimumLength = mkBv(0) - val maximumLengthExpr = mkBv(maximumLength) - mkAnd( - memory.types.evalIsSubtype(array, arrayType), - mkBvSignedGreaterOrEqualExpr(length, minimumLength), - mkBvSignedLessOrEqualExpr(length, maximumLengthExpr), - ) - } - private fun primitiveModel( methodName: String, arity: Int, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt new file mode 100644 index 0000000000..e8e8de1ccc --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt @@ -0,0 +1,100 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsStringType +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.api.evalTypeEquals +import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard +import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.resolvedInstanceInputs +import org.usvm.machine.state.TsState +import org.usvm.util.arrayStorageType +import org.usvm.util.hasDenseArrayShape +import org.usvm.util.mkArrayLengthLValue + +internal const val SOURCE_ARRAY_MODEL_CAPACITY = 16 + +internal object TsDenseArrayModelSupport { + val denseReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + val (array, arrayType) = state.concreteArray(call, inputs) + ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + if (!state.hasDenseArrayShape(array, arrayType)) { + return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + } + state.boundedArrayGuard(array, arrayType, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY) + } + + val joinAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 1) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val separator = inputs.getOrNull(1) + ?.takeUnless { it == state.ctx.mkUndefinedValue() } + ?: state.mkInitializedStringConstant(",") + if (separator !is UConcreteHeapRef) return@TsEtsIrUnknownCallModelInputAdapter null + val unsupportedSeparator = separator in state.associatedFunction || + with(state.ctx) { separator.hasFakeValueBranch() } + if (unsupportedSeparator) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + listOf(inputs.first(), separator) + } + + val joinDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val receiverGuard = denseReceiverDomain.evaluate(state, call, inputs) + val separatorGuard = state.memory.types.evalTypeEquals(inputs[1].asExpr(addressSort), EtsStringType) + mkAnd( + receiverGuard, + separatorGuard, + ) + } + } + + val reduceAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (inputs.size < 2) return@TsEtsIrUnknownCallModelInputAdapter null + val callback = inputs[1] as? UConcreteHeapRef + ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (callback !in state.associatedFunction) return@TsEtsIrUnknownCallModelInputAdapter null + listOf( + inputs.first(), + callback, + inputs.getOrNull(2) ?: state.ctx.mkUndefinedValue(), + state.ctx.mkBool(call.arguments.size >= 2), + ) + } +} + +internal fun TsState.concreteArray( + call: TsUnknownCall, + inputs: List>, +): Pair? { + val receiver = inputs.firstOrNull() as? UConcreteHeapRef ?: return null + if (with(ctx) { receiver.hasFakeValueBranch() }) return null + + val staticType = call.receiver?.source?.type ?: return null + val arrayType = arrayStorageType(receiver, staticType) as? EtsArrayType ?: return null + if (arrayType.dimensions != 1) return null + + return receiver to arrayType +} + +internal fun TsState.boundedArrayGuard( + array: UConcreteHeapRef, + arrayType: EtsArrayType, + maximumLength: Int, +): UBoolExpr = with(ctx) { + val length = memory.read(mkArrayLengthLValue(array, arrayType)) + val minimumLength = mkBv(0) + val maximumLengthExpr = mkBv(maximumLength) + mkAnd( + memory.types.evalIsSubtype(array, arrayType), + mkBvSignedGreaterOrEqualExpr(length, minimumLength), + mkBvSignedLessOrEqualExpr(length, maximumLengthExpr), + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt new file mode 100644 index 0000000000..11915eca23 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt @@ -0,0 +1,157 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.UIteExpr +import org.usvm.api.evalTypeEquals +import org.usvm.api.initializeArray +import org.usvm.isFalse +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelSuccessor +import org.usvm.machine.expr.mkFpToUint32AfterValidation +import org.usvm.machine.expr.mkValidArrayLength +import org.usvm.machine.state.TsState +import org.usvm.sizeSort +import org.usvm.util.arrayStorageType +import org.usvm.util.hasDenseArrayShape +import org.usvm.util.markDenseInputArray +import org.usvm.util.mkArrayLengthLValue + +/** Memory and primitive-value operations used by the source split/join/reduce algorithms. */ +internal object TsDenseArrayPrimitives { + private val stringsType = EtsArrayType(EtsStringType, dimensions = 1) + + fun allocateStrings(state: TsState, inputs: List>): TsUnknownCallModelExecution? = + with(state.ctx) { + // All capacity slots are initialized, so subsequent in-range writes preserve density. + if (inputs.single() != mkFp64(SOURCE_ARRAY_MODEL_CAPACITY.toDouble())) return null + execution(guard = trueExpr) { + val descriptor = ctx.arrayDescriptorOf(stringsType) + val array = memory.allocConcrete(stringsType) + val empty = mkInitializedStringConstant("") + memory.initializeArray( + arrayHeapRef = array, + type = descriptor, + sort = ctx.addressSort, + sizeSort = ctx.sizeSort, + contents = List(SOURCE_ARRAY_MODEL_CAPACITY) { empty }.asSequence(), + ) + markDenseInputArray(array = array, type = stringsType) + array + } + } + + fun truncateDense(state: TsState, inputs: List>): TsUnknownCallModelExecution? = + with(state.ctx) { + val array = inputs[0] as? UConcreteHeapRef ?: return null + if (!state.hasDenseArrayShape(array, stringsType)) return null + val length = inputs[1].takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) ?: return null + val validLength = mkValidArrayLength(length) + val converted = mkFpToUint32AfterValidation(length, validLength).asExpr(sizeSort) + val lengthLocation = mkArrayLengthLValue(array, stringsType) + val oldLength = state.memory.read(lengthLocation) + val guard = mkAnd(validLength, mkBvUnsignedLessOrEqualExpr(converted, oldLength)) + execution(guard = guard) { + memory.write(lengthLocation, converted, guard = ctx.trueExpr) + markDenseInputArray(array = array, type = stringsType) + array + } + } + + fun requireDense(state: TsState, inputs: List>): TsUnknownCallModelExecution? { + val array = inputs.single() as? UConcreteHeapRef ?: return null + val type = state.arrayStorageType(array, EtsArrayType(EtsUnknownType, dimensions = 1)) as? EtsArrayType + ?: return null + if (!state.hasDenseArrayShape(array, type)) return null + return execution(guard = state.ctx.trueExpr) { ctx.mkUndefinedValue() } + } + + fun elementString(state: TsState, inputs: List>): TsUnknownCallModelExecution? = + with(state.ctx) { + val value = inputs.single() + if (value.isFakeObject()) { + val kind = value.getFakeType(state.memory) + val ref = value.extractRef(state.memory) + val nullish = mkOr(mkEq(ref, mkUndefinedValue()), mkEq(ref, nullRef)) + val referenceGuard = if (kind.refTypeExpr.isFalse || state.hasUnsafeStringReference(ref)) { + falseExpr + } else { + val isString = state.memory.types.evalTypeEquals(ref, EtsStringType) + mkAnd(kind.refTypeExpr, mkOr(isString, nullish)) + } + val successors = buildList { + if (!kind.boolTypeExpr.isFalse) { + add( + TsUnknownCallModelSuccessor( + guard = kind.boolTypeExpr, + completion = TsUnknownCallModelCompletion.Normal { + booleanString(value.extractBool(memory)) + }, + ) + ) + } + if (!referenceGuard.isFalse) { + add( + TsUnknownCallModelSuccessor( + guard = referenceGuard, + completion = TsUnknownCallModelCompletion.Normal { + ctx.mkIte(nullish, mkInitializedStringConstant(""), ref) + }, + ) + ) + } + } + if (successors.isEmpty()) return null + + return TsUnknownCallModelExecution( + successors = successors, + residualGuard = mkNot(mkOr(kind.boolTypeExpr, referenceGuard)), + ) + } + when { + value.sort == boolSort -> execution(guard = trueExpr) { + booleanString(value.asExpr(ctx.boolSort)) + } + value.sort == addressSort -> { + val ref = value.asExpr(addressSort) + if (state.hasUnsafeStringReference(ref)) return null + val nullish = mkOr(mkEq(ref, mkUndefinedValue()), mkEq(ref, nullRef)) + val guard = mkOr(nullish, state.memory.types.evalTypeEquals(ref, EtsStringType)) + execution(guard = guard) { ctx.mkIte(nullish, mkInitializedStringConstant(""), ref) } + } + else -> null + } + } + + private fun TsState.booleanString(value: UBoolExpr): UHeapRef = with(ctx) { + mkIte(value, mkInitializedStringConstant("true"), mkInitializedStringConstant("false")) + } + + private fun TsState.hasUnsafeStringReference(ref: UHeapRef): Boolean = with(ctx) { + when { + ref.hasFakeValueBranch() -> true + ref is UConcreteHeapRef -> ref in associatedFunction + ref is UIteExpr<*> -> hasUnsafeStringReference(ref.trueBranch.asExpr(addressSort)) || + hasUnsafeStringReference(ref.falseBranch.asExpr(addressSort)) + else -> false + } + } + + private fun execution(guard: UBoolExpr, result: TsState.() -> UExpr<*>): TsUnknownCallModelExecution { + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.Normal(result), + ) + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = with(guard.ctx) { mkNot(guard) }, + ) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt index ea1b1d6896..3c7b8e923f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt @@ -1,6 +1,7 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsStringType @@ -16,13 +17,13 @@ import org.usvm.machine.call.TsUnknownCallModel import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.machine.expr.builtInErrorSignature +import org.usvm.machine.expr.builtInTypeErrorSignature import org.usvm.types.single -/** Narrow built-in `Error(message: string)` constructor model. */ +/** Built-in Error and TypeError constructors with string messages. */ internal object TsErrorEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { const val CONSTRUCTOR_ID: String = "ts.error.constructor" - private const val ERROR_CLASS = "Error" private const val RESOURCE = "/org/usvm/machine/call/models/ErrorModels.ts" private val artifact by lazy { @@ -38,20 +39,34 @@ internal object TsErrorEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { field.enclosingClass.name == "ErrorValue" && field.enclosingClass.file == artifact.file.signature override val models: List by lazy { - listOf(constructorModel()) + listOf( + constructorModel(builtInErrorSignature, modelId = CONSTRUCTOR_ID, methodName = "construct"), + constructorModel( + builtInTypeErrorSignature, + modelId = "ts.typeError.constructor", + methodName = "constructTypeError", + ), + ) } - private fun constructorModel(): TsUnknownCallModel { + private fun constructorModel( + builtinSignature: EtsClassSignature, + modelId: String, + methodName: String, + ): TsUnknownCallModel { val target = TsUnknownCallTarget( methodName = CONSTRUCTOR_NAME, - enclosingClassName = ERROR_CLASS, + enclosingClassName = builtinSignature.name, failureReason = TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, ) + val entryPoint = artifact.file.allClasses.single { it.name == "ErrorModels" } + .methods.single { it.name == methodName } + return TsEtsIrUnknownCallModel( - id = CONSTRUCTOR_ID, + id = modelId, target = target, - artifact = artifact, + artifact = artifact.copy(entryPoint = entryPoint), domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> with(state.ctx) { val receiver = inputs.getOrNull(0) as? UConcreteHeapRef @@ -60,7 +75,6 @@ internal object TsErrorEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr if (messageValue.sort != addressSort) return@TsEtsIrUnknownCallModelDomainGuard falseExpr val message = messageValue.asExpr(addressSort) - val builtinSignature = builtInErrorSignature val builtinErrorType = EtsClassType(signature = builtinSignature) val receiverRuntimeType = state.memory.typeStreamOf(receiver).single() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index e351445103..ec9a33424a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -18,6 +18,7 @@ import org.usvm.machine.call.TsUnknownCallModelSuccessor import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.machine.call.resolvedInstanceInputs +import org.usvm.machine.expr.mkEcmaScriptToUint32 import org.usvm.machine.state.TsState import org.usvm.sizeSort import org.usvm.util.mkStringBackingElementLValue @@ -31,6 +32,7 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private const val PRIMITIVES_CLASS_NAME = "StringModelPrimitives" private const val RESOURCE_NAME = "/org/usvm/machine/call/models/StringModels.ts" private const val REPLACE_ALL_INPUT_COUNT = 3 + private const val DEFAULT_SPLIT_LIMIT = 4294967295.0 private val baseArtifact by lazy { loadBundledEtsIrUnknownCallModelArtifact( @@ -165,6 +167,44 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } } + private val splitAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + with(state.ctx) { + val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val separator = inputs.getOrNull(1) + val omitted = separator == null || separator == mkUndefinedValue() + val limit = inputs.getOrNull(2) + val numericLimit = limit?.takeIf { it.sort == fp64Sort }?.asExpr(fp64Sort) + val convertedLimit = when { + limit == null || limit == mkUndefinedValue() -> mkFp64(DEFAULT_SPLIT_LIMIT) + numericLimit != null -> mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = mkEcmaScriptToUint32(numericLimit), + signed = false, + ) + else -> return@TsEtsIrUnknownCallModelInputAdapter null + } + val search = if (omitted) state.mkInitializedStringConstant("") else requireNotNull(separator) + listOf(inputs.first(), search, convertedLimit, mkBool(omitted)) + } + } + + private val splitDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val stringsGuard = receiverAndSearchDomain.evaluate(state, call, inputs) + if (stringsGuard == falseExpr) return@TsEtsIrUnknownCallModelDomainGuard falseExpr + + val receiver = inputs.first().asExpr(addressSort) + val characters = state.memory.read(mkStringBackingLValue(receiver)) + val length = state.memory.read(mkStringBackingLengthLValue(characters)) + val boundedResult = mkBvSignedLessOrEqualExpr(length, mkBv(SOURCE_ARRAY_MODEL_CAPACITY - 1)) + val zeroLimit = mkFpEqualExpr(inputs[2].asExpr(fp64Sort), mkFp64(0.0)) + val omittedSeparator = inputs[3].asExpr(boolSort) + mkAnd(stringsGuard, mkOr(boundedResult, zeroLimit, omittedSeparator)) + } + } + private val asciiReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> with(state.ctx) { val receiverGuard = receiverDomain.evaluate(state, call, inputs) @@ -202,6 +242,12 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { override val models: List by lazy { listOf( + sourceModel( + id = "ts.string.split", + methodName = "split", + inputAdapter = splitAdapter, + domainGuard = splitDomain, + ), sourceModel( id = "ts.string.charAt", methodName = "charAt", @@ -292,6 +338,16 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = receiverOnlyAdapter, domainGuard = asciiReceiverDomain, ), + arrayPrimitiveModel( + methodName = "allocateStrings", + arity = 1, + implementation = TsDenseArrayPrimitives::allocateStrings, + ), + arrayPrimitiveModel( + methodName = "truncateDense", + arity = 2, + implementation = TsDenseArrayPrimitives::truncateDense, + ), primitiveModel( methodName = "codeUnitAt", arity = 2, @@ -321,6 +377,10 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { domainGuard = domainGuard, inputAdapter = inputAdapter, requiredModelIds = buildSet { + if (methodName == "split") { + add("ts.array.primitive.allocateStrings") + add("ts.array.primitive.truncateDense") + } val convertsCase = methodName in setOf("toUpperCase", "toLowerCase") if (convertsCase) { add(PRIMITIVE_CODE_UNIT_AT_ID) @@ -363,6 +423,25 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { implementation = implementation, ) + private val arrayPrimitiveClassSignature by lazy { + baseArtifact.file.allClasses.single { it.name == "ArrayModelPrimitives" }.signature + } + + private fun arrayPrimitiveModel( + methodName: String, + arity: Int, + implementation: (TsState, List>) -> TsUnknownCallModelExecution?, + ): TsUnknownCallModel = TsPrimitiveUnknownCallModel( + idPrefix = "ts.array.primitive", + methodName = methodName, + enclosingClassName = "ArrayModelPrimitives", + arity = arity, + helperClassSignature = { arrayPrimitiveClassSignature }, + sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass }, + owningModelIds = { sourceModelIds }, + implementation = implementation, + ) + private fun stringCodeUnitAt( state: TsState, inputs: List>, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 32e7b31f5c..120776dd90 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -182,8 +182,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( allowUnqualifiedTarget = true, ) - // join has no source model yet; the model run intentionally sends it to the residual policy. - if (modeledArrayCall || (usesModelDispatcher && expr.callee.name == "join")) { + if (modeledArrayCall) { dispatchArrayModel(stmt) return TsExprApproximationResult.ResolveFailure } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt index cbddae1432..cb0561b411 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt @@ -23,6 +23,8 @@ import org.usvm.types.singleOrNull import org.usvm.util.boxArrayValue internal val builtInErrorSignature = EtsClassSignature.UNKNOWN.copy(name = "Error") +internal val builtInTypeErrorSignature = EtsClassSignature.UNKNOWN.copy(name = "TypeError") +private val builtInErrorSignatures = setOf(builtInErrorSignature, builtInTypeErrorSignature) /** Matches exact SDK identities and the interpreter's own TypeError, excluding source class shadows. */ internal fun EtsType.isModeledErrorType(): Boolean = @@ -39,7 +41,7 @@ internal fun EtsFieldSignature.isErrorModelStorageDefinitionField(): Boolean = (name == ERROR_NAME_STORAGE_FIELD || name == ERROR_MESSAGE_STORAGE_FIELD) internal fun EtsFieldSignature.isUnresolvedErrorField(): Boolean = - enclosingClass == builtInErrorSignature && (name == "name" || name == "message") + enclosingClass in builtInErrorSignatures && (name == "name" || name == "message") internal enum class ErrorStorageField { NAME, MESSAGE } @@ -60,7 +62,7 @@ private fun EtsFieldSignature.errorModelDefinitionStorageField(): ErrorStorageFi } internal fun EtsFieldSignature.errorModelStorageField(): ErrorStorageField? { - if (enclosingClass != builtInErrorSignature && enclosingClass != EtsClassSignature.UNKNOWN) { + if (enclosingClass !in builtInErrorSignatures && enclosingClass != EtsClassSignature.UNKNOWN) { return null } @@ -88,7 +90,9 @@ private fun TsContext.resolveErrorStorageField( val concreteInstance = instance as? UConcreteHeapRef ?: return null val runtimeType = scope.calcOnState { memory.typeStreamOf(concreteInstance).singleOrNull() } - return candidateStorageField.takeIf { runtimeType == EtsClassType(signature = builtInErrorSignature) } + return candidateStorageField.takeIf { + runtimeType is EtsClassType && runtimeType.signature in builtInErrorSignatures + } } internal fun TsContext.readModeledErrorField( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index e6c717f6a2..53d14765d2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -382,6 +382,7 @@ class TsState( /** Snapshot of the regions that establish dense Calls input-array contents. */ data class TsDenseInputArray( val type: EtsArrayType, + val length: UExpr, val lengthRegion: UReadOnlyMemoryRegion<*, *>, val elementRegion: UReadOnlyMemoryRegion<*, *>, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt index 136c13370c..54ea54872d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt @@ -96,8 +96,10 @@ fun TsState.markDenseInputArray( val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) val elementRegionId = UArrayRegionId(descriptor, elementSort) + val length = memory.read(mkArrayLengthLValue(array, type)) denseInputArrays[array] = TsDenseInputArray( type = type, + length = length, lengthRegion = memory.getRegion(lengthRegionId), elementRegion = memory.getRegion(elementRegionId), ) @@ -121,3 +123,12 @@ internal fun TsState.isUnmodifiedDenseInputArray( memory.getRegion(lengthRegionId) === snapshot.lengthRegion && memory.getRegion(elementRegionId) === snapshot.elementRegion } + +/** In-range payload writes preserve density; unsupported deletions stop before stale values can escape. */ +internal fun TsState.hasDenseArrayShape(array: UConcreteHeapRef, type: EtsArrayType): Boolean = with(ctx) { + val snapshot = denseInputArrays[array] ?: return false + if (snapshot.type != type) return false + + // Writes to other arrays share a region without changing this receiver's shape. + memory.read(mkArrayLengthLValue(array, type)) == snapshot.length +} diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts index db3b8b86c7..7df2c6545e 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts @@ -2,9 +2,44 @@ declare class ArrayModelPrimitives { static grow(receiver: any[], length: number): void; static allocate(length: number): any[]; static allocateLike(receiver: any[], length: number): any[]; + static elementString(value: any): string; + static requireDense(receiver: any[]): void; } export class ArrayModels { + static join(receiver: any[], separator: string): string { + const length = receiver.length; + let result = ""; + let index = 0; + while (index < length) { + if (index !== 0) result += separator; + result += ArrayModelPrimitives.elementString(receiver[index]); + index++; + } + return result; + } + + static reduce(receiver: any[], callback: (acc: any, current: any, index: number, array: any[]) => any, + initial: any, hasInitial: boolean): any { + const length = receiver.length; + if (length === 0 && !hasInitial) throw new TypeError("Reduce of empty array with no initial value"); + + let accumulator = initial; + let index = 0; + if (!hasInitial) { + accumulator = receiver[0]; + index = 1; + } + while (index < length) { + accumulator = callback(accumulator, receiver[index], index, receiver); + // Element mutation is supported. Structural mutation/deletion remains residual + // until the engine can represent HasProperty for holes after arbitrary callbacks. + ArrayModelPrimitives.requireDense(receiver); + index++; + } + return accumulator; + } + static fromLength(length: number): any[] { return ArrayModelPrimitives.allocate(length); } diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ErrorModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ErrorModels.ts index ca847a6ea2..fc34c648da 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ErrorModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ErrorModels.ts @@ -5,6 +5,12 @@ export class ErrorValue { } export class ErrorModels { + static constructTypeError(receiver: ErrorValue, message: string): ErrorValue { + receiver.__usvmErrorName = "TypeError"; + receiver.__usvmErrorMessage = message; + return receiver; + } + static construct(receiver: ErrorValue, message: string): ErrorValue { receiver.__usvmErrorName = "Error"; receiver.__usvmErrorMessage = message; diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts index f475de2afc..5ee6af4642 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts @@ -3,7 +3,55 @@ declare class StringModelPrimitives { static fromCodeUnit(codeUnit: number): string; } +declare class ArrayModelPrimitives { + static allocateStrings(length: number): string[]; + static truncateDense(receiver: string[], length: number): string[]; +} + export class StringModels { + static split(receiver: string, separator: string, limit: number, omitted: boolean): string[] { + const result = ArrayModelPrimitives.allocateStrings(16); + // The adapter supplies an exact uint32 limit, including the omitted default. + if (limit === 0) return ArrayModelPrimitives.truncateDense(result, 0); + if (omitted) { + result[0] = receiver; + return ArrayModelPrimitives.truncateDense(result, 1); + } + + const length = receiver.length; + const separatorLength = separator.length; + let count = 0; + if (separatorLength === 0) { + while (count < length && count < limit) { + result[count] = receiver[count]; + count++; + } + return ArrayModelPrimitives.truncateDense(result, count); + } + + let start = 0; + let position = 0; + while (position + separatorLength <= length) { + let offset = 0; + while (offset < separatorLength && + receiver[position + offset] === + separator[offset]) { + offset++; + } + if (offset === separatorLength) { + result[count] = StringModels.slice(receiver, start, position); + count++; + if (count === limit) return ArrayModelPrimitives.truncateDense(result, count); + position += separatorLength; + start = position; + } else { + position++; + } + } + result[count] = StringModels.slice(receiver, start, length); + return ArrayModelPrimitives.truncateDense(result, count + 1); + } + static charAt(receiver: string, index: number): string { const length = receiver.length; const integerIndex = StringModels.normalizeCharIndex(index, length); diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt new file mode 100644 index 0000000000..9937ba27a0 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt @@ -0,0 +1,203 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +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.machine.TsAnalysisStopReason +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +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.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class TsGapModelsSourceTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/GapModelSource.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + override val tsOptions = TsOptions(maxArraySize = 16) + 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, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `split and reduce preserve source values aliases and ignored argument effects`() { + for (name in listOf("splitEdges", "reduceAliases", "reduceEmptyError", "ignoredArguments")) { + discoverProperties( + method = method(name), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + } + + @Test + fun `join preserves composition nullish elements and runtime boolean overrides`() { + val expectedValues = mapOf( + "composedMutations" to "cba", + "independentArrays" to "abcd", + "joinRuntimeKinds" to "--true-false", + ) + + for ((name, expected) in expectedValues) { + discoverProperties( + method = method(name), + { result -> result.value == expected }, + invariants = arrayOf({ result -> result.value == expected }), + ) + } + } + + @Test + fun `reduce preserves callback effects optional initial values and thrown values`() { + val expectedValues = mapOf( + "reduceMutation" to 75.0, + "reduceOmitted" to 6.0, + "reduceUndefined" to 8.0, + "reduceInitialEmpty" to 12.0, + "reduceThrows" to 7.0, + ) + + for ((name, expected) in expectedValues) { + discoverProperties( + method = method(name), + { result -> result.number == expected }, + invariants = arrayOf({ result -> result.number == expected }), + ) + } + } + + @Test + fun `join keeps symbolic boolean kinds and source selected lengths`() { + discoverProperties( + method = method("symbolicBooleans"), + { first, second, both, result -> + first.value && !second.value && both.value && result.value == "true-false" + }, + { first, _, both, result -> !first.value && !both.value && result.value == "false" }, + invariants = arrayOf({ first, second, both, result -> + val expected = if (both.value) "${first.value}-${second.value}" else first.value.toString() + + result.value == expected + }), + ) + } + + @Test + fun `unrelated helpers and unsupported coercions remain residual`() { + val residualCallees = mapOf( + "unrelatedPrivateHelper" to "elementString", + "joinCallable" to "join", + "splitCallable" to "split", + "joinNumbers" to "elementString", + "splitLong" to "split", + "reduceShrink" to "requireDense", + ) + + for ((name, callee) in residualCallees) { + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + val analysis = TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer) + .use { machine -> machine.analyzeWithOutcome(listOf(method(name))) } + + assertTrue(analysis.states.isEmpty(), name) + val expectedResidual = events.any { event -> + event.callee.name == callee && event.outcome == TsUnknownCallOutcome.PATH_STOPPED + } + assertTrue(expectedResidual, "$name: $events") + } + } + + @Test + fun `callback deletion cannot escape as a stale exception payload`() { + val limitations = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + val analysis = TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer) + .use { machine -> machine.analyzeWithOutcome(listOf(method("reduceDeleteThrows"))) } + + assertTrue(analysis.states.isEmpty()) + assertTrue(limitations.any { it.reason == TsRuntimeFeatureLimitationReason.ARRAY_ELEMENT_DELETE }) + } + + @Test + fun `generated model witnesses replay in JavaScript`() { + val methodNames = listOf( + "splitEdges", "reduceAliases", "reduceEmptyError", "ignoredArguments", "composedMutations", + "independentArrays", "joinRuntimeKinds", "reduceMutation", "reduceOmitted", "reduceUndefined", + "reduceInitialEmpty", "reduceThrows", "symbolicBooleans", + ) + val script = buildString { + appendLine(source.readText()) + for (name in methodNames) { + for (test in runner(method(name), options)) { + val arguments = test.before.parameters.joinToString { jsValue(it) } + val expected = jsValue(test.returnValue) + + appendLine( + "if (!Object.is(new GapModelSource().$name($arguments), $expected)) throw Error('$name');" + ) + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "gap-model-source-witnesses", + timeoutMessage = "Sequence and callback model replay timed out", + ) + } + + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "GapModelSource") + + 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/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index 8c3ec5deff..377b8647e9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -185,12 +185,18 @@ class TsUnknownCallModelCatalogTest { "ts.array.includes", "ts.array.indexOf", "ts.array.isArray", + "ts.array.join", "ts.array.lastIndexOf", "ts.array.pop", "ts.array.primitive.allocate", "ts.array.primitive.allocateLike", + "ts.array.primitive.allocateStrings", + "ts.array.primitive.elementString", "ts.array.primitive.grow", + "ts.array.primitive.requireDense", + "ts.array.primitive.truncateDense", "ts.array.push", + "ts.array.reduce", "ts.array.reverse", TsArrayShiftIntrinsicModel.MODEL_ID, "ts.array.slice", @@ -208,6 +214,7 @@ class TsUnknownCallModelCatalogTest { TsNumericIntrinsicModelFamily.NUMBER_IS_INTEGER_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_NAN_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID, + "ts.number.parseFloat", "ts.string.charAt", "ts.string.charCodeAt", "ts.string.endsWith", @@ -218,6 +225,7 @@ class TsUnknownCallModelCatalogTest { "ts.string.primitive.fromCodeUnit", "ts.string.replaceAll", "ts.string.slice", + "ts.string.split", "ts.string.startsWith", "ts.string.substring", "ts.string.toLowerCase", @@ -225,6 +233,7 @@ class TsUnknownCallModelCatalogTest { "ts.string.trim", "ts.string.trimEnd", "ts.string.trimStart", + "ts.typeError.constructor", ) assertEquals(expectedModelIds, catalog.modelIds.filterNot { it.startsWith("ts.date.") }) diff --git a/usvm-ts/src/test/resources/models/GapModelSource.ts b/usvm-ts/src/test/resources/models/GapModelSource.ts new file mode 100644 index 0000000000..1fa89f16a2 --- /dev/null +++ b/usvm-ts/src/test/resources/models/GapModelSource.ts @@ -0,0 +1,143 @@ +declare class ArrayModelPrimitives { + static elementString(value: boolean): string; +} + +export class GapModelSource { + private numbers(): number[] { + // The cast deliberately changes the declared type; runtime storage and overrides must survive it. + const values = "a,b,c".split(",") as unknown as number[]; + values[0] = 1; + values[1] = 2; + values[2] = 3; + return values; + } + + splitEdges(): boolean { + const fields = ",a,,".split(","); + return fields.length === 4 && fields[0] === "" && fields[1] === "a" && fields[3] === "" && + "abc".split().join() === "abc" && "abc".split(undefined).join() === "abc" && + "".split("").length === 0 && "".split(",").length === 1 && + "abc".split("", 0).length === 0 && "abc".split("", 2).join("-") === "a-b" && + "abc".split("", 4294967297).join("") === "a" && + "abcdefghijklmnop".split().length === 1 && "abcdefghijklmnop".split("", 0).length === 0 && + "😀".split("").length === 2 && "😀".split("").join("") === "😀"; + } + + composedMutations(): string { + return "abc".split("").reverse().join(""); + } + + independentArrays(): string { + const first = "ab".split(""); + const second = "cd".split(""); + return first.join("") + second.join(""); + } + + joinRuntimeKinds(): string { + const values = "a,b,c,d".split(",") as any[]; + values[0] = null; + values[1] = undefined; + values[2] = true; + values[3] = false; + return values.join("-"); + } + + symbolicBooleans(first: boolean, second: boolean, both: boolean): string { + const values = "a,b".split(",", both ? 2 : 1) as unknown as boolean[]; + values[0] = first; + if (values.length > 1) values[1] = second; + return values.join("-"); + } + + reduceMutation(): number { + const values = this.numbers(); + const multiplier = 2; + const result = values.reduce((acc, current, index, array) => { + if (index === 0) array[1] = 10; + return acc + current * multiplier + index; + }, 4); + return result + values[1] * 4; + } + + reduceOmitted(): number { + return this.numbers().reduce((acc, value) => acc + value); + } + + reduceUndefined(): number { + return "a".split("").reduce((acc, value) => acc === undefined ? 8 : 9, undefined); + } + + reduceAliases(): boolean { + const values = this.numbers(); + const seed = { total: 0 }; + const result = values.reduce((acc, value, index, array) => { + if (array !== values) throw 99; + acc.total += value; + return acc; + }, seed); + return result === seed && seed.total === 6; + } + + reduceEmptyError(): boolean { + try { + "".split("").reduce((left, right) => left + right); + } catch (error) { + return error.name === "TypeError" && error.message === "Reduce of empty array with no initial value"; + } + return false; + } + + reduceInitialEmpty(): number { + return "".split("").reduce((acc, value) => { throw value; }, 12); + } + + reduceThrows(): number { + try { + "a".split("").reduce((acc, value) => { throw 7; }, 0); + } catch (error) { + return error; + } + return -1; + } + + ignoredArguments(): boolean { + let calls = 0; + const joined = "a-b".split("-", 2, calls++).join("/", calls++); + const reduced = this.numbers().reduce((left, right) => left + right, 0, calls++); + return joined === "a/b" && reduced === 6 && calls === 3; + } + + unrelatedPrivateHelper(): string { + return ArrayModelPrimitives.elementString(true); + } + + joinCallable(): string { + return "a".split("").join((() => 1) as any); + } + + splitCallable(): string[] { + return "a".split((() => 1) as any); + } + + joinNumbers(): string { + return this.numbers().join(","); + } + + splitLong(): string[] { + return "abcdefghijklmnop".split(""); + } + + reduceShrink(): number { + return this.numbers().reduce((acc, value, index, array) => { + array.length = 0; + return acc + value; + }, 0); + } + + reduceDeleteThrows(): number { + return this.numbers().reduce((acc, value, index, array) => { + delete array[0]; + throw array[0]; + }, 0); + } +} From 56e432c8f93db0ddc0efddbe0e867efdd378a987 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:28:49 +0300 Subject: [PATCH 3/8] Use the JavaScript null identity in array join and reject vacuous model tests --- .../call/intrinsic/TsDenseArrayPrimitives.kt | 4 +-- .../machine/call/TsGapModelsSourceTest.kt | 36 +++++++++++++++---- .../test/resources/models/GapModelSource.ts | 7 ++++ 3 files changed, 39 insertions(+), 8 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt index 11915eca23..f2f5688f00 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt @@ -79,7 +79,7 @@ internal object TsDenseArrayPrimitives { if (value.isFakeObject()) { val kind = value.getFakeType(state.memory) val ref = value.extractRef(state.memory) - val nullish = mkOr(mkEq(ref, mkUndefinedValue()), mkEq(ref, nullRef)) + val nullish = mkOr(mkEq(ref, mkUndefinedValue()), mkEq(ref, mkTsNullValue())) val referenceGuard = if (kind.refTypeExpr.isFalse || state.hasUnsafeStringReference(ref)) { falseExpr } else { @@ -122,7 +122,7 @@ internal object TsDenseArrayPrimitives { value.sort == addressSort -> { val ref = value.asExpr(addressSort) if (state.hasUnsafeStringReference(ref)) return null - val nullish = mkOr(mkEq(ref, mkUndefinedValue()), mkEq(ref, nullRef)) + val nullish = mkOr(mkEq(ref, mkUndefinedValue()), mkEq(ref, mkTsNullValue())) val guard = mkOr(nullish, state.memory.types.evalTypeEquals(ref, EtsStringType)) execution(guard = guard) { ctx.mkIte(nullish, mkInitializedStringConstant(""), ref) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt index 9937ba27a0..c681141904 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt @@ -36,11 +36,28 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) override val tsOptions = TsOptions(maxArraySize = 16) override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> - TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> - val analysis = machine.analyzeWithOutcome(listOf(method)) + val calls = mutableListOf() + val limitations = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + calls += event + } - assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) - assertTrue(analysis.unsupportedPaths.isEmpty(), "${method.name}: ${analysis.unsupportedPaths}") + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions, observer = observer).use { machine -> + val analysis = machine.analyzeWithOutcome(listOf(method)) + val residualCalls = calls.filter { event -> event.outcome == TsUnknownCallOutcome.PATH_STOPPED } + val diagnostics = "${method.name}: stop=${analysis.stopReason}, states=${analysis.states.size}, " + + "unsupported=${analysis.unsupportedPaths}, residual=$residualCalls, limitations=$limitations" + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, diagnostics) + assertTrue(analysis.states.isNotEmpty(), diagnostics) + assertTrue(analysis.unsupportedPaths.isEmpty(), diagnostics) + assertTrue(residualCalls.isEmpty(), diagnostics) + assertTrue(limitations.isEmpty(), diagnostics) analysis.states.map { state -> TsTestResolver().resolve(method, state) } } } @@ -103,7 +120,7 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { } @Test - fun `join keeps symbolic boolean kinds and source selected lengths`() { + fun `join keeps symbolic boolean nullish kinds and source selected lengths`() { discoverProperties( method = method("symbolicBooleans"), { first, second, both, result -> @@ -116,6 +133,13 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { result.value == expected }), ) + + discoverProperties( + method = method("symbolicNullish"), + { flag, result -> flag.value && result.value == "true|" }, + { flag, result -> !flag.value && result.value == "|false" }, + invariants = arrayOf({ flag, result -> result.value == if (flag.value) "true|" else "|false" }), + ) } @Test @@ -169,7 +193,7 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { val methodNames = listOf( "splitEdges", "reduceAliases", "reduceEmptyError", "ignoredArguments", "composedMutations", "independentArrays", "joinRuntimeKinds", "reduceMutation", "reduceOmitted", "reduceUndefined", - "reduceInitialEmpty", "reduceThrows", "symbolicBooleans", + "reduceInitialEmpty", "reduceThrows", "symbolicBooleans", "symbolicNullish", ) val script = buildString { appendLine(source.readText()) diff --git a/usvm-ts/src/test/resources/models/GapModelSource.ts b/usvm-ts/src/test/resources/models/GapModelSource.ts index 1fa89f16a2..8bddbc5553 100644 --- a/usvm-ts/src/test/resources/models/GapModelSource.ts +++ b/usvm-ts/src/test/resources/models/GapModelSource.ts @@ -49,6 +49,13 @@ export class GapModelSource { return values.join("-"); } + symbolicNullish(flag: boolean): string { + const values = "a,b".split(",") as any[]; + values[0] = flag ? true : null; + values[1] = flag ? undefined : false; + return values.join("|"); + } + reduceMutation(): number { const values = this.numbers(); const multiplier = 2; From 639832fbcb1d1a488f58920fa1c7c15f4defdae3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:31:44 +0300 Subject: [PATCH 4/8] Model numeric array join with symbolic integer digits and exact concrete formatting --- usvm-ts/UNKNOWN_CALL_MODELS.md | 2 +- .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 6 +- .../call/intrinsic/TsDenseArrayPrimitives.kt | 24 +++- .../usvm/machine/call/models/ArrayModels.ts | 30 ++++- .../machine/call/TsGapModelsSourceTest.kt | 110 +++++++++++++++++- .../test/resources/models/GapModelSource.ts | 66 +++++++++++ 6 files changed, 232 insertions(+), 6 deletions(-) diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 94b5e94ae1..f3a60eb63f 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -71,7 +71,7 @@ The built-in catalog includes the following public APIs and their internal stora | `ts.array.pop` | TypeScript/EtsIR body | Zero-argument `pop` on a definitely one-dimensional array that also satisfies the symbolic runtime type guard. | | `ts.array.includes`, `ts.array.indexOf`, `ts.array.lastIndexOf` | TypeScript/EtsIR bodies | One-dimensional arrays and numeric positions, with the missing-slot exclusions below. | | `ts.array.push`, `ts.array.fill`, `ts.array.reverse`, `ts.array.unshift`, `ts.array.slice`, `ts.array.concat` | TypeScript/EtsIR bodies with storage growth/allocation primitives | One-dimensional arrays with length/result at most 16. Push/unshift accept up to three arguments; resolved-sort arrays require matching element sorts, while mixed arrays retain runtime value kinds. Concat accepts one same-type array. Except push and full-range `fill(value)`, these operations require a current dense-array proof. | -| `ts.array.join` | TypeScript/EtsIR body with a primitive element conversion | Dense arrays of at most 16 strings, booleans or nullish values, including runtime overrides in typed storage. Separator must be a string or omitted/undefined; numeric and object element coercion uses fallback. | +| `ts.array.join` | TypeScript/EtsIR body with a primitive element conversion | Dense arrays of at most 16 strings, booleans, numbers or nullish values, including runtime overrides in typed storage. Symbolic numbers support safe integers, signed zero, NaN and infinities; concrete numbers reuse exact ECMAScript decimal formatting. Symbolic fractions/unsafe integers and object coercion use fallback. Separator must be a string or omitted/undefined. | | `ts.array.reduce` | TypeScript/EtsIR body | Dense arrays of at most 16 elements and a known source callback. Preserves initial-value omission, accumulator/receiver aliases, captured variables, in-range writes and callback exceptions. Structural mutation uses fallback. | | `ts.string.charAt`, `ts.string.charCodeAt`, `ts.string.includes`, `ts.string.indexOf`, `ts.string.lastIndexOf`, `ts.string.startsWith`, `ts.string.endsWith` | TypeScript/EtsIR bodies | Strings in initialized UTF-16 storage, including symbolic code units and numeric positions. | | `ts.string.slice`, `ts.string.substring`, `ts.string.trim`, `ts.string.trimStart`, `ts.string.trimEnd` | TypeScript/EtsIR bodies | UTF-16 range copying; substring clamps/swaps bounds, and trim uses the ECMAScript whitespace set. | diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index 0a148aa6bc..c0a78a0967 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -444,7 +444,11 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { domainGuard = domainGuard, inputAdapter = inputAdapter, requiredModelIds = buildSet { - if (methodName == "join") add("ts.array.primitive.elementString") + if (methodName == "join") { + add("ts.array.primitive.elementString") + add(TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID) + add(MATH_FLOOR_MODEL_ID) + } if (methodName == "reduce") { add("ts.array.primitive.requireDense") add("ts.typeError.constructor") diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt index f2f5688f00..9d721ef342 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt @@ -1,5 +1,6 @@ package org.usvm.machine.call.intrinsic +import io.ksmt.expr.KFp64Value import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsStringType @@ -17,6 +18,7 @@ import org.usvm.machine.call.TsUnknownCallModelExecution import org.usvm.machine.call.TsUnknownCallModelSuccessor import org.usvm.machine.expr.mkFpToUint32AfterValidation import org.usvm.machine.expr.mkValidArrayLength +import org.usvm.machine.expr.toEcmaScriptString import org.usvm.machine.state.TsState import org.usvm.sizeSort import org.usvm.util.arrayStorageType @@ -86,6 +88,13 @@ internal object TsDenseArrayPrimitives { val isString = state.memory.types.evalTypeEquals(ref, EtsStringType) mkAnd(kind.refTypeExpr, mkOr(isString, nullish)) } + val concreteNumber = if (kind.fpTypeExpr.isFalse) { + null + } else { + value.extractFp(state.memory) as? KFp64Value + } + val numberText = concreteNumber?.value?.toEcmaScriptString() + val numberGuard = if (numberText != null) kind.fpTypeExpr else falseExpr val successors = buildList { if (!kind.boolTypeExpr.isFalse) { add( @@ -107,15 +116,28 @@ internal object TsDenseArrayPrimitives { ) ) } + if (numberText != null && !numberGuard.isFalse) { + add( + TsUnknownCallModelSuccessor( + guard = numberGuard, + completion = TsUnknownCallModelCompletion.Normal { + mkInitializedStringConstant(numberText) + }, + ) + ) + } } if (successors.isEmpty()) return null return TsUnknownCallModelExecution( successors = successors, - residualGuard = mkNot(mkOr(kind.boolTypeExpr, referenceGuard)), + residualGuard = mkNot(mkOr(kind.boolTypeExpr, referenceGuard, numberGuard)), ) } when { + value is KFp64Value -> execution(guard = trueExpr) { + mkInitializedStringConstant(value.value.toEcmaScriptString()) + } value.sort == boolSort -> execution(guard = trueExpr) { booleanString(value.asExpr(ctx.boolSort)) } diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts index 7df2c6545e..7d9b30a349 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts @@ -13,12 +13,40 @@ export class ArrayModels { let index = 0; while (index < length) { if (index !== 0) result += separator; - result += ArrayModelPrimitives.elementString(receiver[index]); + const value = receiver[index]; + result += typeof value === "number" + ? ArrayModels.numberString(value) + : ArrayModelPrimitives.elementString(value); index++; } return result; } + private static numberString(value: number): string { + if (value !== value) return "NaN"; + if (value === Infinity) return "Infinity"; + if (value === -Infinity) return "-Infinity"; + if (value === 0) return "0"; + + // The primitive uses exact ECMAScript formatting for concrete values. + // Symbolic fractions and unsafe integers remain residual. + if (!Number.isSafeInteger(value)) return ArrayModelPrimitives.elementString(value); + + const negative = value < 0; + let remaining = negative ? -value : value; + let result = ""; + while (remaining > 0) { + // For safe integers the quotient rounds by less than 0.1, so floor + // and the subsequent exact integer subtraction recover the digit. + const quotient = Math.floor(remaining / 10); + const digit = remaining - quotient * 10; + result = "0123456789"[digit] + result; + remaining = quotient; + } + + return negative ? "-" + result : result; + } + static reduce(receiver: any[], callback: (acc: any, current: any, index: number, array: any[]) => any, initial: any, hasInitial: boolean): any { const length = receiver.length; diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt index c681141904..ffa87bd579 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt @@ -89,6 +89,7 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { "composedMutations" to "cba", "independentArrays" to "abcd", "joinRuntimeKinds" to "--true-false", + "joinNumbers" to "1,2,3", ) for ((name, expected) in expectedValues) { @@ -142,13 +143,115 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { ) } + @Test + fun `join formats safe integer limits special values and concrete decimal boundaries`() { + val expectedValues = mapOf( + "numericJoinSafeIntegerEdges" to "-9007199254740991|-1000000001|-10|-1|0|0|10|9007199254740991", + "numericJoinSpecials" to "NaN|Infinity|-Infinity|0|0", + "numericJoinConcreteDecimals" to "0.1|1e-7|0.000001|100000000000000000000|1e+21|1000000000000000100", + ) + + for ((name, expected) in expectedValues) { + discoverProperties( + method = method(name), + { result -> result.value == expected }, + invariants = arrayOf({ result -> result.value == expected }), + ) + } + } + + @Test + fun `join preserves symbolic integer digits special values and mixed runtime kinds`() { + discoverProperties( + method = method("numericJoinSymbolicInteger"), + { value, result -> + value.number in -12.0..-10.0 && result.value == value.number.toInt().toString() + }, + { value, result -> value.number == 0.0 && result.value == "0" }, + { value, result -> value.number in 1.0..9.0 && result.value == value.number.toInt().toString() }, + { value, result -> value.number in 10.0..12.0 && result.value == value.number.toInt().toString() }, + { _, result -> result.value == "outside" }, + invariants = arrayOf({ value, result -> + val number = value.number + val smallInteger = number.isFinite() && number % 1.0 == 0.0 && number in -12.0..12.0 + val expected = if (smallInteger) number.toInt().toString() else "outside" + + result.value == expected + }), + ) + discoverProperties( + method = method("numericJoinSymbolicSpecial"), + { value, result -> value.number.isNaN() && result.value == "NaN" }, + { value, result -> value.number == Double.POSITIVE_INFINITY && result.value == "Infinity" }, + { value, result -> value.number == Double.NEGATIVE_INFINITY && result.value == "-Infinity" }, + invariants = arrayOf({ value, result -> + val expected = when { + value.number.isNaN() -> "NaN" + value.number == Double.POSITIVE_INFINITY -> "Infinity" + value.number == Double.NEGATIVE_INFINITY -> "-Infinity" + else -> "finite" + } + + result.value == expected + }), + ) + discoverProperties( + method = method("numericJoinRuntimeKind"), + { flag, result -> flag.value && result.value == "-42" }, + { flag, result -> !flag.value && result.value == "false" }, + invariants = arrayOf({ flag, result -> result.value == if (flag.value) "-42" else "false" }), + ) + } + + @Test + fun `numeric join includes its dependencies under an explicit model selection`() { + val method = method("numericJoinSafeIntegerEdges") + val selectedOptions = tsOptions.copy( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(setOf("ts.array.join", "ts.string.split")), + ) + + val analysis = TsMachine(scene = scene, options = options, tsOptions = selectedOptions) + .use { machine -> machine.analyzeWithOutcome(listOf(method)) } + val values = analysis.states.map { state -> TsTestResolver().resolve(method, state).returnValue } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertEquals( + listOf(TsTestValue.TsString(value = "-9007199254740991|-1000000001|-10|-1|0|0|10|9007199254740991")), + values, + ) + } + + @Test + fun `join leaves symbolic fractional and unsafe integer formatting residual`() { + for (name in listOf("numericJoinSymbolicFraction", "numericJoinSymbolicUnsafeInteger")) { + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + val method = method(name) + + val analysis = TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer) + .use { machine -> machine.analyzeWithOutcome(listOf(method)) } + val values = analysis.states.map { state -> TsTestResolver().resolve(method, state).returnValue } + val numericResidual = events.any { event -> + event.callee.name == "elementString" && event.outcome == TsUnknownCallOutcome.PATH_STOPPED + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name) + assertTrue(values.isNotEmpty(), name) + assertTrue(values.all { value -> value == TsTestValue.TsString(value = "outside") }, "$name: $values") + assertTrue(numericResidual, "$name: $events") + } + } + @Test fun `unrelated helpers and unsupported coercions remain residual`() { val residualCallees = mapOf( "unrelatedPrivateHelper" to "elementString", "joinCallable" to "join", "splitCallable" to "split", - "joinNumbers" to "elementString", "splitLong" to "split", "reduceShrink" to "requireDense", ) @@ -192,8 +295,11 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { fun `generated model witnesses replay in JavaScript`() { val methodNames = listOf( "splitEdges", "reduceAliases", "reduceEmptyError", "ignoredArguments", "composedMutations", - "independentArrays", "joinRuntimeKinds", "reduceMutation", "reduceOmitted", "reduceUndefined", + "independentArrays", "joinRuntimeKinds", "joinNumbers", "reduceMutation", "reduceOmitted", + "reduceUndefined", "reduceInitialEmpty", "reduceThrows", "symbolicBooleans", "symbolicNullish", + "numericJoinSafeIntegerEdges", "numericJoinSpecials", "numericJoinConcreteDecimals", + "numericJoinSymbolicInteger", "numericJoinSymbolicSpecial", "numericJoinRuntimeKind", ) val script = buildString { appendLine(source.readText()) diff --git a/usvm-ts/src/test/resources/models/GapModelSource.ts b/usvm-ts/src/test/resources/models/GapModelSource.ts index 8bddbc5553..03a01572dd 100644 --- a/usvm-ts/src/test/resources/models/GapModelSource.ts +++ b/usvm-ts/src/test/resources/models/GapModelSource.ts @@ -130,6 +130,72 @@ export class GapModelSource { return this.numbers().join(","); } + private joinNumberValue(value: number): string { + const values = "a".split("") as unknown as number[]; + values[0] = value; + return values.join(); + } + + numericJoinSafeIntegerEdges(): string { + const values = "a,b,c,d,e,f,g,h".split(",") as unknown as number[]; + values[0] = -9007199254740991; + values[1] = -1000000001; + values[2] = -10; + values[3] = -1; + values[4] = -0; + values[5] = 0; + values[6] = 10; + values[7] = 9007199254740991; + return values.join("|"); + } + + numericJoinSpecials(): string { + const values = "a,b,c,d,e".split(",") as unknown as number[]; + values[0] = NaN; + values[1] = Infinity; + values[2] = -Infinity; + values[3] = -0; + values[4] = 0; + return values.join("|"); + } + + numericJoinConcreteDecimals(): string { + const values = "a,b,c,d,e,f".split(",") as unknown as number[]; + values[0] = 0.1; + values[1] = 1e-7; + values[2] = 1e-6; + values[3] = 1e20; + values[4] = 1e21; + values[5] = 1000000000000000100; + return values.join("|"); + } + + numericJoinSymbolicInteger(value: number): string { + if (!Number.isInteger(value) || value < -12 || value > 12) return "outside"; + return this.joinNumberValue(value); + } + + numericJoinSymbolicSpecial(value: number): string { + if (Number.isFinite(value)) return "finite"; + return this.joinNumberValue(value); + } + + numericJoinRuntimeKind(flag: boolean): string { + const values = "a".split("") as any[]; + values[0] = flag ? -42 : false; + return values.join(); + } + + numericJoinSymbolicFraction(value: number): string { + if (value > 0 && value < 1) return this.joinNumberValue(value); + return "outside"; + } + + numericJoinSymbolicUnsafeInteger(value: number): string { + if (value > 9007199254740991 && value <= 1e16) return this.joinNumberValue(value); + return "outside"; + } + splitLong(): string[] { return "abcdefghijklmnop".split(""); } From ca3760cdfb3895bfe9c69617fc5814535dd8d339 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:50:03 +0300 Subject: [PATCH 5/8] Resolve lint findings in source model primitives --- .../call/intrinsic/TsDenseArrayPrimitives.kt | 42 +++++++++---------- .../call/intrinsic/TsErrorEtsIrModelFamily.kt | 3 +- .../call/intrinsic/TsNumberParseFloatModel.kt | 7 ++-- .../intrinsic/TsStringEtsIrModelFamily.kt | 5 ++- 4 files changed, 28 insertions(+), 29 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt index 9d721ef342..a6162a6ecd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayPrimitives.kt @@ -97,41 +97,39 @@ internal object TsDenseArrayPrimitives { val numberGuard = if (numberText != null) kind.fpTypeExpr else falseExpr val successors = buildList { if (!kind.boolTypeExpr.isFalse) { - add( - TsUnknownCallModelSuccessor( - guard = kind.boolTypeExpr, - completion = TsUnknownCallModelCompletion.Normal { - booleanString(value.extractBool(memory)) - }, - ) + val successor = TsUnknownCallModelSuccessor( + guard = kind.boolTypeExpr, + completion = TsUnknownCallModelCompletion.Normal { + booleanString(value.extractBool(memory)) + }, ) + add(successor) } if (!referenceGuard.isFalse) { - add( - TsUnknownCallModelSuccessor( - guard = referenceGuard, - completion = TsUnknownCallModelCompletion.Normal { - ctx.mkIte(nullish, mkInitializedStringConstant(""), ref) - }, - ) + val successor = TsUnknownCallModelSuccessor( + guard = referenceGuard, + completion = TsUnknownCallModelCompletion.Normal { + ctx.mkIte(nullish, mkInitializedStringConstant(""), ref) + }, ) + add(successor) } if (numberText != null && !numberGuard.isFalse) { - add( - TsUnknownCallModelSuccessor( - guard = numberGuard, - completion = TsUnknownCallModelCompletion.Normal { - mkInitializedStringConstant(numberText) - }, - ) + val successor = TsUnknownCallModelSuccessor( + guard = numberGuard, + completion = TsUnknownCallModelCompletion.Normal { + mkInitializedStringConstant(numberText) + }, ) + add(successor) } } if (successors.isEmpty()) return null + val supportedGuard = mkOr(kind.boolTypeExpr, referenceGuard, numberGuard) return TsUnknownCallModelExecution( successors = successors, - residualGuard = mkNot(mkOr(kind.boolTypeExpr, referenceGuard, numberGuard)), + residualGuard = mkNot(supportedGuard), ) } when { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt index 3c7b8e923f..cd4d4acb7a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt @@ -61,7 +61,8 @@ internal object TsErrorEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) val entryPoint = artifact.file.allClasses.single { it.name == "ErrorModels" } - .methods.single { it.name == methodName } + .methods + .single { it.name == methodName } return TsEtsIrUnknownCallModel( id = modelId, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumberParseFloatModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumberParseFloatModel.kt index b6a7d3186a..10282213cf 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumberParseFloatModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumberParseFloatModel.kt @@ -53,10 +53,9 @@ internal object TsNumberParseFloatModel : TsBuiltInUnknownCallModelFamily { val characters = state.memory.read(mkStringBackingLValue(input)) val length = state.memory.read(mkStringBackingLengthLValue(characters)) val isString = state.memory.types.evalTypeEquals(input, EtsStringType) - val isBounded = mkAnd( - mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), - mkBvSignedLessOrEqualExpr(length, mkBv(MAX_INPUT_LENGTH)), - ) + val hasNonNegativeLength = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val isWithinLengthLimit = mkBvSignedLessOrEqualExpr(length, mkBv(MAX_INPUT_LENGTH)) + val isBounded = mkAnd(hasNonNegativeLength, isWithinLengthLimit) mkAnd(isString, isBounded) } }, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index ec9a33424a..501a84638f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -32,7 +32,8 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private const val PRIMITIVES_CLASS_NAME = "StringModelPrimitives" private const val RESOURCE_NAME = "/org/usvm/machine/call/models/StringModels.ts" private const val REPLACE_ALL_INPUT_COUNT = 3 - private const val DEFAULT_SPLIT_LIMIT = 4294967295.0 + private const val DEFAULT_SPLIT_LIMIT = 4_294_967_295.0 + private const val SPLIT_OMITTED_SEPARATOR_INPUT_INDEX = 3 private val baseArtifact by lazy { loadBundledEtsIrUnknownCallModelArtifact( @@ -200,7 +201,7 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { val length = state.memory.read(mkStringBackingLengthLValue(characters)) val boundedResult = mkBvSignedLessOrEqualExpr(length, mkBv(SOURCE_ARRAY_MODEL_CAPACITY - 1)) val zeroLimit = mkFpEqualExpr(inputs[2].asExpr(fp64Sort), mkFp64(0.0)) - val omittedSeparator = inputs[3].asExpr(boolSort) + val omittedSeparator = inputs[SPLIT_OMITTED_SEPARATOR_INPUT_INDEX].asExpr(boolSort) mkAnd(stringsGuard, mkOr(boundedResult, zeroLimit, omittedSeparator)) } } From 4d3bfbbe61f36b546a7ad1fccce03bbe5d7eda48 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:04:21 +0300 Subject: [PATCH 6/8] Wrap parseFloat regression machine arguments --- .../org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt index e9176f45cc..a5be24d7f2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsNumberParseFloatEtsIrTest.kt @@ -71,7 +71,12 @@ class TsNumberParseFloatEtsIrTest : TsMethodTestRunner() { } val method = getMethod(methodName = "unsupportedMantissa", className = "NumberParseFloatEtsIr") - val states = TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> + val states = TsMachine( + scene = scene, + options = options, + tsOptions = tsOptions, + observer = observer, + ).use { machine -> machine.analyze(methods = listOf(method)) } From 9ae2c3d5cf23dd28543b9e6a7fec70be7a4b12f4 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 23:27:15 +0300 Subject: [PATCH 7/8] Preserve explicit deletion limitations after rebasing gap models --- .../src/main/kotlin/org/usvm/machine/expr/DeleteArray.kt | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeleteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeleteArray.kt index 816810f2ae..afc46c12f9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeleteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeleteArray.kt @@ -3,6 +3,7 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.deleteKnownArrayIndex @@ -23,7 +24,12 @@ internal fun TsExprResolver.tryDeleteArrayIndex(value: EtsArrayAccess): TsExprAp val knownOwnSlots = scope.calcOnState { array in knownArrayPropertyPresence } if (!knownOwnSlots) { - throw UnsupportedOperationException("Array index deletion requires known own-slot provenance") + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_ELEMENT_DELETE, + detail = "Array index deletion requires known own-slot provenance", + ) + scope.assert(falseExpr) + return TsExprApproximationResult.ResolveFailure } val resolvedIndex = resolve(value.index) ?: return TsExprApproximationResult.ResolveFailure From 41a59af265661bba8a5b93f3dee2b9e15a1706e3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 00:03:20 +0300 Subject: [PATCH 8/8] Opt source gap model tests into TypeScript assertion erasure --- .../test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt index ffa87bd579..3310f542df 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsGapModelsSourceTest.kt @@ -34,7 +34,7 @@ class TsGapModelsSourceTest : TsMethodTestRunner() { private val source = getResourcePath("/models/GapModelSource.ts") override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) - override val tsOptions = TsOptions(maxArraySize = 16) + override val tsOptions = TsOptions(maxArraySize = 16, eraseTypeAssertions = true) override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> val calls = mutableListOf() val limitations = mutableListOf()