From a21909efa73b5eb7c8bd12bdf2e65a15a37fe791 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 16 Oct 2026 00:10:36 +0300 Subject: [PATCH] Compute Date time fields without calendar decomposition --- .../usvm/machine/call/models/DateModels.ts | 26 +++++++++-- .../usvm/machine/call/TsDateEtsIrModelTest.kt | 46 +++++++++++++++++++ .../src/test/resources/models/DateEtsIr.ts | 13 ++++++ .../resources/models/DateModelsComparison.mjs | 13 ++++++ 4 files changed, 93 insertions(+), 5 deletions(-) diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts index 95cf12d404..b932aa2e69 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts @@ -110,7 +110,11 @@ 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 { @@ -118,15 +122,23 @@ export class DateModels { } 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 { @@ -134,7 +146,11 @@ export class DateModels { } 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 { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt index 7a8e8b53a7..2f8530e576 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt +++ b/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) diff --git a/usvm-ts/src/test/resources/models/DateEtsIr.ts b/usvm-ts/src/test/resources/models/DateEtsIr.ts index b69dda3126..ceea90e27b 100644 --- a/usvm-ts/src/test/resources/models/DateEtsIr.ts +++ b/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(); diff --git a/usvm-ts/src/test/resources/models/DateModelsComparison.mjs b/usvm-ts/src/test/resources/models/DateModelsComparison.mjs index 0f11f6fd0e..305c0d5be0 100644 --- a/usvm-ts/src/test/resources/models/DateModelsComparison.mjs +++ b/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],