src/main/gov/nasa/jpf/listener/SimpleIdleFilter.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
  19 package gov.nasa.jpf.listener;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.ListenerAdapter;
  24 import gov.nasa.jpf.search.Search;
  25 import gov.nasa.jpf.util.ObjVector;
  26 import gov.nasa.jpf.vm.Instruction;
  27 import gov.nasa.jpf.vm.VM;
  28 import gov.nasa.jpf.vm.ThreadInfo;
  29
  30 import java.util.logging.Logger;
  31
  32
  33 /**
  34  * This is the simple version of IdleFilter. This one simply breaks all back-edges
  35  * encountered to make sure JPF's partial-order reduction doesn't add meaningless
  36  * transitions forever. This is our dual of the cycle-proviso in classic po-reduction theory.
  37  *
  38  *  One can set how many back-edges to consider before breaking, but by default it is 1
  39  *
  40  */
  41 public class SimpleIdleFilter extends ListenerAdapter {
  42
  43           static Logger log = JPF.getLogger("gov.nasa.jpf.listener.SimpleIdleFilter");
  44
  45           static class ThreadStat {
  46             String tname;
  47
  48             int backJumps;
  49
  50             int loopStartPc;
  51
  52             int loopEndPc;
  53
  54             int loopStackDepth;
  55
  56             ThreadStat(String tname) {
  57               this.tname = tname;
  58             }
  59           }
  60
  61           ObjVector<ThreadStat> threadStats = new ObjVector<ThreadStat>();
  62
  63           ThreadStat ts;
  64
  65           int maxBackJumps;
  66
  67           // ----------------------------------------------------- SearchListener
  68           // interface
  69
  70           public SimpleIdleFilter(Config config) {
  71             maxBackJumps = config.getInt("idle.max_backjumps", 1);
  72           }
  73
  74           @Override
  75           public void stateAdvanced(Search search) {
  76             ts.backJumps = 0;
  77             ts.loopStackDepth = 0;
  78             ts.loopStartPc = ts.loopEndPc = 0;
  79           }
  80
  81           @Override
  82           public void stateBacktracked(Search search) {
  83             ts.backJumps = 0;
  84             ts.loopStackDepth = 0;
  85             ts.loopStartPc = ts.loopEndPc = 0;
  86           }
  87
  88           // ----------------------------------------------------- VMListener interface
  89           @Override
  90           public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
  91
  92        if (!executedInsn.isBackJump()) {     // Put this test first for a performance optimization.
  93          return;
  94        }
  95
  96             int tid = ti.getId();
  97             ts = threadStats.get(tid);
  98             if (ts == null) {
  99               ts = new ThreadStat(ti.getName());
 100               threadStats.set(tid, ts);
 101             }
 102
 103        ts.backJumps++;
 104
 105        int loopStackDepth = ti.getStackDepth();
 106        int loopPc = nextInsn.getPosition();
 107
 108        if ((loopStackDepth != ts.loopStackDepth) || (loopPc != ts.loopStartPc)) {
 109          // new loop, reset
 110          ts.loopStackDepth = loopStackDepth;
 111          ts.loopStartPc = loopPc;
 112          ts.loopEndPc = executedInsn.getPosition();
 113          ts.backJumps = 0;
 114        } else {
 115          if (ts.backJumps > maxBackJumps) {
 116            ti.reschedule("idleFilter"); // this breaks the executePorStep loop
 117          }
 118        }
 119           }
 120 }