[TS] Compute Date time fields without calendar decomposition

usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts

@@ -110,31 +110,47 @@ export class DateModels {
     }
 
     static getDay(receiver: DateValue): number {
-        return DateModels.parts(receiver.timestamp).day;
+        const timestamp = receiver.timestamp;
+        if (DateModels.isInvalid(timestamp)) return NaN;
+
+        const days = DateModels.floorDiv(timestamp, DateModels.MS_PER_DAY);
+        return DateModels.mod(days + 4, 7);
     }
 
     static getFullYear(receiver: DateValue): number {
         return DateModels.parts(receiver.timestamp).year;
     }
 
     static getHours(receiver: DateValue): number {
-        return DateModels.parts(receiver.timestamp).hours;
+        const timestamp = receiver.timestamp;
+        if (DateModels.isInvalid(timestamp)) return NaN;
+
+        const withinDay = DateModels.mod(timestamp, DateModels.MS_PER_DAY);
+        return DateModels.floorDiv(withinDay, DateModels.MS_PER_HOUR);
     }
 
     static getMilliseconds(receiver: DateValue): number {
-        return DateModels.parts(receiver.timestamp).milliseconds;
+        return DateModels.mod(receiver.timestamp, DateModels.MS_PER_SECOND);
     }
 
     static getMinutes(receiver: DateValue): number {
-        return DateModels.parts(receiver.timestamp).minutes;
+        const timestamp = receiver.timestamp;
+        if (DateModels.isInvalid(timestamp)) return NaN;
+
+        const withinHour = DateModels.mod(timestamp, DateModels.MS_PER_HOUR);
+        return DateModels.floorDiv(withinHour, DateModels.MS_PER_MINUTE);
     }
 
     static getMonth(receiver: DateValue): number {
         return DateModels.parts(receiver.timestamp).month;
     }
 
     static getSeconds(receiver: DateValue): number {
-        return DateModels.parts(receiver.timestamp).seconds;
+        const timestamp = receiver.timestamp;
+        if (DateModels.isInvalid(timestamp)) return NaN;
+
+        const withinMinute = DateModels.mod(timestamp, DateModels.MS_PER_MINUTE);
+        return DateModels.floorDiv(withinMinute, DateModels.MS_PER_SECOND);
     }
 
     static getTime(receiver: DateValue): number {

usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt

@@ -2,6 +2,7 @@ package org.usvm.machine.call
 
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.callExpr
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
@@ -14,6 +15,7 @@ import org.usvm.api.TsTestValue
 import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
+import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.util.TsTestResolver
 import org.usvm.util.assertNodeReplay
 import org.usvm.util.getResourcePath
@@ -216,6 +218,50 @@ class TsDateEtsIrModelTest {
         assertNaN(methodName = "invalidTimezoneOffset")
     }
 
+    @Test
+    fun `time getters preserve negative clipped boundaries invalid dates and positive zero`() {
+        val expectedValues = mapOf(
+            "timeFieldsBeforeEpoch" to 345_599_999.0,
+            "timeFieldsEpoch" to 345_600_000.0,
+            "timeFieldsMinimum" to 172_800_000.0,
+            "timeFieldsMaximum" to 518_400_000.0,
+            "timeFieldsFraction" to 345_540_000.0,
+        )
+
+        for ((name, expected) in expectedValues) {
+            assertNumber(methodName = name, expected = expected)
+        }
+        assertNaN(methodName = "timeFieldsInvalid")
+
+        replayDateArguments(
+            assertions = expectedValues.map { (name, expected) -> "Object.is(example.$name(), $expected)" } +
+                "Number.isNaN(example.timeFieldsInvalid())",
+        )
+    }
+
+    @Test
+    fun `time getters avoid calendar decomposition`() {
+        var calendarSteps = 0
+        var totalSteps = 0
+        val observer = object : TsInterpreterObserver {
+            override fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) {
+                totalSteps++
+                val methodName = stmt.location.method.name
+                if (methodName == "parts" || methodName == "civilFromDays") calendarSteps++
+            }
+        }
+
+        val states = TsMachine(
+            scene = scene,
+            options = machineOptions,
+            tsOptions = TsOptions(),
+            observer = observer,
+        ).use { machine -> machine.analyze(listOf(method("timeFieldsBeforeEpoch"))) }
+
+        assertEquals(expected = 1, actual = states.size)
+        assertEquals(expected = 0, actual = calendarSteps, message = "Executed $totalSteps instructions")
+    }
+
     @Test
     fun `Date truncates fractional timestamps and components toward zero`() {
         assertNumber(methodName = "fractionalTimestamps", expected = 9.0)

usvm-ts/src/test/resources/models/DateEtsIr.ts

@@ -212,6 +212,19 @@ export class DateEtsIr {
         return copy.getTime();
     }
 
+    private timeFields(timestamp: number): number {
+        const date = new Date(timestamp);
+        return date.getUTCDay() * 86_400_000 + date.getUTCHours() * 3_600_000 +
+            date.getUTCMinutes() * 60_000 + date.getUTCSeconds() * 1_000 + date.getUTCMilliseconds();
+    }
+
+    timeFieldsBeforeEpoch(): number { return this.timeFields(-1); }
+    timeFieldsEpoch(): number { return this.timeFields(-0); }
+    timeFieldsMinimum(): number { return this.timeFields(-8_640_000_000_000_000); }
+    timeFieldsMaximum(): number { return this.timeFields(8_640_000_000_000_000); }
+    timeFieldsFraction(): number { return this.timeFields(-60_000.9); }
+    timeFieldsInvalid(): number { return this.timeFields(NaN); }
+
     foreignReceiverThroughAny(): number {
         const impostor: any = new DateImpostor();
         return impostor.getTime();

usvm-ts/src/test/resources/models/DateModelsComparison.mjs

@@ -34,6 +34,19 @@ const timestamps = [
     NaN,
 ];
 
+// Sample the complete clipped timestamp range and both sides of unit boundaries.
+let sampleSeed = 0x319621;
+for (let index = 0; index < 10_000; index++) {
+    sampleSeed = (Math.imul(sampleSeed, 1664525) + 1013904223) >>> 0;
+    timestamps.push(Math.trunc((sampleSeed / 0x1_0000_0000 * 2 - 1) * 8_640_000_000_000_000));
+}
+for (const period of [1_000, 60_000, 3_600_000, 86_400_000]) {
+    for (const multiple of [-10_000_000, -1, 0, 1, 10_000_000]) {
+        for (const offset of [-1, -0.1, 0, 0.1, 1]) timestamps.push(multiple * period + offset);
+    }
+}
+timestamps.push(Infinity, -Infinity);
+
 const getters = [
     ["getDate", (date) => date.getUTCDate(), DateModels.getDate],
     ["getDay", (date) => date.getUTCDay(), DateModels.getDay],