[TS] Support globals and imports

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

@@ -2,14 +2,19 @@ package org.usvm.machine.expr
 
 import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsStringType
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.api.makeSymbolicPrimitive
 import org.usvm.isFalse
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsSizeSort
 import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.TsState
 import org.usvm.machine.types.EtsFakeType
 import org.usvm.machine.types.ExprWithTypeConstraint
 import org.usvm.types.single
@@ -182,3 +187,47 @@ fun TsContext.mkNullishExpr(
     // Non-reference types (numbers, booleans, strings) are never nullish
     return mkFalse()
 }
+
+fun TsState.throwException(reason: String) {
+    val ref = ctx.mkStringConstantRef(reason)
+    methodResult = TsMethodResult.TsException(ref, EtsStringType)
+}
+
+fun TsContext.checkUndefinedOrNullPropertyRead(
+    scope: TsStepScope,
+    instance: UHeapRef,
+    propertyName: String,
+): Unit? {
+    val ref = instance.unwrapRef(scope)
+    val condition = mkAnd(
+        mkNot(mkHeapRefEq(ref, mkUndefinedValue())),
+        mkNot(mkHeapRefEq(ref, mkTsNullValue())),
+    )
+    return scope.fork(
+        condition,
+        blockOnFalseState = { throwException("Undefined or null property access: $propertyName of $ref") }
+    )
+}
+
+fun TsContext.checkNegativeIndexRead(
+    scope: TsStepScope,
+    index: UExpr<TsSizeSort>,
+): Unit? {
+    val condition = mkBvSignedGreaterOrEqualExpr(index, mkBv(0))
+    return scope.fork(
+        condition,
+        blockOnFalseState = { throwException("Negative index access: $index") }
+    )
+}
+
+fun TsContext.checkReadingInRange(
+    scope: TsStepScope,
+    index: UExpr<TsSizeSort>,
+    length: UExpr<TsSizeSort>,
+): Unit? {
+    val condition = mkBvSignedLessExpr(index, length)
+    return scope.fork(
+        condition,
+        blockOnFalseState = { throwException("Index out of bounds: $index, length: $length") }
+    )
+}

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

@@ -0,0 +1,134 @@
+package org.usvm.machine.expr
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayAccess
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsBooleanType
+import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsUnknownType
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.api.typeStreamOf
+import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.machine.TsContext
+import org.usvm.machine.TsSizeSort
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.types.mkFakeValue
+import org.usvm.sizeSort
+import org.usvm.types.first
+import org.usvm.util.mkArrayIndexLValue
+import org.usvm.util.mkArrayLengthLValue
+
+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 arrayRef = array.asExpr(addressSort)
+
+    // Check for undefined or null array access.
+    checkUndefinedOrNullPropertyRead(scope, arrayRef, "[]") ?: return null
+
+    // Resolve the index.
+    val resolvedIndex = resolve(value.index) ?: return null
+    check(resolvedIndex.sort == fp64Sort) {
+        "Expected fp64 sort for index, got: ${resolvedIndex.sort}"
+    }
+    val index = resolvedIndex.asExpr(fp64Sort)
+
+    // Convert the index to a bit-vector.
+    val bvIndex = mkFpToBvExpr(
+        roundingMode = fpRoundingModeSortDefaultValue(),
+        value = index,
+        bvSize = sizeSort.sizeBits.toInt(),
+        isSigned = true,
+    ).asExpr(sizeSort)
+
+    // Determine the array type.
+    val arrayType = if (isAllocatedConcreteHeapRef(arrayRef)) {
+        scope.calcOnState { memory.typeStreamOf(arrayRef).first() }
+    } else {
+        value.array.type
+    }
+    check(arrayType is EtsArrayType) {
+        "Expected EtsArrayType, got: ${value.array.type}"
+    }
+
+    // Read the array element.
+    readArray(scope, arrayRef, bvIndex, arrayType)
+}
+
+fun TsContext.readArray(
+    scope: TsStepScope,
+    array: UHeapRef,
+    index: UExpr<TsSizeSort>,
+    arrayType: EtsArrayType,
+): UExpr<*>? {
+    // Read the array length.
+    val length = scope.calcOnState {
+        val lengthLValue = mkArrayLengthLValue(array, arrayType)
+        memory.read(lengthLValue)
+    }
+
+    // Check for out-of-bounds access.
+    checkNegativeIndexRead(scope, index) ?: return null
+    checkReadingInRange(scope, index, length) ?: return null
+
+    // Determine the element sort.
+    val sort = typeToSort(arrayType.elementType)
+
+    // If the element type is known, we can read it directly.
+    if (sort !is TsUnresolvedSort) {
+        val lValue = mkArrayIndexLValue(
+            sort = sort,
+            ref = array,
+            index = index,
+            type = arrayType,
+        )
+        return scope.calcOnState { memory.read(lValue) }
+    }
+
+    // Concrete arrays with the unresolved sort should consist of fake objects only.
+    if (array is UConcreteHeapRef) {
+        // Read a fake object from the array.
+        val lValue = mkArrayIndexLValue(
+            sort = addressSort,
+            ref = array,
+            index = index,
+            type = arrayType,
+        )
+        return scope.calcOnState { memory.read(lValue) }
+    }
+
+    // If the element type is unresolved, we need to create a fake object
+    // that can hold boolean, number, and reference values.
+    // We read all three types from the array and combine them into a fake object.
+    return scope.calcOnState {
+        val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1)
+        val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType)
+        val bool = memory.read(boolLValue)
+
+        val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1)
+        val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType)
+        val fp = memory.read(fpLValue)
+
+        val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
+        val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType)
+        val ref = memory.read(refLValue)
+
+        // If the read reference is already a fake object, we can return it directly.
+        // Otherwise, we need to create a new fake object and write it back to the memory.
+        if (ref.isFakeObject()) {
+            ref
+        } else {
+            val fakeObj = mkFakeValue(bool, fp, ref)
+            lValuesToAllocatedFakeObjects += refLValue to fakeObj
+            memory.write(refLValue, fakeObj, guard = trueExpr)
+            fakeObj
+        }
+    }
+}

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

@@ -0,0 +1,171 @@
+package org.usvm.machine.expr
+
+import io.ksmt.utils.asExpr
+import mu.KotlinLogging
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsFieldSignature
+import org.jacodb.ets.model.EtsInstanceFieldRef
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsStaticFieldRef
+import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.machine.TsContext
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.interpreter.isInitialized
+import org.usvm.machine.interpreter.markInitialized
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.localsCount
+import org.usvm.machine.state.newStmt
+import org.usvm.machine.types.EtsAuxiliaryType
+import org.usvm.machine.types.mkFakeValue
+import org.usvm.util.EtsHierarchy
+import org.usvm.util.TsResolutionResult
+import org.usvm.util.createFakeField
+import org.usvm.util.mkFieldLValue
+import org.usvm.util.resolveEtsField
+
+private val logger = KotlinLogging.logger {}
+
+internal fun TsExprResolver.handleInstanceFieldRef(
+    value: EtsInstanceFieldRef,
+): UExpr<*>? = with(ctx) {
+    val instanceLocal = value.instance
+
+    // Resolve the instance.
+    val instance = resolve(instanceLocal) ?: return null
+    check(instance.sort == addressSort) {
+        "Expected address sort for instance, got: ${instance.sort}"
+    }
+    val instanceRef = instance.asExpr(addressSort)
+
+    // TODO: consider moving this to 'readField'
+    // Check for undefined or null property access.
+    checkUndefinedOrNullPropertyRead(scope, instanceRef, value.field.name) ?: return null
+
+    // Handle reading "length" property for arrays.
+    if (value.field.name == "length" && instanceLocal.type is EtsArrayType) {
+        return readLengthArray(scope, instanceLocal, instanceRef)
+    }
+
+    // Handle reading "length" property for fake objects.
+    // TODO: handle "length" property for arrays inside fake objects
+    if (value.field.name == "length" && instanceRef.isFakeObject()) {
+        return readLengthFake(scope, instanceLocal, instanceRef)
+    }
+
+    // Read the field.
+    return readField(scope, instanceLocal, instanceRef, value.field, hierarchy)
+}
+
+internal fun TsContext.readField(
+    scope: TsStepScope,
+    instanceLocal: EtsLocal?,
+    instance: UHeapRef,
+    field: EtsFieldSignature,
+    hierarchy: EtsHierarchy,
+): UExpr<*> {
+    // Unwrap to get non-fake reference.
+    val unwrappedInstance = instance.unwrapRef(scope)
+
+    val sort = when (val etsField = resolveEtsField(instanceLocal, field, hierarchy)) {
+        is TsResolutionResult.Empty -> {
+            if (field.name !in listOf("i", "LogLevel")) {
+                logger.warn { "Field $field not found, creating fake field" }
+            }
+            // If we didn't find any real fields, let's create a fake one.
+            // 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.
+            unwrappedInstance.createFakeField(scope, field.name)
+            addressSort
+        }
+
+        is TsResolutionResult.Unique -> typeToSort(etsField.property.type)
+
+        is TsResolutionResult.Ambiguous -> unresolvedSort
+    }
+
+    scope.doWithState {
+        // If we accessed some field, we make an assumption that
+        // this field should present in the object.
+        // That's not true in the common case for TS, but that's the decision we made.
+        val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name))
+        // assert is required to update models
+        scope.assert(memory.types.evalIsSubtype(unwrappedInstance, auxiliaryType))
+    }
+
+    // If the field type is known, we can read it directly.
+    if (sort !is TsUnresolvedSort) {
+        val lValue = mkFieldLValue(sort, unwrappedInstance, field)
+        return scope.calcOnState { memory.read(lValue) }
+    }
+
+    // If the field type is unknown, we create a fake object.
+    return scope.calcOnState {
+        val boolLValue = mkFieldLValue(boolSort, instance, field)
+        val fpLValue = mkFieldLValue(fp64Sort, instance, field)
+        val refLValue = mkFieldLValue(addressSort, instance, field)
+
+        val bool = memory.read(boolLValue)
+        val fp = memory.read(fpLValue)
+        val ref = memory.read(refLValue)
+
+        // If a fake object is already created and assigned to the field,
+        // there is no need to recreate another one.
+        if (ref.isFakeObject()) {
+            ref
+        } else {
+            val fakeObj = mkFakeValue(bool, fp, ref)
+            lValuesToAllocatedFakeObjects += refLValue to fakeObj
+            memory.write(refLValue, fakeObj, guard = trueExpr)
+            fakeObj
+        }
+    }
+}
+
+internal fun TsExprResolver.handleStaticFieldRef(
+    value: EtsStaticFieldRef,
+): UExpr<*>? = with(ctx) {
+    return readStaticField(scope, value.field, hierarchy)
+}
+
+internal fun TsContext.readStaticField(
+    scope: TsStepScope,
+    field: EtsFieldSignature,
+    hierarchy: EtsHierarchy,
+): UExpr<*>? {
+    val clazz = scene.projectAndSdkClasses.singleOrNull {
+        it.signature == field.enclosingClass
+    } ?: return null
+
+    val instance = scope.calcOnState { getStaticInstance(clazz) }
+
+    val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME }
+    if (initializer != null) {
+        val isInitialized = scope.calcOnState { isInitialized(clazz) }
+        if (isInitialized) {
+            scope.doWithState {
+                // TODO: Handle static initializer result
+                val result = methodResult
+                // TODO: Why this signature check is needed?
+                // TODO: Why we need to reset methodResult here? Double-check that it is even set anywhere.
+                if (result is TsMethodResult.Success && result.methodSignature == initializer.signature) {
+                    methodResult = TsMethodResult.NoCall
+                }
+            }
+        } else {
+            scope.doWithState {
+                markInitialized(clazz)
+                pushSortsForArguments(instance = null, args = emptyList()) { getLocalIdx(it, lastEnteredMethod) }
+                registerCallee(currentStatement, initializer.cfg)
+                callStack.push(initializer, currentStatement)
+                memory.stack.push(arrayOf(instance), initializer.localsCount)
+                newStmt(initializer.cfg.stmts.first())
+            }
+            return null
+        }
+    }
+
+    return readField(scope, null, instance, field, hierarchy)
+}