diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt index 9a3d0b4c94..60173bd83b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt @@ -36,6 +36,7 @@ private fun createPathSelector( cfgStatisticsFactory: () -> CfgStatistics? = { null }, callGraphStatisticsFactory: () -> CallGraphStatistics? = { null }, loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null }, + coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator? = { null }, ): UPathSelector where Target : UTarget, State : UState<*, Method, Statement, *, Target, State> { @@ -69,14 +70,16 @@ private fun createPathSelector( PathSelectionStrategy.CLOSEST_TO_UNCOVERED -> createClosestToUncoveredPathSelector( requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for closest to uncovered path selector" }, requireNotNull(cfgStatisticsFactory()) { "CFG statistics is required for closest to uncovered path selector" }, - applicationGraph + applicationGraph, + distanceCalculator = coverageDistanceCalculatorFactory(), ) PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM -> createClosestToUncoveredPathSelector( requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for closest to uncovered path selector" }, requireNotNull(cfgStatisticsFactory()) { "CFG statistics is required for closest to uncovered path selector" }, applicationGraph, - random + random, + distanceCalculator = coverageDistanceCalculatorFactory(), ) PathSelectionStrategy.TARGETED -> createTargetedPathSelector( @@ -153,6 +156,7 @@ fun createPathSelector( cfgStatisticsFactory: () -> CfgStatistics? = { null }, callGraphStatisticsFactory: () -> CallGraphStatistics? = { null }, loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null }, + coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator? = { null }, ): UPathSelector where Target : UTarget, State : UState<*, Method, Statement, *, Target, State> = createPathSelector( listOf(initialState), @@ -161,7 +165,8 @@ fun createPathSelector( coverageStatisticsFactory, cfgStatisticsFactory, callGraphStatisticsFactory, - loopStatisticFactory + loopStatisticFactory, + coverageDistanceCalculatorFactory, ) fun createPathSelector( @@ -173,6 +178,7 @@ fun createPathSelector( cfgStatisticsFactory: () -> CfgStatistics? = { null }, callGraphStatisticsFactory: () -> CallGraphStatistics? = { null }, loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null }, + coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator? = { null }, ): UPathSelector where Target : UTarget, State : UState<*, Method, Statement, *, Target, State> { val hasSingleEntryPoint = initialStates.size == 1 val hasUnlimitedScheduling = options.timeout == Duration.INFINITE && @@ -185,7 +191,8 @@ fun createPathSelector( coverageStatisticsFactory, cfgStatisticsFactory, callGraphStatisticsFactory, - loopStatisticFactory + loopStatisticFactory, + coverageDistanceCalculatorFactory, ) } @@ -202,7 +209,8 @@ fun createPathSelector( coverageStatisticsFactory, cfgStatisticsFactory, callGraphStatisticsFactory, - loopStatisticFactory + loopStatisticFactory, + coverageDistanceCalculatorFactory, ) val coverageStatistics = coverageStatisticsFactory() @@ -317,15 +325,16 @@ private fun , applicationGraph: ApplicationGraph, random: Random? = null, + distanceCalculator: CallStackDistanceCalculator? = null, ): UPathSelector { - val distanceCalculator = CallStackDistanceCalculator( + val calculator = distanceCalculator ?: CallStackDistanceCalculator( targets = coverageStatistics.getUncoveredStatements(), cfgStatistics = cfgStatistics, applicationGraph ) coverageStatistics.addOnCoveredObserver { _, method, statement -> - distanceCalculator.removeTarget( + calculator.removeTarget( method, statement ) @@ -334,21 +343,25 @@ private fun > createClosestToUncoveredRandomPathSelector( + distance: StateWeighter, + random: Random, +): UPathSelector = WeightedPathSelector( + priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } }, + weighter = { 1.0 / max(distance.weight(it).toDouble(), 1.0) }, +) + fun > createForkDepthPathSelector( random: Random? = null, ): UPathSelector { diff --git a/usvm-core/src/test/kotlin/org/usvm/ps/ClosestToUncoveredRandomPathSelectorTest.kt b/usvm-core/src/test/kotlin/org/usvm/ps/ClosestToUncoveredRandomPathSelectorTest.kt new file mode 100644 index 0000000000..a7365dde31 --- /dev/null +++ b/usvm-core/src/test/kotlin/org/usvm/ps/ClosestToUncoveredRandomPathSelectorTest.kt @@ -0,0 +1,149 @@ +package org.usvm.ps + +import io.mockk.every +import org.junit.jupiter.api.Test +import org.usvm.PathNode +import org.usvm.PathSelectionStrategy +import org.usvm.TestInstruction +import org.usvm.TestState +import org.usvm.UMachineOptions +import org.usvm.appGraph +import org.usvm.mockState +import org.usvm.statistics.CoverageStatistics +import org.usvm.statistics.distances.CallStackDistanceCalculator +import org.usvm.statistics.distances.CfgStatistics +import org.usvm.statistics.distances.CfgStatisticsImpl +import kotlin.test.assertEquals +import kotlin.test.assertSame +import kotlin.test.assertTrue + +class ClosestToUncoveredRandomPathSelectorTest { + private val graph = appGraph { + method(name = "method", instructionsCount = 7) { + entryPoint(offset = 0) + edge(from = 0, to = 1) + edge(from = 1, to = 2) + edge(from = 0, to = 3) + edge(from = 3, to = 4) + edge(from = 4, to = 5) + edge(from = 5, to = 6) + exitPoint(offset = 2) + exitPoint(offset = 6) + } + } + + @Test + fun `coverage and peek never recalculate queued weights while update touches only its state`() { + val cfg = CfgStatisticsImpl(graph) + val evaluated = mutableListOf() + val countedCfg = object : CfgStatistics by cfg { + override fun getShortestDistanceToExit(method: String, stmtFrom: TestInstruction): UInt { + evaluated.add(stmtFrom) + return cfg.getShortestDistanceToExit(method, stmtFrom) + } + } + val leftGoal = TestInstruction(method = "method", offset = 1) + val rightGoal = TestInstruction(method = "method", offset = 6) + val calculator = CallStackDistanceCalculator( + targets = listOf(leftGoal, rightGoal), + cfgStatistics = countedCfg, + applicationGraph = graph, + ) + val nativeCoverage = CoverageStatistics( + methods = setOf("method"), + applicationGraph = graph, + ) + val left = mockState(id = 1u, startMethod = "method", startInstruction = 1) + val right = mockState(id = 2u, startMethod = "method", startInstruction = 3) + val selector = createPathSelector( + initialState = left, + options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + randomSeed = 0, + ), + applicationGraph = graph, + coverageStatisticsFactory = { nativeCoverage }, + cfgStatisticsFactory = { countedCfg }, + coverageDistanceCalculatorFactory = { calculator }, + ) + selector.add(states = listOf(right)) + assertEquals(expected = listOf(left.currentStatement, right.currentStatement), actual = evaluated) + assertSame(expected = left, actual = selector.peek()) + evaluated.clear() + + assertTrue(calculator.removeTarget(method = "method", statement = leftGoal)) + repeat(256) { selector.peek() } + + assertTrue(evaluated.isEmpty()) + assertEquals(expected = 0, actual = nativeCoverage.getTotalCoveredStatements()) + + selector.update(state = left) + + assertEquals(expected = listOf(left.currentStatement), actual = evaluated) + assertSame(expected = right, actual = selector.peek()) + evaluated.clear() + + val fork = mockState(id = 3u, startMethod = "method", startInstruction = 2) + selector.add(states = listOf(fork)) + + assertEquals(expected = listOf(fork.currentStatement), actual = evaluated) + assertSame(expected = right, actual = selector.peek()) + assertEquals(expected = setOf(left, right, fork), actual = selector.drain().toHashSet()) + } + + @Test + fun `native coverage still removes targets from the supplied calculator`() { + val cfg = CfgStatisticsImpl(graph) + val goal = TestInstruction(method = "method", offset = 1) + val calculator = CallStackDistanceCalculator( + targets = listOf(goal), + cfgStatistics = cfg, + applicationGraph = graph, + ) + val state = mockState(id = 1u, startMethod = "method", startInstruction = 1) + every { state.pathNode } returns PathNode.root() + goal + val coverage = CoverageStatistics( + methods = setOf("method"), + applicationGraph = graph, + ) + val selector = createPathSelector( + initialState = state, + options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + ), + applicationGraph = graph, + coverageStatisticsFactory = { coverage }, + cfgStatisticsFactory = { cfg }, + coverageDistanceCalculatorFactory = { calculator }, + ) + + coverage.onStateTerminated(state = state, stateReachable = true) + selector.update(state = state) + + assertEquals(expected = 1, actual = coverage.getTotalCoveredStatements()) + assertEquals( + expected = UInt.MAX_VALUE, + actual = calculator.calculateDistance(state.currentStatement, state.callStack), + ) + assertSame(expected = state, actual = selector.peek()) + assertEquals(expected = listOf(state), actual = selector.drain().toList()) + } + + @Test + fun `covered prefixes can still lead to uncovered successors`() { + val goal = TestInstruction(method = "method", offset = 6) + val prefix = mockState(id = 1u, startMethod = "method", startInstruction = 3) + val calculator = CallStackDistanceCalculator( + targets = listOf(prefix.currentStatement, goal), + cfgStatistics = CfgStatisticsImpl(graph), + applicationGraph = graph, + ) + + calculator.removeTarget(method = "method", statement = prefix.currentStatement) + + assertEquals( + expected = 3u, + actual = calculator.calculateDistance(prefix.currentStatement, prefix.callStack), + ) + } +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt index 548c40027b..60bece8260 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt @@ -571,6 +571,7 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { TsMachine( scene = scene, options = UMachineOptions( + pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY), stateCollectionStrategy = StateCollectionStrategy.ALL, randomSeed = manifest.seed, collectedStatesLimit = manifest.collectedStatesLimit, diff --git a/usvm-ts-fast-check/README.md b/usvm-ts-fast-check/README.md index 97bf0d95c6..ff5df9bdb9 100644 --- a/usvm-ts-fast-check/README.md +++ b/usvm-ts-fast-check/README.md @@ -12,14 +12,57 @@ remain in [`usvm-ts-pbt`](../usvm-ts-pbt/README.md). One c8 execution produces the existing source-mapped Istanbul statement report and raw V8 ranges. The bounded TypeScript branch converter reads those same raw ranges, the executed source snapshot, and the source map. It emits ordered `if` arms only when the original TypeScript points map back exactly, each arm has a distinct V8 execution -point, and the arm counts add up to the count at the condition. A supported `if` without `else` additionally needs -a single terminating `return` or `throw` in its true arm and a following statement that is reached only on false. +point, and the arm counts add up to the count at the condition. An `if` without `else` uses either a terminating +true arm and a distinct false successor, or a following join whose execution count equals the condition count. +In the latter case the false count is the condition count minus the true count. Missing points, early exits and +throwing conditions that violate this conservation rule remain unknown. Nested `if` statements are supported under those conditions. Ambiguous counts or ranges and unsupported constructs produce diagnostics; exact statement mappings remain available. Loops, `switch`, conditional expressions, logical short-circuit ranges, and function or script ranges are never reinterpreted as `if` arms. The converter does not instrument the TypeScript program or execute it a second time. -The resulting edges are coverage artifacts; target-selection integration belongs to #399/#355. +The DSL's `BOTH` mode uses exact admitted coverage to guide the original property search as described below. + +## PBT edge feedback in `BOTH` + +`DslPropertyRunner.run(program, engine = PropertyEngine.BOTH, configuration = ...)` first runs FastCheck and then +passes its confirmed source edges to the same USVM analysis that searches for a violation of the author checks. +Coverage is enabled automatically in this mode. The predicate, domains and precondition keep their original roles; +coverage affects scheduling only and adds no constraints. + +This mode collects V8 counters only during admitted predicate invocations, excluding the precondition, rejected +inputs, import initialization and shrinking trials. A synchronous worker handshake keeps synchronous precondition +and predicate calls uninterrupted. Each report carries a digest of the manifest and local TypeScript source files. +Absent, stale, unsupported and no-admission evidence produce distinct classifications. Only exact mapped `if` arms +provide known covered or uncovered edges; statement hits and missing branch records provide neither. + +The deterministic selector alternates a nearest known-uncovered edge priority with a fair original-objective turn. +Covered prefixes stay in the graph. Full edge coverage stops the coverage objective while property exploration +continues; statement saturation does not stop a property search. Distances follow calls and active return sites and +are scheduling overapproximations, not claims of feasibility. +Configurations using state merging or selector loop bounds retain their existing selector with an explicit +unsupported-feedback diagnostic; this first policy does not silently bypass those controls. + +When a completed property path crosses a new target, its input is replayed natively as a single explicit example: +no fallback generation and no shrinking. A rejected input, changed oracle result, incompatible source/runtime or +missing claimed edge leaves coverage unchanged. Confirmed additions immediately change subsequent selections in +the running machine. Exact branches first observed during replay also become eligible goals. Each edge has at most +two replay attempts with distinct inputs; failed targets remain listed +as uncovered after that limit. At least half of scheduling turns remain available to the original objective. + +Inspect `run.symbolic?.edgeGuidance` for initial coverage/goals, actual selected states and traversed goals, +evidence revisions, replay outcomes/additions, remaining goals and diagnostics. Selection history is bounded to +4096 entries with an explicit omitted count. `run.elapsedMillis` and `run.budgetMillis` report the shared wall-time +budget; replay entries report native replay costs. FastCheck receives at most one third of the total budget. +After frontend preparation, one third of the remaining time is reserved for final witness replay and shrinking; +feedback replays use at most one third of the symbolic allocation. Mapping, startup, search and replay use the +same monotonic deadline. Stop checks occur between interpreter steps and backend calls; an already-running solver +query, frontend conversion already in progress, or process shutdown can exceed the deadline and is included in +elapsed time. A frontend conversion is never started after the deadline; `symbolicSkippedDueToDeadline` reports +that no symbolic analysis ran, and `requireSuccess()` treats it as inconclusive. + +The admitted collector covers the main Node isolate only. This slice does not infer relations, change PBT +generation, retain a session between separate runner calls or implement the repeated two-way campaign of #355. Run the backend checks with: diff --git a/usvm-ts-fast-check/fast-check-adapter/package-lock.json b/usvm-ts-fast-check/fast-check-adapter/package-lock.json index 3db9388792..146c4e6c08 100644 --- a/usvm-ts-fast-check/fast-check-adapter/package-lock.json +++ b/usvm-ts-fast-check/fast-check-adapter/package-lock.json @@ -8,6 +8,7 @@ "name": "@usvm/fast-check-adapter", "version": "0.1.0", "dependencies": { + "@bcoe/v8-coverage": "1.0.2", "@jridgewell/trace-mapping": "0.3.31", "c8": "10.1.3", "fast-check": "4.9.0", diff --git a/usvm-ts-fast-check/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json index 3fcbf35f61..13635feb47 100644 --- a/usvm-ts-fast-check/fast-check-adapter/package.json +++ b/usvm-ts-fast-check/fast-check-adapter/package.json @@ -12,6 +12,7 @@ "test:compiled": "node --test dist/test/coverage-branches.test.js 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/observe-object.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 dist/test/class-coverage-source.test.js" }, "dependencies": { + "@bcoe/v8-coverage": "1.0.2", "@jridgewell/trace-mapping": "0.3.31", "c8": "10.1.3", "fast-check": "4.9.0", diff --git a/usvm-ts-fast-check/fast-check-adapter/src/coverage-branches.ts b/usvm-ts-fast-check/fast-check-adapter/src/coverage-branches.ts index 67d26044c2..936da4f7a6 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/coverage-branches.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/coverage-branches.ts @@ -353,7 +353,9 @@ function convertIf( if (trueBody === undefined) { return { kind: 'unsupported', reason: 'Empty true arm has no V8 execution point' }; } - if (falseBody === undefined) { + const following = followingStatement(node); + const joinsAfterIf = node.elseStatement === undefined && falseBody === undefined && following !== undefined; + if (falseBody === undefined && !joinsAfterIf) { const reason = node.elseStatement === undefined ? 'An if without else requires a terminating true arm and a following false successor' : 'Empty false arm has no V8 execution point'; @@ -363,7 +365,14 @@ function convertIf( const conditionHits = countAt(node.getStart(ast), ast, coverage, map); const trueHits = countAt(trueBody.getStart(ast), ast, coverage, map); - const falseHits = countAt(falseBody.getStart(ast), ast, coverage, map); + // For a non-terminating true arm, the following statement is a join, not the + // false edge. Conservation is valid only when every condition evaluation + // reaches that join; a throwing condition/arm makes the record ambiguous. + const joinHits = joinsAfterIf ? countAt(following.getStart(ast), ast, coverage, map) : undefined; + const falseHits = joinsAfterIf + ? conditionHits !== undefined && joinHits === conditionHits && trueHits !== undefined + ? conditionHits - trueHits : undefined + : countAt((falseBody as ts.Statement).getStart(ast), ast, coverage, map); if (conditionHits === undefined || trueHits === undefined || falseHits === undefined || trueHits < 0 || falseHits < 0 || trueHits + falseHits !== conditionHits) { @@ -417,13 +426,15 @@ function countAt( const offset = lineLengths.slice(0, generated.line - 1).reduce((sum, length) => sum + length + 1, 0) + generated.column; - const functions = coverage.script.functions.filter(fn => fn.isBlockCoverage && + const functions = coverage.script.functions.filter(fn => fn.ranges.length > 0 && contains(fn.ranges[0] as V8Range, offset)); const orderedFunctions = functions.sort((left, right) => rangeLength(left.ranges[0] as V8Range) - rangeLength(right.ranges[0] as V8Range), ); const functionCoverage = orderedFunctions[0]; - if (functionCoverage === undefined) return undefined; + // A non-invoked inner function has no block counters. Its containing script's + // counters describe initialization, not execution of that function's body. + if (functionCoverage === undefined || !functionCoverage.isBlockCoverage) return undefined; if (orderedFunctions[1] !== undefined && rangeLength(orderedFunctions[1].ranges[0] as V8Range) === rangeLength(functionCoverage.ranges[0] as V8Range)) { return undefined; @@ -452,6 +463,10 @@ function falseSuccessor(node: ts.IfStatement): ts.Statement | undefined { (ts.isReturnStatement(soleStatement) || ts.isThrowStatement(soleStatement)); if (!terminates) return undefined; + return followingStatement(node); +} + +function followingStatement(node: ts.IfStatement): ts.Statement | undefined { const parent = node.parent; if (!ts.isBlock(parent) && !ts.isSourceFile(parent)) return undefined; diff --git a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts index fba52cc37a..b2fd4351b1 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts @@ -1,4 +1,4 @@ -export type AdapterDiagnosticKind = 'invalid-request' | 'entry-point'; +export type AdapterDiagnosticKind = 'invalid-request' | 'entry-point' | 'coverage'; export interface AdapterDiagnosticDescriptor { readonly kind: AdapterDiagnosticKind; diff --git a/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts b/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts index f4b8714dba..93166119d6 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts @@ -1,3 +1,4 @@ +import type { ExecutionCoverage } from './execution-coverage.js'; import { performance } from 'node:perf_hooks'; import fc from 'fast-check'; import type { Parameters, RunDetails } from 'fast-check'; @@ -76,6 +77,8 @@ export interface FastCheckExecutionRequest { timeoutMillis: number; examples: TaggedJsValue[][]; observationRequest?: ObservationRequest; + admittedCoverage?: boolean; + exactReplay?: boolean; } export interface FastCheckFailureDetails { @@ -106,7 +109,7 @@ export interface FastCheckExecutionSuccess { result: FastCheckRunResult; } -export async function executeProperty(requestValue: unknown): Promise { +export async function executeProperty(requestValue: unknown, coverage?: ExecutionCoverage): Promise { const request = validateRequest(requestValue); const startedAt = performance.now(); const recorder = request.observationRequest === undefined @@ -127,12 +130,12 @@ export async function executeProperty(requestValue: unknown): Promise request.replayPath === undefined ? tracker?.phaseOf(values) ?? 'unknown' : 'replay'; - const property = buildProperty(arbitrary, predicate, precondition, contractErrors, recorder, phaseOf); + const property = buildProperty(arbitrary, predicate, precondition, contractErrors, recorder, phaseOf, coverage); const parameters = buildParameters(request, tracker); const details = await checkProperty(property, parameters, request.replayPath); @@ -158,6 +161,7 @@ function buildProperty( contractErrors: ContractErrorState, recorder: ObservationRecorder | undefined, phaseOf: (values: JsConcreteValue[]) => 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown', + coverage: ExecutionCoverage | undefined, ): fc.IProperty<[JsConcreteValue[]]> | fc.IAsyncProperty<[JsConcreteValue[]]> { const asynchronous = predicate.executionKind === 'async' || precondition?.executionKind === 'async'; let selectedCheckId: string | undefined; @@ -166,7 +170,7 @@ function buildProperty( return fc.asyncProperty(arbitrary, (values: JsConcreteValue[]): Promise => preserveAsyncContractError( contractErrors, async () => { - const result = await invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values)); + const result = await invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values), coverage); if (result === null) fc.pre(false); return result; @@ -179,7 +183,7 @@ function buildProperty( () => { let result: boolean | null; try { - result = invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values)) as boolean | null; + result = invokePropertyOnce(values, predicate, precondition, recorder, phaseOf(values), coverage) as boolean | null; } catch (error: unknown) { if (isNamedCheckFailure(error)) { selectedCheckId ??= error.checkId; @@ -202,6 +206,7 @@ function invokePropertyOnce( precondition: LoadedEntryPoint | undefined, recorder: ObservationRecorder | undefined, phase: 'generation' | 'explicit' | 'shrink' | 'replay' | 'unknown', + coverage?: ExecutionCoverage, ): boolean | null | Promise { const invocationValues = cloneArguments(values); const invoke = (): boolean | null | Promise => { @@ -218,6 +223,9 @@ function invokePropertyOnce( throw error; } + const collect = coverage?.admittedOnly === true && phase !== 'shrink' && phase !== 'unknown'; + if (collect) coverage.reset(); + try { const result = await predicate.invoke(invocationValues); recorder?.finish('admitted', result ? 'holds' : 'false'); @@ -226,6 +234,8 @@ function invokePropertyOnce( } catch (error: unknown) { recorder?.finish('admitted', predicateExceptionOutcome(error)); throw error; + } finally { + if (collect) coverage.admit(); } })(); } @@ -241,6 +251,9 @@ function invokePropertyOnce( throw error; } + const collect = coverage?.admittedOnly === true && phase !== 'shrink' && phase !== 'unknown'; + if (collect) coverage.reset(); + try { const result = predicate.invoke(invocationValues) as boolean; recorder?.finish('admitted', result ? 'holds' : 'false'); @@ -249,6 +262,8 @@ function invokePropertyOnce( } catch (error: unknown) { recorder?.finish('admitted', predicateExceptionOutcome(error)); throw error; + } finally { + if (collect) coverage.admit(); } }; @@ -403,6 +418,10 @@ function buildParameters( if (request.seed !== undefined) parameters.seed = request.seed; if (request.replayPath !== undefined) parameters.path = request.replayPath; + if (request.exactReplay) { + parameters.maxSkipsPerRun = 0; + parameters.endOnFailure = true; + } return parameters; } @@ -582,6 +601,14 @@ function validateRequest(value: unknown): FastCheckExecutionRequest { if (request.tsconfig !== undefined) validated.tsconfig = request.tsconfig as string; if (request.seed !== undefined) validated.seed = request.seed as number; if (request.replayPath !== undefined) validated.replayPath = request.replayPath as string; + if (request.admittedCoverage === true) validated.admittedCoverage = true; + if (request.exactReplay === true) { + if (request.numRuns !== 1 || examples.length !== 1 || request.replayPath !== undefined) { + throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Exact replay requires one explicit example', 'exactReplay'); + } + validated.exactReplay = true; + } + if (request.observationRequest !== undefined) { validated.observationRequest = validateObservationRequest(request.observationRequest, manifest); } diff --git a/usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts b/usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts index f9746a5bf3..a752e13142 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/execution-cli.ts @@ -13,13 +13,19 @@ interface FastCheckExecutionFailure { const writeProtocolOutput = process.stdout.write.bind(process.stdout) as typeof process.stdout.write; process.stdout.write = process.stderr.write.bind(process.stderr) as typeof process.stdout.write; -const coverage = await startExecutionCoverage(); +let request: unknown; +let inputError: unknown; +try { request = parseRequest(await readStdin()); } catch (error) { inputError = error; } +const admittedOnly = request !== null && typeof request === 'object' && + (request as Record).admittedCoverage === true; +const timeoutMillis = request !== null && typeof request === 'object' + ? (request as Record).timeoutMillis : undefined; +const coverage = await startExecutionCoverage(admittedOnly, typeof timeoutMillis === 'number' ? timeoutMillis : 60_000); try { let response: FastCheckExecutionSuccess | FastCheckExecutionFailure; try { - const request = parseRequest(await readStdin()); - - response = await executeProperty(request); + if (inputError !== undefined) throw inputError; + response = await executeProperty(request, coverage); } catch (error: unknown) { if (!(error instanceof ProtocolError)) throw error; diff --git a/usvm-ts-fast-check/fast-check-adapter/src/execution-coverage-worker.ts b/usvm-ts-fast-check/fast-check-adapter/src/execution-coverage-worker.ts index 0f821d5e85..0f1ed38a83 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/execution-coverage-worker.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/execution-coverage-worker.ts @@ -1,8 +1,10 @@ import { Session, type Debugger, type Profiler } from 'node:inspector'; -import { parentPort } from 'node:worker_threads'; +import { parentPort, workerData } from 'node:worker_threads'; +import { mergeProcessCovs } from '@bcoe/v8-coverage'; export interface ExecutionCoverageSnapshot { kind: 'coverage'; + admittedInvocations: number; result: Profiler.ScriptCoverage[]; scripts: Record; } @@ -12,13 +14,26 @@ if (port === null) throw new Error('Coverage collector requires a worker'); const session = new Session(); const parsedScripts = new Map(); +const scriptIds = new Map(); session.connectToMainThread(); session.on('Debugger.scriptParsed', ({ params }) => parsedScripts.set(params.scriptId, params)); // Keep the port referenced while inspector replies are pending. A one-shot // listener would let this worker exit before an asynchronous snapshot finishes. -port.on('message', () => { - void takeSnapshot().then(snapshot => port.postMessage(snapshot)).catch(error => { +let admitted: Profiler.ScriptCoverage[] = []; +let admittedInvocations = 0; + +const completion = new Int32Array(workerData.completion); +port.on('message', (command: 'reset' | 'admit' | 'take') => { + void takeSnapshot(command).then(snapshot => { + if (command === 'take') port.postMessage(snapshot); + else { + Atomics.store(completion, 0, 1); + Atomics.notify(completion, 0); + } + }).catch(error => { + Atomics.store(completion, 0, -1); + Atomics.notify(completion, 0); throw error; }); }); @@ -29,16 +44,22 @@ await post('Profiler.startPreciseCoverage', { callCount: true, detailed: true }) port.postMessage('ready'); -async function takeSnapshot(): Promise { +async function takeSnapshot(command: 'reset' | 'admit' | 'take'): Promise { const coverage = await post('Profiler.takePreciseCoverage'); + for (const script of coverage.result) scriptIds.set(script.url, script.scriptId); + if (command === 'admit') { + admitted = mergeProcessCovs([{ result: admitted }, { result: coverage.result }]).result; + admittedInvocations += 1; + } + const result = command === 'take' && workerData.admittedOnly === true ? admitted : coverage.result; const scripts: ExecutionCoverageSnapshot['scripts'] = Object.create(null); - for (const script of coverage.result) { + for (const script of command === 'take' ? result : []) { if (!script.url.startsWith('file:')) continue; const { scriptSource } = await post( - 'Debugger.getScriptSource', { scriptId: script.scriptId }, + 'Debugger.getScriptSource', { scriptId: scriptIds.get(script.url) ?? script.scriptId }, ); - const sourceMapUrl = parsedScripts.get(script.scriptId)?.sourceMapURL; + const sourceMapUrl = parsedScripts.get(scriptIds.get(script.url) ?? script.scriptId)?.sourceMapURL; scripts[script.url] = { // V8 offsets are UTF-16 offsets. Keep CR in a CRLF line, like Node's cache. lineLengths: scriptSource.split(/[\n\u2028\u2029]/).map(line => line.length), @@ -46,10 +67,12 @@ async function takeSnapshot(): Promise { }; } - await post('Profiler.stopPreciseCoverage'); - session.disconnect(); + if (command === 'take') { + await post('Profiler.stopPreciseCoverage'); + session.disconnect(); + } - return { kind: 'coverage', result: coverage.result, scripts }; + return { kind: 'coverage', result, scripts, admittedInvocations }; } function post(method: string, params: object = {}): Promise { diff --git a/usvm-ts-fast-check/fast-check-adapter/src/execution-coverage.ts b/usvm-ts-fast-check/fast-check-adapter/src/execution-coverage.ts index 3931dd187b..ae613942a9 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/execution-coverage.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/execution-coverage.ts @@ -2,23 +2,31 @@ import { mkdirSync, writeFileSync } from 'node:fs'; import { findSourceMap } from 'node:module'; import path from 'node:path'; import { Worker } from 'node:worker_threads'; +import { performance } from 'node:perf_hooks'; +import { protocolError } from './js-value.js'; import type { ExecutionCoverageSnapshot } from './execution-coverage-worker.js'; import { stringifyProtocolJson } from './protocol-json.js'; export interface ExecutionCoverage { + readonly admittedOnly: boolean; + reset(): void; + admit(): void; write(): Promise; close(): Promise; } /** Collect coverage without invoking serializers installed by the source under test. */ -export async function startExecutionCoverage(): Promise { +export async function startExecutionCoverage(admittedOnly = false, timeoutMillis = 60_000): Promise { const rawDirectory = process.env.USVM_V8_COVERAGE_DIRECTORY; if (rawDirectory === undefined || rawDirectory.length === 0) return undefined; + const deadline = performance.now() + timeoutMillis; // Inspector's protocol serializer also consults inherited toJSON, so its // session lives in a worker that never executes the source under test. + const completion = new Int32Array(new SharedArrayBuffer(Int32Array.BYTES_PER_ELEMENT)); const worker = new Worker(new URL('./execution-coverage-worker.js', import.meta.url), { env: { ...process.env, NODE_V8_COVERAGE: '' }, + workerData: { admittedOnly, completion: completion.buffer }, }); let workerFailure: Error | undefined; let workerExited = false; @@ -61,21 +69,42 @@ export async function startExecutionCoverage(): Promise { + const pending = receive(); + worker.postMessage(command); + const report = await pending; + if (report === 'ready') throw new Error('Coverage collector did not produce a snapshot'); + return report; + } + + // A synchronous handshake preserves the uninterrupted precondition/predicate + // call: yielding here could run user microtasks and change its result. + function snapshotSync(command: 'reset' | 'admit'): void { + Atomics.store(completion, 0, 0); + worker.postMessage(command); + const remaining = Math.max(0, deadline - performance.now()); + const outcome = Atomics.wait(completion, 0, 0, remaining); + if (outcome === 'timed-out' || Atomics.load(completion, 0) !== 1) { + throw protocolError({ kind: 'coverage', code: 'coverage.snapshot.failed' }, + 'Admitted coverage snapshot failed or exhausted the run deadline', 'coverage'); + } + } return { + admittedOnly, + reset(): void { snapshotSync('reset'); }, + admit(): void { snapshotSync('admit'); }, async write(): Promise { // Descendants already hold their inherited environment. Clear the main // process before coverage is drained or any shutdown hook can serialize it. delete process.env.NODE_V8_COVERAGE; - const pending = receive(); - worker.postMessage('take'); - const snapshot = await pending; - if (snapshot === 'ready') throw new Error('Coverage collector did not produce a snapshot'); + const reportSnapshot = await snapshot('take'); const sourceMapCache: Record = Object.create(null); - for (const [url, script] of Object.entries(snapshot.scripts)) { + for (const [url, script] of Object.entries(reportSnapshot.scripts)) { const sourceMap = findSourceMap(url); if (sourceMap !== undefined || script.sourceMapUrl !== undefined) { sourceMapCache[url] = { @@ -86,8 +115,11 @@ export async function startExecutionCoverage(): Promise { diff --git a/usvm-ts-fast-check/fast-check-adapter/src/v8-coverage.d.ts b/usvm-ts-fast-check/fast-check-adapter/src/v8-coverage.d.ts new file mode 100644 index 0000000000..e685feb73d --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/v8-coverage.d.ts @@ -0,0 +1,7 @@ +declare module '@bcoe/v8-coverage' { + import type { Profiler } from 'node:inspector'; + + export function mergeProcessCovs(reports: { result: Profiler.ScriptCoverage[] }[]): { + result: Profiler.ScriptCoverage[]; + }; +} diff --git a/usvm-ts-fast-check/fast-check-adapter/test/coverage-branches.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/coverage-branches.test.ts index 612c2e6441..0c0020a047 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/coverage-branches.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/coverage-branches.test.ts @@ -288,6 +288,74 @@ ${calls} } }); +test('if without else measures the missing edge through conservation at a shared join', async () => { + for (const [calls, expected] of [ + ['subject(1);', [1, 0]], + ['subject(-1);', [0, 1]], + ['subject(1); subject(-1);', [1, 1]], + ] as const) { + const fixture = await runCoverage(` +function subject(value: number): number { + let result = 1; + if (value > 0) { result = 1; } + return result; +} +${calls} +`); + try { + const report = await convertV8IfBranches(fixture.raw, [fixture.root]); + + assert.deepEqual(report.files[0]?.branches[0]?.arms.map(arm => arm.hits), expected); + assert.deepEqual(report.diagnostics, []); + } finally { + await rm(fixture.root, { recursive: true, force: true }); + } + } +}); + +test('a throwing condition cannot create a false-edge count at a shared join', async () => { + const fixture = await runCoverage(` +function gate(value: number): boolean { if (value < 0) throw new Error('expected'); return value > 0; } +function subject(value: number): number { + let result = 1; + if (gate(value)) { result = 1; } + return result; +} +for (const value of [-1, 1]) { try { subject(value); } catch {} } +`); + try { + const report = await convertV8IfBranches(fixture.raw, [fixture.root]); + + assert.equal(report.files[0]?.branches.some(branch => branch.location.start.line === 5), false); + assert.ok(report.diagnostics.some(entry => entry.code === 'coverage.branch.ambiguous')); + } finally { + await rm(fixture.root, { recursive: true, force: true }); + } +}); + +test('an uncalled function cannot inherit exact if counts from its containing script', async () => { + const fixture = await runCoverage(` +function neverCalled(value: number): number { + let result = 0; + if (value > 0) { result = 1; } + return result; +} +function subject(value: number): number { + if (value > 0) { return 1; } else { return 2; } +} +subject(1); +`); + try { + const report = await convertV8IfBranches(fixture.raw, [fixture.root]); + + assert.deepEqual(report.files[0]?.branches.map(branch => branch.arms.map(arm => arm.hits)), [[1, 0]]); + assert.equal(report.files[0]?.branches.some(branch => branch.location.start.line === 4), false); + assert.ok(report.diagnostics.some(entry => entry.code === 'coverage.branch.ambiguous')); + } finally { + await rm(fixture.root, { recursive: true, force: true }); + } +}); + test('duplicate V8 scripts remain ambiguous', async () => { const fixture = await runCoverage(` function subject(value: number): number { diff --git a/usvm-ts-fast-check/fast-check-adapter/test/execution-cli.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/execution-cli.test.ts index 767df48fe5..def9e9d338 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/execution-cli.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/execution-cli.test.ts @@ -12,6 +12,129 @@ import { convertV8IfBranches } from '../src/coverage-branches.js'; const cliPath = fileURLToPath(new URL('../src/execution-cli.js', import.meta.url)); const coverageLauncher = fileURLToPath(new URL('../src/coverage-launcher.js', import.meta.url)); +test('admitted coverage excludes rejected preconditions and keeps sync predicate semantics', async () => { + const sourceRoot = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-admitted-coverage-'))); + const raw = path.join(sourceRoot, 'raw'); + try { + await writeFile(path.join(sourceRoot, 'helper.ts'), ` +export function helper(value: boolean): number { + if (value) { return 1; } + else { return 2; } +} +`); + await writeFile(path.join(sourceRoot, 'property.ts'), ` +import { helper } from './helper'; +let changed = false; +export function precondition(value: boolean): boolean { + helper(!value); + queueMicrotask(() => { changed = true; }); + return value; +} +export function predicate(_value: boolean): boolean { return helper(false) === 2 && !changed; } +`); + const request = executionRequest(sourceRoot); + const manifest = request.manifest as Record; + manifest.inputs = [{ name: 'value', domain: { kind: 'boolean' } }]; + manifest.precondition = { module: 'property.ts', exportName: 'precondition', executionKind: 'sync' }; + request.examples = [[{ kind: 'boolean', value: false }], [{ kind: 'boolean', value: true }]]; + request.admittedCoverage = true; + request.timeoutMillis = 5_000; + + const invocation = await invokeCli(JSON.stringify(request), { coverageDirectory: raw, timeoutMillis: 10_000 }); + const response = JSON.parse(invocation.stdout) as { status: string; result: { status: string; numSkips: number } }; + const branches = await convertV8IfBranches(raw, [sourceRoot]); + + assert.equal(invocation.exitCode, 0, invocation.stderr); + assert.equal(response.status, 'ok'); + assert.equal(response.result.status, 'success'); + assert.equal(response.result.numSkips, 1); + assert.deepEqual(branches.files.find(file => file.path.endsWith('/helper.ts'))?.branches + .map(branch => branch.arms.map(arm => arm.hits)), [[0, 1]]); + assert.equal(await readFile(path.join(raw, 'admitted-count.txt'), 'utf8'), '1'); + } finally { + await rm(sourceRoot, { recursive: true, force: true }); + } +}); + +test('admitted snapshots merge both branch outcomes without counting shrink trials', async () => { + const sourceRoot = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-admitted-merge-'))); + try { + await writeFile(path.join(sourceRoot, 'helper.ts'), ` +export function helper(value: boolean): number { + if (value) { return 1; } + else { return 2; } +} +`); + await writeFile(path.join(sourceRoot, 'property.ts'), ` +import { helper } from './helper'; +export function predicate(value: boolean): boolean { helper(value); return true; } +export function failing(value: number): boolean { helper(value === 0); return value === 0; } +`); + const request = executionRequest(sourceRoot); + const manifest = request.manifest as Record; + manifest.inputs = [{ name: 'value', domain: { kind: 'boolean' } }]; + request.examples = [[{ kind: 'boolean', value: true }], [{ kind: 'boolean', value: false }]]; + request.admittedCoverage = true; + request.numRuns = 2; + request.timeoutMillis = 5_000; + const raw = path.join(sourceRoot, 'raw'); + + const invocation = await invokeCli(JSON.stringify(request), { coverageDirectory: raw, timeoutMillis: 10_000 }); + const branches = await convertV8IfBranches(raw, [sourceRoot]); + + assert.equal(invocation.exitCode, 0, invocation.stderr); + assert.deepEqual(branches.files.find(file => file.path.endsWith('/helper.ts'))?.branches + .map(branch => branch.arms.map(arm => arm.hits)), [[1, 1]]); + assert.equal(await readFile(path.join(raw, 'admitted-count.txt'), 'utf8'), '2'); + + manifest.inputs = [{ name: 'value', domain: { kind: 'integer', min: 0, max: 10 } }]; + manifest.predicate = { module: 'property.ts', exportName: 'failing', executionKind: 'sync' }; + request.examples = [[{ kind: 'number', value: 'finite', bits: '4024000000000000' }]]; + request.numRuns = 1; + const shrinkRaw = path.join(sourceRoot, 'shrink-raw'); + const shrink = await invokeCli(JSON.stringify(request), { coverageDirectory: shrinkRaw, timeoutMillis: 10_000 }); + const shrinkResponse = JSON.parse(shrink.stdout) as { result: { numShrinks: number } }; + const shrinkBranches = await convertV8IfBranches(shrinkRaw, [sourceRoot]); + + assert.equal(shrink.exitCode, 0, shrink.stderr); + assert.ok(shrinkResponse.result.numShrinks > 0); + assert.deepEqual(shrinkBranches.files.find(file => file.path.endsWith('/helper.ts'))?.branches + .map(branch => branch.arms.map(arm => arm.hits)), [[0, 1]]); + assert.equal(await readFile(path.join(shrinkRaw, 'admitted-count.txt'), 'utf8'), '1'); + } finally { + await rm(sourceRoot, { recursive: true, force: true }); + } +}); + +test('exact replay stops on a rejected example without generated fallback', async () => { + const sourceRoot = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-exact-coverage-'))); + try { + await writeFile(path.join(sourceRoot, 'property.ts'), ` +export function precondition(value: boolean): boolean { return value; } +export function predicate(_value: boolean): boolean { return false; } +`); + const request = executionRequest(sourceRoot); + const manifest = request.manifest as Record; + manifest.inputs = [{ name: 'value', domain: { kind: 'boolean' } }]; + manifest.precondition = { module: 'property.ts', exportName: 'precondition', executionKind: 'sync' }; + request.examples = [[{ kind: 'boolean', value: false }]]; + request.exactReplay = true; + + const invocation = await invokeCli(JSON.stringify(request)); + const response = JSON.parse(invocation.stdout) as { result: { + numRuns: number; numSkips: number; counterexample: unknown; failure: { kind: string }; + } }; + + assert.equal(invocation.exitCode, 0, invocation.stderr); + assert.equal(response.result.numRuns, 0); + assert.equal(response.result.numSkips, 1); + assert.equal(response.result.counterexample, null); + assert.equal(response.result.failure.kind, 'precondition-exhausted'); + } finally { + await rm(sourceRoot, { recursive: true, force: true }); + } +}); + test('execution CLI emits one successful response document', async () => { const sourceRoot = await realpath(await mkdtemp(path.join(tmpdir(), 'usvm-execution-cli-'))); try { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt index 9b32e22127..dd9fd60826 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt @@ -3,10 +3,13 @@ package org.usvm.ts.pbt.dsl import kotlinx.serialization.json.Json import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions import org.usvm.ts.pbt.backend.ProjectionCapability import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.PropertyFailureDetails import org.usvm.ts.pbt.backend.PropertyFailureKind import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunResult @@ -16,12 +19,14 @@ import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.mapping.PropertyEtsMapper import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.usvm.UsvmCoverageFeedback import org.usvm.ts.pbt.usvm.UsvmPropertySearchResult import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus import org.usvm.ts.pbt.usvm.UsvmPropertySearcher import java.nio.file.Files import java.nio.file.Path import kotlin.time.Duration.Companion.milliseconds +import kotlin.time.TimeSource /** Selects execution without changing the author property or its JavaScript semantics. */ enum class PropertyEngine { @@ -36,6 +41,9 @@ data class DslPropertyRun( val concrete: PropertyRunResult?, val symbolic: UsvmPropertySearchResult?, val symbolicReplay: PropertyRunResult?, + val elapsedMillis: Long = 0, + val budgetMillis: Long? = null, + val symbolicSkippedDueToDeadline: Boolean = false, ) { fun requireSuccess() { val violation = listOfNotNull(concrete, symbolicReplay).firstOrNull { @@ -46,8 +54,13 @@ data class DslPropertyRun( } val concreteFailure = concrete?.status == PropertyRunStatus.FAILURE val incompleteSearch = symbolic != null && symbolic.status != UsvmPropertySearchStatus.NO_VIOLATION_REACHED - if (concreteFailure || incompleteSearch) { - throw DslPropertyExecutionError(this, "Property run was inconclusive: ${concrete?.failure ?: symbolic}") + if (concreteFailure || incompleteSearch || symbolicSkippedDueToDeadline) { + val message = if (symbolicSkippedDueToDeadline) { + "The total deadline expired before symbolic analysis could start" + } else { + "Property run was inconclusive: ${concrete?.failure ?: symbolic}" + } + throw DslPropertyExecutionError(this, message) } } @@ -100,6 +113,9 @@ class DslPropertyRunner(sourceRoots: List) { engine: PropertyEngine = PropertyEngine.FAST_CHECK, configuration: PropertyRunConfiguration = PropertyRunConfiguration(), ): DslPropertyRun { + val started = TimeSource.Monotonic.markNow() + fun remainingMillis(): Long = configuration.timeoutMillis - started.elapsedNow().inWholeMilliseconds + val directory = Files.createTempDirectory("usvm-kotlin-property-") try { val compiled = PropertyTypeScriptCompiler().compile( @@ -112,26 +128,67 @@ class DslPropertyRunner(sourceRoots: List) { copySources(directory) val sourceRoots = listOf(directory) val backend = FastCheckBackend(sourceRoots = sourceRoots) + val hybridConfiguration = if (engine == PropertyEngine.BOTH) { + val request = configuration.coverageRequest ?: PropertyCoverageRequest() + configuration.copy( + coverageRequest = request.copy(admittedOnly = true), + ) + } else { + configuration + } val concrete = if (engine != PropertyEngine.USVM) { - backend.run(property = compiled.definition, configuration = configuration) + val concreteBudget = if (engine == PropertyEngine.BOTH) { + minOf(remainingMillis(), maxOf(1L, configuration.timeoutMillis / CONCRETE_BUDGET_DIVISOR)) + } else { + remainingMillis() + } + if (concreteBudget <= 0L) { + exhaustedConcreteRun(compiled, configuration, started.elapsedNow().inWholeMilliseconds) + } else { + backend.run( + property = compiled.definition, + configuration = hybridConfiguration.copy(timeoutMillis = concreteBudget), + ) + } } else { null } val symbolic = if (engine != PropertyEngine.FAST_CHECK) { - search(compiled, directory, sourceRoots, configuration) + search( + compiled = compiled, + directory = directory, + sourceRoots = sourceRoots, + configuration = hybridConfiguration, + concrete = concrete, + backend = backend, + remainingMillis = ::remainingMillis, + ) } else { null } val candidate = symbolic?.inputs - val replay = if (candidate != null) { + val replay = if (candidate != null && remainingMillis() > 0) { backend.run( property = compiled.definition, - configuration = configuration.copy(replayPath = null, examples = listOf(candidate), numRuns = 1), + configuration = configuration.copy( + replayPath = null, + examples = listOf(candidate), + numRuns = 1, + timeoutMillis = remainingMillis().coerceAtLeast(1L), + ), ) } else { null } - return DslPropertyRun(compiled, concrete, symbolic, replay) + return DslPropertyRun( + property = compiled, + concrete = concrete, + symbolic = symbolic, + symbolicReplay = replay, + elapsedMillis = started.elapsedNow().inWholeMilliseconds, + budgetMillis = configuration.timeoutMillis, + symbolicSkippedDueToDeadline = engine != PropertyEngine.FAST_CHECK && symbolic == null, + ) } finally { Files.walk(directory).use { paths -> paths.sorted(Comparator.reverseOrder()).forEach(Files::deleteIfExists) @@ -144,21 +201,90 @@ class DslPropertyRunner(sourceRoots: List) { directory: Path, sourceRoots: List, configuration: PropertyRunConfiguration, - ): UsvmPropertySearchResult { + concrete: PropertyRunResult?, + backend: FastCheckBackend, + remainingMillis: () -> Long, + ): UsvmPropertySearchResult? { + if (remainingMillis() <= 0L) return null + val scene = loadEtsProjectAutoConvert(directory, provider = EtsIrProvider.TS_FRONTEND) + if (remainingMillis() <= 0L) return null + val manifest = compiled.definition.toManifest() - val mapping = PropertyEtsMapper(scene = scene, sourceRoots = sourceRoots).map(manifest) + val mapping = PropertyEtsMapper(scene = scene, sourceRoots = sourceRoots).map(manifest, concrete?.coverage) + val remainingBudgetMillis = remainingMillis() + if (remainingBudgetMillis <= 0L) return null + + val finalReplayReserveMillis = remainingBudgetMillis / FINAL_REPLAY_BUDGET_DIVISOR + val searchBudgetMillis = remainingBudgetMillis - finalReplayReserveMillis + fun symbolicRemainingMillis(): Long = remainingMillis() - finalReplayReserveMillis + val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), solverType = SolverType.YICES, - timeout = configuration.timeoutMillis.milliseconds, + timeout = searchBudgetMillis.milliseconds, ) - return UsvmPropertySearcher(scene = scene, machineOptions = options).search( + val replayBudgetMillis = searchBudgetMillis / FEEDBACK_REPLAY_BUDGET_DIVISOR + var spentReplayMillis = 0L + val feedback = if (concrete != null) { + UsvmCoverageFeedback(initialCoverage = concrete.coverage) { inputs -> + val replayRemaining = minOf(symbolicRemainingMillis(), replayBudgetMillis - spentReplayMillis) + if (replayRemaining <= 0L) { + null + } else { + val replayStarted = TimeSource.Monotonic.markNow() + try { + backend.run( + property = compiled.definition, + configuration = configuration.copy( + replayPath = null, + examples = listOf(inputs), + numRuns = 1, + timeoutMillis = replayRemaining, + exactReplay = true, + ), + ) + } finally { + spentReplayMillis += replayStarted.elapsedNow().inWholeMilliseconds + } + } + } + } else { + null + } + return UsvmPropertySearcher( + scene = scene, + machineOptions = options, + deadlineReached = { symbolicRemainingMillis() <= 0L }, + ).search( manifest = manifest, mapping = mapping, concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + coverageFeedback = feedback, ) } + private fun exhaustedConcreteRun( + compiled: CompiledDslProperty, + configuration: PropertyRunConfiguration, + elapsedMillis: Long, + ) = PropertyRunResult( + propertyId = compiled.definition.id, + status = PropertyRunStatus.FAILURE, + seed = configuration.seed ?: 0, + replayPath = null, + counterexample = null, + numRuns = 0, + numSkips = 0, + numShrinks = 0, + failure = PropertyFailureDetails( + kind = PropertyFailureKind.TIMEOUT, + errorName = "HybridDeadlineExceeded", + message = "The total property deadline expired before the concrete run", + ), + executionTimeMillis = elapsedMillis, + ) + private fun resolveModule(module: String, directory: Path): String { val modulePath = Path.of(module) val normalized = !modulePath.isAbsolute && '\\' !in module && @@ -199,6 +325,9 @@ class DslPropertyRunner(sourceRoots: List) { private companion object { const val GENERATED_MODULE = "__usvm_kotlin_property.ts" + const val CONCRETE_BUDGET_DIVISOR = 3L + const val FEEDBACK_REPLAY_BUDGET_DIVISOR = 3L + const val FINAL_REPLAY_BUDGET_DIVISOR = 3L val EXCLUDED_DIRECTORIES = setOf("node_modules", ".git", ".gradle", "build") } } diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt index 3fc53edcbf..7510d63640 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt @@ -1,10 +1,12 @@ package org.usvm.ts.pbt.fastcheck import org.usvm.ts.pbt.FastCheckDiagnosticCode +import org.usvm.ts.pbt.backend.CoverageDiagnostic import org.usvm.ts.pbt.backend.PropertyBasedTestingBackend import org.usvm.ts.pbt.backend.PropertyCoverageCapability import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.coverage.captureCoverageIdentity import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyDefinition @@ -44,6 +46,8 @@ class FastCheckBackend( validateConfiguration(property, configuration) val manifest = property.toManifest() + val admittedCoverage = configuration.coverageRequest?.admittedOnly == true + val identity = if (admittedCoverage) captureCoverageIdentity(manifest, sourceRoots) else null val sourceRootPaths = sourceRoots.map(Path::toString) val request = FastCheckExecutionRequest( manifest = manifest, @@ -56,9 +60,24 @@ class FastCheckBackend( examples = configuration.examples, observationRequest = configuration.observationRequest, coverageRequest = configuration.coverageRequest, + admittedCoverage = admittedCoverage, + exactReplay = configuration.exactReplay, ) - return client.check(request) + val result = client.check(request) + val coverage = result.coverage + if (identity == null || coverage == null) return result + + val unchanged = identity == captureCoverageIdentity(manifest, sourceRoots) + val diagnostics = if (unchanged) { + coverage.diagnostics + } else { + coverage.diagnostics + CoverageDiagnostic( + code = "coverage.source.stale", + message = "TypeScript sources changed during the concrete run", + ) + } + return result.copy(coverage = coverage.copy(identity = identity, diagnostics = diagnostics)) } private fun validateConfiguration( diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt index 25fd5c04f1..5a8a8dd095 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageSession.kt @@ -106,7 +106,13 @@ internal class FastCheckCoverageSession private constructor( ) } - return result.copy(coverage = artifact) + val admittedInvocations = if (coverageRequest.admittedOnly) { + Files.readString(workspace.rawDirectory.resolve("admitted-count.txt")).trim().toInt() + } else { + null + } + + return result.copy(coverage = artifact.copy(admittedInvocations = admittedInvocations)) } private fun propertyEntryPointPaths(): Set { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt index 53246a08fc..6722f4d231 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckExecutionProtocol.kt @@ -20,6 +20,8 @@ internal data class FastCheckExecutionRequest( val timeoutMillis: Long, val examples: List> = emptyList(), val observationRequest: PropertyObservationRequest? = null, + val admittedCoverage: Boolean = false, + val exactReplay: Boolean = false, @Transient val coverageRequest: PropertyCoverageRequest? = null, ) diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt index efa49c7a0b..dea8903b7a 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt @@ -10,12 +10,15 @@ import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus import kotlin.test.assertEquals import kotlin.test.assertFailsWith import kotlin.test.assertNotNull +import kotlin.test.assertNull import kotlin.test.assertTrue class KotlinPropertyDslTest { private val roots = listOf(testResourcesRoot().resolve("properties/dsl")) private val runner = DslPropertyRunner(sourceRoots = roots) - private val configuration = PropertyRunConfiguration(seed = 42, numRuns = 50, timeoutMillis = 10_000) + + // Functional assertions include cold frontend initialization in the runner's shared timeout. + private val configuration = PropertyRunConfiguration(seed = 42, numRuns = 50) @Test fun `calculator runs through existing concrete and symbolic execution`() { @@ -197,12 +200,39 @@ class KotlinPropertyDslTest { val run = runner.run(program = program, engine = PropertyEngine.BOTH, configuration = configuration) - assertEquals("unexpected", run.concrete?.failure?.checkId) - assertEquals("Error", run.concrete?.failure?.errorName) - assertEquals("unexpected", run.symbolicReplay?.failure?.checkId) + val diagnostic = run.executionDiagnostic() + assertEquals("unexpected", run.concrete?.failure?.checkId, diagnostic) + assertEquals("Error", run.concrete?.failure?.errorName, diagnostic) + val replay = assertNotNull(run.symbolicReplay, diagnostic) + assertEquals("unexpected", replay.failure?.checkId, diagnostic) assertFailsWith { run.requireSuccess() } } + @Test + fun `expired total deadline skips symbolic analysis and cannot report success`() { + val program = addition(exportName = "add") + + val run = runner.run( + program = program, + engine = PropertyEngine.USVM, + configuration = configuration.copy(timeoutMillis = 1), + ) + + val diagnostic = run.executionDiagnostic() + assertTrue(run.symbolicSkippedDueToDeadline, diagnostic) + assertNull(run.concrete, diagnostic) + assertNull(run.symbolic, diagnostic) + assertNull(run.symbolicReplay, diagnostic) + assertTrue(run.elapsedMillis >= 1, diagnostic) + assertFailsWith { run.requireSuccess() } + } + + private fun DslPropertyRun.executionDiagnostic(): String = + "elapsedMillis=$elapsedMillis, budgetMillis=$budgetMillis, " + + "symbolicSkippedDueToDeadline=$symbolicSkippedDueToDeadline, symbolicStatus=${symbolic?.status}, " + + "concreteStatus=${concrete?.status}, replayStatus=${symbolicReplay?.status}, " + + "replayFailure=${symbolicReplay?.failure}" + private fun addition(exportName: String): DslProperty = defineProperty(id = "calculator.$exportName") { val sum = function<(Double, Double) -> Double>(module = "calculator.ts", exportName = exportName) val a by int(min = -100, max = 100) diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/PbtEdgeGuidanceTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/PbtEdgeGuidanceTest.kt new file mode 100644 index 0000000000..a80dce86d2 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/PbtEdgeGuidanceTest.kt @@ -0,0 +1,140 @@ +package org.usvm.ts.pbt.dsl + +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.testResourcesRoot +import org.usvm.ts.pbt.usvm.UsvmEdgeReplayStatus +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class PbtEdgeGuidanceTest { + private val runner = DslPropertyRunner(sourceRoots = listOf(testResourcesRoot().resolve("properties/dsl"))) + private val configuration = PropertyRunConfiguration(seed = 42, numRuns = 1, timeoutMillis = 30_000) + + @Test + fun `real PBT evidence changes the pending state selected in the original property search`() { + val program = positiveResult(exportName = "branch") + + val positive = run(program, examples = listOf(1)) + val negative = run(program, examples = listOf(-1)) + + val positiveTrace = assertNotNull(positive.symbolic?.edgeGuidance) + val negativeTrace = assertNotNull(negative.symbolic?.edgeGuidance) + assertEquals(setOf(true), positiveTrace.initialCovered.map { it.outcome }.toSet()) + assertEquals(setOf(false), positiveTrace.initialGoals.map { it.outcome }.toSet()) + assertEquals(setOf(false), negativeTrace.initialCovered.map { it.outcome }.toSet()) + assertEquals(setOf(true), negativeTrace.initialGoals.map { it.outcome }.toSet()) + val positiveSelection = positiveTrace.selections.first { it.pendingStates > 1 && it.distance == 0 } + val negativeSelection = negativeTrace.selections.first { it.pendingStates > 1 && it.distance == 0 } + assertEquals(false, positiveSelection.goal?.outcome) + assertEquals(true, negativeSelection.goal?.outcome) + assertTrue(positiveSelection.goal in positiveSelection.traversedGoals) + assertTrue(negativeSelection.goal in negativeSelection.traversedGoals) + assertEquals(setOf(false), positiveSelection.traversedGoals.map { it.outcome }.toSet()) + assertEquals(setOf(true), negativeSelection.traversedGoals.map { it.outcome }.toSet()) + val replayConfirmedNewEdge = positiveTrace.replays.any { + it.status == UsvmEdgeReplayStatus.CONFIRMED && it.additions.isNotEmpty() + } + assertTrue(replayConfirmedNewEdge, positiveTrace.toString()) + assertTrue(positiveTrace.remainingGoals.isEmpty(), positiveTrace.toString()) + assertTrue(negativeTrace.remainingGoals.isEmpty(), negativeTrace.toString()) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, positive.symbolic?.status) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, negative.symbolic?.status) + } + + @Test + fun `covered prefixes remain traversable for a nested missing edge and confirmed additions change later choices`() { + val program = positiveResult(exportName = "nested") + + val run = run(program, examples = listOf(1)) + + val trace = assertNotNull(run.symbolic?.edgeGuidance) + val nestedMissing = trace.initialGoals.single { it.outcome } + assertTrue(trace.replays.any { nestedMissing in it.additions }, trace.toString()) + assertTrue(trace.selections.any { it.evidenceRevision > 0 }, trace.toString()) + assertTrue(trace.remainingGoals.isEmpty(), trace.toString()) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, run.symbolic?.status) + } + + @Test + fun `native replay can make a previously unknown nested branch an exact goal in the same machine`() { + val program = positiveResult(exportName = "hidden") + + val run = run(program, examples = listOf(-1)) + + val trace = assertNotNull(run.symbolic?.edgeGuidance) + assertTrue(trace.initialGoals.none { it.method.contains("nested") }) + assertTrue(trace.replays.any { replay -> replay.additions.any { it.method.contains("nested") } }) + val nestedOutcomes = trace.confirmedCovered.filter { it.method.contains("nested") } + .groupBy { it.conditionIndex }.mapValues { (_, edges) -> edges.map { it.outcome }.toSet() } + assertEquals(2, nestedOutcomes.size) + val innerCondition = nestedOutcomes.entries.single { it.value == setOf(true, false) }.key + val selectedInnerGoal = trace.selections.any { + it.evidenceRevision > 0 && it.goal?.method?.contains("nested") == true && + it.goal?.conditionIndex == innerCondition + } + assertTrue(selectedInnerGoal) + // hidden calls nested only for positive inputs: nested's outer false edge remains infeasible here. + val remaining = trace.remainingGoals.single() + assertTrue(remaining.method.contains("nested")) + assertEquals(false, remaining.outcome) + assertEquals(setOf(true), nestedOutcomes.getValue(remaining.conditionIndex)) + assertTrue(remaining !in trace.confirmedCovered) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, run.symbolic?.status) + } + + @Test + fun `if without else retains a missing edge even when every statement was covered`() { + val program = positiveResult(exportName = "withoutElse") + + val run = run(program, examples = listOf(1)) + + val trace = assertNotNull(run.symbolic?.edgeGuidance) + val coverage = assertNotNull(run.concrete?.coverage) + val source = coverage.files.single { it.path.endsWith("edge-guidance.ts") } + val functionStatements = source.statements.filter { it.location.start.line in 23..28 } + assertTrue(functionStatements.isNotEmpty()) + assertTrue(functionStatements.all { it.hits > 0 }, functionStatements.toString()) + val missingOutcomes = trace.initialGoals.filter { it.method.contains("withoutElse") }.map { it.outcome }.toSet() + assertEquals(setOf(false), missingOutcomes) + assertTrue(trace.remainingGoals.isEmpty(), trace.toString()) + } + + @Test + fun `fully covered code still searches for a violation of the original property`() { + val program = defineProperty(id = "edge-guidance.saturated") { + val branch = function<(Double) -> Double>(module = "edge-guidance.ts", exportName = "branch") + val input by int(min = -100, max = 100) + + check(name = "original") { branch(input) notEqualTo input } + } + + val run = run(program, examples = listOf(-1, 3)) + + val trace = assertNotNull(run.symbolic?.edgeGuidance) + assertTrue(trace.initialGoals.isEmpty(), trace.toString()) + assertTrue(trace.selections.isNotEmpty()) + assertTrue(trace.selections.all { it.goal == null && it.originalObjectiveTurn }) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, run.symbolic?.status) + assertEquals("original", run.symbolicReplay?.failure?.checkId) + } + + private fun positiveResult(exportName: String): DslProperty = defineProperty(id = "edge-guidance.$exportName") { + val function = function<(Double) -> Double>(module = "edge-guidance.ts", exportName = exportName) + val input by int(min = -100, max = 100) + + check(name = "positive") { function(input) greaterThan 0 } + } + + private fun run(program: DslProperty, examples: List): DslPropertyRun = runner.run( + program = program, + engine = PropertyEngine.BOTH, + configuration = configuration.copy( + numRuns = examples.size, + examples = examples.map { listOf(JsConcreteValue.number(it.toDouble())) }, + ), + ) +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt index 4c4dee032c..7e6c46b9fa 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckCoverageTest.kt @@ -160,7 +160,7 @@ class FastCheckCoverageTest { } @Test - fun `unsupported TypeScript branch retains exact statement coverage`() { + fun `nonterminating if without else retains exact branch counts`() { val result = backend.run( property = property( exportName = "coversNonterminal", @@ -174,9 +174,31 @@ class FastCheckCoverageTest { candidate.path.endsWith("properties/coverage/nonterminal-source-under-test.ts") } + assertTrue(file.statements.any { statement -> statement.hits > 0 }) + assertEquals(listOf(1L, 0L), exactIf(file).arms.map { arm -> arm.hits }) + } + + @Test + fun `unsupported TypeScript branch retains exact statement coverage`() { + val result = backend.run( + property = property( + exportName = "coversLogical", + domain = IntegerDomain(min = 1, max = 1), + ), + configuration = configuration, + ) + + val coverage = assertNotNull(result.coverage) + val file = coverage.files.single { candidate -> + candidate.path.endsWith("properties/coverage/logical-source-under-test.ts") + } + assertTrue(file.statements.any { statement -> statement.hits > 0 }) assertTrue(file.branches.none { branch -> branch.type == "if" }) - assertTrue(coverage.diagnostics.any { diagnostic -> diagnostic.code == "coverage.branch.unsupported" }) + val unsupportedBranch = coverage.diagnostics.any { diagnostic -> + diagnostic.code == "coverage.branch.unsupported" && diagnostic.path == file.path + } + assertTrue(unsupportedBranch) } @Test diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/UsvmEdgeFeedbackContractTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/UsvmEdgeFeedbackContractTest.kt new file mode 100644 index 0000000000..e2c211bd2e --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/UsvmEdgeFeedbackContractTest.kt @@ -0,0 +1,235 @@ +package org.usvm.ts.pbt.fastcheck + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyCoverageArtifact +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcesRoot +import org.usvm.ts.pbt.usvm.UsvmCoverageEvidenceStatus +import org.usvm.ts.pbt.usvm.UsvmCoverageFeedback +import org.usvm.ts.pbt.usvm.UsvmEdgeReplayStatus +import org.usvm.ts.pbt.usvm.UsvmPropertySearchResult +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import org.usvm.ts.pbt.usvm.UsvmPropertySearcher +import java.util.concurrent.CancellationException +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotNull +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class UsvmEdgeFeedbackContractTest { + @Test + fun `only concrete evidence changes the selected pending path for the same scene and symbolic query`() { + val property = property() + val positive = backend.run(property, configuration) + val negative = backend.run( + property, + configuration.copy(examples = listOf(listOf(JsConcreteValue.number(-1.0)))), + ) + + val positiveSearch = search(property, positive.coverage) { null } + val negativeSearch = search(property, negative.coverage) { null } + + val positiveSelection = assertNotNull(positiveSearch.edgeGuidance).selections + .first { it.pendingStates > 1 && it.distance == 0 } + val negativeSelection = assertNotNull(negativeSearch.edgeGuidance).selections + .first { it.pendingStates > 1 && it.distance == 0 } + assertEquals(false, positiveSelection.goal?.outcome) + assertEquals(true, negativeSelection.goal?.outcome) + assertTrue(positiveSelection.goal in positiveSelection.traversedGoals) + assertTrue(negativeSelection.goal in negativeSelection.traversedGoals) + assertEquals(setOf(false), positiveSelection.traversedGoals.map { it.outcome }.toSet()) + assertEquals(setOf(true), negativeSelection.traversedGoals.map { it.outcome }.toSet()) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, positiveSearch.status) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, negativeSearch.status) + } + + @Test + fun `native replay cancellation propagates instead of becoming an ordinary replay failure`() { + val property = property() + val initial = backend.run(property, configuration) + + assertFailsWith { + search(property, initial.coverage) { throw CancellationException("cancelled") } + } + } + + @Test + fun `absent stale unsupported and no-admission evidence keep distinct outcomes and original property search`() { + val property = property() + val initial = backend.run(property, configuration) + val coverage = assertNotNull(initial.coverage) + val identity = assertNotNull(coverage.identity) + val stale = coverage.copy(identity = identity.copy(manifestSha256 = "0".repeat(64))) + val unsupported = coverage.copy( + files = coverage.files.map { file -> file.copy(branches = file.branches.filter { it.type != "if" }) }, + ) + val variants = listOf( + null to UsvmCoverageEvidenceStatus.ABSENT, + stale to UsvmCoverageEvidenceStatus.STALE, + coverage.copy(identity = null) to UsvmCoverageEvidenceStatus.UNSUPPORTED, + coverage.copy(admittedInvocations = 0) to UsvmCoverageEvidenceStatus.NO_ADMITTED_INPUTS, + unsupported to UsvmCoverageEvidenceStatus.UNSUPPORTED, + ) + + for ((evidence, status) in variants) { + val result = search(property, evidence) { error("No exact goals should request replay") } + + val trace = assertNotNull(result.edgeGuidance) + assertEquals(status, trace.evidenceStatus) + assertTrue(trace.initialGoals.isEmpty()) + assertTrue(trace.initialCovered.isEmpty()) + assertTrue(trace.selections.isNotEmpty()) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + } + } + + @Test + fun `failed replay and wrong edge receipt leave the target concretely uncovered`() { + val property = property() + val initial = backend.run(property, configuration) + val coverage = assertNotNull(initial.coverage) + + val failed = search(property, coverage) { throw IllegalStateException("native failure") } + val mismatched = search(property, coverage) { initial } + + val results = listOf( + failed to UsvmEdgeReplayStatus.REPLAY_FAILED, + mismatched to UsvmEdgeReplayStatus.EDGE_MISMATCH, + ) + for ((result, expectedStatus) in results) { + val trace = assertNotNull(result.edgeGuidance) + assertEquals(trace.initialGoals, trace.remainingGoals) + assertEquals(trace.initialCovered, trace.confirmedCovered) + assertTrue(trace.replays.isNotEmpty(), trace.toString()) + assertTrue(trace.replays.all { it.status == expectedStatus && it.additions.isEmpty() }, trace.toString()) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + } + } + + @Test + fun `exhausted replay attempts stop guiding without confirming coverage or dropping paths`() { + val property = property().copy( + precondition = TypeScriptEntryPoint(module = "guidance-property.ts", exportName = "retryAdmission"), + ) + val initial = backend.run(property, configuration) + + val result = search(property, initial.coverage) { null } + + val trace = assertNotNull(result.edgeGuidance) + assertEquals(1, trace.initialGoals.size) + assertEquals(trace.attemptLimitPerGoal, trace.replays.size) + assertEquals(trace.initialGoals, trace.remainingGoals) + assertEquals(trace.initialCovered, trace.confirmedCovered) + assertTrue(trace.replays.all { it.status == UsvmEdgeReplayStatus.NOT_RUN }, trace.toString()) + assertEquals(trace.replays.size, trace.replays.map { it.inputs }.distinct().size) + assertEquals(null, trace.selections.last().goal) + val originalTurns = trace.selections.filterIndexed { index, _ -> index % 2 == 1 } + assertTrue(originalTurns.isNotEmpty()) + assertTrue(originalTurns.all { it.originalObjectiveTurn }, trace.toString()) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + } + + @Test + fun `rejected precondition cannot remove a source edge from the real coverage target queue`() { + val property = property().copy( + predicate = TypeScriptEntryPoint(module = "guidance-property.ts", exportName = "guarded"), + precondition = TypeScriptEntryPoint(module = "guidance-property.ts", exportName = "admission"), + ) + val initial = backend.run( + property, + configuration.copy( + examples = listOf(listOf(JsConcreteValue.number(-1.0)), listOf(JsConcreteValue.number(1.0))), + ), + ) + + val result = search(property, assertNotNull(initial.coverage)) { null } + + val trace = assertNotNull(result.edgeGuidance) + assertEquals(1, initial.numSkips) + assertEquals(setOf(false), trace.initialCovered.map { it.outcome }.toSet()) + assertEquals(setOf(true), trace.initialGoals.map { it.outcome }.toSet()) + assertEquals(trace.initialGoals, trace.remainingGoals) + assertTrue( + trace.replays.isEmpty(), + "The source edge reached only in the guard cannot confirm predicate coverage", + ) + assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, result.status) + } + + @Test + fun `caller deadline stops before any symbolic queue selection`() { + val property = property() + val manifest = property.toManifest() + val mapping = PropertyEtsMapper(scene = scene, sourceRoots = roots).map(manifest) + val searcher = UsvmPropertySearcher( + scene = scene, + machineOptions = UMachineOptions(solverType = SolverType.YICES, timeout = 10.seconds), + deadlineReached = { true }, + ) + + val result = searcher.search( + manifest = manifest, + mapping = mapping, + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + coverageFeedback = UsvmCoverageFeedback(initialCoverage = null) { error("Deadline forbids replay") }, + ) + + assertEquals(UsvmPropertySearchStatus.TIMEOUT, result.status) + assertTrue(assertNotNull(result.edgeGuidance).selections.isEmpty()) + } + + private fun search( + property: PropertyDefinition, + coverage: PropertyCoverageArtifact?, + replay: (List) -> PropertyRunResult?, + ): UsvmPropertySearchResult { + val manifest = property.toManifest() + val mapping = PropertyEtsMapper(scene = scene, sourceRoots = roots).map(manifest, coverage) + return UsvmPropertySearcher( + scene = scene, + machineOptions = UMachineOptions(solverType = SolverType.YICES, timeout = 10.seconds), + ).search( + manifest = manifest, + mapping = mapping, + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + coverageFeedback = UsvmCoverageFeedback(initialCoverage = coverage, replay = replay), + ) + } + + private fun property() = PropertyDefinition( + id = PropertyId("edge-feedback.contract"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = -100, max = 100))), + predicate = TypeScriptEntryPoint(module = "guidance-property.ts", exportName = "valid"), + ) + + private companion object { + val roots = listOf(testResourcesRoot().resolve("properties/dsl")) + val backend = FastCheckBackend(sourceRoots = roots) + val scene: EtsScene by lazy { loadEtsProjectAutoConvert(roots.single(), provider = EtsIrProvider.TS_FRONTEND) } + val configuration = PropertyRunConfiguration( + seed = 42, + numRuns = 1, + timeoutMillis = 10_000, + examples = listOf(listOf(JsConcreteValue.number(1.0))), + coverageRequest = PropertyCoverageRequest(admittedOnly = true), + ) + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/coverage/CoverageProperties.ts b/usvm-ts-fast-check/src/test/resources/properties/coverage/CoverageProperties.ts index 653db26a2d..c32bef35d3 100644 --- a/usvm-ts-fast-check/src/test/resources/properties/coverage/CoverageProperties.ts +++ b/usvm-ts-fast-check/src/test/resources/properties/coverage/CoverageProperties.ts @@ -1,6 +1,7 @@ import { classify } from './source-under-test.ts'; import { classifyNested } from './nested-source-under-test.ts'; import { nonterminal } from './nonterminal-source-under-test.ts'; +import { logical } from './logical-source-under-test.ts'; export function coversPositive(value: number): boolean { return classify(value) === 'positive'; @@ -29,3 +30,8 @@ export function coversNonterminal(value: number): boolean { nonterminal(value); return true; } + +export function coversLogical(value: number): boolean { + logical(value); + return true; +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/coverage/logical-source-under-test.ts b/usvm-ts-fast-check/src/test/resources/properties/coverage/logical-source-under-test.ts new file mode 100644 index 0000000000..99e65e4225 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/coverage/logical-source-under-test.ts @@ -0,0 +1,7 @@ +export function logical(value: number): number { + let result = 0; + if (value > 0 && value < 10) { + result += 1; + } + return result; +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/dsl/edge-guidance.ts b/usvm-ts-fast-check/src/test/resources/properties/dsl/edge-guidance.ts new file mode 100644 index 0000000000..eedcd3ae9c --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/dsl/edge-guidance.ts @@ -0,0 +1,35 @@ +export function branch(value: number): number { + if (value > 0) { + return 1; + } else { + return 2; + } +} + +export function nested(value: number): number { + if (value > 0) { + if (value === 42) { + return 3; + } else { + return 1; + } + } else { + return 2; + } +} + +export function withoutElse(value: number): number { + let result = 1; + if (value > 0) { + result = 1; + } + return result; +} + +export function hidden(value: number): number { + if (value > 0) { + return nested(value); + } else { + return 2; + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/dsl/guidance-property.ts b/usvm-ts-fast-check/src/test/resources/properties/dsl/guidance-property.ts new file mode 100644 index 0000000000..e512753868 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/dsl/guidance-property.ts @@ -0,0 +1,20 @@ +import { branch } from './edge-guidance'; + +export function valid(value: number): boolean { + return branch(value) > 0; +} + +export function admission(value: number): boolean { + branch(-value); + return value > 0; +} + +export function guarded(value: number): boolean { + return branch(-value) > 0; +} + +export function retryAdmission(value: number): boolean { + if (value === -1) return true; + if (value === -2) return true; + return true; +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt index 566ad6afd4..c053c02fd2 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyBasedTestingBackend.kt @@ -29,6 +29,8 @@ data class PropertyRunConfiguration( val examples: List> = emptyList(), val coverageRequest: PropertyCoverageRequest? = null, val observationRequest: PropertyObservationRequest? = null, + /** Execute the single explicit example, without generation after rejection or shrinking. */ + val exactReplay: Boolean = false, ) { init { require(numRuns > 0) { "Number of runs must be positive" } @@ -36,6 +38,9 @@ data class PropertyRunConfiguration( require(timeoutMillis <= MAX_TIMEOUT_MILLIS) { "Timeout exceeds the maximum delay supported by Node timers" } + require(!exactReplay || (numRuns == 1 && examples.size == 1 && replayPath == null)) { + "Exact replay requires one explicit example, one run, and no replay path" + } } companion object { diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyCoverage.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyCoverage.kt index 1b29ef0765..ca0f41346f 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyCoverage.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyCoverage.kt @@ -119,6 +119,8 @@ data class PropertyCoverageRequest( val includePatterns: List = emptyList(), val excludePatterns: List = emptyList(), val includeUnexecutedSources: Boolean = false, + /** Collect predicate invocations admitted by the precondition, excluding shrinking trials. */ + val admittedOnly: Boolean = false, ) { init { require(scopes.isNotEmpty()) { "At least one coverage scope is required" } @@ -247,8 +249,13 @@ data class PropertyCoverageArtifact( val provenance: CoverageProvenance, val files: List, val diagnostics: List = emptyList(), + val identity: PropertyCoverageIdentity? = null, + val admittedInvocations: Int? = null, ) { init { + require(admittedInvocations == null || admittedInvocations >= 0) { + "Admitted invocation count must not be negative" + } require(backendId.isNotBlank()) { "Coverage backend ID must not be blank" } require(backendVersion.isNotBlank()) { "Coverage backend version must not be blank" } require(files.map(SourceFileCoverage::path).distinct().size == files.size) { @@ -256,3 +263,10 @@ data class PropertyCoverageArtifact( } } } + +/** Exact property and source snapshot used by an admitted-only concrete run. */ +@Serializable +data class PropertyCoverageIdentity( + val manifestSha256: String, + val sourceSha256: Map, +) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/PropertyCoverageIdentity.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/PropertyCoverageIdentity.kt new file mode 100644 index 0000000000..2ccf7730eb --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/coverage/PropertyCoverageIdentity.kt @@ -0,0 +1,40 @@ +package org.usvm.ts.pbt.coverage + +import org.usvm.ts.pbt.backend.PropertyCoverageIdentity +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import java.nio.file.Files +import java.nio.file.Path +import java.security.MessageDigest +import java.util.stream.Collectors + +/** Snapshots the declared support/oracle and the local TypeScript files used by the concrete runtime. */ +fun captureCoverageIdentity(manifest: PropertyManifest, sourceRoots: List): PropertyCoverageIdentity { + val sources = sortedMapOf() + for (root in sourceRoots) { + val files = Files.walk(root).use { paths -> + paths.filter { isCoverageSource(root, it) }.collect(Collectors.toList()) + } + for (path in files) { + sources[path.toRealPath().toString()] = sha256(Files.readAllBytes(path)) + } + } + + val manifestBytes = PropertyManifestJson.encode(manifest).toByteArray(Charsets.UTF_8) + return PropertyCoverageIdentity( + manifestSha256 = sha256(manifestBytes), + sourceSha256 = sources, + ) +} + +private fun isCoverageSource(root: Path, path: Path): Boolean { + val excluded = root.relativize(path).any { it.toString() in EXCLUDED_DIRECTORIES } + val typeScript = path.toString().endsWith(".ts") || path.toString().endsWith(".ets") + return !excluded && typeScript && Files.isRegularFile(path) +} + +private fun sha256(bytes: ByteArray): String = MessageDigest.getInstance("SHA-256") + .digest(bytes) + .joinToString("") { byte -> "%02x".format(byte) } + +private val EXCLUDED_DIRECTORIES = setOf("node_modules", ".git", ".gradle", "build", "dist") diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt new file mode 100644 index 0000000000..55fc793b43 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCoverageFeedback.kt @@ -0,0 +1,75 @@ +package org.usvm.ts.pbt.usvm + +import org.usvm.ts.pbt.backend.PropertyCoverageArtifact +import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.model.JsConcreteValue + +/** Concrete feedback for the original property analysis. A replay must execute exactly [inputs]. */ +data class UsvmCoverageFeedback( + val initialCoverage: PropertyCoverageArtifact?, + val replay: (inputs: List) -> PropertyRunResult?, +) + +/** Why a report can or cannot supply exact coverage goals for this property/source snapshot. */ +enum class UsvmCoverageEvidenceStatus { + ABSENT, + STALE, + UNSUPPORTED, + NO_ADMITTED_INPUTS, + EXACT, + PARTIAL, +} + +/** Distinguishes a CFG edge from either of its endpoint statements. */ +data class UsvmCoverageEdge( + val method: String, + val conditionIndex: Int, + val successorIndex: Int, + val outcome: Boolean, +) + +/** A real queue decision made during the original predicate analysis. */ +data class UsvmEdgeSelection( + val evidenceRevision: Int, + val stateId: UInt, + val statement: String, + val pendingStates: Int, + val goal: UsvmCoverageEdge?, + val distance: Int?, + val originalObjectiveTurn: Boolean, + val traversedGoals: Set, +) + +/** Concrete confirmation outcomes; none except CONFIRMED can add edges. */ +enum class UsvmEdgeReplayStatus { + CONFIRMED, + EDGE_MISMATCH, + REJECTED_OR_INCOMPATIBLE, + NOT_RUN, + REPLAY_FAILED, +} + +/** A bounded exact-input native replay and its effect on the shared edge set. */ +data class UsvmEdgeReplay( + val inputs: List, + val status: UsvmEdgeReplayStatus, + val additions: Set, + val remainingGoals: Set, + val elapsedMillis: Long, +) + +/** Bounded history; symbolic reachability never updates [confirmedCovered]. */ +data class UsvmEdgeGuidanceTrace( + val evidenceStatus: UsvmCoverageEvidenceStatus, + val initialCovered: Set, + val initialGoals: Set, + val confirmedCovered: Set, + val remainingGoals: Set, + val attemptedGoals: Set, + val attemptLimitPerGoal: Int, + val selections: List, + val omittedSelections: Int, + val replays: List, + val diagnostics: List, + val elapsedMillis: Long, +) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt new file mode 100644 index 0000000000..9e12fb632c --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmEdgeGuidance.kt @@ -0,0 +1,382 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.usvm.UPathSelector +import org.usvm.machine.TsConcreteMethodCallStmt +import org.usvm.machine.TsEntryPointGuardResultStmt +import org.usvm.machine.TsGraph +import org.usvm.machine.TsMethodCall +import org.usvm.machine.state.TsState +import org.usvm.ps.BfsPathSelector +import org.usvm.ps.createClosestToUncoveredRandomPathSelector +import org.usvm.ts.pbt.backend.PropertyCoverageArtifact +import org.usvm.ts.pbt.backend.PropertyFailureKind +import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.coverage.captureCoverageIdentity +import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.mapping.EtsBranchArmTarget +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue +import java.nio.file.Path +import java.util.concurrent.CancellationException +import kotlin.random.Random +import kotlin.time.TimeSource + +/** Owns only exact concrete edge evidence and a seeded NURS scheduling hint, never path constraints. */ +internal class UsvmEdgeGuidance( + private val scene: EtsScene, + private val manifest: PropertyManifest, + mapping: PropertyEtsMappingArtifact, + private val feedback: UsvmCoverageFeedback, + val selectionSupported: Boolean, + private val random: Random, +) { + private val roots = mapping.provenance.sourceRoots.map(Path::of) + private val started = TimeSource.Monotonic.markNow() + private val identity = captureCoverageIdentity(manifest, roots) + private val targets = linkedMapOf() + private val covered = linkedSetOf() + private val attempted = linkedSetOf() + private val attemptsByGoal = hashMapOf() + private val replayedInputs = hashSetOf>() + private val selections = mutableListOf() + private val replays = mutableListOf() + private val diagnostics = mutableListOf() + private var revision = 0 + private var omittedSelections = 0 + private val evidenceStatus: UsvmCoverageEvidenceStatus + private val initialCovered: Set + private val initialGoals: Set + + init { + val coverage = feedback.initialCoverage + evidenceStatus = evidenceStatus(coverage) + val usable = evidenceStatus == UsvmCoverageEvidenceStatus.EXACT || + evidenceStatus == UsvmCoverageEvidenceStatus.PARTIAL + if (usable) { + val evidence = exactEdges(requireNotNull(coverage)) + evidence.forEach { (edge, target, hits) -> + targets[edge] = target + if (hits > 0) covered += edge + } + } + initialCovered = covered.toSet() + initialGoals = pendingGoals() + } + + private fun evidenceStatus(coverage: PropertyCoverageArtifact?): UsvmCoverageEvidenceStatus { + if (!selectionSupported) { + diagnostics += "Edge scheduling does not support state merging or selector loop bounds; " + + "original selection retained" + return UsvmCoverageEvidenceStatus.UNSUPPORTED + } + if (coverage == null) return UsvmCoverageEvidenceStatus.ABSENT + if (!coverage.provenance.request.admittedOnly || coverage.identity == null) { + return UsvmCoverageEvidenceStatus.UNSUPPORTED + } + val stale = coverage.identity != identity || coverage.propertyId.value != manifest.propertyId || + coverage.diagnostics.any { it.code == "coverage.source.stale" } + if (stale) return UsvmCoverageEvidenceStatus.STALE + if (coverage.admittedInvocations == null) return UsvmCoverageEvidenceStatus.UNSUPPORTED + if (coverage.admittedInvocations == 0) return UsvmCoverageEvidenceStatus.NO_ADMITTED_INPUTS + + val mapped = mapper().map(manifest, coverage).coverage + val exact = exactEdges(coverage) + val mappingDiagnostics = mapped.diagnostics + mapped.branches.flatMap { branch -> + branch.mapping.diagnostics + branch.arms.flatMap { it.mapping.diagnostics } + } + diagnostics += mappingDiagnostics.map { "${it.code}: ${it.message}" }.distinct() + if (exact.isEmpty()) return UsvmCoverageEvidenceStatus.UNSUPPORTED + + val unknownBranches = mapped.branches.any { it.mapping.status != EtsMappingStatus.EXACT } + return if (unknownBranches || mapped.diagnostics.isNotEmpty()) { + UsvmCoverageEvidenceStatus.PARTIAL + } else { + UsvmCoverageEvidenceStatus.EXACT + } + } + + private fun mapper() = PropertyEtsMapper(scene = scene, sourceRoots = roots) + + private fun exactEdges(coverage: PropertyCoverageArtifact): List { + return mapper().map(manifest, coverage).coverage.branches.flatMap { branch -> + val sourcePath = branch.location?.path + if (sourcePath !in identity.sourceSha256) return@flatMap emptyList() + + branch.arms.flatMap { arm -> + if (arm.mapping.status != EtsMappingStatus.EXACT) return@flatMap emptyList() + + arm.mapping.targets.mapNotNull { target -> + val method = target.condition.location.method + val successors = method.cfg.successors(target.condition) + if (successors.distinct().size != 2) return@mapNotNull null + + val edge = UsvmCoverageEdge( + method = method.signature.toString(), + conditionIndex = method.cfg.stmts.indexOf(target.condition), + successorIndex = method.cfg.stmts.indexOf(target.successor), + outcome = target.outcome, + ) + ObservedEdge(edge = edge, target = target, hits = arm.coverage.hits) + } + } + } + } + + fun selector(initialStates: Map, graph: TsGraph): UPathSelector { + return EdgePathSelector(initialStates.values, graph) + } + + fun confirm(state: TsState, inputs: List, expectsViolation: Boolean) { + val claimed = traversedGoals(state) + if (claimed.isEmpty()) return + + if (!replayedInputs.add(inputs)) return + attempted += claimed + claimed.forEach { goal -> attemptsByGoal[goal] = (attemptsByGoal[goal] ?: 0) + 1 } + + val replayStarted = TimeSource.Monotonic.markNow() + val decision = replay(inputs, claimed, expectsViolation) + + replays += UsvmEdgeReplay( + inputs = inputs, + status = decision.status, + additions = decision.additions, + remainingGoals = pendingGoals(), + elapsedMillis = replayStarted.elapsedNow().inWholeMilliseconds, + ) + } + + // Feedback is optional: an arbitrary backend/transport exception must not + // abort the original symbolic property objective or manufacture coverage. + @Suppress("TooGenericExceptionCaught") + private fun replay( + inputs: List, + claimed: Set, + expectsViolation: Boolean, + ): ReplayDecision = try { + val result = feedback.replay(inputs) + if (result == null) { + ReplayDecision(status = UsvmEdgeReplayStatus.NOT_RUN) + } else { + confirmReplay(result, inputs, claimed, expectsViolation) + } + } catch (error: InterruptedException) { + Thread.currentThread().interrupt() + throw error + } catch (error: CancellationException) { + throw error + } catch (error: Exception) { + if (Thread.currentThread().isInterrupted) throw error + + diagnostics += "Concrete replay failed: ${error.message}" + ReplayDecision(status = UsvmEdgeReplayStatus.REPLAY_FAILED) + } + + private fun confirmReplay( + result: PropertyRunResult, + inputs: List, + claimed: Set, + expectsViolation: Boolean, + ): ReplayDecision { + val coverage = result.coverage + val compatible = coverage != null && isCompatible(coverage) + val matchesOracle = matchesOracle(result, inputs, expectsViolation) + if (!matchesOracle || !compatible) { + return ReplayDecision(status = UsvmEdgeReplayStatus.REJECTED_OR_INCOMPATIBLE) + } + + val observed = exactEdges(requireNotNull(coverage)) + val confirmed = observed.filter { it.hits > 0 }.mapTo(hashSetOf()) { it.edge } + if (!confirmed.containsAll(claimed)) return ReplayDecision(status = UsvmEdgeReplayStatus.EDGE_MISMATCH) + + observed.forEach { targets.putIfAbsent(it.edge, it.target) } + val additions = confirmed - covered + covered += additions + if (additions.isNotEmpty()) revision += 1 + return ReplayDecision(status = UsvmEdgeReplayStatus.CONFIRMED, additions = additions) + } + + private fun matchesOracle( + result: PropertyRunResult, + inputs: List, + expectsViolation: Boolean, + ): Boolean { + val propertyFailure = result.failure?.kind == PropertyFailureKind.PROPERTY + val completed = result.status == PropertyRunStatus.SUCCESS || + (propertyFailure && result.counterexample == inputs) + val exact = result.numSkips == 0 && result.numRuns == 1 && result.numShrinks == 0 + return exact && completed && propertyFailure == expectsViolation + } + + private fun isCompatible(coverage: PropertyCoverageArtifact): Boolean { + val original = feedback.initialCoverage ?: return false + val sameBackend = coverage.backendId == original.backendId && + coverage.backendVersion == original.backendVersion && coverage.kind == original.kind + val fresh = coverage.identity == identity && captureCoverageIdentity(manifest, roots) == identity && + coverage.diagnostics.none { it.code == "coverage.source.stale" } + val sameRuntime = coverage.provenance == original.provenance && coverage.admittedInvocations == 1 + return sameBackend && fresh && sameRuntime + } + + private fun pendingGoals(): Set = targets.keys - covered + + // Failed attempts remain uncovered. Try at most two distinct concrete inputs + // per edge; property exploration retains half of all scheduling turns. + private fun availableGoals(): Set = pendingGoals().filterTo(linkedSetOf()) { + (attemptsByGoal[it] ?: 0) < MAX_REPLAY_ATTEMPTS_PER_GOAL + } + + private fun traversedGoals(state: TsState): Set { + if (state.entryPointGuardActive) return emptySet() + + val path = state.pathNode.allStatements.takeWhile { it !is TsEntryPointGuardResultStmt } + return availableGoals().filterTo(linkedSetOf()) { edge -> + val target = targets.getValue(edge) + path.zipWithNext().any { (successor, condition) -> + condition == target.condition && successor == target.successor + } + } + } + + fun snapshot() = UsvmEdgeGuidanceTrace( + evidenceStatus = evidenceStatus, + initialCovered = initialCovered, + initialGoals = initialGoals, + confirmedCovered = covered.toSet(), + remainingGoals = pendingGoals(), + attemptedGoals = attempted.toSet(), + attemptLimitPerGoal = MAX_REPLAY_ATTEMPTS_PER_GOAL, + selections = selections.toList(), + omittedSelections = omittedSelections, + replays = replays.toList(), + diagnostics = diagnostics.toList(), + elapsedMillis = started.elapsedNow().inWholeMilliseconds, + ) + + private data class ObservedEdge(val edge: UsvmCoverageEdge, val target: EtsBranchArmTarget, val hits: Long) + private data class GoalDistance(val goal: UsvmCoverageEdge, val distance: Int) + private data class ReplayDecision( + val status: UsvmEdgeReplayStatus, + val additions: Set = emptySet(), + ) + + private inner class EdgePathSelector( + initialStates: Collection, + private val graph: TsGraph, + ) : UPathSelector { + private val states = hashSetOf() + private val original = BfsPathSelector() + private val coverage = createClosestToUncoveredRandomPathSelector( + distance = { state -> nearestGoal(state)?.distance?.toUInt() ?: UInt.MAX_VALUE }, + random = random, + ) + private var turn = 0L + + init { + add(initialStates) + } + + override fun isEmpty(): Boolean = states.isEmpty() + override fun add(states: Collection) { + this.states.addAll(states) + original.add(states) + coverage.add(states) + } + override fun update(state: TsState) = coverage.update(state) + override fun remove(state: TsState) { + states.remove(state) + original.remove(state) + coverage.remove(state) + } + + override fun drain(): Sequence = sequence { + for (state in coverage.drain()) { + states.remove(state) + original.remove(state) + yield(state) + } + } + + override fun peek(): TsState { + val originalTurn = turn % 2L == 1L + val guidedState = if (originalTurn) null else coverage.peek() + val goal = guidedState?.let { nearestGoal(it) } + val state = if (goal == null) original.peek() else requireNotNull(guidedState) + original.remove(state) + original.add(listOf(state)) + turn += 1 + + if (selections.size < MAX_RECORDED_SELECTIONS) { + selections += UsvmEdgeSelection( + evidenceRevision = revision, + stateId = state.id, + statement = state.currentStatement.toString(), + pendingStates = states.size, + goal = goal?.goal, + distance = goal?.distance, + originalObjectiveTurn = originalTurn || goal == null, + traversedGoals = traversedGoals(state), + ) + } else { + omittedSelections += 1 + } + return state + } + + private fun nearestGoal(state: TsState): GoalDistance? { + val pending = availableGoals() + val crossed = traversedGoals(state).firstOrNull { it in pending } + if (crossed != null) return GoalDistance(goal = crossed, distance = 0) + if (pending.isEmpty()) return null + + val queue = ArrayDeque>() + val visited = hashSetOf() + val returnSites = hashMapOf>() + state.callStack.forEach { frame -> + val returnSite = frame.returnSite + if (returnSite != null) returnSites.getOrPut(frame.method) { hashSetOf() } += returnSite + } + queue += state.currentStatement to 0 + while (queue.isNotEmpty() && visited.size < MAX_DISTANCE_STATEMENTS) { + val (statement, distance) = queue.removeFirst() + if (!visited.add(statement)) continue + if (statement is TsEntryPointGuardResultStmt) { + queue += statement.entryPoint to distance + 1 + continue + } + + val goal = pending.firstOrNull { targets.getValue(it).condition == statement } + if (goal != null) return GoalDistance(goal = goal, distance = distance + 1) + + graph.successors(statement).forEach { queue += it to distance + 1 } + val callees = when (statement) { + is TsConcreteMethodCallStmt -> sequenceOf(statement.callee) + is TsMethodCall -> graph.callees(statement.returnSite) + else -> graph.callees(statement) + } + callees.forEach { callee -> + returnSites.getOrPut(callee) { hashSetOf() }.addAll(graph.successors(statement)) + graph.entryPoints(callee).forEach { queue += it to distance + 1 } + } + // Returns are an overapproximation for priority only, never a reachability claim. + val method = graph.methodOf(statement) + if (statement in graph.exitPoints(method)) { + returnSites[method].orEmpty().forEach { queue += it to distance + 1 } + } + } + return null + } + } + + private companion object { + const val MAX_RECORDED_SELECTIONS = 4096 + const val MAX_DISTANCE_STATEMENTS = 20_000 + const val MAX_REPLAY_ATTEMPTS_PER_GOAL = 2 + } +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt index 192f8ae6a5..4f88c78aba 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearchModel.kt @@ -32,6 +32,7 @@ data class UsvmPropertySearchResult( val inputs: List?, val capability: UsvmPropertyProjectionCapability, val diagnostics: List, + val edgeGuidance: UsvmEdgeGuidanceTrace? = null, ) { init { when (status) { diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 10bf82289f..9d89581a83 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt @@ -3,6 +3,7 @@ package org.usvm.ts.pbt.usvm import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsType +import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions @@ -27,15 +28,24 @@ import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.mapping.EtsEntryPointTarget import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact import org.usvm.ts.pbt.model.PropertyId +import kotlin.random.Random /** Searches mapped TypeScript predicates for concrete property violations with USVM. */ class UsvmPropertySearcher( private val scene: EtsScene, - machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), + machineOptions: UMachineOptions = UMachineOptions( + solverType = SolverType.YICES, + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + ), private val tsOptions: TsOptions = TsOptions(), projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(), + private val deadlineReached: (() -> Boolean)? = null, ) { - private val machineOptions = machineOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL) + private val machineOptions = machineOptions.copy( + stateCollectionStrategy = StateCollectionStrategy.ALL, + // Statement saturation cannot establish the absence of a property violation. + stopOnCoverage = 0, + ) private val projectionOptions = projectionOptions.copy( maxSymbolicCollectionLength = minOf(projectionOptions.maxSymbolicCollectionLength, tsOptions.maxArraySize), maxSymbolicStringLength = minOf(projectionOptions.maxSymbolicStringLength, tsOptions.maxArraySize), @@ -46,6 +56,7 @@ class UsvmPropertySearcher( manifest: PropertyManifest, mapping: PropertyEtsMappingArtifact, concreteCapability: ProjectionCapability, + coverageFeedback: UsvmCoverageFeedback? = null, ): UsvmPropertySearchResult { val capability = capabilityResolver.resolve( manifest = manifest, @@ -73,13 +84,26 @@ class UsvmPropertySearcher( ), ) val precondition = mapping.precondition?.exactTargetOrNull() + val guidedSelectionSupported = !machineOptions.useMerging && !machineOptions.loopIterativeDeepening && + machineOptions.loopIterationLimit == null + val guidance = coverageFeedback?.let { feedback -> + UsvmEdgeGuidance( + scene = scene, + manifest = manifest, + mapping = mapping, + feedback = feedback, + selectionSupported = guidedSelectionSupported, + random = Random(seed = machineOptions.randomSeed), + ) + } return executeSearch( manifest = manifest, predicate = predicate, precondition = precondition, capability = capability, - ) + guidance = guidance, + ).copy(edgeGuidance = guidance?.snapshot()) } private fun executeSearch( @@ -87,10 +111,23 @@ class UsvmPropertySearcher( predicate: EtsEntryPointTarget, precondition: EtsEntryPointTarget?, capability: UsvmPropertyProjectionCapability, + guidance: UsvmEdgeGuidance?, ): UsvmPropertySearchResult { lateinit var projection: UsvmDeclaredDomainProjection val target = UsvmViolationTsTarget() - val observer = UsvmViolationObserver(target) + lateinit var observer: UsvmViolationObserver + observer = UsvmViolationObserver(target) { state -> + if (guidance != null) { + val violation = observer.violationStates.lastOrNull { it.pathNode === state.pathNode } + val replayState = violation ?: state + val inputs = runCatching { + UsvmCandidateInputResolver(projection.objectShapes).resolve( + replayState, manifest.inputs, projection, + ) + }.getOrNull() + if (inputs != null) guidance.confirm(replayState, inputs, expectsViolation = violation != null) + } + } val objectShapes = PlainObjectInputShapes(scene, manifest.inputs.map { it.domain }) val domainProjector = UsvmDomainProjector(projectionOptions, objectShapes) @@ -99,6 +136,8 @@ class UsvmPropertySearcher( options = machineOptions, tsOptions = tsOptions, machineObserver = observer, + deadlineReached = deadlineReached, + pathSelectorFactory = guidance?.takeIf { it.selectionSupported }?.let { it::selector }, ).use { machine -> val analysis = machine.analyzeWithMetadata( methods = listOf(predicate.method), @@ -418,6 +457,7 @@ private class UsvmViolationTsTarget : TsTarget(location = null) private class UsvmViolationObserver( private val target: UsvmViolationTsTarget, + private val onCompletedState: (TsState) -> Unit = {}, ) : UMachineObserver { private val mutableViolationStates = mutableListOf() @@ -457,6 +497,7 @@ private class UsvmViolationObserver( TsMethodResult.NoCall -> Unit } + onCompletedState(state) } private fun recordViolation(state: TsState) { diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionSearchTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionSearchTest.kt index 2025445eba..7ae0c2752b 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionSearchTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPreconditionSearchTest.kt @@ -42,7 +42,8 @@ class UsvmPreconditionSearchTest { val unsupported = search(manifest = errorPrecondition, propertySearcher = searcherWithoutModels) assertEquals(UsvmPropertySearchStatus.PRECONDITION_REJECTED, rejected.status) - assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, modeled.status) + assertEquals(UsvmPropertySearchStatus.PROPERTY_ERROR, modeled.status) + assertTrue(modeled.diagnostics.any { it.code == "usvm.precondition.threw" }) assertEquals(UsvmPropertyViolationTarget.PREDICATE_FALSE, modeled.target) assertEquals(listOf(JsConcreteValue.number(0.0)), modeled.inputs) assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, unsupported.status) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 80e389983f..0902d42d98 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt import org.usvm.CoverageZone +import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachine @@ -37,6 +38,7 @@ import org.usvm.statistics.collectors.CoveredNewStatesCollector import org.usvm.statistics.collectors.StatesCollector import org.usvm.statistics.collectors.TargetsReachedStatesCollector import org.usvm.statistics.constraints.SoftConstraintsObserver +import org.usvm.statistics.distances.CallStackDistanceCalculator import org.usvm.statistics.distances.CfgStatisticsImpl import org.usvm.statistics.distances.PlainCallGraphStatistics import org.usvm.stopstrategies.StopStrategy @@ -78,9 +80,13 @@ data class TsMachineAnalysisResult( val runtimeLimited: Boolean get() = unsupportedPaths.isNotEmpty() } +/** Symbolically executes TypeScript entry points with shared coverage guidance. */ class TsMachine( scene: EtsScene, - override val options: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), + override val options: UMachineOptions = UMachineOptions( + solverType = SolverType.YICES, + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + ), private val tsOptions: TsOptions, private val machineObserver: UMachineObserver? = null, private val observer: TsInterpreterObserver? = null, @@ -88,6 +94,10 @@ class TsMachine( unknownCallModels: TsUnknownCallModelCatalog? = null, /** Creates an observer with access to the analysis queue, including unsupported terminal states. */ private val machineObserverFactory: ((UPathSelector) -> UMachineObserver)? = null, + /** Replaces scheduling for a caller-owned objective without changing the interpreted program. */ + private val pathSelectorFactory: ((Map, TsGraph) -> UPathSelector)? = null, + /** Caller-owned monotonic deadline, checked before setup and between interpreter steps. */ + private val deadlineReached: (() -> Boolean)? = null, ) : UMachine() { init { val hasCompatibleCoverageScope = tsOptions.classCoverageTargets == null || @@ -143,6 +153,24 @@ class TsMachine( throwExceptionOnStepFailure = options.throwExceptionOnStepFailure, ) private val cfgStatistics = CfgStatisticsImpl(graph) + private val externallyCoveredStatements = hashSetOf() + private var coverageDistanceCalculator: CallStackDistanceCalculator? = null + + /** + * Reports caller-confirmed coverage on the analysis thread, including before analysis starts. + * This removes distance goals without changing native coverage counters or refreshing queued weights. + * Reports are retained across analyses on this machine. + */ + fun markCovered(statements: Collection): Boolean { + var changed = false + for (statement in statements) { + if (externallyCoveredStatements.add(statement)) { + coverageDistanceCalculator?.removeTarget(graph.methodOf(statement), statement) + changed = true + } + } + return changed + } /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */ fun analyze( @@ -186,8 +214,10 @@ class TsMachine( targets: List = emptyList(), configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, ): TsMachineAnalysisResult { + coverageDistanceCalculator = null interpreter.resetStepFailure() failureTrackingUnknownCallObserver.reset() + if (deadlineReached?.invoke() == true) return deadlineAnalysisResult() val (initialStates, unsupportedPaths, infeasibleEntryPoints) = createInitialStates(methods, targets, configureInitialState) @@ -207,15 +237,11 @@ class TsMachine( applicationGraph = graph, ) - val callGraphStatistics: PlainCallGraphStatistics = - when (options.targetSearchDepth) { - 0u -> PlainCallGraphStatistics() - else -> TODO("Unsupported yet") - } + val callGraphStatistics = createCallGraphStatistics() val timeStatistics = createTimeStatistics() - val pathSelector = createPathSelector( + val pathSelector = pathSelectorFactory?.invoke(initialStates, graph) ?: createPathSelector( initialStates = initialStates, options = options, applicationGraph = graph, @@ -223,6 +249,7 @@ class TsMachine( coverageStatisticsFactory = { coverageStatistics }, cfgStatisticsFactory = { cfgStatistics }, callGraphStatisticsFactory = { callGraphStatistics }, + coverageDistanceCalculatorFactory = { getCoverageDistanceCalculator(coverageStatistics) }, ) val statesCollector = createStatesCollector(coverageStatistics) @@ -250,7 +277,7 @@ class TsMachine( ) override fun shouldStop(): Boolean { - if (options.timeout <= kotlin.time.Duration.ZERO) { + if (options.timeout <= kotlin.time.Duration.ZERO || deadlineReached?.invoke() == true) { timedOut = true return true } @@ -319,6 +346,19 @@ class TsMachine( ) } + private fun createCallGraphStatistics(): PlainCallGraphStatistics = when (options.targetSearchDepth) { + 0u -> PlainCallGraphStatistics() + else -> TODO("Unsupported yet") + } + + private fun getCoverageDistanceCalculator( + coverageStatistics: CoverageStatistics, + ): CallStackDistanceCalculator = coverageDistanceCalculator ?: CallStackDistanceCalculator( + targets = coverageStatistics.getUncoveredStatements().filterNot { it in externallyCoveredStatements }, + cfgStatistics = cfgStatistics, + applicationGraph = graph, + ).also { coverageDistanceCalculator = it } + private fun createStatesCollector( coverageStatistics: CoverageStatistics, ): StatesCollector = when (options.stateCollectionStrategy) { @@ -370,6 +410,11 @@ class TsMachine( infeasibleEntryPoints = infeasibleEntryPoints, ) + private fun deadlineAnalysisResult(): TsMachineAnalysisResult = emptyAnalysisResult(emptySet(), emptyList()).copy( + stopReason = TsAnalysisStopReason.STOPPED, + timedOut = true, + ) + private data class InitialStatesResult( val initialStates: Map, val unsupportedPaths: MutableSet, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineExternalCoverageTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineExternalCoverageTest.kt new file mode 100644 index 0000000000..d2ce585a46 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineExternalCoverageTest.kt @@ -0,0 +1,103 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.CoverageZone +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.machine.state.TsState +import org.usvm.statistics.UMachineObserver +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.getResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** External coverage affects scheduling only, independently of native collection and stopping. */ +class TsMachineExternalCoverageTest : TsMethodTestRunner() { + override val scene = EtsScene( + projectFiles = listOf( + loadEtsFileAutoConvert( + getResourcePath("/samples/coverage/ClassCoverage.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + @Test + fun `TypeScript defaults to NURS and respects an explicit strategy`() { + TsMachine(scene = scene, tsOptions = TsOptions()).use { machine -> + assertEquals( + expected = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + actual = machine.options.pathSelectionStrategies, + ) + } + val explicitOptions = options.copy(pathSelectionStrategies = listOf(PathSelectionStrategy.BFS)) + + TsMachine(scene = scene, options = explicitOptions, tsOptions = TsOptions()).use { machine -> + assertEquals(expected = listOf(PathSelectionStrategy.BFS), actual = machine.options.pathSelectionStrategies) + } + } + + @Test + fun `external saturation before analysis neither stops execution nor suppresses native witnesses`() { + val method = getMethod(methodName = "entry", className = "HelperCoverage") + val statements = scene.projectClasses.flatMap { owner -> owner.methods.flatMap { it.cfg.stmts } } + val analysisOptions = options.copy( + coverageZone = CoverageZone.CLASS, + stateCollectionStrategy = StateCollectionStrategy.COVERED_NEW, + stopOnCoverage = 100, + timeout = Duration.INFINITE, + ) + + TsMachine(scene = scene, options = analysisOptions, tsOptions = TsOptions()).use { machine -> + assertTrue(machine.markCovered(statements)) + assertFalse(machine.markCovered(statements)) + + repeat(2) { + val result = machine.analyzeWithMetadata(methods = listOf(method)) + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + assertEquals(expected = 2, actual = result.states.size) + assertFalse(result.engineFailed) + } + } + } + + @Test + fun `external coverage can arrive on the analysis thread while paths are queued`() { + val method = getMethod(methodName = "entry", className = "HelperCoverage") + val statements = scene.projectClasses.flatMap { owner -> owner.methods.flatMap { it.cfg.stmts } } + lateinit var machine: TsMachine + var reported = false + val observer = object : UMachineObserver { + override fun onStatePeeked(state: TsState) { + if (!reported) { + reported = machine.markCovered(statements) + } + } + } + val analysisOptions = options.copy( + coverageZone = CoverageZone.CLASS, + stateCollectionStrategy = StateCollectionStrategy.COVERED_NEW, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + machine = TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + machineObserver = observer, + ) + + val result = machine.use { it.analyzeWithMetadata(methods = listOf(method)) } + + assertTrue(reported) + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + assertEquals(expected = 2, actual = result.states.size) + assertFalse(result.engineFailed) + } +} diff --git a/usvm-util/src/main/kotlin/org/usvm/algorithms/DeterministicPriorityCollection.kt b/usvm-util/src/main/kotlin/org/usvm/algorithms/DeterministicPriorityCollection.kt index af9eb77830..a2b866e182 100644 --- a/usvm-util/src/main/kotlin/org/usvm/algorithms/DeterministicPriorityCollection.kt +++ b/usvm-util/src/main/kotlin/org/usvm/algorithms/DeterministicPriorityCollection.kt @@ -17,10 +17,12 @@ class DeterministicPriorityCollection(private val comparator: Compa override val count: Int get() = priorityQueue.size + if (topElement == null) 0 else 1 override fun peek(): T { - if (topElement == null) { - topElement = priorityQueue.remove() - } - return topElement!!.first + val currentTop = topElement + if (currentTop != null) return currentTop.first + + val next = priorityQueue.remove() + topElement = next + return next.first } override fun update(element: T, priority: Priority) { @@ -44,7 +46,7 @@ class DeterministicPriorityCollection(private val comparator: Compa assert({ !priorityQueue.any { (e, _) -> e == element } }) { "Element already exists in priority queue" } val currentTop = topElement - if (currentTop != null && comparator.compare(currentTop.second, priority) < 0) { + if (currentTop != null && comparator.compare(currentTop.second, priority) > 0) { topElement = element to priority priorityQueue.add(currentTop) return diff --git a/usvm-util/src/test/kotlin/org/usvm/algorithms/DeterministicPriorityCollectionTest.kt b/usvm-util/src/test/kotlin/org/usvm/algorithms/DeterministicPriorityCollectionTest.kt new file mode 100644 index 0000000000..c5d182a099 --- /dev/null +++ b/usvm-util/src/test/kotlin/org/usvm/algorithms/DeterministicPriorityCollectionTest.kt @@ -0,0 +1,62 @@ +package org.usvm.algorithms + +import org.junit.jupiter.api.Test +import kotlin.test.assertEquals + +internal class DeterministicPriorityCollectionTest { + @Test + fun `adding a worse priority keeps the cached minimum`() { + val collection = DeterministicPriorityCollection(naturalOrder()) + collection.add(element = "first", priority = 1) + assertEquals("first", collection.peek()) + + collection.add(element = "second", priority = 2) + + assertEquals("first", collection.peek()) + collection.remove("first") + assertEquals("second", collection.peek()) + assertEquals(1, collection.count) + } + + @Test + fun `adding a better priority replaces the cached minimum`() { + val collection = DeterministicPriorityCollection(naturalOrder()) + collection.add(element = "second", priority = 2) + assertEquals("second", collection.peek()) + + collection.add(element = "first", priority = 1) + + assertEquals("first", collection.peek()) + collection.remove("first") + assertEquals("second", collection.peek()) + assertEquals(1, collection.count) + } + + @Test + fun `adding a worse priority keeps the cached maximum with reverse order`() { + val collection = DeterministicPriorityCollection(reverseOrder()) + collection.add(element = "first", priority = 2) + assertEquals("first", collection.peek()) + + collection.add(element = "second", priority = 1) + + assertEquals("first", collection.peek()) + collection.remove("first") + assertEquals("second", collection.peek()) + assertEquals(1, collection.count) + } + + @Test + fun `adding a better priority replaces the cached maximum with reverse order`() { + val collection = DeterministicPriorityCollection(reverseOrder()) + collection.add(element = "second", priority = 1) + assertEquals("second", collection.peek()) + + collection.add(element = "first", priority = 2) + + assertEquals("first", collection.peek()) + collection.remove("first") + assertEquals("second", collection.peek()) + assertEquals(1, collection.count) + } +}