[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.
@@ -251,7 +251,8 @@ Numeric-result and predicate methods can still use symbolic numeric positions ov
 
 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:
 
@@ -287,6 +288,23 @@ 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.
+
+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 only; string parsing and copying another Date are outside
+  the model domain;
+- 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

@@ -62,6 +62,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

@@ -87,6 +87,7 @@ class TsMachine(
         scene = analysisScene,
         components = components,
         applicationAndSdkClasses = scene.projectAndSdkClasses,
+        dateNowMilliseconds = tsOptions.dateNowMilliseconds,
     )
     private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher(
         models = requireNotNull(resolvedUnknownCallModels),

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

@@ -9,4 +9,20 @@ data class TsOptions(
     val maxArraySize: Int = 1_000,
     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/TsUnknownCall.kt

@@ -141,19 +141,18 @@ internal fun TsUnknownCallDispatcher.dispatch(
         is EtsPtrCallExpr -> 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,