Impl statics via "instance" fields

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

@@ -84,6 +84,7 @@ import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.api.allocateArray
+import org.usvm.collections.immutable.getOrPut
 import org.usvm.isTrue
 import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.TsStaticFieldLValue
@@ -107,6 +108,7 @@ import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
 import org.usvm.util.throwExceptionWithoutStackFrameDrop
+import org.usvm.util.type
 
 private val logger = KotlinLogging.logger {}
 
@@ -734,8 +736,18 @@ class TsExprResolver(
         val clazz = scene.projectAndSdkClasses.singleOrNull {
             it.signature == value.field.enclosingClass
         } ?: return null
-        val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME }
 
+        val instance = scope.calcOnState {
+            val (updated, result) = staticStorage.getOrPut(clazz, ownership) {
+                val address = memory.allocConcrete(clazz.type)
+                // TODO: memory.types.allocate(...)
+                address
+            }
+            staticStorage = updated
+            result
+        }
+
+        val initializer = clazz.methods.singleOrNull { it.name == STATIC_INIT_METHOD_NAME }
         if (initializer != null) {
             val isInitialized = scope.calcOnState { isInitialized(clazz) }
             if (isInitialized) {
@@ -760,9 +772,9 @@ class TsExprResolver(
             }
         }
 
-        val field = resolveInstanceField(null, value.field)
+        val field = clazz.fields.single { it.name == value.field.name }
         val sort = typeToSort(field.type)
-        val lValue = TsStaticFieldLValue(value.field, sort)
+        val lValue = mkFieldLValue(sort, instance, field.signature)
         val expr = scope.calcOnState { memory.read(lValue) }
 
         if (assertIsSubtype(expr, value.type)) {

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

@@ -26,6 +26,7 @@ import org.usvm.StepResult
 import org.usvm.StepScope
 import org.usvm.UInterpreter
 import org.usvm.api.targets.TsTarget
+import org.usvm.collections.immutable.getOrPut
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.forkblacklists.UForkBlackList
 import org.usvm.machine.TsApplicationGraph
@@ -45,6 +46,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.type
 import org.usvm.utils.ensureSat
 
 typealias TsStepScope = StepScope<TsState, EtsType, EtsStmt, TsContext>
@@ -193,14 +195,32 @@ class TsInterpreter(
                 }
 
                 is EtsStaticFieldRef -> {
-                    val field = exprResolver.resolveInstanceField(null, lhv.field)
+                    val clazz = scene.projectAndSdkClasses.singleOrNull {
+                        it.signature == lhv.field.enclosingClass
+                    } ?: return@doWithState
+
+        val instance = scope.calcOnState {
+            val (updated, result) = staticStorage.getOrPut(clazz, ownership) {
+                val address = memory.allocConcrete(clazz.type)
+                // TODO: memory.types.allocate(...)
+                address
+            }
+            staticStorage = updated
+            result
+        }
+
+                    // 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)
-                        val lValue = TsStaticFieldLValue(field.signature, addressSort)
                         memory.write(lValue, fakeObject, guard = trueExpr)
                     } else {
-                        val lValue = TsStaticFieldLValue(field.signature, sort)
+                        val lValue = mkFieldLValue(sort, instance, field.signature)
                         memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
                     }
                 }

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

@@ -8,7 +8,9 @@ import org.jacodb.ets.model.EtsFieldSubSignature
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collection.field.UFieldLValue
 import org.usvm.collections.immutable.getOrDefault
 import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
 import org.usvm.collections.immutable.internal.MutabilityOwnership
@@ -68,26 +70,27 @@ internal class TsStaticFieldsMemoryRegion<Sort : USort>(
 }
 
 internal fun TsState.isInitialized(clazz: EtsClass): Boolean {
-    val initializedFlag = ctx.staticFieldsInitializedFlag(clazz)
+    val instance = staticStorage[clazz]!!
+    val initializedFlag = ctx.staticFieldsInitializedFlag(instance, clazz.signature)
     return memory.read(initializedFlag).isTrue
 }
 
 internal fun TsState.markInitialized(clazz: EtsClass) {
-    val initializedFlag = ctx.staticFieldsInitializedFlag(clazz)
+    val instance = staticStorage[clazz]!!
+    val initializedFlag = ctx.staticFieldsInitializedFlag(instance, clazz.signature)
     memory.write(initializedFlag, ctx.trueExpr, guard = ctx.trueExpr)
 }
 
-private fun TsContext.staticFieldsInitializedFlag(clazz: EtsClass): TsStaticFieldLValue<UBoolSort> {
+private fun TsContext.staticFieldsInitializedFlag(
+    instance: UHeapRef,
+    clazz: EtsClassSignature,
+): UFieldLValue<EtsFieldSignature, UBoolSort> {
     val field = EtsFieldSignature(
-        enclosingClass = clazz.signature,
-        sub = staticFieldsInitializedFlagField,
-    )
-    return TsStaticFieldLValue(field, boolSort)
-}
-
-private val staticFieldsInitializedFlagField: EtsFieldSubSignature by lazy {
-    EtsFieldSubSignature(
-        name = "__initialized__",
-        type = EtsBooleanType,
+        enclosingClass = clazz,
+        sub = EtsFieldSubSignature(
+            name = "__initialized__",
+            type = EtsBooleanType,
+        ),
     )
+    return UFieldLValue(boolSort, instance, field)
 }

usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt

@@ -4,9 +4,12 @@ import org.jacodb.ets.base.EtsLocal
 import org.jacodb.ets.base.EtsStmt
 import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.base.EtsValue
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsMethod
 import org.usvm.PathNode
 import org.usvm.UCallStack
+import org.usvm.UConcreteHeapRef
 import org.usvm.USort
 import org.usvm.UState
 import org.usvm.api.targets.TsTarget
@@ -33,16 +36,17 @@ class TsState(
     var methodResult: TsMethodResult = TsMethodResult.NoCall,
     targets: UTargetsSet<TsTarget, EtsStmt> = UTargetsSet.empty(),
     private var localToSortStack: MutableList<UPersistentHashMap<Int, USort>> = mutableListOf(persistentHashMapOf()),
+    var staticStorage: UPersistentHashMap<EtsClass, UConcreteHeapRef> = persistentHashMapOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
-    ctx,
-    ownership,
-    callStack,
-    pathConstraints,
-    memory,
-    models,
-    pathNode,
-    forkPoints,
-    targets
+    ctx = ctx,
+    initOwnership = ownership,
+    callStack = callStack,
+    pathConstraints = pathConstraints,
+    memory = memory,
+    models = models,
+    pathNode = pathNode,
+    forkPoints = forkPoints,
+    targets = targets,
 ) {
     fun getOrPutSortForLocal(localIdx: Int, localType: EtsType): USort {
         val localToSort = localToSortStack.last()
@@ -91,18 +95,19 @@ class TsState(
         this.ownership = newThisOwnership
 
         return TsState(
-            ctx,
-            cloneOwnership,
-            entrypoint,
-            callStack.clone(),
-            clonedConstraints,
-            memory.clone(clonedConstraints.typeConstraints, newThisOwnership, cloneOwnership),
-            models,
-            pathNode,
-            forkPoints,
-            methodResult,
-            targets.clone(),
-            localToSortStack.toMutableList(),
+            ctx = ctx,
+            ownership = cloneOwnership,
+            entrypoint = entrypoint,
+            callStack = callStack.clone(),
+            pathConstraints = clonedConstraints,
+            memory = memory.clone(clonedConstraints.typeConstraints, newThisOwnership, cloneOwnership),
+            models = models,
+            pathNode = pathNode,
+            forkPoints = forkPoints,
+            methodResult = methodResult,
+            targets = targets.clone(),
+            localToSortStack = localToSortStack.toMutableList(),
+            staticStorage = staticStorage,
         )
     }
 

usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt

@@ -1,7 +1,9 @@
 package org.usvm.util
 
 import io.ksmt.sort.KFp64Sort
+import org.jacodb.ets.base.EtsClassType
 import org.jacodb.ets.base.EtsType
+import org.jacodb.ets.model.EtsClass
 import org.usvm.UBoolSort
 import org.usvm.UExpr
 import org.usvm.UHeapRef
@@ -16,3 +18,6 @@ fun TsContext.boolToFp(expr: UExpr<UBoolSort>): UExpr<KFp64Sort> =
 fun TsState.throwExceptionWithoutStackFrameDrop(address: UHeapRef, type: EtsType) {
     methodResult = TsMethodResult.TsException(address, type)
 }
+
+val EtsClass.type: EtsType
+    get() = EtsClassType(signature, typeParameters)