e447741a3c50e736474bb424f2d478b452cb658c
[jpf-core.git] / src / main / gov / nasa / jpf / search / Search.java
1 /*
2  * Copyright (C) 2014, United States Government, as represented by the
3  * Administrator of the National Aeronautics and Space Administration.
4  * All rights reserved.
5  *
6  * The Java Pathfinder core (jpf-core) platform is licensed under the
7  * Apache License, Version 2.0 (the "License"); you may not use this file except
8  * in compliance with the License. You may obtain a copy of the License at
9  * 
10  *        http://www.apache.org/licenses/LICENSE-2.0. 
11  *
12  * Unless required by applicable law or agreed to in writing, software
13  * distributed under the License is distributed on an "AS IS" BASIS,
14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15  * See the License for the specific language governing permissions and 
16  * limitations under the License.
17  */
18 package gov.nasa.jpf.search;
19
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.ConfigChangeListener;
22 import gov.nasa.jpf.Error;
23 import gov.nasa.jpf.JPF;
24 import gov.nasa.jpf.JPFException;
25 import gov.nasa.jpf.JPFListenerException;
26 import gov.nasa.jpf.Property;
27 import gov.nasa.jpf.State;
28 import gov.nasa.jpf.report.Reporter;
29 import gov.nasa.jpf.util.IntVector;
30 import gov.nasa.jpf.util.JPFLogger;
31 import gov.nasa.jpf.util.Misc;
32 import gov.nasa.jpf.vm.VM;
33 import gov.nasa.jpf.vm.Path;
34 import gov.nasa.jpf.vm.ThreadList;
35 import gov.nasa.jpf.vm.Transition;
36
37 import java.util.ArrayList;
38 import java.util.List;
39 import java.util.concurrent.atomic.AtomicBoolean;
40
41 /**
42  * the mother of all search classes. Mostly takes care of listeners, keeping
43  * track of state attributes and errors. This class mainly keeps the
44  * general search info like depth, configured properties etc.
45  */
46 public abstract class Search {
47   
48   protected static JPFLogger log = JPF.getLogger("gov.nasa.jpf.search");
49   
50   /** error encountered during last transition, null otherwise */
51   protected Error currentError = null;
52   protected ArrayList<Error> errors = new ArrayList<Error>();
53
54   protected int       depth = 0;
55   protected VM       vm;
56
57   protected ArrayList<Property> properties;
58
59   protected boolean matchDepth;
60   protected long    minFreeMemory;
61   protected int     depthLimit;
62   protected boolean getAllErrors;
63
64   // message explaining the last search constraint hit
65   protected String lastSearchConstraint;
66
67   // these states control the search loop
68   protected boolean done = false;
69   protected boolean doBacktrack = false;
70
71   // do we have a probe request
72   protected AtomicBoolean notifyProbeListeners = new AtomicBoolean(false);
73
74   /** search listeners. We keep them in a simple array to avoid
75    creating objects on each notification */
76   protected SearchListener[] listeners = new SearchListener[0];
77
78   /** this is a special SearchListener that is always notified last, so that
79    * PublisherExtensions can be sure the notification has been processed by all listeners */
80   protected Reporter reporter;
81
82   protected final Config config; // to later-on access settings that are only used once (not ideal)
83
84   // don't forget to unregister or we have a HUGE memory leak if the same Config object is
85   // reused for several JPF runs
86   class ConfigListener implements ConfigChangeListener {
87
88     @Override
89     public void propertyChanged(Config config, String key, String oldValue, String newValue) {
90       // Different Config instance
91       if (!config.equals(Search.this.config)) {
92         return;
93       }
94
95       // Check if Search configuration changed
96       if (key.startsWith("search.")){
97         String k = key.substring(7);
98         if ("match_depth".equals(k) ||
99             "min_free".equals(k) ||
100             "multiple_errors".equals(k)){
101           initialize(config);
102         }
103       }
104     }
105     
106     @Override
107     public void jpfRunTerminated (Config config){
108       config.removeChangeListener(this);
109     }
110   }
111   
112   /** storage to keep track of state depths */
113   protected final IntVector stateDepth = new IntVector();
114
115   protected Search (Config config, VM vm) {
116     this.vm = vm;
117     this.config = config;
118
119     initialize( config);
120
121     properties = getProperties(config);
122     if (properties.isEmpty()) {
123       log.severe("no property");
124     }
125     
126     config.addChangeListener( new ConfigListener());
127   }
128
129   protected void initialize( Config conf){
130     depthLimit = conf.getInt("search.depth_limit", Integer.MAX_VALUE);
131     matchDepth = conf.getBoolean("search.match_depth");
132     minFreeMemory = conf.getMemorySize("search.min_free", 1024<<10);    
133     getAllErrors = conf.getBoolean("search.multiple_errors");
134   }
135   
136   /**
137    * called after the JPF run is finished. Shouldn't be public, but is called by JPF
138    */
139   public void cleanUp(){
140     // nothing here, the ConfigListener removes itself
141   }
142   
143   public Config getConfig() {
144     return config;
145   }
146   
147   public abstract void search ();
148
149   public void setReporter(Reporter reporter){
150     this.reporter = reporter;
151   }
152
153   public void addListener (SearchListener newListener) {
154     log.info("SearchListener added: ", newListener);
155     listeners = Misc.appendElement(listeners, newListener);
156   }
157
158   public boolean hasListenerOfType (Class<?> listenerCls) {
159     return Misc.hasElementOfType(listeners, listenerCls);
160   }
161   
162   public <T> T getNextListenerOfType(Class<T> type, T prev){
163     return Misc.getNextElementOfType(listeners, type, prev);
164   }
165
166
167   public void removeListener (SearchListener removeListener) {
168     listeners = Misc.removeElement(listeners, removeListener);
169   }
170
171
172   public void addProperty (Property newProperty) {
173     properties.add(newProperty);
174   }
175
176   public void removeProperty (Property oldProperty) {
177      properties.remove(oldProperty);
178   }
179
180   /**
181    * return set of configured properties
182    * note there is a name clash here - JPF 'properties' have nothing to do with
183    * Java properties (java.util.Properties)
184    */
185   protected ArrayList<Property> getProperties (Config config) {
186     Class<?>[] argTypes = { Config.class, Search.class };
187     Object[] args = { config, this };
188
189     ArrayList<Property> list = config.getInstances("search.properties", Property.class,
190                                                    argTypes, args);
191
192     return list;
193   }
194
195   // check for property violation, return true if not done
196   protected boolean hasPropertyTermination () {
197     if (currentError != null){
198       if (done){
199         return true;
200       } else { // we search for multiple errors, so we ignore and go on
201         doBacktrack = true;
202       }
203     }
204
205     return false;
206   }
207
208   // this should only be called once per transition, otherwise it keeps adding the same error
209   protected boolean checkPropertyViolation () {
210     for (Property p : properties) {
211       if (!p.check(this, vm)) {
212         error(p, vm.getClonedPath(), vm.getThreadList());
213         return true;
214       }
215     }
216
217     return false;
218   }
219
220   public List<Error> getErrors () {
221     return errors;
222   }
223
224   public int getNumberOfErrors(){
225     return errors.size();
226   }
227
228   public String getLastSearchConstraint() {
229     return lastSearchConstraint;
230   }
231
232   /**
233    * request a probe
234    * 
235    * This does not do the actual listener notification, it only stores
236    * the request, which is then processed from within JPFs inner execution loop.
237    * As a consequence, probeSearch() can be called async, and searchProbed() listeners
238    * don't have to bother with synchronization or inconsistent JPF states (notification 
239    * happens from within JPFs main thread after a completed Instruction execution)
240    */
241   public void probeSearch(){
242     notifyProbeListeners.set(true);
243   }
244   
245   /**
246    * this does the actual notification and resets the request, hence this call
247    * should only happen from within JPFs main thread
248    */
249   public void checkAndResetProbeRequest(){
250     if (notifyProbeListeners.compareAndSet(true, false)){
251       notifySearchProbed();
252     }
253   }
254   
255   /**
256    * @return error encountered during *last* transition (null otherwise)
257    */
258   public Error getCurrentError(){
259     return currentError;
260   }
261
262   public Error getLastError() {
263     int i=errors.size()-1;
264     if (i >=0) {
265       return errors.get(i);
266     } else {
267       return null;
268     }
269   }
270
271   public boolean hasErrors(){
272     return !errors.isEmpty();
273   }
274
275   public VM getVM() {
276     return vm;
277   }
278
279   public boolean isEndState () {
280     return vm.isEndState();
281   }
282
283   public boolean isErrorState(){
284     return (currentError != null);
285   }
286
287   public boolean hasNextState () {
288     return !isEndState();
289   }
290
291   public boolean transitionOccurred(){
292     return vm.transitionOccurred();
293   }
294
295   public boolean isNewState () {
296     boolean isNew = vm.isNewState();
297
298     if (matchDepth) {
299       int id = vm.getStateId();
300
301       if (isNew) {
302         setStateDepth(id, depth);
303       } else {
304         return depth < getStateDepth(id);
305       }
306     }
307
308     return isNew;
309   }
310
311   public boolean isVisitedState () {
312     return !isNewState();
313   }
314
315   public boolean isIgnoredState(){
316     return vm.isIgnoredState();
317   }
318
319   public boolean isProcessedState(){
320     return vm.getChoiceGenerator().isProcessed();
321   }
322
323   public boolean isDone(){
324     return done;
325   }
326
327   public int getDepth () {
328     return depth;
329   }
330
331   public String getSearchConstraint () {
332     return lastSearchConstraint;
333   }
334
335   public Transition getTransition () {
336     return vm.getLastTransition();
337   }
338
339   public int getStateId () {
340     return vm.getStateId();
341   }
342
343   public int getPurgedStateId () {
344     return -1; // a lot of Searches don't purge any states
345   }
346
347
348   /**
349    * this is somewhat redundant to SystemState.setIgnored(), but we don't
350    * want to mix the case of overriding state matching with backtracking when
351    * searching for multiple errors
352    */
353   public boolean requestBacktrack () {
354     return doBacktrack = true;
355   }
356
357
358   protected boolean checkAndResetBacktrackRequest() {
359     if (doBacktrack){
360       doBacktrack = false;
361       return true;
362     } else {
363       return false;
364     }
365   }
366
367   public boolean supportsBacktrack () {
368     return true;
369   }
370
371   public boolean supportsRestoreState () {
372     // not supported by default
373     return false;
374   }
375
376   public int getDepthLimit () {
377     return depthLimit;
378   }
379   
380   public void setDepthLimit(int limit){
381     depthLimit = limit;
382   }
383
384   protected SearchState getSearchState () {
385     return new SearchState(this);
386   }
387
388   // can be used by SearchListeners to create path-less errors (liveness)
389   public void error (Property property) {
390     error(property, null, null);
391   }
392
393   public void error (Property property, Path path, ThreadList threadList) {
394
395     if (getAllErrors) {
396        // otherwise we are going to overwrite it if we go on
397       try {
398         property = property.clone();
399         path = path.clone();
400         threadList = (ThreadList) threadList.clone(); // this makes it a snapshot (deep) clone
401       } catch (CloneNotSupportedException cnsx){
402         throw new JPFException("failed to clone error information: " + cnsx);
403       }
404       done = false;
405       
406     } else {
407       done = true;
408     }
409
410     currentError = new Error(errors.size()+1, property, path, threadList);
411
412     errors.add(currentError);
413
414     // we should not reset the property until listeners have been notified
415     // (the listener might be the property itself, in which case it could get
416     // confused if propertyViolated() notifications happen after a reset)
417   }
418
419   public void resetProperties(){
420     for (Property p : properties) {
421       p.reset();
422     }
423   }
424
425   protected void notifyStateAdvanced () {
426     try {
427       for (int i = 0; i < listeners.length; i++) {
428         listeners[i].stateAdvanced(this);
429       }
430       if (reporter != null){
431         // reporter always comes last to ensure all listeners have been notified
432         reporter.stateAdvanced(this);
433       }
434     } catch (Throwable t) {
435       throw new JPFListenerException("exception during stateAdvanced() notification", t);
436     }
437   }
438
439   protected void notifyStateProcessed() {
440     try {
441       for (int i = 0; i < listeners.length; i++) {
442         listeners[i].stateProcessed(this);
443       }
444       if (reporter != null){
445         reporter.stateProcessed(this);
446       }
447     } catch (Throwable t) {
448       throw new JPFListenerException("exception during stateProcessed() notification", t);
449     }
450   }
451
452   protected void notifyStateStored() {
453     try {
454       for (int i = 0; i < listeners.length; i++) {
455         listeners[i].stateStored(this);
456       }
457       if (reporter != null){
458         reporter.stateStored(this);
459       }
460     } catch (Throwable t) {
461       throw new JPFListenerException("exception during stateStored() notification", t);
462     }
463   }
464
465   protected void notifyStateRestored() {
466     try {
467       for (int i = 0; i < listeners.length; i++) {
468         listeners[i].stateRestored(this);
469       }
470       if (reporter != null){
471         reporter.stateRestored(this);
472       }
473     } catch (Throwable t) {
474       throw new JPFListenerException("exception during stateRestored() notification", t);
475     }
476   }
477
478   protected void notifyStateBacktracked() {
479     try {
480       for (int i = 0; i < listeners.length; i++) {
481         listeners[i].stateBacktracked(this);
482       }
483       if (reporter != null){
484         reporter.stateBacktracked(this);
485       }
486     } catch (Throwable t) {
487       throw new JPFListenerException("exception during stateBacktracked() notification", t);
488     }
489   }
490
491   protected void notifyStatePurged() {
492     try {
493       for (int i = 0; i < listeners.length; i++) {
494         listeners[i].statePurged(this);
495       }
496       if (reporter != null){
497         reporter.statePurged(this);
498       }
499     } catch (Throwable t) {
500       throw new JPFListenerException("exception during statePurged() notification", t);
501     }
502   }
503
504   public void notifySearchProbed() {
505     try {
506       for (int i = 0; i < listeners.length; i++) {
507         listeners[i].searchProbed(this);
508       }
509       if (reporter != null){
510         reporter.searchProbed(this);
511       }
512     } catch (Throwable t) {
513       throw new JPFListenerException("exception during searchProbed() notification", t);
514     }
515   }
516
517   
518   protected void notifyPropertyViolated() {
519     try {
520       for (int i = 0; i < listeners.length; i++) {
521         listeners[i].propertyViolated(this);
522       }
523       if (reporter != null){
524         reporter.propertyViolated(this);
525       }
526     } catch (Throwable t) {
527       throw new JPFListenerException("exception during propertyViolated() notification", t);
528     }
529
530     // reset properties if getAllErrors is set
531     if (getAllErrors){
532       resetProperties();
533     }
534   }
535
536   protected void notifySearchStarted() {
537     try {
538       for (int i = 0; i < listeners.length; i++) {
539         listeners[i].searchStarted(this);
540       }
541       if (reporter != null){
542         reporter.searchStarted(this);
543       }
544     } catch (Throwable t) {
545       throw new JPFListenerException("exception during searchStarted() notification", t);
546     }
547   }
548
549   public void notifySearchConstraintHit(String details) {
550     try {
551       lastSearchConstraint = details;
552       for (int i = 0; i < listeners.length; i++) {
553         listeners[i].searchConstraintHit(this);
554       }
555       if (reporter != null){
556         reporter.searchConstraintHit(this);
557       }
558     } catch (Throwable t) {
559       throw new JPFListenerException("exception during searchConstraintHit() notification", t);
560     }
561   }
562
563   protected void notifySearchFinished() {
564     try {
565       for (int i = 0; i < listeners.length; i++) {
566         listeners[i].searchFinished(this);
567       }
568       if (reporter != null){
569         reporter.searchFinished(this);
570       }
571     } catch (Throwable t) {
572       throw new JPFListenerException("exception during searchFinished() notification", t);
573     }
574   }
575
576   protected boolean forward () {
577     currentError = null;
578
579     boolean ret = vm.forward();
580
581     checkPropertyViolation();
582     return ret;
583   }
584
585   protected boolean backtrack () {
586     return vm.backtrack();
587   }
588
589   public void setIgnoredState (boolean cond) {
590     vm.ignoreState(cond);
591   }
592
593   protected void restoreState (State state) {
594     // not supported by default
595   }
596
597   /** this can be used by listeners to terminate the search */
598   public void terminate () {
599     done = true;
600   }
601
602   protected void setStateDepth (int stateId, int depth) {
603     stateDepth.set(stateId, depth + 1);
604   }
605
606   public int getStateDepth (int stateId) {
607     int depthPlusOne = stateDepth.get(stateId);
608     if (depthPlusOne <= 0) {
609       throw new JPFException("Asked for depth of unvisited state");
610     } else {
611       return depthPlusOne - 1;
612     }
613   }
614
615   /**
616    * check if we have a minimum amount of free memory left. If not, we rather want to stop in time
617    * (with a threshold amount left) so that we can report something useful, and not just die silently
618    * with a OutOfMemoryError (which isn't handled too gracefully by most VMs)
619    */
620   public boolean checkStateSpaceLimit () {
621     Runtime rt = Runtime.getRuntime();
622
623     long avail = rt.freeMemory();
624
625     // we could also just check for a max number of states, but what really
626     // limits us is the memory required to store states
627
628     if (avail < minFreeMemory) {
629       // try to collect first
630       rt.gc();
631       avail = rt.freeMemory();
632
633       if (avail < minFreeMemory) {
634         // Ok, we give up, threshold reached
635         return false;
636       }
637     }
638
639     return true;
640   }
641 }
642