Initial support for static fields in JcInterpreter (#30)

.github/workflows/build-and-run-tests.yml

@@ -45,4 +45,11 @@ jobs:
 
       # Runs a set of commands using the runners shell
       - name: Build and run tests
-        run: ./gradlew build --no-daemon
+        run: ./gradlew build --no-daemon
+
+      - name: Upload usvm test reports
+        uses: actions/upload-artifact@v3
+        if: always()
+        with:
+          name: usvm-tests-report-${{ matrix.os }}
+          path: ./**/build/reports/tests/test/

usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt

@@ -10,6 +10,7 @@ import org.jacodb.api.JcRefType
 import org.jacodb.api.JcType
 import org.jacodb.api.JcTypedField
 import org.jacodb.api.JcTypedMethod
+import org.jacodb.api.PredefinedPrimitives
 import org.jacodb.api.cfg.JcAddExpr
 import org.jacodb.api.cfg.JcAndExpr
 import org.jacodb.api.cfg.JcArgument
@@ -75,7 +76,10 @@ import org.jacodb.api.ext.ifArrayGetElementType
 import org.jacodb.api.ext.int
 import org.jacodb.api.ext.isAssignable
 import org.jacodb.api.ext.long
+import org.jacodb.api.ext.objectType
 import org.jacodb.api.ext.short
+import org.jacodb.impl.bytecode.JcFieldImpl
+import org.jacodb.impl.types.FieldInfo
 import org.usvm.UArrayIndexLValue
 import org.usvm.UArrayLengthLValue
 import org.usvm.UBvSort
@@ -87,12 +91,14 @@ import org.usvm.URegisterLValue
 import org.usvm.USizeExpr
 import org.usvm.USizeSort
 import org.usvm.USort
+import org.usvm.isTrue
 import org.usvm.machine.operator.JcBinaryOperator
 import org.usvm.machine.operator.JcUnaryOperator
 import org.usvm.machine.operator.ensureBvExpr
 import org.usvm.machine.operator.mkNarrow
 import org.usvm.machine.operator.wideTo32BitsIfNeeded
 import org.usvm.machine.state.JcMethodResult
+import org.usvm.machine.state.JcState
 import org.usvm.machine.state.addNewMethodCall
 import org.usvm.machine.state.lastStmt
 import org.usvm.machine.state.throwException
@@ -106,6 +112,7 @@ class JcExprResolver(
     private val scope: JcStepScope,
     private val applicationGraph: JcApplicationGraph,
     private val localToIdx: (JcMethod, JcLocal) -> Int,
+    private val mkClassRef: (JcRefType, JcState) -> UHeapRef,
     private val hardMaxArrayLength: Int = 1_500, // TODO: move to options
 ) : JcExprVisitor<UExpr<out USort>?> {
     /**
@@ -367,10 +374,20 @@ class JcExprResolver(
     private fun resolveInvoke(
         method: JcTypedMethod,
         resolveArguments: () -> List<UExpr<out USort>>?,
+    ): UExpr<out USort>? = ensureStaticFieldsInitialized(method.enclosingType) {
+        resolveInvokeNoStaticInitializationCheck(method, resolveArguments)
+    }
+
+    private fun resolveInvokeNoStaticInitializationCheck(
+        method: JcTypedMethod,
+        resolveArguments: () -> List<UExpr<out USort>>?,
     ): UExpr<out USort>? {
         val result = scope.calcOnState { methodResult } ?: return null
         return when (result) {
             is JcMethodResult.Success -> {
+                check(result.method == method.method) {
+                    "Expected result from ${method.method} but actual is ${result.method}"
+                }
                 scope.doWithState { methodResult = JcMethodResult.NoCall }
                 result.value
             }
@@ -423,19 +440,77 @@ class JcExprResolver(
 
     // region lvalue resolving
 
-    private fun resolveFieldRef(instance: JcValue?, field: JcTypedField): ULValue? = with(ctx) {
-        if (instance != null) {
-            val instanceRef = resolveJcExpr(instance)?.asExpr(addressSort) ?: return null
-            checkNullPointer(instanceRef) ?: return null
-            val sort = ctx.typeToSort(field.fieldType)
-            UFieldLValue(sort, instanceRef, field.field)
-        } else {
-            val sort = ctx.typeToSort(field.fieldType)
-            JcStaticFieldRef(sort, field.field)
-            // TODO: can't extend UMemoryBase for now...
+    private fun resolveFieldRef(instance: JcValue?, field: JcTypedField): ULValue? =
+        ensureStaticFieldsInitialized(field.enclosingType) {
+            with(ctx) {
+                if (instance != null) {
+                    val instanceRef = resolveJcExpr(instance)?.asExpr(addressSort) ?: return null
+                    checkNullPointer(instanceRef) ?: return null
+                    val sort = ctx.typeToSort(field.fieldType)
+                    UFieldLValue(sort, instanceRef, field.field)
+                } else {
+                    val sort = ctx.typeToSort(field.fieldType)
+                    val classRef = scope.calcOnState {
+                        mkClassRef(field.enclosingType, this)
+                    } ?: return null
+                    UFieldLValue(sort, classRef, field.field)
+                }
+            }
+        }
+
+    /**
+     * Run a class static initializer for [type] if it didn't run before the current state.
+     * The class static initialization state is tracked by the synthetic [staticFieldsInitializedFlagField] field.
+     * */
+    private inline fun <T> ensureStaticFieldsInitialized(type: JcRefType, body: () -> T): T? {
+        // java.lang.Object has no static fields, but has non-trivial initializer
+        if (type == ctx.cp.objectType) {
+            return body()
+        }
+
+        val initializer = type.jcClass.declaredMethods.firstOrNull { it.isClassInitializer }
+
+        // Class has no static initializer
+        if (initializer == null) {
+            return body()
+        }
+
+        val classRef = scope.calcOnState { mkClassRef(type, this) } ?: return null
+
+        val initializedFlag = staticFieldsInitializedFlag(type, classRef)
+
+        val staticFieldsInitialized = scope.calcOnState {
+            memory.read(initializedFlag).asExpr(ctx.booleanSort)
+        } ?: return null
+
+
+        if (staticFieldsInitialized.isTrue) {
+            scope.doWithState {
+                // Handle static initializer result
+                val result = methodResult
+                if (result is JcMethodResult.Success && result.method == initializer) {
+                    methodResult = JcMethodResult.NoCall
+                }
+            }
+
+            return body()
         }
+
+        // Run static initializer before the current statement
+        scope.doWithState {
+            memory.write(initializedFlag, ctx.trueExpr)
+            addNewMethodCall(applicationGraph, initializer, emptyList())
+        }
+        return null
     }
 
+    private fun staticFieldsInitializedFlag(type: JcRefType, classRef: UHeapRef) =
+        UFieldLValue(
+            fieldSort = ctx.booleanSort,
+            field = JcFieldImpl(type.jcClass, staticFieldsInitializedFlagField),
+            ref = classRef
+        )
+
     private fun resolveArrayAccess(array: JcValue, index: JcValue): ULValue? = with(ctx) {
         val arrayRef = resolveJcExpr(array)?.asExpr(addressSort) ?: return null
         checkNullPointer(arrayRef) ?: return null
@@ -661,4 +736,19 @@ class JcExprResolver(
         val result1 = resolveJcExpr(dependency1) ?: return null
         return block(result0, result1)
     }
+
+    companion object {
+        /**
+         * Synthetic field to track static field initialization state.
+         * */
+        private val staticFieldsInitializedFlagField by lazy {
+            FieldInfo(
+                name = "__initialized__",
+                signature = null,
+                access = 0,
+                type = PredefinedPrimitives.Boolean,
+                annotations = emptyList()
+            )
+        }
+    }
 }

usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt

@@ -21,6 +21,7 @@ import org.jacodb.api.cfg.JcThis
 import org.jacodb.api.cfg.JcThrowInst
 import org.usvm.StepResult
 import org.usvm.StepScope
+import org.usvm.UHeapRef
 import org.usvm.UInterpreter
 import org.usvm.URegisterLValue
 import org.usvm.machine.state.JcMethodResult
@@ -188,28 +189,20 @@ class JcInterpreter(
 
     private fun visitCallStmt(scope: JcStepScope, stmt: JcCallInst) {
         val exprResolver = exprResolverWithScope(scope)
+        exprResolver.resolveJcExpr(stmt.callExpr) ?: return
 
-        val result = requireNotNull(scope.calcOnState { methodResult })
-
-        when (result) {
-            JcMethodResult.NoCall -> {
-                exprResolver.resolveJcExpr(stmt.callExpr)
-            }
-
-            is JcMethodResult.Success -> {
-                val nextStmt = stmt.nextStmt
-                scope.doWithState {
-                    methodResult = JcMethodResult.NoCall
-                    newStmt(nextStmt)
-                } ?: return
-            }
-
-            is JcMethodResult.Exception -> error("Exception should be handled earlier")
+        scope.doWithState {
+            val nextStmt = stmt.nextStmt
+            newStmt(nextStmt)
         }
     }
 
     private fun exprResolverWithScope(scope: JcStepScope) =
-        JcExprResolver(ctx, scope, applicationGraph, ::mapLocalToIdxMapper)
+        JcExprResolver(
+            ctx, scope, applicationGraph,
+            ::mapLocalToIdxMapper,
+            ::classInstanceAllocator
+        )
 
     private val localVarToIdx = mutableMapOf<JcMethod, MutableMap<String, Int>>() // (method, localName) -> idx
 
@@ -228,4 +221,15 @@ class JcInterpreter(
         }
 
     private val JcInst.nextStmt get() = location.method.instList[location.index + 1]
+
+    private val classInstanceAllocatedRefs = mutableMapOf<String, UHeapRef>()
+
+    private fun classInstanceAllocator(type: JcRefType, state: JcState): UHeapRef {
+        // Don't use type.typeName here, because it contains generic parameters
+        val className = type.jcClass.name
+        return classInstanceAllocatedRefs.getOrPut(className) {
+            // Allocate globally unique ref
+            state.memory.heap.allocate()
+        }
+    }
 }

usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcMethodResult.kt

@@ -1,5 +1,6 @@
 package org.usvm.machine.state
 
+import org.jacodb.api.JcMethod
 import org.usvm.UExpr
 import org.usvm.USort
 
@@ -13,9 +14,10 @@ sealed interface JcMethodResult {
     object NoCall : JcMethodResult
 
     /**
-     * A method successfully returned a [value].
+     * A [method] successfully returned a [value].
      */
     class Success(
+        val method: JcMethod,
         val value: UExpr<out USort>
     ) : JcMethodResult
 

usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt

@@ -14,13 +14,14 @@ fun JcState.newStmt(stmt: JcInst) {
 }
 
 fun JcState.returnValue(valueToReturn: UExpr<out USort>) {
+    val returnFromMethod = callStack.lastMethod()
     // TODO: think about it later
     val returnSite = callStack.pop()
     if (callStack.isNotEmpty()) {
         memory.stack.pop()
     }
 
-    methodResult = JcMethodResult.Success(valueToReturn)
+    methodResult = JcMethodResult.Success(returnFromMethod, valueToReturn)
 
     if (returnSite != null) {
         newStmt(returnSite)
@@ -65,8 +66,16 @@ fun JcState.addNewMethodCall(
         return
     }
 
+    // TODO: move to appropriate place. Skip native method in static initializer
+    if (method.name == "registerNatives" && method.enclosingClass.name == "java.lang.Class") {
+        val nextStmt = applicationGraph.successors(lastStmt).single()
+        newStmt(nextStmt)
+        return
+    }
+
     // TODO: find concrete implementation (I guess, the method should be already concrete)
-    val entryPoint = applicationGraph.entryPoints(method).single()
+    val entryPoint = applicationGraph.entryPoints(method).singleOrNull()
+        ?: error("No entrypoint found for method: $method")
     val returnSite = lastStmt
     callStack.push(method, returnSite)
     memory.stack.push(arguments.toTypedArray(), method.localsCount)

usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithStatics.java

@@ -0,0 +1,44 @@
+package org.usvm.samples.objects;
+
+public class ObjectWithStatics {
+    static Object refStaticField;
+
+    static int primitiveStaticField;
+
+    static {
+        refStaticField = new Object();
+        primitiveStaticField = 17;
+    }
+
+    private Object getRefFiled() {
+        return refStaticField;
+    }
+
+    private int getPrimitiveFiled() {
+        return primitiveStaticField;
+    }
+
+    int staticsAreEqual() {
+        if (ObjectWithStatics.refStaticField != getRefFiled()) {
+            return 1;
+        }
+        if (ObjectWithStatics.primitiveStaticField != getPrimitiveFiled()) {
+            return 2;
+        }
+        return 0;
+    }
+
+    int mutateStatics() {
+        int initial = getPrimitiveFiled();
+        primitiveStaticField++;
+        int mutated = getPrimitiveFiled();
+        return mutated - initial;
+    }
+
+    int staticsInitialized() {
+        if (ObjectWithStatics.primitiveStaticField != 17) {
+            return 1;
+        }
+        return 0;
+    }
+}

usvm-jvm/src/test/kotlin/org/usvm/samples/algorithms/CorrectBracketSequencesTest.kt

@@ -40,7 +40,7 @@ internal class CorrectBracketSequencesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Unexpected lvalue org.usvm.machine.JcStaticFieldRef@527d1fe1")
+    @Disabled("No entrypoint found for method")
     fun testIsCbs() {
         val method = CorrectBracketSequences::isCbs
         checkDiscoveredPropertiesWithExceptions(

usvm-jvm/src/test/kotlin/org/usvm/samples/algorithms/SortTest.kt

@@ -9,7 +9,7 @@ import org.usvm.util.isException
 
 internal class SortTest : JavaMethodTestRunner() {
     @Test
-    @Disabled("Unexpected lvalue org.usvm.machine.JcStaticFieldRef@3a182eaf")
+    @Disabled("No entrypoint found for method")
     fun testQuickSort() {
         checkDiscoveredProperties(
             Sort::quickSort,
@@ -31,7 +31,7 @@ internal class SortTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Sequence is empty.")
+    @Disabled("No entrypoint found for method")
     fun testArrayCopy() {
         checkDiscoveredProperties(
             Sort::arrayCopy,
@@ -41,7 +41,7 @@ internal class SortTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Sequence is empty.")
+    @Disabled("No entrypoint found for method")
     fun testMergeSort() {
         checkDiscoveredProperties(
             Sort::mergeSort,