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   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        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   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   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   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   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   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        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   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   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
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags