From 33a6df107728374629985acf75a91f9427e5087a Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 01:22:25 +0300 Subject: [PATCH 01/23] Report Calls runtime limits and reject only unsupported raw IR --- .../org/usvm/ts/calls/CallsExperiment.kt | 13 +- .../usvm/ts/calls/CallsIrReadinessIssue.kt | 149 ++++++++++++++ .../ts/calls/CallsUnknownCallTelemetry.kt | 56 +++++- .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 56 +++++- .../calls/CallsReadinessAndTelemetryTest.kt | 190 ++++++++++++++++++ ...CurrentTsCallsSymbolicEngineTestSupport.kt | 3 + 6 files changed, 444 insertions(+), 23 deletions(-) create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt index b3e34a5537..994ee9e322 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt @@ -6,6 +6,7 @@ import kotlinx.serialization.decodeFromString import kotlinx.serialization.encodeToString import kotlinx.serialization.json.Json import org.usvm.PathSelectionStrategy +import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.call.TsResidualCallPolicy import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.ts.pbt.model.JsConcreteValue @@ -116,6 +117,7 @@ internal enum class CallsSymbolicStatus { UNREACHED, UNREPRESENTABLE, UNSUPPORTED, + RUNTIME_LIMITATION, TIMEOUT, UNKNOWN, TOOL_ERROR, @@ -134,6 +136,7 @@ internal data class CallsSymbolicSearchRequest( val seed: Long, val budget: Duration, val unknownCallEventSink: ((TsUnknownCallEvent) -> Unit)? = null, + val runtimeLimitationEventSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)? = null, ) internal data class CallsSymbolicSearchResult( @@ -406,7 +409,7 @@ internal class CallsExperimentRunner( target: CallsSourceTarget, seed: Long, profile: CallsExperimentProfile, - appendUnknownCall: (CallsUnknownCallRecord) -> Unit, + appendUnknownCall: (CallsRawRecord) -> Unit, ): CallsTargetResult { val request = CallsSymbolicSearchRequest( sourceRoot = sourceRoot, @@ -424,9 +427,14 @@ internal class CallsExperimentRunner( cell = request.cellIdentity(experimentId = manifest.experimentId), appendAndFlush = appendUnknownCall, ) + val runtimeLimitationSink = callsRuntimeLimitationEventSink( + cell = request.cellIdentity(experimentId = manifest.experimentId), + appendAndFlush = appendUnknownCall, + ) val symbolic = symbolicEngine.search( request.copy( unknownCallEventSink = eventWrites.track(unknownCallSink), + runtimeLimitationEventSink = eventWrites.track(runtimeLimitationSink), ), ) eventWrites.requireComplete() @@ -600,7 +608,8 @@ internal object CallsExperimentAggregator { replayConfirmed = rows.count { result -> result.replayStatus == CallsReplayStatus.CONFIRMED }, replayRejected = rows.count { result -> result.replayStatus == CallsReplayStatus.REJECTED }, unsupported = rows.count { result -> - result.symbolicStatus == CallsSymbolicStatus.UNSUPPORTED + result.symbolicStatus == CallsSymbolicStatus.UNSUPPORTED || + result.symbolicStatus == CallsSymbolicStatus.RUNTIME_LIMITATION }, timeouts = rows.count { result -> result.symbolicStatus == CallsSymbolicStatus.TIMEOUT || diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt new file mode 100644 index 0000000000..5c51a1f3ff --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt @@ -0,0 +1,149 @@ +package org.usvm.ts.calls + +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsRawEntity +import org.jacodb.ets.model.EtsRawStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.utils.getOperands +import org.usvm.machine.TsGraph + +internal data class CallsIrReadinessIssue( + val reasonCode: CallsSymbolicPreflightReasonCode, + val diagnostic: String, +) + +internal fun callsIrReadinessIssue( + method: EtsMethod, + graph: TsGraph, + source: String, +): CallsIrReadinessIssue? { + val sourceFile = method.signature.enclosingClass.file + val pending = ArrayDeque().apply { addLast(method) } + val visited = hashSetOf() + + while (pending.isNotEmpty()) { + val currentMethod = pending.removeFirst() + if (!visited.add(currentMethod)) continue + + currentMethod.irReadinessIssue( + source = source, + )?.let { issue -> return issue } + + currentMethod.sameFileCallees(graph = graph, sourceFile = sourceFile) + .forEach(pending::addLast) + } + + return null +} + +private fun EtsMethod.sameFileCallees( + graph: TsGraph, + sourceFile: EtsFileSignature, +): Sequence = cfg.stmts.asSequence() + .flatMap { statement -> + val directCallees = runCatching { graph.callees(statement).toList() }.getOrDefault(emptyList()) + val pointerCallees = statement.walkEntities().filterIsInstance().flatMap { call -> + val signature = (call.ptr.type as? EtsFunctionType)?.signature ?: return@flatMap emptyList() + graph.cp.projectClasses.filter { owner -> owner.signature == signature.enclosingClass } + .flatMap { owner -> owner.methods } + .filter { callee -> callee.signature == signature } + } + (directCallees + pointerCallees).asSequence() + } + .filter { callee -> callee.signature.enclosingClass.file == sourceFile } + +private fun EtsMethod.irReadinessIssue( + source: String, +): CallsIrReadinessIssue? { + val statements = cfg.stmts + val entitiesByStatement = statements.associateWith { statement -> statement.walkEntities() } + val rawNodes = buildList { + entitiesByStatement.forEach { (statement, statementEntities) -> + val sourceSnippet = statement.sourceSnippet(source) + if (statement is EtsRawStmt) { + add(RawNode(kind = statement.kind, extra = statement.extra, sourceSnippet = sourceSnippet)) + } + statementEntities.filterIsInstance().forEach { entity -> + add(RawNode(kind = entity.kind, extra = entity.extra, sourceSnippet = sourceSnippet)) + } + } + } + rawNodes.firstOrNull(RawNode::isDestructuring)?.let { raw -> + return raw.issue(CallsSymbolicPreflightReasonCode.DESTRUCTURING_UNSUPPORTED, name) + } + rawNodes.firstOrNull(RawNode::isSpread)?.let { raw -> + return raw.issue(CallsSymbolicPreflightReasonCode.SPREAD_UNSUPPORTED, name) + } + rawNodes.firstOrNull(RawNode::isRegexLiteral)?.let { raw -> + return raw.issue(CallsSymbolicPreflightReasonCode.REGEX_LITERAL_UNSUPPORTED, name) + } + rawNodes.firstOrNull()?.let { raw -> + return raw.issue(CallsSymbolicPreflightReasonCode.RAW_ENTITY_UNSUPPORTED, name) + } + + return null +} + +private fun EtsStmt.sourceSnippet(source: String): String { + val origin = location.origin ?: return "" + if (origin.startOffset !in 0..source.length || origin.endOffset !in origin.startOffset..source.length) return "" + + return source.substring(origin.startOffset, origin.endOffset) +} + +private fun EtsStmt.walkEntities(): List { + val result = mutableListOf() + val pending = ArrayDeque() + getOperands().forEach(pending::addLast) + while (pending.isNotEmpty()) { + val entity = pending.removeFirst() + result += entity + entity.getOperands().forEach(pending::addLast) + } + + return result +} + +private data class RawNode( + val kind: String, + val extra: Map, + val sourceSnippet: String, +) { + private val normalizedDescription: String = sequenceOf(kind) + .plus(extra.entries.sortedBy { (key, _) -> key }.flatMap { (key, value) -> sequenceOf(key, value.toString()) }) + .plus(sourceSnippet) + .joinToString(separator = " ") + .lowercase() + + fun matches(vararg markers: String): Boolean = markers.any(normalizedDescription::contains) + + fun isDestructuring(): Boolean = matches("destruct", "bindingpattern", "binding pattern") || + DESTRUCTURING_DECLARATION.containsMatchIn(sourceSnippet) || + DESTRUCTURING_ASSIGNMENT.containsMatchIn(sourceSnippet) + + fun isSpread(): Boolean = matches("spread") || sourceSnippet.contains("...") + + fun isRegexLiteral(): Boolean = matches("regex", "regexp", "regular expression") || + REGEX_LITERAL.containsMatchIn(sourceSnippet) + + fun issue(reasonCode: CallsSymbolicPreflightReasonCode, methodName: String): CallsIrReadinessIssue = issue( + reasonCode = reasonCode, + diagnostic = "Reachable EtsIR contains unsupported raw node kind $kind in $methodName", + ) +} + +private val DESTRUCTURING_DECLARATION = Regex("""\b(?:const|let|var)\s*[\[{]""") +private val DESTRUCTURING_ASSIGNMENT = Regex("""(?:^|[;{}])\s*[\[{][^=]*[\]}]\s*=""") +private val REGEX_LITERAL = Regex("""/(?:\\.|[^/\r\n])+/[a-z]*""") + +private fun issue( + reasonCode: CallsSymbolicPreflightReasonCode, + diagnostic: String, +): CallsIrReadinessIssue = CallsIrReadinessIssue( + reasonCode = reasonCode, + diagnostic = diagnostic, +) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetry.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetry.kt index e110d0a2b9..9af0ae2733 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetry.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetry.kt @@ -4,6 +4,8 @@ import kotlinx.serialization.SerialName import kotlinx.serialization.Serializable import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsNamespaceSignature +import org.jacodb.ets.model.EtsStmt +import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.call.TsResidualCallPolicy import org.usvm.machine.call.TsUnknownCallDecision import org.usvm.machine.call.TsUnknownCallEvent @@ -72,6 +74,34 @@ internal data class CallsUnknownCallRecord( } } +@Serializable +@SerialName("runtime-limitation") +internal data class CallsRuntimeLimitationRecord( + val cell: CallsExperimentCellIdentity, + val eventIndex: Int, + val callSite: CallsUnknownCallSite, + val reason: String, + val detail: String, +) : CallsRawRecord + +internal fun callsRuntimeLimitationEventSink( + cell: CallsExperimentCellIdentity, + appendAndFlush: (CallsRuntimeLimitationRecord) -> Unit, +): (TsRuntimeFeatureLimitationEvent) -> Unit { + var eventIndex = 0 + return { event -> + eventIndex++ + val record = CallsRuntimeLimitationRecord( + cell = cell, + eventIndex = eventIndex, + callSite = event.statement.toCallsUnknownCallSite(), + reason = event.reason.name, + detail = event.detail, + ) + appendAndFlush(record) + } +} + internal fun CallsSymbolicSearchRequest.cellIdentity(experimentId: String): CallsExperimentCellIdentity = CallsExperimentCellIdentity( experimentId = experimentId, @@ -90,21 +120,12 @@ internal fun CallsExperimentCellIdentity.unknownCallRecord( event: TsUnknownCallEvent, eventIndex: Int, ): CallsUnknownCallRecord { - val containingMethod = event.callSite.location.method.signature - val origin = event.callSite.location.origin val decision = event.decision return CallsUnknownCallRecord( cell = this, eventIndex = eventIndex, - callSite = CallsUnknownCallSite( - sourcePath = containingMethod.enclosingClass.file.fileName, - statementIndex = event.callSite.location.index, - startOffset = origin?.startOffset, - endOffset = origin?.endOffset, - start = origin?.let { span -> CallsSourcePosition(line = span.startLine, column = span.startColumn) }, - end = origin?.let { span -> CallsSourcePosition(line = span.endLine, column = span.endColumn) }, - ), + callSite = event.callSite.toCallsUnknownCallSite(), callee = event.callee.toCallsUnknownCallCallee(), failureReason = event.failureReason.name, decision = when (decision) { @@ -117,6 +138,21 @@ internal fun CallsExperimentCellIdentity.unknownCallRecord( ) } +private fun EtsStmt.toCallsUnknownCallSite(): CallsUnknownCallSite { + val stmtLocation = location + val origin = stmtLocation.origin + val containingMethod = stmtLocation.method.signature + + return CallsUnknownCallSite( + sourcePath = containingMethod.enclosingClass.file.fileName, + statementIndex = stmtLocation.index, + startOffset = origin?.startOffset, + endOffset = origin?.endOffset, + start = origin?.let { CallsSourcePosition(line = it.startLine, column = it.startColumn) }, + end = origin?.let { CallsSourcePosition(line = it.endLine, column = it.endColumn) }, + ) +} + internal fun callsUnknownCallEventSink( cell: CallsExperimentCellIdentity, appendAndFlush: (CallsUnknownCallRecord) -> Unit, diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index d14219f3f6..539f3e0a49 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -12,9 +12,11 @@ import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsGraph import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.call.TsUnknownCallModelSelection import org.usvm.machine.interpreter.TsInitialStateSolverUnknownException @@ -58,6 +60,10 @@ internal enum class CallsSymbolicPreflightReasonCode { ENTRY_MAPPING_UNMAPPED, ENTRY_MAPPING_AMBIGUOUS, LEXICAL_CAPTURE_UNSUPPORTED, + DESTRUCTURING_UNSUPPORTED, + SPREAD_UNSUPPORTED, + REGEX_LITERAL_UNSUPPORTED, + RAW_ENTITY_UNSUPPORTED, TARGET_ORIGIN_UNMAPPED, TARGET_ORIGIN_UNSUPPORTED, FRONTEND_OR_PREFLIGHT_ERROR, @@ -80,7 +86,7 @@ internal class CurrentTsCallsSymbolicEngine( private val bundledNativeFrontendRevision: String = CallsBuildIdentity.nativeFrontendRevision, ) : CallsSymbolicEngine { private val verifiedProjects = mutableMapOf() - private val preparedTargets = mutableMapOf() + private var preparedTarget: Pair? = null private var verifiedNativeFrontendIdentity: String? = null override fun search(request: CallsSymbolicSearchRequest): CallsSymbolicSearchResult { @@ -165,7 +171,10 @@ internal class CurrentTsCallsSymbolicEngine( lexicalEnvironment = prepared.lexicalEnvironment, captures = prepared.captures, ) - val interpreterObserver = request.unknownCallEventSink?.let(::UnknownCallEventSinkObserver) + val interpreterObserver = UnknownCallEventSinkObserver( + sink = request.unknownCallEventSink, + runtimeLimitationSink = request.runtimeLimitationEventSink, + ) val analysis = TsMachine( scene = scene, options = machineOptions, @@ -187,10 +196,10 @@ internal class CurrentTsCallsSymbolicEngine( if (states.isEmpty()) { val status = when (analysis.stopReason) { TsAnalysisStopReason.EXHAUSTED -> { - if (analysis.unsupportedPaths.isEmpty()) { - CallsSymbolicStatus.UNREACHED - } else { - CallsSymbolicStatus.UNSUPPORTED + when { + interpreterObserver.runtimeLimitations.isNotEmpty() -> CallsSymbolicStatus.RUNTIME_LIMITATION + analysis.unsupportedPaths.isNotEmpty() -> CallsSymbolicStatus.UNSUPPORTED + else -> CallsSymbolicStatus.UNREACHED } } // The machine options above disable every stop condition except the per-target timeout. @@ -202,7 +211,12 @@ internal class CurrentTsCallsSymbolicEngine( return result( status = status, startedAt = startedAt, - diagnostic = analysis.unsupportedPaths.joinToString().ifEmpty { null }, + diagnostic = buildList { + addAll(analysis.unsupportedPaths) + if (interpreterObserver.runtimeLimitations.isNotEmpty()) { + add(interpreterObserver.runtimeLimitations.joinToString(prefix = "Runtime feature limitations: ")) + } + }.joinToString().ifEmpty { null }, ) } @@ -231,7 +245,8 @@ internal class CurrentTsCallsSymbolicEngine( } private fun prepareSafely(request: CallsSymbolicPreflightRequest): CallsTargetPreparation { - preparedTargets[request]?.let { preparation -> return preparation } + val cached = preparedTarget + if (cached?.first == request) return cached.second val preparation = runCatching { prepare(request) }.getOrElse { error -> CallsTargetPreparation.Rejected( @@ -240,7 +255,9 @@ internal class CurrentTsCallsSymbolicEngine( diagnostic = error.message ?: error::class.java.name, ) } - preparedTargets[request] = preparation + if (preparation !is CallsTargetPreparation.Rejected || preparation.status != CallsSymbolicStatus.TOOL_ERROR) { + preparedTarget = request to preparation + } return preparation } @@ -345,6 +362,15 @@ internal class CurrentTsCallsSymbolicEngine( ) } + val readinessIssue = callsIrReadinessIssue(method = method, graph = TsGraph(scene), source = sourceText) + if (readinessIssue != null) { + return CallsTargetPreparation.Rejected( + status = CallsSymbolicStatus.UNSUPPORTED, + reasonCode = readinessIssue.reasonCode, + diagnostic = readinessIssue.diagnostic, + ) + } + val exactTargetCandidates = exactTargetCandidates(method, request.target) val targetObservation = when (request.target.mode) { CallsSourceTargetMode.ENTRY -> { @@ -612,10 +638,18 @@ internal class CurrentTsCallsSymbolicEngine( } private class UnknownCallEventSinkObserver( - private val sink: (TsUnknownCallEvent) -> Unit, + private val sink: ((TsUnknownCallEvent) -> Unit)?, + private val runtimeLimitationSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)?, ) : TsInterpreterObserver { + val runtimeLimitations = linkedSetOf() + override fun onUnknownCall(event: TsUnknownCallEvent) { - sink(event) + sink?.invoke(event) + } + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + runtimeLimitations += event.reason.name + runtimeLimitationSink?.invoke(event) } } diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt new file mode 100644 index 0000000000..0c2ecfb4d2 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt @@ -0,0 +1,190 @@ +package org.usvm.ts.calls + +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.StringDomain +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +internal class CallsReadinessAndTelemetryTest : CurrentTsCallsSymbolicEngineTestSupport() { + @Test + fun `runtime limitation is reported instead of an unreached target`() { + val fixture = fixture( + source = """ + export function writesNamedProperty(value: number): boolean { + const values = [1]; + values[0.5] = value; + return true; + } + """.trimIndent(), + exportName = "writesNamedProperty", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "return true;", + ) + val limitations = mutableListOf() + + val result = fixture.search( + modelIds = emptySet(), + runtimeLimitationEventSink = limitations::add, + ) + + assertEquals(CallsSymbolicStatus.RUNTIME_LIMITATION, result.status, result.toString()) + assertEquals(TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, limitations.single().reason) + assertTrue(result.diagnostic.orEmpty().contains("ARRAY_NAMED_PROPERTY_WRITE")) + } + + @Test + fun `completed return rejects a partial ordinary return expression`() { + val fixture = fixture( + source = "export function increment(value: number): number { return value + 1; }", + exportName = "increment", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "1", + targetMode = CallsSourceTargetMode.COMPLETED_RETURN, + returnExpression = "1", + ) + + val preflight = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.UNSUPPORTED, preflight.status) + assertEquals(CallsSymbolicPreflightReasonCode.TARGET_ORIGIN_UNSUPPORTED, preflight.reasonCode) + } + + @Test + fun `completed return accepts a module-local arrow exported by clause`() { + val expression = "value > 0" + val fixture = fixture( + source = "const aliasedArrow = (value: number): boolean => $expression; export { aliasedArrow };", + exportName = "aliasedArrow", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = expression, + targetMode = CallsSourceTargetMode.COMPLETED_RETURN, + returnExpression = expression, + ) + + val preflight = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, preflight.status, preflight.toString()) + } + + @Test + fun `preflight rejects regex raw entities with a stable reason`() { + val fixture = fixture( + source = """ + export function containsA(value: string): boolean { + if (/a/.test(value)) { + return true; + } + return false; + } + """.trimIndent(), + exportName = "containsA", + inputs = listOf(PropertyInput(name = "value", domain = StringDomain(maxLength = 3))), + targetStatement = "return true;", + ) + + val result = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.UNSUPPORTED, result.status) + assertEquals(CallsSymbolicPreflightReasonCode.REGEX_LITERAL_UNSUPPORTED, result.reasonCode, result.toString()) + } + + @Test + fun `preflight rejects regex raw entities in a reachable same-file helper`() { + val fixture = fixture( + source = """ + function helper(): boolean { + return /x/.test("x"); + } + + export function callsHelper(value: number): boolean { + return helper() && value > 0; + } + """.trimIndent(), + exportName = "callsHelper", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "return helper() && value > 0;", + ) + + val result = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.UNSUPPORTED, result.status) + assertEquals(CallsSymbolicPreflightReasonCode.REGEX_LITERAL_UNSUPPORTED, result.reasonCode, result.toString()) + } + + @Test + fun `preflight ignores regex raw entities in an unreachable same-file helper`() { + val fixture = fixture( + source = """ + function unusedHelper(): boolean { + return /x/.test("x"); + } + + export function ignoresHelper(value: number): boolean { + if (value > 0) { + return true; + } + return false; + } + """.trimIndent(), + exportName = "ignoresHelper", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "return true;", + ) + + val result = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, result.status, result.toString()) + } + + @Test + fun `ordinary own prototype property is not rejected by a source name blacklist`() { + val fixture = fixture( + source = """ + export function ownPrototype(value: number): boolean { + const owner = { prototype: value }; + if (owner.prototype === 7) return true; + return false; + } + """.trimIndent(), + exportName = "ownPrototype", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "return true;", + ) + + val preflight = fixture.preflight() + val result = fixture.search(modelIds = emptySet()) + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, preflight.status, preflight.toString()) + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + fixture.assertReplayConfirmed(assertNotNull(result.inputs, result.toString())) + } + + @Test + fun `lowered destructuring and literal spread are not rejected by syntax alone`() { + val fixture = fixture( + source = """ + export function loweredPatterns(value: number): boolean { + const [first] = [value]; + const values = [first, ...[2, 3]]; + if (values[0] === 7) return true; + return false; + } + """.trimIndent(), + exportName = "loweredPatterns", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "return true;", + ) + + val preflight = fixture.preflight() + val result = fixture.search(modelIds = emptySet()) + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, preflight.status, preflight.toString()) + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + fixture.assertReplayConfirmed(assertNotNull(result.inputs, result.toString())) + } +} diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTestSupport.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTestSupport.kt index 07741b88d0..fad479dfeb 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTestSupport.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTestSupport.kt @@ -1,6 +1,7 @@ package org.usvm.ts.calls import org.junit.jupiter.api.io.TempDir +import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyInput @@ -108,6 +109,7 @@ internal open class CurrentTsCallsSymbolicEngineTestSupport { fun search( modelIds: Set, unknownCallEventSink: ((TsUnknownCallEvent) -> Unit)? = null, + runtimeLimitationEventSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)? = null, profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, ): CallsSymbolicSearchResult = engine.search( CallsSymbolicSearchRequest( @@ -121,6 +123,7 @@ internal open class CurrentTsCallsSymbolicEngineTestSupport { seed = 0, budget = 10.seconds, unknownCallEventSink = unknownCallEventSink, + runtimeLimitationEventSink = runtimeLimitationEventSink, ) ) From c509fdd7cb3714509773af554d8c9eff2c5c3c8c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:09:19 +0300 Subject: [PATCH 02/23] Load validated local source closures for Calls and clean generated IR --- .../usvm/ts/calls/CallsIrReadinessIssue.kt | 46 +++- .../org/usvm/ts/calls/CallsSourceProject.kt | 107 ++++++++ .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 29 ++- .../ts/calls/CallsLocalSourceClosureTest.kt | 211 +++++++++++++++ .../usvm/ts/calls/CallsSourceProjectTest.kt | 67 +++++ ...CurrentTsCallsSymbolicEngineTestSupport.kt | 22 +- .../fast-check-adapter/package.json | 2 +- .../src/local-source-closure.ts | 242 ++++++++++++++++++ .../src/source-inspector-cli.ts | 97 +++---- .../test/local-source-closure.test.ts | 156 +++++++++++ .../fastcheck/TypeScriptSourceInspector.kt | 17 ++ 11 files changed, 922 insertions(+), 74 deletions(-) create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceProject.kt create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsLocalSourceClosureTest.kt create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceProjectTest.kt create mode 100644 usvm-ts-fast-check/fast-check-adapter/src/local-source-closure.ts create mode 100644 usvm-ts-fast-check/fast-check-adapter/test/local-source-closure.test.ts diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt index 5c51a1f3ff..4223224ace 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt @@ -7,7 +7,11 @@ import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsPtrCallExpr import org.jacodb.ets.model.EtsRawEntity import org.jacodb.ets.model.EtsRawStmt +import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME import org.jacodb.ets.utils.getOperands import org.usvm.machine.TsGraph @@ -19,9 +23,8 @@ internal data class CallsIrReadinessIssue( internal fun callsIrReadinessIssue( method: EtsMethod, graph: TsGraph, - source: String, + sourceByFile: Map, ): CallsIrReadinessIssue? { - val sourceFile = method.signature.enclosingClass.file val pending = ArrayDeque().apply { addLast(method) } val visited = hashSetOf() @@ -30,19 +33,21 @@ internal fun callsIrReadinessIssue( if (!visited.add(currentMethod)) continue currentMethod.irReadinessIssue( - source = source, + source = sourceByFile.getValue(currentMethod.signature.enclosingClass.file), )?.let { issue -> return issue } - currentMethod.sameFileCallees(graph = graph, sourceFile = sourceFile) + currentMethod.projectCallees(graph = graph, sourceFiles = sourceByFile.keys) + .forEach(pending::addLast) + currentMethod.projectStaticInitializers(graph = graph, sourceFiles = sourceByFile.keys) .forEach(pending::addLast) } return null } -private fun EtsMethod.sameFileCallees( +private fun EtsMethod.projectCallees( graph: TsGraph, - sourceFile: EtsFileSignature, + sourceFiles: Set, ): Sequence = cfg.stmts.asSequence() .flatMap { statement -> val directCallees = runCatching { graph.callees(statement).toList() }.getOrDefault(emptyList()) @@ -54,7 +59,34 @@ private fun EtsMethod.sameFileCallees( } (directCallees + pointerCallees).asSequence() } - .filter { callee -> callee.signature.enclosingClass.file == sourceFile } + .filter { callee -> callee.signature.enclosingClass.file in sourceFiles } + +private fun EtsMethod.projectStaticInitializers( + graph: TsGraph, + sourceFiles: Set, +): Sequence = cfg.stmts.asSequence() + .flatMap { it.walkEntities().asSequence() } + .filterIsInstance() + .map { it.field.enclosingClass } + .filter { it.file in sourceFiles } + .distinct() + .mapNotNull { signature -> + val owner = graph.cp.projectClasses.singleOrNull { it.signature == signature } ?: return@mapNotNull null + owner.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME } + ?: owner.takeIf { it.name == DEFAULT_ARK_CLASS_NAME } + ?.methods + ?.singleOrNull { it.name == DEFAULT_ARK_METHOD_NAME } + } + +internal fun callsIrReadinessIssue( + method: EtsMethod, + graph: TsGraph, + source: String, +): CallsIrReadinessIssue? = callsIrReadinessIssue( + method = method, + graph = graph, + sourceByFile = mapOf(method.signature.enclosingClass.file to source), +) private fun EtsMethod.irReadinessIssue( source: String, diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceProject.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceProject.kt new file mode 100644 index 0000000000..e93b44b1c9 --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceProject.kt @@ -0,0 +1,107 @@ +package org.usvm.ts.calls + +import org.jacodb.ets.dto.EtsFileDto +import org.jacodb.ets.dto.toEtsFile +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.generateEtsIR +import org.jacodb.ets.utils.loadEtsProjectFromIR +import org.usvm.ts.pbt.fastcheck.TypeScriptSourceInspector +import java.nio.file.Files +import java.nio.file.Path +import kotlin.time.Duration.Companion.seconds + +internal sealed interface CallsSourceProject { + data class Loaded( + val scene: EtsScene, + val entryModule: String, + val sourceByFile: Map, + ) : CallsSourceProject + + data class Unsupported(val issue: CallsIrReadinessIssue) : CallsSourceProject +} + +internal fun loadCallsSourceProject(sourceRoot: Path, source: Path): CallsSourceProject { + val closure = TypeScriptSourceInspector.localSourceClosure(sourceRoot = sourceRoot, source = source) + if (closure.reasonCode != null) { + return CallsSourceProject.Unsupported( + issue = CallsIrReadinessIssue( + reasonCode = CallsSymbolicPreflightReasonCode.valueOf(requireNotNull(closure.reasonCode)), + diagnostic = requireNotNull(closure.diagnostic), + ), + ) + } + + val entryModule = sourceRoot.relativize(source).toString() + require(entryModule in closure.files) { "Dependency closure does not contain its entry source" } + if (closure.files.size == 1) { + val entry = loadSingleCallsSource(source) + return CallsSourceProject.Loaded( + scene = EtsScene(projectFiles = listOf(entry)), + entryModule = source.fileName.toString(), + sourceByFile = mapOf(entry.signature to Files.readString(source)), + ) + } + + val sources = closure.files.associateWith { relative -> + val path = sourceRoot.resolve(relative).normalize() + require(path.startsWith(sourceRoot) && path.toRealPath().startsWith(sourceRoot.toRealPath())) { + "Dependency source escapes its frozen root: $relative" + } + Files.readString(path) + } + val temporaryProject = Files.createTempDirectory("usvm-calls-source-closure-").toRealPath() + try { + for (relative in closure.files) { + val copy = temporaryProject.resolve(relative) + Files.createDirectories(copy.parent) + Files.copy(sourceRoot.resolve(relative), copy) + } + val generatedIr = generateEtsIR( + keepPartialOutputOnFailure = false, + projectPath = temporaryProject, + isProject = true, + loadEntrypoints = false, + timeout = 30.seconds, + provider = EtsIrProvider.TS_FRONTEND, + ) + val scene = try { + loadEtsProjectFromIR(projectFilesPath = generatedIr, sdkFilesPath = null) + } finally { + generatedIr.toFile().deleteRecursively() + } + val sourceByFile = scene.projectFiles.associate { file -> + val filePath = Path.of(file.signature.fileName) + val relative = if (filePath.isAbsolute) { + temporaryProject.relativize(filePath).toString() + } else { + filePath.toString() + } + file.signature to requireNotNull(sources[relative]) { + "Frontend source identity is outside the inspected closure: ${file.signature}" + } + } + require(sourceByFile.size == closure.files.size) { "Frontend omitted or duplicated a dependency source" } + + return CallsSourceProject.Loaded(scene = scene, entryModule = entryModule, sourceByFile = sourceByFile) + } finally { + temporaryProject.toFile().deleteRecursively() + } +} + +private fun loadSingleCallsSource(source: Path): EtsFile { + val generatedIr = generateEtsIR( + keepPartialOutputOnFailure = false, + projectPath = source, + useArkAnalyzerTypeInference = 1, + provider = EtsIrProvider.TS_FRONTEND, + ) + + return try { + Files.newInputStream(generatedIr).use { stream -> EtsFileDto.loadFromJson(stream).toEtsFile() } + } finally { + Files.deleteIfExists(generatedIr) + } +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index 539f3e0a49..74e121ad2d 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -6,8 +6,6 @@ import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt -import org.jacodb.ets.utils.EtsIrProvider -import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions @@ -56,6 +54,7 @@ internal enum class CallsSymbolicPreflightStatus { internal enum class CallsSymbolicPreflightReasonCode { INPUT_DOMAIN_UNSUPPORTED, IMPORTED_CALLEES_UNSUPPORTED, + TOP_LEVEL_INITIALIZATION_UNSUPPORTED, ENTRY_MAPPING_UNSUPPORTED, ENTRY_MAPPING_UNMAPPED, ENTRY_MAPPING_AMBIGUOUS, @@ -246,7 +245,8 @@ internal class CurrentTsCallsSymbolicEngine( private fun prepareSafely(request: CallsSymbolicPreflightRequest): CallsTargetPreparation { val cached = preparedTarget - if (cached?.first == request) return cached.second + val cachedRevisionMatches = verifiedProjects[request.sourceRoot] == request.project.revision + if (cached?.first == request && cachedRevisionMatches) return cached.second val preparation = runCatching { prepare(request) }.getOrElse { error -> CallsTargetPreparation.Rejected( @@ -290,19 +290,16 @@ internal class CurrentTsCallsSymbolicEngine( ) } - val sourceFile = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) - if (sourceFile.importInfos.isNotEmpty()) { - return CallsTargetPreparation.Rejected( + val loaded = when (val project = loadCallsSourceProject(sourceRoot = request.sourceRoot, source = source)) { + is CallsSourceProject.Loaded -> project + is CallsSourceProject.Unsupported -> return CallsTargetPreparation.Rejected( status = CallsSymbolicStatus.UNSUPPORTED, - reasonCode = CallsSymbolicPreflightReasonCode.IMPORTED_CALLEES_UNSUPPORTED, - diagnostic = "Single-file symbolic replay does not support imported project callees", + reasonCode = project.issue.reasonCode, + diagnostic = project.issue.diagnostic, ) } - - val scene = EtsScene(projectFiles = listOf(sourceFile)) - val frontendEntryPoint = request.function.entryPoint.copy( - module = requireNotNull(source.fileName).toString(), - ) + val scene = loaded.scene + val frontendEntryPoint = request.function.entryPoint.copy(module = loaded.entryModule) val propertyManifest = PropertyManifest( propertyId = "calls.mapping", inputs = request.function.inputs, @@ -362,7 +359,11 @@ internal class CurrentTsCallsSymbolicEngine( ) } - val readinessIssue = callsIrReadinessIssue(method = method, graph = TsGraph(scene), source = sourceText) + val readinessIssue = callsIrReadinessIssue( + method = method, + graph = TsGraph(scene), + sourceByFile = loaded.sourceByFile, + ) if (readinessIssue != null) { return CallsTargetPreparation.Rejected( status = CallsSymbolicStatus.UNSUPPORTED, diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsLocalSourceClosureTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsLocalSourceClosureTest.kt new file mode 100644 index 0000000000..7d8482e484 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsLocalSourceClosureTest.kt @@ -0,0 +1,211 @@ +package org.usvm.ts.calls + +import org.usvm.machine.call.TsUnknownCallDecision +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.StringDomain +import java.nio.file.Files +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +internal class CallsLocalSourceClosureTest : CurrentTsCallsSymbolicEngineTestSupport() { + @Test + fun `source closure is reloaded after checkout revision changes`() { + val fixture = importedFixture( + exportName = "revisionSensitive", + dependency = "export function helper(value: string): boolean { return true; }", + ) + val first = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, first.status, first.toString()) + + Files.writeString( + fixture.sourceRoot.resolve("helper.ts"), + "export function replacement(value: string): boolean { return true; }", + ) + runGit(fixture.sourceRoot, "add", "helper.ts") + runGit(fixture.sourceRoot, "commit", "-m", "replace helper") + val nextRevision = runGit(fixture.sourceRoot, "rev-parse", "HEAD").trim() + + val second = fixture.preflight(project = fixture.project.copy(revision = nextRevision)) + + assertEquals( + CallsSymbolicPreflightReasonCode.IMPORTED_CALLEES_UNSUPPORTED, + second.reasonCode, + second.toString(), + ) + } + + @Test + fun `loads local dependency closure and replays a nested source target`() { + val fixture = fixture( + source = """ + import { magnitude } from '../helpers'; + export function positiveMagnitude(value: number): boolean { + if (magnitude(value) === 42) return true; + return false; + } + """.trimIndent(), + exportName = "positiveMagnitude", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "return true;", + targetMode = CallsSourceTargetMode.COMPLETED_RETURN, + returnExpression = "true", + sourceFileName = "entry/Fixture.ts", + dependencies = mapOf( + "helpers/index.ts" to """ + import { absolute } from './Fixture.js'; + export function magnitude(value: number): number { return absolute(value); } + """.trimIndent(), + "helpers/Fixture.ts" to "export function absolute(value: number): number { return Math.abs(value); }", + "unrelated.ts" to "throw new Error('This module must not be loaded');", + ), + ) + val events = mutableListOf() + + val preflight = fixture.preflight() + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, preflight.status, preflight.toString()) + val result = fixture.search(modelIds = setOf("ts.math.abs"), unknownCallEventSink = events::add) + + val inputs = assertNotNull(result.inputs, "$result; events=$events") + assertEquals(42.0, kotlin.math.abs(assertIs(inputs.single()).toDouble())) + assertTrue(events.any { (it.decision as? TsUnknownCallDecision.ModelApplied)?.modelId == "ts.math.abs" }) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `preflight checks regex in a reachable imported helper using its own source`() { + val fixture = importedFixture( + exportName = "importedRegex", + dependency = "export function helper(value: string): boolean { return /a/.test(value); }", + ) + + val result = fixture.preflight() + + assertEquals(CallsSymbolicPreflightReasonCode.REGEX_LITERAL_UNSUPPORTED, result.reasonCode, result.toString()) + } + + @Test + fun `preflight does not inspect an unreachable imported helper body`() { + val fixture = importedFixture( + exportName = "unreachableRegex", + dependency = """ + export function helper(value: string): boolean { return value.length > 0; } + export function unused(value: string): boolean { return /a/.test(value); } + """.trimIndent(), + ) + + val result = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, result.status, result.toString()) + } + + @Test + fun `preflight rejects transitive external imports`() { + val fixture = importedFixture( + exportName = "externalImport", + dependency = """ + import { existsSync } from 'node:fs'; + export function helper(value: string): boolean { return existsSync(value); } + """.trimIndent(), + ) + + val result = fixture.preflight() + + assertEquals( + CallsSymbolicPreflightReasonCode.IMPORTED_CALLEES_UNSUPPORTED, + result.reasonCode, + result.toString(), + ) + assertTrue(result.diagnostic.orEmpty().contains("node:fs")) + } + + @Test + fun `preflight rejects dependency module initialization effects`() { + val fixture = importedFixture( + exportName = "moduleEffects", + dependency = """ + let threshold = 0; + threshold = 1; + export function helper(value: string): boolean { return value.length > threshold; } + """.trimIndent(), + ) + + val result = fixture.preflight() + + assertEquals( + CallsSymbolicPreflightReasonCode.TOP_LEVEL_INITIALIZATION_UNSUPPORTED, + result.reasonCode, + result.toString(), + ) + } + + @Test + fun `preflight rejects missing imports and does not treat them as unknown calls`() { + val fixture = importedFixture( + exportName = "missingImport", + dependency = """ + import { absent } from './missing'; + export function helper(value: string): boolean { return absent(value); } + """.trimIndent(), + ) + + val result = fixture.preflight() + + assertEquals( + CallsSymbolicPreflightReasonCode.IMPORTED_CALLEES_UNSUPPORTED, + result.reasonCode, + result.toString(), + ) + assertTrue(result.diagnostic.orEmpty().contains("./missing")) + } + + @Test + fun `preflight ignores explicitly type-only external imports`() { + val fixture = importedFixture( + exportName = "typeOnlyImport", + dependency = """ + import type { ExternalType } from 'missing-type-package'; + export function helper(value: string): boolean { return value.length > 0; } + """.trimIndent(), + ) + + val result = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, result.status, result.toString()) + } + + @Test + fun `preflight checks a regex initializer in an imported module`() { + val fixture = importedFixture( + exportName = "importedInitializer", + dependency = """ + const pattern = /a/; + export function helper(value: string): boolean { return pattern.test(value); } + """.trimIndent(), + ) + + val result = fixture.preflight() + + assertEquals(CallsSymbolicPreflightReasonCode.REGEX_LITERAL_UNSUPPORTED, result.reasonCode, result.toString()) + } + + private fun importedFixture(exportName: String, dependency: String): SymbolicFixture = fixture( + source = """ + import { helper } from './helper'; + export function $exportName(value: string): boolean { return helper(value); } + """.trimIndent(), + exportName = exportName, + inputs = listOf(PropertyInput(name = "value", domain = StringDomain(maxLength = 3))), + targetStatement = "return helper(value);", + targetMode = CallsSourceTargetMode.COMPLETED_RETURN, + returnExpression = "helper(value)", + dependencies = mapOf("helper.ts" to dependency), + ) + +} diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceProjectTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceProjectTest.kt new file mode 100644 index 0000000000..4aa94ff589 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceProjectTest.kt @@ -0,0 +1,67 @@ +package org.usvm.ts.calls + +import org.junit.jupiter.api.Test +import java.nio.file.Files +import java.nio.file.Path +import kotlin.io.path.createDirectories +import kotlin.io.path.createTempDirectory +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.assertFails +import kotlin.test.assertFalse + +class CallsSourceProjectTest { + @Test + fun `single and multi file conversion failures remove partial IR`() { + checkCleanup(frontendExitCode = 1) + } + + @Test + fun `single and multi file IR decoding failures remove generated output`() { + checkCleanup(frontendExitCode = 0) + } + + private fun checkCleanup(frontendExitCode: Int) { + val root = createTempDirectory(prefix = "calls-frontend-cleanup-") + val frontend = root.resolve("frontend") + val script = frontend.resolve("dist/index.js") + val recordedPath = script.resolveSibling("generated-path") + val sourceRoot = root.resolve("sources").createDirectories() + val source = sourceRoot.resolve("entry.ts") + val previousFrontend = System.getProperty("ets.frontend.dir") + script.parent.createDirectories() + script.writeText( + """ + const fs = require('node:fs'); + const path = require('node:path'); + const output = process.argv.filter(arg => arg !== '-v').at(-1); + fs.writeFileSync(path.join(__dirname, 'generated-path'), output); + const file = fs.statSync(output).isDirectory() ? path.join(output, 'partial.json') : output; + fs.writeFileSync(file, '{'); + process.exit($frontendExitCode); + """.trimIndent(), + ) + System.setProperty("ets.frontend.dir", frontend.toString()) + + try { + source.writeText("export function entry(value: number): number { return value; }") + assertFails { loadCallsSourceProject(sourceRoot = sourceRoot, source = source) } + assertFalse(Files.exists(Path.of(recordedPath.readText()))) + + sourceRoot.resolve("helper.ts").writeText("export function helper(value: number): number { return value; }") + source.writeText( + "import { helper } from './helper'; " + + "export function entry(value: number): number { return helper(value); }", + ) + assertFails { loadCallsSourceProject(sourceRoot = sourceRoot, source = source) } + assertFalse(Files.exists(Path.of(recordedPath.readText()))) + } finally { + if (previousFrontend == null) { + System.clearProperty("ets.frontend.dir") + } else { + System.setProperty("ets.frontend.dir", previousFrontend) + } + root.toFile().deleteRecursively() + } + } +} diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTestSupport.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTestSupport.kt index fad479dfeb..9e030f9db8 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTestSupport.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTestSupport.kt @@ -22,14 +22,22 @@ internal open class CurrentTsCallsSymbolicEngineTestSupport { targetStatement: String, targetMode: CallsSourceTargetMode = CallsSourceTargetMode.ENTRY, returnExpression: String? = null, + sourceFileName: String = "Fixture.ts", + dependencies: Map = emptyMap(), ): SymbolicFixture { val sourceRoot = Files.createDirectory(directory.resolve(exportName)) - val sourceFile = sourceRoot.resolve("Fixture.ts") + val sourceFile = sourceRoot.resolve(sourceFileName) + Files.createDirectories(sourceFile.parent) Files.writeString(sourceFile, source) + dependencies.forEach { (relative, content) -> + val dependency = sourceRoot.resolve(relative) + Files.createDirectories(dependency.parent) + Files.writeString(dependency, content) + } runGit(sourceRoot, "init") runGit(sourceRoot, "config", "user.name", "USVM Tests") runGit(sourceRoot, "config", "user.email", "usvm@example.test") - runGit(sourceRoot, "add", "Fixture.ts") + runGit(sourceRoot, "add", ".") runGit(sourceRoot, "commit", "-m", "fixture") val revision = runGit(sourceRoot, "rev-parse", "HEAD").trim() val targetStart = source.indexOf(targetStatement) @@ -44,7 +52,7 @@ internal open class CurrentTsCallsSymbolicEngineTestSupport { val target = CallsSourceTarget( targetId = "$exportName#$targetStatement", siteId = "$exportName:$targetStart:$targetEnd", - sourcePath = "Fixture.ts", + sourcePath = sourceFileName, startOffset = targetStart, endOffset = targetEnd, start = sourcePositionAt(source = source, offset = targetStart), @@ -55,8 +63,8 @@ internal open class CurrentTsCallsSymbolicEngineTestSupport { ) val function = CallsFunctionCase( functionId = exportName, - sourceFile = "Fixture.ts", - entryPoint = TypeScriptEntryPoint(module = "Fixture.ts", exportName = exportName), + sourceFile = sourceFileName, + entryPoint = TypeScriptEntryPoint(module = sourceFileName, exportName = exportName), inputs = inputs, targets = listOf(target), ) @@ -76,7 +84,7 @@ internal open class CurrentTsCallsSymbolicEngineTestSupport { ) } - private fun runGit(directory: Path, vararg arguments: String): String { + protected fun runGit(directory: Path, vararg arguments: String): String { val process = ProcessBuilder(listOf("git", "-C", directory.toString()) + arguments) .redirectErrorStream(true) .start() @@ -96,7 +104,7 @@ internal open class CurrentTsCallsSymbolicEngineTestSupport { bundledNativeFrontendRevision = "bundled:test", ) - fun preflight(): CallsSymbolicPreflightResult = engine.preflight( + fun preflight(project: CallsProjectCase = this.project): CallsSymbolicPreflightResult = engine.preflight( CallsSymbolicPreflightRequest( sourceRoot = sourceRoot, project = project, diff --git a/usvm-ts-fast-check/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json index 0d0aa6d3dd..4e41b2c075 100644 --- a/usvm-ts-fast-check/fast-check-adapter/package.json +++ b/usvm-ts-fast-check/fast-check-adapter/package.json @@ -9,7 +9,7 @@ "build": "tsc --project tsconfig.json", "pretest": "npm run build", "test": "npm run test:compiled", - "test:compiled": "node --test dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js" + "test:compiled": "node --test dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js" }, "dependencies": { "c8": "10.1.3", diff --git a/usvm-ts-fast-check/fast-check-adapter/src/local-source-closure.ts b/usvm-ts-fast-check/fast-check-adapter/src/local-source-closure.ts new file mode 100644 index 0000000000..def09fdc91 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/local-source-closure.ts @@ -0,0 +1,242 @@ +import { existsSync, readFileSync, realpathSync, statSync } from 'node:fs' +import path from 'node:path' +import ts from 'typescript' + +interface LocalSourceClosure { + files: string[] + reasonCode?: string + diagnostic?: string +} + +/** Inspect source only. Never execute a project or consult a profile/model result. */ +export function inspectLocalSourceClosure(rootPath: string, entryPath: string): LocalSourceClosure { + const root = realpathSync(rootPath) + const entry = path.resolve(root, path.relative(path.resolve(rootPath), path.resolve(entryPath))) + const pending = [entry] + let entryInitializationIssue: { reasonCode: string, diagnostic: string } | undefined + const files = new Set() + const runtimeImportRanges = new Map>() + const sources = new Map() + const dependencies = new Map() + + const reject = (reasonCode: string, diagnostic: string): LocalSourceClosure => ({ + files: [...files].sort(), reasonCode, diagnostic, + }) + + while (pending.length > 0) { + const file = pending.shift()! + const relative = path.relative(root, file) + if (relative.startsWith(`..${path.sep}`) || relative === '..' || path.isAbsolute(relative) + || realpathSync(file) !== file) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', `Source escapes the project or uses a symlink: ${file}`) + } + if (files.has(relative)) continue + files.add(relative) + + const source = ts.createSourceFile(file, readFileSync(file, 'utf8'), ts.ScriptTarget.Latest, true) + sources.set(file, source) + const edges: string[] = [] + dependencies.set(file, edges) + const imports: string[] = [] + const ranges: Array<{ start: number, end: number }> = [] + runtimeImportRanges.set(file, ranges) + for (const statement of source.statements) { + if (ts.isImportDeclaration(statement)) { + const clause = statement.importClause + if (clause?.isTypeOnly) continue + if (clause && !clause.name && clause.namedBindings && ts.isNamedImports(clause.namedBindings) + && clause.namedBindings.elements.length > 0 + && clause.namedBindings.elements.every(element => element.isTypeOnly)) continue + if (!ts.isStringLiteral(statement.moduleSpecifier)) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', `Nonliteral module specifier in ${relative}`) + } + imports.push(statement.moduleSpecifier.text) + ranges.push({ start: statement.getStart(source), end: statement.end }) + } else if (ts.isExportDeclaration(statement)) { + if (statement.isTypeOnly) continue + if (statement.exportClause && ts.isNamedExports(statement.exportClause) + && statement.exportClause.elements.length > 0 + && statement.exportClause.elements.every(element => element.isTypeOnly)) continue + ranges.push({ start: statement.getStart(source), end: statement.end }) + if (statement.moduleSpecifier) { + if (!ts.isStringLiteral(statement.moduleSpecifier)) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', `Nonliteral re-export in ${relative}`) + } + imports.push(statement.moduleSpecifier.text) + } + } else if (ts.isImportEqualsDeclaration(statement)) { + if (!statement.isTypeOnly) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', `Import assignment in ${relative}`) + } + } else { + const reasonCode = isAmbientRuntimeDeclaration(statement) + ? 'IMPORTED_CALLEES_UNSUPPORTED' + : !safeModuleStatement(statement, source) ? 'TOP_LEVEL_INITIALIZATION_UNSUPPORTED' : undefined + if (reasonCode !== undefined) { + const diagnostic = reasonCode === 'IMPORTED_CALLEES_UNSUPPORTED' + ? `Ambient runtime declaration in ${relative} at offset ${statement.getStart(source)}` + : `Unsupported module initialization in ${relative} at offset ${statement.getStart(source)}` + if (file !== entry) return reject(reasonCode, diagnostic) + entryInitializationIssue ??= { reasonCode, diagnostic } + } + } + } + + let dynamicImport = false + const visit = (node: ts.Node): void => { + if (ts.isCallExpression(node) && (node.expression.kind === ts.SyntaxKind.ImportKeyword + || ts.isIdentifier(node.expression) && node.expression.text === 'require')) dynamicImport = true + ts.forEachChild(node, visit) + } + visit(source) + if (dynamicImport) return reject('IMPORTED_CALLEES_UNSUPPORTED', `Dynamic import or require in ${relative}`) + + for (const specifier of imports) { + if (!specifier.startsWith('./') && !specifier.startsWith('../')) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', `External or aliased module ${specifier} in ${relative}`) + } + const target = path.resolve(path.dirname(file), specifier) + if (existsSync(path.join(target, 'package.json'))) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', `Directory package resolution is unsupported: ${specifier} in ${relative}`) + } + if (target.endsWith('.js') && existsSync(target)) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', `JavaScript runtime source is unsupported: ${specifier} in ${relative}`) + } + const candidates = (target.endsWith('.js') + ? [target.slice(0, -3) + '.ts'] + : [target, `${target}.ts`, path.join(target, 'index.ts')]) + .filter(candidate => candidate.endsWith('.ts') && !candidate.endsWith('.d.ts')) + .filter(candidate => existsSync(candidate) && statSync(candidate).isFile()) + if (candidates.length !== 1) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', + `Expected one local TypeScript module for ${specifier} in ${relative}, found ${candidates.length}`) + } + pending.push(candidates[0]!) + edges.push(candidates[0]!) + } + } + + // A single source keeps the existing capture/readiness validation, including supported + // block captures and immutable object aliases. Loading additional modules needs the + // stricter initialization contract because their bindings are not reconstructed there. + if (files.size > 1 && entryInitializationIssue !== undefined) { + return reject(entryInitializationIssue.reasonCode, entryInitializationIssue.diagnostic) + } + + // Replay overlays link dependency files to the original checkout. A back-import + // would then create a second entry-module instance with different mutable state. + if (hasDependencyCycle(dependencies)) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', 'Cyclic local module dependencies are unsupported by source replay') + } + + // Ask TypeScript to validate the imported bindings as well as the files. Diagnostics + // in unrelated function bodies do not determine closure admission. + if ([...runtimeImportRanges.values()].some(ranges => ranges.length > 0)) { + const options: ts.CompilerOptions = { + target: ts.ScriptTarget.ES2022, module: ts.ModuleKind.ESNext, + moduleResolution: ts.ModuleResolutionKind.Node10, noLib: true, noEmit: true, + allowImportingTsExtensions: true, types: [], + } + const host = ts.createCompilerHost(options) + const directories = new Set() + for (const file of sources.keys()) { + let directory = path.dirname(file) + while (directory.startsWith(root)) { + directories.add(directory) + if (directory === root) break + directory = path.dirname(directory) + } + } + host.fileExists = file => sources.has(path.resolve(file)) + host.readFile = file => sources.get(path.resolve(file))?.text + host.getSourceFile = file => sources.get(path.resolve(file)) + host.directoryExists = directory => directories.has(path.resolve(directory)) + host.getDirectories = () => [] + host.realpath = file => path.resolve(file) + const program = ts.createProgram([...sources.keys()], options, host) + for (const [file, ranges] of runtimeImportRanges) { + if (ranges.length === 0) continue + const source = program.getSourceFile(file)! + const invalidImport = program.getSemanticDiagnostics(source).find(diagnostic => + diagnostic.category === ts.DiagnosticCategory.Error && diagnostic.start !== undefined + && ranges.some(range => diagnostic.start! >= range.start && diagnostic.start! < range.end)) + if (invalidImport) { + return reject('IMPORTED_CALLEES_UNSUPPORTED', + `${path.relative(root, file)}: ${ts.flattenDiagnosticMessageText(invalidImport.messageText, '\n')}`) + } + } + } + + return { files: [...files].sort() } +} + +function hasDependencyCycle(dependencies: Map): boolean { + const active = new Set() + const visited = new Set() + const visit = (file: string): boolean => { + if (active.has(file)) return true + if (visited.has(file)) return false + active.add(file) + for (const dependency of dependencies.get(file) ?? []) { + if (visit(dependency)) return true + } + active.delete(file) + visited.add(file) + return false + } + return [...dependencies.keys()].some(visit) +} + +function isAmbientRuntimeDeclaration(statement: ts.Statement): boolean { + if (!ts.isVariableStatement(statement) && !ts.isFunctionDeclaration(statement) + && !ts.isClassDeclaration(statement) && !ts.isEnumDeclaration(statement)) return false + return statement.modifiers?.some(modifier => modifier.kind === ts.SyntaxKind.DeclareKeyword) ?? false +} + +function safeModuleStatement(statement: ts.Statement, source: ts.SourceFile): boolean { + if (ts.isFunctionDeclaration(statement) || ts.isInterfaceDeclaration(statement) + || ts.isTypeAliasDeclaration(statement) || ts.isEmptyStatement(statement)) return true + if (ts.isExpressionStatement(statement) && ts.isStringLiteral(statement.expression)) return true + if (ts.isVariableStatement(statement)) { + return statement.declarationList.declarations.every(declaration => ts.isIdentifier(declaration.name) + && (!declaration.initializer || safeInitializer(declaration.initializer, source))) + } + if (ts.isExportAssignment(statement)) return !statement.isExportEquals && safeInitializer(statement.expression, source) + if (ts.isClassDeclaration(statement)) { + if (statement.heritageClauses?.length || ts.getDecorators(statement)?.length) return false + return statement.members.every(member => !ts.isClassStaticBlockDeclaration(member) + && !(member.name && ts.isComputedPropertyName(member.name)) + && !(ts.canHaveDecorators(member) && ts.getDecorators(member)?.length) + && !(ts.isPropertyDeclaration(member) && member.initializer + && member.modifiers?.some(modifier => modifier.kind === ts.SyntaxKind.StaticKeyword))) + } + if (ts.isEnumDeclaration(statement)) { + return statement.members.every(member => !member.initializer || ts.isLiteralExpression(member.initializer)) + } + return false +} + +function safeInitializer(expression: ts.Expression, source: ts.SourceFile, seen = new Set()): boolean { + if (seen.has(expression)) return false + seen.add(expression) + if (ts.isParenthesizedExpression(expression) || ts.isAsExpression(expression) + || ts.isTypeAssertionExpression(expression) || ts.isSatisfiesExpression(expression) + || ts.isNonNullExpression(expression)) return safeInitializer(expression.expression, source, seen) + if (ts.isLiteralExpression(expression) || ts.isArrowFunction(expression) || ts.isFunctionExpression(expression) + || expression.kind === ts.SyntaxKind.TrueKeyword || expression.kind === ts.SyntaxKind.FalseKeyword + || expression.kind === ts.SyntaxKind.NullKeyword) return true + if (ts.isPrefixUnaryExpression(expression) + && [ts.SyntaxKind.PlusToken, ts.SyntaxKind.MinusToken, ts.SyntaxKind.ExclamationToken, ts.SyntaxKind.TildeToken] + .includes(expression.operator)) return safeInitializer(expression.operand, source, seen) + if (!ts.isIdentifier(expression)) return false + for (const statement of source.statements) { + if (ts.isFunctionDeclaration(statement) && statement.name?.text === expression.text) return Boolean(statement.body) + if (!ts.isVariableStatement(statement)) continue + for (const declaration of statement.declarationList.declarations) { + if (ts.isIdentifier(declaration.name) && declaration.name.text === expression.text && declaration.initializer + && declaration.getStart(source) < expression.getStart(source) + && (ts.isArrowFunction(declaration.initializer) || ts.isFunctionExpression(declaration.initializer))) return true + } + } + return false +} diff --git a/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts b/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts index c1aa2a4cd3..bf4b033df1 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts @@ -1,54 +1,61 @@ -import { readFileSync } from 'node:fs' +import { readFileSync, writeFileSync } from 'node:fs' import ts from 'typescript' import { instrumentSourceReplay } from './source-replay.js' import { inspectSourceCaptures } from './source-captures.js' +import { inspectLocalSourceClosure } from './local-source-closure.js' const [operation, sourcePath, ...arguments_] = process.argv.slice(2) if (sourcePath === undefined) throw new Error('Expected a TypeScript source path') -const source = readFileSync(sourcePath, 'utf8') -const sourceFile = ts.createSourceFile(sourcePath, source, ts.ScriptTarget.Latest, true, ts.ScriptKind.TS) -const diagnostics = ts.transpileModule(source, { - compilerOptions: { target: ts.ScriptTarget.Latest }, - fileName: sourcePath, - reportDiagnostics: true, -}).diagnostics?.filter((diagnostic) => diagnostic.category === ts.DiagnosticCategory.Error) ?? [] -if (diagnostics.length > 0) throw new Error(ts.flattenDiagnosticMessageText(diagnostics[0]?.messageText ?? '', '\n')) +if (operation === 'inspect-local-closure') { + const entryPath = arguments_[0] + if (entryPath === undefined) throw new Error('Expected an entry source path') + writeFileSync(1, JSON.stringify(inspectLocalSourceClosure(sourcePath, entryPath))) +} else { + const source = readFileSync(sourcePath, 'utf8') + const sourceFile = ts.createSourceFile(sourcePath, source, ts.ScriptTarget.Latest, true, ts.ScriptKind.TS) + const diagnostics = ts.transpileModule(source, { + compilerOptions: { target: ts.ScriptTarget.Latest }, + fileName: sourcePath, + reportDiagnostics: true, + }).diagnostics?.filter((diagnostic) => diagnostic.category === ts.DiagnosticCategory.Error) ?? [] + if (diagnostics.length > 0) throw new Error(ts.flattenDiagnosticMessageText(diagnostics[0]?.messageText ?? '', '\n')) -if (operation === 'inspect-captures') { - const [exportName, namesText] = arguments_ - if (exportName === undefined || namesText === undefined) throw new Error('Expected export and capture names') - const names: unknown = JSON.parse(namesText) - if (!Array.isArray(names) || !names.every((name) => typeof name === 'string')) throw new Error('Invalid capture names') - process.stdout.write(JSON.stringify(inspectSourceCaptures(sourcePath, exportName, names as string[]))) -} else if (operation === 'expression-arrow') { - const [exportName, startText, endText] = arguments_ - const start = Number(startText) - const end = Number(endText) - const matches = sourceFile.statements.filter(ts.isVariableStatement).flatMap((statement) => { - const exported = statement.modifiers?.some((modifier) => modifier.kind === ts.SyntaxKind.ExportKeyword) - if (!exported) return [] - return statement.declarationList.declarations.filter((declaration) => - ts.isIdentifier(declaration.name) && declaration.name.text === exportName - && declaration.initializer !== undefined && ts.isArrowFunction(declaration.initializer) - && !ts.isBlock(declaration.initializer.body) - && declaration.initializer.body.getStart(sourceFile) === start && declaration.initializer.body.getEnd() === end, - ) - }) - process.stdout.write(matches.length === 1 ? 'true' : 'false') -} else if (operation === 'instrument-replay') { - const [mode, startText, endText, expressionStartText, expressionEndText, marker] = arguments_ - if ((mode !== 'ENTRY' && mode !== 'COMPLETED_RETURN') || marker === undefined) { - throw new Error('Expected replay mode, offsets and marker') + if (operation === 'inspect-captures') { + const [exportName, namesText] = arguments_ + if (exportName === undefined || namesText === undefined) throw new Error('Expected export and capture names') + const names: unknown = JSON.parse(namesText) + if (!Array.isArray(names) || !names.every((name) => typeof name === 'string')) throw new Error('Invalid capture names') + process.stdout.write(JSON.stringify(inspectSourceCaptures(sourcePath, exportName, names as string[]))) + } else if (operation === 'expression-arrow') { + const [exportName, startText, endText] = arguments_ + const start = Number(startText) + const end = Number(endText) + const matches = sourceFile.statements.filter(ts.isVariableStatement).flatMap((statement) => { + const exported = statement.modifiers?.some((modifier) => modifier.kind === ts.SyntaxKind.ExportKeyword) + if (!exported) return [] + return statement.declarationList.declarations.filter((declaration) => + ts.isIdentifier(declaration.name) && declaration.name.text === exportName + && declaration.initializer !== undefined && ts.isArrowFunction(declaration.initializer) + && !ts.isBlock(declaration.initializer.body) + && declaration.initializer.body.getStart(sourceFile) === start && declaration.initializer.body.getEnd() === end, + ) + }) + process.stdout.write(matches.length === 1 ? 'true' : 'false') + } else if (operation === 'instrument-replay') { + const [mode, startText, endText, expressionStartText, expressionEndText, marker] = arguments_ + if ((mode !== 'ENTRY' && mode !== 'COMPLETED_RETURN') || marker === undefined) { + throw new Error('Expected replay mode, offsets and marker') + } + const result = instrumentSourceReplay(sourceFile, { + mode, + start: Number(startText), + end: Number(endText), + expressionStart: expressionStartText === '-' ? null : Number(expressionStartText), + expressionEnd: expressionEndText === '-' ? null : Number(expressionEndText), + marker, + }) + process.stdout.write(JSON.stringify(result)) + } else { + throw new Error(`Unknown source inspection operation: ${operation}`) } - const result = instrumentSourceReplay(sourceFile, { - mode, - start: Number(startText), - end: Number(endText), - expressionStart: expressionStartText === '-' ? null : Number(expressionStartText), - expressionEnd: expressionEndText === '-' ? null : Number(expressionEndText), - marker, - }) - process.stdout.write(JSON.stringify(result)) -} else { - throw new Error(`Unknown source inspection operation: ${operation}`) } diff --git a/usvm-ts-fast-check/fast-check-adapter/test/local-source-closure.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/local-source-closure.test.ts new file mode 100644 index 0000000000..0a3ba69507 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/test/local-source-closure.test.ts @@ -0,0 +1,156 @@ +import assert from 'node:assert/strict' +import { mkdtempSync, mkdirSync, realpathSync, rmSync, symlinkSync, writeFileSync } from 'node:fs' +import { tmpdir } from 'node:os' +import path from 'node:path' +import test from 'node:test' +import ts from 'typescript' +import { inspectLocalSourceClosure } from '../src/local-source-closure.js' + +function workspace(files: Record, action: (root: string) => void): void { + const root = realpathSync(mkdtempSync(path.join(tmpdir(), 'usvm-closure-test-'))) + try { + for (const [relative, source] of Object.entries(files)) { + const file = path.join(root, relative) + mkdirSync(path.dirname(file), { recursive: true }) + writeFileSync(file, source) + } + action(root) + } finally { + rmSync(root, { recursive: true, force: true }) + } +} + +test('local closure follows reexports while ignoring unrelated effects and type imports', () => { + workspace({ + 'entry.ts': "import { helper } from './barrel'; export function entry() { return helper(); }", + 'barrel.ts': "export { helper } from './nested/helper.js';", + 'nested/helper.ts': "import type { Missing } from 'external'; " + + 'export function helper() { return 1; }', + 'unrelated.ts': "throw new Error('unrelated');", + }, root => { + assert.deepEqual(inspectLocalSourceClosure(root, path.join(root, 'entry.ts')), { + files: ['barrel.ts', 'entry.ts', 'nested/helper.ts'], + }) + }) +}) + +for (const [name, entry, helper, expected] of [ + ['external import', "import { x } from 'node:fs';", '', 'IMPORTED_CALLEES_UNSUPPORTED'], + ['missing module', "import { helper } from './missing';", '', 'IMPORTED_CALLEES_UNSUPPORTED'], + ['missing export', "import { missing } from './helper';", 'export const helper = 1;', 'IMPORTED_CALLEES_UNSUPPORTED'], + ['side effect dependency', "import './helper';", 'console.log(1);', 'TOP_LEVEL_INITIALIZATION_UNSUPPORTED'], + ['top level call', "import './helper'; const value = Math.random();", '', 'TOP_LEVEL_INITIALIZATION_UNSUPPORTED'], + ['dynamic import', "export function load() { return import('./helper'); }", '', 'IMPORTED_CALLEES_UNSUPPORTED'], + ['require', "export function load() { return require('./helper'); }", '', 'IMPORTED_CALLEES_UNSUPPORTED'], +] as const) { + test(`local closure rejects ${name}`, () => { + workspace({ 'entry.ts': entry, 'helper.ts': helper }, root => { + assert.equal(inspectLocalSourceClosure(root, path.join(root, 'entry.ts')).reasonCode, expected) + }) + }) +} + +for (const [name, declaration] of [ + ['constant', 'export declare const helper: () => number;'], + ['function', 'export declare function helper(): number;'], + ['class', 'export declare class helper { value(): number; }'], +] as const) { + test(`local closure rejects ambient runtime ${name} exports`, () => { + workspace({ + 'entry.ts': "import { helper } from './helper'; export function entry() { return helper(); }", + 'helper.ts': declaration, + }, root => { + const result = inspectLocalSourceClosure(root, path.join(root, 'entry.ts')) + assert.equal(result.reasonCode, 'IMPORTED_CALLEES_UNSUPPORTED') + assert.match(result.diagnostic!, /Ambient runtime declaration/) + }) + }) +} + +test('local closure rejects ambiguous extensionless imports', () => { + workspace({ + 'entry.ts': "import './helper';", + 'helper.ts': 'export const x = 1;', + 'helper/index.ts': 'export const x = 2;', + }, root => { + assert.equal(inspectLocalSourceClosure(root, path.join(root, 'entry.ts')).reasonCode, 'IMPORTED_CALLEES_UNSUPPORTED') + }) +}) + +test('local closure accepts a symlink alias for the root but rejects dependency symlinks', () => { + workspace({ 'real/entry.ts': 'export function value() { return 1; }' }, root => { + const alias = path.join(root, 'alias') + symlinkSync(path.join(root, 'real'), alias) + assert.deepEqual(inspectLocalSourceClosure(alias, path.join(alias, 'entry.ts')), { files: ['entry.ts'] }) + + writeFileSync(path.join(root, 'entry.ts'), "import './link';") + symlinkSync(path.join(root, 'real/entry.ts'), path.join(root, 'link.ts')) + assert.equal(inspectLocalSourceClosure(root, path.join(root, 'entry.ts')).reasonCode, 'IMPORTED_CALLEES_UNSUPPORTED') + }) +}) + +test('local closure rejects a local export of an absent binding', () => { + workspace({ + 'entry.ts': "import { missing } from './barrel'; export function entry() { return missing(); }", + 'barrel.ts': 'export { missing };', + }, root => { + assert.equal(inspectLocalSourceClosure(root, path.join(root, 'entry.ts')).reasonCode, 'IMPORTED_CALLEES_UNSUPPORTED') + }) +}) + +test('local closure rejects package directory redirection before checking different source files', () => { + workspace({ + 'entry.ts': "import { helper } from './lib'; export function entry() { return helper(); }", + 'lib/index.ts': 'export const wrongExport = 1;', + 'lib/actual.ts': 'export function helper() { return 2; }', + 'lib/package.json': '{"main":"./actual.ts"}', + }, root => { + const result = inspectLocalSourceClosure(root, path.join(root, 'entry.ts')) + assert.equal(result.reasonCode, 'IMPORTED_CALLEES_UNSUPPORTED') + assert.match(result.diagnostic!, /Directory package resolution/) + }) +}) + +test('local closure rejects a cycle that would split mutable module state in replay', () => { + workspace({ + 'entry.ts': "import { readCount } from './helper'; export let count = 0; " + + 'export function entry(value: number) { count = value; return readCount() === value; }', + 'helper.ts': "import { count } from './entry'; export function readCount() { return count; }", + }, root => { + const result = inspectLocalSourceClosure(root, path.join(root, 'entry.ts')) + assert.equal(result.reasonCode, 'IMPORTED_CALLEES_UNSUPPORTED') + assert.match(result.diagnostic!, /Cyclic local module/) + }) +}) + +test('binding inspection does not read ignored type imports outside the runtime closure', () => { + workspace({ + 'project/entry.ts': "import type { Outside } from '../outside'; import { helper } from './helper'; " + + 'export function entry() { return helper(); }', + 'project/helper.ts': 'export function helper() { return 1; }', + 'outside.ts': 'export interface Outside { value: number }', + }, root => { + const originalRead = ts.sys.readFile + const reads: string[] = [] + ts.sys.readFile = file => { reads.push(path.resolve(file)); return originalRead(file) } + try { + const project = path.join(root, 'project') + assert.deepEqual(inspectLocalSourceClosure(project, path.join(project, 'entry.ts')), { + files: ['entry.ts', 'helper.ts'], + }) + assert.equal(reads.includes(path.join(root, 'outside.ts')), false) + } finally { + ts.sys.readFile = originalRead + } + }) +}) + + +test('single-source captures retain their dedicated validation route', () => { + workspace({ + 'entry.ts': 'const source = { value: 7 }; const alias = source; ' + + 'export const entry = () => source === alias;', + }, root => { + assert.deepEqual(inspectLocalSourceClosure(root, path.join(root, 'entry.ts')), { files: ['entry.ts'] }) + }) +}) diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt index d10202806c..992fa65184 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt @@ -10,6 +10,16 @@ import java.util.concurrent.TimeUnit /** Uses the native TypeScript AST when lowered source ranges need validation or replay instrumentation. */ object TypeScriptSourceInspector { + fun localSourceClosure(sourceRoot: Path, source: Path): TypeScriptLocalSourceClosure { + val output = inspect( + source = sourceRoot, + operation = "inspect-local-closure", + arguments = listOf(source.toString()), + ) + + return PropertyManifestJson.json.decodeFromString(output) + } + fun isExportedExpressionArrowBody( source: Path, exportName: String, @@ -131,3 +141,10 @@ data class TypeScriptSourceCapture( val reason: String?, val origin: String? = null, ) + +@Serializable +data class TypeScriptLocalSourceClosure( + val files: List, + val reasonCode: String? = null, + val diagnostic: String? = null, +) From 41191e3a85d2e5316f5af809dc3a265f9734851c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:20:22 +0300 Subject: [PATCH 03/23] Validate completed returns and reject unmodeled intrinsic regex allocation --- .../usvm/ts/calls/CallsIrReadinessIssue.kt | 21 +++++- .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 17 +++++ .../calls/CallsReadinessAndTelemetryTest.kt | 64 ++++++++++++++++++- .../src/source-inspector-cli.ts | 10 ++- 4 files changed, 106 insertions(+), 6 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt index 4223224ace..0cd776ddb5 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt @@ -1,9 +1,11 @@ package org.usvm.ts.calls +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsEntity import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNewExpr import org.jacodb.ets.model.EtsPtrCallExpr import org.jacodb.ets.model.EtsRawEntity import org.jacodb.ets.model.EtsRawStmt @@ -34,6 +36,7 @@ internal fun callsIrReadinessIssue( currentMethod.irReadinessIssue( source = sourceByFile.getValue(currentMethod.signature.enclosingClass.file), + graph = graph, )?.let { issue -> return issue } currentMethod.projectCallees(graph = graph, sourceFiles = sourceByFile.keys) @@ -90,9 +93,25 @@ internal fun callsIrReadinessIssue( private fun EtsMethod.irReadinessIssue( source: String, + graph: TsGraph, ): CallsIrReadinessIssue? { val statements = cfg.stmts val entitiesByStatement = statements.associateWith { statement -> statement.walkEntities() } + val intrinsicRegexAllocation = entitiesByStatement.values.asSequence().flatten() + .filterIsInstance() + .any { allocation -> + val type = allocation.type as? EtsClassType ?: return@any false + val intrinsicOwner = type.signature.file == EtsFileSignature.UNKNOWN || + graph.cp.sdkClasses.any { owner -> owner.signature == type.signature } + type.signature.name == "RegExp" && intrinsicOwner + } + if (intrinsicRegexAllocation) { + return issue( + reasonCode = CallsSymbolicPreflightReasonCode.REGEX_LITERAL_UNSUPPORTED, + diagnostic = "Reachable EtsIR allocates an intrinsic RegExp without a runtime model in $name", + ) + } + val rawNodes = buildList { entitiesByStatement.forEach { (statement, statementEntities) -> val sourceSnippet = statement.sourceSnippet(source) @@ -159,7 +178,7 @@ private data class RawNode( fun isSpread(): Boolean = matches("spread") || sourceSnippet.contains("...") - fun isRegexLiteral(): Boolean = matches("regex", "regexp", "regular expression") || + fun isRegexLiteral(): Boolean = matches("regex", "regexp", "regularexpression", "regular expression") || REGEX_LITERAL.containsMatchIn(sourceSnippet) fun issue(reasonCode: CallsSymbolicPreflightReasonCode, methodName: String): CallsIrReadinessIssue = issue( diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index 74e121ad2d..818d6e9104 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -395,6 +395,23 @@ internal class CurrentTsCallsSymbolicEngine( } CallsSourceTargetMode.COMPLETED_RETURN -> { + val sourceTarget = TypeScriptSourceInspector.instrumentReplay( + source = source, + mode = request.target.mode.name, + startOffset = request.target.startOffset, + endOffset = request.target.endOffset, + expressionStartOffset = request.target.returnExpressionStartOffset, + expressionEndOffset = request.target.returnExpressionEndOffset, + marker = "__usvm_completed_return_preflight", + ) + if (sourceTarget.reason != null) { + return CallsTargetPreparation.Rejected( + status = CallsSymbolicStatus.UNSUPPORTED, + reasonCode = CallsSymbolicPreflightReasonCode.TARGET_ORIGIN_UNSUPPORTED, + diagnostic = sourceTarget.reason, + ) + } + val returnStatement = completedReturnCandidate( method = method, target = request.target, diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt index 0c2ecfb4d2..59ecb8bde0 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt @@ -72,7 +72,41 @@ internal class CallsReadinessAndTelemetryTest : CurrentTsCallsSymbolicEngineTest } @Test - fun `preflight rejects regex raw entities with a stable reason`() { + fun `completed return rejects a partial expression inside an exact return statement`() { + val fixture = fixture( + source = "export function increment(value: number): number { return value + 1; }", + exportName = "increment", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "return value + 1;", + targetMode = CallsSourceTargetMode.COMPLETED_RETURN, + returnExpression = "1", + ) + + val preflight = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.UNSUPPORTED, preflight.status) + assertEquals(CallsSymbolicPreflightReasonCode.TARGET_ORIGIN_UNSUPPORTED, preflight.reasonCode) + } + + @Test + fun `completed return accepts a renamed module-local arrow export`() { + val expression = "value > 0" + val fixture = fixture( + source = "const local = (value: number): boolean => $expression; export { local as renamed };", + exportName = "renamed", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = expression, + targetMode = CallsSourceTargetMode.COMPLETED_RETURN, + returnExpression = expression, + ) + + val preflight = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, preflight.status, preflight.toString()) + } + + @Test + fun `preflight rejects lowered intrinsic regex allocation with a stable reason`() { val fixture = fixture( source = """ export function containsA(value: string): boolean { @@ -94,7 +128,7 @@ internal class CallsReadinessAndTelemetryTest : CurrentTsCallsSymbolicEngineTest } @Test - fun `preflight rejects regex raw entities in a reachable same-file helper`() { + fun `preflight rejects lowered regex allocation in a reachable same-file helper`() { val fixture = fixture( source = """ function helper(): boolean { @@ -117,7 +151,7 @@ internal class CallsReadinessAndTelemetryTest : CurrentTsCallsSymbolicEngineTest } @Test - fun `preflight ignores regex raw entities in an unreachable same-file helper`() { + fun `preflight ignores regex allocation in an unreachable same-file helper`() { val fixture = fixture( source = """ function unusedHelper(): boolean { @@ -141,6 +175,30 @@ internal class CallsReadinessAndTelemetryTest : CurrentTsCallsSymbolicEngineTest assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, result.status, result.toString()) } + @Test + fun `preflight does not confuse a source RegExp class with the intrinsic constructor`() { + val fixture = fixture( + source = """ + class RegExp { + test(value: string): boolean { return value === "a"; } + } + export function localRegex(value: string): boolean { + const pattern = new RegExp(); + return pattern.test(value); + } + """.trimIndent(), + exportName = "localRegex", + inputs = listOf(PropertyInput(name = "value", domain = StringDomain(maxLength = 3))), + targetStatement = "return pattern.test(value);", + targetMode = CallsSourceTargetMode.COMPLETED_RETURN, + returnExpression = "pattern.test(value)", + ) + + val preflight = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, preflight.status, preflight.toString()) + } + @Test fun `ordinary own prototype property is not rejected by a source name blacklist`() { val fixture = fixture( diff --git a/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts b/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts index bf4b033df1..5869fe5313 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts @@ -30,11 +30,17 @@ if (operation === 'inspect-local-closure') { const [exportName, startText, endText] = arguments_ const start = Number(startText) const end = Number(endText) + const localExports = sourceFile.statements.filter(ts.isExportDeclaration).flatMap((statement) => { + if (statement.moduleSpecifier !== undefined || statement.isTypeOnly + || statement.exportClause === undefined || !ts.isNamedExports(statement.exportClause)) return [] + return statement.exportClause.elements.filter((element) => !element.isTypeOnly && element.name.text === exportName) + .map((element) => (element.propertyName ?? element.name).text) + }) const matches = sourceFile.statements.filter(ts.isVariableStatement).flatMap((statement) => { const exported = statement.modifiers?.some((modifier) => modifier.kind === ts.SyntaxKind.ExportKeyword) - if (!exported) return [] return statement.declarationList.declarations.filter((declaration) => - ts.isIdentifier(declaration.name) && declaration.name.text === exportName + ts.isIdentifier(declaration.name) + && ((exported && declaration.name.text === exportName) || localExports.includes(declaration.name.text)) && declaration.initializer !== undefined && ts.isArrowFunction(declaration.initializer) && !ts.isBlock(declaration.initializer.body) && declaration.initializer.body.getStart(sourceFile) === start && declaration.initializer.body.getEnd() === end, From 7decf18afde30dd81e93c4d666330645cf349087 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:22:33 +0300 Subject: [PATCH 04/23] Support bounded dense array appends through indexed writes --- .../org/usvm/machine/expr/WriteArray.kt | 30 ++++++++- .../machine/expr/ArrayAppendSourceTest.kt | 67 +++++++++++++++++++ .../resources/models/ArrayAppendSource.ts | 41 ++++++++++++ .../models/NumericBoundarySemantics.ts | 2 +- 4 files changed, 136 insertions(+), 4 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayAppendSourceTest.kt create mode 100644 usvm-ts/src/test/resources/models/ArrayAppendSource.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index 6cdb528374..44181b60d3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -99,6 +99,7 @@ internal fun TsExprResolver.handleAssignToArrayIndex( scope.assert(indexIsSupported) ?: return null val bvIndex = mkFpToUint32AfterValidation(index.value, indexIsSupported).asExpr(sizeSort) + extendArrayForIndexAppend(array = array, index = bvIndex, arrayType = storageType) ?: return null return assignToArrayIndex( scope = scope, @@ -115,6 +116,30 @@ internal fun TsExprResolver.handleAssignToArrayIndex( ) } +private fun TsExprResolver.extendArrayForIndexAppend( + array: UHeapRef, + index: UExpr, + arrayType: EtsArrayType, +): Unit? = with(ctx) { + val lengthLValue = mkArrayLengthLValue(array, arrayType) + val length = scope.calcOnState { memory.read(lengthLValue) } + val isAppend = mkEq(index, length) + val belowCapacity = mkBvSignedLessExpr(length, mkBv(options.maxArraySize)) + val appendExceedsCapacity = mkAnd(isAppend, mkNot(belowCapacity)) + if (scope.checkSat(appendExceedsCapacity) != null) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, + detail = "array index append exceeds configured length bound ${options.maxArraySize}", + ) + } + scope.assert(mkNot(appendExceedsCapacity)) ?: return null + + // Dense appends have no uninitialized gap. Sparse growth remains unsupported below. + scope.doWithState { + memory.write(lengthLValue, mkBvAddExpr(length, mkBv(1)), guard = isAppend) + } +} + fun TsContext.assignToArrayIndex( scope: TsStepScope, array: UHeapRef, @@ -131,9 +156,8 @@ fun TsContext.assignToArrayIndex( memory.read(lengthLValue) } - // Note: out-of-bound write is not an error in JS, since it can grow the array. - // However, we decided to forbid this behavior in our model for simplicity. - // Instead, we only allow writing to existing indices. + // Callers extend the length for supported dense appends before writing the element. + // Skipping indices would create holes, which this storage model does not represent. val indexIsNonNegative = mkBvSignedGreaterOrEqualExpr(index, mkBv(0)) val indexIsBelowLength = mkBvSignedLessExpr(index, length) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayAppendSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayAppendSourceTest.kt new file mode 100644 index 0000000000..2796513877 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayAppendSourceTest.kt @@ -0,0 +1,67 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +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.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class ArrayAppendSourceTest : TsMethodTestRunner() { + override val scene = EtsScene( + projectFiles = listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/ArrayAppendSource.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + override val tsOptions = TsOptions(maxArraySize = 3) + + @Test + fun `dense appends preserve length payload kinds and aliases`() { + listOf("appendToEmpty", "appendThroughMixedAlias", "overwriteAtCapacity", "appendAfterTruncate") + .forEach { methodName -> + discoverProperties( + method = getMethod(methodName = methodName, className = "ArrayAppendSource"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `capacity and sparse growth remain explicit limitations`() { + val boundaries = mapOf( + "appendBeyondCapacity" to TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, + "sparseGrowth" to TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, + ) + + for ((methodName, expectedReason) in boundaries) { + val method = getMethod(methodName = methodName, className = "ArrayAppendSource") + val reasons = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + reasons += event.reason + } + } + + TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), methodName) + assertEquals(listOf(expectedReason), reasons, methodName) + } + } + } +} diff --git a/usvm-ts/src/test/resources/models/ArrayAppendSource.ts b/usvm-ts/src/test/resources/models/ArrayAppendSource.ts new file mode 100644 index 0000000000..070dba9dca --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayAppendSource.ts @@ -0,0 +1,41 @@ +export class ArrayAppendSource { + static appendToEmpty(): number { + const values: number[] = []; + values[0] = 7; + values[values.length] = 11; + return values.length === 2 && values[0] === 7 && values[1] === 11 ? 1 : 0; + } + + static appendThroughMixedAlias(): number { + const values = [7]; + const alias: any[] = values; + alias[alias.length] = null; + alias[alias.length] = true; + return values.length === 3 && alias[0] === 7 && alias[1] === null && alias[2] === true ? 1 : 0; + } + + static overwriteAtCapacity(): number { + const values = [1, 2, 3]; + values[0] = 7; + return values.length === 3 && values[0] === 7 && values[2] === 3 ? 1 : 0; + } + + static appendAfterTruncate(): number { + const values = [1, 2, 3]; + values.length = 1; + values[values.length] = 7; + return values.length === 2 && values[1] === 7 && values[2] === undefined ? 1 : 0; + } + + static appendBeyondCapacity(): number { + const values = [1, 2, 3]; + values[values.length] = 7; + return values.length; + } + + static sparseGrowth(): number { + const values = [1]; + values[2] = 7; + return values.length; + } +} diff --git a/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts index a69494c314..50b9808d09 100644 --- a/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts +++ b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts @@ -135,7 +135,7 @@ export class NumericBoundarySemantics { outOfRangeArrayWrite(): number { const values = [11, 22]; - values[2] = 7; + values[3] = 7; return values[1]; } From 043dfc6be9c146d9834dbe927d3610d605709f85 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:29:14 +0300 Subject: [PATCH 05/23] Keep completed-return diagnostic in a stable local value --- .../kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index 818d6e9104..3235a2eb7e 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -404,11 +404,12 @@ internal class CurrentTsCallsSymbolicEngine( expressionEndOffset = request.target.returnExpressionEndOffset, marker = "__usvm_completed_return_preflight", ) - if (sourceTarget.reason != null) { + val sourceTargetReason = sourceTarget.reason + if (sourceTargetReason != null) { return CallsTargetPreparation.Rejected( status = CallsSymbolicStatus.UNSUPPORTED, reasonCode = CallsSymbolicPreflightReasonCode.TARGET_ORIGIN_UNSUPPORTED, - diagnostic = sourceTarget.reason, + diagnostic = sourceTargetReason, ) } From ec1bd08f6b6bd99a189bea3ee64d459157cf7fc1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:49:11 +0300 Subject: [PATCH 06/23] Model bounded native array iteration with exact symbol provenance --- .../org/usvm/machine/TsInterpreterObserver.kt | 1 + .../org/usvm/machine/expr/ArrayIterator.kt | 172 ++++++++++++++++++ .../usvm/machine/expr/CallApproximations.kt | 9 + .../kotlin/org/usvm/machine/expr/ReadArray.kt | 2 +- .../kotlin/org/usvm/machine/expr/ReadField.kt | 3 + .../machine/expr/TsCapturedInstanceCall.kt | 4 + .../org/usvm/machine/expr/TsExprResolver.kt | 2 + .../org/usvm/machine/expr/WriteArray.kt | 5 + .../kotlin/org/usvm/machine/state/TsState.kt | 11 ++ .../machine/expr/ArrayIteratorSourceTest.kt | 89 +++++++++ .../resources/models/ArrayIteratorSource.ts | 89 +++++++++ 11 files changed, 386 insertions(+), 1 deletion(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt create mode 100644 usvm-ts/src/test/resources/models/ArrayIteratorSource.ts 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 3d93cd387c..702d368b65 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -97,6 +97,7 @@ enum class TsRuntimeFeatureLimitationReason { ARRAY_NAMED_PROPERTY_READ, ARRAY_NAMED_PROPERTY_WRITE, ARRAY_INDEX_GROWTH, + ARRAY_ITERATOR_UNSUPPORTED, ARRAY_LENGTH_CAPACITY, ARRAY_LENGTH_GROWTH, } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt new file mode 100644 index 0000000000..9a93d03e8e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -0,0 +1,172 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsWellKnownSymbol +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.isTrue +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.TsSizeSort +import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.machine.types.iteWriteIntoFakeObject +import org.usvm.util.arrayStorageType +import org.usvm.util.mkArrayLengthLValue + +/** State belongs to a particular native array iterator, independently of its source binding. */ +data class TsArrayIterator( + val array: UHeapRef, + val arrayType: EtsArrayType, + val index: UExpr, + val exhausted: UBoolExpr, +) + +data class TsArrayIteratorResult(val done: UBoolExpr, val value: UExpr<*>) + +private val iteratorType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinArrayIterator")) +private val iteratorResultType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinArrayIteratorResult")) + +internal fun TsExprResolver.tryApproximateArrayIteratorCall( + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult = with(ctx) { + if (stmt.call.wellKnownSymbol == EtsWellKnownSymbol.ITERATOR) { + return TsExprApproximationResult.from(createArrayIterator(stmt)) + } + + val reference = stmt.instance as? UConcreteHeapRef ?: return TsExprApproximationResult.NoApproximation + val iterator = scope.calcOnState { arrayIterators[reference] } + ?: return TsExprApproximationResult.NoApproximation + if (stmt.call.callee.name != "next") return TsExprApproximationResult.NoApproximation + + TsExprApproximationResult.from(advanceArrayIterator(reference, iterator)) +} + +private fun TsExprResolver.createArrayIterator(stmt: TsVirtualMethodCallStmt): UHeapRef? = with(ctx) { + if (stmt.instance.sort != addressSort) { + unsupportedArrayIterator("The intrinsic iterator requires a modeled runtime array") + return null + } + + val array = stmt.instance.asExpr(addressSort) + val arrayType = scope.calcOnState { arrayStorageType(array, stmt.call.instance.type) } as? EtsArrayType + if (arrayType == null) { + unsupportedArrayIterator("Custom and non-array iterators are not modeled") + return null + } + + val runtimeArray = scope.calcOnState { memory.types.evalIsSubtype(array, arrayType) } + if (scope.checkSat(mkNot(runtimeArray)) != null) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED, + detail = "The receiver can have a custom or non-array iterator", + ) + } + scope.assert(runtimeArray) ?: return null + + scope.calcOnState { + val iterator = memory.allocConcrete(iteratorType) + arrayIterators += iterator to TsArrayIterator( + array = array, + arrayType = arrayType, + index = mkBv(0), + exhausted = falseExpr, + ) + iterator + } +} + +private fun TsExprResolver.advanceArrayIterator( + reference: UConcreteHeapRef, + iterator: TsArrayIterator, +): UHeapRef? = with(ctx) { + val invalidated = scope.calcOnState { iterator.array in unsupportedIteratorArrays } + if (invalidated) { + unsupportedArrayIterator("Array iteration after deleting an indexed property is not modeled") + return null + } + + val length = scope.calcOnState { memory.read(mkArrayLengthLValue(iterator.array, iterator.arrayType)) } + val withinCapacity = mkAnd( + mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), + mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)), + ) + if (scope.checkSat(mkAnd(mkNot(iterator.exhausted), mkNot(withinCapacity))) != null) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED, + detail = "The array iterator exceeds the configured length bound ${options.maxArraySize}", + ) + } + scope.assert(mkOr(iterator.exhausted, withinCapacity)) ?: return null + + val done = mkOr(iterator.exhausted, mkBvSignedGreaterOrEqualExpr(iterator.index, length)) + val initialized = scope.calcOnState { + // Symbolic array inputs use the engine's dense input contract. Allocations need actual slot writes. + val array = iterator.array + val denseInput = !isAllocatedConcreteHeapRef(array) || + (array is UConcreteHeapRef && denseInputArrays[array] != null) + if (denseInput) { + trueExpr + } else { + val initializedSlots = initializedArrayIndices[array].orEmpty() + mkOr(initializedSlots.map { index -> mkEq(iterator.index, index) }) + } + } + val supportedRead = mkOr(done, initialized) + if (scope.checkSat(mkNot(supportedRead)) != null) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED, + detail = "Array iteration over uninitialized slots is not modeled", + ) + } + scope.assert(supportedRead) ?: return null + + val value = if (done.isTrue) { + mkUndefinedValue() + } else { + val element = readArrayElement(scope, iterator.array, iterator.index, iterator.arrayType) + iteWriteIntoFakeObject( + scope = scope, + condition = done, + trueBranchValue = mkUndefinedValue(), + falseBranchValue = element, + ) + } + + scope.calcOnState { + arrayIterators += reference to iterator.copy( + index = mkIte(done, iterator.index, mkBvAddExpr(iterator.index, mkBv(1))), + exhausted = done, + ) + val result = memory.allocConcrete(iteratorResultType) + arrayIteratorResults += result to TsArrayIteratorResult(done = done, value = value) + result + } +} + +internal fun TsExprResolver.readArrayIteratorField(reference: UHeapRef, name: String): UExpr<*>? = with(ctx) { + if (reference !is UConcreteHeapRef) return null + + val result = scope.calcOnState { arrayIteratorResults[reference] } + if (result != null) { + return when (name) { + "done" -> result.done + "value" -> result.value + else -> mkUndefinedValue() + } + } + + val isIterator = scope.calcOnState { arrayIterators[reference] != null } + if (isIterator && name == "return") return mkUndefinedValue() + + null +} + +private fun TsExprResolver.unsupportedArrayIterator(detail: String) { + reportRuntimeFeatureLimitation(TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED, detail) + scope.assert(ctx.falseExpr) +} 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 f25e722c75..e5a76195f1 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 @@ -152,6 +152,9 @@ internal fun TsExprResolver.tryApproximateInstanceCall( val expr = stmt.call val instance = stmt.instance + val iterator = tryApproximateArrayIteratorCall(stmt) + if (iterator !is TsExprApproximationResult.NoApproximation) return iterator + // Mock `.toString()` method calls if (expr.callee.name == "toString") { if (expr.args.isNotEmpty()) { @@ -176,6 +179,12 @@ internal fun TsExprResolver.tryApproximateInstanceCall( val instanceType = scope.calcOnState { arrayStorageType(array, expr.instance.type) } if (instanceType is EtsArrayType) { + // These bulk moves do not carry initialized-slot provenance for sparse allocations. + val movesArraySlots = expr.callee.name in setOf("shift", "unshift", "reverse") + if (movesArraySlots) { + scope.doWithState { initializedArrayIndices -= array } + } + val elementSort = typeToSort(instanceType.componentType) .takeIf { it !is TsUnresolvedSort } ?: addressSort diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt index 8512ba59b4..83e15f718f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -137,7 +137,7 @@ private fun TsContext.readArrayProperty( ) } -private fun TsContext.readArrayElement( +internal fun TsContext.readArrayElement( scope: TsStepScope, array: UHeapRef, index: UExpr, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 6a1e55ccc2..29d7db9202 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -87,6 +87,9 @@ internal fun TsExprResolver.handleInstanceFieldRef( checkUndefinedOrNullPropertyRead(scope, rawInstance, propertyName = value.field.name) ?: return null val instance = resolveHeapRef(scope, rawInstance) ?: return null + val iteratorField = readArrayIteratorField(instance, value.field.name) + if (iteratorField != null) return iteratorField + // Handle reading "length" property. val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } val usesArrayLength = storageType is EtsArrayType || storageType == EtsStringType || diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt index 0c94b12f75..569377d79e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt @@ -63,6 +63,10 @@ internal fun TsExprResolver.tryCaptureInstanceCall( receiver.sort == addressSort -> receiver.asExpr(addressSort) else -> null } + val builtinReturn = field.field.name == "return" && reference is UConcreteHeapRef && + scope.calcOnState { arrayIterators[reference] != null } + if (builtinReturn) return TsExprApproximationResult.SuccessfulApproximation(mkUndefinedValue()) + if (reference != null) { val referenceGuard = if (receiver.isFakeObject()) receiver.getFakeType(scope).refTypeExpr else trueExpr val valid = mkOr(mkNot(referenceGuard), mkNotNullOrUndefined(reference)) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 224f294426..71338da7cd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -565,6 +565,8 @@ class TsExprResolver( scope.doWithState { memory.write(deletedFieldLValue(instance, operand.field), trueExpr, guard = trueExpr) + val storageType = arrayStorageType(instance, operand.instance.type) + if (storageType is EtsArrayType) unsupportedIteratorArrays += instance } mkTrue() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index 44181b60d3..51da953ca7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -168,6 +168,11 @@ fun TsContext.assignToArrayIndex( } scope.assert(indexIsInRange) ?: return null + scope.doWithState { + val writtenIndices = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to (writtenIndices + index) + } + val elementSort = typeToSort(arrayType.componentType) // If the element sort is known, write directly. 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 a75c6b7526..d01c01afcc 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 @@ -27,7 +27,10 @@ import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.constraints.UPathConstraints import org.usvm.machine.TsContext import org.usvm.machine.TsInputPropertyPresence +import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.TrackedObjectProperty +import org.usvm.machine.expr.TsArrayIterator +import org.usvm.machine.expr.TsArrayIteratorResult import org.usvm.machine.expr.TsCapturedInstanceCall import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsFunction @@ -72,6 +75,10 @@ class TsState( var methodToRef: UPersistentHashMap = persistentHashMapOf(), var associatedFunction: UPersistentHashMap = persistentHashMapOf(), var capturedInstanceCalls: UPersistentHashMap = persistentHashMapOf(), + internal var arrayIterators: Map = emptyMap(), + internal var arrayIteratorResults: Map = emptyMap(), + internal var unsupportedIteratorArrays: Set = emptySet(), + internal var initializedArrayIndices: Map>> = emptyMap(), var boundThis: UPersistentHashMap = persistentHashMapOf(), var dfltObject: UPersistentHashMap = persistentHashMapOf(), @@ -341,6 +348,10 @@ class TsState( methodToRef = methodToRef, associatedFunction = associatedFunction, capturedInstanceCalls = capturedInstanceCalls, + arrayIterators = arrayIterators, + arrayIteratorResults = arrayIteratorResults, + initializedArrayIndices = initializedArrayIndices, + unsupportedIteratorArrays = unsupportedIteratorArrays, boundThis = boundThis, dfltObject = dfltObject, dfltObjectFieldSorts = dfltObjectFieldSorts, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt new file mode 100644 index 0000000000..dbf87ec783 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt @@ -0,0 +1,89 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +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.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class ArrayIteratorSourceTest : TsMethodTestRunner() { + override val scene = EtsScene( + projectFiles = listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/ArrayIteratorSource.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + override val tsOptions = TsOptions(maxArraySize = 6) + + @Test + fun `native array iteration preserves values evaluation order and live length`() { + val methods = listOf( + "literalSpread", "destructure", "preserveKindsAndAliases", "evaluationOrder", + "liveLength", "shortenedLength", "exhaustedDestructuring", + ) + + for (methodName in methods) { + discoverProperties( + method = getMethod(methodName = methodName, className = "ArrayIteratorSource"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `symbolic array inputs retain both feasible branches`() { + discoverProperties, TsTestValue.TsNumber>( + method = getMethod(methodName = "symbolicInput", className = "ArrayIteratorSource"), + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 0.0 || result.number == 1.0 }), + ) + } + + @Test + fun `custom iterables and sparse arrays retain explicit limitations`() { + for (methodName in listOf("stringNamedLookalike", "sparseArray", "deletedSlot")) { + val method = getMethod(methodName = methodName, className = "ArrayIteratorSource") + val reasons = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + reasons += event.reason + } + } + + TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), methodName) + assertEquals(listOf(TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED), reasons, methodName) + } + } + } + + @Test + fun `own symbol overrides cannot silently use the native array iterator`() { + val method = getMethod(methodName = "customSymbolOverride", className = "ArrayIteratorSource") + + TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.isNotEmpty(), outcome.toString()) + } + } +} diff --git a/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts b/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts new file mode 100644 index 0000000000..68c57cedf3 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts @@ -0,0 +1,89 @@ +export class ArrayIteratorSource { + static literalSpread(): number { + const values = [7, 11]; + const copy = [3, ...values, 13]; + return copy.length === 4 && copy[0] === 3 && copy[1] === 7 && copy[2] === 11 && copy[3] === 13 ? 1 : 0; + } + + static destructure(): number { + const [first, , ...rest] = [7, 11, 13, 17]; + return first === 7 && rest.length === 2 && rest[0] === 13 && rest[1] === 17 ? 1 : 0; + } + + static preserveKindsAndAliases(): number { + const object = { value: 7 }; + const typed = [object]; + const mixed: any[] = typed; + mixed[mixed.length] = null; + mixed[mixed.length] = true; + const copy = [...mixed]; + copy[0].value = 11; + return object.value === 11 && copy[1] === null && copy[2] === true ? 1 : 0; + } + + static orderedValue(order: number[], value: number): number { + order[order.length] = value; + return value; + } + + static evaluationOrder(): number { + const order: number[] = []; + const values = [ArrayIteratorSource.orderedValue(order, 1), ...[ArrayIteratorSource.orderedValue(order, 2)], + ArrayIteratorSource.orderedValue(order, 3)]; + return order.length === 3 && order[0] === 1 && order[1] === 2 && order[2] === 3 && values[1] === 2 ? 1 : 0; + } + + static liveLength(): number { + const values = [1]; + let total = 0; + for (const value of values) { + total += value; + if (values.length === 1) values[values.length] = 2; + } + return total === 3 ? 1 : 0; + } + + static shortenedLength(): number { + const values = [1, 2, 3]; + let total = 0; + for (const value of values) { + total += value; + values.length = 1; + } + return total === 1 ? 1 : 0; + } + + static exhaustedDestructuring(): number { + const values: number[] = []; + const [first = ArrayIteratorSource.orderedValue(values, 7), second] = values; + return first === 7 && second === undefined && values.length === 1 ? 1 : 0; + } + + static symbolicInput(values: number[]): number { + if (values.length !== 2 || values[0] !== 7 || values[1] !== 11) return 0; + const copy = [...values]; + return copy.length === 2 && copy[0] === 7 && copy[1] === 11 ? 1 : 2; + } + + static stringNamedLookalike(): number { + const values: any = { "Symbol.iterator"() { return [7]; } }; + return [...values].length; + } + + static sparseArray(): number { + const values = [1, , 3]; + return [...values].length; + } + + static deletedSlot(): number { + const values = [1, 2]; + delete values[0]; + return [...values].length; + } + + static customSymbolOverride(): number { + const values: any = [1, 2]; + values[Symbol.iterator] = () => ({ next: () => ({ done: true }) }); + return [...values].length; + } +} From 069af503872faaeed834b29bf6d7e676c48642dd Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:07:47 +0300 Subject: [PATCH 07/23] Preserve iterator slot provenance through native array moves --- .../intrinsic/TsArrayShiftIntrinsicModel.kt | 2 + .../usvm/machine/expr/CallApproximations.kt | 45 ++++++++++++++---- .../machine/expr/ArrayIteratorSourceTest.kt | 7 ++- .../resources/models/ArrayIteratorSource.ts | 47 +++++++++++++++++++ 4 files changed, 91 insertions(+), 10 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt index 738278bbe9..1432017426 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt @@ -59,6 +59,8 @@ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { length = newLength, ) memory.write(lengthLValue, newLength, guard = trueExpr) + val initialized = initializedArrayIndices[input.array].orEmpty() + initializedArrayIndices += input.array to initialized.map { index -> mkBvSubExpr(index, one) }.toSet() }, ) 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 e5a76195f1..d04e5ca369 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 @@ -22,6 +22,7 @@ import org.usvm.api.readArrayIndex import org.usvm.getIntValue import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isFalse +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.call.TsUnknownCallFailureReason @@ -40,11 +41,13 @@ import org.usvm.machine.types.TsUnresolvedArrayKind import org.usvm.machine.types.mkFakeValue import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.sizeSort +import org.usvm.util.TsTypedArrayStorage import org.usvm.util.arrayStorageType import org.usvm.util.componentType import org.usvm.util.copyArrayElements import org.usvm.util.forEachArrayPayloadRegion import org.usvm.util.initializeArrayKind +import org.usvm.util.initializeTypedArrayOverrides import org.usvm.util.mkArrayLengthLValue import org.usvm.util.readTypedArrayElement import org.usvm.util.resolveEtsMethods @@ -179,12 +182,6 @@ internal fun TsExprResolver.tryApproximateInstanceCall( val instanceType = scope.calcOnState { arrayStorageType(array, expr.instance.type) } if (instanceType is EtsArrayType) { - // These bulk moves do not carry initialized-slot provenance for sparse allocations. - val movesArraySlots = expr.callee.name in setOf("shift", "unshift", "reverse") - if (movesArraySlots) { - scope.doWithState { initializedArrayIndices -= array } - } - val elementSort = typeToSort(instanceType.componentType) .takeIf { it !is TsUnresolvedSort } ?: addressSort @@ -603,6 +600,8 @@ private fun TsExprResolver.removeArrayElement( if (first) { copyArrayElements(array, array, arrayType, fromSrc = mkBv(1), fromDst = mkBv(0), length = newLength) + val initialized = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to initialized.map { index -> mkBvSubExpr(index, mkBv(1)) }.toSet() } memory.write(lengthLValue, newLength, guard = trueExpr) @@ -728,6 +727,11 @@ private fun TsExprResolver.handleArrayFill( length = fillLength, ) + val initialized = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to initialized.map { index -> + mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index) + }.toSet() + // Return the modified original array array } @@ -817,6 +821,9 @@ private fun TsExprResolver.handleArrayUnshift( length = length, ) + val initialized = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to initialized.map { index -> mkBvAddExpr(index, mkBv(1)) }.toSet() + // Write the new element to the start of the array assignToArrayIndex(scope, array, index = mkBv(0), expr = arg, arrayType = arrayType) ?: return@calcOnState null @@ -1214,7 +1221,19 @@ private fun TsExprResolver.handleArrayReverse( val lengthLValue = mkArrayLengthLValue(array, arrayType) val length = memory.read(lengthLValue) - val reversedIndices = (0 until ARRAY_REVERSE_MAX_SIZE).map { index -> + val withinCapacity = mkAnd( + mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), + mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)), + ) + if (scope.checkSat(mkNot(withinCapacity)) != null) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, + detail = "Array.reverse exceeds the configured length bound ${options.maxArraySize}", + ) + } + scope.assert(withinCapacity) ?: return@calcOnState null + + val reversedIndices = (0 until options.maxArraySize).map { index -> mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index.toBv()) } forEachArrayPayloadRegion(arrayType) { region, sort -> @@ -1228,6 +1247,16 @@ private fun TsExprResolver.handleArrayReverse( val contents = reversedIndices.map { index -> memory.readArrayIndex(array, index, kind, boolSort) } initializeArrayKind(reversedArray, kind, contents) } + } else { + initializeTypedArrayOverrides(array) + val hasBoxedValues = reversedIndices.asSequence().map { index -> + memory.readArrayIndex(array, index, TsTypedArrayStorage.HAS_BOXED_VALUE, boolSort) + } + val boxedValues = reversedIndices.asSequence().map { index -> + memory.readArrayIndex(array, index, TsTypedArrayStorage.BOXED_VALUE, addressSort) + } + memory.initializeArray(reversedArray, TsTypedArrayStorage.HAS_BOXED_VALUE, boolSort, sizeSort, hasBoxedValues) + memory.initializeArray(reversedArray, TsTypedArrayStorage.BOXED_VALUE, addressSort, sizeSort, boxedValues) } copyArrayElements( @@ -1243,5 +1272,3 @@ private fun TsExprResolver.handleArrayReverse( array } } - -private const val ARRAY_REVERSE_MAX_SIZE = 5000 diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt index dbf87ec783..da008bc5dd 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt @@ -32,6 +32,7 @@ class ArrayIteratorSourceTest : TsMethodTestRunner() { val methods = listOf( "literalSpread", "destructure", "preserveKindsAndAliases", "evaluationOrder", "liveLength", "shortenedLength", "exhaustedDestructuring", + "reversedMixedAlias", "unshiftedMixedAlias", "shiftedMixedAlias", ) for (methodName in methods) { @@ -55,7 +56,11 @@ class ArrayIteratorSourceTest : TsMethodTestRunner() { @Test fun `custom iterables and sparse arrays retain explicit limitations`() { - for (methodName in listOf("stringNamedLookalike", "sparseArray", "deletedSlot")) { + val methods = listOf( + "stringNamedLookalike", "sparseArray", "deletedSlot", + "reversedSparseArray", "unshiftedSparseArray", "shiftedSparseArray", + ) + for (methodName in methods) { val method = getMethod(methodName = methodName, className = "ArrayIteratorSource") val reasons = mutableListOf() val observer = object : TsInterpreterObserver { diff --git a/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts b/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts index 68c57cedf3..e7b0ff1d27 100644 --- a/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts +++ b/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts @@ -65,6 +65,53 @@ export class ArrayIteratorSource { return copy.length === 2 && copy[0] === 7 && copy[1] === 11 ? 1 : 2; } + static reversedMixedAlias(): number { + const values = [7, 11, 13]; + const alias: any[] = values; + alias[1] = true; + alias[2] = null; + values.reverse(); + const copy = [...alias]; + return copy.length === 3 && copy[0] === null && copy[1] === true && copy[2] === 7 ? 1 : 0; + } + + static unshiftedMixedAlias(): number { + const values = [7, 11]; + const alias: any[] = values; + alias[1] = null; + alias.unshift(true); + const copy = [...alias]; + return copy.length === 3 && copy[0] === true && copy[1] === 7 && copy[2] === null ? 1 : 0; + } + + static shiftedMixedAlias(): number { + const values = [7, 11, 13]; + const alias: any[] = values; + alias[1] = null; + alias[2] = true; + const first = alias.shift(); + const copy = [...alias]; + return first === 7 && copy.length === 2 && copy[0] === null && copy[1] === true ? 1 : 0; + } + + static shiftedSparseArray(): number { + const values = [1, , 3]; + values.shift(); + return [...values].length; + } + + static reversedSparseArray(): number { + const values = [1, , 3]; + values.reverse(); + return [...values].length; + } + + static unshiftedSparseArray(): number { + const values = [1, , 3]; + values.unshift(7); + return [...values].length; + } + static stringNamedLookalike(): number { const values: any = { "Symbol.iterator"() { return [7]; } }; return [...values].length; From b34945c55e4b5110030962563c28071d33f43fbe Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:11:47 +0300 Subject: [PATCH 08/23] Support bounded native string iterators over UTF16 code points --- .../org/usvm/machine/TsInterpreterObserver.kt | 1 + .../org/usvm/machine/expr/ArrayIterator.kt | 26 +-- .../usvm/machine/expr/CallApproximations.kt | 2 +- .../kotlin/org/usvm/machine/expr/ReadField.kt | 2 +- .../org/usvm/machine/expr/StringIterator.kt | 102 ++++++++++++ .../machine/expr/TsCapturedInstanceCall.kt | 2 +- .../kotlin/org/usvm/machine/state/TsState.kt | 9 +- .../machine/expr/StringIteratorSourceTest.kt | 153 ++++++++++++++++++ .../resources/models/StringIteratorSource.ts | 54 +++++++ 9 files changed, 335 insertions(+), 16 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt create mode 100644 usvm-ts/src/test/resources/models/StringIteratorSource.ts 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 702d368b65..d115df1717 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -100,4 +100,5 @@ enum class TsRuntimeFeatureLimitationReason { ARRAY_ITERATOR_UNSUPPORTED, ARRAY_LENGTH_CAPACITY, ARRAY_LENGTH_GROWTH, + STRING_ITERATOR_UNSUPPORTED, } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt index 9a93d03e8e..c3f10ce528 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -26,24 +26,30 @@ data class TsArrayIterator( val exhausted: UBoolExpr, ) -data class TsArrayIteratorResult(val done: UBoolExpr, val value: UExpr<*>) +data class TsIteratorResult(val done: UBoolExpr, val value: UExpr<*>) private val iteratorType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinArrayIterator")) -private val iteratorResultType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinArrayIteratorResult")) +internal val iteratorResultType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinIteratorResult")) -internal fun TsExprResolver.tryApproximateArrayIteratorCall( +internal fun TsExprResolver.tryApproximateBuiltinIteratorCall( stmt: TsVirtualMethodCallStmt, ): TsExprApproximationResult = with(ctx) { if (stmt.call.wellKnownSymbol == EtsWellKnownSymbol.ITERATOR) { + val string = tryCreateStringIterator(stmt) + if (string !is TsExprApproximationResult.NoApproximation) return string + return TsExprApproximationResult.from(createArrayIterator(stmt)) } val reference = stmt.instance as? UConcreteHeapRef ?: return TsExprApproximationResult.NoApproximation - val iterator = scope.calcOnState { arrayIterators[reference] } - ?: return TsExprApproximationResult.NoApproximation if (stmt.call.callee.name != "next") return TsExprApproximationResult.NoApproximation - TsExprApproximationResult.from(advanceArrayIterator(reference, iterator)) + val stringIterator = scope.calcOnState { stringIterators[reference] } + if (stringIterator != null) return TsExprApproximationResult.from(advanceStringIterator(reference, stringIterator)) + + val arrayIterator = scope.calcOnState { arrayIterators[reference] } + ?: return TsExprApproximationResult.NoApproximation + TsExprApproximationResult.from(advanceArrayIterator(reference, arrayIterator)) } private fun TsExprResolver.createArrayIterator(stmt: TsVirtualMethodCallStmt): UHeapRef? = with(ctx) { @@ -143,15 +149,15 @@ private fun TsExprResolver.advanceArrayIterator( exhausted = done, ) val result = memory.allocConcrete(iteratorResultType) - arrayIteratorResults += result to TsArrayIteratorResult(done = done, value = value) + iteratorResults += result to TsIteratorResult(done = done, value = value) result } } -internal fun TsExprResolver.readArrayIteratorField(reference: UHeapRef, name: String): UExpr<*>? = with(ctx) { +internal fun TsExprResolver.readBuiltinIteratorField(reference: UHeapRef, name: String): UExpr<*>? = with(ctx) { if (reference !is UConcreteHeapRef) return null - val result = scope.calcOnState { arrayIteratorResults[reference] } + val result = scope.calcOnState { iteratorResults[reference] } if (result != null) { return when (name) { "done" -> result.done @@ -160,7 +166,7 @@ internal fun TsExprResolver.readArrayIteratorField(reference: UHeapRef, name: St } } - val isIterator = scope.calcOnState { arrayIterators[reference] != null } + val isIterator = scope.calcOnState { arrayIterators[reference] != null || stringIterators[reference] != null } if (isIterator && name == "return") return mkUndefinedValue() null 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 d04e5ca369..20b52f399a 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 @@ -155,7 +155,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( val expr = stmt.call val instance = stmt.instance - val iterator = tryApproximateArrayIteratorCall(stmt) + val iterator = tryApproximateBuiltinIteratorCall(stmt) if (iterator !is TsExprApproximationResult.NoApproximation) return iterator // Mock `.toString()` method calls diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 29d7db9202..9a3603f575 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -87,7 +87,7 @@ internal fun TsExprResolver.handleInstanceFieldRef( checkUndefinedOrNullPropertyRead(scope, rawInstance, propertyName = value.field.name) ?: return null val instance = resolveHeapRef(scope, rawInstance) ?: return null - val iteratorField = readArrayIteratorField(instance, value.field.name) + val iteratorField = readBuiltinIteratorField(instance, value.field.name) if (iteratorField != null) return iteratorField // Handle reading "length" property. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt new file mode 100644 index 0000000000..859c8467d0 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt @@ -0,0 +1,102 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsStringLiteralType +import org.jacodb.ets.model.EtsStringType +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.isTrue +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.TsSizeSort +import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.util.allocateBoundedString +import org.usvm.util.arrayStorageType +import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.stringCharacters +import org.usvm.util.stringLength + +/** A string iterator keeps its original immutable string when the source binding is reassigned. */ +data class TsStringIterator( + val string: UHeapRef, + val index: UExpr, + val exhausted: UBoolExpr, +) + +private val stringIteratorType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinStringIterator")) + +internal fun TsExprResolver.tryCreateStringIterator( + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult = with(ctx) { + if (stmt.instance.sort != addressSort) return TsExprApproximationResult.NoApproximation + + val string = stmt.instance.asExpr(addressSort) + val lengthBound = scope.calcOnState { boundedStringBackingRefs[string] } + if (lengthBound == null) { + val storageType = scope.calcOnState { arrayStorageType(string, stmt.call.instance.type) } + val requiresStringBacking = storageType == EtsStringType || storageType is EtsStringLiteralType + if (!requiresStringBacking) return TsExprApproximationResult.NoApproximation + + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.STRING_ITERATOR_UNSUPPORTED, + detail = "String iteration requires modeled UTF-16 backing", + ) + scope.assert(falseExpr) + return TsExprApproximationResult.ResolveFailure + } + + // The private backing registry is runtime evidence; a String annotation alone cannot create an iterator. + val length = scope.calcOnState { stringLength(string) } + ensureLengthBounds(scope = scope, length = length, maxLength = lengthBound) + ?: return TsExprApproximationResult.ResolveFailure + + val iterator = scope.calcOnState { + val reference = memory.allocConcrete(stringIteratorType) + stringIterators += reference to TsStringIterator(string = string, index = mkBv(0), exhausted = falseExpr) + reference + } + TsExprApproximationResult.SuccessfulApproximation(iterator) +} + +internal fun TsExprResolver.advanceStringIterator( + reference: UConcreteHeapRef, + iterator: TsStringIterator, +): UHeapRef = with(ctx) { + val length = scope.calcOnState { stringLength(iterator.string) } + val done = mkOr(iterator.exhausted, mkBvSignedGreaterOrEqualExpr(iterator.index, length)) + val width: UExpr + val value: UHeapRef + if (done.isTrue) { + width = mkBv(0) + value = mkUndefinedValue() + } else { + val nextIndex = mkBvAddExpr(iterator.index, mkBv(1)) + val (first, second) = scope.calcOnState { + val characters = stringCharacters(iterator.string) + memory.read(mkStringBackingElementLValue(characters, iterator.index)) to + memory.read(mkStringBackingElementLValue(characters, nextIndex)) + } + val firstIsHighSurrogate = mkEq(mkBvAndExpr(first, mkBv(0xfc00, bv16Sort)), mkBv(0xd800, bv16Sort)) + val secondIsLowSurrogate = mkEq(mkBvAndExpr(second, mkBv(0xfc00, bv16Sort)), mkBv(0xdc00, bv16Sort)) + val pair = mkAnd(firstIsHighSurrogate, mkBvSignedLessExpr(nextIndex, length), secondIsLowSurrogate) + width = mkIte(pair, mkBv(2), mkBv(1)) + + val character = scope.calcOnState { + allocateBoundedString(length = width, codeUnits = listOf(first, second)) + } + value = mkIte(done, mkUndefinedValue(), character) + } + + scope.calcOnState { + stringIterators += reference to iterator.copy( + index = mkIte(done, iterator.index, mkBvAddExpr(iterator.index, width)), + exhausted = done, + ) + val result = memory.allocConcrete(iteratorResultType) + iteratorResults += result to TsIteratorResult(done = done, value = value) + result + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt index 569377d79e..7cc6bbd6bd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt @@ -64,7 +64,7 @@ internal fun TsExprResolver.tryCaptureInstanceCall( else -> null } val builtinReturn = field.field.name == "return" && reference is UConcreteHeapRef && - scope.calcOnState { arrayIterators[reference] != null } + scope.calcOnState { arrayIterators[reference] != null || stringIterators[reference] != null } if (builtinReturn) return TsExprApproximationResult.SuccessfulApproximation(mkUndefinedValue()) if (reference != null) { 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 d01c01afcc..b5dc837a0b 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 @@ -30,8 +30,9 @@ import org.usvm.machine.TsInputPropertyPresence import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.TrackedObjectProperty import org.usvm.machine.expr.TsArrayIterator -import org.usvm.machine.expr.TsArrayIteratorResult import org.usvm.machine.expr.TsCapturedInstanceCall +import org.usvm.machine.expr.TsIteratorResult +import org.usvm.machine.expr.TsStringIterator import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsFunction import org.usvm.memory.ULValue @@ -76,7 +77,8 @@ class TsState( var associatedFunction: UPersistentHashMap = persistentHashMapOf(), var capturedInstanceCalls: UPersistentHashMap = persistentHashMapOf(), internal var arrayIterators: Map = emptyMap(), - internal var arrayIteratorResults: Map = emptyMap(), + internal var stringIterators: Map = emptyMap(), + internal var iteratorResults: Map = emptyMap(), internal var unsupportedIteratorArrays: Set = emptySet(), internal var initializedArrayIndices: Map>> = emptyMap(), var boundThis: UPersistentHashMap = persistentHashMapOf(), @@ -349,7 +351,8 @@ class TsState( associatedFunction = associatedFunction, capturedInstanceCalls = capturedInstanceCalls, arrayIterators = arrayIterators, - arrayIteratorResults = arrayIteratorResults, + iteratorResults = iteratorResults, + stringIterators = stringIterators, initializedArrayIndices = initializedArrayIndices, unsupportedIteratorArrays = unsupportedIteratorArrays, boundThis = boundThis, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt new file mode 100644 index 0000000000..ef1829245f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt @@ -0,0 +1,153 @@ +package org.usvm.machine.expr + +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.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.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.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class StringIteratorSourceTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/StringIteratorSource.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + override val tsOptions = TsOptions(maxArraySize = 8) + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + val limitations = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions, observer = observer).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, method.name) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${method.name}: ${outcome.unsupportedPaths}") + assertTrue(limitations.isEmpty(), "${method.name}: $limitations") + outcome.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `string iteration combines surrogate pairs and preserves isolated units`() { + for (methodName in literalMethods) { + discoverProperties( + method = method(methodName), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `symbolic iteration explores empty lone unit pair and separate unit branches`() { + discoverProperties( + method = method("symbolicWidth"), + { _, result -> result.number == -1.0 }, + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + { _, result -> result.number == 2.0 }, + { _, result -> result.number == 3.0 }, + invariants = arrayOf({ input, result -> + val value = input.value + val expected = when { + value.length > 2 -> -1 + value.isEmpty() -> 0 + value.length == 1 -> 1 + Character.isSurrogatePair(value[0], value[1]) -> 2 + else -> 3 + } + result.number == expected.toDouble() + }), + ) + } + + @Test + fun `symbolic iterator result retains exact UTF16 payload`() { + discoverProperties( + method = method("symbolicFirst"), + { _, result -> result.value.isEmpty() }, + { _, result -> result.value.length == 1 }, + { _, result -> result.value.length == 2 }, + invariants = arrayOf({ input, result -> + val value = input.value + val expected = when { + value.length != 2 -> "" + Character.isSurrogatePair(value[0], value[1]) -> value + else -> value.take(1) + } + result.value == expected + }), + ) + } + + @Test + fun `literal and generated symbolic witnesses replay with native string iteration`() { + val script = buildString { + appendLine(source.readText()) + for (methodName in literalMethods) { + appendLine("if (StringIteratorSource.$methodName() !== 1) throw Error('$methodName');") + } + for (methodName in listOf("symbolicWidth", "symbolicFirst")) { + val tests = runner(method(methodName), options) + assertTrue(tests.isNotEmpty(), methodName) + for (test in tests) { + val input = assertIs(test.before.parameters.single()).value + val expected = when (val result = test.returnValue) { + is TsTestValue.TsString -> jsString(result.value) + else -> assertIs(result).number.toString() + } + val invocation = "StringIteratorSource.$methodName(${jsString(input)})" + appendLine("if ($invocation !== $expected) throw Error('$methodName');") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "string-iterator", + timeoutMessage = "String iterator replay timed out", + ) + } + + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "StringIteratorSource") + + private val literalMethods = listOf( + "mixedUtf16", "reversedSurrogates", "destructuring", + "exhaustedDestructuring", "reboundSource", "shadowedSymbol", + ) +} diff --git a/usvm-ts/src/test/resources/models/StringIteratorSource.ts b/usvm-ts/src/test/resources/models/StringIteratorSource.ts new file mode 100644 index 0000000000..01164b26b4 --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringIteratorSource.ts @@ -0,0 +1,54 @@ +export class StringIteratorSource { + static mixedUtf16(): number { + const values = [..."A\ud83d\ude00\ud800B\udc00\u0000"]; + return values.length === 6 && values[0] === "A" && values[1] === "\ud83d\ude00" && + values[2] === "\ud800" && values[3] === "B" && values[4] === "\udc00" && values[5] === "\u0000" ? 1 : 0; + } + + static reversedSurrogates(): number { + const values = [..."\udc00\ud800"]; + return values.length === 2 && values[0] === "\udc00" && values[1] === "\ud800" ? 1 : 0; + } + + static destructuring(): number { + const [first, second, ...rest] = "\ud83d\ude00A\ud800"; + return first === "\ud83d\ude00" && second === "A" && rest.length === 1 && rest[0] === "\ud800" ? 1 : 0; + } + + static exhaustedDestructuring(): number { + const [first, second = "end", third] = "\ud83d\ude00"; + return first === "\ud83d\ude00" && second === "end" && third === undefined ? 1 : 0; + } + + static reboundSource(): number { + let source = "A\ud83d\ude00"; + let count = 0; + let units = 0; + for (const value of source) { + count++; + units += value.length; + source = "different"; + } + return count === 2 && units === 3 ? 1 : 0; + } + + static shadowedSymbol(): number { + const Symbol = { iterator: "wrong" }; + const values = [..."\ud83d\ude00"]; + return Symbol.iterator === "wrong" && values.length === 1 && values[0].length === 2 ? 1 : 0; + } + + static symbolicWidth(value: string): number { + if (value.length > 2) return -1; + const values = [...value]; + if (values.length === 0) return 0; + if (values.length === 1) return values[0].length; + return 3; + } + + static symbolicFirst(value: string): string { + if (value.length !== 2) return ""; + const [first] = value; + return first; + } +} From 2919f2937c954e62e5c9f6417ad10f0da5c1de3c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:19:14 +0300 Subject: [PATCH 09/23] Apply iterator provenance reversal in the reverse implementation --- .../kotlin/org/usvm/machine/expr/CallApproximations.kt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 20b52f399a..353958aa2b 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 @@ -727,11 +727,6 @@ private fun TsExprResolver.handleArrayFill( length = fillLength, ) - val initialized = initializedArrayIndices[array].orEmpty() - initializedArrayIndices += array to initialized.map { index -> - mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index) - }.toSet() - // Return the modified original array array } @@ -1268,6 +1263,11 @@ private fun TsExprResolver.handleArrayReverse( length = length ) + val initialized = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to initialized.map { index -> + mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index) + }.toSet() + // Return the modified original array array } From 7924887b6953e0d2d7cc72215d7230fea230dfb1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:53:50 +0300 Subject: [PATCH 10/23] Cover source SDK constructor shadows in native iterator inputs --- .../expr/SourceSdkConstructorShadowTest.kt | 51 +++++++++++++++++++ .../models/SourceSdkConstructorShadow.ts | 17 +++++++ 2 files changed, 68 insertions(+) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt create mode 100644 usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt new file mode 100644 index 0000000000..1bc352a8a6 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt @@ -0,0 +1,51 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.io.TempDir +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test + +class SourceSdkConstructorShadowTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/SourceSdkConstructorShadow.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + + @Test + fun `file global source methods retain their implementation before SDK constructor matching`() { + for (name in methods) { + discoverProperties( + method = getMethod(methodName = name, className = "SourceSdkConstructorShadow"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `source constructor shadows agree with native JavaScript`() { + val script = buildString { + appendLine(source.readText()) + for (name in methods) { + appendLine("if (SourceSdkConstructorShadow.$name() !== 1) throw Error('$name');") + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "source-sdk-constructor-shadow", + timeoutMessage = "Source constructor shadow replay timed out", + ) + } + + private val methods = listOf("objectMethodKeepsSourceImplementation", "arrayMethodKeepsSourceImplementation") +} diff --git a/usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts b/usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts new file mode 100644 index 0000000000..b56e79ab22 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts @@ -0,0 +1,17 @@ +// @ts-expect-error This source binding implements only the method used below. +const Object: typeof globalThis.Object = { setPrototypeOf(target: any, _prototype: any): any { target[0] = 9; return target; } }; + +// @ts-expect-error This source binding implements only the method used below. +const Array: typeof globalThis.Array = { isArray: (_value: unknown): boolean => false }; + +export class SourceSdkConstructorShadow { + static objectMethodKeepsSourceImplementation(): number { + const values = [7]; + const result = Object.setPrototypeOf(values, { 0: 11 }); + return result === values && values[0] === 9 ? 1 : 0; + } + + static arrayMethodKeepsSourceImplementation(): number { + return Array.isArray([]) ? 0 : 1; + } +} From 0acbbbc0b3f4237768c7dcce0929bc13f74c5203 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:37:26 +0300 Subject: [PATCH 11/23] Track own sparse array slots through native iteration and mutation --- .../intrinsic/TsArrayShiftIntrinsicModel.kt | 38 +++- .../org/usvm/machine/expr/ArrayIterator.kt | 13 +- .../machine/expr/ArrayPrototypeBoundary.kt | 87 +++++++++ .../usvm/machine/expr/CallApproximations.kt | 36 ++-- .../org/usvm/machine/expr/DeleteArray.kt | 39 ++++ .../kotlin/org/usvm/machine/expr/ReadArray.kt | 23 +++ .../kotlin/org/usvm/machine/expr/ReadField.kt | 6 + .../machine/expr/TsCapturedInstanceCall.kt | 3 + .../org/usvm/machine/expr/TsExprResolver.kt | 7 + .../org/usvm/machine/expr/WriteArray.kt | 4 +- .../org/usvm/machine/expr/WriteField.kt | 8 + .../kotlin/org/usvm/machine/state/TsState.kt | 5 +- .../org/usvm/util/ArrayIndexPresence.kt | 46 +++++ .../machine/expr/ArrayIteratorSourceTest.kt | 7 +- .../expr/SparseArrayIteratorSourceTest.kt | 175 +++++++++++++++++ .../models/SparseArrayIteratorSource.ts | 183 ++++++++++++++++++ 16 files changed, 634 insertions(+), 46 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayPrototypeBoundary.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeleteArray.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt create mode 100644 usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt index 1432017426..47dce2f746 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt @@ -6,6 +6,7 @@ import org.usvm.UAddressSort import org.usvm.UExpr import org.usvm.USort import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.machine.TsSizeSort import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallFailureReason @@ -15,11 +16,17 @@ import org.usvm.machine.call.TsUnknownCallModelSuccessor import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.state.TsState +import org.usvm.machine.types.EtsFakeType +import org.usvm.machine.types.TsUnresolvedValue +import org.usvm.machine.types.iteUnresolvedValue import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.util.arrayStorageType import org.usvm.util.copyArrayElements +import org.usvm.util.knownArrayIndexPresence import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.moveInitializedArrayIndices import org.usvm.util.readTypedArrayElement +import org.usvm.util.truncateKnownArrayIndices /** Engine intrinsic for `Array.shift`, whose bulk move is implemented by symbolic-memory `memcpy`. */ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { @@ -59,8 +66,8 @@ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { length = newLength, ) memory.write(lengthLValue, newLength, guard = trueExpr) - val initialized = initializedArrayIndices[input.array].orEmpty() - initializedArrayIndices += input.array to initialized.map { index -> mkBvSubExpr(index, one) }.toSet() + moveInitializedArrayIndices(input.array) { index -> mkBvSubExpr(index, one) } + truncateKnownArrayIndices(input.array, newLength) }, ) @@ -93,17 +100,28 @@ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { input: ArrayShiftInput, index: UExpr, ): TsUnknownCallModelCompletion = with(ctx) { - if (input.elementSort !is TsUnresolvedSort) { - val element = readTypedArrayElement(input.array, index, input.arrayType) - return@with if (element.hasBoxedValue.isFalse) { - TsUnknownCallModelCompletion.Normal { element.nativeValue } - } else { - TsUnknownCallModelCompletion.Unresolved(element.unresolvedValue) + val present = knownArrayIndexPresence(input.array, index) + if (present?.isFalse == true) return@with TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() } + + val element = if (input.elementSort !is TsUnresolvedSort) { + val typed = readTypedArrayElement(input.array, index, input.arrayType) + val unboxedPresent = (present == null || present.isTrue) && typed.hasBoxedValue.isFalse + if (unboxedPresent) { + return@with TsUnknownCallModelCompletion.Normal { typed.nativeValue } } + typed.unresolvedValue + } else { + readUnresolvedArrayElement(memory, input.array, index) } + if (present == null || present.isTrue) return@with TsUnknownCallModelCompletion.Unresolved(element) - val firstElement = readUnresolvedArrayElement(memory, input.array, index) - TsUnknownCallModelCompletion.Unresolved(firstElement) + val absent = TsUnresolvedValue( + boolValue = falseExpr, + fpValue = mkFp64(0.0), + refValue = mkUndefinedValue(), + type = EtsFakeType.mkRef(ctx), + ) + TsUnknownCallModelCompletion.Unresolved(iteUnresolvedValue(present, element, absent)) } private class ArrayShiftInput( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt index c3f10ce528..536facab0d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -17,6 +17,7 @@ import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.writtenArrayIndexPresence /** State belongs to a particular native array iterator, independently of its source binding. */ data class TsArrayIterator( @@ -92,7 +93,7 @@ private fun TsExprResolver.advanceArrayIterator( ): UHeapRef? = with(ctx) { val invalidated = scope.calcOnState { iterator.array in unsupportedIteratorArrays } if (invalidated) { - unsupportedArrayIterator("Array iteration after deleting an indexed property is not modeled") + unsupportedArrayIterator("Array iteration needs known element-presence and value storage") return null } @@ -111,22 +112,22 @@ private fun TsExprResolver.advanceArrayIterator( val done = mkOr(iterator.exhausted, mkBvSignedGreaterOrEqualExpr(iterator.index, length)) val initialized = scope.calcOnState { - // Symbolic array inputs use the engine's dense input contract. Allocations need actual slot writes. + // Inputs are dense; known allocations distinguish written own slots from holes. val array = iterator.array val denseInput = !isAllocatedConcreteHeapRef(array) || (array is UConcreteHeapRef && denseInputArrays[array] != null) - if (denseInput) { + val knownOwnSlots = array in knownArrayPropertyPresence + if (denseInput || knownOwnSlots) { trueExpr } else { - val initializedSlots = initializedArrayIndices[array].orEmpty() - mkOr(initializedSlots.map { index -> mkEq(iterator.index, index) }) + writtenArrayIndexPresence(array, iterator.index) } } val supportedRead = mkOr(done, initialized) if (scope.checkSat(mkNot(supportedRead)) != null) { reportRuntimeFeatureLimitation( reason = TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED, - detail = "Array iteration over uninitialized slots is not modeled", + detail = "Array iteration requires known own-slot provenance", ) } scope.assert(supportedRead) ?: return null diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayPrototypeBoundary.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayPrototypeBoundary.kt new file mode 100644 index 0000000000..602f596a82 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayPrototypeBoundary.kt @@ -0,0 +1,87 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsType +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.isFalse +import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.util.arrayStorageType + +/** Missing own array slots may yield undefined only while prototype changes stay outside the supported domain. */ +internal fun TsExprResolver.ensureSupportedArrayPrototypeAccess(receiver: UHeapRef, fieldName: String): Boolean { + if (receiver is UIteExpr<*>) { + val resolved = ctx.resolveHeapRef(scope, receiver) ?: return false + return ensureSupportedArrayPrototypeAccess(resolved, fieldName) + } + + if (fieldName == "__proto__") { + val runtimeType = scope.calcOnState { arrayStorageType(receiver, EtsUnknownType) } + if (runtimeType is EtsArrayType) { + throw UnsupportedOperationException("Array prototype access and mutation are not modeled") + } + } + if (fieldName != "prototype" || receiver !is UConcreteHeapRef) return true + + val signature = ctx.classConstructorSignature(receiver) ?: return true + val coreConstructor = ctx.scene.sdkClasses.any { clazz -> + clazz.signature == signature && clazz.name in setOf("Object", "Array") + } + if (coreConstructor) { + throw UnsupportedOperationException("Builtin Object and Array prototype access is not modeled") + } + return true +} + +internal fun TsExprResolver.ensureSupportedObjectMutation(stmt: TsVirtualMethodCallStmt): Boolean = with(ctx) { + val changesOrExposesProperties = stmt.call.callee.name in setOf( + "setPrototypeOf", "getPrototypeOf", "defineProperty", "defineProperties", "assign", + "freeze", "seal", "preventExtensions", + ) + if (!changesOrExposesProperties) return true + + val receiver = stmt.instance as? UConcreteHeapRef ?: return true + val signature = ctx.classConstructorSignature(receiver) ?: return true + val builtinObject = ctx.scene.sdkClasses.any { clazz -> clazz.name == "Object" && clazz.signature == signature } + if (!builtinObject) return true + + if (stmt.call.callee.name == "getPrototypeOf") { + // Even an ordinary object can expose Object.prototype, which supplies inherited array indexes. + throw UnsupportedOperationException("Builtin prototype reflection is not modeled") + } + + val target = stmt.args.firstOrNull() ?: return true + val staticType = stmt.call.args.firstOrNull()?.type ?: EtsUnknownType + val targetsArray = arrayTargetCondition(target, staticType) + if (targetsArray.isFalse) return true + + // Ordinary object targets retain their existing dispatcher/model behavior. + scope.fork(mkNot(targetsArray), blockOnFalseState = { + terminateAsUnsupported(reason = "Reflective Object operations on arrays are not modeled") + }) != null +} + +private fun TsExprResolver.arrayTargetCondition(target: UExpr<*>, staticType: EtsType): UBoolExpr = with(ctx) { + if (target.sort != addressSort) return falseExpr + if (target.isFakeObject()) { + val referenceKind = target.getFakeType(scope).refTypeExpr + val reference = target.extractRef(scope) + return mkAnd(referenceKind, arrayTargetCondition(reference, staticType)) + } + if (target is UIteExpr<*>) { + return mkIte( + target.condition, + arrayTargetCondition(target.trueBranch, staticType), + arrayTargetCondition(target.falseBranch, staticType), + ) + } + + val reference = target.asExpr(addressSort) + val runtimeType = scope.calcOnState { arrayStorageType(reference, staticType) } + mkBool(runtimeType is EtsArrayType) +} 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 353958aa2b..5808744f44 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 @@ -21,7 +21,6 @@ import org.usvm.api.memcpy import org.usvm.api.readArrayIndex import org.usvm.getIntValue import org.usvm.isAllocatedConcreteHeapRef -import org.usvm.isFalse import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt @@ -38,8 +37,6 @@ import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.lastStmt import org.usvm.machine.state.newStmt import org.usvm.machine.types.TsUnresolvedArrayKind -import org.usvm.machine.types.mkFakeValue -import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.sizeSort import org.usvm.util.TsTypedArrayStorage import org.usvm.util.arrayStorageType @@ -49,8 +46,9 @@ import org.usvm.util.forEachArrayPayloadRegion import org.usvm.util.initializeArrayKind import org.usvm.util.initializeTypedArrayOverrides import org.usvm.util.mkArrayLengthLValue -import org.usvm.util.readTypedArrayElement +import org.usvm.util.moveInitializedArrayIndices import org.usvm.util.resolveEtsMethods +import org.usvm.util.truncateKnownArrayIndices private val logger = KotlinLogging.logger {} @@ -154,6 +152,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( ): TsExprApproximationResult = with(ctx) { val expr = stmt.call val instance = stmt.instance + if (!ensureSupportedObjectMutation(stmt)) return TsExprApproximationResult.ResolveFailure val iterator = tryApproximateBuiltinIteratorCall(stmt) if (iterator !is TsExprApproximationResult.NoApproximation) return iterator @@ -572,7 +571,6 @@ private fun TsExprResolver.removeArrayElement( arrayType: EtsArrayType, first: Boolean, ): UExpr<*>? = with(ctx) { - val storageSort = typeToSort(arrayType.componentType) val lengthLValue = mkArrayLengthLValue(array, arrayType) val length = scope.calcOnState { memory.read(lengthLValue) } val nonEmpty = mkNot(mkEq(length, mkBv(0))) @@ -587,22 +585,13 @@ private fun TsExprResolver.removeArrayElement( scope.calcOnState { val newLength = mkBvSubExpr(length, mkBv(1)) val index = if (first) mkBv(0) else newLength - val removed = if (storageSort is TsUnresolvedSort) { - mkFakeValue(scope, readUnresolvedArrayElement(memory, array, index)) - } else { - val element = readTypedArrayElement(array, index, arrayType) - if (element.hasBoxedValue.isFalse) { - element.nativeValue - } else { - mkFakeValue(scope, element.unresolvedValue) - } - } + val removed = readArrayElement(scope, array, index, arrayType) if (first) { copyArrayElements(array, array, arrayType, fromSrc = mkBv(1), fromDst = mkBv(0), length = newLength) - val initialized = initializedArrayIndices[array].orEmpty() - initializedArrayIndices += array to initialized.map { index -> mkBvSubExpr(index, mkBv(1)) }.toSet() + moveInitializedArrayIndices(array) { index -> mkBvSubExpr(index, mkBv(1)) } } + truncateKnownArrayIndices(array, newLength) memory.write(lengthLValue, newLength, guard = trueExpr) removed @@ -727,6 +716,11 @@ private fun TsExprResolver.handleArrayFill( length = fillLength, ) + // This legacy fill path does not preserve boxed overrides or sparse-slot metadata. + knownArrayPropertyPresence -= array + initializedArrayIndices -= array + unsupportedIteratorArrays += array + // Return the modified original array array } @@ -816,8 +810,7 @@ private fun TsExprResolver.handleArrayUnshift( length = length, ) - val initialized = initializedArrayIndices[array].orEmpty() - initializedArrayIndices += array to initialized.map { index -> mkBvAddExpr(index, mkBv(1)) }.toSet() + moveInitializedArrayIndices(array) { index -> mkBvAddExpr(index, mkBv(1)) } // Write the new element to the start of the array assignToArrayIndex(scope, array, index = mkBv(0), expr = arg, arrayType = arrayType) @@ -1263,10 +1256,7 @@ private fun TsExprResolver.handleArrayReverse( length = length ) - val initialized = initializedArrayIndices[array].orEmpty() - initializedArrayIndices += array to initialized.map { index -> - mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index) - }.toSet() + moveInitializedArrayIndices(array) { index -> mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index) } // Return the modified original array array 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 new file mode 100644 index 0000000000..816810f2ae --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeleteArray.kt @@ -0,0 +1,39 @@ +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.sizeSort +import org.usvm.util.arrayStorageType +import org.usvm.util.deleteKnownArrayIndex + +internal fun TsExprResolver.tryDeleteArrayIndex(value: EtsArrayAccess): TsExprApproximationResult = with(ctx) { + val resolved = resolve(value.array) ?: return TsExprApproximationResult.ResolveFailure + val rawArray = if (resolved.isFakeObject()) { + scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: return TsExprApproximationResult.ResolveFailure + resolved.extractRef(scope) + } else { + resolved.asExpr(addressSort) + } + checkUndefinedOrNullPropertyRead(scope, rawArray, propertyName = "[]") + ?: return TsExprApproximationResult.ResolveFailure + val array = resolveHeapRef(scope, rawArray) ?: return TsExprApproximationResult.ResolveFailure + val storageType = scope.calcOnState { arrayStorageType(array, value.array.type) } + if (storageType !is EtsArrayType) return TsExprApproximationResult.NoApproximation + + val knownOwnSlots = scope.calcOnState { array in knownArrayPropertyPresence } + if (!knownOwnSlots) { + throw UnsupportedOperationException("Array index deletion requires known own-slot provenance") + } + + val resolvedIndex = resolve(value.index) ?: return TsExprApproximationResult.ResolveFailure + val numericIndex = extractNumericArrayIndex(scope, resolvedIndex) + val supportedKey = mkAnd(numericIndex.isNumeric, mkValidArrayIndexProperty(numericIndex.value)) + scope.fork(supportedKey, blockOnFalseState = { + terminateAsUnsupported(reason = "Deleting a named array property needs prototype semantics") + }) ?: return TsExprApproximationResult.ResolveFailure + + val index = mkFpToUint32AfterValidation(numericIndex.value, supportedKey).asExpr(sizeSort) + scope.doWithState { deleteKnownArrayIndex(array, index) } + TsExprApproximationResult.SuccessfulApproximation(mkTrue()) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt index 83e15f718f..b2744e5d02 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -23,6 +23,7 @@ import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.componentType +import org.usvm.util.knownArrayIndexPresence import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.readTypedArrayElement @@ -62,6 +63,8 @@ internal fun TsExprResolver.handleArrayAccess( val propertyName = concreteStringValue(resolvedIndex) if (propertyName != null && storageType !is EtsArrayType) { + if (!ensureSupportedArrayPrototypeAccess(array, propertyName)) return null + val field = EtsFieldSignature( name = propertyName, enclosingClass = EtsClassSignature.UNKNOWN, @@ -142,6 +145,26 @@ internal fun TsContext.readArrayElement( array: UHeapRef, index: UExpr, arrayType: EtsArrayType, +): UExpr<*> { + val present = scope.calcOnState { knownArrayIndexPresence(array, index) } + if (present?.isFalse == true) return mkUndefinedValue() + + val element = readArrayElementPayload(scope, array, index, arrayType) + if (present == null || present.isTrue) return element + + return iteWriteIntoFakeObject( + scope = scope, + condition = present, + trueBranchValue = element, + falseBranchValue = mkUndefinedValue(), + ) +} + +private fun TsContext.readArrayElementPayload( + scope: TsStepScope, + array: UHeapRef, + index: UExpr, + arrayType: EtsArrayType, ): UExpr<*> { // Determine the element sort. val sort = typeToSort(arrayType.componentType) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 9a3603f575..e7fd221fa9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -86,6 +86,7 @@ internal fun TsExprResolver.handleInstanceFieldRef( // Check for undefined or null property access. checkUndefinedOrNullPropertyRead(scope, rawInstance, propertyName = value.field.name) ?: return null val instance = resolveHeapRef(scope, rawInstance) ?: return null + if (!ensureSupportedArrayPrototypeAccess(instance, value.field.name)) return null val iteratorField = readBuiltinIteratorField(instance, value.field.name) if (iteratorField != null) return iteratorField @@ -425,6 +426,11 @@ private fun TsContext.materializeTypedStringField( internal fun TsExprResolver.handleStaticFieldRef( value: EtsStaticFieldRef, ): UExpr<*>? = with(ctx) { + if (value.field.name == "prototype") { + val constructor = classConstructorRef(value.field.enclosingClass) + if (!ensureSupportedArrayPrototypeAccess(constructor, value.field.name)) return null + } + return readStaticField(scope, value.field, hierarchy) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt index 7cc6bbd6bd..b7169cb3ab 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt @@ -68,6 +68,9 @@ internal fun TsExprResolver.tryCaptureInstanceCall( if (builtinReturn) return TsExprApproximationResult.SuccessfulApproximation(mkUndefinedValue()) if (reference != null) { + if (!ensureSupportedArrayPrototypeAccess(reference, field.field.name)) { + return TsExprApproximationResult.ResolveFailure + } val referenceGuard = if (receiver.isFakeObject()) receiver.getFakeType(scope).refTypeExpr else trueExpr val valid = mkOr(mkNot(referenceGuard), mkNotNullOrUndefined(reference)) scope.fork(valid, blockOnFalseState = { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 71338da7cd..edbb50e0fa 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -580,6 +580,12 @@ class TsExprResolver( is EtsCastExpr -> visit(EtsDeleteExpr(arg = operand.arg)) is EtsArrayAccess -> { + when (val result = tryDeleteArrayIndex(operand)) { + is TsExprApproximationResult.SuccessfulApproximation -> return result.expr + TsExprApproximationResult.ResolveFailure -> return null + TsExprApproximationResult.NoApproximation -> {} + } + val index = resolve(operand.index) ?: return null val propertyName = concreteStringValue(index) ?: throw UnsupportedOperationException("Symbolic object property keys in delete are not supported") @@ -1554,6 +1560,7 @@ class TsExprResolver( val descriptor = arrayDescriptorOf(arrayType) val address = memory.allocConcrete(descriptor) memory.initializeArrayLength(address, descriptor, sizeSort, bvSize.asExpr(sizeSort)) + knownArrayPropertyPresence += address address } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index 51da953ca7..e3455e1868 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -64,6 +64,8 @@ internal fun TsExprResolver.handleAssignToArrayIndex( val propertyName = concreteStringValue(resolvedIndex) if (propertyName != null && storageType !is EtsArrayType) { + if (!ensureSupportedArrayPrototypeAccess(array, propertyName)) return null + val field = EtsFieldSignature( name = propertyName, enclosingClass = EtsClassSignature.UNKNOWN, @@ -170,7 +172,7 @@ fun TsContext.assignToArrayIndex( scope.doWithState { val writtenIndices = initializedArrayIndices[array].orEmpty() - initializedArrayIndices += array to (writtenIndices + index) + initializedArrayIndices += array to (writtenIndices + (index to trueExpr)) } val elementSort = typeToSort(arrayType.componentType) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index c53578a18e..95a7cdb50b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -25,6 +25,7 @@ import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.resolveEtsField +import org.usvm.util.truncateKnownArrayIndices private val logger = KotlinLogging.logger {} @@ -85,6 +86,7 @@ internal fun TsExprResolver.handleAssignToInstanceField( // Check for undefined or null field access. checkUndefinedOrNullPropertyRead(scope, rawInstance, field.name) ?: return null val instance = resolveHeapRef(scope, rawInstance) ?: return null + if (!ensureSupportedArrayPrototypeAccess(instance, field.name)) return null val arrayType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } as? EtsArrayType if (field.name == "length" && arrayType != null) { @@ -165,6 +167,7 @@ private fun TsContext.assignToArrayLength( return scope.doWithState { memory.write(lengthLValue, length, guard = trueExpr) + truncateKnownArrayIndices(array, length) } } @@ -285,6 +288,11 @@ internal fun TsExprResolver.handleAssignToStaticField( lhv: EtsStaticFieldRef, expr: UExpr<*>, ): Unit? = with(ctx) { + if (lhv.field.name == "prototype") { + val constructor = classConstructorRef(lhv.field.enclosingClass) + if (!ensureSupportedArrayPrototypeAccess(constructor, lhv.field.name)) return null + } + assignToStaticField(scope, lhv.field, expr) } 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 b5dc837a0b..e6c717f6a2 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 @@ -11,6 +11,7 @@ import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType import org.usvm.PathNode +import org.usvm.UBoolExpr import org.usvm.UCallStack import org.usvm.UConcreteHeapRef import org.usvm.UExpr @@ -79,8 +80,9 @@ class TsState( internal var arrayIterators: Map = emptyMap(), internal var stringIterators: Map = emptyMap(), internal var iteratorResults: Map = emptyMap(), + internal var knownArrayPropertyPresence: Set = emptySet(), internal var unsupportedIteratorArrays: Set = emptySet(), - internal var initializedArrayIndices: Map>> = emptyMap(), + internal var initializedArrayIndices: Map, UBoolExpr>> = emptyMap(), var boundThis: UPersistentHashMap = persistentHashMapOf(), var dfltObject: UPersistentHashMap = persistentHashMapOf(), @@ -355,6 +357,7 @@ class TsState( stringIterators = stringIterators, initializedArrayIndices = initializedArrayIndices, unsupportedIteratorArrays = unsupportedIteratorArrays, + knownArrayPropertyPresence = knownArrayPropertyPresence, boundThis = boundThis, dfltObject = dfltObject, dfltObjectFieldSorts = dfltObjectFieldSorts, diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt new file mode 100644 index 0000000000..edf9fe061c --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt @@ -0,0 +1,46 @@ +package org.usvm.util + +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.machine.TsSizeSort +import org.usvm.machine.state.TsState + +/** Presence of own numeric slots in arrays allocated by a supported NewArray expression. */ +internal fun TsState.knownArrayIndexPresence(array: UHeapRef, index: UExpr): UBoolExpr? { + if (array !in knownArrayPropertyPresence) return null + + return writtenArrayIndexPresence(array, index) +} + +internal fun TsState.writtenArrayIndexPresence(array: UHeapRef, index: UExpr): UBoolExpr = with(ctx) { + val initialized = initializedArrayIndices[array].orEmpty() + mkOr(initialized.map { (writtenIndex, present) -> mkAnd(mkEq(index, writtenIndex), present) }) +} + +internal fun TsState.deleteKnownArrayIndex(array: UHeapRef, index: UExpr) = with(ctx) { + val initialized = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to initialized.mapValues { (writtenIndex, present) -> + mkAnd(present, mkNot(mkEq(index, writtenIndex))) + } +} + +internal fun TsState.truncateKnownArrayIndices(array: UHeapRef, length: UExpr) = with(ctx) { + val initialized = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to initialized.mapValues { (index, present) -> + val inRange = mkAnd(mkBvSignedGreaterOrEqualExpr(index, mkBv(0)), mkBvSignedLessExpr(index, length)) + mkAnd(present, inRange) + } +} + +internal fun TsState.moveInitializedArrayIndices( + array: UHeapRef, + newIndex: (UExpr) -> UExpr, +) = with(ctx) { + val moved = linkedMapOf, UBoolExpr>() + for ((index, present) in initializedArrayIndices[array].orEmpty()) { + val target = newIndex(index) + moved[target] = mkOr(moved[target] ?: falseExpr, present) + } + initializedArrayIndices += array to moved +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt index da008bc5dd..9b577c3f4f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt @@ -55,11 +55,8 @@ class ArrayIteratorSourceTest : TsMethodTestRunner() { } @Test - fun `custom iterables and sparse arrays retain explicit limitations`() { - val methods = listOf( - "stringNamedLookalike", "sparseArray", "deletedSlot", - "reversedSparseArray", "unshiftedSparseArray", "shiftedSparseArray", - ) + fun `custom iterables retain explicit limitations`() { + val methods = listOf("stringNamedLookalike") for (methodName in methods) { val method = getMethod(methodName = methodName, className = "ArrayIteratorSource") val reasons = mutableListOf() diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt new file mode 100644 index 0000000000..281f854e80 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SparseArrayIteratorSourceTest.kt @@ -0,0 +1,175 @@ +package org.usvm.machine.expr + +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.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 java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class SparseArrayIteratorSourceTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/SparseArrayIteratorSource.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + override val tsOptions = TsOptions(maxArraySize = 6) + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + val limitations = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions, observer = observer).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, method.name) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${method.name}: ${outcome.unsupportedPaths}") + assertTrue(limitations.isEmpty(), "${method.name}: $limitations") + outcome.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `known own holes yield undefined through direct reads spread destructuring and live iteration`() { + for (name in supportedMethods) { + discoverProperties( + method = method(name), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `symbolic deletion preserves conditional slot presence`() { + discoverProperties( + method = method("symbolicDelete"), + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + { _, result -> result.number == 2.0 }, + invariants = arrayOf({ index, result -> + val expected = when (index.number) { + 0.0 -> 1.0 + 1.0 -> 2.0 + else -> 0.0 + } + result.number == expected + }), + ) + discoverProperties( + method = method("symbolicWriteThenDelete"), + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ index, result -> + val expected = if (index.number == 0.0 || index.number == 1.0) 1.0 else 0.0 + result.number == expected + }), + ) + } + + @Test + fun `unmodeled prototype access and mutation cannot justify missing own slots`() { + val unsupportedMethods = listOf( + "mutateArrayPrototype", "mutateObjectPrototype", "mutatePrototypeThroughBracketAlias", "setArrayPrototype", + "setArrayPrototypeThroughAliases", "getAndMutateArrayPrototype", "setLegacyPrototype", + "getAndMutateObjectPrototype", "freezeThenDelete", "defineIndexedProperty", + ) + val machineOptions = options.copy(throwExceptionOnStepFailure = false) + + for (name in unsupportedMethods) { + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method(name))) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, name) + assertTrue(outcome.states.isEmpty(), name) + assertTrue(outcome.unsupportedPaths.isNotEmpty(), "$name: $outcome") + } + } + } + + @Test + fun `unknown array storage retains explicit iterator limitations`() { + for (name in listOf("unknownCopiedStorage", "unsupportedFillStorage")) { + val limitations = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event.reason + } + } + + TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method(name))) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, name) + assertTrue(outcome.states.isEmpty(), name) + assertEquals(listOf(TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED), limitations, name) + } + } + } + + @Test + fun `supported sparse array witnesses replay in native JavaScript`() { + val script = buildString { + appendLine(source.readText()) + for (name in supportedMethods) { + appendLine("if (SparseArrayIteratorSource.$name() !== 1) throw Error('$name');") + } + for (name in listOf("symbolicDelete", "symbolicWriteThenDelete")) { + val tests = runner(method(name), options) + assertTrue(tests.isNotEmpty(), name) + for (test in tests) { + val input = assertIs(test.before.parameters.single()).number + val expected = assertIs(test.returnValue).number + appendLine("if (SparseArrayIteratorSource.$name($input) !== $expected) throw Error('$name');") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "sparse-array-iterator", + timeoutMessage = "Sparse array iterator replay timed out", + ) + } + + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "SparseArrayIteratorSource") + + private val supportedMethods = listOf( + "literalHoles", "newArrayHoles", "deletedSlot", "rewriteDeletedSlot", "movesPreserveHoles", + "shiftMissingFirstSlot", "truncateAndMoveHoles", "destructureHoles", "forOfHoles", "liveDelete", + "sourceObjectLookalike", + ) +} diff --git a/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts b/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts new file mode 100644 index 0000000000..f9d5920b37 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SparseArrayIteratorSource.ts @@ -0,0 +1,183 @@ +export class SparseArrayIteratorSource { + static literalHoles(): number { + const values = [7, , 11]; + const copy = [...values]; + return values[1] === undefined && copy.length === 3 && copy[0] === 7 && + copy[1] === undefined && copy[2] === 11 ? 1 : 0; + } + + static newArrayHoles(): number { + const values = new Array(3); + values[1] = 7; + const copy = [...values]; + return copy.length === 3 && copy[0] === undefined && copy[1] === 7 && copy[2] === undefined ? 1 : 0; + } + + static deletedSlot(): number { + const values = [7, 11]; + const removed = delete values[1]; + const copy = [...values]; + return removed && values[1] === undefined && copy.length === 2 && copy[0] === 7 && copy[1] === undefined ? 1 : 0; + } + + static rewriteDeletedSlot(): number { + const values = [7, 11]; + const alias: any[] = values; + delete values[0]; + alias[0] = true; + const copy = [...alias]; + return copy.length === 2 && copy[0] === true && copy[1] === 11 ? 1 : 0; + } + + static movesPreserveHoles(): number { + const values = [1, , 3]; + values.reverse(); + values.unshift(7); + const removed = values.shift(); + const copy = [...values]; + return removed === 7 && copy.length === 3 && copy[0] === 3 && copy[1] === undefined && copy[2] === 1 ? 1 : 0; + } + + static shiftMissingFirstSlot(): number { + const values = [, 3]; + const removed = values.shift(); + const copy = [...values]; + return removed === undefined && copy.length === 1 && copy[0] === 3 ? 1 : 0; + } + + static truncateAndMoveHoles(): number { + const values = [7, , 11]; + values.length = 2; + values.reverse(); + values.unshift(13); + const last = values.pop(); + const copy = [...values]; + return last === 7 && copy.length === 2 && copy[0] === 13 && copy[1] === undefined ? 1 : 0; + } + + static destructureHoles(): number { + const [first = 7, second, ...rest] = [, 11, ,]; + return first === 7 && second === 11 && rest.length === 1 && rest[0] === undefined ? 1 : 0; + } + + static forOfHoles(): number { + let count = 0; + for (const value of [, ,]) { + if (value !== undefined) return 0; + count++; + } + return count === 2 ? 1 : 0; + } + + static liveDelete(): number { + const values = [7, 11]; + let count = 0; + let holes = 0; + for (const value of values) { + if (value === undefined) holes++; + count++; + delete values[1]; + } + return count === 2 && holes === 1 ? 1 : 0; + } + + static sourceObjectLookalike(): number { + const Object = { setPrototypeOf(values: any[], prototype: any) { return values; } }; + const values = [, 7]; + Object.setPrototypeOf(values, { 0: 9 }); + const copy = [...values]; + return copy[0] === undefined && copy[1] === 7 ? 1 : 0; + } + + static symbolicDelete(index: number): number { + if (index !== 0 && index !== 1) return 0; + const values = [7, 11]; + delete values[index]; + const copy = [...values]; + if (index === 0) return copy[0] === undefined && copy[1] === 11 ? 1 : 3; + return copy[0] === 7 && copy[1] === undefined ? 2 : 3; + } + + static symbolicWriteThenDelete(index: number): number { + if (index !== 0 && index !== 1) return 0; + const values = new Array(2); + values[index] = 7; + delete values[0]; + const copy = [...values]; + return copy[0] === undefined && (index === 0 ? copy[1] === undefined : copy[1] === 7) ? 1 : 2; + } + + static mutateArrayPrototype(): any { + Array.prototype[0] = 7; + return [...[,]][0]; + } + + static mutateObjectPrototype(): any { + Object.prototype[0] = 7; + return [...[,]][0]; + } + + static mutatePrototypeThroughBracketAlias(): any { + const NativeObject: any = Object; + const name = "prototype"; + NativeObject[name][0] = 7; + return [...[,]][0]; + } + + static setArrayPrototype(): any { + const values = [,]; + Object.setPrototypeOf(values, { 0: 7 }); + return [...values][0]; + } + + static setArrayPrototypeThroughAliases(): any { + const NativeObject = Object; + const values: any = [,]; + const alias: any = values; + NativeObject.setPrototypeOf(alias, { 0: 7 }); + return [...values][0]; + } + + static getAndMutateArrayPrototype(): any { + const values = [,]; + const prototype = Object.getPrototypeOf(values); + prototype[0] = 7; + return [...values][0]; + } + + static getAndMutateObjectPrototype(): any { + const prototype = Object.getPrototypeOf({}); + prototype[0] = 7; + return [...[,]][0]; + } + + static setLegacyPrototype(): any { + const values: any = [,]; + values.__proto__ = { 0: 7 }; + return [...values][0]; + } + + static freezeThenDelete(): any { + const values = [7]; + Object.freeze(values); + delete values[0]; + return [...values][0]; + } + + static defineIndexedProperty(): any { + const values: any = [,]; + Object.defineProperty(values, "0", { value: 7 }); + return [...values][0]; + } + + static unknownCopiedStorage(): number { + const values = [7, 11].slice(); + return [...values].length; + } + + static unsupportedFillStorage(): number { + const values = new Array(2); + values.fill(7); + return [...values].length; + } +} From 884f5d414398989e765568c25393929ad872b4f9 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:43:50 +0300 Subject: [PATCH 12/23] Reverse boxed array metadata through its private lvalues --- .../org/usvm/machine/expr/CallApproximations.kt | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) 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 5808744f44..728215b558 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 @@ -38,7 +38,6 @@ import org.usvm.machine.state.lastStmt import org.usvm.machine.state.newStmt import org.usvm.machine.types.TsUnresolvedArrayKind import org.usvm.sizeSort -import org.usvm.util.TsTypedArrayStorage import org.usvm.util.arrayStorageType import org.usvm.util.componentType import org.usvm.util.copyArrayElements @@ -49,6 +48,8 @@ import org.usvm.util.mkArrayLengthLValue import org.usvm.util.moveInitializedArrayIndices import org.usvm.util.resolveEtsMethods import org.usvm.util.truncateKnownArrayIndices +import org.usvm.util.typedArrayBoxedLValue +import org.usvm.util.typedArrayOverrideLValue private val logger = KotlinLogging.logger {} @@ -1237,14 +1238,14 @@ private fun TsExprResolver.handleArrayReverse( } } else { initializeTypedArrayOverrides(array) - val hasBoxedValues = reversedIndices.asSequence().map { index -> - memory.readArrayIndex(array, index, TsTypedArrayStorage.HAS_BOXED_VALUE, boolSort) - } - val boxedValues = reversedIndices.asSequence().map { index -> - memory.readArrayIndex(array, index, TsTypedArrayStorage.BOXED_VALUE, addressSort) + for ((destination, source) in reversedIndices.withIndex()) { + val target = destination.toBv() + val hasBoxedValue = memory.read(typedArrayOverrideLValue(array, source)) + val boxedValue = memory.read(typedArrayBoxedLValue(array, source)) + + memory.write(typedArrayOverrideLValue(reversedArray, target), hasBoxedValue, guard = trueExpr) + memory.write(typedArrayBoxedLValue(reversedArray, target), boxedValue, guard = trueExpr) } - memory.initializeArray(reversedArray, TsTypedArrayStorage.HAS_BOXED_VALUE, boolSort, sizeSort, hasBoxedValues) - memory.initializeArray(reversedArray, TsTypedArrayStorage.BOXED_VALUE, addressSort, sizeSort, boxedValues) } copyArrayElements( From 95c3599e4887ba2f0d255c303a9204e15bc5db02 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:46:06 +0300 Subject: [PATCH 13/23] Use the allocated-reference contract when checking dense arrays --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt index 536facab0d..79e370b96e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -114,8 +114,7 @@ private fun TsExprResolver.advanceArrayIterator( val initialized = scope.calcOnState { // Inputs are dense; known allocations distinguish written own slots from holes. val array = iterator.array - val denseInput = !isAllocatedConcreteHeapRef(array) || - (array is UConcreteHeapRef && denseInputArrays[array] != null) + val denseInput = !isAllocatedConcreteHeapRef(array) || denseInputArrays[array] != null val knownOwnSlots = array in knownArrayPropertyPresence if (denseInput || knownOwnSlots) { trueExpr From e35ff7df2d30f5b02e4d4e7cc32a015e3debdbf7 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:53:48 +0300 Subject: [PATCH 14/23] Fork native string iterator steps and retain unsupported property writes --- .../org/usvm/machine/expr/StringIterator.kt | 23 ++++++++++++------- .../org/usvm/machine/expr/WriteArray.kt | 7 +++++- 2 files changed, 21 insertions(+), 9 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt index 859c8467d0..0e4c5cfbad 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt @@ -64,12 +64,16 @@ internal fun TsExprResolver.tryCreateStringIterator( internal fun TsExprResolver.advanceStringIterator( reference: UConcreteHeapRef, iterator: TsStringIterator, -): UHeapRef = with(ctx) { +): UHeapRef? = with(ctx) { val length = scope.calcOnState { stringLength(iterator.string) } val done = mkOr(iterator.exhausted, mkBvSignedGreaterOrEqualExpr(iterator.index, length)) + val isDone = scope.calcOnState { models.first().eval(done).isTrue } + val exhaustionBranch = if (isDone) done else mkNot(done) + scope.fork(exhaustionBranch) ?: return null + val width: UExpr val value: UHeapRef - if (done.isTrue) { + if (isDone) { width = mkBv(0) value = mkUndefinedValue() } else { @@ -82,21 +86,24 @@ internal fun TsExprResolver.advanceStringIterator( val firstIsHighSurrogate = mkEq(mkBvAndExpr(first, mkBv(0xfc00, bv16Sort)), mkBv(0xd800, bv16Sort)) val secondIsLowSurrogate = mkEq(mkBvAndExpr(second, mkBv(0xfc00, bv16Sort)), mkBv(0xdc00, bv16Sort)) val pair = mkAnd(firstIsHighSurrogate, mkBvSignedLessExpr(nextIndex, length), secondIsLowSurrogate) - width = mkIte(pair, mkBv(2), mkBv(1)) + val isPair = scope.calcOnState { models.first().eval(pair).isTrue } + val widthBranch = if (isPair) pair else mkNot(pair) + scope.fork(widthBranch) ?: return null + + width = if (isPair) mkBv(2) else mkBv(1) - val character = scope.calcOnState { + value = scope.calcOnState { allocateBoundedString(length = width, codeUnits = listOf(first, second)) } - value = mkIte(done, mkUndefinedValue(), character) } scope.calcOnState { stringIterators += reference to iterator.copy( - index = mkIte(done, iterator.index, mkBvAddExpr(iterator.index, width)), - exhausted = done, + index = mkBvAddExpr(iterator.index, width), + exhausted = mkBool(isDone), ) val result = memory.allocConcrete(iteratorResultType) - iteratorResults += result to TsIteratorResult(done = done, value = value) + iteratorResults += result to TsIteratorResult(done = mkBool(isDone), value = value) result } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index e3455e1868..3bbe16de40 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -98,7 +98,12 @@ internal fun TsExprResolver.handleAssignToArrayIndex( detail = "property key is not a supported numeric array index: $resolvedIndex", ) } - scope.assert(indexIsSupported) ?: return null + scope.fork(indexIsSupported, blockOnFalseState = { + terminateAsUnsupported( + reason = "${TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE}: " + + "Property key is not a supported numeric array index: $resolvedIndex", + ) + }) ?: return null val bvIndex = mkFpToUint32AfterValidation(index.value, indexIsSupported).asExpr(sizeSort) extendArrayForIndexAppend(array = array, index = bvIndex, arrayType = storageType) ?: return null From e5d164208555f41b6e7644d511dfe4d28262b8a7 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:09:10 +0300 Subject: [PATCH 15/23] Retain explicit unsupported outcomes for ambient Symbol values --- .../org/usvm/machine/expr/ArrayIterator.kt | 7 ++++-- .../usvm/machine/expr/CallApproximations.kt | 5 ++-- .../org/usvm/machine/expr/TsExprResolver.kt | 4 +++ ...{StringIterator.kt => TsStringIterator.kt} | 14 +++++++++-- .../machine/expr/ArrayIteratorSourceTest.kt | 19 +++++++++----- .../expr/SourceSdkConstructorShadowTest.kt | 4 ++- .../resources/models/ArrayIteratorSource.ts | 25 +++++++++++++++++++ .../models/SourceSdkConstructorShadow.ts | 9 +++++++ 8 files changed, 74 insertions(+), 13 deletions(-) rename usvm-ts/src/main/kotlin/org/usvm/machine/expr/{StringIterator.kt => TsStringIterator.kt} (90%) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt index 79e370b96e..4b51d83fb7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -27,6 +27,7 @@ data class TsArrayIterator( val exhausted: UBoolExpr, ) +/** The result object's fields are kept separate from the iterator's mutable cursor. */ data class TsIteratorResult(val done: UBoolExpr, val value: UExpr<*>) private val iteratorType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinArrayIterator")) @@ -102,7 +103,8 @@ private fun TsExprResolver.advanceArrayIterator( mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)), ) - if (scope.checkSat(mkAnd(mkNot(iterator.exhausted), mkNot(withinCapacity))) != null) { + val activeBeyondCapacity = mkAnd(mkNot(iterator.exhausted), mkNot(withinCapacity)) + if (scope.checkSat(activeBeyondCapacity) != null) { reportRuntimeFeatureLimitation( reason = TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED, detail = "The array iterator exceeds the configured length bound ${options.maxArraySize}", @@ -144,8 +146,9 @@ private fun TsExprResolver.advanceArrayIterator( } scope.calcOnState { + val nextIndex = mkBvAddExpr(iterator.index, mkBv(1)) arrayIterators += reference to iterator.copy( - index = mkIte(done, iterator.index, mkBvAddExpr(iterator.index, mkBv(1))), + index = mkIte(done, iterator.index, nextIndex), exhausted = done, ) val result = memory.allocConcrete(iteratorResultType) 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 728215b558..7e93892ed1 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 @@ -590,7 +590,7 @@ private fun TsExprResolver.removeArrayElement( if (first) { copyArrayElements(array, array, arrayType, fromSrc = mkBv(1), fromDst = mkBv(0), length = newLength) - moveInitializedArrayIndices(array) { index -> mkBvSubExpr(index, mkBv(1)) } + moveInitializedArrayIndices(array) { sourceIndex -> mkBvSubExpr(sourceIndex, mkBv(1)) } } truncateKnownArrayIndices(array, newLength) memory.write(lengthLValue, newLength, guard = trueExpr) @@ -1214,7 +1214,8 @@ private fun TsExprResolver.handleArrayReverse( mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)), ) - if (scope.checkSat(mkNot(withinCapacity)) != null) { + val capacityExceeded = mkNot(withinCapacity) + if (scope.checkSat(capacityExceeded) != null) { reportRuntimeFeatureLimitation( reason = TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, detail = "Array.reverse exceeds the configured length bound ${options.maxArraySize}", diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index edbb50e0fa..fa6523a116 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -1749,6 +1749,10 @@ class TsSimpleValueResolver( val hasSourceBinding = isParameter || isGlobal || isImported if (hasSourceBinding) return resolveLocal(local) + if (local.name == "Symbol") { + throw UnsupportedOperationException("Builtin Symbol values are not modeled") + } + val sdkConstructor = ctx.scene.sdkConstructorForGlobal(local) if (sdkConstructor != null) return ctx.classConstructorRef(sdkConstructor.signature) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt similarity index 90% rename from usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt rename to usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt index 0e4c5cfbad..829bec3a63 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt @@ -28,6 +28,10 @@ data class TsStringIterator( private val stringIteratorType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinStringIterator")) +private const val SURROGATE_KIND_MASK = 0xfc00 +private const val HIGH_SURROGATE_KIND = 0xd800 +private const val LOW_SURROGATE_KIND = 0xdc00 + internal fun TsExprResolver.tryCreateStringIterator( stmt: TsVirtualMethodCallStmt, ): TsExprApproximationResult = with(ctx) { @@ -83,8 +87,14 @@ internal fun TsExprResolver.advanceStringIterator( memory.read(mkStringBackingElementLValue(characters, iterator.index)) to memory.read(mkStringBackingElementLValue(characters, nextIndex)) } - val firstIsHighSurrogate = mkEq(mkBvAndExpr(first, mkBv(0xfc00, bv16Sort)), mkBv(0xd800, bv16Sort)) - val secondIsLowSurrogate = mkEq(mkBvAndExpr(second, mkBv(0xfc00, bv16Sort)), mkBv(0xdc00, bv16Sort)) + val firstIsHighSurrogate = mkEq( + mkBvAndExpr(first, mkBv(SURROGATE_KIND_MASK, bv16Sort)), + mkBv(HIGH_SURROGATE_KIND, bv16Sort), + ) + val secondIsLowSurrogate = mkEq( + mkBvAndExpr(second, mkBv(SURROGATE_KIND_MASK, bv16Sort)), + mkBv(LOW_SURROGATE_KIND, bv16Sort), + ) val pair = mkAnd(firstIsHighSurrogate, mkBvSignedLessExpr(nextIndex, length), secondIsLowSurrogate) val isPair = scope.calcOnState { models.first().eval(pair).isTrue } val widthBranch = if (isPair) pair else mkNot(pair) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt index 9b577c3f4f..6ed0133fa3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt @@ -33,6 +33,7 @@ class ArrayIteratorSourceTest : TsMethodTestRunner() { "literalSpread", "destructure", "preserveKindsAndAliases", "evaluationOrder", "liveLength", "shortenedLength", "exhaustedDestructuring", "reversedMixedAlias", "unshiftedMixedAlias", "shiftedMixedAlias", + "localSymbolShadow", ) for (methodName in methods) { @@ -78,14 +79,20 @@ class ArrayIteratorSourceTest : TsMethodTestRunner() { @Test fun `own symbol overrides cannot silently use the native array iterator`() { - val method = getMethod(methodName = "customSymbolOverride", className = "ArrayIteratorSource") + val methodNames = listOf( + "customSymbolOverride", "builtinSymbolKey", "aliasedSymbolOverride", "bracketSymbolOverride", + ) + + for (methodName in methodNames) { + val method = getMethod(methodName = methodName, className = "ArrayIteratorSource") - TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> - val outcome = machine.analyzeWithOutcome(methods = listOf(method)) + TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method)) - assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) - assertTrue(outcome.states.isEmpty()) - assertTrue(outcome.unsupportedPaths.isNotEmpty(), outcome.toString()) + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), methodName) + assertTrue(outcome.unsupportedPaths.isNotEmpty(), "$methodName: $outcome") + } } } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt index 1bc352a8a6..c22b62787b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt @@ -47,5 +47,7 @@ class SourceSdkConstructorShadowTest : TsMethodTestRunner() { ) } - private val methods = listOf("objectMethodKeepsSourceImplementation", "arrayMethodKeepsSourceImplementation") + private val methods = listOf( + "objectMethodKeepsSourceImplementation", "arrayMethodKeepsSourceImplementation", "symbolKeyKeepsSourceImplementation", + ) } diff --git a/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts b/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts index e7b0ff1d27..53db5c433b 100644 --- a/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts +++ b/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts @@ -133,4 +133,29 @@ export class ArrayIteratorSource { values[Symbol.iterator] = () => ({ next: () => ({ done: true }) }); return [...values].length; } + + static builtinSymbolKey(): any { + return Symbol.iterator; + } + + static aliasedSymbolOverride(): number { + const symbols = Symbol; + const values: any = [1, 2]; + values[symbols.iterator] = () => ({ next: () => ({ done: true }) }); + return [...values].length; + } + + static bracketSymbolOverride(): number { + const values: any = [1, 2]; + values[Symbol["iterator"]] = () => ({ next: () => ({ done: true }) }); + return [...values].length; + } + + static localSymbolShadow(): number { + const Symbol = { iterator: 0 }; + const values = [1, 2]; + values[Symbol.iterator] = 7; + const copy = [...values]; + return copy[0] === 7 && copy[1] === 2 ? 1 : 0; + } } diff --git a/usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts b/usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts index b56e79ab22..b9147e4cb7 100644 --- a/usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts +++ b/usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts @@ -4,6 +4,9 @@ const Object: typeof globalThis.Object = { setPrototypeOf(target: any, _prototyp // @ts-expect-error This source binding implements only the method used below. const Array: typeof globalThis.Array = { isArray: (_value: unknown): boolean => false }; +// @ts-expect-error This source binding deliberately uses a numeric property key. +const Symbol: typeof globalThis.Symbol = { iterator: 0 }; + export class SourceSdkConstructorShadow { static objectMethodKeepsSourceImplementation(): number { const values = [7]; @@ -14,4 +17,10 @@ export class SourceSdkConstructorShadow { static arrayMethodKeepsSourceImplementation(): number { return Array.isArray([]) ? 0 : 1; } + + static symbolKeyKeepsSourceImplementation(): number { + const values = [7]; + values[Symbol.iterator] = 11; + return values[0] === 11 ? 1 : 0; + } } From 29405a6717644dd192666da4ffa8a17c77f86f9d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:10:34 +0300 Subject: [PATCH 16/23] Ignore Array.shift arguments after evaluating their side effects --- .../intrinsic/TsArrayShiftIntrinsicModel.kt | 4 -- .../usvm/machine/expr/CallApproximations.kt | 4 -- .../call/ArrayShiftArgumentsSourceTest.kt | 53 +++++++++++++++++++ .../call/TsArrayShiftIntrinsicModelTest.kt | 25 +++++---- .../resources/models/ArrayShiftIntrinsic.ts | 18 +++++-- 5 files changed, 84 insertions(+), 20 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/ArrayShiftArgumentsSourceTest.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt index 47dce2f746..4d266e101f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt @@ -75,10 +75,6 @@ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { } private fun resolveInput(state: TsState, call: TsUnknownCall): ArrayShiftInput? = with(state.ctx) { - if (call.arguments.isNotEmpty()) { - return@with null - } - val receiver = call.receiver ?: return@with null val receiverValue = receiver.resolved ?: return@with null if (receiverValue.sort != addressSort) { 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 7e93892ed1..5e60d75e33 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 @@ -756,10 +756,6 @@ private fun TsExprResolver.handleArrayShift( arrayType: EtsArrayType, array: UHeapRef, ): UExpr<*>? = with(ctx) { - check(stmt.args.isEmpty()) { - "Array.shift() should have no arguments, but got ${stmt.args.size}" - } - removeArrayElement(stmt, array, arrayType, first = true) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/ArrayShiftArgumentsSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/ArrayShiftArgumentsSourceTest.kt new file mode 100644 index 0000000000..6a4acc6571 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/ArrayShiftArgumentsSourceTest.kt @@ -0,0 +1,53 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.io.TempDir +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test + +class ArrayShiftArgumentsSourceTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/ArrayShiftIntrinsic.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + + @Test + fun `ignored shift arguments execute before observing the receiver`() { + for (methodName in sideEffectMethods) { + discoverProperties( + method = getMethod(methodName = methodName, className = "ArrayShiftIntrinsic"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `ignored shift arguments preserve native JavaScript side effects`() { + val script = buildString { + appendLine(source.readText()) + appendLine("const subject = new ArrayShiftIntrinsic();") + appendLine("if (subject.shiftWithArguments() !== 48) throw Error('shiftWithArguments');") + for (methodName in sideEffectMethods) { + appendLine("if (subject.$methodName() !== 1) throw Error('$methodName');") + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "array-shift-ignored-arguments", + timeoutMessage = "Array.shift argument replay timed out", + ) + } + + private val sideEffectMethods = listOf("shiftWithArgumentSideEffects", "shiftAfterArgumentEmptiesReceiver") +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt index 64a7ef403c..b03c341584 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt @@ -249,8 +249,22 @@ class TsArrayShiftIntrinsicModelTest { } @Test - fun `array shift with arguments uses residual fallback`() { - assertUsesResidualFallback(methodName = "shiftWithArguments") + fun `array shift ignores arguments through the registered model`() { + val result = analyze(methodName = "shiftWithArguments") + + assertEquals(48.0, assertIs(result.values.single()).number) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `compatibility dispatcher also ignores shift arguments`() { + val result = analyze( + methodName = "shiftWithArguments", + dispatcher = TsCompatibilityUnknownCallDispatcher, + ) + + assertEquals(48.0, assertIs(result.values.single()).number) + assertTrue(result.events.isEmpty()) } @Test @@ -330,13 +344,6 @@ class TsArrayShiftIntrinsicModelTest { } } - private fun assertUsesResidualFallback(methodName: String) { - val result = analyze(methodName) - - assertTrue(result.values.isEmpty()) - assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.single().outcome) - } - private fun makeFakeReceiver(state: TsState): UConcreteHeapRef { val result = assertIs(state.methodResult).value val fakeReceiver = assertIs(result) diff --git a/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts index 146989eed6..f9c86f480e 100644 --- a/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts +++ b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts @@ -67,9 +67,21 @@ export class ArrayShiftIntrinsic { } shiftWithArguments(): number { - const values = [1]; - values.shift(0); - return 48; + const values = [1, 2]; + const first = values.shift(99); + return first === 1 && values[0] === 2 && values.length === 1 ? 48 : 0; + } + + shiftWithArgumentSideEffects(): number { + const values = [10, 20, 30]; + const first = values.shift(values.pop(), values[0] = 7); + return first === 7 && values[0] === 20 && values.length === 1 ? 1 : 0; + } + + shiftAfterArgumentEmptiesReceiver(): number { + const values = [10]; + const first = values.shift(values.pop()); + return first === undefined && values.length === 0 ? 1 : 0; } readBeforeShift(values: any[]): number { From e72deba8abbead2d1e937a758cb899839b127e54 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:17:20 +0300 Subject: [PATCH 17/23] Simplify nested iterator and reverse constraints --- .../kotlin/org/usvm/machine/expr/ArrayIterator.kt | 7 +++---- .../org/usvm/machine/expr/CallApproximations.kt | 7 +++---- .../org/usvm/machine/expr/TsStringIterator.kt | 13 +++++-------- 3 files changed, 11 insertions(+), 16 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt index 4b51d83fb7..7eba4f05e6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -99,10 +99,9 @@ private fun TsExprResolver.advanceArrayIterator( } val length = scope.calcOnState { memory.read(mkArrayLengthLValue(iterator.array, iterator.arrayType)) } - val withinCapacity = mkAnd( - mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), - mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)), - ) + val nonNegativeLength = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val withinMaximumLength = mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) + val withinCapacity = mkAnd(nonNegativeLength, withinMaximumLength) val activeBeyondCapacity = mkAnd(mkNot(iterator.exhausted), mkNot(withinCapacity)) if (scope.checkSat(activeBeyondCapacity) != null) { reportRuntimeFeatureLimitation( 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 5e60d75e33..3269143d94 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 @@ -1206,10 +1206,9 @@ private fun TsExprResolver.handleArrayReverse( val lengthLValue = mkArrayLengthLValue(array, arrayType) val length = memory.read(lengthLValue) - val withinCapacity = mkAnd( - mkBvSignedGreaterOrEqualExpr(length, mkBv(0)), - mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)), - ) + val nonNegativeLength = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val withinMaximumLength = mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) + val withinCapacity = mkAnd(nonNegativeLength, withinMaximumLength) val capacityExceeded = mkNot(withinCapacity) if (scope.checkSat(capacityExceeded) != null) { reportRuntimeFeatureLimitation( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt index 829bec3a63..daa3dbc221 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt @@ -87,14 +87,11 @@ internal fun TsExprResolver.advanceStringIterator( memory.read(mkStringBackingElementLValue(characters, iterator.index)) to memory.read(mkStringBackingElementLValue(characters, nextIndex)) } - val firstIsHighSurrogate = mkEq( - mkBvAndExpr(first, mkBv(SURROGATE_KIND_MASK, bv16Sort)), - mkBv(HIGH_SURROGATE_KIND, bv16Sort), - ) - val secondIsLowSurrogate = mkEq( - mkBvAndExpr(second, mkBv(SURROGATE_KIND_MASK, bv16Sort)), - mkBv(LOW_SURROGATE_KIND, bv16Sort), - ) + val surrogateKindMask = mkBv(SURROGATE_KIND_MASK, bv16Sort) + val firstKind = mkBvAndExpr(first, surrogateKindMask) + val secondKind = mkBvAndExpr(second, surrogateKindMask) + val firstIsHighSurrogate = mkEq(firstKind, mkBv(HIGH_SURROGATE_KIND, bv16Sort)) + val secondIsLowSurrogate = mkEq(secondKind, mkBv(LOW_SURROGATE_KIND, bv16Sort)) val pair = mkAnd(firstIsHighSurrogate, mkBvSignedLessExpr(nextIndex, length), secondIsLowSurrogate) val isPair = scope.calcOnState { models.first().eval(pair).isTrue } val widthBranch = if (isPair) pair else mkNot(pair) From e224c68184a5e81ba499a6352f0813d13c189628 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:20:00 +0300 Subject: [PATCH 18/23] Wrap iterator source regression case lists --- .../org/usvm/machine/expr/ArrayIteratorSourceTest.kt | 5 ++++- .../usvm/machine/expr/SourceSdkConstructorShadowTest.kt | 4 +++- .../org/usvm/machine/expr/StringIteratorSourceTest.kt | 8 ++++++-- 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt index 6ed0133fa3..59d3b04517 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt @@ -80,7 +80,10 @@ class ArrayIteratorSourceTest : TsMethodTestRunner() { @Test fun `own symbol overrides cannot silently use the native array iterator`() { val methodNames = listOf( - "customSymbolOverride", "builtinSymbolKey", "aliasedSymbolOverride", "bracketSymbolOverride", + "customSymbolOverride", + "builtinSymbolKey", + "aliasedSymbolOverride", + "bracketSymbolOverride", ) for (methodName in methodNames) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt index c22b62787b..b453b46ab4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt @@ -48,6 +48,8 @@ class SourceSdkConstructorShadowTest : TsMethodTestRunner() { } private val methods = listOf( - "objectMethodKeepsSourceImplementation", "arrayMethodKeepsSourceImplementation", "symbolKeyKeepsSourceImplementation", + "objectMethodKeepsSourceImplementation", + "arrayMethodKeepsSourceImplementation", + "symbolKeyKeepsSourceImplementation", ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt index ef1829245f..f3840d81f0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt @@ -147,7 +147,11 @@ class StringIteratorSourceTest : TsMethodTestRunner() { private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "StringIteratorSource") private val literalMethods = listOf( - "mixedUtf16", "reversedSurrogates", "destructuring", - "exhaustedDestructuring", "reboundSource", "shadowedSymbol", + "mixedUtf16", + "reversedSurrogates", + "destructuring", + "exhaustedDestructuring", + "reboundSource", + "shadowedSymbol", ) } From d88b8706921a2d0787894851824bb2ffa1806bac Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:32:43 +0300 Subject: [PATCH 19/23] Preserve generated array slot provenance in Calls iteration --- .../org/usvm/ts/calls/CallsInputSnapshot.kt | 3 + .../CurrentTsCallsExtendedInputDomainsTest.kt | 68 +++++++++++++++++++ .../org/usvm/util/ArrayIndexPresence.kt | 17 ++++- 3 files changed, 87 insertions(+), 1 deletion(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputSnapshot.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputSnapshot.kt index c53e2018f9..58f65526c9 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputSnapshot.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputSnapshot.kt @@ -17,6 +17,7 @@ import org.usvm.machine.state.TsState import org.usvm.model.UModelBase import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.util.componentType +import org.usvm.util.markDenseArrayOwnSlots import org.usvm.util.markDenseInputArray internal sealed interface CallsInputSnapshot { @@ -65,6 +66,8 @@ internal data class ArrayInputSnapshot( ) : CallsInputSnapshot { override fun markDenseInputs(state: TsState) { elements.forEach { element -> element.markDenseInputs(state) } + state.markDenseArrayOwnSlots(array = reference, length = length, capacity = elements.size) + val elementSort = state.ctx.typeToSort(runtimeType.componentType) if (elementSort !is TsUnresolvedSort) { state.markDenseInputArray(array = reference, type = runtimeType) diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsExtendedInputDomainsTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsExtendedInputDomainsTest.kt index ed578267c4..0a55acb9ca 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsExtendedInputDomainsTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsExtendedInputDomainsTest.kt @@ -261,6 +261,67 @@ internal class CurrentTsCallsExtendedInputDomainsTest : CurrentTsCallsSymbolicEn } + @Test + fun `optional array spread preserves numeric and undefined slots and replays source`() { + val fixture = fixture( + source = """ + export function mixedSpread(values: (number | undefined)[]): boolean { + const copy = [...values]; + if (copy.length === 2 && copy[0] === 7 && copy[1] === undefined) { + return true; + } + return false; + } + """.trimIndent(), + exportName = "mixedSpread", + inputs = optionalArrayInputs(), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + val inputs = assertNotNull(result.inputs, result.toString()) + val values = assertIs(inputs.single()).elements + val expectedValues = listOf(JsConcreteValue.number(7.0), JsConcreteValue.Undefined) + assertEquals(expectedValues, values) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `optional array for of preserves numeric and undefined slots and replays source`() { + val fixture = fixture( + source = """ + export function mixedIteration(values: (number | undefined)[]): boolean { + let first: number | undefined; + let second: number | undefined; + let count = 0; + for (const value of values) { + if (count === 0) first = value; + else second = value; + count++; + } + if (count === 2 && first === 7 && second === undefined) { + return true; + } + return false; + } + """.trimIndent(), + exportName = "mixedIteration", + inputs = optionalArrayInputs(), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + val inputs = assertNotNull(result.inputs, result.toString()) + val values = assertIs(inputs.single()).elements + val expectedValues = listOf(JsConcreteValue.number(7.0), JsConcreteValue.Undefined) + assertEquals(expectedValues, values) + fixture.assertReplayConfirmed(inputs) + } + @Test fun `optional array slots preserve independent numeric and undefined values`() { val fixture = fixture( @@ -296,4 +357,11 @@ internal class CurrentTsCallsExtendedInputDomainsTest : CurrentTsCallsSymbolicEn ) fixture.assertReplayConfirmed(inputs) } + + private fun optionalArrayInputs(): List { + val elementDomain = OptionalDomain(value = IntegerDomain(min = 0, max = 10)) + val domain = ArrayDomain(element = elementDomain, minLength = 2, maxLength = 2) + val input = PropertyInput(name = "values", domain = domain) + return listOf(input) + } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt index edf9fe061c..938df34ce1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt @@ -1,12 +1,27 @@ package org.usvm.util import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.machine.TsSizeSort import org.usvm.machine.state.TsState -/** Presence of own numeric slots in arrays allocated by a supported NewArray expression. */ +/** A generated dense array owns every live slot, including slots whose value is undefined. */ +fun TsState.markDenseArrayOwnSlots( + array: UConcreteHeapRef, + length: UExpr, + capacity: Int, +) = with(ctx) { + val presence = (0 until capacity).associate { index -> + val symbolicIndex = mkBv(index) + symbolicIndex to mkBvSignedLessExpr(symbolicIndex, length) + } + initializedArrayIndices += array to presence + knownArrayPropertyPresence += array +} + +/** Presence of own numeric slots in source arrays and generated array inputs. */ internal fun TsState.knownArrayIndexPresence(array: UHeapRef, index: UExpr): UBoolExpr? { if (array !in knownArrayPropertyPresence) return null From b1ac33d2aa46218d3aa7200bac501375e0f7ab4d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:37:32 +0300 Subject: [PATCH 20/23] Keep generated slot presence keys at the symbolic index type --- usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt index 938df34ce1..03450edb83 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt @@ -13,7 +13,7 @@ fun TsState.markDenseArrayOwnSlots( length: UExpr, capacity: Int, ) = with(ctx) { - val presence = (0 until capacity).associate { index -> + val presence: Map, UBoolExpr> = (0 until capacity).associate { index -> val symbolicIndex = mkBv(index) symbolicIndex to mkBvSignedLessExpr(symbolicIndex, length) } From 3a11039d06aee321762682a82e0abbe3b995a7ca Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 06:11:16 +0300 Subject: [PATCH 21/23] Align array write regressions with supported dense appends --- .../usvm/samples/arrays/AllocatedArrays.kt | 38 ++++++- .../org/usvm/samples/arrays/InputArrays.kt | 107 +++++++++++++++++- .../resources/samples/arrays/InputArrays.ts | 11 ++ 3 files changed, 151 insertions(+), 5 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt index 1619f5233e..869554eb16 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt @@ -2,6 +2,7 @@ package org.usvm.samples.arrays import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir import org.usvm.UMachineOptions import org.usvm.api.TsTestValue import org.usvm.machine.TsInterpreterObserver @@ -10,14 +11,20 @@ import org.usvm.machine.TsOptions import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.test.util.checkers.eq as exactly -import org.usvm.test.util.checkers.noResultsExpected import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay import org.usvm.util.eq +import org.usvm.util.getResourcePath import org.usvm.util.neq +import java.nio.file.Path +import kotlin.io.path.readText import kotlin.test.assertEquals import kotlin.test.assertTrue class AllocatedArrays : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + private val tsPath = "/samples/arrays/AllocatedArrays.ts" override val scene: EtsScene = loadScene(tsPath) @@ -112,7 +119,34 @@ class AllocatedArrays : TsMethodTestRunner() { @Test fun `test writeInTheIndexEqualToLength`() { - assertArrayIndexGrowthLimitation("writeInTheIndexEqualToLength") + val method = getMethod(methodName = "writeInTheIndexEqualToLength") + val expected = listOf(1.0, 2.0, 3.0, 4.0) + + checkMatches>( + method = method, + analysisResultNumberMatches = exactly(1), + { result -> result.values.map { it.number } == expected }, + ) + } + + @Test + fun `write at the allocated array length appends in native JavaScript`() { + val source = getResourcePath(tsPath).readText() + val script = source + """ + + const values = new AllocatedArrays().writeInTheIndexEqualToLength(); + const expected = [1, 2, 3, 4]; + if (values.length !== expected.length || values.some((value, index) => value !== expected[index])) { + throw new Error('Appending at the allocated array length changed its contents'); + } + """.trimIndent() + + assertNodeReplay( + source = script, + directory = directory, + name = "allocated-array-append", + timeoutMessage = "Allocated array append replay timed out", + ) } private fun assertArrayIndexGrowthLimitation(methodName: String) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt index 486ec151b3..37c36ad524 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt @@ -3,12 +3,22 @@ package org.usvm.samples.arrays import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.RepeatedTest import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay import org.usvm.util.eq +import org.usvm.util.getResourcePath import org.usvm.util.neq +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertIs +import kotlin.test.assertTrue class InputArrays : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + private val tsPath = "/samples/arrays/InputArrays.ts" override val scene: EtsScene = loadScene(tsPath) @@ -39,11 +49,102 @@ class InputArrays : TsMethodTestRunner() { @Test fun testWriteIntoInputArray() { - val method = getMethod("writeIntoInputArray") + val method = getMethod(methodName = "writeIntoInputArray") + discoverProperties, TsTestValue.TsNumber>( + method = method, + { x, r -> + val first = x.values.firstOrNull() + (r eq 1) && first != null && (first eq 1) + }, + { x, r -> + val first = x.values.firstOrNull() + (r eq 1) && (first == null || (first neq 1)) + }, + invariants = arrayOf({ _, result -> result eq 1 }), + ) + } + + @Test + fun `writing a nonempty input retains both original first element branches`() { + val method = getMethod(methodName = "writeIntoNonEmptyInputArray") + discoverProperties, TsTestValue.TsNumber>( method = method, - { x, r -> (r eq 1) && (x.values[0] eq 1) }, - { x, r -> (r eq 1) && (x.values[0] neq 1) }, + { x, r -> (r eq 0) && x.values.isEmpty() }, + { x, r -> + val first = x.values.firstOrNull() + (r eq 1) && first != null && (first eq 1) + }, + { x, r -> + val first = x.values.firstOrNull() + (r eq 2) && first != null && (first neq 1) + }, + invariants = arrayOf({ input, result -> + val first = input.values.firstOrNull() + val expected = when { + first == null -> 0 + first eq 1 -> 1 + else -> 2 + } + result eq expected + }), + ) + } + + @Test + fun `input array append and overwrite witnesses replay in native JavaScript`() { + val source = getResourcePath(tsPath).readText() + val methodNames = listOf("writeIntoInputArray", "writeIntoNonEmptyInputArray") + val script = buildString { + appendLine(source) + appendLine("function assertOriginalWrite(input) {") + appendLine(" const expected = [1, ...input.slice(1)];") + appendLine(" const result = new InputArrays().writeIntoInputArray(input);") + appendLine(" const valuesMatch = input.every((value, index) => Object.is(value, expected[index]));") + appendLine(" if (result !== 1 || input.length !== expected.length || !valuesMatch) {") + appendLine(" throw new Error('Original input write failed to preserve length or tail');") + appendLine(" }") + appendLine("}") + appendLine("assertOriginalWrite([2, 7, 11]);") + appendLine("assertOriginalWrite([NaN, -0, Infinity]);") + + for (methodName in methodNames) { + val method = getMethod(methodName = methodName) + val tests = runner(method, options) + assertTrue(tests.isNotEmpty(), methodName) + + for (test in tests) { + val before = assertIs>(test.before.parameters.single()) + val after = assertIs>(test.after.parameters.single()) + val expectedResult = assertIs(test.returnValue).number + val beforeValues = before.values.joinToString { value -> + assertIs(value).number.toString() + } + val afterValues = after.values.joinToString { value -> + assertIs(value).number.toString() + } + + appendLine("{") + appendLine(" assertOriginalWrite([$beforeValues]);") + appendLine(" const actual = [$beforeValues];") + appendLine(" const expected = [$afterValues];") + appendLine(" const result = new InputArrays().$methodName(actual);") + appendLine(" const valuesMatch = actual.every((value, index) =>") + appendLine(" Object.is(value, expected[index]));") + appendLine(" const resultMatches = Object.is(result, $expectedResult);") + appendLine(" if (!resultMatches || actual.length !== expected.length || !valuesMatch) {") + appendLine(" throw new Error('$methodName changed its result or post-call array');") + appendLine(" }") + appendLine("}") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "input-array-append-and-overwrite", + timeoutMessage = "Input array append and overwrite replay timed out", ) } diff --git a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts index 0ddeeed8fa..15f6d27ded 100644 --- a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts +++ b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts @@ -16,6 +16,17 @@ class InputArrays { return x[0]; } + writeIntoNonEmptyInputArray(x: number[]) { + if (x.length === 0) return 0; + if (x[0] === 1) { + const result = this.writeIntoInputArray(x); + return result === 1 ? 1 : -1; + } + + const result = this.writeIntoInputArray(x); + return result === 1 ? 2 : -1; + } + idForArrayOfNumbers(x: number[]) { return x; } From 42be59d5dc9adf4e385ffd6846eef1101a06321d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:11:39 +0300 Subject: [PATCH 22/23] Pin published iterator lowering prerequisites --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index a2b43d6e04..c76ea758e4 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "7596ae5834" + const val jacodb = "932733f542" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" From ec761fbbadf2ad6dd7bb01391c2ebd66529fb752 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 22:58:26 +0300 Subject: [PATCH 23/23] Use merged iterator lowering artifact --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index c76ea758e4..60886e5c49 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "932733f542" + const val jacodb = "55a0990fa1" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0"