gov.nasa.jpf.vm

Class JPF_sun_misc_Unsafe

java.lang.Object

gov.nasa.jpf.vm.NativePeer

gov.nasa.jpf.vm.JPF_sun_misc_Unsafe

All Implemented Interfaces:

Cloneable

public class JPF_sun_misc_Unsafe
extends NativePeer

we don't want this class! This is a hodgepodge of stuff that shouldn't be in Java, but is handy for some hacks. The reason we have it here - very rudimentary - is that java.util.concurrent makes use of the atomic compare&swap which is in it. The choice was to duplicate a lot of relatively difficult code in the "right" class (java.util.concurrent.locks.AbstractQueuedSynchronizer) or a small amount of straight forward code in the "wrong" class (sun.misc.Unsafe). Knowing a bit about the "library chase" game, we opt for the latter <2do> this might change with better modeling of high level java.util.concurrent constructs

Constructor Summary

Constructors

Constructor and Description
JPF_sun_misc_Unsafe()

Method Summary

Methods

Modifier and Type	Method and Description
long	allocateMemory__J__J(MJIEnv env, int unsafeRef, long nBytes)
int	arrayBaseOffset__Ljava_lang_Class_2__I(MJIEnv env, int unsafeRef, int clazz)
int	arrayIndexScale__Ljava_lang_Class_2__I(MJIEnv env, int unsafeRef, int clazz)
boolean	compareAndSwapInt__Ljava_lang_Object_2JII__Z(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, int expect, int update)
boolean	compareAndSwapLong__Ljava_lang_Object_2JJJ__Z(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, long expect, long update)
boolean	compareAndSwapObject__Ljava_lang_Object_2JLjava_lang_Object_2Ljava_lang_Object_2__Z(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, int expectRef, int updateRef)
void	ensureClassInitialized__Ljava_lang_Class_2__V(MJIEnv env, int unsafeRef, int clsObjRef)
int	fieldOffset__Ljava_lang_reflect_Field_2__I(MJIEnv env, int unsafeRef, int fieldRef) we don't really return an offset here, since that would be useless.
void	freeMemory__J__V(MJIEnv env, int unsafeRef, long startAddress)
boolean	getBoolean__Ljava_lang_Object_2J__Z(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
boolean	getBooleanVolatile__Ljava_lang_Object_2J__Z(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
byte	getByte__J__B(MJIEnv env, int unsafeRef, long address)
byte	getByte__Ljava_lang_Object_2J__B(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
byte	getByteVolatile__Ljava_lang_Object_2J__B(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
char	getChar__J__C(MJIEnv env, int unsafeRef, long address)
char	getChar__Ljava_lang_Object_2J__C(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
char	getCharVolatile__Ljava_lang_Object_2J__C(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
double	getDouble__Ljava_lang_Object_2J__D(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
double	getDoubleVolatile__Ljava_lang_Object_2J__D(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
float	getFloat__Ljava_lang_Object_2J__F(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
float	getFloatVolatile__Ljava_lang_Object_2J__F(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
int	getInt__J__I(MJIEnv env, int unsafeRef, long address)
int	getInt__Ljava_lang_Object_2J__I(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
int	getIntVolatile__Ljava_lang_Object_2J__I(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
long	getLong__J__J(MJIEnv env, int unsafeRef, long address)
long	getLong__Ljava_lang_Object_2J__J(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
long	getLongVolatile__Ljava_lang_Object_2J__J(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
int	getObject__Ljava_lang_Object_2J__Ljava_lang_Object_2(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
int	getObjectVolatile__Ljava_lang_Object_2J__Ljava_lang_Object_2(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
short	getShort__Ljava_lang_Object_2J__S(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
short	getShortVolatile__Ljava_lang_Object_2J__S(MJIEnv env, int unsafeRef, int objRef, long fieldOffset)
int	getUnsafe____Lsun_misc_Unsafe_2(MJIEnv env, int clsRef)
long	objectFieldOffset__Ljava_lang_reflect_Field_2__J(MJIEnv env, int unsafeRef, int fieldRef)
void	park__ZJ__V(MJIEnv env, int unsafeRef, boolean isAbsoluteTime, long timeout)
void	putBoolean__Ljava_lang_Object_2JZ__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, boolean val)
void	putBooleanVolatile__Ljava_lang_Object_2JZ__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, boolean val)
void	putByte__JB__V(MJIEnv env, int unsafeRef, long address, byte val)
void	putByte__Ljava_lang_Object_2JB__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, byte val)
void	putByteVolatile__Ljava_lang_Object_2JB__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, byte val)
void	putChar__JC__V(MJIEnv env, int unsafeRef, long address, char val)
void	putChar__Ljava_lang_Object_2JC__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, char val)
void	putCharVolatile__Ljava_lang_Object_2JC__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, char val)
void	putDouble__Ljava_lang_Object_2JD__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, double val)
void	putDoubleVolatile__Ljava_lang_Object_2JD__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, double val)
void	putFloat__Ljava_lang_Object_2JF__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, float val)
void	putFloatVolatile__Ljava_lang_Object_2JF__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, float val)
void	putInt__JI__V(MJIEnv env, int unsafeRef, long address, int val)
void	putInt__Ljava_lang_Object_2JI__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, int val)
void	putIntVolatile__Ljava_lang_Object_2JI__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, int val)
void	putLong__JJ__V(MJIEnv env, int unsafeRef, long address, long val)
void	putLong__Ljava_lang_Object_2JJ__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, long val)
void	putLongVolatile__Ljava_lang_Object_2JJ__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, long val)
void	putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, int valRef)
void	putObjectVolatile__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, int valRef)
void	putOrderedInt__Ljava_lang_Object_2JI__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, int val)
void	putOrderedLong__Ljava_lang_Object_2JJ__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, long val)
void	putOrderedObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, int valRef)
void	putShort__Ljava_lang_Object_2JS__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, short val)
void	putShortVolatile__Ljava_lang_Object_2JS__V(MJIEnv env, int unsafeRef, int objRef, long fieldOffset, short val)
void	unpark__Ljava_lang_Object_2__V(MJIEnv env, int unsafeRef, int objRef)

Methods inherited from class gov.nasa.jpf.vm.NativePeer

getInstance, getInstance, getPeerClass, getPeerClassName, init, initialize, initializePeerClass

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

JPF_sun_misc_Unsafe

public JPF_sun_misc_Unsafe()

Method Detail

getUnsafe____Lsun_misc_Unsafe_2

public int getUnsafe____Lsun_misc_Unsafe_2(MJIEnv env,
                                  int clsRef)

objectFieldOffset__Ljava_lang_reflect_Field_2__J

public long objectFieldOffset__Ljava_lang_reflect_Field_2__J(MJIEnv env,
                                                    int unsafeRef,
                                                    int fieldRef)

fieldOffset__Ljava_lang_reflect_Field_2__I

public int fieldOffset__Ljava_lang_reflect_Field_2__I(MJIEnv env,
                                             int unsafeRef,
                                             int fieldRef)

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 registration id

compareAndSwapObject__Ljava_lang_Object_2JLjava_lang_Object_2Ljava_lang_Object_2__Z

public boolean compareAndSwapObject__Ljava_lang_Object_2JLjava_lang_Object_2Ljava_lang_Object_2__Z(MJIEnv env,
                                                                                          int unsafeRef,
                                                                                          int objRef,
                                                                                          long fieldOffset,
                                                                                          int expectRef,
                                                                                          int updateRef)

compareAndSwapInt__Ljava_lang_Object_2JII__Z

public boolean compareAndSwapInt__Ljava_lang_Object_2JII__Z(MJIEnv env,
                                                   int unsafeRef,
                                                   int objRef,
                                                   long fieldOffset,
                                                   int expect,
                                                   int update)

compareAndSwapLong__Ljava_lang_Object_2JJJ__Z

public boolean compareAndSwapLong__Ljava_lang_Object_2JJJ__Z(MJIEnv env,
                                                    int unsafeRef,
                                                    int objRef,
                                                    long fieldOffset,
                                                    long expect,
                                                    long update)

park__ZJ__V

public void park__ZJ__V(MJIEnv env,
               int unsafeRef,
               boolean isAbsoluteTime,
               long timeout)

unpark__Ljava_lang_Object_2__V

public void unpark__Ljava_lang_Object_2__V(MJIEnv env,
                                  int unsafeRef,
                                  int objRef)

ensureClassInitialized__Ljava_lang_Class_2__V

public void ensureClassInitialized__Ljava_lang_Class_2__V(MJIEnv env,
                                                 int unsafeRef,
                                                 int clsObjRef)

getObject__Ljava_lang_Object_2J__Ljava_lang_Object_2

public int getObject__Ljava_lang_Object_2J__Ljava_lang_Object_2(MJIEnv env,
                                                       int unsafeRef,
                                                       int objRef,
                                                       long fieldOffset)

getObjectVolatile__Ljava_lang_Object_2J__Ljava_lang_Object_2

public int getObjectVolatile__Ljava_lang_Object_2J__Ljava_lang_Object_2(MJIEnv env,
                                                               int unsafeRef,
                                                               int objRef,
                                                               long fieldOffset)

putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V

public void putObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env,
                                                         int unsafeRef,
                                                         int objRef,
                                                         long fieldOffset,
                                                         int valRef)

putObjectVolatile__Ljava_lang_Object_2JLjava_lang_Object_2__V

public void putObjectVolatile__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env,
                                                                 int unsafeRef,
                                                                 int objRef,
                                                                 long fieldOffset,
                                                                 int valRef)

putOrderedObject__Ljava_lang_Object_2JLjava_lang_Object_2__V

public void putOrderedObject__Ljava_lang_Object_2JLjava_lang_Object_2__V(MJIEnv env,
                                                                int unsafeRef,
                                                                int objRef,
                                                                long fieldOffset,
                                                                int valRef)

getBoolean__Ljava_lang_Object_2J__Z

public boolean getBoolean__Ljava_lang_Object_2J__Z(MJIEnv env,
                                          int unsafeRef,
                                          int objRef,
                                          long fieldOffset)

getBooleanVolatile__Ljava_lang_Object_2J__Z

public boolean getBooleanVolatile__Ljava_lang_Object_2J__Z(MJIEnv env,
                                                  int unsafeRef,
                                                  int objRef,
                                                  long fieldOffset)

putBoolean__Ljava_lang_Object_2JZ__V

public void putBoolean__Ljava_lang_Object_2JZ__V(MJIEnv env,
                                        int unsafeRef,
                                        int objRef,
                                        long fieldOffset,
                                        boolean val)

putBooleanVolatile__Ljava_lang_Object_2JZ__V

public void putBooleanVolatile__Ljava_lang_Object_2JZ__V(MJIEnv env,
                                                int unsafeRef,
                                                int objRef,
                                                long fieldOffset,
                                                boolean val)

getByte__Ljava_lang_Object_2J__B

public byte getByte__Ljava_lang_Object_2J__B(MJIEnv env,
                                    int unsafeRef,
                                    int objRef,
                                    long fieldOffset)

getByteVolatile__Ljava_lang_Object_2J__B

public byte getByteVolatile__Ljava_lang_Object_2J__B(MJIEnv env,
                                            int unsafeRef,
                                            int objRef,
                                            long fieldOffset)

putByte__Ljava_lang_Object_2JB__V

public void putByte__Ljava_lang_Object_2JB__V(MJIEnv env,
                                     int unsafeRef,
                                     int objRef,
                                     long fieldOffset,
                                     byte val)

putByteVolatile__Ljava_lang_Object_2JB__V

public void putByteVolatile__Ljava_lang_Object_2JB__V(MJIEnv env,
                                             int unsafeRef,
                                             int objRef,
                                             long fieldOffset,
                                             byte val)

getChar__Ljava_lang_Object_2J__C

public char getChar__Ljava_lang_Object_2J__C(MJIEnv env,
                                    int unsafeRef,
                                    int objRef,
                                    long fieldOffset)

getCharVolatile__Ljava_lang_Object_2J__C

public char getCharVolatile__Ljava_lang_Object_2J__C(MJIEnv env,
                                            int unsafeRef,
                                            int objRef,
                                            long fieldOffset)

putChar__Ljava_lang_Object_2JC__V

public void putChar__Ljava_lang_Object_2JC__V(MJIEnv env,
                                     int unsafeRef,
                                     int objRef,
                                     long fieldOffset,
                                     char val)

putCharVolatile__Ljava_lang_Object_2JC__V

public void putCharVolatile__Ljava_lang_Object_2JC__V(MJIEnv env,
                                             int unsafeRef,
                                             int objRef,
                                             long fieldOffset,
                                             char val)

getShort__Ljava_lang_Object_2J__S

public short getShort__Ljava_lang_Object_2J__S(MJIEnv env,
                                      int unsafeRef,
                                      int objRef,
                                      long fieldOffset)

getShortVolatile__Ljava_lang_Object_2J__S

public short getShortVolatile__Ljava_lang_Object_2J__S(MJIEnv env,
                                              int unsafeRef,
                                              int objRef,
                                              long fieldOffset)

putShort__Ljava_lang_Object_2JS__V

public void putShort__Ljava_lang_Object_2JS__V(MJIEnv env,
                                      int unsafeRef,
                                      int objRef,
                                      long fieldOffset,
                                      short val)

putShortVolatile__Ljava_lang_Object_2JS__V

public void putShortVolatile__Ljava_lang_Object_2JS__V(MJIEnv env,
                                              int unsafeRef,
                                              int objRef,
                                              long fieldOffset,
                                              short val)

getInt__Ljava_lang_Object_2J__I

public int getInt__Ljava_lang_Object_2J__I(MJIEnv env,
                                  int unsafeRef,
                                  int objRef,
                                  long fieldOffset)

getIntVolatile__Ljava_lang_Object_2J__I

public int getIntVolatile__Ljava_lang_Object_2J__I(MJIEnv env,
                                          int unsafeRef,
                                          int objRef,
                                          long fieldOffset)

putInt__Ljava_lang_Object_2JI__V

public void putInt__Ljava_lang_Object_2JI__V(MJIEnv env,
                                    int unsafeRef,
                                    int objRef,
                                    long fieldOffset,
                                    int val)

putIntVolatile__Ljava_lang_Object_2JI__V

public void putIntVolatile__Ljava_lang_Object_2JI__V(MJIEnv env,
                                            int unsafeRef,
                                            int objRef,
                                            long fieldOffset,
                                            int val)

putOrderedInt__Ljava_lang_Object_2JI__V

public void putOrderedInt__Ljava_lang_Object_2JI__V(MJIEnv env,
                                           int unsafeRef,
                                           int objRef,
                                           long fieldOffset,
                                           int val)

getFloat__Ljava_lang_Object_2J__F

public float getFloat__Ljava_lang_Object_2J__F(MJIEnv env,
                                      int unsafeRef,
                                      int objRef,
                                      long fieldOffset)

getFloatVolatile__Ljava_lang_Object_2J__F

public float getFloatVolatile__Ljava_lang_Object_2J__F(MJIEnv env,
                                              int unsafeRef,
                                              int objRef,
                                              long fieldOffset)

putFloat__Ljava_lang_Object_2JF__V

public void putFloat__Ljava_lang_Object_2JF__V(MJIEnv env,
                                      int unsafeRef,
                                      int objRef,
                                      long fieldOffset,
                                      float val)

putFloatVolatile__Ljava_lang_Object_2JF__V

public void putFloatVolatile__Ljava_lang_Object_2JF__V(MJIEnv env,
                                              int unsafeRef,
                                              int objRef,
                                              long fieldOffset,
                                              float val)

getLong__Ljava_lang_Object_2J__J

public long getLong__Ljava_lang_Object_2J__J(MJIEnv env,
                                    int unsafeRef,
                                    int objRef,
                                    long fieldOffset)

getLongVolatile__Ljava_lang_Object_2J__J

public long getLongVolatile__Ljava_lang_Object_2J__J(MJIEnv env,
                                            int unsafeRef,
                                            int objRef,
                                            long fieldOffset)

putLong__Ljava_lang_Object_2JJ__V

public void putLong__Ljava_lang_Object_2JJ__V(MJIEnv env,
                                     int unsafeRef,
                                     int objRef,
                                     long fieldOffset,
                                     long val)

putLongVolatile__Ljava_lang_Object_2JJ__V

public void putLongVolatile__Ljava_lang_Object_2JJ__V(MJIEnv env,
                                             int unsafeRef,
                                             int objRef,
                                             long fieldOffset,
                                             long val)

putOrderedLong__Ljava_lang_Object_2JJ__V

public void putOrderedLong__Ljava_lang_Object_2JJ__V(MJIEnv env,
                                            int unsafeRef,
                                            int objRef,
                                            long fieldOffset,
                                            long val)

getDouble__Ljava_lang_Object_2J__D

public double getDouble__Ljava_lang_Object_2J__D(MJIEnv env,
                                        int unsafeRef,
                                        int objRef,
                                        long fieldOffset)

getDoubleVolatile__Ljava_lang_Object_2J__D

public double getDoubleVolatile__Ljava_lang_Object_2J__D(MJIEnv env,
                                                int unsafeRef,
                                                int objRef,
                                                long fieldOffset)

putDouble__Ljava_lang_Object_2JD__V

public void putDouble__Ljava_lang_Object_2JD__V(MJIEnv env,
                                       int unsafeRef,
                                       int objRef,
                                       long fieldOffset,
                                       double val)

putDoubleVolatile__Ljava_lang_Object_2JD__V

public void putDoubleVolatile__Ljava_lang_Object_2JD__V(MJIEnv env,
                                               int unsafeRef,
                                               int objRef,
                                               long fieldOffset,
                                               double val)

arrayBaseOffset__Ljava_lang_Class_2__I

public int arrayBaseOffset__Ljava_lang_Class_2__I(MJIEnv env,
                                         int unsafeRef,
                                         int clazz)

arrayIndexScale__Ljava_lang_Class_2__I

public int arrayIndexScale__Ljava_lang_Class_2__I(MJIEnv env,
                                         int unsafeRef,
                                         int clazz)

allocateMemory__J__J

public long allocateMemory__J__J(MJIEnv env,
                        int unsafeRef,
                        long nBytes)

freeMemory__J__V

public void freeMemory__J__V(MJIEnv env,
                    int unsafeRef,
                    long startAddress)

getByte__J__B

public byte getByte__J__B(MJIEnv env,
                 int unsafeRef,
                 long address)

putByte__JB__V

public void putByte__JB__V(MJIEnv env,
                  int unsafeRef,
                  long address,
                  byte val)

getChar__J__C

public char getChar__J__C(MJIEnv env,
                 int unsafeRef,
                 long address)

putChar__JC__V

public void putChar__JC__V(MJIEnv env,
                  int unsafeRef,
                  long address,
                  char val)

getInt__J__I

public int getInt__J__I(MJIEnv env,
               int unsafeRef,
               long address)

putInt__JI__V

public void putInt__JI__V(MJIEnv env,
                 int unsafeRef,
                 long address,
                 int val)

getLong__J__J

public long getLong__J__J(MJIEnv env,
                 int unsafeRef,
                 long address)

putLong__JJ__V

public void putLong__JJ__V(MJIEnv env,
                  int unsafeRef,
                  long address,
                  long val)