2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
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;
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
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
38 private static Random random;
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.
49 private static Random getRandom() {
51 random = new Random(42);
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)
62 public static void setPeerClass (Class<?> cls) {
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) {
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);
74 if (counter == null) {
75 counter = new int[id >= MAX_COUNTERS ? (id+1) : MAX_COUNTERS];
77 if ((id < 0) || (id >= counter.length)) {
85 public static void resetCounter (int id) {
87 JPF_gov_nasa_jpf_vm_Verify.resetCounter__I__V(null, 0, id);
89 if ((counter != null) && (id >= 0) && (id < counter.length)) {
95 public static void setCounter (int id, int val) {
97 JPF_gov_nasa_jpf_vm_Verify.setCounter__II__V(null, 0, id, val);
99 if ((counter != null) && (id >= 0) && (id < counter.length)) {
106 public static int incrementCounter (int id) {
108 return JPF_gov_nasa_jpf_vm_Verify.incrementCounter__I__I(null, 0, id);
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;
118 if ((id >= 0) && (id < counter.length)) {
119 return ++counter[id];
126 public static final int NO_VALUE = -1;
128 public static void putValue (String key, int value) {
129 throw new UnsupportedOperationException("putValue requires JPF execution");
132 public static int getValue (String key) {
133 throw new UnsupportedOperationException("getValue requires JPF execution");
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
139 static BitSet[] bitSets;
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;
150 if (bitSets[id] == null) {
151 bitSets[id] = new BitSet();
156 public static void setBitInBitSet(int id, int bit, boolean value) {
158 // this is executed if we did run JPF
159 JPF_gov_nasa_jpf_vm_Verify.setBitInBitSet__IIZ__V(null, 0, id, bit, value);
161 // this is executed if we run this without previously executing JPF
163 bitSets[id].set(bit, value);
167 public static boolean getBitInBitSet(int id, int bit) {
169 // this is executed if we did run JPF
170 return JPF_gov_nasa_jpf_vm_Verify.getBitInBitSet__II__Z(null, 0, id, bit);
173 // this is executed if we run this without previously executing JPF
175 return bitSets[id].get(bit);
180 * Adds a comment to the error trace, which will be printed and saved.
182 public static void addComment (String s) {}
185 * Backwards compatibility START
186 * @deprecated use "assert cond : msg"
189 public static void assertTrue (String s, boolean cond) {
191 System.out.println(s);
197 * Checks that the condition is true.
198 * @deprecated use 'assert' directly
201 public static void assertTrue (boolean cond) {
203 throw new AssertionError("Verify.assertTrue failed");
207 public static void atLabel (String label) {}
209 public static void atLabel (int label) {}
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)
216 public static void beginAtomic () {}
219 * Marks the end of an atomic block.
220 * EVIL - see beginAtomic()
222 public static void endAtomic () {}
224 public static void boring (boolean cond) {}
226 public static void busyWait (long duration) {
227 // this gets only executed outside of JPF
228 while (duration > 0) {
233 public static boolean isCalledFromClass (String refClsName) {
234 Throwable t = new Throwable();
235 StackTraceElement[] st = t.getStackTrace();
243 Class<?> refClazz = Class.forName(refClsName);
244 Class<?> callClazz = Class.forName(st[2].getClassName());
246 return (refClazz.isAssignableFrom(callClazz));
248 } catch (ClassNotFoundException cfnx) {
253 public static void ignoreIf (boolean cond) {}
255 public static void instrumentPoint (String label) {}
257 public static void instrumentPointDeep (String label) {}
259 public static void instrumentPointDeepRecur (String label, int depth) {}
261 public static void interesting (boolean cond) {}
263 public static void breakTransition (String reason) {}
265 /** for testing and debugging purposes */
266 public static int breakTransition (String reason, int min, int max) {
271 * simple debugging aids to imperatively print the current path output of the SUT
272 * (to be used with vm.path_output)
274 public static void printPathOutput(String msg) {}
275 public static void printPathOutput(boolean cond, String msg) {}
277 public static void threadPrint (String s) {
278 System.out.print( Thread.currentThread().getName());
279 System.out.print(": ");
283 public static void threadPrintln (String s) {
285 System.out.println();
288 public static void print (String s) {
292 public static void println (String s) {
293 System.out.println(s);
296 public static void print (String s, int i) {
297 System.out.print(s + " : " + i);
300 public static void print (String s, boolean b) {
301 System.out.print(s + " : " + b);
304 public static void println() {
305 System.out.println();
309 * this is to avoid StringBuilders
311 public static void print (String... args){
312 for (String s : args){
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
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; }
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]; }
332 public static void setLocalAttribute (String varName, int val) {}
333 public static int getLocalAttribute (String varName) { return 0; }
335 public static void addLocalAttribute (String varName, int val) {}
336 public static int[] getLocalAttributes (String varName) { return new int[0]; }
338 public static void setElementAttribute (Object arr, int idx, int val){}
339 public static int getElementAttribute (Object arr, int idx) { return 0; }
341 public static void addElementAttribute (Object arr, int idx, int val){}
342 public static int[] getElementAttributes (Object arr, int idx) { return new int[0]; }
344 public static void setObjectAttribute (Object o, int val) {}
345 public static int getObjectAttribute (Object o) { return 0; }
347 public static void addObjectAttribute (Object o, int val) {}
348 public static int[] getObjectAttributes (Object o) { return new int[0]; }
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")
356 public static boolean getBoolean () {
357 // just executed when not running inside JPF, native otherwise
358 return ((System.currentTimeMillis() & 1) != 0);
362 * new boolean choice generator that also tells jpf which value to
363 * use first by default in a search.
365 public static boolean getBoolean (boolean falseFirst) {
366 // this is only executed when not running JPF
372 * Returns int nondeterministically between (and including) min and max.
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;
379 public static int getIntFromList (int... values){
380 if (values != null && values.length > 0) {
381 int i = getRandom().nextInt(values.length);
384 return getRandom().nextInt();
388 public static Object getObject (String key) {
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
397 public static int getInt (String key){
398 // this is only executed when not running JPF, native otherwise
399 return getRandom().nextInt();
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
407 public static double getDouble (String key){
408 // this is only executed when not running JPF, native otherwise
409 return getRandom().nextDouble();
412 public static double getDoubleFromList (double... values){
413 if (values != null && values.length > 0) {
414 int i = getRandom().nextInt(values.length);
417 return getRandom().nextDouble();
421 public static long getLongFromList (long...values){
422 if (values != null && values.length > 0) {
423 int i = getRandom().nextInt(values.length);
426 return getRandom().nextLong();
430 public static float getFloatFromList (float...values){
431 if (values != null && values.length > 0) {
432 int i = getRandom().nextInt(values.length);
435 return getRandom().nextFloat();
441 * Returns a random number between 0 and max inclusive.
443 public static int random (int max) {
444 // this is only executed when not running JPF
445 return getRandom().nextInt(max + 1);
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
453 public static boolean randomBool () {
454 // this is only executed when not running JPF
455 return getRandom().nextBoolean();
458 public static long currentTimeMillis () {
459 return System.currentTimeMillis();
462 // Backwards compatibility START
463 public static Object randomObject (String type) {
467 public static boolean isRunningInJPF() {
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,
477 * Vector v = new Vector();
479 * if (Verify.getBoolean()) {
480 * v.addAll(eleventyBillionObjectCollection);
483 * // compare states here
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
493 public static boolean vmIsMatchingStates() {
497 public static void storeTrace (String fileName, String comment) {
498 // intercepted in NativePeer
501 public static void storeTraceIf (boolean cond, String fileName, String comment) {
503 storeTrace(fileName, comment);
507 public static void storeTraceAndTerminate (String fileName, String comment) {
508 storeTrace(fileName, comment);
512 public static void storeTraceAndTerminateIf (boolean cond, String fileName, String comment) {
514 storeTrace(fileName, comment);
519 public static boolean isTraceReplay () {
520 return false; // native
523 public static boolean isShared (Object o){
524 return false; // native
527 public static void setShared (Object o, boolean isShared) {
531 public static void freezeSharedness (Object o, boolean freeze) {
535 public static void terminateSearch () {
539 public static void setHeuristicSearchValue (int n){
540 // native - to control UserHeuristic
543 public static void resetHeuristicSearchValue (){
544 // native - to control UserHeuristic
547 public static int getHeuristicSearchValue (){
548 // native - to control UserHeuristic
552 public static void setProperties (String... p) {
556 public static String getProperty (String key) {
561 public static <T> T createFromJSON(Class<T> clazz, String json){
565 public static void writeObjectToFile(Object object, String fileName) {
567 FileOutputStream fso = new FileOutputStream(fileName);
568 ObjectOutputStream oos = new ObjectOutputStream(fso);
569 oos.writeObject(object);
573 } catch (Exception ex) {
574 throw new RuntimeException(ex);
579 public static <T> T readObjectFromFile(Class<T> clazz, String fileName) {
582 FileInputStream fis = new FileInputStream(fileName);
583 ObjectInputStream ois = new ObjectInputStream(fis);
585 Object read = ois.readObject();
590 catch (Exception ex) {
591 throw new RuntimeException(ex);
597 //--- model logging support
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
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;
610 public static void log( String loggerId, int logLevel, String msg){
611 System.err.println(msg);
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);
619 public static void log( String loggerId, int logLevel, String format, Object... args){
620 System.err.printf(format, args);