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 c079df94b2..0d913621ee 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 @@ -249,7 +249,7 @@ fun TsContext.checkReadingInRange( ) } -fun TsContext.checkLengthBounds( +fun TsContext.ensureLengthBounds( scope: TsStepScope, length: UExpr, maxLength: Int, 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 5f5a7932d1..684c8902dc 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 @@ -1,6 +1,7 @@ package org.usvm.machine.expr 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.EtsBooleanType @@ -20,18 +21,30 @@ import org.usvm.types.first import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue +private val logger = KotlinLogging.logger {} + internal fun TsExprResolver.handleArrayAccess( value: EtsArrayAccess, ): UExpr<*>? = with(ctx) { // Resolve the array. - val array = resolve(value.array) ?: return null - check(array.sort == addressSort) { - "Expected address sort for array, got: ${array.sort}" + val array = run { + val resolved = resolve(value.array) ?: return null + if (resolved.isFakeObject()) { + scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: run { + logger.warn { "UNSAT after ensuring fake object is ref-typed" } + return null + } + resolved.extractRef(scope) + } else { + check(resolved.sort == addressSort) { + "Expected address sort for array, got: ${resolved.sort}" + } + resolved.asExpr(addressSort) + } } - val arrayRef = array.asExpr(addressSort) // Check for undefined or null array access. - checkUndefinedOrNullPropertyRead(scope, arrayRef, propertyName = "[]") ?: return null + checkUndefinedOrNullPropertyRead(scope, array, propertyName = "[]") ?: return null // Resolve the index. val resolvedIndex = resolve(value.index) ?: return null @@ -49,8 +62,8 @@ internal fun TsExprResolver.handleArrayAccess( ).asExpr(sizeSort) // Determine the array type. - val arrayType = if (isAllocatedConcreteHeapRef(arrayRef)) { - scope.calcOnState { memory.typeStreamOf(arrayRef).first() } + val arrayType = if (isAllocatedConcreteHeapRef(array)) { + scope.calcOnState { memory.typeStreamOf(array).first() } } else { value.array.type } @@ -59,7 +72,7 @@ internal fun TsExprResolver.handleArrayAccess( } // Read the array element. - readArray(scope, arrayRef, bvIndex, arrayType) + readArray(scope, array, bvIndex, arrayType) } fun TsContext.readArray( @@ -103,7 +116,11 @@ fun TsContext.readArray( index = index, type = arrayType, ) - return scope.calcOnState { memory.read(lValue) } + val fake = scope.calcOnState { memory.read(lValue) } + check(fake.isFakeObject()) { + "Expected fake object in concrete array with unresolved element type, got: $fake" + } + return fake } // If the element type is unresolved, we need to create a fake object diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt index c5eb6af7db..fa4d83b68b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt @@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef @@ -30,6 +31,11 @@ fun TsContext.readLengthProperty( EtsArrayType(EtsUnknownType, dimensions = 1) } + is EtsStringType -> { + // Strings are treated as arrays of characters (represented as strings). + EtsArrayType(EtsStringType, dimensions = 1) + } + else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type") } @@ -53,7 +59,7 @@ fun TsContext.readArrayLength( } // Check that the length is within the allowed bounds. - checkLengthBounds(scope, length, maxArraySize) ?: return null + ensureLengthBounds(scope, length, maxArraySize) ?: return null // Convert the length to fp64. return mkBvToFpExpr( 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 40851d8b8c..b283ae66cc 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 @@ -1160,13 +1160,24 @@ class TsSimpleValueResolver( } if (local.name.startsWith(ANONYMOUS_METHOD_PREFIX)) { + val currentMethod = scope.calcOnState { lastEnteredMethod } val sig = EtsMethodSignature( - enclosingClass = EtsClassSignature.UNKNOWN, + enclosingClass = currentMethod.signature.enclosingClass, name = local.name, parameters = emptyList(), returnType = EtsUnknownType, ) val methods = ctx.resolveEtsMethods(sig) + if (methods.isEmpty()) { + logger.error { "Cannot resolve anonymous method for local: $local" } + scope.assert(ctx.mkFalse()) + return null + } + if (methods.size > 1) { + logger.error { "Multiple methods found for anonymous method local: $local" } + scope.assert(ctx.mkFalse()) + return null + } val method = methods.single() val ref = scope.calcOnState { getMethodRef(method) } return ref diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt index 17df6cff52..607a702e42 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -1,5 +1,6 @@ package org.usvm.util +import mu.KotlinLogging import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsField @@ -12,6 +13,8 @@ import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME import org.usvm.machine.TsContext +private val logger = KotlinLogging.logger {} + fun TsContext.resolveEtsField( instance: EtsLocal?, field: EtsFieldSignature, @@ -68,10 +71,12 @@ private fun tryGetSingleField( val clazz = classes.single() val fields = clazz.getAllFields(hierarchy).filter { it.name == fieldName } if (fields.isEmpty()) { - error("No field with name '$fieldName' in class '${clazz.name}'") + // logger.warn { "No field with name '$fieldName' in class '${clazz.name}'" } + return null } if (fields.size > 1) { - error("Multiple fields with name '$fieldName' in class '${clazz.name}': $fields") + logger.warn { "Multiple fields with name '$fieldName' in class '${clazz.name}': $fields" } + return null } return fields.single() } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt new file mode 100644 index 0000000000..f08399946a --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt @@ -0,0 +1,28 @@ +package org.usvm.samples.lang + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.RepeatedTest +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq + +class Optional : TsMethodTestRunner() { + private val tsPath = "/samples/lang/Optional.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Disabled("Input union types are not supported yet") + @RepeatedTest(10, failureThreshold = 1) + fun `test nullableArgument`() { + val method = getMethod("nullableArgument") + discoverProperties( + method = method, + { x, r -> (r eq 0) && (x is TsTestValue.TsUndefined) }, + { x, r -> (r eq 0) && (x is TsTestValue.TsNull) }, + { x, r -> (r eq 1) && (x is TsTestValue.TsNumber) && (x eq 1) }, + { x, r -> (r eq 2) && (x is TsTestValue.TsNumber) && (x eq 2) }, + { x, r -> (r eq 10) && (x is TsTestValue.TsNumber) }, + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/lang/Optional.ts b/usvm-ts/src/test/resources/samples/lang/Optional.ts new file mode 100644 index 0000000000..36985963b0 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/Optional.ts @@ -0,0 +1,16 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class Optional { + nullableArgument(x: number | null): number { + let value: number = 42; + if (x === undefined) return 0; + if (x !== null) { + if (x === 1) return x; // 1 + value = x; + if (x === 2) return value; // 2 + return 10; + } + return 0; + } +}