src/main/gov/nasa/jpf/vm/Verify.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 java.io.FileInputStream;
  21 import java.io.FileOutputStream;
  22 import java.io.ObjectInputStream;
  23 import java.io.ObjectOutputStream;
  24 import java.util.BitSet;
  25 import java.util.Random;
  26
  27
  28 /**
  29  * Verify is the programmatic interface of JPF that can be used from inside of
  30  * applications. In order to enable programs to run outside of the JPF
  31  * environment, we provide (mostly empty) bodies for the methods that are
  32  * otherwise intercepted by the native peer class
  33  */
  34 public class Verify {
  35   static final int MAX_COUNTERS = 10;
  36   static int[] counter;  // only here so that we don't pull in all JPF classes at RT
  37
  38   private static Random random;
  39
  40   /*
  41    * only set if this was used from within a JPF context. This is mainly to
  42    * enable encapsulation of JPF specific types so that they only get
  43    * pulled in on demand, and we otherwise can still use the same Verify class
  44    * for JPF-external execution. We use a class object to make sure it doesn't
  45    * get recycled once JPF is terminated.
  46    */
  47   static Class<?> peer;
  48
  49   private static Random getRandom() {
  50     if (random == null) {
  51       random = new Random(42);
  52     }
  53     return random;
  54   }
  55
  56   /*
  57    * register the peer class, which is only done from within a JPF execution
  58    * context. Be aware of that this migh actually load the real Verify class.
  59    * The sequence usually is
  60    *   JPF(Verify) -> VM(JPF_gov_nasa_jpf_vm_Verify) -> VM(Verify)
  61    */
  62   public static void setPeerClass (Class<?> cls) {
  63     peer = cls;
  64   }
  65
  66   // note this is NOT marked native because we might also call it from host VM code
  67   // (beware that Verify is a different class there!). When executed by JPF,
  68   // this is an MJI method
  69   public static int getCounter (int id) {
  70     if (peer != null) {
  71       // this is executed if we are in a JPF context
  72       return JPF_gov_nasa_jpf_vm_Verify.getCounter__I__I(null, 0, id);
  73     } else {
  74       if (counter == null) {
  75         counter = new int[id >= MAX_COUNTERS ? (id+1) : MAX_COUNTERS];
  76       }
  77       if ((id < 0) || (id >= counter.length)) {
  78         return 0;
  79       }
  80
  81       return counter[id];
  82     }
  83   }
  84
  85   public static void resetCounter (int id) {
  86     if (peer != null){
  87       JPF_gov_nasa_jpf_vm_Verify.resetCounter__I__V(null, 0, id);
  88     } else {
  89       if ((counter != null) && (id >= 0) && (id < counter.length)) {
  90         counter[id] = 0;
  91       }
  92     }
  93   }
  94
  95   public static void setCounter (int id, int val) {
  96     if (peer != null){
  97       JPF_gov_nasa_jpf_vm_Verify.setCounter__II__V(null, 0, id, val);
  98     } else {
  99       if ((counter != null) && (id >= 0) && (id < counter.length)) {
 100         counter[id] = val;
 101       }
 102     }
 103   }
 104
 105
 106   public static int incrementCounter (int id) {
 107     if (peer != null){
 108       return JPF_gov_nasa_jpf_vm_Verify.incrementCounter__I__I(null, 0, id);
 109     } else {
 110       if (counter == null) {
 111         counter = new int[(id >= MAX_COUNTERS) ? id+1 : MAX_COUNTERS];
 112       } else if (id >= counter.length) {
 113         int[] newCounter = new int[id+1];
 114         System.arraycopy(counter, 0, newCounter, 0, counter.length);
 115         counter = newCounter;
 116       }
 117
 118       if ((id >= 0) && (id < counter.length)) {
 119         return ++counter[id];
 120       }
 121
 122       return 0;
 123     }
 124   }
 125
 126   public static final int NO_VALUE = -1;
 127
 128   public static void putValue (String key, int value) {
 129     throw new UnsupportedOperationException("putValue requires JPF execution");
 130   }
 131
 132   public static int getValue (String key) {
 133     throw new UnsupportedOperationException("getValue requires JPF execution");
 134   }
 135
 136   // same mechanism and purpose as the counters, but with BitSets, which is
 137   // more convenient if we have a lot of different events to check
 138
 139   static BitSet[] bitSets;
 140
 141   private static void checkBitSetId(int id) {
 142     if (bitSets == null) {
 143       bitSets = new BitSet[id + 1];
 144     } else if (id >= bitSets.length) {
 145       BitSet[] newBitSets = new BitSet[id + 1];
 146       System.arraycopy(bitSets, 0, newBitSets, 0, bitSets.length);
 147       bitSets = newBitSets;
 148     }
 149
 150     if (bitSets[id] == null) {
 151       bitSets[id] = new BitSet();
 152     }
 153   }
 154
 155
 156   public static void setBitInBitSet(int id, int bit, boolean value) {
 157     if (peer != null){
 158       // this is executed if we did run JPF
 159       JPF_gov_nasa_jpf_vm_Verify.setBitInBitSet__IIZ__V(null, 0, id, bit, value);
 160     } else {
 161       // this is executed if we run this without previously executing JPF
 162       checkBitSetId(id);
 163       bitSets[id].set(bit, value);
 164     }
 165   }
 166
 167   public static boolean getBitInBitSet(int id, int bit) {
 168     if (peer != null){
 169       // this is executed if we did run JPF
 170       return JPF_gov_nasa_jpf_vm_Verify.getBitInBitSet__II__Z(null, 0, id, bit);
 171
 172     } else {
 173       // this is executed if we run this without previously executing JPF
 174       checkBitSetId(id);
 175       return bitSets[id].get(bit);
 176     }
 177   }
 178
 179   /**
 180    * Adds a comment to the error trace, which will be printed and saved.
 181    */
 182   public static void addComment (String s) {}
 183
 184   /**
 185    * Backwards compatibility START
 186    * @deprecated use "assert cond : msg"
 187    */
 188   @Deprecated
 189   public static void assertTrue (String s, boolean cond) {
 190     if (!cond) {
 191       System.out.println(s);
 192       assertTrue(cond);
 193     }
 194   }
 195
 196   /**
 197    * Checks that the condition is true.
 198    * @deprecated use 'assert' directly
 199    */
 200   @Deprecated
 201   public static void assertTrue (boolean cond) {
 202     if (!cond) {
 203       throw new AssertionError("Verify.assertTrue failed");
 204     }
 205   }
 206
 207   public static void atLabel (String label) {}
 208
 209   public static void atLabel (int label) {}
 210
 211   /**
 212    * Marks the beginning of an atomic block.
 213    * THIS IS EVIL, DON'T USE IT FOR OPTIMIZATION - THAT'S WHAT POR IS FOR!
 214    * (it's mostly here to support model classes that need to execute atomic)
 215    */
 216   public static void beginAtomic () {}
 217
 218   /**
 219    * Marks the end of an atomic block.
 220    * EVIL - see beginAtomic()
 221    */
 222   public static void endAtomic () {}
 223
 224   public static void boring (boolean cond) {}
 225
 226   public static void busyWait (long duration) {
 227     // this gets only executed outside of JPF
 228     while (duration > 0) {
 229       duration--;
 230     }
 231   }
 232
 233   public static boolean isCalledFromClass (String refClsName) {
 234     Throwable t = new Throwable();
 235     StackTraceElement[] st = t.getStackTrace();
 236
 237     if (st.length < 3) {
 238       // main() or run()
 239       return false;
 240     }
 241
 242     try {
 243       Class<?> refClazz = Class.forName(refClsName);
 244       Class<?> callClazz = Class.forName(st[2].getClassName());
 245
 246       return (refClazz.isAssignableFrom(callClazz));
 247
 248     } catch (ClassNotFoundException cfnx) {
 249       return false;
 250     }
 251   }
 252
 253   public static void ignoreIf (boolean cond) {}
 254
 255   public static void instrumentPoint (String label) {}
 256
 257   public static void instrumentPointDeep (String label) {}
 258
 259   public static void instrumentPointDeepRecur (String label, int depth) {}
 260
 261   public static void interesting (boolean cond) {}
 262
 263   public static void breakTransition (String reason) {}
 264
 265  /** for testing and debugging purposes */
 266   public static int breakTransition (String reason, int min, int max) {
 267     return -1;
 268   }
 269
 270   /**
 271    * simple debugging aids to imperatively print the current path output of the SUT
 272    * (to be used with vm.path_output)
 273    */
 274   public static void printPathOutput(String msg) {}
 275   public static void printPathOutput(boolean cond, String msg) {}
 276
 277   public static void threadPrint (String s) {
 278     System.out.print( Thread.currentThread().getName());
 279     System.out.print(": ");
 280     System.out.print(s);
 281   }
 282
 283   public static void threadPrintln (String s) {
 284     threadPrint(s);
 285     System.out.println();
 286   }
 287
 288   public static void print (String s) {
 289     System.out.print(s);
 290   }
 291
 292   public static void println (String s) {
 293     System.out.println(s);
 294   }
 295
 296   public static void print (String s, int i) {
 297     System.out.print(s + " : " + i);
 298   }
 299
 300   public static void print (String s, boolean b) {
 301     System.out.print(s + " : " + b);
 302   }
 303
 304   public static void println() {
 305     System.out.println();
 306   }
 307
 308   /**
 309    * this is to avoid StringBuilders
 310    */
 311   public static void print (String... args){
 312     for (String s : args){
 313       System.out.print(s);
 314     }
 315   }
 316
 317   /**
 318    * note - these are mostly for debugging purposes (to see if attributes get
 319    * propagated correctly, w/o having to write a listener), since attributes are
 320    * supposed to be created at the native side, and hence can't be accessed from
 321    * the application
 322    */
 323
 324   //--- use these if you know there are single attributes
 325   public static void setFieldAttribute (Object o, String fieldName, int val) {}
 326   public static int getFieldAttribute (Object o, String fieldName) { return 0; }
 327
 328   //--- use these for multiple attributes
 329   public static void addFieldAttribute (Object o, String fieldName, int val) {}
 330   public static int[] getFieldAttributes (Object o, String fieldName) { return new int[0]; }
 331
 332   public static void setLocalAttribute (String varName, int val) {}
 333   public static int getLocalAttribute (String varName) { return 0; }
 334
 335   public static void addLocalAttribute (String varName, int val) {}
 336   public static int[] getLocalAttributes (String varName) { return new int[0]; }
 337
 338   public static void setElementAttribute (Object arr, int idx, int val){}
 339   public static int getElementAttribute (Object arr, int idx) { return 0; }
 340
 341   public static void addElementAttribute (Object arr, int idx, int val){}
 342   public static int[] getElementAttributes (Object arr, int idx) { return new int[0]; }
 343
 344   public static void setObjectAttribute (Object o, int val) {}
 345   public static int getObjectAttribute (Object o) { return 0; }
 346
 347   public static void addObjectAttribute (Object o, int val) {}
 348   public static int[] getObjectAttributes (Object o) { return new int[0]; }
 349
 350
 351   /**
 352    * this is the new boolean choice generator. Since there's no real
 353    * heuristic involved with boolean values, we skip the id (it's a
 354    * hardwired "boolean")
 355    */
 356   public static boolean getBoolean () {
 357     // just executed when not running inside JPF, native otherwise
 358     return ((System.currentTimeMillis() & 1) != 0);
 359   }
 360
 361   /**
 362    * new boolean choice generator that also tells jpf which value to
 363    * use first by default in a search.
 364    */
 365   public static boolean getBoolean (boolean falseFirst) {
 366     // this is only executed when not running JPF
 367     return getBoolean();
 368   }
 369
 370
 371   /**
 372    * Returns int nondeterministically between (and including) min and max.
 373    */
 374   public static int getInt (int min, int max) {
 375     // this is only executed when not running JPF, native otherwise
 376     return getRandom().nextInt((max-min+1)) + min;
 377   }
 378
 379   public static int getIntFromList (int... values){
 380     if (values != null && values.length > 0) {
 381       int i = getRandom().nextInt(values.length);
 382       return values[i];
 383     } else {
 384       return getRandom().nextInt();
 385     }
 386   }
 387
 388   public static Object getObject (String key) {
 389     return "?";
 390   }
 391
 392   /**
 393    * this is the API for int value choice generators. 'id' is used to identify
 394    * both the corresponding ChoiceGenerator subclass, and the application specific
 395    * ctor parameters from the normal JPF configuration mechanism
 396    */
 397   public static int getInt (String key){
 398     // this is only executed when not running JPF, native otherwise
 399     return getRandom().nextInt();
 400   }
 401
 402   /**
 403    * this is the API for double value choice generators. 'id' is used to identify
 404    * both the corresponding ChoiceGenerator subclass, and the application specific
 405    * ctor parameters from the normal JPF configuration mechanism
 406    */
 407   public static double getDouble (String key){
 408     // this is only executed when not running JPF, native otherwise
 409     return getRandom().nextDouble();
 410   }
 411
 412   public static double getDoubleFromList (double... values){
 413     if (values != null && values.length > 0) {
 414       int i = getRandom().nextInt(values.length);
 415       return values[i];
 416     } else {
 417       return getRandom().nextDouble();
 418     }
 419   }
 420
 421   public static long getLongFromList (long...values){
 422     if (values != null && values.length > 0) {
 423       int i = getRandom().nextInt(values.length);
 424       return values[i];
 425     } else {
 426       return getRandom().nextLong();
 427     }
 428   }
 429
 430   public static float getFloatFromList (float...values){
 431     if (values != null && values.length > 0) {
 432       int i = getRandom().nextInt(values.length);
 433       return values[i];
 434     } else {
 435       return getRandom().nextFloat();
 436     }
 437   }
 438
 439
 440   /**
 441    * Returns a random number between 0 and max inclusive.
 442    */
 443   public static int random (int max) {
 444     // this is only executed when not running JPF
 445     return getRandom().nextInt(max + 1);
 446   }
 447
 448   /**
 449    * Returns a random boolean value, true or false. Note this gets
 450    * handled by the native peer, and is just here to enable running
 451    * instrumented applications w/o JPF
 452    */
 453   public static boolean randomBool () {
 454     // this is only executed when not running JPF
 455     return getRandom().nextBoolean();
 456   }
 457
 458   public static long currentTimeMillis () {
 459     return System.currentTimeMillis();
 460   }
 461
 462   // Backwards compatibility START
 463   public static Object randomObject (String type) {
 464     return null;
 465   }
 466
 467   public static boolean isRunningInJPF() {
 468     return false;
 469   }
 470
 471   /**
 472    * USE CAREFULLY - returns true if the virtual machine this code is
 473    * running under is doing state matching.  This can be used as a hint
 474    * as to whether data structures (that are known to be correct!)
 475    * should be configured to use a canonical representation.  For example,
 476    * <pre><code>
 477    * Vector v = new Vector();
 478    * v.add(obj1);
 479    * if (Verify.getBoolean()) {
 480    *     v.addAll(eleventyBillionObjectCollection);
 481    *     v.setSize(1);
 482    * }
 483    * // compare states here
 484    * </code></pre>
 485    * To the programmer, the states are (almost certainly) the same.  To
 486    * the VM, they could be different (capacity inside the Vector).  For
 487    * the sake of speed, Vector does not store things canonically, but this
 488    * can cause (probably mild) state explosion if matching states.  If
 489    * you know whether states are being matched, you can choose the right
 490    * structure--as long as those structures aren't what you're looking for
 491    * bugs in!
 492    */
 493   public static boolean vmIsMatchingStates() {
 494     return false;
 495   }
 496
 497   public static void storeTrace (String fileName, String comment) {
 498     // intercepted in NativePeer
 499   }
 500
 501   public static void storeTraceIf (boolean cond, String fileName, String comment) {
 502     if (cond) {
 503       storeTrace(fileName, comment);
 504     }
 505   }
 506
 507   public static void storeTraceAndTerminate (String fileName, String comment) {
 508     storeTrace(fileName, comment);
 509     terminateSearch();
 510   }
 511
 512   public static void storeTraceAndTerminateIf (boolean cond, String fileName, String comment) {
 513     if (cond) {
 514       storeTrace(fileName, comment);
 515       terminateSearch();
 516     }
 517   }
 518
 519   public static boolean isTraceReplay () {
 520     return false; // native
 521   }
 522
 523   public static boolean isShared (Object o){
 524     return false; // native
 525   }
 526
 527   public static void setShared (Object o, boolean isShared) {
 528     // native
 529   }
 530
 531   public static void freezeSharedness (Object o, boolean freeze) {
 532     // native
 533   }
 534
 535   public static void terminateSearch () {
 536     // native
 537   }
 538
 539   public static void setHeuristicSearchValue (int n){
 540     // native - to control UserHeuristic
 541   }
 542
 543   public static void resetHeuristicSearchValue (){
 544     // native - to control UserHeuristic
 545   }
 546
 547   public static int getHeuristicSearchValue (){
 548     // native - to control UserHeuristic
 549     return 0;
 550   }
 551
 552   public static void setProperties (String... p) {
 553     // native
 554   }
 555
 556   public static String getProperty (String key) {
 557     // native
 558     return null;
 559   }
 560
 561   public static <T> T createFromJSON(Class<T> clazz, String json){
 562     return null;
 563   }
 564
 565   public static void writeObjectToFile(Object object, String fileName) {
 566     try {
 567       FileOutputStream fso = new FileOutputStream(fileName);
 568       ObjectOutputStream oos = new ObjectOutputStream(fso);
 569       oos.writeObject(object);
 570       oos.flush();
 571       oos.close();
 572
 573     } catch (Exception ex) {
 574       throw new RuntimeException(ex);
 575     }
 576
 577   }
 578
 579   public static <T> T readObjectFromFile(Class<T> clazz, String fileName) {
 580     try
 581     {
 582       FileInputStream fis = new FileInputStream(fileName);
 583       ObjectInputStream ois = new ObjectInputStream(fis);
 584
 585       Object read = ois.readObject();
 586
 587       return (T) read;
 588
 589     }
 590     catch (Exception ex) {
 591       throw new RuntimeException(ex);
 592     }
 593
 594   }
 595
 596
 597   //--- model logging support
 598
 599   /*
 600    * we add these here so that we don't need to pull in any java.util.logging classes
 601    * Note - these need to be kept in sync with our native peer
 602    */
 603   public static final int SEVERE = 1;
 604   public static final int WARNING = 2;
 605   public static final int INFO = 3;
 606   public static final int FINE = 4;
 607   public static final int FINER = 5;
 608   public static final int FINEST = 6;
 609
 610   public static void log( String loggerId, int logLevel, String msg){
 611     System.err.println(msg);
 612   }
 613
 614   // to avoid construction of strings on the model side
 615   public static void log( String loggerId, int logLevel, String msg, String arg){
 616     System.err.println(msg);
 617   }
 618
 619   public static void log( String loggerId, int logLevel, String format, Object... args){
 620     System.err.printf(format, args);
 621   }
 622
 623
 624 }