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 java.util.Random  ;
22  
23  
24  /**
25   * Verify is the programmatic interface of JPF that can be used from inside of
26   * applications. In order to enable programs to run outside of the JPF
27   * environment, we provide (mostly empty) bodies for the methods that are
28   * otherwise intercepted by the native peer class
29   */
30  public class Verify {
31    static final int MAX_COUNTERS = 10;
32    static int[] counter;  // only here so that we don't pull in all JPF classes at RT
33    
34    private static Random   random;
35  
36    /*
37     * only set if this was used from within a JPF context. This is mainly to
38     * enable encapsulation of JPF specific types so that they only get
39     * pulled in on demand, and we otherwise can still use the same Verify class
40     * for JPF-external execution. We use a class object to make sure it doesn't
41     * get recycled once JPF is terminated.
42     */
43    static Class   peer;
44    
45    /*
46     * register the peer class, which is only done from within a JPF execution
47     * context. Be aware of that this migh actually load the real Verify class.
48     * The sequence usually is
49     *   JPF(Verify) -> JVM(JPF_gov_nasa_jpf_jvm_Verify) -> JVM(Verify)
50     */
51    public static void setPeerClass (Class   cls) {
52      peer = cls;
53    }
54    
55    // note this is NOT marked native because we might also call it from host VM code
56    // (beware that Verify is a different class there!). When executed by JPF,
57    // this is an MJI method
58    public static int getCounter (int id) {
59      if (peer != null) {
60        // this is executed if we are in a JPF context
61        return JPF_gov_nasa_jpf_jvm_Verify.getCounter(null, 0, id);
62      } else {
63        if (counter == null) {
64          counter = new int[id >= MAX_COUNTERS ? (id+1) : MAX_COUNTERS];
65        }
66        if ((id < 0) || (id >= counter.length)) {
67          return 0;
68        }
69  
70        return counter[id];
71      }
72    }
73  
74    public static void resetCounter (int id) {
75      if (peer != null){
76        JPF_gov_nasa_jpf_jvm_Verify.resetCounter(null, 0, id);
77      } else {
78        if ((counter != null) && (id >= 0) && (id < counter.length)) {
79          counter[id] = 0;
80        }
81      }
82    }
83  
84    public static int incrementCounter (int id) {
85      if (peer != null){
86        return JPF_gov_nasa_jpf_jvm_Verify.incrementCounter(null, 0, id);
87      } else {
88        if (counter == null) {
89          counter = new int[(id >= MAX_COUNTERS) ? id+1 : MAX_COUNTERS];
90        } else if (id >= counter.length) {
91          int[] newCounter = new int[id+1];
92          System.arraycopy(counter, 0, newCounter, 0, counter.length);
93          counter = newCounter;
94        }
95        
96        if ((id >= 0) && (id < counter.length)) {
97          return ++counter[id];
98        }
99  
100       return 0;
101     }
102   }
103 
104   
105   //  Backwards compatibility END
106 
107   /**
108    * Adds a comment to the error trace, which will be printed and saved.
109    */
110   public static void addComment (String   s) {}
111 
112   /*
113    * Backwards compatibility START
114    * @deprecated use "assert cond : msg"
115    */
116   public static void assertTrue (String   s, boolean cond) {
117     if (!cond) {
118       System.out.println(s);
119       assertTrue(cond);
120     }
121   }
122 
123   /**
124    * Checks that the condition is true.
125    * @deprecated use 'assert' directly
126    */
127   public static void assertTrue (boolean cond) {
128     if (!cond) {
129       throw new AssertionError  ("Verify.assertTrue failed");
130     }
131   }
132 
133   public static void atLabel (String   label) {}
134 
135   public static void atLabel (int label) {}
136 
137   /**
138    * Marks the beginning of an atomic block.
139    */
140   public static void beginAtomic () {}
141 
142   /**
143    * Marks the end of an atomic block.
144    */
145   public static void endAtomic () {}
146   
147   public static void boring (boolean cond) {}
148 
149   public static void busyWait (long duration) {
150     // this gets only executed outside of JPF
151     while (duration > 0) {
152       duration--;
153     }
154   }
155 
156   public static boolean isCalledFromClass (String   refClsName) {
157     Throwable   t = new Throwable  ();
158     StackTraceElement  [] st = t.getStackTrace();
159     
160     if (st.length < 3) {
161       // main() or run()
162       return false;
163     }
164     
165     try {
166       Class   refClazz = Class.forName(refClsName);
167       Class   callClazz = Class.forName(st[2].getClassName());
168       
169       return (refClazz.isAssignableFrom(callClazz));
170       
171     } catch (ClassNotFoundException   cfnx) {
172       return false;
173     }
174   }
175   
176   public static void dumpState () {}
177 
178   public static void ignoreIf (boolean cond) {}
179 
180   public static void instrumentPoint (String   label) {}
181 
182   public static void instrumentPointDeep (String   label) {}
183 
184   public static void instrumentPointDeepRecur (String   label, int depth) {}
185 
186   public static void interesting (boolean cond) {}
187 
188   public static void print (String   s) {
189     System.out.println(s);
190   }
191 
192   public static void print (String   s, int i) {
193     System.out.println(s + " : " + i);
194   }
195 
196   public static void print (String   s, boolean b) {
197     System.out.println(s + " : " + b);
198   }
199 
200   
201   /**
202    * this is the new boolean choice generator. Since there's no real
203    * heuristic involved with boolean values, we skip the id (it's a
204    * hardwired "boolean")
205    */
206   public static boolean getBoolean () {
207     // just executed when not running inside JPF, native otherwise
208     return ((System.currentTimeMillis() & 1) != 0);
209   }
210 
211   public static int getInt (int min, int max) {
212     // this is only executed when not running JPF, native otherwise
213     if (random == null) {
214       random = new Random  ();
215     }
216     
217     return random.nextInt((max-min+1)) + min;    
218   }
219   
220   /**
221    * this is the API for int value choice generators. 'id' is used to identify
222    * both the corresponding ChoiceGenerator subclass, and the application specific
223    * ctor parameters from the normal JPF configuration mechanism
224    */
225   public static int getInt (String   key){
226     // this is only executed when not running JPF, native otherwise
227     if (random == null) {
228       random = new Random  ();
229     }
230     return random.nextInt();
231   }
232 
233   /**
234    * this is the API for double 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 double getDouble (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.nextDouble();
244   }
245 
246   /**
247    * Returns a random number between 0 and max inclusive.
248    */
249   public static int random (int max) {
250     // this is only executed when not running JPF
251     if (random == null) {
252       random = new Random  ();
253     }
254     return random.nextInt(max + 1);
255   }
256 
257   /**
258    * Returns a random boolean value, true or false. Note this gets
259    * handled by the native peer, and is just here to enable running
260    * instrumented applications w/o JPF
261    */
262   public static boolean randomBool () {
263     // this is only executed when not running JPF
264     if (random == null) {
265       random = new Random  ();
266     }
267     return random.nextBoolean();
268   }
269 
270   public long currentTimeMillis () {
271     return System.currentTimeMillis();
272   }
273   
274   // Backwards compatibility START
275   public static Object   randomObject (String   type) {
276     return null;
277   }
278 
279  }
280
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags