[TS] Propagate failed value materialization through callers

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

@@ -12,7 +12,7 @@ import org.usvm.UHeapRef
 import org.usvm.api.allocateConcreteRef
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.state.TsState
-import org.usvm.machine.types.mkFakeValue
+import org.usvm.machine.types.mkInitialFakeValue
 import org.usvm.ts.pbt.fastcheck.TypeScriptCaptureKind
 import org.usvm.ts.pbt.fastcheck.TypeScriptSourceCapture
 import org.usvm.ts.pbt.mapping.EtsLexicalEnvironmentBinding
@@ -165,9 +165,9 @@ private fun TsState.captureStorageValue(payload: UExpr<*>, type: EtsType): UExpr
     if (declaredSort !is TsUnresolvedSort) return payload
 
     when (payload.sort) {
-        boolSort -> mkFakeValue(scope = null, boolValue = payload.asExpr(boolSort))
-        fp64Sort -> mkFakeValue(scope = null, fpValue = payload.asExpr(fp64Sort))
-        addressSort -> mkFakeValue(scope = null, refValue = payload.asExpr(addressSort))
+        boolSort -> mkInitialFakeValue(boolValue = payload.asExpr(boolSort))
+        fp64Sort -> mkInitialFakeValue(fpValue = payload.asExpr(fp64Sort))
+        addressSort -> mkInitialFakeValue(refValue = payload.asExpr(addressSort))
         else -> error("Unsupported captured payload sort: ${payload.sort}")
     }
 }

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

@@ -14,7 +14,7 @@ import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.state.TsState
 import org.usvm.machine.types.EtsFakeType
 import org.usvm.machine.types.extractValue
-import org.usvm.machine.types.mkFakeValue
+import org.usvm.machine.types.mkInitialFakeValue
 import org.usvm.sizeSort
 import org.usvm.ts.pbt.model.ArrayDomain
 import org.usvm.ts.pbt.model.BooleanDomain
@@ -147,8 +147,7 @@ private fun TsState.materializeCallsOptional(
         fpTypeExpr = numberKind,
         refTypeExpr = referenceKind,
     )
-    val value = mkFakeValue(
-        scope = null,
+    val value = mkInitialFakeValue(
         boolValue = nestedBool.first ?: falseExpr,
         fpValue = nestedNumber.first ?: mkFp64(0.0),
         refValue = reference,

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

@@ -4,6 +4,7 @@ import org.junit.jupiter.api.io.TempDir
 import org.usvm.SolverType
 import org.usvm.ts.pbt.model.ArrayDomain
 import org.usvm.ts.pbt.model.BooleanDomain
+import org.usvm.ts.pbt.model.ConstantDomain
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.NumberDomain
@@ -219,28 +220,41 @@ class CallsClassDataRegistryOracleTest {
             constructorInputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)),
         )
 
-        val result = CurrentTsCallsClassCoverageEngine().search(
-            CallsClassSearchRequest(
-                harness = harness,
-                profile = CallsExperimentProfile.EMPTY_STOP,
-                frozenModelIds = emptySet(),
-                expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision,
-                seed = 1,
-                budget = 3.seconds,
-                timeQuantum = 100.milliseconds,
-                solverQueryLimit = 1.seconds,
-                solverType = SolverType.YICES,
-                candidateCap = 20,
-                requireEntryPointWitness = true,
-            ),
-        )
+        // Coverage-directed search need not enumerate every input model for each entry point.
+        val branchInputs = listOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false))
+        val candidates = branchInputs.flatMap { flag ->
+            val inputs = listOf(PropertyInput(name = "flag", domain = ConstantDomain(flag)))
+            val branchHarness = harness.copy(
+                surface = harness.surface.copy(constructorInputs = inputs),
+                functions = harness.functions.map { it.copy(inputs = inputs) },
+            )
+            val result = CurrentTsCallsClassCoverageEngine().search(
+                CallsClassSearchRequest(
+                    harness = branchHarness,
+                    profile = CallsExperimentProfile.EMPTY_STOP,
+                    frozenModelIds = emptySet(),
+                    expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision,
+                    seed = 1,
+                    budget = 3.seconds,
+                    timeQuantum = 100.milliseconds,
+                    solverQueryLimit = 1.seconds,
+                    solverType = SolverType.YICES,
+                    candidateCap = 20,
+                    requireEntryPointWitness = true,
+                ),
+            )
+
+            val scenarioIds = result.search.candidates.map { it.entryPointId }.toSet()
+            assertEquals(harness.scenarios.map { it.id }.toSet(), scenarioIds, "flag=$flag")
+            result.search.candidates.forEach { assertEquals(listOf(flag), it.inputs) }
+            result.search.candidates
+        }
 
         val constructorScenarioId = harness.scenarios.first().id
-        val constructorBranches = result.search.candidates.filter { it.entryPointId == constructorScenarioId }
+        val constructorBranches = candidates.filter { it.entryPointId == constructorScenarioId }
             .map { it.inputs.single() }.toSet()
         assertEquals(setOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)), constructorBranches)
-        assertEquals(harness.scenarios.map { it.id }.toSet(), result.search.candidates.map { it.entryPointId }.toSet())
-        for (candidate in result.search.candidates) {
+        for (candidate in candidates) {
             val index = harness.scenarios.indexOfFirst { it.id == candidate.entryPointId }
             val original = OriginalTypeScriptClassReplayer(
                 directory,

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt

@@ -19,7 +19,7 @@ import org.usvm.api.initializeArrayLength
 import org.usvm.api.makeSymbolicPrimitive
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.state.TsState
-import org.usvm.machine.types.mkFakeValue
+import org.usvm.machine.types.mkInitialFakeValue
 import org.usvm.sizeSort
 import org.usvm.ts.pbt.backend.ProjectionLevel
 import org.usvm.ts.pbt.mapping.EtsInputBinding
@@ -236,8 +236,7 @@ class UsvmDomainProjector(
                 return@with sameSortIte(chooseValue, nestedValue, nilValue)
             }
 
-            val fakeValue = state.mkFakeValue(
-                scope = null,
+            val fakeValue = state.mkInitialFakeValue(
                 boolValue = nestedValue.asOptionalBool(),
                 fpValue = nestedValue.asOptionalFp(),
                 refValue = (nestedValue.asOptionalRef() ?: nilValue.asOptionalRef()),
@@ -371,8 +370,7 @@ class UsvmDomainProjector(
         private fun box(value: UExpr<out USort>): UConcreteHeapRef = with(state.ctx) {
             if (value is UConcreteHeapRef && value.isFakeObject()) return@with value
 
-            state.mkFakeValue(
-                scope = null,
+            state.mkInitialFakeValue(
                 boolValue = value.asOptionalBool(),
                 fpValue = value.asOptionalFp(),
                 refValue = value.asOptionalRef(),

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

@@ -34,7 +34,7 @@ fun mockMethodCall(
     method: EtsMethodSignature,
     resultType: EtsType = method.returnType,
 ) {
-    val result = makeFreshUnknownCallResult(scope, resultType)
+    val result = makeFreshUnknownCallResult(scope, resultType) ?: return
 
     scope.doWithState {
         setMockMethodCallResult(method, result)
@@ -50,7 +50,7 @@ internal fun TsState.setMockMethodCallResult(
 }
 
 /** Native Date construction retains its allocated identity even when its timestamp is opaque. */
-internal fun makeFreshUnknownCallResult(scope: TsStepScope, call: TsUnknownCall): UExpr<*> {
+internal fun makeFreshUnknownCallResult(scope: TsStepScope, call: TsUnknownCall): UExpr<*>? {
     val date = scope.calcOnState { intrinsicDateConstructorReceiver(call) }
     if (date == null) return makeFreshUnknownCallResult(scope, call.resultType)
 
@@ -65,7 +65,7 @@ internal fun makeFreshUnknownCallResult(scope: TsStepScope, call: TsUnknownCall)
 internal fun makeFreshUnknownCallResult(
     scope: TsStepScope,
     resultType: EtsType,
-): UExpr<*> = scope.calcOnState {
+): UExpr<*>? = scope.calcOnState {
     if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue()
     val literal = makeLiteralResult(resultType)
     if (literal != null) return@calcOnState literal
@@ -120,7 +120,7 @@ private fun TsState.makeLiteralResult(type: EtsType): UExpr<*>? = when (type) {
     else -> null
 }
 
-private fun TsState.makeFiniteLiteralUnion(scope: TsStepScope, variants: List<EtsType>): UExpr<*> {
+private fun TsState.makeFiniteLiteralUnion(scope: TsStepScope, variants: List<EtsType>): UExpr<*>? {
     var result = requireNotNull(makeLiteralResult(variants.first()))
     for (variant in variants.drop(1)) {
         val selected = makeSymbolicPrimitive(ctx.boolSort)
@@ -130,7 +130,7 @@ private fun TsState.makeFiniteLiteralUnion(scope: TsStepScope, variants: List<Et
             condition = selected,
             trueBranchValue = value,
             falseBranchValue = result,
-        )
+        ) ?: return null
     }
 
     return result

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

@@ -265,7 +265,7 @@ class TsContext(
         else -> false
     }
 
-    fun UExpr<*>.toFakeObject(scope: TsStepScope): UConcreteHeapRef {
+    fun UExpr<*>.toFakeObject(scope: TsStepScope): UConcreteHeapRef? {
         if (isFakeObject()) {
             return this
         }

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

@@ -74,7 +74,7 @@ class TsModelUnknownCallDispatcher(
             }
 
             TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> {
-                val result = makeFreshUnknownCallResult(scope, call)
+                val result = makeFreshUnknownCallResult(scope, call) ?: return TsUnknownCallOutcome.PATH_STOPPED
                 scope.doWithState {
                     setMockMethodCallResult(call.callee, result)
                     newStmt(call.callSite)
@@ -98,7 +98,7 @@ class TsModelUnknownCallDispatcher(
         val freshResidualResult = if (
             residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN
         ) {
-            makeFreshUnknownCallResult(scope, call)
+            makeFreshUnknownCallResult(scope, call) ?: return TsUnknownCallOutcome.PATH_STOPPED
         } else {
             null
         }
@@ -117,9 +117,10 @@ class TsModelUnknownCallDispatcher(
             val completion = successor.completion as? TsUnknownCallModelCompletion.Unresolved
                 ?: return@map null
 
-            scope.calcOnState {
+            val result = scope.calcOnState {
                 mkFakeValue(scope = scope, value = completion.value)
-            }
+            } ?: return TsUnknownCallOutcome.PATH_STOPPED
+            result
         }
         val guardedStateChanges = application.execution.successors.mapIndexed { index, successor ->
             successor.guard to modelStateChange(

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt

@@ -135,13 +135,13 @@ private fun TsExprResolver.advanceArrayIterator(
     val value = if (done.isTrue) {
         mkUndefinedValue()
     } else {
-        val element = readArrayElement(scope, iterator.array, iterator.index, iterator.arrayType)
+        val element = readArrayElement(scope, iterator.array, iterator.index, iterator.arrayType) ?: return null
         iteWriteIntoFakeObject(
             scope = scope,
             condition = done,
             trueBranchValue = mkUndefinedValue(),
             falseBranchValue = element,
-        )
+        ) ?: return null
     }
 
     scope.calcOnState {

usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt

@@ -668,7 +668,7 @@ private fun TsExprResolver.removeArrayElement(
     scope.calcOnState {
         val newLength = mkBvSubExpr(length, mkBv(1))
         val index = if (first) mkBv(0) else newLength
-        val removed = readArrayElement(scope, array, index, arrayType)
+        val removed = readArrayElement(scope, array, index, arrayType) ?: return@calcOnState null
 
         if (first) {
             copyArrayElements(
@@ -730,10 +730,14 @@ private fun TsExprResolver.handleArrayFill(
     val containsFakeValue = resolvedValue.sort == addressSort &&
         resolvedValue.asExpr(addressSort).hasFakeValueBranch()
     val usesBoxedValue = hasResolvedElementSort && (!valueMatchesElementSort || containsFakeValue)
-    val boxedValue = if (usesBoxedValue) boxArrayValue(scope, resolvedValue) else null
+    val boxedValue = if (usesBoxedValue) {
+        boxArrayValue(scope, resolvedValue) ?: return null
+    } else {
+        null
+    }
 
     val nativeValue = when {
-        !hasResolvedElementSort -> resolvedValue.toFakeObject(scope)
+        !hasResolvedElementSort -> resolvedValue.toFakeObject(scope) ?: return null
         !usesBoxedValue -> resolvedValue
         elementSort == boolSort -> falseExpr
         elementSort == fp64Sort -> mkFp64(0.0)

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt

@@ -112,9 +112,9 @@ internal fun TsContext.writeModeledErrorField(
     instance: UHeapRef,
     field: EtsFieldSignature,
     value: UExpr<*>,
-): Boolean {
+): Boolean? {
     val storageField = resolveErrorStorageField(scope, instance, field) ?: return false
-    val payload = boxArrayValue(scope, value)
+    val payload = boxArrayValue(scope, value) ?: return null
 
     scope.doWithState {
         memory.write(

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt

@@ -127,7 +127,7 @@ private fun TsContext.readArrayProperty(
         return mkUndefinedValue()
     }
 
-    val element = readArrayElement(scope, array, index, arrayType)
+    val element = readArrayElement(scope, array, index, arrayType) ?: return null
     if (elementExists.isTrue) {
         return element
     }
@@ -145,11 +145,11 @@ internal fun TsContext.readArrayElement(
     array: UHeapRef,
     index: UExpr<TsSizeSort>,
     arrayType: EtsArrayType,
-): UExpr<*> {
+): UExpr<*>? {
     val present = scope.calcOnState { knownArrayIndexPresence(array, index) }
     if (present?.isFalse == true) return mkUndefinedValue()
 
-    val element = readArrayElementPayload(scope, array, index, arrayType)
+    val element = readArrayElementPayload(scope, array, index, arrayType) ?: return null
     if (present == null || present.isTrue) return element
 
     return iteWriteIntoFakeObject(
@@ -165,7 +165,7 @@ private fun TsContext.readArrayElementPayload(
     array: UHeapRef,
     index: UExpr<TsSizeSort>,
     arrayType: EtsArrayType,
-): UExpr<*> {
+): UExpr<*>? {
     // Determine the element sort.
     val sort = typeToSort(arrayType.componentType)
 
@@ -183,7 +183,7 @@ private fun TsContext.readArrayElementPayload(
 
     return scope.calcOnState {
         val value = readUnresolvedArrayElement(memory, array, index)
-        val fakeObj = mkFakeValue(scope = scope, value = value)
+        val fakeObj = mkFakeValue(scope = scope, value = value) ?: return@calcOnState null
         if (fakeObj != value.refValue) {
             val refLValue = mkArrayIndexLValue(addressSort, array, index, arrayType)
             memory.write(refLValue, fakeObj, guard = trueExpr)

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt

@@ -191,12 +191,12 @@ private fun TsContext.resolveDeclaredField(
         scope.assert(fieldExists) ?: return null
     }
 
-    val storedValue = readField(scope, instance, field, storageSort)
+    val storedValue = readField(scope, instance, field, storageSort) ?: return null
     val value = materializeFieldValue(scope, storedValue, storageSort, declaredType) ?: return null
     return applyFieldDeletion(scope, deleted, value)
 }
 
-private fun TsContext.applyFieldDeletion(scope: TsStepScope, deleted: UBoolExpr, value: UExpr<*>): UExpr<*> {
+private fun TsContext.applyFieldDeletion(scope: TsStepScope, deleted: UBoolExpr, value: UExpr<*>): UExpr<*>? {
     if (deleted.isFalse) return value
 
     // Conditional deletion yields undefined on the deleted branch, while preserving the stored runtime kind.
@@ -349,7 +349,7 @@ private fun TsContext.readField(
     instance: UHeapRef,
     field: EtsFieldSignature,
     sort: USort,
-): UExpr<*> {
+): UExpr<*>? {
     if (sort !is TsUnresolvedSort) {
         val lValue = mkFieldLValue(sort, instance, field.name)
         return scope.calcOnState { memory.read(lValue) }
@@ -370,7 +370,7 @@ private fun TsContext.readField(
         if (ref.hasFakeValueBranch()) {
             boxRuntimeValue(scope = scope, value = ref)
         } else {
-            val fakeObj = mkFakeValue(scope, bool, fp, ref)
+            val fakeObj = mkFakeValue(scope, bool, fp, ref) ?: return@calcOnState null
             lValuesToAllocatedFakeObjects += refLValue to fakeObj
             memory.write(refLValue, fakeObj, guard = trueExpr)
             fakeObj

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

@@ -1376,7 +1376,7 @@ class TsExprResolver(
                             "Promise settlement callback should have exactly one argument, but got ${expr.args.size}"
                         }
                         val value = resolve(expr.args.single()) ?: return null
-                        val fakeValue = value.toFakeObject(scope)
+                        val fakeValue = value.toFakeObject(scope) ?: return null
                         scope.doWithState {
                             if (!isResolved(callback.promise)) {
                                 markResolved(callback.promise)

usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt

@@ -196,7 +196,7 @@ fun TsContext.assignToArrayIndex(
             }
         }
 
-        val fake = boxArrayValue(scope, expr)
+        val fake = boxArrayValue(scope, expr) ?: return null
         val kind = fake.getFakeType(scope)
         val compatibleKind = when (elementSort) {
             boolSort -> kind.boolTypeExpr
@@ -231,7 +231,7 @@ fun TsContext.assignToArrayIndex(
         index = index.asExpr(sizeSort),
         type = arrayType,
     )
-    val fakeExpr = boxArrayValue(scope, expr)
+    val fakeExpr = boxArrayValue(scope, expr) ?: return null
     return scope.doWithState {
         memory.write(lValue, fakeExpr, guard = trueExpr)
     }