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 gov.nasa.jpf.Config;
022: import gov.nasa.jpf.JPFException;
023:
024: /**
025: * native peer class for programmatic JPF interface (that can be used inside
026: * of apps to verify - if you are aware of the danger that comes with it)
027: */
028: public class JPF_gov_nasa_jpf_jvm_Verify {
029: static final int MAX_COUNTERS = 10;
030:
031: static int[] counter;
032: static boolean supportIgnorePath;
033:
034: public static boolean init(Config config) {
035: supportIgnorePath = config.getBoolean("vm.verify.ignore_path");
036: counter = null;
037:
038: Verify.setPeerClass(JPF_gov_nasa_jpf_jvm_Verify.class);
039:
040: return true;
041: }
042:
043: public static final int getCounter(MJIEnv env, int clsObjRef,
044: int counterId) {
045: if ((counter == null) || (counterId < 0)
046: || (counterId >= counter.length)) {
047: return 0;
048: }
049:
050: return counter[counterId];
051: }
052:
053: public static final void resetCounter(MJIEnv env, int clsObjRef,
054: int counterId) {
055: if ((counter == null) || (counterId < 0)
056: || (counterId >= counter.length)) {
057: return;
058: }
059: counter[counterId] = 0;
060: }
061:
062: public static final int incrementCounter(MJIEnv env, int clsObjRef,
063: int counterId) {
064: if (counterId < 0) {
065: return 0;
066: }
067:
068: if (counter == null) {
069: counter = new int[(counterId >= MAX_COUNTERS) ? counterId + 1
070: : MAX_COUNTERS];
071: } else if (counterId >= counter.length) {
072: int[] newCounter = new int[counterId + 1];
073: System.arraycopy(counter, 0, newCounter, 0, counter.length);
074: counter = newCounter;
075: }
076:
077: return ++counter[counterId];
078: }
079:
080: public static final long currentTimeMillis(MJIEnv env, int clsObjRef) {
081: return System.currentTimeMillis();
082: }
083:
084: public static String getType(int objRef, MJIEnv env) {
085: DynamicArea da = env.getDynamicArea();
086:
087: return Types.getTypeName(da.get(objRef).getType());
088: }
089:
090: public static void setAnnotation(MJIEnv env, int clsObjRef,
091: int stringRef) {
092: SystemState ss = env.getSystemState();
093: String cmt = env.getStringObject(stringRef);
094: ss.trail().setAnnotation(cmt);
095: }
096:
097: public static void assertTrue__Z(MJIEnv env, int clsObjRef,
098: boolean b) {
099: env.getThreadInfo().list.ks.ss.violatedAssertion |= !b;
100: }
101:
102: public static void atLabel__I(MJIEnv env, int clsObjRef, int label) {
103: Labels.set(Integer.toString(label), env.getThreadInfo().getPC(
104: -1).getNext());
105: }
106:
107: public static void atLabel__Ljava_lang_String_2(MJIEnv env,
108: int clsObjRef, int stringRef) {
109: String label = env.getStringObject(stringRef);
110: Labels.set(label, env.getThreadInfo().getPC(-1).getNext());
111: }
112:
113: public static void beginAtomic(MJIEnv env, int clsObjRef) {
114: env.getThreadInfo().list.ks.setAtomic();
115: }
116:
117: public static void busyWait(MJIEnv env, int clsObjRef) {
118: // nothing required here (we systematically explore scheduling
119: // sequences anyway), but we need to intercept the call
120: }
121:
122: public static void dumpStack(MJIEnv env, int clsObjRef) {
123: SystemState ss = env.getSystemState();
124: System.out.println("dumping the state");
125: ss.ks.log();
126: }
127:
128: public static void endAtomic(MJIEnv env, int clsObjRef) {
129: env.getThreadInfo().list.ks.clearAtomic();
130: }
131:
132: public static void ignoreIf(MJIEnv env, int clsObjRef, boolean b) {
133: if (supportIgnorePath) {
134: env.getThreadInfo().list.ks.ss.ignored |= b;
135: }
136: }
137:
138: public static void interesting(MJIEnv env, int clsObjRef, boolean b) {
139: env.getThreadInfo().list.ks.ss.interesting |= b;
140: }
141:
142: public static boolean isCalledFromClass(MJIEnv env, int clsObjRef,
143: int clsNameRef) {
144: String refClassName = env.getStringObject(clsNameRef);
145: ThreadInfo ti = env.getThreadInfo();
146: int stackDepth = ti.countStackFrames();
147:
148: if (stackDepth < 2) {
149: return false; // native methods don't have a stackframe
150: }
151:
152: String mthClassName = ti.getCallStackClass(1);
153: ClassInfo ci = ClassInfo.getClassInfo(mthClassName);
154:
155: return ci.instanceOf(refClassName);
156: }
157:
158: ////// <2do> those will be refactored
159: public static final boolean getBoolean(MJIEnv env, int clsObjRef) {
160: JVM vm = env.getVM();
161:
162: ChoiceGenerator gen = vm.getChoiceGenerator();
163: if (gen == null) {
164: gen = vm.createBooleanChoiceGenerator();
165: }
166: if (gen instanceof BooleanChoiceGenerator) {
167: return ((BooleanChoiceGenerator) gen).getNextChoice(vm);
168: } else {
169: // we are in trouble
170: throw new JPFException("wrong ChoiceGenerator type: " + gen
171: + " not boolean");
172: }
173: }
174:
175: public static final int getInt__II(MJIEnv env, int clsObjRef,
176: int min, int max) {
177: JVM vm = env.getVM();
178:
179: ChoiceGenerator gen = vm.getChoiceGenerator();
180: if (gen == null) {
181: gen = vm.createIntChoiceGenerator(min, max);
182: }
183: if (gen instanceof IntChoiceGenerator) {
184: return ((IntChoiceGenerator) gen).getNextChoice(vm);
185: } else {
186: // we are in trouble
187: throw new JPFException("wrong ChoiceGenerator type: " + gen
188: + " not boolean");
189: }
190: }
191:
192: public static final int getInt__Ljava_lang_String_2(MJIEnv env,
193: int clsObjRef, int idRef) {
194: JVM vm = env.getVM();
195:
196: // there is only one per state, so if we have been here before, we don't
197: // have to qualify which one it is (the id is mainly used whencreating
198: // the beast). That's good, because it means we don't have ti convert
199: // the String all the time
200: ChoiceGenerator gen = vm.getChoiceGenerator();
201: String id = null;
202:
203: if (gen == null) {
204: id = env.getStringObject(idRef);
205: // generate a new ChoiceGenerator object for this state
206: gen = vm.createChoiceGenerator(id);
207: }
208:
209: if (gen instanceof IntChoiceGenerator) {
210: return ((IntChoiceGenerator) gen).getNextChoice(vm);
211: } else {
212: // we are in trouble
213: if (id == null) {
214: id = env.getStringObject(idRef);
215: }
216: throw new JPFException("wrong ChoiceGenerator type: " + gen
217: + " for id: " + id);
218: }
219: }
220:
221: public static final double getDouble(MJIEnv env, int clsObjRef,
222: int idRef) {
223: JVM vm = env.getVM();
224:
225: // there is only one per state, so if we have been here before, we don't
226: // have to qualify which one it is (the id is mainly used when creating
227: // the beast). That's good, because it means we don't have to convert
228: // the String all the time
229: ChoiceGenerator gen = vm.getChoiceGenerator();
230: String id = null;
231:
232: if (gen == null) {
233: id = env.getStringObject(idRef);
234: // generate a new ChoiceGenerator object for this state
235: gen = vm.createChoiceGenerator(id);
236: }
237:
238: if (gen instanceof DoubleChoiceGenerator) {
239: return ((DoubleChoiceGenerator) gen).getNextChoice(vm);
240: } else {
241: // we are in trouble
242: if (id == null) {
243: id = env.getStringObject(idRef);
244: }
245: throw new JPFException("wrong ChoiceGenerator type: " + gen
246: + " for id: " + id);
247: }
248: }
249:
250: /**
251: * <?> pcm - I wonder what this is good for. Returning ANY object of a
252: * given type, regardless of where it is referenced, if it is
253: * synchronized (thread!) and whatever? Looks like it should be called
254: * 'randomError'?
255: * answer: In what sense is this a 'randomError'? Could you please elaborate?
256: * This is used to model the environment of a software component:
257: * some (static) analysis is done to see what objects can be affected by
258: * the environment; the (most general) environment is then modeled as
259: * nondeterministically changing any of these objects; if assumptions are
260: * present, the environment can be restricted.
261: */
262: public static final int randomObject(MJIEnv env, int clsObjRef,
263: int stringRef) {
264: SystemState ss = env.getSystemState();
265: String objType = env.getStringObject(stringRef);
266: DynamicArea da = env.getDynamicArea();
267: int[] map = arrayOfObjectsOfType(da, objType);
268:
269: if (map.length == 0) {
270: return -1;
271: } else {
272: return (map[ss.random(map.length)]);
273: }
274: }
275:
276: public static final boolean randomBool(MJIEnv env, int clsObjRef) {
277: SystemState ss = env.getSystemState();
278:
279: return (ss.random(2) != 0);
280: }
281:
282: public static final double randomDouble(MJIEnv env, int clsObjRef,
283: int keyRef) {
284: SystemState ss = env.getSystemState();
285:
286: //int id = env.getStateId();
287: int id = ss.getId();
288: String key = env.getStringObject(keyRef);
289:
290: System.out.println("randomDouble from: " + key + ", state: "
291: + id);
292:
293: return (double) ss.random(3);
294: }
295:
296: public static final int random(MJIEnv env, int clsObjRef, int x) {
297: SystemState ss = env.getSystemState();
298:
299: // int id = JVM.jvm.stateSet.add(ss); // BAD - hash recompute
300: //System.out.println("randomInt from: " + id);
301:
302: return ss.random(x + 1);
303: }
304:
305: static void boring(MJIEnv env, int clsObjRef, boolean b) {
306: env.getThreadInfo().list.ks.ss.boring |= b;
307: }
308:
309: private static int[] arrayOfObjectsOfType(DynamicArea da,
310: String type) {
311: int[] map = new int[0];
312: int map_size = 0;
313:
314: for (int i = 0; i < da.elements.length; i++) {
315: if (da.elements[i] != null) {
316: if ((Types.getTypeName(da.elements[i].getType()))
317: .equals(type)) {
318: if (map_size >= map.length) {
319: int[] n = new int[map_size + 1];
320: System.arraycopy(map, 0, n, 0, map.length);
321: map = n;
322: }
323:
324: map[map_size] = i;
325: map_size++;
326: }
327: }
328: }
329:
330: return map;
331: }
332: }
|