From 490e5dd13669d9ae7e4f6edb5376badcea511718 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 02:04:19 +0300 Subject: [PATCH 1/2] [TS Calls] Select candidates by target class coverage --- .../org/usvm/ts/calls/CallsCoverageScope.kt | 69 +++++++ .../org/usvm/ts/calls/CallsCoverageSearch.kt | 60 ++++-- .../org/usvm/ts/calls/CallsExperiment.kt | 2 + .../org/usvm/ts/calls/CallsSourceProject.kt | 16 +- .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 3 + .../ts/calls/CallsCoverageExperimentTest.kt | 183 +++++++++++++++++- .../usvm/ts/calls/CallsCoverageSourceTest.kt | 14 ++ 7 files changed, 324 insertions(+), 23 deletions(-) create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageScope.kt diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageScope.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageScope.kt new file mode 100644 index 0000000000..e93cfe0c44 --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageScope.kt @@ -0,0 +1,69 @@ +package org.usvm.ts.calls + +import kotlinx.serialization.Serializable +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsStmt +import java.nio.file.Path + +/** Selects symbolic candidate novelty; original-source coverage still uses its separate frozen universe. */ +@Serializable +internal data class CallsSymbolicCoverageClass( + val sourceFile: String, + val className: String, +) { + init { + val sourcePath = Path.of(sourceFile) + val isRelativeSource = sourceFile.isNotBlank() && !sourcePath.isAbsolute && + sourcePath.normalize() == sourcePath && !sourcePath.startsWith("..") && sourceFile != "." + require(isRelativeSource) { "Symbolic coverage class source must be a normalized relative path" } + require(className.isNotBlank()) { "Symbolic coverage class name must not be blank" } + } +} + +internal sealed interface CallsSymbolicCoverageScope { + data class Selected( + val classSignature: EtsClassSignature?, + val statements: Set, + ) : CallsSymbolicCoverageScope + + data class Rejected( + val status: CallsCoverageSearchStatus, + val diagnostic: String, + ) : CallsSymbolicCoverageScope +} + +internal fun resolveCallsSymbolicCoverageScope( + preparation: CallsFunctionPreparation.Eligible, + target: CallsSymbolicCoverageClass?, +): CallsSymbolicCoverageScope { + if (target == null) { + return CallsSymbolicCoverageScope.Selected( + classSignature = null, + statements = preparation.method.cfg.stmts.toSet(), + ) + } + + val targetPath = target.sourceFile.replace('\\', '/') + val classes = preparation.scene.projectClasses.filter { owner -> + owner.name == target.className && preparation.sourcePaths[owner.signature.file] == targetPath + } + if (classes.size != 1) { + val status = if (classes.isEmpty()) CallsCoverageSearchStatus.UNMAPPED else CallsCoverageSearchStatus.AMBIGUOUS + return CallsSymbolicCoverageScope.Rejected( + status = status, + diagnostic = "Symbolic coverage class $targetPath:${target.className} resolves to ${classes.size} classes", + ) + } + + val owner = classes.single() + val methods = owner.methods.filter { method -> method.signature.enclosingClass == owner.signature } + val statements = methods.flatMapTo(hashSetOf()) { method -> method.cfg.stmts } + if (statements.isEmpty()) { + return CallsSymbolicCoverageScope.Rejected( + status = CallsCoverageSearchStatus.UNSUPPORTED, + diagnostic = "Symbolic coverage class $targetPath:${target.className} has no executable statements", + ) + } + + return CallsSymbolicCoverageScope.Selected(classSignature = owner.signature, statements = statements) +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt index 1be8e31024..969e3b2ade 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt @@ -3,6 +3,7 @@ package org.usvm.ts.calls import kotlinx.serialization.Serializable import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsStmt +import org.usvm.CoverageZone import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions @@ -90,26 +91,26 @@ internal data class CallsCoverageSearchRequest( } } -/** Runs one function without a return target and records completed coverage-novel paths. */ +/** Runs one function and records completed paths adding coverage in its declared symbolic scope. */ internal class CurrentTsCallsCoverageEngine( private val sourceEngine: CurrentTsCallsSymbolicEngine = CurrentTsCallsSymbolicEngine(), ) { fun search(request: CallsCoverageSearchRequest): CallsCoverageSearchResult { val preparationStarted = TimeSource.Monotonic.markNow() - val preparation = sourceEngine.prepareFunction( - CallsFunctionPreflightRequest( - sourceRoot = request.sourceRoot, - project = request.project, - function = request.function, - expectedNativeFrontendRevision = request.expectedNativeFrontendRevision, - ), - ) - val preparationElapsedMillis = preparationStarted.elapsedNow().inWholeMilliseconds + val preparation = sourceEngine.prepareFunction(request.toFunctionPreflightRequest()) if (preparation is CallsFunctionPreparation.Rejected) { - return preparation.coverageResult(preparationElapsedMillis = preparationElapsedMillis) + return preparation.coverageResult( + preparationElapsedMillis = preparationStarted.elapsedNow().inWholeMilliseconds, + ) } preparation as CallsFunctionPreparation.Eligible + val scope = resolveCallsSymbolicCoverageScope(preparation, target = request.function.symbolicCoverageClass) + val preparationElapsedMillis = preparationStarted.elapsedNow().inWholeMilliseconds + if (scope is CallsSymbolicCoverageScope.Rejected) { + return emptyCoverageResult(scope.status, preparationElapsedMillis, scope.diagnostic) + } + scope as CallsSymbolicCoverageScope.Selected val symbolicInputs = CallsSymbolicInputs( inputs = request.function.inputs, bindings = preparation.inputBindings, @@ -122,6 +123,7 @@ internal class CurrentTsCallsCoverageEngine( val machineCallStarted = TimeSource.Monotonic.markNow() val observer = CompletedCoverageCandidateObserver( method = preparation.method, + coverageStatements = scope.statements, inputDomains = request.function.inputs, symbolicInputs = symbolicInputs, candidateCap = request.candidateCap, @@ -145,7 +147,7 @@ internal class CurrentTsCallsCoverageEngine( } } val inputCapacity = request.function.inputs.maxOfOrNull { it.domain.callsInputCapacity() } ?: 0 - val machineOptions = coverageMachineOptions(request) + val machineOptions = coverageMachineOptions(request, scope) val machineResult = runCatching { TsMachine( scene = symbolicInputs.scene, @@ -154,6 +156,7 @@ internal class CurrentTsCallsCoverageEngine( maxArraySize = maxOf(TsOptions().maxArraySize, inputCapacity), unknownCallModelSelection = modelSelection, unknownCallFallback = request.profile.fallback, + classCoverageTargets = scope.classSignature?.let { signature -> setOf(signature) }, ), machineObserver = observer, observer = interpreterObserver, @@ -197,7 +200,10 @@ internal class CurrentTsCallsCoverageEngine( ) } - private fun coverageMachineOptions(request: CallsCoverageSearchRequest): UMachineOptions = + private fun coverageMachineOptions( + request: CallsCoverageSearchRequest, + scope: CallsSymbolicCoverageScope.Selected, + ): UMachineOptions = UMachineOptions( pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY), stateCollectionStrategy = StateCollectionStrategy.COVERED_NEW, @@ -206,16 +212,36 @@ internal class CurrentTsCallsCoverageEngine( solverTimeout = request.solverQueryLimit, solverType = request.solverType, stopOnCoverage = CALLS_STOP_ON_COVERAGE, + coverageZone = if (scope.classSignature == null) CoverageZone.METHOD else CoverageZone.CLASS, + removeCoveredEntryPoints = scope.classSignature == null, stopOnTargetsReached = false, throwExceptionOnStepFailure = true, ) } +private fun CallsCoverageSearchRequest.toFunctionPreflightRequest(): CallsFunctionPreflightRequest = + CallsFunctionPreflightRequest( + sourceRoot = sourceRoot, + project = project, + function = function, + expectedNativeFrontendRevision = expectedNativeFrontendRevision, + ) + private fun CallsFunctionPreparation.Rejected.coverageResult( preparationElapsedMillis: Long, +): CallsCoverageSearchResult = emptyCoverageResult( + status = status.toCoverageStatus(), + preparationElapsedMillis = preparationElapsedMillis, + diagnostic = "$reasonCode: $diagnostic", +) + +private fun emptyCoverageResult( + status: CallsCoverageSearchStatus, + preparationElapsedMillis: Long, + diagnostic: String, ): CallsCoverageSearchResult { return CallsCoverageSearchResult( - status = status.toCoverageStatus(), + status = status, candidates = emptyList(), selectedStates = 0, executedSteps = 0, @@ -226,12 +252,13 @@ private fun CallsFunctionPreparation.Rejected.coverageResult( machineSetupElapsedMillis = 0, searchElapsedMillis = 0, machineTeardownElapsedMillis = 0, - diagnostic = "$reasonCode: $diagnostic", + diagnostic = diagnostic, ) } private class CompletedCoverageCandidateObserver( private val method: EtsMethod, + private val coverageStatements: Set, private val inputDomains: List, private val symbolicInputs: CallsSymbolicInputs, private val candidateCap: Int, @@ -240,7 +267,6 @@ private class CompletedCoverageCandidateObserver( private val onCandidate: (CallsCoverageCandidate) -> Unit, private val onExtractionFailure: (String) -> Unit, ) : UMachineObserver { - private val entryStatements: Set = method.cfg.stmts.toSet() private val coveredStatements = hashSetOf() private val inputKeys = hashSetOf() private var machineStarted: TimeSource.Monotonic.ValueTimeMark? = null @@ -295,7 +321,7 @@ private class CompletedCoverageCandidateObserver( } } val pathStatements = state.pathNode.allStatements.filterTo(hashSetOf()) { statement -> - statement in entryStatements + statement in coverageStatements } val newStatements = pathStatements.count { statement -> statement !in coveredStatements } if (newStatements == 0) return 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 5a8bc4c4d2..99ada8b646 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 @@ -48,6 +48,8 @@ internal data class CallsFunctionCase( val entryPoint: TypeScriptEntryPoint, val inputs: List, val targets: List, + /** Optional target class for coverage-novel symbolic candidates through this function. */ + val symbolicCoverageClass: CallsSymbolicCoverageClass? = null, ) @Serializable 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 index e93b44b1c9..90c1ad3b4c 100644 --- 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 @@ -18,6 +18,7 @@ internal sealed interface CallsSourceProject { val scene: EtsScene, val entryModule: String, val sourceByFile: Map, + val sourcePaths: Map, ) : CallsSourceProject data class Unsupported(val issue: CallsIrReadinessIssue) : CallsSourceProject @@ -42,6 +43,7 @@ internal fun loadCallsSourceProject(sourceRoot: Path, source: Path): CallsSource scene = EtsScene(projectFiles = listOf(entry)), entryModule = source.fileName.toString(), sourceByFile = mapOf(entry.signature to Files.readString(source)), + sourcePaths = mapOf(entry.signature to entryModule.replace('\\', '/')), ) } @@ -72,20 +74,26 @@ internal fun loadCallsSourceProject(sourceRoot: Path, source: Path): CallsSource } finally { generatedIr.toFile().deleteRecursively() } - val sourceByFile = scene.projectFiles.associate { file -> + val sourcePaths = 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]) { + require(relative in sources) { "Frontend source identity is outside the inspected closure: ${file.signature}" } + file.signature to relative } - require(sourceByFile.size == closure.files.size) { "Frontend omitted or duplicated a dependency source" } + require(sourcePaths.size == closure.files.size) { "Frontend omitted or duplicated a dependency source" } - return CallsSourceProject.Loaded(scene = scene, entryModule = entryModule, sourceByFile = sourceByFile) + return CallsSourceProject.Loaded( + scene = scene, + entryModule = entryModule, + sourceByFile = sourcePaths.mapValues { (_, relative) -> sources.getValue(relative) }, + sourcePaths = sourcePaths.mapValues { (_, relative) -> relative.replace('\\', '/') }, + ) } finally { temporaryProject.toFile().deleteRecursively() } 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 ada0139f1d..3e4ce47438 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 @@ -1,6 +1,7 @@ package org.usvm.ts.calls import mu.KotlinLogging +import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsLexicalEnvType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsReturnStmt @@ -56,6 +57,7 @@ internal sealed interface CallsFunctionPreparation { val inputBindings: List, val lexicalEnvironment: EtsLexicalEnvironmentBinding?, val captures: List, + val sourcePaths: Map, ) : CallsFunctionPreparation data class Rejected( @@ -409,6 +411,7 @@ internal class CurrentTsCallsSymbolicEngine( inputBindings = mappedTarget.bindings.inputs, lexicalEnvironment = lexicalEnvironment, captures = sourceCaptures, + sourcePaths = loaded.sourcePaths, ) } diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt index f8cddffa5c..d2e8618849 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt @@ -296,9 +296,182 @@ class CallsCoverageExperimentTest { assertTrue(replay.coveredStatementKeys.isNotEmpty()) } + @Test + fun `class novelty retains private helper candidates in every profile`() { + val fixture = fixture( + source = """ + export class Covered { + static run(flag: boolean): number { return Covered.choose(flag); } + private static choose(flag: boolean): number { + if (flag) { return 1; } + return 2; + } + } + export function harness(flag: boolean): number { Covered.run(flag); return 0; } + """.trimIndent(), + exportName = "harness", + inputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)), + ) + val engine = CurrentTsCallsCoverageEngine(testSourceEngine()) + val request = coverageRequest(fixture) + val classFunction = fixture.function.copy( + symbolicCoverageClass = CallsSymbolicCoverageClass(sourceFile = "Fixture.ts", className = "Covered"), + ) + + val entrySearch = engine.search(request) + val classSearches = CallsExperimentProfile.entries.associateWith { profile -> + engine.search(request.copy(function = classFunction, profile = profile)) + } + + assertEquals(expected = 1, actual = entrySearch.candidates.size, message = entrySearch.toString()) + for ((profile, search) in classSearches) { + assertEquals( + expected = CallsCoverageSearchStatus.EXHAUSTED, + actual = search.status, + message = "$profile: $search", + ) + assertEquals(expected = 2, actual = search.candidates.size, message = "$profile: $search") + assertEquals( + expected = setOf(listOf(JsConcreteValue.Boolean(true)), listOf(JsConcreteValue.Boolean(false))), + actual = search.candidates.map { candidate -> candidate.inputs }.toSet(), + ) + assertTrue(search.candidates.all { candidate -> candidate.newSymbolicStatements > 0 }) + } + + val replays = OriginalTypeScriptCoverageReplayer( + sourceRoot = fixture.sourceRoot, + function = classFunction, + ).use { replayer -> + classSearches.getValue(CallsExperimentProfile.EMPTY_STOP).candidates.map { candidate -> + replayer.replay(inputs = candidate.inputs, timeoutMillis = 20_000L) + } + } + + assertEquals(expected = 2, actual = replays.flatMap { replay -> replay.coveredIfArmKeys }.toSet().size) + assertTrue(replays.all { replay -> replay.completion == CallsCoverageCompletion.RETURNED }) + } + + @Test + fun `class novelty retains constructor branches through a constant wrapper`() { + val fixture = fixture( + source = """ + export class Covered { + value: number; + constructor(flag: boolean) { + if (flag) { this.value = 1; } else { this.value = 2; } + } + } + export function harness(flag: boolean): number { const value = new Covered(flag); return 0; } + """.trimIndent(), + exportName = "harness", + inputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)), + symbolicCoverageClass = CallsSymbolicCoverageClass(sourceFile = "Fixture.ts", className = "Covered"), + ) + + val search = CurrentTsCallsCoverageEngine(testSourceEngine()).search(coverageRequest(fixture)) + + assertEquals( + expected = CallsCoverageSearchStatus.EXHAUSTED, + actual = search.status, + message = search.toString(), + ) + assertEquals(expected = 2, actual = search.candidates.size, message = search.toString()) + } + + @Test + fun `class scope distinguishes source paths and ignores foreign class branches`() { + val fixture = fixture( + source = """ + import { Target as Chosen } from './chosen/Target'; + import { Target as Foreign } from './foreign/Target'; + export function harness(flag: boolean): number { Chosen.run(); Foreign.run(flag); return 0; } + """.trimIndent(), + exportName = "harness", + inputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)), + additionalSources = mapOf( + "chosen/Target.ts" to "export class Target { static run(): number { return 7; } }", + "foreign/Target.ts" to """ + export class Target { + static run(flag: boolean): number { if (flag) { return 1; } return 2; } + } + """.trimIndent(), + ), + symbolicCoverageClass = CallsSymbolicCoverageClass(sourceFile = "chosen/Target.ts", className = "Target"), + ) + + val search = CurrentTsCallsCoverageEngine(testSourceEngine()).search(coverageRequest(fixture)) + + assertEquals( + expected = CallsCoverageSearchStatus.EXHAUSTED, + actual = search.status, + message = search.toString(), + ) + assertEquals(expected = 1, actual = search.candidates.size, message = search.toString()) + } + + @Test + fun `wrapper-only coverage does not create class candidates`() { + val fixture = fixture( + source = """ + export class Covered { static unused(): number { return 7; } } + export function harness(flag: boolean): number { if (flag) { return 1; } return 2; } + """.trimIndent(), + exportName = "harness", + inputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)), + symbolicCoverageClass = CallsSymbolicCoverageClass(sourceFile = "Fixture.ts", className = "Covered"), + ) + val emitted = mutableListOf() + + val search = CurrentTsCallsCoverageEngine(testSourceEngine()).search( + coverageRequest(fixture, onCandidate = emitted::add), + ) + + assertEquals( + expected = CallsCoverageSearchStatus.EXHAUSTED, + actual = search.status, + message = search.toString(), + ) + assertEquals(expected = emptyList(), actual = search.candidates) + assertEquals(expected = emptyList(), actual = emitted) + assertTrue(search.executedSteps > 0) + } + + @Test + fun `unmapped coverage classes are rejected before symbolic search`() { + val fixture = fixture( + source = """ + export class Covered { static run(): number { return 7; } } + export function harness(): number { return Covered.run(); } + """.trimIndent(), + exportName = "harness", + inputs = emptyList(), + ) + val engine = CurrentTsCallsCoverageEngine(testSourceEngine()) + val targets = listOf( + CallsSymbolicCoverageClass(sourceFile = "Fixture.ts", className = "Missing"), + CallsSymbolicCoverageClass(sourceFile = "Missing.ts", className = "Covered"), + ) + + for (target in targets) { + val request = coverageRequest(fixture).copy( + function = fixture.function.copy(symbolicCoverageClass = target), + ) + + val search = engine.search(request) + + assertEquals( + expected = CallsCoverageSearchStatus.UNMAPPED, + actual = search.status, + message = search.toString(), + ) + assertEquals(expected = 0L, actual = search.executedSteps) + assertEquals(expected = emptyList(), actual = search.candidates) + } + } + private fun coverageRequest( fixture: CoverageFixture, - onCandidate: (CallsCoverageCandidate) -> Unit, + onCandidate: (CallsCoverageCandidate) -> Unit = {}, solverType: SolverType = SolverType.YICES, ) = CallsCoverageSearchRequest( sourceRoot = fixture.sourceRoot, @@ -325,10 +498,15 @@ class CallsCoverageExperimentTest { exportName: String, inputs: List, additionalSources: Map = emptyMap(), + symbolicCoverageClass: CallsSymbolicCoverageClass? = null, ): CoverageFixture { val sourceRoot = Files.createDirectory(directory.resolve(exportName)) Files.writeString(sourceRoot.resolve("Fixture.ts"), source) - additionalSources.forEach { (name, contents) -> Files.writeString(sourceRoot.resolve(name), contents) } + additionalSources.forEach { (name, contents) -> + val file = sourceRoot.resolve(name) + Files.createDirectories(file.parent) + Files.writeString(file, contents) + } runGit(sourceRoot, "init") runGit(sourceRoot, "config", "user.name", "USVM Tests") runGit(sourceRoot, "config", "user.email", "usvm@example.test") @@ -341,6 +519,7 @@ class CallsCoverageExperimentTest { entryPoint = TypeScriptEntryPoint(module = "Fixture.ts", exportName = exportName), inputs = inputs, targets = emptyList(), + symbolicCoverageClass = symbolicCoverageClass, ) val project = CallsProjectCase( projectId = exportName, diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt index d590706752..034a75ca4e 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt @@ -157,6 +157,20 @@ class CallsCoverageSourceTest { ) ) ), + original.copy( + projects = listOf( + project.copy( + functions = listOf( + function.copy( + symbolicCoverageClass = CallsSymbolicCoverageClass( + sourceFile = "Fixture.ts", + className = "DifferentClass", + ), + ), + ), + ), + ), + ), original.copy(modelSet = original.modelSet.copy(ids = setOf("ts.array.includes"))), ) From 6ec8f98c12f60ab268a026b34da2320c9595bc9f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 02:17:24 +0300 Subject: [PATCH 2/2] [TS Calls] Exclude mismatched replays from coverage checkpoints --- .../org/usvm/ts/calls/CallsCoverageCell.kt | 9 ++- .../usvm/ts/calls/CallsCoverageSourceTest.kt | 61 +++++++++++++++++-- 2 files changed, 64 insertions(+), 6 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt index 72c857e79c..ff96c00951 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt @@ -345,8 +345,13 @@ private fun coverageCheckpoints( search.candidates[index].emittedAtMillis <= checkpoint } val replayed = indices.mapNotNull { index -> events[index].replay } - val coveredStatements = replayed.flatMap { it.coveredStatementKeys }.toSet() - val coveredIfArms = replayed.flatMap { it.coveredIfArmKeys }.toSet() + val accepted = indices.mapNotNull { index -> + val event = events[index] + val expectedCompletion = search.candidates[index].completion + event.replay?.takeIf { replay -> event.error == null && replay.completion == expectedCompletion } + } + val coveredStatements = accepted.flatMap { it.coveredStatementKeys }.toSet() + val coveredIfArms = accepted.flatMap { it.coveredIfArmKeys }.toSet() require(universe.supportedStatementKeys.containsAll(coveredStatements)) { "Replayed statements extend beyond the frozen coverage universe" } diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt index 034a75ca4e..edc596e80b 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt @@ -4,6 +4,7 @@ import kotlinx.serialization.decodeFromString import org.junit.jupiter.api.io.TempDir import org.usvm.SolverType import org.usvm.ts.pbt.model.BooleanDomain +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.TypeScriptEntryPoint @@ -131,6 +132,54 @@ class CallsCoverageSourceTest { assertFalse(Files.exists(directory.resolve("universe-output/universe.json"))) } + @Test + fun `only completion-matching native replays contribute checkpoint coverage`() { + val fixture = fixture() + val universe = OriginalTypeScriptCoverageReplayer( + sourceRoot = fixture.source.sourceRoot, + function = fixture.source.function, + ).use { replayer -> replayer.probeUniverse(timeoutMillis = 20_000L) } + fixture.writeUniverse(universe) + + for (completion in CallsCoverageCompletion.entries) { + val candidate = CallsCoverageCandidate( + emittedAtMillis = 1L, + emittedAtStep = 1L, + inputs = listOf(JsConcreteValue.Boolean(true)), + newSymbolicStatements = 1, + completion = completion, + ) + val cell = fixture.copy(output = Files.createDirectory(directory.resolve(completion.name))) + cell.persistSearch(search = emptySearch.copy(candidates = listOf(candidate), selectedStates = 1)) + + cell.runCell() + + val result = CallsExperimentJson.json.decodeFromString( + Files.readString(cell.output.resolve("result.json")), + ) + val event = CallsExperimentJson.json.decodeFromString( + Files.readAllLines(cell.output.resolve("replays.jsonl")).single(), + ) + val replay = requireNotNull(event.replay) + val checkpoint = result.checkpoints.single() + val isAccepted = completion == CallsCoverageCompletion.RETURNED + val acceptedCount = if (isAccepted) 1 else 0 + + assertEquals(expected = 0, actual = result.replayErrors) + assertEquals(expected = 1 - acceptedCount, actual = result.completionMismatches) + assertEquals(expected = CallsCoverageCompletion.RETURNED, actual = replay.completion) + assertTrue(replay.coveredStatementKeys.isNotEmpty()) + assertEquals(expected = 1, actual = checkpoint.emittedCandidates) + assertEquals(expected = 1, actual = checkpoint.replayedCandidates) + if (isAccepted) { + assertTrue(checkpoint.coveredStatements > 0) + } else { + assertEquals(expected = 0, actual = checkpoint.coveredStatements) + assertEquals(expected = 0, actual = checkpoint.coveredIfArms) + } + } + } + @Test fun `resumed search rejects changed export domain and frozen models at the same manifest path`() { val fixture = fixture() @@ -352,7 +401,7 @@ class CallsCoverageSourceTest { ) { private val universePath: Path = manifestPath.resolveSibling("universe.json") - fun writeUniverse() { + fun writeUniverse(universe: CallsCoverageUniverse = sampleUniverse) { val identity = CallsCoverageUniverseIdentity( toolRevision = TOOL_REVISION, nativeFrontendRevision = FRONTEND_REVISION, @@ -362,7 +411,7 @@ class CallsCoverageSourceTest { functionIndex = 0, sourceFile = source.function.sourceFile, ) - val record = CallsCoverageUniverseRecord(identity = identity, universe = sampleUniverse) + val record = CallsCoverageUniverseRecord(identity = identity, universe = universe) Files.writeString(universePath, CallsExperimentJson.json.encodeToUtf8SafeString(record)) } @@ -382,7 +431,11 @@ class CallsCoverageSourceTest { return output } - fun persistSearch(schemaVersion: Int = 3, solver: String = source.manifest.solver) { + fun persistSearch( + schemaVersion: Int = 3, + solver: String = source.manifest.solver, + search: CallsCoverageSearchResult = emptySearch, + ) { val identity = CallsCoverageCellIdentity( schemaVersion = schemaVersion, toolRevision = TOOL_REVISION, @@ -406,7 +459,7 @@ class CallsCoverageSourceTest { ) Files.writeString( output.resolve("search.json"), - CallsExperimentJson.json.encodeToUtf8SafeString(emptySearch) + CallsExperimentJson.json.encodeToUtf8SafeString(search) ) }