diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index a2b43d6e04..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 = "7596ae5834" + const val jacodb = "55a0990fa1" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" 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/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/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..0cd776ddb5 --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsIrReadinessIssue.kt @@ -0,0 +1,200 @@ +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 +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 + +internal data class CallsIrReadinessIssue( + val reasonCode: CallsSymbolicPreflightReasonCode, + val diagnostic: String, +) + +internal fun callsIrReadinessIssue( + method: EtsMethod, + graph: TsGraph, + sourceByFile: Map, +): CallsIrReadinessIssue? { + val pending = ArrayDeque().apply { addLast(method) } + val visited = hashSetOf() + + while (pending.isNotEmpty()) { + val currentMethod = pending.removeFirst() + if (!visited.add(currentMethod)) continue + + currentMethod.irReadinessIssue( + source = sourceByFile.getValue(currentMethod.signature.enclosingClass.file), + graph = graph, + )?.let { issue -> return issue } + + 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.projectCallees( + graph: TsGraph, + sourceFiles: Set, +): 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 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, + 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) + 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", "regularexpression", "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/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/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..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 @@ -6,15 +6,15 @@ 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 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 @@ -54,10 +54,15 @@ 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, 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 +85,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 +170,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 +195,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 +210,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 +244,9 @@ internal class CurrentTsCallsSymbolicEngine( } private fun prepareSafely(request: CallsSymbolicPreflightRequest): CallsTargetPreparation { - preparedTargets[request]?.let { preparation -> return preparation } + val cached = preparedTarget + 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( @@ -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 } @@ -273,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, @@ -345,6 +359,19 @@ internal class CurrentTsCallsSymbolicEngine( ) } + val readinessIssue = callsIrReadinessIssue( + method = method, + graph = TsGraph(scene), + sourceByFile = loaded.sourceByFile, + ) + 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 -> { @@ -368,6 +395,24 @@ 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", + ) + val sourceTargetReason = sourceTarget.reason + if (sourceTargetReason != null) { + return CallsTargetPreparation.Rejected( + status = CallsSymbolicStatus.UNSUPPORTED, + reasonCode = CallsSymbolicPreflightReasonCode.TARGET_ORIGIN_UNSUPPORTED, + diagnostic = sourceTargetReason, + ) + } + val returnStatement = completedReturnCandidate( method = method, target = request.target, @@ -612,10 +657,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/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/CallsReadinessAndTelemetryTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt new file mode 100644 index 0000000000..59ecb8bde0 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsReadinessAndTelemetryTest.kt @@ -0,0 +1,248 @@ +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 `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 { + 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 lowered regex allocation 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 allocation 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 `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( + 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/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/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-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..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 @@ -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 @@ -21,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) @@ -43,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), @@ -54,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), ) @@ -75,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() @@ -95,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, @@ -108,6 +117,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 +131,7 @@ internal open class CurrentTsCallsSymbolicEngineTestSupport { seed = 0, budget = 10.seconds, unknownCallEventSink = unknownCallEventSink, + runtimeLimitationEventSink = runtimeLimitationEventSink, ) ) 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..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 @@ -1,54 +1,67 @@ -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 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) + return statement.declarationList.declarations.filter((declaration) => + 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, + ) + }) + 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, +) 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..d115df1717 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,8 @@ enum class TsRuntimeFeatureLimitationReason { ARRAY_NAMED_PROPERTY_READ, ARRAY_NAMED_PROPERTY_WRITE, ARRAY_INDEX_GROWTH, + ARRAY_ITERATOR_UNSUPPORTED, ARRAY_LENGTH_CAPACITY, ARRAY_LENGTH_GROWTH, + STRING_ITERATOR_UNSUPPORTED, } 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..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 @@ -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,6 +66,8 @@ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { length = newLength, ) memory.write(lengthLValue, newLength, guard = trueExpr) + moveInitializedArrayIndices(input.array) { index -> mkBvSubExpr(index, one) } + truncateKnownArrayIndices(input.array, newLength) }, ) @@ -66,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) { @@ -91,17 +96,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 new file mode 100644 index 0000000000..7eba4f05e6 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -0,0 +1,180 @@ +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 +import org.usvm.util.writtenArrayIndexPresence + +/** 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, +) + +/** 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")) +internal val iteratorResultType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinIteratorResult")) + +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 + if (stmt.call.callee.name != "next") return TsExprApproximationResult.NoApproximation + + 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) { + 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 needs known element-presence and value storage") + return null + } + + val length = scope.calcOnState { memory.read(mkArrayLengthLValue(iterator.array, iterator.arrayType)) } + 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( + 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 { + // Inputs are dense; known allocations distinguish written own slots from holes. + val array = iterator.array + val denseInput = !isAllocatedConcreteHeapRef(array) || denseInputArrays[array] != null + val knownOwnSlots = array in knownArrayPropertyPresence + if (denseInput || knownOwnSlots) { + trueExpr + } else { + writtenArrayIndexPresence(array, iterator.index) + } + } + val supportedRead = mkOr(done, initialized) + if (scope.checkSat(mkNot(supportedRead)) != null) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_ITERATOR_UNSUPPORTED, + detail = "Array iteration requires known own-slot provenance", + ) + } + 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 { + val nextIndex = mkBvAddExpr(iterator.index, mkBv(1)) + arrayIterators += reference to iterator.copy( + index = mkIte(done, iterator.index, nextIndex), + exhausted = done, + ) + val result = memory.allocConcrete(iteratorResultType) + iteratorResults += result to TsIteratorResult(done = done, value = value) + result + } +} + +internal fun TsExprResolver.readBuiltinIteratorField(reference: UHeapRef, name: String): UExpr<*>? = with(ctx) { + if (reference !is UConcreteHeapRef) return null + + val result = scope.calcOnState { iteratorResults[reference] } + if (result != null) { + return when (name) { + "done" -> result.done + "value" -> result.value + else -> mkUndefinedValue() + } + } + + val isIterator = scope.calcOnState { arrayIterators[reference] != null || stringIterators[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/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 f25e722c75..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 @@ -21,7 +21,7 @@ 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 import org.usvm.machine.call.TsUnknownCallFailureReason @@ -37,17 +37,19 @@ 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.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.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 {} @@ -151,6 +153,10 @@ 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 // Mock `.toString()` method calls if (expr.callee.name == "toString") { @@ -566,7 +572,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))) @@ -581,20 +586,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) + moveInitializedArrayIndices(array) { sourceIndex -> mkBvSubExpr(sourceIndex, mkBv(1)) } } + truncateKnownArrayIndices(array, newLength) memory.write(lengthLValue, newLength, guard = trueExpr) removed @@ -719,6 +717,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 } @@ -753,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) } @@ -808,6 +807,8 @@ private fun TsExprResolver.handleArrayUnshift( length = length, ) + 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) ?: return@calcOnState null @@ -1205,7 +1206,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 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( + 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 -> @@ -1219,6 +1232,16 @@ private fun TsExprResolver.handleArrayReverse( val contents = reversedIndices.map { index -> memory.readArrayIndex(array, index, kind, boolSort) } initializeArrayKind(reversedArray, kind, contents) } + } else { + initializeTypedArrayOverrides(array) + 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) + } } copyArrayElements( @@ -1230,9 +1253,9 @@ private fun TsExprResolver.handleArrayReverse( length = length ) + moveInitializedArrayIndices(array) { index -> mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index) } + // Return the modified original array array } } - -private const val ARRAY_REVERSE_MAX_SIZE = 5000 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 8512ba59b4..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, @@ -137,7 +140,27 @@ private fun TsContext.readArrayProperty( ) } -private fun TsContext.readArrayElement( +internal fun TsContext.readArrayElement( + scope: TsStepScope, + 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, 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..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,10 @@ 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 // Handle reading "length" property. val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } @@ -422,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 0c94b12f75..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 @@ -63,7 +63,14 @@ 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 || stringIterators[reference] != null } + 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 224f294426..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 @@ -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() @@ -578,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") @@ -1552,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 } @@ -1740,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/TsStringIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt new file mode 100644 index 0000000000..daa3dbc221 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsStringIterator.kt @@ -0,0 +1,116 @@ +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")) + +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) { + 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 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 (isDone) { + 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 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) + scope.fork(widthBranch) ?: return null + + width = if (isPair) mkBv(2) else mkBv(1) + + value = scope.calcOnState { + allocateBoundedString(length = width, codeUnits = listOf(first, second)) + } + } + + scope.calcOnState { + stringIterators += reference to iterator.copy( + index = mkBvAddExpr(iterator.index, width), + exhausted = mkBool(isDone), + ) + val result = memory.allocConcrete(iteratorResultType) + 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 6cdb528374..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 @@ -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, @@ -96,9 +98,15 @@ 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 return assignToArrayIndex( scope = scope, @@ -115,6 +123,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 +163,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) @@ -144,6 +175,11 @@ fun TsContext.assignToArrayIndex( } scope.assert(indexIsInRange) ?: return null + scope.doWithState { + val writtenIndices = initializedArrayIndices[array].orEmpty() + initializedArrayIndices += array to (writtenIndices + (index to trueExpr)) + } + val elementSort = typeToSort(arrayType.componentType) // If the element sort is known, write directly. 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 a75c6b7526..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 @@ -27,8 +28,12 @@ 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.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 @@ -72,6 +77,12 @@ class TsState( var methodToRef: UPersistentHashMap = persistentHashMapOf(), var associatedFunction: UPersistentHashMap = persistentHashMapOf(), var capturedInstanceCalls: UPersistentHashMap = persistentHashMapOf(), + 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, UBoolExpr>> = emptyMap(), var boundThis: UPersistentHashMap = persistentHashMapOf(), var dfltObject: UPersistentHashMap = persistentHashMapOf(), @@ -341,6 +352,12 @@ class TsState( methodToRef = methodToRef, associatedFunction = associatedFunction, capturedInstanceCalls = capturedInstanceCalls, + arrayIterators = arrayIterators, + iteratorResults = iteratorResults, + 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..03450edb83 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayIndexPresence.kt @@ -0,0 +1,61 @@ +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 + +/** 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: Map, UBoolExpr> = (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 + + 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/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/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/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..59d3b04517 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayIteratorSourceTest.kt @@ -0,0 +1,101 @@ +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", + "reversedMixedAlias", "unshiftedMixedAlias", "shiftedMixedAlias", + "localSymbolShadow", + ) + + 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 retain explicit limitations`() { + val methods = listOf("stringNamedLookalike") + for (methodName in methods) { + 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 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)) + + 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 new file mode 100644 index 0000000000..b453b46ab4 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/SourceSdkConstructorShadowTest.kt @@ -0,0 +1,55 @@ +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", + "symbolKeyKeepsSourceImplementation", + ) +} 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/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..f3840d81f0 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/StringIteratorSourceTest.kt @@ -0,0 +1,157 @@ +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/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/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/ArrayIteratorSource.ts b/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts new file mode 100644 index 0000000000..53db5c433b --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayIteratorSource.ts @@ -0,0 +1,161 @@ +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 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; + } + + 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; + } + + 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/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 { 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]; } 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..b9147e4cb7 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SourceSdkConstructorShadow.ts @@ -0,0 +1,26 @@ +// @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 }; + +// @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]; + const result = Object.setPrototypeOf(values, { 0: 11 }); + return result === values && values[0] === 9 ? 1 : 0; + } + + static arrayMethodKeepsSourceImplementation(): number { + return Array.isArray([]) ? 0 : 1; + } + + static symbolKeyKeepsSourceImplementation(): number { + const values = [7]; + values[Symbol.iterator] = 11; + return values[0] === 11 ? 1 : 0; + } +} 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; + } +} 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; + } +} 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; }