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.JPF;
22 import gov.nasa.jpf.ListenerAdapter;
23 import gov.nasa.jpf.search.DFSearch;
24 import gov.nasa.jpf.search.Search;
25 import gov.nasa.jpf.search.heuristic.BFSHeuristic;
26 import gov.nasa.jpf.vm.ElementInfo;
27 import gov.nasa.jpf.vm.VM;
28 import gov.nasa.jpf.vm.ThreadInfo;
30 import java.util.ArrayList;
31 import java.util.Arrays;
32 import java.util.HashMap;
33 import java.util.List;
34 import java.util.logging.Level;
35 import java.util.logging.Logger;
38 * A listener that tracks information about the stack depth of when a lock is first acquired. If
40 * Writing a test for this class is very difficult. Hence, a lot of asserts are added.
42 public class LockedStackDepth extends ListenerAdapter
44 private static final Logger s_logger = JPF.getLogger(LockedStackDepth.class.getName());
45 private static final Integer EMPTY[] = new Integer[0];
46 private static final int THREAD_FLAG = 0x80000000;
48 private final HashMap<Integer, Operation> m_operations = new HashMap<Integer, Operation>();
49 private final HashMap<Integer, Integer> m_state = new HashMap<Integer, Integer>();
50 private final HashMap<Operation, Integer> m_index = new HashMap<Operation, Integer>();
51 private final ArrayList<Operation> m_apply = new ArrayList<Operation>();
52 private Operation m_current;
54 public int getLockedStackDepth(ElementInfo lock)
59 lockIndex = lock.getObjectRef();
60 result = m_state.get(makeKey(lock));
62 if (s_logger.isLoggable(Level.INFO))
63 s_logger.info("Depth = " + result + " | Lock Index = " + lockIndex + " | Lock = " + lock);
73 public List<ElementInfo> getLockedInTopFrame(ThreadInfo thread)
75 ArrayList<ElementInfo> result;
79 threadDepth = thread.getStackDepth();
80 result = new ArrayList<ElementInfo>();
82 for (Integer key : m_state.keySet())
87 if (threadDepth != m_state.get(key))
90 lock = thread.getElementInfo(key);
95 if (!lock.isLockedBy(thread))
105 public void objectLocked(VM vm, ThreadInfo thread, ElementInfo ei)
114 depth = new Operation(thread, null).getOldDepth();
117 depth = thread.getStackDepth();
119 assert thread.getLockCount() == 0;
120 assert thread.getLockObject() == null;
121 assert lock.isLockedBy(thread);
123 if (m_state.containsKey(makeKey(lock))) // So that a breakpoint on the next line will only get hit if the assert will trigger.
124 assert !m_state.containsKey(makeKey(lock));
126 assert !m_state.containsKey(makeKey(thread));
129 new Operation(lock, depth);
133 public void objectUnlocked(VM vm, ThreadInfo thread, ElementInfo ei)
141 depth = new Operation(lock, null).getOldDepth();
143 assert !m_state.containsKey(makeKey(lock));
144 assert !m_state.containsKey(makeKey(thread));
147 if (thread.isWaiting())
149 assert !lock.isLockedBy(thread);
150 assert lock.getLockCount() == 0;
151 assert thread.getLockCount() > 0;
152 assert thread.getLockObject() == lock;
153 new Operation(thread, depth);
157 assert lock.isLockedBy(thread);
158 assert lock.getLockCount() > 0;
159 assert thread.getLockCount() == 0;
160 assert thread.getLockObject() == null;
165 public void searchStarted(Search search)
167 m_operations.clear();
174 public void stateAdvanced(Search search)
178 id = search.getStateId();
180 if (!m_operations.containsKey(id)) // Don't overwrite the original chain of Operations to get to the same state. The original chain is more likely to be shorter.
181 m_operations.put(id, m_current);
183 if (s_logger.isLoggable(Level.FINE))
184 s_logger.fine("State Advanced: " + id);
190 public void stateProcessed(Search search)
194 if (!(search instanceof DFSearch)) // Can't remove from m_operations since Search could go back to the state.
195 if (!(search instanceof BFSHeuristic))
198 id = search.getStateId();
200 m_operations.remove(id); // DFSearch won't ever revisit this state. It is safe to remove and allow for cleanup.
202 if (s_logger.isLoggable(Level.FINE))
203 s_logger.fine("State Processed: " + id);
207 public void stateBacktracked(Search search)
213 public void stateRestored(Search search)
218 private void switchTo(Search search)
223 id = search.getStateId();
224 next = m_operations.get(id);
226 if (s_logger.isLoggable(Level.FINE))
227 s_logger.fine("State Switching: " + id);
229 assert (id <= 0) || (m_operations.containsKey(id));
237 if (s_logger.isLoggable(Level.FINE))
238 s_logger.fine("State Switched: " + id);
241 private void switchTo(Operation next)
247 for (operation = next; operation != null; operation = operation.getParent()) // Go through all of the operations leading back to the root.
249 m_index.put(operation, m_apply.size()); // Keep track of the index into m_apply where operation is found
250 m_apply.add(operation);
255 for (operation = m_current; operation != null; operation = operation.getParent()) // Go through all of the operations leading back to the root.
257 index = m_index.get(operation);
259 if (index != null) // If a common ancestor is found, stop going back.
262 operation.revert(); // Revert the operation since it isn't common to both states.
266 index = m_apply.size(); // No common ancestor found. Must apply all of the operations.
268 for (i = index; --i >= 0; ) // Apply all of the operations required to get back to the "next" state.
269 m_apply.get(i).apply();
275 private void logState()
277 StringBuilder message;
279 Integer key, keys[], depth;
282 if (!s_logger.isLoggable(Level.FINER))
285 message = new StringBuilder();
286 keys = m_state.keySet().toArray(EMPTY);
289 message.append("State | Size = ");
290 message.append(keys.length);
292 for (i = 0; i < keys.length; i++)
295 depth = m_state.get(key);
297 if ((key & THREAD_FLAG) != 0)
302 message.append('\n');
303 message.append("Depth = ");
304 message.append(depth);
305 message.append(" | Key = ");
306 message.append(key & ~THREAD_FLAG);
307 message.append(" | ");
308 message.append(type);
311 s_logger.finer(message.toString());
314 private void logStack(ThreadInfo thread)
316 if (!s_logger.isLoggable(Level.FINEST))
319 s_logger.finest(thread.getStackTrace());
322 private static int makeKey(ElementInfo lock)
324 return(lock.getObjectRef());
327 private static int makeKey(ThreadInfo thread)
329 return(thread.getThreadObjectRef() ^ THREAD_FLAG);
332 private class Operation
334 private final Operation m_parent;
335 private final Integer m_key;
336 private final Integer m_oldDepth;
337 private final Integer m_newDepth;
339 public Operation(ElementInfo lock, Integer newDepth)
341 this(makeKey(lock), newDepth);
344 public Operation(ThreadInfo thread, Integer newDepth)
346 this(makeKey(thread), newDepth);
349 private Operation(Integer key, Integer newDepth)
351 m_parent = m_current;
354 m_newDepth = newDepth;
355 m_oldDepth = m_state.get(key);
360 public Operation getParent()
365 public Integer getOldDepth()
370 public Integer getNewDepth()
387 private void change(Integer depth)
392 m_state.remove(m_key);
395 previous = m_state.put(m_key, depth);
397 assert previous == null;
401 private void log(String header)
403 String message, subheader, depthStr, type;
406 if (!s_logger.isLoggable(Level.FINE))
409 if (m_newDepth != null)
416 subheader = "Remove";
420 depthStr = String.valueOf(depth);
422 switch (depthStr.length())
424 case 1: depthStr = " " + depthStr; break;
425 case 2: depthStr = " " + depthStr; break;
426 case 3: depthStr = " " + depthStr; break;
430 if ((m_key & THREAD_FLAG) != 0)
435 message = header + " " + subheader + " | Depth = " + depthStr + " | Key = " + (m_key & ~THREAD_FLAG) + " | " + type;
437 s_logger.fine(message);