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 {@code Search} abstract class is at the heart of all search classes. Even when it is not extended by child classes, it will
  43  * be embedded in the logic as an input for some of the methods.
  44  *
  45  * <p>The main purpose of the {@code Search} class is to track general search information such as depth, configured properties,
  46  * errors, etc. as well as to define how the search algorithm functions. In its simplest form, a search algorithm can be defined
  47  * using the abstract method {@code search} with a series of {@code forward} and {@code backtrack}. More complex search
  48  * algorithms can also make use of the state storing functionality of the {@code Search} class, as well as ignoring states and
  49  * removing states from the search tree.
  50  *
  51  * <p>Another very important aspect of the {@code Search} class is not only to implement search algorithms, but also to define
  52  * the information that describes the current search loop. This is crucial in order to enable the {@code SearchListener} and
  53  * {@code SearchListenerAdapter} classes responsible for extracting crucial data from the search loop during its verification
  54  * efforts.
  55  */
  56 public abstract class Search {
  57
  58   /** The {@code JPFLogger} object assigned to the {@code gov.nasa.jpf.search} subsystem
  59    * @see gov.nasa.jpf.util.JPFLogger
  60    */
  61   protected static JPFLogger log = JPF.getLogger("gov.nasa.jpf.search");
  62
  63   /** The value of {@code currentError} will either be the error encountered during last
  64    *  transition or null if no error was encountered */
  65   protected Error currentError = null;
  66
  67   /** A running list of all errors encountered during verification. The list will always
  68    * contain the current and past values of {@code currentError}. Errors are set added
  69    * during verification in the {@code error}
  70    * method.
  71    *
  72    * <p>{@code errors} will only hold one error before verification stops unless {@code getAllErrors}
  73    * is set to true
  74    *
  75    * @see #error(Property, Path, ThreadList)
  76    * @see #getAllErrors
  77    */
  78   protected ArrayList<Error> errors = new ArrayList<Error>();
  79
  80   /**  {@code depth} represents the current depth of the search tree. */
  81   protected int depth = 0;
  82   /** {@code vm} represents the virtual machine that the search algorithm will be traversing*/
  83   protected VM vm;
  84
  85   /** A list of properties provided from the search configuration at the start of verification. Every property has a {@code check}
  86    * method that will be used during verification to tell if any of the properties have been violated.*/
  87   protected ArrayList<Property> properties;
  88
  89   /** A property set by the user before verification. If {@code matchDepth} is true it will change the behavior of
  90    * {@code isNewState()}.
  91    * @see #isNewState() */
  92   protected boolean matchDepth;
  93   /** A property set by the user to define what the minimum memory required to keep verifying is. The reason this is a non-zero
  94    * value is to ensure some memory is left over to output a legible message before ending execution instead of simply throwing
  95    * an {@code OutOfMemoryError}.
  96    *
  97    * <p> The default value for {@code minFreeMemory} is 1024 << 10 bytes. */
  98   protected long    minFreeMemory;
  99   /** A property set by the user to define what the maximum depth allowed during verification is.
 100    *
 101    * <p>By default the value is set to {@code Integer.MAX_VALUE}*/
 102   protected int     depthLimit;
 103
 104   /** A property set by the user to define whether to halt execution after encountering the first error during verification.
 105    * If {@code getAllErrors} is set to true, verification will not stop after the first error, and every possible error
 106    * during verification will be logged as a result. */
 107   protected boolean getAllErrors;
 108
 109   /** A {@code String} set to contain details on what the constraint that caused verification to halt was. Will generally be
 110    * used by the {@code searchContraintHit} methods in {@code SearchListeners}.
 111    *
 112    * @see gov.nasa.jpf.search.SearchListener#searchConstraintHit(Search) */
 113   protected String lastSearchConstraint;
 114
 115   /** {@code done} is a flag set during verification to notify the search loop when verification has finished. */
 116   protected boolean done = false;
 117   /** {@code doBacktrack} is a flag set during verification in order to request that the search loop backtracks
 118    * one state.*/
 119   protected boolean doBacktrack = false;
 120
 121  /** {@code notifyProbeListeners} is a flag set during verification stating whether or not a probe has been
 122   * requested. When a probe is requested, relevant {@code SearchListeners} will be notified via {@code checkAndResetProbeRequest}*/
 123   protected AtomicBoolean notifyProbeListeners = new AtomicBoolean(false);
 124
 125   /** {@code listeners} is an array used to hold {@code SearchListener} objects. We keep them in a simple array to avoid
 126    creating objects on each notification */
 127   protected SearchListener[] listeners = new SearchListener[0];
 128
 129   /** {@code reporter} is a special listener that is always notified last in order to ensure all other listeners have been notified
 130    * beforehand. {@code reporter} is used to report information about the search loop to whichever output method the user has
 131    * specified.
 132    *
 133    *  <p>By default, the output method is to console.*/
 134   protected Reporter reporter;
 135
 136   /** {@code config} is an object passed in during instantiation of the {@code Search} object and it specifies the properties and
 137    * configurations the search loop should run under. The value behind {@code config} is only ever used once and stored within this
 138    * object.*/
 139   protected final Config config;
 140
 141   /**
 142    * {@code ConfigListener} is an implementation of the interface {@code ConfigChangeListener} and is used to subscribe to changes
 143    * that occur to the configuration of JPF in order to update the {@code config} object. While highly useful, one should always
 144    * remember to unregister the {@code config} object from each {@code ConfigListener} once it is no longer needed. Failure to
 145    * do this will cause massive memory leaks to begin piling up as a result of the same {@code Config} object being used across
 146    * several JPF executions.
 147    *
 148    */
 149   class ConfigListener implements ConfigChangeListener {
 150
 151     @Override
 152     public void propertyChanged(Config config, String key, String oldValue, String newValue) {
 153       // Different Config instance
 154       if (!config.equals(Search.this.config)) {
 155         return;
 156       }
 157
 158       // Check if Search configuration changed
 159       if (key.startsWith("search.")){
 160         String k = key.substring(7);
 161         if ("match_depth".equals(k) ||
 162             "min_free".equals(k) ||
 163             "multiple_errors".equals(k)){
 164           initialize(config);
 165         }
 166       }
 167     }
 168
 169     @Override
 170     public void jpfRunTerminated (Config config){
 171       config.removeChangeListener(this);
 172     }
 173   }
 174
 175   /** {@code stateDepth} is an int vector storage system (akin to a map) that is responsible for associating states with their
 176    * corresponding depths.
 177    *
 178    * <p>{@code stateDepth} maps the state id of every state to the corresponding depth, in a one to one mapping.*/
 179   protected final IntVector stateDepth = new IntVector();
 180
 181   /**
 182    * Constructs a {@code Search} object using the configuration specified by the user in {@code config} and a virtual machine
 183    * that will be used for verification.
 184    *
 185    *  @param config The configuration and properties that the search loop will be required to commence verification under
 186    *  @param vm The virtual machine that the search loop will traverse and verify states from
 187    */
 188   protected Search (Config config, VM vm) {
 189     this.vm = vm;
 190     this.config = config;
 191
 192     initialize( config);
 193
 194     properties = getProperties(config);
 195     if (properties.isEmpty()) {
 196       log.severe("no property");
 197     }
 198
 199     config.addChangeListener( new ConfigListener());
 200   }
 201
 202   /**
 203    * Initializes the properties that the search loop will need to run under in order to make sure that each iteration of the search
 204    * loop is in compliance with the properties set by JPF and the user.
 205    *
 206    * @param conf The configuration object ({@code config}) that contains the necessary information to initialize the property values
 207    */
 208   protected void initialize( Config conf){
 209     depthLimit = conf.getInt("search.depth_limit", Integer.MAX_VALUE);
 210     matchDepth = conf.getBoolean("search.match_depth");
 211     minFreeMemory = conf.getMemorySize("search.min_free", 1024<<10);
 212     getAllErrors = conf.getBoolean("search.multiple_errors");
 213   }
 214
 215   /**
 216    * Called after the JPF run is finished. Should not be public, but is called by JPF
 217    */
 218   public void cleanUp(){
 219     // nothing here, the ConfigListener removes itself
 220   }
 221
 222   /**
 223    * Returns the {@code config} object that is used by the {@code Search} class.
 224    *
 225    * @return The configuration object that is used for verification
 226    */
 227   public Config getConfig() {
 228     return config;
 229   }
 230
 231   /**
 232    * One of the most important methods in the {@code Search} class. {@code search} is used to specify what the algorithm and behavior
 233    * for verification are. When the term "search loop" is brought up in other documentation, it generally means the loop that is used
 234    * running in the {@code search} method.
 235    */
 236   public abstract void search ();
 237
 238   /**
 239    * Sets the {@code reporter} object used during verification to the specified {@code reporter}.
 240    *
 241    * @param reporter The reporter used to replace the current reporter object in the {@code Search} class
 242    */
 243   public void setReporter(Reporter reporter){
 244     this.reporter = reporter;
 245   }
 246
 247   /**
 248    * Appends a {@code SearchListener} object to the {@code listener} array. In addition to appending the search listener, the action is also logged
 249    * to the JPFLog {@code log} used in the {@code Search} class.
 250    *
 251    * @param newListener A new {@code SearchListener} to append to the {@code listener} array
 252    */
 253   public void addListener (SearchListener newListener) {
 254     log.info("SearchListener added: ", newListener);
 255     listeners = Misc.appendElement(listeners, newListener);
 256   }
 257
 258   /**
 259    * Checks whether a listener of the same type as {@code listenerCls} exists in {@code listeners} already.
 260    *
 261    * @param listenerCls The object type to check {@code listeners} against
 262    * @return true if an element of the same type as the input parameter exists in {@code listeners}. False otherwise
 263    */
 264   public boolean hasListenerOfType (Class<?> listenerCls) {
 265     return Misc.hasElementOfType(listeners, listenerCls);
 266   }
 267
 268   /**
 269    * Returns the next element in {@code listeners} after the element matching {@code prev} that is of the same type as {@code type}.
 270    *
 271    * @param type The type of element to search for and return
 272    * @param prev The previous element to begin the search from
 273    * @return An element of the same class as {@code type} and coming after {@code prev} in the {@code listeners} array
 274    */
 275   public <T> T getNextListenerOfType(Class<T> type, T prev){
 276     return Misc.getNextElementOfType(listeners, type, prev);
 277   }
 278
 279   /**
 280    * Remove the specified {@code SearchListener} from the {@code listeners} array.
 281    *
 282    * @param removeListener The element to remove from the {@code listeners} array
 283    */
 284   public void removeListener (SearchListener removeListener) {
 285     listeners = Misc.removeElement(listeners, removeListener);
 286   }
 287
 288   /**
 289    * Add a new property to {@code properties}
 290    *
 291    * @param newProperty The property to add to {@code properties}
 292    */
 293   public void addProperty (Property newProperty) {
 294     properties.add(newProperty);
 295   }
 296
 297   /**
 298    * Remove the specified property from {@code properties}
 299    *
 300    * @param oldProperty The property to remove from {@code properties}
 301    */
 302   public void removeProperty (Property oldProperty) {
 303      properties.remove(oldProperty);
 304   }
 305
 306   /**
 307    * Returns the list of configured properties.
 308    *
 309    * <p>Note there is a name clash here - JPF 'properties' have nothing to do with Java properties (java.util.Properties)
 310    *
 311    * @param config The config object to retrieve the properties list from
 312    * @return The list of configured properties
 313    */
 314   protected ArrayList<Property> getProperties (Config config) {
 315     Class<?>[] argTypes = { Config.class, Search.class };
 316     Object[] args = { config, this };
 317
 318     ArrayList<Property> list = config.getInstances("search.properties", Property.class,
 319                                                    argTypes, args);
 320
 321     return list;
 322   }
 323
 324   /**
 325    * Check for property violations and return true if a property is violated and the search loop has finished running (i.e. {@code done}
 326    * is set to true). Returns false otherwise.
 327    *
 328    * @return true if an a property has been violated (i.e. {@code currentError} is not null) and {@code done} is true
 329    */
 330   protected boolean hasPropertyTermination () {
 331     if (currentError != null){
 332       if (done){
 333         return true;
 334       } else { // we search for multiple errors, so we ignore and go on
 335         doBacktrack = true;
 336       }
 337     }
 338
 339     return false;
 340   }
 341
 342   /**
 343    * Iterates through {@code properties} and checks for property violations. {@code checkPropertyViolation} should only be
 344    * called once per transition to avoid it adding the same error every time it is called.
 345    *
 346    * @return true if a property violation is found, false otherwise
 347    */
 348   protected boolean checkPropertyViolation () {
 349     for (Property p : properties) {
 350       if (!p.check(this, vm)) {
 351         error(p, vm.getClonedPath(), vm.getThreadList());
 352         return true;
 353       }
 354     }
 355
 356     return false;
 357   }
 358
 359   /**
 360    * Returns the list of errors encountered during verification
 361    *
 362    * @return The list of errors encountered during verification
 363    */
 364   public List<Error> getErrors () {
 365     return errors;
 366   }
 367
 368   /**
 369    * Returns the number of errors encountered during verification. Will always return 1 if {@code getAllErrors} is false
 370    *
 371    * @return The number of errors encountered during verification
 372    */
 373   public int getNumberOfErrors(){
 374     return errors.size();
 375   }
 376
 377   /**
 378    * Returns the search constraint that was most recently encountered
 379    *
 380    * @return A String detailing the search constraint most recently hit or null if none was encountered
 381    */
 382   public String getLastSearchConstraint() {
 383     return lastSearchConstraint;
 384   }
 385
 386   /**
 387    * Request a probe
 388    *
 389    * <p>This does not perform the actual listener notification, it only stores
 390    * the request, which is then processed from within JPFs inner execution loop.
 391    * As a consequence, {@code probeSearch} can be called asynchronously, and {@code searchProbed} listeners
 392    * don't have to bother with synchronization or inconsistent JPF states (notification
 393    * happens from within JPFs main thread after a completed Instruction execution)
 394    */
 395   public void probeSearch(){
 396     notifyProbeListeners.set(true);
 397   }
 398
 399   /**
 400    * Performs the actual notification and resets the request, hence this call should only happen from within JPFs main thread
 401    */
 402   public void checkAndResetProbeRequest(){
 403     if (notifyProbeListeners.compareAndSet(true, false)){
 404       notifySearchProbed();
 405     }
 406   }
 407
 408   /**
 409    * Returns the most recent error encountered during the last transition
 410    *
 411    * @return The error encountered during the last transition or null if none was encountered
 412    */
 413   public Error getCurrentError(){
 414     return currentError;
 415   }
 416
 417   /**
 418    * Returns the most recent error encountered in the past
 419    *
 420    * @return The most recent error encountered in the past or none if no error has been encountered during verification
 421    */
 422   public Error getLastError() {
 423     int i=errors.size()-1;
 424     if (i >=0) {
 425       return errors.get(i);
 426     } else {
 427       return null;
 428     }
 429   }
 430
 431   /**
 432    * Returns whether or not the search loop has encountered an error yet
 433    *
 434    * @return true if an error has been encountered, false otherwise
 435    */
 436   public boolean hasErrors(){
 437     return !errors.isEmpty();
 438   }
 439
 440   /**
 441    * Returns the {@code vm} object used by the search loop
 442    *
 443    * @return the {@code vm} object used by {@code Search}
 444    */
 445   public VM getVM() {
 446     return vm;
 447   }
 448
 449   /**
 450    * Returns true if the search loop has transitioned into an end state in the virtual machine
 451    *
 452    * @return true if the current state of the {@code vm} is an end state
 453    */
 454   public boolean isEndState () {
 455     return vm.isEndState();
 456   }
 457
 458   /**
 459    * Returns if an error has been encountered during the transition into the current state
 460    *
 461    * @return true if an error has been encountered during the most recent transition, false otherwise
 462    */
 463   public boolean isErrorState(){
 464     return (currentError != null);
 465   }
 466
 467   /**
 468    * Returns whether of not the current state is an end state in the virtual machine
 469    *
 470    * @return true if this is not an end state of the {@code vm}, false otherwise
 471    */
 472   public boolean hasNextState () {
 473     return !isEndState();
 474   }
 475
 476   /**
 477    * Returns whether a transition has occurred from the previous state or not
 478    *
 479    * @return true if a transition has occurred, false otherwise
 480    */
 481   public boolean transitionOccurred(){
 482     return vm.transitionOccurred();
 483   }
 484
 485   /**
 486    * Returns whether the current state in the search loop is a new state and false otherwise.
 487    *
 488    * <p>However, if {@code matchDepth} is set to true,
 489    * then it  will true if the state is new or if the states depth is less than the previously recorded depth. If the state is new, the states
 490    * depth will also be recorded for future use.
 491    *
 492    * @return true if the current state is a new state and false otherwise (behaviour changes if {@code matchDepth} is true
 493    */
 494   public boolean isNewState () {
 495     boolean isNew = vm.isNewState();
 496
 497     if (matchDepth) {
 498       int id = vm.getStateId();
 499
 500       if (isNew) {
 501         setStateDepth(id, depth);
 502       } else {
 503         return depth < getStateDepth(id);
 504       }
 505     }
 506
 507     return isNew;
 508   }
 509
 510   /**
 511    * Returns whether the current state has been visited yet. The opposite of {@code isNewState}
 512    *
 513    * @return true if the state has been visited, false otherwise (behavior changes if {@code matchDepth} is true)
 514    * @see #isNewState()
 515    */
 516   public boolean isVisitedState () {
 517     return !isNewState();
 518   }
 519
 520   /**
 521    * Returns whether the current state is an ignored state in the virtual machine
 522    *
 523    * @return true if the current state is an ignored state, false otherwise
 524    */
 525   public boolean isIgnoredState(){
 526     return vm.isIgnoredState();
 527   }
 528
 529   /**
 530    * Returns whether the current state has been fully explored by the search loop.
 531    *
 532    * @return true if the current state has been fully explored and processed, false otherwise
 533    */
 534   public boolean isProcessedState(){
 535     return vm.getChoiceGenerator().isProcessed();
 536   }
 537
 538   /**
 539    * Return whether the search loop has finished verification
 540    *
 541    * @return true if the search loop has finished verification, false otherwise
 542    */
 543   public boolean isDone(){
 544     return done;
 545   }
 546
 547   /**
 548    * Return the current depth of the search loop
 549    *
 550    * @return The current depth inside the search tree.
 551    */
 552   public int getDepth () {
 553     return depth;
 554   }
 555
 556   /**
 557    * Returns the most recent search constraint that was encountered
 558    *
 559    * @return A String detailing the most recent search constraint that was encountered
 560    */
 561   public String getSearchConstraint () {
 562     return lastSearchConstraint;
 563   }
 564
 565   /**
 566    * Returns the most recent transition that has occurred
 567    *
 568    * @return The last transition that occurred during verification, or null if none has occurred
 569    */
 570   public Transition getTransition () {
 571     return vm.getLastTransition();
 572   }
 573
 574   /**
 575    * Returns the state id of the current state
 576    *
 577    * @return The state id of the current state
 578    */
 579   public int getStateId () {
 580     return vm.getStateId();
 581   }
 582
 583   /**
 584    * Returns the purged states id
 585    *
 586    * <p>Note that while it should return the purged states id, it currently only returns -1 as a
 587    * result of many searches not utilizing this functionality. If it is required, {@code getPurgedStateId}
 588    * should be overridden and changed in subsequent child classes.
 589    *
 590    * @return The purged states id (currently only returns -1)
 591    */
 592   public int getPurgedStateId () {
 593     return -1; // a lot of Searches don't purge any states
 594   }
 595
 596
 597   /**
 598    * Requests that the search loop backtracks one step
 599    *
 600    * <p>This is somewhat redundant to {@code SystemState.setIgnored}, but we don't
 601    * want to mix the case of overriding state matching with backtracking when
 602    * searching for multiple errors.
 603    *
 604    * @return The value of {@code doBacktrack} after is has been set to true (i.e. always true)
 605    */
 606   public boolean requestBacktrack () {
 607     return doBacktrack = true;
 608   }
 609
 610   /**
 611    * Returns the value of {@code doBacktrack} as well as resetting {@code doBacktrack} to false
 612    *
 613    * @return the value of {@code doBackTrack}
 614    */
 615   protected boolean checkAndResetBacktrackRequest() {
 616     if (doBacktrack){
 617       doBacktrack = false;
 618       return true;
 619     } else {
 620       return false;
 621     }
 622   }
 623
 624   /**
 625    * Returns whether the search algorithm supports backtracking or not
 626    *
 627    * @return true if the search algorithm supports backtracking, false otherwise (by default the return
 628    * is true unless overridden)
 629    */
 630   public boolean supportsBacktrack () {
 631     return true;
 632   }
 633
 634   /**
 635    * Returns whether the search algorithm supports restoring states that have been stored (a useful method in
 636    * BreadthFirstSearch)
 637    *
 638    * @return true if the search algorithm supports restoring states, false otherwise (by default the return
 639    * is false as the function is unsupported)
 640    */
 641   public boolean supportsRestoreState () {
 642     // not supported by default
 643     return false;
 644   }
 645
 646   /**
 647    * Returns the depth limit set at the beginning of verification
 648    *
 649    * @return The {@code depthLimit} property
 650    */
 651   public int getDepthLimit () {
 652     return depthLimit;
 653   }
 654
 655   /**
 656    * Sets a new value for the {@code depthLimit} property
 657    *
 658    * @param limit The new limit to set {@code depthLimit} to
 659    */
 660   public void setDepthLimit(int limit){
 661     depthLimit = limit;
 662   }
 663
 664   /**
 665    * Returns a {@code SearchState} object with information describing the current state in the search loop
 666    *
 667    * @return A {@code SearchState} object with information about the current state
 668    */
 669   protected SearchState getSearchState () {
 670     return new SearchState(this);
 671   }
 672
 673   /**
 674    * Creates a new error with the corresponding {@code Property} that causes the error. Does not provide a {@code Path} or {@code ThreadList}, and
 675    * can therefore be used by {@code SearchListeners} to create path-less errors to ensure liveness.
 676    *
 677    * @param property the property that caused the error
 678    * @see #error(Property, Path, ThreadList)
 679    */
 680   public void error (Property property) {
 681     error(property, null, null);
 682   }
 683
 684   /**
 685    * Creates an error with the corresponding {@code Property} that causes the error, alongside the {@code Path}, and {@code ThreadList}.
 686    *
 687    * <p>Will set {@code done} to true and halt the search loop  if {@code getAllErrors} is false. If {@code getAllErrors} is true, it will
 688    * clone the {@code Property}, {@code Path}, and {@code ThreadList} objects that were passed in (as not cloning them may cause subsequent
 689    * operations to overwrite information still in use) and add them to the {@code errors} list
 690    * and continue verification.
 691    *
 692    * <p>The property that caused the error is not reset here as the listeners attached to the search should be notified of the error first.
 693    * This becomes especially problematic if one of the listeners caused the property violation, as which point it would get  confused
 694    * if the {@code propertyViolated()} notification happens after the property is reset.
 695    *
 696    * @param property The property that causes the error
 697    * @param path The path corresponding to the error
 698    * @param threadList The list of thread information corresponding to the error
 699    */
 700   public void error (Property property, Path path, ThreadList threadList) {
 701
 702     if (getAllErrors) {
 703        // otherwise we are going to overwrite it if we go on
 704       try {
 705         property = property.clone();
 706         path = path.clone();
 707         threadList = (ThreadList) threadList.clone(); // this makes it a snapshot (deep) clone
 708       } catch (CloneNotSupportedException cnsx){
 709         throw new JPFException("failed to clone error information: " + cnsx);
 710       }
 711       done = false;
 712
 713     } else {
 714       done = true;
 715     }
 716
 717     currentError = new Error(errors.size()+1, property, path, threadList);
 718
 719     errors.add(currentError);
 720
 721   }
 722
 723   /**
 724    * Resets all properties, returning violated properties to their default states.
 725    */
 726   public void resetProperties(){
 727     for (Property p : properties) {
 728       p.reset();
 729     }
 730   }
 731
 732   /**
 733    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has advanced states.
 734    */
 735   protected void notifyStateAdvanced () {
 736     try {
 737       for (int i = 0; i < listeners.length; i++) {
 738         listeners[i].stateAdvanced(this);
 739       }
 740       if (reporter != null){
 741         // reporter always comes last to ensure all listeners have been notified
 742         reporter.stateAdvanced(this);
 743       }
 744     } catch (Throwable t) {
 745       throw new JPFListenerException("exception during stateAdvanced() notification", t);
 746     }
 747   }
 748
 749   /**
 750    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has finished processing
 751    * the current state.
 752    */
 753   protected void notifyStateProcessed() {
 754     try {
 755       for (int i = 0; i < listeners.length; i++) {
 756         listeners[i].stateProcessed(this);
 757       }
 758       if (reporter != null){
 759         reporter.stateProcessed(this);
 760       }
 761     } catch (Throwable t) {
 762       throw new JPFListenerException("exception during stateProcessed() notification", t);
 763     }
 764   }
 765
 766   /**
 767    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has stored the current state.
 768    */
 769   protected void notifyStateStored() {
 770     try {
 771       for (int i = 0; i < listeners.length; i++) {
 772         listeners[i].stateStored(this);
 773       }
 774       if (reporter != null){
 775         reporter.stateStored(this);
 776       }
 777     } catch (Throwable t) {
 778       throw new JPFListenerException("exception during stateStored() notification", t);
 779     }
 780   }
 781
 782   /**
 783    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has restored a currently
 784    * stored state.
 785    */
 786   protected void notifyStateRestored() {
 787     try {
 788       for (int i = 0; i < listeners.length; i++) {
 789         listeners[i].stateRestored(this);
 790       }
 791       if (reporter != null){
 792         reporter.stateRestored(this);
 793       }
 794     } catch (Throwable t) {
 795       throw new JPFListenerException("exception during stateRestored() notification", t);
 796     }
 797   }
 798
 799   /**
 800    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has backtracked to a
 801    * previous state.
 802    */
 803   protected void notifyStateBacktracked() {
 804     try {
 805       for (int i = 0; i < listeners.length; i++) {
 806         listeners[i].stateBacktracked(this);
 807       }
 808       if (reporter != null){
 809         reporter.stateBacktracked(this);
 810       }
 811     } catch (Throwable t) {
 812       throw new JPFListenerException("exception during stateBacktracked() notification", t);
 813     }
 814   }
 815
 816   /**
 817    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has purged the current state.
 818    */
 819   protected void notifyStatePurged() {
 820     try {
 821       for (int i = 0; i < listeners.length; i++) {
 822         listeners[i].statePurged(this);
 823       }
 824       if (reporter != null){
 825         reporter.statePurged(this);
 826       }
 827     } catch (Throwable t) {
 828       throw new JPFListenerException("exception during statePurged() notification", t);
 829     }
 830   }
 831
 832   /**
 833    * Notifies the {@code SearchListener} objects in the {@code listeners} list that a probe request has been triggered during
 834    * verification.
 835    */
 836   public void notifySearchProbed() {
 837     try {
 838       for (int i = 0; i < listeners.length; i++) {
 839         listeners[i].searchProbed(this);
 840       }
 841       if (reporter != null){
 842         reporter.searchProbed(this);
 843       }
 844     } catch (Throwable t) {
 845       throw new JPFListenerException("exception during searchProbed() notification", t);
 846     }
 847   }
 848
 849
 850   /**
 851    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has encountered a property
 852    * violation
 853    */
 854   protected void notifyPropertyViolated() {
 855     try {
 856       for (int i = 0; i < listeners.length; i++) {
 857         listeners[i].propertyViolated(this);
 858       }
 859       if (reporter != null){
 860         reporter.propertyViolated(this);
 861       }
 862     } catch (Throwable t) {
 863       throw new JPFListenerException("exception during propertyViolated() notification", t);
 864     }
 865
 866     // reset properties if getAllErrors is set
 867     if (getAllErrors){
 868       resetProperties();
 869     }
 870   }
 871
 872   /**
 873    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has begun verification.
 874    */
 875   protected void notifySearchStarted() {
 876     try {
 877       for (int i = 0; i < listeners.length; i++) {
 878         listeners[i].searchStarted(this);
 879       }
 880       if (reporter != null){
 881         reporter.searchStarted(this);
 882       }
 883     } catch (Throwable t) {
 884       throw new JPFListenerException("exception during searchStarted() notification", t);
 885     }
 886   }
 887
 888   /**
 889    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has encountered a
 890    * search constraint. The {@code details} String outlines the search constraint that was hit as well as any other
 891    * relevant information.
 892    *
 893    * @param details Information regarding the recent search constraint that was encountered.
 894    */
 895   public void notifySearchConstraintHit(String details) {
 896     try {
 897       lastSearchConstraint = details;
 898       for (int i = 0; i < listeners.length; i++) {
 899         listeners[i].searchConstraintHit(this);
 900       }
 901       if (reporter != null){
 902         reporter.searchConstraintHit(this);
 903       }
 904     } catch (Throwable t) {
 905       throw new JPFListenerException("exception during searchConstraintHit() notification", t);
 906     }
 907   }
 908
 909   /**
 910    * Notifies the {@code SearchListener} objects in the {@code listeners} list that the search loop has finished verification.
 911    */
 912   protected void notifySearchFinished() {
 913     try {
 914       for (int i = 0; i < listeners.length; i++) {
 915         listeners[i].searchFinished(this);
 916       }
 917       if (reporter != null){
 918         reporter.searchFinished(this);
 919       }
 920     } catch (Throwable t) {
 921       throw new JPFListenerException("exception during searchFinished() notification", t);
 922     }
 923   }
 924
 925   /**
 926    * Requests that the virtual machine move to the next unvisited state below the current one in the search tree.
 927    * {@code forward} along with {@code backtrack} constitute the two methods that are generally used to advance
 928    * the search algorithm during verification.
 929    *
 930    * @return true if a state exists and the virtual machine can move to it, false if the state does not exist
 931    * or if it was previously explored.
 932    * @see #backtrack()
 933    */
 934   protected boolean forward () {
 935     currentError = null;
 936
 937     boolean ret = vm.forward();
 938
 939     checkPropertyViolation();
 940     return ret;
 941   }
 942
 943   /**
 944    * Requests that the virtual machine move to the previous state in the search tree. {@code backtrack} along
 945    * with {@code forward} constitute the two methods that are generally used to advance the search algorithm
 946    * during verification.
 947    *
 948    * @return true if the backtrack to the previous state was successful, false otherwise
 949    */
 950   protected boolean backtrack () {
 951     return vm.backtrack();
 952   }
 953
 954   /**
 955    * Requests that the virtual machine sets whether the current state should be ignored in all future iterations
 956    * of the search loop. This should not be used without cause as it causes the search tree to be pruned whenever
 957    * it is called, which is expensive, especially in larger trees.
 958    *
 959    * @param cond Whether or not the current state should be ignored
 960    */
 961   public void setIgnoredState (boolean cond) {
 962     vm.ignoreState(cond);
 963   }
 964
 965   /**
 966    * Restores a previously stored virtual machine state.
 967    *
 968    * <p>By default this method is not supported, and therefore requires implementation logic in child classes.
 969    *
 970    * @param state The stored state to be restored
 971    */
 972   protected void restoreState (State state) {
 973     // not supported by default
 974   }
 975
 976   /**
 977    * Sets {@code done} to true in order to terminate the search loop.
 978    *
 979    * <p>Can be used by listeners to terminate the search.
 980    *
 981    */
 982   public void terminate () {
 983     done = true;
 984   }
 985
 986   /**
 987    * Sets the depth of the specified state given its state id.
 988    *
 989    * <p>When the depth of the state is set, it is set as depth + 1. This is to differentiate between
 990    * states that have had their depths set, and states that have not (in which case their default depth
 991    * will be 0).
 992    *
 993    * @param stateId The state in question
 994    * @param depth The new depth to set for the state
 995    */
 996   protected void setStateDepth (int stateId, int depth) {
 997     stateDepth.set(stateId, depth + 1);
 998   }
 999
1000
1001   /**
1002    * Returns the saved depth of the specified state given its state id.
1003    *
1004    * <p>If the state in question has not had its state depth set previously, then it will by default have
1005    * a depth that is less than or equal to 0. Otherwise if the state has been visited, the depth will be
1006    * returned.
1007    *
1008    * @param stateId The state to return the depth of
1009    * @return The depth of the specified state
1010    * @throws JPFException If the state has not been visited in the past
1011    */
1012   public int getStateDepth (int stateId) {
1013     int depthPlusOne = stateDepth.get(stateId);
1014     if (depthPlusOne <= 0) {
1015       throw new JPFException("Asked for depth of unvisited state");
1016     } else {
1017       return depthPlusOne - 1;
1018     }
1019   }
1020
1021   /**
1022    * Check if there is the minimum amount of free memory left or more. If not, we would rather stop in time
1023    * (with a threshold amount left) in order to report something useful, and not just end verification silently
1024    * with a OutOfMemoryError (which is not handled too gracefully by most VMs)
1025    *
1026    * <p>If the minimum amount of memory has been reached, the method will first try to activate garbage collection
1027    * and then check again if that made a difference. If the amount of memory available is still less than the
1028    * minimum amount of memory, then we return false.
1029    *
1030    * @return true if we have more memory than the minimum free memory, false otherwise.
1031    */
1032   public boolean checkStateSpaceLimit () {
1033     Runtime rt = Runtime.getRuntime();
1034
1035     long avail = rt.freeMemory();
1036
1037     // we could also just check for a max number of states, but what really
1038     // limits us is the memory required to store states
1039
1040     if (avail < minFreeMemory) {
1041       // try to collect first
1042       rt.gc();
1043       avail = rt.freeMemory();
1044
1045       if (avail < minFreeMemory) {
1046         // Ok, we give up, threshold reached
1047         return false;
1048       }
1049     }
1050
1051     return true;
1052   }
1053 }
1054