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 b63ba1306a..5451d23632 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 @@ -20,11 +20,25 @@ import { protocolError, type TaggedJsValue, } from './js-value.js'; -import { projectDomain } from './project-domain.js'; +import { buildPropertyArbitrary, validateJointGenerator } from './property-arbitrary.js'; export interface PropertyManifestInput { name: string; domain: unknown; + generatorId?: string; +} + +export interface PropertySourcePointWire { + module: string; + line: number; + column: number; +} + +export interface PropertyAssertionWire { + id: string; + source: PropertySourcePointWire; + testedCall?: PropertySourcePointWire; + operands: Array<{ id: string; source: PropertySourcePointWire }>; } export interface PropertyManifestWire { @@ -32,6 +46,14 @@ export interface PropertyManifestWire { inputs: PropertyManifestInput[]; predicate: TypeScriptEntryPointReference; precondition?: TypeScriptEntryPointReference; + assertions?: PropertyAssertionWire[]; + sourceIdentity?: { sourceSha256: string; buildSha256: string; buildScope: string }; + generator?: { + id: string; + kind: 'array-index'; + arrayInputIndex: number; + indexInputIndex: number; + }; } export interface FastCheckExecutionRequest { @@ -78,10 +100,7 @@ export async function executeProperty(requestValue: unknown): Promise - projectDomain(input.domain, `manifest.inputs[${index}].domain`)), - ); + const arbitrary = buildPropertyArbitrary(request.manifest); const contractErrors: ContractErrorState = { first: undefined }; const property = buildProperty(arbitrary, predicate, precondition, contractErrors); const parameters = buildParameters(request); @@ -248,6 +267,17 @@ function buildParameters(request: FastCheckExecutionRequest): Parameters<[JsConc const values = example.map((value, valueIndex) => decodeJsValue(value, `examples[${exampleIndex}][${valueIndex}]`)); + if (request.manifest.generator !== undefined) { + const [array, index] = values; + if (!Array.isArray(array) || typeof index !== 'number' || !Number.isInteger(index) + || index < 0 || index >= array.length) { + throw protocolError( + adapterDiagnostic.protocolExamplesInvalid, + 'Explicit example violates declared joint generator support', + `examples[${exampleIndex}]`, + ); + } + } return [values]; }); @@ -457,7 +487,16 @@ function validateManifest(value: unknown): PropertyManifestWire { ); } - return { name: input.name, domain: input.domain }; + const validatedInput: PropertyManifestInput = { name: input.name, domain: input.domain }; + if (input.generatorId !== undefined) { + if (typeof input.generatorId !== 'string' || input.generatorId.length === 0) { + throw protocolError(adapterDiagnostic.protocolManifestInputInvalid, 'Invalid generator ID', `manifest.inputs[${index}].generatorId`); + } + + validatedInput.generatorId = input.generatorId; + } + + return validatedInput; }); const validated: PropertyManifestWire = { @@ -470,9 +509,89 @@ function validateManifest(value: unknown): PropertyManifestWire { validated.precondition = validateEntryPoint(manifest.precondition, 'manifest.precondition'); } + if (manifest.generator !== undefined) { + const generator = requireRecord( + manifest.generator, + adapterDiagnostic.protocolManifestInvalid, + 'Generator must be an object', + 'manifest.generator', + ); + const validGenerator = typeof generator.id === 'string' && generator.id.length > 0 + && generator.kind === 'array-index' + && generator.arrayInputIndex === 0 && generator.indexInputIndex === 1 + && inputs.length === 2; + if (!validGenerator) { + throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid joint generator', 'manifest.generator'); + } + + validated.generator = generator as unknown as NonNullable; + validateJointGenerator(validated); + } + + if (manifest.assertions !== undefined) { + if (!Array.isArray(manifest.assertions)) { + throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Assertions must be an array', 'manifest.assertions'); + } + + validated.assertions = manifest.assertions.map((value: unknown, index: number) => + validateAssertion(value, `manifest.assertions[${index}]`)); + } + + if (manifest.sourceIdentity !== undefined) { + const identity = requireRecord(manifest.sourceIdentity, adapterDiagnostic.protocolManifestInvalid, + 'Source identity must be an object', 'manifest.sourceIdentity'); + if (typeof identity.sourceSha256 !== 'string' || typeof identity.buildSha256 !== 'string' + || typeof identity.buildScope !== 'string') { + throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid source identity', 'manifest.sourceIdentity'); + } + + validated.sourceIdentity = { + sourceSha256: identity.sourceSha256, + buildSha256: identity.buildSha256, + buildScope: identity.buildScope, + }; + } + return validated; } +function validateAssertion(value: unknown, path: string): PropertyAssertionWire { + const assertion = requireRecord(value, adapterDiagnostic.protocolManifestInvalid, 'Assertion must be an object', path); + if (typeof assertion.id !== 'string' || !Array.isArray(assertion.operands)) { + throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid assertion identity or operands', path); + } + + const operands = assertion.operands.map((value: unknown, index: number) => { + const operandPath = `${path}.operands[${index}]`; + const operand = requireRecord(value, adapterDiagnostic.protocolManifestInvalid, 'Operand must be an object', operandPath); + if (typeof operand.id !== 'string') { + throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid operand ID', operandPath); + } + + return { id: operand.id, source: validateSourcePoint(operand.source, `${operandPath}.source`) }; + }); + const result: PropertyAssertionWire = { + id: assertion.id, + source: validateSourcePoint(assertion.source, `${path}.source`), + operands, + }; + if (assertion.testedCall !== undefined) { + result.testedCall = validateSourcePoint(assertion.testedCall, `${path}.testedCall`); + } + + return result; +} + +function validateSourcePoint(value: unknown, path: string): PropertySourcePointWire { + const point = requireRecord(value, adapterDiagnostic.protocolManifestInvalid, 'Source point must be an object', path); + if (typeof point.module !== 'string' || !Number.isInteger(point.line) || !Number.isInteger(point.column) + || (point.line as number) < 1 || (point.column as number) < 1) { + throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Invalid source point', path); + } + + return { module: point.module, line: point.line as number, column: point.column as number }; +} + function validateEntryPoint(value: unknown, entryPath: string): TypeScriptEntryPointReference { const entryPoint = requireRecord( value, diff --git a/usvm-ts-fast-check/fast-check-adapter/src/property-arbitrary.ts b/usvm-ts-fast-check/fast-check-adapter/src/property-arbitrary.ts new file mode 100644 index 0000000000..cdbd82ceb2 --- /dev/null +++ b/usvm-ts-fast-check/fast-check-adapter/src/property-arbitrary.ts @@ -0,0 +1,59 @@ +import fc from 'fast-check'; +import { adapterDiagnostic } from './diagnostics.js'; +import type { JsConcreteValue } from './js-value.js'; +import { protocolError } from './js-value.js'; +import type { PropertyManifestWire } from './execute-property.js'; +import { projectDomain } from './project-domain.js'; + +/** Constructs declared joint support; it does not interpret predicate or precondition behavior. */ +export function buildPropertyArbitrary(manifest: PropertyManifestWire): fc.Arbitrary { + const generator = manifest.generator; + if (generator === undefined) { + return fc.tuple(...manifest.inputs.map((input, index) => + projectDomain(input.domain, `manifest.inputs[${index}].domain`))); + } + + validateJointGenerator(manifest); + + const array = projectDomain(manifest.inputs[0]?.domain, 'manifest.inputs[0].domain'); + + return array.chain((value) => { + if (!Array.isArray(value) || value.length === 0) { + throw protocolError(adapterDiagnostic.protocolManifestInvalid, 'Array-index generator requires a nonempty array', 'manifest.generator'); + } + + return fc.integer({ min: 0, max: value.length - 1 }).map((index): JsConcreteValue[] => [value, index]); + }); +} + +/** Checks the declared domains before a dependent arbitrary can sample outside either one. */ +export function validateJointGenerator(manifest: PropertyManifestWire): void { + const generator = manifest.generator; + if (generator === undefined) return; + + const arrayDomain = manifest.inputs[0]?.domain; + const indexDomain = manifest.inputs[1]?.domain; + const array = asRecord(arrayDomain); + const index = asRecord(indexDomain); + const valid = generator.kind === 'array-index' + && generator.arrayInputIndex === 0 && generator.indexInputIndex === 1 + && manifest.inputs.length === 2 + && array?.kind === 'array' && Number.isInteger(array.minLength) && Number.isInteger(array.maxLength) + && (array.minLength as number) >= 1 && (array.maxLength as number) <= 32 + && (array.minLength as number) <= (array.maxLength as number) + && index?.kind === 'integer' && index.min === 0 + && index.max === (array.maxLength as number) - 1; + if (!valid) { + throw protocolError( + adapterDiagnostic.protocolManifestInvalid, + 'Array-index generator requires a nonempty bounded array and index domain 0..maxLength-1', + 'manifest.generator', + ); + } +} + +function asRecord(value: unknown): Record | undefined { + return value !== null && typeof value === 'object' && !Array.isArray(value) + ? value as Record + : undefined; +} diff --git a/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts index c4f98a1bc8..f8e6bdd80c 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts @@ -4,6 +4,7 @@ import { tmpdir } from 'node:os'; import path from 'node:path'; import test from 'node:test'; import { fileURLToPath } from 'node:url'; +import { tsImport } from 'tsx/esm/api'; import { encodeJsValue, ProtocolError } from '../src/js-value.js'; import { executeProperty, @@ -11,6 +12,95 @@ import { type FastCheckRunResult, } from '../src/execute-property.js'; +test('pinned fast-check callback shim preserves length assertion outcomes on bounded arrays', async () => { + const fixture = path.resolve( + path.dirname(fileURLToPath(import.meta.url)), + '../../../src/test/resources/properties/real/ArrayArbitraryProperty.ts', + ); + const property = await tsImport(fixture, import.meta.url) as { + AssertionError: new (message: string) => Error; + expect(values: number[]): { toHaveLength(expected: number): void }; + originalUniqueAssertion(values: number[]): void; + originalUniqueOracle(values: number[]): boolean; + }; + const cases = [[], [0], [0, 1], [1, 1], [0, 1, 0], [10, 9, 8, 7], [10, 10, 10, 10]]; + + for (const values of cases) { + const expected = values.length === new Set(values).size; + + if (expected) { + assert.equal(property.originalUniqueAssertion(values), undefined); + assert.equal(property.originalUniqueOracle(values), true); + } else { + assert.throws(() => property.originalUniqueAssertion(values), property.AssertionError); + assert.throws(() => property.originalUniqueOracle(values), property.AssertionError); + } + } +}); + +test('assertion shim evaluates expected operand before reading actual length and preserves thrown values', async () => { + const fixture = path.resolve( + path.dirname(fileURLToPath(import.meta.url)), + '../../../src/test/resources/properties/real/ArrayArbitraryProperty.ts', + ); + const property = await tsImport(fixture, import.meta.url) as { + expect(values: number[]): { toHaveLength(expected: number): void }; + }; + const order: string[] = []; + const value = { + get length(): number { + order.push('actual'); + return 1; + }, + } as number[]; + const expected = (): number => { + order.push('expected'); + return 1; + }; + + property.expect(value).toHaveLength(expected()); + + assert.deepEqual(order, ['expected', 'actual']); + + const thrown = new Error('length getter'); + const throwing = { + get length(): number { + throw thrown; + }, + } as number[]; + + assert.throws(() => property.expect(throwing).toHaveLength(1), (error) => error === thrown); +}); + +test('rejects array-index manifests that conflict with declared input domains before sampling', async () => { + await withPropertyModule(async (sourceRoot) => { + const array = (minLength: number, maxLength: number) => ({ + kind: 'array', + element: { kind: 'integer', min: 0, max: 1 }, + minLength, + maxLength, + }); + const invalidDomains = [ + [array(1, 3), { kind: 'integer', min: 99, max: 99 }], + [array(0, 3), { kind: 'integer', min: 0, max: 2 }], + [array(1, 33), { kind: 'integer', min: 0, max: 32 }], + ]; + + for (const inputDomains of invalidDomains) { + const request = executionRequest(sourceRoot, 'alwaysTrue', { inputDomains }); + request.manifest.generator = { + id: 'values.valid-index', + kind: 'array-index', + arrayInputIndex: 0, + indexInputIndex: 1, + }; + + await assert.rejects(executeProperty(request), (error: unknown) => + error instanceof ProtocolError && error.path === 'manifest.generator'); + } + }); +}); + test('executes a synchronous TypeScript predicate with deterministic success details', async () => { await withPropertyModule(async (sourceRoot) => { const request = executionRequest(sourceRoot, 'alwaysTrue'); diff --git a/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts index 28d2c26c7c..992f9c4d2d 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts @@ -5,6 +5,25 @@ import { projectDomain, projectionCapability, } from '../src/project-domain.js'; +import { buildPropertyArbitrary } from '../src/property-arbitrary.js'; + +test('joint array-index generator keeps index within the generated array', () => { + const arbitrary = buildPropertyArbitrary({ + propertyId: 'example.array-index', + predicate: { module: 'example.ts', exportName: 'property', executionKind: 'sync' }, + inputs: [ + { name: 'values', domain: { kind: 'array', element: { kind: 'integer', min: 0, max: 2 }, minLength: 1, maxLength: 4 } }, + { name: 'index', domain: { kind: 'integer', min: 0, max: 3 } }, + ], + generator: { id: 'values.valid-index', kind: 'array-index', arrayInputIndex: 0, indexInputIndex: 1 }, + }); + + const samples = fc.sample(arbitrary, { seed: 42, numRuns: 100 }); + + assert.ok(samples.every(([values, index]) => Array.isArray(values) + && typeof index === 'number' && Number.isInteger(index) && index >= 0 && index < values.length)); + assert.ok(samples.some(([values, index]) => Array.isArray(values) && values.length > 1 && index === 1)); +}); test('bounded integers use a real fast-check arbitrary', () => { const samples = sample({ kind: 'integer', min: -3, max: 7 }); 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 7b2d95510d..9a4d539a17 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 @@ -9,6 +9,7 @@ import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.JsNumberKind import org.usvm.ts.pbt.model.PropertyDefinition +import org.usvm.ts.pbt.model.accepts import org.usvm.ts.pbt.model.contains import org.usvm.ts.pbt.validation.requireValid import org.usvm.ts.pbt.validation.validatePropertyDefinition @@ -96,6 +97,19 @@ class FastCheckBackend( ) } } + + validateJointExample(property, example, index) + } + } + + private fun validateJointExample(property: PropertyDefinition, example: List, index: Int) { + if (property.generator?.accepts(example) == false) { + throw invalidRequest( + code = FastCheckDiagnosticCode.BACKEND_EXAMPLES_DOMAIN, + message = "Explicit example violates the declared joint generator support", + property = property, + path = "examples[$index]", + ) } } diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt index 88cfa2756a..e81dd6ac8c 100644 --- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/ExamplePropertiesTest.kt @@ -1,27 +1,67 @@ package org.usvm.ts.pbt.examples import org.junit.jupiter.api.Test +import org.usvm.ts.pbt.backend.PropertyRunConfiguration +import org.usvm.ts.pbt.backend.PropertyRunStatus +import org.usvm.ts.pbt.fastcheck.FastCheckBackend import org.usvm.ts.pbt.fastcheck.FastCheckProjectionClient import org.usvm.ts.pbt.fastcheck.FastCheckProjectionRequest +import org.usvm.ts.pbt.fastcheck.PbtBackendException import org.usvm.ts.pbt.manifest.PropertyManifestJson import org.usvm.ts.pbt.manifest.toManifest import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.ArrayIndexGenerator import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyId import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcesRoot import org.usvm.ts.pbt.validation.validatePropertyDefinition import kotlin.test.assertEquals +import kotlin.test.assertFailsWith import kotlin.test.assertNotNull import kotlin.test.assertTrue class ExamplePropertiesTest { + @Test + fun `declared array index relationship holds during generation and rejects invalid examples`() { + val property = PropertyDefinition( + id = PropertyId("example.array-index"), + inputs = listOf( + PropertyInput("values", ArrayDomain(IntegerDomain(min = 0, max = 2), minLength = 1, maxLength = 4)), + PropertyInput("index", IntegerDomain(min = 0, max = 3)), + ), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = "indexedValueIsPresent"), + generator = ArrayIndexGenerator(id = "values.valid-index", arrayInputIndex = 0, indexInputIndex = 1), + ) + val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + + val run = backend.run(property, PropertyRunConfiguration(seed = 42, numRuns = 100)) + + assertEquals(PropertyRunStatus.SUCCESS, run.status) + assertFailsWith { + backend.run( + property, + PropertyRunConfiguration( + examples = listOf( + listOf( + JsConcreteValue.Array(listOf(JsConcreteValue.number(1.0))), + JsConcreteValue.number(1.0), + ), + ), + ), + ) + } + } + @Test fun `four Kotlin property shapes validate serialize and project through fast-check`() { assertNotNull(javaClass.getResource("/properties/examples/PropertyExamples.ts")) val client = FastCheckProjectionClient() + val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) examples.forEach { definition -> assertTrue(validatePropertyDefinition(definition).isValid, definition.id.value) @@ -40,6 +80,10 @@ class ExamplePropertiesTest { assertEquals(5, response.samples.size) assertTrue(response.samples.all { it.size == definition.inputs.size }) + + val run = backend.run(definition, PropertyRunConfiguration(seed = 42, numRuns = 5)) + + assertEquals(definition.id, run.propertyId) } } diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/RealSuiteRegistrationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/RealSuiteRegistrationTest.kt new file mode 100644 index 0000000000..a0439768f4 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/examples/RealSuiteRegistrationTest.kt @@ -0,0 +1,106 @@ +package org.usvm.ts.pbt.examples + +import org.junit.jupiter.api.Test +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.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.PropertyManifestJson +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.model.ArrayDomain +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.PropertySourceIdentity +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.model.TypeScriptEntryPoint +import org.usvm.ts.pbt.testResourcesRoot +import java.nio.file.Files +import java.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertNotNull + +class RealSuiteRegistrationTest { + @Test + fun `original fast-check uniqueness oracle retains its assertion and failure`() { + val source = testResourcesRoot().resolve(MODULE) + val sourceHash = MessageDigest.getInstance("SHA-256") + .digest(Files.readAllBytes(source)) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + val definition = property( + exportName = "originalUniqueOracle", + sourceIdentity = PropertySourceIdentity( + sourceSha256 = sourceHash, + buildSha256 = sourceHash, + buildScope = "direct TypeScript source input; transpiled output is not pinned", + ), + ) + val backend = FastCheckBackend(sourceRoots = listOf(testResourcesRoot())) + val explicitExample = listOf( + JsConcreteValue.Array( + listOf( + JsConcreteValue.number(1.0), + JsConcreteValue.number(1.0), + ), + ), + ) + + val manifest = PropertyManifestJson.decode(PropertyManifestJson.encode(definition.toManifest())) + val failed = backend.run(definition, PropertyRunConfiguration(examples = listOf(explicitExample), numRuns = 1)) + val passed = backend.run( + property(exportName = "correctUniqueOracle", sourceIdentity = definition.sourceIdentity), + PropertyRunConfiguration(seed = 42, numRuns = 30), + ) + + assertEquals("fast-check.array-bias.unique", manifest.propertyId) + assertEquals("no-duplicates", manifest.assertions.single().id) + assertEquals( + listOf("filtered-array", "expected-set-size"), + manifest.assertions.single().operands.map(PropertyOperand::id), + ) + assertEquals(sourceHash, manifest.sourceIdentity?.sourceSha256) + assertEquals(PropertyRunStatus.FAILURE, failed.status) + assertEquals(PropertyFailureKind.PROPERTY, failed.failure?.kind) + assertEquals("AssertionError", failed.failure?.errorName) + assertNotNull(failed.counterexample) + assertEquals(PropertyRunStatus.SUCCESS, passed.status) + } + + private fun property(exportName: String, sourceIdentity: PropertySourceIdentity?) = PropertyDefinition( + id = PropertyId("fast-check.array-bias.unique"), + inputs = listOf( + PropertyInput( + name = "values", + domain = ArrayDomain(IntegerDomain(min = 0, max = 10), minLength = 0, maxLength = 8), + generatorId = "fast-check.array-integers", + ), + ), + predicate = TypeScriptEntryPoint(module = MODULE, exportName = exportName), + assertions = listOf( + PropertyAssertion( + id = "no-duplicates", + source = PropertySourcePoint(module = MODULE, line = 18, column = 5), + testedCall = PropertySourcePoint(module = MODULE, line = 17, column = 22), + operands = listOf( + PropertyOperand( + id = "filtered-array", + source = PropertySourcePoint(module = MODULE, line = 18, column = 12), + ), + PropertyOperand( + id = "expected-set-size", + source = PropertySourcePoint(module = MODULE, line = 18, column = 34), + ), + ), + ), + ), + sourceIdentity = sourceIdentity, + ) + + private companion object { + const val MODULE = "properties/real/ArrayArbitraryProperty.ts" + } +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/examples/PropertyExamples.ts b/usvm-ts-fast-check/src/test/resources/properties/examples/PropertyExamples.ts index 06c91b5b9d..0e7369bf4b 100644 --- a/usvm-ts-fast-check/src/test/resources/properties/examples/PropertyExamples.ts +++ b/usvm-ts-fast-check/src/test/resources/properties/examples/PropertyExamples.ts @@ -17,3 +17,7 @@ export function divisionRoundTrip(dividend: number, divisor: number): boolean { export function reverseTwicePreservesValues(values: number[]): boolean { return [...values].reverse().reverse().every((value, index) => value === values[index]); } + +export function indexedValueIsPresent(values: number[], index: number): boolean { + return values[index] !== undefined; +} diff --git a/usvm-ts-fast-check/src/test/resources/properties/real/ArrayArbitraryProperty.ts b/usvm-ts-fast-check/src/test/resources/properties/real/ArrayArbitraryProperty.ts new file mode 100644 index 0000000000..45f9bfadac --- /dev/null +++ b/usvm-ts-fast-check/src/test/resources/properties/real/ArrayArbitraryProperty.ts @@ -0,0 +1,33 @@ +// Adapted from fast-check ArrayArbitrary.spec.ts at 85eeab9e87c9d37e66cc7819260e3df1e72305ae (MIT). +// Only this one Vitest assertion is shimmed; the callback body below matches the upstream property. +export class AssertionError extends Error { + override name = 'AssertionError'; +} + +export function expect(value: T[]): { toHaveLength(expected: number): void } { + return { + toHaveLength(expected: number): void { + if (value.length !== expected) throw new AssertionError(`Expected length ${expected}, received ${value.length}`); + }, + }; +} + +export function originalUniqueAssertion(arr: number[]): void { + const removeDuplicates = (values: number[]) => [...values]; + const filtered = removeDuplicates(arr); + expect(filtered).toHaveLength(new Set(filtered).size); +} + +export function originalUniqueOracle(values: number[]): boolean { + originalUniqueAssertion(values); + + return true; +} + +export function correctUniqueOracle(values: number[]): boolean { + const filtered = [...new Set(values)]; + + expect(filtered).toHaveLength(new Set(filtered).size); + + return true; +} diff --git a/usvm-ts-pbt/PROPERTY_REGISTRATION.md b/usvm-ts-pbt/PROPERTY_REGISTRATION.md new file mode 100644 index 0000000000..fe8816f03a --- /dev/null +++ b/usvm-ts-pbt/PROPERTY_REGISTRATION.md @@ -0,0 +1,26 @@ +# Bounded property registration (#395) + +`PropertyDefinition` keeps the original exported TypeScript predicate and optional precondition as the only executable oracle. `PropertyManifest` carries the same fields to concrete and symbolic consumers. Assertions, operands, and tested-call points are author-supplied identities and source locations; they do not evaluate expressions. #396 may observe supported points once, and #397 may use the metadata to focus inference. An opaque predicate continues to run, but its internal assertions have no identities until annotated. + +## Inventory and migration + +The existing examples are `isCommutative` (two integers), `boundedValueStaysBounded` (one bounded integer), `divisionRoundTrip` with `nonZeroDivisor` (original precondition), and `reverseTwicePreservesValues` (array). Their predicates remain unchanged. `indexedValueIsPresent` adds a bounded array and an index constrained by its actual length. + +The selected real suite is [fast-check's `ArrayArbitrary.spec.ts` `biasIts` property](https://github.com/dubzzz/fast-check/blob/85eeab9e87c9d37e66cc7819260e3df1e72305ae/packages/fast-check/test/arbitraries/ArrayArbitrary.spec.ts), MIT licensed. Its callback body and assertion `expect(filtered).toHaveLength(new Set(filtered).size)` are retained in `originalUniqueAssertion` in `ArrayArbitraryProperty.ts`. A local shim implements only the used `toHaveLength` assertion, throwing `AssertionError` on mismatch; the boolean entry point invokes the callback and returns true on normal completion. The shim preserves the failure class and tested success/failure/evaluation order for this assertion, but not Vitest's full diagnostics. The original deliberately faulty identity deduplicator still fails; a Set-based version passes. The registration bounds the input to dense arrays of length 0–8 with integers 0–10. This changes generated support and the size distribution, so it is a development adaptation, not an identical native fast-check run. + +The manual adaptation is one exported boolean wrapper around the original callback, a one-method assertion shim, one `PropertyDefinition` with one input domain, one stable assertion ID, two operand IDs, source points, and a source/build-input hash. It does not translate the oracle into a Kotlin expression or another assertion DSL. The test computes SHA-256 from the TypeScript file bytes used as direct execution input; `buildScope` records that transpiled output and transitive imports are **not** pinned by this hash. Registrants of bundled projects must provide a hash and scope for their actual build artifact. The current runner transports the declared hashes but does not independently verify them against loaded files, so consumers must not infer that a matching runtime build was proved. + +## Joint support + +`ArrayIndexGenerator` has a stable ID and explicitly links input 0, a nonempty dense bounded array, to input 1, an integer index. The index domain must be `0..maxLength-1`; joint admissibility further requires `index < values.length`. Kotlin and the adapter reject incompatible declarations before execution. The concrete arbitrary constructs the pair together. Kotlin and the adapter reject explicit examples outside that joint set. USVM adds the corresponding constraint over the symbolic array length and index. The original predicate still decides success or failure. This direct relation does not infer support from samples and does not implement arbitrary dependent fast-check closures or generator-choice search (#400). + +| Capability | Independent supported domains | Array/index relation | Native closure/combinator outside the declared model | +| --- | --- | --- | --- | +| Concrete generation and original oracle | Yes | Yes | Concrete-only in its native suite; no general import | +| Direct symbolic projection | Subject to existing EtsIR/domain capability | Yes, bounded relation | Unsupported | +| Explicit examples | Domain validation | Joint support validation | No declared validation | +| External-example shrinking | Existing `fc.check` examples; exact-input API belongs to #353 | Native chain arbitrary preserves relation during generated shrinking | No general guarantee | +| Empirical observations | #396 | #396 | No automatic observation | +| Generator-choice search | #400 | #400 | Unsupported | + +Declared domains and joint support are hard admissibility conditions. The TypeScript precondition separately admits or rejects an input. Fast-check probability, size bias, and observed values are separate evidence; none narrows the declared symbolic set. Assertion false or throw is an original-oracle failure, while precondition exhaustion, unsupported behavior, and timeouts remain distinct outcomes. diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt index 02df059163..1d3257e617 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt @@ -46,6 +46,9 @@ internal object PbtDiagnosticCode { const val USVM_SOLVER_UNKNOWN = "usvm.solver.unknown" const val PROPERTY_ID_INVALID = "property.id.invalid" + const val PROPERTY_ASSERTION_INVALID = "property.assertion.invalid" + const val PROPERTY_GENERATOR_INVALID = "property.generator.invalid" + const val PROPERTY_SOURCE_INVALID = "property.source.invalid" const val PROPERTY_INPUTS_EMPTY = "property.inputs.empty" const val INPUT_NAME_DUPLICATE = "input.name.duplicate" const val INPUT_NAME_INVALID = "input.name.invalid" diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt index 48e52ecbb2..03f0617c55 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/manifest/PropertyManifest.kt @@ -4,8 +4,11 @@ import kotlinx.serialization.Serializable import kotlinx.serialization.decodeFromString import kotlinx.serialization.encodeToString import kotlinx.serialization.json.Json +import org.usvm.ts.pbt.model.ArrayIndexGenerator +import org.usvm.ts.pbt.model.PropertyAssertion import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.PropertySourceIdentity import org.usvm.ts.pbt.model.TypeScriptEntryPoint import org.usvm.ts.pbt.validation.requireValid import org.usvm.ts.pbt.validation.validatePropertyDefinition @@ -22,6 +25,9 @@ data class PropertyManifest( val inputs: List, val predicate: TypeScriptEntryPoint, val precondition: TypeScriptEntryPoint? = null, + val assertions: List = emptyList(), + val generator: ArrayIndexGenerator? = null, + val sourceIdentity: PropertySourceIdentity? = null, ) fun PropertyDefinition.toManifest(): PropertyManifest { @@ -31,6 +37,9 @@ fun PropertyDefinition.toManifest(): PropertyManifest { inputs = inputs, predicate = predicate, precondition = precondition, + assertions = assertions, + generator = generator, + sourceIdentity = sourceIdentity, ) } diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt index 01b548b25e..11e25e660e 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDefinition.kt @@ -35,6 +35,9 @@ data class PropertyDefinition( val inputs: List, val predicate: TypeScriptEntryPoint, val precondition: TypeScriptEntryPoint? = null, + val assertions: List = emptyList(), + val generator: ArrayIndexGenerator? = null, + val sourceIdentity: PropertySourceIdentity? = null, ) /** @@ -47,6 +50,7 @@ data class PropertyDefinition( data class PropertyInput( val name: String, val domain: PropertyDomain, + val generatorId: String? = null, ) /** diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertySemantics.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertySemantics.kt new file mode 100644 index 0000000000..e5ff152b40 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertySemantics.kt @@ -0,0 +1,53 @@ +package org.usvm.ts.pbt.model + +import kotlinx.serialization.Serializable + +/** Stable author-assigned identity and exact source point of an original assertion. */ +@Serializable +data class PropertyAssertion( + val id: String, + val source: PropertySourcePoint, + val testedCall: PropertySourcePoint? = null, + val operands: List = emptyList(), +) + +/** Stable identity of an explicitly named assertion operand, without evaluating it. */ +@Serializable +data class PropertyOperand( + val id: String, + val source: PropertySourcePoint, +) + +/** One-based source position in a project-relative TypeScript module. */ +@Serializable +data class PropertySourcePoint( + val module: String, + val line: Int, + val column: Int, +) + +/** Hashes supplied by the registrant; scope is the named source file and recorded build artifact. */ +@Serializable +data class PropertySourceIdentity( + val sourceSha256: String, + val buildSha256: String, + val buildScope: String, +) + +/** A supported joint construction relation, independent of sampling probability or size bias. */ +@Serializable +data class ArrayIndexGenerator( + val id: String, + val arrayInputIndex: Int, + val indexInputIndex: Int, + val kind: String = "array-index", +) + +/** Checks only declared support; preconditions remain original TypeScript code. */ +fun ArrayIndexGenerator.accepts(values: List): Boolean { + val array = values.getOrNull(arrayInputIndex) as? JsConcreteValue.Array ?: return false + val index = values.getOrNull(indexInputIndex) as? JsConcreteValue.Number ?: return false + val number = runCatching(index::toDouble).getOrNull() ?: return false + + return number.isFinite() && number % 1.0 == 0.0 && number >= 0 && number < array.elements.size +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt index 4ba065068f..142ecac457 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt @@ -24,6 +24,7 @@ import org.usvm.machine.types.mkFakeValue import org.usvm.sizeSort import org.usvm.ts.pbt.mapping.EtsInputBinding import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.ArrayIndexGenerator import org.usvm.ts.pbt.model.BooleanDomain import org.usvm.ts.pbt.model.ConstantDomain import org.usvm.ts.pbt.model.IntegerDomain @@ -35,6 +36,7 @@ import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.StringDomain import org.usvm.ts.pbt.model.TupleDomain import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkRegisterStackLValue /** One symbolic input written to the mapped EtsIR stack slot. */ @@ -57,6 +59,7 @@ class UsvmDomainProjector( state: TsState, inputs: List, bindings: List, + generator: ArrayIndexGenerator? = null, ): UsvmDeclaredDomainProjection { require(inputs.size == bindings.size) { "Property input count ${inputs.size} does not match EtsIR binding count ${bindings.size}" @@ -91,6 +94,25 @@ class UsvmDomainProjector( ) } + if (generator != null) { + require(generator.arrayInputIndex == 0 && generator.indexInputIndex == 1) + + val array = projectedInputs[generator.arrayInputIndex].value.asExpr(state.ctx.addressSort) + val arrayType = bindings[generator.arrayInputIndex].parameter.type as EtsArrayType + val index = projectedInputs[generator.indexInputIndex].value.asExpr(state.ctx.fp64Sort) + val length = state.memory.read(mkArrayLengthLValue(array, arrayType)).asExpr(state.ctx.sizeSort) + with(state.ctx) { + val lengthAsNumber = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = length.cast(), + signed = true, + ) + + state.pathConstraints += mkFpLessExpr(index, lengthAsNumber) + } + } + return UsvmDeclaredDomainProjection( inputs = projectedInputs, initialState = state.clone(), 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 2a00cb839f..790a163142 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 @@ -104,6 +104,7 @@ class UsvmPropertySearcher( state = state, inputs = manifest.inputs, bindings = predicate.bindings.inputs, + generator = manifest.generator, ) if (precondition != null) { state.prependBooleanEntryPointGuard( diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt index 09079ca167..932bb44fac 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt @@ -3,6 +3,7 @@ package org.usvm.ts.pbt.validation import org.usvm.ts.pbt.PbtDiagnosticCode import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.ArrayIndexGenerator import org.usvm.ts.pbt.model.BooleanDomain import org.usvm.ts.pbt.model.ConstantDomain import org.usvm.ts.pbt.model.IntegerDomain @@ -11,9 +12,12 @@ import org.usvm.ts.pbt.model.JsNumber import org.usvm.ts.pbt.model.JsNumberKind import org.usvm.ts.pbt.model.NumberDomain import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyAssertion import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyDomain import org.usvm.ts.pbt.model.PropertyInput +import org.usvm.ts.pbt.model.PropertySourceIdentity +import org.usvm.ts.pbt.model.PropertySourcePoint import org.usvm.ts.pbt.model.StringDomain import org.usvm.ts.pbt.model.TupleDomain import org.usvm.ts.pbt.model.TypeScriptEntryPoint @@ -48,6 +52,9 @@ fun validatePropertyDefinition(definition: PropertyDefinition): PropertyValidati inputs = definition.inputs, predicate = definition.predicate, precondition = definition.precondition, + assertions = definition.assertions, + generator = definition.generator, + sourceIdentity = definition.sourceIdentity, ) fun validatePropertyManifest(manifest: PropertyManifest): PropertyValidationResult { @@ -56,6 +63,9 @@ fun validatePropertyManifest(manifest: PropertyManifest): PropertyValidationResu inputs = manifest.inputs, predicate = manifest.predicate, precondition = manifest.precondition, + assertions = manifest.assertions, + generator = manifest.generator, + sourceIdentity = manifest.sourceIdentity, ) } @@ -70,6 +80,9 @@ private fun validateProperty( inputs: List, predicate: TypeScriptEntryPoint, precondition: TypeScriptEntryPoint?, + assertions: List, + generator: ArrayIndexGenerator?, + sourceIdentity: PropertySourceIdentity?, ): PropertyValidationResult { val diagnostics = mutableListOf() if (!isCanonicalPropertyId(propertyId)) { @@ -104,14 +117,101 @@ private fun validateProperty( path = path, ) } + if (input.generatorId != null && !isCanonicalPropertyId(input.generatorId)) { + diagnostics += diagnostic( + PbtDiagnosticCode.PROPERTY_GENERATOR_INVALID, + "Invalid generator ID", + "$path.generatorId", + ) + } validateDomain(input.domain, "$path.domain", diagnostics) } validateEntryPoint(predicate, "predicate", diagnostics) precondition?.let { validateEntryPoint(it, "precondition", diagnostics) } + validateAssertions(assertions, diagnostics) + generator?.let { validateGenerator(it, inputs, diagnostics) } + sourceIdentity?.let { validateSourceIdentity(it, diagnostics) } return diagnostics.toResult() } +private fun validateAssertions( + assertions: List, + diagnostics: MutableList, +) { + val seen = mutableSetOf() + assertions.forEachIndexed { index, assertion -> + val path = "assertions[$index]" + if (!isCanonicalPropertyId(assertion.id) || !seen.add(assertion.id)) { + diagnostics += diagnostic( + PbtDiagnosticCode.PROPERTY_ASSERTION_INVALID, + "Assertion ID is invalid or repeated", + "$path.id", + ) + } + + validateSourcePoint(assertion.source, "$path.source", diagnostics) + assertion.testedCall?.let { validateSourcePoint(it, "$path.testedCall", diagnostics) } + val operands = mutableSetOf() + assertion.operands.forEachIndexed { operandIndex, operand -> + val operandPath = "$path.operands[$operandIndex]" + if (!isCanonicalPropertyId(operand.id) || !operands.add(operand.id)) { + diagnostics += diagnostic( + PbtDiagnosticCode.PROPERTY_ASSERTION_INVALID, + "Operand ID is invalid or repeated", + "$operandPath.id", + ) + } + validateSourcePoint(operand.source, "$operandPath.source", diagnostics) + } + } +} + +private fun validateSourcePoint( + point: PropertySourcePoint, + path: String, + diagnostics: MutableList, +) { + if (!isProjectRelativePosixPath(point.module) || point.line < 1 || point.column < 1) { + diagnostics += diagnostic(PbtDiagnosticCode.PROPERTY_SOURCE_INVALID, "Invalid source point", path) + } +} + +private fun validateGenerator( + generator: ArrayIndexGenerator, + inputs: List, + diagnostics: MutableList, +) { + val array = inputs.getOrNull(generator.arrayInputIndex)?.domain as? ArrayDomain + val index = inputs.getOrNull(generator.indexInputIndex)?.domain as? IntegerDomain + val valid = generator.kind == "array-index" && isCanonicalPropertyId(generator.id) && + inputs.size == 2 && generator.arrayInputIndex == 0 && generator.indexInputIndex == 1 && + array != null && array.minLength >= 1 && array.maxLength <= MAX_DIRECT_ARRAY_LENGTH && + index != null && index.min == 0 && index.max == array.maxLength - 1 + if (!valid) { + diagnostics += diagnostic( + PbtDiagnosticCode.PROPERTY_GENERATOR_INVALID, + "Array-index construction requires a nonempty bounded array followed by its valid index range", + "generator", + ) + } +} + +private fun validateSourceIdentity( + identity: PropertySourceIdentity, + diagnostics: MutableList, +) { + if (!identity.sourceSha256.matches(SHA256_REGEX) || + !identity.buildSha256.matches(SHA256_REGEX) || identity.buildScope.isBlank() + ) { + diagnostics += diagnostic( + PbtDiagnosticCode.PROPERTY_SOURCE_INVALID, + "Expected lowercase SHA-256 hashes", + "sourceIdentity", + ) + } +} + private fun validateDomain( domain: PropertyDomain, path: String, @@ -369,6 +469,8 @@ private fun diagnostic(code: String, message: String, path: String) = Validation ) private val FINITE_NUMBER_BITS_REGEX = Regex("[0-9a-f]{16}") +private val SHA256_REGEX = Regex("[0-9a-f]{64}") +private const val MAX_DIRECT_ARRAY_LENGTH = 32 private const val JS_NUMBER_HEX_RADIX = 16 // ECMAScript permits these otherwise invisible Unicode characters after the first identifier character. diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt index b18601d748..31bf803489 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt @@ -18,6 +18,7 @@ import org.usvm.machine.state.TsState import org.usvm.ts.pbt.manifest.PropertyManifest import org.usvm.ts.pbt.mapping.PropertyEtsMapper import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.ArrayIndexGenerator import org.usvm.ts.pbt.model.BooleanDomain import org.usvm.ts.pbt.model.IntegerDomain import org.usvm.ts.pbt.model.PropertyDomain @@ -57,6 +58,44 @@ class UsvmCollectionDomainProjectorTest { assertFalse(acceptsTuple(domain, number = 3.0, boolean = true, length = 1)) } + @Test + fun `joint array index support constrains symbolic index by actual length`() { + val generator = ArrayIndexGenerator(id = "array.valid-index", arrayInputIndex = 0, indexInputIndex = 1) + val manifest = PropertyManifest( + propertyId = "usvm.collection.index", + inputs = listOf( + PropertyInput("values", ArrayDomain(IntegerDomain(0, 2), minLength = 1, maxLength = 2)), + PropertyInput("index", IntegerDomain(min = 0, max = 1)), + ), + predicate = TypeScriptEntryPoint(module = "UsvmCapabilityFixture.ts", exportName = "acceptsArrayIndex"), + generator = generator, + ) + val target = mapper.map(manifest).predicate.targets.single() + + fun accepts(length: Int, index: Int) = runCatchingAnalyze(target.method) { state -> + val projection = projector.configure( + state = state, + inputs = manifest.inputs, + bindings = target.bindings.inputs, + generator = generator, + ) + + with(state.ctx) { + val array = projection.inputs[0].value.asExpr(addressSort) + val projectedLength = state.memory.read( + mkArrayLengthLValue(array, EtsArrayType(EtsNumberType, dimensions = 1)), + ) + val projectedIndex = projection.inputs[1].value.asExpr(fp64Sort) + + state.pathConstraints += mkEq(projectedLength, mkBv(length)) + state.pathConstraints += mkEq(projectedIndex, mkFp(index.toDouble(), fp64Sort)) + } + } + + assertTrue(accepts(length = 2, index = 1)) + assertFalse(accepts(length = 1, index = 1)) + } + @Test fun `oversized arrays are rejected before materialization`() { val domain = ArrayDomain(IntegerDomain(), maxLength = 3) diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts index b252f65a86..ec6edb1925 100644 --- a/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts +++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts @@ -26,6 +26,10 @@ export function acceptsNumberArray(value: number[]): boolean { return value.length > 0; } +export function acceptsArrayIndex(values: number[], index: number): boolean { + return values[index] === values[index]; +} + export function acceptsOptionalNumberArray(value: number[] | undefined): boolean { return value === undefined || value.length > 0; }