diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index 8a68506075..715799695d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -16,7 +16,10 @@ import org.jacodb.ets.model.EtsVoidType import org.usvm.UAddressSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.expr.dateModelTimestampLValue +import org.usvm.machine.expr.intrinsicDateConstructorReceiver import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -46,6 +49,18 @@ internal fun TsState.setMockMethodCallResult( methodResult = TsMethodResult.Success.MockedCall(result, method) } +/** Native Date construction retains its allocated identity even when its timestamp is opaque. */ +internal fun makeFreshUnknownCallResult(scope: TsStepScope, call: TsUnknownCall): UExpr<*> { + val date = scope.calcOnState { intrinsicDateConstructorReceiver(call) } + if (date == null) return makeFreshUnknownCallResult(scope, call.resultType) + + scope.doWithState { + val timestamp = makeSymbolicPrimitive(ctx.fp64Sort) + memory.write(ctx.dateModelTimestampLValue(date), timestamp, guard = ctx.trueExpr) + } + return date +} + /** Creates a fresh opaque result through [scope], keeping solver models consistent with new constraints. */ internal fun makeFreshUnknownCallResult( scope: TsStepScope, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt index 966ce27b7d..cb1fadef65 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt @@ -14,7 +14,7 @@ import org.usvm.util.EtsHierarchy import kotlin.io.path.deleteIfExists import kotlin.io.path.inputStream -private val coreRuntimeClassNames = setOf("Object", "Function", "Array") +private val coreRuntimeClassNames = setOf("Object", "Function", "Array", "Date") // JacoDB ships the matching TypeScript lib*.d.ts next to its frontend. Single-file conversion supports // declarations, while project mode deliberately skips them. Cache the DTO, not mutable scene-owned classes. @@ -23,8 +23,23 @@ private val coreRuntimeSdk: EtsFileDto by lazy { val ir = generateEtsIR(library, loadEntrypoints = false, provider = EtsIrProvider.TS_FRONTEND) try { val file = ir.inputStream().use { EtsFileDto.loadFromJson(it) } + // The ES5 library augments Date in several interface declarations with one identity. + val runtimeClasses = file.classes.filter { it.signature.name in coreRuntimeClassNames } + val mergedClasses = runtimeClasses.groupBy { it.signature }.values.map { declarations -> + val first = declarations.first() + // Date supplies nominal identity only. Its APIs retain their existing unknown-call boundary. + val methods = if (first.signature.name == "Date") { + emptyList() + } else { + declarations.flatMap { it.methods }.distinctBy { it.signature } + } + first.copy( + fields = declarations.flatMap { it.fields }.distinctBy { it.signature }, + methods = methods, + ) + } file.copy( - classes = file.classes.filter { it.signature.name in coreRuntimeClassNames }, + classes = mergedClasses, namespaces = emptyList(), ) } finally { @@ -38,9 +53,9 @@ internal fun EtsClassType.isCoreRuntimePrototypeIdentity(): Boolean = signature.name in setOf("Function", "Array") /** - * Load Object, Function and Array from the standard declarations bundled in the pinned JacoDB dependency. - * Keep their signatures and members and preserve SDK declarations supplied by the caller. Declaration files - * describe prototypes and APIs; executing an SDK API still requires an interpreter implementation or model. + * Load Object, Function, Array and Date from the standard declarations bundled in the pinned JacoDB dependency. + * Keep existing Object/Function/Array members and add nominal Date identity. Preserve SDK declarations + * supplied by the caller. Date APIs continue through the existing unknown-call and semantic-model boundary. */ internal fun EtsScene.withCoreRuntimeSdk(): EtsScene { val missingNames = coreRuntimeClassNames - sdkClasses.map { it.name }.toSet() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 0bb7dd13dd..3abdbba2f7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -3,7 +3,6 @@ package org.usvm.machine.call import mu.KotlinLogging import org.usvm.UExpr import org.usvm.api.makeFreshUnknownCallResult -import org.usvm.api.mockMethodCall import org.usvm.api.setMockMethodCallResult import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.call.intrinsic.TsDateEtsIrModelFamily @@ -75,8 +74,11 @@ class TsModelUnknownCallDispatcher( } TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { - mockMethodCall(scope, call.callee, call.resultType) - scope.doWithState { newStmt(call.callSite) } + val result = makeFreshUnknownCallResult(scope, call) + scope.doWithState { + setMockMethodCallResult(call.callee, result) + newStmt(call.callSite) + } } } @@ -96,7 +98,7 @@ class TsModelUnknownCallDispatcher( val freshResidualResult = if ( residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN ) { - makeFreshUnknownCallResult(scope, call.resultType) + makeFreshUnknownCallResult(scope, call) } else { null } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateConstructorIdentity.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateConstructorIdentity.kt new file mode 100644 index 0000000000..cef4c46f03 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DateConstructorIdentity.kt @@ -0,0 +1,78 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.callExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.api.typeStreamOf +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsState +import org.usvm.types.singleOrNull +import org.usvm.util.EtsHierarchy +import org.usvm.util.mkFieldLValue + +internal val intrinsicDateInstanceType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "Date")) +internal val intrinsicDateConstructorSignature = EtsHierarchy.OBJECT_CLASS.signature.copy(name = "Date") + +internal fun TsContext.isIntrinsicDateConstructorProperty( + scope: TsStepScope, + instance: UHeapRef, + name: String, +): Boolean { + if (name != CONSTRUCTOR_NAME || !isAllocatedConcreteHeapRef(instance)) return false + val type = scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() } + return type == intrinsicDateInstanceType +} + +internal fun TsContext.readIntrinsicDateConstructor( + scope: TsStepScope, + instance: UHeapRef, + name: String, +): UExpr<*>? { + if (!isIntrinsicDateConstructorProperty(scope, instance, name)) return null + + val hasPrototypeMutation = scope.calcOnState { (instance to PROTOTYPE_PROPERTY_NAME) in writtenConcreteFields } + if (hasPrototypeMutation) { + throw UnsupportedOperationException("Date constructor lookup after prototype mutation is not modeled") + } + + val constructor = classConstructorRef(intrinsicDateConstructorSignature) + val wasWritten = scope.calcOnState { (instance to name) in writtenConcreteFields } + if (!wasWritten) return constructor + + val ownConstructor = mkFieldLValue(addressSort, instance, name) + val deleted = deletedFieldLValue(instance, name) + return scope.calcOnState { + ctx.mkIte(memory.read(deleted), constructor, memory.read(ownConstructor)) + } +} + +internal fun TsState.intrinsicDateConstructorReceiver(call: TsUnknownCall): UHeapRef? { + if (call.callee.name != CONSTRUCTOR_NAME || call.callSite.callExpr !is EtsInstanceCallExpr) return null + val resolvedReceiver = call.receiver?.resolved ?: return null + if (resolvedReceiver.sort != ctx.addressSort) return null + + val receiver = resolvedReceiver.asExpr(ctx.addressSort) + if (!isAllocatedConcreteHeapRef(receiver)) return null + + val type = memory.typeStreamOf(receiver).singleOrNull() + return if (type == intrinsicDateInstanceType) receiver else null +} + +/** The intrinsic constructor value is known, but its mutable prototype object is not represented. */ +internal fun TsContext.ensureSupportedDatePrototypeAccess(instance: UHeapRef, name: String) { + val constructor = instance as? UConcreteHeapRef ?: return + val isDatePrototype = name == "prototype" && + classConstructorSignature(constructor) == intrinsicDateConstructorSignature + if (isDatePrototype) { + throw UnsupportedOperationException("Date.prototype access is not modeled") + } +} 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 22d93c21b2..052820007b 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 @@ -89,6 +89,7 @@ internal fun TsExprResolver.handleInstanceFieldRef( checkUndefinedOrNullPropertyRead(scope, rawInstance, propertyName = value.field.name) ?: return null val instance = resolveHeapRef(scope, rawInstance) ?: return null if (!ensureSupportedArrayPrototypeAccess(instance, value.field.name)) return null + ensureSupportedDatePrototypeAccess(instance, value.field.name) val iteratorField = readBuiltinIteratorField(instance, value.field.name) if (iteratorField != null) return iteratorField @@ -147,6 +148,9 @@ private fun TsContext.resolveDeclaredField( field: EtsFieldSignature, hierarchy: EtsHierarchy, ): UExpr<*>? { + val dateConstructor = readIntrinsicDateConstructor(scope, instance, field.name) + if (dateConstructor != null) return dateConstructor + val deleted = scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) } if (deleted.isTrue) return mkUndefinedValue() @@ -440,6 +444,7 @@ internal fun TsExprResolver.handleStaticFieldRef( if (value.field.name == "prototype") { val constructor = classConstructorRef(value.field.enclosingClass) if (!ensureSupportedArrayPrototypeAccess(constructor, value.field.name)) return null + ensureSupportedDatePrototypeAccess(constructor, value.field.name) } return readStaticField(scope, value.field, hierarchy) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 9c7d7f35ea..e2a3f7ebab 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -586,6 +586,7 @@ class TsExprResolver( private fun prototypeFallbackReason(instance: UHeapRef, operand: EtsInstanceFieldRef): String? { val name = operand.field.name + if (ctx.isIntrinsicDateConstructorProperty(scope, instance, name)) return null if (name in OBJECT_PROTOTYPE_PROPERTIES) { return "Deleting '$name' requires unsupported Object.prototype lookup" } @@ -1222,7 +1223,12 @@ class TsExprResolver( } private fun runtimeInstanceof(objectType: EtsRefType, checkType: EtsRefType): UBoolExpr = with(ctx) { - val objectClass = hierarchy.classesForType(objectType).singleOrNull() + val runtimeType = if (objectType == intrinsicDateInstanceType) { + EtsClassType(intrinsicDateConstructorSignature) + } else { + objectType + } + val objectClass = hierarchy.classesForType(runtimeType).singleOrNull() ?: throw UnsupportedOperationException("Unknown instanceof receiver class: $objectType") val constructorClass = hierarchy.classesForType(checkType).singleOrNull() ?: throw UnsupportedOperationException("Unknown instanceof constructor class: $checkType") @@ -1573,6 +1579,10 @@ class TsExprResolver( private fun constructRuntimeClass(constructorValue: EtsValue): UExpr? = with(ctx) { val constructorType = resolveRuntimeConstructor(constructorValue, operation = RuntimeConstructorOperation.NEW) ?: return@with null + if (constructorType.signature == intrinsicDateConstructorSignature) { + return@with scope.calcOnState { memory.allocConcrete(intrinsicDateInstanceType) } + } + val clazz = scene.projectClasses.singleOrNull { it.signature == constructorType.signature } ?: throw UnsupportedOperationException("Unknown new project class: ${constructorType.signature}") 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 23d42871b8..2e53177a5f 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 @@ -111,6 +111,7 @@ internal fun TsExprResolver.handleAssignToInstanceField( checkUndefinedOrNullPropertyRead(scope, rawInstance, field.name) ?: return null val instance = resolveHeapRef(scope, rawInstance) ?: return null if (!ensureSupportedArrayPrototypeAccess(instance, field.name)) return null + ensureSupportedDatePrototypeAccess(instance, field.name) val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } if (storageType == EtsStringType) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/DateConstructorIdentityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/DateConstructorIdentityTest.kt new file mode 100644 index 0000000000..b099a7e9b5 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/DateConstructorIdentityTest.kt @@ -0,0 +1,129 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsMethod +import org.junit.jupiter.api.io.TempDir +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.ValueSource +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.util.TsMethodTestRunner +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.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class DateConstructorIdentityTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val sourcePath = "/samples/types/DateConstructorIdentity.ts" + override val scene = loadScene(sourcePath) + private var modelsEnabled = false + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + val selection = if (modelsEnabled) { + TsUnknownCallModelSelection.All + } else { + TsUnknownCallModelSelection.Only(ids = emptySet()) + } + val selectedOptions = tsOptions.copy( + unknownCallModelSelection = selection, + unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ) + + TsMachine(scene = scene, options = options, tsOptions = selectedOptions).use { machine -> + val result = machine.analyzeWithMetadata(listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason) + assertFalse(result.engineFailed) + assertTrue(result.unsupportedPaths.isEmpty(), result.unsupportedPaths.joinToString()) + result.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + @ParameterizedTest + @ValueSource(booleans = [false, true]) + fun `Date has a stable constructor identity and exact instanceof semantics`(withModels: Boolean) { + modelsEnabled = withModels + options = options.copy(timeout = 5.seconds, stepsFromLastCovered = 200L) + val methods = listOf( + "direct", "noArguments", "argumentEffects", "stableGlobal", "aliased", "inheritedConstructor", "otherValues", + "shadowed", + ) + + methods.forEach { methodName -> + discoverProperties( + method = getMethod(methodName = methodName, className = "DateConstructorIdentity"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + replay(methods) + } + + @ParameterizedTest + @ValueSource(booleans = [false, true]) + fun `Date constructor properties retain inheritance and own overrides`(withModels: Boolean) { + modelsEnabled = withModels + options = options.copy(timeout = 5.seconds, stepsFromLastCovered = 200L) + val methods = listOf("cloneThroughConstructor", "ownConstructor", "deletedOwnConstructor") + + methods.forEach { methodName -> + discoverProperties( + method = getMethod(methodName = methodName, className = "DateConstructorIdentity"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + replay(methods) + } + + @ParameterizedTest + @ValueSource(booleans = [false, true]) + fun `Date prototype mutation remains explicitly unsupported`(withModels: Boolean) { + val selection = if (withModels) { + TsUnknownCallModelSelection.All + } else { + TsUnknownCallModelSelection.Only(ids = emptySet()) + } + val selectedOptions = tsOptions.copy( + unknownCallModelSelection = selection, + unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ) + val method = getMethod(methodName = "mutatedPrototype", className = "DateConstructorIdentity") + + TsMachine(scene = scene, options = options, tsOptions = selectedOptions).use { machine -> + val result = machine.analyzeWithMetadata(listOf(method)) + + assertFalse(result.engineFailed) + assertTrue(result.states.isEmpty()) + assertTrue(result.unsupportedPaths.any { it.contains("Date.prototype access is not modeled") }) + } + } + + private fun replay(methodNames: List) { + val source = getResourcePath(sourcePath).readText() + val assertions = methodNames.joinToString(separator = "\n") { name -> + "if (!new DateConstructorIdentity().$name()) throw Error('$name');" + } + + assertNodeReplay( + source = "$source\n$assertions", + directory = directory, + name = "date-identity-$modelsEnabled", + timeoutMessage = "Date constructor replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/types/DateConstructorIdentity.ts b/usvm-ts/src/test/resources/samples/types/DateConstructorIdentity.ts new file mode 100644 index 0000000000..67edad3304 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/DateConstructorIdentity.ts @@ -0,0 +1,76 @@ +// @ts-nocheck + +class DateConstructorIdentity { + direct(): boolean { + return new Date(0) instanceof Date; + } + + noArguments(): boolean { + return new Date() instanceof Date; + } + + argumentEffects(): boolean { + const counter = { value: 0 }; + const date = new Date(counter.value = counter.value + 1); + return counter.value === 1 && date instanceof Date; + } + + stableGlobal(): boolean { + return Date === Date && typeof Date === "function"; + } + + aliased(): boolean { + const NativeDate = Date; + const date = new NativeDate(0); + return date instanceof Date && NativeDate === Date; + } + + inheritedConstructor(): boolean { + const date = new Date(0); + return date.constructor === Date; + } + + cloneThroughConstructor(): boolean { + const date = new Date(0); + if (date instanceof Date) { + return new date.constructor(456) instanceof Date; + } + return false; + } + + ownConstructor(): boolean { + const date = new Date(0); + date.constructor = ApplicationDate; + return date.constructor === ApplicationDate && new date.constructor() instanceof ApplicationDate; + } + + deletedOwnConstructor(): boolean { + const date = new Date(0); + date.constructor = ApplicationDate; + delete date.constructor; + return date.constructor === Date; + } + + otherValues(): boolean { + return !(null instanceof Date) && !(undefined instanceof Date) && !(42 instanceof Date) + && !({ timestamp: 0 } instanceof Date) && !(Date instanceof Date); + } + + mutatedPrototype(): boolean { + Date.prototype.constructor = ApplicationDate; + return new Date(0).constructor === Date; + } + + nativeConstructor(): typeof Date { + return Date; + } + + shadowed(): boolean { + const NativeDate = this.nativeConstructor(); + const Date = ApplicationDate; + const date = new Date(); + return date instanceof Date && !(date instanceof NativeDate); + } +} + +class ApplicationDate {}