From deebfbbbc84adb9461bafa69463605f44d54b441 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 17 Oct 2026 00:43:03 +0300 Subject: [PATCH] Allow explicit large native input exports within matching transport bounds --- .../fast-check-adapter/src/input-export.ts | 2 +- .../test/input-export.test.ts | 13 ++++++- usvm-ts-fast-check/scripts/pbt_experiment.py | 4 +- .../scripts/test_pbt_experiment.py | 12 ++++++ .../pbt/fastcheck/FastCheckProcessClient.kt | 21 ++++++++-- .../campaign/GuidedPropertyCampaignTest.kt | 12 ++++-- .../pbt/fastcheck/FastCheckInputExportTest.kt | 39 +++++++++++++++++++ .../ts/pbt/backend/PropertyInputExport.kt | 10 +++-- 8 files changed, 97 insertions(+), 16 deletions(-) diff --git a/usvm-ts-fast-check/fast-check-adapter/src/input-export.ts b/usvm-ts-fast-check/fast-check-adapter/src/input-export.ts index 15d101df3a..250ae5f1ff 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/input-export.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/input-export.ts @@ -88,7 +88,7 @@ export function validateInputExportRequest(value: unknown, manifest: PropertyMan && Number.isInteger(request.maxInvocations) && (request.maxInvocations as number) >= 1 && (request.maxInvocations as number) <= 100_000 && Number.isInteger(request.maxBytes) && (request.maxBytes as number) >= 1024 - && (request.maxBytes as number) <= 2 * 1024 * 1024 + && (request.maxBytes as number) <= 64 * 1024 * 1024 && Number.isInteger(request.maxArrayElements) && (request.maxArrayElements as number) >= 1 && (request.maxArrayElements as number) <= 64 && Array.isArray(request.sources); if (!valid) throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid input export bounds', 'inputExportRequest'); diff --git a/usvm-ts-fast-check/fast-check-adapter/test/input-export.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/input-export.test.ts index 588542e87c..c8426ddbc9 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/input-export.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/input-export.test.ts @@ -6,6 +6,7 @@ import path from 'node:path'; import test from 'node:test'; import { executeProperty } from '../src/execute-property.js'; import { ProtocolError } from '../src/js-value.js'; +import { validateInputExportRequest } from '../src/input-export.js'; const source = `export async function delayed(value: number): Promise { await new Promise(resolve => setTimeout(resolve, 100)); return true; @@ -14,7 +15,7 @@ const source = `export async function delayed(value: number): Promise { function request(sourceRoot: string) { return { manifest: { propertyId: 'input.late', inputs: [{ name: 'value', domain: { kind: 'integer', min: 0, max: 1 } }], - predicate: { module: 'properties.ts', exportName: 'delayed', executionKind: 'async' } }, + predicate: { module: 'properties.ts', exportName: 'delayed', executionKind: 'async' as const } }, sourceRoots: [sourceRoot], seed: 37, numRuns: 1, timeoutMillis: 10, examples: [], inputExportRequest: { sources: [{ module: 'properties.ts', sha256: createHash('sha256').update(source).digest('hex') }], maxInvocations: 100, maxBytes: 65_536, maxArrayElements: 16 }, @@ -41,7 +42,7 @@ test('a late asynchronous outcome cannot rewrite the already published input rec test('input export rejects invalid wire bounds and source identities before loading the property', async () => { const invalid = [ - { ...request('/missing').inputExportRequest, maxBytes: 2 * 1024 * 1024 + 1 }, + { ...request('/missing').inputExportRequest, maxBytes: 64 * 1024 * 1024 + 1 }, { ...request('/missing').inputExportRequest, maxInvocations: 100_001 }, { ...request('/missing').inputExportRequest, sources: [null] }, { ...request('/missing').inputExportRequest, sources: [{ module: 'other.ts', sha256: '0'.repeat(64) }] }, @@ -51,3 +52,11 @@ test('input export rejects invalid wire bounds and source identities before load error => error instanceof ProtocolError && error.code === 'protocol.request.invalid'); } }); + +test('explicit large input export remains bounded without changing the ordinary byte allowance', () => { + const ordinary = request('/unused'); + const large = { ...ordinary.inputExportRequest, maxBytes: 64 * 1024 * 1024 }; + + assert.equal(validateInputExportRequest(large, ordinary.manifest).maxBytes, 64 * 1024 * 1024); + assert.equal(validateInputExportRequest(ordinary.inputExportRequest, ordinary.manifest).maxBytes, 65_536); +}); diff --git a/usvm-ts-fast-check/scripts/pbt_experiment.py b/usvm-ts-fast-check/scripts/pbt_experiment.py index 1bd4b57d38..cfd46872e8 100644 --- a/usvm-ts-fast-check/scripts/pbt_experiment.py +++ b/usvm-ts-fast-check/scripts/pbt_experiment.py @@ -81,9 +81,9 @@ def validate_manifest(manifest): raise ValueError("PBT, runner validation and class replay allocations must fit the total budget") valid_limits = manifest["numRuns"] > 0 and 0 < manifest["pbtInputLimit"] <= 100_000 \ and manifest["symbolicInputLimit"] > 0 and 1 <= manifest["maxArrayElements"] <= 64 \ - and 1024 <= manifest["maxObservationBytes"] <= 2 * 1024 * 1024 + and 1024 <= manifest["maxObservationBytes"] <= 64 * 1024 * 1024 if not valid_limits: - raise ValueError("Frozen limits must fit the compact export's 100000-record/64-element/2MiB contract") + raise ValueError("Frozen limits must fit the compact export's 100000-record/64-element/64MiB contract") unique_cases = manifest["cases"] and len({case["id"] for case in manifest["cases"]}) == len(manifest["cases"]) if not unique_cases: raise ValueError("The manifest must contain distinct case identities") diff --git a/usvm-ts-fast-check/scripts/test_pbt_experiment.py b/usvm-ts-fast-check/scripts/test_pbt_experiment.py index de9a1154c0..80c293d750 100644 --- a/usvm-ts-fast-check/scripts/test_pbt_experiment.py +++ b/usvm-ts-fast-check/scripts/test_pbt_experiment.py @@ -152,6 +152,18 @@ def test_functional_quota_and_early_success_are_not_full_budget_results(self): self.assertTrue(driver.full_budget_eligible(row)) + def test_budget_driven_quota_is_independent_of_the_explicit_large_capture_limit(self): + manifest = driver.read_json(ROOT.parent / "experiments/two-phase-smoke/manifest.json") + manifest.update(comparisonKind="equal-budget", numRuns=1_000_000, + pbtInputLimit=100_000, maxObservationBytes=64 * 1024 * 1024) + + driver.validate_manifest(manifest) + + manifest["maxObservationBytes"] += 1 + with self.assertRaisesRegex(ValueError, "64MiB"): + driver.validate_manifest(manifest) + + def test_process_timeout_retains_raw_output_and_failure(self): process = driver.run_process( ["node", "-e", "process.stdout.write('started'); setInterval(() => {}, 1000)"], self.root, "slow", 0.2, 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 89c6037ec7..5c9ccbe487 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 @@ -2,6 +2,7 @@ package org.usvm.ts.pbt.fastcheck import kotlinx.serialization.decodeFromString import org.usvm.ts.pbt.FastCheckDiagnosticCode +import org.usvm.ts.pbt.backend.PropertyInputExportRequest import org.usvm.ts.pbt.backend.PropertyRunResult import org.usvm.ts.pbt.manifest.PropertyManifestJson import org.usvm.ts.pbt.model.JsConcreteValue @@ -19,10 +20,22 @@ internal class FastCheckProcessClient( private val transportGraceMillis: Long = DEFAULT_TRANSPORT_GRACE_MILLIS, private val shutdownGraceMillis: Long = DEFAULT_SHUTDOWN_GRACE_MILLIS, ) { - private val transport = FastCheckProcessTransport( + private val defaultTransport = createTransport(maxStdoutBytes = MAX_STDOUT_BYTES) + + private fun transport(request: FastCheckExecutionRequest): FastCheckProcessTransport { + val requestedBytes = request.inputExportRequest?.maxBytes ?: PropertyInputExportRequest.DEFAULT_MAX_BYTES + val additionalExportBytes = (requestedBytes - PropertyInputExportRequest.DEFAULT_MAX_BYTES) + .coerceAtLeast(minimumValue = 0) + + if (additionalExportBytes == 0) return defaultTransport + + return createTransport(maxStdoutBytes = MAX_STDOUT_BYTES + additionalExportBytes) + } + + private fun createTransport(maxStdoutBytes: Int) = FastCheckProcessTransport( nodeExecutable = nodeExecutable, maxRequestBytes = MAX_REQUEST_BYTES, - maxStdoutBytes = MAX_STDOUT_BYTES, + maxStdoutBytes = maxStdoutBytes, maxStderrBytes = MAX_STDERR_BYTES, shutdownGraceMillis = shutdownGraceMillis, ) @@ -179,7 +192,7 @@ internal class FastCheckProcessClient( command: List, timeoutMillis: Long, ): FastCheckOperationResult = try { - transport.invokeWithResult( + transport(request).invokeWithResult( command = command, request = encodedRequest, timeoutMillis = timeoutMillis, @@ -202,7 +215,7 @@ internal class FastCheckProcessClient( command: List, timeoutMillis: Long = saturatedAdd(request.timeoutMillis, transportGraceMillis), ): FastCheckProcessOutput = try { - transport.invoke( + transport(request).invoke( command = command, request = encodedRequest, timeoutMillis = timeoutMillis, diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/GuidedPropertyCampaignTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/GuidedPropertyCampaignTest.kt index fc39124bcb..a2a4caadd4 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/GuidedPropertyCampaignTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/campaign/GuidedPropertyCampaignTest.kt @@ -68,7 +68,9 @@ class GuidedPropertyCampaignTest { val configuration = configuration.copy( examples = examples(1), inputExportRequest = PropertyInputExportRequest( - sources = listOf(PropertyObservationSource(module = MODULE, sha256 = campaignSourceSha256(root.resolve(MODULE)))), + sources = listOf( + PropertyObservationSource(module = MODULE, sha256 = campaignSourceSha256(root.resolve(MODULE))) + ), ), ) @@ -79,10 +81,12 @@ class GuidedPropertyCampaignTest { pbtAllocationMillis = 15_000, ) - assertEquals(1, artifact.result.concrete?.inputExport?.records?.size) - assertNull(artifact.result.concrete?.observations) + val concrete = assertNotNull(artifact.result.concrete) + assertEquals(1, concrete.inputExport?.records?.size) + assertNull(concrete.observations) assertNotNull(artifact.result.symbolic?.edgeGuidance) - assertTrue(assertNotNull(artifact.result.concrete?.coverage).provenance.request.admittedOnly) + val concreteCoverage = assertNotNull(concrete.coverage) + assertTrue(concreteCoverage.provenance.request.admittedOnly) } @Test diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckInputExportTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckInputExportTest.kt index 72954d93a6..6835d4eec6 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckInputExportTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckInputExportTest.kt @@ -99,6 +99,45 @@ class FastCheckInputExportTest { assertEquals(text, firstInput.elements.single()) } + @Test + fun `explicit large input export crosses the ordinary stdout limit without losing inputs`() { + val text = JsConcreteValue.String("x".repeat(n = 9000) + "\uD800") + val property = property(predicate = "textHolds", domain = ConstantDomain(value = text)) + val requests = listOf( + PropertyInputExportRequest(sources = sources), + PropertyInputExportRequest(sources = sources, maxBytes = 8 * 1024 * 1024), + ) + + val results = requests.map { request -> + backend.run( + property, + configuration.copy( + numRuns = 600, + inputExportRequest = request, + observationRequest = PropertyObservationRequest(points = emptyList(), sources = sources), + coverageRequest = PropertyCoverageRequest(admittedOnly = true), + ), + ) + } + + val ordinary = assertNotNull(results[0].inputExport) + val large = assertNotNull(results[1].inputExport) + val encodedBytes = PropertyManifestJson.json.encodeToUtf8SafeString(large).toByteArray(Charsets.UTF_8).size + assertEquals(2 * 1024 * 1024, requests[0].maxBytes) + assertEquals(PropertyRunStatus.SUCCESS, results[1].status) + assertEquals(600, large.records.size) + assertTrue(encodedBytes > 4 * 1024 * 1024) + assertTrue(encodedBytes <= requests[1].maxBytes) + assertTrue(ordinary.droppedInvocations > 0) + assertEquals(0, large.droppedInvocations) + assertEquals(0, large.unsupportedInputs) + assertEquals(0, large.pendingInvocations) + assertNotNull(results[1].coverage) + assertNotNull(results[1].observations) + val firstInput = large.records.first().input.value as JsConcreteValue.Array + assertEquals(text, firstInput.elements.single()) + } + @Test fun `UTF16 and array inputs survive the actual process and artifact roundtrip`() { val values = JsConcreteValue.Array(listOf(JsConcreteValue.String("\uD800"), JsConcreteValue.String("\uDC00"))) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyInputExport.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyInputExport.kt index dd06d9bf9d..899fd4e507 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyInputExport.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/backend/PropertyInputExport.kt @@ -13,14 +13,19 @@ import org.usvm.ts.pbt.observation.PropertyObservationValue data class PropertyInputExportRequest( val sources: List, val maxInvocations: Int = 20_000, - val maxBytes: Int = MAX_INPUT_EXPORT_BYTES, + val maxBytes: Int = DEFAULT_MAX_BYTES, val maxArrayElements: Int = MAX_INPUT_EXPORT_ARRAY_ELEMENTS, ) { init { require(maxInvocations in 1..MAX_INPUT_EXPORT_INVOCATIONS) - require(maxBytes in MIN_INPUT_EXPORT_BYTES..MAX_INPUT_EXPORT_BYTES) + require(maxBytes in MIN_INPUT_EXPORT_BYTES..MAX_BYTES) require(maxArrayElements in 1..MAX_INPUT_EXPORT_ARRAY_ELEMENTS) } + + companion object { + const val DEFAULT_MAX_BYTES: Int = 2 * 1024 * 1024 + const val MAX_BYTES: Int = 64 * 1024 * 1024 + } } /** The input snapshot precedes precondition and predicate mutations. */ @@ -50,6 +55,5 @@ data class PropertyInputExportArtifact( } internal const val MIN_INPUT_EXPORT_BYTES = 1024 -internal const val MAX_INPUT_EXPORT_BYTES = 2 * 1024 * 1024 internal const val MAX_INPUT_EXPORT_INVOCATIONS = 100_000 internal const val MAX_INPUT_EXPORT_ARRAY_ELEMENTS = 64