From 8dfe313b80b9aab3e9757355d9aaa753c467ea02 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 23:45:55 +0300 Subject: [PATCH 1/2] Reject class IR hits outside the pre-frozen diagnostic universe --- .../usvm/ts/calls/CallsClassRawAnalysis.kt | 24 ++++- .../ts/calls/CallsClassRawAnalysisTest.kt | 87 +++++++++++++++++++ .../usvm/ts/calls/CallsClassStartSmokeTest.kt | 27 ++++++ 3 files changed, 136 insertions(+), 2 deletions(-) create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawAnalysisTest.kt diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt index 21690c3dfe..328c77d6c6 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt @@ -88,9 +88,17 @@ internal data class CallsClassRawAnalysis( /** Retains raw symbolic outcomes without requiring finite native observation domains. */ internal class ClassRawAnalysisObserver( private val sourceFile: String, - private val universe: List, + universe: List, private val output: Path, ) : UMachineObserver { + private val universe = universe.toList() + private val universePoints = this.universe.toSet() + private val universeViolations = linkedSetOf() + + init { + require(universePoints.size == this.universe.size) { "Class IR universe contains duplicate points" } + } + private val entered = linkedSetOf() private val snapshots = CallsClassRawSnapshotStore(output = output) private val snapshotFailures = mutableListOf() @@ -111,7 +119,13 @@ internal class ClassRawAnalysisObserver( private var quantumOverruns = 0L fun recordOriginalEntry(stmt: EtsStmt) { - entered += stmt.toClassRawIrPoint(sourceFile = sourceFile) + val point = stmt.toClassRawIrPoint(sourceFile = sourceFile) + if (point !in universePoints) { + universeViolations += point + error("Original class IR entry is outside its frozen universe: $point") + } + + entered += point sourceKinds.merge(stmt::class.java.simpleName, 1L, Long::plus) } @@ -217,6 +231,12 @@ internal class ClassRawAnalysisObserver( fun result(manifest: CallsClassStartManifest, analysisElapsedMillis: Long): CallsClassRawAnalysis { val encodedUniverse = encodeCallsArtifact(universe).toByteArray(Charsets.UTF_8) val journals = snapshots.finish() + // Exploratory execution may retain interpreter failures as terminal states. + // Such a failure must still invalidate this diagnostic denominator. + check(universeViolations.isEmpty()) { + "Original class IR entries are outside their frozen universe: $universeViolations" + } + return CallsClassRawAnalysis( budgetMillis = manifest.budgetMillis, analysisElapsedMillis = analysisElapsedMillis, diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawAnalysisTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawAnalysisTest.kt new file mode 100644 index 0000000000..67f27f8c69 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawAnalysisTest.kt @@ -0,0 +1,87 @@ +package org.usvm.ts.calls + +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsMethodImpl +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsSourceSpan +import org.jacodb.ets.model.EtsStmtLocation +import org.jacodb.ets.model.EtsUndefinedType +import org.junit.jupiter.api.io.TempDir +import java.nio.file.Path +import kotlin.test.Test +import kotlin.test.assertFailsWith +import kotlin.test.assertTrue + +class CallsClassRawAnalysisTest { + @TempDir + lateinit var directory: Path + + @Test + fun `unknown hit invalidates the frozen universe even if its callback failure is caught`() { + val admitted = statement(methodName = "read") + val unexpected = statement(methodName = "%AM0\$read") + val universe = mutableListOf(point(admitted)) + val observer = ClassRawAnalysisObserver(sourceFile = "Target.ts", universe = universe, output = directory) + + observer.recordOriginalEntry(admitted) + universe += point(unexpected) + val callbackFailure = assertFailsWith { observer.recordOriginalEntry(unexpected) } + val resultFailure = assertFailsWith { + observer.result(manifest = manifest(), analysisElapsedMillis = 0) + } + + assertTrue(callbackFailure.message.orEmpty().contains("outside its frozen universe")) + assertTrue(resultFailure.message.orEmpty().contains("outside their frozen universe")) + assertTrue(resultFailure.message.orEmpty().contains("%AM0\$read")) + } + + private fun statement(methodName: String): EtsReturnStmt { + val owner = EtsClassSignature( + name = "Target", + file = EtsFileSignature(projectName = "fixture", fileName = "Target.ts"), + ) + val method = EtsMethodImpl( + EtsMethodSignature( + enclosingClass = owner, + name = methodName, + parameters = emptyList(), + returnType = EtsUndefinedType, + ), + ) + val location = EtsStmtLocation(method = method, index = 0) + location.origin = EtsSourceSpan( + fileName = "Target.ts", startOffset = 0, endOffset = 7, + startLine = 0, startColumn = 0, endLine = 0, endColumn = 7, nodeKind = "ReturnStatement", + ) + return EtsReturnStmt(location = location, returnValue = null) + } + + private fun point(stmt: EtsReturnStmt): CallsClassRawIrPoint = CallsClassRawIrPoint( + method = stmt.location.method.signature.toString(), + statementIndex = 0, + sourceFile = "Target.ts", + startOffset = 0, + endOffset = 7, + nodeKind = "ReturnStatement", + ) + + private fun manifest(): CallsClassStartManifest = CallsClassStartManifest( + toolRevision = "fixture", + nativeFrontendRevision = "fixture", + ledgerSha256 = "b".repeat(64), + expectedClassCount = 1, + classes = listOf( + CallsClassStartCase( + classId = "target", + identity = "fixture@Target", + projectRevision = "a".repeat(40), + sourceRoot = directory.toString(), + sourceFile = "Target.ts", + className = "Target", + inputSha256 = mapOf("Target.ts" to "c".repeat(64)), + ), + ), + ) +} diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt index a55db490f7..acd94c5d99 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -181,6 +181,33 @@ class CallsClassStartSmokeTest { assertTrue(result.stage != "TARGET", result.toString()) } + @Test + fun `interface before runtime class keeps lifted closures in the frozen IR universe`() { + assertMergedClosureUniverse(interfaceFirst = true) + } + + @Test + fun `interface after runtime class keeps lifted closures in the frozen IR universe`() { + assertMergedClosureUniverse(interfaceFirst = false) + } + + private fun assertMergedClosureUniverse(interfaceFirst: Boolean) { + val augmentation = "export interface Target { read(value: number): number; }" + val implementation = "export class Target { read(value: number): number { " + + "const increment = (input: number): number => { return input + 1; }; return increment(value); } }" + val source = if (interfaceFirst) augmentation + implementation else implementation + augmentation + + val result = runFixture(sourceText = source, exploratory = true) + + assertTrue(result.started, result.toString()) + val raw = checkNotNull(result.rawAnalysis) + val closurePoints = raw.sourceMappedIrUniverse.filter { it.method.contains("%AM") } + assertTrue(closurePoints.isNotEmpty(), raw.toString()) + assertTrue(raw.sourceMappedIrEntered.any { it in closurePoints }, raw.toString()) + assertTrue(raw.sourceMappedIrUniverse.containsAll(raw.sourceMappedIrEntered), raw.toString()) + assertTrue(raw.returnedStates > 0, raw.toString()) + } + @Test fun `lowered closures keep complete IR but require their owning member environment`() { val result = runFixture( From 9a9434a324ba840300031e5e5bd4815fcbd3b1da Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 00:12:32 +0300 Subject: [PATCH 2/2] Pin closure ownership frontend required by source regression --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 351592d50d..a36dd82748 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "7db549ef2a6c2cd05e9403e3e2e7087df7c5fcc2" + const val jacodb = "c6d1fe316cdca9b08a674e1638ff6d485ae17824" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0"