From 1edec54d3012e3a9cfdda1a3bcf950c3a49ae0cd Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 12 Sep 2025 13:53:46 +0300 Subject: [PATCH 1/7] Handle reading from fake array --- .../kotlin/org/usvm/machine/expr/ReadArray.kt | 35 ++++++++++++++----- 1 file changed, 26 insertions(+), 9 deletions(-) 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 From c9b53c1265d9835a6c3cbf7decf065cffcfe7c7b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 12 Sep 2025 15:17:23 +0300 Subject: [PATCH 2/7] Support string length --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt | 6 ++++++ 1 file changed, 6 insertions(+) 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..979063a544 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") } From c5b13468712f4095761867d0d0e0a0398907d19f Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 12 Sep 2025 16:35:21 +0300 Subject: [PATCH 3/7] Log warn instead of errors --- .../src/main/kotlin/org/usvm/util/EtsFieldResolver.kt | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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() } From 72c73a6460bebc4e015b3794e4728ab23fe23374 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 12 Sep 2025 16:36:15 +0300 Subject: [PATCH 4/7] Kill the state on method resolution failure --- .../kotlin/org/usvm/machine/expr/TsExprResolver.kt | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) 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 From b0834150949908af6e496ff79f26d1ffb0933719 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 12 Sep 2025 17:43:42 +0300 Subject: [PATCH 5/7] Add test with nullable argument --- .../kotlin/org/usvm/samples/lang/Optional.kt | 26 +++++++++++++++++++ .../test/resources/samples/lang/Optional.ts | 16 ++++++++++++ 2 files changed, 42 insertions(+) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt create mode 100644 usvm-ts/src/test/resources/samples/lang/Optional.ts 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..176be14703 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt @@ -0,0 +1,26 @@ +package org.usvm.samples.lang + +import org.jacodb.ets.model.EtsScene +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import kotlin.test.Test + +class Optional : TsMethodTestRunner() { + private val tsPath = "/samples/lang/Optional.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + 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; + } +} From 31ff0873dae9bcb05e3507b17c9903f64a22e534 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 15 Sep 2025 13:49:56 +0300 Subject: [PATCH 6/7] Disable test with input union type --- usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 index 176be14703..f08399946a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt @@ -1,17 +1,19 @@ 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 -import kotlin.test.Test class Optional : TsMethodTestRunner() { private val tsPath = "/samples/lang/Optional.ts" override val scene: EtsScene = loadScene(tsPath) - @Test + @Disabled("Input union types are not supported yet") + @RepeatedTest(10, failureThreshold = 1) fun `test nullableArgument`() { val method = getMethod("nullableArgument") discoverProperties( From 64a374eec8ce76837f4e4cfc874b04befc6f9ebc Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 15 Sep 2025 14:20:06 +0300 Subject: [PATCH 7/7] Rename --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt | 2 +- usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt index 979063a544..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 @@ -59,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(