diff --git a/build.xml b/build.xml
index 9be556d6..761898dd 100644
--- a/build.xml
+++ b/build.xml
@@ -161,6 +161,9 @@
includes="*,gov/nasa/jpf/**,classloader_specific_tests/**">
+
+
+
diff --git a/src/classes/modules/java.base/jdk/internal/misc/Unsafe.java b/src/classes/modules/java.base/jdk/internal/misc/Unsafe.java
index 90fac10f..6cf88ed5 100644
--- a/src/classes/modules/java.base/jdk/internal/misc/Unsafe.java
+++ b/src/classes/modules/java.base/jdk/internal/misc/Unsafe.java
@@ -41,6 +41,11 @@ public static Unsafe getUnsafe() {
// a numeric id for the corresponding FieldInfo here
public native int fieldOffset (Field f);
public native long objectFieldOffset (Field f);
+ public native long objectFieldOffset(Class c, String name);
+
+ public final native boolean compareAndSetInt(Object o, long offset, int expected, int x);
+ public final native boolean compareAndSetLong(Object o, long offset, long expected, long x);
+ public final native boolean compareAndSetObject(Object o, long offset, Object expected, Object x);
// those do the usual CAS magic
public native boolean compareAndSwapObject (Object oThis, long offset, Object expect, Object update);
@@ -73,6 +78,10 @@ public void putInt(Object obj, int offset, int i) {
public native Object getObject(Object obj, long l);
public native Object getObjectVolatile(Object obj, long l);
+ public final Object getObjectAcquire(Object o, long offset) {
+ return getObjectVolatile(o, offset);
+ }
+
@Deprecated
public Object getObject(Object obj, int offset) {
return getObject(obj, (long) offset);
@@ -208,8 +217,11 @@ public void putDouble(Object obj, int offset, double d) {
public native int arrayBaseOffset(Class clazz);
public native int arrayIndexScale(Class clazz);
-
-
+
+ public final void putObjectRelease(Object o, long offset, Object x) {
+ putObjectVolatile(o, offset, x);
+ }
+
//--- java.nio finally breaks object boundaries - hello, evil pointer arithmetic
/**
diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java
index 90a5dcfe..40132bce 100644
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_Class.java
@@ -490,7 +490,7 @@ public int getConstructor___3Ljava_lang_Class_2__Ljava_lang_reflect_Constructor_
}
// this is only used for system classes such as java.lang.reflect.Method
- ClassInfo getInitializedClassInfo (MJIEnv env, String clsName){
+ static ClassInfo getInitializedClassInfo (MJIEnv env, String clsName){
ThreadInfo ti = env.getThreadInfo();
Instruction insn = ti.getPC();
ClassInfo ci = ClassLoaderInfo.getSystemResolvedClassInfo( clsName);
diff --git a/src/peers/gov/nasa/jpf/vm/JPF_sun_misc_Unsafe.java b/src/peers/gov/nasa/jpf/vm/JPF_jdk_internal_misc_Unsafe.java
similarity index 91%
rename from src/peers/gov/nasa/jpf/vm/JPF_sun_misc_Unsafe.java
rename to src/peers/gov/nasa/jpf/vm/JPF_jdk_internal_misc_Unsafe.java
index bccad5ce..ab65914e 100644
--- a/src/peers/gov/nasa/jpf/vm/JPF_sun_misc_Unsafe.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_jdk_internal_misc_Unsafe.java
@@ -27,6 +27,7 @@
import gov.nasa.jpf.vm.SystemState;
import gov.nasa.jpf.vm.ThreadInfo;
+import static gov.nasa.jpf.vm.JPF_java_lang_Class.FIELD_CLASSNAME;
/**
* we don't want this class! This is a hodgepodge of stuff that shouldn't be in Java, but
@@ -39,11 +40,11 @@
*
* <2do> this might change with better modeling of high level java.util.concurrent constructs
*/
-public class JPF_sun_misc_Unsafe extends NativePeer {
+public class JPF_jdk_internal_misc_Unsafe extends NativePeer {
@MJI
public int getUnsafe____Lsun_misc_Unsafe_2 (MJIEnv env, int clsRef) {
- int objRef = env.getStaticReferenceField("sun.misc.Unsafe", "theUnsafe");
+ int objRef = env.getStaticReferenceField("jdk.internal.misc.Unsafe", "theUnsafe");
return objRef;
}
@@ -52,6 +53,48 @@ public long objectFieldOffset__Ljava_lang_reflect_Field_2__J (MJIEnv env, int un
return fieldOffset__Ljava_lang_reflect_Field_2__I(env, unsafeRef, fieldRef);
}
+ /**
+ * NativePeer method for {@link jdk.internal.misc.Unsafe#objectFieldOffset(java.lang.Class, java.lang.String)}
+ */
+ @MJI
+ public long objectFieldOffset__Ljava_lang_Class_2Ljava_lang_String_2__J (MJIEnv env, int unsafeRef, int clsRef, int nameRef) {
+ ClassInfo ci = env.getReferredClassInfo(clsRef);
+ String fname = env.getStringObject(nameRef);
+ FieldInfo fi = null;
+
+ fi = ci.getInstanceField(fname);
+ if (fi == null) {
+ fi = ci.getStaticField(fname);
+ }
+
+ if (fi == null) {
+ env.throwException("java.lang.NoSuchFieldException", fname);
+ return MJIEnv.NULL;
+
+ } else {
+ ClassInfo fci = JPF_java_lang_Class.getInitializedClassInfo(env, FIELD_CLASSNAME);
+ if (fci == null) {
+ env.repeatInvocation();
+ return MJIEnv.NULL;
+ }
+ int fieldRef = JPF_java_lang_Class.createFieldObject(env, fi, fci);
+ return env.getIntField(fieldRef, "regIdx");
+ }
+ }
+
+ /**
+ * NativePeer method for {@link jdk.internal.misc.Unsafe#compareAndSetObject(java.lang.Object, long, java.lang.Object, java.lang.Object)}
+ */
+ @MJI
+ public boolean compareAndSetObject__Ljava_lang_Object_2JLjava_lang_Object_2Ljava_lang_Object_2__Z(MJIEnv env, int unsafeRef, int oRef, long offset, int expectedRef, int xRef) {
+ int actual = getObject__Ljava_lang_Object_2J__Ljava_lang_Object_2(env, unsafeRef, oRef, offset);
+ if (actual == expectedRef) {
+ putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(env, unsafeRef, oRef, offset, xRef);
+ return true;
+ }
+ return false;
+ }
+
/**
* we don't really return an offset here, since that would be useless. What we really want is
* to identify the corresponding FieldInfo, and that's much easier done with the Field
@@ -64,6 +107,34 @@ public int fieldOffset__Ljava_lang_reflect_Field_2__I (MJIEnv env, int unsafeRef
return env.getIntField(fieldRef, "regIdx");
}
+ /**
+ * NativePeer method for {@link jdk.internal.misc.Unsafe#compareAndSetInt(java.lang.Object, long, int, int)}
+ */
+ @MJI
+ public boolean compareAndSetInt__Ljava_lang_Object_2JII__Z (MJIEnv env, int unsafeRef,
+ int oRef, long offset, int expected, int x) {
+ int actual = getInt__Ljava_lang_Object_2J__I(env, unsafeRef, oRef, offset);
+ if (actual == expected) {
+ putInt__Ljava_lang_Object_2JI__V(env, unsafeRef, oRef, offset, x);
+ return true;
+ }
+ return false;
+ }
+
+ /**
+ * NativePeer method for {@link jdk.internal.misc.Unsafe#compareAndSetLong(Object, long, long, long)}
+ */
+ @MJI
+ public boolean compareAndSetLong__Ljava_lang_Object_2JJJ__Z (MJIEnv env, int unsafeRef,
+ int oRef, long offset, long expected, long x) {
+ long actual = getLong__Ljava_lang_Object_2J__J(env, unsafeRef, oRef, offset);
+ if (actual == expected) {
+ putLong__Ljava_lang_Object_2JJ__V(env, unsafeRef, oRef, offset, x);
+ return true;
+ }
+ return false;
+ }
+
@MJI
public boolean compareAndSwapObject__Ljava_lang_Object_2JLjava_lang_Object_2Ljava_lang_Object_2__Z (MJIEnv env, int unsafeRef,
int objRef, long fieldOffset,
diff --git a/src/tests/gov/nasa/jpf/test/java/misc/UnsafeTest.java b/src/tests/gov/nasa/jpf/test/java/misc/UnsafeTest.java
new file mode 100644
index 00000000..ee052b80
--- /dev/null
+++ b/src/tests/gov/nasa/jpf/test/java/misc/UnsafeTest.java
@@ -0,0 +1,68 @@
+package gov.nasa.jpf.test.java.misc;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import jdk.internal.misc.Unsafe;
+import org.junit.Test;
+
+public class UnsafeTest extends TestJPF {
+
+ private class TestClass {
+ int intVar = 0;
+ }
+
+ private final Unsafe unsafe = Unsafe.getUnsafe();
+
+ /**
+ * Test NativePeer method for {@link Unsafe#objectFieldOffset(java.lang.Class, java.lang.String)}
+ */
+ @Test
+ public void objectFieldOffset() {
+ if (verifyNoPropertyViolation()) {
+ unsafe.objectFieldOffset(TestClass.class, "intVar");
+ }
+ }
+
+ /**
+ * Test NativePeer method for {@link Unsafe#getInt(Object, long)}
+ */
+ @Test
+ public void getInt() {
+ if (verifyNoPropertyViolation()) {
+ TestClass o = new TestClass();
+ long intFieldOffset = unsafe.objectFieldOffset(TestClass.class, "intVar");
+
+ assert unsafe.getInt(o, intFieldOffset) == 0;
+ }
+ }
+
+ /**
+ * Test NativePeer method for {@link Unsafe#putInt(Object, long, int)}
+ */
+ @Test
+ public void putInt() {
+ if (verifyNoPropertyViolation()) {
+ TestClass o = new TestClass();
+ long intFieldOffset = unsafe.objectFieldOffset(TestClass.class, "intVar");
+ int x = 77;
+
+ unsafe.putInt(o, intFieldOffset, x);
+ assert o.intVar == x;
+ }
+ }
+
+ /**
+ * Test NativePeer method for {@link Unsafe#compareAndSetInt(Object, long, int, int)}
+ */
+ @Test
+ public void compareAndSetInt() {
+ if (verifyNoPropertyViolation()) {
+ TestClass o = new TestClass();
+ long intFieldOffset = unsafe.objectFieldOffset(TestClass.class, "intVar");
+ int expected = 0;
+ int x = 3;
+
+ unsafe.compareAndSetInt(o, intFieldOffset, expected, x);
+ assert o.intVar == 3;
+ }
+ }
+}
\ No newline at end of file