From 5ef7830e23265a3a2f851ecb77b884dbf3fdb465 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 8 Oct 2026 00:47:02 +0300 Subject: [PATCH 01/10] Model Date calls with verified owner and receiver identity --- usvm-ts/UNKNOWN_CALL_MODELS.md | 22 +- .../main/kotlin/org/usvm/machine/TsContext.kt | 1 + .../main/kotlin/org/usvm/machine/TsMachine.kt | 2 + .../main/kotlin/org/usvm/machine/TsOptions.kt | 18 +- .../org/usvm/machine/call/TsUnknownCall.kt | 23 +- .../machine/call/TsUnknownCallModelCatalog.kt | 11 +- .../call/intrinsic/TsDateEtsIrModelFamily.kt | 424 +++++++++++++ .../usvm/machine/expr/CallApproximations.kt | 8 +- .../kotlin/org/usvm/machine/expr/ReadField.kt | 6 +- .../org/usvm/machine/expr/WriteField.kt | 6 +- .../usvm/machine/call/models/DateModels.ts | 559 ++++++++++++++++++ .../usvm/machine/call/TsDateEtsIrModelTest.kt | 228 +++++++ .../machine/call/TsDateModelsArtifactTest.kt | 32 + .../TsEtsIrUnknownCallModelExecutionTest.kt | 23 + .../call/TsUnknownCallModelCatalogTest.kt | 7 +- .../src/test/resources/models/DateEtsIr.ts | 94 +++ .../resources/models/DateModelsComparison.mjs | 130 ++++ .../test/resources/models/DateShadowEtsIr.ts | 10 + .../models/EtsIrSemanticModelCalls.ts | 4 + 19 files changed, 1586 insertions(+), 22 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt create mode 100644 usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateModelsArtifactTest.kt create mode 100644 usvm-ts/src/test/resources/models/DateEtsIr.ts create mode 100644 usvm-ts/src/test/resources/models/DateModelsComparison.mjs create mode 100644 usvm-ts/src/test/resources/models/DateShadowEtsIr.ts diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 46c204fb8a..28f85fdb65 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/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,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; diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 31afa99738..8d64a927a5 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/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 = scene.projectAndSdkClasses, + internal val dateNowMilliseconds: Double? = null, ) : UContext(components) { val undefinedSort: TsUndefinedSort by lazy { TsUndefinedSort(this) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 405ce95895..617691f4c8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -90,6 +90,8 @@ 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), diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index 52188fafad..43223856ff 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/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 + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt index ee9c4d4a16..650ef9599a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt +++ b/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( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt index c55afe0251..a3cb6ddb40 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt +++ b/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, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt new file mode 100644 index 0000000000..5040590247 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt @@ -0,0 +1,424 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsValue +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.usvm.UExpr +import org.usvm.api.typeStreamOf +import org.usvm.machine.call.TsEtsIrUnknownCallModel +import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact +import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard +import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallModel +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +import org.usvm.machine.state.TsState +import org.usvm.types.singleOrNull + +/** Numeric `Date` API family implemented by an ordinary TypeScript source body. */ +internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { + private const val DATE_CLASS = "Date" + private const val MAX_CONSTRUCTOR_ARGUMENTS = 7 + private const val RESOURCE = "/org/usvm/machine/call/models/DateModels.ts" + private val builtinDateSignature = EtsClassSignature.UNKNOWN.copy(name = DATE_CLASS) + private val builtinDateType = EtsClassType(signature = builtinDateSignature) + private val getterNames = listOf( + "getDate", + "getDay", + "getFullYear", + "getHours", + "getMilliseconds", + "getMinutes", + "getMonth", + "getSeconds", + "getTime", + "getTimezoneOffset", + "getUTCDate", + "getUTCDay", + "getUTCFullYear", + "getUTCHours", + "getUTCMilliseconds", + "getUTCMinutes", + "getUTCMonth", + "getUTCSeconds", + "toISOString", + "valueOf", + ) + + /** Normalize only model lookup; residual calls and observation retain the frontend signature. */ + internal fun canonicalModelCall(state: TsState, call: TsUnknownCall): TsUnknownCall? { + if (call.callee.enclosingClass.name == DATE_CLASS) return null + + val receiverValue = call.receiver ?: return null + if (!isDateReceiver(state, receiverValue.source, receiverValue.resolved)) return null + + return call.copy(callee = call.callee.copy(enclosingClass = builtinDateSignature)) + } + + internal fun isDateReceiver(state: TsState, source: EtsValue, receiver: UExpr<*>?): Boolean { + val sourceLooksDate = (source as? EtsLocal)?.name == DATE_CLASS || when (val type = source.type) { + is EtsClassType -> type.signature.name == DATE_CLASS + is EtsUnclearRefType -> type.typeName == DATE_CLASS + else -> false + } + if (sourceLooksDate) return true + if (receiver?.sort != state.ctx.addressSort) return false + + val runtimeType = state.memory.typeStreamOf(receiver.asExpr(state.ctx.addressSort)).singleOrNull() + return (runtimeType as? EtsClassType)?.signature?.name == DATE_CLASS + } + + private val artifact by lazy { + loadBundledEtsIrUnknownCallModelArtifact( + resourceName = RESOURCE, + sourceFileName = "DateModels.ts", + entryPointClassName = "DateModels", + entryPointMethodName = "construct", + ) + } + + override val models: List by lazy { + buildList { + add(constructorModel()) + add(utcModel()) + add(nowModel()) + + for (methodName in getterNames) { + add(instanceModel(idSuffix = methodName, methodName = methodName, consumedArgs = 0)) + } + + add(instanceModel(idSuffix = "set-date", methodName = "setDate", consumedArgs = 1)) + add( + instanceArityModel( + idSuffix = "set-full-year", + methodName = "setFullYear", + entryPointName = "setFullYear", + minArgs = 1, + maxArgs = 3, + ) + ) + add( + instanceArityModel( + idSuffix = "set-hours", + methodName = "setHours", + entryPointName = "setHours", + minArgs = 1, + maxArgs = 4, + ) + ) + add( + instanceModel( + idSuffix = "set-milliseconds", + methodName = "setMilliseconds", + consumedArgs = 1, + ) + ) + add( + instanceArityModel( + idSuffix = "set-minutes", + methodName = "setMinutes", + entryPointName = "setMinutes", + minArgs = 1, + maxArgs = 3, + ) + ) + add( + instanceArityModel( + idSuffix = "set-month", + methodName = "setMonth", + entryPointName = "setMonth", + minArgs = 1, + maxArgs = 2, + ) + ) + add( + instanceArityModel( + idSuffix = "set-seconds", + methodName = "setSeconds", + entryPointName = "setSeconds", + minArgs = 1, + maxArgs = 2, + ) + ) + add(instanceModel(idSuffix = "set-time", methodName = "setTime", consumedArgs = 1)) + add(instanceModel(idSuffix = "set-utc-date", methodName = "setUTCDate", consumedArgs = 1)) + add( + instanceArityModel( + idSuffix = "set-utc-full-year", + methodName = "setUTCFullYear", + entryPointName = "setUTCFullYear", + minArgs = 1, + maxArgs = 3, + ) + ) + add( + instanceArityModel( + idSuffix = "set-utc-hours", + methodName = "setUTCHours", + entryPointName = "setUTCHours", + minArgs = 1, + maxArgs = 4, + ) + ) + add( + instanceModel( + idSuffix = "set-utc-milliseconds", + methodName = "setUTCMilliseconds", + consumedArgs = 1, + ) + ) + add( + instanceArityModel( + idSuffix = "set-utc-minutes", + methodName = "setUTCMinutes", + entryPointName = "setUTCMinutes", + minArgs = 1, + maxArgs = 3, + ) + ) + add( + instanceArityModel( + idSuffix = "set-utc-month", + methodName = "setUTCMonth", + entryPointName = "setUTCMonth", + minArgs = 1, + maxArgs = 2, + ) + ) + add( + instanceArityModel( + idSuffix = "set-utc-seconds", + methodName = "setUTCSeconds", + entryPointName = "setUTCSeconds", + minArgs = 1, + maxArgs = 2, + ) + ) + } + } + + private fun constructorModel(): TsUnknownCallModel = model( + idSuffix = "constructor", + methodName = CONSTRUCTOR_NAME, + entryPointName = "construct", + domainGuard = instanceGuard(minArgs = 0, numericArgs = MAX_CONSTRUCTOR_ARGUMENTS), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + with(state.ctx) { + val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + val nowMilliseconds = dateNowMilliseconds + if (call.arguments.isEmpty() && nowMilliseconds == null) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + val arguments = call.resolvedArguments(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS)?.toMutableList() + ?: return@TsEtsIrUnknownCallModelInputAdapter null + while (arguments.size < MAX_CONSTRUCTOR_ARGUMENTS) { + arguments += mkFp64(0.0) + } + val providedArgumentCount = mkFp64(call.arguments.size.toDouble()) + val fallbackClock = mkFp64(nowMilliseconds ?: 0.0) + + buildList { + add(receiver) + add(providedArgumentCount) + add(fallbackClock) + addAll(arguments) + } + } + }, + ) + + private fun nowModel(): TsUnknownCallModel = model( + idSuffix = "now", + methodName = "now", + entryPointName = "now", + domainGuard = numericGuard(minArgs = 0, numericArgs = 0), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, _ -> + with(state.ctx) { + listOf(mkFp64(dateNowMilliseconds ?: return@TsEtsIrUnknownCallModelInputAdapter null)) + } + }, + ) + + private fun utcModel(): TsUnknownCallModel = model( + idSuffix = "utc", + methodName = "UTC", + entryPointName = "utc", + domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> + if (call.hasBuiltinDateStaticOwner() && + call.hasNumericOrUndefinedArguments(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS, state = state) + ) { + state.ctx.trueExpr + } else { + state.ctx.falseExpr + } + }, + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + with(state.ctx) { + val arguments = call.arguments.take(MAX_CONSTRUCTOR_ARGUMENTS).map { argument -> + when (val resolved = argument.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null) { + mkUndefinedValue() -> mkFp64NaN() + else -> resolved + } + }.toMutableList() + while (arguments.size < MAX_CONSTRUCTOR_ARGUMENTS) { + arguments += mkFp64(0.0) + } + + listOf(mkFp64(call.arguments.size.toDouble())) + arguments + } + }, + ) + + private fun instanceModel( + idSuffix: String, + methodName: String, + consumedArgs: Int, + ): TsUnknownCallModel = model( + idSuffix = idSuffix, + methodName = methodName, + entryPointName = methodName, + domainGuard = instanceGuard(minArgs = 0, numericArgs = consumedArgs), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + val arguments = call.resolvedArguments(consumedArgs) + ?: return@TsEtsIrUnknownCallModelInputAdapter null + listOf(receiver) + arguments + }, + ) + + private fun instanceArityModel( + idSuffix: String, + methodName: String, + entryPointName: String, + minArgs: Int, + maxArgs: Int, + ): TsUnknownCallModel = model( + idSuffix = idSuffix, + methodName = methodName, + entryPointName = entryPointName, + domainGuard = instanceGuard(minArgs = minArgs, numericArgs = maxArgs), + inputAdapter = arityAdapter(maxArgs = maxArgs), + ) + + private fun model( + idSuffix: String, + methodName: String, + entryPointName: String, + domainGuard: TsEtsIrUnknownCallModelDomainGuard, + inputAdapter: TsEtsIrUnknownCallModelInputAdapter, + ) = TsEtsIrUnknownCallModel( + id = "ts.date.$idSuffix", + target = TsUnknownCallTarget( + methodName = methodName, + enclosingClassName = DATE_CLASS, + ), + artifact = artifact.withEntryPoint(entryPointName), + domainGuard = domainGuard, + inputAdapter = inputAdapter, + requiredModelIds = setOf("ts.math.floor"), + ) + + private fun instanceGuard( + minArgs: Int, + numericArgs: Int, + ) = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> + with(state.ctx) { + val receiver = call.receiver + val receiverValue = receiver?.resolved + if ( + call.callee.enclosingClass != builtinDateSignature || + receiverValue?.sort != addressSort || + receiverValue.asExpr(addressSort).hasFakeValueBranch() + ) { + falseExpr + } else if (!call.hasNumericArguments(minArgs = minArgs, numericArgs = numericArgs, state = state)) { + falseExpr + } else { + val runtimeType = state.memory.typeStreamOf(receiverValue.asExpr(addressSort)).singleOrNull() + if (runtimeType == builtinDateType) { + trueExpr + } else { + falseExpr + } + } + } + } + + private fun numericGuard( + minArgs: Int, + numericArgs: Int, + ) = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> + if (call.hasBuiltinDateStaticOwner() && + call.hasNumericArguments(minArgs = minArgs, numericArgs = numericArgs, state = state) + ) { + state.ctx.trueExpr + } else { + state.ctx.falseExpr + } + } + + private fun TsUnknownCall.hasBuiltinDateStaticOwner(): Boolean { + if (callee.enclosingClass != builtinDateSignature) return false + + val owner = receiver?.source as? EtsLocal ?: return false + val ownerType = owner.type as? EtsFunctionType ?: return false + return owner.name == DATE_CLASS && + ownerType.signature.enclosingClass == EtsClassSignature.UNKNOWN && + ownerType.signature.name.isEmpty() && + ownerType.signature.parameters.isEmpty() && + ownerType.signature.returnType == EtsStringType + } + + private fun arityAdapter(maxArgs: Int) = TsEtsIrUnknownCallModelInputAdapter { state, call -> + with(state.ctx) { + val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + val arguments = call.resolvedArguments(maxArgs)?.toMutableList() + ?: return@TsEtsIrUnknownCallModelInputAdapter null + while (arguments.size < maxArgs) { + arguments += mkFp64(0.0) + } + + listOf(receiver, mkFp64(call.arguments.size.toDouble())) + arguments + } + } + + private fun TsUnknownCall.resolvedArguments(maxArgs: Int): List>? = + arguments.take(maxArgs).map { argument -> + argument.resolved ?: return null + } + + private fun TsUnknownCall.hasNumericArguments( + minArgs: Int, + numericArgs: Int, + state: TsState, + ): Boolean { + if (arguments.size < minArgs) { + return false + } + + return arguments.take(numericArgs).all { argument -> argument.resolved?.sort == state.ctx.fp64Sort } + } + + private fun TsUnknownCall.hasNumericOrUndefinedArguments( + maxArgs: Int, + state: TsState, + ): Boolean = with(state.ctx) { + arguments.take(maxArgs).all { argument -> + val resolved = argument.resolved + resolved?.sort == fp64Sort || resolved == mkUndefinedValue() + } + } + + private fun TsEtsIrUnknownCallModelArtifact.withEntryPoint(methodName: String): TsEtsIrUnknownCallModelArtifact { + val modelClass = file.allClasses.single { it.name == "DateModels" } + val method = modelClass.methods.single { it.name == methodName } + return copy(entryPoint = method) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 5ea7ca9200..548f558ec3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -27,6 +27,7 @@ import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModelDispatcher import org.usvm.machine.call.dispatch import org.usvm.machine.call.hasBuiltinGlobalOwner +import org.usvm.machine.call.intrinsic.TsDateEtsIrModelFamily import org.usvm.machine.expr.TsExprApproximationResult.Companion.from import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.markResolved @@ -142,7 +143,12 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `.valueOf()` method calls if (expr.callee.name == "valueOf") { - return from(handleValueOf(expr, instance)) + val receiverIsDate = scope.calcOnState { + TsDateEtsIrModelFamily.isDateReceiver(state = this, source = expr.instance, receiver = instance) + } + if (!receiverIsDate) { + return from(handleValueOf(expr, instance)) + } } if (instance.sort != addressSort) return TsExprApproximationResult.NoApproximation diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 7edb730e7a..aac66b3c65 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -165,7 +165,8 @@ private fun TsContext.resolveDeclaredField( (resolvedField as? TsResolutionResult.Unique)?.property?.type } - if (!wasWritten) { + val requiresDeclaredPresence = !wasWritten && !field.isDateModelTimestamp() + if (requiresDeclaredPresence) { val fieldExists = scope.calcOnState { memory.types.evalIsSubtype(instance, EtsAuxiliaryType(properties = setOf(field.name))) } @@ -445,3 +446,6 @@ private val NATIVE_TYPED_ARRAY_NAMES = setOf( "Int8Array", "Uint8Array", "Uint8ClampedArray", "Int16Array", "Uint16Array", "Int32Array", "Uint32Array", "Float32Array", "Float64Array", "BigInt64Array", "BigUint64Array", ) + +private fun EtsFieldSignature.isDateModelTimestamp(): Boolean = + enclosingClass.name == "DateValue" && enclosingClass.file.fileName == "DateModels.ts" && name == "timestamp" diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 0c34a78733..410e114c0b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -184,7 +184,8 @@ fun TsContext.assignToInstanceField( // An object literal can acquire a new own property after creation. Requiring its // allocation type to declare the field would reject that valid JavaScript write. - if (objectLiteralClass == null) { + val requiresDeclaredPresence = objectLiteralClass == null && !field.isDateModelTimestamp() + if (requiresDeclaredPresence) { val fieldExists = scope.calcOnState { val supertype = EtsAuxiliaryType(properties = setOf(field.name)) memory.types.evalIsSubtype(unwrappedInstance, supertype) @@ -313,3 +314,6 @@ fun TsContext.assignToStaticField( } } } + +private fun EtsFieldSignature.isDateModelTimestamp(): Boolean = + enclosingClass.name == "DateValue" && enclosingClass.file.fileName == "DateModels.ts" && name == "timestamp" 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 new file mode 100644 index 0000000000..701bb52013 --- /dev/null +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts @@ -0,0 +1,559 @@ +// Numeric Date semantic model. Local-time operations intentionally use UTC. + +export class DateValue { + timestamp: number = NaN; +} + +class DateParts { + year: number; + month: number; + date: number; + day: number; + hours: number; + minutes: number; + seconds: number; + milliseconds: number; + + constructor( + year: number, + month: number, + date: number, + day: number, + hours: number, + minutes: number, + seconds: number, + milliseconds: number, + ) { + this.year = year; + this.month = month; + this.date = date; + this.day = day; + this.hours = hours; + this.minutes = minutes; + this.seconds = seconds; + this.milliseconds = milliseconds; + } +} + +export class DateModels { + private static readonly MS_PER_SECOND = 1_000; + private static readonly MS_PER_MINUTE = 60_000; + private static readonly MS_PER_HOUR = 3_600_000; + private static readonly MS_PER_DAY = 86_400_000; + private static readonly MAX_TIME = 8_640_000_000_000_000; + + static construct( + receiver: DateValue, + argumentCount: number, + nowMilliseconds: number, + yearOrTimestamp: number, + month: number, + date: number, + hours: number, + minutes: number, + seconds: number, + milliseconds: number, + ): DateValue { + if (argumentCount === 0) { + receiver.timestamp = DateModels.timeClip(nowMilliseconds); + return receiver; + } + + if (argumentCount === 1) { + receiver.timestamp = DateModels.timeClip(yearOrTimestamp); + return receiver; + } + + receiver.timestamp = DateModels.makeDate( + DateModels.normalizeConstructorYear(yearOrTimestamp), + month, + argumentCount >= 3 ? date : 1, + argumentCount >= 4 ? hours : 0, + argumentCount >= 5 ? minutes : 0, + argumentCount >= 6 ? seconds : 0, + argumentCount >= 7 ? milliseconds : 0, + ); + return receiver; + } + + static utc( + argumentCount: number, + year: number, + month: number, + date: number, + hours: number, + minutes: number, + seconds: number, + milliseconds: number, + ): number { + if (argumentCount < 1) { + return NaN; + } + + return DateModels.makeDate( + DateModels.normalizeConstructorYear(year), + argumentCount >= 2 ? month : 0, + argumentCount >= 3 ? date : 1, + argumentCount >= 4 ? hours : 0, + argumentCount >= 5 ? minutes : 0, + argumentCount >= 6 ? seconds : 0, + argumentCount >= 7 ? milliseconds : 0, + ); + } + + static now(nowMilliseconds: number): number { + return DateModels.timeClip(nowMilliseconds); + } + + static getDate(receiver: DateValue): number { + return DateModels.parts(receiver.timestamp).date; + } + + static getDay(receiver: DateValue): number { + return DateModels.parts(receiver.timestamp).day; + } + + static getFullYear(receiver: DateValue): number { + return DateModels.parts(receiver.timestamp).year; + } + + static getHours(receiver: DateValue): number { + return DateModels.parts(receiver.timestamp).hours; + } + + static getMilliseconds(receiver: DateValue): number { + return DateModels.parts(receiver.timestamp).milliseconds; + } + + static getMinutes(receiver: DateValue): number { + return DateModels.parts(receiver.timestamp).minutes; + } + + static getMonth(receiver: DateValue): number { + return DateModels.parts(receiver.timestamp).month; + } + + static getSeconds(receiver: DateValue): number { + return DateModels.parts(receiver.timestamp).seconds; + } + + static getTime(receiver: DateValue): number { + return receiver.timestamp; + } + + static getTimezoneOffset(receiver: DateValue): number { + return DateModels.isInvalid(receiver.timestamp) ? NaN : 0; + } + + static getUTCDate(receiver: DateValue): number { + return DateModels.getDate(receiver); + } + + static getUTCDay(receiver: DateValue): number { + return DateModels.getDay(receiver); + } + + static getUTCFullYear(receiver: DateValue): number { + return DateModels.getFullYear(receiver); + } + + static getUTCHours(receiver: DateValue): number { + return DateModels.getHours(receiver); + } + + static getUTCMilliseconds(receiver: DateValue): number { + return DateModels.getMilliseconds(receiver); + } + + static getUTCMinutes(receiver: DateValue): number { + return DateModels.getMinutes(receiver); + } + + static getUTCMonth(receiver: DateValue): number { + return DateModels.getMonth(receiver); + } + + static getUTCSeconds(receiver: DateValue): number { + return DateModels.getSeconds(receiver); + } + + static setDate(receiver: DateValue, date: number): number { + return DateModels.setDateFields(receiver, 1, date, 0, 0); + } + + static setFullYear( + receiver: DateValue, + argumentCount: number, + year: number, + month: number, + date: number, + ): number { + const current = DateModels.partsOrEpoch(receiver.timestamp); + return DateModels.replaceDate( + receiver, + year, + argumentCount >= 2 ? month : current.month, + argumentCount >= 3 ? date : current.date, + current, + ); + } + + static setHours( + receiver: DateValue, + argumentCount: number, + hours: number, + minutes: number, + seconds: number, + milliseconds: number, + ): number { + return DateModels.setTimeFields(receiver, argumentCount, hours, minutes, seconds, milliseconds, 0); + } + + static setMilliseconds(receiver: DateValue, milliseconds: number): number { + return DateModels.setTimeFields(receiver, 4, 0, 0, 0, milliseconds, 3); + } + + static setMinutes( + receiver: DateValue, + argumentCount: number, + minutes: number, + seconds: number, + milliseconds: number, + ): number { + return DateModels.setTimeFields(receiver, argumentCount + 1, 0, minutes, seconds, milliseconds, 1); + } + + static setMonth(receiver: DateValue, argumentCount: number, month: number, date: number): number { + return DateModels.setDateFields(receiver, argumentCount + 1, 0, month, date); + } + + static setSeconds(receiver: DateValue, argumentCount: number, seconds: number, milliseconds: number): number { + return DateModels.setTimeFields(receiver, argumentCount + 2, 0, 0, seconds, milliseconds, 2); + } + + static setTime(receiver: DateValue, timestamp: number): number { + receiver.timestamp = DateModels.timeClip(timestamp); + return receiver.timestamp; + } + + static setUTCDate(receiver: DateValue, date: number): number { + return DateModels.setDate(receiver, date); + } + + static setUTCFullYear( + receiver: DateValue, + argumentCount: number, + year: number, + month: number, + date: number, + ): number { + return DateModels.setFullYear(receiver, argumentCount, year, month, date); + } + + static setUTCHours( + receiver: DateValue, + argumentCount: number, + hours: number, + minutes: number, + seconds: number, + milliseconds: number, + ): number { + return DateModels.setHours(receiver, argumentCount, hours, minutes, seconds, milliseconds); + } + + static setUTCMilliseconds(receiver: DateValue, milliseconds: number): number { + return DateModels.setMilliseconds(receiver, milliseconds); + } + + static setUTCMinutes( + receiver: DateValue, + argumentCount: number, + minutes: number, + seconds: number, + milliseconds: number, + ): number { + return DateModels.setMinutes(receiver, argumentCount, minutes, seconds, milliseconds); + } + + static setUTCMonth(receiver: DateValue, argumentCount: number, month: number, date: number): number { + return DateModels.setMonth(receiver, argumentCount, month, date); + } + + static setUTCSeconds(receiver: DateValue, argumentCount: number, seconds: number, milliseconds: number): number { + return DateModels.setSeconds(receiver, argumentCount, seconds, milliseconds); + } + + static toISOString(receiver: DateValue): string { + const parts = DateModels.parts(receiver.timestamp); + if (DateModels.isInvalid(parts.year)) { + throw new RangeError("Invalid time value"); + } + + return DateModels.formatYear(parts.year) + "-" + + DateModels.pad2(parts.month + 1) + "-" + + DateModels.pad2(parts.date) + "T" + + DateModels.pad2(parts.hours) + ":" + + DateModels.pad2(parts.minutes) + ":" + + DateModels.pad2(parts.seconds) + "." + + DateModels.pad3(parts.milliseconds) + "Z"; + } + + static valueOf(receiver: DateValue): number { + return receiver.timestamp; + } + + private static setDateFields( + receiver: DateValue, + argumentCount: number, + first: number, + second: number, + third: number, + ): number { + if (DateModels.isInvalid(receiver.timestamp)) { + return DateModels.invalidate(receiver); + } + + const current = DateModels.parts(receiver.timestamp); + if (argumentCount === 1) { + return DateModels.replaceDate(receiver, current.year, current.month, first, current); + } + + return DateModels.replaceDate( + receiver, + current.year, + second, + argumentCount >= 3 ? third : current.date, + current, + ); + } + + private static setTimeFields( + receiver: DateValue, + argumentCount: number, + hours: number, + minutes: number, + seconds: number, + milliseconds: number, + firstField: number, + ): number { + if (DateModels.isInvalid(receiver.timestamp)) { + return DateModels.invalidate(receiver); + } + + const current = DateModels.parts(receiver.timestamp); + const nextHours = firstField === 0 ? hours : current.hours; + const nextMinutes = firstField <= 1 && argumentCount >= 2 ? minutes : current.minutes; + const nextSeconds = firstField <= 2 && argumentCount >= 3 ? seconds : current.seconds; + const nextMilliseconds = argumentCount >= 4 ? milliseconds : current.milliseconds; + + receiver.timestamp = DateModels.makeDate( + current.year, + current.month, + current.date, + nextHours, + nextMinutes, + nextSeconds, + nextMilliseconds, + ); + return receiver.timestamp; + } + + private static replaceDate( + receiver: DateValue, + year: number, + month: number, + date: number, + time: DateParts, + ): number { + receiver.timestamp = DateModels.makeDate( + year, + month, + date, + time.hours, + time.minutes, + time.seconds, + time.milliseconds, + ); + return receiver.timestamp; + } + + private static makeDate( + year: number, + month: number, + date: number, + hours: number, + minutes: number, + seconds: number, + milliseconds: number, + ): number { + year = DateModels.toInteger(year); + month = DateModels.toInteger(month); + date = DateModels.toInteger(date); + hours = DateModels.toInteger(hours); + minutes = DateModels.toInteger(minutes); + seconds = DateModels.toInteger(seconds); + milliseconds = DateModels.toInteger(milliseconds); + + if ( + DateModels.isInvalid(year) || DateModels.isInvalid(month) || DateModels.isInvalid(date) || + DateModels.isInvalid(hours) || DateModels.isInvalid(minutes) || DateModels.isInvalid(seconds) || + DateModels.isInvalid(milliseconds) + ) { + return NaN; + } + + const normalizedYear = year + DateModels.floorDiv(month, 12); + const normalizedMonth = DateModels.mod(month, 12); + const days = DateModels.daysFromCivil(normalizedYear, normalizedMonth, date); + const timestamp = days * DateModels.MS_PER_DAY + hours * DateModels.MS_PER_HOUR + + minutes * DateModels.MS_PER_MINUTE + seconds * DateModels.MS_PER_SECOND + milliseconds; + return DateModels.timeClip(timestamp); + } + + private static parts(timestamp: number): DateParts { + if (DateModels.isInvalid(timestamp)) { + return new DateParts(NaN, NaN, NaN, NaN, NaN, NaN, NaN, NaN); + } + + const normalizedTimestamp = timestamp === 0 ? 0 : timestamp; + const days = DateModels.floorDiv(normalizedTimestamp, DateModels.MS_PER_DAY); + let withinDay = normalizedTimestamp - days * DateModels.MS_PER_DAY; + const hours = DateModels.floorDiv(withinDay, DateModels.MS_PER_HOUR); + withinDay -= hours * DateModels.MS_PER_HOUR; + const minutes = DateModels.floorDiv(withinDay, DateModels.MS_PER_MINUTE); + withinDay -= minutes * DateModels.MS_PER_MINUTE; + const seconds = DateModels.floorDiv(withinDay, DateModels.MS_PER_SECOND); + const milliseconds = withinDay - seconds * DateModels.MS_PER_SECOND; + + const civil = DateModels.civilFromDays(days); + return new DateParts( + civil.year, + civil.month, + civil.date, + DateModels.mod(days + 4, 7), + hours, + minutes, + seconds, + milliseconds, + ); + } + + private static partsOrEpoch(timestamp: number): DateParts { + return DateModels.isInvalid(timestamp) ? DateModels.parts(0) : DateModels.parts(timestamp); + } + + private static daysFromCivil(year: number, month: number, date: number): number { + const adjustedYear = year - (month <= 1 ? 1 : 0); + const era = DateModels.floorDiv(adjustedYear, 400); + const yearOfEra = adjustedYear - era * 400; + const adjustedMonth = month + (month > 1 ? -2 : 10); + const dayOfYear = DateModels.floorDiv(153 * adjustedMonth + 2, 5) + date - 1; + const dayOfEra = yearOfEra * 365 + DateModels.floorDiv(yearOfEra, 4) - + DateModels.floorDiv(yearOfEra, 100) + dayOfYear; + return era * 146_097 + dayOfEra - 719_468; + } + + private static civilFromDays(days: number): DateParts { + const adjustedDays = days + 719_468; + const era = DateModels.floorDiv(adjustedDays, 146_097); + const dayOfEra = adjustedDays - era * 146_097; + const yearOfEra = DateModels.floorDiv( + dayOfEra - DateModels.floorDiv(dayOfEra, 1_460) + + DateModels.floorDiv(dayOfEra, 36_524) - DateModels.floorDiv(dayOfEra, 146_096), + 365, + ); + let year = yearOfEra + era * 400; + const dayOfYear = dayOfEra - ( + 365 * yearOfEra + DateModels.floorDiv(yearOfEra, 4) - DateModels.floorDiv(yearOfEra, 100) + ); + const monthPrime = DateModels.floorDiv(5 * dayOfYear + 2, 153); + const date = dayOfYear - DateModels.floorDiv(153 * monthPrime + 2, 5) + 1; + const month = monthPrime + (monthPrime < 10 ? 2 : -10); + year += month <= 1 ? 1 : 0; + return new DateParts(year, month, date, 0, 0, 0, 0, 0); + } + + private static normalizeConstructorYear(year: number): number { + year = DateModels.toInteger(year); + return year >= 0 && year <= 99 ? year + 1900 : year; + } + + private static timeClip(timestamp: number): number { + if (DateModels.isInvalid(timestamp) || timestamp > DateModels.MAX_TIME || timestamp < -DateModels.MAX_TIME) { + return NaN; + } + + const clipped = DateModels.toInteger(timestamp); + return clipped === 0 ? 0 : clipped; + } + + private static toInteger(value: number): number { + if (value === 0 || DateModels.isInvalid(value)) { + return value; + } + + return value < 0 ? -Math.floor(-value) : Math.floor(value); + } + + private static floorDiv(dividend: number, divisor: number): number { + return Math.floor(dividend / divisor); + } + + private static mod(dividend: number, divisor: number): number { + const remainder = dividend % divisor; + if (remainder === 0) { + return 0; + } + + return remainder < 0 ? remainder + divisor : remainder; + } + + private static isInvalid(value: number): boolean { + return value !== value; + } + + private static invalidate(receiver: DateValue): number { + receiver.timestamp = NaN; + return receiver.timestamp; + } + + private static digit(value: number): string { + if (value === 0) return "0"; + if (value === 1) return "1"; + if (value === 2) return "2"; + if (value === 3) return "3"; + if (value === 4) return "4"; + if (value === 5) return "5"; + if (value === 6) return "6"; + if (value === 7) return "7"; + if (value === 8) return "8"; + return "9"; + } + + private static pad2(value: number): string { + return DateModels.digit(DateModels.floorDiv(value, 10)) + DateModels.digit(DateModels.mod(value, 10)); + } + + private static pad3(value: number): string { + return DateModels.digit(DateModels.floorDiv(value, 100)) + + DateModels.pad2(DateModels.mod(value, 100)); + } + + private static pad4(value: number): string { + return DateModels.pad2(DateModels.floorDiv(value, 100)) + DateModels.pad2(DateModels.mod(value, 100)); + } + + private static pad6(value: number): string { + return DateModels.pad3(DateModels.floorDiv(value, 1_000)) + DateModels.pad3(DateModels.mod(value, 1_000)); + } + + private static formatYear(year: number): string { + if (year >= 0 && year <= 9_999) { + return DateModels.pad4(year); + } + + const sign = year < 0 ? "-" : "+"; + const absoluteYear = year < 0 ? -year : year; + return sign + DateModels.pad6(absoluteYear); + } +} 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 new file mode 100644 index 0000000000..8aa9655463 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt @@ -0,0 +1,228 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.callExpr +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertNotNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsDateEtsIrModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/DateEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `Date now and zero argument constructor share the configured fixed clock`() { + val method = method("fixedClock") + val states = analyze( + method = method, + tsOptions = TsOptions(dateNowMilliseconds = 1_710_067_696_789.0), + ) + val value = TsTestResolver().resolve(method, states.single()).returnValue + + assertEquals(0.0, assertIs(value).number) + } + + @Test + fun `clock dependent Date calls remain unsupported without an explicit clock`() { + assertTrue(analyze(method("fixedClock")).isEmpty()) + } + + @Test + fun `numeric constructors getters UTC and overflow execute through source models`() { + assertNumber(methodName = "epochYear", expected = 1970.0) + assertNumber(methodName = "leapDay", expected = 129.0) + assertNumber(methodName = "overflow", expected = 20_231_201.0) + } + + @Test + fun `UTC distinguishes omitted arguments from explicit undefined`() { + assertNaN(methodName = "utcNoArguments") + assertNaN(methodName = "utcUndefinedYear") + assertNumber(methodName = "utcYearOnly", expected = 1_577_836_800_000.0) + assertNaN(methodName = "utcExplicitUndefined") + } + + @Test + fun `timezone offset of an invalid Date is NaN`() { + assertNaN(methodName = "invalidTimezoneOffset") + } + + @Test + fun `Date truncates fractional timestamps and components toward zero`() { + assertNumber(methodName = "fractionalTimestamps", expected = 9.0) + assertNumber(methodName = "fractionalUtcDay", expected = 1.0) + } + + @Test + fun `Date calls through any aliases use the Date model`() { + assertNumber(methodName = "anyAliasValueOf", expected = 123.0) + assertNumber(methodName = "anyAliasGetTime", expected = 456.0) + } + + @Test + fun `Date alias model observation keeps the frontend callee`() { + val method = method("anyAliasGetTime") + val sourceCall = assertNotNull( + method.cfg.stmts.single { stmt -> stmt.callExpr?.callee?.name == "getTime" }.callExpr + ) + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + + assertTrue(states.isNotEmpty()) + val dateEvents = events.filter { event -> + (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId == "ts.date.getTime" + } + assertTrue(dateEvents.isNotEmpty()) + assertTrue(dateEvents.all { event -> event.callee == sourceCall.callee }) + } + + @Test + fun `Date model does not replace an unavailable user Date static method`() { + val shadowFile = loadEtsFileAutoConvert( + getResourcePath("/models/DateShadowEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + val shadowScene = EtsScene(listOf(shadowFile)) + val method = shadowScene.projectClasses + .single { it.name == "DateShadowEtsIr" } + .methods + .single { it.name == "call" } + + val states = TsMachine( + scene = shadowScene, + options = machineOptions, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze(listOf(method)) + } + + assertTrue(states.isEmpty()) + } + + @Test + fun `UTC minute and millisecond setters execute through source models`() { + assertNumber(methodName = "utcMinuteSetters", expected = 7_318_000.0) + } + + @Test + fun `concrete ISO formatting executes through the source model`() { + val method = method("isoEpoch") + val value = TsTestResolver().resolve(method, analyze(method).single()).returnValue + + assertEquals("1970-01-01T00:00:00.000Z", assertIs(value).value) + } + + @Test + fun `setter updates the shared Date timestamp slot`() { + assertNumber(methodName = "setter", expected = 951_782_400_029.0) + } + + @Test + fun `symbolic numeric timestamp round trips through constructor and valueOf`() { + val method = method("symbolicRoundTrip") + val states = analyze(method) + + assertTrue(states.isNotEmpty()) + val tests = states.map { state -> TsTestResolver().resolve(method, state) } + tests.forEach { test -> + val timestamp = assertIs(test.before.parameters.single()).number + val actual = assertIs(test.returnValue).number + val expected = if (!timestamp.isFinite() || timestamp < -MAX_DATE_TIME || timestamp > MAX_DATE_TIME) { + Double.NaN + } else { + timestamp.toLong().toDouble() + } + + if (expected.isNaN()) { + assertTrue(actual.isNaN(), "TimeClip($timestamp) must be NaN, got $actual") + } else { + assertEquals(expected, actual, "TimeClip($timestamp)") + } + } + + assertTrue( + tests.any { test -> + assertIs(test.returnValue).number.isNaN() + } + ) + assertTrue( + tests.any { test -> + assertIs(test.returnValue).number.isFinite() + } + ) + } + + private fun assertNumber(methodName: String, expected: Double) { + val method = method(methodName) + val values = analyze(method).map { state -> TsTestResolver().resolve(method, state).returnValue } + + assertEquals(expected, assertIs(values.single()).number) + } + + private fun assertNaN(methodName: String) { + val method = method(methodName) + val values = analyze(method).map { state -> TsTestResolver().resolve(method, state).returnValue } + + assertTrue(assertIs(values.single()).number.isNaN()) + } + + private fun analyze( + method: EtsMethod, + tsOptions: TsOptions = TsOptions(), + ) = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + ).use { machine -> machine.analyze(listOf(method)) } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { it.name == "DateEtsIr" } + .methods + .single { it.name == name } + + private companion object { + const val MAX_DATE_TIME = 8_640_000_000_000_000.0 + + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateModelsArtifactTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateModelsArtifactTest.kt new file mode 100644 index 0000000000..ff2ded3ff9 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateModelsArtifactTest.kt @@ -0,0 +1,32 @@ +package org.usvm.machine.call + +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class TsDateModelsArtifactTest { + @Test + fun `built in catalog registers Date family`() { + val ids = TsBuiltInUnknownCallModels.catalog().modelIds + + assertTrue("ts.date.constructor" in ids, ids.toString()) + assertTrue("ts.date.getTime" in ids, ids.toString()) + assertTrue("ts.date.now" in ids, ids.toString()) + } + + @Test + fun `native frontend loads Date source model family`() { + val artifact = loadBundledEtsIrUnknownCallModelArtifact( + resourceName = "/org/usvm/machine/call/models/DateModels.ts", + sourceFileName = "DateModels.ts", + entryPointClassName = "DateModels", + entryPointMethodName = "construct", + ) + val dateModels = artifact.file.allClasses.single { it.name == "DateModels" } + + assertEquals("construct", artifact.entryPoint.name) + assertTrue(dateModels.methods.any { it.name == "getTime" }) + assertTrue(dateModels.methods.any { it.name == "toISOString" }) + assertTrue(dateModels.methods.all { method -> method.cfg.instructions.isNotEmpty() }) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt index 67e2155165..69e78589b6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt @@ -38,6 +38,16 @@ class TsEtsIrUnknownCallModelExecutionTest { private val modelClass = baseArtifact.file.allClasses.single { it.name == "EtsIrSemanticModels" } private val models = TsUnknownCallModelCatalog( models = listOf( + model( + id = "test.ets-ir.namespace-adapter", + targetName = "abs", + entryPointName = "absolute", + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + call.arguments.map { argument -> + argument.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + } + }, + ), model( id = "test.ets-ir.absolute", targetName = "absolute", @@ -93,6 +103,17 @@ class TsEtsIrUnknownCallModelExecutionTest { ), ) + @Test + fun `custom adapter can ignore an unresolved namespace receiver`() { + val result = analyze(methodName = "namespaceReceiverCanBeIgnored") + + assertTrue( + result.values.filterIsInstance().any { value -> value.number == 2.0 }, + result.values.toString(), + ) + assertEquals(listOf("test.ets-ir.namespace-adapter"), result.modelIds.distinct()) + } + @Test fun `pure EtsIR body maps argument and return value`() { val result = analyze(methodName = "pureArgumentAndReturn") @@ -202,6 +223,7 @@ class TsEtsIrUnknownCallModelExecutionTest { targetName: String, entryPointName: String, domainGuard: TsEtsIrUnknownCallModelDomainGuard = TsEtsIrUnknownCallModelDomainGuard.ALWAYS, + inputAdapter: TsEtsIrUnknownCallModelInputAdapter = TsEtsIrUnknownCallModelInputAdapter.IDENTITY, ): TsUnknownCallModel { val artifact = baseArtifact.copy( entryPoint = modelClass.methods.single { it.name == entryPointName }, @@ -212,6 +234,7 @@ class TsEtsIrUnknownCallModelExecutionTest { target = TsUnknownCallTarget(methodName = targetName), artifact = artifact, domainGuard = domainGuard, + inputAdapter = inputAdapter, ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index 307ee9d89b..dfdd156694 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -210,11 +210,14 @@ class TsUnknownCallModelCatalogTest { "ts.string.toUpperCase", ) - assertEquals(expectedModelIds, catalog.modelIds) + assertEquals(expectedModelIds, catalog.modelIds.filterNot { it.startsWith("ts.date.") }) + assertTrue("ts.date.constructor" in catalog.modelIds) + assertTrue("ts.date.now" in catalog.modelIds) + assertEquals(expected = 38, actual = catalog.modelIds.count { it.startsWith("ts.date.") }) assertSame(catalog, TsBuiltInUnknownCallModels.catalog()) assertFailsWith { (catalog.modelIds as MutableList).clear() } assertEquals( - expectedModelIds, + catalog.modelIds, TsBuiltInUnknownCallModels.catalog().modelIds, ) assertTrue(TsBuiltInUnknownCallModels.catalog(TsUnknownCallModelSelection.Only(emptySet())).modelIds.isEmpty()) diff --git a/usvm-ts/src/test/resources/models/DateEtsIr.ts b/usvm-ts/src/test/resources/models/DateEtsIr.ts new file mode 100644 index 0000000000..cc6b6a6533 --- /dev/null +++ b/usvm-ts/src/test/resources/models/DateEtsIr.ts @@ -0,0 +1,94 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +export class DateEtsIr { + fixedClock(): number { + return Date.now() - new Date().getTime(); + } + + epochYear(): number { + return new Date(0).getUTCFullYear(); + } + + isoEpoch(): string { + return new Date(0).toISOString(); + } + + leapDay(): number { + const date = new Date(Date.UTC(2000, 1, 29, 12, 34, 56, 789)); + return date.getUTCMonth() * 100 + date.getUTCDate(); + } + + overflow(): number { + const date = new Date(Date.UTC(2024, -1, 0, 25, -1, 0, 0)); + return date.getUTCFullYear() * 10_000 + (date.getUTCMonth() + 1) * 100 + date.getUTCDate(); + } + + utcNoArguments(): number { + return Date.UTC(); + } + + utcUndefinedYear(): number { + return Date.UTC(undefined); + } + + utcYearOnly(): number { + return Date.UTC(2020); + } + + utcExplicitUndefined(): number { + return Date.UTC(2020, undefined); + } + + invalidTimezoneOffset(): number { + return new Date(NaN).getTimezoneOffset(); + } + + fractionalTimestamps(): number { + return new Date(1.9).getTime() * 10 + new Date(-1.9).getTime(); + } + + fractionalUtcDay(): number { + return new Date(Date.UTC(2024, 0, 1.9)).getUTCDate(); + } + + anyAliasValueOf(): number { + const date: any = new Date(123); + return date.valueOf(); + } + + anyAliasGetTime(): number { + const date: any = new Date(456); + return date.getTime(); + } + + utcMinuteSetters(): number { + const date = new Date(0); + const minutesTimestamp = date.setUTCMinutes(61, -2, 1_001); + const millisecondsTimestamp = date.setUTCMilliseconds(-1); + return minutesTimestamp + millisecondsTimestamp; + } + + setter(): number { + const date = new Date(0); + const timestamp = date.setUTCFullYear(2000, 1, 29); + return timestamp + date.getUTCDate(); + } + + symbolicRoundTrip(timestamp: number): number { + if (timestamp === 123.9) { + return new Date(timestamp).valueOf(); + } + if (timestamp === -123.9) { + return new Date(timestamp).valueOf(); + } + + return new Date(timestamp).valueOf(); + } + + castForeignReceiver(): number { + return (new DateImpostor() as unknown as Date).getTime(); + } +} + +class DateImpostor {} diff --git a/usvm-ts/src/test/resources/models/DateModelsComparison.mjs b/usvm-ts/src/test/resources/models/DateModelsComparison.mjs new file mode 100644 index 0000000000..0f11f6fd0e --- /dev/null +++ b/usvm-ts/src/test/resources/models/DateModelsComparison.mjs @@ -0,0 +1,130 @@ +import assert from "node:assert/strict"; +import { DateModels, DateValue } from "../../../main/resources/org/usvm/machine/call/models/DateModels.ts"; + +function modeled(...arguments_) { + const receiver = new DateValue(); + DateModels.construct(receiver, arguments_.length, 0, ...arguments_, 0, 0, 0, 0, 0, 0, 0); + return receiver; +} + +function nativeResult(operation, arguments_) { + const date = new Date(...arguments_); + const result = operation(date); + return [result, date.getTime()]; +} + +function modelResult(operation, arguments_) { + const date = modeled(...arguments_); + const result = operation(date); + return [result, date.timestamp]; +} + +const timestamps = [ + -8_640_000_000_000_000, + -2_208_988_800_001, + -1.9, + -1, + -0, + 0, + 1.9, + 951_827_696_789, + 1_710_067_696_789, + 8_640_000_000_000_000, + 8_640_000_000_000_001, + NaN, +]; + +const getters = [ + ["getDate", (date) => date.getUTCDate(), DateModels.getDate], + ["getDay", (date) => date.getUTCDay(), DateModels.getDay], + ["getFullYear", (date) => date.getUTCFullYear(), DateModels.getFullYear], + ["getHours", (date) => date.getUTCHours(), DateModels.getHours], + ["getMilliseconds", (date) => date.getUTCMilliseconds(), DateModels.getMilliseconds], + ["getMinutes", (date) => date.getUTCMinutes(), DateModels.getMinutes], + ["getMonth", (date) => date.getUTCMonth(), DateModels.getMonth], + ["getSeconds", (date) => date.getUTCSeconds(), DateModels.getSeconds], + ["getTime", (date) => date.getTime(), DateModels.getTime], +]; + +for (const timestamp of timestamps) { + const receiver = modeled(timestamp); + const native = new Date(timestamp); + for (const [name, nativeGetter, modelGetter] of getters) { + assert.deepEqual(modelGetter(receiver), nativeGetter(native), `${name}(${timestamp})`); + } +} + +const componentCases = [ + [1970, 0], + [99, 11, 31, 23, 59, 59, 999], + [2000, 1, 29, 12, 34, 56, 789], + [1900, 1, 29], + [2024, -14, 0, -2, 120, -90, 2_001], + [2024, 0, 1.9], + [-1, 0, 1], + [275760, 8, 13], +]; + +const utcBoundaryCases = [ + [], + [undefined], + [2020], + [2020, undefined], +]; + +for (const arguments_ of utcBoundaryCases) { + assert.deepEqual( + DateModels.utc(arguments_.length, ...arguments_, 0, 0, 0, 0, 0, 0, 0), + Date.UTC(...arguments_), + `UTC(${arguments_.join(",")})`, + ); +} + +for (const arguments_ of componentCases) { + assert.deepEqual( + modeled(...arguments_).timestamp, + new Date(Date.UTC(...arguments_)).getTime(), + `constructor(${arguments_.join(",")})`, + ); + assert.deepEqual( + DateModels.utc(arguments_.length, ...arguments_, 0, 0, 0, 0, 0, 0, 0), + Date.UTC(...arguments_), + `UTC(${arguments_.join(",")})`, + ); +} + +const setterCases = [ + ["setDate", [0], (date, args) => date.setUTCDate(...args), (date, args) => DateModels.setDate(date, ...args)], + ["setFullYear", [2024, 13, 0], (date, args) => date.setUTCFullYear(...args), (date, args) => DateModels.setFullYear(date, args.length, ...args, 0, 0)], + ["setHours", [-1, 70, -80, 1_500], (date, args) => date.setUTCHours(...args), (date, args) => DateModels.setHours(date, args.length, ...args, 0, 0, 0)], + ["setMilliseconds", [-1], (date, args) => date.setUTCMilliseconds(...args), (date, args) => DateModels.setMilliseconds(date, ...args)], + ["setMinutes", [61, -2, 1_001], (date, args) => date.setUTCMinutes(...args), (date, args) => DateModels.setMinutes(date, args.length, ...args, 0, 0)], + ["setMonth", [-13, 40], (date, args) => date.setUTCMonth(...args), (date, args) => DateModels.setMonth(date, args.length, ...args, 0)], + ["setSeconds", [-61, 2_000], (date, args) => date.setUTCSeconds(...args), (date, args) => DateModels.setSeconds(date, args.length, ...args, 0)], + ["setTime", [-1.9], (date, args) => date.setTime(...args), (date, args) => DateModels.setTime(date, ...args)], + ["setUTCMilliseconds", [-1], (date, args) => date.setUTCMilliseconds(...args), (date, args) => DateModels.setUTCMilliseconds(date, ...args)], + ["setUTCMinutes", [61, -2, 1_001], (date, args) => date.setUTCMinutes(...args), (date, args) => DateModels.setUTCMinutes(date, args.length, ...args, 0, 0)], +]; + +for (const timestamp of [-1, 0, 951_827_696_789]) { + for (const [name, args, nativeSetter, modelSetter] of setterCases) { + assert.deepEqual( + modelResult((date) => modelSetter(date, args), [timestamp]), + nativeResult((date) => nativeSetter(date, args), [timestamp]), + `${name} from ${timestamp}`, + ); + } +} + +for (const timestamp of [-62_167_219_200_000, -1, 0, 253_402_300_799_999]) { + const receiver = modeled(timestamp); + assert.equal(DateModels.toISOString(receiver), new Date(timestamp).toISOString()); +} + +assert.deepEqual( + DateModels.getTimezoneOffset(modeled(NaN)), + new Date(NaN).getTimezoneOffset(), + "getTimezoneOffset(NaN)", +); + +console.log("DateModels comparison passed"); diff --git a/usvm-ts/src/test/resources/models/DateShadowEtsIr.ts b/usvm-ts/src/test/resources/models/DateShadowEtsIr.ts new file mode 100644 index 0000000000..88e028a97e --- /dev/null +++ b/usvm-ts/src/test/resources/models/DateShadowEtsIr.ts @@ -0,0 +1,10 @@ +// @ts-nocheck +declare class Date { + static UTC(year: number): number; +} + +export class DateShadowEtsIr { + call(): number { + return Date.UTC(2020); + } +} diff --git a/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts index 3c9c667e55..adad1b361e 100644 --- a/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts @@ -11,6 +11,10 @@ declare class ExternalModels { } export class EtsIrSemanticModelCalls { + namespaceReceiverCanBeIgnored(): number { + return Math.abs(-2); + } + pureArgumentAndReturn(): number { return ExternalModels.absolute(-42); } From 21005a79645cfb467e9b0163cd1a9c44a270de7f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 10 Oct 2026 23:55:17 +0300 Subject: [PATCH 02/10] Preserve global Date static calls through native capture --- .../kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt | 7 +++++++ .../kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt | 3 +++ 2 files changed, 10 insertions(+) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt index 436e5fad9e..f4d943c552 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt +++ b/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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt index 00f06d3f79..73d7305a52 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt @@ -21,6 +21,7 @@ import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue import org.usvm.machine.call.isBuiltinArrayConstructor import org.usvm.machine.call.isBuiltinGlobalType +import org.usvm.machine.call.isBuiltinDateGlobalType import org.usvm.machine.state.lastStmt import org.usvm.util.getAllFields import org.usvm.util.mkFieldLValue @@ -159,6 +160,8 @@ private fun isImplicitModeledGlobal(source: EtsLocal, callee: EtsMethodSignature return true } + if (source.type.isBuiltinDateGlobalType()) return true + val modeled = when (source.name) { "Logger" -> true "Number" -> callee.name == "isNaN" From bdae77404417bce9bae7074bc85e452eb50aa148 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 11 Oct 2026 00:42:40 +0300 Subject: [PATCH 03/10] Fix compatibility adapter lint --- .../main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt index 73d7305a52..29dbe97939 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt @@ -20,8 +20,8 @@ import org.usvm.api.allocateConcreteRef import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue import org.usvm.machine.call.isBuiltinArrayConstructor -import org.usvm.machine.call.isBuiltinGlobalType import org.usvm.machine.call.isBuiltinDateGlobalType +import org.usvm.machine.call.isBuiltinGlobalType import org.usvm.machine.state.lastStmt import org.usvm.util.getAllFields import org.usvm.util.mkFieldLValue From f5c3156070be1bc0226bbafd6e56c16915d065cb Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 19:51:15 +0300 Subject: [PATCH 04/10] Make Date models independent and isolate their timestamp storage --- usvm-ts/UNKNOWN_CALL_MODELS.md | 3 +- .../main/kotlin/org/usvm/machine/TsMachine.kt | 1 - .../machine/call/TsEtsIrUnknownCallModel.kt | 10 ++++-- .../call/intrinsic/TsDateEtsIrModelFamily.kt | 28 +++++++++------ .../org/usvm/machine/expr/DateModelStorage.kt | 34 +++++++++++++++++++ .../kotlin/org/usvm/machine/expr/ReadField.kt | 10 +++--- .../org/usvm/machine/expr/WriteField.kt | 12 ++++--- .../usvm/machine/call/TsDateEtsIrModelTest.kt | 12 +++++++ .../src/test/resources/models/DateEtsIr.ts | 6 ++++ 9 files changed, 91 insertions(+), 25 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateModelStorage.kt diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 28f85fdb65..871ec6c376 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -302,7 +302,8 @@ In contrast, `Array.pop` is expressed as the TypeScript body shown above. 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. +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: diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 617691f4c8..3ad6c0632f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -91,7 +91,6 @@ class TsMachine( // 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), diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt index a55c40d2e2..878035c90e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt @@ -192,8 +192,14 @@ fun interface TsEtsIrUnknownCallModelDomainGuard { } private fun TsUnknownCall.resolvedInputs(): List>? = 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( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt index 5040590247..12de67afd0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt @@ -3,6 +3,7 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsStringType @@ -84,6 +85,10 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } + internal fun ownsStorageDefinitionField(field: EtsFieldSignature): Boolean = + field.name == "timestamp" && field.enclosingClass.name == "DateValue" && + field.enclosingClass.file == artifact.file.signature + override val models: List by lazy { buildList { add(constructorModel()) @@ -241,7 +246,8 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { domainGuard = numericGuard(minArgs = 0, numericArgs = 0), inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, _ -> with(state.ctx) { - listOf(mkFp64(dateNowMilliseconds ?: return@TsEtsIrUnknownCallModelInputAdapter null)) + val nowMilliseconds = dateNowMilliseconds ?: return@TsEtsIrUnknownCallModelInputAdapter null + listOf(mkFp64(nowMilliseconds)) } }, ) @@ -251,9 +257,9 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { methodName = "UTC", entryPointName = "utc", domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> - if (call.hasBuiltinDateStaticOwner() && + val hasSupportedInputs = call.hasBuiltinDateStaticOwner() && call.hasNumericOrUndefinedArguments(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS, state = state) - ) { + if (hasSupportedInputs) { state.ctx.trueExpr } else { state.ctx.falseExpr @@ -262,7 +268,8 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> with(state.ctx) { val arguments = call.arguments.take(MAX_CONSTRUCTOR_ARGUMENTS).map { argument -> - when (val resolved = argument.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null) { + val resolved = argument.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + when (resolved) { mkUndefinedValue() -> mkFp64NaN() else -> resolved } @@ -331,12 +338,11 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> with(state.ctx) { val receiver = call.receiver - val receiverValue = receiver?.resolved - if ( - call.callee.enclosingClass != builtinDateSignature || - receiverValue?.sort != addressSort || + val receiverValue = receiver?.resolved ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val unsupportedReceiver = call.callee.enclosingClass != builtinDateSignature || + receiverValue.sort != addressSort || receiverValue.asExpr(addressSort).hasFakeValueBranch() - ) { + if (unsupportedReceiver) { falseExpr } else if (!call.hasNumericArguments(minArgs = minArgs, numericArgs = numericArgs, state = state)) { falseExpr @@ -355,9 +361,9 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { minArgs: Int, numericArgs: Int, ) = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> - if (call.hasBuiltinDateStaticOwner() && + val hasSupportedInputs = call.hasBuiltinDateStaticOwner() && call.hasNumericArguments(minArgs = minArgs, numericArgs = numericArgs, state = state) - ) { + if (hasSupportedInputs) { state.ctx.trueExpr } else { state.ctx.falseExpr diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateModelStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateModelStorage.kt new file mode 100644 index 0000000000..6c60cd0f5e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateModelStorage.kt @@ -0,0 +1,34 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFieldSignature +import org.usvm.UConcreteHeapRef +import org.usvm.UHeapRef +import org.usvm.api.typeStreamOf +import org.usvm.collection.field.UFieldLValue +import org.usvm.machine.TsContext +import org.usvm.machine.call.intrinsic.TsDateEtsIrModelFamily +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.types.singleOrNull + +internal enum class DateStorageField { TIMESTAMP } + +internal fun TsContext.isDateModelTimestamp( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, +): Boolean { + val looksLikeStorageDefinition = field.name == "timestamp" && field.enclosingClass.name == "DateValue" + if (!looksLikeStorageDefinition || instance !is UConcreteHeapRef) return false + + val applicationOwnsDefinition = applicationAndSdkClasses.any { owner -> owner.signature == field.enclosingClass } + if (applicationOwnsDefinition || !TsDateEtsIrModelFamily.ownsStorageDefinitionField(field)) return false + + val runtimeType = scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() } + val builtinDateType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "Date")) + return runtimeType == builtinDateType +} + +internal fun TsContext.dateModelTimestampLValue(instance: UHeapRef) = + UFieldLValue(fp64Sort, instance, DateStorageField.TIMESTAMP) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index aac66b3c65..6a1e55ccc2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -121,6 +121,10 @@ internal fun TsContext.resolveField( ): UExpr<*>? { checkNotFake(instance) val receiver = resolveHeapRef(scope, instance) ?: return null + if (isDateModelTimestamp(scope = scope, instance = receiver, field = field)) { + val timestamp = dateModelTimestampLValue(receiver) + return scope.calcOnState { memory.read(timestamp) } + } // Input fields have symbolic initial presence. Allocations use their declaration and later writes. return if (!isAllocatedConcreteHeapRef(receiver) && instanceLocal?.type !is EtsArrayType) { @@ -165,8 +169,7 @@ private fun TsContext.resolveDeclaredField( (resolvedField as? TsResolutionResult.Unique)?.property?.type } - val requiresDeclaredPresence = !wasWritten && !field.isDateModelTimestamp() - if (requiresDeclaredPresence) { + if (!wasWritten) { val fieldExists = scope.calcOnState { memory.types.evalIsSubtype(instance, EtsAuxiliaryType(properties = setOf(field.name))) } @@ -446,6 +449,3 @@ private val NATIVE_TYPED_ARRAY_NAMES = setOf( "Int8Array", "Uint8Array", "Uint8ClampedArray", "Int16Array", "Uint16Array", "Int32Array", "Uint32Array", "Float32Array", "Float64Array", "BigInt64Array", "BigUint64Array", ) - -private fun EtsFieldSignature.isDateModelTimestamp(): Boolean = - enclosingClass.name == "DateValue" && enclosingClass.file.fileName == "DateModels.ts" && name == "timestamp" diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 410e114c0b..35734c96d2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -171,6 +171,12 @@ fun TsContext.assignToInstanceField( ): Unit? { // Unwrap to get non-fake reference. val unwrappedInstance = resolveHeapRef(scope, instance.unwrapRef(scope)) ?: return null + if (isDateModelTimestamp(scope = scope, instance = unwrappedInstance, field = field)) { + val timestamp = dateModelTimestampLValue(unwrappedInstance) + return scope.doWithState { + memory.write(timestamp, expr.asExpr(fp64Sort), guard = trueExpr) + } + } if (!isAllocatedConcreteHeapRef(unwrappedInstance) && instanceLocal.type !is EtsArrayType) { trackInputProperty(scope, unwrappedInstance, instanceLocal, field.name, hierarchy) ?: return null @@ -184,8 +190,7 @@ fun TsContext.assignToInstanceField( // An object literal can acquire a new own property after creation. Requiring its // allocation type to declare the field would reject that valid JavaScript write. - val requiresDeclaredPresence = objectLiteralClass == null && !field.isDateModelTimestamp() - if (requiresDeclaredPresence) { + if (objectLiteralClass == null) { val fieldExists = scope.calcOnState { val supertype = EtsAuxiliaryType(properties = setOf(field.name)) memory.types.evalIsSubtype(unwrappedInstance, supertype) @@ -314,6 +319,3 @@ fun TsContext.assignToStaticField( } } } - -private fun EtsFieldSignature.isDateModelTimestamp(): Boolean = - enclosingClass.name == "DateValue" && enclosingClass.file.fileName == "DateModels.ts" && name == "timestamp" 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 8aa9655463..53c30a7b0b 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 @@ -129,6 +129,13 @@ class TsDateEtsIrModelTest { assertTrue(states.isEmpty()) } + @Test + fun `Date casts do not give unrelated objects Date storage`() { + val states = analyze(method("castForeignReceiver")) + + assertTrue(states.isEmpty()) + } + @Test fun `UTC minute and millisecond setters execute through source models`() { assertNumber(methodName = "utcMinuteSetters", expected = 7_318_000.0) @@ -147,6 +154,11 @@ class TsDateEtsIrModelTest { assertNumber(methodName = "setter", expected = 951_782_400_029.0) } + @Test + fun `deleting a public timestamp property preserves the private Date value`() { + assertNumber(methodName = "deletePublicTimestamp", expected = 456.0) + } + @Test fun `symbolic numeric timestamp round trips through constructor and valueOf`() { val method = method("symbolicRoundTrip") diff --git a/usvm-ts/src/test/resources/models/DateEtsIr.ts b/usvm-ts/src/test/resources/models/DateEtsIr.ts index cc6b6a6533..c12974ee2b 100644 --- a/usvm-ts/src/test/resources/models/DateEtsIr.ts +++ b/usvm-ts/src/test/resources/models/DateEtsIr.ts @@ -75,6 +75,12 @@ export class DateEtsIr { return timestamp + date.getUTCDate(); } + deletePublicTimestamp(): number { + const date: any = new Date(456); + delete date.timestamp; + return date.getTime(); + } + symbolicRoundTrip(timestamp: number): number { if (timestamp === 123.9) { return new Date(timestamp).valueOf(); From f68516e1d2c815813eae2eaf283343b8e3a224df Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 20:09:53 +0300 Subject: [PATCH 05/10] Exercise foreign Date receiver through a supported any alias --- .../kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt | 4 ++-- usvm-ts/src/test/resources/models/DateEtsIr.ts | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) 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 53c30a7b0b..20576f2fe8 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 @@ -130,8 +130,8 @@ class TsDateEtsIrModelTest { } @Test - fun `Date casts do not give unrelated objects Date storage`() { - val states = analyze(method("castForeignReceiver")) + fun `unrelated objects do not acquire Date behavior through any aliases`() { + val states = analyze(method("foreignReceiverThroughAny")) assertTrue(states.isEmpty()) } diff --git a/usvm-ts/src/test/resources/models/DateEtsIr.ts b/usvm-ts/src/test/resources/models/DateEtsIr.ts index c12974ee2b..f9ed115eab 100644 --- a/usvm-ts/src/test/resources/models/DateEtsIr.ts +++ b/usvm-ts/src/test/resources/models/DateEtsIr.ts @@ -92,8 +92,9 @@ export class DateEtsIr { return new Date(timestamp).valueOf(); } - castForeignReceiver(): number { - return (new DateImpostor() as unknown as Date).getTime(); + foreignReceiverThroughAny(): number { + const impostor: any = new DateImpostor(); + return impostor.getTime(); } } From 82e175aeba53f9e11987f8bb58bc5bc2124c3252 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 20:11:23 +0300 Subject: [PATCH 06/10] Route Date instance models only by runtime receiver identity --- .../call/intrinsic/TsDateEtsIrModelFamily.kt | 18 ++++++------------ .../usvm/machine/expr/CallApproximations.kt | 2 +- .../usvm/machine/call/TsDateEtsIrModelTest.kt | 5 +++++ usvm-ts/src/test/resources/models/DateEtsIr.ts | 5 +++++ 4 files changed, 17 insertions(+), 13 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt index 12de67afd0..9ec053f7d4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt @@ -7,8 +7,6 @@ import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsStringType -import org.jacodb.ets.model.EtsUnclearRefType -import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UExpr import org.usvm.api.typeStreamOf @@ -58,22 +56,18 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { if (call.callee.enclosingClass.name == DATE_CLASS) return null val receiverValue = call.receiver ?: return null - if (!isDateReceiver(state, receiverValue.source, receiverValue.resolved)) return null + val canonicalCall = call.copy(callee = call.callee.copy(enclosingClass = builtinDateSignature)) + val builtinStaticOwner = canonicalCall.hasBuiltinDateStaticOwner() + if (!builtinStaticOwner && !isDateReceiver(state, receiverValue.resolved)) return null - return call.copy(callee = call.callee.copy(enclosingClass = builtinDateSignature)) + return canonicalCall } - internal fun isDateReceiver(state: TsState, source: EtsValue, receiver: UExpr<*>?): Boolean { - val sourceLooksDate = (source as? EtsLocal)?.name == DATE_CLASS || when (val type = source.type) { - is EtsClassType -> type.signature.name == DATE_CLASS - is EtsUnclearRefType -> type.typeName == DATE_CLASS - else -> false - } - if (sourceLooksDate) return true + internal fun isDateReceiver(state: TsState, receiver: UExpr<*>?): Boolean { if (receiver?.sort != state.ctx.addressSort) return false val runtimeType = state.memory.typeStreamOf(receiver.asExpr(state.ctx.addressSort)).singleOrNull() - return (runtimeType as? EtsClassType)?.signature?.name == DATE_CLASS + return runtimeType == builtinDateType } private val artifact by lazy { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 548f558ec3..c5bc2d329c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -144,7 +144,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `.valueOf()` method calls if (expr.callee.name == "valueOf") { val receiverIsDate = scope.calcOnState { - TsDateEtsIrModelFamily.isDateReceiver(state = this, source = expr.instance, receiver = instance) + TsDateEtsIrModelFamily.isDateReceiver(state = this, receiver = instance) } if (!receiverIsDate) { return from(handleValueOf(expr, instance)) 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 20576f2fe8..d8961bba3c 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 @@ -46,6 +46,11 @@ class TsDateEtsIrModelTest { assertTrue(analyze(method("fixedClock")).isEmpty()) } + @Test + fun `a primitive named Date keeps its ordinary valueOf behavior`() { + assertNumber(methodName = "primitiveNamedDate", expected = 123.0) + } + @Test fun `numeric constructors getters UTC and overflow execute through source models`() { assertNumber(methodName = "epochYear", expected = 1970.0) diff --git a/usvm-ts/src/test/resources/models/DateEtsIr.ts b/usvm-ts/src/test/resources/models/DateEtsIr.ts index f9ed115eab..6b60679c30 100644 --- a/usvm-ts/src/test/resources/models/DateEtsIr.ts +++ b/usvm-ts/src/test/resources/models/DateEtsIr.ts @@ -6,6 +6,11 @@ export class DateEtsIr { return Date.now() - new Date().getTime(); } + primitiveNamedDate(): number { + const Date = 123; + return Date.valueOf(); + } + epochYear(): number { return new Date(0).getUTCFullYear(); } From bb635f3fa6f90432fbbc01216848e7973f508859 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 20:16:54 +0300 Subject: [PATCH 07/10] Align Date storage file name with declaration --- .../machine/expr/{DateModelStorage.kt => DateStorageField.kt} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename usvm-ts/src/main/kotlin/org/usvm/machine/expr/{DateModelStorage.kt => DateStorageField.kt} (100%) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateModelStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateStorageField.kt similarity index 100% rename from usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateModelStorage.kt rename to usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateStorageField.kt From 4e671611ddd7b2a80b0a89f781dfea34d7073daa Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 23:51:29 +0300 Subject: [PATCH 08/10] Fix Date argument conversion and omitted setter inputs --- usvm-ts/UNKNOWN_CALL_MODELS.md | 7 +- .../call/intrinsic/TsDateEtsIrModelFamily.kt | 200 ++++++++++-------- .../usvm/machine/call/TsDateEtsIrModelTest.kt | 159 ++++++++++++++ .../src/test/resources/models/DateEtsIr.ts | 114 ++++++++++ 4 files changed, 392 insertions(+), 88 deletions(-) diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 871ec6c376..d68e3f1e81 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -311,8 +311,11 @@ The current experiment has these explicit limits: 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; +- 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. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt index 9ec053f7d4..97d276e3a9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt @@ -1,14 +1,16 @@ package org.usvm.machine.call.intrinsic +import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFieldSignature -import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsLocal -import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.usvm.UBoolExpr import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.UIteExpr import org.usvm.api.typeStreamOf import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact @@ -17,9 +19,13 @@ import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallModel import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.call.isBuiltinDateGlobalType import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +import org.usvm.machine.expr.dateModelTimestampLValue +import org.usvm.machine.expr.mkIsNullOrUndefined import org.usvm.machine.state.TsState import org.usvm.types.singleOrNull +import org.usvm.util.boolToFp /** Numeric `Date` API family implemented by an ordinary TypeScript source body. */ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { @@ -99,7 +105,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-full-year", methodName = "setFullYear", entryPointName = "setFullYear", - minArgs = 1, maxArgs = 3, ) ) @@ -108,7 +113,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-hours", methodName = "setHours", entryPointName = "setHours", - minArgs = 1, maxArgs = 4, ) ) @@ -124,7 +128,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-minutes", methodName = "setMinutes", entryPointName = "setMinutes", - minArgs = 1, maxArgs = 3, ) ) @@ -133,7 +136,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-month", methodName = "setMonth", entryPointName = "setMonth", - minArgs = 1, maxArgs = 2, ) ) @@ -142,7 +144,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-seconds", methodName = "setSeconds", entryPointName = "setSeconds", - minArgs = 1, maxArgs = 2, ) ) @@ -153,7 +154,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-utc-full-year", methodName = "setUTCFullYear", entryPointName = "setUTCFullYear", - minArgs = 1, maxArgs = 3, ) ) @@ -162,7 +162,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-utc-hours", methodName = "setUTCHours", entryPointName = "setUTCHours", - minArgs = 1, maxArgs = 4, ) ) @@ -178,7 +177,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-utc-minutes", methodName = "setUTCMinutes", entryPointName = "setUTCMinutes", - minArgs = 1, maxArgs = 3, ) ) @@ -187,7 +185,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-utc-month", methodName = "setUTCMonth", entryPointName = "setUTCMonth", - minArgs = 1, maxArgs = 2, ) ) @@ -196,7 +193,6 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "set-utc-seconds", methodName = "setUTCSeconds", entryPointName = "setUTCSeconds", - minArgs = 1, maxArgs = 2, ) ) @@ -207,7 +203,7 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "constructor", methodName = CONSTRUCTOR_NAME, entryPointName = "construct", - domainGuard = instanceGuard(minArgs = 0, numericArgs = MAX_CONSTRUCTOR_ARGUMENTS), + domainGuard = instanceGuard(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS, allowDateCopy = true), inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> with(state.ctx) { val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null @@ -215,7 +211,12 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { if (call.arguments.isEmpty() && nowMilliseconds == null) { return@TsEtsIrUnknownCallModelInputAdapter null } - val arguments = call.resolvedArguments(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS)?.toMutableList() + + val arguments = call.numericArguments( + maxArgs = MAX_CONSTRUCTOR_ARGUMENTS, + state = state, + allowDateCopy = true, + )?.map { it.value }?.toMutableList() ?: return@TsEtsIrUnknownCallModelInputAdapter null while (arguments.size < MAX_CONSTRUCTOR_ARGUMENTS) { arguments += mkFp64(0.0) @@ -237,7 +238,7 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "now", methodName = "now", entryPointName = "now", - domainGuard = numericGuard(minArgs = 0, numericArgs = 0), + domainGuard = staticOwnerGuard(maxArgs = 0), inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, _ -> with(state.ctx) { val nowMilliseconds = dateNowMilliseconds ?: return@TsEtsIrUnknownCallModelInputAdapter null @@ -250,24 +251,12 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = "utc", methodName = "UTC", entryPointName = "utc", - domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> - val hasSupportedInputs = call.hasBuiltinDateStaticOwner() && - call.hasNumericOrUndefinedArguments(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS, state = state) - if (hasSupportedInputs) { - state.ctx.trueExpr - } else { - state.ctx.falseExpr - } - }, + domainGuard = staticOwnerGuard(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS), inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> with(state.ctx) { - val arguments = call.arguments.take(MAX_CONSTRUCTOR_ARGUMENTS).map { argument -> - val resolved = argument.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null - when (resolved) { - mkUndefinedValue() -> mkFp64NaN() - else -> resolved - } - }.toMutableList() + val arguments = call.numericArguments(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS, state = state) + ?.map { it.value }?.toMutableList() + ?: return@TsEtsIrUnknownCallModelInputAdapter null while (arguments.size < MAX_CONSTRUCTOR_ARGUMENTS) { arguments += mkFp64(0.0) } @@ -285,11 +274,16 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix = idSuffix, methodName = methodName, entryPointName = methodName, - domainGuard = instanceGuard(minArgs = 0, numericArgs = consumedArgs), - inputAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + domainGuard = instanceGuard(maxArgs = consumedArgs), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null - val arguments = call.resolvedArguments(consumedArgs) + val arguments = call.numericArguments(maxArgs = consumedArgs, state = state) + ?.map { it.value }?.toMutableList() ?: return@TsEtsIrUnknownCallModelInputAdapter null + while (arguments.size < consumedArgs) { + arguments += state.ctx.mkFp64NaN() + } + listOf(receiver) + arguments }, ) @@ -298,13 +292,12 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { idSuffix: String, methodName: String, entryPointName: String, - minArgs: Int, maxArgs: Int, ): TsUnknownCallModel = model( idSuffix = idSuffix, methodName = methodName, entryPointName = entryPointName, - domainGuard = instanceGuard(minArgs = minArgs, numericArgs = maxArgs), + domainGuard = instanceGuard(maxArgs = maxArgs), inputAdapter = arityAdapter(maxArgs = maxArgs), ) @@ -327,40 +320,31 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) private fun instanceGuard( - minArgs: Int, - numericArgs: Int, + maxArgs: Int, + allowDateCopy: Boolean = false, ) = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> with(state.ctx) { - val receiver = call.receiver - val receiverValue = receiver?.resolved ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val receiverValue = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr val unsupportedReceiver = call.callee.enclosingClass != builtinDateSignature || receiverValue.sort != addressSort || receiverValue.asExpr(addressSort).hasFakeValueBranch() if (unsupportedReceiver) { - falseExpr - } else if (!call.hasNumericArguments(minArgs = minArgs, numericArgs = numericArgs, state = state)) { - falseExpr - } else { - val runtimeType = state.memory.typeStreamOf(receiverValue.asExpr(addressSort)).singleOrNull() - if (runtimeType == builtinDateType) { - trueExpr - } else { - falseExpr - } + return@TsEtsIrUnknownCallModelDomainGuard falseExpr } + + val arguments = call.numericArguments(maxArgs = maxArgs, state = state, allowDateCopy = allowDateCopy) + ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + + mkAnd(mkBool(isDateReceiver(state = state, receiver = receiverValue)), mkAnd(arguments.map { it.guard })) } } - private fun numericGuard( - minArgs: Int, - numericArgs: Int, - ) = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> - val hasSupportedInputs = call.hasBuiltinDateStaticOwner() && - call.hasNumericArguments(minArgs = minArgs, numericArgs = numericArgs, state = state) - if (hasSupportedInputs) { - state.ctx.trueExpr - } else { - state.ctx.falseExpr + private fun staticOwnerGuard(maxArgs: Int) = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> + with(state.ctx) { + val arguments = call.numericArguments(maxArgs = maxArgs, state = state) + ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + + mkAnd(mkBool(call.hasBuiltinDateStaticOwner()), mkAnd(arguments.map { it.guard })) } } @@ -368,52 +352,96 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { if (callee.enclosingClass != builtinDateSignature) return false val owner = receiver?.source as? EtsLocal ?: return false - val ownerType = owner.type as? EtsFunctionType ?: return false - return owner.name == DATE_CLASS && - ownerType.signature.enclosingClass == EtsClassSignature.UNKNOWN && - ownerType.signature.name.isEmpty() && - ownerType.signature.parameters.isEmpty() && - ownerType.signature.returnType == EtsStringType + return owner.name == DATE_CLASS && owner.type.isBuiltinDateGlobalType() } private fun arityAdapter(maxArgs: Int) = TsEtsIrUnknownCallModelInputAdapter { state, call -> with(state.ctx) { val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null - val arguments = call.resolvedArguments(maxArgs)?.toMutableList() + val arguments = call.numericArguments(maxArgs = maxArgs, state = state)?.map { it.value }?.toMutableList() ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (arguments.isEmpty()) { + // The mandatory first parameter is undefined when omitted; later parameters keep their defaults. + arguments += mkFp64NaN() + } + + val providedArgumentCount = arguments.size while (arguments.size < maxArgs) { arguments += mkFp64(0.0) } - listOf(receiver, mkFp64(call.arguments.size.toDouble())) + arguments + listOf(receiver, mkFp64(providedArgumentCount.toDouble())) + arguments } } - private fun TsUnknownCall.resolvedArguments(maxArgs: Int): List>? = - arguments.take(maxArgs).map { argument -> - argument.resolved ?: return null - } + private data class NumericDateArgument(val value: UExpr, val guard: UBoolExpr) - private fun TsUnknownCall.hasNumericArguments( - minArgs: Int, - numericArgs: Int, + private fun TsUnknownCall.numericArguments( + maxArgs: Int, state: TsState, - ): Boolean { - if (arguments.size < minArgs) { - return false - } + allowDateCopy: Boolean = false, + ): List? = arguments.take(maxArgs).map { argument -> + val resolved = argument.resolved ?: return null + numericArgument(state = state, value = resolved, allowDateCopy = allowDateCopy && arguments.size == 1) + } + + private fun numericArgument( + state: TsState, + value: UExpr<*>, + allowDateCopy: Boolean, + ): NumericDateArgument = with(state.ctx) { + when { + value.isFakeObject() -> { + val type = value.getFakeType(state.memory) + val reference = numericArgument(state, value.extractRef(state.memory), allowDateCopy = allowDateCopy) + val booleanNumber = boolToFp(value.extractBool(state.memory)) + val result = mkIte( + type.fpTypeExpr, + value.extractFp(state.memory), + mkIte(type.boolTypeExpr, booleanNumber, reference.value), + ) + val guard = mkOr(type.fpTypeExpr, type.boolTypeExpr, mkAnd(type.refTypeExpr, reference.guard)) + + NumericDateArgument(value = result, guard = guard) + } + + value is UIteExpr<*> -> { + val whenTrue = numericArgument(state, value.trueBranch, allowDateCopy = allowDateCopy) + val whenFalse = numericArgument(state, value.falseBranch, allowDateCopy = allowDateCopy) - return arguments.take(numericArgs).all { argument -> argument.resolved?.sort == state.ctx.fp64Sort } + NumericDateArgument( + value = mkIte(value.condition, whenTrue.value, whenFalse.value), + guard = mkIte(value.condition, whenTrue.guard, whenFalse.guard), + ) + } + + value.sort == fp64Sort -> NumericDateArgument(value = value.asExpr(fp64Sort), guard = trueExpr) + value.sort == boolSort -> NumericDateArgument( + value = boolToFp(value.asExpr(boolSort)), + guard = trueExpr, + ) + + value.sort == addressSort -> referenceArgument(state, value.asExpr(addressSort), allowDateCopy = allowDateCopy) + else -> NumericDateArgument(value = mkFp64NaN(), guard = falseExpr) + } } - private fun TsUnknownCall.hasNumericOrUndefinedArguments( - maxArgs: Int, + private fun referenceArgument( state: TsState, - ): Boolean = with(state.ctx) { - arguments.take(maxArgs).all { argument -> - val resolved = argument.resolved - resolved?.sort == fp64Sort || resolved == mkUndefinedValue() + reference: UHeapRef, + allowDateCopy: Boolean, + ): NumericDateArgument = with(state.ctx) { + val isNull = mkHeapRefEq(reference, mkTsNullValue()) + val isNullish = mkIsNullOrUndefined(reference) + val copiesDate = allowDateCopy && isDateReceiver(state = state, receiver = reference) + val timestamp = if (copiesDate) { + state.memory.read(dateModelTimestampLValue(reference)) + } else { + mkFp64NaN() } + val value = mkIte(isNull, mkFp64(0.0), mkIte(isNullish, mkFp64NaN(), timestamp)) + + NumericDateArgument(value = value, guard = mkOr(isNullish, mkBool(copiesDate))) } private fun TsEtsIrUnknownCallModelArtifact.withEntryPoint(methodName: String): TsEtsIrUnknownCallModelArtifact { 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 d8961bba3c..7a8e8b53a7 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 @@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.callExpr import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.io.TempDir import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy @@ -14,7 +15,10 @@ import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions 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.Test import kotlin.test.assertEquals import kotlin.test.assertIs @@ -23,6 +27,9 @@ import kotlin.test.assertTrue import kotlin.time.Duration class TsDateEtsIrModelTest { + @TempDir + lateinit var replayDirectory: Path + private val sourceFile = loadEtsFileAutoConvert( getResourcePath("/models/DateEtsIr.ts"), provider = EtsIrProvider.TS_FRONTEND, @@ -66,6 +73,144 @@ class TsDateEtsIrModelTest { assertNaN(methodName = "utcExplicitUndefined") } + @Test + fun `explicit undefined Date constructor arguments invalidate the date`() { + assertNaN(methodName = "undefinedConstructor") + assertNaN(methodName = "undefinedConstructorComponent") + + val method = method("undefinedConstructor") + val states = analyze(method = method, tsOptions = TsOptions(dateNowMilliseconds = 123.0)) + val value = TsTestResolver().resolve(method, states.single()).returnValue + + assertTrue(assertIs(value).number.isNaN()) + replayDateArguments( + assertions = listOf( + "Number.isNaN(example.undefinedConstructor())", + "Number.isNaN(example.undefinedConstructorComponent())", + ), + ) + } + + @Test + fun `missing required and explicit undefined setter arguments invalidate return and receiver`() { + val methodNames = listOf( + "missingSetTime", + "missingSetMonth", + "missingSetMinutes", + "undefinedSetDate", + "undefinedOptionalSetterComponent", + ) + + for (methodName in methodNames) { + val method = method(methodName) + val states = analyze(method) + val value = TsTestResolver().resolve(method, states.single()).returnValue + + assertTrue(assertIs(value).value, methodName) + } + + replayDateArguments(assertions = methodNames.map { "example.$it()" }) + } + + @Test + fun `omitted optional setter components preserve the existing date components`() { + val method = method("omittedOptionalSetterComponents") + val states = analyze(method) + val value = TsTestResolver().resolve(method, states.single()).returnValue + + assertTrue(assertIs(value).value) + replayDateArguments(assertions = listOf("example.omittedOptionalSetterComponents()")) + } + + @Test + fun `copy construction preserves valid and invalid Date instants independently`() { + assertNumber(methodName = "copiedDateKeepsItsOwnTimestamp", expected = 123.0) + assertNaN(methodName = "copiedInvalidDateStaysInvalid") + + replayDateArguments( + assertions = listOf( + "example.copiedDateKeepsItsOwnTimestamp() === 123", + "Number.isNaN(example.copiedInvalidDateStaysInvalid())", + ), + ) + } + + @Test + fun `primitive Date argument coercions preserve booleans null and boxed values`() { + assertNumber(methodName = "primitiveConstructorCoercions", expected = 10.0) + assertNumber(methodName = "boxedPrimitiveComponents", expected = 1_000.0) + assertNumber(methodName = "boxedDateCopy", expected = 123.0) + + replayDateArguments( + assertions = listOf( + "example.primitiveConstructorCoercions() === 10", + "example.boxedPrimitiveComponents() === 1000", + "example.boxedDateCopy() === 123", + ), + ) + } + + @Test + fun `boxed number and undefined alternatives preserve constructor and setter results`() { + val scenarios = mapOf("boxedConstructorArgument" to 123.0, "boxedSetterArgument" to 246.0) + + for ((methodName, numericResult) in scenarios) { + val method = method(methodName) + val tests = analyze(method).map { state -> TsTestResolver().resolve(method, state) } + val observedChoices = mutableSetOf() + + for (test in tests) { + val useNumber = assertIs(test.before.parameters.single()).value + val result = assertIs(test.returnValue).number + observedChoices += useNumber + + if (useNumber) { + assertEquals(numericResult, result, methodName) + } else { + assertTrue(result.isNaN(), methodName) + } + } + + assertEquals(setOf(true, false), observedChoices, methodName) + } + + replayDateArguments( + assertions = listOf( + "example.boxedConstructorArgument(true) === 123", + "Number.isNaN(example.boxedConstructorArgument(false))", + "example.boxedSetterArgument(true) === 246", + "Number.isNaN(example.boxedSetterArgument(false))", + ), + ) + } + + @Test + fun `unsupported boxed object conversions keep a residual outcome`() { + val method = method("boxedUnsupportedArgument") + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + val tests = states.map { state -> TsTestResolver().resolve(method, state) } + + assertTrue(tests.isNotEmpty()) + tests.forEach { test -> + assertTrue(assertIs(test.before.parameters.single()).value) + assertEquals(123.0, assertIs(test.returnValue).number) + } + assertTrue(events.any { event -> event.decision is TsUnknownCallDecision.ResidualFallback }) + replayDateArguments(assertions = listOf("example.boxedUnsupportedArgument(true) === 123")) + } + @Test fun `timezone offset of an invalid Date is NaN`() { assertNaN(methodName = "invalidTimezoneOffset") @@ -199,6 +344,20 @@ class TsDateEtsIrModelTest { ) } + private fun replayDateArguments(assertions: List) { + val source = getResourcePath("/models/DateEtsIr.ts").readText() + val checks = assertions.joinToString(separator = "\n") { assertion -> + "if (!($assertion)) throw new Error('Date argument replay failed: $assertion');" + } + + assertNodeReplay( + source = source + "\nconst example = new DateEtsIr();\n" + checks, + directory = replayDirectory, + name = "date-arguments", + timeoutMessage = "Date argument replay timed out", + ) + } + private fun assertNumber(methodName: String, expected: Double) { val method = method(methodName) val values = analyze(method).map { state -> TsTestResolver().resolve(method, state).returnValue } diff --git a/usvm-ts/src/test/resources/models/DateEtsIr.ts b/usvm-ts/src/test/resources/models/DateEtsIr.ts index 6b60679c30..2f204150c5 100644 --- a/usvm-ts/src/test/resources/models/DateEtsIr.ts +++ b/usvm-ts/src/test/resources/models/DateEtsIr.ts @@ -97,6 +97,120 @@ export class DateEtsIr { return new Date(timestamp).valueOf(); } + undefinedConstructor(): number { + return new Date(undefined).getTime(); + } + + undefinedConstructorComponent(): number { + return new Date(2024, 0, undefined).getTime(); + } + + missingSetTime(): boolean { + const date = new Date(0); + + const result = date.setTime(); + + return Number.isNaN(result) && Number.isNaN(date.getTime()); + } + + missingSetMonth(): boolean { + const date = new Date(0); + + const result = date.setUTCMonth(); + + return Number.isNaN(result) && Number.isNaN(date.getTime()); + } + + missingSetMinutes(): boolean { + const date = new Date(0); + + const result = date.setUTCMinutes(); + + return Number.isNaN(result) && Number.isNaN(date.getTime()); + } + + undefinedSetDate(): boolean { + const date = new Date(0); + + const result = date.setUTCDate(undefined); + + return Number.isNaN(result) && Number.isNaN(date.getTime()); + } + + undefinedOptionalSetterComponent(): boolean { + const date = new Date(0); + + const result = date.setUTCFullYear(2024, undefined); + + return Number.isNaN(result) && Number.isNaN(date.getTime()); + } + + omittedOptionalSetterComponents(): boolean { + const date = new Date(Date.UTC(2024, 0, 2, 3, 4, 5, 6)); + + date.setUTCFullYear(2025); + date.setUTCHours(8); + + return date.getUTCFullYear() === 2025 && date.getUTCMonth() === 0 && date.getUTCDate() === 2 + && date.getUTCHours() === 8 && date.getUTCMinutes() === 4 + && date.getUTCSeconds() === 5 && date.getUTCMilliseconds() === 6; + } + + copiedDateKeepsItsOwnTimestamp(): number { + const original = new Date(123); + const copy = new Date(original); + + original.setTime(456); + + return copy.getTime(); + } + + copiedInvalidDateStaysInvalid(): number { + return new Date(new Date(NaN)).getTime(); + } + + primitiveConstructorCoercions(): number { + return new Date(true).getTime() * 10 + new Date(false).getTime() + new Date(null).getTime(); + } + + boxedConstructorArgument(useNumber: boolean): number { + const values: any[] = [123, undefined]; + return new Date(values[useNumber ? 0 : 1]).getTime(); + } + + boxedSetterArgument(useNumber: boolean): number { + const date = new Date(0); + const values: any[] = [123, undefined]; + + const result = date.setTime(values[useNumber ? 0 : 1]); + + return result + date.getTime(); + } + + boxedPrimitiveComponents(): number { + const values: any[] = [true, null]; + const date = new Date(0); + + date.setUTCSeconds(values[0], values[1]); + + return date.getTime() + Date.UTC(1970, values[1], values[0]); + } + + boxedUnsupportedArgument(useNumber: boolean): number { + const values: any[] = [123, new DateImpostor()]; + return new Date(values[useNumber ? 0 : 1]).getTime(); + } + + boxedDateCopy(): number { + const original = new Date(123); + const values: any[] = [original, false]; + const copy = new Date(values[0]); + + original.setTime(456); + + return copy.getTime(); + } + foreignReceiverThroughAny(): number { const impostor: any = new DateImpostor(); return impostor.getTime(); From 9567a5b1a54d6c7cdffc31a0981abf317acd2790 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 00:02:55 +0300 Subject: [PATCH 09/10] Handle nullish Date inputs and isolate boxed argument regressions --- .../call/intrinsic/TsDateEtsIrModelFamily.kt | 12 ++++-- .../src/test/resources/models/DateEtsIr.ts | 37 ++++++++++++------- 2 files changed, 31 insertions(+), 18 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt index 97d276e3a9..069ce78a88 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt @@ -11,6 +11,7 @@ import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UIteExpr +import org.usvm.UNullRef import org.usvm.api.typeStreamOf import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact @@ -69,11 +70,14 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { return canonicalCall } - internal fun isDateReceiver(state: TsState, receiver: UExpr<*>?): Boolean { - if (receiver?.sort != state.ctx.addressSort) return false + internal fun isDateReceiver(state: TsState, receiver: UExpr<*>?): Boolean = with(state.ctx) { + if (receiver?.sort != addressSort) return@with false - val runtimeType = state.memory.typeStreamOf(receiver.asExpr(state.ctx.addressSort)).singleOrNull() - return runtimeType == builtinDateType + val isNullish = receiver is UNullRef || receiver == mkTsNullValue() + if (isNullish) return@with false + + val runtimeType = state.memory.typeStreamOf(receiver.asExpr(addressSort)).singleOrNull() + runtimeType == builtinDateType } private val artifact by lazy { diff --git a/usvm-ts/src/test/resources/models/DateEtsIr.ts b/usvm-ts/src/test/resources/models/DateEtsIr.ts index 2f204150c5..b69dda3126 100644 --- a/usvm-ts/src/test/resources/models/DateEtsIr.ts +++ b/usvm-ts/src/test/resources/models/DateEtsIr.ts @@ -149,11 +149,11 @@ export class DateEtsIr { const date = new Date(Date.UTC(2024, 0, 2, 3, 4, 5, 6)); date.setUTCFullYear(2025); + const afterYearChange = date.getTime(); date.setUTCHours(8); - return date.getUTCFullYear() === 2025 && date.getUTCMonth() === 0 && date.getUTCDate() === 2 - && date.getUTCHours() === 8 && date.getUTCMinutes() === 4 - && date.getUTCSeconds() === 5 && date.getUTCMilliseconds() === 6; + return afterYearChange === Date.UTC(2025, 0, 2, 3, 4, 5, 6) + && date.getTime() === Date.UTC(2025, 0, 2, 8, 4, 5, 6); } copiedDateKeepsItsOwnTimestamp(): number { @@ -174,37 +174,38 @@ export class DateEtsIr { } boxedConstructorArgument(useNumber: boolean): number { - const values: any[] = [123, undefined]; - return new Date(values[useNumber ? 0 : 1]).getTime(); + const box = new DateArgumentBox(useNumber ? 123 : undefined); + return new Date(box.value).getTime(); } boxedSetterArgument(useNumber: boolean): number { const date = new Date(0); - const values: any[] = [123, undefined]; + const box = new DateArgumentBox(useNumber ? 123 : undefined); - const result = date.setTime(values[useNumber ? 0 : 1]); + const result = date.setTime(box.value); return result + date.getTime(); } boxedPrimitiveComponents(): number { - const values: any[] = [true, null]; + const boolean = new DateArgumentBox(true); + const nullish = new DateArgumentBox(null); const date = new Date(0); - date.setUTCSeconds(values[0], values[1]); + date.setUTCSeconds(boolean.value, nullish.value); - return date.getTime() + Date.UTC(1970, values[1], values[0]); + return date.getTime() + Date.UTC(1970, nullish.value, boolean.value); } boxedUnsupportedArgument(useNumber: boolean): number { - const values: any[] = [123, new DateImpostor()]; - return new Date(values[useNumber ? 0 : 1]).getTime(); + const box = new DateArgumentBox(useNumber ? 123 : new DateImpostor()); + return new Date(box.value).getTime(); } boxedDateCopy(): number { const original = new Date(123); - const values: any[] = [original, false]; - const copy = new Date(values[0]); + const box = new DateArgumentBox(original); + const copy = new Date(box.value); original.setTime(456); @@ -218,3 +219,11 @@ export class DateEtsIr { } class DateImpostor {} + +class DateArgumentBox { + value: any; + + constructor(value: any) { + this.value = value; + } +} From 7d730cd85077908e05ff612439f9799c2af5f0e9 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 00:12:46 +0300 Subject: [PATCH 10/10] Format Date argument conversion and extract boolean conversion --- .../call/intrinsic/TsDateEtsIrModelFamily.kt | 20 +++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt index 069ce78a88..b6813d6de1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt @@ -259,7 +259,8 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> with(state.ctx) { val arguments = call.numericArguments(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS, state = state) - ?.map { it.value }?.toMutableList() + ?.map { it.value } + ?.toMutableList() ?: return@TsEtsIrUnknownCallModelInputAdapter null while (arguments.size < MAX_CONSTRUCTOR_ARGUMENTS) { arguments += mkFp64(0.0) @@ -282,7 +283,8 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null val arguments = call.numericArguments(maxArgs = consumedArgs, state = state) - ?.map { it.value }?.toMutableList() + ?.map { it.value } + ?.toMutableList() ?: return@TsEtsIrUnknownCallModelInputAdapter null while (arguments.size < consumedArgs) { arguments += state.ctx.mkFp64NaN() @@ -420,12 +422,18 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { } value.sort == fp64Sort -> NumericDateArgument(value = value.asExpr(fp64Sort), guard = trueExpr) - value.sort == boolSort -> NumericDateArgument( - value = boolToFp(value.asExpr(boolSort)), - guard = trueExpr, + value.sort == boolSort -> { + val booleanNumber = boolToFp(value.asExpr(boolSort)) + + NumericDateArgument(value = booleanNumber, guard = trueExpr) + } + + value.sort == addressSort -> referenceArgument( + state = state, + reference = value.asExpr(addressSort), + allowDateCopy = allowDateCopy, ) - value.sort == addressSort -> referenceArgument(state, value.asExpr(addressSort), allowDateCopy = allowDateCopy) else -> NumericDateArgument(value = mkFp64NaN(), guard = falseExpr) } }