Add and implement put related reference methods

javapathfinder · Apr 24, 2024 · be07378 · be07378
1 parent 595cb07
commit be07378
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 12 deletions.
diff --git a/src/classes/modules/java.base/jdk/internal/misc/Unsafe.java b/src/classes/modules/java.base/jdk/internal/misc/Unsafe.java
@@ -194,8 +194,33 @@ public Object getObject(Object obj, int offset) {
     return getObject(obj, (long) offset);
   }
 
-  public native void putObject(Object obj, long l, Object obj1);
-  public native void putObjectVolatile(Object obj, long l, Object obj1);
+  public final void putObject(Object o, long offset, Object x) {
+    putReference(o, offset, x);
+  }
+
+  public final void putObjectOpaque(Object o, long offset, Object x) {
+    putReferenceOpaque(o, offset, x);
+  }
+
+  public final void putObjectRelease(Object o, long offset, Object x) {
+    putReferenceRelease(o, offset, x);
+  }
+  public final void putObjectVolatile(Object o, long offset, Object x) {
+    putReferenceVolatile(o, offset, x);
+  }
+
+  public native void putReference(Object o, long offset, Object x);
+
+
+  public final void putReferenceOpaque(Object o, long offset, Object x) {
+    putReferenceVolatile(o, offset, x);
+  }
+
+  public final void putReferenceRelease(Object o, long offset, Object x) {
+    putReferenceVolatile(o, offset, x);
+  }
+
+  public native void putReferenceVolatile(Object o, long offset, Object x);
 
   @Deprecated
   public void putObject(Object obj, int offset, Object obj1) {
@@ -330,10 +355,6 @@ public void putDouble(Object obj, int offset, double d) {
 
   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_jdk_internal_misc_Unsafe.java b/src/peers/gov/nasa/jpf/vm/JPF_jdk_internal_misc_Unsafe.java
@@ -106,7 +106,7 @@ public long objectFieldOffset__Ljava_lang_Class_2Ljava_lang_String_2__J (MJIEnv
   public boolean compareAndSetReference__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);
+      putReference__Ljava_lang_Object_2JLjava_lang_Object_2__V(env, unsafeRef, oRef, offset, xRef);
       return true;
     }
     return false;
@@ -158,7 +158,7 @@ public boolean compareAndSwapObject__Ljava_lang_Object_2JLjava_lang_Object_2Ljav
                                                                                                              int expectRef, int updateRef) {
     int actual = getObject__Ljava_lang_Object_2J__Ljava_lang_Object_2(env, unsafeRef, objRef, fieldOffset);
     if (actual == expectRef) {
-      putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(env, unsafeRef, objRef, fieldOffset, updateRef);
+      putReference__Ljava_lang_Object_2JLjava_lang_Object_2__V(env, unsafeRef, objRef, fieldOffset, updateRef);
       return true;
     }
     return false;
@@ -299,7 +299,7 @@ public int getObjectVolatile__Ljava_lang_Object_2J__Ljava_lang_Object_2 (MJIEnv
   }
 
   @MJI
-  public void putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V (MJIEnv env, int unsafeRef,
+  public void putReference__Ljava_lang_Object_2JLjava_lang_Object_2__V (MJIEnv env, int unsafeRef,
                                                                             int objRef, long fieldOffset, int valRef) {
     ElementInfo ei = env.getModifiableElementInfo(objRef);
 
@@ -312,9 +312,9 @@ public void putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V (MJIEnv env, i
   }
 
   @MJI
-  public void putObjectVolatile__Ljava_lang_Object_2JLjava_lang_Object_2__V (MJIEnv env, int unsafeRef,
+  public void putReferenceVolatile__Ljava_lang_Object_2JLjava_lang_Object_2__V (MJIEnv env, int unsafeRef,
       int objRef, long fieldOffset, int valRef) {
-    putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V( env, unsafeRef, objRef, fieldOffset, valRef);
+    putReference__Ljava_lang_Object_2JLjava_lang_Object_2__V( env, unsafeRef, objRef, fieldOffset, valRef);
   }
 
   @MJI
@@ -324,7 +324,7 @@ public void putOrderedObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(
                                                                                   int objRef,
                                                                                   long fieldOffset,
                                                                                   int valRef) {
-    putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(env, unsafeRef, objRef, fieldOffset, valRef);
+    putReference__Ljava_lang_Object_2JLjava_lang_Object_2__V(env, unsafeRef, objRef, fieldOffset, valRef);
   }
 
   @MJI