Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/Dependencies.kt
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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<CallsClassRawIrPoint>,
universe: List<CallsClassRawIrPoint>,
private val output: Path,
) : UMachineObserver<TsState> {
private val universe = universe.toList()
private val universePoints = this.universe.toSet()
private val universeViolations = linkedSetOf<CallsClassRawIrPoint>()

init {
require(universePoints.size == this.universe.size) { "Class IR universe contains duplicate points" }
}

private val entered = linkedSetOf<CallsClassRawIrPoint>()
private val snapshots = CallsClassRawSnapshotStore(output = output)
private val snapshotFailures = mutableListOf<String>()
Expand All @@ -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)
}

Expand Down Expand Up @@ -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,
Expand Down
Original file line number Diff line number Diff line change
@@ -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<IllegalStateException> { observer.recordOriginalEntry(unexpected) }
val resultFailure = assertFailsWith<IllegalStateException> {
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)),
),
),
)
}
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
Loading