[TS] Model Date construction and calendar operations

usvm-ts/UNKNOWN_CALL_MODELS.md

@@ -48,7 +48,7 @@ This is the only model-selection setting.
 | --- | --- |
 | `TsUnknownCallModelSelection.All` | Enable every built-in model. This is the default. |
 | `TsUnknownCallModelSelection.Only(emptySet())` | Disable every built-in model. |
-| `TsUnknownCallModelSelection.Only(setOf("id", ...))` | Enable exactly the listed built-in model IDs. |
+| `TsUnknownCallModelSelection.Only(setOf("id", ...))` | Enable the listed built-in model IDs and their declared dependencies. |
 
 Unknown IDs are rejected when the machine creates its immutable per-run catalog. The selected models are captured at that
 point, so later mutations of the selection set cannot change an active run.
@@ -261,7 +261,8 @@ limit of 16 code units and uses residual fallback for non-ASCII inputs.
 
 The entry point must be static and have a non-empty body. After its input adapter handles optional arguments or drops
 non-semantic namespace receivers, its parameter count must equal the adapted input count. Unresolved required inputs
-or an arity mismatch make the model not applicable.
+or an arity mismatch make the model not applicable. An `inputAdapter` can resolve inputs directly from the raw call,
+including omitted optional arguments. It returns `null` if a required input cannot be resolved.
 
 The domain guard has three useful outcomes:
 
@@ -297,6 +298,27 @@ Widening a local from `number[]` to `any[]` therefore keeps the same element and
 
 In contrast, `Array.pop` is expressed as the TypeScript body shown above.
 
+### Date experiment boundary
+
+The built-in Date family keeps Gregorian calendar arithmetic, component overflow, leap years, and TimeClip in
+`DateModels.ts`. Kotlin only routes calls, injects the experiment clock, and exposes the model's numeric timestamp
+slot on a Date receiver. This private storage is separate from ordinary JavaScript properties, so deleting a
+user-visible `timestamp` property cannot change the modeled instant.
+
+The current experiment has these explicit limits:
+
+- local getters, setters, and numeric component constructors use UTC, so `getTimezoneOffset()` returns zero and DST
+  behavior is outside the model domain;
+- `Date.now()` and `new Date()` require `TsOptions.dateNowMilliseconds`; one fixed value is reused throughout the
+  analysis, and both calls use fallback when it is absent;
+- one-argument construction supports numeric timestamps, boolean/null/undefined primitive conversion, and copying
+  another modeled Date's internal timestamp; string parsing and arbitrary object coercion remain outside the model
+  domain. Numeric primitive arguments also work through runtime-kind guarded `any` values;
+- missing mandatory setter arguments and explicit `undefined` numeric components produce NaN and invalidate the
+  receiver, while omitted optional components keep their defaults or existing values;
+- symbolic string formatting is not claimed: `toISOString()` is a source implementation for supported concrete
+  execution, while symbolic string conversion remains subject to the engine's string limitations.
+
 Good intrinsic candidates include:
 
 - bulk symbolic-memory copy or fill;

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

@@ -64,6 +64,7 @@ class TsContext(
     val scene: EtsScene,
     components: TsComponents,
     internal val applicationAndSdkClasses: List<EtsClass> = scene.projectAndSdkClasses,
+    internal val dateNowMilliseconds: Double? = null,
 ) : UContext<TsSizeSort>(components) {
     val undefinedSort: TsUndefinedSort by lazy { TsUndefinedSort(this) }
 

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

@@ -90,6 +90,7 @@ class TsMachine(
         components = components,
         // Model bodies are reachable only through their dispatcher and its domain guards.
         applicationAndSdkClasses = scene.projectClasses + runtimeScene.sdkClasses,
+        dateNowMilliseconds = tsOptions.dateNowMilliseconds,
     )
     private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher(
         models = requireNotNull(resolvedUnknownCallModels),

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

@@ -25,4 +25,20 @@ data class TsOptions(
     val inputPropertyPresence: TsInputPropertyPresence = TsInputPropertyPresence.DECLARED_FIELDS,
     val unknownCallModelSelection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All,
     val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH,
-)
+    /** Fixed experiment clock used by `Date.now()` and `new Date()`; `null` leaves those calls unsupported. */
+    val dateNowMilliseconds: Double? = null,
+) {
+    init {
+        val isValidDateNow = dateNowMilliseconds == null ||
+            dateNowMilliseconds.isFinite() &&
+            dateNowMilliseconds % 1.0 == 0.0 &&
+            dateNowMilliseconds in -DATE_TIME_CLIP_BOUND_MILLIS..DATE_TIME_CLIP_BOUND_MILLIS
+        require(isValidDateNow) {
+            "The fixed Date clock must be an integral TimeClip-range millisecond timestamp"
+        }
+    }
+
+    private companion object {
+        const val DATE_TIME_CLIP_BOUND_MILLIS = 8_640_000_000_000_000.0
+    }
+}

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

@@ -6,6 +6,7 @@ import org.jacodb.ets.model.EtsFunctionType
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethodSignature
 import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUnclearRefType
 import org.jacodb.ets.model.EtsUnknownType
@@ -52,3 +53,9 @@ internal fun TsContext.isBuiltinArrayConstructor(value: UExpr<*>): Boolean {
 
     return signature.name == "Array" && signature.file == EtsHierarchy.OBJECT_CLASS.signature.file
 }
+
+internal fun EtsType.isBuiltinDateGlobalType(): Boolean = this is EtsFunctionType &&
+    signature.enclosingClass == EtsClassSignature.UNKNOWN &&
+    signature.name.isEmpty() &&
+    signature.parameters.isEmpty() &&
+    signature.returnType == EtsStringType

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

@@ -192,8 +192,14 @@ fun interface TsEtsIrUnknownCallModelDomainGuard {
 }
 
 private fun TsUnknownCall.resolvedInputs(): List<UExpr<*>>? = buildList {
-    receiver?.let { receiver -> add(receiver.resolved ?: return null) }
-    arguments.forEach { argument -> add(argument.resolved ?: return null) }
+    receiver?.let { receiver ->
+        val value = receiver.resolved ?: return null
+        add(value)
+    }
+    arguments.forEach { argument ->
+        val value = argument.resolved ?: return null
+        add(value)
+    }
 }
 
 private fun findEntryPoint(

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

@@ -149,19 +149,18 @@ internal fun TsUnknownCallDispatcher.dispatch(
         is EtsPtrCallExpr -> call.receiver ?: call.ptr
         else -> null
     }
-    return dispatch(
-        scope,
-        TsUnknownCall(
-            callee = callee,
-            receiver = receiverSource?.let { TsUnknownCallValue(it, resolvedReceiver) },
-            arguments = call.args.zip(resolvedArguments) { source, resolved ->
-                TsUnknownCallValue(source, resolved)
-            },
-            resultType = call.type,
-            callSite = callSite,
-            failureReason = failureReason,
-        ),
+    val unknownCall = TsUnknownCall(
+        callee = callee,
+        receiver = receiverSource?.let { TsUnknownCallValue(it, resolvedReceiver) },
+        arguments = call.args.zip(resolvedArguments) { source, resolved ->
+            TsUnknownCallValue(source, resolved)
+        },
+        resultType = call.type,
+        callSite = callSite,
+        failureReason = failureReason,
     )
+
+    return dispatch(scope, unknownCall)
 }
 
 internal fun TsUnknownCallDispatcher.dispatch(

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

@@ -2,6 +2,7 @@ package org.usvm.machine.call
 
 import org.jacodb.ets.model.EtsFile
 import org.jacodb.ets.model.EtsFileSignature
+import org.usvm.machine.call.intrinsic.TsDateEtsIrModelFamily
 import org.usvm.machine.state.TsState
 import java.util.Collections
 import java.util.IdentityHashMap
@@ -75,12 +76,18 @@ class TsUnknownCallModelCatalog(
     }
 
     fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication {
-        val model = select(call) ?: return TsUnknownCallModelApplication.NotApplicable
+        val directModel = select(call)
+        val modelCall = if (directModel == null) {
+            TsDateEtsIrModelFamily.canonicalModelCall(state, call) ?: call
+        } else {
+            call
+        }
+        val model = directModel ?: select(modelCall) ?: return TsUnknownCallModelApplication.NotApplicable
         if (state.isUnknownCallModelActive(model.id)) {
             return TsUnknownCallModelApplication.NotApplicable
         }
 
-        val execution = model.apply(state, call) ?: return TsUnknownCallModelApplication.NotApplicable
+        val execution = model.apply(state, modelCall) ?: return TsUnknownCallModelApplication.NotApplicable
 
         return TsUnknownCallModelApplication.Applied(
             modelId = model.id,