KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > jvm > JPF_gov_nasa_jpf_jvm_Verify


1 //
2
// Copyright (C) 2005 United States Government as represented by the
3
// Administrator of the National Aeronautics and Space Administration
4
// (NASA). All Rights Reserved.
5
//
6
// This software is distributed under the NASA Open Source Agreement
7
// (NOSA), version 1.3. The NOSA has been approved by the Open Source
8
// Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9
// directory tree for the complete NOSA document.
10
//
11
// THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12
// KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13
// LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14
// SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15
// A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16
// THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17
// DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18
//
19
package gov.nasa.jpf.jvm;
20
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.JPFException;
23
24 /**
25  * native peer class for programmatic JPF interface (that can be used inside
26  * of apps to verify - if you are aware of the danger that comes with it)
27  */

28 public class JPF_gov_nasa_jpf_jvm_Verify {
29   static final int MAX_COUNTERS = 10;
30   
31   static int[] counter;
32   static boolean supportIgnorePath;
33
34   public static boolean init (Config config) {
35     supportIgnorePath = config.getBoolean("vm.verify.ignore_path");
36     counter = null;
37     
38     Verify.setPeerClass( JPF_gov_nasa_jpf_jvm_Verify.class);
39     
40     return true;
41   }
42   
43   public static final int getCounter (MJIEnv env, int clsObjRef, int counterId) {
44     if ((counter == null) || (counterId < 0) || (counterId >= counter.length)) {
45       return 0;
46     }
47
48     return counter[counterId];
49   }
50
51   public static final void resetCounter (MJIEnv env, int clsObjRef, int counterId) {
52     if ((counter == null) || (counterId < 0) || (counterId >= counter.length)) {
53       return;
54     }
55     counter[counterId] = 0;
56   }
57   
58   public static final int incrementCounter (MJIEnv env, int clsObjRef, int counterId) {
59     if (counterId < 0) {
60       return 0;
61     }
62     
63     if (counter == null) {
64       counter = new int[(counterId >= MAX_COUNTERS) ? counterId+1 : MAX_COUNTERS];
65     } else if (counterId >= counter.length) {
66       int[] newCounter = new int[counterId+1];
67       System.arraycopy(counter, 0, newCounter, 0, counter.length);
68       counter = newCounter;
69     }
70
71     return ++counter[counterId];
72   }
73
74   public static final long currentTimeMillis (MJIEnv env, int clsObjRef) {
75     return System.currentTimeMillis();
76   }
77   
78   public static String JavaDoc getType (int objRef, MJIEnv env) {
79     DynamicArea da = env.getDynamicArea();
80
81     return Types.getTypeName(da.get(objRef).getType());
82   }
83
84   public static void setAnnotation (MJIEnv env, int clsObjRef, int stringRef) {
85     SystemState ss = env.getSystemState();
86     String JavaDoc cmt = env.getStringObject(stringRef);
87     ss.trail().setAnnotation(cmt);
88   }
89
90   public static void assertTrue__Z (MJIEnv env, int clsObjRef, boolean b) {
91     env.getThreadInfo().list.ks.ss.violatedAssertion |= !b;
92   }
93
94   public static void atLabel__I (MJIEnv env, int clsObjRef, int label) {
95     Labels.set(Integer.toString(label), env.getThreadInfo().getPC(-1).getNext());
96   }
97
98   public static void atLabel__Ljava_lang_String_2 (MJIEnv env, int clsObjRef,
99                                                    int stringRef) {
100     String JavaDoc label = env.getStringObject(stringRef);
101     Labels.set(label, env.getThreadInfo().getPC(-1).getNext());
102   }
103
104   public static void beginAtomic (MJIEnv env, int clsObjRef) {
105     env.getThreadInfo().list.ks.setAtomic();
106   }
107
108   public static void busyWait (MJIEnv env, int clsObjRef) {
109     // nothing required here (we systematically explore scheduling
110
// sequences anyway), but we need to intercept the call
111
}
112
113   public static void dumpStack (MJIEnv env, int clsObjRef) {
114     SystemState ss = env.getSystemState();
115     System.out.println("dumping the state");
116     ss.ks.log();
117   }
118
119   public static void endAtomic (MJIEnv env, int clsObjRef) {
120     env.getThreadInfo().list.ks.clearAtomic();
121   }
122
123   public static void ignoreIf (MJIEnv env, int clsObjRef, boolean b) {
124     if (supportIgnorePath) {
125       env.getThreadInfo().list.ks.ss.ignored |= b;
126     }
127   }
128
129   public static void interesting (MJIEnv env, int clsObjRef, boolean b) {
130     env.getThreadInfo().list.ks.ss.interesting |= b;
131   }
132
133   public static boolean isCalledFromClass (MJIEnv env, int clsObjRef,
134                                            int clsNameRef) {
135     String JavaDoc refClassName = env.getStringObject(clsNameRef);
136     ThreadInfo ti = env.getThreadInfo();
137     int stackDepth = ti.countStackFrames();
138
139     if (stackDepth < 2) {
140       return false; // native methods don't have a stackframe
141
}
142     
143     String JavaDoc mthClassName = ti.getCallStackClass(1);
144     ClassInfo ci = ClassInfo.getClassInfo(mthClassName);
145     
146     return ci.instanceOf(refClassName);
147   }
148   
149   ////// <2do> those will be refactored
150
public static final boolean getBoolean (MJIEnv env, int clsObjRef) {
151     JVM vm = env.getVM();
152     
153     ChoiceGenerator gen = vm.getChoiceGenerator();
154     if (gen == null) {
155       gen = vm.createBooleanChoiceGenerator();
156     }
157     if (gen instanceof BooleanChoiceGenerator) {
158       return ((BooleanChoiceGenerator)gen).getNextChoice(vm);
159     } else {
160       // we are in trouble
161
throw new JPFException("wrong ChoiceGenerator type: " + gen + " not boolean");
162     }
163   }
164   
165   public static final int getInt__II (MJIEnv env, int clsObjRef, int min, int max) {
166     JVM vm = env.getVM();
167     
168     ChoiceGenerator gen = vm.getChoiceGenerator();
169     if (gen == null) {
170       gen = vm.createIntChoiceGenerator(min, max);
171     }
172     if (gen instanceof IntChoiceGenerator) {
173       return ((IntChoiceGenerator)gen).getNextChoice(vm);
174     } else {
175       // we are in trouble
176
throw new JPFException("wrong ChoiceGenerator type: " + gen + " not boolean");
177     }
178   }
179   
180   public static final int getInt__Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int idRef) {
181     JVM vm = env.getVM();
182     
183     // there is only one per state, so if we have been here before, we don't
184
// have to qualify which one it is (the id is mainly used whencreating
185
// the beast). That's good, because it means we don't have ti convert
186
// the String all the time
187
ChoiceGenerator gen = vm.getChoiceGenerator();
188     String JavaDoc id = null;
189     
190     if (gen == null) {
191       id = env.getStringObject(idRef);
192       // generate a new ChoiceGenerator object for this state
193
gen = vm.createChoiceGenerator(id);
194     }
195     
196     if (gen instanceof IntChoiceGenerator) {
197       return ((IntChoiceGenerator)gen).getNextChoice(vm);
198     } else {
199       // we are in trouble
200
if (id == null) {
201         id = env.getStringObject(idRef);
202       }
203       throw new JPFException("wrong ChoiceGenerator type: " + gen + " for id: " + id);
204     }
205   }
206   
207   public static final double getDouble (MJIEnv env, int clsObjRef, int idRef) {
208     JVM vm = env.getVM();
209     
210     // there is only one per state, so if we have been here before, we don't
211
// have to qualify which one it is (the id is mainly used when creating
212
// the beast). That's good, because it means we don't have to convert
213
// the String all the time
214
ChoiceGenerator gen = vm.getChoiceGenerator();
215     String JavaDoc id = null;
216     
217     if (gen == null) {
218       id = env.getStringObject(idRef);
219       // generate a new ChoiceGenerator object for this state
220
gen = vm.createChoiceGenerator(id);
221     }
222     
223     if (gen instanceof DoubleChoiceGenerator) {
224       return ((DoubleChoiceGenerator)gen).getNextChoice(vm);
225     } else {
226       // we are in trouble
227
if (id == null) {
228         id = env.getStringObject(idRef);
229       }
230       throw new JPFException("wrong ChoiceGenerator type: " + gen + " for id: " + id);
231     }
232   }
233   
234   /**
235    * <?> pcm - I wonder what this is good for. Returning ANY object of a
236    * given type, regardless of where it is referenced, if it is
237    * synchronized (thread!) and whatever? Looks like it should be called
238    * 'randomError'?
239    * answer: In what sense is this a 'randomError'? Could you please elaborate?
240    * This is used to model the environment of a software component:
241    * some (static) analysis is done to see what objects can be affected by
242    * the environment; the (most general) environment is then modeled as
243    * nondeterministically changing any of these objects; if assumptions are
244    * present, the environment can be restricted.
245    */

246   public static final int randomObject (MJIEnv env, int clsObjRef, int stringRef) {
247     SystemState ss = env.getSystemState();
248     String JavaDoc objType = env.getStringObject(stringRef);
249     DynamicArea da = env.getDynamicArea();
250     int[] map = arrayOfObjectsOfType(da, objType);
251
252     if (map.length == 0) {
253       return -1;
254     } else {
255       return (map[ss.random(map.length)]);
256     }
257   }
258
259
260   public static final boolean randomBool (MJIEnv env, int clsObjRef) {
261     SystemState ss = env.getSystemState();
262
263     return (ss.random(2) != 0);
264   }
265
266   public static final double randomDouble (MJIEnv env, int clsObjRef, int keyRef) {
267     SystemState ss = env.getSystemState();
268     
269     //int id = env.getStateId();
270
int id = ss.getId();
271     String JavaDoc key = env.getStringObject(keyRef);
272
273 System.out.println("randomDouble from: " + key + ", state: " +id);
274     
275     return (double)ss.random(3);
276   }
277   
278   
279   public static final int random (MJIEnv env, int clsObjRef, int x) {
280     SystemState ss = env.getSystemState();
281
282 // int id = JVM.jvm.stateSet.add(ss); // BAD - hash recompute
283
//System.out.println("randomInt from: " + id);
284

285     return ss.random(x + 1);
286   }
287
288   static void boring (MJIEnv env, int clsObjRef, boolean b) {
289     env.getThreadInfo().list.ks.ss.boring |= b;
290   }
291
292   private static int[] arrayOfObjectsOfType (DynamicArea da, String JavaDoc type) {
293     int[] map = new int[0];
294     int map_size = 0;
295
296     for (int i = 0; i < da.elements.length; i++) {
297       if (da.elements[i] != null) {
298         if ((Types.getTypeName(da.elements[i].getType())).equals(type)) {
299           if (map_size >= map.length) {
300             int[] n = new int[map_size + 1];
301             System.arraycopy(map, 0, n, 0, map.length);
302             map = n;
303           }
304
305           map[map_size] = i;
306           map_size++;
307         }
308       }
309     }
310
311     return map;
312   }
313 }
314
Popular Tags