src/main/gov/nasa/jpf/listener/LockedStackDepth.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.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;
  29
  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;
  36
  37 /**
  38  * A listener that tracks information about the stack depth of when a lock is first acquired.  If
  39  *
  40  * Writing a test for this class is very difficult.  Hence, a lot of asserts are added.
  41  */
  42 public class LockedStackDepth extends ListenerAdapter
  43 {
  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;
  47
  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;
  53
  54    public int getLockedStackDepth(ElementInfo lock)
  55    {
  56       Integer result;
  57       int lockIndex;
  58
  59       lockIndex = lock.getObjectRef();
  60       result    = m_state.get(makeKey(lock));
  61
  62       if (s_logger.isLoggable(Level.INFO))
  63          s_logger.info("Depth = " + result + " | Lock Index = " + lockIndex + " | Lock = " + lock);
  64
  65       if (result == null)
  66          return(-1);
  67
  68       assert result >= 0;
  69
  70       return(result);
  71    }
  72
  73    public List<ElementInfo> getLockedInTopFrame(ThreadInfo thread)
  74    {
  75       ArrayList<ElementInfo> result;
  76       ElementInfo lock;
  77       int threadDepth;
  78
  79       threadDepth = thread.getStackDepth();
  80       result      = new ArrayList<ElementInfo>();
  81
  82       for (Integer key : m_state.keySet())
  83       {
  84          if (key < 0)
  85             continue;
  86
  87          if (threadDepth != m_state.get(key))
  88             continue;
  89
  90          lock = thread.getElementInfo(key);
  91
  92          if (lock == null)
  93             continue;
  94
  95          if (!lock.isLockedBy(thread))
  96             continue;
  97
  98          result.add(lock);
  99       }
 100
 101       return(result);
 102    }
 103
 104    @Override
 105    public void objectLocked(VM vm, ThreadInfo thread, ElementInfo ei)
 106    {
 107       ElementInfo lock;
 108       Integer depth;
 109
 110       lock   = ei;
 111
 112       logStack(thread);
 113
 114       depth  = new Operation(thread, null).getOldDepth();
 115
 116       if (depth == null)
 117          depth = thread.getStackDepth();
 118
 119       assert thread.getLockCount() == 0;
 120       assert thread.getLockObject() == null;
 121       assert lock.isLockedBy(thread);
 122
 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));
 125
 126       assert !m_state.containsKey(makeKey(thread));
 127       assert depth >= 0;
 128
 129       new Operation(lock, depth);
 130    }
 131
 132    @Override
 133    public void objectUnlocked(VM vm, ThreadInfo thread, ElementInfo ei)
 134    {
 135       ElementInfo lock;
 136       Integer depth;
 137
 138       logStack(thread);
 139
 140       lock   = ei;
 141       depth  = new Operation(lock, null).getOldDepth();
 142
 143       assert !m_state.containsKey(makeKey(lock));
 144       assert !m_state.containsKey(makeKey(thread));
 145       assert depth >= 0;
 146
 147       if (thread.isWaiting())
 148       {
 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);
 154       }
 155       else
 156       {
 157          assert lock.isLockedBy(thread);
 158          assert lock.getLockCount() > 0;
 159          assert thread.getLockCount() == 0;
 160          assert thread.getLockObject() == null;
 161       }
 162    }
 163
 164    @Override
 165    public void searchStarted(Search search)
 166    {
 167       m_operations.clear();
 168       m_state.clear();
 169
 170       m_current = null;
 171    }
 172
 173    @Override
 174    public void stateAdvanced(Search search)
 175    {
 176       Integer id;
 177
 178       id = search.getStateId();
 179
 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);
 182
 183       if (s_logger.isLoggable(Level.FINE))
 184          s_logger.fine("State Advanced: " + id);
 185
 186       logState();
 187    }
 188
 189    @Override
 190    public void stateProcessed(Search search)
 191    {
 192       Integer id;
 193
 194       if (!(search instanceof DFSearch))  // Can't remove from m_operations since Search could go back to the state.
 195          if (!(search instanceof BFSHeuristic))
 196             return;
 197
 198       id = search.getStateId();
 199
 200       m_operations.remove(id);            // DFSearch won't ever revisit this state.  It is safe to remove and allow for cleanup.
 201
 202       if (s_logger.isLoggable(Level.FINE))
 203          s_logger.fine("State Processed: " + id);
 204    }
 205
 206    @Override
 207    public void stateBacktracked(Search search)
 208    {
 209       switchTo(search);
 210    }
 211
 212    @Override
 213    public void stateRestored(Search search)
 214    {
 215       switchTo(search);
 216    }
 217
 218    private void switchTo(Search search)
 219    {
 220       Operation next;
 221       Integer id;
 222
 223       id   = search.getStateId();
 224       next = m_operations.get(id);
 225
 226       if (s_logger.isLoggable(Level.FINE))
 227          s_logger.fine("State Switching: " + id);
 228
 229       assert (id <= 0) || (m_operations.containsKey(id));
 230
 231       switchTo(next);
 232
 233       m_current = next;
 234
 235       logState();
 236
 237       if (s_logger.isLoggable(Level.FINE))
 238          s_logger.fine("State Switched:  " + id);
 239    }
 240
 241    private void switchTo(Operation next)
 242    {
 243       Operation operation;
 244       Integer index;
 245       int i;
 246
 247       for (operation = next; operation != null; operation = operation.getParent())  // Go through all of the operations leading back to the root.
 248       {
 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);
 251       }
 252
 253       index = null;
 254
 255       for (operation = m_current; operation != null; operation = operation.getParent())  // Go through all of the operations leading back to the root.
 256       {
 257          index = m_index.get(operation);
 258
 259          if (index != null)        // If a common ancestor is found, stop going back.
 260             break;
 261
 262          operation.revert();       // Revert the operation since it isn't common to both states.
 263       }
 264
 265       if (index == null)
 266          index = m_apply.size();   // No common ancestor found.  Must apply all of the operations.
 267
 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();
 270
 271       m_index.clear();
 272       m_apply.clear();
 273    }
 274
 275    private void logState()
 276    {
 277       StringBuilder message;
 278       String type;
 279       Integer key, keys[], depth;
 280       int i;
 281
 282       if (!s_logger.isLoggable(Level.FINER))
 283          return;
 284
 285       message = new StringBuilder();
 286       keys    = m_state.keySet().toArray(EMPTY);
 287
 288       Arrays.sort(keys);
 289       message.append("State | Size = ");
 290       message.append(keys.length);
 291
 292       for (i = 0; i < keys.length; i++)
 293       {
 294          key   = keys[i];
 295          depth = m_state.get(key);
 296
 297          if ((key & THREAD_FLAG) != 0)
 298             type = "Thread";
 299          else
 300             type = "Lock";
 301
 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);
 309       }
 310
 311       s_logger.finer(message.toString());
 312    }
 313
 314    private void logStack(ThreadInfo thread)
 315    {
 316       if (!s_logger.isLoggable(Level.FINEST))
 317          return;
 318
 319       s_logger.finest(thread.getStackTrace());
 320    }
 321
 322    private static int makeKey(ElementInfo lock)
 323    {
 324       return(lock.getObjectRef());
 325    }
 326
 327    private static int makeKey(ThreadInfo thread)
 328    {
 329       return(thread.getThreadObjectRef() ^ THREAD_FLAG);
 330    }
 331
 332    private class Operation
 333    {
 334       private final Operation m_parent;
 335       private final Integer   m_key;
 336       private final Integer   m_oldDepth;
 337       private final Integer   m_newDepth;
 338
 339       public Operation(ElementInfo lock, Integer newDepth)
 340       {
 341          this(makeKey(lock), newDepth);
 342       }
 343
 344       public Operation(ThreadInfo thread, Integer newDepth)
 345       {
 346          this(makeKey(thread), newDepth);
 347       }
 348
 349       private Operation(Integer key, Integer newDepth)
 350       {
 351          m_parent   = m_current;
 352          m_current  = this;
 353          m_key      = key;
 354          m_newDepth = newDepth;
 355          m_oldDepth = m_state.get(key);
 356
 357          apply();
 358       }
 359
 360       public Operation getParent()
 361       {
 362          return(m_parent);
 363       }
 364
 365       public Integer getOldDepth()
 366       {
 367          return(m_oldDepth);
 368       }
 369
 370       public Integer getNewDepth()
 371       {
 372          return(m_newDepth);
 373       }
 374
 375       public void apply()
 376       {
 377          change(m_newDepth);
 378          log("Apply ");
 379       }
 380
 381       public void revert()
 382       {
 383          change(m_oldDepth);
 384          log("Revert");
 385       }
 386
 387       private void change(Integer depth)
 388       {
 389          Integer previous;
 390
 391          if (depth == null)
 392             m_state.remove(m_key);
 393          else
 394          {
 395             previous = m_state.put(m_key, depth);
 396
 397             assert previous == null;
 398          }
 399       }
 400
 401       private void log(String header)
 402       {
 403          String message, subheader, depthStr, type;
 404          Integer depth;
 405
 406          if (!s_logger.isLoggable(Level.FINE))
 407             return;
 408
 409          if (m_newDepth != null)
 410          {
 411             subheader = "Add   ";
 412             depth     = m_newDepth;
 413          }
 414          else
 415          {
 416             subheader = "Remove";
 417             depth     = m_oldDepth;
 418          }
 419
 420          depthStr = String.valueOf(depth);
 421
 422          switch (depthStr.length())
 423          {
 424             case 1: depthStr = "   " + depthStr; break;
 425             case 2: depthStr = "  " + depthStr; break;
 426             case 3: depthStr = " " + depthStr; break;
 427             default: break;
 428          }
 429
 430          if ((m_key & THREAD_FLAG) != 0)
 431             type = "Thread";
 432          else
 433             type = "Lock";
 434
 435          message = header + " " + subheader + " | Depth = " + depthStr + " | Key = " + (m_key & ~THREAD_FLAG) + " | " + type;
 436
 437          s_logger.fine(message);
 438       }
 439    }
 440 }