001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.jvm;
020:
021: import java.util.Random;
022:
023: /**
024: * Verify is the programmatic interface of JPF that can be used from inside of
025: * applications. In order to enable programs to run outside of the JPF
026: * environment, we provide (mostly empty) bodies for the methods that are
027: * otherwise intercepted by the native peer class
028: */
029: public class Verify {
030: static final int MAX_COUNTERS = 10;
031: static int[] counter; // only here so that we don't pull in all JPF classes at RT
032:
033: private static Random random;
034:
035: /*
036: * only set if this was used from within a JPF context. This is mainly to
037: * enable encapsulation of JPF specific types so that they only get
038: * pulled in on demand, and we otherwise can still use the same Verify class
039: * for JPF-external execution. We use a class object to make sure it doesn't
040: * get recycled once JPF is terminated.
041: */
042: static Class peer;
043:
044: /*
045: * register the peer class, which is only done from within a JPF execution
046: * context. Be aware of that this migh actually load the real Verify class.
047: * The sequence usually is
048: * JPF(Verify) -> JVM(JPF_gov_nasa_jpf_jvm_Verify) -> JVM(Verify)
049: */
050: public static void setPeerClass(Class cls) {
051: peer = cls;
052: }
053:
054: // note this is NOT marked native because we might also call it from host VM code
055: // (beware that Verify is a different class there!). When executed by JPF,
056: // this is an MJI method
057: public static int getCounter(int id) {
058: if (peer != null) {
059: // this is executed if we are in a JPF context
060: return JPF_gov_nasa_jpf_jvm_Verify.getCounter(null, 0, id);
061: } else {
062: if (counter == null) {
063: counter = new int[id >= MAX_COUNTERS ? (id + 1)
064: : MAX_COUNTERS];
065: }
066: if ((id < 0) || (id >= counter.length)) {
067: return 0;
068: }
069:
070: return counter[id];
071: }
072: }
073:
074: public static void resetCounter(int id) {
075: if (peer != null) {
076: JPF_gov_nasa_jpf_jvm_Verify.resetCounter(null, 0, id);
077: } else {
078: if ((counter != null) && (id >= 0) && (id < counter.length)) {
079: counter[id] = 0;
080: }
081: }
082: }
083:
084: public static int incrementCounter(int id) {
085: if (peer != null) {
086: return JPF_gov_nasa_jpf_jvm_Verify.incrementCounter(null,
087: 0, id);
088: } else {
089: if (counter == null) {
090: counter = new int[(id >= MAX_COUNTERS) ? id + 1
091: : MAX_COUNTERS];
092: } else if (id >= counter.length) {
093: int[] newCounter = new int[id + 1];
094: System.arraycopy(counter, 0, newCounter, 0,
095: counter.length);
096: counter = newCounter;
097: }
098:
099: if ((id >= 0) && (id < counter.length)) {
100: return ++counter[id];
101: }
102:
103: return 0;
104: }
105: }
106:
107: // Backwards compatibility END
108:
109: /**
110: * Adds a comment to the error trace, which will be printed and saved.
111: */
112: public static void addComment(String s) {
113: }
114:
115: /*
116: * Backwards compatibility START
117: * @deprecated use "assert cond : msg"
118: */
119: public static void assertTrue(String s, boolean cond) {
120: if (!cond) {
121: System.out.println(s);
122: assertTrue(cond);
123: }
124: }
125:
126: /**
127: * Checks that the condition is true.
128: * @deprecated use 'assert' directly
129: */
130: public static void assertTrue(boolean cond) {
131: if (!cond) {
132: throw new AssertionError("Verify.assertTrue failed");
133: }
134: }
135:
136: public static void atLabel(String label) {
137: }
138:
139: public static void atLabel(int label) {
140: }
141:
142: /**
143: * Marks the beginning of an atomic block.
144: */
145: public static void beginAtomic() {
146: }
147:
148: /**
149: * Marks the end of an atomic block.
150: */
151: public static void endAtomic() {
152: }
153:
154: public static void boring(boolean cond) {
155: }
156:
157: public static void busyWait(long duration) {
158: // this gets only executed outside of JPF
159: while (duration > 0) {
160: duration--;
161: }
162: }
163:
164: public static boolean isCalledFromClass(String refClsName) {
165: Throwable t = new Throwable();
166: StackTraceElement[] st = t.getStackTrace();
167:
168: if (st.length < 3) {
169: // main() or run()
170: return false;
171: }
172:
173: try {
174: Class refClazz = Class.forName(refClsName);
175: Class callClazz = Class.forName(st[2].getClassName());
176:
177: return (refClazz.isAssignableFrom(callClazz));
178:
179: } catch (ClassNotFoundException cfnx) {
180: return false;
181: }
182: }
183:
184: public static void dumpState() {
185: }
186:
187: public static void ignoreIf(boolean cond) {
188: }
189:
190: public static void instrumentPoint(String label) {
191: }
192:
193: public static void instrumentPointDeep(String label) {
194: }
195:
196: public static void instrumentPointDeepRecur(String label, int depth) {
197: }
198:
199: public static void interesting(boolean cond) {
200: }
201:
202: public static void print(String s) {
203: System.out.println(s);
204: }
205:
206: public static void print(String s, int i) {
207: System.out.println(s + " : " + i);
208: }
209:
210: public static void print(String s, boolean b) {
211: System.out.println(s + " : " + b);
212: }
213:
214: /**
215: * this is the new boolean choice generator. Since there's no real
216: * heuristic involved with boolean values, we skip the id (it's a
217: * hardwired "boolean")
218: */
219: public static boolean getBoolean() {
220: // just executed when not running inside JPF, native otherwise
221: return ((System.currentTimeMillis() & 1) != 0);
222: }
223:
224: public static int getInt(int min, int max) {
225: // this is only executed when not running JPF, native otherwise
226: if (random == null) {
227: random = new Random();
228: }
229:
230: return random.nextInt((max - min + 1)) + min;
231: }
232:
233: /**
234: * this is the API for int value choice generators. 'id' is used to identify
235: * both the corresponding ChoiceGenerator subclass, and the application specific
236: * ctor parameters from the normal JPF configuration mechanism
237: */
238: public static int getInt(String key) {
239: // this is only executed when not running JPF, native otherwise
240: if (random == null) {
241: random = new Random();
242: }
243: return random.nextInt();
244: }
245:
246: /**
247: * this is the API for double value choice generators. 'id' is used to identify
248: * both the corresponding ChoiceGenerator subclass, and the application specific
249: * ctor parameters from the normal JPF configuration mechanism
250: */
251: public static double getDouble(String key) {
252: // this is only executed when not running JPF, native otherwise
253: if (random == null) {
254: random = new Random();
255: }
256: return random.nextDouble();
257: }
258:
259: /**
260: * Returns a random number between 0 and max inclusive.
261: */
262: public static int random(int max) {
263: // this is only executed when not running JPF
264: if (random == null) {
265: random = new Random();
266: }
267: return random.nextInt(max + 1);
268: }
269:
270: /**
271: * Returns a random boolean value, true or false. Note this gets
272: * handled by the native peer, and is just here to enable running
273: * instrumented applications w/o JPF
274: */
275: public static boolean randomBool() {
276: // this is only executed when not running JPF
277: if (random == null) {
278: random = new Random();
279: }
280: return random.nextBoolean();
281: }
282:
283: public long currentTimeMillis() {
284: return System.currentTimeMillis();
285: }
286:
287: // Backwards compatibility START
288: public static Object randomObject(String type) {
289: return null;
290: }
291:
292: }
|