diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeletedFieldLValue.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeletedFieldLValue.kt new file mode 100644 index 0000000000..61266499e9 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/DeletedFieldLValue.kt @@ -0,0 +1,86 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsFieldSignature +import org.usvm.UBoolExpr +import org.usvm.UBoolSort +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.machine.TsContext +import org.usvm.memory.UFlatUpdates +import org.usvm.memory.ULValue +import org.usvm.memory.UMemoryRegion +import org.usvm.memory.UMemoryRegionId +import org.usvm.memory.UMemoryUpdatesVisitor +import org.usvm.memory.USymbolicCollectionUpdates +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( + override val sort: UBoolSort, + override val key: UHeapRef, + val name: String, +) : ULValue { + override val memoryRegionId: UMemoryRegionId = DeletedFieldRegionId(name, sort) +} + +private data class DeletedFieldRegionId( + val name: String, + override val sort: UBoolSort, +) : UMemoryRegionId { + override fun emptyRegion(): UMemoryRegion = DeletedFieldRegion(sort) +} + +/** The marker records execution events, so input references also start with no deletion. */ +private class DeletedFieldRegion( + private val sort: UBoolSort, + private val updates: USymbolicCollectionUpdates = UFlatUpdates(UHeapRefKeyInfo), +) : UMemoryRegion { + override fun read(key: UHeapRef): UBoolExpr { + val ctx = sort.uctx + val visitor = object : UMemoryUpdatesVisitor { + override fun visitSelect(result: UBoolExpr, key: UHeapRef): UBoolExpr = result + + override fun visitInitialValue(): UBoolExpr = ctx.falseExpr + + override fun visitUpdate(previous: UBoolExpr, update: UUpdateNode): UBoolExpr { + val guard = update.includesSymbolically(key, composer = null) + val value = update.value(key, composer = null) + + return ctx.mkIte(guard, value, previous) + } + } + + return updates.read(key, composer = null).accept(visitor, lookupCache = hashMapOf()) + } + + override fun write( + key: UHeapRef, + value: UExpr, + guard: UBoolExpr, + ownership: MutabilityOwnership, + ): UMemoryRegion = DeletedFieldRegion(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) 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 7cc1a9b381..043645e385 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 @@ -17,10 +17,13 @@ import org.usvm.USort import org.usvm.USymbolicHeapRef import org.usvm.api.evalTypeEquals import org.usvm.api.makeSymbolicRefUntyped +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.iteWriteIntoFakeObject import org.usvm.machine.types.mkFakeValue import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult @@ -77,6 +80,9 @@ private fun TsContext.resolveField( ): UExpr<*>? { checkNotFake(instance) + 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 -> { @@ -104,20 +110,31 @@ private fun TsContext.resolveField( scope.assert(fieldExists) ?: return null val value = readField(scope, instance, field, sort) - if (resolvedField !is TsResolutionResult.Unique || sort is TsUnresolvedSort) return value - - val maxStringLength = scope.calcOnState { maxStringLength } - return when (val fieldType = resolvedField.property.type) { - is EtsStringLiteralType -> materializeTypedStringField( - scope = scope, - value = value.asExpr(addressSort), - literal = fieldType.value, - maxStringLength = maxStringLength, - ) + 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 + is EtsStringType -> materializeTypedStringField(scope, value.asExpr(addressSort), maxStringLength) + else -> value + } ?: return null } + + if (deleted.isFalse) return materializedValue + + return iteWriteIntoFakeObject( + scope = scope, + condition = deleted, + trueBranchValue = mkUndefinedValue(), + falseBranchValue = materializedValue, + ) } /** Reading a field always produces a value; path validation belongs to [resolveField]. */ 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 0bf3bbab14..6b9179e3e7 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 @@ -18,7 +18,9 @@ import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsCastExpr import org.jacodb.ets.model.EtsCaughtExceptionRef +import org.jacodb.ets.model.EtsClassCategory import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsClosureFieldRef import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -121,6 +123,8 @@ import org.usvm.sizeSort import org.usvm.types.singleOrNull import org.usvm.util.EtsHierarchy import org.usvm.util.SymbolResolutionResult +import org.usvm.util.arrayStorageType +import org.usvm.util.getAllMethods import org.usvm.util.isResolved import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue @@ -435,42 +439,76 @@ class TsExprResolver( } override fun visit(expr: EtsDeleteExpr): UExpr? = with(ctx) { - logger.warn { - "delete operator is not fully supported, the result may not be accurate" - } - - // The delete operator removes a property from an object and returns true/false - // For property access like "delete obj.prop", we need to handle EtsInstanceFieldRef when (val operand = expr.arg) { is EtsInstanceFieldRef -> { - val instance = resolve(operand.instance)?.asExpr(addressSort) ?: return null + val resolved = resolve(operand.instance) ?: return null + val instance = if (resolved.isFakeObject()) { + scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: return null + resolved.extractRef(scope) + } else { + resolved.asExpr(addressSort) + } - // Check for null/undefined access checkUndefinedOrNullPropertyRead(scope, instance, operand.field.name) ?: return null - // For now, we simulate deletion by setting the property to undefined - // This is a simplification of the real semantics but sufficient for basic cases - // TODO: This is incorrect for cases that the existing field is not of sort Address. - // In such case, the "overwriting" the field value with undefined does nothing - // to the actual number/boolean/string value inside the field, - // [if only we read the field using that "other" sort]. - val fieldLValue = mkFieldLValue(addressSort, instance, operand.field) + val prototypeFallback = prototypeFallbackReason(instance, operand) + if (prototypeFallback != null) { + throw UnsupportedOperationException(prototypeFallback) + } + scope.doWithState { - memory.write(fieldLValue, mkUndefinedValue(), guard = trueExpr) + memory.write(deletedFieldLValue(instance, operand.field), trueExpr, guard = trueExpr) } - // The delete operator returns true in most cases for property deletion mkTrue() } + is EtsCastExpr -> visit(EtsDeleteExpr(arg = operand.arg)) + + is EtsArrayAccess, + is EtsStaticFieldRef, + is EtsLocal, + is EtsParameterRef, + is EtsGlobalRef, + is EtsClosureFieldRef, + is EtsCaughtExceptionRef, + -> { + resolve(operand) ?: return null + throw UnsupportedOperationException("Deleting ${operand::class.simpleName} is not supported") + } + else -> { - // For other operands (like variables), delete typically returns true without effect - resolve(operand) ?: return null // Evaluate for potential side effects + resolve(operand) ?: return null mkTrue() } } } + private fun prototypeFallbackReason(instance: UHeapRef, operand: EtsInstanceFieldRef): String? { + val name = operand.field.name + if (name in OBJECT_PROTOTYPE_PROPERTIES) { + return "Deleting '$name' requires unsupported Object.prototype lookup" + } + + val receiverType = scope.calcOnState { arrayStorageType(instance, operand.instance.type) } + if (receiverType is EtsArrayType) { + if (name == "length") { + return "Deleting Array.length is not supported" + } + + return "Deleting a named Array property requires unsupported Array.prototype lookup" + } + + if (receiverType !is EtsClassType) return null + + val inheritedMethod = hierarchy.classesForType(receiverType) + .asSequence() + .filter { clazz -> clazz.category != EtsClassCategory.OBJECT } + .flatMap { clazz -> clazz.getAllMethods(hierarchy).asSequence() } + .any { method -> !method.isStatic && method.name == name } + return if (inheritedMethod) "Deleting '$name' requires unsupported class prototype method lookup" else null + } + override fun visit(expr: EtsVoidExpr): UExpr? = with(ctx) { // The void operator evaluates its operand for side effects and returns undefined. resolve(expr.arg) ?: return null diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 2a465cc790..b23c10d385 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 @@ -193,6 +193,8 @@ fun TsContext.assignToInstanceField( memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr) } } + + memory.write(deletedFieldLValue(unwrappedInstance, field), falseExpr, guard = trueExpr) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/DeleteProperty.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/DeleteProperty.kt new file mode 100644 index 0000000000..f9cf673eb9 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/DeleteProperty.kt @@ -0,0 +1,394 @@ +package org.usvm.samples.operators + +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.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.eq +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class DeleteProperty : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + override val scene: EtsScene = loadScene("/samples/operators/DeleteProperty.ts") + + @Test + fun `number property reads as undefined after delete`() { + val method = getMethod("readAfterDelete") + + discoverProperties( + method = method, + { _, result -> result == TsTestValue.TsUndefined }, + invariants = arrayOf({ _, result -> result == TsTestValue.TsUndefined }), + ) + } + + @Test + fun `delete example exhausts paths without interpreter failure`() { + val method = getMethod("readAfterDelete") + val options = UMachineOptions( + stopOnCoverage = 0, + timeout = Duration.INFINITE, + throwExceptionOnStepFailure = true, + ) + + val result = TsMachine(scene, options, TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason) + assertTrue(result.states.isNotEmpty()) + } + + @Test + fun `boolean property reads as undefined after delete`() { + val method = getMethod("deleteBoolean") + + discoverProperties( + method, + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `typed number property reads as undefined after delete`() { + val method = getMethod("deleteTypedNumber") + + discoverProperties( + method, + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `reference property reads as undefined after delete`() { + val method = getMethod("deleteReference") + + discoverProperties( + method, + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `alias observes delete`() { + val method = getMethod("aliasSeesDelete") + + discoverProperties( + method, + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `reassignment restores deleted property`() { + val method = getMethod("restoreAfterDelete") + + discoverProperties( + method, + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `deleting missing property succeeds`() { + val method = getMethod("deleteMissing") + + discoverProperties( + method, + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `conditional delete preserves both read outcomes`() { + val method = getMethod("readAfterConditionalDelete") + + discoverProperties( + method = method, + { shouldDelete, result -> shouldDelete.value && (result eq 1) }, + { shouldDelete, result -> !shouldDelete.value && (result eq 2) }, + invariants = arrayOf({ shouldDelete, result -> result eq (if (shouldDelete.value) 1 else 2) }), + ) + + val options = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + + val analysis = TsMachine(scene, options, TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), "${analysis.unsupportedPaths}") + assertEquals(setOf(false, true), tests.map { test -> + assertIs(test.before.parameters.single()).value + }.toSet()) + tests.forEach { test -> + val shouldDelete = assertIs(test.before.parameters.single()).value + val result = assertIs(test.returnValue).number.toInt() + assertEquals(if (shouldDelete) 1 else 2, result, "$test") + } + } + + @Test + fun `typed string property can be deleted and restored`() { + val method = getMethod("deleteAndRestoreString") + + discoverProperties( + method = method, + { _, result -> result eq 1 }, + invariants = arrayOf({ _, result -> result eq 1 }), + ) + } + + @Test + fun `conditional string delete preserves the untouched value`() { + val method = getMethod("conditionalDeleteString") + + discoverProperties( + method = method, + { _, shouldDelete, result -> shouldDelete.value && (result eq 1) }, + { _, shouldDelete, result -> !shouldDelete.value && (result eq 2) }, + invariants = arrayOf({ _, shouldDelete, result -> result eq (if (shouldDelete.value) 1 else 2) }), + ) + } + + @Test + fun `deleting a property of an input object reads as undefined`() { + discoverProperties( + method = getMethod("deleteInput"), + { _, result -> result eq 1 }, + invariants = arrayOf({ _, result -> result eq 1 }), + ) + } + + @Test + fun `input property is not marked deleted before any delete`() { + discoverProperties( + method = getMethod("untouchedInput"), + { _, result -> result eq 1 }, + invariants = arrayOf({ _, result -> result eq 1 }), + ) + } + + @Test + fun `input alias observes delete and reassignment restores the field`() { + for (name in listOf("deleteInputAlias", "restoreInput")) { + discoverProperties( + method = getMethod(name), + { _, result -> result eq 1 }, + invariants = arrayOf({ _, result -> result eq 1 }), + ) + } + } + + @Test + fun `conditional input deletion preserves both paths`() { + discoverProperties( + method = getMethod("conditionalDeleteInput"), + { _, shouldDelete, result -> shouldDelete.value && (result eq 1) }, + { _, shouldDelete, result -> !shouldDelete.value && (result eq 2) }, + invariants = arrayOf({ _, shouldDelete, result -> result eq (if (shouldDelete.value) 1 else 2) }), + ) + } + + @Test + fun `delete affects aliased inputs and preserves a distinct receiver`() { + discoverProperties( + method = getMethod("deletePossiblyAliasedInputs"), + { _, _, result -> result eq 1 }, + { _, _, result -> result eq 2 }, + invariants = arrayOf({ _, _, result -> (result eq 1) || (result eq 2) }), + ) + } + + @Test + fun `deleting a value expression returns true`() { + discoverProperties( + method = getMethod("deleteValueExpression"), + { _, result -> result.value }, + invariants = arrayOf({ _, result -> result.value }), + ) + } + + @Test + fun `deleting an assignment expression preserves its side effect`() { + discoverProperties( + method = getMethod("deleteAssignmentExpression"), + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `type assertion on a value preserves delete semantics`() { + discoverProperties( + method = getMethod("deleteCastedValue"), + { result -> result eq 1 }, + invariants = arrayOf({ result -> result eq 1 }), + ) + } + + @Test + fun `type assertion losing a property reference reports unsupported`() { + val method = getMethod("deleteCastedField") + val options = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + + val analysis = TsMachine(scene, options, TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.states.isEmpty()) + assertTrue(analysis.unsupportedPaths.any { "Deleting EtsLocal" in it }) + } + + @Test + fun `input deletion and value operand witnesses replay in Node`() { + val names = listOf( + "deleteInput", "untouchedInput", "deleteInputAlias", "restoreInput", "conditionalDeleteInput", + "deleteValueExpression", "deleteAssignmentExpression", "deleteCastedValue", + ) + val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL, stopOnCoverage = 0) + val tests = names.associateWith { name -> runner(getMethod(name), options) } + + fun serialize(value: TsTestValue): String = when (value) { + is TsTestValue.TsClass -> value.properties.entries.joinToString(prefix = "{", postfix = "}") { (name, field) -> + "${jsString(name)}: ${serialize(field)}" + } + + is TsTestValue.TsNumber -> value.number.toString() + is TsTestValue.TsBoolean -> value.value.toString() + is TsTestValue.TsString -> jsString(value.value) + TsTestValue.TsUndefined -> "undefined" + else -> error("Unsupported replay value: $value") + } + + val script = buildString { + appendLine(getResourcePath("/samples/operators/DeleteProperty.ts").readText()) + tests.forEach { (name, generated) -> + assertTrue(generated.isNotEmpty(), "$name produced no witnesses") + + generated.forEachIndexed { index, test -> + val arguments = test.before.parameters.joinToString { value -> serialize(value) } + val expected = serialize(test.returnValue) + + appendLine("if (new DeleteProperty().$name($arguments) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "delete-input-witnesses", + timeoutMessage = "Input deletion replay timed out", + failureContext = script.take(n = 1000), + ) + } + + @Test + fun `deleting an own property with a prototype fallback reports unsupported outcome`() { + val method = getMethod("deleteOwnToString") + val options = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + + val analysis = TsMachine(scene, options, TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.states.isEmpty()) + assertTrue(analysis.unsupportedPaths.any { "Object.prototype lookup" in it }) + } + + @Test + fun `deleting prototype methods reports unsupported while own field remains supported`() { + val options = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + val prototypeMethod = getMethod("deletePrototypeMethod") + val arrayMethod = getMethod("deleteArrayPrototypeMethod") + val ownField = getMethod("deleteClassOwnField") + val ownMethod = getMethod("deleteObjectLiteralMethod") + + val analyses = TsMachine(scene, options, TsOptions()).use { machine -> + listOf(prototypeMethod, arrayMethod, ownField, ownMethod).map { method -> + method to machine.analyzeWithOutcome(methods = listOf(method)) + }.toMap() + } + val methodAnalysis = analyses.getValue(prototypeMethod) + val arrayAnalysis = analyses.getValue(arrayMethod) + val fieldAnalysis = analyses.getValue(ownField) + val ownMethodAnalysis = analyses.getValue(ownMethod) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, methodAnalysis.stopReason) + assertTrue(methodAnalysis.states.isEmpty()) + assertTrue(methodAnalysis.unsupportedPaths.any { "class prototype method" in it }) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, arrayAnalysis.stopReason) + assertTrue(arrayAnalysis.states.isEmpty()) + assertTrue(arrayAnalysis.unsupportedPaths.any { "Array.prototype lookup" in it }) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, fieldAnalysis.stopReason) + assertTrue(fieldAnalysis.unsupportedPaths.isEmpty()) + val fieldResult = fieldAnalysis.states.single().let { state -> TsTestResolver().resolve(ownField, state) } + assertEquals(1.0, assertIs(fieldResult.returnValue).number) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, ownMethodAnalysis.stopReason) + assertTrue(ownMethodAnalysis.unsupportedPaths.isEmpty()) + val ownMethodResult = ownMethodAnalysis.states.single().let { state -> TsTestResolver().resolve(ownMethod, state) } + assertEquals(1.0, assertIs(ownMethodResult.returnValue).number) + + val script = buildString { + appendLine(getResourcePath("/samples/operators/DeleteProperty.ts").readText()) + appendLine("if (new DeleteProperty().deletePrototypeMethod() !== 0) throw Error('prototype method');") + appendLine("if (new DeleteProperty().deleteArrayPrototypeMethod() !== 0) throw Error('array prototype');") + appendLine("if (new DeleteProperty().deleteClassOwnField() !== 1) throw Error('own field');") + appendLine("if (new DeleteProperty().deleteObjectLiteralMethod() !== 1) throw Error('own method');") + } + assertNodeReplay( + source = script, + directory = directory, + name = "delete-prototype-method", + timeoutMessage = "Node replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/operators/DeleteProperty.ts b/usvm-ts/src/test/resources/samples/operators/DeleteProperty.ts new file mode 100644 index 0000000000..e7ebcc54a2 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/DeleteProperty.ts @@ -0,0 +1,186 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class DeleteMethodSubject { + ownValue: number = 5; + + method(): number { + return 7; + } +} + +class DeleteProperty { + readAfterDelete(value: number): number | undefined { + const object: { x?: number } = { x: value }; + delete object.x; + return object.x; + } + + deleteTypedNumber(): number { + const object: { x: number } = { x: 5 }; + delete object.x; + return object.x === undefined ? 1 : 0; + } + + deleteBoolean(): number { + const object: { flag: boolean } = { flag: true }; + delete object.flag; + return object.flag === undefined ? 1 : 0; + } + + deleteReference(): number { + const object: { nested: object } = { nested: { value: 1 } }; + delete object.nested; + return object.nested === undefined ? 1 : 0; + } + + aliasSeesDelete(): number { + const object: { x?: number } = { x: 2 }; + const alias = object; + delete alias.x; + + return object.x === undefined ? 1 : 0; + } + + restoreAfterDelete(): number { + const object: { x?: number } = { x: 2 }; + delete object.x; + + object.x = 3; + return object.x === 3 ? 1 : 0; + } + + deleteMissing(): number { + const object: { x?: number } = {}; + const result = delete object.x; + return result === true && object.x === undefined ? 1 : 0; + } + + readAfterConditionalDelete(shouldDelete: boolean): number { + const object: { x?: number } = { x: 5 }; + if (shouldDelete) { + delete object.x; + } + + return object.x === undefined ? 1 : 2; + } + + deleteAndRestoreString(value: string): number { + const object: { value: string } = { value }; + delete object.value; + if (object.value !== undefined) return 0; + + object.value = value; + return object.value === value ? 1 : 0; + } + + conditionalDeleteString(value: string, shouldDelete: boolean): number { + const object: { value: string } = { value }; + if (shouldDelete) { + delete object.value; + } + + if (shouldDelete) return object.value === undefined ? 1 : 0; + return object.value === value ? 2 : 0; + } + + deleteInput(object: { x?: number }): number { + delete object.x; + return object.x === undefined ? 1 : 0; + } + + untouchedInput(object: { x: boolean }): number { + return object.x === undefined ? 0 : 1; + } + + deleteInputAlias(object: { x?: number }): number { + const alias = object; + delete alias.x; + + return object.x === undefined ? 1 : 0; + } + + restoreInput(object: { x?: number }): number { + delete object.x; + if (object.x !== undefined) return 0; + + object.x = 7; + return object.x === 7 ? 1 : 0; + } + + conditionalDeleteInput(object: { x: boolean }, shouldDelete: boolean): number { + const original = object.x; + if (shouldDelete) { + delete object.x; + } + + if (shouldDelete) return object.x === undefined ? 1 : 0; + return object.x === original ? 2 : 0; + } + + deletePossiblyAliasedInputs(first: { x: boolean }, second: { x: boolean }): number { + if (first === second) { + delete first.x; + return second.x === undefined ? 1 : 0; + } + + const original = second.x; + delete first.x; + return second.x === original ? 2 : 0; + } + + deleteValueExpression(value: number): boolean { + return delete (value + 1); + } + + deleteAssignmentExpression(): number { + const object = { value: 0 }; + const result = delete (object.value = 1); + + return result === true && object.value === 1 ? 1 : 0; + } + + deleteCastedField(): number { + const object = { value: 1 }; + delete (object.value as any); + + return object.value === undefined ? 1 : 0; + } + + deleteCastedValue(): number { + const object = { value: 0 }; + const result = delete ((object.value = 1) as number); + + return result === true && object.value === 1 ? 1 : 0; + } + + deleteOwnToString(): number { + const object = { toString: 1 }; + delete object.toString; + return object.toString === undefined ? 1 : 0; + } + + deletePrototypeMethod(): number { + const instance = new DeleteMethodSubject(); + delete instance.method; + return instance.method === undefined ? 1 : 0; + } + + deleteClassOwnField(): number { + const instance = new DeleteMethodSubject(); + delete instance.ownValue; + return instance.ownValue === undefined ? 1 : 0; + } + + deleteObjectLiteralMethod(): number { + const object = { method(): number { return 7; } }; + delete object.method; + return object.method === undefined ? 1 : 0; + } + + deleteArrayPrototypeMethod(): number { + const values = [1, 2]; + delete values.push; + return values.push === undefined ? 1 : 0; + } +}