[TS] Support globals and imports

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 = "d3e97200d6"
+    const val jacodb = "3629f15faf"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt

@@ -22,12 +22,13 @@ fun mockMethodCall(
             result = when (sort) {
                 is UAddressSort -> makeSymbolicRefUntyped()
 
-                is TsUnresolvedSort -> ctx.mkFakeValue(
-                    scope,
-                    makeSymbolicPrimitive(ctx.boolSort),
-                    makeSymbolicPrimitive(ctx.fp64Sort),
-                    makeSymbolicRefUntyped()
-                )
+                is TsUnresolvedSort -> scope.calcOnState {
+                    mkFakeValue(
+                        makeSymbolicPrimitive(ctx.boolSort),
+                        makeSymbolicPrimitive(ctx.fp64Sort),
+                        makeSymbolicRefUntyped()
+                    )
+                }
 
                 else -> makeSymbolicPrimitive(sort)
             }

usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt

@@ -30,7 +30,12 @@ sealed interface TsTestValue {
     data object TsUnknown : TsTestValue
     data object TsNull : TsTestValue
     data object TsUndefined : TsTestValue
-    data object TsException : TsTestValue
+
+    sealed interface TsException : TsTestValue {
+        data object UnknownException : TsException
+        data class StringException(val message: String) : TsException
+        data class ObjectException(val value: TsTestValue) : TsException
+    }
 
     data class TsBoolean(val value: Boolean) : TsTestValue
 

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

@@ -8,15 +8,20 @@ import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsEnumValueType
 import org.jacodb.ets.model.EtsGenericType
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsParameterRef
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStringType
+import org.jacodb.ets.model.EtsThis
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUndefinedType
 import org.jacodb.ets.model.EtsUnionType
 import org.jacodb.ets.model.EtsUnknownType
+import org.jacodb.ets.model.EtsValue
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
@@ -111,6 +116,23 @@ class TsContext(
         return heapRefToStringConstant[ref]
     }
 
+    fun getLocalIdx(local: EtsValue, method: EtsMethod): Int? =
+        // Note: below, 'n' means the number of arguments
+        when (local) {
+            // Note: 'this' has index 0
+            is EtsThis -> 0
+
+            // Note: arguments have indices from 1 to n
+            is EtsParameterRef -> local.index + 1
+
+            // Note: locals have indices starting from (n+1)
+            is EtsLocal -> method.locals.indexOfFirst { it.name == local.name }
+                .takeIf { it >= 0 }
+                ?.let { it + method.parameters.size + 1 }
+
+            else -> error("Unexpected local: $local")
+        }
+
     fun typeToSort(type: EtsType): USort = when (type) {
         is EtsBooleanType -> boolSort
         is EtsNumberType -> fp64Sort
@@ -272,7 +294,7 @@ class TsContext(
     fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
         return scope.calcOnState { extractRef(memory) }
     }
-    
+
     // This is an identifier for a special function representing the 'resolve' function used in promises.
     // It is not a real function in the code, but we need it to handle promise resolution.
     val resolveFunctionRef: UConcreteHeapRef = allocateConcreteRef()

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

@@ -1,8 +1,6 @@
 package org.usvm.machine.expr
 
-import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
-import io.ksmt.utils.cast
 import mu.KotlinLogging
 import org.jacodb.ets.model.EtsAddExpr
 import org.jacodb.ets.model.EtsAndExpr
@@ -73,7 +71,6 @@ import org.jacodb.ets.model.EtsStringConstant
 import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsSubExpr
 import org.jacodb.ets.model.EtsThis
-import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsTypeOfExpr
 import org.jacodb.ets.model.EtsUnaryExpr
 import org.jacodb.ets.model.EtsUnaryPlusExpr
@@ -87,21 +84,17 @@ import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
 import org.jacodb.ets.utils.getDeclaredLocals
-import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
-import org.usvm.UBoolSort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.UIteExpr
 import org.usvm.USort
-import org.usvm.api.allocateConcreteRef
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.initializeArrayLength
 import org.usvm.api.makeSymbolicPrimitive
 import org.usvm.api.mockMethodCall
 import org.usvm.api.typeStreamOf
-import org.usvm.dataflow.ts.infer.tryGetKnownType
 import org.usvm.dataflow.ts.util.type
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.machine.Constants
@@ -136,7 +129,6 @@ import org.usvm.util.isResolved
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
-import org.usvm.util.mkRegisterStackLValue
 import org.usvm.util.resolveEtsField
 import org.usvm.util.resolveEtsMethods
 import org.usvm.util.throwExceptionWithoutStackFrameDrop
@@ -161,12 +153,11 @@ private const val ECMASCRIPT_BITWISE_SHIFT_MASK = 0b11111
 class TsExprResolver(
     internal val ctx: TsContext,
     internal val scope: TsStepScope,
-    private val localToIdx: (EtsMethod, EtsValue) -> Int?,
     private val hierarchy: EtsHierarchy,
 ) : EtsEntity.Visitor<UExpr<out USort>?> {
 
     val simpleValueResolver: TsSimpleValueResolver =
-        TsSimpleValueResolver(ctx, scope, localToIdx)
+        TsSimpleValueResolver(ctx, scope)
 
     fun resolve(expr: EtsEntity): UExpr<out USort>? {
         return expr.accept(this)
@@ -217,15 +208,15 @@ class TsExprResolver(
 
     // region SIMPLE VALUE
 
-    override fun visit(value: EtsLocal): UExpr<out USort> {
+    override fun visit(value: EtsLocal): UExpr<out USort>? {
         return simpleValueResolver.visit(value)
     }
 
-    override fun visit(value: EtsParameterRef): UExpr<out USort> {
+    override fun visit(value: EtsParameterRef): UExpr<out USort>? {
         return simpleValueResolver.visit(value)
     }
 
-    override fun visit(value: EtsThis): UExpr<out USort> {
+    override fun visit(value: EtsThis): UExpr<out USort>? {
         return simpleValueResolver.visit(value)
     }
 
@@ -1182,7 +1173,7 @@ class TsExprResolver(
                     val fakeObj = if (refValue.isFakeObject()) {
                         refValue
                     } else {
-                        mkFakeValue(scope, boolValue, fpValue, refValue).also {
+                        mkFakeValue(boolValue, fpValue, refValue).also {
                             lValuesToAllocatedFakeObjects += refLValue to it
                         }
                     }
@@ -1215,7 +1206,7 @@ class TsExprResolver(
 
         scope.fork(
             neqNull,
-            blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
+            blockOnFalseState = allocateException("Undefined or null property access: $ref")
         )
     }
 
@@ -1224,7 +1215,7 @@ class TsExprResolver(
 
         scope.fork(
             condition,
-            blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
+            blockOnFalseState = allocateException("Negative index access: $index")
         )
     }
 
@@ -1233,13 +1224,13 @@ class TsExprResolver(
 
         scope.fork(
             condition,
-            blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
+            blockOnFalseState = allocateException("Index out of bounds: $index, length: $length")
         )
     }
 
-    private fun allocateException(type: EtsType): (TsState) -> Unit = { state ->
-        val address = state.memory.allocConcrete(type)
-        state.throwExceptionWithoutStackFrameDrop(address, type)
+    private fun allocateException(reason: String): (TsState) -> Unit = { state ->
+        val s = ctx.mkStringConstantRef(reason)
+        state.throwExceptionWithoutStackFrameDrop(s, EtsStringType)
     }
 
     private fun handleFieldRef(
@@ -1261,7 +1252,7 @@ class TsExprResolver(
                 // It is possible due to mistakes in the IR or if the field was added explicitly
                 // in the code.
                 // Probably, the right behaviour here is to fork the state.
-                resolvedAddr.createFakeField(field.name, scope)
+                resolvedAddr.createFakeField(scope, field.name)
                 addressSort
             }
 
@@ -1293,7 +1284,7 @@ class TsExprResolver(
                 val fakeRef = if (ref.isFakeObject()) {
                     ref
                 } else {
-                    mkFakeValue(scope, bool, fp, ref).also {
+                    mkFakeValue(bool, fp, ref).also {
                         lValuesToAllocatedFakeObjects += refLValue to it
                     }
                 }
@@ -1438,7 +1429,7 @@ class TsExprResolver(
             } else {
                 scope.doWithState {
                     markInitialized(clazz)
-                    pushSortsForArguments(instance = null, args = emptyList(), localToIdx)
+                    pushSortsForArguments(instance = null, args = emptyList()) { getLocalIdx(it, lastEnteredMethod) }
                     registerCallee(currentStatement, initializer.cfg)
                     callStack.push(initializer, currentStatement)
                     memory.stack.push(arrayOf(instanceRef), initializer.localsCount)
@@ -1541,7 +1532,7 @@ class TsExprResolver(
 
             scope.fork(
                 condition,
-                blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
+                blockOnFalseState = allocateException("Invalid array size: ${size.asExpr(fp64Sort)}")
             )
 
             if (arrayType.elementType is EtsArrayType) {
@@ -1561,124 +1552,13 @@ class TsExprResolver(
 class TsSimpleValueResolver(
     private val ctx: TsContext,
     private val scope: TsStepScope,
-    private val localToIdx: (EtsMethod, EtsValue) -> Int?,
 ) : EtsValue.Visitor<UExpr<out USort>?> {
 
-    private fun resolveLocal(local: EtsValue): UExpr<*> = with(ctx) {
-        val currentMethod = scope.calcOnState { lastEnteredMethod }
-        val entrypoint = scope.calcOnState { entrypoint }
-
-        val localIdx = localToIdx(currentMethod, local)
-
-        // If there is no local variable corresponding to the local,
-        // we treat it as a field of some global object with the corresponding name.
-        // It helps us to support global variables that are missed in the IR.
-        if (localIdx == null) {
-            require(local is EtsLocal)
-
-            // Handle closures
-            if (local.name.startsWith("%closures")) {
-                val existingClosures = scope.calcOnState { closureObject[local.name] }
-                if (existingClosures != null) {
-                    return existingClosures
-                }
-                val type = local.type
-                check(type is EtsLexicalEnvType)
-                val obj = allocateConcreteRef()
-                for (captured in type.closures) {
-                    val resolvedCaptured = resolveLocal(captured)
-                    val lValue = mkFieldLValue(resolvedCaptured.sort, obj, captured.name)
-                    scope.doWithState {
-                        memory.write(lValue, resolvedCaptured.cast(), guard = ctx.trueExpr)
-                    }
-                }
-                scope.doWithState {
-                    setClosureObject(local.name, obj)
-                }
-                return obj
-            }
-
-            val globalObject = scope.calcOnState { globalObject }
-
-            val localName = local.name
-            // Check whether this local was already created or not
-            if (localName in scope.calcOnState { addedArtificialLocals }) {
-                val sort = ctx.typeToSort(local.type)
-                val lValue = if (sort is TsUnresolvedSort) {
-                    mkFieldLValue(ctx.addressSort, globalObject, local.name)
-                } else {
-                    mkFieldLValue(sort, globalObject, local.name)
-                }
-                return scope.calcOnState { memory.read(lValue) }
-            }
-
-            logger.warn { "Cannot resolve local $local, creating a field of the global object" }
-
-            scope.doWithState {
-                addedArtificialLocals += localName
-            }
-
-            val sort = ctx.typeToSort(local.type)
-            val lValue = if (sort is TsUnresolvedSort) {
-                globalObject.createFakeField(localName, scope)
-                mkFieldLValue(ctx.addressSort, globalObject, local.name)
-            } else {
-                mkFieldLValue(sort, globalObject, local.name)
-            }
-            return scope.calcOnState { memory.read(lValue) }
-        }
-
-        val sort = scope.calcOnState {
-            val type = local.tryGetKnownType(currentMethod)
-            getOrPutSortForLocal(localIdx, type)
-        }
-
-        // If we are not in the entrypoint, all correct values are already resolved and we can just return
-        // a registerStackLValue for the local
-        if (currentMethod != entrypoint) {
-            val lValue = mkRegisterStackLValue(sort, localIdx)
-            return scope.calcOnState { memory.read(lValue) }
-        }
-
-        // arguments and this for the first stack frame
-        when (sort) {
-            is UBoolSort -> {
-                val lValue = mkRegisterStackLValue(sort, localIdx)
-                scope.calcOnState { memory.read(lValue) }
-            }
-
-            is KFp64Sort -> {
-                val lValue = mkRegisterStackLValue(sort, localIdx)
-                scope.calcOnState { memory.read(lValue) }
-            }
-
-            is UAddressSort -> {
-                val lValue = mkRegisterStackLValue(sort, localIdx)
-                scope.calcOnState { memory.read(lValue) }
-            }
-
-            is TsUnresolvedSort -> {
-                check(local is EtsThis || local is EtsParameterRef) {
-                    "Only This and ParameterRef are expected here"
-                }
-
-                val boolRValue = ctx.mkRegisterReading(localIdx, ctx.boolSort)
-                val fpRValue = ctx.mkRegisterReading(localIdx, ctx.fp64Sort)
-                val refRValue = ctx.mkRegisterReading(localIdx, ctx.addressSort)
-
-                val fakeObject = ctx.mkFakeValue(scope, boolRValue, fpRValue, refRValue)
-                val lValue = mkRegisterStackLValue(ctx.addressSort, localIdx)
-                scope.calcOnState {
-                    memory.write(lValue, fakeObject.asExpr(ctx.addressSort), guard = ctx.trueExpr)
-                }
-                fakeObject
-            }
-
-            else -> error("Unsupported sort $sort")
-        }
+    private fun resolveLocal(local: EtsValue): UExpr<*>? = with(ctx) {
+        resolveLocal(scope, local)
     }
 
-    override fun visit(local: EtsLocal): UExpr<out USort> {
+    override fun visit(local: EtsLocal): UExpr<out USort>? {
         if (local.name == "NaN") {
             return ctx.mkFp64NaN()
         }
@@ -1710,11 +1590,11 @@ class TsSimpleValueResolver(
         return resolveLocal(local)
     }
 
-    override fun visit(value: EtsParameterRef): UExpr<out USort> {
+    override fun visit(value: EtsParameterRef): UExpr<out USort>? {
         return resolveLocal(value)
     }
 
-    override fun visit(value: EtsThis): UExpr<out USort> {
+    override fun visit(value: EtsThis): UExpr<out USort>? {
         return resolveLocal(value)
     }