src/main/gov/nasa/jpf/listener/NoStateCycles.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.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.PropertyListenerAdapter;
  22 import gov.nasa.jpf.search.Search;
  23 import gov.nasa.jpf.vm.VM;
  24 import gov.nasa.jpf.vm.SystemState;
  25
  26 import java.util.ArrayList;
  27 import java.util.HashSet;
  28
  29
  30 /**
  31  * If there is a cycle in the states of the program, JPF doesn't execute the
  32  * already visited states.  A cycle in the states may represent the ability for
  33  * the program to hang.  This property finds and outputs cycles in the states
  34  * so that they may be investigated.
  35  *
  36  * The following might need to be added to listener property...
  37  *   gov.nasa.jpf.tools.SimpleIdleFilter
  38  *   gov.nasa.jpf.tools.IdleFilter
  39  */
  40
  41 public class NoStateCycles extends PropertyListenerAdapter {
  42
  43   private final HashSet<Integer>   m_inStack = new HashSet<Integer>();
  44   private final ArrayList<Integer> m_stack   = new ArrayList<Integer>();
  45
  46   private int m_cycleFound = -1;
  47   private int m_stackPos   = -1;
  48
  49   public NoStateCycles(Config config) {
  50     if (!config.getString("search.class").equals("gov.nasa.jpf.search.DFSearch"))
  51       config.throwException("search.class must be gov.nasa.jpf.search.DFSearch");   // Or any class which does a depth first search.
  52   }
  53
  54   @Override
  55    public void stateAdvanced(Search search) {
  56      SystemState state;
  57      Integer id;
  58
  59      state = search.getVM().getSystemState();
  60      if (state.isInitState())
  61        return;
  62
  63      id = state.getId();
  64
  65      if ((m_stackPos < 0) && (m_inStack.contains(id))) {
  66        m_cycleFound = id;
  67
  68        for (m_stackPos = m_stack.size() - 1; m_stackPos >= 0; m_stackPos--)
  69          if (m_stack.get(m_stackPos).equals(id))
  70            break;
  71      }
  72
  73      m_stack.add(id);
  74      m_inStack.add(id);
  75    }
  76
  77   @Override
  78    public void stateBacktracked(Search search) {
  79      Integer id;
  80      int pos;
  81
  82      pos = m_stack.size() - 1;
  83      id  = m_stack.remove(pos);
  84      m_inStack.remove(id);
  85
  86      if (m_stackPos >= pos)
  87        m_stackPos = -1;
  88    }
  89
  90   @Override
  91    public boolean check(Search search, VM vm) {
  92      return(m_cycleFound < 0);
  93    }
  94
  95    @Override
  96    public void reset () {
  97      m_cycleFound = -1;
  98    }
  99
 100    @Override
 101   public String getErrorMessage () {
 102      StringBuilder result;
 103      int i, id;
 104
 105      result = new StringBuilder();
 106      result.append("States:\n");
 107
 108      for (i = m_stack.size() - 1; i >= 0; i--) {
 109        id = m_stack.get(i);
 110
 111        result.append("  ");
 112        result.append(id);
 113        result.append('\n');
 114
 115        if (id == m_cycleFound)
 116          break;
 117      }
 118
 119      return(result.toString());
 120    }
 121
 122    @Override
 123   public String getExplanation () {
 124      return("Finds cycles in states.  A cycle suggests that the program might be able to hang.");
 125    }
 126 }