Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
61 commits
Select commit Hold shift + click to select a range
beef938
Support parameterized EtsIR model families
CaelmBleidd Sep 20, 2026
c48f468
Add primary numeric intrinsic models
CaelmBleidd Sep 20, 2026
28becf2
Test primary numeric intrinsic semantics
CaelmBleidd Sep 20, 2026
f403bbe
Allow calls runner to use bundled frontend
CaelmBleidd Sep 20, 2026
51d405d
Model Array and String search methods in TypeScript
CaelmBleidd Sep 20, 2026
6ec06c8
Let EtsIR adapters resolve raw call inputs
CaelmBleidd Sep 20, 2026
3f826bc
Test adapters with unresolved namespace receivers
CaelmBleidd Sep 20, 2026
c7daaf0
Extend source sequence models
CaelmBleidd Sep 20, 2026
b4a22f7
Expand semantic model dependencies
CaelmBleidd Sep 20, 2026
0826fab
Bound sequence offset normalization
CaelmBleidd Sep 20, 2026
635026a
Add adjacent numeric intrinsic models
CaelmBleidd Sep 20, 2026
d1f242a
Declare source model dependencies and domains
CaelmBleidd Sep 20, 2026
24acd4d
Model numeric Date APIs in TypeScript
CaelmBleidd Sep 20, 2026
d0b9f2d
Guard sparse Array search domains
CaelmBleidd Sep 20, 2026
fdd0611
Canonicalize Array search zero results
CaelmBleidd Sep 20, 2026
dbfcfa2
Require concrete String code units
CaelmBleidd Sep 20, 2026
284a6d2
Handle Date UTC omissions and invalid timezone offsets
CaelmBleidd Sep 20, 2026
c9890ed
Truncate Date fractions toward zero
CaelmBleidd Sep 20, 2026
563718b
Resolve Date calls through any aliases
CaelmBleidd Sep 20, 2026
33781b4
Model remaining UTC minute setters
CaelmBleidd Sep 20, 2026
1cdd5f1
Strengthen Date model registrations and tests
CaelmBleidd Sep 20, 2026
cf2d6d8
Fix Date registration formatting
CaelmBleidd Sep 20, 2026
6f32a79
Use Math.floor in Date calendar arithmetic
CaelmBleidd Sep 20, 2026
194ea90
Document model coverage and declare Date rounding dependency
CaelmBleidd Sep 20, 2026
1a6315d
Fix Date test formatting
CaelmBleidd Sep 20, 2026
2e80186
Allow modeled NaN checks in Array removal matrix
CaelmBleidd Sep 20, 2026
b279fbe
Satisfy numeric model style checks
CaelmBleidd Sep 20, 2026
8e1353c
Clean up sequence model style
CaelmBleidd Sep 20, 2026
c08c8c6
Support symbolic Calls inputs and preflight telemetry
CaelmBleidd Sep 20, 2026
d57f7d9
Fix symbolic value semantics and add bounded array and string models
CaelmBleidd Sep 20, 2026
411b48b
Support Error and Array constructors, replacement, and erased assertions
CaelmBleidd Sep 20, 2026
2502bdb
Reject callable arguments before querying modeled string types
CaelmBleidd Sep 20, 2026
1ec9cd9
Isolate Error model storage from user property resolution
CaelmBleidd Sep 20, 2026
8799236
Handle conditional string operands before type lookup (#392)
CaelmBleidd Sep 22, 2026
d6e6ccf
fix(ts): write fake values using field sort (#393)
CaelmBleidd Sep 22, 2026
3b97760
fix(ts): guard built-in Date model provenance
CaelmBleidd Sep 30, 2026
81d76b9
refactor(ts): share model field and call site resolution
CaelmBleidd Sep 30, 2026
a1bbe45
Model built-in TypeError construction for array callbacks
CaelmBleidd Sep 21, 2026
98b13a6
Execute split, join and dense reduce callbacks through source models
CaelmBleidd Sep 21, 2026
6247c15
Parse bounded decimal prefixes with exact binary64 rounding
CaelmBleidd Sep 21, 2026
615bc30
Load validated local TypeScript dependencies in Calls experiments
CaelmBleidd Sep 21, 2026
78985c2
fix(ts): refresh source closure and reject ambient runtime exports
CaelmBleidd Sep 30, 2026
e63ae37
style(ts): keep model stack lint clean
CaelmBleidd Sep 30, 2026
dd8847f
Handle residual runtime limitations in TypeScript search
CaelmBleidd Sep 30, 2026
f2cb653
Deduplicate array storage limitation telemetry per analysis
CaelmBleidd Sep 30, 2026
c627855
Route synthetic virtual receivers through unknown-call policy
CaelmBleidd Sep 30, 2026
df0530b
Classify synthetic field receivers as runtime limitations
CaelmBleidd Sep 30, 2026
457dd31
Report conditional field receivers as runtime limitations
CaelmBleidd Sep 30, 2026
240bf62
fix(ts): keep fake type reflexive in type constraints
CaelmBleidd Sep 30, 2026
abbee67
style(ts): clear new runtime stack lint findings
CaelmBleidd Sep 30, 2026
d61d7e4
fix(ts): keep fresh string constraint on residual branch
CaelmBleidd Oct 1, 2026
8db662c
fix(ts): distinguish infeasible fresh string from solver uncertainty
CaelmBleidd Oct 1, 2026
3598f5a
fix(ts-calls): bound solver queries by search budget
CaelmBleidd Oct 1, 2026
5b55c65
Map exact c8 TypeScript if arms to CFG coverage
CaelmBleidd Sep 30, 2026
0f66e4f
[TS] Share analysis hooks and UTF-16 infrastructure between PBT and C…
CaelmBleidd Oct 1, 2026
77674c5
[TS] Preserve protocol values across user code and validate number bits
CaelmBleidd Oct 1, 2026
ab880e4
[TS] Reuse bounded process and coverage fixes from PBT
CaelmBleidd Oct 1, 2026
b1c0c7d
[TS] Apply frontend cleanup and retain modeled thrown Error types
CaelmBleidd Oct 1, 2026
1ae4c13
[TS] Add source-replayed coverage experiment cells
CaelmBleidd Oct 1, 2026
1b29522
[TS] Replay zero-argument coverage candidates
CaelmBleidd Oct 1, 2026
6979da0
[TS] Integrate latest model hardening for coverage
CaelmBleidd Oct 1, 2026
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 = "ddb127d9ef"
const val jacodb = "873f8e99faf3f1e4736935be96ce1c319985c574"
const val juliet = "1.3.2"
const val junit = "5.9.3"
const val kotlin = "2.1.0"
Expand Down
9 changes: 8 additions & 1 deletion usvm-ts-calls/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,13 @@ val toolStatus = providers.exec {
workingDir(rootProject.projectDir)
commandLine("git", "status", "--porcelain", "--untracked-files=all")
}.standardOutput.asText.map(String::trim)
val nativeFrontendRevision = providers.gradleProperty("nativeFrontendRevision")
.orElse("bundled:${Versions.jacodb}")

val generateBuildMetadata = tasks.register("generateBuildMetadata") {
inputs.property("toolRevision", toolRevision)
inputs.property("toolStatus", toolStatus)
inputs.property("nativeFrontendRevision", nativeFrontendRevision)
outputs.dir(generatedBuildMetadataDirectory)

doLast {
Expand All @@ -39,7 +42,11 @@ val generateBuildMetadata = tasks.register("generateBuildMetadata") {
.file("org/usvm/ts/calls/build.properties")
.asFile
metadataFile.parentFile.mkdirs()
metadataFile.writeText("tool.revision=$buildIdentity\n", Charsets.UTF_8)
metadataFile.writeText(
"tool.revision=$buildIdentity\n" +
"native.frontend.revision=${nativeFrontendRevision.get()}\n",
Charsets.UTF_8,
)
}
}

Expand Down
202 changes: 202 additions & 0 deletions usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt
Original file line number Diff line number Diff line change
@@ -0,0 +1,202 @@
package org.usvm.ts.calls

import kotlinx.serialization.Serializable
import kotlinx.serialization.decodeFromString
import org.usvm.ts.pbt.model.encodeToUtf8SafeString
import java.nio.ByteBuffer
import java.nio.channels.FileChannel
import java.nio.file.Files
import java.nio.file.Path
import java.nio.file.StandardCopyOption
import java.nio.file.StandardOpenOption
import kotlin.time.Duration.Companion.milliseconds

@Serializable
internal data class CallsCoverageCellIdentity(
val schemaVersion: Int,
val toolRevision: String,
val nativeFrontendRevision: String,
val sourceManifest: String,
val projectIndex: Int,
val functionIndex: Int,
val profile: CallsExperimentProfile,
val seed: Long,
val budgetMillis: Long,
val solverLimitMillis: Long,
val candidateCap: Int,
)

@Serializable
internal data class CallsCoverageReplayEvent(
val index: Int,
val replay: CallsCoverageReplayResult? = null,
val error: String? = null,
)

@Serializable
internal data class CallsCoverageCheckpoint(
val searchBudgetMillis: Long,
val emittedCandidates: Int,
val replayedCandidates: Int,
val coveredStatements: Int,
val coveredIfArms: Int,
)

@Serializable
internal data class CallsCoverageCellResult(
val identity: CallsCoverageCellIdentity,
val search: CallsCoverageSearchResult,
val replayErrors: Int,
val completionMismatches: Int,
val checkpoints: List<CallsCoverageCheckpoint>,
)

internal fun runCoverageCell(args: List<String>) {
require(args.size == 9) { "coverage-cell requires 9 arguments" }
val manifestPath = Path.of(args[0]).toRealPath()
val manifest = CallsExperimentJson.decodeManifest(Files.readString(manifestPath))
val projectIndex = args[1].toInt()
val functionIndex = args[2].toInt()
val profile = CallsExperimentProfile.valueOf(args[3])
val seed = args[4].toLong()
val output = Path.of(args[5]).toAbsolutePath().normalize()
val budgetMillis = args[6].toLong()
val solverLimitMillis = args[7].toLong()
val candidateCap = args[8].toInt()
val project = manifest.projects[projectIndex]
val function = project.functions[functionIndex]
require(seed in manifest.seeds) { "Seed is outside the frozen source manifest" }
require(budgetMillis > 0 && solverLimitMillis in 1..budgetMillis && candidateCap > 0)
require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { "ETS_FRONTEND_SCRIPT must be unset" }

val identity = CallsCoverageCellIdentity(
schemaVersion = 1,
toolRevision = CallsBuildIdentity.toolRevision,
nativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision,
sourceManifest = manifestPath.toString(),
projectIndex = projectIndex,
functionIndex = functionIndex,
profile = profile,
seed = seed,
budgetMillis = budgetMillis,
solverLimitMillis = solverLimitMillis,
candidateCap = candidateCap,
)
require(Regex("[0-9a-f]{40}").matches(identity.toolRevision)) { "Coverage build must be clean" }

Files.createDirectories(output)
val identityPath = output.resolve("identity.json")
val expectedIdentity = encode(identity)
if (Files.exists(identityPath)) {
require(Files.readString(identityPath).trim() == expectedIdentity) { "Cell identity changed" }
} else {
require(Files.list(output).use { entries -> entries.findAny().isEmpty }) { "Output directory is not empty" }
atomicWrite(identityPath, expectedIdentity)
}
require(!Files.exists(output.resolve("result.json"))) { "Cell already completed" }

val candidatePath = output.resolve("candidates.jsonl")
val searchPath = output.resolve("search.json")
val search = if (Files.exists(searchPath)) {
CallsExperimentJson.json.decodeFromString<CallsCoverageSearchResult>(Files.readString(searchPath))
} else {
require(!Files.exists(candidatePath)) { "Interrupted search requires investigation before restart" }
val request = CallsCoverageSearchRequest(
sourceRoot = manifestPath.parent.resolve(project.sourceRoot).toRealPath(),
project = project,
function = function,
profile = profile,
frozenModelIds = manifest.modelSet.ids,
expectedNativeFrontendRevision = identity.nativeFrontendRevision,
seed = seed,
budget = budgetMillis.milliseconds,
solverQueryLimit = solverLimitMillis.milliseconds,
candidateCap = candidateCap,
onCandidate = { candidate -> appendDurably(candidatePath, encode(candidate)) },
)
val result = CurrentTsCallsCoverageEngine().search(request)
val persistedCandidates = readLines<CallsCoverageCandidate>(candidatePath)
require(result.candidates == persistedCandidates) { "Persisted candidate journal differs from search result" }
atomicWrite(searchPath, encode(result))
result
}

val replayPath = output.resolve("replays.jsonl")
val events = readLines<CallsCoverageReplayEvent>(replayPath).toMutableList()
require(events.map(CallsCoverageReplayEvent::index) == events.indices.toList()) {
"Replay journal has missing or duplicate indices"
}
if (search.candidates.isNotEmpty()) {
OriginalTypeScriptCoverageReplayer(
sourceRoot = manifestPath.parent.resolve(project.sourceRoot),
function = function,
).use { replayer ->
search.candidates.indices.drop(events.size).forEach { index ->
val candidate = search.candidates[index]
val replay = runCatching {
replayer.replay(inputs = candidate.inputs, timeoutMillis = REPLAY_TIMEOUT_MILLIS)
}
val event = CallsCoverageReplayEvent(
index = index,
replay = replay.getOrNull(),
error = replay.exceptionOrNull()?.let { error -> error.message ?: error::class.java.name },
)
appendDurably(replayPath, encode(event))
events += event
}
}
}

val checkpoints = listOf(30_000L, 60_000L, 120_000L).filter { it <= budgetMillis }.map { checkpoint ->
val indices = search.candidates.indices.filter { index ->
search.candidates[index].emittedAtMillis <= checkpoint
}
val replayed = indices.mapNotNull { index -> events[index].replay }
CallsCoverageCheckpoint(
searchBudgetMillis = checkpoint,
emittedCandidates = indices.size,
replayedCandidates = replayed.size,
coveredStatements = replayed.flatMap { it.coveredStatementKeys }.toSet().size,
coveredIfArms = replayed.flatMap { it.coveredIfArmKeys }.toSet().size,
)
}
val result = CallsCoverageCellResult(
identity = identity,
search = search,
replayErrors = events.count { it.error != null },
completionMismatches = events.indices.count { index ->
events[index].replay?.completion != null &&
events[index].replay?.completion != search.candidates[index].completion
},
checkpoints = checkpoints,
)
atomicWrite(output.resolve("result.json"), encode(result))
println(encode(result))
}

private inline fun <reified T> readLines(path: Path): List<T> = if (Files.exists(path)) {
Files.readAllLines(path).filter(String::isNotBlank).map { line ->
CallsExperimentJson.json.decodeFromString<T>(line)
}
} else {
emptyList()
}

private inline fun <reified T> encode(value: T): String = CallsExperimentJson.json.encodeToUtf8SafeString(value)

private fun appendDurably(path: Path, line: String) {
val bytes = ByteBuffer.wrap((line + "\n").toByteArray(Charsets.UTF_8))
FileChannel.open(path, StandardOpenOption.CREATE, StandardOpenOption.WRITE, StandardOpenOption.APPEND).use { channel ->
while (bytes.hasRemaining()) channel.write(bytes)
channel.force(true)
}
}

private fun atomicWrite(path: Path, contents: String) {
val temporary = path.resolveSibling("${path.fileName}.tmp")
Files.writeString(temporary, contents + "\n")
FileChannel.open(temporary, StandardOpenOption.READ).use { it.force(true) }
Files.move(temporary, path, StandardCopyOption.ATOMIC_MOVE)
}

private const val REPLAY_TIMEOUT_MILLIS = 20_000L
Loading