diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 46c204fb8a..d68e3f1e81 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,27 @@ Widening a local from `number[]` to `any[]` therefore keeps the same element and In contrast, `Array.pop` is expressed as the TypeScript body shown above. +### Date experiment boundary + +The built-in Date family keeps Gregorian calendar arithmetic, component overflow, leap years, and TimeClip in +`DateModels.ts`. Kotlin only routes calls, injects the experiment clock, and exposes the model's numeric timestamp +slot on a Date receiver. This private storage is separate from ordinary JavaScript properties, so deleting a +user-visible `timestamp` property cannot change the modeled instant. + +The current experiment has these explicit limits: + +- local getters, setters, and numeric component constructors use UTC, so `getTimezoneOffset()` returns zero and DST + behavior is outside the model domain; +- `Date.now()` and `new Date()` require `TsOptions.dateNowMilliseconds`; one fixed value is reused throughout the + analysis, and both calls use fallback when it is absent; +- one-argument construction supports numeric timestamps, boolean/null/undefined primitive conversion, and copying + another modeled Date's internal timestamp; string parsing and arbitrary object coercion remain outside the model + domain. Numeric primitive arguments also work through runtime-kind guarded `any` values; +- missing mandatory setter arguments and explicit `undefined` numeric components produce NaN and invalidate the + receiver, while omitted optional components keep their defaults or existing values; +- symbolic string formatting is not claimed: `toISOString()` is a source implementation for supported concrete + execution, while symbolic string conversion remains subject to the engine's string limitations. + Good intrinsic candidates include: - bulk symbolic-memory copy or fill; 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..3ad6c0632f 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,7 @@ class TsMachine( components = components, // Model bodies are reachable only through their dispatcher and its domain guards. applicationAndSdkClasses = scene.projectClasses + runtimeScene.sdkClasses, + dateNowMilliseconds = tsOptions.dateNowMilliseconds, ) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), 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/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/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/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..b6813d6de1 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt @@ -0,0 +1,464 @@ +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.EtsLocal +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.UNullRef +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.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 { + 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 + val canonicalCall = call.copy(callee = call.callee.copy(enclosingClass = builtinDateSignature)) + val builtinStaticOwner = canonicalCall.hasBuiltinDateStaticOwner() + if (!builtinStaticOwner && !isDateReceiver(state, receiverValue.resolved)) return null + + return canonicalCall + } + + internal fun isDateReceiver(state: TsState, receiver: UExpr<*>?): Boolean = with(state.ctx) { + if (receiver?.sort != addressSort) return@with false + + 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 { + loadBundledEtsIrUnknownCallModelArtifact( + resourceName = RESOURCE, + sourceFileName = "DateModels.ts", + entryPointClassName = "DateModels", + entryPointMethodName = "construct", + ) + } + + 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()) + 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", + maxArgs = 3, + ) + ) + add( + instanceArityModel( + idSuffix = "set-hours", + methodName = "setHours", + entryPointName = "setHours", + maxArgs = 4, + ) + ) + add( + instanceModel( + idSuffix = "set-milliseconds", + methodName = "setMilliseconds", + consumedArgs = 1, + ) + ) + add( + instanceArityModel( + idSuffix = "set-minutes", + methodName = "setMinutes", + entryPointName = "setMinutes", + maxArgs = 3, + ) + ) + add( + instanceArityModel( + idSuffix = "set-month", + methodName = "setMonth", + entryPointName = "setMonth", + maxArgs = 2, + ) + ) + add( + instanceArityModel( + idSuffix = "set-seconds", + methodName = "setSeconds", + entryPointName = "setSeconds", + 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", + maxArgs = 3, + ) + ) + add( + instanceArityModel( + idSuffix = "set-utc-hours", + methodName = "setUTCHours", + entryPointName = "setUTCHours", + maxArgs = 4, + ) + ) + add( + instanceModel( + idSuffix = "set-utc-milliseconds", + methodName = "setUTCMilliseconds", + consumedArgs = 1, + ) + ) + add( + instanceArityModel( + idSuffix = "set-utc-minutes", + methodName = "setUTCMinutes", + entryPointName = "setUTCMinutes", + maxArgs = 3, + ) + ) + add( + instanceArityModel( + idSuffix = "set-utc-month", + methodName = "setUTCMonth", + entryPointName = "setUTCMonth", + maxArgs = 2, + ) + ) + add( + instanceArityModel( + idSuffix = "set-utc-seconds", + methodName = "setUTCSeconds", + entryPointName = "setUTCSeconds", + maxArgs = 2, + ) + ) + } + } + + private fun constructorModel(): TsUnknownCallModel = model( + idSuffix = "constructor", + methodName = CONSTRUCTOR_NAME, + entryPointName = "construct", + domainGuard = instanceGuard(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS, allowDateCopy = true), + 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.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) + } + 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 = staticOwnerGuard(maxArgs = 0), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, _ -> + with(state.ctx) { + val nowMilliseconds = dateNowMilliseconds ?: return@TsEtsIrUnknownCallModelInputAdapter null + listOf(mkFp64(nowMilliseconds)) + } + }, + ) + + private fun utcModel(): TsUnknownCallModel = model( + idSuffix = "utc", + methodName = "UTC", + entryPointName = "utc", + domainGuard = staticOwnerGuard(maxArgs = MAX_CONSTRUCTOR_ARGUMENTS), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + with(state.ctx) { + 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) + } + + 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(maxArgs = consumedArgs), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + 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 + }, + ) + + private fun instanceArityModel( + idSuffix: String, + methodName: String, + entryPointName: String, + maxArgs: Int, + ): TsUnknownCallModel = model( + idSuffix = idSuffix, + methodName = methodName, + entryPointName = entryPointName, + domainGuard = instanceGuard(maxArgs = 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( + maxArgs: Int, + allowDateCopy: Boolean = false, + ) = TsEtsIrUnknownCallModelDomainGuard { state, call, _ -> + with(state.ctx) { + val receiverValue = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val unsupportedReceiver = call.callee.enclosingClass != builtinDateSignature || + receiverValue.sort != addressSort || + receiverValue.asExpr(addressSort).hasFakeValueBranch() + if (unsupportedReceiver) { + 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 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 })) + } + } + + private fun TsUnknownCall.hasBuiltinDateStaticOwner(): Boolean { + if (callee.enclosingClass != builtinDateSignature) return false + + val owner = receiver?.source as? EtsLocal ?: return false + 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.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(providedArgumentCount.toDouble())) + arguments + } + } + + private data class NumericDateArgument(val value: UExpr, val guard: UBoolExpr) + + private fun TsUnknownCall.numericArguments( + maxArgs: Int, + state: TsState, + 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) + + 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 -> { + val booleanNumber = boolToFp(value.asExpr(boolSort)) + + NumericDateArgument(value = booleanNumber, guard = trueExpr) + } + + value.sort == addressSort -> referenceArgument( + state = state, + reference = value.asExpr(addressSort), + allowDateCopy = allowDateCopy, + ) + + else -> NumericDateArgument(value = mkFp64NaN(), guard = falseExpr) + } + } + + private fun referenceArgument( + state: TsState, + 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 { + 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..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 @@ -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, 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/DateStorageField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateStorageField.kt new file mode 100644 index 0000000000..6c60cd0f5e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateStorageField.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 7edb730e7a..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) { 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..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,6 +20,7 @@ import org.usvm.api.allocateConcreteRef import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue import org.usvm.machine.call.isBuiltinArrayConstructor +import org.usvm.machine.call.isBuiltinDateGlobalType import org.usvm.machine.call.isBuiltinGlobalType import org.usvm.machine.state.lastStmt import org.usvm.util.getAllFields @@ -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" 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..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 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..7a8e8b53a7 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt @@ -0,0 +1,404 @@ +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.junit.jupiter.api.io.TempDir +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.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 +import kotlin.test.assertNotNull +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, + ) + 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 `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) + 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 `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") + } + + @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 `unrelated objects do not acquire Date behavior through any aliases`() { + val states = analyze(method("foreignReceiverThroughAny")) + + 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 `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") + 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 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 } + + 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..b69dda3126 --- /dev/null +++ b/usvm-ts/src/test/resources/models/DateEtsIr.ts @@ -0,0 +1,229 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +export class DateEtsIr { + fixedClock(): number { + return Date.now() - new Date().getTime(); + } + + primitiveNamedDate(): number { + const Date = 123; + return Date.valueOf(); + } + + 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(); + } + + 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(); + } + if (timestamp === -123.9) { + return new Date(timestamp).valueOf(); + } + + 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); + const afterYearChange = date.getTime(); + date.setUTCHours(8); + + return afterYearChange === Date.UTC(2025, 0, 2, 3, 4, 5, 6) + && date.getTime() === Date.UTC(2025, 0, 2, 8, 4, 5, 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 box = new DateArgumentBox(useNumber ? 123 : undefined); + return new Date(box.value).getTime(); + } + + boxedSetterArgument(useNumber: boolean): number { + const date = new Date(0); + const box = new DateArgumentBox(useNumber ? 123 : undefined); + + const result = date.setTime(box.value); + + return result + date.getTime(); + } + + boxedPrimitiveComponents(): number { + const boolean = new DateArgumentBox(true); + const nullish = new DateArgumentBox(null); + const date = new Date(0); + + date.setUTCSeconds(boolean.value, nullish.value); + + return date.getTime() + Date.UTC(1970, nullish.value, boolean.value); + } + + boxedUnsupportedArgument(useNumber: boolean): number { + const box = new DateArgumentBox(useNumber ? 123 : new DateImpostor()); + return new Date(box.value).getTime(); + } + + boxedDateCopy(): number { + const original = new Date(123); + const box = new DateArgumentBox(original); + const copy = new Date(box.value); + + original.setTime(456); + + return copy.getTime(); + } + + foreignReceiverThroughAny(): number { + const impostor: any = new DateImpostor(); + return impostor.getTime(); + } +} + +class DateImpostor {} + +class DateArgumentBox { + value: any; + + constructor(value: any) { + this.value = value; + } +} 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); }