2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.listener;
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;
30 import java.util.logging.Logger;
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.
38 * One can set how many back-edges to consider before breaking, but by default it is 1
41 public class SimpleIdleFilter extends ListenerAdapter {
43 static Logger log = JPF.getLogger("gov.nasa.jpf.listener.SimpleIdleFilter");
45 static class ThreadStat {
56 ThreadStat(String tname) {
61 ObjVector<ThreadStat> threadStats = new ObjVector<ThreadStat>();
67 // ----------------------------------------------------- SearchListener
70 public SimpleIdleFilter(Config config) {
71 maxBackJumps = config.getInt("idle.max_backjumps", 1);
75 public void stateAdvanced(Search search) {
77 ts.loopStackDepth = 0;
78 ts.loopStartPc = ts.loopEndPc = 0;
82 public void stateBacktracked(Search search) {
84 ts.loopStackDepth = 0;
85 ts.loopStartPc = ts.loopEndPc = 0;
88 // ----------------------------------------------------- VMListener interface
90 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
92 if (!executedInsn.isBackJump()) { // Put this test first for a performance optimization.
97 ts = threadStats.get(tid);
99 ts = new ThreadStat(ti.getName());
100 threadStats.set(tid, ts);
105 int loopStackDepth = ti.getStackDepth();
106 int loopPc = nextInsn.getPosition();
108 if ((loopStackDepth != ts.loopStackDepth) || (loopPc != ts.loopStartPc)) {
110 ts.loopStackDepth = loopStackDepth;
111 ts.loopStartPc = loopPc;
112 ts.loopEndPc = executedInsn.getPosition();
115 if (ts.backJumps > maxBackJumps) {
116 ti.reschedule("idleFilter"); // this breaks the executePorStep loop