src/peers/gov/nasa/jpf/vm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.annotation.MJI;
  22
  23
  24 /**
  25  * a full peer for the AtomicReferenceFieldUpdater
  26  */
  27 public class JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater extends AtomicFieldUpdater {
  28
  29   @MJI
  30   public void $init__Ljava_lang_Class_2Ljava_lang_Class_2Ljava_lang_String_2__V (MJIEnv env, int objRef,
  31                                  int tClsObjRef, int fClsObjRef, int fNameRef) {
  32
  33     // direct Object subclass, so we don't have to call a super ctor
  34
  35     ClassInfo ci = env.getReferredClassInfo(tClsObjRef);
  36     String fname = env.getStringObject(fNameRef);
  37     FieldInfo fi = ci.getInstanceField(fname);
  38
  39     ClassInfo fci = fi.getTypeClassInfo();
  40
  41     ClassInfo fciCheck = env.getReferredClassInfo( fClsObjRef);
  42     if (!fci.isInstanceOf(fciCheck)) {
  43       // that's also just an approximation, but we need to check
  44       env.throwException("java.lang.RuntimeException", "wrong field type");
  45     }
  46
  47     int fidx = fi.getFieldIndex();
  48     env.setIntField(objRef, "fieldId", fidx);
  49   }
  50
  51   @MJI
  52   public boolean compareAndSet__Ljava_lang_Object_2Ljava_lang_Object_2Ljava_lang_Object_2__Z
  53                                   (MJIEnv env, int objRef, int tRef, int fExpect, int fUpdate){
  54
  55     if (tRef == MJIEnv.NULL){
  56       env.throwException("java.lang.NullPointerException", "AtomicFieldUpdater called on null object");
  57       return false;
  58     }
  59
  60     ThreadInfo ti = env.getThreadInfo();
  61     ElementInfo ei = ti.getModifiableElementInfo(tRef);
  62     FieldInfo fi = getFieldInfo( ti.getElementInfo(objRef), ei);
  63
  64     if (reschedulesAccess(ti, ei, fi)){
  65       env.repeatInvocation();
  66       return false;
  67     }
  68
  69     int v = ei.getReferenceField(fi);
  70     if (v == fExpect) {
  71       ei.setReferenceField(fi, fUpdate);
  72       return true;
  73     } else {
  74       return false;
  75     }
  76   }
  77
  78   @MJI
  79   public boolean weakCompareAndSet__Ljava_lang_Object_2Ljava_lang_Object_2Ljava_lang_Object_2__Z
  80   (MJIEnv env, int objRef, int tRef, int fExpect, int fUpdate){
  81     return(compareAndSet__Ljava_lang_Object_2Ljava_lang_Object_2Ljava_lang_Object_2__Z(env, objRef, tRef, fExpect, fUpdate));
  82   }
  83
  84   @MJI
  85   public void set__Ljava_lang_Object_2Ljava_lang_Object_2__V (MJIEnv env, int objRef, int tRef, int fNewValue){
  86
  87     if (tRef == MJIEnv.NULL){
  88       env.throwException("java.lang.NullPointerException", "AtomicFieldUpdater called on null object");
  89       return;
  90     }
  91
  92     ThreadInfo ti = env.getThreadInfo();
  93     ElementInfo ei = ti.getModifiableElementInfo(tRef);
  94     FieldInfo fi = getFieldInfo( ti.getElementInfo(objRef), ei);
  95
  96     if (reschedulesAccess(ti, ei, fi)){
  97       env.repeatInvocation();
  98       return;
  99     }
 100
 101     ei.setReferenceField(fi, fNewValue);
 102   }
 103
 104   @MJI
 105   public void lazySet__Ljava_lang_Object_2Ljava_lang_Object_2__V (MJIEnv env, int objRef, int tRef, int fNewValue){
 106      set__Ljava_lang_Object_2Ljava_lang_Object_2__V(env, objRef, tRef, fNewValue);
 107   }
 108
 109   @MJI
 110   public int get__Ljava_lang_Object_2__Ljava_lang_Object_2 (MJIEnv env, int objRef, int tRef){
 111     if (tRef == MJIEnv.NULL){
 112       env.throwException("java.lang.NullPointerException", "AtomicFieldUpdater called on null object");
 113       return MJIEnv.NULL;
 114     }
 115
 116     ThreadInfo ti = env.getThreadInfo();
 117     ElementInfo ei = ti.getElementInfo(tRef);
 118     FieldInfo fi = getFieldInfo( ti.getElementInfo(objRef), ei);
 119
 120     if (reschedulesAccess(ti, ei, fi)){
 121       env.repeatInvocation();
 122       return MJIEnv.NULL;
 123     }
 124
 125     return ei.getReferenceField(fi);
 126   }
 127
 128   @MJI
 129   public int getAndSet__Ljava_lang_Object_2Ljava_lang_Object_2__Ljava_lang_Object_2 (MJIEnv env, int objRef, int tRef, int fNewValue){
 130     if (tRef == MJIEnv.NULL){
 131       env.throwException("java.lang.NullPointerException", "AtomicFieldUpdater called on null object");
 132       return MJIEnv.NULL;
 133     }
 134
 135     ThreadInfo ti = env.getThreadInfo();
 136     ElementInfo ei = ti.getElementInfo(tRef);
 137     FieldInfo fi = getFieldInfo( ti.getElementInfo(objRef), ei);
 138
 139     if (reschedulesAccess(ti, ei, fi)){
 140       env.repeatInvocation();
 141       return MJIEnv.NULL;
 142     }
 143
 144     int result = ei.getReferenceField(fi);
 145     ei.setReferenceField(fi, fNewValue);
 146
 147     return result;
 148   }
 149 }