Add an approximation for VM

UnitTestBot · Feb 19, 2024 · 4f7ee87 · 4f7ee87
1 parent c321cfb
commit 4f7ee87
Show file tree

Hide file tree

Showing 3 changed files with 52 additions and 3 deletions.
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt
@@ -98,7 +98,10 @@ internal class JcStaticFieldsMemoryRegion<Sort : USort>(
 
     companion object {
         val fieldShouldBeSymbolic: (JcField) -> Boolean = { field ->
-            field.type.isPrimitive && !field.isFinal && field.name != staticFieldsInitializedFlagField.name
+            field.type.isPrimitive
+                    && !field.isFinal
+                    && field.name != staticFieldsInitializedFlagField.name
+                    && !field.enclosingClass.declaration.location.isRuntime
         }
     }
 }

diff --git a/...m/src/sample-approximations/java/org/usvm/samples/approximations/TestVMApproximation.java b/...m/src/sample-approximations/java/org/usvm/samples/approximations/TestVMApproximation.java
@@ -0,0 +1,46 @@
+package org.usvm.samples.approximations;
+
+import org.jacodb.approximation.annotation.Approximate;
+
+import java.util.Map;
+
+@SuppressWarnings("ALL")
+@Approximate(jdk.internal.misc.VM.class)
+public class TestVMApproximation {
+
+    // the init level when the VM is fully initialized
+    private static final int JAVA_LANG_SYSTEM_INITED = 1;
+    private static final int MODULE_SYSTEM_INITED = 2;
+    private static final int SYSTEM_LOADER_INITIALIZING = 3;
+    private static final int SYSTEM_BOOTED = 4;
+    private static final int SYSTEM_SHUTDOWN = 5;
+
+
+    // 0, 1, 2, ...
+    private static volatile int initLevel = 0;
+    private static final Object lock = new Object();
+
+    private static long directMemory = 64 * 1024 * 1024;
+
+    // buffers, allocated by ByteBuffer.allocateDirect, to be page aligned.
+    private static boolean pageAlignDirectMemory;
+
+    private static Map<String, String> savedProps;
+
+    /* Current count of objects pending for finalization */
+    private static volatile int finalRefCount;
+
+    /* Peak count of objects pending for finalization */
+    private static volatile int peakFinalRefCount;
+
+    /* The threadStatus field is set by the VM at state transition
+     * in the hotspot implementation. Its value is set according to
+     * the JVM TI specification GetThreadState function.
+     */
+    private static final int JVMTI_THREAD_STATE_ALIVE = 0x0001;
+    private static final int JVMTI_THREAD_STATE_TERMINATED = 0x0002;
+    private static final int JVMTI_THREAD_STATE_RUNNABLE = 0x0004;
+    private static final int JVMTI_THREAD_STATE_BLOCKED_ON_MONITOR_ENTER = 0x0400;
+    private static final int JVMTI_THREAD_STATE_WAITING_INDEFINITELY = 0x0010;
+    private static final int JVMTI_THREAD_STATE_WAITING_WITH_TIMEOUT = 0x0020;
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt
@@ -6,7 +6,7 @@ import org.junit.jupiter.api.Test
 import org.usvm.CoverageZone
 import org.usvm.PathSelectionStrategy
 import org.usvm.UMachineOptions
-import org.usvm.samples.JavaMethodTestRunner
+import org.usvm.samples.approximations.ApproximationsTestRunner
 import org.usvm.test.util.checkers.between
 import org.usvm.test.util.checkers.eq
 import org.usvm.test.util.checkers.ge
@@ -16,7 +16,7 @@ import org.usvm.util.UsvmTest
 import org.usvm.util.isException
 import kotlin.math.pow
 
-internal class RecursionTest : JavaMethodTestRunner() {
+internal class RecursionTest : ApproximationsTestRunner() {
     @UsvmTest([Options([PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM])])
     fun testFactorial(options: UMachineOptions) {
         withOptions(options) {