Handle residual TypeScript runtime limitations in Calls experiments

usvm-ts-calls/build.gradle.kts

@@ -26,11 +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("jacodbVersion", Versions.jacodb)
+    inputs.property("nativeFrontendRevision", nativeFrontendRevision)
     outputs.dir(generatedBuildMetadataDirectory)
 
     doLast {
@@ -42,7 +44,7 @@ val generateBuildMetadata = tasks.register("generateBuildMetadata") {
         metadataFile.parentFile.mkdirs()
         metadataFile.writeText(
             "tool.revision=$buildIdentity\n" +
-                "native.frontend.revision=bundled:${Versions.jacodb}\n",
+                "native.frontend.revision=${nativeFrontendRevision.get()}\n",
             Charsets.UTF_8,
         )
     }

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

@@ -14,6 +14,7 @@ import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
+import org.usvm.machine.TsRuntimeFeatureLimitationReason
 import org.usvm.machine.call.TsUnknownCallEvent
 import org.usvm.machine.call.TsUnknownCallModelSelection
 import org.usvm.machine.state.TsMethodResult
@@ -149,6 +150,7 @@ internal class CurrentTsCallsSymbolicEngine(
             stateCollectionStrategy = StateCollectionStrategy.REACHED_TARGET,
             randomSeed = request.seed,
             timeout = request.budget,
+            solverTimeout = request.budget,
             solverType = SolverType.Z3,
             stopOnCoverage = CALLS_STOP_ON_COVERAGE,
             stopOnTargetsReached = false,
@@ -624,19 +626,26 @@ internal class CurrentTsCallsSymbolicEngine(
         }
     }
 
-    private class UnknownCallEventSinkObserver(
+    internal class UnknownCallEventSinkObserver(
         private val sink: ((TsUnknownCallEvent) -> Unit)?,
         private val runtimeLimitationSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)?,
     ) : TsInterpreterObserver {
         val runtimeLimitations = linkedSetOf<String>()
 
+        // Keep one telemetry record per unsupported storage and statement in this analysis.
+        private val reportedArrayStorageLimitations = hashSetOf<Pair<EtsStmt, String>>()
+
         override fun onUnknownCall(event: TsUnknownCallEvent) {
             sink?.invoke(event)
         }
 
         override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) {
             runtimeLimitations += event.reason.name
-            runtimeLimitationSink?.invoke(event)
+            if (event.reason != TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE ||
+                reportedArrayStorageLimitations.add(event.statement to event.detail)
+            ) {
+                runtimeLimitationSink?.invoke(event)
+            }
         }
     }
 

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetryTest.kt

@@ -4,6 +4,8 @@ import kotlinx.serialization.decodeFromString
 import kotlinx.serialization.encodeToString
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.usvm.machine.TsRuntimeFeatureLimitationEvent
+import org.usvm.machine.TsRuntimeFeatureLimitationReason
 import org.usvm.machine.call.TsResidualCallPolicy
 import org.usvm.machine.call.TsUnknownCallDecision
 import org.usvm.machine.call.TsUnknownCallEvent
@@ -17,6 +19,54 @@ import kotlin.test.assertNotNull
 import kotlin.test.assertNull
 
 class CallsUnknownCallTelemetryTest {
+    @Test
+    fun `observer records array storage limitation once per statement and detail`() {
+        val source = resourcePath("/calls/SourceTargetReplayFixture.ts")
+        val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)
+        val method = file.allClasses.flatMap { cls -> cls.methods }
+            .single { candidate -> candidate.name == "completesReturnExpression" }
+        val statements = method.cfg.stmts.take(2)
+        val records = mutableListOf<TsRuntimeFeatureLimitationEvent>()
+        val observer = CurrentTsCallsSymbolicEngine.UnknownCallEventSinkObserver(
+            sink = null,
+            runtimeLimitationSink = records::add,
+        )
+        val arrayStorage = TsRuntimeFeatureLimitationEvent(
+            statement = statements[0],
+            reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE,
+            detail = "storage=Uint8Array",
+        )
+        val otherStorage = arrayStorage.copy(detail = "storage=Uint16Array")
+        val otherStatement = arrayStorage.copy(statement = statements[1])
+        val otherReason = arrayStorage.copy(reason = TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_READ)
+
+        // Repeated callbacks represent different states reaching the same unsupported access.
+        observer.onRuntimeFeatureLimitation(arrayStorage)
+        observer.onRuntimeFeatureLimitation(arrayStorage)
+        observer.onRuntimeFeatureLimitation(otherStorage)
+        observer.onRuntimeFeatureLimitation(otherStatement)
+        observer.onRuntimeFeatureLimitation(otherReason)
+        observer.onRuntimeFeatureLimitation(otherReason)
+
+        assertEquals(
+            listOf(arrayStorage, otherStorage, otherStatement, otherReason, otherReason),
+            records,
+        )
+        assertEquals(
+            setOf("ARRAY_STORAGE_TYPE", "ARRAY_NAMED_PROPERTY_READ"),
+            observer.runtimeLimitations,
+        )
+
+        val nextAnalysisRecords = mutableListOf<TsRuntimeFeatureLimitationEvent>()
+        val nextAnalysis = CurrentTsCallsSymbolicEngine.UnknownCallEventSinkObserver(
+            sink = null,
+            runtimeLimitationSink = nextAnalysisRecords::add,
+        )
+        nextAnalysis.onRuntimeFeatureLimitation(arrayStorage)
+
+        assertEquals(listOf(arrayStorage), nextAnalysisRecords)
+    }
+
     @Test
     fun `sink converts unknown call events into ordered serializable cell records`() {
         val source = resourcePath("/calls/SourceTargetReplayFixture.ts")

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt

@@ -19,6 +19,7 @@ import kotlin.test.assertFailsWith
 import kotlin.test.assertIs
 import kotlin.test.assertNotNull
 import kotlin.test.assertTrue
+import kotlin.time.Duration
 import kotlin.time.Duration.Companion.seconds
 
 private const val ERROR_CONSTRUCTOR_MODEL_ID: String = "ts.error.constructor"
@@ -94,6 +95,65 @@ class CurrentTsCallsSymbolicEngineTest {
         assertEquals(emptyList(), result.inputs)
     }
 
+    @Test
+    fun `partial array join with fresh string residual does not fail search`() {
+        val fixture = fixture(
+            source = """
+                export function lineWrap(text: string, MAX: number = 15): string[] {
+                  const lines: string[] = []
+
+                  const segments = text.split(' ')
+
+                  const l = segments.length
+
+                  let line_segments: string[] = []
+                  let line_segments_char_count = 0
+
+                  for (let i = 0; i < l; i++) {
+                    const segment = segments[i]
+                    const segment_l = segment.length
+
+                    if (line_segments_char_count + line_segments.length - 1 + segment_l > MAX) {
+                      lines.push(line_segments.join(' '))
+                      line_segments = []
+                      line_segments_char_count = 0
+                    }
+
+                    line_segments.push(segment)
+                    line_segments_char_count += segment_l
+                  }
+
+                  if (line_segments.length > 0) {
+                    lines.push(line_segments.join(' '))
+                  }
+
+                  return lines
+                }
+            """.trimIndent(),
+            exportName = "lineWrap",
+            inputs = listOf(
+                PropertyInput(name = "text", domain = StringDomain(maxLength = 10)),
+                PropertyInput(name = "MAX", domain = NumberDomain()),
+            ),
+            targetStatement = "return lines",
+            targetMode = CallsSourceTargetMode.COMPLETED_RETURN,
+            returnExpression = "lines",
+            sourceFileName = "src/spec/lineWrap.ts",
+        )
+        val unknownCalls = mutableListOf<TsUnknownCallEvent>()
+
+        val result = fixture.search(
+            modelIds = setOf("ts.string.split", "ts.array.join", "ts.array.push"),
+            profile = CallsExperimentProfile.FROZEN_FRESH,
+            unknownCallEventSink = unknownCalls::add,
+            seed = 29,
+            budget = 30.seconds,
+        )
+
+        assertTrue(result.status != CallsSymbolicStatus.TOOL_ERROR, result.toString())
+        assertTrue(unknownCalls.any { it.callee.name == "join" }, "Array.join was not exercised")
+    }
+
     @Test
     fun `fresh array element can be assigned to numeric object field`() {
         val returnExpression = "{ major: parts[0] || 0, minor: parts[1] || 0, patch: parts[2] || 0 }"
@@ -1180,6 +1240,8 @@ class CurrentTsCallsSymbolicEngineTest {
             profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP,
             unknownCallEventSink: ((TsUnknownCallEvent) -> Unit)? = null,
             runtimeLimitationEventSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)? = null,
+            seed: Long = 0,
+            budget: Duration = 10.seconds,
         ): CallsSymbolicSearchResult = engine.search(
             CallsSymbolicSearchRequest(
                 sourceRoot = sourceRoot,
@@ -1189,8 +1251,8 @@ class CurrentTsCallsSymbolicEngineTest {
                 profile = profile,
                 frozenModelIds = modelIds,
                 expectedNativeFrontendRevision = "bundled:test",
-                seed = 0,
-                budget = 10.seconds,
+                seed = seed,
+                budget = budget,
                 unknownCallEventSink = unknownCallEventSink,
                 runtimeLimitationEventSink = runtimeLimitationEventSink,
             )

usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt

@@ -1,26 +1,45 @@
 package org.usvm.api
 
 import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsVoidType
 import org.usvm.UAddressSort
+import org.usvm.UBoolExpr
 import org.usvm.UExpr
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
 import org.usvm.machine.types.mkFakeValue
+import org.usvm.solver.USatResult
+import org.usvm.solver.UUnknownResult
+import org.usvm.solver.UUnsatResult
 
 fun mockMethodCall(
     scope: TsStepScope,
     method: EtsMethodSignature,
     resultType: EtsType = method.returnType,
-) {
-    val result = makeFreshUnknownCallResult(scope, resultType)
+): Boolean {
+    val prepared = prepareFreshUnknownCallResult(scope, resultType)
+    prepared.admissibilityGuard?.let { guard ->
+        val state = scope.calcOnState { this }
+        if (scope.assert(guard) == null) {
+            val constraints = state.pathConstraints.clone()
+            constraints += guard
+
+            when (state.ctx.solver<EtsType>().check(constraints)) {
+                is UUnsatResult -> return false
+                is UUnknownResult -> error("Solver could not decide fresh string type for $method")
+                is USatResult -> error("Fresh string type was satisfiable after its fork failed for $method")
+            }
+        }
+    }
 
     scope.doWithState {
-        setMockMethodCallResult(method, result)
+        setMockMethodCallResult(method, prepared.value)
     }
+    return true
 }
 
 /** Stores a prepared opaque result on this state without applying callee effects or exceptions. */
@@ -31,23 +50,39 @@ internal fun TsState.setMockMethodCallResult(
     methodResult = TsMethodResult.Success.MockedCall(result, method)
 }
 
-/** Creates a fresh opaque result through [scope], keeping solver models consistent with new constraints. */
-internal fun makeFreshUnknownCallResult(
+internal data class PreparedFreshUnknownCallResult(
+    val value: UExpr<*>,
+    val admissibilityGuard: UBoolExpr? = null,
+)
+
+/** Prepares a fresh opaque result; callers must apply [PreparedFreshUnknownCallResult.admissibilityGuard]. */
+internal fun prepareFreshUnknownCallResult(
     scope: TsStepScope,
     resultType: EtsType,
-): UExpr<*> = scope.calcOnState {
-    if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue()
+): PreparedFreshUnknownCallResult {
+    if (resultType is EtsStringType) {
+        // The type guard belongs only to the branch using this result. Asserting it before a
+        // partial model forks could discard satisfiable model successors.
+        val ref = scope.calcOnState { makeSymbolicRefUntyped() }
+        val guard = scope.calcOnState { memory.types.evalTypeEquals(ref, EtsStringType) }
+        return PreparedFreshUnknownCallResult(value = ref, admissibilityGuard = guard)
+    }
+
+    val value = scope.calcOnState {
+        if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue()
 
-    when (val sort = ctx.typeToSort(resultType)) {
-        is UAddressSort -> makeSymbolicRefUntyped()
+        when (val sort = ctx.typeToSort(resultType)) {
+            is UAddressSort -> makeSymbolicRefUntyped()
 
-        is TsUnresolvedSort -> mkFakeValue(
-            scope,
-            boolValue = makeSymbolicPrimitive(ctx.boolSort),
-            fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
-            refValue = makeSymbolicRefUntyped(),
-        )
+            is TsUnresolvedSort -> mkFakeValue(
+                scope,
+                boolValue = makeSymbolicPrimitive(ctx.boolSort),
+                fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
+                refValue = makeSymbolicRefUntyped(),
+            )
 
-        else -> makeSymbolicPrimitive(sort)
+            else -> makeSymbolicPrimitive(sort)
+        }
     }
+    return PreparedFreshUnknownCallResult(value = value)
 }

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -10,6 +10,7 @@ import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsEnumValueType
 import org.jacodb.ets.model.EtsGenericType
+import org.jacodb.ets.model.EtsIntersectionType
 import org.jacodb.ets.model.EtsLexicalEnvType
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
@@ -151,6 +152,16 @@ class TsContext(
         is EtsNullType -> addressSort
         is EtsUndefinedType -> addressSort
         is EtsUnionType -> unresolvedSort
+        is EtsIntersectionType -> {
+            val memberSorts = type.types.map(::typeToSort)
+            val commonSort = memberSorts.firstOrNull()
+
+            if (commonSort != null && memberSorts.all { it == commonSort }) {
+                commonSort
+            } else {
+                unresolvedSort
+            }
+        }
         is EtsRefType -> addressSort
         is EtsLexicalEnvType -> addressSort
         is EtsAnyType -> unresolvedSort

usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt

@@ -91,6 +91,12 @@ data class TsRuntimeFeatureLimitationEvent(
 /** Stable identifiers for bounded runtime features reported by [TsRuntimeFeatureLimitationEvent]. */
 enum class TsRuntimeFeatureLimitationReason {
     ARRAY_ELEMENT_DELETE,
+    CAUGHT_EXCEPTION_VALUE,
+    REGULAR_EXPRESSION_LITERAL,
+    STRING_CONCAT_OPERAND_CONVERSION,
+    ARRAY_STORAGE_TYPE,
+    CONDITIONAL_FIELD_RECEIVER,
+    FAKE_FIELD_RECEIVER_TYPE,
     ARRAY_NAMED_PROPERTY_READ,
     ARRAY_NAMED_PROPERTY_WRITE,
     ARRAY_INDEX_GROWTH,

usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt

@@ -105,7 +105,9 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
             TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED,
             TsUnknownCallFailureReason.LOGGING_CALL,
             -> {
-                mockMethodCall(scope, call.callee)
+                if (!mockMethodCall(scope, call.callee)) {
+                    return TsUnknownCallOutcome.PATH_STOPPED
+                }
                 scope.doWithState { newStmt(call.callSite) }
                 return TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN
             }