diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt new file mode 100644 index 0000000000..3188a5e071 --- /dev/null +++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/inference/DslNumericLocalRelationTest.kt @@ -0,0 +1,327 @@ +package org.usvm.ts.pbt.inference + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +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.dsl.CompiledDslProperty +import org.usvm.ts.pbt.dsl.DslNumericLocalCapture +import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler +import org.usvm.ts.pbt.dsl.defineProperty +import org.usvm.ts.pbt.dsl.invoke +import org.usvm.ts.pbt.dsl.lessOrEqual +import org.usvm.ts.pbt.fastcheck.FastCheckBackend +import org.usvm.ts.pbt.manifest.toManifest +import org.usvm.ts.pbt.mapping.EtsMappingDiagnostic +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMapper +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.observation.ObservationBuildStatus +import org.usvm.ts.pbt.observation.ObservationPointKind +import org.usvm.ts.pbt.observation.ObservationValueStatus +import org.usvm.ts.pbt.observation.PropertyObservationSource +import org.usvm.ts.pbt.observation.PropertyPointEvent +import org.usvm.ts.pbt.usvm.bindDslNumericLocalRelation +import java.nio.file.Files +import java.nio.file.Path +import java.security.MessageDigest +import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertTrue + +class DslNumericLocalRelationTest { + @TempDir + lateinit var root: Path + + @Test + fun `compiler program and actual native receipt bind the result after its original numeric store`() { + val fixture = prepare() + val capture = assertNotNull(fixture.compiled.numericLocalCapture) + + val binding = bindDslNumericLocalRelation( + fixture.compiled, + fixture.mapping, + fixture.inference, + fixture.relation + ) + + assertEquals(ScalarRelationStatus.SAMPLED, fixture.relation.status) + assertEquals(EtsMappingStatus.EXACT, binding.status, binding.diagnostics.toString()) + assertEquals(ObservationBuildStatus.UNVERIFIED, fixture.inference.buildStatus) + assertEquals(capture.binding, binding.targets.single().compiler) + assertEquals("result", binding.targets.single().local.name) + assertEquals(0, binding.targets.single().inputIndex) + } + + @Test + fun `forged local ABI node kind and wrapper cannot become compiler authority through a source hash`() { + val fixture = prepare() + val compiled = fixture.compiled + val capture = assertNotNull(compiled.numericLocalCapture) + val badBindings = listOf( + capture.binding.copy(localName = "other"), + capture.binding.copy(abi = "other-callback"), + capture.binding.copy(nodeId = capture.binding.nodeId + 1), + capture.binding.copy(occurrence = 1), + capture.binding.copy(predicateAssignment = capture.binding.companionAssignment), + ) + val badCaptures = badBindings.map { binding -> + capture.copy(binding = binding, result = capture.result.copy(compilerLocal = binding)) + } + capture.copy(result = capture.result.copy(kind = ObservationPointKind.INTERMEDIATE)) + val badPrograms = badCaptures.map { compiled.copy(numericLocalCapture = it) } + listOf( + compiled.copy(typeScript = compiled.typeScript.replace("const result =", "let result =")), + compiled.copy(resolvedModules = emptyMap()), + ) + + badPrograms.forEach { changed -> + val binding = bindDslNumericLocalRelation(changed, fixture.mapping, fixture.inference, fixture.relation) + + assertEquals(EtsMappingStatus.UNSUPPORTED, binding.status) + assertTrue(binding.targets.isEmpty()) + assertEquals("usvm.dsl-local.compiler-mismatch", binding.diagnostics.single().code) + } + } + + @Test + fun `the selected original input can precede the result in a relation`() { + val fixture = prepare() + val original = fixture.relation + val evidence = original.evidence.map { it.copy(left = it.right, right = it.left) } + val reversed = original.copy( + pair = ScalarObservationPair(original.pair.right, original.pair.left), + evidence = evidence + ) + val inference = fixture.inference.copy(relations = listOf(reversed)) + + val binding = bindDslNumericLocalRelation(fixture.compiled, fixture.mapping, inference, reversed) + + assertEquals(EtsMappingStatus.EXACT, binding.status) + assertEquals(false, binding.targets.single().resultIsLeft) + } + + @Test + fun `swapped input parameters wrong names and wrong stack slots cannot activate an exact point`() { + val fixture = prepare() + val entry = fixture.mapping.predicate.targets.single() + val inputs = entry.bindings.inputs + val first = inputs[0] + val second = inputs[1] + val invalidInputs = listOf( + inputs.reversed(), + listOf(first.copy(stackSlot = second.stackSlot), second), + listOf(first.copy(parameter = second.parameter), second), + listOf(first.copy(propertyInputName = second.propertyInputName), second), + ) + + invalidInputs.forEach { changed -> + val target = entry.copy(bindings = entry.bindings.copy(inputs = changed)) + val predicate = fixture.mapping.predicate.copy(targets = listOf(target)) + val mapping = fixture.mapping.copy(predicate = predicate) + + val binding = bindDslNumericLocalRelation(fixture.compiled, mapping, fixture.inference, fixture.relation) + + assertEquals(EtsMappingStatus.UNSUPPORTED, binding.status) + assertEquals("usvm.dsl-local.input-mismatch", binding.diagnostics.single().code) + assertTrue(binding.targets.isEmpty()) + } + } + + @Test + fun `repeated nested out of order wrong context and unavailable receipts cannot activate exact guidance`() { + val fixture = prepare() + val relation = fixture.relation + val repeated = relation.copy( + evidence = relation.evidence.map { evidence -> + val duplicate = evidence.left.copy(occurrence = 1) + val invocation = evidence.invocation.copy(points = evidence.invocation.points + duplicate) + + evidence.copy(invocation = invocation) + } + ) + val nested = relation.copy( + evidence = relation.evidence.map { evidence -> + evidence.copy(invocation = evidence.invocation.copy(parentInvocationId = 1)) + } + ) + val wrongContext = relation.copy( + evidence = relation.evidence.map { evidence -> + val original = assertNotNull(evidence.invocation.callSite) + val invocation = evidence.invocation.copy(callSite = original.copy(line = original.line + 1)) + + evidence.copy(invocation = invocation) + } + ) + val wrongInput = relation.copy( + evidence = relation.evidence.map { evidence -> + val input = evidence.invocation.input.copy( + value = JsConcreteValue.Array(listOf(JsConcreteValue.number(-1.0))) + ) + + evidence.copy(invocation = evidence.invocation.copy(input = input)) + } + ) + val unavailable = relation.changedResult { event -> + event.copy(value = event.value.copy(status = ObservationValueStatus.UNSUPPORTED, value = null)) + } + val wrongTime = relation.changedResult { event -> event.copy(eventOrdinal = 0) } + val wrongLocal = relation.changedResult { event -> + val compiler = assertNotNull(event.compilerLocal) + + event.copy(compilerLocal = compiler.copy(localName = "other")) + } + + listOf(repeated, nested, wrongContext, wrongInput, unavailable, wrongTime, wrongLocal).forEach { changed -> + val inference = fixture.inference.copy(relations = listOf(changed)) + + val binding = bindDslNumericLocalRelation(fixture.compiled, fixture.mapping, inference, changed) + + assertEquals(EtsMappingStatus.UNSUPPORTED, binding.status) + assertTrue(binding.targets.isEmpty()) + } + } + + @Test + fun `changed selected wrapper or helper source cannot activate a stale challenge`() { + val fixture = prepare() + val generated = root.resolve("generated.ts") + Files.writeString(generated, fixture.compiled.typeScript + "\n// changed selected source\n") + + val staleWrapper = bindDslNumericLocalRelation( + fixture.compiled, + fixture.mapping, + fixture.inference, + fixture.relation + ) + Files.writeString(generated, fixture.compiled.typeScript) + Files.writeString( + root.resolve("functions.ts"), + "export function transform(input: number): number { return input; }" + ) + val staleHelper = bindDslNumericLocalRelation( + fixture.compiled, + fixture.mapping, + fixture.inference, + fixture.relation + ) + + assertEquals(EtsMappingStatus.UNSUPPORTED, staleWrapper.status) + assertEquals(EtsMappingStatus.UNSUPPORTED, staleHelper.status) + assertTrue(staleWrapper.diagnostics.any { it.code == "usvm.dsl-local.source-stale" }) + assertTrue(staleHelper.diagnostics.any { it.code == "usvm.dsl-local.source-stale" }) + } + + @Test + fun `ambiguous entries and missing source remain distinct from an exact point`() { + val fixture = prepare() + val predicate = fixture.mapping.predicate + val diagnostic = EtsMappingDiagnostic(code = "test.ambiguous-entry", message = "Two original entries") + val ambiguousPredicate = EtsMappingResult( + status = EtsMappingStatus.AMBIGUOUS, + targets = predicate.targets + predicate.targets, + diagnostics = listOf(diagnostic), + ) + val ambiguousMapping = fixture.mapping.copy(predicate = ambiguousPredicate) + + val ambiguous = bindDslNumericLocalRelation( + fixture.compiled, + ambiguousMapping, + fixture.inference, + fixture.relation + ) + Files.delete(root.resolve("generated.ts")) + val missing = bindDslNumericLocalRelation( + fixture.compiled, + fixture.mapping, + fixture.inference, + fixture.relation + ) + + assertEquals(EtsMappingStatus.AMBIGUOUS, ambiguous.status) + assertEquals(2, ambiguous.targets.size) + assertEquals(EtsMappingStatus.UNMAPPED, missing.status) + assertTrue(missing.targets.isEmpty()) + } + + private fun ScalarRelation.changedResult( + change: (PropertyPointEvent) -> PropertyPointEvent, + ): ScalarRelation { + val changed = evidence.map { evidence -> + val result = change(evidence.left) + val points = evidence.invocation.points.map { event -> if (event == evidence.left) result else event } + + evidence.copy(left = result, invocation = evidence.invocation.copy(points = points)) + } + + return copy(evidence = changed) + } + + private fun prepare(): Fixture { + val compiled = compile() + val capture = assertNotNull(compiled.numericLocalCapture) + val sources = capture.observationRequest().sources + source(module = "functions.ts") + val request = capture.observationRequest().copy(sources = sources) + val observation = FastCheckBackend(sourceRoots = listOf(root)).run( + compiled.definition, + PropertyRunConfiguration(seed = 42, numRuns = 8, observationRequest = request), + ) + val inference = inferScalarRelations( + compiled.definition, + assertNotNull(observation.observations), + listOf(ScalarObservationPair(capture.result, capture.input)), + ) + val relation = inference.relations.single { it.template == ScalarRelationTemplate.STRICT_EQUAL } + val files = listOf("functions.ts", "generated.ts").map { module -> + loadEtsFileAutoConvert(root.resolve(module), provider = EtsIrProvider.TS_FRONTEND) + } + val scene = EtsScene(files) + val mapping = PropertyEtsMapper(scene, sourceRoots = listOf(root)).map(compiled.definition.toManifest()) + + return Fixture(compiled, mapping, inference, relation) + } + + private fun source(module: String): PropertyObservationSource { + val hash = MessageDigest.getInstance("SHA-256").digest(Files.readAllBytes(root.resolve(module))) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + + return PropertyObservationSource(module, hash) + } + + private fun compile(): CompiledDslProperty { + val source = """ + export function transform(input: number): number { + if (input === 417) return input - 1; + return input; + } + """.trimIndent() + Files.writeString(root.resolve("functions.ts"), source) + val program = defineProperty(id = "dsl.local-relation") { + val transform = function<(Double) -> Double>(module = "functions.ts", exportName = "transform") + val input by int(min = 0, max = 1000) + val other by int(min = 0, max = 1000) + val result by value(transform(input)) + + check(name = "bound") { result lessOrEqual input } + check(name = "other-input") { other lessOrEqual 1000 } + } + val compiled = PropertyTypeScriptCompiler().compile( + program, + generatedModule = "generated.ts", + resolveModule = { "./$it" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "bound"), + ) + Files.writeString(root.resolve("generated.ts"), compiled.typeScript) + + return compiled + } + + private data class Fixture( + val compiled: CompiledDslProperty, + val mapping: PropertyEtsMappingArtifact, + val inference: ScalarRelationInference, + val relation: ScalarRelation, + ) +} diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/PropertyTypeScriptCompiler.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/PropertyTypeScriptCompiler.kt index eae82c7bc8..5872d67026 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/PropertyTypeScriptCompiler.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/dsl/PropertyTypeScriptCompiler.kt @@ -20,6 +20,8 @@ data class CompiledDslProperty( val typeScript: String, val expressionLocations: Map>, val numericLocalCapture: CompiledDslNumericLocalCapture? = null, + /** Retains import decisions so a point consumer can reproduce this compiler output from the original program. */ + val resolvedModules: Map = emptyMap(), ) /** One expression occurrence in generated TypeScript; columns are one-based UTF-16 and end-exclusive. */ @@ -58,6 +60,7 @@ private class PropertyEmitter( private val capture = numericLocalCapture?.let { program.selectNumericLocalCapture(it) } private val source = StringBuilder() private val functions = linkedMapOf() + private val resolvedModules = linkedMapOf() private val expressionLocations = mutableMapOf>() private val assertions = mutableListOf() private var line = 1 @@ -69,6 +72,10 @@ private class PropertyEmitter( allExpressions().forEach(::collectFunctions) functions.forEach { (function, alias) -> val path = resolveModule(function.module) + val previous = resolvedModules.putIfAbsent(function.module, path) + require(capture == null || previous == null || previous == path) { + "A captured program requires one stable import resolution per module" + } appendLine("import { ${function.exportName} as $alias } from ${quote(path)};") } val parameters = program.inputs.joinToString { input -> @@ -107,7 +114,7 @@ private class PropertyEmitter( companionAssignment = requireNotNull(companionAssignment), ) - return CompiledDslProperty(program, definition, typeScript, locations, localCapture) + return CompiledDslProperty(program, definition, typeScript, locations, localCapture, resolvedModules.toMap()) } private fun emitPredicate(parameters: String, diagnostic: Boolean) { diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt index 8787c9e4c9..dd93babb40 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt @@ -19,6 +19,7 @@ import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.usvm.ts.pbt.PbtDiagnosticCode import org.usvm.ts.pbt.manifest.PropertyManifest +import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.TypeScriptEntryPoint import java.util.IdentityHashMap @@ -240,19 +241,6 @@ internal class EtsEntryPointResolver( return modulePaths.any(filePaths::contains) } - private fun EtsMethod.bindingParameters(): EtsBindingParameters { - // The frontend lifts arrow-function captures into one leading lexical-environment parameter. - // It is not a source argument; the interpreter recognizes the same parameter by its semantic type. - val hiddenClosure = parameters.firstOrNull()?.takeIf { parameter -> - parameter.type is EtsLexicalEnvType - } - - return EtsBindingParameters( - lexicalEnvironment = hiddenClosure, - inputs = if (hiddenClosure == null) parameters else parameters.drop(1), - ) - } - private fun EtsMethod.bindingsFor( manifest: PropertyManifest, parameters: EtsBindingParameters, @@ -261,13 +249,7 @@ internal class EtsEntryPointResolver( signature = signature.enclosingClass, typeParameters = requireNotNull(enclosingClass).typeParameters, ) - val inputBindings = manifest.inputs.zip(parameters.inputs).map { (input, parameter) -> - EtsInputBinding( - propertyInputName = input.name, - parameter = parameter, - stackSlot = parameter.index + RECEIVER_STACK_SLOTS, - ) - } + val inputBindings = inputBindingsFor(manifest.inputs) return EtsEntryPointBindings( receiver = EtsReceiverBinding( @@ -286,6 +268,27 @@ internal class EtsEntryPointResolver( } } +/** The same positional transport used by the entry mapper and consumers of its mapping artifacts. */ +internal fun EtsMethod.inputBindingsFor(inputs: List): List = + inputs.zip(bindingParameters().inputs).map { (input, parameter) -> + EtsInputBinding( + propertyInputName = input.name, + parameter = parameter, + stackSlot = parameter.index + RECEIVER_STACK_SLOTS, + ) + } + +private fun EtsMethod.bindingParameters(): EtsBindingParameters { + // The frontend lifts arrow-function captures into one leading lexical-environment parameter. + // It is not a source argument; the interpreter recognizes the same parameter by its semantic type. + val hiddenClosure = parameters.firstOrNull()?.takeIf { parameter -> parameter.type is EtsLexicalEnvType } + + return EtsBindingParameters( + lexicalEnvironment = hiddenClosure, + inputs = if (hiddenClosure == null) parameters else parameters.drop(1), + ) +} + private data class EtsBindingParameters( val lexicalEnvironment: EtsMethodParameter?, val inputs: List, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt new file mode 100644 index 0000000000..18e85f9d17 --- /dev/null +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDslNumericLocalBinding.kt @@ -0,0 +1,255 @@ +package org.usvm.ts.pbt.usvm + +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNumberType +import org.usvm.ts.pbt.dsl.CompiledDslProperty +import org.usvm.ts.pbt.dsl.DslNumericLocalCapture +import org.usvm.ts.pbt.dsl.PropertyTypeScriptCompiler +import org.usvm.ts.pbt.inference.ScalarRelation +import org.usvm.ts.pbt.inference.ScalarRelationInference +import org.usvm.ts.pbt.inference.ScalarRelationStatus +import org.usvm.ts.pbt.inference.matches +import org.usvm.ts.pbt.mapping.EtsEntryPointTarget +import org.usvm.ts.pbt.mapping.EtsInputBinding +import org.usvm.ts.pbt.mapping.EtsMappingDiagnostic +import org.usvm.ts.pbt.mapping.EtsMappingResult +import org.usvm.ts.pbt.mapping.EtsMappingStatus +import org.usvm.ts.pbt.mapping.PropertyEtsMappingArtifact +import org.usvm.ts.pbt.mapping.SourceLocationNormalizer +import org.usvm.ts.pbt.mapping.inputBindingsFor +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.PropertySourcePoint +import org.usvm.ts.pbt.observation.CompilerNumericLocalBinding +import java.io.IOException +import java.nio.file.Files +import java.nio.file.InvalidPathException +import java.nio.file.Path +import java.security.MessageDigest + +/** Exact only for this compiler-owned post-store point; executable body/build provenance stays independent. */ +data class UsvmDslNumericLocalBinding( + val method: EtsMethod, + val assignment: EtsAssignStmt, + val companionAssignment: EtsAssignStmt, + val local: EtsLocal, + val inputIndex: Int, + val input: EtsInputBinding, + val resultIsLeft: Boolean, + val compiler: CompilerNumericLocalBinding, + val relation: ScalarRelation, +) + +/** Binds the retained compiler program and a complete native receipt to one original post-store point. */ +fun bindDslNumericLocalRelation( + compiled: CompiledDslProperty, + mapping: PropertyEtsMappingArtifact, + inference: ScalarRelationInference, + relation: ScalarRelation, +): EtsMappingResult { + val sameProperty = inference.property == compiled.definition && inference.propertyId == compiled.program.id && + mapping.propertyId == compiled.definition.id + if (!sameProperty) return unbound(reason = "property-mismatch", message = "The original property changed") + + val capture = compiled.numericLocalCapture + if (capture == null || !compiled.isReproducibleCompilerOutput()) { + return unbound( + reason = "compiler-mismatch", + message = "The retained program must reproduce the compiler output" + ) + } + val sampled = relation in inference.relations && relation.status == ScalarRelationStatus.SAMPLED && + relation.limitations.isEmpty() && relation.evidence.isNotEmpty() + if (!sampled) return unbound(reason = "not-sampled", message = "A complete sampled relation is required") + + val resultIsLeft = relation.pair.left == capture.result && relation.pair.right == capture.input + val resultIsRight = relation.pair.right == capture.result && relation.pair.left == capture.input + if (!resultIsLeft && !resultIsRight) { + return unbound(reason = "pair-mismatch", message = "The selected compiler result and original input must match") + } + val inputIndex = requireNotNull(capture.input.inputIndex) + val receiptsMatch = relation.evidence.all { evidence -> + val original = evidence.invocation.input.value as? JsConcreteValue.Array + val result = if (resultIsLeft) evidence.left else evidence.right + val input = if (resultIsLeft) evidence.right else evidence.left + val resultEvents = evidence.invocation.points.filter { it.pointId == capture.result.id } + val inputEvents = evidence.invocation.points.filter { it.pointId == capture.input.id } + + evidence.invocation.parentInvocationId == null && evidence.invocation.callSite == capture.result.callSite && + resultEvents.singleOrNull() == result && inputEvents.singleOrNull() == input && + result.matches(capture.result) && input.matches(capture.input) && + result.value.value is JsConcreteValue.Number && input.value.value is JsConcreteValue.Number && + input.value.value == original?.elements?.getOrNull(inputIndex) && input.eventOrdinal < result.eventOrdinal + } + val pinnedSource = inference.sources.singleOrNull { it.module == compiled.definition.predicate.module } + if (!receiptsMatch || pinnedSource?.sha256 != capture.binding.sourceSha256) { + return unbound( + reason = "receipt-mismatch", + message = "Compiler receipt, original input or selected source changed" + ) + } + + val predicateMapping = mapping.predicate + val unavailableEntry = predicateMapping.status == EtsMappingStatus.UNMAPPED || + predicateMapping.status == EtsMappingStatus.UNSUPPORTED + if (unavailableEntry) { + return EtsMappingResult( + predicateMapping.status, + targets = emptyList(), + diagnostics = predicateMapping.diagnostics + ) + } + val inputBindingsMatch = predicateMapping.targets.all { entry -> + val expected = entry.method.inputBindingsFor(compiled.definition.inputs) + + expected.size == compiled.definition.inputs.size && entry.bindings.inputs == expected + } + if (!inputBindingsMatch) { + return unbound(reason = "input-mismatch", message = "The original positional input bindings changed") + } + val locations = SourceLocationNormalizer(mapping.provenance.sourceRoots.map(Path::of)) + val module = compiled.definition.predicate.module + val paths = try { + locations.sourcePathCandidates(module).filter(Files::isRegularFile) + } catch (_: InvalidPathException) { + return unbound(reason = "source-unmapped", message = "The generated module path is unavailable") + } + if (paths.isEmpty()) { + return unbound( + reason = "source-unmapped", + message = "The generated source file is missing", + status = EtsMappingStatus.UNMAPPED + ) + } + val candidates = predicateMapping.targets.flatMap { entry -> + entry.bindCompilerStores(compiled, relation, resultIsLeft, paths, locations) + } + if (candidates.isEmpty()) { + return unbound( + reason = "store-unmapped", + message = "The original predicate and companion require their declared numeric local stores", + status = EtsMappingStatus.UNMAPPED, + ) + } + val ambiguous = paths.size != 1 || candidates.size != 1 || predicateMapping.status == EtsMappingStatus.AMBIGUOUS + if (ambiguous) { + val diagnostic = + diagnostic(reason = "store-ambiguous", message = "Several generated sources, entries or stores match") + + return EtsMappingResult(EtsMappingStatus.AMBIGUOUS, targets = candidates, diagnostics = listOf(diagnostic)) + } + val sourceMatches = compiled.matchesPinnedSources(inference, locations, generatedSource = paths.single()) + if (!sourceMatches) { + return unbound(reason = "source-stale", message = "The generated source no longer matches the original program") + } + + return EtsMappingResult(EtsMappingStatus.EXACT, targets = candidates) +} + +private fun EtsEntryPointTarget.bindCompilerStores( + compiled: CompiledDslProperty, + relation: ScalarRelation, + resultIsLeft: Boolean, + paths: List, + locations: SourceLocationNormalizer, +): List { + val capture = requireNotNull(compiled.numericLocalCapture) + val inputIndex = requireNotNull(capture.input.inputIndex) + val input = bindings.inputs.getOrNull(inputIndex) + val validEntry = method.name == capture.binding.predicateExportName && + bindings.inputs.size == compiled.definition.inputs.size && input?.parameter?.type == EtsNumberType + if (!validEntry) return emptyList() + + val owner = method.enclosingClass + val companionMethods = owner?.methods.orEmpty().filter { companion -> + companion.name == capture.binding.companionExportName && + companion.parameters.lastOrNull()?.name == "__usvmObserve" && + companion.parameters.size == method.parameters.size + 1 + } + val originals = method.storesAt(capture.binding.predicateAssignment, capture.binding.localName, paths, locations) + val companions = companionMethods.flatMap { companion -> + companion.storesAt(capture.binding.companionAssignment, capture.binding.localName, paths, locations) + } + + return originals.flatMap { assignment -> + companions.map { companion -> + UsvmDslNumericLocalBinding( + method = method, + assignment = assignment, + companionAssignment = companion, + local = assignment.lhv as EtsLocal, + inputIndex = inputIndex, + input = requireNotNull(input), + resultIsLeft = resultIsLeft, + compiler = capture.binding, + relation = relation, + ) + } + } +} + +private fun CompiledDslProperty.matchesPinnedSources( + inference: ScalarRelationInference, + locations: SourceLocationNormalizer, + generatedSource: Path, +): Boolean = try { + val selectedSourcesMatch = inference.sources.all { source -> + val paths = locations.sourcePathCandidates(source.module).filter(Files::isRegularFile) + val path = paths.singleOrNull() + val hash = path?.let { file -> + MessageDigest.getInstance("SHA-256").digest(Files.readAllBytes(file)) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + } + + hash == source.sha256 + } + + selectedSourcesMatch && Files.readString(generatedSource) == typeScript +} catch (_: IOException) { + false +} catch (_: InvalidPathException) { + false +} + +private fun CompiledDslProperty.isReproducibleCompilerOutput(): Boolean = try { + val capture = requireNotNull(numericLocalCapture) + val regenerated = PropertyTypeScriptCompiler().compile( + program, + generatedModule = definition.predicate.module, + resolveModule = { module -> requireNotNull(resolvedModules[module]) { "Unretained module: $module" } }, + numericLocalCapture = DslNumericLocalCapture(capture.binding.localName, capture.result.assertionId), + ) + + definition == regenerated.definition && typeScript == regenerated.typeScript && + numericLocalCapture == regenerated.numericLocalCapture +} catch (_: IllegalArgumentException) { + false +} + +private fun EtsMethod.storesAt( + point: PropertySourcePoint, + localName: String, + paths: List, + locations: SourceLocationNormalizer, +): List = cfg.instructions.filterIsInstance().filter { assignment -> + val local = assignment.lhv as? EtsLocal + val origin = assignment.location.origin + val pathsMatch = origin != null && locations.sourcePathCandidates(origin.fileName).any { it in paths } + + local != null && local.name == localName && local.type == EtsNumberType && origin != null && pathsMatch && + origin.startLine == point.line - 1 && origin.startColumn == point.column - 1 +} + +private fun unbound( + reason: String, + message: String, + status: EtsMappingStatus = EtsMappingStatus.UNSUPPORTED, +): EtsMappingResult { + val diagnostic = diagnostic(reason, message) + + return EtsMappingResult(status = status, targets = emptyList(), diagnostics = listOf(diagnostic)) +} + +private fun diagnostic(reason: String, message: String): EtsMappingDiagnostic = + EtsMappingDiagnostic(code = "usvm.dsl-local.$reason", message = message) diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCompilerTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCompilerTest.kt index c1bb8d8f6d..c30aaef989 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCompilerTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/dsl/DslNumericLocalCompilerTest.kt @@ -9,6 +9,29 @@ import kotlin.test.assertNull import kotlin.test.assertTrue class DslNumericLocalCompilerTest { + @Test + fun `captured program rejects inconsistent module decisions instead of claiming reproducible identity`() { + val program = defineProperty(id = "dsl.unstable-imports") { + val first = function<(Double) -> Double>(module = "helpers.ts", exportName = "first") + val second = function<(Double) -> Double>(module = "helpers.ts", exportName = "second") + val input by int() + val result by value(first(input)) + + check(name = "bound") { result lessOrEqual input } + check(name = "other") { second(input) lessOrEqual input } + } + var resolutions = 0 + + assertFailsWith { + PropertyTypeScriptCompiler().compile( + program, + generatedModule = "generated.ts", + resolveModule = { "./helper-${resolutions++}.ts" }, + numericLocalCapture = DslNumericLocalCapture(localName = "result", checkName = "bound"), + ) + } + } + @Test fun `capture is opt in and its receipt identifies both generated assignments`() { val program = program()