[TS] Preserve native Date constructor identity

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

@@ -16,7 +16,10 @@ import org.jacodb.ets.model.EtsVoidType
 import org.usvm.UAddressSort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
+import org.usvm.machine.call.TsUnknownCall
 import org.usvm.machine.expr.TsUnresolvedSort
+import org.usvm.machine.expr.dateModelTimestampLValue
+import org.usvm.machine.expr.intrinsicDateConstructorReceiver
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
@@ -46,6 +49,18 @@ internal fun TsState.setMockMethodCallResult(
     methodResult = TsMethodResult.Success.MockedCall(result, method)
 }
 
+/** Native Date construction retains its allocated identity even when its timestamp is opaque. */
+internal fun makeFreshUnknownCallResult(scope: TsStepScope, call: TsUnknownCall): UExpr<*> {
+    val date = scope.calcOnState { intrinsicDateConstructorReceiver(call) }
+    if (date == null) return makeFreshUnknownCallResult(scope, call.resultType)
+
+    scope.doWithState {
+        val timestamp = makeSymbolicPrimitive(ctx.fp64Sort)
+        memory.write(ctx.dateModelTimestampLValue(date), timestamp, guard = ctx.trueExpr)
+    }
+    return date
+}
+
 /** Creates a fresh opaque result through [scope], keeping solver models consistent with new constraints. */
 internal fun makeFreshUnknownCallResult(
     scope: TsStepScope,

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

@@ -14,7 +14,7 @@ import org.usvm.util.EtsHierarchy
 import kotlin.io.path.deleteIfExists
 import kotlin.io.path.inputStream
 
-private val coreRuntimeClassNames = setOf("Object", "Function", "Array")
+private val coreRuntimeClassNames = setOf("Object", "Function", "Array", "Date")
 
 // JacoDB ships the matching TypeScript lib*.d.ts next to its frontend. Single-file conversion supports
 // declarations, while project mode deliberately skips them. Cache the DTO, not mutable scene-owned classes.
@@ -23,8 +23,23 @@ private val coreRuntimeSdk: EtsFileDto by lazy {
     val ir = generateEtsIR(library, loadEntrypoints = false, provider = EtsIrProvider.TS_FRONTEND)
     try {
         val file = ir.inputStream().use { EtsFileDto.loadFromJson(it) }
+        // The ES5 library augments Date in several interface declarations with one identity.
+        val runtimeClasses = file.classes.filter { it.signature.name in coreRuntimeClassNames }
+        val mergedClasses = runtimeClasses.groupBy { it.signature }.values.map { declarations ->
+            val first = declarations.first()
+            // Date supplies nominal identity only. Its APIs retain their existing unknown-call boundary.
+            val methods = if (first.signature.name == "Date") {
+                emptyList()
+            } else {
+                declarations.flatMap { it.methods }.distinctBy { it.signature }
+            }
+            first.copy(
+                fields = declarations.flatMap { it.fields }.distinctBy { it.signature },
+                methods = methods,
+            )
+        }
         file.copy(
-            classes = file.classes.filter { it.signature.name in coreRuntimeClassNames },
+            classes = mergedClasses,
             namespaces = emptyList(),
         )
     } finally {
@@ -38,9 +53,9 @@ internal fun EtsClassType.isCoreRuntimePrototypeIdentity(): Boolean =
         signature.name in setOf("Function", "Array")
 
 /**
- * Load Object, Function and Array from the standard declarations bundled in the pinned JacoDB dependency.
- * Keep their signatures and members and preserve SDK declarations supplied by the caller. Declaration files
- * describe prototypes and APIs; executing an SDK API still requires an interpreter implementation or model.
+ * Load Object, Function, Array and Date from the standard declarations bundled in the pinned JacoDB dependency.
+ * Keep existing Object/Function/Array members and add nominal Date identity. Preserve SDK declarations
+ * supplied by the caller. Date APIs continue through the existing unknown-call and semantic-model boundary.
  */
 internal fun EtsScene.withCoreRuntimeSdk(): EtsScene {
     val missingNames = coreRuntimeClassNames - sdkClasses.map { it.name }.toSet()

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

@@ -3,7 +3,6 @@ package org.usvm.machine.call
 import mu.KotlinLogging
 import org.usvm.UExpr
 import org.usvm.api.makeFreshUnknownCallResult
-import org.usvm.api.mockMethodCall
 import org.usvm.api.setMockMethodCallResult
 import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.call.intrinsic.TsDateEtsIrModelFamily
@@ -75,8 +74,11 @@ class TsModelUnknownCallDispatcher(
             }
 
             TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> {
-                mockMethodCall(scope, call.callee, call.resultType)
-                scope.doWithState { newStmt(call.callSite) }
+                val result = makeFreshUnknownCallResult(scope, call)
+                scope.doWithState {
+                    setMockMethodCallResult(call.callee, result)
+                    newStmt(call.callSite)
+                }
             }
         }
 
@@ -96,7 +98,7 @@ class TsModelUnknownCallDispatcher(
         val freshResidualResult = if (
             residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN
         ) {
-            makeFreshUnknownCallResult(scope, call.resultType)
+            makeFreshUnknownCallResult(scope, call)
         } else {
             null
         }

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

@@ -0,0 +1,78 @@
+package org.usvm.machine.expr
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsInstanceCallExpr
+import org.jacodb.ets.utils.CONSTRUCTOR_NAME
+import org.jacodb.ets.utils.callExpr
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.api.typeStreamOf
+import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.machine.TsContext
+import org.usvm.machine.call.TsUnknownCall
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsState
+import org.usvm.types.singleOrNull
+import org.usvm.util.EtsHierarchy
+import org.usvm.util.mkFieldLValue
+
+internal val intrinsicDateInstanceType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "Date"))
+internal val intrinsicDateConstructorSignature = EtsHierarchy.OBJECT_CLASS.signature.copy(name = "Date")
+
+internal fun TsContext.isIntrinsicDateConstructorProperty(
+    scope: TsStepScope,
+    instance: UHeapRef,
+    name: String,
+): Boolean {
+    if (name != CONSTRUCTOR_NAME || !isAllocatedConcreteHeapRef(instance)) return false
+    val type = scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() }
+    return type == intrinsicDateInstanceType
+}
+
+internal fun TsContext.readIntrinsicDateConstructor(
+    scope: TsStepScope,
+    instance: UHeapRef,
+    name: String,
+): UExpr<*>? {
+    if (!isIntrinsicDateConstructorProperty(scope, instance, name)) return null
+
+    val hasPrototypeMutation = scope.calcOnState { (instance to PROTOTYPE_PROPERTY_NAME) in writtenConcreteFields }
+    if (hasPrototypeMutation) {
+        throw UnsupportedOperationException("Date constructor lookup after prototype mutation is not modeled")
+    }
+
+    val constructor = classConstructorRef(intrinsicDateConstructorSignature)
+    val wasWritten = scope.calcOnState { (instance to name) in writtenConcreteFields }
+    if (!wasWritten) return constructor
+
+    val ownConstructor = mkFieldLValue(addressSort, instance, name)
+    val deleted = deletedFieldLValue(instance, name)
+    return scope.calcOnState {
+        ctx.mkIte(memory.read(deleted), constructor, memory.read(ownConstructor))
+    }
+}
+
+internal fun TsState.intrinsicDateConstructorReceiver(call: TsUnknownCall): UHeapRef? {
+    if (call.callee.name != CONSTRUCTOR_NAME || call.callSite.callExpr !is EtsInstanceCallExpr) return null
+    val resolvedReceiver = call.receiver?.resolved ?: return null
+    if (resolvedReceiver.sort != ctx.addressSort) return null
+
+    val receiver = resolvedReceiver.asExpr(ctx.addressSort)
+    if (!isAllocatedConcreteHeapRef(receiver)) return null
+
+    val type = memory.typeStreamOf(receiver).singleOrNull()
+    return if (type == intrinsicDateInstanceType) receiver else null
+}
+
+/** The intrinsic constructor value is known, but its mutable prototype object is not represented. */
+internal fun TsContext.ensureSupportedDatePrototypeAccess(instance: UHeapRef, name: String) {
+    val constructor = instance as? UConcreteHeapRef ?: return
+    val isDatePrototype = name == "prototype" &&
+        classConstructorSignature(constructor) == intrinsicDateConstructorSignature
+    if (isDatePrototype) {
+        throw UnsupportedOperationException("Date.prototype access is not modeled")
+    }
+}

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

@@ -89,6 +89,7 @@ internal fun TsExprResolver.handleInstanceFieldRef(
     checkUndefinedOrNullPropertyRead(scope, rawInstance, propertyName = value.field.name) ?: return null
     val instance = resolveHeapRef(scope, rawInstance) ?: return null
     if (!ensureSupportedArrayPrototypeAccess(instance, value.field.name)) return null
+    ensureSupportedDatePrototypeAccess(instance, value.field.name)
 
     val iteratorField = readBuiltinIteratorField(instance, value.field.name)
     if (iteratorField != null) return iteratorField
@@ -147,6 +148,9 @@ private fun TsContext.resolveDeclaredField(
     field: EtsFieldSignature,
     hierarchy: EtsHierarchy,
 ): UExpr<*>? {
+    val dateConstructor = readIntrinsicDateConstructor(scope, instance, field.name)
+    if (dateConstructor != null) return dateConstructor
+
     val deleted = scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) }
     if (deleted.isTrue) return mkUndefinedValue()
 
@@ -440,6 +444,7 @@ internal fun TsExprResolver.handleStaticFieldRef(
     if (value.field.name == "prototype") {
         val constructor = classConstructorRef(value.field.enclosingClass)
         if (!ensureSupportedArrayPrototypeAccess(constructor, value.field.name)) return null
+        ensureSupportedDatePrototypeAccess(constructor, value.field.name)
     }
 
     return readStaticField(scope, value.field, hierarchy)

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

@@ -586,6 +586,7 @@ class TsExprResolver(
 
     private fun prototypeFallbackReason(instance: UHeapRef, operand: EtsInstanceFieldRef): String? {
         val name = operand.field.name
+        if (ctx.isIntrinsicDateConstructorProperty(scope, instance, name)) return null
         if (name in OBJECT_PROTOTYPE_PROPERTIES) {
             return "Deleting '$name' requires unsupported Object.prototype lookup"
         }
@@ -1222,7 +1223,12 @@ class TsExprResolver(
     }
 
     private fun runtimeInstanceof(objectType: EtsRefType, checkType: EtsRefType): UBoolExpr = with(ctx) {
-        val objectClass = hierarchy.classesForType(objectType).singleOrNull()
+        val runtimeType = if (objectType == intrinsicDateInstanceType) {
+            EtsClassType(intrinsicDateConstructorSignature)
+        } else {
+            objectType
+        }
+        val objectClass = hierarchy.classesForType(runtimeType).singleOrNull()
             ?: throw UnsupportedOperationException("Unknown instanceof receiver class: $objectType")
         val constructorClass = hierarchy.classesForType(checkType).singleOrNull()
             ?: throw UnsupportedOperationException("Unknown instanceof constructor class: $checkType")
@@ -1573,6 +1579,10 @@ class TsExprResolver(
     private fun constructRuntimeClass(constructorValue: EtsValue): UExpr<out USort>? = with(ctx) {
         val constructorType = resolveRuntimeConstructor(constructorValue, operation = RuntimeConstructorOperation.NEW)
             ?: return@with null
+        if (constructorType.signature == intrinsicDateConstructorSignature) {
+            return@with scope.calcOnState { memory.allocConcrete(intrinsicDateInstanceType) }
+        }
+
         val clazz = scene.projectClasses.singleOrNull { it.signature == constructorType.signature }
             ?: throw UnsupportedOperationException("Unknown new project class: ${constructorType.signature}")
 

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

@@ -111,6 +111,7 @@ internal fun TsExprResolver.handleAssignToInstanceField(
     checkUndefinedOrNullPropertyRead(scope, rawInstance, field.name) ?: return null
     val instance = resolveHeapRef(scope, rawInstance) ?: return null
     if (!ensureSupportedArrayPrototypeAccess(instance, field.name)) return null
+    ensureSupportedDatePrototypeAccess(instance, field.name)
 
     val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) }
     if (storageType == EtsStringType) {

usvm-ts/src/test/kotlin/org/usvm/samples/types/DateConstructorIdentityTest.kt

@@ -0,0 +1,129 @@
+package org.usvm.samples.types
+
+import org.jacodb.ets.model.EtsMethod
+import org.junit.jupiter.api.io.TempDir
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.ValueSource
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTest
+import org.usvm.api.TsTestValue
+import org.usvm.machine.TsAnalysisStopReason
+import org.usvm.machine.TsMachine
+import org.usvm.machine.call.TsResidualCallPolicy
+import org.usvm.machine.call.TsUnknownCallModelSelection
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.assertEquals
+import kotlin.test.assertFalse
+import kotlin.test.assertTrue
+import kotlin.time.Duration.Companion.seconds
+
+class DateConstructorIdentityTest : TsMethodTestRunner() {
+    @TempDir
+    lateinit var directory: Path
+
+    private val sourcePath = "/samples/types/DateConstructorIdentity.ts"
+    override val scene = loadScene(sourcePath)
+    private var modelsEnabled = false
+
+    override val runner: (EtsMethod, UMachineOptions) -> List<TsTest> = { method, options ->
+        val selection = if (modelsEnabled) {
+            TsUnknownCallModelSelection.All
+        } else {
+            TsUnknownCallModelSelection.Only(ids = emptySet())
+        }
+        val selectedOptions = tsOptions.copy(
+            unknownCallModelSelection = selection,
+            unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+        )
+
+        TsMachine(scene = scene, options = options, tsOptions = selectedOptions).use { machine ->
+            val result = machine.analyzeWithMetadata(listOf(method))
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason)
+            assertFalse(result.engineFailed)
+            assertTrue(result.unsupportedPaths.isEmpty(), result.unsupportedPaths.joinToString())
+            result.states.map { state -> TsTestResolver().resolve(method, state) }
+        }
+    }
+
+    @ParameterizedTest
+    @ValueSource(booleans = [false, true])
+    fun `Date has a stable constructor identity and exact instanceof semantics`(withModels: Boolean) {
+        modelsEnabled = withModels
+        options = options.copy(timeout = 5.seconds, stepsFromLastCovered = 200L)
+        val methods = listOf(
+            "direct", "noArguments", "argumentEffects", "stableGlobal", "aliased", "inheritedConstructor", "otherValues",
+            "shadowed",
+        )
+
+        methods.forEach { methodName ->
+            discoverProperties<TsTestValue.TsBoolean>(
+                method = getMethod(methodName = methodName, className = "DateConstructorIdentity"),
+                { result -> result.value },
+                invariants = arrayOf({ result -> result.value }),
+            )
+        }
+
+        replay(methods)
+    }
+
+    @ParameterizedTest
+    @ValueSource(booleans = [false, true])
+    fun `Date constructor properties retain inheritance and own overrides`(withModels: Boolean) {
+        modelsEnabled = withModels
+        options = options.copy(timeout = 5.seconds, stepsFromLastCovered = 200L)
+        val methods = listOf("cloneThroughConstructor", "ownConstructor", "deletedOwnConstructor")
+
+        methods.forEach { methodName ->
+            discoverProperties<TsTestValue.TsBoolean>(
+                method = getMethod(methodName = methodName, className = "DateConstructorIdentity"),
+                { result -> result.value },
+                invariants = arrayOf({ result -> result.value }),
+            )
+        }
+
+        replay(methods)
+    }
+
+    @ParameterizedTest
+    @ValueSource(booleans = [false, true])
+    fun `Date prototype mutation remains explicitly unsupported`(withModels: Boolean) {
+        val selection = if (withModels) {
+            TsUnknownCallModelSelection.All
+        } else {
+            TsUnknownCallModelSelection.Only(ids = emptySet())
+        }
+        val selectedOptions = tsOptions.copy(
+            unknownCallModelSelection = selection,
+            unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+        )
+        val method = getMethod(methodName = "mutatedPrototype", className = "DateConstructorIdentity")
+
+        TsMachine(scene = scene, options = options, tsOptions = selectedOptions).use { machine ->
+            val result = machine.analyzeWithMetadata(listOf(method))
+
+            assertFalse(result.engineFailed)
+            assertTrue(result.states.isEmpty())
+            assertTrue(result.unsupportedPaths.any { it.contains("Date.prototype access is not modeled") })
+        }
+    }
+
+    private fun replay(methodNames: List<String>) {
+        val source = getResourcePath(sourcePath).readText()
+        val assertions = methodNames.joinToString(separator = "\n") { name ->
+            "if (!new DateConstructorIdentity().$name()) throw Error('$name');"
+        }
+
+        assertNodeReplay(
+            source = "$source\n$assertions",
+            directory = directory,
+            name = "date-identity-$modelsEnabled",
+            timeoutMessage = "Date constructor replay timed out",
+        )
+    }
+}