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 new file mode 100644 index 0000000000..456ce62ef4 --- /dev/null +++ b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifact.kt @@ -0,0 +1,49 @@ +package org.usvm.ts.pbt.campaign + +import kotlinx.serialization.Serializable +import kotlinx.serialization.decodeFromString +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.WitnessRole +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import java.nio.file.Files +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. + * Existing source and tool identities remain in the property and result provenance; absent identities stay unknown. + */ +@Serializable +data class PropertyCampaignArtifact( + val property: PropertyDefinition, + val configuration: PropertyRunConfiguration, + val validationReserveMillis: Long, + val result: PropertyCampaignResult, + val targetRole: WitnessRole = WitnessRole.PROPERTY, +) { + init { + val resultProperties = listOfNotNull( + result.propertyId, + result.concrete?.propertyId, + result.symbolic?.propertyId, + result.confirmation?.candidate?.propertyId, + ) + val sameProperty = resultProperties.all { it == property.id } + require(sameProperty) { "Campaign evidence belongs to another property" } + require(validationReserveMillis > 0) { "Validation reserve must be positive" } + require(targetRole == WitnessRole.PROPERTY) { "Direct controls search the original property" } + } + + /** Writes this completed snapshot; failure leaves the caller's artifact available for another destination. */ + fun write(path: Path) { + val json = PropertyManifestJson.json.encodeToUtf8SafeString(this) + Files.writeString(path, json) + } + + companion object { + fun read(path: Path): PropertyCampaignArtifact = + PropertyManifestJson.json.decodeFromString(Files.readString(path)) + } +} 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 5bc4afda2b..17fa372a68 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 @@ -1,5 +1,6 @@ package org.usvm.ts.pbt.campaign +import kotlinx.serialization.Serializable import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrGenerationTimeoutException import org.jacodb.ets.utils.EtsIrProvider @@ -38,14 +39,18 @@ import java.security.MessageDigest import java.util.concurrent.CancellationException import kotlin.time.Duration.Companion.milliseconds +@Serializable enum class PropertyCampaignMode { PBT_ONLY, SYMBOLIC_ONLY, SEQUENTIAL } +@Serializable enum class PropertyCampaignPhase { PREPARATION, PBT, SYMBOLIC, CONFIRMATION } /** COMPLETED describes orchestration; inspect the retained engine results for unsupported or incomplete work. */ +@Serializable enum class PropertyCampaignStop { COMPLETED, DEADLINE, EXECUTION_FAILURE } /** Only native violations count as confirmed; symbolic inputs remain candidates until replay succeeds. */ +@Serializable data class PropertyCampaignResult( val propertyId: PropertyId, val mode: PropertyCampaignMode, @@ -69,6 +74,18 @@ class PropertyCampaignRunner( private val nodeExecutable: String = "node", private val machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), ) { + /** Captures the requested direct controls and their actual result without repeating execution. */ + fun runArtifact( + property: PropertyDefinition, + mode: PropertyCampaignMode, + 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, diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifactTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifactTest.kt new file mode 100644 index 0000000000..1095fccad5 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/PropertyCampaignArtifactTest.kt @@ -0,0 +1,312 @@ +package org.usvm.ts.pbt.campaign + +import kotlinx.serialization.json.JsonObject +import kotlinx.serialization.json.JsonPrimitive +import kotlinx.serialization.json.jsonObject +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +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.WitnessReductionStatus +import org.usvm.ts.pbt.backend.WitnessReplayConfiguration +import org.usvm.ts.pbt.backend.WitnessReplayStatus +import org.usvm.ts.pbt.backend.WitnessRole +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.ConstantDomain +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.PropertyOperand +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.observation.ObservationOrigin +import org.usvm.ts.pbt.observation.ObservationPointKind +import org.usvm.ts.pbt.observation.PropertyObservationPoint +import org.usvm.ts.pbt.observation.PropertyObservationRequest +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.testResourcesRoot +import org.usvm.ts.pbt.usvm.UsvmPropertySearchStatus +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.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +class PropertyCampaignArtifactTest { + @TempDir + lateinit var directory: Path + + private val root = testResourcesRoot() + private val configuration = PropertyRunConfiguration(seed = 354, numRuns = 1, timeoutMillis = 60_000) + + @Test + fun `saved concrete violation retains actual source coverage and bounded observations`() { + val module = "properties/real/ArrayArbitraryProperty.ts" + val source = PropertySourcePoint(module = module, line = 16, column = 5) + val call = PropertySourcePoint(module = module, line = 18, column = 22) + val property = PropertyDefinition( + id = PropertyId(value = "artifact.observed"), + inputs = listOf( + PropertyInput( + name = "values", + domain = ArrayDomain(IntegerDomain(min = 0, max = 10), minLength = 0, maxLength = 8), + ), + ), + predicate = TypeScriptEntryPoint(module = module, exportName = "originalUniqueOracle"), + assertions = listOf( + PropertyAssertion( + id = "no-duplicates", + source = PropertySourcePoint(module = module, line = 20, column = 5), + testedCall = call, + operands = listOf(PropertyOperand(id = "input-array", source = source)), + ), + ), + ) + val hash = MessageDigest.getInstance("SHA-256").digest(Files.readAllBytes(root.resolve(module))) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + val duplicate = JsConcreteValue.Array(listOf(JsConcreteValue.number(1.0), JsConcreteValue.number(1.0))) + val requested = configuration.copy( + examples = listOf(listOf(duplicate)), + coverageRequest = PropertyCoverageRequest(scopes = setOf(CoverageScope.PROPERTY_ENTRY_POINTS)), + observationRequest = PropertyObservationRequest( + sources = listOf(PropertyObservationSource(module = module, sha256 = hash)), + points = listOf( + PropertyObservationPoint( + id = "input-array", + assertionId = "no-duplicates", + operandId = "input-array", + source = source, + callSite = call, + kind = ObservationPointKind.ARGUMENT, + inputIndex = 0, + ), + ), + ), + ) + + val artifact = PropertyCampaignRunner(sourceRoot = root).runArtifact( + property = property, + mode = PropertyCampaignMode.PBT_ONLY, + configuration = requested, + ) + val restored = saveAndRead(artifact) + + assertTrue(restored.result.confirmedViolation) + assertEquals(PropertyFailureKind.PROPERTY, restored.result.concrete?.failure?.kind) + assertEquals("no-duplicates", restored.property.assertions.single().id) + assertEquals(requested, restored.configuration) + assertTrue(assertNotNull(restored.result.concrete?.coverage).files.isNotEmpty()) + val observations = assertNotNull(restored.result.concrete?.observations) + val invocation = observations.invocations.first() + assertEquals(listOf(PropertyObservationSource(module = module, sha256 = hash)), observations.verifiedSources) + assertEquals(ObservationOrigin.FAST_CHECK, invocation.origin) + assertEquals(duplicate, invocation.points.single().value.value) + assertNull(restored.result.symbolic) + assertEquals(artifact, restored) + } + + @Test + fun `saved symbolic candidate keeps native confirmation reduction and available provenance`() { + val artifact = PropertyCampaignRunner(sourceRoot = root.resolve("properties/campaign")).runArtifact( + property = symbolicProperty(), + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + ) + + val restored = saveAndRead(artifact) + + assertNull(restored.result.concrete) + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, restored.result.symbolic?.status) + assertEquals(listOf(JsConcreteValue.number(42.0)), restored.result.symbolic?.inputs) + val confirmation = assertNotNull(restored.result.confirmation) + assertEquals(WitnessReplayStatus.CONFIRMED_PROPERTY_VIOLATION, confirmation.status) + assertEquals(WitnessReductionStatus.EXHAUSTED, confirmation.reduction.status) + assertEquals(listOf(JsConcreteValue.number(42.0)), confirmation.reduction.inputs) + assertTrue(confirmation.candidate.sources.isNotEmpty()) + assertNotNull(confirmation.originalReplay?.runtimeVersion) + assertEquals("fast-check", confirmation.backendId) + assertEquals(WitnessRole.PROPERTY, restored.targetRole) + assertTrue(restored.result.confirmedViolation) + assertNull(restored.property.sourceIdentity) + assertEquals(artifact, restored) + + val mismatched = confirmation.copy( + candidate = confirmation.candidate.copy(propertyId = PropertyId(value = "other.property")), + ) + assertFailsWith { + artifact.copy(result = artifact.result.copy(confirmation = mismatched)) + } + val symbolic = assertNotNull(artifact.result.symbolic) + val otherSymbolic = symbolic.copy(propertyId = PropertyId(value = "other.property")) + val mixedResult = artifact.result.copy(symbolic = otherSymbolic) + assertFailsWith { + artifact.copy(result = mixedResult) + } + } + + @Test + fun `saved unsupported native replay retains the original unconfirmed candidate`() { + val property = symbolicProperty().copy( + assertions = listOf( + PropertyAssertion( + id = "not-forty-two", + source = PropertySourcePoint(module = "DirectControls.ts", line = 5, column = 1), + ), + ), + ) + val artifact = PropertyCampaignRunner(sourceRoot = root.resolve("properties/campaign")).runArtifact( + property = property, + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + ) + + val restored = saveAndRead(artifact) + + assertNotNull(restored.result.symbolic?.inputs) + assertEquals(restored.result.symbolic?.inputs, restored.result.confirmation?.candidate?.inputs) + assertEquals(WitnessReplayStatus.UNSUPPORTED_REPLAY, restored.result.confirmation?.status) + assertFalse(restored.result.confirmedViolation) + assertEquals(artifact, restored) + } + + @Test + fun `saved confirmation timeout retains its candidate and campaign stop phase`() { + val property = symbolicProperty() + val sourceRoot = root.resolve("properties/campaign") + val prepared = PropertyCampaignRunner(sourceRoot = sourceRoot).runArtifact( + property = property, + mode = PropertyCampaignMode.SYMBOLIC_ONLY, + configuration = configuration, + ) + val candidate = assertNotNull(prepared.result.confirmation).candidate + assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, prepared.result.symbolic?.status) + + val executable = directory.resolve("waiting-node") + val started = directory.resolve("waiting-node-started") + executable.writeText( + "#!/bin/sh\nprintf started > \"$started\"\nexec node -e 'setInterval(() => {}, 1000)'\n", + ) + check(executable.toFile().setExecutable(true)) + val backend = FastCheckBackend( + sourceRoots = listOf(sourceRoot), + nodeExecutable = executable.toString(), + ) + + val confirmation = backend.confirmWitness( + property = property, + candidate = candidate, + configuration = WitnessReplayConfiguration(timeoutMillis = 1_000, validationReserveMillis = 250), + ) + + // Serialization needs a real timeout snapshot without charging frontend startup to the replay budget. + val artifact = prepared.copy( + result = prepared.result.copy( + confirmation = confirmation, + stop = PropertyCampaignStop.DEADLINE, + stoppedAt = PropertyCampaignPhase.CONFIRMATION, + ), + ) + val restored = saveAndRead(artifact) + + assertTrue(Files.isRegularFile(started), "The native confirmation process did not start") + assertEquals(PropertyCampaignStop.DEADLINE, restored.result.stop) + assertEquals(PropertyCampaignPhase.CONFIRMATION, restored.result.stoppedAt) + assertEquals(WitnessReplayStatus.TIMEOUT, restored.result.confirmation?.status) + assertEquals(listOf(JsConcreteValue.number(42.0)), restored.result.confirmation?.candidate?.inputs) + assertEquals(candidate, restored.result.confirmation?.candidate) + assertEquals(configuration, restored.configuration) + assertEquals(prepared.validationReserveMillis, restored.validationReserveMillis) + assertFalse(restored.result.confirmedViolation) + assertEquals(artifact, restored) + } + + @Test + fun `UTF8 file preserves native special-value inputs and isolated UTF16 surrogates`() { + val values = listOf( + JsConcreteValue.number(-0.0), + JsConcreteValue.number(Double.NaN), + JsConcreteValue.String(value = "\ud800"), + JsConcreteValue.Undefined, + JsConcreteValue.number(Double.POSITIVE_INFINITY), + ) + val property = PropertyDefinition( + id = PropertyId(value = "artifact.special-values"), + inputs = values.mapIndexed { index, value -> + PropertyInput(name = "value$index", domain = ConstantDomain(value)) + }, + predicate = TypeScriptEntryPoint( + module = "properties/witness/ExternalWitness.ts", + exportName = "specialValues", + ), + ) + val artifact = PropertyCampaignRunner(sourceRoot = root).runArtifact( + property = property, + mode = PropertyCampaignMode.PBT_ONLY, + configuration = configuration.copy(examples = listOf(values)), + ) + + val restored = saveAndRead(artifact) + + assertTrue(restored.result.confirmedViolation) + assertEquals(values, restored.result.concrete?.counterexample) + assertEquals(listOf(values), restored.configuration.examples) + assertTrue(Files.readString(directory.resolve("campaign.json")).contains("\\ud800")) + assertEquals(artifact, restored) + } + + @Test + fun `artifact rejects a result for a different property during creation and file reading`() { + val artifact = PropertyCampaignRunner(sourceRoot = root.resolve("properties/campaign")).runArtifact( + property = symbolicProperty(), + mode = PropertyCampaignMode.PBT_ONLY, + configuration = configuration, + ) + val other = artifact.result.copy(propertyId = PropertyId(value = "other.property")) + + assertFailsWith { artifact.copy(result = other) } + val concrete = assertNotNull(artifact.result.concrete) + val otherConcrete = concrete.copy(propertyId = PropertyId(value = "other.property")) + val mixedResult = artifact.result.copy(concrete = otherConcrete) + assertFailsWith { + artifact.copy(result = mixedResult) + } + + val path = directory.resolve("campaign.json") + artifact.write(path) + val json = PropertyManifestJson.json.parseToJsonElement(Files.readString(path)).jsonObject + val result = json.getValue("result").jsonObject + val mismatchedConcrete = JsonObject( + result.getValue("concrete").jsonObject + ("propertyId" to JsonPrimitive("other.property")), + ) + val mismatchedResult = JsonObject(result + ("concrete" to mismatchedConcrete)) + Files.writeString(path, JsonObject(json + ("result" to mismatchedResult)).toString()) + + assertFailsWith { PropertyCampaignArtifact.read(path) } + } + + private fun saveAndRead(artifact: PropertyCampaignArtifact): PropertyCampaignArtifact { + val path = directory.resolve("campaign.json") + artifact.write(path) + + return PropertyCampaignArtifact.read(path) + } + + private fun symbolicProperty() = PropertyDefinition( + id = PropertyId(value = "artifact.symbolic"), + inputs = listOf(PropertyInput(name = "value", domain = IntegerDomain(min = 0, max = 100))), + predicate = TypeScriptEntryPoint(module = "DirectControls.ts", exportName = "isolatedFailure"), + precondition = TypeScriptEntryPoint(module = "DirectControls.ts", exportName = "admits"), + ) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt index 5772b997aa..ca28e3adf5 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/ProjectionCapability.kt @@ -1,6 +1,9 @@ package org.usvm.ts.pbt.backend +import kotlinx.serialization.Serializable + /** Describes how faithfully a backend can project a Kotlin property domain. */ +@Serializable enum class ProjectionLevel { /** Every value produced by the backend has the declared Kotlin domain semantics. */ EXACT, @@ -13,6 +16,7 @@ enum class ProjectionLevel { } /** Describes which execution modes remain available for a complete property. */ +@Serializable enum class PropertyCapabilityLevel { /** Both concrete and symbolic projections preserve the declared property semantics. */ EXACT, @@ -34,6 +38,7 @@ enum class PropertyCapabilityLevel { * @property message human-readable description of the limitation * @property path location of the affected value in the property model */ +@Serializable data class CapabilityDiagnostic( val code: String, val message: String, @@ -46,6 +51,7 @@ data class CapabilityDiagnostic( * @property level semantic fidelity of the projection * @property diagnostics limitations and directions that explain a non-exact [level] */ +@Serializable data class ProjectionCapability( val level: ProjectionLevel, val diagnostics: List = emptyList(), 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..5bf804c305 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 @@ -21,6 +21,7 @@ interface PropertyBasedTestingBackend { } /** Backend-neutral controls for one concrete property run. */ +@Serializable data class PropertyRunConfiguration( val seed: Int? = null, val replayPath: String? = null, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt index 8b075df90a..0e2c168f32 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionModel.kt @@ -1,5 +1,6 @@ package org.usvm.ts.pbt.usvm +import kotlinx.serialization.Serializable import org.usvm.machine.TsOptions import org.usvm.ts.pbt.backend.ProjectionCapability import org.usvm.ts.pbt.backend.PropertyCapabilityLevel @@ -19,6 +20,7 @@ data class UsvmProjectionOptions( } /** Capability of one ordered property input at its stable manifest path. */ +@Serializable data class UsvmInputProjectionCapability( val inputName: String, val path: String, @@ -26,6 +28,7 @@ data class UsvmInputProjectionCapability( ) /** Combined concrete and symbolic execution capability for one property. */ +@Serializable data class UsvmPropertyProjectionCapability( val inputs: List, val precondition: ProjectionCapability, 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..427f532566 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 @@ -1,10 +1,12 @@ package org.usvm.ts.pbt.usvm +import kotlinx.serialization.Serializable import org.usvm.ts.pbt.backend.CapabilityDiagnostic import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyId /** Terminal outcome of one USVM property-violation search. */ +@Serializable enum class UsvmPropertySearchStatus { VIOLATION_REACHED, NO_VIOLATION_REACHED, @@ -18,6 +20,7 @@ enum class UsvmPropertySearchStatus { } /** Supported ways in which a mapped predicate can violate its property. */ +@Serializable enum class UsvmPropertyViolationTarget { PREDICATE_FALSE, UNEXPECTED_EXCEPTION, @@ -25,6 +28,7 @@ enum class UsvmPropertyViolationTarget { } /** Backend-neutral result of searching one mapped TypeScript property with USVM. */ +@Serializable data class UsvmPropertySearchResult( val propertyId: PropertyId, val status: UsvmPropertySearchStatus,