AbstractSearch


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.search;
20  
21  import java.io.FileWriter  ;
22  import java.io.IOException  ;
23  
24  import gov.nasa.jpf.Config;
25  import gov.nasa.jpf.JPFException;
26  import gov.nasa.jpf.VM;
27  import gov.nasa.jpf.Search;
28  import gov.nasa.jpf.SearchListener;
29  import gov.nasa.jpf.SearchListenerMulticaster;
30  import gov.nasa.jpf.SearchState;
31  import gov.nasa.jpf.State;
32  
33  import gov.nasa.jpf.Error;
34  import gov.nasa.jpf.ErrorList;
35  import gov.nasa.jpf.Path;
36  import gov.nasa.jpf.Property;
37  
38  
39  import gov.nasa.jpf.util.Debug;
40  import gov.nasa.jpf.Transition;
41  
42  import gov.nasa.jpf.util.DynamicIntArray;
43  
44  /**
45   * the mother of all search classes. Mostly takes care of listeners, keeping
46   * track of state attributes and errors. This class mainly keeps the
47   * general search info like depth, configured properties etc.
48   */
49  public abstract class AbstractSearch implements Search {
50    protected ErrorList errors = new ErrorList();
51  
52    protected int       depth = 0;
53    protected VM        vm;
54    protected Property  property;
55  
56    // the forward() attributes, e.g. used by the listeners
57    protected boolean isEndState = false;
58    protected boolean isNewState = true;
59  
60    protected boolean matchDepth;
61    protected long    minFreeMemory;
62    protected int     depthLimit;
63    
64    protected String   lastSearchConstraint;
65  
66    // these states control the search loop
67    protected boolean done = false;
68    protected boolean doBacktrack = false;
69    SearchListener     listener;
70    
71    Config config; // to later-on access settings that are only used once (not ideal)
72    
73    // statistics
74    //int maxSearchDepth = 0;
75    
76    /** (on demand) storage to keep track of state depths */
77    DynamicIntArray stateDepth;
78  
79    protected AbstractSearch (Config config, VM vm) {
80      this.vm = vm;
81      this.config = config;
82      
83      depthLimit = config.getInt("search.depth_limit", -1);
84      matchDepth = config.getBoolean("search.match_depth");
85      minFreeMemory = config.getMemorySize("search.min_free", 1024<<10);
86      
87      try {
88        property = getProperties(config);
89        if (property == null) {
90          Debug.println(Debug.ERROR, "no property");
91        }
92      
93        addListeners(config);
94      } catch (Throwable   t) {
95        Debug.println(Debug.ERROR, "Search initialization failed: " + t);
96      }
97    }
98  
99    public void addProperty (Property newProperty) {
100     property = PropertyMulticaster.add(property, newProperty);
101   }
102   
103   public void removeProperty (Property oldProperty) {
104      property = PropertyMulticaster.remove(property, oldProperty);
105   }
106   
107   /**
108    * return set of configured properties
109    * note there is a nameclash here - JPF 'properties' have nothing to do with
110    * Java properties (java.util.Properties)
111    */
112   protected Property getProperties (Config config) throws Config.Exception {
113     Property props = null;
114     
115     Object  [] a = config.getInstances("search.properties", Property.class);
116     if (a != null) {
117       for (int i=0; i<a.length; i++) {
118         props = PropertyMulticaster.add(props, (Property)a[i]);
119       }
120     }
121         
122     return props;
123   }
124 
125   protected boolean hasPropertyTermination () {
126     if (isPropertyViolated()) {
127       if (done) {
128         return true;
129       }
130     }
131     
132     return false;
133   }
134   
135   boolean isPropertyViolated () {
136     if ((property != null) && !property.check(vm, null)) {
137       error(property, vm.getPath());
138       return true;
139     }
140     
141     return false;
142   }
143   
144   void addListeners (Config config) throws Config.Exception {
145     Object  [] listeners = config.getInstances("search.listener", SearchListener.class);
146     if (listeners != null) {
147       for (int i=0; i<listeners.length; i++) {
148         addListener( (SearchListener) listeners[i]);
149       }
150     }
151   }
152   
153   public void addListener (SearchListener newListener) {
154     listener = SearchListenerMulticaster.add(listener, newListener);
155   }
156 
157   public void removeListener (SearchListener removeListener) {
158     listener = SearchListenerMulticaster.remove(listener,removeListener);
159   }
160 
161   public ErrorList getErrors () {
162     return errors;
163   }
164 
165   public VM getVM() {
166     return vm;
167   }
168   
169   public boolean isEndState () {
170     return isEndState;
171   }
172   
173   public boolean hasNextState () {
174     return !isEndState();
175   }
176 
177   public boolean isNewState () {
178     boolean isNew = vm.isNewState();
179 
180     if (matchDepth) {
181       int id = vm.getStateId();
182 
183       if (isNew) {
184         setStateDepth(id, depth);
185       } else {
186         if (depth >= getStateDepth(id)) {
187           return false;
188         }
189       }
190     }
191 
192     return isNew;
193   }
194 
195   public boolean isVisitedState () {
196     return !isNewState();
197   }
198 
199   public int getSearchDepth () {
200     return depth;
201   }
202 
203   public String   getSearchConstraint () {
204     return lastSearchConstraint;
205   }
206   
207   public Transition getTransition () {
208     return vm.getLastTransition();
209   }
210 
211   public int getStateNumber () {
212     return vm.getStateId();
213   }
214 
215   public boolean requestBacktrack () {
216     return false;
217   }
218 
219   public boolean supportsBacktrack () {
220     return false;
221   }
222 
223   public boolean supportsRestoreState () {
224     // not supported by default
225     return false;
226   }
227 
228   protected int getMaxSearchDepth () {
229     int searchDepth = Integer.MAX_VALUE;
230 
231     if (depthLimit > 0) {
232       int initialDepth = vm.getPathLength();
233 
234       if ((Integer.MAX_VALUE - initialDepth) > depthLimit) {
235         searchDepth = depthLimit + initialDepth;
236       }
237     }
238 
239     return searchDepth;
240   }
241 
242   public int getDepthLimit () {
243     return depthLimit;
244   }
245   
246   protected SearchState getSearchState () {
247     return new AbstractSearchState();
248   }
249 
250   protected void error (Property property, Path path) {
251     Error   error = new Error  (property, path);
252 
253     if (config.getBoolean("search.print_errors")) {
254       Debug.println(Debug.ERROR, error);
255     } else {
256       Debug.println(Debug.ERROR, "\tFound error #" + errors.size());
257     }
258 
259     String   fname = config.getString("search.error_path");
260     boolean getAllErrors = config.getBoolean("search.multiple_errors");
261     if (fname != null) {
262       if (getAllErrors) {
263         int i = fname.lastIndexOf('.');
264 
265         if (i >= 0) {
266           fname = fname.substring(0, i) + '-' + errors.size() +
267                   fname.substring(i);
268         }
269       }
270       
271       savePath(path, fname);
272     }
273 
274     errors.addError(error);
275     done = !getAllErrors;
276     notifyPropertyViolated();
277   }
278 
279   public void savePath(Path path, String   fname) {
280     try {
281       FileWriter   w = new FileWriter  (fname);
282       vm.savePath(path, w);
283       w.close();
284     } catch (IOException   e) {
285       Debug.println(Debug.ERROR, "Failed to saved trace: " + fname);
286     }
287   }
288   
289   protected void notifyStateAdvanced () {
290     if (listener != null) {
291       listener.stateAdvanced(this);
292     }
293   }
294 
295   protected void notifyStateProcessed () {
296     if (listener != null) {
297       listener.stateProcessed(this);
298     }
299   }
300   
301   protected void notifyStateRestored () {
302     if (listener != null) {
303       listener.stateRestored(this);
304     }
305   }
306   
307   protected void notifyStateBacktracked () {
308     if (listener != null) {
309       listener.stateBacktracked(this);
310     }
311   }
312 
313   protected void notifyPropertyViolated () {
314     if (listener != null) {
315       listener.propertyViolated(this);
316     }
317   }
318 
319   protected void notifySearchStarted () {
320     if (listener != null) {
321       listener.searchStarted(this);
322     }
323   }
324 
325   protected void notifySearchConstraintHit (String   constraintId) {
326     if (listener != null) {
327       lastSearchConstraint = constraintId;
328       listener.searchConstraintHit(this);
329     }
330   }
331 
332   protected void notifySearchFinished () {
333     if (listener != null) {
334       listener.searchFinished(this);
335     }
336   }
337 
338 
339   protected boolean forward () {
340     boolean ret = vm.forward();
341     
342     if (ret) {
343       isNewState = vm.isNewState();
344     } else {
345       isNewState = false;
346     }
347     
348     isEndState = vm.isEndState();
349     
350     return ret;
351   }
352 
353   protected boolean backtrack () {
354     isNewState = false;
355     isEndState = false;
356     
357     return vm.backtrack();
358   }
359 
360   protected void restoreState (State state) {
361     // not supported by default
362   }
363 
364 
365   void setStateDepth (int stateId, int depth) {
366     if (stateDepth == null) {
367       stateDepth = new DynamicIntArray(1024);
368     }
369 
370     stateDepth.set(stateId, depth);
371   }
372 
373   int getStateDepth (int stateId) {
374     try {
375       return stateDepth.get(stateId);
376     } catch (Throwable   x) {
377       throw new JPFException( "failed to determine state depth: " + x);
378     }
379   }
380 
381   /**
382    * check if we have a minimum amount of free memory left. If not, we rather want to stop in time
383    * (with a threshold amount left) so that we can report something useful, and not just die silently
384    * with a OutOfMemoryError (which isn't handled too gracefully by most VMs)
385    */
386   boolean checkStateSpaceLimit () {
387     Runtime   rt = Runtime.getRuntime();
388     
389     long avail = rt.freeMemory();
390     
391     // we could also just check for a max number of states, but what really
392     // limits us is the memory required to store states
393     
394     if (avail < minFreeMemory) {
395       // try to collect first
396       rt.gc();
397       avail = rt.freeMemory();
398       
399       if (avail < minFreeMemory) {
400         // Ok, we give up, threshold reached
401         return false;
402       }
403     }
404       
405     return true;
406   }
407   
408   /**
409    * DOCUMENT ME!
410    */
411   class AbstractSearchState implements SearchState {
412     int depth;
413 
414     AbstractSearchState () {
415       depth = AbstractSearch.this.depth;
416     }
417 
418     public int getSearchDepth () {
419       return depth;
420     }
421   }
422 }
423 
424
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags