Fix TypeScript execution and Calls/PBT contracts after full review

.github/workflows/ci.yml

@@ -154,6 +154,18 @@ jobs:
       - name: Run TS PBT integration baseline
         run: env -u ARKANALYZER_DIR ETS_IR_PROVIDER=ts-frontend ./gradlew :usvm-ts-pbt:check :usvm-ts-fast-check:check
 
+      - name: Upload Gradle reports
+        if: (!cancelled())
+        uses: actions/upload-artifact@v4
+        with:
+          name: gradle-reports-ts-pbt
+          path: |
+            usvm-ts-pbt/build/test-results/**/*.xml
+            usvm-ts-pbt/build/reports/tests/
+            usvm-ts-fast-check/build/test-results/**/*.xml
+            usvm-ts-fast-check/build/reports/tests/
+          retention-days: 1
+
   lint:
     runs-on: ubuntu-latest
     steps:

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt

@@ -170,8 +170,8 @@ internal fun runCoverageCell(
         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
+            val replayCompletion = events[index].replay?.completion
+            replayCompletion != null && replayCompletion != search.candidates[index].completion
         },
         replayElapsedMillis = events.sumOf { event -> event.replay?.replayElapsedMillis ?: 0L },
         cellElapsedMillis = cellStarted.elapsedNow().inWholeMilliseconds,
@@ -235,11 +235,12 @@ private fun parseCoverageCellRequest(
     )
     require(universeRecord.identity == expectedUniverseIdentity) { "Coverage universe identity differs" }
     val universe = universeRecord.universe
-    require(source.function.sourceFile in universe.sourceFiles && universe.supportedStatementKeys.isNotEmpty()) {
+    val includesEntrySource = source.function.sourceFile in universe.sourceFiles
+    val hasSupportedStatements = universe.supportedStatementKeys.isNotEmpty()
+    require(includesEntrySource && hasSupportedStatements) {
         "Coverage universe does not include the entry source statements"
     }
 
-
     val identity = CallsCoverageCellIdentity(
         schemaVersion = 3,
         toolRevision = runtimeToolRevision,

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt

@@ -7,10 +7,12 @@ import org.usvm.ts.pbt.backend.PropertyCoverageRequest
 import org.usvm.ts.pbt.backend.PropertyRunConfiguration
 import org.usvm.ts.pbt.backend.PropertyRunStatus
 import org.usvm.ts.pbt.backend.SourceFileCoverage
+import org.usvm.ts.pbt.backend.SourceRange
 import org.usvm.ts.pbt.fastcheck.FastCheckBackend
 import org.usvm.ts.pbt.fastcheck.FastCheckRuntime
 import org.usvm.ts.pbt.fastcheck.TypeScriptSourceInspector
 import org.usvm.ts.pbt.model.BooleanDomain
+import org.usvm.ts.pbt.model.ExecutionKind
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.PropertyId
@@ -71,7 +73,7 @@ internal class OriginalTypeScriptCoverageReplayer(
     }
 
     private fun prepareReplay(): CoverageReplaySetup {
-        require(function.entryPoint.executionKind == org.usvm.ts.pbt.model.ExecutionKind.SYNC) {
+        require(function.entryPoint.executionKind == ExecutionKind.SYNC) {
             "Coverage replay requires a synchronous entry point"
         }
         val source = sourceRoot.resolve(function.sourceFile).normalize()
@@ -262,7 +264,7 @@ private fun collectHits(
     }
 }
 
-private fun org.usvm.ts.pbt.backend.SourceRange.stableKey(): String =
+private fun SourceRange.stableKey(): String =
     "${start.line}:${start.column}-${end.line}:${end.column}"
 
 private fun coverageWrapper(
@@ -302,8 +304,9 @@ private fun coverageWrapper(
             return { kind: 'number', value: 'finite', bits };
           }
           if (Array.isArray(value)) return { kind: 'array', elements: value.map(encodeValue) };
-          if (value !== null && typeof value === 'object' &&
-              (Object.getPrototypeOf(value) === Object.prototype || Object.getPrototypeOf(value) === null)) {
+          const isPlainObject = value !== null && typeof value === 'object' &&
+            (Object.getPrototypeOf(value) === Object.prototype || Object.getPrototypeOf(value) === null);
+          if (isPlainObject) {
             const fields = Object.fromEntries(Object.entries(value).map(([name, field]) => {
               if (['__proto__', 'constructor', 'prototype'].includes(name)) {
                 throw new Error('Unsupported replay object property name');

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt

@@ -89,22 +89,28 @@ internal data class CallsExperimentManifest(
             "Tool revision must identify a clean Git commit"
         }
         require(toolRevision == modelSet.toolRevision) { "Tool and model-set revisions must match" }
+
         val functions = projects.flatMap(CallsProjectCase::functions)
-        require(functions.map(CallsFunctionCase::functionId).distinct().size == functions.size) {
+        val uniqueFunctionIds = functions.map(CallsFunctionCase::functionId).distinct()
+        require(uniqueFunctionIds.size == functions.size) {
             "Function IDs must be unique"
         }
-        require(functions.all { function -> function.sourceFile == function.entryPoint.module }) {
+        val sourceFilesMatchEntryPoints = functions.all { function ->
+            function.sourceFile == function.entryPoint.module
+        }
+        require(sourceFilesMatchEntryPoints) {
             "Function source files must match their replay entry-point modules"
         }
+
         val targets = functions.flatMap(CallsFunctionCase::targets)
-        require(targets.map(CallsSourceTarget::targetId).distinct().size == targets.size) {
+        val uniqueTargetIds = targets.map(CallsSourceTarget::targetId).distinct()
+        require(uniqueTargetIds.size == targets.size) {
             "Target IDs must be unique"
         }
-        require(
-            functions.all { function ->
-                function.targets.all { target -> target.sourcePath == function.sourceFile }
-            },
-        ) {
+        val targetsBelongToFunctionSourceFiles = functions.all { function ->
+            function.targets.all { target -> target.sourcePath == function.sourceFile }
+        }
+        require(targetsBelongToFunctionSourceFiles) {
             "Every target must belong to its function source file"
         }
     }
@@ -267,12 +273,12 @@ internal object CallsBuildIdentity {
     }
 
     val toolRevision: String by lazy {
-        checkNotNull(properties.getProperty("tool.revision")).takeIf(String::isNotBlank)
+        properties.getProperty("tool.revision")?.takeIf(String::isNotBlank)
             ?: error("Missing tool revision in calls build identity")
     }
 
     val nativeFrontendRevision: String by lazy {
-        checkNotNull(properties.getProperty("native.frontend.revision")).takeIf(String::isNotBlank)
+        properties.getProperty("native.frontend.revision")?.takeIf(String::isNotBlank)
             ?: error("Missing native frontend revision in calls build identity")
     }
 }
@@ -282,6 +288,8 @@ internal class CallsExperimentRunner(
     private val targetReplayer: CallsTargetReplayer,
     private val runtimeToolRevision: String = CallsBuildIdentity.toolRevision,
     private val eventRecordWriter: ((Path, CallsRawRecord) -> Unit)? = null,
+    private val sourceCheckoutVerifier: (Path, String) -> Unit = ::verifyCallsGitCheckout,
+    private val frontendRuntimeVerifier: (String) -> Unit = ::verifyCallsExternalFrontendRuntime,
 ) {
     fun run(
         manifest: CallsExperimentManifest,
@@ -348,6 +356,15 @@ internal class CallsExperimentRunner(
                 resultRows = resultRows,
             ),
         )
+
+        manifest.projects.forEach { project ->
+            val sourceRoot = manifestDirectory.resolve(project.sourceRoot).normalize().toRealPath()
+            sourceCheckoutVerifier(sourceRoot, project.revision)
+        }
+        if (!manifest.nativeFrontendRevision.startsWith("bundled:")) {
+            frontendRuntimeVerifier(manifest.nativeFrontendRevision)
+        }
+
         Files.move(
             partialOutput,
             rawOutput,
@@ -415,6 +432,8 @@ internal class CallsExperimentRunner(
         profile: CallsExperimentProfile,
         appendUnknownCall: (CallsRawRecord) -> Unit,
     ): CallsTargetResult {
+        sourceCheckoutVerifier(sourceRoot, project.revision)
+
         val request = CallsSymbolicSearchRequest(
             sourceRoot = sourceRoot,
             project = project,
@@ -443,14 +462,19 @@ internal class CallsExperimentRunner(
             ),
         )
         eventWrites.requireComplete()
+        sourceCheckoutVerifier(sourceRoot, project.revision)
+
         val replay = symbolic.inputs?.let { inputs ->
-            targetReplayer.replay(
+            val replayResult = targetReplayer.replay(
                 sourceRoots = listOf(sourceRoot),
                 entryPoint = function.entryPoint,
                 inputs = inputs,
                 target = target,
                 timeoutMillis = manifest.perTargetBudgetMillis,
             )
+            sourceCheckoutVerifier(sourceRoot, project.revision)
+
+            replayResult
         }
 
         return CallsTargetResult(
@@ -543,16 +567,17 @@ internal object CallsRawResultsReader {
         require(results.all { result -> result.experimentId == metadata.experimentId }) {
             "Result experiment ID does not match metadata"
         }
-        require(
-            results.all { result ->
-                val identity = targetIdentities[Triple(result.projectId, result.functionId, result.targetId)]
-                identity != null &&
-                    result.revision == identity.revision &&
-                    result.development == identity.development &&
-                    result.siteId == identity.siteId &&
-                    result.targetMode == identity.targetMode
-            },
-        ) { "Result target identity does not match metadata" }
+        val resultsMatchTargetIdentities = results.all { result ->
+            val identity = targetIdentities[Triple(result.projectId, result.functionId, result.targetId)]
+            identity != null &&
+                result.revision == identity.revision &&
+                result.development == identity.development &&
+                result.siteId == identity.siteId &&
+                result.targetMode == identity.targetMode
+        }
+
+        require(resultsMatchTargetIdentities) { "Result target identity does not match metadata" }
+
         val resultKeys = results.map { result ->
             ResultKey(
                 projectId = result.projectId,

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt

@@ -18,6 +18,7 @@ fun main(args: Array<String>) {
         "coverage-cell" -> runCoverageCell(args.drop(1))
         "replay-witness" -> replayWitness(args.drop(1))
         "summarize" -> summarize(args.drop(1))
+        "frontend-identity" -> System.out.appendLine(frontendIdentity(args.drop(1)))
         else -> error(usage())
     }
 }
@@ -82,6 +83,9 @@ private fun summarize(args: List<String>) {
     val rawInput = Path.of(args[0]).toAbsolutePath().normalize()
     val output = Path.of(args[1]).toAbsolutePath().normalize()
     val summary = CallsExperimentAggregator.summarize(rawInput)
+    val outputIsRawInput = rawInput == output || (Files.exists(output) && Files.isSameFile(rawInput, output))
+    require(!outputIsRawInput) { "Summary output must differ from raw input" }
+
     val json = Json {
         encodeDefaults = true
         explicitNulls = false
@@ -91,6 +95,12 @@ private fun summarize(args: List<String>) {
     Files.writeString(output, json.encodeToUtf8SafeString(summary) + "\n")
 }
 
+internal fun frontendIdentity(args: List<String>): String {
+    require(args.size == 1) { usage() }
+    val frontendDirectory = Path.of(args.single()).toRealPath()
+    return callsExternalFrontendIdentity(frontendDirectory)
+}
+
 private fun usage(): String = """
     Usage:
       calls class-catalog
@@ -102,6 +112,7 @@ private fun usage(): String = """
       calls coverage-cell <source-manifest.json> <project-index> <function-index> <profile> <seed> <output-directory> <budget-ms> <solver-limit-ms> <candidate-cap> <universe.json>
       calls replay-witness <frozen-manifest.json> <results.jsonl> <project-id> <function-id> <target-id> <profile> <seed>
       calls summarize <results.jsonl> <summary.json>
+      calls frontend-identity <external-frontend-directory>
 """.trimIndent()
 
 private const val REPLAY_WITNESS_ARGUMENT_COUNT = 7