src/main/gov/nasa/jpf/listener/OverlappingMethodAnalyzer.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.vm.ElementInfo;
  24 import gov.nasa.jpf.vm.MethodInfo;
  25 import gov.nasa.jpf.vm.ThreadInfo;
  26
  27 import java.io.PrintWriter;
  28 import java.util.ArrayDeque;
  29 import java.util.Deque;
  30 import java.util.HashMap;
  31 import java.util.Iterator;
  32 import java.util.Map;
  33
  34 /**
  35  * this is a specialized MethodAnalyzer that looks for overlapping method
  36  * calls on the same object from different threads.
  37  *
  38  * <2do> transition reporting does not work yet
  39  */
  40 public class OverlappingMethodAnalyzer extends MethodAnalyzer {
  41
  42   public OverlappingMethodAnalyzer (Config config, JPF jpf){
  43     super(config,jpf);
  44   }
  45
  46   MethodOp getReturnOp (MethodOp op, boolean withinSameThread){
  47     MethodInfo mi = op.mi;
  48     int stateId = op.stateId;
  49     int stackDepth = op.stackDepth;
  50     ElementInfo ei = op.ei;
  51     ThreadInfo ti = op.ti;
  52
  53     for (MethodOp o = op.p; o != null; o = o.p){
  54       if (withinSameThread && o.ti != ti){
  55         break;
  56       }
  57
  58       if ((o.mi == mi) && (o.ti == ti) && (o.stackDepth == stackDepth) && (o.ei == ei)){
  59         return o;
  60       }
  61     }
  62
  63     return null;
  64   }
  65
  66   // check if there is an open exec from another thread for the same ElementInfo
  67   boolean isOpenExec (HashMap<ThreadInfo,Deque<MethodOp>> openExecs, MethodOp op){
  68     ThreadInfo ti = op.ti;
  69     ElementInfo ei = op.ei;
  70
  71     for (Map.Entry<ThreadInfo, Deque<MethodOp>> e : openExecs.entrySet()) {
  72       if (e.getKey() != ti) {
  73         Deque<MethodOp> s = e.getValue();
  74         for (Iterator<MethodOp> it = s.descendingIterator(); it.hasNext();) {
  75           MethodOp o = it.next();
  76           if (o.ei == ei) {
  77             return true;
  78           }
  79         }
  80       }
  81     }
  82
  83     return false;
  84   }
  85
  86   // clean up (if necessary) - both RETURNS and exceptions
  87   void cleanUpOpenExec (HashMap<ThreadInfo,Deque<MethodOp>> openExecs, MethodOp op){
  88     ThreadInfo ti = op.ti;
  89     int stackDepth = op.stackDepth;
  90
  91     Deque<MethodOp> stack = openExecs.get(ti);
  92     if (stack != null && !stack.isEmpty()) {
  93       for (MethodOp o = stack.peek(); o != null && o.stackDepth >= stackDepth; o = stack.peek()) {
  94         stack.pop();
  95       }
  96     }
  97   }
  98
  99   void addOpenExec (HashMap<ThreadInfo,Deque<MethodOp>> openExecs, MethodOp op){
 100     ThreadInfo ti = op.ti;
 101     Deque<MethodOp> stack = openExecs.get(ti);
 102
 103     if (stack == null){
 104       stack = new ArrayDeque<MethodOp>();
 105       stack.push(op);
 106       openExecs.put(ti, stack);
 107
 108     } else {
 109       stack.push(op);
 110     }
 111   }
 112
 113   @Override
 114   void printOn (PrintWriter pw) {
 115     MethodOp start = firstOp;
 116
 117     HashMap<ThreadInfo,Deque<MethodOp>> openExecs = new HashMap<ThreadInfo,Deque<MethodOp>>();
 118
 119     int lastStateId  = -1;
 120     int lastTid = start.ti.getId();
 121
 122     for (MethodOp op = start; op != null; op = op.p) {
 123
 124       cleanUpOpenExec(openExecs, op);
 125
 126       if (op.isMethodEnter()) {  // EXEC or CALL_EXEC
 127         MethodOp retOp = getReturnOp(op, true);
 128         if (retOp != null) { // completed, skip
 129           if (!isOpenExec(openExecs, op)) {
 130             op = retOp;
 131             lastStateId = op.stateId;
 132             continue;
 133           }
 134         } else { // this is an open method exec, record it
 135           addOpenExec(openExecs, op);
 136         }
 137       }
 138
 139       op = consolidateOp(op);
 140
 141       if (showTransition) {
 142         if (op.stateId != lastStateId) {
 143           if (lastStateId >= 0){
 144             pw.print("------------------------------------------ #");
 145             pw.println(lastStateId);
 146           }
 147         }
 148         lastStateId = op.stateId;
 149
 150       } else {
 151         int tid = op.ti.getId();
 152         if (tid != lastTid) {
 153           lastTid = tid;
 154           pw.println("------------------------------------------");
 155         }
 156       }
 157
 158       op.printOn(pw, this);
 159       pw.println();
 160     }
 161   }
 162
 163   MethodOp consolidateOp (MethodOp op){
 164     for (MethodOp o = op.p; o != null; o = o.p){
 165       if (showTransition && (o.stateId != op.stateId)){
 166         break;
 167       }
 168       if (o.isSameMethod(op)){
 169         switch (o.type) {
 170           case RETURN:
 171             switch (op.type){
 172               case CALL_EXECUTE:
 173                 op = o.clone(OpType.CALL_EXEC_RETURN); break;
 174               case EXECUTE:
 175                 op = o.clone(OpType.EXEC_RETURN); break;
 176             }
 177             break;
 178           case EXEC_RETURN:
 179             switch (op.type){
 180               case CALL:
 181                 op = o.clone(OpType.CALL_EXEC_RETURN); break;
 182             }
 183             break;
 184           case CALL_EXECUTE:  // simple loop
 185             switch (op.type){
 186               case CALL_EXEC_RETURN:
 187                 op = o;
 188             }
 189             break;
 190         }
 191       } else {
 192         break;
 193       }
 194     }
 195
 196     return op;
 197   }
 198 }