src/peers/gov/nasa/jpf/vm/JPF_java_lang_ThreadLocal.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  * peer for java.lang.ThreadLocal
  25  */
  26 public class JPF_java_lang_ThreadLocal extends NativePeer {
  27
  28   @MJI
  29   public int getEntry____Ljava_lang_ThreadLocal$Entry_2 (MJIEnv env, int objRef){
  30     ThreadInfo ti = env.getThreadInfo();
  31     int tObjRef = ti.getThreadObjectRef();
  32
  33     int aRef = env.getReferenceField(tObjRef, "threadLocals");
  34     if (aRef == MJIEnv.NULL){
  35       return MJIEnv.NULL;
  36     }
  37     int[] erefs = env.getReferenceArrayObject(aRef);
  38     int len = env.getArrayLength(aRef);
  39
  40
  41     for (int i=0; i<len; i++){
  42       int e = erefs[i];
  43       int k = env.getReferenceField(e, "ref");
  44
  45       if (k == objRef){
  46         return e;
  47       }
  48     }
  49
  50     return MJIEnv.NULL;
  51   }
  52
  53   @MJI
  54   public void addEntry__Ljava_lang_ThreadLocal$Entry_2 (MJIEnv env, int objRef, int eRef){
  55     ThreadInfo ti = env.getThreadInfo();
  56     int tObjRef = ti.getThreadObjectRef();
  57     int aRef = env.getReferenceField(tObjRef, "threadLocals");
  58
  59     if (aRef == MJIEnv.NULL){ // first entry
  60       int newaRef = env.newObjectArray("Ljava/lang/ThreadLocal.Entry;", 1);
  61       env.setReferenceArrayElement(newaRef, 0, eRef);
  62       env.setReferenceField(tObjRef, "threadLocals", newaRef);
  63
  64     } else {
  65       int len = env.getArrayLength(aRef);
  66       int[] erefs = env.getReferenceArrayObject(aRef);
  67
  68       // new key/value
  69       int newaRef = env.newObjectArray("Ljava/lang/ThreadLocal.Entry;", len+1);
  70       env.arrayCopy(aRef, 0, newaRef, 0, len);
  71       env.setReferenceArrayElement(newaRef, len, eRef);
  72       env.setReferenceField(tObjRef, "threadLocals", newaRef);
  73     }
  74
  75   }
  76
  77   @MJI
  78   public void removeEntry__Ljava_lang_ThreadLocal$Entry_2 (MJIEnv env, int objRef, int eRef){
  79     ThreadInfo ti = env.getThreadInfo();
  80     int tObjRef = ti.getThreadObjectRef();
  81     int aRef = env.getReferenceField(tObjRef, "threadLocals");
  82
  83     if (aRef != MJIEnv.NULL){
  84       int len = env.getArrayLength(aRef);
  85       int[] erefs = env.getReferenceArrayObject(aRef);
  86       int newaRef = env.newObjectArray("Ljava/lang/ThreadLocal.Entry;", len-1);
  87
  88       for (int i=0, j=0; i<len; i++){
  89         int e = erefs[i];
  90         if (e != eRef){
  91           env.setReferenceArrayElement(newaRef, j++, e);
  92         }
  93       }
  94
  95       env.setReferenceField(tObjRef, "threadLocals", newaRef);
  96     }
  97   }
  98 }