Implement missing, and/or unlinked native methods in Unsafe

build.xml

@@ -161,6 +161,9 @@
            includes="*,gov/nasa/jpf/**,classloader_specific_tests/**">
       <compilerarg value="-Xlint:all,-serial,-rawtypes,-unchecked"/>
 
+      <compilerarg value="--add-exports"/>
+      <compilerarg value="java.base/jdk.internal.misc=ALL-UNNAMED"/>
+
       <include name="*gov/nasa/jpf/**"/>
       <include name="classloader_specific_tests/**"/>
       <include name="java8/**" if="have_java8"/>

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
 
   /**

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);

src/peers/gov/nasa/jpf/vm/JPF_sun_misc_Unsafe.java → 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,

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;
+        }
+    }
+}