Java API By Example, From Geeks To Geeks.

1 // 2 // Copyright (C) 2005 United States Government as represented by the 3 // Administrator of the National Aeronautics and Space Administration 4 // (NASA). All Rights Reserved. 5 // 6 // This software is distributed under the NASA Open Source Agreement 7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source 8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution 9 // directory tree for the complete NOSA document. 10 // 11 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY 12 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT 13 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO 14 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR 15 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT 16 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT 17 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. 18 // 19 package gov.nasa.jpf.jvm; 20 21 import gov.nasa.jpf.Config; 22 import gov.nasa.jpf.JPFException; 23 import gov.nasa.jpf.jvm.bytecode.INVOKESTATIC; 24 import gov.nasa.jpf.jvm.bytecode.Instruction; 25 import gov.nasa.jpf.jvm.bytecode.InvokeInstruction; 26 import gov.nasa.jpf.jvm.bytecode.MONITORENTER; 27 import gov.nasa.jpf.jvm.bytecode.ReturnInstruction; 28 import gov.nasa.jpf.util.CoverageManager; 29 import gov.nasa.jpf.util.Debug; 30 import gov.nasa.jpf.util.HashData; 31 import gov.nasa.jpf.util.HashPool; 32 33 import java.io.PrintWriter ; 34 35 import java.util.BitSet ; 36 import java.util.Iterator ; 37 import java.util.LinkedList ; 38 39 40 /** 41  * Represents a thread. It contains the state of the thread, static 42  * information about the thread, and the stack frames. 43  * Race detection and lock order also store some information 44  * in this data structure. 45  */ 46 public class ThreadInfo implements Storable { 47    48   /** <2do> - just a bloody guess, we need to change the livelock detection */ 49   static final int LIVELOCK_STEPS = 5000; 50    51   static final int NEW = 0; 52   static final int RUNNING = 1; 53    54   // thread is running, but has to acquire target/this lock on first op 55 // (first insn in a synchronized run method) 56 public static final int SYNC_RUNNING = 2; 57   public static final int WAITING = 3; 58   public static final int NOTIFIED = 4; 59   public static final int STOPPED = 5; 60   public static final int INTERRUPTED = 6; 61   public static final int TERMINATED = 7; 62    63   /**Pool used to store the thread data.*/ 64   protected static HashPool threadDataPool = new HashPool(); 65    66   /** Pool used to store the stack frames.*/ 67   protected static HashPool stackFramePool = new HashPool(); 68    69   static ThreadInfo current; 70    71   /** do we want a forced reschedule */ 72   boolean yield; 73    74   protected ExceptionInfo pendingException; 75    76   /** backtrack-relevant Information about the thread */ 77   protected ThreadData threadData; 78    79   /** 80    * Some information about the thread that are used to handle 81    * atomicity. 82    */ 83   protected AtomicData atomicData; 84    85   /** 86    * The stack frames of the JVM. 87    * <2do> pcm - right now this gets re-allocated on every push/pop, 88    * turn it into a real stack at some point 89    */ 90   protected StackFrame[] stack; 91    92   /** 93    * Reference of the thread list it is in. 94    */ 95   public ThreadList list; 96    97   /** 98    * Position in the thread list. 99    */ 100   public int index; 101    102   /** 103    * Contains the index of the thread data last used. 104    */ 105   public int tdIndex = -1; 106    107   /** 108    * Identifies which thread has changed. 109    */ 110   public BitSet hasChanged; 111    112   /** 113    * Set if any stack frame changed. 114    */ 115   public boolean anyChanged; 116    117   /** 118    * Keeps the information from the last storing. 119    */ 120   protected int[] data; 121    122   /** 123    * Remembers which is the lowest changed stack frame. 124    */ 125   protected int lowestChanged; 126    127   /** 128    * cache for last return value (useful for direct calls that don't change the stack) 129    */ 130   long returnValue; 131    132   /** 133    * not so nice we cross-couple the NativePeers with ThreadInfo, 134    * but to carry on with the JNI analogy, a MJIEnv is clearly 135    * owned by a thread (even though we don't have much ThreadInfo 136    * state dependency in here (yet), hence the simplistic init) 137    */ 138   MJIEnv env; 139    140   /** 141    * the VM we are running on. Bad backlink, but then again, we can't really 142    * test a ThreadInfo outside a VM context anyways. 143    * <2do> If we keep 'list' as a field, 'vm' might be moved over there 144    * (all threads in the list share the same VM) 145    */ 146   JVM vm; 147    148   /** 149    * list of lock objects currently held by this thread. 150    * unfortunately, we cannot organize this as a stack, since it might get 151    * restored (from the heap) in random order 152    */ 153   LinkedList lockedObjects = new LinkedList (); 154    155    156   // the following parameters are configurable. Would be nice if we could keep 157 // them on a per-instance basis, but there are a few locations 158 // (e.g. ThreadList) where we loose the init context, and it's questionable 159 // if we want to change this at runtime, or POR might make sense on a per-thread 160 // basis 161 162   /** do we halt on each throw, i.e. don't look for an exception handler? 163    * Useful to find empty handler blocks, or misusd exceptions 164    */ 165   static boolean haltOnThrow; 166    167   /** is on-the-fly partial order in effect? */ 168   static boolean porInEffect; 169    170   /** do we treat access of fields referring to objects that are reachable 171    * from different threads as boundary steps (i.e. starting a new Transition)? 172    */ 173   static boolean porFieldBoundaries; 174    175   /** detect field synchronization (find locks which are used to synchronize 176    * field access - if we have viable candidates, and we find the locks taken, 177    * we don't treat access of the corresponding field as a boundary step 178    */ 179   static boolean porSyncDetection; 180      181   static boolean init (Config config) { 182     threadDataPool = new HashPool(); 183     stackFramePool = new HashPool(); 184     current = null; 185      186     haltOnThrow = config.getBoolean("vm.halt_on_throw"); 187     porInEffect = config.getBoolean("vm.por"); 188     porFieldBoundaries = config.getBoolean("vm.por.field_boundaries"); 189     porSyncDetection = config.getBoolean("vm.por.sync_detection"); 190      191     return true; 192   } 193    194   /** 195    * Creates a new thread info. It is associated with the object 196    * passed and sets the target object as well. 197    */ 198   public ThreadInfo (JVM vm, int o) { 199     DynamicArea da = vm.getDynamicArea(); 200     ElementInfo ei = da.get(o); 201      202     this.vm = vm; 203      204     threadData = new ThreadData(); 205     threadData.status = NEW; 206      207     if (o != -1) { 208       threadData.ci = ei.getClassInfo(); 209     } 210      211     threadData.objref = o; 212     threadData.target = -1; 213     threadData.lockCount = 0; 214      215     // this is nasty - 'priority', 'name', 'target' and 'group' are not taken 216 // from the object, but set within the java.lang.Thread ctors 217 218     atomicData = new AtomicData(); 219     atomicData.currentMethod = null; 220     atomicData.line = -1; 221     atomicData.inSameMethod = false; 222      223     stack = new StackFrame[0]; 224      225     hasChanged = new BitSet (); 226     anyChanged = false; 227     data = new int[0]; 228     lowestChanged = -1; 229      230     env = new MJIEnv(this); 231   } 232    233   public ThreadInfo (ThreadInfo ti) { 234     if (ti.tdIndex == -1) { 235       threadData = (ThreadData) ti.threadData.clone(); 236     } else { 237       threadData = ti.threadData; 238     } 239      240     atomicData = (AtomicData) ti.atomicData.clone(); 241      242     if (ti.stack != null) { 243       int l = ti.stack.length; 244       stack = new StackFrame[l]; 245        246       if (ti.anyChanged) { 247         for (int i = 0; i < l; i++) { 248           if (ti.hasChanged.get(i)) { 249             stack[i] = (StackFrame) ti.stack[i].clone(); 250           } else { 251             stack[i] = ti.stack[i]; 252           } 253         } 254       } else { 255         System.arraycopy(ti.stack, 0, stack, 0, l); 256       } 257     } else { 258       stack = null; 259     } 260      261     vm = ti.vm; 262     list = null; 263     index = -1; 264     tdIndex = ti.tdIndex; 265     hasChanged = (BitSet ) ti.hasChanged.clone(); 266     anyChanged = ti.anyChanged; 267     data = ti.data; 268     lowestChanged = ti.lowestChanged; 269      270     env = new MJIEnv(this); 271   } 272    273   /** 274    * Creates a new empty thread info. Used to backtrack. 275    */ 276   ThreadInfo (ThreadList l, int i) { 277     list = l; 278     index = i; 279      280     stack = new StackFrame[0]; 281     tdIndex = -1; 282     data = new int[0]; 283     hasChanged = new BitSet (); 284      285     vm = JVM.getVM(); // <2do> cut this 286 287     env = new MJIEnv(this); 288      289     // <2do> what about the other fields? 290 } 291    292   public static ThreadInfo getCurrent() { 293     return current; 294   } 295 296   public boolean holdsLock (ElementInfo ei) { 297     return lockedObjects.contains(ei); 298   } 299      300   public JVM getVM () { 301     return vm; 302   } 303    304    305   public void setReturnValue (long ret) { 306     returnValue = ret; 307   } 308   /** 309    * the return value from the last StackFrame (that had a return) 310    * Note: it's the callers responsibility to know about type and validity 311    * (the method might have no / int / long return value) 312    */ 313   public long getReturnValue () { 314     return returnValue; 315   } 316    317   public boolean usePor () { 318     return porInEffect; 319   } 320    321   public boolean usePorFieldBoundaries () { 322     return porFieldBoundaries; 323   } 324    325   public boolean usePorSyncDetection () { 326     return porSyncDetection; 327   } 328    329   /** 330    * Checks if the thread is waiting to execute a nondeterministic choice 331    * due to an abstraction, i.e. due to a Bandera.choose() call 332    */ 333   public boolean isAbstractionNonDeterministic () { 334     if (getPC() == null) { 335       return false; 336     } 337      338     return getPC().examineAbstraction(list.ks.ss, list.ks, this); 339   } 340    341   /** 342    * An alive thread is either running, waiting, notified, or interrupted. 343    */ 344   public boolean isAlive () { 345     return (threadData.status != TERMINATED); 346     /* 347      boolean alive = (threadData.status == RUNNING) || 348      (threadData.status == SYNC_RUNNING) || 349      (threadData.status == WAITING) || 350      (threadData.status == INTERRUPTED) || 351      (threadData.status == NOTIFIED); 352       353      return alive; 354      */ 355   } 356    357   /** 358    * Returns the information necessary to backtrack. 359    */ 360   public Object getBacktrackData () { 361     return atomicData.clone(); 362   } 363    364   public boolean getBooleanLocal (String lname) { 365     return Types.intToBoolean(getLocalVariable(lname)); 366   } 367    368   public boolean getBooleanLocal (int lindex) { 369     return Types.intToBoolean(getLocalVariable(lindex)); 370   } 371    372   public boolean getBooleanLocal (int fr, String lname) { 373     return Types.intToBoolean(getLocalVariable(fr, lname)); 374   } 375    376   public boolean getBooleanLocal (int fr, int lindex) { 377     return Types.intToBoolean(getLocalVariable(fr, lindex)); 378   } 379    380   public boolean getBooleanReturnValue () { 381     return Types.intToBoolean(peek()); 382   } 383    384   public byte getByteLocal (String lname) { 385     return (byte) getLocalVariable(lname); 386   } 387    388   public byte getByteLocal (int lindex) { 389     return (byte) getLocalVariable(lindex); 390   } 391    392   public byte getByteLocal (int fr, String lname) { 393     return (byte) getLocalVariable(fr, lname); 394   } 395    396   public byte getByteLocal (int fr, int lindex) { 397     return (byte) getLocalVariable(fr, lindex); 398   } 399    400   public byte getByteReturnValue () { 401     return (byte) peek(); 402   } 403    404   public String [] getCallStack () { 405     int size = stack.length; 406     String [] callStack = new String [size]; 407      408     for (int i = 0; i < size; i++) { 409       callStack[i] = frame(i).getStackTrace(); 410     } 411      412     return callStack; 413   } 414    415   public String getCallStackClass (int i) { 416     if (i < stack.length) { 417       StackFrame fr = frame(i); 418        419       return fr.getClassInfo().getName(); 420     } 421      422     return null; 423   } 424    425   public String getCallStackFile (int i) { 426     if (i < stack.length) { 427       StackFrame fr = frame(i); 428        429       return fr.getClassInfo().getSourceFileName(); 430     } 431      432     return null; 433   } 434    435   public int getCallStackLine (int i) { 436     if (i < stack.length) { 437       StackFrame fr = frame(i); 438        439       return fr.getLine(); 440     } 441      442     return 0; 443   } 444    445   public String getCallStackMethod (int i) { 446     if (i < stack.length) { 447       StackFrame fr = frame(i); 448        449       return fr.getMethodInfo().getName(); 450     } 451      452     return null; 453   } 454    455   /** 456    * Returns the this pointer of the callee from the stack. 457    */ 458   public int getCalleeThis (MethodInfo mi) { 459     return top().getCalleeThis(mi); 460   } 461    462   /** 463    * Returns the this pointer of the callee from the stack. 464    */ 465   public int getCalleeThis (int size) { 466     return top().getCalleeThis(size); 467   } 468    469   public boolean isCalleeThis (Reference r) { 470     if ((stack.length == 0) || (r == null)) { 471       return false; 472     } 473      474     Instruction pc = getPC(); 475      476     if (pc == null) { 477       return false; 478     } 479      480     if (!(pc instanceof InvokeInstruction)) { 481       return false; 482     } 483      484     if (pc instanceof INVOKESTATIC) { 485       return false; 486     } 487      488     InvokeInstruction i = (InvokeInstruction) pc; 489      490     return getCalleeThis(Types.getArgumentsSize(i.signature) + 1) == ((ElementInfo) r).getIndex(); 491   } 492    493   public char getCharLocal (String lname) { 494     return (char) getLocalVariable(lname); 495   } 496    497   public char getCharLocal (int lindex) { 498     return (char) getLocalVariable(lindex); 499   } 500    501   public char getCharLocal (int fr, String lname) { 502     return (char) getLocalVariable(fr, lname); 503   } 504    505   public char getCharLocal (int fr, int lindex) { 506     return (char) getLocalVariable(fr, lindex); 507   } 508    509   public char getCharReturnValue () { 510     return (char) peek(); 511   } 512    513   /** 514    * Returns the class information. 515    */ 516   public ClassInfo getClassInfo () { 517     return threadData.ci; 518   } 519    520   public double getDoubleLocal (String lname) { 521     return Types.longToDouble(getLongLocalVariable(lname)); 522   } 523    524   public double getDoubleLocal (int lindex) { 525     return Types.longToDouble(getLongLocalVariable(lindex)); 526   } 527    528   public double getDoubleLocal (int fr, String lname) { 529     return Types.longToDouble(getLongLocalVariable(fr, lname)); 530   } 531    532   public double getDoubleLocal (int fr, int lindex) { 533     return Types.longToDouble(getLongLocalVariable(fr, lindex)); 534   } 535    536   public double getDoubleReturnValue () { 537     return Types.longToDouble(longPeek()); 538   } 539    540   /** 541    * An enabled thread is either running, notified, or interrupted. 542    */ 543   public boolean isEnabled () { 544     boolean isEnabled = (threadData.status == RUNNING) || 545                         (threadData.status == SYNC_RUNNING) || 546                         (threadData.status == INTERRUPTED) || 547                         (threadData.status == NOTIFIED); 548     return isEnabled; 549   } 550    551   public float getFloatLocal (String lname) { 552     return Types.intToFloat(getLocalVariable(lname)); 553   } 554    555   public float getFloatLocal (int lindex) { 556     return Types.intToFloat(getLocalVariable(lindex)); 557   } 558    559   public float getFloatLocal (int fr, String lname) { 560     return Types.intToFloat(getLocalVariable(fr, lname)); 561   } 562    563   public float getFloatLocal (int fr, int lindex) { 564     return Types.intToFloat(getLocalVariable(fr, lindex)); 565   } 566    567   public float getFloatReturnValue () { 568     return Types.intToFloat(peek()); 569   } 570    571   public int getIntLocal (String lname) { 572     return getLocalVariable(lname); 573   } 574    575   public int getIntLocal (int lindex) { 576     return getLocalVariable(lindex); 577   } 578    579   public int getIntLocal (int fr, String lname) { 580     return getLocalVariable(fr, lname); 581   } 582    583   public int getIntLocal (int fr, int lindex) { 584     return getLocalVariable(fr, lindex); 585   } 586    587   public int getIntReturnValue () { 588     return peek(); 589   } 590    591   public boolean isInterrupted (boolean resetStatus) { 592     boolean ret = (getStatus() == INTERRUPTED); 593      594     if (resetStatus) { 595       // <2do> pcm is that true? check the specs 596 setStatus(RUNNING); 597     } 598      599     return ret; 600   } 601    602   /** 603    * return our internal thread number (order of creation) 604    */ 605   public int getIndex () { 606     return index; 607   } 608    609   /** 610    * Returns the line number of the program counter of the top stack frame. 611    */ 612   public int getLine () { 613     if (stack.length == 0) return -1; 614      615     return top().getLine(); 616   } 617    618   /** 619    * Returns the line the thread is at. 620    */ 621   public int getLine (int idx) { 622     return frame(idx).getLine(); 623   } 624    625   public String [] getLocalNames () { 626     return top().getLocalVariableNames(); 627   } 628    629   public String [] getLocalNames (int fr) { 630     return frame(fr).getLocalVariableNames(); 631   } 632    633   /** 634    * Sets the value of a local variable. 635    */ 636   public void setLocalVariable (int idx, int v, boolean ref) { 637     topClone().setLocalVariable(idx, v, ref); 638   } 639    640   /** 641    * Returns the value of a local variable in a particular frame. 642    */ 643   public int getLocalVariable (int fr, int idx) { 644     return frame(fr).getLocalVariable(idx); 645   } 646    647   /** 648    * Returns the value of a local variable. 649    */ 650   public int getLocalVariable (int idx) { 651     return top().getLocalVariable(idx); 652   } 653    654   /** 655    * Gets the value of a local variable from its name and frame. 656    */ 657   public int getLocalVariable (int fr, String name) { 658     return frame(fr).getLocalVariable(name); 659   } 660    661   /** 662    * Gets the value of a local variable from its name. 663    */ 664   public int getLocalVariable (String name) { 665     return top().getLocalVariable(name); 666   } 667    668   /** 669    * Checks if a local variable is a reference. 670    */ 671   public boolean isLocalVariableRef (int idx) { 672     return top().isLocalVariableRef(idx); 673   } 674    675   /** 676    * Gets the type associated with a local variable. 677    */ 678   public String getLocalVariableType (int fr, String name) { 679     return frame(fr).getLocalVariableType(name); 680   } 681    682   /** 683    * Gets the type associated with a local variable. 684    */ 685   public String getLocalVariableType (String name) { 686     return top().getLocalVariableType(name); 687   } 688    689   /** 690    * Sets the number of locks held at the time of a wait. 691    */ 692   public void setLockCount (int l) { 693     if (threadData.lockCount != l) { 694       threadDataClone().lockCount = l; 695     } 696   } 697    698   /** 699    * Returns the number of locks in the last wait. 700    */ 701   public int getLockCount () { 702     return threadData.lockCount; 703   } 704      705   public LinkedList getLockedObjects () { 706     return lockedObjects; 707   } 708    709   public int[] getLockedObjectReferences () { 710     int[] a = new int[lockedObjects.size()]; 711     int i=0; 712     for (Iterator it=lockedObjects.iterator(); it.hasNext();) { 713       a[i++] = ((ElementInfo)it.next()).getIndex(); 714     } 715      716     return a; 717   } 718    719   public long getLongLocal (String lname) { 720     return getLongLocalVariable(lname); 721   } 722    723   public long getLongLocal (int lindex) { 724     return getLongLocalVariable(lindex); 725   } 726    727   public long getLongLocal (int fr, String lname) { 728     return getLongLocalVariable(fr, lname); 729   } 730    731   public long getLongLocal (int fr, int lindex) { 732     return getLongLocalVariable(fr, lindex); 733   } 734    735   /** 736    * Sets the value of a long local variable. 737    */ 738   public void setLongLocalVariable (int idx, long v) { 739     topClone().setLongLocalVariable(idx, v); 740   } 741    742   /** 743    * Returns the value of a long local variable. 744    */ 745   public long getLongLocalVariable (int fr, int idx) { 746     return frame(fr).getLongLocalVariable(idx); 747   } 748    749   /** 750    * Returns the value of a long local variable. 751    */ 752   public long getLongLocalVariable (int idx) { 753     return top().getLongLocalVariable(idx); 754   } 755    756   /** 757    * Gets the value of a long local variable from its name. 758    */ 759   public long getLongLocalVariable (int fr, String name) { 760     return frame(fr).getLongLocalVariable(name); 761   } 762    763   /** 764    * Gets the value of a long local variable from its name. 765    */ 766   public long getLongLocalVariable (String name) { 767     return top().getLongLocalVariable(name); 768   } 769    770   public long getLongReturnValue () { 771     return longPeek(); 772   } 773    774   /** 775    * Returns the current method in the top stack frame. 776    */ 777   public MethodInfo getMethod () { 778     if (stack.length > 0) { 779       return top().getMethodInfo(); 780     } else { 781       return null; 782     } 783   } 784    785   public boolean isInCtor () { 786     // <2do> - hmm, if we don't do this the whole stack, we miss factored 787 // init funcs 788 MethodInfo mi = getMethod(); 789     return mi.isCtor(); 790   } 791    792   /** 793    * Returns the method info of a specific stack frame. 794    */ 795   public MethodInfo getMethod (int idx) { 796     if (stack.length > 0) { 797       return frame(idx).getMethodInfo(); 798     } else { 799       return null; 800     } 801   } 802    803   public String getName () { 804     return threadData.name; 805   } 806    807   /** 808    * Checks if the thread is waiting to execute a nondeterministic choice, 809    * due to the use of Verify.random... calls. 810    * 811    * <?> pcm - this is not called anywhere, but is part of the 'iThreadInfo' 812    * interface. We clean this up when we remove the interface 813    */ 814   public boolean isNonDeterministic () { 815     if (getPC() == null) { 816       return false; 817     } 818      819     return !getPC().isDeterministic(list.ks.ss, list.ks, this); 820   } 821    822   public Reference getObjectLocal (String lname) { 823     return list.ks.da.get(getLocalVariable(lname)); 824   } 825    826   public Reference getObjectLocal (int lindex) { 827     return list.ks.da.get(getLocalVariable(lindex)); 828   } 829    830   public Reference getObjectLocal (int fr, String lname) { 831     return list.ks.da.get(getLocalVariable(fr, lname)); 832   } 833    834   public Reference getObjectLocal (int fr, int lindex) { 835     return list.ks.da.get(getLocalVariable(fr, lindex)); 836   } 837    838   /** 839    * Returns the object reference. 840    */ 841   public int getObjectReference () { 842     return threadData.objref; 843   } 844    845   public Reference getObjectReturnValue () { 846     return list.ks.da.get(peek()); 847   } 848    849   public Object getOperandAttr () { 850     return top().getOperandAttr(); 851   } 852    853   public Object getOperandAttr (int opStackOffset) { 854     return top().getOperandAttr(opStackOffset); 855   } 856    857   public void setOperandAttr (Object attr) { 858     top().setOperandAttr(attr); 859   } 860    861   /** 862    * Checks if the top operand is a reference. 863    */ 864   public boolean isOperandRef () { 865     return top().isOperandRef(); 866   } 867    868   /** 869    * Checks if an operand is a reference. 870    */ 871   public boolean isOperandRef (int idx) { 872     return top().isOperandRef(idx); 873   } 874    875   /** 876    * Sets the program counter of the top stack frame. 877    */ 878   public void setPC (Instruction pc) { 879     topClone().setPC(pc); 880   } 881    882   /** 883    * Returns the program counter of a stack frame. 884    */ 885   public Instruction getPC (int i) { 886     return frame(i).getPC(); 887   } 888    889   /** 890    * Returns the program counter of the top stack frame. 891    */ 892   public Instruction getPC () { 893     if (stack.length == 0) { 894       return null; 895     } 896      897     return top().getPC(); 898   } 899    900   public ExceptionInfo getPendingException () { 901     return pendingException; 902   } 903    904   /** 905    * Returns true if it is possible to execute the next instruction 906    * of this thread. This function is used by the scheduler to determine 907    * which threads can be executed. 908    * 909    * <?> pcm - watch out, it's not just used from Scheduler, but also from 910    * within ThreadInfo itself 911    */ 912   public boolean isRunnable () { 913     if (!isEnabled()) { 914       // this filters out waits 915 return false; 916     } 917      918     // this is for newly created threads with synchronized run() methods 919 if (threadData.status == SYNC_RUNNING) { 920       int sync = (threadData.target != -1) 921         ? threadData.target : threadData.objref; 922       ElementInfo ei = list.ks.da.get(sync); 923        924       if ((ei != null) && !ei.canLock(this)) { 925         return false; 926       } 927     } 928      929     Instruction pc = getPC(); 930      931     if (pc == null) { 932       return false; 933     } 934      935     // the instruction needs to be executable as well 936 // pcm - for now, this is about insns which might require a lock in order to be 937 // executable (invokeX,monitorEnter) 938 return pc.isExecutable(list.ks.ss, list.ks, this); 939   } 940    941   public short getShortLocal (String lname) { 942     return (short) getLocalVariable(lname); 943   } 944    945   public short getShortLocal (int lindex) { 946     return (short) getLocalVariable(lindex); 947   } 948    949   public short getShortLocal (int fr, String lname) { 950     return (short) getLocalVariable(fr, lname); 951   } 952    953   public short getShortLocal (int fr, int lindex) { 954     return (short) getLocalVariable(fr, lindex); 955   } 956    957   public short getShortReturnValue () { 958     return (short) peek(); 959   } 960    961   /** 962    * get the current stack trace of this thread 963    * this is called during creation of a Throwable, hence we should skip 964    * all throwable ctors in here 965    * <2do> this is only a partial solution,since we don't catch exceptions 966    * in Throwable ctors yet 967    */ 968   public String getStackTrace () { 969     StringBuffer sb = new StringBuffer (256); 970 971     for (int i = stack.length - 1; i >= 0; i--) { 972       StackFrame sf = frame(i); 973       MethodInfo mi = sf.getMethodInfo(); 974        975       if (mi.isCtor()){ 976         ClassInfo ci = mi.getClassInfo(); 977         if (ci.instanceOf("java.lang.Throwable")) { 978           continue; 979         } 980       } 981 982       sb.append(frame(i).getStackTrace()); 983       sb.append("\n"); 984     } 985      986     return sb.toString(); 987   } 988    989   /** 990    * Updates the status of the thread. 991    */ 992   public void setStatus (int s) { 993     if (threadData.status != s) { 994        995       if ((s == RUNNING) || (s == SYNC_RUNNING)) { 996         JVM.getVM().notifyThreadStarted(this); 997       } else if (s == TERMINATED) { 998         JVM.getVM().notifyThreadTerminated(this); 999       } 1000       1001      threadDataClone().status = s; 1002    } 1003  } 1004   1005  /** 1006   * Returns the current status of the thread. 1007   */ 1008  public int getStatus () { 1009    return threadData.status; 1010  } 1011   1012  /** 1013   * Returns the information necessary to store. 1014   * 1015   * <2do> pcm - not clear to me how lower stack frames can contribute to 1016   * a different threadinfo state hash - only the current one can be changed 1017   * by the executing method 1018   */ 1019  public int[] getStoringData () { 1020    int length = stack.length; 1021     1022    int[] data = new int[length + 2]; 1023    data[0] = getThreadDataIndex(); 1024    data[1] = length; 1025     1026    if (anyChanged) { 1027      if (lowestChanged > 0) { 1028        System.arraycopy(this.data, 2, data, 2, lowestChanged); 1029      } 1030       1031      for (int i = lowestChanged, j = i + 2; i < length; i++, j++) { 1032        data[j] = getStackFrameIndex(i); 1033      } 1034    } else if (length > 0) { 1035      System.arraycopy(this.data, 2, data, 2, length); 1036    } 1037     1038    anyChanged = false; 1039    hasChanged = new BitSet (); 1040    lowestChanged = -1; 1041     1042    this.data = data; 1043     1044    return data; 1045  } 1046   1047  public String getStringLocal (String lname) { 1048    return list.ks.da.get(getLocalVariable(lname)).asString(); 1049  } 1050   1051  public String getStringLocal (int lindex) { 1052    return list.ks.da.get(getLocalVariable(lindex)).asString(); 1053  } 1054   1055  public String getStringLocal (int fr, String lname) { 1056    return list.ks.da.get(getLocalVariable(fr, lname)).asString(); 1057  } 1058   1059  public String getStringLocal (int fr, int lindex) { 1060    return list.ks.da.get(getLocalVariable(fr, lindex)).asString(); 1061  } 1062   1063  public String getStringReturnValue () { 1064    return list.ks.da.get(peek()).asString(); 1065  } 1066   1067  /** 1068   * Sets the target of the thread. 1069   */ 1070  public void setTarget (int t) { 1071    if (threadData.target != t) { 1072      threadDataClone().target = t; 1073    } 1074  } 1075   1076  /** 1077   * Returns the object reference of the target. 1078   */ 1079  public int getTarget () { 1080    return threadData.target; 1081  } 1082   1083  /** 1084   * Returns the pointer to the object reference of the executing method 1085   */ 1086  public int getThis () { 1087    return top().getThis(); 1088  } 1089   1090  public boolean isThis (Reference r) { 1091    if (r == null) { 1092      return false; 1093    } 1094     1095    if (stack.length == 0) { 1096      return false; 1097    } 1098     1099    return getMethod().isStatic() 1100      ? false : ((ElementInfo) r).getIndex() == getLocalVariable(0); 1101  } 1102   1103  public boolean atInvoke (String mname) { 1104    if (stack.length == 0) { 1105      return false; 1106    } 1107     1108    Instruction pc = getPC(); 1109     1110    if (!(pc instanceof InvokeInstruction)) { 1111      return false; 1112    } 1113     1114    InvokeInstruction i = (InvokeInstruction) pc; 1115     1116    return mname.equals(i.cname + "." + i.mname); 1117  } 1118   1119  public boolean atLabel (String label) { 1120    return Labels.isAt(label, this); 1121  } 1122   1123  public boolean atMethod (String mname) { 1124    if (stack.length == 0) { 1125      return false; 1126    } 1127     1128    return getMethod().getCompleteName().equals(mname); 1129  } 1130   1131  public boolean atPosition (int position) { 1132    if (stack.length == 0) { 1133      return false; 1134    } 1135     1136    Instruction pc = getPC(); 1137     1138    if (pc == null) { 1139      return false; 1140    } 1141     1142    return pc.getPosition() == position; 1143  } 1144   1145  public boolean atReturn () { 1146    if (stack.length == 0) { 1147      return false; 1148    } 1149     1150    Instruction pc = getPC(); 1151     1152    if (pc == null) { 1153      return false; 1154    } 1155     1156    return pc instanceof ReturnInstruction; 1157  } 1158   1159   1160  /** 1161   * reset any information that has to be re-computed in a backtrack 1162   * (i.e. hasn't been stored explicitly) 1163   */ 1164  void resetVolatiles () { 1165    // resetting lock sets goes here 1166 lockedObjects = new LinkedList (); 1167  } 1168   1169  void addLockedObject (ElementInfo ei) { 1170    lockedObjects.add(ei); 1171  } 1172   1173  void removeLockedObject (ElementInfo ei) { 1174    lockedObjects.remove(ei); 1175  } 1176   1177  /** 1178   * Restores the state of the system. 1179   */ 1180  public void backtrackTo (ArrayOffset storing, Object backtrack) { 1181     1182    resetVolatiles(); 1183     1184    setThreadDataIndex(storing.get()); 1185     1186    int length = storing.get(); 1187    int l = stack.length; 1188     1189    int[] data = new int[length + 2]; 1190    data[0] = tdIndex; 1191    data[1] = length; 1192    System.arraycopy(storing.data, storing.offset, data, 2, length); 1193     1194    if (length != l) { 1195      if (l > length) { 1196        l = length; 1197      } 1198       1199      StackFrame[] n = new StackFrame[length]; 1200       1201      if (l > 0) { 1202        System.arraycopy(stack, 0, n, 0, l); 1203      } 1204       1205      stack = n; 1206    } 1207     1208    for (int i = 0; i < length; i++) { 1209      setStackFrameIndex(i, storing.get()); 1210    } 1211     1212    atomicData = (AtomicData) backtrack; 1213     1214    anyChanged = false; 1215    hasChanged = new BitSet (); 1216    lowestChanged = -1; 1217     1218    this.data = data; 1219  } 1220   1221  /** 1222   * Pops a set of values from the caller stack frame. 1223   */ 1224  public void callerPop (int n) { 1225    frameClone(-1).pop(n); 1226  } 1227   1228  /** 1229   * Clears the operand stack of all value. 1230   */ 1231  public void clearOperandStack () { 1232    topClone().clearOperandStack(); 1233  } 1234   1235  public Object clone () { 1236    return new ThreadInfo(this); 1237  } 1238   1239  public StackFrame[] cloneStack() { 1240    StackFrame[] sf = null; 1241     1242    // add a StackFrame if the current method is native 1243 // (we only use this in debuging and exception handling so far) 1244 1245    // are we executing in a native method? If yes, it's not on the stack 1246 // and we have to add it on the fly (assuming this is called rather 1247 // infrequently as part of exception handling). Otherwise we really should 1248 // add a StackFrame for every native call 1249 MethodInfo nativeMth = env.getMethodInfo(); 1250    if (nativeMth != null){ 1251      sf = new StackFrame[stack.length +1]; 1252      System.arraycopy(stack, 0, sf, 0, stack.length); 1253      sf[stack.length] = new StackFrame(nativeMth, false, null); 1254      // <2do> we probably should fill in the params/locals here 1255 } else { 1256      sf = (StackFrame[]) stack.clone(); 1257    } 1258     1259    return sf; 1260  } 1261   1262  /** 1263   * Returns the number of stack frames. 1264   */ 1265  public int countStackFrames () { 1266    return stack.length; 1267  } 1268   1269  int createStackTraceElement ( String clsName, String mthName, String fileName, int line) { 1270    DynamicArea da = DynamicArea.getHeap(); 1271     1272    ClassInfo ci = ClassInfo.getClassInfo("java.lang.StackTraceElement"); 1273    int sRef = da.newObject(ci, this); 1274     1275    ElementInfo sei = da.get(sRef); 1276    sei.setReferenceField("clsName", da.newString(clsName, this)); 1277    sei.setReferenceField("mthName", da.newString(mthName, this)); 1278    sei.setReferenceField("fileName", da.newString(fileName, this)); 1279    sei.setIntField("line", line); 1280     1281    return sRef; 1282  } 1283   1284  public int getStackTrace (int objref) { 1285    DynamicArea da = DynamicArea.getHeap(); 1286    int stackDepth = countStackFrames(); 1287    int i, j=0; 1288    int aRef; 1289    ElementInfo aei; 1290     1291    // are we executing in a native method? If yes, it's not on the stack 1292 MethodInfo nativeMth = env.getMethodInfo(); 1293    if (nativeMth != null){ 1294      aRef = da.newArray("Ljava/lang/StackTraceElement", stackDepth+1, this); 1295      aei = da.get(aRef); 1296       1297      aei.setElement( j++, 1298          createStackTraceElement( nativeMth.getClassInfo().getName(), 1299                                    nativeMth.getName(), 1300                                    nativeMth.getClassInfo().getSourceFileName(), -1)); 1301    } else { 1302      aRef = da.newArray("Ljava/lang/StackTraceElement", stackDepth, this); 1303      aei = da.get(aRef); 1304    } 1305     1306    for (i = stackDepth - 1; i >= 0; i--, j++) { 1307      aei.setElement( j, 1308          createStackTraceElement( getCallStackClass(i), getCallStackMethod(i), 1309                         getCallStackFile(i), getCallStackLine(i))); 1310     } 1311 1312    return aRef; 1313  } 1314   1315  void print (PrintWriter pw, String s) { 1316    if (pw != null){ 1317      pw.print(s); 1318    } else { 1319      vm.print(s); 1320    } 1321  } 1322     1323  public void printStackTrace (int objRef) { 1324    printStackTrace(null, objRef); 1325  } 1326   1327  public void printPendingExceptionOn (PrintWriter pw) { 1328    if (pendingException != null) { 1329      printStackTrace( pw, pendingException.getExceptionReference()); 1330    } 1331  } 1332   1333  public void printStackTrace (PrintWriter pw, int objRef) { 1334    // 'env' usage is not ideal, since we don't know from what context we are called, and 1335 // hence the MJIEnv calling context might not be set (no Method or ClassInfo) 1336 // on the other hand, we don't want to re-implement all the MJIEnv accessor methods 1337 print(pw, env.getClassInfo(objRef).getName()); 1338     1339    int msgRef = env.getReferenceField(objRef,"detailMessage"); 1340    if (msgRef != MJIEnv.NULL) { 1341      print(pw, ": "); 1342      print(pw, env.getStringObject(msgRef)); 1343    } 1344    print(pw, "\n"); 1345     1346    int aRef = env.getReferenceField(objRef, "stackTrace"); // StackTrace[] 1347 if (aRef != MJIEnv.NULL) { 1348      int len = env.getArrayLength(aRef); 1349      for (int i=0; i<len; i++) { 1350        int sRef = env.getReferenceArrayElement(aRef, i); 1351        String clsName = env.getStringObject(env.getReferenceField(sRef, "clsName")); 1352        String mthName = env.getStringObject(env.getReferenceField(sRef, "mthName")); 1353        String fileName = env.getStringObject(env.getReferenceField(sRef, "fileName")); 1354        int line = env.getIntField(sRef, "line"); 1355         1356        print(pw, "\tat "); 1357        print(pw, clsName); 1358        print(pw, "."); 1359        print(pw, mthName); 1360        print(pw, "("); 1361        print(pw, fileName); 1362        print(pw, ":"); 1363         1364        if (line < 0){ 1365          print(pw, "native"); 1366        } else { 1367          print(pw, Integer.toString(line)); 1368        } 1369         1370        print(pw, ")"); 1371        print(pw, "\n"); 1372      } 1373    } 1374  } 1375   1376  // <2do> - not yet functional, fix free calls!! 1377 void callThrowableCtor (ClassInfo ci, int objRef, int msgRef) { 1378    MethodInfo mi = ci.getMethod("<init>(Ljava/lang/String;)", true); 1379    if (mi != null) { 1380      push(objRef, true); 1381      push(msgRef, true); 1382      executeMethod(mi); 1383    } 1384  } 1385   1386  /** 1387   * Creates an exception and throws it. 1388   */ 1389  public Instruction createAndThrowException (ClassInfo ci, String details) { 1390    DynamicArea da = DynamicArea.getHeap(); 1391    int objref = da.newObject(ci, this); 1392    int msgref = -1; 1393         1394    ElementInfo ei = da.get(objref); 1395     1396    // <2do> pcm - this is not correct! We have to call a propper ctor 1397 // for the Throwable (for now, we just explicitly set the details) 1398 if (details != null) { 1399      msgref = da.newString(details, this); 1400      ei.setReferenceField("detailMessage", "java.lang.Throwable", msgref); 1401    } 1402     1403    return throwException(objref); 1404  } 1405     1406  /** 1407   * Creates an exception and throws it. 1408   */ 1409  public Instruction createAndThrowException (String cname) { 1410    return createAndThrowException(ClassInfo.getClassInfo(cname), null); 1411  } 1412   1413  public Instruction createAndThrowException (String cname, String details) { 1414    return createAndThrowException(ClassInfo.getClassInfo(cname), details); 1415  } 1416     1417  /** 1418   * Duplicates a value on the top stack frame. 1419   */ 1420  public void dup () { 1421    topClone().dup(); 1422  } 1423   1424  /** 1425   * Duplicates a long value on the top stack frame. 1426   */ 1427  public void dup2 () { 1428    topClone().dup2(); 1429  } 1430   1431  /** 1432   * Duplicates a long value on the top stack frame. 1433   */ 1434  public void dup2_x1 () { 1435    topClone().dup2_x1(); 1436  } 1437   1438  /** 1439   * Duplicates a long value on the top stack frame. 1440   */ 1441  public void dup2_x2 () { 1442    topClone().dup2_x2(); 1443  } 1444   1445  /** 1446   * Duplicates a value on the top stack frame. 1447   */ 1448  public void dup_x1 () { 1449    topClone().dup_x1(); 1450  } 1451   1452  /** 1453   * Duplicates a value on the top stack frame. 1454   */ 1455  public void dup_x2 () { 1456    topClone().dup_x2(); 1457  } 1458   1459  /** 1460   * Execute next instruction. 1461   */ 1462  public Instruction executeInstruction () { 1463    // this is for threads with synchronized run() methods 1464 // (where we have to grab the lock as soon as we start to execute, no 1465 // matter what the insn is) 1466 if (threadData.status == SYNC_RUNNING) { 1467      int sync = (threadData.target != -1) 1468        ? threadData.target : threadData.objref; 1469      ElementInfo ei = list.ks.da.get(sync); 1470      // gets unlocked when we return from run(); 1471 ei.lock(this); 1472      setStatus(RUNNING); 1473    } 1474     1475    Instruction pc = getPC(); 1476     1477    CoverageManager.incInstruction(pc, index); // <2do> should be a listener! 1478 1479    TrailInfo trail = list.ks.ss.trail(); 1480    Step step = new Step(getMethod().getClassInfo().getSourceFileName(), 1481                         getLine(), pc); 1482    trail.addStep(step); 1483     1484    if (pc.isFirstInstruction() && getMethod().isAtomic()) { 1485      list.ks.setAtomic(); 1486    } 1487     1488//System.out.println("@ " + pc.getMethod().getCompleteName() + " " + pc.getPosition() + " : " + pc); 1489 // execute the next bytecode 1490 Instruction nextPc = pc.execute(list.ks.ss, list.ks, this); 1491     1492    // we did not return from the last frame stack 1493 if (stack.length != 0) { 1494      setPC(nextPc); 1495    } 1496     1497    // here we have our bytecode exec observation point 1498 // (note we have to do this after we have set the pc, since a listener 1499 // might come back to do checks like isRunnable) 1500 vm.notifyInstructionExecuted(this, pc, nextPc); 1501     1502    return nextPc; 1503  } 1504   1505   1506  /** 1507   * Executes a method call. It executes the whole method as one atomic step and 1508   * returns when the call is over Arguments have to be already on the stack 1509   * 1510   * This is our entry point for calling methods without corresponding 1511   * INVOKE insns (e.g. <clinit>(), finalize() or method executions from native code 1512   */ 1513  public void executeMethod (MethodInfo mi) { 1514    int depth = countStackFrames(); 1515  1516    mi.execute(this, true); 1517  1518    KernelState ks = list.ks; 1519    SystemState ss = ks.ss; 1520     1521    while (depth < countStackFrames()) { 1522      Instruction pc = executeInstruction(); 1523       1524      if (ss.violatedAssertion) { 1525        break; 1526      } 1527             1528      if (pc == null) { // might be a thread in static init 1529 break; 1530      } 1531 1532      if (!pc.isExecutable(ss, ks, this)) { 1533        throw new BlockedAtomicException(); 1534      } 1535    } 1536  } 1537     1538  /** 1539   * Executes next step. 1540   * @return false if intermediate step (due to Nondeterminism or Buchi observable) 1541   */ 1542  public boolean executeStep () throws JPFException { 1543    current = this; 1544     1545    if (porInEffect) { 1546      return executePorStep(); 1547    } else { 1548      return executeAtomicLinesStep(); 1549    } 1550  } 1551   1552  // we just got our last stack frame popped, so it's time to close down 1553 public void finish () { 1554    setStatus(TERMINATED); 1555     1556    // need to own the lock before we can notify 1557 int objref = getObjectReference(); 1558    ElementInfo ei = list.ks.da.get(objref); 1559     1560    ei.lock(this); 1561    ei.notifiesAll(); 1562    ei.unlock(this); 1563     1564    // stack is gone, so reachability might change 1565 list.ks.ss.activateGC(); 1566     1567    //list.remove(index); 1568 } 1569   1570  public void hash (HashData hd) { 1571    threadData.hash(hd); 1572    atomicData.hash(hd); 1573     1574    for (int i = 0, l = stack.length; i < l; i++) { 1575      frame(i).hash(hd); 1576    } 1577  } 1578   1579  public int hashCode () { 1580    HashData hd = new HashData(); 1581     1582    hash(hd); 1583     1584    return hd.getValue(); 1585  } 1586   1587  public void interrupt () { 1588    if (getStatus() != WAITING) { 1589      return; 1590    } 1591     1592    setStatus(INTERRUPTED); 1593  } 1594   1595  /** 1596   * Called when a lock is acquired. Updates the information 1597   * related to the locks. 1598   */ 1599  public void lock (Ref ref) { 1600  } 1601   1602  public void log () { 1603    Debug.println(Debug.MESSAGE, 1604                  "TH#" + index + " #" + threadData.target + " #" + 1605                    threadData.objref + " " + threadData.status); 1606     1607    for (int i = 0; i < stack.length; i++) { 1608      frame(i).log(i); 1609    } 1610  } 1611   1612  /** 1613   * Peeks the top long value from the top stack frame. 1614   */ 1615  public long longPeek () { 1616    return top().longPeek(); 1617  } 1618   1619  /** 1620   * Peeks a long value from the top stack frame. 1621   */ 1622  public long longPeek (int n) { 1623    return top().longPeek(n); 1624  } 1625   1626  /** 1627   * Pops the top long value from the top stack frame. 1628   */ 1629  public long longPop () { 1630    return topClone().longPop(); 1631  } 1632   1633  /** 1634   * Pushes a long value of the top stack frame. 1635   */ 1636  public void longPush (long v) { 1637    topClone().longPush(v); 1638  } 1639   1640   1641  /** 1642   * mark all objects during gc phase1 which are reachable from this threads 1643   * root set (Thread object, Runnable, stack) 1644   * @aspects: gc 1645   */ 1646  void markRoots () { 1647    DynamicArea heap = DynamicArea.getHeap(); 1648     1649    // 1. mark the Thread object itself 1650 heap.markThreadRoot(threadData.objref, index); 1651     1652    // 2. and its runnable 1653 if (threadData.target != -1) { 1654      heap.markThreadRoot(threadData.target,index); 1655    } 1656     1657    // 3. now all references on the stack 1658 for (int i = 0, l = stack.length; i < l; i++) { 1659      frame(i).markThreadRoots(index); 1660    } 1661  } 1662     1663  /** 1664   * Adds a new stack frame for a new called method. 1665   * 1666   * <2do> - turn this into a real stack - don't reallocate 1667   */ 1668  public void pushFrame (StackFrame frame) { 1669    atomicData.inSameMethod = false; 1670     1671    int depth = stack.length; 1672    StackFrame[] n = new StackFrame[depth + 1]; 1673    System.arraycopy(stack, 0, n, 0, depth); 1674    stack = n; 1675     1676    stack[depth] = frame; 1677     1678    hasChanged.set(depth); 1679    anyChanged = true; 1680    list.ks.data = null; 1681     1682    if ((lowestChanged == -1) || (lowestChanged > depth)) { 1683      lowestChanged = depth; 1684    } 1685  } 1686   1687  public ElementInfo objectAtBlockedSynchronized () { 1688    if (stack.length == 0) { 1689      return null; 1690    } 1691     1692    Instruction pc = getPC(); 1693     1694    if (pc == null) { 1695      return null; 1696    } 1697     1698    if (pc instanceof InvokeInstruction) { 1699      if (!getMethod().canEnter(this)) { 1700        return getMethod().getBlockedObject(this, true); 1701      } 1702    } 1703     1704    if (pc instanceof MONITORENTER) { 1705      if (!pc.isExecutable(list.ks.ss, list.ks, this)) { 1706        return list.ks.da.get(peek()); 1707      } 1708    } 1709     1710    return null; 1711  } 1712   1713  /** 1714   * Peeks the top value from the top stack frame. 1715   */ 1716  public int peek () { 1717    if (stack.length > 0) { 1718      return top().peek(); 1719    } else { 1720      // <?> not really sure what to do here, but if the stack is gone, so is the thread 1721 return -1; 1722    } 1723  } 1724   1725  /** 1726   * Peeks a int value from the top stack frame. 1727   */ 1728  public int peek (int n) { 1729    if (stack.length > 0) { 1730      return top().peek(n); 1731    } else { 1732      // <?> see peek() 1733 return -1; 1734    } 1735  } 1736   1737  /** 1738   * Pops the top value from the top stack frame. 1739   */ 1740  public int pop () { 1741    if (stack.length > 0) { 1742      return topClone().pop(); 1743    } else { 1744      // <?> see peek() 1745 return -1; 1746    } 1747  } 1748   1749  /** 1750   * Pops a set of values from the top stack frame. 1751   */ 1752  public void pop (int n) { 1753    if (stack.length > 0) { 1754      topClone().pop(n); 1755    } 1756  } 1757   1758  /** 1759   * Removes a stack frame. 1760   */ 1761  public boolean popFrame () { 1762    int last = stack.length - 1; 1763    StackFrame sf = stack[last]; 1764     1765    if (getMethod().isAtomic()) { 1766      list.ks.clearAtomic(); 1767    } 1768     1769    if (sf.hasAnyRef()) { 1770      ((SystemState) JVM.getVM().getSystemState()).activateGC(); 1771    } 1772     1773    StackFrame[] n = new StackFrame[last]; 1774    System.arraycopy(stack, 0, n, 0, last); 1775    stack = n; 1776     1777    if (last == 0) { 1778      atomicData.inSameMethod = false; 1779      finish(); 1780    } else { 1781      atomicData.inSameMethod = (getMethod() == atomicData.currentMethod); 1782    } 1783     1784    hasChanged.set(last); 1785    anyChanged = true; 1786    list.ks.data = null; 1787     1788    if ((lowestChanged == -1) || (lowestChanged > last)) { 1789      lowestChanged = last; 1790    } 1791     1792    return (last > 0); 1793  } 1794   1795  public void printInternalErrorTrace (Throwable e) { 1796    String msg = e.getMessage(); 1797     1798    if (msg != null) { 1799      Debug.println(Debug.ERROR, 1800                    "exception " + e.getClass().getName() + ": " + msg); 1801    } else { 1802      Debug.println(Debug.ERROR, "exception " + e.getClass().getName()); 1803    } 1804     1805    printStackTrace(); 1806     1807    if (msg != null) { 1808      Debug.println(Debug.ERROR, 1809                    "exception " + e.getClass().getName() + ": " + msg); 1810    } else { 1811      Debug.println(Debug.ERROR, "exception " + e.getClass().getName()); 1812    } 1813     1814    printStackContent(); 1815  } 1816   1817  /** 1818   * Prints the content of the stack. 1819   */ 1820  public void printStackContent () { 1821    for (int i = stack.length - 1; i >= 0; i--) { 1822      frame(i).printStackContent(); 1823    } 1824  } 1825   1826  /** 1827   * Prints the trace of the stack. 1828   */ 1829  public void printStackTrace () { 1830    for (int i = stack.length - 1; i >= 0; i--) { 1831      frame(i).printStackTrace(); 1832    } 1833  } 1834   1835  /** 1836   * Pushes a value on the top stack frame. 1837   */ 1838  public void push (int v, boolean ref) { 1839    if (stack.length > 0) { // otherwise we don't have anything to push onto 1840 topClone().push(v, ref); 1841    } 1842  } 1843   1844  /** 1845   * Removes the arguments of a method call. 1846   */ 1847  public void removeArguments (MethodInfo mi) { 1848    int i = mi.getArgumentsSize(); 1849     1850    if (i != 0) { 1851      pop(i); 1852    } 1853  } 1854   1855  /** 1856   * Swaps two entry on the stack. 1857   */ 1858  public void swap () { 1859    topClone().swap(); 1860  } 1861   1862  /** 1863   * Throws an exception throught the stack frames. 1864   */ 1865  public Instruction throwException (int objref) { 1866    DynamicArea da = DynamicArea.getHeap(); 1867    ElementInfo ei = da.get(objref); 1868    ClassInfo ci = ei.getClassInfo(); 1869    MethodInfo mi; 1870    Instruction insn; 1871    int nFrames = countStackFrames(); 1872    int i, j; 1873 1874//System.out.println("## ---- got: " + ci.getName()); 1875 1876    // we need to store the stack trace in the exception object before 1877 // we start to unwind the stack looking for a handler. Unfortunately, 1878 // the stack dump is accessible for the application, so we have to 1879 // create it in JPF object land 1880 int stRef = getStackTrace(objref); 1881    ei.setReferenceField("stackTrace", "java.lang.Throwable", stRef); 1882     1883    // but we still keep this in JPF itself too, so that it's more accessible 1884 // for post-mortem 'debugging', and preserves as much JPF execution 1885 // state as possible (e.g. prevents subsequent GC) 1886 pendingException = new ExceptionInfo(this, ei); 1887     1888    vm.notifyExceptionThrown(this, ei); 1889     1890    if (!haltOnThrow) { 1891      for (j=0; j<nFrames; j++) { 1892        mi = getMethod(); 1893        insn = getPC(); 1894         1895        ExceptionHandler[] exceptions = mi.getExceptions(); 1896//System.out.println("## unwinding to: " + mi.getClassInfo().getName() + "." + mi.getUniqueName()); 1897 // this is the point where we can check for 1898 // "articifial" stack frames. There is no corresponding 1899 // INVOKE instruction in the frame underneath 1900 if ( (j==0) || (insn instanceof InvokeInstruction)) { 1901          int p = insn.getPosition(); 1902                     1903          if (exceptions != null) { 1904            // checks the exception catched in order 1905 for (i = 0; i < exceptions.length; i++) { 1906              ExceptionHandler eh = exceptions[i]; 1907               1908              // if it falls in the right range 1909 if ((p >= eh.getBegin()) && (p <= eh.getEnd())) { 1910                String en = eh.getName(); 1911//System.out.println("## checking: " + ci.getName() + " handler: " + en + " depth: " + stack.length); 1912 1913                // checks if this type of exception is caught here 1914 if ((en == null) || ci.instanceOf(en)) { 1915//System.out.println("## handle"); 1916 // clears all the operand stack 1917 clearOperandStack(); 1918                   1919                  // pushes the exception on the stack instead 1920 push(objref, true); 1921                   1922                  // jumps to the exception handler 1923 Instruction startOfHandlerBlock = mi.getInstructionAt(eh.getHandler()); 1924                  setPC(startOfHandlerBlock); // set! we might be in a isDeterministic / isRunnable 1925 1926                  pendingException = null; // handled, no need to keep it 1927 1928                  return startOfHandlerBlock; 1929                } 1930              } 1931            } 1932          } 1933           1934          if ("<clinit>".equals(mi.getName())) { 1935//System.out.println("## bail"); 1936 // we are done here, nobody can handle this - <clinits> don't nest, there is no calling 1937 // context but we should maybe wrap it up into an ExceptionInInitializerError (even though 1938 // that makes it harder to read, and the indirection is not buying us anything) 1939 break; 1940          } 1941           1942        } else { // ! (insn instanceof InvokeInstruction) 1943 } 1944         1945        mi.leave(this); 1946         1947        // remove a frame 1948 popFrame(); 1949      } 1950       1951      // we keep the thread alive to ease post mortem debugging 1952 // <2do> really just required if we check for uncaught exceptions, 1953 // but we always do 1954 //finish(); // toast this thread 1955 } 1956 1957//System.out.println("## unhandled!"); 1958 1959    // Ok, I finally made my peace wuth UncaughtException - we can be called from various places, 1960 // including the VM (<clinit>, finalizer) and we can't rely on that all these locations check 1961 // for pc == null. Even if they would, at this point there is nothing to do anymore, get to the 1962 // NoUncaughtProperty reporting as quickly as possible, since chances are we would be even 1963 // obfuscating the problem 1964 NoUncaughtExceptionsProperty.setExceptionInfo(pendingException); 1965    throw new UncaughtException(this, objref); 1966  } 1967   1968  /** 1969   * Called when a lock is released. Updates the information 1970   * related to the locks. 1971   */ 1972  public void unlock (Ref ref) { 1973  } 1974   1975  protected void setStackFrameIndex (int i, int idx) { 1976    if (hasChanged.get(i) || ((i + 2) >= data.length) || 1977          (data[i + 2] != idx)) { 1978      stack[i] = (StackFrame) stackFramePool.getObject(idx); 1979    } 1980  } 1981   1982  protected int getStackFrameIndex (int i) { 1983    if (hasChanged.get(i)) { 1984      HashPool.PoolEntry e = stackFramePool.getEntry(stack[i]); 1985       1986      stack[i] = (StackFrame) e.getObject(); 1987       1988      return e.getIndex(); 1989    } else { 1990      return data[i + 2]; 1991    } 1992  } 1993   1994  protected void setThreadDataIndex (int idx) { 1995    if (tdIndex == idx) { 1996      return; 1997    } 1998     1999    tdIndex = idx; 2000    threadData = (ThreadData) threadDataPool.getObject(idx); 2001  } 2002   2003  protected int getThreadDataIndex () { 2004    if (tdIndex != -1) { 2005      return tdIndex; 2006    } 2007     2008    HashPool.PoolEntry e = threadDataPool.getEntry(threadData); 2009    threadData = (ThreadData) e.getObject(); 2010     2011    return tdIndex = e.getIndex(); 2012  } 2013     2014  /** 2015   * Executes a step where lines are atomic. 2016   * @return false if intermediate step (due to Nondeterminism or Buchi observable) 2017   */ 2018  protected boolean executeAtomicLinesStep () throws JPFException { 2019    atomicData.line = getLine(); 2020    atomicData.currentMethod = getMethod(); 2021    atomicData.inSameMethod = true; 2022     2023    int[] lines = atomicData.currentMethod.getLineNumbers(); 2024     2025    while (true) { 2026      Instruction pc = executeInstruction(); 2027       2028      if (list.ks.ss.violatedAssertion) { 2029        break; 2030      } 2031             2032      if (pc == null) { 2033        break; 2034      } 2035       2036      if (pc.isObservable()) { 2037        list.ks.ss.trail().setAnnotation("observable instruction"); 2038        return false; 2039      } 2040       2041      if (list.ks.ss.isIgnored()) { 2042        throw new IgnoreIfException(); 2043      } 2044       2045      if (!pc.isDeterministic(list.ks.ss, list.ks, this)) { 2046        return false; 2047      } 2048       2049      if (list.ks.atomicLevel > 0) { 2050        if (!isRunnable()) { 2051          throw new BlockedAtomicException(); 2052        } 2053         2054        continue; // we are still atomic, loop 2055 } 2056       2057      if (!isRunnable()) { 2058        break; 2059      } 2060       2061      // <?> pcm - how do we treat methods without line number tables? 2062 // Apparently, AspectJ does this, and I would assume the same for many 2063 // bytecode (re)writers 2064 if (!atomicData.inSameMethod || (lines == null) || 2065            (atomicData.line != lines[pc.getOffset()] && 2066               !(pc instanceof ReturnInstruction))) { 2067        atomicData.currentMethod = null; 2068        atomicData.line = -1; 2069         2070        break; 2071      } 2072    } 2073     2074    return true; 2075  } 2076     2077  /** 2078   * execute a step using on-the-fly partial order reduction 2079   */ 2080  protected boolean executePorStep () throws JPFException { 2081         2082    while (true) { 2083      Instruction pc = executeInstruction(); 2084             2085      if (list.ks.ss.violatedAssertion) { 2086        break; 2087      } 2088             2089      if (pc == null) { 2090        break; 2091      } 2092       2093      if (pc.isObservable()) { 2094        list.ks.ss.trail().setAnnotation("observable instruction"); 2095        return false; 2096      } 2097       2098      if (list.ks.ss.isIgnored()) { 2099        throw new IgnoreIfException(); 2100      } 2101       2102      if (!pc.isDeterministic(list.ks.ss, list.ks, this)) { 2103        return false; 2104      } 2105       2106      if (list.ks.atomicLevel > 0) { 2107        // <2do> this is dangerous with Object.wait(J) from an atomic 2108 // section in a lib method (like Thread.join()) ! 2109 if (!isRunnable()) { 2110          throw new BlockedAtomicException(); 2111        } 2112        continue; // we are still atomic, loop 2113 } 2114 2115      // this will catch MONITOR_ENTER/EXIT, wait, sync run, if they can't exec 2116 if (!isRunnable()) { 2117        return true; 2118      } 2119       2120      // this will filter out all insns which might alter the state differently 2121 // depending on the scheduling sequence 2122 // Thread.start : always 2123 // sync invoke, MonitorEnter/Exit : other runnable threads 2124 // field / array access : other runnable threads & multi-thread reachable 2125 // runnable wait/notify ?? 2126 if ( yield || pc.isSchedulingRelevant(list.ks.ss, list.ks, this)) { 2127        yield = false; 2128        break; 2129      } 2130    } 2131     2132    return true; 2133  } 2134   2135  /** 2136   * request a reschedule no matter what the next insn is 2137   * (can be used by listeners who directly modify thread states) 2138   */ 2139  public void yield () { 2140    yield = true; 2141  } 2142   2143  public boolean hasOtherRunnables () { 2144    return list.hasOtherRunnablesThan(index); 2145  } 2146   2147  /** 2148   * Returns a specific stack frame. 2149   */ 2150  protected StackFrame frame (int idx) { 2151    if (idx < 0) { 2152      idx += (stack.length - 1); 2153    } 2154     2155    return stack[idx]; 2156  } 2157   2158  /** 2159   * Returns a clone of a specific stack frame. 2160   */ 2161  protected StackFrame frameClone (int i) { 2162    if (i < 0) { 2163      i += (stack.length - 1); 2164    } 2165     2166    if (hasChanged.get(i)) { 2167      return stack[i]; 2168    } 2169     2170    hasChanged.set(i); 2171    anyChanged = true; 2172    list.ks.data = null; 2173     2174    if ((lowestChanged == -1) || (lowestChanged > i)) { 2175      lowestChanged = i; 2176    } 2177     2178    return stack[i] = (StackFrame) stack[i].clone(); 2179  } 2180   2181  /** 2182   * Returns a clone of the thread data. 2183   */ 2184  protected ThreadData threadDataClone () { 2185    if (tdIndex == -1) { 2186      return threadData; 2187    } 2188     2189    tdIndex = -1; 2190    list.ks.data = null; 2191     2192    return threadData = (ThreadData) threadData.clone(); 2193  } 2194   2195  /** 2196   * Returns the top stack frame. 2197   */ 2198  public StackFrame top () { 2199    if (stack.length > 0) { 2200      return stack[stack.length - 1]; 2201    } else { 2202      return null; 2203    } 2204  } 2205   2206  /** 2207   * Returns a clone of the top stack frame. 2208   */ 2209  protected StackFrame topClone () { 2210    int i = stack.length - 1; 2211     2212    if (hasChanged.get(i)) { 2213      return stack[i]; 2214    } 2215     2216    hasChanged.set(i); 2217    anyChanged = true; 2218    list.ks.data = null; 2219     2220    if ((lowestChanged == -1) || (lowestChanged > i)) { 2221      lowestChanged = i; 2222    } 2223     2224    return stack[i] = (StackFrame) stack[i].clone(); 2225  } 2226   2227  void setDaemon (boolean isDaemon) { 2228    threadDataClone().isDaemon = isDaemon; 2229  } 2230   2231  boolean isDaemon () { 2232    return threadData.isDaemon; 2233  } 2234   2235  MJIEnv getMJIEnv () { 2236    return env; 2237  } 2238   2239  void setName (String newName) { 2240    threadDataClone().name = newName; 2241     2242    // see 'setPriority()', only that it's more serious here, because the 2243 // java.lang.Thread name is stored as a char[] 2244 } 2245   2246  void setPriority (int newPrio) { 2247    if (threadData.priority != newPrio) { 2248      threadDataClone().priority = newPrio; 2249       2250      // note that we don't update the java.lang.Thread object, but 2251 // use our threadData value (which works because the object 2252 // values are just used directly from the Thread ctors (from where we pull 2253 // it out in our ThreadInfo ctor), and henceforth only via our intercepted 2254 // native getters 2255 } 2256  } 2257   2258  int getPriority () { 2259    return threadData.priority; 2260  } 2261   2262  /** 2263   * this is the method that factorizes common Thread object initialization 2264   * (get's called by all ctors). 2265   * BEWARE - it's hidden magic (undocumented), and should be replaced by our 2266   * own Thread impl at some point 2267   */ 2268  void init (int rGroup, int rRunnable, int rName, long stackSize, 2269             boolean setPriority) { 2270    DynamicArea da = JVM.getVM().getDynamicArea(); 2271    ElementInfo ei = da.get(rName); 2272     2273    ThreadData td = threadDataClone(); 2274    threadData.name = ei.asString(); 2275    threadData.target = rRunnable; 2276     2277    // stackSize and setPriority are only used by native subsystems 2278 } 2279   2280  /** 2281   * did we call the current method directly, i.e. no via a INVOKE bytecode insn? 2282   */ 2283  public boolean wasDirectCall () { 2284    return top().isDirectCall(); 2285  } 2286} 2287 2288 2289 2290 2291 2292 2293 2294 2295 2296 2297 2298

A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame Popular Tags