From 484724dfa2e29cc35b0d65553a1a31001fc68670 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:04:04 +0300 Subject: [PATCH 01/12] Handle residual intersection and missing field owner types against main --- .../main/kotlin/org/usvm/machine/TsContext.kt | 12 ++++- .../org/usvm/machine/types/TsTypeSystem.kt | 10 ++-- .../kotlin/org/usvm/util/EtsFieldResolver.kt | 3 +- .../usvm/machine/TsContextTypeToSortTest.kt | 51 +++++++++++++++++++ .../usvm/machine/types/TsTypeSystemTest.kt | 46 +++++++++++++++-- .../org/usvm/util/EtsFieldResolverTest.kt | 40 +++++++++++++++ 6 files changed, 152 insertions(+), 10 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTypeToSortTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/util/EtsFieldResolverTest.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index fa079747fe..44e9bd806e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -2,6 +2,8 @@ package org.usvm.machine import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr +import kotlin.contracts.ExperimentalContracts +import kotlin.contracts.contract import org.jacodb.ets.model.EtsAliasType import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType @@ -11,6 +13,7 @@ import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType +import org.jacodb.ets.model.EtsIntersectionType import org.jacodb.ets.model.EtsLexicalEnvType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod @@ -54,8 +57,6 @@ import org.usvm.machine.types.EtsFakeType import org.usvm.memory.UReadOnlyMemory import org.usvm.types.single import org.usvm.util.mkFieldLValue -import kotlin.contracts.ExperimentalContracts -import kotlin.contracts.contract typealias TsSizeSort = UBv32Sort @@ -165,6 +166,13 @@ class TsContext( is EtsNullType -> addressSort is EtsUndefinedType -> addressSort is EtsUnionType -> unresolvedSort + is EtsIntersectionType -> { + val memberSorts = type.types.map(::typeToSort) + val commonSort = memberSorts.firstOrNull() ?: unresolvedSort + val hasCommonSort = memberSorts.all { it == commonSort } + + if (hasCommonSort) commonSort else unresolvedSort + } is EtsRefType -> addressSort is EtsLexicalEnvType -> addressSort is EtsAnyType -> unresolvedSort 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 e63b31039d..87879a401f 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 @@ -74,6 +74,12 @@ class TsTypeSystem( // "never" is the universal subtype: never can be assigned to any type. if (unwrappedType is EtsNeverType) return true + // A fake type only matches itself. Distinct wrappers do not establish a + // TypeScript subtype relation; callers handle those branches explicitly. + if (unwrappedType is EtsFakeType || unwrappedSupertype is EtsFakeType) { + return unwrappedSupertype === unwrappedType + } + // When "never" is in supertype position, only never <: never. if (unwrappedSupertype is EtsNeverType) return type is EtsNeverType @@ -168,10 +174,6 @@ class TsTypeSystem( // Class and structural types - require(unwrappedType !is EtsFakeType && unwrappedSupertype !is EtsFakeType) { - "Fake types should not occur in type constraints" - } - if (unwrappedSupertype is EtsAuxiliaryType && unwrappedType is EtsAuxiliaryType) { return unwrappedType.properties.all { it in unwrappedSupertype.properties } } 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 607a702e42..2fbbe2fa8a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -24,7 +24,8 @@ fun TsContext.resolveEtsField( if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) { val classes = hierarchy.classesForType(EtsClassType(field.enclosingClass)) if (classes.isEmpty()) { - error("Cannot resolve class ${field.enclosingClass.name}") + logger.warn { "Cannot resolve class ${field.enclosingClass.name} for field ${field.name}" } + return TsResolutionResult.Empty } if (classes.size > 1) { error("Multiple classes with name ${field.enclosingClass.name}") diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTypeToSortTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTypeToSortTest.kt new file mode 100644 index 0000000000..65b829f429 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTypeToSortTest.kt @@ -0,0 +1,51 @@ +package org.usvm.machine + +import io.mockk.mockk +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsIntersectionType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsUnclearRefType +import org.junit.jupiter.api.Test +import kotlin.test.assertEquals + +class TsContextTypeToSortTest { + private val ctx = TsContext( + scene = EtsScene(projectFiles = emptyList()), + components = mockk(), + ) + + @Test + fun `intersection of reference types has reference sort`() { + val window = EtsClassType( + signature = EtsClassSignature( + name = "Window", + file = EtsFileSignature.UNKNOWN, + ), + ) + val globalThis = EtsUnclearRefType( + name = "globalThis", + typeParameters = emptyList(), + ) + val type = EtsIntersectionType(types = listOf(window, globalThis)) + + val sort = ctx.typeToSort(type) + + assertEquals(ctx.addressSort, sort) + } + + @Test + fun `intersection with incompatible sorts remains unresolved`() { + val globalThis = EtsUnclearRefType( + name = "globalThis", + typeParameters = emptyList(), + ) + val type = EtsIntersectionType(types = listOf(EtsNumberType, globalThis)) + + val sort = ctx.typeToSort(type) + + assertEquals(ctx.unresolvedSort, sort) + } +} 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 7db0ac6cd7..ec89f23c48 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,5 +1,9 @@ package org.usvm.machine.types +import io.mockk.mockk +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType @@ -17,15 +21,51 @@ 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.machine.TsContext import org.usvm.machine.withCoreRuntimeSdk import org.usvm.types.TypesResult +import org.usvm.types.USingleTypeStream 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 `synthetic wrapper does not satisfy structural type constraints`() { + val scene = EtsScene(projectFiles = emptyList()) + val context = TsContext(scene = scene, components = mockk()) + val typeSystem = TsTypeSystem( + scene = scene, + typeOperationsTimeout = 1.seconds, + hierarchy = EtsHierarchy(scene), + ) + val fakeType = EtsFakeType.mkRef(context) + val structuralType = EtsAuxiliaryType(properties = setOf("style")) + + val fakeHasProperty = typeSystem.isSupertype(structuralType, fakeType) + val propertyHasFakeType = typeSystem.isSupertype(fakeType, structuralType) + + assertFalse(fakeHasProperty) + assertFalse(propertyHasFakeType) + } + + @Test + fun `fake type remains in a singleton stream after filtering by itself`() { + val scene = EtsScene(projectFiles = emptyList()) + val context = TsContext(scene = scene, components = mockk()) + val typeSystem = TsTypeSystem( + scene = scene, + typeOperationsTimeout = 1.seconds, + hierarchy = EtsHierarchy(scene), + ) + val fakeType = EtsFakeType.mkRef(context) + val stream = USingleTypeStream(typeSystem = typeSystem, singleType = fakeType) + + val filtered = stream.filterBySupertype(fakeType).filterBySubtype(fakeType) + + assertTrue(typeSystem.isSupertype(fakeType, fakeType)) + assertFalse(filtered.isEmpty ?: true) + } + @Test fun `runtime object constraint accepts references and excludes primitive or unresolved types`() { val scene = EtsScene(projectFiles = emptyList()) diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/EtsFieldResolverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/util/EtsFieldResolverTest.kt new file mode 100644 index 0000000000..300ec9c550 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/EtsFieldResolverTest.kt @@ -0,0 +1,40 @@ +package org.usvm.util + +import io.mockk.mockk +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +import org.junit.jupiter.api.Test +import org.usvm.machine.TsContext +import kotlin.test.assertEquals + +class EtsFieldResolverTest { + @Test + fun `missing built-in class leaves its field unresolved`() { + val scene = EtsScene(projectFiles = emptyList()) + val ctx = TsContext(scene = scene, components = mockk()) + val hierarchy = EtsHierarchy(scene) + + for ((className, fieldName) in listOf("RangeError" to "stack", "URL" to "searchParams")) { + val signature = EtsClassSignature( + name = className, + file = EtsFileSignature.UNKNOWN, + ) + val field = EtsFieldSignature( + enclosingClass = signature, + name = fieldName, + type = EtsStringType, + ) + + val result = ctx.resolveEtsField( + instance = null, + field = field, + hierarchy = hierarchy, + ) + + assertEquals(TsResolutionResult.Empty, result) + } + } +} From 1d91b83c5512db7cd89731b80e30affcdaa7f7c4 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:13:29 +0300 Subject: [PATCH 02/12] Give opaque string returns real bounded UTF16 backing --- .../src/main/kotlin/org/usvm/api/TsMock.kt | 36 +++++++++++++ .../machine/call/FreshStringMockSourceTest.kt | 50 +++++++++++++++++++ .../call/TsUnknownCallDispatcherTest.kt | 47 ++++++++++++++++- .../baseline/CallFallbackBaseline.ts | 8 +++ .../test/resources/models/FreshStringMock.ts | 13 +++++ 5 files changed, 153 insertions(+), 1 deletion(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt create mode 100644 usvm-ts/src/test/resources/models/FreshStringMock.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index 7ab3d97d96..3cbfb57312 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -1,15 +1,23 @@ package org.usvm.api +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringLiteralType +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsVoidType import org.usvm.UAddressSort +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.types.mkFakeValue +import org.usvm.sizeSort +import org.usvm.util.mkStringBackingLValue +import org.usvm.util.mkStringBackingLengthLValue fun mockMethodCall( scope: TsStepScope, @@ -37,6 +45,8 @@ internal fun makeFreshUnknownCallResult( resultType: EtsType, ): UExpr<*> = scope.calcOnState { if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue() + if (resultType is EtsStringLiteralType) return@calcOnState mkInitializedStringConstant(resultType.value) + if (resultType == EtsStringType) return@calcOnState makeFreshBoundedString() when (val sort = ctx.typeToSort(resultType)) { is UAddressSort -> makeSymbolicRefUntyped() @@ -51,3 +61,29 @@ internal fun makeFreshUnknownCallResult( else -> makeSymbolicPrimitive(sort) } } + +/** An opaque string still has a real bounded UTF-16 backing and cannot become an arbitrary object reference. */ +private fun TsState.makeFreshBoundedString(): UConcreteHeapRef = with(ctx) { + val string = memory.allocConcrete(EtsStringType) + val characters = memory.allocConcrete(EtsArrayType(elementType = EtsNumberType, dimensions = 1)) + val length = makeSymbolicPrimitive(sizeSort) + val minimum = mkBv(0) + val maximum = mkBv(maxStringLength) + val lengthBounds = mkAnd( + mkBvSignedGreaterOrEqualExpr(length, minimum), + mkBvSignedLessOrEqualExpr(length, maximum), + ) + pathConstraints += lengthBounds + + memory.initializeArray( + arrayHeapRef = characters, + type = stringBackingArrayDescriptor, + sort = bv16Sort, + sizeSort = sizeSort, + contents = (0 until maxStringLength).asSequence().map { makeSymbolicPrimitive(bv16Sort) }, + ) + memory.write(mkStringBackingLengthLValue(characters), length, guard = trueExpr) + memory.write(mkStringBackingLValue(string), characters, guard = trueExpr) + boundedStringBackingRefs += string + string +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt new file mode 100644 index 0000000000..c5959bbe73 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt @@ -0,0 +1,50 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertIs +import kotlin.test.assertTrue + +class FreshStringMockSourceTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/FreshStringMock.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(projectFiles = listOf(sourceFile)) + + @Test + fun `fresh string result has a readable private length`() { + val values = analyze("length") + + assertTrue(values.isNotEmpty()) + values.forEach { value -> assertTrue(assertIs(value).number in 0.0..8.0) } + } + + @Test + fun `fresh string result retains backing through ordinary concatenation`() { + val values = analyze("concat") + + assertTrue(values.isNotEmpty()) + values.forEach { value -> assertTrue(assertIs(value).value.endsWith("!")) } + } + + private fun analyze(methodName: String): List { + val method = scene.projectClasses.single { clazz -> clazz.name == "FreshStringMock" } + .methods.single { candidate -> candidate.name == methodName } + return TsMachine( + scene = scene, + options = UMachineOptions(throwExceptionOnStepFailure = true, stepsFromLastCovered = 128L), + tsOptions = TsOptions(maxArraySize = 8, unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), + ).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state).returnValue } + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt index 7a36ae965e..6400e5cf93 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt @@ -24,6 +24,7 @@ import org.usvm.UBoolSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UMachineOptions +import org.usvm.api.evalTypeEquals import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget import org.usvm.isTrue @@ -241,6 +242,30 @@ class TsUnknownCallDispatcherTest { ) } + @Test + fun `partial string model keeps modeled and typed fresh successors`() { + val observer = RecordingUnknownCallObserver() + + val states = analyzeAllStates( + methodName = "modeledStringCallForks", + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = catalog(PartialStringModel), + observer = observer, + ) + + assertEquals(2, states.size) + assertEquals( + listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), + observer.events.map { it.outcome }, + ) + states.forEach { state -> + val result = assertIs(state.methodResult).value + val isString = state.memory.types.evalTypeEquals(result.asExpr(state.ctx.addressSort), EtsStringType) + assertTrue(state.models.isNotEmpty()) + assertTrue(state.models.all { model -> model.eval(isString).isTrue }) + } + } + @Test fun `partial model sends residual domain to stop fallback`() { val observer = RecordingUnknownCallObserver() @@ -753,6 +778,25 @@ class TsUnknownCallDispatcherTest { } } + private object PartialStringModel : TestModel( + id = "partial-string-model", + methodName = "convert", + enclosingClassName = "ExternalString", + ) { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val condition = requireNotNull(call.arguments.single().resolved).asExpr(state.ctx.boolSort) + val successor = TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { mkInitializedStringConstant("modeled") }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.mkNot(condition), + ) + } + } + private object ExceptionalModel : TestModel(id = "exceptional-model", methodName = "fail") { override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { val successor = TsUnknownCallModelSuccessor( @@ -796,8 +840,9 @@ class TsUnknownCallDispatcherTest { private abstract class TestModel( override val id: String, methodName: String, + enclosingClassName: String? = null, ) : TsUnknownCallModel { - override val target = TsUnknownCallTarget(methodName = methodName) + override val target = TsUnknownCallTarget(methodName = methodName, enclosingClassName = enclosingClassName) } private class RecordingUnknownCallObserver : TsInterpreterObserver { diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts index cda3bc5711..f0d6d4ba48 100644 --- a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts +++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts @@ -18,6 +18,10 @@ declare class ExternalBoolean { static convert(value: boolean): boolean; } +declare class ExternalString { + static convert(value: boolean): string; +} + declare class ExternalAny { static value(): any; } @@ -87,6 +91,10 @@ class CallFallbackBaseline { return ExternalBoolean.convert(value); } + modeledStringCallForks(value: boolean): string { + return ExternalString.convert(value); + } + modeledUnknownCallReturnsAlias(receiver: ExternalReceiver): number { if (ExternalModeledCall.identity(receiver) === receiver) { return 122; diff --git a/usvm-ts/src/test/resources/models/FreshStringMock.ts b/usvm-ts/src/test/resources/models/FreshStringMock.ts new file mode 100644 index 0000000000..0e96c3c8ae --- /dev/null +++ b/usvm-ts/src/test/resources/models/FreshStringMock.ts @@ -0,0 +1,13 @@ +declare class ExternalString { + static value(): string; +} + +export class FreshStringMock { + static length(): number { + return ExternalString.value().length; + } + + static concat(): string { + return ExternalString.value() + "!"; + } +} From 562b51ab22973c6350900a69a417c2d1fea425d8 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:14:03 +0300 Subject: [PATCH 03/12] Report residual runtime boundaries and terminate unsupported storage paths --- .../org/usvm/machine/TsInterpreterObserver.kt | 26 +++++ .../kotlin/org/usvm/machine/expr/ReadArray.kt | 7 +- .../kotlin/org/usvm/machine/expr/ReadField.kt | 24 ++++- .../org/usvm/machine/expr/ReadLength.kt | 10 +- .../org/usvm/machine/expr/TsExprResolver.kt | 51 +++++++++- .../org/usvm/machine/expr/WriteArray.kt | 7 +- .../usvm/machine/interpreter/TsInterpreter.kt | 1 + .../expr/RuntimeLimitationBoundariesTest.kt | 96 +++++++++++++++++++ .../models/RuntimeLimitationBoundaries.ts | 15 +++ 9 files changed, 227 insertions(+), 10 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt create mode 100644 usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index 132c6413be..3d93cd387c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -4,6 +4,7 @@ import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsCallExpr import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsThrowStmt import org.usvm.UBoolExpr import org.usvm.machine.call.TsUnknownCallEvent @@ -21,6 +22,11 @@ interface TsInterpreterObserver : UInterpreterObserver { // default empty implementation } + /** Reports a satisfiable path stopped at an explicit runtime modeling boundary. */ + fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + // default empty implementation + } + fun onAssignStatement( simpleValueResolver: TsSimpleValueResolver, stmt: EtsAssignStmt, @@ -74,3 +80,23 @@ interface TsInterpreterObserver : UInterpreterObserver { // default empty implementation } } + +/** A feasible execution path stopped because the runtime model deliberately omits [reason]. */ +data class TsRuntimeFeatureLimitationEvent( + val statement: EtsStmt, + val reason: TsRuntimeFeatureLimitationReason, + val detail: String, +) + +/** Stable identifiers for bounded runtime features reported by [TsRuntimeFeatureLimitationEvent]. */ +enum class TsRuntimeFeatureLimitationReason { + REGULAR_EXPRESSION_LITERAL, + FRONTEND_UNSUPPORTED_VALUE, + STRING_CONCAT_OPERAND_CONVERSION, + ARRAY_STORAGE_TYPE, + ARRAY_NAMED_PROPERTY_READ, + ARRAY_NAMED_PROPERTY_WRITE, + ARRAY_INDEX_GROWTH, + ARRAY_LENGTH_CAPACITY, + ARRAY_LENGTH_GROWTH, +} 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 2a1dae990a..5e07a39ab8 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 @@ -10,6 +10,7 @@ import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.machine.TsContext +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.mkFakeValue @@ -58,7 +59,11 @@ internal fun TsExprResolver.handleArrayAccess( return resolveField(scope, value.array, array, field, hierarchy) } if (receiverType !is EtsArrayType) { - throw UnsupportedOperationException("Symbolic object property keys are not supported") + stopRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE, + detail = "Indexed access requires supported storage: static=${value.array.type}, storage=$receiverType", + ) + return null } check(resolvedIndex.sort == fp64Sort) { 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 1bd686f5d5..ca412afd0a 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 @@ -2,7 +2,9 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import mu.KotlinLogging +import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature @@ -17,6 +19,7 @@ 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.jacodb.ets.model.EtsUnknownType import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UExpr @@ -85,11 +88,23 @@ internal fun TsExprResolver.handleInstanceFieldRef( val instance = resolveHeapRef(scope, rawInstance) ?: return null // Handle reading "length" property. - if (value.field.name == "length") { + val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } + val usesArrayLength = storageType is EtsArrayType || storageType == EtsStringType || + storageType == EtsAnyType || storageType == EtsUnknownType + val nativeTypedArray = storageType is EtsClassType && + storageType.signature.file == EtsClassSignature.UNKNOWN.file && + storageType.signature.name in NATIVE_TYPED_ARRAY_NAMES + if (value.field.name == "length" && (usesArrayLength || nativeTypedArray)) { 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) + if (!isObjectProperty) return readLengthProperty( + scope = scope, + instanceLocal = instanceLocal, + instance = instance, + maxArraySize = options.maxArraySize, + onFeatureLimitation = ::reportRuntimeFeatureLimitation, + ) } // Read the field. @@ -424,3 +439,8 @@ fun TsContext.readStaticField( // Read the field. return resolveField(scope, null, instance, field, hierarchy) } + +private val NATIVE_TYPED_ARRAY_NAMES = setOf( + "Int8Array", "Uint8Array", "Uint8ClampedArray", "Int16Array", "Uint16Array", + "Int32Array", "Uint32Array", "Float32Array", "Float64Array", "BigInt64Array", "BigUint64Array", +) 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 b30f330466..918e39f15c 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 @@ -12,6 +12,7 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.machine.TsContext +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort @@ -26,6 +27,7 @@ fun TsContext.readLengthProperty( instanceLocal: EtsLocal, instance: UHeapRef, maxArraySize: Int, + onFeatureLimitation: ((TsRuntimeFeatureLimitationReason, String) -> Unit)? = null, ): UExpr<*>? { // Determine the array type. val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } @@ -50,7 +52,13 @@ fun TsContext.readLengthProperty( ) } - else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type") + else -> { + val reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE + val detail = "Length read requires supported array storage: static=${instanceLocal.type}, storage=$type" + onFeatureLimitation?.invoke(reason, detail) + scope.doWithState { terminateAsUnsupported(reason = "$reason: $detail") } + return null + } } // Read the length of the array. 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 283441ffc6..2973e52123 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 @@ -2,6 +2,7 @@ package org.usvm.machine.expr import io.ksmt.expr.KFp64Value import io.ksmt.utils.asExpr +import kotlinx.serialization.json.JsonPrimitive import mu.KotlinLogging import org.jacodb.ets.model.EtsAddExpr import org.jacodb.ets.model.EtsAndExpr @@ -111,7 +112,10 @@ import org.usvm.isTrue import org.usvm.machine.TS_TYPE_ERROR_TYPE import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext +import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.call.TsUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.dispatch @@ -174,6 +178,7 @@ class TsExprResolver( internal val options: TsOptions, internal val hierarchy: EtsHierarchy, internal val unknownCallDispatcher: TsUnknownCallDispatcher, + internal val observer: TsInterpreterObserver? = null, ) : EtsEntity.Visitor?> { val simpleValueResolver: TsSimpleValueResolver = @@ -183,14 +188,37 @@ class TsExprResolver( return expr.accept(this) } - override fun visit(value: EtsRawEntity): Nothing { + override fun visit(value: EtsRawEntity): UExpr? { if (value.kind == "UnsupportedValue") { - throw UnsupportedOperationException("Unsupported frontend value: $value") + val kindName = when (val raw = value.extra["kindName"]) { + is JsonPrimitive -> raw.content + is String -> raw + else -> null + } + val reason = if (kindName == "RegularExpressionLiteral") { + TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL + } else { + TsRuntimeFeatureLimitationReason.FRONTEND_UNSUPPORTED_VALUE + } + stopRuntimeFeatureLimitation(reason = reason, detail = "Unsupported frontend value: $value") + return null } error("Cannot handle ${value::class.java.simpleName}: $value") } + internal fun reportRuntimeFeatureLimitation(reason: TsRuntimeFeatureLimitationReason, detail: String) { + val statement = scope.calcOnState { lastStmt } + observer?.onRuntimeFeatureLimitation( + TsRuntimeFeatureLimitationEvent(statement = statement, reason = reason, detail = detail), + ) + } + + internal fun stopRuntimeFeatureLimitation(reason: TsRuntimeFeatureLimitationReason, detail: String) { + reportRuntimeFeatureLimitation(reason = reason, detail = detail) + scope.doWithState { terminateAsUnsupported(reason = "$reason: $detail") } + } + private fun resolveUnaryOperator( operator: TsUnaryOperator, expr: EtsUnaryExpr, @@ -807,7 +835,12 @@ class TsExprResolver( 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") + val detail = "Unsupported string concatenation operand: $type, $value" + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.STRING_CONCAT_OPERAND_CONVERSION, + detail = detail, + ) + terminateAsUnsupported(reason = detail) }) ?: return null value.extractRef(scope) } else { @@ -815,14 +848,22 @@ class TsExprResolver( } concreteStringValue(operand)?.let { return mkStringConstant(it, scope) } if (!isStringOperandType(type) || operand.sort != addressSort) { - throw UnsupportedOperationException("Unsupported string concatenation operand: $type, $operand") + stopRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.STRING_CONCAT_OPERAND_CONVERSION, + detail = "Unsupported string concatenation operand: $type, $operand", + ) + return null } // 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") + stopRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.STRING_CONCAT_OPERAND_CONVERSION, + detail = "String concatenation needs a modeled string backing for $ref", + ) + return null } ref } 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 501b11d928..2b728f86a6 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 @@ -9,6 +9,7 @@ import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.machine.TsContext +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort @@ -49,7 +50,11 @@ internal fun TsExprResolver.handleAssignToArrayIndex( return assignToInstanceField(scope, lhv.array, array, field, expr, hierarchy) } if (receiverType !is EtsArrayType) { - throw UnsupportedOperationException("Symbolic object property keys are not supported") + stopRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE, + detail = "Indexed access requires supported storage: static=${lhv.array.type}, storage=$receiverType", + ) + return null } check(resolvedIndex.sort == fp64Sort) { 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 0b5757cc7a..8339586be6 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 @@ -773,6 +773,7 @@ class TsInterpreter( options = options, hierarchy = graph.hierarchy, unknownCallDispatcher = unknownCallDispatcher, + observer = observer, ) fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt new file mode 100644 index 0000000000..bd339ed45f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt @@ -0,0 +1,96 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertTrue + +class RuntimeLimitationBoundariesTest : TsMethodTestRunner() { + override val scene = EtsScene( + listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/RuntimeLimitationBoundaries.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + @Test + fun `regular expression limitation terminates once with its exact reason`() { + val observer = RecordingObserver() + val target = method("regularExpressionLiteral") + + TsMachine( + scene = scene, + options = UMachineOptions(throwExceptionOnStepFailure = true, stepsFromLastCovered = 128L), + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> + val outcome = machine.analyzeWithOutcome(listOf(target)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "REGULAR_EXPRESSION_LITERAL" in it }) + } + assertEquals(listOf(TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL), observer.reasons) + } + + @Test + fun `unsupported storage terminates while a supported sibling still returns`() { + val observer = RecordingObserver() + val target = method("unknownStorageOrSupportedSibling") + + TsMachine( + scene = scene, + options = UMachineOptions(throwExceptionOnStepFailure = true, stepsFromLastCovered = 128L), + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> + val outcome = machine.analyzeWithOutcome(listOf(target)) + val values = outcome.states.map { state -> TsTestResolver().resolve(target, state).returnValue } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.any { "ARRAY_STORAGE_TYPE" in it }) + assertTrue(values.any { value -> value is TsTestValue.TsNumber && value.number == 7.0 }) + } + assertTrue(observer.reasons.isNotEmpty()) + assertTrue(observer.reasons.all { reason -> reason == TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE }) + assertTrue(observer.reasons.size < 128) + } + + @Test + fun `ordinary object length is read as its actual field`() { + discoverProperties( + method = method("ordinaryLengthField"), + { result -> result.number == 17.0 }, + invariants = arrayOf({ result -> result.number == 17.0 }), + ) + } + + private fun method(name: String): EtsMethod = getMethod( + methodName = name, + className = "RuntimeLimitationBoundaries", + ) + + private class RecordingObserver : TsInterpreterObserver { + val reasons = mutableListOf() + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + reasons += event.reason + } + } +} diff --git a/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts b/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts new file mode 100644 index 0000000000..ae4a5a0b02 --- /dev/null +++ b/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts @@ -0,0 +1,15 @@ +export class RuntimeLimitationBoundaries { + static regularExpressionLiteral(): boolean { + return /value/.test("value"); + } + + static unknownStorageOrSupportedSibling(flag: boolean, values: unknown): number { + if (flag) return 7; + return (values as any)[0]; + } + + static ordinaryLengthField(): number { + const record = { length: 17 }; + return record.length; + } +} From 38bf49dd18241a1d0c85db94a437fb9cab838ed8 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:12:19 +0300 Subject: [PATCH 04/12] Strengthen source regressions for opaque string results --- .../main/kotlin/org/usvm/machine/TsContext.kt | 4 +- .../machine/call/FreshStringMockSourceTest.kt | 80 ++++++++++++++----- .../usvm/machine/types/TsTypeSystemTest.kt | 6 +- .../test/resources/models/FreshStringMock.ts | 10 +++ 4 files changed, 75 insertions(+), 25 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 44e9bd806e..31afa99738 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -2,8 +2,6 @@ package org.usvm.machine import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr -import kotlin.contracts.ExperimentalContracts -import kotlin.contracts.contract import org.jacodb.ets.model.EtsAliasType import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType @@ -57,6 +55,8 @@ import org.usvm.machine.types.EtsFakeType import org.usvm.memory.UReadOnlyMemory import org.usvm.types.single import org.usvm.util.mkFieldLValue +import kotlin.contracts.ExperimentalContracts +import kotlin.contracts.contract typealias TsSizeSort = UBv32Sort diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt index c5959bbe73..0d2763cca1 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt @@ -1,50 +1,90 @@ package org.usvm.machine.call +import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +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.TsOptions +import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver import org.usvm.util.getResourcePath import kotlin.test.Test -import kotlin.test.assertIs +import kotlin.test.assertEquals import kotlin.test.assertTrue -class FreshStringMockSourceTest { +class FreshStringMockSourceTest : TsMethodTestRunner() { private val sourceFile = loadEtsFileAutoConvert( getResourcePath("/models/FreshStringMock.ts"), provider = EtsIrProvider.TS_FRONTEND, ) - private val scene = EtsScene(projectFiles = listOf(sourceFile)) + override val scene = EtsScene(projectFiles = listOf(sourceFile)) + override val tsOptions = TsOptions( + maxArraySize = 8, + unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ) + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + val analysis = machine.analyzeWithOutcome(methods = listOf(method)) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), "${method.name}: ${analysis.unsupportedPaths}") + analysis.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + stepsFromLastCovered = 128L, + ) + } @Test fun `fresh string result has a readable private length`() { - val values = analyze("length") - - assertTrue(values.isNotEmpty()) - values.forEach { value -> assertTrue(assertIs(value).number in 0.0..8.0) } + discoverProperties( + method = method("length"), + { result -> result.number in 0.0..8.0 }, + invariants = arrayOf({ result -> result.number in 0.0..8.0 }), + ) } @Test fun `fresh string result retains backing through ordinary concatenation`() { - val values = analyze("concat") + discoverProperties( + method = method("concat"), + { result -> result.value.endsWith("!") }, + invariants = arrayOf({ result -> result.value.endsWith("!") }), + ) + } - assertTrue(values.isNotEmpty()) - values.forEach { value -> assertTrue(assertIs(value).value.endsWith("!")) } + @Test + fun `fresh strings retain both empty and nonempty source branches`() { + discoverProperties( + method = method("branchOnLength"), + { result -> result.number == 0.0 }, + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 0.0 || result.number == 1.0 }), + ) } - private fun analyze(methodName: String): List { - val method = scene.projectClasses.single { clazz -> clazz.name == "FreshStringMock" } - .methods.single { candidate -> candidate.name == methodName } - return TsMachine( - scene = scene, - options = UMachineOptions(throwExceptionOnStepFailure = true, stepsFromLastCovered = 128L), - tsOptions = TsOptions(maxArraySize = 8, unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), - ).use { machine -> - machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state).returnValue } - } + @Test + fun `opaque literal return keeps its declared string value`() { + discoverProperties( + method = method("literal"), + { result -> result.value == "known" }, + invariants = arrayOf({ result -> result.value == "known" }), + ) } + + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "FreshStringMock") } 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 ec89f23c48..9dd4449224 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,9 +1,6 @@ package org.usvm.machine.types import io.mockk.mockk -import kotlin.test.assertFalse -import kotlin.test.assertTrue -import kotlin.time.Duration.Companion.seconds import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType @@ -27,6 +24,9 @@ import org.usvm.types.TypesResult import org.usvm.types.USingleTypeStream 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 diff --git a/usvm-ts/src/test/resources/models/FreshStringMock.ts b/usvm-ts/src/test/resources/models/FreshStringMock.ts index 0e96c3c8ae..c3d0d4a4cd 100644 --- a/usvm-ts/src/test/resources/models/FreshStringMock.ts +++ b/usvm-ts/src/test/resources/models/FreshStringMock.ts @@ -1,5 +1,6 @@ declare class ExternalString { static value(): string; + static literal(): "known"; } export class FreshStringMock { @@ -10,4 +11,13 @@ export class FreshStringMock { static concat(): string { return ExternalString.value() + "!"; } + + static branchOnLength(): number { + const value = ExternalString.value(); + return value.length === 0 ? 0 : 1; + } + + static literal(): string { + return ExternalString.literal(); + } } From 6f7d8cdf89a1758a05dfd2e0d3d231ae589768c6 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:23:03 +0300 Subject: [PATCH 05/12] Distinguish string concatenation capacity residuals from supported paths --- .../machine/call/FreshStringMockSourceTest.kt | 23 +++++++++++++++++-- .../test/resources/models/FreshStringMock.ts | 6 +++++ 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt index 0d2763cca1..5cf5264be7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt @@ -59,9 +59,28 @@ class FreshStringMockSourceTest : TsMethodTestRunner() { } @Test - fun `fresh string result retains backing through ordinary concatenation`() { + fun `fresh concatenation reports its capacity residual and preserves supported suffix witnesses`() { + val method = method("concat") + + TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + val outcome = machine.analyzeWithOutcome(methods = listOf(method)) + val values = outcome.states.map { state -> TsTestResolver().resolve(method, state).returnValue } + val onlyCapacityResiduals = outcome.unsupportedPaths.all { diagnostic -> + "String concatenation result exceeds configured length bound 8" in diagnostic + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isNotEmpty()) + assertTrue(onlyCapacityResiduals) + assertTrue(values.isNotEmpty()) + assertTrue(values.all { value -> value is TsTestValue.TsString && value.value.endsWith("!") }) + } + } + + @Test + fun `fresh string concatenation exhausts the supported source domain without residuals`() { discoverProperties( - method = method("concat"), + method = method("concatWithinBound"), { result -> result.value.endsWith("!") }, invariants = arrayOf({ result -> result.value.endsWith("!") }), ) diff --git a/usvm-ts/src/test/resources/models/FreshStringMock.ts b/usvm-ts/src/test/resources/models/FreshStringMock.ts index c3d0d4a4cd..24961c5f6f 100644 --- a/usvm-ts/src/test/resources/models/FreshStringMock.ts +++ b/usvm-ts/src/test/resources/models/FreshStringMock.ts @@ -12,6 +12,12 @@ export class FreshStringMock { return ExternalString.value() + "!"; } + static concatWithinBound(): string { + const value = ExternalString.value(); + if (value.length >= 8) return "!"; + return value + "!"; + } + static branchOnLength(): number { const value = ExternalString.value(); return value.length === 0 ? 0 : 1; From 83e6e5867dc8874215d62ee2d53717a04b6c1398 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:25:39 +0300 Subject: [PATCH 06/12] Preserve finite literal alternatives in opaque call results --- .../src/main/kotlin/org/usvm/api/TsMock.kt | 61 ++++++++++++++++++- .../machine/call/FreshStringMockSourceTest.kt | 43 +++++++++++++ .../test/resources/models/FreshStringMock.ts | 40 ++++++++++++ 3 files changed, 143 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index 3cbfb57312..f7ac37a74e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -1,11 +1,17 @@ package org.usvm.api import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanLiteralType +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNullType +import org.jacodb.ets.model.EtsNumberLiteralType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStringLiteralType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUndefinedType +import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsVoidType import org.usvm.UAddressSort import org.usvm.UConcreteHeapRef @@ -14,6 +20,7 @@ import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.machine.types.mkFakeValue import org.usvm.sizeSort import org.usvm.util.mkStringBackingLValue @@ -45,8 +52,15 @@ internal fun makeFreshUnknownCallResult( resultType: EtsType, ): UExpr<*> = scope.calcOnState { if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue() - if (resultType is EtsStringLiteralType) return@calcOnState mkInitializedStringConstant(resultType.value) + val literal = makeLiteralResult(resultType) + if (literal != null) return@calcOnState literal if (resultType == EtsStringType) return@calcOnState makeFreshBoundedString() + if (resultType is EtsUnionType) { + val variants = resultType.finiteLiteralVariants() + if (!variants.isNullOrEmpty()) { + return@calcOnState makeFiniteLiteralUnion(scope = scope, variants = variants) + } + } when (val sort = ctx.typeToSort(resultType)) { is UAddressSort -> makeSymbolicRefUntyped() @@ -62,6 +76,51 @@ internal fun makeFreshUnknownCallResult( } } +private fun EtsType.finiteLiteralVariants(): List? { + return when (this) { + is EtsUnionType -> { + val variants = mutableListOf() + for (member in types) { + val memberVariants = member.finiteLiteralVariants() ?: return null + variants += memberVariants + } + variants.distinct() + } + + is EtsStringLiteralType, is EtsNumberLiteralType, is EtsBooleanLiteralType, + EtsNullType, EtsUndefinedType, + -> listOf(this) + + EtsBooleanType -> listOf(EtsBooleanLiteralType(value = false), EtsBooleanLiteralType(value = true)) + else -> null + } +} + +private fun TsState.makeLiteralResult(type: EtsType): UExpr<*>? = when (type) { + is EtsStringLiteralType -> mkInitializedStringConstant(type.value) + is EtsNumberLiteralType -> ctx.mkFp64(type.value) + is EtsBooleanLiteralType -> ctx.mkBool(type.value) + EtsNullType -> ctx.mkTsNullValue() + EtsUndefinedType -> ctx.mkUndefinedValue() + else -> null +} + +private fun TsState.makeFiniteLiteralUnion(scope: TsStepScope, variants: List): UExpr<*> { + var result = requireNotNull(makeLiteralResult(variants.first())) + for (variant in variants.drop(1)) { + val selected = makeSymbolicPrimitive(ctx.boolSort) + val value = requireNotNull(makeLiteralResult(variant)) + result = ctx.iteWriteIntoFakeObject( + scope = scope, + condition = selected, + trueBranchValue = value, + falseBranchValue = result, + ) + } + + return result +} + /** An opaque string still has a real bounded UTF-16 backing and cannot become an arbitrary object reference. */ private fun TsState.makeFreshBoundedString(): UConcreteHeapRef = with(ctx) { val string = memory.allocConcrete(EtsStringType) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt index 5cf5264be7..8616d268bc 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt @@ -105,5 +105,48 @@ class FreshStringMockSourceTest : TsMethodTestRunner() { ) } + @Test + fun `opaque string literal union retains exactly its allowed values`() { + discoverProperties( + method = method("stringUnion"), + { result -> result.number == 1.0 }, + { result -> result.number == 2.0 }, + invariants = arrayOf({ result -> result.number in setOf(1.0, 2.0) }), + ) + } + + @Test + fun `opaque finite union preserves string number boolean and nullish kinds`() { + discoverProperties( + method = method("finiteUnion"), + { result -> result.number == 1.0 }, + { result -> result.number == 2.0 }, + { result -> result.number == 3.0 }, + { result -> result.number == 4.0 }, + { result -> result.number == 5.0 }, + invariants = arrayOf({ result -> result.number in setOf(1.0, 2.0, 3.0, 4.0, 5.0) }), + ) + } + + @Test + fun `opaque boolean union preserves both boolean values`() { + discoverProperties( + method = method("booleanUnion"), + { result -> result.number == 1.0 }, + { result -> result.number == 2.0 }, + { result -> result.number == 3.0 }, + invariants = arrayOf({ result -> result.number in setOf(1.0, 2.0, 3.0) }), + ) + } + + @Test + fun `opaque primitive literals retain their exact declared values`() { + discoverProperties( + method = method("exactPrimitiveLiterals"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } + private fun method(name: String): EtsMethod = getMethod(methodName = name, className = "FreshStringMock") } diff --git a/usvm-ts/src/test/resources/models/FreshStringMock.ts b/usvm-ts/src/test/resources/models/FreshStringMock.ts index 24961c5f6f..8a9593ac05 100644 --- a/usvm-ts/src/test/resources/models/FreshStringMock.ts +++ b/usvm-ts/src/test/resources/models/FreshStringMock.ts @@ -1,6 +1,13 @@ declare class ExternalString { static value(): string; static literal(): "known"; + static stringChoice(): "left" | "right"; + static finiteChoice(): "known" | 7 | true | null | undefined; + static booleanChoice(): "known" | boolean; + static numberLiteral(): 7; + static booleanLiteral(): true; + static nullLiteral(): null; + static undefinedLiteral(): undefined; } export class FreshStringMock { @@ -26,4 +33,37 @@ export class FreshStringMock { static literal(): string { return ExternalString.literal(); } + + static stringUnion(): number { + const value = ExternalString.stringChoice(); + if (value === "left") return 1; + if (value === "right") return 2; + return -1; + } + + static finiteUnion(): number { + const value = ExternalString.finiteChoice(); + if (typeof value === "string") return value === "known" ? 1 : -1; + if (typeof value === "number") return value === 7 ? 2 : -1; + if (typeof value === "boolean") return value === true ? 3 : -1; + if (value === null) return 4; + if (value === undefined) return 5; + return -1; + } + + static booleanUnion(): number { + const value = ExternalString.booleanChoice(); + if (value === "known") return 1; + if (value === true) return 2; + if (value === false) return 3; + return -1; + } + + static exactPrimitiveLiterals(): number { + if (ExternalString.numberLiteral() !== 7) return -1; + if (ExternalString.booleanLiteral() !== true) return -1; + if (ExternalString.nullLiteral() !== null) return -1; + if (ExternalString.undefinedLiteral() !== undefined) return -1; + return 1; + } } From efe95930698c37ba3129f4e8acb4619a36a57261 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:33:36 +0300 Subject: [PATCH 07/12] Keep runtime boundary diagnostics aligned with current frontend lowering --- .../org/usvm/machine/expr/TsExprResolver.kt | 13 ++++++++ .../machine/call/FreshStringMockSourceTest.kt | 4 +-- .../expr/RuntimeLimitationBoundariesTest.kt | 31 +++++++++++++++---- .../models/RuntimeLimitationBoundaries.ts | 11 +++++-- 4 files changed, 48 insertions(+), 11 deletions(-) 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 2973e52123..45932d7213 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 @@ -31,6 +31,7 @@ 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.EtsFileSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsGlobalRef import org.jacodb.ets.model.EtsGtEqExpr @@ -1522,6 +1523,18 @@ class TsExprResolver( override fun visit(expr: EtsNewExpr): UExpr? = with(ctx) { expr.constructorValue?.let { return@with constructRuntimeClass(it) } + val classType = expr.type as? EtsClassType + val intrinsicRegex = classType?.signature?.name == "RegExp" && + (classType.signature.file == EtsFileSignature.UNKNOWN || + scene.sdkClasses.any { owner -> owner.signature == classType.signature }) + if (intrinsicRegex) { + stopRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL, + detail = "Intrinsic RegExp allocation has no runtime model", + ) + return@with null + } + // Try to resolve the concrete type if possible. // Otherwise, create an object with UnclearRefType val resolvedType = if (expr.type.isResolved()) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt index 8616d268bc..e02c6b72ef 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/FreshStringMockSourceTest.kt @@ -66,12 +66,12 @@ class FreshStringMockSourceTest : TsMethodTestRunner() { val outcome = machine.analyzeWithOutcome(methods = listOf(method)) val values = outcome.states.map { state -> TsTestResolver().resolve(method, state).returnValue } val onlyCapacityResiduals = outcome.unsupportedPaths.all { diagnostic -> - "String concatenation result exceeds configured length bound 8" in diagnostic + "String concatenation result exceeds the configured length bound 8" in diagnostic } assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) assertTrue(outcome.unsupportedPaths.isNotEmpty()) - assertTrue(onlyCapacityResiduals) + assertTrue(onlyCapacityResiduals, outcome.unsupportedPaths.toString()) assertTrue(values.isNotEmpty()) assertTrue(values.all { value -> value is TsTestValue.TsString && value.value.endsWith("!") }) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt index bd339ed45f..8244fa9351 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt @@ -44,15 +44,18 @@ class RuntimeLimitationBoundariesTest : TsMethodTestRunner() { assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) assertTrue(outcome.states.isEmpty()) - assertTrue(outcome.unsupportedPaths.any { "REGULAR_EXPRESSION_LITERAL" in it }) + assertTrue( + outcome.unsupportedPaths.any { "REGULAR_EXPRESSION_LITERAL" in it }, + outcome.unsupportedPaths.toString(), + ) } assertEquals(listOf(TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL), observer.reasons) } @Test - fun `unsupported storage terminates while a supported sibling still returns`() { + fun `unsupported operand conversion terminates while a supported sibling still returns`() { val observer = RecordingObserver() - val target = method("unknownStorageOrSupportedSibling") + val target = method("unsupportedConversionOrSupportedSibling") TsMachine( scene = scene, @@ -64,14 +67,30 @@ class RuntimeLimitationBoundariesTest : TsMethodTestRunner() { val values = outcome.states.map { state -> TsTestResolver().resolve(target, state).returnValue } assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) - assertTrue(outcome.unsupportedPaths.any { "ARRAY_STORAGE_TYPE" in it }) - assertTrue(values.any { value -> value is TsTestValue.TsNumber && value.number == 7.0 }) + assertTrue( + outcome.unsupportedPaths.any { "STRING_CONCAT_OPERAND_CONVERSION" in it }, + outcome.unsupportedPaths.toString(), + ) + assertTrue(values.any { value -> value is TsTestValue.TsString && value.value == "supported" }) } assertTrue(observer.reasons.isNotEmpty()) - assertTrue(observer.reasons.all { reason -> reason == TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE }) + assertTrue( + observer.reasons.all { reason -> + reason == TsRuntimeFeatureLimitationReason.STRING_CONCAT_OPERAND_CONVERSION + }, + ) assertTrue(observer.reasons.size < 128) } + @Test + fun `ordinary numeric object key is not an array storage limitation`() { + discoverProperties( + method = method("ordinaryNumericKeyField"), + { result -> result.number == 17.0 }, + invariants = arrayOf({ result -> result.number == 17.0 }), + ) + } + @Test fun `ordinary object length is read as its actual field`() { discoverProperties( diff --git a/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts b/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts index ae4a5a0b02..8c734dbc94 100644 --- a/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts +++ b/usvm-ts/src/test/resources/models/RuntimeLimitationBoundaries.ts @@ -3,9 +3,14 @@ export class RuntimeLimitationBoundaries { return /value/.test("value"); } - static unknownStorageOrSupportedSibling(flag: boolean, values: unknown): number { - if (flag) return 7; - return (values as any)[0]; + static unsupportedConversionOrSupportedSibling(flag: boolean, value: { field: number }): string { + if (flag) return "supported"; + return "prefix" + value; + } + + static ordinaryNumericKeyField(): number { + const value = { 0: 17 }; + return value[0]; } static ordinaryLengthField(): number { From eead173f36258858ec384705f94415d14eceb0ce Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:46:29 +0300 Subject: [PATCH 08/12] Pin the published JacoDB runtime prerequisite artifact --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index c3fd4b5fd6..541d682c48 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "bcad76ffd7" + const val jacodb = "ab4caf1fca" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" From 93ee014e37b9bcc33dd787db8febad5ac6e4a893 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:53:54 +0300 Subject: [PATCH 09/12] Clarify runtime owner checks and field length dispatch --- .../kotlin/org/usvm/machine/expr/ReadField.kt | 17 +++++++++-------- .../org/usvm/machine/expr/TsExprResolver.kt | 9 ++++++--- 2 files changed, 15 insertions(+), 11 deletions(-) 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 ca412afd0a..5f491b230a 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 @@ -95,16 +95,17 @@ internal fun TsExprResolver.handleInstanceFieldRef( storageType.signature.file == EtsClassSignature.UNKNOWN.file && storageType.signature.name in NATIVE_TYPED_ARRAY_NAMES if (value.field.name == "length" && (usesArrayLength || nativeTypedArray)) { - 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 = scope, - instanceLocal = instanceLocal, - instance = instance, - maxArraySize = options.maxArraySize, - onFeatureLimitation = ::reportRuntimeFeatureLimitation, - ) + if (!isObjectProperty) { + return readLengthProperty( + scope = scope, + instanceLocal = instanceLocal, + instance = instance, + maxArraySize = options.maxArraySize, + onFeatureLimitation = ::reportRuntimeFeatureLimitation, + ) + } } // Read the field. 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 45932d7213..5484d7d03e 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 @@ -1524,9 +1524,12 @@ class TsExprResolver( expr.constructorValue?.let { return@with constructRuntimeClass(it) } val classType = expr.type as? EtsClassType - val intrinsicRegex = classType?.signature?.name == "RegExp" && - (classType.signature.file == EtsFileSignature.UNKNOWN || - scene.sdkClasses.any { owner -> owner.signature == classType.signature }) + val hasRegexName = classType?.signature?.name == "RegExp" + val hasIntrinsicOwner = classType != null && ( + classType.signature.file == EtsFileSignature.UNKNOWN || + scene.sdkClasses.any { owner -> owner.signature == classType.signature } + ) + val intrinsicRegex = hasRegexName && hasIntrinsicOwner if (intrinsicRegex) { stopRuntimeFeatureLimitation( reason = TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL, From e495f604309ac58f48c84ee8a7525ec08cca2468 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 05:11:21 +0300 Subject: [PATCH 10/12] Expect typed frontend diagnostics in prototype regression --- .../kotlin/org/usvm/samples/operators/InOperatorPresenceTest.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index e2519d5615..4bccaa953c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/InOperatorPresenceTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/InOperatorPresenceTest.kt @@ -114,7 +114,7 @@ class InOperatorPresenceTest : PropertyTestRunner("/samples/operators/InOperator val rejectedByInterpreter = outcome.unsupportedPaths.any { "prototype mutation" in it } // The native frontend rejects special __proto__ initializers before interpreter execution. val rejectedByFrontend = isPrototypeInitializer && outcome.unsupportedPaths.any { - it.startsWith("Unsupported frontend value: UnsupportedValue") && + it.startsWith("FRONTEND_UNSUPPORTED_VALUE: Unsupported frontend value: UnsupportedValue") && "\"kindName\":\"ObjectLiteralExpression\"" in it && "__proto__" in it } assertTrue(rejectedByInterpreter || rejectedByFrontend, "${outcome.unsupportedPaths}") From e4605cab72522c26f330acb80dae33434cbfcd00 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 13 Oct 2026 11:49:49 +0300 Subject: [PATCH 11/12] Use merged JacoDB neo for declared nullish call results --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 541d682c48..a2b43d6e04 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "ab4caf1fca" + const val jacodb = "7596ae5834" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" From f4be539696011ce3527bfa767a8d3729a5a94970 Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 13 Oct 2026 12:15:51 +0300 Subject: [PATCH 12/12] Restore the fake type constraint invariant --- .../org/usvm/machine/types/TsTypeSystem.kt | 10 ++--- .../usvm/machine/types/TsTypeSystemTest.kt | 43 ++++++++----------- 2 files changed, 22 insertions(+), 31 deletions(-) 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 87879a401f..ccfeba6150 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 @@ -53,6 +53,10 @@ class TsTypeSystem( val unwrappedSupertype = unwrapAlias(supertype) val unwrappedType = unwrapAlias(type) + require(unwrappedType !is EtsFakeType && unwrappedSupertype !is EtsFakeType) { + "Fake types should not occur in type constraints" + } + // Runtime object checks exclude primitive and nullish values, independently of TS assignability. if (unwrappedSupertype == EtsObjectType) return unwrappedType is EtsRefType @@ -74,12 +78,6 @@ class TsTypeSystem( // "never" is the universal subtype: never can be assigned to any type. if (unwrappedType is EtsNeverType) return true - // A fake type only matches itself. Distinct wrappers do not establish a - // TypeScript subtype relation; callers handle those branches explicitly. - if (unwrappedType is EtsFakeType || unwrappedSupertype is EtsFakeType) { - return unwrappedSupertype === unwrappedType - } - // When "never" is in supertype position, only never <: never. if (unwrappedSupertype is EtsNeverType) return type is EtsNeverType 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 9dd4449224..a44475a890 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 @@ -10,6 +10,7 @@ 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.EtsNeverType import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsScene @@ -21,16 +22,16 @@ import org.junit.jupiter.api.Test import org.usvm.machine.TsContext import org.usvm.machine.withCoreRuntimeSdk import org.usvm.types.TypesResult -import org.usvm.types.USingleTypeStream import org.usvm.util.EtsHierarchy import org.usvm.util.type +import kotlin.test.assertFailsWith import kotlin.test.assertFalse import kotlin.test.assertTrue import kotlin.time.Duration.Companion.seconds class TsTypeSystemTest { @Test - fun `synthetic wrapper does not satisfy structural type constraints`() { + fun `fake types are rejected in type constraints before subtype shortcuts`() { val scene = EtsScene(projectFiles = emptyList()) val context = TsContext(scene = scene, components = mockk()) val typeSystem = TsTypeSystem( @@ -39,31 +40,23 @@ class TsTypeSystemTest { hierarchy = EtsHierarchy(scene), ) val fakeType = EtsFakeType.mkRef(context) - val structuralType = EtsAuxiliaryType(properties = setOf("style")) - - val fakeHasProperty = typeSystem.isSupertype(structuralType, fakeType) - val propertyHasFakeType = typeSystem.isSupertype(fakeType, structuralType) - - assertFalse(fakeHasProperty) - assertFalse(propertyHasFakeType) - } - - @Test - fun `fake type remains in a singleton stream after filtering by itself`() { - val scene = EtsScene(projectFiles = emptyList()) - val context = TsContext(scene = scene, components = mockk()) - val typeSystem = TsTypeSystem( - scene = scene, - typeOperationsTimeout = 1.seconds, - hierarchy = EtsHierarchy(scene), + val comparisonTypes = listOf( + EtsAuxiliaryType(properties = setOf("style")), + EtsAnyType, + EtsUnknownType, + EtsNeverType, + EtsObjectType, + fakeType, ) - val fakeType = EtsFakeType.mkRef(context) - val stream = USingleTypeStream(typeSystem = typeSystem, singleType = fakeType) - - val filtered = stream.filterBySupertype(fakeType).filterBySubtype(fakeType) - assertTrue(typeSystem.isSupertype(fakeType, fakeType)) - assertFalse(filtered.isEmpty ?: true) + for (type in comparisonTypes) { + assertFailsWith { + typeSystem.isSupertype(supertype = type, type = fakeType) + } + assertFailsWith { + typeSystem.isSupertype(supertype = fakeType, type = type) + } + } } @Test