diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt b/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt index 7ba39b77aa..aa9ea88d68 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt @@ -127,6 +127,7 @@ inline fun foldHeapRef( val (concreteHeapRefs, symbolicHeapRefs) = splitUHeapRef( ref, initialGuard, + ignoreNullRefs = ignoreNullRefs, collapseHeapRefs = collapseHeapRefs, staticIsConcrete = staticIsConcrete ) diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt index b5da90d860..22803f5e8b 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt @@ -12,23 +12,23 @@ import org.usvm.UAddressSort import org.usvm.UBv32SizeExprProvider import org.usvm.UBv32Sort import org.usvm.UComponents +import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UIteExpr import org.usvm.USizeSort -import org.usvm.UConcreteHeapRef import org.usvm.api.allocateConcreteRef import org.usvm.api.initializeArrayLength +import org.usvm.api.memcpy import org.usvm.api.readArrayIndex import org.usvm.api.readField import org.usvm.api.writeArrayIndex import org.usvm.api.writeField import org.usvm.collection.field.UInputFieldReading -import org.usvm.sizeSort -import org.usvm.mkSizeExpr -import org.usvm.api.memcpy import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.constraints.UEqualityConstraints import org.usvm.constraints.UTypeConstraints +import org.usvm.mkSizeExpr +import org.usvm.sizeSort import kotlin.test.assertEquals import kotlin.test.assertIs import kotlin.test.assertNotNull @@ -99,6 +99,25 @@ class HeapRefSplittingTest { assertEquals(!cond, reading.collection.updates.single().guard) } + @Test + fun `conditional null payloads round trip through input fields and arrays`() = with(ctx) { + val receiver = mkRegisterReading(idx = 0, sort = addressSort) + val payload = mkRegisterReading(idx = 1, sort = addressSort) + val array = allocateConcreteRef() + val condition by boolSort + val index = mkSizeExpr(0) + val alternatives = listOf(mkIte(condition, payload, nullRef), mkIte(condition, nullRef, payload)) + val field = "nullablePayload" + + alternatives.forEach { value -> + heap.writeField(receiver, field, addressSort, value, guard = trueExpr) + heap.writeArrayIndex(array, index, arrayDescr.first, arrayDescr.second, value, guard = trueExpr) + + assertEquals(value, heap.readField(receiver, field, addressSort)) + assertEquals(value, heap.readArrayIndex(array, index, arrayDescr.first, arrayDescr.second)) + } + } + @Test fun testInterleavedWritingToArray(): Unit = with(ctx) { val arrayRef = allocateConcreteRef() 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..52188fafad 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -3,10 +3,26 @@ package org.usvm.machine import org.usvm.machine.call.TsResidualCallPolicy import org.usvm.machine.call.TsUnknownCallModelSelection +/** Initial own-property assumptions for symbolic input objects; writes and deletes always take precedence. */ +enum class TsInputPropertyPresence { + /** Required declared fields are present; optional and undeclared fields remain symbolic. */ + DECLARED_FIELDS, + + /** Every queried own property may initially be present or absent, independently of annotations. */ + SYMBOLIC, + + /** Every queried own property is initially present, possibly with an undefined value. */ + ASSUME_PRESENT, + + /** Every queried own property is initially absent. */ + ASSUME_ABSENT, +} + data class TsOptions( val interproceduralAnalysis: Boolean = true, val enableVisualization: Boolean = false, val maxArraySize: Int = 1_000, + val inputPropertyPresence: TsInputPropertyPresence = TsInputPropertyPresence.DECLARED_FIELDS, val unknownCallModelSelection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All, val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index de1a7869a8..f5fb2783dc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -10,6 +10,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UIteExpr +import org.usvm.UNullRef import org.usvm.UOrExpr import org.usvm.USort import org.usvm.USymbolicHeapRef @@ -31,6 +32,27 @@ import org.usvm.util.boolToFp import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue +/** + * Select one leaf reference for operations that depend on its allocation or storage type. + * The model only orders the branches: fork schedules the other feasible branch at the same statement. + */ +internal fun TsContext.resolveHeapRef(scope: TsStepScope, ref: UHeapRef): UHeapRef? { + var receiver = ref + while (receiver is UIteExpr<*>) { + val conditional = receiver + val takeTrueBranch = scope.calcOnState { models.first().eval(conditional.condition).isTrue } + val branchCondition = if (takeTrueBranch) conditional.condition else mkNot(conditional.condition) + scope.fork(branchCondition) ?: return null + + receiver = if (takeTrueBranch) { + conditional.trueBranch.asExpr(addressSort) + } else { + conditional.falseBranch.asExpr(addressSort) + } + } + return receiver +} + fun TsContext.checkNotFake(expr: UExpr<*>) { require(!expr.isFakeObject()) { "Fake object handling should be done outside of this function" @@ -40,6 +62,8 @@ fun TsContext.checkNotFake(expr: UExpr<*>) { // `any` is assignable both to and from string, so a type-relation query cannot identify // a materialized string. Inspect the concrete type stream before reading its backing array. private fun TsState.stringTypeCondition(ref: UHeapRef): UBoolExpr = with(ctx) { + if (ref is UNullRef) return@with falseExpr + when (ref) { is UConcreteHeapRef, is USymbolicHeapRef -> { val type = memory.types.getTypeStream(ref).singleOrNull() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt new file mode 100644 index 0000000000..2dd94a1e7e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt @@ -0,0 +1,189 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsField +import org.jacodb.ets.model.EtsFieldImpl +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.usvm.UBoolExpr +import org.usvm.UBoolSort +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.USort +import org.usvm.collection.field.UFieldLValue +import org.usvm.isFalse +import org.usvm.machine.TsContext +import org.usvm.machine.TsInputPropertyPresence +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.types.EtsFakeType +import org.usvm.machine.types.EtsObjectType +import org.usvm.machine.types.TsUnresolvedValue +import org.usvm.machine.types.extractValue +import org.usvm.machine.types.iteUnresolvedValue +import org.usvm.memory.UReadOnlyMemory +import org.usvm.util.EtsHierarchy +import org.usvm.util.getAllMethods +import org.usvm.util.mkFieldLValue + +private enum class PropertySlot { + INITIAL_PRESENCE, + BOOL_KIND, + NUMBER_KIND, + REF_KIND, + BOOL_VALUE, + NUMBER_VALUE, + REF_VALUE, +} +private data class PropertyField(val name: String, val slot: PropertySlot, val written: Boolean) + +private fun propertyLValue(sort: S, ref: UHeapRef, name: String, slot: PropertySlot, written: Boolean) = + UFieldLValue(sort, ref, PropertyField(name, slot, written)) + +internal fun TsContext.initialPropertyPresenceLValue(ref: UHeapRef, name: String): UFieldLValue<*, UBoolSort> = + propertyLValue(boolSort, ref, name, PropertySlot.INITIAL_PRESENCE, written = false) + +/** Resolve only the receiver's declaration, never an unrelated same-name field in the scene. */ +internal fun declaredInputField(local: EtsLocal?, name: String, hierarchy: EtsHierarchy): EtsField? { + val type = local?.type + if (type !is EtsClassType && type !is EtsUnclearRefType) return null + + val fields = hierarchy.classesForType(type).flatMap { receiver -> + val owners = hierarchy.getAncestors(receiver).filter { owner -> + owner.fields.any { !it.isStatic && it.name == name } + } + // A redeclaration shadows the ancestor's type and optional flag. + val nearestOwners = owners.filter { owner -> + owners.none { descendant -> owner != descendant && owner in hierarchy.getAncestors(descendant) } + } + nearestOwners.flatMap { owner -> owner.fields.filter { !it.isStatic && it.name == name } } + } + return fields.distinctBy { it.signature }.singleOrNull() +} + +internal fun TsContext.trackInputProperty( + scope: TsStepScope, + instance: UHeapRef, + local: EtsLocal?, + name: String, + hierarchy: EtsHierarchy, +): UBoolExpr? { + val unsupported = inputPropertyUnsupportedReason(local, name, hierarchy) + if (unsupported != null) throw UnsupportedOperationException(unsupported) + + // Reference-sort payloads also contain strings; only runtime objects can receive own fields. + val objectReceiver = scope.calcOnState { + memory.types.evalIsSubtype(instance, EtsObjectType) + } + scope.assert(objectReceiver) ?: return null + + val field = declaredInputField(local, name, hierarchy) + val initial = scope.calcOnState { memory.read(initialPropertyPresenceLValue(instance, name)) } + val assumedPresence = when (scope.calcOnState { inputPropertyPresence }) { + TsInputPropertyPresence.DECLARED_FIELDS -> { + if (field != null && (field as? EtsFieldImpl)?.isOptional != true) true else null + } + TsInputPropertyPresence.SYMBOLIC -> null + TsInputPropertyPresence.ASSUME_PRESENT -> true + TsInputPropertyPresence.ASSUME_ABSENT -> false + } + if (assumedPresence != null) { + val presenceConstraint = if (assumedPresence) initial else mkNot(initial) + scope.assert(presenceConstraint) ?: return null + } + + scope.doWithState { + val optional = (field as? EtsFieldImpl)?.isOptional == true + trackedObjectProperties += TrackedObjectProperty(instance, name, field?.type, optional = optional) + } + return initial +} + +private fun inputPropertyUnsupportedReason(local: EtsLocal?, name: String, hierarchy: EtsHierarchy): String? { + if (name in OBJECT_PROTOTYPE_PROPERTIES) return "Input property '$name' requires unsupported prototype lookup" + + val type = local?.type + if (type is EtsArrayType) return "Named input array properties require array presence semantics" + if (type !is EtsClassType && type !is EtsUnclearRefType) return null + + val inheritedMethod = hierarchy.classesForType(type).flatMap { it.getAllMethods(hierarchy) } + .any { !it.isStatic && it.name == name } + return if (inheritedMethod) "Input property '$name' requires unsupported class prototype lookup" else null +} + +internal fun TsContext.inputPropertyPresence( + scope: TsStepScope, + instance: UHeapRef, + name: String, + initial: UBoolExpr, +): UBoolExpr = scope.calcOnState { + val written = memory.read(writtenPropertyLValue(instance, name)) + val deleted = memory.read(deletedFieldLValue(instance, name)) + val everPresent = mkOr(initial, written) + mkAnd(everPresent, mkNot(deleted)) +} + +/** Input values use real field payloads; kind selectors and mutation payloads have separate synthetic regions. */ +internal fun TsContext.readInputPropertyValue( + memory: UReadOnlyMemory, + instance: UHeapRef, + name: String, + written: Boolean, +): TsUnresolvedValue { + fun payload(sort: S, slot: PropertySlot): UExpr = if (written) { + memory.read(propertyLValue(sort, instance, name, slot, written = true)) + } else { + memory.read(mkFieldLValue(sort, instance, name)) + } + fun kind(slot: PropertySlot) = memory.read(propertyLValue(boolSort, instance, name, slot, written)) + + val type = EtsFakeType( + boolTypeExpr = kind(PropertySlot.BOOL_KIND), + fpTypeExpr = kind(PropertySlot.NUMBER_KIND), + refTypeExpr = kind(PropertySlot.REF_KIND), + ) + return TsUnresolvedValue( + boolValue = payload(boolSort, PropertySlot.BOOL_VALUE), + fpValue = payload(fp64Sort, PropertySlot.NUMBER_VALUE), + refValue = payload(addressSort, PropertySlot.REF_VALUE), + type = type, + ) +} + +internal fun TsContext.writeInputPropertyValue(scope: TsStepScope, instance: UHeapRef, name: String, value: UExpr<*>) { + scope.doWithState { + val (bool, boolKind) = extractValue(value, boolSort, ::getIntermediateBoolLValue) + val (number, numberKind) = extractValue(value, fp64Sort, ::getIntermediateFpLValue) + val (ref, refKind) = extractValue(value, addressSort, ::getIntermediateRefLValue) + + fun write(slot: PropertySlot, sort: S, payload: UExpr) { + val lValue = propertyLValue(sort, instance, name, slot, written = true) + memory.write(lValue, payload, guard = trueExpr) + } + + write(PropertySlot.BOOL_KIND, boolSort, boolKind) + write(PropertySlot.NUMBER_KIND, boolSort, numberKind) + write(PropertySlot.REF_KIND, boolSort, refKind) + bool?.let { write(PropertySlot.BOOL_VALUE, boolSort, it) } + number?.let { write(PropertySlot.NUMBER_VALUE, fp64Sort, it) } + ref?.let { write(PropertySlot.REF_VALUE, addressSort, it) } + + memory.write(writtenPropertyLValue(instance, name), trueExpr, guard = trueExpr) + memory.write(deletedFieldLValue(instance, name), falseExpr, guard = trueExpr) + } +} + +/** Select payloads before materializing a wrapper, so symbolic aliases never turn wrappers into ordinary objects. */ +internal fun TsContext.currentInputPropertyValue( + memory: UReadOnlyMemory, + instance: UHeapRef, + name: String, + initial: TsUnresolvedValue, +): TsUnresolvedValue { + val written = memory.read(writtenPropertyLValue(instance, name)) + if (written.isFalse) return initial + + val value = readInputPropertyValue(memory, instance, name, written = true) + return iteUnresolvedValue(written, value, initial) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ObjectPropertyUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ObjectPropertyUtil.kt new file mode 100644 index 0000000000..c10cef332a --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ObjectPropertyUtil.kt @@ -0,0 +1,74 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassCategory +import org.jacodb.ets.model.EtsClassType +import org.usvm.UBoolExpr +import org.usvm.UHeapRef +import org.usvm.api.typeStreamOf +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.isFalse +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.types.singleOrNull +import org.usvm.util.EtsHierarchy + +internal const val PROTOTYPE_PROPERTY_NAME = "__proto__" + +// Reading these names after deleting an own property requires Object.prototype lookup. +internal val OBJECT_PROTOTYPE_PROPERTIES = setOf( + "__defineGetter__", + "__defineSetter__", + "__lookupGetter__", + "__lookupSetter__", + PROTOTYPE_PROPERTY_NAME, + "constructor", + "hasOwnProperty", + "isPrototypeOf", + "propertyIsEnumerable", + "toLocaleString", + "toString", + "valueOf", +) + +/** Allocated object literals retain their own declaration, independently of the local's widened type. */ +internal fun TsContext.objectLiteralClass( + scope: TsStepScope, + instance: UHeapRef, + hierarchy: EtsHierarchy, +): EtsClass? { + if (!isAllocatedConcreteHeapRef(instance)) return null + + val type = scope.calcOnState { memory.typeStreamOf(instance).singleOrNull() } as? EtsClassType ?: return null + return hierarchy.classesForType(type).singleOrNull()?.takeIf { it.category == EtsClassCategory.OBJECT } +} + +internal fun EtsClass.hasOwnProperty(name: String): Boolean = + fields.any { it.name == name } || methods.any { it.name == name } + +private fun TsStepScope.hasPrototypeMutation(instance: UHeapRef, clazz: EtsClass): Boolean = calcOnState { + clazz.fields.any { it.name == PROTOTYPE_PROPERTY_NAME } || + (instance to PROTOTYPE_PROPERTY_NAME) in writtenConcreteFields +} + +internal fun TsStepScope.ensureNoPrototypeMutation(instance: UHeapRef, clazz: EtsClass) { + // EtsIR records both { __proto__: value } and later assignments as ordinary fields. + if (hasPrototypeMutation(instance, clazz)) { + throw UnsupportedOperationException("Object literal prototype mutation in 'in' is not supported") + } +} + +internal fun TsStepScope.ensureMissingPropertyHasNoPrototype(instance: UHeapRef, clazz: EtsClass, name: String) { + if (hasPrototypeMutation(instance, clazz) || name in OBJECT_PROTOTYPE_PROPERTIES) { + throw UnsupportedOperationException("Reading '$name' requires unsupported prototype lookup") + } +} + +internal fun ensureOwnPropertyLookup(name: String, hasOwnProperty: Boolean, deleted: UBoolExpr) { + val ownPropertyMayBeMissing = !hasOwnProperty || !deleted.isFalse + val requiresPrototypeLookup = name == PROTOTYPE_PROPERTY_NAME || + name in OBJECT_PROTOTYPE_PROPERTIES && ownPropertyMayBeMissing + if (requiresPrototypeLookup) { + throw UnsupportedOperationException("Prototype lookup for '$name' in 'in' is not supported") + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeletedFieldLValue.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/PropertyMutationLValue.kt similarity index 65% rename from usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeletedFieldLValue.kt rename to usvm-ts/src/main/kotlin/org/usvm/machine/expr/PropertyMutationLValue.kt index 61266499e9..26293fdc03 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeletedFieldLValue.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/PropertyMutationLValue.kt @@ -17,24 +17,31 @@ import org.usvm.memory.UUpdateNode import org.usvm.memory.key.UHeapRefKeyInfo import org.usvm.uctx -/** Separate from value storage: a deleted property has no value in any sort. */ -internal data class DeletedFieldLValue( +internal enum class PropertyMutationKind { + DELETED, + WRITTEN, +} + +/** Execution-time mutation markers, separate from initial presence and stored values. */ +internal data class PropertyMutationLValue( override val sort: UBoolSort, override val key: UHeapRef, val name: String, + val kind: PropertyMutationKind, ) : ULValue { - override val memoryRegionId: UMemoryRegionId = DeletedFieldRegionId(name, sort) + override val memoryRegionId: UMemoryRegionId = PropertyMutationRegionId(name, kind, sort) } -private data class DeletedFieldRegionId( +private data class PropertyMutationRegionId( val name: String, + val kind: PropertyMutationKind, override val sort: UBoolSort, ) : UMemoryRegionId { - override fun emptyRegion(): UMemoryRegion = DeletedFieldRegion(sort) + override fun emptyRegion(): UMemoryRegion = PropertyMutationRegion(sort) } -/** The marker records execution events, so input references also start with no deletion. */ -private class DeletedFieldRegion( +/** No write or deletion has occurred before execution, even on a symbolic input reference. */ +private class PropertyMutationRegion( private val sort: UBoolSort, private val updates: USymbolicCollectionUpdates = UFlatUpdates(UHeapRefKeyInfo), ) : UMemoryRegion { @@ -61,26 +68,20 @@ private class DeletedFieldRegion( value: UExpr, guard: UBoolExpr, ownership: MutabilityOwnership, - ): UMemoryRegion = DeletedFieldRegion(sort, updates.write(key, value, guard)) + ): UMemoryRegion = PropertyMutationRegion(sort, updates.write(key, value, guard)) } -// Reading these names after deleting an own property requires Object.prototype lookup. -internal val OBJECT_PROTOTYPE_PROPERTIES = setOf( - "__defineGetter__", - "__defineSetter__", - "__lookupGetter__", - "__lookupSetter__", - "__proto__", - "constructor", - "hasOwnProperty", - "isPrototypeOf", - "propertyIsEnumerable", - "toLocaleString", - "toString", - "valueOf", -) - internal fun TsContext.deletedFieldLValue( instance: UHeapRef, field: EtsFieldSignature, -): DeletedFieldLValue = DeletedFieldLValue(boolSort, instance, field.name) +): PropertyMutationLValue = deletedFieldLValue(instance, field.name) + +internal fun TsContext.deletedFieldLValue( + instance: UHeapRef, + fieldName: String, +): PropertyMutationLValue = PropertyMutationLValue(boolSort, instance, fieldName, kind = PropertyMutationKind.DELETED) + +internal fun TsContext.writtenPropertyLValue( + instance: UHeapRef, + fieldName: String, +): PropertyMutationLValue = PropertyMutationLValue(boolSort, instance, fieldName, kind = PropertyMutationKind.WRITTEN) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt index 4ffb6e227e..2a1dae990a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -4,6 +4,9 @@ import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.machine.TsContext @@ -22,7 +25,7 @@ internal fun TsExprResolver.handleArrayAccess( value: EtsArrayAccess, ): UExpr<*>? = with(ctx) { // Resolve the array. - val array = run { + val rawArray = run { val resolved = resolve(value.array) ?: return null if (resolved.isFakeObject()) { scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: run { @@ -39,10 +42,25 @@ internal fun TsExprResolver.handleArrayAccess( } // Check for undefined or null array access. - checkUndefinedOrNullPropertyRead(scope, array, propertyName = "[]") ?: return null + checkUndefinedOrNullPropertyRead(scope, rawArray, propertyName = "[]") ?: return null + val array = resolveHeapRef(scope, rawArray) ?: return null // Resolve the index. val resolvedIndex = resolve(value.index) ?: return null + val receiverType = scope.calcOnState { arrayStorageType(array, value.array.type) } + val propertyName = concreteStringValue(resolvedIndex) + if (propertyName != null && receiverType !is EtsArrayType) { + val field = EtsFieldSignature( + name = propertyName, + enclosingClass = EtsClassSignature.UNKNOWN, + type = EtsUnknownType, + ) + return resolveField(scope, value.array, array, field, hierarchy) + } + if (receiverType !is EtsArrayType) { + throw UnsupportedOperationException("Symbolic object property keys are not supported") + } + check(resolvedIndex.sort == fp64Sort) { "Expected fp64 sort for index, got: ${resolvedIndex.sort}" } @@ -56,13 +74,8 @@ internal fun TsExprResolver.handleArrayAccess( isSigned = true, ).asExpr(sizeSort) - val arrayType = scope.calcOnState { arrayStorageType(array, value.array.type) } - check(arrayType is EtsArrayType) { - "Expected EtsArrayType, got: ${value.array.type}" - } - // Read the array element. - readArray(scope, array, bvIndex, arrayType) + readArray(scope, array, bvIndex, receiverType) } fun TsContext.readArray( 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 043645e385..0fcfbc301c 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 @@ -3,13 +3,21 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsField +import org.jacodb.ets.model.EtsFieldImpl import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStringLiteralType import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUndefinedType +import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef @@ -17,16 +25,22 @@ import org.usvm.USort import org.usvm.USymbolicHeapRef import org.usvm.api.evalTypeEquals import org.usvm.api.makeSymbolicRefUntyped +import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isFalse import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.ensureStaticsInitialized import org.usvm.machine.types.EtsAuxiliaryType +import org.usvm.machine.types.EtsFakeType +import org.usvm.machine.types.TsUnresolvedValue +import org.usvm.machine.types.iteUnresolvedValue import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.toAuxiliaryType import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult +import org.usvm.util.arrayStorageType import org.usvm.util.createFakeField import org.usvm.util.mkFieldLValue import org.usvm.util.mkStringBackingElementLValue @@ -42,7 +56,7 @@ internal fun TsExprResolver.handleInstanceFieldRef( val instanceLocal = value.instance // Resolve the instance. - val instance: UHeapRef = run { + val rawInstance: UHeapRef = run { val resolved = resolve(instanceLocal) ?: return null if (resolved.isFakeObject()) { scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: run { @@ -60,18 +74,22 @@ internal fun TsExprResolver.handleInstanceFieldRef( // TODO: consider moving this to 'readField' // Check for undefined or null property access. - checkUndefinedOrNullPropertyRead(scope, instance, propertyName = value.field.name) ?: return null + checkUndefinedOrNullPropertyRead(scope, rawInstance, propertyName = value.field.name) ?: return null + val instance = resolveHeapRef(scope, rawInstance) ?: return null // Handle reading "length" property. if (value.field.name == "length") { - return readLengthProperty(scope, instanceLocal, instance, options.maxArraySize) + val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } + val isObjectProperty = storageType is EtsClassType || storageType is EtsUnclearRefType || + scope.calcOnState { trackedObjectProperties.any { it.instance == instance && it.name == "length" } } + if (!isObjectProperty) return readLengthProperty(scope, instanceLocal, instance, options.maxArraySize) } // Read the field. return resolveField(scope, instanceLocal, instance, value.field, hierarchy) } -private fun TsContext.resolveField( +internal fun TsContext.resolveField( scope: TsStepScope, instanceLocal: EtsLocal?, instance: UHeapRef, @@ -79,64 +97,180 @@ private fun TsContext.resolveField( hierarchy: EtsHierarchy, ): UExpr<*>? { checkNotFake(instance) + val receiver = resolveHeapRef(scope, instance) ?: return null + // Input fields have symbolic initial presence. Allocations use their declaration and later writes. + return if (!isAllocatedConcreteHeapRef(receiver) && instanceLocal?.type !is EtsArrayType) { + resolveInputField(scope, instanceLocal, receiver, field, hierarchy) + } else { + resolveDeclaredField(scope, instanceLocal, receiver, field, hierarchy) + } +} + +private fun TsContext.resolveDeclaredField( + scope: TsStepScope, + local: EtsLocal?, + instance: UHeapRef, + field: EtsFieldSignature, + hierarchy: EtsHierarchy, +): UExpr<*>? { val deleted = scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) } if (deleted.isTrue) return mkUndefinedValue() - val resolvedField = resolveEtsField(instanceLocal, field, hierarchy) - val sort = when (resolvedField) { - is TsResolutionResult.Empty -> { - if (field.name !in listOf("i", "LogLevel")) { - logger.warn { "Field $field not found, creating fake field" } - } - // If we didn't find any real fields, let's create a fake one. - // It is possible due to mistakes in the IR or if the field was added explicitly - // in the code. - // Probably, the right behaviour here is to fork the state. - instance.createFakeField(scope, field.name) - addressSort - } - - is TsResolutionResult.Unique -> typeToSort(resolvedField.property.type) - - is TsResolutionResult.Ambiguous -> unresolvedSort + // A literal's own declarations, rather than scene-wide same-name fields, determine its initial storage. + val objectClass = objectLiteralClass(scope, instance, hierarchy) + val wasWritten = scope.calcOnState { (instance to field.name) in writtenConcreteFields } + if (objectClass != null && !wasWritten && !objectClass.hasOwnProperty(field.name)) { + scope.ensureMissingPropertyHasNoPrototype(instance, objectClass, field.name) + return mkUndefinedValue() } - val fieldExists = scope.calcOnState { - // We assume a field accessed by the program is present, even though TS permits absent fields. - val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name)) - memory.types.evalIsSubtype(instance, auxiliaryType) + val declaredLiteralField = objectClass?.fields?.singleOrNull { it.name == field.name } + val resolvedField = resolveEtsField(local, field, hierarchy) + val writtenSort = scope.calcOnState { writtenObjectLiteralFieldSorts[instance to field.name] } + val declaredLiteralSort = declaredLiteralField?.let { typeToSort(it.type) } + val sort = writtenSort ?: declaredLiteralSort ?: resolvedFieldSort(scope, instance, field, resolvedField) + val declaredType = if (objectClass != null) { + declaredLiteralField?.type + } else { + (resolvedField as? TsResolutionResult.Unique)?.property?.type } - scope.assert(fieldExists) ?: return null - val value = readField(scope, instance, field, sort) - val materializedValue = if (resolvedField !is TsResolutionResult.Unique || sort is TsUnresolvedSort) { - value - } else { - val maxStringLength = scope.calcOnState { maxStringLength } - when (val fieldType = resolvedField.property.type) { - is EtsStringLiteralType -> materializeTypedStringField( - scope = scope, - value = value.asExpr(addressSort), - literal = fieldType.value, - maxStringLength = maxStringLength, - ) - - is EtsStringType -> materializeTypedStringField(scope, value.asExpr(addressSort), maxStringLength) - else -> value - } ?: return null + if (!wasWritten) { + val fieldExists = scope.calcOnState { + memory.types.evalIsSubtype(instance, EtsAuxiliaryType(properties = setOf(field.name))) + } + scope.assert(fieldExists) ?: return null } - if (deleted.isFalse) return materializedValue + val storedValue = readField(scope, instance, field, sort) + val value = materializeFieldValue(scope, storedValue, sort, declaredType) ?: return null + if (deleted.isFalse) return value + // Conditional deletion yields undefined on the deleted branch, while preserving the stored runtime kind. return iteWriteIntoFakeObject( scope = scope, condition = deleted, trueBranchValue = mkUndefinedValue(), - falseBranchValue = materializedValue, + falseBranchValue = value, + ) +} + +private fun TsContext.resolvedFieldSort( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, + resolved: TsResolutionResult, +): USort = when (resolved) { + is TsResolutionResult.Unique -> typeToSort(resolved.property.type) + is TsResolutionResult.Ambiguous -> unresolvedSort + TsResolutionResult.Empty -> { + if (field.name !in listOf("i", "LogLevel")) { + logger.warn { "Field $field not found, creating fake field" } + } + instance.createFakeField(scope, field.name) + addressSort + } +} + +private fun TsContext.materializeFieldValue( + scope: TsStepScope, + value: UExpr<*>, + sort: USort, + type: EtsType?, +): UExpr<*>? { + if (sort is TsUnresolvedSort || (type !is EtsStringType && type !is EtsStringLiteralType)) return value + + return materializeTypedStringField( + scope = scope, + value = value.asExpr(addressSort), + maxStringLength = scope.calcOnState { maxStringLength }, + literal = (type as? EtsStringLiteralType)?.value, ) } +private fun TsContext.resolveInputField( + scope: TsStepScope, + local: EtsLocal?, + instance: UHeapRef, + field: EtsFieldSignature, + hierarchy: EtsHierarchy, +): UExpr<*>? { + val initialPresence = trackInputProperty(scope, instance, local, field.name, hierarchy) ?: return null + val present = inputPropertyPresence(scope, instance, field.name, initialPresence) + val written = scope.calcOnState { memory.read(writtenPropertyLValue(instance, field.name)) } + val activeInitial = mkAnd(present, mkNot(written)) + + // Annotation constraints apply only while the initial field value is visible, before a write or deletion. + val declared = declaredInputField(local, field.name, hierarchy) + val rawInitial = scope.calcOnState { readInputPropertyValue(memory, instance, field.name, written = false) } + val initial = prepareInitialInputField(scope, rawInitial, declared, activeInitial, hierarchy) ?: return null + val current = scope.calcOnState { currentInputPropertyValue(memory, instance, field.name, initial) } + + // Missing and present-but-undefined are distinct states; both read as an undefined reference value. + val undefined = current.copy(refValue = mkUndefinedValue(), type = EtsFakeType.mkRef(this)) + val value = iteUnresolvedValue(present, current, undefined) + return scope.calcOnState { mkFakeValue(scope, value) } +} + +private fun TsContext.prepareInitialInputField( + scope: TsStepScope, + value: TsUnresolvedValue, + field: EtsField?, + activeInitial: UBoolExpr, + hierarchy: EtsHierarchy, +): TsUnresolvedValue? { + val optional = (field as? EtsFieldImpl)?.isOptional == true + val sort = field?.let { typeToSort(it.type) } ?: unresolvedSort + val expectedKind = when (sort) { + boolSort -> value.type.boolTypeExpr + fp64Sort -> value.type.fpTypeExpr + addressSort -> value.type.refTypeExpr + else -> trueExpr + } + val isUndefined = mkHeapRefEq(value.refValue, mkUndefinedValue()) + val undefinedKind = mkAnd(value.type.refTypeExpr, isUndefined) + val allowedKind = if (optional) mkOr(expectedKind, undefinedKind) else expectedKind + val exactlyOneKind = value.type.mkExactlyOneTypeConstraint(this) + val initialKindConstraint = mkImplies(activeInitial, mkAnd(allowedKind, exactlyOneKind)) + // Use the selectors stored on the input reference, so differently typed aliases agree. + scope.assert(initialKindConstraint) ?: return null + + // Optional references may be undefined even when the field exists. + val activeReference = if (optional) mkAnd(activeInitial, mkNot(isUndefined)) else activeInitial + val referenceConstraint = initialReferenceConstraint(scope, value.refValue, field?.type, hierarchy) + val activeReferenceConstraint = mkImplies(activeReference, referenceConstraint) + scope.assert(activeReferenceConstraint) ?: return null + + if (field?.type !is EtsStringType && field?.type !is EtsStringLiteralType) return value + + val stringRef = materializeTypedStringField( + scope = scope, + value = value.refValue, + maxStringLength = scope.calcOnState { maxStringLength }, + literal = (field.type as? EtsStringLiteralType)?.value, + activeGuard = activeReference, + ) ?: return null + val initialRef = if (optional) mkIte(isUndefined, mkUndefinedValue(), stringRef) else stringRef + return value.copy(refValue = initialRef) +} + +private fun TsContext.initialReferenceConstraint( + scope: TsStepScope, + ref: UHeapRef, + type: EtsType?, + hierarchy: EtsHierarchy, +): UBoolExpr = when (type) { + is EtsClassType -> scope.calcOnState { + val auxiliary = type.toAuxiliaryType(hierarchy) + val classConstraint = auxiliary?.let { memory.types.evalIsSubtype(ref, it) } ?: trueExpr + mkAnd(mkNotNullOrUndefined(ref), classConstraint) + } + is EtsNullType -> mkHeapRefEq(ref, mkTsNullValue()) + is EtsUndefinedType -> mkHeapRefEq(ref, mkUndefinedValue()) + else -> trueExpr +} + /** Reading a field always produces a value; path validation belongs to [resolveField]. */ private fun TsContext.readField( scope: TsStepScope, @@ -177,6 +311,7 @@ private fun TsContext.materializeTypedStringField( value: UHeapRef, maxStringLength: Int, literal: String? = null, + activeGuard: UBoolExpr = trueExpr, ): UHeapRef? { // A prior write may have supplied an allocated literal or an already materialized string. // Keep its original reference so its existing backing array remains authoritative. @@ -187,10 +322,11 @@ private fun TsContext.materializeTypedStringField( return value } if (literal != null && literal.length > maxStringLength) { - scope.doWithState { + val initialValueIsInactive = mkNot(activeGuard) + scope.fork(initialValueIsInactive, blockOnFalseState = { terminateAsUnsupported(reason = "Literal string field exceeds configured string length $maxStringLength") - } - return null + }) ?: return null + return value } val stringRef = scope.calcOnState { makeSymbolicRefUntyped() } @@ -222,7 +358,8 @@ private fun TsContext.materializeTypedStringField( contents, ) } - scope.assert(constraints) ?: return null + val activeStringConstraints = mkImplies(activeGuard, constraints) + scope.assert(activeStringConstraints) ?: return null scope.doWithState { boundedStringBackingRefs += stringRef } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TrackedObjectProperty.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TrackedObjectProperty.kt new file mode 100644 index 0000000000..9e4208cf12 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TrackedObjectProperty.kt @@ -0,0 +1,12 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsType +import org.usvm.UHeapRef + +/** A concrete name observed on an input reference; immutable metadata is shared safely by state clones. */ +data class TrackedObjectProperty( + val instance: UHeapRef, + val name: String, + val declaredType: EtsType?, + val optional: Boolean = false, +) 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 6b9179e3e7..09150a8b55 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 @@ -28,6 +28,7 @@ import org.jacodb.ets.model.EtsDivExpr import org.jacodb.ets.model.EtsEntity import org.jacodb.ets.model.EtsEqExpr import org.jacodb.ets.model.EtsExpExpr +import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsGlobalRef import org.jacodb.ets.model.EtsGtEqExpr @@ -93,7 +94,6 @@ import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength -import org.usvm.api.makeSymbolicPrimitive import org.usvm.api.memcpy import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type @@ -378,84 +378,70 @@ class TsExprResolver( override fun visit(expr: EtsTypeOfExpr): UExpr? = with(ctx) { val arg = resolve(expr.arg) ?: return null + if (arg.sort == fp64Sort) return mkStringConstant("number", scope) + if (arg.sort == boolSort) return mkStringConstant("boolean", scope) + check(arg.sort == addressSort) { "Unsupported typeof sort: ${arg.sort}" } - if (arg.sort == fp64Sort) { - return mkStringConstant("number", scope) - } - if (arg.sort == boolSort) { - return mkStringConstant("boolean", scope) - } - if (arg.sort == addressSort) { - val ref = arg.asExpr(addressSort) - val isKnownFunction = scope.calcOnState { - val unwrappedRef = ref.unwrapRefWithPathConstraint(scope) - unwrappedRef is UConcreteHeapRef && ( - associatedFunction[unwrappedRef] != null || - memory.types.getTypeStream(unwrappedRef).singleOrNull() is EtsFunctionType - ) - } - if (isKnownFunction) { - return mkStringConstant("function", scope) - } + if (!arg.isFakeObject()) return typeOfReference(arg.asExpr(addressSort)) - return mkIte( - condition = mkHeapRefEq(ref, mkTsNullValue()), - trueBranch = mkStringConstant("object", scope), - falseBranch = mkIte( - condition = mkHeapRefEq(ref, mkUndefinedValue()), - trueBranch = mkStringConstant("undefined", scope), - falseBranch = mkIte( - condition = scope.calcOnState { - val unwrappedRef = ref.unwrapRefWithPathConstraint(scope) - - // TODO: adhoc: "expand" ITE - if (unwrappedRef is UIteExpr<*>) { - val trueBranch = unwrappedRef.trueBranch - val falseBranch = unwrappedRef.falseBranch - if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) { - val unwrappedTrueExpr = - trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) - val unwrappedFalseExpr = - falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) - return@calcOnState mkIte( - condition = unwrappedRef.condition, - trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType), - falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType), - ) - } - } + val type = arg.getFakeType(scope) + val referenceType = typeOfReference(arg.extractRef(scope)) + val numericOrReference = mkIte(type.fpTypeExpr, mkStringConstant("number", scope), referenceType) + mkIte(type.boolTypeExpr, mkStringConstant("boolean", scope), numericOrReference) + } - memory.types.evalTypeEquals(unwrappedRef, EtsStringType) - }, - trueBranch = mkStringConstant("string", scope), - falseBranch = mkStringConstant("object", scope), - ) - ) - ) + private fun typeOfReference(ref: UHeapRef): UHeapRef = with(ctx) { + if (ref is UIteExpr<*>) { + val trueType = typeOfReference(ref.trueBranch.asExpr(addressSort)) + val falseType = typeOfReference(ref.falseBranch.asExpr(addressSort)) + return mkIte(ref.condition, trueType, falseType) } - - logger.error { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + val knownFunction = scope.calcOnState { + if (ref is UConcreteHeapRef) { + associatedFunction[ref] != null || memory.types.getTypeStream(ref).singleOrNull() is EtsFunctionType + } else { + false + } + } + if (knownFunction) return mkStringConstant("function", scope) + + val isString = scope.calcOnState { memory.types.evalTypeEquals(ref, EtsStringType) } + val stringType = mkStringConstant("string", scope) + val objectType = mkStringConstant("object", scope) + val stringOrObject = mkIte(isString, stringType, objectType) + val undefinedType = mkStringConstant("undefined", scope) + val isUndefined = mkHeapRefEq(ref, mkUndefinedValue()) + val undefinedOrObject = mkIte( + condition = isUndefined, + trueBranch = undefinedType, + falseBranch = stringOrObject, + ) + mkIte(mkHeapRefEq(ref, mkTsNullValue()), objectType, undefinedOrObject) } override fun visit(expr: EtsDeleteExpr): UExpr? = with(ctx) { when (val operand = expr.arg) { is EtsInstanceFieldRef -> { val resolved = resolve(operand.instance) ?: return null - val instance = if (resolved.isFakeObject()) { + val rawInstance = if (resolved.isFakeObject()) { scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: return null resolved.extractRef(scope) } else { resolved.asExpr(addressSort) } - checkUndefinedOrNullPropertyRead(scope, instance, operand.field.name) ?: return null + checkUndefinedOrNullPropertyRead(scope, rawInstance, operand.field.name) ?: return null + val instance = resolveHeapRef(scope, rawInstance) ?: return null val prototypeFallback = prototypeFallbackReason(instance, operand) if (prototypeFallback != null) { throw UnsupportedOperationException(prototypeFallback) } + if (!isAllocatedConcreteHeapRef(instance)) { + trackInputProperty(scope, instance, operand.instance, operand.field.name, hierarchy) ?: return null + } + scope.doWithState { memory.write(deletedFieldLValue(instance, operand.field), trueExpr, guard = trueExpr) } @@ -465,7 +451,19 @@ class TsExprResolver( is EtsCastExpr -> visit(EtsDeleteExpr(arg = operand.arg)) - is EtsArrayAccess, + is EtsArrayAccess -> { + val index = resolve(operand.index) ?: return null + val propertyName = concreteStringValue(index) + ?: throw UnsupportedOperationException("Symbolic object property keys in delete are not supported") + val field = EtsFieldSignature( + enclosingClass = EtsClassSignature.UNKNOWN, + name = propertyName, + type = EtsUnknownType, + ) + val property = EtsInstanceFieldRef(instance = operand.array, field = field, type = field.type) + visit(EtsDeleteExpr(arg = property)) + } + is EtsStaticFieldRef, is EtsLocal, is EtsParameterRef, @@ -641,8 +639,8 @@ class TsExprResolver( return@resolveAfterResolved ctx.mkStringConstant(lhsString + rhsString, scope) } - val left = stringOperand(lhs, expr.left.type) - val right = stringOperand(rhs, expr.right.type) + val left = stringOperand(lhs, expr.left.type) ?: return null + val right = stringOperand(rhs, expr.right.type) ?: return null with(ctx) { val leftChars = scope.calcOnState { @@ -707,17 +705,27 @@ class TsExprResolver( return resolveBinaryOperator(TsBinaryOperator.Add, expr) } - private fun stringOperand(value: UExpr<*>, type: EtsType): UHeapRef = with(ctx) { - concreteStringValue(value)?.let { return mkStringConstant(it, scope) } - - if (!isStringOperandType(type) || value.sort != addressSort || value.isFakeObject()) { - throw UnsupportedOperationException("Unsupported string concatenation operand: $type, $value") + private fun stringOperand(value: UExpr<*>, type: EtsType): UHeapRef? = with(ctx) { + val operand = value.extractSingleValueFromFakeObjectOrNull(scope) ?: if (value.isFakeObject()) { + val referenceKind = value.getFakeType(scope).refTypeExpr + scope.fork(referenceKind, blockOnFalseState = { + terminateAsUnsupported(reason = "Unsupported string concatenation operand: $type, $value") + }) ?: return null + value.extractRef(scope) + } else { + value + } + concreteStringValue(operand)?.let { return mkStringConstant(it, scope) } + if (!isStringOperandType(type) || operand.sort != addressSort) { + throw UnsupportedOperationException("Unsupported string concatenation operand: $type, $operand") } - val ref = value.asExpr(addressSort) + + // Resolve a conditional field payload through the same forker used for property and array receivers. + val ref = resolveHeapRef(scope, operand.asExpr(addressSort)) ?: return null + concreteStringValue(ref)?.let { return mkStringConstant(it, scope) } if (scope.calcOnState { ref !in boundedStringBackingRefs }) { throw UnsupportedOperationException("String concatenation needs a modeled string backing for $ref") } - ref } @@ -727,7 +735,7 @@ class TsExprResolver( else -> false } - private fun concreteStringValue(value: UExpr<*>): String? = with(ctx) { + internal fun concreteStringValue(value: UExpr<*>): String? = with(ctx) { when { value == trueExpr -> "true" value == falseExpr -> "false" @@ -1010,19 +1018,45 @@ class TsExprResolver( override fun visit(expr: EtsInExpr): UExpr? = with(ctx) { val property = resolve(expr.left) ?: return null - val obj = resolve(expr.right)?.asExpr(addressSort) ?: return null + val resolvedObject = resolve(expr.right) ?: return null + if (resolvedObject.sort != addressSort) { + throw UnsupportedOperationException( + "The right operand of 'in' is not modeled as an object: $resolvedObject" + ) + } + val rawObject = if (resolvedObject.isFakeObject()) { + scope.assert(resolvedObject.getFakeType(scope).refTypeExpr) ?: return null + resolvedObject.extractRef(scope) + } else { + resolvedObject.asExpr(addressSort) + } - // Check for null/undefined access - checkUndefinedOrNullPropertyRead(scope, obj, propertyName = "") ?: return null + checkUndefinedOrNullPropertyRead(scope, rawObject, propertyName = "") ?: return null + val obj = resolveHeapRef(scope, rawObject) ?: return null - logger.warn { - "The 'in' operator is supported yet, the result may not be accurate" + if (expr.right is EtsLocal && expr.right.type is EtsArrayType) { + throw UnsupportedOperationException("The 'in' operator for arrays requires element presence semantics") } + val propertyName = concreteStringValue(property) + ?: throw UnsupportedOperationException("Symbolic property keys in 'in' are not supported: $property") - // For now, just return a symbolic boolean (that can be true or false) - scope.calcOnState { - makeSymbolicPrimitive(boolSort) + if (!isAllocatedConcreteHeapRef(obj)) { + val local = expr.right as? EtsLocal + val initial = trackInputProperty(scope, obj, local, propertyName, hierarchy) ?: return null + return inputPropertyPresence(scope, obj, propertyName, initial) } + + val objectClass = objectLiteralClass(scope, obj, hierarchy) + ?: throw UnsupportedOperationException("The 'in' operator requires an object literal: $obj") + scope.ensureNoPrototypeMutation(obj, objectClass) + + // Presence depends on own declarations and writes, never on the payload's value. + val wasWritten = scope.calcOnState { (obj to propertyName) in writtenConcreteFields } + val hasOwnProperty = objectClass.hasOwnProperty(propertyName) || wasWritten + val deleted = scope.calcOnState { memory.read(deletedFieldLValue(obj, propertyName)) } + ensureOwnPropertyLookup(propertyName, hasOwnProperty, deleted) + + if (hasOwnProperty) mkNot(deleted) else mkFalse() } override fun visit(expr: EtsInstanceOfExpr): UExpr? = with(ctx) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index f24700c2fe..ca0b4022f7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -3,6 +3,9 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.machine.TsContext @@ -22,13 +25,34 @@ internal fun TsExprResolver.handleAssignToArrayIndex( check(resolvedArray.sort == addressSort) { "Expected address sort for array, got: ${resolvedArray.sort}" } - val array = resolvedArray.asExpr(addressSort) + val rawArray = if (resolvedArray.isFakeObject()) { + scope.assert(resolvedArray.getFakeType(scope).refTypeExpr) ?: return null + resolvedArray.extractRef(scope) + } else { + resolvedArray.asExpr(addressSort) + } // Check for undefined or null array access. - checkUndefinedOrNullPropertyRead(scope, array, propertyName = "[]") ?: return null + checkUndefinedOrNullPropertyRead(scope, rawArray, propertyName = "[]") ?: return null + val array = resolveHeapRef(scope, rawArray) ?: return null // Resolve the index. val resolvedIndex = resolve(lhv.index) ?: return null + val receiverType = scope.calcOnState { arrayStorageType(array, lhv.array.type) } + val propertyName = concreteStringValue(resolvedIndex) + if (propertyName != null && receiverType !is EtsArrayType) { + val field = EtsFieldSignature( + name = propertyName, + enclosingClass = EtsClassSignature.UNKNOWN, + type = EtsUnknownType, + ) + assignToInstanceField(scope, lhv.array, array, field, expr, hierarchy) + return Unit + } + if (receiverType !is EtsArrayType) { + throw UnsupportedOperationException("Symbolic object property keys are not supported") + } + check(resolvedIndex.sort == fp64Sort) { "Expected fp64 sort for index, got: ${resolvedIndex.sort}" } @@ -42,12 +66,7 @@ internal fun TsExprResolver.handleAssignToArrayIndex( isSigned = true, ).asExpr(sizeSort) - val arrayType = scope.calcOnState { arrayStorageType(array, lhv.array.type) } - check(arrayType is EtsArrayType) { - "Expected EtsArrayType, got: ${lhv.array.type}" - } - - return assignToArrayIndex(scope, array, bvIndex, expr, arrayType) + return assignToArrayIndex(scope, array, bvIndex, expr, receiverType) } fun TsContext.assignToArrayIndex( 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 b23c10d385..a5e4a9b506 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 @@ -11,6 +11,7 @@ import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStaticFieldRef import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.ensureStaticsInitialized @@ -34,7 +35,7 @@ internal fun TsExprResolver.handleAssignToInstanceField( val field = lhv.field // Resolve the instance. - val instance: UHeapRef = run { + val rawInstance: UHeapRef = run { val resolved = resolve(instanceLocal) ?: return null if (resolved.isFakeObject()) { scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: run { @@ -51,7 +52,8 @@ internal fun TsExprResolver.handleAssignToInstanceField( } // Check for undefined or null field access. - checkUndefinedOrNullPropertyRead(scope, instance, field.name) ?: return null + checkUndefinedOrNullPropertyRead(scope, rawInstance, field.name) ?: return null + val instance = resolveHeapRef(scope, rawInstance) ?: return null val arrayType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } as? EtsArrayType if (field.name == "length" && arrayType != null) { @@ -138,22 +140,41 @@ fun TsContext.assignToInstanceField( hierarchy: EtsHierarchy, ) { // Unwrap to get non-fake reference. - val unwrappedInstance = instance.unwrapRef(scope) + val unwrappedInstance = resolveHeapRef(scope, instance.unwrapRef(scope)) ?: return - 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 (!isAllocatedConcreteHeapRef(unwrappedInstance) && instanceLocal.type !is EtsArrayType) { + trackInputProperty(scope, unwrappedInstance, instanceLocal, field.name, hierarchy) ?: return + writeInputPropertyValue(scope, unwrappedInstance, field.name, expr) + return + } + + val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy) + val declaredObjectLiteralField = objectLiteralClass?.fields?.singleOrNull { it.name == field.name } + val newObjectLiteralField = objectLiteralClass != null && declaredObjectLiteralField == null + + // An object literal can acquire a new own property after creation. Requiring its + // allocation type to declare the field would reject that valid JavaScript write. + if (objectLiteralClass == null) { + val fieldExists = scope.calcOnState { + val supertype = EtsAuxiliaryType(properties = setOf(field.name)) + memory.types.evalIsSubtype(unwrappedInstance, supertype) + } + scope.assert(fieldExists) ?: return } // Determine the field sort. - val sort = when (etsField) { - is TsResolutionResult.Empty -> unresolvedSort - is TsResolutionResult.Unique -> typeToSort(etsField.property.type) - is TsResolutionResult.Ambiguous -> unresolvedSort + val sort = when { + declaredObjectLiteralField != null -> typeToSort(declaredObjectLiteralField.type) + newObjectLiteralField -> { + // The receiver has no declared field. A scene-wide same-name field is unrelated. + expr.sort + } + + else -> when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) { + is TsResolutionResult.Empty -> unresolvedSort + is TsResolutionResult.Unique -> typeToSort(etsField.property.type) + is TsResolutionResult.Ambiguous -> unresolvedSort + } } // If the field type is unknown, we create a fake object for the expr and assign it. @@ -195,6 +216,12 @@ fun TsContext.assignToInstanceField( } memory.write(deletedFieldLValue(unwrappedInstance, field), falseExpr, guard = trueExpr) + if (isAllocatedConcreteHeapRef(unwrappedInstance)) { + writtenConcreteFields = writtenConcreteFields + (unwrappedInstance to field.name) + if (newObjectLiteralField) { + saveObjectLiteralFieldSort(unwrappedInstance, field.name, sort) + } + } } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 9d42276687..59a8aa3a1b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -54,6 +54,7 @@ import org.usvm.machine.call.dispatch import org.usvm.machine.expr.TsExprApproximationResult import org.usvm.machine.expr.TsExprResolver import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.expr.assignToInstanceField import org.usvm.machine.expr.checkUndefinedOrNullPropertyRead import org.usvm.machine.expr.ensureTruthinessSupported import org.usvm.machine.expr.handleAssignToArrayIndex @@ -281,7 +282,8 @@ class TsInterpreter( } val possibleTypes = scope.calcOnState { - memory.typeStreamOf(receiver).take(scene.projectAndSdkClasses.size) + // The type stream also contains the default Object type when no SDK Object is in the scene. + memory.typeStreamOf(receiver).take(scene.projectAndSdkClasses.size + 1) } if (possibleTypes !is TypesResult.SuccessfulTypesResult) { @@ -616,10 +618,17 @@ class TsInterpreter( check(instance.sort == addressSort) { "Expected address sort for the instance, got: ${instance.sort}" } - val fieldLValue = mkFieldLValue(expr.sort, instance.asExpr(addressSort), lhv.field) - scope.doWithState { - memory.write(fieldLValue, expr.cast(), guard = trueExpr) - } + val instanceRef = instance.asExpr(addressSort) + checkUndefinedOrNullPropertyRead(scope, instanceRef, propertyName = lhv.field.name) ?: return null + + assignToInstanceField( + scope = scope, + instanceLocal = lhv.instance, + instance = instanceRef, + field = lhv.field, + expr = expr, + hierarchy = exprResolver.hierarchy, + ) } } @@ -764,6 +773,7 @@ class TsInterpreter( ownership = MutabilityOwnership(), entrypoint = method, maxStringLength = options.maxArraySize, + inputPropertyPresence = options.inputPropertyPresence, targets = UTargetsSet.from(targets), ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 1d7ac99326..3a9ef594eb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -152,6 +152,19 @@ private fun TsContext.referenceOrStringValueEquals( scope: TsStepScope, activeGuard: UBoolExpr = trueExpr, ): UBoolExpr? { + if (lhs is UIteExpr<*>) { + val trueGuard = mkAnd(activeGuard, lhs.condition) + val falseGuard = mkAnd(activeGuard, mkNot(lhs.condition)) + val trueResult = referenceOrStringValueEquals(lhs.trueBranch.asExpr(addressSort), rhs, scope, trueGuard) + ?: return null + val falseResult = referenceOrStringValueEquals(lhs.falseBranch.asExpr(addressSort), rhs, scope, falseGuard) + ?: return null + return mkIte(lhs.condition, trueResult, falseResult) + } + if (rhs is UIteExpr<*>) { + return referenceOrStringValueEquals(rhs, lhs, scope, activeGuard) + } + val sameReference = mkHeapRefEq(lhs, rhs) if (sameReference.isTrue) return trueExpr @@ -787,96 +800,43 @@ sealed interface TsBinaryOperator { ): UBoolExpr? { check(lhs.isFakeObject() || rhs.isFakeObject()) - var lhsValue: UExpr<*> = lhs - var rhsValue: UExpr<*> = rhs - - val typeConstraint = when { - lhs.isFakeObject() && rhs.isFakeObject() -> { - val lhsType = lhs.getFakeType(scope) - val rhsType = rhs.getFakeType(scope) - mkAnd( - lhsType.boolTypeExpr eq rhsType.boolTypeExpr, - lhsType.fpTypeExpr eq rhsType.fpTypeExpr, - // TODO support type equality - lhsType.refTypeExpr eq rhsType.refTypeExpr, - ) - } + if (lhs.isFakeObject() && rhs.isFakeObject()) { + val leftType = lhs.getFakeType(scope) + val rightType = rhs.getFakeType(scope) + val boolGuard = mkAnd(leftType.boolTypeExpr, rightType.boolTypeExpr) + val numberGuard = mkAnd(leftType.fpTypeExpr, rightType.fpTypeExpr) + val refGuard = mkAnd(leftType.refTypeExpr, rightType.refTypeExpr) + val referenceActive = mkAnd(activeGuard, refGuard) + + val boolEqual = onBool(lhs.extractBool(scope), rhs.extractBool(scope), scope) + val numberEqual = onFp(lhs.extractFp(scope), rhs.extractFp(scope), scope) + val refEqual = onRefWithGuard(lhs.extractRef(scope), rhs.extractRef(scope), scope, referenceActive) + ?: return null + return mkOr(mkAnd(boolGuard, boolEqual), mkAnd(numberGuard, numberEqual), mkAnd(refGuard, refEqual)) + } - lhs.isFakeObject() -> { - val lhsType = lhs.getFakeType(scope) - when (rhs.sort) { - boolSort -> { - lhsValue = lhs.extractBool(scope) - lhsType.boolTypeExpr - } - - fp64Sort -> { - lhsValue = lhs.extractFp(scope) - lhsType.fpTypeExpr - } - - // TODO support type equality - addressSort -> { - lhsValue = lhs.extractRef(scope) - lhsType.refTypeExpr - } - - else -> error("Unsupported sort ${rhs.sort}") - } + val fake = if (lhs.isFakeObject()) lhs else rhs + val ordinary = if (lhs.isFakeObject()) rhs else lhs + check(fake.isFakeObject()) + val type = fake.getFakeType(scope) + return when (ordinary.sort) { + boolSort -> { + val equal = onBool(fake.extractBool(scope), ordinary.asExpr(boolSort), scope) + mkAnd(type.boolTypeExpr, equal) } - - rhs.isFakeObject() -> { - val rhsType = rhs.getFakeType(scope) - when (lhs.sort) { - boolSort -> { - rhsValue = rhs.extractBool(scope) - rhsType.boolTypeExpr - } - - fp64Sort -> { - rhsValue = rhs.extractFp(scope) - rhsType.fpTypeExpr - } - - // TODO support type equality - addressSort -> { - rhsValue = rhs.extractRef(scope) - rhsType.refTypeExpr - } - - else -> error("Unsupported sort ${lhs.sort}") - } + fp64Sort -> { + val equal = onFp(fake.extractFp(scope), ordinary.asExpr(fp64Sort), scope) + mkAnd(type.fpTypeExpr, equal) } - - else -> { - error("Should not be called") + addressSort -> { + val referenceActive = mkAnd(activeGuard, type.refTypeExpr) + val fakeRef = fake.extractRef(scope) + val ordinaryRef = ordinary.asExpr(addressSort) + val equal = onRefWithGuard(fakeRef, ordinaryRef, scope, referenceActive) ?: return null + mkAnd(type.refTypeExpr, equal) } + else -> error("Unsupported strict equality sort: ${ordinary.sort}") } - - check(!lhsValue.isFakeObject()) { "Nested fake objects are not supported" } - check(!rhsValue.isFakeObject()) { "Nested fake objects are not supported" } - - // Note: this is the case 'ref === ref', - // which should be `true` only if both have the same reference. - // It is not correct to delegate to `Eq.resolve` in this case, - // since `==` treats `null == undefined`, while `null !== undefined`. - if (lhsValue.sort == addressSort && rhsValue.sort == addressSort) { - val left = lhsValue.asExpr(addressSort) - val right = rhsValue.asExpr(addressSort) - val lhsRefGuard = if (lhs.isFakeObject()) lhs.getFakeType(scope).refTypeExpr else trueExpr - val rhsRefGuard = if (rhs.isFakeObject()) rhs.getFakeType(scope).refTypeExpr else trueExpr - val refComparisonGuard = mkAnd(activeGuard, typeConstraint, lhsRefGuard, rhsRefGuard) - return mkAnd( - typeConstraint, - onRefWithGuard(left, right, scope, refComparisonGuard) ?: return null - ) - } - - val looseEqualityConstraint = with(Eq) { - resolve(lhsValue, rhsValue, scope, activeGuard)?.asExpr(boolSort) ?: return null - } - - return mkAnd(typeConstraint, looseEqualityConstraint) } override fun TsContext.internalResolve( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index c5b244ee33..f3ec36b48f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -25,6 +25,8 @@ import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.constraints.UPathConstraints import org.usvm.machine.TsContext +import org.usvm.machine.TsInputPropertyPresence +import org.usvm.machine.expr.TrackedObjectProperty import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsFunction import org.usvm.memory.ULValue @@ -48,6 +50,7 @@ class TsState( ownership: MutabilityOwnership, override val entrypoint: EtsMethod, val maxStringLength: Int, + val inputPropertyPresence: TsInputPropertyPresence = TsInputPropertyPresence.DECLARED_FIELDS, callStack: UCallStack = UCallStack(), pathConstraints: UPathConstraints = UPathConstraints(ctx, ownership), memory: UMemory = UMemory(ctx, ownership, pathConstraints.typeConstraints), @@ -90,6 +93,9 @@ class TsState( /** Unresolved reference payloads that may acquire string backing after type refinement. */ var symbolicStringCandidates: Set = emptySet(), var unsupportedReason: String? = null, + var trackedObjectProperties: Set = emptySet(), + var writtenConcreteFields: Set> = emptySet(), + var writtenObjectLiteralFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, @@ -128,6 +134,10 @@ class TsState( localToSortStack[localToSortStack.lastIndex] = updated } + fun saveObjectLiteralFieldSort(ref: UHeapRef, fieldName: String, sort: USort) { + writtenObjectLiteralFieldSorts = writtenObjectLiteralFieldSorts.put(ref to fieldName, sort, ownership) + } + fun pushLocalToSortStack() { localToSortStack.add(persistentHashMapOf()) } @@ -303,6 +313,7 @@ class TsState( ownership = cloneOwnership, entrypoint = entrypoint, maxStringLength = maxStringLength, + inputPropertyPresence = inputPropertyPresence, callStack = callStack.clone(), pathConstraints = clonedConstraints, memory = memory.clone(clonedConstraints.typeConstraints, newThisOwnership, cloneOwnership), @@ -327,6 +338,9 @@ class TsState( boundedStringBackingRefs = boundedStringBackingRefs, symbolicStringCandidates = symbolicStringCandidates, unsupportedReason = unsupportedReason, + trackedObjectProperties = trackedObjectProperties, + writtenConcreteFields = writtenConcreteFields, + writtenObjectLiteralFieldSorts = writtenObjectLiteralFieldSorts, activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsObjectType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsObjectType.kt new file mode 100644 index 0000000000..773f289b71 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsObjectType.kt @@ -0,0 +1,11 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsRefType +import org.jacodb.ets.model.EtsType + +/** Internal runtime-object supertype: class instances, arrays and functions, excluding primitive payloads. */ +internal data object EtsObjectType : EtsRefType { + override val typeName: String get() = "RuntimeObject" + + override fun accept(visitor: EtsType.Visitor): R = error("Internal runtime type") +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index cefcc35885..b167374f86 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -52,6 +52,9 @@ class TsTypeSystem( val unwrappedSupertype = unwrapAlias(supertype) val unwrappedType = unwrapAlias(type) + // Runtime object checks exclude primitive and nullish values, independently of TS assignability. + if (unwrappedSupertype == EtsObjectType) return unwrappedType is EtsRefType + // In JS/TS, any reference type inherits from Object if (unwrappedSupertype is EtsClassType && unwrappedSupertype.signature == EtsHierarchy.OBJECT_CLASS.signature @@ -217,6 +220,7 @@ class TsTypeSystem( override fun hasCommonSubtype(type: EtsType, types: Collection): Boolean { val t = unwrapAlias(type) return when (t) { + EtsObjectType -> true is EtsNominalType -> true is EtsAuxiliaryType -> true // structural types can always be refined is EtsPrimitiveType -> types.isEmpty() // primitive has no subtypes, so only when no other constraints @@ -284,6 +288,8 @@ class TsTypeSystem( .plus(sequenceOf(EtsNumberType, EtsBooleanType, EtsStringType)) } + EtsObjectType -> scene.projectAndSdkClasses.asSequence().map { it.type } + is EtsAuxiliaryType -> { scene.projectAndSdkClasses .asSequence() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt index 9e77ec7776..b28b8fe3ee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt @@ -4,6 +4,7 @@ import io.ksmt.sort.KFp64Sort import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.machine.TsContext /** * A read-only snapshot of payloads and kind selectors, without a heap identity or allocation. @@ -15,3 +16,22 @@ data class TsUnresolvedValue( val refValue: UHeapRef, val type: EtsFakeType, ) + +/** Join both payloads and kind selectors without allocating wrapper identities for either branch. */ +internal fun TsContext.iteUnresolvedValue( + condition: UBoolExpr, + trueValue: TsUnresolvedValue, + falseValue: TsUnresolvedValue, +): TsUnresolvedValue { + val type = EtsFakeType( + boolTypeExpr = mkIte(condition, trueValue.type.boolTypeExpr, falseValue.type.boolTypeExpr), + fpTypeExpr = mkIte(condition, trueValue.type.fpTypeExpr, falseValue.type.fpTypeExpr), + refTypeExpr = mkIte(condition, trueValue.type.refTypeExpr, falseValue.type.refTypeExpr), + ) + return TsUnresolvedValue( + boolValue = mkIte(condition, trueValue.boolValue, falseValue.boolValue), + fpValue = mkIte(condition, trueValue.fpValue, falseValue.fpValue), + refValue = mkIte(condition, trueValue.refValue, falseValue.refValue), + type = type, + ) +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt index 2e699edffc..af2cb291a0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt @@ -1,20 +1,52 @@ package org.usvm.machine.types +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFieldImpl import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnknownType import org.junit.jupiter.api.Test import org.usvm.util.EtsHierarchy import org.usvm.util.type +import kotlin.test.assertFalse import kotlin.test.assertTrue import kotlin.time.Duration.Companion.seconds class TsTypeSystemTest { + @Test + fun `runtime object constraint accepts references and excludes primitive or unresolved types`() { + val scene = EtsScene(projectFiles = emptyList()) + val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, hierarchy = EtsHierarchy(scene)) + val references = listOf( + EtsHierarchy.OBJECT_CLASS, + EtsArrayType(EtsNumberType, dimensions = 1), + EtsTupleType(emptyList()), + ) + val nonObjects = listOf( + EtsStringType, + EtsNumberType, + EtsBooleanType, + EtsNullType, + EtsUndefinedType, + EtsAnyType, + EtsUnknownType, + ) + + references.forEach { assertTrue(typeSystem.isSupertype(EtsObjectType, it), it.typeName) } + nonObjects.forEach { assertFalse(typeSystem.isSupertype(EtsObjectType, it), it.typeName) } + } + @Test fun `auxiliary type is a subtype of a class containing its properties`() { val fileSignature = EtsFileSignature(projectName = "test", fileName = "types.ts") diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/InOperatorFieldCollisionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/InOperatorFieldCollisionTest.kt new file mode 100644 index 0000000000..c319c4ad60 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/InOperatorFieldCollisionTest.kt @@ -0,0 +1,25 @@ +package org.usvm.samples.operators + +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.util.eq + +class InOperatorFieldCollisionTest : PropertyTestRunner("/samples/operators/InOperatorFieldCollision.ts") { + @Test + fun `own fields retain their actual sort despite unrelated declarations`() { + val methods = listOf( + "numericFieldWithStringCollision", "writtenStringField", "declaredStringField", + "run", "declaredProperty", "reassignedProperty", + ) + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "Probe") + + discoverProperties( + method = method, + { result -> result eq 7 }, + invariants = arrayOf({ result -> result eq 7 }), + ) + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/InOperatorPresenceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/InOperatorPresenceTest.kt new file mode 100644 index 0000000000..7ea90bed48 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/InOperatorPresenceTest.kt @@ -0,0 +1,134 @@ +package org.usvm.samples.operators + +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.util.eq +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class InOperatorPresenceTest : PropertyTestRunner("/samples/operators/InOperator.ts") { + @Test + fun `in checks own field presence through writes and deletion`() { + val methods = listOf( + "hasPresentNumberProperty", + "hasUndefinedProperty", + "lacksProperty", + "lacksOptionalProperty", + "hasOwnConstructorMethod", + "hasAddedProperty", + "lacksDeletedProperty", + "hasRestoredProperty", + ) + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "InOperator") + + discoverProperties( + method = method, + { _, result -> result eq 1 }, + invariants = arrayOf({ _, result -> result eq 1 }), + ) + } + } + + @Test + fun `conditional deletion preserves both presence outcomes`() { + val method = getMethod(methodName = "conditionalDelete", className = "InOperator") + + discoverProperties( + method = method, + { shouldDelete, result -> shouldDelete.value && (result eq 0) }, + { shouldDelete, result -> !shouldDelete.value && (result eq 1) }, + invariants = arrayOf({ shouldDelete, result -> result eq (if (shouldDelete.value) 0 else 1) }), + ) + } + + @Test + fun `added field remains readable after presence check`() { + val methodName = "readsAddedProperty" + val method = getMethod(methodName = methodName, className = "InOperator") + + discoverProperties( + method = method, + { input, result -> result eq input }, + invariants = arrayOf({ input, result -> result eq input }), + ) + } + + @Test + fun `absent optional field reads as undefined after negative presence check`() { + val methodName = "readsMissingOptionalAfterIn" + val method = getMethod(methodName = methodName, className = "InOperator") + + discoverProperties( + method = method, + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `block scoped top level write updates field presence`() { + val methodName = "readsBlockScopedResult" + val method = getMethod(methodName = methodName, className = "InOperator") + + discoverProperties( + method = method, + { result -> result eq 7 }, + invariants = arrayOf({ result -> result eq 7 }), + ) + } + + @Test + fun `unmodeled keys arrays and prototypes have explicit unsupported outcomes`() { + val methods = listOf( + "hasSymbolicKey", + "testInOperatorObject", + "testInOperatorArray", + "testInOperatorObjectAfterDelete", + "specialPrototypeInitializer", + "inheritedThroughPrototypeInitializer", + "inheritedThroughAssignedPrototype", + "deletedToStringExposesPrototype", + "inheritedConstructor", + ) + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "InOperator") + val outcome = TsMachine( + scene = scene, + options = options.copy(throwExceptionOnStepFailure = false), + tsOptions = tsOptions, + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), methodName) + assertTrue(outcome.unsupportedPaths.isNotEmpty(), methodName) + if (methodName.endsWith("PrototypeInitializer") || methodName == "inheritedThroughAssignedPrototype") { + assertTrue(outcome.unsupportedPaths.any { "prototype mutation" in it }, + "${outcome.unsupportedPaths}") + } + if (methodName == "deletedToStringExposesPrototype" || methodName == "inheritedConstructor") { + assertTrue(outcome.unsupportedPaths.any { it.contains("prototype lookup", ignoreCase = true) }, + "${outcome.unsupportedPaths}") + } + } + + replayPrototypeInitializer() + } + + private fun replayPrototypeInitializer() { + val assertions = + "if (new InOperator().specialPrototypeInitializer() !== false) throw Error('null prototype');\n" + + "if (new InOperator().inheritedThroughPrototypeInitializer() !== true) throw Error('inherited');\n" + + "if (new InOperator().inheritedThroughAssignedPrototype() !== true) throw Error('assigned prototype');\n" + + "if (new InOperator().deletedToStringExposesPrototype() !== true) throw Error('revealed prototype');\n" + + "if (new InOperator().inheritedConstructor() !== true) throw Error('inherited constructor');\n" + + replayInOperatorScript(directory, sourcePath, scriptName = "specialPrototypeInitializer", assertions = assertions) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/PropertyTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/PropertyTestRunner.kt new file mode 100644 index 0000000000..7dc80fa938 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/PropertyTestRunner.kt @@ -0,0 +1,137 @@ +package org.usvm.samples.operators + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.io.TempDir +import org.usvm.StateCollectionStrategy +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.TsCompatibilityUnknownCallDispatcher +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import java.util.IdentityHashMap +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** Property discovery and Node replay consume the same exhaustive analysis and witness snapshots. */ +abstract class PropertyTestRunner(protected val sourcePath: String) : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + override val scene: EtsScene = loadScene(sourcePath) + + init { + options = options.copy( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + throwExceptionOnStepFailure = true, + ) + } + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + val outcome = TsMachine( + scene = scene, + options = options, + tsOptions = tsOptions, + unknownCallDispatcher = TsCompatibilityUnknownCallDispatcher, + ).use { it.analyzeWithOutcome(methods = listOf(method)) } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, method.name) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${method.name}: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), method.name) + val tests = outcome.states.map { state -> + assertIs(state.methodResult, method.name) + TsTestResolver().resolve(method, state) + } + replay(method, tests) + tests + } + + private fun replay(method: EtsMethod, tests: List) { + val assertions = buildString { + tests.forEachIndexed { index, test -> + appendLine("{") + val serializer = ReplayObjects(this) + val args = test.before.parameters.map { serializer.value(it) } + appendLine("const actual = new ${method.enclosingClass!!.name}().${method.name}(${args.joinToString()});") + val expected = serializer.value(test.returnValue) + appendLine("if (!same(actual, $expected)) throw Error('${method.name} result $index');") + test.after.parameters.forEachIndexed { argIndex, after -> + val expectedAfter = serializer.value(after) + appendLine("if (!same(${args[argIndex]}, $expectedAfter)) throw Error('${method.name} input $argIndex state $index');") + } + appendLine("}") + } + } + val equals = """ + function same(a, b) { + if (Object.is(a, b)) return true; + if (a === null || b === null || typeof a !== 'object' || typeof b !== 'object') return false; + const ka = Object.keys(a), kb = Object.keys(b); + return ka.length === kb.length && ka.every(k => Object.hasOwn(b, k) && same(a[k], b[k])); + } + """.trimIndent() + + replayInOperatorScript(directory, sourcePath, method.name, "$equals\n$assertions") + } + + private class ReplayObjects(private val script: StringBuilder) { + private val objects = IdentityHashMap() + + fun value(value: TsTestValue): String = when (value) { + is TsTestValue.TsBoolean -> value.value.toString() + is TsTestValue.TsNumber -> when { + value.number.isNaN() -> "NaN" + value.number == Double.POSITIVE_INFINITY -> "Infinity" + value.number == Double.NEGATIVE_INFINITY -> "-Infinity" + else -> value.number.toString() + } + is TsTestValue.TsString -> jsString(value.value) + TsTestValue.TsUndefined -> "undefined" + TsTestValue.TsNull -> "null" + is TsTestValue.TsClass -> objects[value] ?: run { + val ref = "obj${objects.size}" + objects[value] = ref + script.appendLine("const $ref = {};") + value.properties.forEach { (key, field) -> + val payload = value(field) + script.appendLine("Object.defineProperty($ref, ${jsString(key)}, {value: $payload, writable: true, enumerable: true, configurable: true});") + } + ref + } + is TsTestValue.TsArray<*> -> "[${value.values.joinToString { value(it) }}]" + else -> error("Unsupported replay value: $value") + } + } +} + +internal fun replayInOperatorScript( + directory: Path, + sourcePath: String, + scriptName: String, + assertions: String, +) { + val source = buildString { + appendLine(getResourcePath(sourcePath).readText()) + append(assertions) + } + + assertNodeReplay( + source = source, + directory = directory, + name = scriptName, + timeoutMessage = "Node replay timed out: $scriptName", + ) +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/SymbolicPropertiesTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/SymbolicPropertiesTest.kt new file mode 100644 index 0000000000..9373fd0986 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/SymbolicPropertiesTest.kt @@ -0,0 +1,204 @@ +package org.usvm.samples.operators + +import org.junit.jupiter.api.Test +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsInputPropertyPresence +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.eq +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class SymbolicPropertiesTest : PropertyTestRunner("/samples/operators/SymbolicProperties.ts") { + override val tsOptions: TsOptions = TsOptions(maxArraySize = 8) + + @Test + fun `required fields exist and optional or unknown fields have both initial possibilities`() { + checkSingleInput(name = "required", expected = setOf(1)) + checkSingleInput(name = "inheritedFields", expected = setOf(1)) + checkSingleInput(name = "optional", expected = setOf(0, 1)) + checkSingleInput(name = "unknown", expected = setOf(0, 1)) + checkSingleInput(name = "repeatedPresence", expected = setOf(1)) + checkSingleInput(name = "absentRead", expected = setOf(1, 2)) + checkSingleInput(name = "readsUnknown", expected = setOf(0, 1, 2, 3)) + checkSingleInput(name = "comparesUnknownValues", expected = setOf(0, 1, 2)) + } + + @Test + fun `literal payloads can be added and their runtime kind can change`() { + val methods = listOf( + "writesNumber", "writesBoolean", "writesString", "writesUndefined", "writesNull", + "writesObject", "writesArray", "changesDeclaredKind", "changesKinds", "bracketLiteral", "nestedInput", + "deletesBracketLiteral", "numericLiteralKey", "lengthProperty", "unusualKeys", "rewritesLongLiteral", + ) + + methods.forEach { checkSingleInput(it, expected = setOf(1)) } + } + + @Test + fun `deletion restoration and local aliases agree with reads and presence`() { + listOf("deletes", "deletesUnknown", "restores", "localAlias", "deletesLongLiteral").forEach { + checkSingleInput(it, expected = setOf(1)) + } + } + + @Test + fun `conditional writes deletes and kind changes remain branch independent`() { + listOf("conditionalWrite", "conditionalDelete", "conditionalKinds").forEach { name -> + val method = getMethod(methodName = name, className = "SymbolicProperties") + + val trueResult = if (name == "conditionalDelete") 0 else 1 + val falseResult = 1 - trueResult + + discoverProperties( + method = method, + { _, flag, result -> flag.value && result eq trueResult }, + { _, flag, result -> !flag.value && result eq falseResult }, + invariants = arrayOf({ _, flag, result -> result eq if (flag.value) trueResult else falseResult }), + ) + } + } + + @Test + fun `distinct and aliased symbolic receivers share only matching heap updates`() { + listOf("aliasWrite", "aliasKindChange", "aliasDelete", "aliasStringChange", "aliasObjectChange", "aliasArrayChange").forEach { name -> + val method = getMethod(methodName = name, className = "SymbolicProperties") + + discoverProperties( + method = method, + { _, _, result -> result eq 0 }, + { _, _, result -> result eq 1 }, + invariants = arrayOf({ _, _, result -> result eq 0 || result eq 1 }), + ) + } + } + + @Test + fun `symbolic payload writes do not force input field capability`() { + val name = "writesSymbolic" + val method = getMethod(methodName = name, className = "SymbolicProperties") + + discoverProperties( + method = method, + { _, value, result -> !value.number.isNaN() && result eq 1 }, + { _, value, result -> value.number.isNaN() && result eq -1 }, + invariants = arrayOf({ _, value, result -> result eq if (value.number.isNaN()) -1 else 1 }), + ) + } + + @Test + fun `symbolic boolean string reference and unknown payloads preserve their values`() { + listOf("writesSymbolicBoolean", "writesSymbolicString", "writesSymbolicObject", "copiesUnknown").forEach { name -> + val method = getMethod(methodName = name, className = "SymbolicProperties") + + discoverProperties( + method = method, + { _, _, result -> result eq 1 }, + invariants = arrayOf({ _, _, result -> result eq 1 }), + ) + } + } + + @Test + fun `optional string presence guards string backing constraints`() { + checkSingleInput(name = "optionalUndefinedPresence", expected = setOf(0, 1, 2)) + checkSingleInput(name = "optionalString", expected = setOf(0, 1, 2, 3)) + } + + @Test + fun `returned object snapshots include additions and omit deletions`() { + listOf("returnsWrittenObject", "returnsDeletedObject").forEach { name -> + val method = getMethod(methodName = name, className = "SymbolicProperties") + + discoverProperties( + method = method, + { _, result -> if (name == "returnsWrittenObject") "fresh" in result.properties else "x" !in result.properties }, + invariants = arrayOf({ _, result -> + if (name == "returnsWrittenObject") "fresh" in result.properties else "x" !in result.properties + }), + ) + } + } + + @Test + fun `symbolic keys and inherited prototype names remain explicit unsupported outcomes`() { + listOf("symbolicKey", "prototypeName").forEach { name -> + val method = getMethod(methodName = name, className = "SymbolicProperties") + val options = options.copy(throwExceptionOnStepFailure = false) + val outcome = TsMachine(scene, options = options, tsOptions = tsOptions).use { + it.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty(), name) + assertTrue(outcome.unsupportedPaths.isNotEmpty(), name) + } + } + + private fun checkSingleInput(name: String, expected: Set) { + val method = getMethod(methodName = name, className = "SymbolicProperties") + val matchers: Array<(TsTestValue, TsTestValue.TsNumber) -> Boolean> = expected.map { number -> + { _: TsTestValue, result: TsTestValue.TsNumber -> result eq number } + }.toTypedArray() + + discoverProperties( + method = method, + analysisResultMatchers = matchers, + invariants = arrayOf({ _: TsTestValue, result: TsTestValue.TsNumber -> result.number.toInt() in expected }), + ) + } +} + +class SymbolicPropertyPresenceModesTest : PropertyTestRunner("/samples/operators/SymbolicProperties.ts") { + private var policy = TsInputPropertyPresence.DECLARED_FIELDS + override val tsOptions: TsOptions get() = TsOptions(inputPropertyPresence = policy) + + @Test + fun `explicit policies affect initial presence but writes and deletions override them`() { + val expectedRequired = mapOf( + TsInputPropertyPresence.DECLARED_FIELDS to setOf(1), + TsInputPropertyPresence.SYMBOLIC to setOf(0, 1), + TsInputPropertyPresence.ASSUME_PRESENT to setOf(1), + TsInputPropertyPresence.ASSUME_ABSENT to setOf(0), + ) + + expectedRequired.forEach { (mode, expected) -> + policy = mode + val method = getMethod(methodName = "required", className = "SymbolicProperties") + val matchers: Array<(TsTestValue, TsTestValue.TsNumber) -> Boolean> = expected.map { number -> + { _: TsTestValue, result: TsTestValue.TsNumber -> result eq number } + }.toTypedArray() + + discoverProperties( + method = method, + analysisResultMatchers = matchers, + invariants = arrayOf({ _: TsTestValue, result: TsTestValue.TsNumber -> result.number.toInt() in expected }), + ) + val expectedUnknown = when (mode) { + TsInputPropertyPresence.ASSUME_PRESENT -> setOf(1) + TsInputPropertyPresence.ASSUME_ABSENT -> setOf(0) + else -> setOf(0, 1) + } + listOf("optional", "unknown").forEach { name -> + val initialMatchers: Array<(TsTestValue, TsTestValue.TsNumber) -> Boolean> = expectedUnknown.map { number -> + { _: TsTestValue, result: TsTestValue.TsNumber -> result eq number } + }.toTypedArray() + discoverProperties( + method = getMethod(methodName = name, className = "SymbolicProperties"), + analysisResultMatchers = initialMatchers, + invariants = arrayOf({ _: TsTestValue, result: TsTestValue.TsNumber -> + result.number.toInt() in expectedUnknown + }), + ) + } + listOf("writesUndefined", "deletes", "restores").forEach { name -> + discoverProperties( + method = getMethod(methodName = name, className = "SymbolicProperties"), + { _, result -> result eq 1 }, + invariants = arrayOf({ _, result -> result eq 1 }), + ) + } + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt index 4d550e4ae7..63abaf7f31 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt @@ -3,6 +3,7 @@ package org.usvm.samples.types import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.RepeatedTest import org.junit.jupiter.api.Test +import org.usvm.StateCollectionStrategy import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner import org.usvm.util.eq @@ -66,62 +67,39 @@ class TypeStream : TsMethodTestRunner() { } @RepeatedTest(10, failureThreshold = 1) - fun `use unique field`() { - val method = getMethod("useUniqueField") - discoverProperties( - method = method, - { x, r -> - x as TsTestValue.TsClass - r as TsTestValue.TsNumber - (r eq 1) && x.name == "FirstChild" - }, - invariants = arrayOf( - { x, _ -> - if (x is TsTestValue.TsClass) { - x.name == "FirstChild" - } else true - }, - { _, r -> - if (r is TsTestValue.TsNumber) { - r eq 1 - } else true - }, - ) - ) + fun `reading an undeclared unique field does not narrow the nominal receiver type`() { + checkDynamicFieldRead(methodName = "useUniqueField") } @RepeatedTest(10, failureThreshold = 1) - fun `use non unique field`() { - val method = getMethod("useNonUniqueField") - discoverProperties( - method = method, - { x, r -> - x as TsTestValue.TsClass - r as TsTestValue.TsNumber - (r eq 1) && x.name == "FirstChild" - }, - { x, r -> - x as TsTestValue.TsClass - r as TsTestValue.TsNumber - (r eq 2) && x.name == "SecondChild" - }, - { x, r -> - x as TsTestValue.TsClass - r as TsTestValue.TsNumber - (r eq 3) && x.name == "Parent" - }, - invariants = arrayOf( - { _, r -> - if (r is TsTestValue.TsNumber) { - r.number in listOf(1.0, 2.0, 3.0) - } else true - }, - { _, r -> + fun `reading a shared field preserves every compatible nominal receiver type`() { + checkDynamicFieldRead(methodName = "useNonUniqueField") + } + + private fun checkDynamicFieldRead(methodName: String) { + val method = getMethod(methodName) + val exhaustive = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL, stopOnCoverage = 0) + + withOptions(exhaustive) { + discoverProperties( + method = method, + { x, r -> x is TsTestValue.TsClass && x.name == "FirstChild" && r is TsTestValue.TsNumber && r eq 1 }, + { x, r -> x is TsTestValue.TsClass && x.name == "SecondChild" && r is TsTestValue.TsNumber && r eq 2 }, + { x, r -> x is TsTestValue.TsClass && x.name == "Parent" && r is TsTestValue.TsNumber && r eq 3 }, + { x, r -> x == TsTestValue.TsUndefined && r is TsTestValue.TsException }, + invariants = arrayOf({ x, r -> if (r is TsTestValue.TsNumber) { - r neq -1 - } else true - }, + x is TsTestValue.TsClass && when (x.name) { + "FirstChild" -> r eq 1 + "SecondChild" -> r eq 2 + "Parent" -> r eq 3 + else -> false + } + } else { + (x == TsTestValue.TsUndefined || x == TsTestValue.TsNull) && r is TsTestValue.TsException + } + }), ) - ) + } } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt index 6da4e92b79..ee7d788e82 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt @@ -42,6 +42,8 @@ abstract class TsMethodTestRunner : TestRunner List = { method, options -> - val tsMachineOptions = TsOptions() TsMachine( scene, options, - tsMachineOptions, + tsOptions, unknownCallDispatcher = TsCompatibilityUnknownCallDispatcher, ).use { machine -> val states = machine.analyze(listOf(method)) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index ef0f1c60d7..3ddbe5bc3c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -40,17 +40,21 @@ import org.usvm.isAllocated import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue import org.usvm.machine.TsContext +import org.usvm.machine.expr.TrackedObjectProperty import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.expr.deletedFieldLValue import org.usvm.machine.expr.extractDouble import org.usvm.machine.expr.extractInt +import org.usvm.machine.expr.initialPropertyPresenceLValue +import org.usvm.machine.expr.readInputPropertyValue import org.usvm.machine.expr.toConcreteBoolValue +import org.usvm.machine.expr.writtenPropertyLValue import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory import org.usvm.mkSizeExpr -import org.usvm.model.UModel import org.usvm.model.UModelBase import org.usvm.sizeSort import org.usvm.types.first @@ -73,7 +77,8 @@ class TsTestResolver { memory, method, resolvedLValuesToFakeObjects, - state.maxStringLength + state.maxStringLength, + propertyState = state, ) val afterMemoryScope = MemoryScope( this, @@ -81,7 +86,8 @@ class TsTestResolver { memory, method, resolvedLValuesToFakeObjects, - state.maxStringLength + state.maxStringLength, + propertyState = state, ) val result = when (val res = state.methodResult) { @@ -177,7 +183,16 @@ class TsTestResolver { method: EtsMethod, resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, maxStringLength: Int, - ) : TsTestStateResolver(ctx, model, finalStateMemory, method, resolvedLValuesToFakeObjects, maxStringLength) { + propertyState: TsState, + ) : TsTestStateResolver( + ctx = ctx, + model = model, + finalStateMemory = finalStateMemory, + method = method, + resolvedLValuesToFakeObjects = resolvedLValuesToFakeObjects, + maxStringLength = maxStringLength, + propertyState = propertyState, + ) { fun resolveState(): TsParametersState { val thisInstance = resolveThisInstance() val parameters = resolveParameters() @@ -194,7 +209,10 @@ open class TsTestStateResolver( val method: EtsMethod, val resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, val maxStringLength: Int, + private val propertyState: TsState? = null, ) { + private val resolvedClasses = hashMapOf() + fun resolveLValue( lValue: ULValue<*, *>, ): TsTestValue { @@ -236,6 +254,7 @@ open class TsTestStateResolver( heapRef: UExpr, ): TsTestValue { val concreteRef = evaluateInModel(heapRef) as UConcreteHeapRef + if (with(ctx) { concreteRef.isFakeObject() }) return resolveFakeObject(concreteRef) if (concreteRef.address == 0) { return TsTestValue.TsUndefined @@ -487,6 +506,8 @@ open class TsTestStateResolver( concreteRef: UConcreteHeapRef, heapRef: UHeapRef, ): TsTestValue.TsClass = with(ctx) { + resolvedClasses[concreteRef]?.let { return it } + val type = if (concreteRef.isAllocated) { finalStateMemory.typeStreamOf(concreteRef).first() } else { @@ -494,43 +515,100 @@ open class TsTestStateResolver( } check(type is EtsRefType) { "Expected EtsRefType, but got $type" } val clazz = resolveClass(type) - val properties = clazz.fields - .filterNot { field -> - field as EtsFieldImpl - field.modifiers.isStatic + val properties = linkedMapOf() + val result = TsTestValue.TsClass(clazz.name, properties) + resolvedClasses[concreteRef] = result + + val tracked = propertyState?.trackedObjectProperties.orEmpty() + .filter { evaluateInModel(it.instance) == concreteRef } + .groupBy { it.name } + val declaredFields = clazz.fields.filterNot { (it as EtsFieldImpl).modifiers.isStatic } + declaredFields.forEach { field -> + if (field.name in tracked) return@forEach + if ((field as EtsFieldImpl).isOptional && !concreteRef.isAllocated) return@forEach + if (resolveMode == ResolveMode.CURRENT && + model.eval(finalStateMemory.read(deletedFieldLValue(heapRef, field.name))).isTrue + ) { + return@forEach } - .associate { field -> - val sort = typeToSort(field.type) - if (sort == unresolvedSort) { - val lValue = mkFieldLValue(addressSort, heapRef, field.signature) - val fakeObject = if (memory is UModel) { - resolvedLValuesToFakeObjects.firstOrNull { it.first == lValue }?.second - } else { - resolvedLValuesToFakeObjects.lastOrNull { it.first == lValue }?.second - } + properties[field.name] = resolveObjectField(concreteRef, heapRef, field.name, field.type) + } + tracked.forEach { (name, entries) -> + val entry = entries.firstOrNull { it.declaredType != null } ?: entries.first() + resolveTrackedProperty(concreteRef, entry)?.let { properties[name] = it } + } + if (resolveMode == ResolveMode.CURRENT) applyConcreteWrites(properties, concreteRef, heapRef) - if (fakeObject != null) { - val obj = resolveFakeObject(fakeObject) - field.name to obj - } else { - val fieldExpr = finalStateMemory.read(lValue) as? UConcreteHeapRef - ?: error("UnresolvedSort should be represented by a fake object instance") - // TODO check values if fieldExpr is correct here - // Probably we have to pass fieldExpr as symbolic value and something as a concrete one - val obj = resolveExpr(fieldExpr) - field.name to obj - } - } else { - val lValue = mkFieldLValue(sort, concreteRef.asExpr(addressSort), field.signature) - val fieldExpr = memory.read(lValue) - // TODO check values if fieldExpr is correct here - // Probably we have to pass fieldExpr as symbolic value and something as a concrete one - val obj = resolveExpr(fieldExpr) - field.name to obj - } + result + } + + private fun resolveTrackedProperty(ref: UConcreteHeapRef, entry: TrackedObjectProperty): TsTestValue? = with(ctx) { + val name = entry.name + val propertyRef = entry.instance + val initialPresence = model.eval(model.read(initialPropertyPresenceLValue(ref, name))).isTrue + val written = resolveMode == ResolveMode.CURRENT && + model.eval(finalStateMemory.read(writtenPropertyLValue(propertyRef, name))).isTrue + val deleted = resolveMode == ResolveMode.CURRENT && + model.eval(finalStateMemory.read(deletedFieldLValue(propertyRef, name))).isTrue + if ((!initialPresence && !written) || deleted) return null + + val declaredType = entry.declaredType + val sort = declaredType?.let { typeToSort(it) } ?: unresolvedSort + if (!written && sort !is TsUnresolvedSort && !entry.optional) { + return resolveObjectField(ref, ref, name, declaredType!!, initial = true) + } + + val valueMemory = if (written) finalStateMemory else model + val valueRef = if (written) propertyRef else ref + val value = readInputPropertyValue(valueMemory, valueRef, name, written) + when { + model.eval(value.type.boolTypeExpr).isTrue -> resolveExpr(value.boolValue) + model.eval(value.type.fpTypeExpr).isTrue -> resolveExpr(value.fpValue) + model.eval(value.type.refTypeExpr).isTrue -> resolveExpr(value.refValue) + else -> TsTestValue.TsUndefined // A property whose value was never read is unconstrained. + } + } + + private fun applyConcreteWrites( + properties: MutableMap, + ref: UConcreteHeapRef, + heapRef: UHeapRef, + ) = with(ctx) { + propertyState?.writtenConcreteFields.orEmpty().filter { it.first == ref }.forEach { (_, name) -> + if (model.eval(finalStateMemory.read(deletedFieldLValue(heapRef, name))).isTrue) { + properties.remove(name) + } else if (name !in properties) { + val sort = propertyState?.writtenObjectLiteralFieldSorts?.get(ref to name) ?: addressSort + properties[name] = resolveLValue(mkFieldLValue(sort, heapRef, name)) } - TsTestValue.TsClass(clazz.name, properties) + } + } + + private fun resolveObjectField( + ref: UConcreteHeapRef, + heapRef: UHeapRef, + name: String, + type: EtsType, + initial: Boolean = false, + ): TsTestValue = with(ctx) { + val sort = typeToSort(type) + val valueMemory = if (initial) model else memory + val valueRef = if (initial || resolveMode == ResolveMode.MODEL) ref else heapRef + if (sort !is TsUnresolvedSort) { + return resolveExpr(valueMemory.read(mkFieldLValue(sort, valueRef, name))) + } + + val lValue = mkFieldLValue(addressSort, ref, name) + val fakeObject = if (resolveMode == ResolveMode.MODEL) { + resolvedLValuesToFakeObjects.firstOrNull { it.first == lValue }?.second + } else { + resolvedLValuesToFakeObjects.lastOrNull { it.first == lValue }?.second + } + if (fakeObject != null) return resolveFakeObject(fakeObject) + + // Unread fields can be concretized to undefined. Evaluating also recognizes symbolic wrapper branches. + resolveExpr(valueMemory.read(mkFieldLValue(addressSort, valueRef, name))) } internal var resolveMode: ResolveMode = ResolveMode.ERROR diff --git a/usvm-ts/src/test/resources/samples/operators/InOperator.ts b/usvm-ts/src/test/resources/samples/operators/InOperator.ts index ba87e91ff5..5a9e4f1df8 100644 --- a/usvm-ts/src/test/resources/samples/operators/InOperator.ts +++ b/usvm-ts/src/test/resources/samples/operators/InOperator.ts @@ -1,7 +1,116 @@ // @ts-nocheck // noinspection JSUnusedGlobalSymbols +let blockScopedResult = 0; +{ + let obj = {}; + obj.x = 7; + blockScopedResult = "x" in obj ? 7 : 0; +} + class InOperator { + readsBlockScopedResult(): number { + return blockScopedResult; + } + + hasPresentNumberProperty(value: number): number { + const obj = { x: value }; + if ("x" in obj) return 1; + return -1; + } + + hasUndefinedProperty(value: number): number { + const obj = { x: undefined, y: value }; + if ("x" in obj) return 1; + return -1; + } + + lacksProperty(value: number): number { + const obj = { x: value }; + if ("missing" in obj) return -1; + return 1; + } + + lacksOptionalProperty(value: number): number { + const obj: { x?: number } = {}; + return "x" in obj ? -1 : 1; + } + + hasOwnConstructorMethod(value: number): number { + const obj = { constructor() {} }; + return "constructor" in obj ? 1 : -1; + } + + hasAddedProperty(value: number): number { + const obj: { x?: number } = {}; + obj.x = value; + return "x" in obj ? 1 : -1; + } + + readsAddedProperty(value: number): number { + const obj = {}; + obj.x = value; + if (!("x" in obj)) return -1; + return obj.x; + } + + readsMissingOptionalAfterIn(): number { + const obj: { x?: number } = {}; + if ("x" in obj) return 0; + return obj.x === undefined ? 1 : -1; + } + + lacksDeletedProperty(value: number): number { + const obj = { x: value }; + delete obj.x; + return "x" in obj ? -1 : 1; + } + + hasRestoredProperty(value: number): number { + const obj = { x: value }; + delete obj.x; + obj.x = value; + return "x" in obj ? 1 : -1; + } + + conditionalDelete(shouldDelete: boolean): number { + const obj = { x: 1 }; + if (shouldDelete) delete obj.x; + return "x" in obj ? 1 : 0; + } + + specialPrototypeInitializer(): boolean { + const obj = { __proto__: null }; + return "__proto__" in obj; + } + + inheritedThroughPrototypeInitializer(): boolean { + const obj = { __proto__: { inherited: 1 } }; + return "inherited" in obj; + } + + inheritedThroughAssignedPrototype(): boolean { + const obj = {}; + obj.__proto__ = { inherited: 1 }; + return "inherited" in obj; + } + + deletedToStringExposesPrototype(): boolean { + const obj = { toString: 1 }; + delete obj.toString; + return "toString" in obj; + } + + inheritedConstructor(): boolean { + const obj = {}; + return "constructor" in obj; + } + + hasSymbolicKey(key: string): boolean { + const obj = { x: 1 }; + return key in obj; + } + testInOperatorObject(): number { let obj = { x: 42, y: undefined }; diff --git a/usvm-ts/src/test/resources/samples/operators/InOperatorFieldCollision.ts b/usvm-ts/src/test/resources/samples/operators/InOperatorFieldCollision.ts new file mode 100644 index 0000000000..347b840375 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/InOperatorFieldCollision.ts @@ -0,0 +1,52 @@ +// @ts-nocheck + +let result = 0; +{ + let obj = {}; + obj.x = 7; + result = "x" in obj ? obj.x : 0; +} + +class Other { + x: boolean = false; +} + +class OtherString { + shadowedNumber: string = "unrelated"; +} + +class Probe { + numericFieldWithStringCollision(): number { + const obj = {}; + obj.shadowedNumber = 7; + return "shadowedNumber" in obj ? obj.shadowedNumber : 0; + } + + writtenStringField(): number { + const obj = {}; + obj.y = "1234567"; + return "y" in obj ? obj.y.length : 0; + } + + declaredStringField(): number { + const obj = { y: "1234567" }; + return "y" in obj ? obj.y.length : 0; + } + + run(): number { + return result; + } + + declaredProperty(): number { + const obj = { x: 1 }; + obj.x = 7; + return obj.x; + } + + reassignedProperty(): number { + const obj = {}; + obj.x = false; + obj.x = 7; + return obj.x; + } +} diff --git a/usvm-ts/src/test/resources/samples/operators/SymbolicProperties.ts b/usvm-ts/src/test/resources/samples/operators/SymbolicProperties.ts new file mode 100644 index 0000000000..b696028284 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/SymbolicProperties.ts @@ -0,0 +1,303 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class UnrelatedPropertyOwner { + fresh: string; +} + +class PropertyBase { + inherited: number; + redeclared?: string; +} + +class PropertyChild extends PropertyBase { + redeclared: string; +} + +class SymbolicProperties { + inheritedFields(obj: PropertyChild): number { + return "inherited" in obj && "redeclared" in obj && obj.redeclared !== undefined ? 1 : -1; + } + + required(obj: { x: number }): number { + return "x" in obj ? 1 : 0; + } + + optional(obj: { x?: number }): number { + return "x" in obj ? 1 : 0; + } + + unknown(obj: Object): number { + return "fresh" in obj ? 1 : 0; + } + + repeatedPresence(obj: Object): number { + const before = "fresh" in obj; + return before === ("fresh" in obj) ? 1 : -1; + } + + absentRead(obj: { x?: number }): number { + if ("x" in obj) return 2; + return obj.x === undefined ? 1 : -1; + } + + readsUnknown(obj: Object): number { + if (!("fresh" in obj)) return obj.fresh === undefined ? 0 : -1; + if (typeof obj.fresh === "number") return 1; + if (typeof obj.fresh === "boolean") return 2; + return 3; + } + + writesNumber(obj: Object): number { + obj.fresh = 42; + return "fresh" in obj && obj.fresh === 42 ? 1 : -1; + } + + writesBoolean(obj: Object): number { + obj.fresh = false; + return "fresh" in obj && obj.fresh === false ? 1 : -1; + } + + writesString(obj: Object): number { + obj.fresh = "hello"; + return "fresh" in obj && obj.fresh === "hello" && obj.fresh.length === 5 ? 1 : -1; + } + + rewritesLongLiteral(obj: { text: "initial value exceeds the length bound" }): number { + obj.text = "short"; + return "text" in obj && obj.text === "short" ? 1 : -1; + } + + deletesLongLiteral(obj: { text: "initial value exceeds the length bound" }): number { + delete obj.text; + return !("text" in obj) && obj.text === undefined ? 1 : -1; + } + + writesUndefined(obj: Object): number { + obj.fresh = undefined; + return "fresh" in obj && obj.fresh === undefined ? 1 : -1; + } + + writesNull(obj: Object): number { + obj.fresh = null; + return "fresh" in obj && obj.fresh === null ? 1 : -1; + } + + writesObject(obj: Object): number { + obj.fresh = { nested: 7 }; + return "fresh" in obj && obj.fresh.nested === 7 ? 1 : -1; + } + + writesArray(obj: Object): number { + obj.fresh = [4, 0]; + obj.fresh[1] = 8; + return "fresh" in obj && obj.fresh[1] === 8 ? 1 : -1; + } + + changesDeclaredKind(obj: { x: number }): number { + obj.x = "changed"; + return "x" in obj && obj.x === "changed" ? 1 : -1; + } + + changesKinds(obj: Object): number { + obj.fresh = 1; + if (obj.fresh !== 1) return -1; + obj.fresh = true; + if (obj.fresh !== true) return -2; + obj.fresh = "a"; + if (obj.fresh !== "a") return -3; + obj.fresh = undefined; + return "fresh" in obj && obj.fresh === undefined ? 1 : -4; + } + + deletes(obj: { x: number }): number { + delete obj.x; + return !("x" in obj) && obj.x === undefined ? 1 : -1; + } + + deletesUnknown(obj: Object): number { + delete obj.fresh; + return !("fresh" in obj) && obj.fresh === undefined ? 1 : -1; + } + + restores(obj: Object): number { + obj.fresh = 1; + delete obj.fresh; + if ("fresh" in obj || obj.fresh !== undefined) return -1; + obj.fresh = "restored"; + return "fresh" in obj && obj.fresh === "restored" ? 1 : -2; + } + + conditionalWrite(obj: Object, write: boolean): number { + delete obj.fresh; + if (write) obj.fresh = 7; + if ("fresh" in obj) return obj.fresh === 7 ? 1 : -1; + return obj.fresh === undefined ? 0 : -2; + } + + conditionalDelete(obj: { x: number }, remove: boolean): number { + if (remove) delete obj.x; + if ("x" in obj) return 1; + return obj.x === undefined ? 0 : -1; + } + + conditionalKinds(obj: Object, flag: boolean): number { + if (flag) obj.fresh = 3; + else obj.fresh = "s"; + if (!("fresh" in obj)) return -1; + return flag ? (obj.fresh === 3 ? 1 : -2) : (obj.fresh === "s" ? 0 : -3); + } + + localAlias(obj: Object): number { + const alias = obj; + alias.fresh = 9; + if (!("fresh" in obj) || obj.fresh !== 9) return -1; + delete obj.fresh; + return !("fresh" in alias) && alias.fresh === undefined ? 1 : -2; + } + + aliasWrite(a: Object, b: Object): number { + delete b.fresh; + a.fresh = 13; + if (a === b) return "fresh" in b && b.fresh === 13 ? 1 : -1; + return !("fresh" in b) && b.fresh === undefined ? 0 : -2; + } + + aliasStringChange(a: Object, b: Object): number { + delete b.fresh; + a.fresh = "alias"; + if (a !== b) return 0; + return "fresh" in b && b.fresh === "alias" && b.fresh.length === 5 ? 1 : -1; + } + + aliasObjectChange(a: Object, b: Object): number { + delete b.fresh; + a.fresh = { nested: 7, length: 2 }; + if (a !== b) return 0; + if (!("nested" in b.fresh) || b.fresh["nested"] !== 7 || b.fresh.length !== 2) return -1; + b.fresh.nested = 8; + if (a.fresh.nested !== 8) return -2; + delete b.fresh["nested"]; + if ("nested" in a.fresh || a.fresh.nested !== undefined) return -3; + a.fresh.nested = 9; + return "nested" in b.fresh && b.fresh.nested === 9 ? 1 : -4; + } + + aliasArrayChange(a: Object, b: Object): number { + delete b.fresh; + a.fresh = [4, 0]; + if (a !== b) return 0; + b.fresh[1] = 8; + return "fresh" in b && a.fresh[1] === 8 ? 1 : -1; + } + + lengthProperty(obj: Object): number { + obj.length = 7; + if (!("length" in obj) || obj.length !== 7) return -1; + delete obj.length; + return !("length" in obj) && obj.length === undefined ? 1 : -2; + } + + unusualKeys(obj: Object): number { + obj[""] = 1; + obj["поле😀"] = false; + return "" in obj && "поле😀" in obj && obj[""] === 1 && obj["поле😀"] === false ? 1 : -1; + } + + aliasKindChange(a: { x: number }, b: { x: number }): number { + if (a !== b) return 0; + a.x = false; + return "x" in b && b.x === false ? 1 : -1; + } + + aliasDelete(a: { x: number }, b: { x: number }): number { + delete a.x; + if (a === b) return !("x" in b) && b.x === undefined ? 1 : -1; + return "x" in b ? 0 : -2; + } + + writesSymbolic(obj: Object, value: number): number { + obj.fresh = value; + return "fresh" in obj && obj.fresh === value ? 1 : -1; + } + + writesSymbolicBoolean(obj: Object, value: boolean): number { + obj.fresh = value; + return "fresh" in obj && obj.fresh === value ? 1 : -1; + } + + writesSymbolicString(obj: Object, value: string): number { + obj.fresh = value; + return "fresh" in obj && obj.fresh === value && obj.fresh.length === value.length ? 1 : -1; + } + + writesSymbolicObject(obj: Object, value: { x: number }): number { + obj.fresh = value; + obj.fresh.x = 8; + return "fresh" in obj && obj.fresh === value && value.x === 8 ? 1 : -1; + } + + copiesUnknown(a: Object, b: Object): number { + a.copy = b.fresh; + return "copy" in a && (a.copy === b.fresh || a.copy !== a.copy) ? 1 : -1; + } + + bracketLiteral(obj: Object): number { + obj["a-b"] = 21; + return "a-b" in obj && obj["a-b"] === 21 ? 1 : -1; + } + + deletesBracketLiteral(obj: Object): number { + obj["a-b"] = undefined; + if (!("a-b" in obj)) return -1; + delete obj["a-b"]; + return !("a-b" in obj) && obj["a-b"] === undefined ? 1 : -2; + } + + numericLiteralKey(obj: Object): number { + obj[12] = "v"; + if (!(12 in obj) || obj[12] !== "v") return -1; + delete obj[12]; + return !("12" in obj) ? 1 : -2; + } + + comparesUnknownValues(obj: Object): number { + const value = obj.fresh; + if (typeof value === "number") return value === obj.fresh ? 1 : 2; + return value === obj.fresh ? 0 : -1; + } + + nestedInput(obj: { inner: { x: number } }): number { + obj.inner.fresh = 5; + return "fresh" in obj.inner && obj.inner.fresh === 5 ? 1 : -1; + } + + optionalUndefinedPresence(obj: { x?: number }): number { + if (!("x" in obj)) return obj.x === undefined ? 0 : -1; + return obj.x === undefined ? 1 : 2; + } + + optionalString(obj: { text?: string }): number { + if (!("text" in obj)) return obj.text === undefined ? 0 : -1; + if (obj.text === undefined) return 3; + return obj.text === "hi" ? 1 : 2; + } + + returnsWrittenObject(obj: Object): Object { + obj.fresh = { x: 7 }; + return obj; + } + + returnsDeletedObject(obj: { x: number }): Object { + delete obj.x; + return obj; + } + + prototypeName(obj: Object): number { + return "toString" in obj ? 1 : 0; + } + + symbolicKey(obj: Object, key: string): number { + return key in obj ? 1 : 0; + } +}