src/peers/gov/nasa/jpf/vm/JPF_java_util_Random.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 package gov.nasa.jpf.vm;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.ConfigChangeListener;
  22 import gov.nasa.jpf.JPFException;
  23 import gov.nasa.jpf.annotation.MJI;
  24 import gov.nasa.jpf.vm.JPF_gov_nasa_jpf_vm_Verify;
  25 import gov.nasa.jpf.vm.MJIEnv;
  26 import gov.nasa.jpf.vm.NativePeer;
  27
  28 import java.lang.reflect.Field;
  29 import java.util.Random;
  30 import java.util.concurrent.atomic.AtomicLong;
  31
  32 import sun.misc.Unsafe;
  33
  34 /**
  35  * MJI NativePeer class for java.util.Random library abstraction
  36  *
  37  * model - peer delegation is done via restoring a singleton, which unfortunately
  38  * has to resort to the rather nasty Unsafe mechanism because the required
  39  * random internals are private. We could use per-instance native objects
  40  * stored as object attributes, but that would only partly solve the problem
  41  * because we still would have to backtrack the internal state of such objects
  42  */
  43 @SuppressWarnings("sunapi")
  44 public class JPF_java_util_Random extends NativePeer {
  45
  46   static class Delegatee extends Random {
  47     @Override
  48         public int next (int nBits){
  49       return super.next(nBits);
  50     }
  51   }
  52
  53   // we need this because cg.enumerate_random might be set on demand
  54   static class ConfigListener implements ConfigChangeListener {
  55     JPF_java_util_Random nativeRandom;
  56
  57     public ConfigListener(JPF_java_util_Random nativeRandom) {
  58       this.nativeRandom = nativeRandom;
  59     }
  60
  61     @Override
  62     public void propertyChanged(Config config, String key, String oldValue, String newValue) {
  63       if ("cg.enumerate_random".equals(key)) {
  64         nativeRandom.setEnumerateRandom(config);
  65       }
  66     }
  67
  68     @Override
  69     public void jpfRunTerminated(Config config){
  70       config.removeChangeListener(this);
  71     }
  72   }
  73
  74   boolean enumerateRandom;
  75
  76   // those are only used if enumerateRandom is not set, i.e. we delegate to the host VM
  77   boolean reproducibleRandom;
  78   long constantSeed;
  79   int[] defaultIntSet; // in case we have an nextInt(), i.e. an unspecified upper boundary
  80   long[] defaultLongSet;
  81   double[] defaultDoubleSet;
  82   float[] defaultFloatSet;
  83
  84   // since peer methods are atomic, we just keep one delegator instead of per-object,
  85   // which would have to rely on attributes and still require storing/restoring
  86   // the seed state with nasty Unsafe
  87   static Delegatee delegatee = new Delegatee();
  88
  89   // this is bad stuff we need to set/retrieve the Random.seed value. We only have
  90   // a choice between a rock and a hard place here - either we depend on this
  91   // field and sun.misc.Unsafe, or we duplicate the algorithms. The hard place
  92   // seems worse than the rock
  93   private static Unsafe unsafe;
  94   private static long seedFieldOffset;
  95
  96   static {
  97     try {
  98       // Unsafe.getUnsafe() can only be called from a SystemClassLoaderContext
  99       Field singletonField = Unsafe.class.getDeclaredField("theUnsafe");
 100       singletonField.setAccessible(true);
 101       unsafe = (Unsafe)singletonField.get(null);
 102
 103       seedFieldOffset = unsafe.objectFieldOffset(Random.class.getDeclaredField("seed"));
 104     } catch (Exception ex) {
 105       throw new JPFException("cannot access java.util.Random internals: " + ex);
 106     }
 107   }
 108
 109   private static void setNativeSeed (Random rand, long seed) {
 110     AtomicLong al = (AtomicLong) unsafe.getObject(rand, seedFieldOffset);
 111     al.set(seed);
 112   }
 113
 114   private static long getNativeSeed (Random rand){
 115     AtomicLong al = (AtomicLong) unsafe.getObject(rand, seedFieldOffset);
 116     return al.longValue();
 117   }
 118
 119   public JPF_java_util_Random (Config conf) {
 120     setEnumerateRandom(conf);
 121     conf.addChangeListener(new ConfigListener(this));
 122
 123     reproducibleRandom = conf.getBoolean("vm.reproducible_random", true);
 124     constantSeed = conf.getLong("vm.random_seed", 42);
 125     defaultIntSet = conf.getIntArray("vm.random_ints", Integer.MIN_VALUE, 0, Integer.MAX_VALUE);
 126     defaultDoubleSet = conf.getDoubleArray("vm.random_doubles", Double.MIN_VALUE, 0, Double.MAX_VALUE);
 127     defaultLongSet = conf.getLongArray("vm.random_longs", Long.MIN_VALUE, 0, Long.MAX_VALUE);
 128     defaultFloatSet = conf.getFloatArray("vm.random_floats", Float.MIN_VALUE, 0, Float.MAX_VALUE);
 129   }
 130
 131   void setEnumerateRandom (Config conf) {
 132     enumerateRandom = conf.getBoolean("cg.enumerate_random", false);
 133
 134     if (enumerateRandom){
 135       JPF_gov_nasa_jpf_vm_Verify.init(conf);
 136     }
 137   }
 138
 139   long computeDefaultSeed(){
 140     Random rand = (reproducibleRandom) ? new Random(constantSeed) : new Random();
 141     return getNativeSeed( rand);
 142   }
 143
 144   static void storeSeed (MJIEnv env, int objRef, long seed){
 145     env.setLongField(objRef, "seed", seed);
 146   }
 147
 148   static long getSeed (MJIEnv env, int objRef){
 149     return env.getLongField(objRef, "seed");
 150   }
 151
 152   static void restoreRandomState (MJIEnv env, int objRef, Random rand){
 153     long seed = getSeed( env, objRef);
 154     setNativeSeed( rand, seed);
 155   }
 156
 157   static void storeRandomState (MJIEnv env, int objRef, Random rand){
 158     long seed = getNativeSeed( rand);
 159     storeSeed( env, objRef, seed);
 160   }
 161
 162
 163   //--- the publics
 164
 165   @MJI
 166   public void $init____V (MJIEnv env, int objRef){
 167     long seed = computeDefaultSeed();
 168     storeSeed( env, objRef, seed);
 169   }
 170
 171   @MJI
 172   public void $init__J__V (MJIEnv env, int objRef, long seedStarter){
 173     // note - the provided seedStarter is modified by java.util.Random, it is
 174     // NOT the internal value that is consecutively used
 175     Random rand = new Random(seedStarter);
 176     storeRandomState(env, objRef, rand);
 177   }
 178
 179   @MJI
 180   public void setSeed__J__V (MJIEnv env, int objRef, long seedStarter){
 181     // my, what an effort to change a long.
 182     restoreRandomState( env, objRef, delegatee);
 183     delegatee.setSeed(seedStarter); // compute the new internal value
 184     storeRandomState(env, objRef, delegatee);
 185   }
 186
 187   @MJI
 188   public boolean nextBoolean____Z (MJIEnv env, int objRef){
 189     if (enumerateRandom){
 190       return JPF_gov_nasa_jpf_vm_Verify.getBoolean____Z(env,-1);
 191
 192     } else {
 193       restoreRandomState(env, objRef, delegatee);
 194       boolean ret = delegatee.nextBoolean();
 195       storeRandomState(env, objRef, delegatee);
 196       return ret;
 197     }
 198   }
 199
 200   @MJI
 201   public int nextInt__I__I (MJIEnv env, int objRef, int n){
 202     if (enumerateRandom){
 203       return JPF_gov_nasa_jpf_vm_Verify.getInt__II__I(env,-1,0,n-1);
 204
 205     } else {
 206       restoreRandomState(env, objRef, delegatee);
 207       int ret = delegatee.nextInt(n);
 208       storeRandomState(env, objRef, delegatee);
 209       return ret;
 210     }
 211   }
 212
 213   @MJI
 214   public int nextInt____I (MJIEnv env, int objRef){
 215     if (enumerateRandom){
 216       return JPF_gov_nasa_jpf_vm_Verify.getIntFromList(env, defaultIntSet);
 217
 218     } else {
 219       restoreRandomState(env, objRef, delegatee);
 220       int ret = delegatee.nextInt();
 221       storeRandomState(env, objRef, delegatee);
 222       return ret;
 223     }
 224   }
 225
 226   @MJI
 227   public int next__I__I (MJIEnv env, int objRef, int nBits){
 228     if (enumerateRandom){
 229       // <2do> we can't do this with an interval since it most likely would explode our state space
 230       return JPF_gov_nasa_jpf_vm_Verify.getIntFromList(env, defaultIntSet);
 231
 232     } else {
 233       restoreRandomState(env, objRef, delegatee);
 234       int ret = delegatee.next( nBits);
 235       storeRandomState(env, objRef, delegatee);
 236       return ret;
 237     }
 238   }
 239
 240   @MJI
 241   public void nextBytes___3B__V (MJIEnv env, int objRef, int dataRef){
 242     // <2do> this one is an even worse state exploder. We could use cascaded CGs,
 243     // but chances are this really kills us, so we just ignore 'enumerateRandom' for now
 244
 245     int n = env.getArrayLength(dataRef);
 246     byte[] data = new byte[n];
 247
 248     restoreRandomState(env, objRef, delegatee);
 249     delegatee.nextBytes(data);
 250     storeRandomState(env, objRef, delegatee);
 251
 252     for (int i = 0; i < n; i++) {
 253       env.setByteArrayElement(dataRef, i, data[i]);
 254     }
 255   }
 256
 257   @MJI
 258   public long nextLong____J (MJIEnv env, int objRef){
 259     if (enumerateRandom){
 260       return JPF_gov_nasa_jpf_vm_Verify.getLongFromList(env, defaultLongSet);
 261
 262     } else {
 263       restoreRandomState(env, objRef, delegatee);
 264       long ret = delegatee.nextLong();
 265       storeRandomState(env, objRef, delegatee);
 266       return ret;
 267     }
 268   }
 269
 270   @MJI
 271   public float nextFloat____F (MJIEnv env, int objRef){
 272     if (enumerateRandom){
 273       return JPF_gov_nasa_jpf_vm_Verify.getFloatFromList(env, defaultFloatSet);
 274
 275     } else {
 276       restoreRandomState(env, objRef, delegatee);
 277       float ret = delegatee.nextFloat();
 278       storeRandomState(env, objRef, delegatee);
 279       return ret;
 280     }
 281   }
 282
 283   @MJI
 284   public double nextDouble____D (MJIEnv env, int objRef){
 285     if (enumerateRandom){
 286       return JPF_gov_nasa_jpf_vm_Verify.getDoubleFromList(env, defaultDoubleSet);
 287
 288     } else {
 289       restoreRandomState(env, objRef, delegatee);
 290       double ret = delegatee.nextDouble();
 291       storeRandomState(env, objRef, delegatee);
 292       return ret;
 293     }
 294   }
 295
 296   @MJI
 297   public double nextGaussian____D (MJIEnv env, int objRef){
 298     // <2do> we don't support this yet, neither for enumerateRandom nor
 299     // delegation (which would require an additional 'haveNextGaussian' state)
 300     restoreRandomState(env, objRef, delegatee);
 301     double ret = delegatee.nextGaussian();
 302     storeRandomState(env, objRef, delegatee);
 303     return ret;
 304   }
 305 }