Members/kono/jpf-core: src/main/gov/nasa/jpf/vm/Verify.java comparison

comparison src/main/gov/nasa/jpf/vm/Verify.java @ 0:61d41facf527

initial v8 import (history reset)

author	Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date	Fri, 23 Jan 2015 10:14:01 -0800
parents
children	f6886b2bda4a

comparison

equal deleted inserted replaced

--1:000000000000
+:61d41facf527
+/*
+* Copyright (C) 2014, United States Government, as represented by the
+* Administrator of the National Aeronautics and Space Administration.
+* All rights reserved.
+*
+* The Java Pathfinder core (jpf-core) platform is licensed under the
+* Apache License, Version 2.0 (the "License"); you may not use this file except
+* in compliance with the License. You may obtain a copy of the License at
+*
+*        http://www.apache.org/licenses/LICENSE-2.0.
+*
+* Unless required by applicable law or agreed to in writing, software
+* distributed under the License is distributed on an "AS IS" BASIS,
+* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+* See the License for the specific language governing permissions and
+* limitations under the License.
+*/
+package gov.nasa.jpf.vm;
+import java.io.FileInputStream;
+import java.io.FileOutputStream;
+import java.io.ObjectInputStream;
+import java.io.ObjectOutputStream;
+import java.util.BitSet;
+import java.util.Random;
+/**
+* Verify is the programmatic interface of JPF that can be used from inside of
+* applications. In order to enable programs to run outside of the JPF
+* environment, we provide (mostly empty) bodies for the methods that are
+* otherwise intercepted by the native peer class
+*/
+public class Verify {
+static final int MAX_COUNTERS = 10;
+static int[] counter;  // only here so that we don't pull in all JPF classes at RT
+private static Random random;
+/*
+* only set if this was used from within a JPF context. This is mainly to
+* enable encapsulation of JPF specific types so that they only get
+* pulled in on demand, and we otherwise can still use the same Verify class
+* for JPF-external execution. We use a class object to make sure it doesn't
+* get recycled once JPF is terminated.
+*/
+static Class<?> peer;
+private static Random getRandom() {
+if (random == null) {
+random = new Random(42);
+}
+return random;
+}
+/*
+* register the peer class, which is only done from within a JPF execution
+* context. Be aware of that this migh actually load the real Verify class.
+* The sequence usually is
+*   JPF(Verify) -> VM(JPF_gov_nasa_jpf_vm_Verify) -> VM(Verify)
+*/
+public static void setPeerClass (Class<?> cls) {
+peer = cls;
+}
+// note this is NOT marked native because we might also call it from host VM code
+// (beware that Verify is a different class there!). When executed by JPF,
+// this is an MJI method
+public static int getCounter (int id) {
+if (peer != null) {
+// this is executed if we are in a JPF context
+return JPF_gov_nasa_jpf_vm_Verify.getCounter__I__I(null, 0, id);
+} else {
+if (counter == null) {
+counter = new int[id >= MAX_COUNTERS ? (id+1) : MAX_COUNTERS];
+}
+if ((id < 0) || (id >= counter.length)) {
+return 0;
+}
+return counter[id];
+}
+}
+public static void resetCounter (int id) {
+if (peer != null){
+JPF_gov_nasa_jpf_vm_Verify.resetCounter__I__V(null, 0, id);
+} else {
+if ((counter != null) && (id >= 0) && (id < counter.length)) {
+counter[id] = 0;
+}
+}
+}
+public static void setCounter (int id, int val) {
+if (peer != null){
+JPF_gov_nasa_jpf_vm_Verify.setCounter__II__V(null, 0, id, val);
+} else {
+if ((counter != null) && (id >= 0) && (id < counter.length)) {
+counter[id] = val;
+}
+}
+}
+public static int incrementCounter (int id) {
+if (peer != null){
+return JPF_gov_nasa_jpf_vm_Verify.incrementCounter__I__I(null, 0, id);
+} else {
+if (counter == null) {
+counter = new int[(id >= MAX_COUNTERS) ? id+1 : MAX_COUNTERS];
+} else if (id >= counter.length) {
+int[] newCounter = new int[id+1];
+System.arraycopy(counter, 0, newCounter, 0, counter.length);
+counter = newCounter;
+}
+if ((id >= 0) && (id < counter.length)) {
+return ++counter[id];
+}
+return 0;
+}
+}
+public static final int NO_VALUE = -1;
+public static void putValue (String key, int value) {
+throw new UnsupportedOperationException("putValue requires JPF execution");
+}
+public static int getValue (String key) {
+throw new UnsupportedOperationException("getValue requires JPF execution");
+}
+// same mechanism and purpose as the counters, but with BitSets, which is
+// more convenient if we have a lot of different events to check
+static BitSet[] bitSets;
+private static void checkBitSetId(int id) {
+if (bitSets == null) {
+bitSets = new BitSet[id + 1];
+} else if (id >= bitSets.length) {
+BitSet[] newBitSets = new BitSet[id + 1];
+System.arraycopy(bitSets, 0, newBitSets, 0, bitSets.length);
+bitSets = newBitSets;
+}
+if (bitSets[id] == null) {
+bitSets[id] = new BitSet();
+}
+}
+public static void setBitInBitSet(int id, int bit, boolean value) {
+if (peer != null){
+// this is executed if we did run JPF
+JPF_gov_nasa_jpf_vm_Verify.setBitInBitSet__IIZ__V(null, 0, id, bit, value);
+} else {
+// this is executed if we run this without previously executing JPF
+checkBitSetId(id);
+bitSets[id].set(bit, value);
+}
+}
+public static boolean getBitInBitSet(int id, int bit) {
+if (peer != null){
+// this is executed if we did run JPF
+return JPF_gov_nasa_jpf_vm_Verify.getBitInBitSet__II__Z(null, 0, id, bit);
+} else {
+// this is executed if we run this without previously executing JPF
+checkBitSetId(id);
+return bitSets[id].get(bit);
+}
+}
+/**
+* Adds a comment to the error trace, which will be printed and saved.
+*/
+public static void addComment (String s) {}
+/**
+* Backwards compatibility START
+* @deprecated use "assert cond : msg"
+*/
+@Deprecated
+public static void assertTrue (String s, boolean cond) {
+if (!cond) {
+System.out.println(s);
+assertTrue(cond);
+}
+}
+/**
+* Checks that the condition is true.
+* @deprecated use 'assert' directly
+*/
+@Deprecated
+public static void assertTrue (boolean cond) {
+if (!cond) {
+throw new AssertionError("Verify.assertTrue failed");
+}
+}
+public static void atLabel (String label) {}
+public static void atLabel (int label) {}
+/**
+* Marks the beginning of an atomic block.
+* THIS IS EVIL, DON'T USE IT FOR OPTIMIZATION - THAT'S WHAT POR IS FOR!
+* (it's mostly here to support model classes that need to execute atomic)
+*/
+public static void beginAtomic () {}
+/**
+* Marks the end of an atomic block.
+* EVIL - see beginAtomic()
+*/
+public static void endAtomic () {}
+public static void boring (boolean cond) {}
+public static void busyWait (long duration) {
+// this gets only executed outside of JPF
+while (duration > 0) {
+duration--;
+}
+}
+public static boolean isCalledFromClass (String refClsName) {
+Throwable t = new Throwable();
+StackTraceElement[] st = t.getStackTrace();
+if (st.length < 3) {
+// main() or run()
+return false;
+}
+try {
+Class<?> refClazz = Class.forName(refClsName);
+Class<?> callClazz = Class.forName(st[2].getClassName());
+return (refClazz.isAssignableFrom(callClazz));
+} catch (ClassNotFoundException cfnx) {
+return false;
+}
+}
+public static void ignoreIf (boolean cond) {}
+public static void instrumentPoint (String label) {}
+public static void instrumentPointDeep (String label) {}
+public static void instrumentPointDeepRecur (String label, int depth) {}
+public static void interesting (boolean cond) {}
+public static void breakTransition (String reason) {}
+/**
+* simple debugging aids to imperatively print the current path output of the SUT
+* (to be used with vm.path_output)
+*/
+public static void printPathOutput(String msg) {}
+public static void printPathOutput(boolean cond, String msg) {}
+public static void threadPrint (String s) {
+System.out.print( Thread.currentThread().getName());
+System.out.print(": ");
+System.out.print(s);
+}
+public static void threadPrintln (String s) {
+threadPrint(s);
+System.out.println();
+}
+public static void print (String s) {
+System.out.print(s);
+}
+public static void println (String s) {
+System.out.println(s);
+}
+public static void print (String s, int i) {
+System.out.print(s + " : " + i);
+}
+public static void print (String s, boolean b) {
+System.out.print(s + " : " + b);
+}
+public static void println() {
+System.out.println();
+}
+/**
+* this is to avoid StringBuilders
+*/
+public static void print (String... args){
+for (String s : args){
+System.out.print(s);
+}
+}
+/**
+* note - these are mostly for debugging purposes (to see if attributes get
+* propagated correctly, w/o having to write a listener), since attributes are
+* supposed to be created at the native side, and hence can't be accessed from
+* the application
+*/
+//--- use these if you know there are single attributes
+public static void setFieldAttribute (Object o, String fieldName, int val) {}
+public static int getFieldAttribute (Object o, String fieldName) { return 0; }
+//--- use these for multiple attributes
+public static void addFieldAttribute (Object o, String fieldName, int val) {}
+public static int[] getFieldAttributes (Object o, String fieldName) { return new int[0]; }
+public static void setLocalAttribute (String varName, int val) {}
+public static int getLocalAttribute (String varName) { return 0; }
+public static void addLocalAttribute (String varName, int val) {}
+public static int[] getLocalAttributes (String varName) { return new int[0]; }
+public static void setElementAttribute (Object arr, int idx, int val){}
+public static int getElementAttribute (Object arr, int idx) { return 0; }
+public static void addElementAttribute (Object arr, int idx, int val){}
+public static int[] getElementAttributes (Object arr, int idx) { return new int[0]; }
+public static void setObjectAttribute (Object o, int val) {}
+public static int getObjectAttribute (Object o) { return 0; }
+public static void addObjectAttribute (Object o, int val) {}
+public static int[] getObjectAttributes (Object o) { return new int[0]; }
+/**
+* this is the new boolean choice generator. Since there's no real
+* heuristic involved with boolean values, we skip the id (it's a
+* hardwired "boolean")
+*/
+public static boolean getBoolean () {
+// just executed when not running inside JPF, native otherwise
+return ((System.currentTimeMillis() & 1) != 0);
+}
+/**
+* new boolean choice generator that also tells jpf which value to
+* use first by default in a search.
+*/
+public static boolean getBoolean (boolean falseFirst) {
+// this is only executed when not running JPF
+return getBoolean();
+}
+/**
+* Returns int nondeterministically between (and including) min and max.
+*/
+public static int getInt (int min, int max) {
+// this is only executed when not running JPF, native otherwise
+return getRandom().nextInt((max-min+1)) + min;
+}
+public static int getIntFromList (int... values){
+if (values != null && values.length > 0) {
+int i = getRandom().nextInt(values.length);
+return values[i];
+} else {
+return getRandom().nextInt();
+}
+}
+public static Object getObject (String key) {
+return "?";
+}
+/**
+* this is the API for int value choice generators. 'id' is used to identify
+* both the corresponding ChoiceGenerator subclass, and the application specific
+* ctor parameters from the normal JPF configuration mechanism
+*/
+public static int getInt (String key){
+// this is only executed when not running JPF, native otherwise
+return getRandom().nextInt();
+}
+/**
+* this is the API for double value choice generators. 'id' is used to identify
+* both the corresponding ChoiceGenerator subclass, and the application specific
+* ctor parameters from the normal JPF configuration mechanism
+*/
+public static double getDouble (String key){
+// this is only executed when not running JPF, native otherwise
+return getRandom().nextDouble();
+}
+public static double getDoubleFromList (double... values){
+if (values != null && values.length > 0) {
+int i = getRandom().nextInt(values.length);
+return values[i];
+} else {
+return getRandom().nextDouble();
+}
+}
+public static long getLongFromList (long...values){
+if (values != null && values.length > 0) {
+int i = getRandom().nextInt(values.length);
+return values[i];
+} else {
+return getRandom().nextLong();
+}
+}
+public static float getFloatFromList (float...values){
+if (values != null && values.length > 0) {
+int i = getRandom().nextInt(values.length);
+return values[i];
+} else {
+return getRandom().nextFloat();
+}
+}
+/**
+* Returns a random number between 0 and max inclusive.
+*/
+public static int random (int max) {
+// this is only executed when not running JPF
+return getRandom().nextInt(max + 1);
+}
+/**
+* Returns a random boolean value, true or false. Note this gets
+* handled by the native peer, and is just here to enable running
+* instrumented applications w/o JPF
+*/
+public static boolean randomBool () {
+// this is only executed when not running JPF
+return getRandom().nextBoolean();
+}
+public static long currentTimeMillis () {
+return System.currentTimeMillis();
+}
+// Backwards compatibility START
+public static Object randomObject (String type) {
+return null;
+}
+public static boolean isRunningInJPF() {
+return false;
+}
+/**
+* USE CAREFULLY - returns true if the virtual machine this code is
+* running under is doing state matching.  This can be used as a hint
+* as to whether data structures (that are known to be correct!)
+* should be configured to use a canonical representation.  For example,
+* <pre><code>
+* Vector v = new Vector();
+* v.add(obj1);
+* if (Verify.getBoolean()) {
+*     v.addAll(eleventyBillionObjectCollection);
+*     v.setSize(1);
+* }
+* // compare states here
+* </code></pre>
+* To the programmer, the states are (almost certainly) the same.  To
+* the VM, they could be different (capacity inside the Vector).  For
+* the sake of speed, Vector does not store things canonically, but this
+* can cause (probably mild) state explosion if matching states.  If
+* you know whether states are being matched, you can choose the right
+* structure--as long as those structures aren't what you're looking for
+* bugs in!
+*/
+public static boolean vmIsMatchingStates() {
+return false;
+}
+public static void storeTrace (String fileName, String comment) {
+// intercepted in NativePeer
+}
+public static void storeTraceIf (boolean cond, String fileName, String comment) {
+if (cond) {
+storeTrace(fileName, comment);
+}
+}
+public static void storeTraceAndTerminate (String fileName, String comment) {
+storeTrace(fileName, comment);
+terminateSearch();
+}
+public static void storeTraceAndTerminateIf (boolean cond, String fileName, String comment) {
+if (cond) {
+storeTrace(fileName, comment);
+terminateSearch();
+}
+}
+public static boolean isTraceReplay () {
+return false; // native
+}
+public static boolean isShared (Object o){
+return false; // native
+}
+public static void setShared (Object o, boolean isShared) {
+// native
+}
+public static void freezeSharedness (Object o, boolean freeze) {
+// native
+}
+public static void terminateSearch () {
+// native
+}
+public static void setProperties (String... p) {
+// native
+}
+public static String getProperty (String key) {
+// native
+return null;
+}
+public static <T> T createFromJSON(Class<T> clazz, String json){
+return null;
+}
+public static void writeObjectToFile(Object object, String fileName) {
+try {
+FileOutputStream fso = new FileOutputStream(fileName);
+ObjectOutputStream oos = new ObjectOutputStream(fso);
+oos.writeObject(object);
+oos.flush();
+oos.close();
+} catch (Exception ex) {
+throw new RuntimeException(ex);
+}
+}
+public static <T> T readObjectFromFile(Class<T> clazz, String fileName) {
+try
+{
+FileInputStream fis = new FileInputStream(fileName);
+ObjectInputStream ois = new ObjectInputStream(fis);
+Object read = ois.readObject();
+return (T) read;
+}
+catch (Exception ex) {
+throw new RuntimeException(ex);
+}
+}
+//--- model logging support
+/*
+* we add these here so that we don't need to pull in any java.util.logging classes
+* Note - these need to be kept in sync with our native peer
+*/
+public static final int SEVERE = 1;
+public static final int WARNING = 2;
+public static final int INFO = 3;
+public static final int FINE = 4;
+public static final int FINER = 5;
+public static final int FINEST = 6;
+public static void log( String loggerId, int logLevel, String msg){
+System.err.println(msg);
+}
+// to avoid construction of strings on the model side
+public static void log( String loggerId, int logLevel, String msg, String arg){
+System.err.println(msg);
+}
+public static void log( String loggerId, int logLevel, String format, Object... args){
+System.err.printf(format, args);
+}
+}

Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/vm/Verify.java @ 0:61d41facf527