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 4af4985aae..7b2bc81865 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 @@ -31,6 +31,8 @@ import { type ObservationRequest, } from './observe-property.js'; +const runtimeVersion = process.version; + export interface PropertyManifestInput { name: string; domain: unknown; @@ -98,6 +100,7 @@ export interface FastCheckRunResult { numShrinks: number; failure: FastCheckFailureDetails | null; executionTimeMillis: number; + runtimeVersion: string; observations?: ObservationArtifact; } @@ -433,6 +436,7 @@ function toRunResult( numShrinks: details.numShrinks, failure, executionTimeMillis, + runtimeVersion, }; if (observations !== undefined) result.observations = observations; 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..99c3a6dda0 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 @@ -25,6 +25,7 @@ test('execution CLI emits one successful response document', async () => { assert.equal(invocation.stderr, ''); assert.equal(invocation.stdout.trim().split('\n').length, 1); assert.equal(response.status, 'ok'); + assert.equal((response.result as Record).runtimeVersion, process.version); assert.equal('protocolVersion' in response, false); } finally { await rm(sourceRoot, { recursive: true, force: true }); @@ -48,6 +49,7 @@ test('execution CLI keeps one JSON response after a predicate adds inherited toJ await writeFile(sourceRoot + '/property.ts', ` export function predicate(value: boolean) { Object.prototype.toJSON = () => { throw new Error('sentinel toJSON'); }; + Object.defineProperty(process, 'version', { value: 'changed-by-property' }); return value; } `); @@ -58,6 +60,7 @@ export function predicate(value: boolean) { assert.equal(invocation.exitCode, 0); assert.equal(invocation.stdout.trim().split('\n').length, 1); assert.equal(response.status, 'ok'); + assert.equal((response.result as Record).runtimeVersion, process.version); } finally { await rm(sourceRoot, { recursive: true, force: true }); } diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt index 456ce62ef4..ce1287e775 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt @@ -12,7 +12,8 @@ import java.nio.file.Path /** * The declared property and direct-run controls with the results actually produced. - * Constructor settings such as machine options, runtime paths and tsconfig are not attested here. + * Metadata records selected files and requested runtime settings, with an explicit limited source scope. + * Effective machine options and complete project/build identities are not attested here. * Existing source and tool identities remain in the property and result provenance; absent identities stay unknown. */ @Serializable @@ -22,6 +23,7 @@ data class PropertyCampaignArtifact( val validationReserveMillis: Long, val result: PropertyCampaignResult, val targetRole: WitnessRole = WitnessRole.PROPERTY, + val metadata: PropertyCampaignMetadata? = null, ) { init { val resultProperties = listOfNotNull( diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignMetadata.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignMetadata.kt new file mode 100644 index 0000000000..553fb39556 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignMetadata.kt @@ -0,0 +1,40 @@ +package org.usvm.ts.pbt.campaign + +import kotlinx.serialization.Serializable +import org.usvm.ts.pbt.observation.PropertyObservationSource +import java.nio.file.Files +import java.nio.file.Path +import java.security.MessageDigest + +/** Files read before engine work; imports, automatically discovered configuration and build outputs are excluded. */ +@Serializable +enum class PropertyCampaignSourceScope { + PROPERTY_ENTRY_MODULES, +} + +/** One explicitly supplied concrete-runtime configuration file, without its extended configuration closure. */ +@Serializable +data class PropertyCampaignTsconfig( + val path: String, + val sha256: String, +) + +/** + * Requested execution settings and the selected files observed before any engine work. + * This is not a full project/build identity: machine options, imports and effective tsconfig are not recorded. + * Observed Node versions belong to the actual concrete run and witness replay results. + */ +@Serializable +data class PropertyCampaignMetadata( + val sourceRoot: String, + val requestedNodeCommand: String, + val sources: List, + val explicitConcreteTsconfig: PropertyCampaignTsconfig? = null, + val sourceScope: PropertyCampaignSourceScope = PropertyCampaignSourceScope.PROPERTY_ENTRY_MODULES, +) + +internal fun campaignSourceSha256(path: Path): String = MessageDigest.getInstance("SHA-256") + .digest(Files.readAllBytes(path)) + .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and BYTE_MASK) } + +private const val BYTE_MASK = 0xff 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 index 17fa372a68..e18dc3b36a 100644 --- 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 @@ -33,9 +33,7 @@ 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 @@ -81,22 +79,12 @@ class PropertyCampaignRunner( configuration: PropertyRunConfiguration = PropertyRunConfiguration(), validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS, ): PropertyCampaignArtifact { - val result = run(property, mode, configuration, validationReserveMillis) - - return PropertyCampaignArtifact(property, configuration, validationReserveMillis, result) - } - - 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 metadata: PropertyCampaignMetadata? = null var phase = PropertyCampaignPhase.PREPARATION var concrete: PropertyRunResult? = null var symbolic: UsvmPropertySearchResult? = null @@ -105,39 +93,46 @@ class PropertyCampaignRunner( 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, + ) = PropertyCampaignArtifact( + property = property, + configuration = configuration, + validationReserveMillis = validationReserveMillis, + result = 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, + ), + metadata = metadata, ) 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) + + metadata = captureMetadata(property = property, root = root) + if (deadline.remainingMillis() <= 0) return result(PropertyCampaignStop.DEADLINE) + + val backend = FastCheckBackend(listOf(root), 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 + val coverageTimedOut = coverageCollectionTimedOut(concrete) 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.PROPERTY) return result() if (concrete.failure?.kind == PropertyFailureKind.TIMEOUT) { return result(PropertyCampaignStop.DEADLINE) } @@ -216,6 +211,32 @@ class PropertyCampaignRunner( } } + fun run( + property: PropertyDefinition, + mode: PropertyCampaignMode, + configuration: PropertyRunConfiguration = PropertyRunConfiguration(), + validationReserveMillis: Long = DEFAULT_VALIDATION_RESERVE_MILLIS, + ): PropertyCampaignResult = runArtifact(property, mode, configuration, validationReserveMillis).result + + private fun captureMetadata(property: PropertyDefinition, root: Path): PropertyCampaignMetadata { + val explicitTsconfig = tsconfig?.toRealPath() + val configuration = explicitTsconfig?.let { path -> + PropertyCampaignTsconfig(path = path.toString(), sha256 = campaignSourceSha256(path)) + } + + return PropertyCampaignMetadata( + sourceRoot = root.toString(), + requestedNodeCommand = nodeExecutable, + sources = captureSources(property = property, root = root), + explicitConcreteTsconfig = configuration, + ) + } + + private fun coverageCollectionTimedOut(result: PropertyRunResult): Boolean = + result.coverage?.diagnostics?.any { diagnostic -> + diagnostic.code == FastCheckDiagnosticCode.COVERAGE_COLLECTION_TIMEOUT + } == true + private fun loadScene(root: Path, timeoutMillis: Long): EtsScene { val directory = generateEtsIR( keepPartialOutputOnFailure = false, @@ -267,17 +288,12 @@ class PropertyCampaignRunner( 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) + PropertyObservationSource(module = module, sha256 = campaignSourceSha256(path)) } } 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/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignMetadataTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignMetadataTest.kt new file mode 100644 index 0000000000..40786536c2 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignMetadataTest.kt @@ -0,0 +1,217 @@ +package org.usvm.ts.pbt.campaign + +import kotlinx.serialization.json.JsonObject +import kotlinx.serialization.json.jsonObject +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.IntegerDomain +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.model.encodeToUtf8SafeString +import org.usvm.ts.pbt.testResourcesRoot +import java.nio.file.Files +import java.nio.file.Path +import java.security.MessageDigest +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class PropertyCampaignMetadataTest { + @TempDir + lateinit var directory: Path + + private val configuration = PropertyRunConfiguration(seed = 354, numRuns = 1, timeoutMillis = 60_000) + + @Test + fun `no finding records selected modules and explicit settings without a version probe`() { + val oracle = directory.resolve("Oracle.ts") + oracle.writeText( + "import { holds } from './Helper'; export function predicate(value: number) { return holds(value); }", + ) + directory.resolve("Helper.ts").writeText("export function holds(value: number) { return value === value; }") + val admission = directory.resolve("Admission.ts") + admission.writeText("export function admits(value: number) { return value >= 0; }") + val tsconfig = directory.resolve("tsconfig.json") + tsconfig.writeText("""{"compilerOptions":{"target":"ES2020"}}""") + val executable = directory.resolve("node-without-version-probe") + executable.writeText("#!/bin/sh\nif [ \"${'$'}1\" = \"--version\" ]; then exit 90; fi\nexec node \"${'$'}@\"\n") + check(executable.toFile().setExecutable(true)) + val property = property().copy( + predicate = TypeScriptEntryPoint(module = "Oracle.ts", exportName = "predicate"), + precondition = TypeScriptEntryPoint(module = "Admission.ts", exportName = "admits"), + ) + + val artifact = PropertyCampaignRunner( + sourceRoot = directory.resolve("."), + tsconfig = tsconfig, + nodeExecutable = executable.toString(), + ).runArtifact(property, PropertyCampaignMode.PBT_ONLY, configuration) + val restored = saveAndRead(artifact) + + val metadata = assertNotNull(restored.metadata) + assertEquals(directory.toRealPath().toString(), metadata.sourceRoot) + assertEquals(executable.toString(), metadata.requestedNodeCommand) + assertEquals(PropertyCampaignSourceScope.PROPERTY_ENTRY_MODULES, metadata.sourceScope) + assertEquals( + mapOf("Oracle.ts" to hash(oracle), "Admission.ts" to hash(admission)), + metadata.sources.associate { source -> source.module to source.sha256 }, + ) + assertEquals( + PropertyCampaignTsconfig(path = tsconfig.toRealPath().toString(), sha256 = hash(tsconfig)), + metadata.explicitConcreteTsconfig, + ) + assertEquals(PropertyRunStatus.SUCCESS, restored.result.concrete?.status) + assertTrue(assertNotNull(restored.result.concrete?.runtimeVersion).startsWith("v")) + assertFalse(restored.result.confirmedViolation) + assertEquals(artifact, restored) + } + + @Test + fun `a concrete violation survives source removal after the initial snapshot`() { + val module = directory.resolve("DirectControls.ts") + module.writeText( + """ + import { unlinkSync } from 'node:fs'; + export function isolatedFailure(value: number): boolean { + unlinkSync(${PropertyManifestJson.json.encodeToUtf8SafeString(module.toString())}); + return false; + } + """.trimIndent(), + ) + val initialHash = hash(module) + + val artifact = PropertyCampaignRunner(sourceRoot = directory).runArtifact( + property = property(), + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration, + ) + val restored = saveAndRead(artifact) + + assertFalse(Files.exists(module)) + assertTrue(restored.result.confirmedViolation) + assertEquals(PropertyCampaignStop.COMPLETED, restored.result.stop) + assertEquals(initialHash, restored.metadata?.sources?.single()?.sha256) + assertNotNull(restored.result.concrete?.runtimeVersion) + assertNull(restored.result.symbolic) + } + + @Test + fun `native confirmation still checks source freshness after both snapshots`() { + val module = directory.resolve("DirectControls.ts") + Files.copy(testResourcesRoot().resolve("properties/campaign/DirectControls.ts"), module) + val initialHash = hash(module) + val executable = directory.resolve("changing-node") + executable.writeText("#!/bin/sh\nprintf '\\n// changed before replay\\n' >> '$module'\nexec node \"${'$'}@\"\n") + check(executable.toFile().setExecutable(true)) + + val artifact = PropertyCampaignRunner( + sourceRoot = directory, + nodeExecutable = executable.toString(), + ).runArtifact(property(), PropertyCampaignMode.SYMBOLIC_ONLY, configuration) + val restored = saveAndRead(artifact) + + assertNotNull(restored.result.symbolic?.inputs) + val confirmation = assertNotNull(restored.result.confirmation) + assertEquals(WitnessReplayStatus.SOURCE_MISMATCH, confirmation.status) + assertEquals(initialHash, restored.metadata?.sources?.single()?.sha256) + assertEquals(initialHash, confirmation.candidate.sources.single().sha256) + assertFalse(restored.result.confirmedViolation) + assertNull(restored.result.concrete) + assertNotNull(confirmation.originalReplay?.runtimeVersion) + } + + @Test + fun `symbolic candidate uses the later source revision while metadata retains the initial snapshot`() { + val module = directory.resolve("DirectControls.ts") + val changedSource = "export function isolatedFailure(value: number): boolean { return value !== 42; }" + val changedJson = PropertyManifestJson.json.encodeToUtf8SafeString(changedSource) + module.writeText( + """ + import { writeFileSync } from 'node:fs'; + export function isolatedFailure(value: number): boolean { + writeFileSync(${PropertyManifestJson.json.encodeToUtf8SafeString(module.toString())}, $changedJson); + return true; + } + """.trimIndent(), + ) + val initialHash = hash(module) + + val artifact = PropertyCampaignRunner(sourceRoot = directory).runArtifact( + property = property(), + mode = PropertyCampaignMode.SEQUENTIAL, + configuration = configuration, + ) + val restored = saveAndRead(artifact) + + assertEquals(PropertyRunStatus.SUCCESS, restored.result.concrete?.status) + val confirmation = assertNotNull(restored.result.confirmation) + assertEquals(initialHash, restored.metadata?.sources?.single()?.sha256) + assertEquals(hash(module), confirmation.candidate.sources.single().sha256) + assertFalse(initialHash == hash(module)) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, confirmation.status) + assertTrue(restored.result.confirmedViolation) + } + + @Test + fun `source capture failure remains a preparation failure without a fabricated runtime`() { + val artifact = PropertyCampaignRunner(sourceRoot = directory).runArtifact( + property = property(), + mode = PropertyCampaignMode.PBT_ONLY, + configuration = configuration, + ) + + assertEquals(PropertyCampaignStop.EXECUTION_FAILURE, artifact.result.stop) + assertEquals(PropertyCampaignPhase.PREPARATION, artifact.result.stoppedAt) + assertNotNull(artifact.result.diagnostic) + assertNull(artifact.metadata) + assertNull(artifact.result.concrete) + assertFalse(artifact.result.confirmedViolation) + } + + @Test + fun `previous artifacts remain readable with unknown metadata and runtime version`() { + val artifact = PropertyCampaignRunner(sourceRoot = testResourcesRoot().resolve("properties/campaign")) + .runArtifact(property(), PropertyCampaignMode.PBT_ONLY, configuration) + val json = PropertyManifestJson.json.parseToJsonElement( + PropertyManifestJson.json.encodeToUtf8SafeString(artifact), + ).jsonObject + val result = json.getValue("result").jsonObject + val concrete = JsonObject(result.getValue("concrete").jsonObject - "runtimeVersion") + val previousResult = JsonObject(result + ("concrete" to concrete)) + val previous = JsonObject((json - "metadata") + ("result" to previousResult)) + val path = directory.resolve("previous.json") + Files.writeString(path, previous.toString()) + + val restored = PropertyCampaignArtifact.read(path) + + assertNull(restored.metadata) + assertNull(restored.result.concrete?.runtimeVersion) + assertEquals(artifact.result.concrete?.counterexample, restored.result.concrete?.counterexample) + } + + private fun property() = PropertyDefinition( + id = PropertyId(value = "metadata.property"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 0, max = 100))), + predicate = TypeScriptEntryPoint(module = "DirectControls.ts", exportName = "isolatedFailure"), + ) + + private fun saveAndRead(artifact: PropertyCampaignArtifact): PropertyCampaignArtifact { + val path = directory.resolve("campaign.json") + artifact.write(path) + + return PropertyCampaignArtifact.read(path) + } + + private fun hash(path: Path): String = MessageDigest.getInstance("SHA-256") + .digest(Files.readAllBytes(path)) + .joinToString(separator = "") { byte -> "%02x".format(byte) } +} 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 5bf804c305..c853d859d6 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 @@ -118,6 +118,8 @@ data class PropertyRunResult( val executionTimeMillis: Long, val coverage: PropertyCoverageArtifact? = null, val observations: PropertyObservationArtifact? = null, + /** Version reported by the process that actually executed this property, absent when unknown. */ + val runtimeVersion: String? = null, ) { init { require(numRuns >= 0) { "Run count must not be negative" }