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.vm.ElementInfo;
24 import gov.nasa.jpf.vm.MethodInfo;
25 import gov.nasa.jpf.vm.ThreadInfo;
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;
35 * this is a specialized MethodAnalyzer that looks for overlapping method
36 * calls on the same object from different threads.
38 * <2do> transition reporting does not work yet
40 public class OverlappingMethodAnalyzer extends MethodAnalyzer {
42 public OverlappingMethodAnalyzer (Config config, JPF jpf){
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;
53 for (MethodOp o = op.p; o != null; o = o.p){
54 if (withinSameThread && o.ti != ti){
58 if ((o.mi == mi) && (o.ti == ti) && (o.stackDepth == stackDepth) && (o.ei == ei)){
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;
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();
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;
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()) {
99 void addOpenExec (HashMap<ThreadInfo,Deque<MethodOp>> openExecs, MethodOp op){
100 ThreadInfo ti = op.ti;
101 Deque<MethodOp> stack = openExecs.get(ti);
104 stack = new ArrayDeque<MethodOp>();
106 openExecs.put(ti, stack);
114 void printOn (PrintWriter pw) {
115 MethodOp start = firstOp;
117 HashMap<ThreadInfo,Deque<MethodOp>> openExecs = new HashMap<ThreadInfo,Deque<MethodOp>>();
119 int lastStateId = -1;
120 int lastTid = start.ti.getId();
122 for (MethodOp op = start; op != null; op = op.p) {
124 cleanUpOpenExec(openExecs, op);
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)) {
131 lastStateId = op.stateId;
134 } else { // this is an open method exec, record it
135 addOpenExec(openExecs, op);
139 op = consolidateOp(op);
141 if (showTransition) {
142 if (op.stateId != lastStateId) {
143 if (lastStateId >= 0){
144 pw.print("------------------------------------------ #");
145 pw.println(lastStateId);
148 lastStateId = op.stateId;
151 int tid = op.ti.getId();
152 if (tid != lastTid) {
154 pw.println("------------------------------------------");
158 op.printOn(pw, this);
163 MethodOp consolidateOp (MethodOp op){
164 for (MethodOp o = op.p; o != null; o = o.p){
165 if (showTransition && (o.stateId != op.stateId)){
168 if (o.isSameMethod(op)){
173 op = o.clone(OpType.CALL_EXEC_RETURN); break;
175 op = o.clone(OpType.EXEC_RETURN); break;
181 op = o.clone(OpType.CALL_EXEC_RETURN); break;
184 case CALL_EXECUTE: // simple loop
186 case CALL_EXEC_RETURN: