From 71fdab8feabe6b16ccd46a33e1589ee1de320992 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 00:50:56 +0300 Subject: [PATCH] Add direct property campaign controls with a shared deadline --- .../usvm/ts/pbt/FastCheckDiagnosticCode.kt | 1 + .../ts/pbt/campaign/PropertyCampaignRunner.kt | 266 +++++++++++++++ .../usvm/ts/pbt/fastcheck/FastCheckBackend.kt | 15 +- .../pbt/fastcheck/FastCheckCoverageSession.kt | 19 ++ .../pbt/fastcheck/FastCheckProcessClient.kt | 53 ++- .../campaign/PropertyCampaignRunnerTest.kt | 312 ++++++++++++++++++ .../fastcheck/FastCheckProcessClientTest.kt | 38 +++ .../properties/campaign/DirectControls.ts | 23 ++ .../usvm/ts/pbt/usvm/UsvmPropertySearcher.kt | 4 + .../ts/pbt/usvm/UsvmPropertySearcherTest.kt | 15 + .../main/kotlin/org/usvm/machine/TsMachine.kt | 3 +- 11 files changed, 740 insertions(+), 9 deletions(-) create mode 100644 usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunner.kt create mode 100644 usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunnerTest.kt create mode 100644 usvm-ts-fast-check/src/test/resources/properties/campaign/DirectControls.ts diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt index c57a625e88..963ad07793 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/FastCheckDiagnosticCode.kt @@ -39,6 +39,7 @@ internal object FastCheckDiagnosticCode { const val BACKEND_RUNTIME_NOT_FOUND = "backend.runtime.not-found" const val COVERAGE_COLLECTOR_NOT_FOUND = "coverage.collector.not-found" + const val COVERAGE_COLLECTION_TIMEOUT = "coverage.collection.timeout" const val COVERAGE_RUNTIME_UNSUPPORTED = "coverage.runtime.unsupported" const val COVERAGE_RUNTIME_VERSION_UNAVAILABLE = "coverage.runtime.version-unavailable" diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunner.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunner.kt new file mode 100644 index 0000000000..5bc4afda2b --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunner.kt @@ -0,0 +1,266 @@ +package org.usvm.ts.pbt.campaign + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrGenerationTimeoutException +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.generateEtsIR +import org.jacodb.ets.utils.loadEtsProjectFromIR +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.ts.pbt.FastCheckDiagnosticCode +import org.usvm.ts.pbt.backend.ProjectionCapability +import org.usvm.ts.pbt.backend.ProjectionLevel +import org.usvm.ts.pbt.backend.PropertyFailureKind +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunResult +import org.usvm.ts.pbt.backend.WitnessEvidenceDelta +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayDeadline +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.captureWitness +import org.usvm.ts.pbt.fastcheck.BackendErrorKind +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.PropertyId +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.usvm.UsvmPropertySearchResult +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import org.usvm.ts.pbt.usvm.UsvmPropertySearcher +import org.usvm.ts.pbt.validation.requireValid +import org.usvm.ts.pbt.validation.validatePropertyDefinition +import java.io.IOException +import java.nio.file.Files +import java.nio.file.Path +import java.security.MessageDigest +import java.util.concurrent.CancellationException +import kotlin.time.Duration.Companion.milliseconds + +enum class PropertyCampaignMode { PBT_ONLY, SYMBOLIC_ONLY, SEQUENTIAL } + +enum class PropertyCampaignPhase { PREPARATION, PBT, SYMBOLIC, CONFIRMATION } + +/** COMPLETED describes orchestration; inspect the retained engine results for unsupported or incomplete work. */ +enum class PropertyCampaignStop { COMPLETED, DEADLINE, EXECUTION_FAILURE } + +/** Only native violations count as confirmed; symbolic inputs remain candidates until replay succeeds. */ +data class PropertyCampaignResult( + val propertyId: PropertyId, + val mode: PropertyCampaignMode, + val concrete: PropertyRunResult?, + val symbolic: UsvmPropertySearchResult?, + val confirmation: WitnessEvidenceDelta?, + val stop: PropertyCampaignStop, + val stoppedAt: PropertyCampaignPhase?, + val elapsedMillis: Long, + val diagnostic: String?, +) { + val confirmedViolation: Boolean + get() = concrete?.failure?.kind == PropertyFailureKind.PROPERTY || + confirmation?.status == WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION +} + +/** Direct controls over the same original property; coverage and observations are retained without feedback. */ +class PropertyCampaignRunner( + private val sourceRoot: Path, + private val tsconfig: Path? = null, + private val nodeExecutable: String = "node", + private val machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), +) { + fun run( + property: PropertyDefinition, + mode: PropertyCampaignMode, + configuration: PropertyRunConfiguration = PropertyRunConfiguration(), + validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS, + ): PropertyCampaignResult { + require(validationReserveMillis > 0) { "Validation reserve must be positive" } + val startedAt = System.nanoTime() + val deadline = WitnessReplayDeadline(timeoutMillis = configuration.timeoutMillis) + requireValid(validatePropertyDefinition(property)) + + var phase = PropertyCampaignPhase.PREPARATION + var concrete: PropertyRunResult? = null + var symbolic: UsvmPropertySearchResult? = null + var confirmation: WitnessEvidenceDelta? = null + + fun result( + stop: PropertyCampaignStop = PropertyCampaignStop.COMPLETED, + diagnostic: String? = null, + ) = PropertyCampaignResult( + propertyId = property.id, + mode = mode, + concrete = concrete, + symbolic = symbolic, + confirmation = confirmation, + stop = stop, + stoppedAt = phase.takeUnless { stop == PropertyCampaignStop.COMPLETED }, + elapsedMillis = (System.nanoTime() - startedAt) / NANOS_PER_MILLISECOND, + diagnostic = diagnostic, + ) + + try { + val root = sourceRoot.toRealPath() + val roots = listOf(root) + val backend = FastCheckBackend(sourceRoots = roots, nodeExecutable = nodeExecutable, tsconfig = tsconfig) + if (deadline.remainingMillis() <= 0) return result(PropertyCampaignStop.DEADLINE) + + if (mode != PropertyCampaignMode.SYMBOLIC_ONLY) { + phase = PropertyCampaignPhase.PBT + concrete = backend.run(property = property, configuration = configuration, deadline = deadline) + + val coverageTimedOut = concrete.coverage?.diagnostics?.any { diagnostic -> + diagnostic.code == FastCheckDiagnosticCode.COVERAGE_COLLECTION_TIMEOUT + } == true + if (coverageTimedOut || deadline.remainingMillis() <= 0) { + return result( + stop = PropertyCampaignStop.DEADLINE, + diagnostic = "Concrete result retained after the campaign or coverage collection timed out", + ) + } + val concreteViolation = concrete.failure?.kind == PropertyFailureKind.PROPERTY + if (concreteViolation) return result() + if (concrete.failure?.kind == PropertyFailureKind.TIMEOUT) { + return result(PropertyCampaignStop.DEADLINE) + } + if (mode == PropertyCampaignMode.PBT_ONLY) return result() + } + + phase = PropertyCampaignPhase.SYMBOLIC + if (deadline.remainingMillis() <= validationReserveMillis) { + return result(PropertyCampaignStop.DEADLINE) + } + + val sources = captureSources(property, root) + val frontendBudgetMillis = deadline.remainingMillis() - validationReserveMillis + if (frontendBudgetMillis <= 0) return result(PropertyCampaignStop.DEADLINE) + + val scene = loadScene(root = root, timeoutMillis = frontendBudgetMillis) + symbolic = search( + property = property, + root = root, + scene = scene, + deadline = deadline, + validationReserveMillis = validationReserveMillis, + ) + if (symbolic == null) return result(PropertyCampaignStop.DEADLINE) + + if (symbolic.target == null) { + return if (symbolic.status == UsvmPropertySearchStatus.TIMEOUT) { + result(PropertyCampaignStop.DEADLINE) + } else { + result() + } + } + + phase = PropertyCampaignPhase.CONFIRMATION + val candidate = symbolic.captureWitness(property = property, sources = sources) + + confirmation = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = WitnessReplayConfiguration( + timeoutMillis = configuration.timeoutMillis, + validationReserveMillis = validationReserveMillis, + coverageRequest = configuration.coverageRequest, + ), + deadline = deadline, + ) + + return if (confirmation.status == WitnessReplayStatus.TIMEOUT) { + result(PropertyCampaignStop.DEADLINE) + } else { + result() + } + } catch (error: PbtBackendException) { + val stop = if (error.kind == BackendErrorKind.TIMEOUT) { + PropertyCampaignStop.DEADLINE + } else { + PropertyCampaignStop.EXECUTION_FAILURE + } + return result(stop = stop, diagnostic = "${error.code}: ${error.message}") + } catch (error: CancellationException) { + throw error + } catch (error: InterruptedException) { + Thread.currentThread().interrupt() + throw error + } catch (error: EtsIrGenerationTimeoutException) { + return result(stop = PropertyCampaignStop.DEADLINE, diagnostic = error.message) + } catch (error: IOException) { + return result(stop = PropertyCampaignStop.EXECUTION_FAILURE, diagnostic = error.message) + } catch (error: IllegalArgumentException) { + return result(stop = PropertyCampaignStop.EXECUTION_FAILURE, diagnostic = error.message) + } catch (error: IllegalStateException) { + return result( + stop = PropertyCampaignStop.EXECUTION_FAILURE, + diagnostic = "${error.javaClass.simpleName}: ${error.message}", + ) + } + } + + private fun loadScene(root: Path, timeoutMillis: Long): EtsScene { + val directory = generateEtsIR( + keepPartialOutputOnFailure = false, + projectPath = root, + isProject = true, + loadEntrypoints = false, + useArkAnalyzerTypeInference = 1, + timeout = timeoutMillis.milliseconds, + provider = EtsIrProvider.TS_FRONTEND, + ) + + try { + return loadEtsProjectFromIR(projectFilesPath = directory, sdkFilesPath = null) + } finally { + directory.toFile().deleteRecursively() + } + } + + private fun search( + property: PropertyDefinition, + root: Path, + scene: EtsScene, + deadline: WitnessReplayDeadline, + validationReserveMillis: Long, + ): UsvmPropertySearchResult? { + if (deadline.remainingMillis() <= validationReserveMillis) return null + + val manifest = property.toManifest() + val mapping = PropertyEtsMapper(scene = scene, sourceRoots = listOf(root)).map(manifest) + val budgetMillis = deadline.remainingMillis() - validationReserveMillis + if (budgetMillis <= 0) return null + + val searchTimeout = minOf(machineOptions.timeout, budgetMillis.milliseconds) + return UsvmPropertySearcher( + scene = scene, + machineOptions = machineOptions.copy(timeout = searchTimeout, stopOnCoverage = 0), + ).search( + manifest = manifest, + mapping = mapping, + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + deadlineReached = { deadline.remainingMillis() <= validationReserveMillis }, + ) + } + + private fun captureSources(property: PropertyDefinition, root: Path): List { + val modules = listOfNotNull(property.predicate.module, property.precondition?.module).distinct() + + return modules.map { module -> + val path = root.resolve(module).toRealPath() + require(path.startsWith(root)) { "Property module escapes its source root: $module" } + + val hash = MessageDigest.getInstance("SHA-256") + .digest(Files.readAllBytes(path)) + .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and BYTE_MASK) } + + PropertyObservationSource(module = module, sha256 = hash) + } + } + + private companion object { + const val DEFAULT_VALIDATION_RESERVE_MILLIS = 5_000L + const val NANOS_PER_MILLISECOND = 1_000_000L + const val BYTE_MASK = 0xff + } +} 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 ceb5ebe4f9..a1cf92d9a2 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 @@ -44,6 +44,19 @@ class FastCheckBackend( override fun run( property: PropertyDefinition, configuration: PropertyRunConfiguration, + ): PropertyRunResult = execute(property, configuration, deadline = null) + + /** Charges preparation and the supervised process to the caller's existing deadline. */ + fun run( + property: PropertyDefinition, + configuration: PropertyRunConfiguration, + deadline: WitnessReplayDeadline, + ): PropertyRunResult = execute(property, configuration, deadline) + + private fun execute( + property: PropertyDefinition, + configuration: PropertyRunConfiguration, + deadline: WitnessReplayDeadline?, ): PropertyRunResult { requireValid(validatePropertyDefinition(property)) validateConfiguration(property, configuration) @@ -63,7 +76,7 @@ class FastCheckBackend( coverageRequest = configuration.coverageRequest, ) - return client.check(request) + return client.check(request, remainingMillis = deadline?.let { it::remainingMillis }) } override fun confirmWitness( 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 a380011f32..0a34c474be 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 @@ -5,6 +5,7 @@ import kotlinx.serialization.decodeFromString import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.BranchCoverage import org.usvm.ts.pbt.backend.CoverageDiagnostic +import org.usvm.ts.pbt.backend.CoverageProvenance import org.usvm.ts.pbt.backend.CoverageScope import org.usvm.ts.pbt.backend.PropertyCoverageArtifact import org.usvm.ts.pbt.backend.PropertyRunResult @@ -69,6 +70,24 @@ internal class FastCheckCoverageSession private constructor( return result.copy(coverage = artifact.value) } + /** Keeps a completed property result usable when its secondary coverage collection cannot finish. */ + fun incompleteArtifact(message: String) = PropertyCoverageArtifact( + backendId = FastCheckBackend.FAST_CHECK_BACKEND_ID, + backendVersion = FastCheckRuntimeMetadata.fastCheckVersion, + propertyId = PropertyId(request.manifest.propertyId), + provenance = CoverageProvenance( + collector = FastCheckRuntimeMetadata.coverageCollector, + runtimeId = "node", + runtimeVersion = runtimeVersion, + sourceRoots = request.sourceRoots, + request = requireNotNull(request.coverageRequest), + ), + files = emptyList(), + diagnostics = listOf( + CoverageDiagnostic(code = FastCheckDiagnosticCode.COVERAGE_COLLECTION_TIMEOUT, message = message), + ), + ) + fun readArtifact(): FastCheckOperationResult { val remaining = remainingMillis?.invoke() if (remaining != null && remaining <= 0) { diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt index 085aeef2be..0d2a9cc59c 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClient.kt @@ -24,33 +24,72 @@ internal class FastCheckProcessClient( ) /** Executes one request and exposes only a fully validated common result. */ - fun check(request: FastCheckExecutionRequest): PropertyRunResult { + fun check( + request: FastCheckExecutionRequest, + remainingMillis: (() -> Long)? = null, + ): PropertyRunResult { val encodedRequest = encodeRequest(request) val coverageSession = request.coverageRequest?.let { - FastCheckCoverageSession.prepare( - nodeExecutable = nodeExecutable, - adapterEntryPoint = adapterEntryPoint, - request = request, - ) + if (remainingMillis == null) { + FastCheckCoverageSession.prepare( + nodeExecutable = nodeExecutable, + adapterEntryPoint = adapterEntryPoint, + request = request, + ) + } else { + val prepared = FastCheckCoverageSession.prepareWithinBudget( + nodeExecutable = nodeExecutable, + adapterEntryPoint = adapterEntryPoint, + request = request, + remainingMillis = remainingMillis, + ) + when (prepared) { + is FastCheckOperationResult.Completed -> prepared.value + is FastCheckOperationResult.TimedOut -> throw deadlineExpired(request, prepared.message) + } + } } try { + val phaseLimit = saturatedAdd(request.timeoutMillis, transportGraceMillis) + val processBudget = remainingMillis?.invoke()?.coerceAtMost(phaseLimit) ?: phaseLimit + if (processBudget <= 0) throw deadlineExpired(request, "Property campaign deadline expired") + val output = invokeAdapter( encodedRequest = encodedRequest, request = request, command = coverageSession?.adapterCommand ?: listOf(nodeExecutable, adapterEntryPoint.toString()), + timeoutMillis = processBudget, ) validateProcessOutput(output, request) val response = decodeResponse(output.stdout, request) val result = decodeSuccessfulResponse(response, request) - return coverageSession?.attachTo(result) ?: result + if (coverageSession == null) return result + if (remainingMillis == null) return coverageSession.attachTo(result) + + return when (val artifact = coverageSession.readArtifact()) { + is FastCheckOperationResult.Completed -> result.copy(coverage = artifact.value) + is FastCheckOperationResult.TimedOut -> result.copy( + coverage = coverageSession.incompleteArtifact(message = artifact.message), + ) + } } finally { coverageSession?.close() } } + private fun deadlineExpired( + request: FastCheckExecutionRequest, + message: String, + ): PbtBackendException = backendError( + kind = BackendErrorKind.TIMEOUT, + code = FastCheckDiagnosticCode.BACKEND_PROCESS_TIMEOUT, + message = message, + request = request, + ) + /** One external operation, using the same supervised transport and optional original-source collector. */ fun witness( request: FastCheckExecutionRequest, diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunnerTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunnerTest.kt new file mode 100644 index 0000000000..0f9b338b10 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignRunnerTest.kt @@ -0,0 +1,312 @@ +package org.usvm.ts.pbt.campaign + +import kotlinx.serialization.json.Json +import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.CoverageScope +import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.PropertyFailureKind +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.backend.WitnessReductionStatus +import org.usvm.ts.pbt.backend.WitnessReplayDeadline +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.fastcheck.BackendErrorKind +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.fastcheck.PbtBackendException +import org.usvm.ts.pbt.model.ExecutionKind +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertyAssertion +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.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.testResourcesRoot +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +import java.nio.file.Files +import kotlin.io.path.createTempDirectory +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class PropertyCampaignRunnerTest { + private val root = testResourcesRoot().resolve("properties/campaign") + private val runner = PropertyCampaignRunner(sourceRoot = root) + private val configuration = PropertyRunConfiguration(seed = 354, numRuns = 1, timeoutMillis = 60_000) + + @Test + fun `PBT only preserves the original admission and named check without symbolic work`() { + val property = property().copy( + predicate = property().predicate.copy(checkResultExportName = "namedResult"), + assertions = listOf( + PropertyAssertion( + id = "not-forty-two", + source = PropertySourcePoint(module = MODULE, line = 5, column = 1), + ), + ), + ) + + val result = runner.run( + property = property, + mode = PropertyCampaignMode.PBT_ONLY, + configuration = configuration.copy(examples = listOf(listOf(JsConcreteValue.number(42.0)))), + ) + + assertTrue(result.confirmedViolation) + assertEquals("not-forty-two", result.concrete?.failure?.checkId) + assertEquals(PropertyFailureKind.PROPERTY, result.concrete?.failure?.kind) + assertEquals(property.id, result.propertyId) + assertNull(result.symbolic) + assertNull(result.confirmation) + } + + @Test + fun `symbolic only searches the original predicate and confirms and reduces the exact candidate`() { + val result = runner.run( + property = property(), + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + ) + + assertNull(result.concrete) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.symbolic?.status) + assertEquals(listOf(JsConcreteValue.number(42.0)), result.symbolic?.inputs) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.confirmation?.status) + assertEquals(result.symbolic?.inputs, result.confirmation?.candidate?.inputs) + assertEquals(listOf(JsConcreteValue.number(42.0)), result.confirmation?.reduction?.inputs) + assertEquals(WitnessReductionStatus.EXHAUSTED, result.confirmation?.reduction?.status) + assertTrue(result.confirmedViolation) + } + + @Test + fun `sequential runs symbolic search after a concrete run with no finding`() { + val result = runner.run( + property = property(), + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration.copy(examples = listOf(listOf(JsConcreteValue.number(20.0)))), + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.concrete?.status) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.symbolic?.status) + assertTrue(result.confirmedViolation) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, result.confirmation?.status) + } + + @Test + fun `sequential retains a concrete violation without demanding another engine`() { + val result = runner.run( + property = property(), + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration.copy(examples = listOf(listOf(JsConcreteValue.number(42.0)))), + ) + + assertTrue(result.confirmedViolation) + assertEquals(listOf(JsConcreteValue.number(42.0)), result.concrete?.counterexample) + assertNull(result.symbolic) + assertNull(result.confirmation) + assertEquals(PropertyCampaignStop.COMPLETED, result.stop) + } + + @Test + fun `direct concrete control retains its actual requested source coverage`() { + val result = runner.run( + property = property(), + mode = PropertyCampaignMode.PBT_ONLY, + configuration = configuration.copy( + coverageRequest = PropertyCoverageRequest(scopes = setOf(CoverageScope.PROPERTY_ENTRY_POINTS)), + ), + ) + + val coverage = assertNotNull(result.concrete?.coverage) + assertTrue(coverage.files.isNotEmpty()) + assertEquals(PropertyCampaignStop.COMPLETED, result.stop) + assertNull(result.symbolic) + } + + @Test + fun `unsupported symbolic work retains the real successful concrete run`() { + val asynchronous = property().copy( + predicate = TypeScriptEntryPoint( + module = MODULE, + exportName = "asyncHolds", + executionKind = ExecutionKind.ASYNC, + ), + ) + + val result = runner.run( + property = asynchronous, + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.concrete?.status) + assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, result.symbolic?.status) + assertFalse(result.confirmedViolation) + assertNull(result.confirmation) + } + + @Test + fun `named checks without an executable binding retain the unconfirmed symbolic candidate`() { + val named = property().copy( + assertions = listOf( + PropertyAssertion( + id = "not-forty-two", + source = PropertySourcePoint(module = MODULE, line = 5, column = 1), + ), + ), + ) + + val result = runner.run( + property = named, + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + ) + + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.symbolic?.status) + assertNotNull(result.symbolic?.inputs) + assertEquals(WitnessReplayStatus.UNSUPPORTED_REPLAY, result.confirmation?.status) + assertFalse(result.confirmedViolation) + } + + @Test + fun `an exhausted search allocation retains the completed concrete result`() { + val result = runner.run( + property = property(), + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration, + validationReserveMillis = configuration.timeoutMillis, + ) + + assertEquals(PropertyRunStatus.SUCCESS, result.concrete?.status) + assertEquals(PropertyCampaignStop.DEADLINE, result.stop) + assertEquals(PropertyCampaignPhase.SYMBOLIC, result.stoppedAt) + assertNull(result.symbolic) + assertFalse(result.confirmedViolation) + } + + @Test + fun `an expired total budget does not become a no finding symbolic result`() { + val result = runner.run( + property = property(), + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration.copy(timeoutMillis = 1), + validationReserveMillis = 1, + ) + + assertEquals(PropertyCampaignStop.DEADLINE, result.stop) + assertNull(result.symbolic) + assertNull(result.confirmation) + assertFalse(result.confirmedViolation) + } + + @Test + fun `a native process timeout consumes the shared budget and prevents symbolic fallback`() { + val hanging = property().copy(predicate = TypeScriptEntryPoint(module = MODULE, exportName = "hangs")) + + val result = runner.run( + property = hanging, + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration.copy(timeoutMillis = 100), + validationReserveMillis = 1, + ) + + assertEquals(PropertyCampaignStop.DEADLINE, result.stop) + assertEquals(PropertyCampaignPhase.PBT, result.stoppedAt) + assertNull(result.symbolic) + assertTrue(result.elapsedMillis < 5_000, "A 100 ms campaign acquired a fresh backend timeout") + } + + @Test + fun `the backend does not reset an already consumed caller deadline`() { + val deadline = WitnessReplayDeadline(timeoutMillis = 1) + while (deadline.remainingMillis() > 0) Thread.onSpinWait() + val backend = FastCheckBackend(sourceRoots = listOf(root)) + + val error = assertFailsWith { + backend.run(property = property(), configuration = configuration, deadline = deadline) + } + + assertEquals(BackendErrorKind.TIMEOUT, error.kind) + } + + @Test + fun `confirmation timeout preserves the exact unconfirmed symbolic candidate`() { + val directory = createTempDirectory(prefix = "campaign-confirmation-timeout-") + val executable = directory.resolve("waiting-node") + executable.writeText("#!/bin/sh\nexec node -e 'setInterval(() => {}, 1000)'\n") + check(executable.toFile().setExecutable(true)) + val waitingRunner = PropertyCampaignRunner(sourceRoot = root, nodeExecutable = executable.toString()) + + try { + val result = waitingRunner.run( + property = property(), + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration.copy(timeoutMillis = 10_000), + validationReserveMillis = 1_000, + ) + + assertEquals(listOf(JsConcreteValue.number(42.0)), result.symbolic?.inputs) + assertEquals(result.symbolic?.inputs, result.confirmation?.candidate?.inputs) + assertEquals(WitnessReplayStatus.TIMEOUT, result.confirmation?.status) + assertEquals(PropertyCampaignStop.DEADLINE, result.stop) + assertEquals(PropertyCampaignPhase.CONFIRMATION, result.stoppedAt) + assertFalse(result.confirmedViolation) + } finally { + directory.toFile().deleteRecursively() + } + } + + @Test + fun `failed symbolic preparation retains the previously completed concrete result`() { + val directory = createTempDirectory(prefix = "campaign-source-change-") + val module = directory.resolve(MODULE) + module.writeText( + """ + import { unlinkSync } from 'node:fs'; + export function removesSource(value: number): boolean { + unlinkSync(${Json.encodeToUtf8SafeString(module.toString())}); + return value === value; + } + """.trimIndent(), + ) + val changingProperty = property().copy( + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "removesSource"), + precondition = null, + ) + + try { + val result = PropertyCampaignRunner(sourceRoot = directory).run( + property = changingProperty, + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration, + ) + + assertFalse(Files.exists(module)) + assertEquals(PropertyRunStatus.SUCCESS, result.concrete?.status) + assertEquals(PropertyCampaignStop.EXECUTION_FAILURE, result.stop) + assertEquals(PropertyCampaignPhase.SYMBOLIC, result.stoppedAt) + assertNotNull(result.diagnostic) + assertNull(result.symbolic) + assertFalse(result.confirmedViolation) + } finally { + directory.toFile().deleteRecursively() + } + } + + private fun property() = PropertyDefinition( + id = PropertyId(value = "campaign.isolated"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 0, max = 100))), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "isolatedFailure"), + precondition = TypeScriptEntryPoint(module = MODULE, exportName = "admits"), + ) + + private companion object { + const val MODULE = "DirectControls.ts" + } +} diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt index fe81c063cd..cf67f0fcdd 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckProcessClientTest.kt @@ -1,7 +1,9 @@ package org.usvm.ts.pbt.fastcheck import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.FastCheckDiagnosticCode import org.usvm.ts.pbt.backend.PropertyCoverageRequest +import org.usvm.ts.pbt.backend.PropertyFailureKind import org.usvm.ts.pbt.backend.PropertyRunStatus import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.model.BooleanDomain @@ -26,9 +28,45 @@ import kotlin.io.path.writeText import kotlin.test.assertEquals import kotlin.test.assertFailsWith import kotlin.test.assertFalse +import kotlin.test.assertNotNull import kotlin.test.assertTrue class FastCheckProcessClientTest { + @Test + fun `coverage deadline expiry retains the native violation with an incomplete artifact`() { + val directory = createTempDirectory(prefix = "completed-property-coverage-timeout-") + val marker = directory.resolve("completed") + directory.resolve("property.ts").writeText( + """ + import { writeFileSync } from 'node:fs'; + export function predicate(value: boolean): boolean { + writeFileSync(${marker.toJavaScriptStringLiteral()}, 'done'); + return false; + } + """.trimIndent(), + ) + val client = FastCheckProcessClient(adapterEntryPoint = FastCheckRuntime.executionEntryPoint()) + + try { + val result = client.check( + request = validRequest.copy( + sourceRoots = listOf(directory.toString()), + coverageRequest = PropertyCoverageRequest(), + ), + remainingMillis = { if (Files.exists(marker)) 0L else 10_000L }, + ) + + assertEquals(PropertyRunStatus.FAILURE, result.status) + assertEquals(PropertyFailureKind.PROPERTY, result.failure?.kind) + assertNotNull(result.counterexample) + val coverage = assertNotNull(result.coverage) + assertTrue(coverage.files.isEmpty()) + assertEquals(FastCheckDiagnosticCode.COVERAGE_COLLECTION_TIMEOUT, coverage.diagnostics.single().code) + } finally { + directory.toFile().deleteRecursively() + } + } + @Test fun `interrupted coverage version probe terminates its process and preserves interruption`() { val runtime = createTempDirectory(prefix = "interrupted-version-probe-") diff --git a/usvm-ts-fast-check/src/test/resources/properties/campaign/DirectControls.ts b/usvm-ts-fast-check/src/test/resources/properties/campaign/DirectControls.ts new file mode 100644 index 0000000000..e8a0f3ca69 --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/campaign/DirectControls.ts @@ -0,0 +1,23 @@ +export function admits(value: number): boolean { + return value >= 20; +} + +export function isolatedFailure(value: number): boolean { + return value !== 42; +} + +export function namedResult(value: number): { passed: boolean; checkId: string; actual: number; expected: number } { + return { passed: value !== 42, checkId: 'not-forty-two', actual: value, expected: 42 }; +} + +export async function asyncHolds(value: number): Promise { + return value === value; +} + +export function hangs(value: number): boolean { + while (value === value) { + // The native process supervisor must stop this invocation. + } + + return true; +} 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..28acbc86e0 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 @@ -46,6 +46,7 @@ class UsvmPropertySearcher( manifest: PropertyManifest, mapping: PropertyEtsMappingArtifact, concreteCapability: ProjectionCapability, + deadlineReached: (() -> Boolean)? = null, ): UsvmPropertySearchResult { val capability = capabilityResolver.resolve( manifest = manifest, @@ -79,6 +80,7 @@ class UsvmPropertySearcher( predicate = predicate, precondition = precondition, capability = capability, + deadlineReached = deadlineReached, ) } @@ -87,6 +89,7 @@ class UsvmPropertySearcher( predicate: EtsEntryPointTarget, precondition: EtsEntryPointTarget?, capability: UsvmPropertyProjectionCapability, + deadlineReached: (() -> Boolean)?, ): UsvmPropertySearchResult { lateinit var projection: UsvmDeclaredDomainProjection val target = UsvmViolationTsTarget() @@ -99,6 +102,7 @@ class UsvmPropertySearcher( options = machineOptions, tsOptions = tsOptions, machineObserver = observer, + deadlineReached = deadlineReached, ).use { machine -> val analysis = machine.analyzeWithMetadata( methods = listOf(predicate.method), diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt index ba5c59748b..bee127d202 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt @@ -340,6 +340,21 @@ class UsvmPropertySearcherTest { assertEquals(UsvmPropertySearchStatus.TIMEOUT, result.status) } + @Test + fun `a caller deadline stops the machine before its independent timeout`() { + val manifest = manifest(predicateExport = "violatedProperty") + + val result = searcher.search( + manifest = manifest, + mapping = mapper.map(manifest), + concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT), + deadlineReached = { true }, + ) + + assertEquals(UsvmPropertySearchStatus.TIMEOUT, result.status) + assertNull(result.inputs) + } + private fun search(manifest: PropertyManifest): UsvmPropertySearchResult = searcher.search( manifest = manifest, mapping = mapper.map(manifest), 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 85b3bd587c..53dec66050 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -83,6 +83,7 @@ class TsMachine( unknownCallModels: TsUnknownCallModelCatalog? = null, /** Creates an observer with access to the analysis queue, including unsupported terminal states. */ private val machineObserverFactory: ((UPathSelector) -> UMachineObserver)? = null, + private val deadlineReached: (() -> Boolean)? = null, ) : UMachine() { init { val hasCompatibleCoverageScope = tsOptions.classCoverageTargets == null || @@ -243,7 +244,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 }