Support static fields

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

@@ -120,10 +120,7 @@ class TsContext(
     fun UExpr<out USort>.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr<out USort>? {
         if (!isFakeObject()) return null
 
-        val type = scope.calcOnState {
-            memory.types.getTypeStream(this@extractSingleValueFromFakeObjectOrNull).single() as FakeType
-        }
-
+        val type = getFakeType(scope)
         return scope.calcOnState {
             when {
                 type.boolTypeExpr.isTrue -> {

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

@@ -16,5 +16,6 @@ class TsComposer(
     ownership: MutabilityOwnership,
 ) : UComposer<EtsType, TsSizeSort>(ctx, memory, ownership), TsTransformer
 
-class TsExprTranslator(ctx: UContext<TsSizeSort>) : UExprTranslator<EtsType, TsSizeSort>(ctx), TsTransformer
-
+class TsExprTranslator(
+    ctx: UContext<TsSizeSort>,
+) : UExprTranslator<EtsType, TsSizeSort>(ctx), TsTransformer

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

@@ -64,15 +64,14 @@ import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.base.EtsTypeOfExpr
 import org.jacodb.ets.base.EtsUnaryExpr
 import org.jacodb.ets.base.EtsUnaryPlusExpr
-import org.jacodb.ets.base.EtsUnclearRefType
 import org.jacodb.ets.base.EtsUndefinedConstant
 import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.base.EtsUnsignedRightShiftExpr
 import org.jacodb.ets.base.EtsValue
 import org.jacodb.ets.base.EtsVoidExpr
 import org.jacodb.ets.base.EtsYieldExpr
+import org.jacodb.ets.base.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.base.UNKNOWN_CLASS_NAME
-import org.jacodb.ets.model.EtsField
 import org.jacodb.ets.model.EtsFieldSignature
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsMethodSignature
@@ -86,12 +85,15 @@ import org.usvm.api.allocateArray
 import org.usvm.isTrue
 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.operator.TsBinaryOperator
 import org.usvm.machine.operator.TsUnaryOperator
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
 import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
+import org.usvm.machine.state.parametersWithThisCount
 import org.usvm.machine.types.FakeType
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.memory.ULValue
@@ -101,6 +103,7 @@ 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.throwExceptionWithoutStackFrameDrop
 
 private val logger = KotlinLogging.logger {}
@@ -111,7 +114,7 @@ class TsExprResolver(
     private val localToIdx: (EtsMethod, EtsValue) -> Int,
 ) : EtsEntity.Visitor<UExpr<out USort>?> {
 
-    private val simpleValueResolver: TsSimpleValueResolver =
+    val simpleValueResolver: TsSimpleValueResolver =
         TsSimpleValueResolver(ctx, scope, localToIdx)
 
     fun resolve(expr: EtsEntity): UExpr<out USort>? {
@@ -446,11 +449,10 @@ class TsExprResolver(
             doWithState {
                 val method = resolveInstanceCall(expr.instance, expr.method)
 
+                check(args.size == method.parametersWithThisCount)
                 pushSortsForArguments(expr.instance, expr.args, localToIdx)
-
                 callStack.push(method, currentStatement)
                 memory.stack.push(args.toTypedArray(), method.localsCount)
-
                 newStmt(method.cfg.stmts.first())
             }
         }
@@ -610,46 +612,47 @@ class TsExprResolver(
         state.throwExceptionWithoutStackFrameDrop(address, type)
     }
 
-    private fun resolveInstanceField(
-        instance: EtsLocal,
+    private fun handleFieldRef(
+        instance: EtsLocal?,
+        instanceRef: UHeapRef,
         field: EtsFieldSignature,
-    ): EtsField {
-        // Perfect signature:
-        if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) {
-            val clazz = ctx.scene.projectAndSdkClasses.single { it.name == field.enclosingClass.name }
-            val fields = clazz.fields.filter { it.name == field.name }
-            if (fields.size == 1) return fields.single()
-        }
+    ): UExpr<out USort>? = with(ctx) {
+        val etsField = resolveEtsField(instance, field)
+        val sort = typeToSort(etsField.type)
 
-        // Unknown signature:
-        val instanceType = instance.type
-        if (instanceType is EtsClassType) {
-            val classes = ctx.scene.projectAndSdkClasses.filter { it.name == instanceType.signature.name }
-            if (classes.size == 1) {
-                val clazz = classes.single()
-                return clazz.fields.single { it.name == field.name }
-            }
-            val fields = classes.flatMap { it.fields.filter { it.name == field.name } }
-            if (fields.size == 1) {
-                return fields.single()
-            }
-        } else if (instanceType is EtsUnclearRefType) {
-            val classes = ctx.scene.projectAndSdkClasses.filter { it.name == instanceType.name }
-            if (classes.size == 1) {
-                val clazz = classes.single()
-                return clazz.fields.single { it.name == field.name }
-            }
-            val fields = classes.flatMap { it.fields.filter { it.name == field.name } }
-            if (fields.size == 1) {
-                return fields.single()
+        val expr = if (sort == unresolvedSort) {
+            val boolLValue = mkFieldLValue(boolSort, instanceRef, field)
+            val fpLValue = mkFieldLValue(fp64Sort, instanceRef, field)
+            val refLValue = mkFieldLValue(addressSort, instanceRef, field)
+
+            scope.calcOnState {
+                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
+                val fakeRef = if (ref.isFakeObject()) {
+                    ref
+                } else {
+                    mkFakeValue(scope, bool, fp, ref)
+                }
+
+                memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
+
+                fakeRef
             }
         } else {
-            val fields = ctx.scene.projectAndSdkClasses.flatMap { it.fields.filter { it.name == field.name } }
-            if (fields.size == 1) {
-                return fields.single()
-            }
+            val lValue = mkFieldLValue(sort, instanceRef, field)
+            scope.calcOnState { memory.read(lValue) }
+        }
+
+        // TODO: check 'field.type' vs 'etsField.type'
+        if (assertIsSubtype(expr, field.type)) {
+            expr
+        } else {
+            null
         }
-        error("Cannot resolve field $field")
     }
 
     override fun visit(value: EtsInstanceFieldRef): UExpr<out USort>? = with(ctx) {
@@ -683,46 +686,40 @@ class TsExprResolver(
             }
         }
 
-        val field = resolveInstanceField(value.instance, value.field)
-        val sort = typeToSort(field.type)
+        return handleFieldRef(value.instance, instanceRef, value.field)
+    }
 
-        val expr = if (sort == unresolvedSort) {
-            val boolLValue = mkFieldLValue(boolSort, instanceRef, value.field)
-            val fpLValue = mkFieldLValue(fp64Sort, instanceRef, value.field)
-            val refLValue = mkFieldLValue(addressSort, instanceRef, value.field)
+    override fun visit(value: EtsStaticFieldRef): UExpr<out USort>? = with(ctx) {
+        val clazz = scene.projectAndSdkClasses.singleOrNull {
+            it.signature == value.field.enclosingClass
+        } ?: return null
 
-            scope.calcOnState {
-                val bool = memory.read(boolLValue)
-                val fp = memory.read(fpLValue)
-                val ref = memory.read(refLValue)
+        val instanceRef = scope.calcOnState { getStaticInstance(clazz) }
 
-                // If a fake object is already created and assigned to the field,
-                // there is no need to recreate another one
-                val fakeRef = if (ref.isFakeObject()) {
-                    ref
-                } else {
-                    mkFakeValue(scope, bool, fp, ref)
+        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
+                    if (result is TsMethodResult.Success && result.method == initializer) {
+                        methodResult = TsMethodResult.NoCall
+                    }
                 }
-
-                memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
-
-                fakeRef
+            } else {
+                scope.doWithState {
+                    markInitialized(clazz)
+                    pushSortsForArguments(instance = null, args = emptyList(), localToIdx)
+                    callStack.push(initializer, currentStatement)
+                    memory.stack.push(arrayOf(instanceRef), initializer.localsCount)
+                    newStmt(initializer.cfg.stmts.first())
+                }
+                return null
             }
-        } else {
-            val lValue = mkFieldLValue(sort, instanceRef, value.field)
-            scope.calcOnState { memory.read(lValue) }
         }
 
-        if (assertIsSubtype(expr, value.type)) {
-            expr
-        } else {
-            null
-        }
-    }
-
-    override fun visit(value: EtsStaticFieldRef): UExpr<out USort>? {
-        logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
-        error("Not supported $value")
+        return handleFieldRef(instance = null, instanceRef, value.field)
     }
 
     // endregion

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

@@ -13,13 +13,15 @@ import org.jacodb.ets.base.EtsNopStmt
 import org.jacodb.ets.base.EtsNullType
 import org.jacodb.ets.base.EtsParameterRef
 import org.jacodb.ets.base.EtsReturnStmt
+import org.jacodb.ets.base.EtsStaticFieldRef
 import org.jacodb.ets.base.EtsStmt
 import org.jacodb.ets.base.EtsSwitchStmt
 import org.jacodb.ets.base.EtsThis
 import org.jacodb.ets.base.EtsThrowStmt
 import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.base.EtsValue
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.utils.getDeclaredLocals
 import org.usvm.StepResult
 import org.usvm.StepScope
 import org.usvm.UInterpreter
@@ -43,6 +45,7 @@ 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.utils.ensureSat
 
 typealias TsStepScope = StepScope<TsState, EtsType, EtsStmt, TsContext>
@@ -178,15 +181,38 @@ class TsInterpreter(
 
                 is EtsInstanceFieldRef -> {
                     val instance = exprResolver.resolve(lhv.instance)?.asExpr(addressSort) ?: return@doWithState
-
-                    val sort = typeToSort(lhv.type)
+                    val etsField = resolveEtsField(lhv.instance, lhv.field)
+                    val sort = typeToSort(etsField.type)
                     if (sort == unresolvedSort) {
                         val fakeObject = expr.toFakeObject(scope)
                         val lValue = mkFieldLValue(addressSort, instance, lhv.field)
                         memory.write(lValue, fakeObject, guard = trueExpr)
                     } else {
                         val lValue = mkFieldLValue(sort, instance, lhv.field)
-                        memory.write(lValue, expr.asExpr(sort), guard = trueExpr)
+                        memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
+                    }
+                }
+
+                is EtsStaticFieldRef -> {
+                    val clazz = scene.projectAndSdkClasses.singleOrNull {
+                        it.signature == lhv.field.enclosingClass
+                    } ?: return@doWithState
+
+                    val instance = scope.calcOnState { getStaticInstance(clazz) }
+
+                    // TODO: initialize the static field first
+                    //  Note: Since we are assigning to a static field, we can omit its initialization,
+                    //        if it does not have any side effects.
+
+                    val field = clazz.fields.single { it.name == lhv.field.name }
+                    val sort = typeToSort(field.type)
+                    if (sort == unresolvedSort) {
+                        val lValue = mkFieldLValue(addressSort, instance, field.signature)
+                        val fakeObject = expr.toFakeObject(scope)
+                        memory.write(lValue, fakeObject, guard = trueExpr)
+                    } else {
+                        val lValue = mkFieldLValue(sort, instance, field.signature)
+                        memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
                     }
                 }
 
@@ -229,17 +255,21 @@ class TsInterpreter(
         TsExprResolver(ctx, scope, ::mapLocalToIdx)
 
     // (method, localName) -> idx
-    private val localVarToIdx: MutableMap<EtsMethod, MutableMap<String, Int>> = hashMapOf()
+    private val localVarToIdx: MutableMap<EtsMethod, Map<String, Int>> = hashMapOf()
 
     private fun mapLocalToIdx(method: EtsMethod, local: EtsValue): Int =
         // Note: below, 'n' means the number of arguments
         when (local) {
             // Note: locals have indices starting from (n+1)
-            is EtsLocal -> localVarToIdx
-                .getOrPut(method) { hashMapOf() }
-                .let {
-                    it.getOrPut(local.name) { method.parametersWithThisCount + it.size }
+            is EtsLocal -> {
+                val map = localVarToIdx.getOrPut(method) {
+                    method.getDeclaredLocals().mapIndexed { idx, local ->
+                        val localIdx = idx + method.parametersWithThisCount
+                        local.name to localIdx
+                    }.toMap()
                 }
+                map[local.name] ?: error("Local not declared: $local")
+            }
 
             // Note: 'this' has index 'n'
             is EtsThis -> method.parameters.size

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsStatic.kt

@@ -0,0 +1,39 @@
+package org.usvm.machine.interpreter
+
+import org.jacodb.ets.base.EtsBooleanType
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsFieldSignature
+import org.jacodb.ets.model.EtsFieldSubSignature
+import org.usvm.UBoolSort
+import org.usvm.UHeapRef
+import org.usvm.collection.field.UFieldLValue
+import org.usvm.isTrue
+import org.usvm.machine.state.TsState
+import org.usvm.util.mkFieldLValue
+
+internal fun TsState.isInitialized(clazz: EtsClass): Boolean {
+    val instance = staticStorage[clazz] ?: error("Static instance for $clazz is not allocated")
+    val initializedFlag = mkStaticFieldsInitializedFlag(instance, clazz.signature)
+    return memory.read(initializedFlag).isTrue
+}
+
+internal fun TsState.markInitialized(clazz: EtsClass) {
+    val instance = staticStorage[clazz] ?: error("Static instance for $clazz is not allocated")
+    val initializedFlag = mkStaticFieldsInitializedFlag(instance, clazz.signature)
+    memory.write(initializedFlag, ctx.trueExpr, guard = ctx.trueExpr)
+}
+
+private fun mkStaticFieldsInitializedFlag(
+    instance: UHeapRef,
+    clazz: EtsClassSignature,
+): UFieldLValue<String, UBoolSort> {
+    val field = EtsFieldSignature(
+        enclosingClass = clazz,
+        sub = EtsFieldSubSignature(
+            name = "__initialized__",
+            type = EtsBooleanType,
+        ),
+    )
+    return mkFieldLValue(instance.ctx.boolSort, instance, field)
+}