[TS] Correct symbolic value and storage semantics

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

@@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsArrayType
 import org.usvm.UAddressSort
 import org.usvm.UExpr
 import org.usvm.USort
+import org.usvm.isFalse
 import org.usvm.machine.TsSizeSort
 import org.usvm.machine.call.TsUnknownCall
 import org.usvm.machine.call.TsUnknownCallFailureReason
@@ -17,8 +18,8 @@ import org.usvm.machine.state.TsState
 import org.usvm.machine.types.readUnresolvedArrayElement
 import org.usvm.util.arrayStorageType
 import org.usvm.util.copyArrayElements
-import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
+import org.usvm.util.readTypedArrayElement
 
 /** Engine intrinsic for `Array.shift`, whose bulk move is implemented by symbolic-memory `memcpy`. */
 internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel {
@@ -91,15 +92,12 @@ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel {
         index: UExpr<TsSizeSort>,
     ): TsUnknownCallModelCompletion = with(ctx) {
         if (input.elementSort !is TsUnresolvedSort) {
-            val firstElementLValue = mkArrayIndexLValue(
-                sort = input.elementSort,
-                ref = input.array,
-                index = index,
-                type = input.arrayType,
-            )
-            val firstElement = memory.read(firstElementLValue)
-
-            return@with TsUnknownCallModelCompletion.Normal { firstElement }
+            val element = readTypedArrayElement(input.array, index, input.arrayType)
+            return@with if (element.hasBoxedValue.isFalse) {
+                TsUnknownCallModelCompletion.Normal { element.nativeValue }
+            } else {
+                TsUnknownCallModelCompletion.Unresolved(element.unresolvedValue)
+            }
         }
 
         val firstElement = readUnresolvedArrayElement(memory, input.array, index)

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

@@ -209,6 +209,13 @@ private fun unaryMathCall(
     }
     val argument = call.arguments.firstOrNull()?.resolved
         ?: return state.normalExecution(state.ctx.mkFp(Double.NaN, state.ctx.fp64Sort))
+    with(state.ctx) {
+        if (argument.isFakeObject()) {
+            val numberGuard = argument.getFakeType(state.memory).fpTypeExpr
+            val result = operation(argument.extractFp(state.memory))
+            return state.normalExecution(result, guard = numberGuard)
+        }
+    }
     if (argument.sort != state.ctx.fp64Sort) {
         return null
     }
@@ -244,13 +251,19 @@ private fun TsUnknownCall.hasGlobalOwner(expectedName: String): Boolean {
     return hasBuiltinGlobalOwner(owner = owner, callee = callee, expectedName = expectedName)
 }
 
-private fun TsState.normalExecution(result: UExpr<*>): TsUnknownCallModelExecution = with(ctx) {
+private fun TsState.normalExecution(
+    result: UExpr<*>,
+    guard: UBoolExpr = ctx.trueExpr,
+): TsUnknownCallModelExecution = with(ctx) {
     val successor = TsUnknownCallModelSuccessor(
-        guard = trueExpr,
+        guard = guard,
         completion = TsUnknownCallModelCompletion.Normal { result },
     )
 
-    TsUnknownCallModelExecution(successors = listOf(successor))
+    TsUnknownCallModelExecution(
+        successors = listOf(successor),
+        residualGuard = guard.takeUnless { it == trueExpr }?.let(::mkNot),
+    )
 }
 
 private fun TsState.isInteger(value: UExpr<KFp64Sort>) = with(ctx) {

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

@@ -21,6 +21,7 @@ import org.usvm.api.memcpy
 import org.usvm.api.readArrayIndex
 import org.usvm.getIntValue
 import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.isFalse
 import org.usvm.machine.TsSizeSort
 import org.usvm.machine.TsVirtualMethodCallStmt
 import org.usvm.machine.call.TsUnknownCallFailureReason
@@ -43,12 +44,29 @@ import org.usvm.util.arrayStorageType
 import org.usvm.util.copyArrayElements
 import org.usvm.util.forEachArrayPayloadRegion
 import org.usvm.util.initializeArrayKind
-import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
+import org.usvm.util.readTypedArrayElement
 import org.usvm.util.resolveEtsMethods
 
 private val logger = KotlinLogging.logger {}
 
+private val modeledStringMethods = setOf(
+    "substring",
+    "trim",
+    "trimStart",
+    "trimEnd",
+    "charAt",
+    "charCodeAt",
+    "endsWith",
+    "includes",
+    "indexOf",
+    "lastIndexOf",
+    "slice",
+    "startsWith",
+    "toLowerCase",
+    "toUpperCase",
+)
+
 internal fun TsExprResolver.tryApproximateGlobalInstanceCall(
     expr: EtsInstanceCallExpr,
 ): TsExprApproximationResult = with(ctx) {
@@ -168,7 +186,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
 
         // Handle `Array.pop() method calls
         if (expr.callee.name == "pop") {
-            return handleArrayPopCall(stmt, instanceType, elementSort)
+            return handleArrayPopCall(stmt, instanceType)
         }
 
         // Handle `Array.fill() method calls
@@ -183,7 +201,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
 
         // Handle `Array.shift() method calls
         if (expr.callee.name == "shift") {
-            return handleArrayShiftCall(stmt, instanceType, elementSort)
+            return handleArrayShiftCall(stmt, instanceType)
         }
 
         // Handle `Array.join() method calls
@@ -217,18 +235,6 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
         }
     }
 
-    val modeledStringMethods = setOf(
-        "charAt",
-        "charCodeAt",
-        "endsWith",
-        "includes",
-        "indexOf",
-        "lastIndexOf",
-        "slice",
-        "startsWith",
-        "toLowerCase",
-        "toUpperCase",
-    )
     if (instanceType is EtsStringType && expr.callee.name in modeledStringMethods) {
         val dispatcher = unknownCallDispatcher
         if (dispatcher !is TsUnknownCallModelDispatcher) {
@@ -300,11 +306,10 @@ private fun EtsMethodSignature.withEnclosingClassName(name: String): EtsMethodSi
 private fun TsExprResolver.handleArrayPopCall(
     stmt: TsVirtualMethodCallStmt,
     instanceType: EtsArrayType,
-    elementSort: USort,
 ): TsExprApproximationResult {
     val dispatcher = unknownCallDispatcher
     if (dispatcher !is TsUnknownCallModelDispatcher) {
-        return from(handleArrayPop(stmt, instanceType, elementSort, stmt.instance.asExpr(ctx.addressSort)))
+        return from(handleArrayPop(stmt, instanceType, stmt.instance.asExpr(ctx.addressSort)))
     }
 
     dispatcher.dispatch(
@@ -320,11 +325,10 @@ private fun TsExprResolver.handleArrayPopCall(
 private fun TsExprResolver.handleArrayShiftCall(
     stmt: TsVirtualMethodCallStmt,
     instanceType: EtsArrayType,
-    elementSort: USort,
 ): TsExprApproximationResult {
     val dispatcher = unknownCallDispatcher
     if (dispatcher !is TsUnknownCallModelDispatcher) {
-        return from(handleArrayShift(stmt, instanceType, elementSort, stmt.instance.asExpr(ctx.addressSort)))
+        return from(handleArrayShift(stmt, instanceType, stmt.instance.asExpr(ctx.addressSort)))
     }
 
     dispatcher.dispatch(
@@ -546,23 +550,22 @@ private fun TsExprResolver.handleArrayPush(
 private fun TsExprResolver.handleArrayPop(
     stmt: TsVirtualMethodCallStmt,
     arrayType: EtsArrayType,
-    elementSort: USort,
     array: UHeapRef,
 ): UExpr<*>? = with(ctx) {
     check(stmt.args.isEmpty()) {
         "Array.pop() should have no arguments, but got ${stmt.args.size}"
     }
 
-    removeArrayElement(stmt, array, arrayType, elementSort, first = false)
+    removeArrayElement(stmt, array, arrayType, first = false)
 }
 
 private fun TsExprResolver.removeArrayElement(
     stmt: TsVirtualMethodCallStmt,
     array: UHeapRef,
     arrayType: EtsArrayType,
-    elementSort: USort,
     first: Boolean,
 ): UExpr<*>? = with(ctx) {
+    val storageSort = typeToSort(arrayType.elementType)
     val lengthLValue = mkArrayLengthLValue(array, arrayType)
     val length = scope.calcOnState { memory.read(lengthLValue) }
     val nonEmpty = mkNot(mkEq(length, mkBv(0)))
@@ -577,10 +580,15 @@ private fun TsExprResolver.removeArrayElement(
     scope.calcOnState {
         val newLength = mkBvSubExpr(length, mkBv(1))
         val index = if (first) mkBv(0) else newLength
-        val removed = if (typeToSort(arrayType.elementType) is TsUnresolvedSort) {
+        val removed = if (storageSort is TsUnresolvedSort) {
             mkFakeValue(scope, readUnresolvedArrayElement(memory, array, index))
         } else {
-            memory.read(mkArrayIndexLValue(elementSort, array, index, arrayType))
+            val element = readTypedArrayElement(array, index, arrayType)
+            if (element.hasBoxedValue.isFalse) {
+                element.nativeValue
+            } else {
+                mkFakeValue(scope, element.unresolvedValue)
+            }
         }
 
         if (first) {
@@ -742,14 +750,13 @@ private const val ARRAY_FILL_MAX_SIZE = 10_000
 private fun TsExprResolver.handleArrayShift(
     stmt: TsVirtualMethodCallStmt,
     arrayType: EtsArrayType,
-    elementSort: USort,
     array: UHeapRef,
 ): UExpr<*>? = with(ctx) {
     check(stmt.args.isEmpty()) {
         "Array.shift() should have no arguments, but got ${stmt.args.size}"
     }
 
-    removeArrayElement(stmt, array, arrayType, elementSort, first = true)
+    removeArrayElement(stmt, array, arrayType, first = true)
 }
 
 /**