diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 2af98497fb..f18d0d4f0c 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. @@ -251,7 +251,8 @@ Numeric-result and predicate methods can still use symbolic numeric positions ov The entry point must be static and have a non-empty body. After its input adapter handles optional arguments or drops non-semantic namespace receivers, its parameter count must equal the adapted input count. Unresolved required inputs -or an arity mismatch make the model not applicable. +or an arity mismatch make the model not applicable. An `inputAdapter` can resolve inputs directly from the raw call, +including omitted optional arguments. It returns `null` if a required input cannot be resolved. The domain guard has three useful outcomes: @@ -287,6 +288,23 @@ Widening a local from `number[]` to `any[]` therefore keeps the same element and In contrast, `Array.pop` is expressed as the TypeScript body shown above. +### Date experiment boundary + +The built-in Date family keeps Gregorian calendar arithmetic, component overflow, leap years, and TimeClip in +`DateModels.ts`. Kotlin only routes calls, injects the experiment clock, and exposes the model's numeric timestamp +slot on a Date receiver. + +The current experiment has these explicit limits: + +- local getters, setters, and numeric component constructors use UTC, so `getTimezoneOffset()` returns zero and DST + behavior is outside the model domain; +- `Date.now()` and `new Date()` require `TsOptions.dateNowMilliseconds`; one fixed value is reused throughout the + analysis, and both calls use fallback when it is absent; +- one-argument construction supports numeric timestamps only; string parsing and copying another Date are outside + the model domain; +- symbolic string formatting is not claimed: `toISOString()` is a source implementation for supported concrete + execution, while symbolic string conversion remains subject to the engine's string limitations. + Good intrinsic candidates include: - bulk symbolic-memory copy or fill; 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 9a939c7e06..77aafc1e5d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -62,6 +62,7 @@ class TsContext( val scene: EtsScene, components: TsComponents, internal val applicationAndSdkClasses: List = 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 ca75767d69..1f0e799607 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -87,6 +87,7 @@ class TsMachine( scene = analysisScene, components = components, applicationAndSdkClasses = scene.projectAndSdkClasses, + dateNowMilliseconds = tsOptions.dateNowMilliseconds, ) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), 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 aca3a3d540..a6b54d2d46 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -9,4 +9,20 @@ data class TsOptions( val maxArraySize: Int = 1_000, val unknownCallModelSelection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All, val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, -) + /** Fixed experiment clock used by `Date.now()` and `new Date()`; `null` leaves those calls unsupported. */ + val dateNowMilliseconds: Double? = null, +) { + init { + val isValidDateNow = dateNowMilliseconds == null || + dateNowMilliseconds.isFinite() && + dateNowMilliseconds % 1.0 == 0.0 && + dateNowMilliseconds in -DATE_TIME_CLIP_BOUND_MILLIS..DATE_TIME_CLIP_BOUND_MILLIS + require(isValidDateNow) { + "The fixed Date clock must be an integral TimeClip-range millisecond timestamp" + } + } + + private companion object { + const val DATE_TIME_CLIP_BOUND_MILLIS = 8_640_000_000_000_000.0 + } +} 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 a46c7d9d6d..4b78745421 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 @@ -141,19 +141,18 @@ internal fun TsUnknownCallDispatcher.dispatch( is EtsPtrCallExpr -> call.ptr else -> null } - return dispatch( - scope, - TsUnknownCall( - callee = callee, - receiver = receiverSource?.let { TsUnknownCallValue(it, resolvedReceiver) }, - arguments = call.args.zip(resolvedArguments) { source, resolved -> - TsUnknownCallValue(source, resolved) - }, - resultType = call.type, - callSite = callSite, - failureReason = failureReason, - ), + val unknownCall = TsUnknownCall( + callee = callee, + receiver = receiverSource?.let { TsUnknownCallValue(it, resolvedReceiver) }, + arguments = call.args.zip(resolvedArguments) { source, resolved -> + TsUnknownCallValue(source, resolved) + }, + resultType = call.type, + callSite = callSite, + failureReason = failureReason, ) + + return dispatch(scope, unknownCall) } internal fun TsUnknownCallDispatcher.dispatch( 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 c7c8d4ca5d..d6720ced80 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 fd27d6f2c5..301a9a1b30 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 @@ -83,13 +83,15 @@ fun TsContext.readField( is TsResolutionResult.Ambiguous -> unresolvedSort } - scope.doWithState { - // If we accessed some field, we make an assumption that - // this field should present in the object. - // That's not true in the common case for TS, but that's the decision we made. - val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name)) - // assert is required to update models - scope.assert(memory.types.evalIsSubtype(instance, auxiliaryType)) + if (!field.isDateModelTimestamp()) { + scope.doWithState { + // If we accessed some field, we make an assumption that + // this field should present in the object. + // That's not true in the common case for TS, but that's the decision we made. + val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name)) + // assert is required to update models + scope.assert(memory.types.evalIsSubtype(instance, auxiliaryType)) + } } // If the field type is known, we can read it directly. @@ -121,6 +123,9 @@ fun TsContext.readField( } } +private fun EtsFieldSignature.isDateModelTimestamp(): Boolean = + enclosingClass.name == "DateValue" && enclosingClass.file.fileName == "DateModels.ts" && name == "timestamp" + internal fun TsExprResolver.handleStaticFieldRef( value: EtsStaticFieldRef, ): UExpr<*>? = with(ctx) { 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 2a465cc790..6b64f9f4e3 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 @@ -143,10 +143,12 @@ fun TsContext.assignToInstanceField( val etsField = resolveEtsField(instanceLocal, field, hierarchy) // If we access some field, we expect that the object must have this field. // It is not always true for TS, but we decided to process it so. - val supertype = EtsAuxiliaryType(properties = setOf(field.name)) - // assert is required to update models - scope.doWithState { - scope.assert(memory.types.evalIsSubtype(unwrappedInstance, supertype)) + if (!field.isDateModelTimestamp()) { + val supertype = EtsAuxiliaryType(properties = setOf(field.name)) + // assert is required to update models + scope.doWithState { + scope.assert(memory.types.evalIsSubtype(unwrappedInstance, supertype)) + } } // Determine the field sort. @@ -196,6 +198,9 @@ fun TsContext.assignToInstanceField( } } +private fun EtsFieldSignature.isDateModelTimestamp(): Boolean = + enclosingClass.name == "DateValue" && enclosingClass.file.fileName == "DateModels.ts" && name == "timestamp" + internal fun TsExprResolver.handleAssignToStaticField( lhv: EtsStaticFieldRef, expr: UExpr<*>, 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 8b167083db..73bb20125f 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 @@ -207,11 +207,14 @@ class TsUnknownCallModelCatalogTest { "ts.string.startsWith", ) - 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); }