0001: //
0002: // Copyright (C) 2005 United States Government as represented by the
0003: // Administrator of the National Aeronautics and Space Administration
0004: // (NASA). All Rights Reserved.
0005: //
0006: // This software is distributed under the NASA Open Source Agreement
0007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
0008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
0009: // directory tree for the complete NOSA document.
0010: //
0011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
0012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
0013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
0014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
0015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
0016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
0017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
0018: //
0019: package gov.nasa.jpf.jvm;
0020:
0021: import gov.nasa.jpf.Config;
0022: import gov.nasa.jpf.JPFException;
0023: import gov.nasa.jpf.jvm.bytecode.INVOKESTATIC;
0024: import gov.nasa.jpf.jvm.bytecode.Instruction;
0025: import gov.nasa.jpf.jvm.bytecode.InvokeInstruction;
0026: import gov.nasa.jpf.jvm.bytecode.MONITORENTER;
0027: import gov.nasa.jpf.jvm.bytecode.ReturnInstruction;
0028: import gov.nasa.jpf.util.CoverageManager;
0029: import gov.nasa.jpf.util.Debug;
0030: import gov.nasa.jpf.util.HashData;
0031: import gov.nasa.jpf.util.HashPool;
0032:
0033: import java.io.PrintWriter;
0034:
0035: import java.util.BitSet;
0036: import java.util.Iterator;
0037: import java.util.LinkedList;
0038:
0039: /**
0040: * Represents a thread. It contains the state of the thread, static
0041: * information about the thread, and the stack frames.
0042: * Race detection and lock order also store some information
0043: * in this data structure.
0044: */
0045: public class ThreadInfo implements Storable {
0046:
0047: /** <2do> - just a bloody guess, we need to change the livelock detection */
0048: static final int LIVELOCK_STEPS = 5000;
0049:
0050: static final int NEW = 0;
0051: static final int RUNNING = 1;
0052:
0053: // thread is running, but has to acquire target/this lock on first op
0054: // (first insn in a synchronized run method)
0055: public static final int SYNC_RUNNING = 2;
0056: public static final int WAITING = 3;
0057: public static final int NOTIFIED = 4;
0058: public static final int STOPPED = 5;
0059: public static final int INTERRUPTED = 6;
0060: public static final int TERMINATED = 7;
0061:
0062: /**Pool used to store the thread data.*/
0063: protected static HashPool threadDataPool = new HashPool();
0064:
0065: /** Pool used to store the stack frames.*/
0066: protected static HashPool stackFramePool = new HashPool();
0067:
0068: static ThreadInfo current;
0069:
0070: /** do we want a forced reschedule */
0071: boolean yield;
0072:
0073: protected ExceptionInfo pendingException;
0074:
0075: /** backtrack-relevant Information about the thread */
0076: protected ThreadData threadData;
0077:
0078: /**
0079: * Some information about the thread that are used to handle
0080: * atomicity.
0081: */
0082: protected AtomicData atomicData;
0083:
0084: /**
0085: * The stack frames of the JVM.
0086: * <2do> pcm - right now this gets re-allocated on every push/pop,
0087: * turn it into a real stack at some point
0088: */
0089: protected StackFrame[] stack;
0090:
0091: /**
0092: * Reference of the thread list it is in.
0093: */
0094: public ThreadList list;
0095:
0096: /**
0097: * Position in the thread list.
0098: */
0099: public int index;
0100:
0101: /**
0102: * Contains the index of the thread data last used.
0103: */
0104: public int tdIndex = -1;
0105:
0106: /**
0107: * Identifies which thread has changed.
0108: */
0109: public BitSet hasChanged;
0110:
0111: /**
0112: * Set if any stack frame changed.
0113: */
0114: public boolean anyChanged;
0115:
0116: /**
0117: * Keeps the information from the last storing.
0118: */
0119: protected int[] data;
0120:
0121: /**
0122: * Remembers which is the lowest changed stack frame.
0123: */
0124: protected int lowestChanged;
0125:
0126: /**
0127: * cache for last return value (useful for direct calls that don't change the stack)
0128: */
0129: long returnValue;
0130:
0131: /**
0132: * not so nice we cross-couple the NativePeers with ThreadInfo,
0133: * but to carry on with the JNI analogy, a MJIEnv is clearly
0134: * owned by a thread (even though we don't have much ThreadInfo
0135: * state dependency in here (yet), hence the simplistic init)
0136: */
0137: MJIEnv env;
0138:
0139: /**
0140: * the VM we are running on. Bad backlink, but then again, we can't really
0141: * test a ThreadInfo outside a VM context anyways.
0142: * <2do> If we keep 'list' as a field, 'vm' might be moved over there
0143: * (all threads in the list share the same VM)
0144: */
0145: JVM vm;
0146:
0147: /**
0148: * list of lock objects currently held by this thread.
0149: * unfortunately, we cannot organize this as a stack, since it might get
0150: * restored (from the heap) in random order
0151: */
0152: LinkedList lockedObjects = new LinkedList();
0153:
0154: // the following parameters are configurable. Would be nice if we could keep
0155: // them on a per-instance basis, but there are a few locations
0156: // (e.g. ThreadList) where we loose the init context, and it's questionable
0157: // if we want to change this at runtime, or POR might make sense on a per-thread
0158: // basis
0159:
0160: /** do we halt on each throw, i.e. don't look for an exception handler?
0161: * Useful to find empty handler blocks, or misusd exceptions
0162: */
0163: static boolean haltOnThrow;
0164:
0165: /** is on-the-fly partial order in effect? */
0166: static boolean porInEffect;
0167:
0168: /** do we treat access of fields referring to objects that are reachable
0169: * from different threads as boundary steps (i.e. starting a new Transition)?
0170: */
0171: static boolean porFieldBoundaries;
0172:
0173: /** detect field synchronization (find locks which are used to synchronize
0174: * field access - if we have viable candidates, and we find the locks taken,
0175: * we don't treat access of the corresponding field as a boundary step
0176: */
0177: static boolean porSyncDetection;
0178:
0179: static boolean init(Config config) {
0180: threadDataPool = new HashPool();
0181: stackFramePool = new HashPool();
0182: current = null;
0183:
0184: haltOnThrow = config.getBoolean("vm.halt_on_throw");
0185: porInEffect = config.getBoolean("vm.por");
0186: porFieldBoundaries = config
0187: .getBoolean("vm.por.field_boundaries");
0188: porSyncDetection = config.getBoolean("vm.por.sync_detection");
0189:
0190: return true;
0191: }
0192:
0193: /**
0194: * Creates a new thread info. It is associated with the object
0195: * passed and sets the target object as well.
0196: */
0197: public ThreadInfo(JVM vm, int o) {
0198: DynamicArea da = vm.getDynamicArea();
0199: ElementInfo ei = da.get(o);
0200:
0201: this .vm = vm;
0202:
0203: threadData = new ThreadData();
0204: threadData.status = NEW;
0205:
0206: if (o != -1) {
0207: threadData.ci = ei.getClassInfo();
0208: }
0209:
0210: threadData.objref = o;
0211: threadData.target = -1;
0212: threadData.lockCount = 0;
0213:
0214: // this is nasty - 'priority', 'name', 'target' and 'group' are not taken
0215: // from the object, but set within the java.lang.Thread ctors
0216:
0217: atomicData = new AtomicData();
0218: atomicData.currentMethod = null;
0219: atomicData.line = -1;
0220: atomicData.inSameMethod = false;
0221:
0222: stack = new StackFrame[0];
0223:
0224: hasChanged = new BitSet();
0225: anyChanged = false;
0226: data = new int[0];
0227: lowestChanged = -1;
0228:
0229: env = new MJIEnv(this );
0230: }
0231:
0232: public ThreadInfo(ThreadInfo ti) {
0233: if (ti.tdIndex == -1) {
0234: threadData = (ThreadData) ti.threadData.clone();
0235: } else {
0236: threadData = ti.threadData;
0237: }
0238:
0239: atomicData = (AtomicData) ti.atomicData.clone();
0240:
0241: if (ti.stack != null) {
0242: int l = ti.stack.length;
0243: stack = new StackFrame[l];
0244:
0245: if (ti.anyChanged) {
0246: for (int i = 0; i < l; i++) {
0247: if (ti.hasChanged.get(i)) {
0248: stack[i] = (StackFrame) ti.stack[i].clone();
0249: } else {
0250: stack[i] = ti.stack[i];
0251: }
0252: }
0253: } else {
0254: System.arraycopy(ti.stack, 0, stack, 0, l);
0255: }
0256: } else {
0257: stack = null;
0258: }
0259:
0260: vm = ti.vm;
0261: list = null;
0262: index = -1;
0263: tdIndex = ti.tdIndex;
0264: hasChanged = (BitSet) ti.hasChanged.clone();
0265: anyChanged = ti.anyChanged;
0266: data = ti.data;
0267: lowestChanged = ti.lowestChanged;
0268:
0269: env = new MJIEnv(this );
0270: }
0271:
0272: /**
0273: * Creates a new empty thread info. Used to backtrack.
0274: */
0275: ThreadInfo(ThreadList l, int i) {
0276: list = l;
0277: index = i;
0278:
0279: stack = new StackFrame[0];
0280: tdIndex = -1;
0281: data = new int[0];
0282: hasChanged = new BitSet();
0283:
0284: vm = JVM.getVM(); // <2do> cut this
0285:
0286: env = new MJIEnv(this );
0287:
0288: // <2do> what about the other fields?
0289: }
0290:
0291: public static ThreadInfo getCurrent() {
0292: return current;
0293: }
0294:
0295: public boolean holdsLock(ElementInfo ei) {
0296: return lockedObjects.contains(ei);
0297: }
0298:
0299: public JVM getVM() {
0300: return vm;
0301: }
0302:
0303: public void setReturnValue(long ret) {
0304: returnValue = ret;
0305: }
0306:
0307: /**
0308: * the return value from the last StackFrame (that had a return)
0309: * Note: it's the callers responsibility to know about type and validity
0310: * (the method might have no / int / long return value)
0311: */
0312: public long getReturnValue() {
0313: return returnValue;
0314: }
0315:
0316: public boolean usePor() {
0317: return porInEffect;
0318: }
0319:
0320: public boolean usePorFieldBoundaries() {
0321: return porFieldBoundaries;
0322: }
0323:
0324: public boolean usePorSyncDetection() {
0325: return porSyncDetection;
0326: }
0327:
0328: /**
0329: * Checks if the thread is waiting to execute a nondeterministic choice
0330: * due to an abstraction, i.e. due to a Bandera.choose() call
0331: */
0332: public boolean isAbstractionNonDeterministic() {
0333: if (getPC() == null) {
0334: return false;
0335: }
0336:
0337: return getPC().examineAbstraction(list.ks.ss, list.ks, this );
0338: }
0339:
0340: /**
0341: * An alive thread is either running, waiting, notified, or interrupted.
0342: */
0343: public boolean isAlive() {
0344: return (threadData.status != TERMINATED);
0345: /*
0346: boolean alive = (threadData.status == RUNNING) ||
0347: (threadData.status == SYNC_RUNNING) ||
0348: (threadData.status == WAITING) ||
0349: (threadData.status == INTERRUPTED) ||
0350: (threadData.status == NOTIFIED);
0351:
0352: return alive;
0353: */
0354: }
0355:
0356: /**
0357: * Returns the information necessary to backtrack.
0358: */
0359: public Object getBacktrackData() {
0360: return atomicData.clone();
0361: }
0362:
0363: public boolean getBooleanLocal(String lname) {
0364: return Types.intToBoolean(getLocalVariable(lname));
0365: }
0366:
0367: public boolean getBooleanLocal(int lindex) {
0368: return Types.intToBoolean(getLocalVariable(lindex));
0369: }
0370:
0371: public boolean getBooleanLocal(int fr, String lname) {
0372: return Types.intToBoolean(getLocalVariable(fr, lname));
0373: }
0374:
0375: public boolean getBooleanLocal(int fr, int lindex) {
0376: return Types.intToBoolean(getLocalVariable(fr, lindex));
0377: }
0378:
0379: public boolean getBooleanReturnValue() {
0380: return Types.intToBoolean(peek());
0381: }
0382:
0383: public byte getByteLocal(String lname) {
0384: return (byte) getLocalVariable(lname);
0385: }
0386:
0387: public byte getByteLocal(int lindex) {
0388: return (byte) getLocalVariable(lindex);
0389: }
0390:
0391: public byte getByteLocal(int fr, String lname) {
0392: return (byte) getLocalVariable(fr, lname);
0393: }
0394:
0395: public byte getByteLocal(int fr, int lindex) {
0396: return (byte) getLocalVariable(fr, lindex);
0397: }
0398:
0399: public byte getByteReturnValue() {
0400: return (byte) peek();
0401: }
0402:
0403: public String[] getCallStack() {
0404: int size = stack.length;
0405: String[] callStack = new String[size];
0406:
0407: for (int i = 0; i < size; i++) {
0408: callStack[i] = frame(i).getStackTrace();
0409: }
0410:
0411: return callStack;
0412: }
0413:
0414: public String getCallStackClass(int i) {
0415: if (i < stack.length) {
0416: StackFrame fr = frame(i);
0417:
0418: return fr.getClassInfo().getName();
0419: }
0420:
0421: return null;
0422: }
0423:
0424: public String getCallStackFile(int i) {
0425: if (i < stack.length) {
0426: StackFrame fr = frame(i);
0427:
0428: return fr.getClassInfo().getSourceFileName();
0429: }
0430:
0431: return null;
0432: }
0433:
0434: public int getCallStackLine(int i) {
0435: if (i < stack.length) {
0436: StackFrame fr = frame(i);
0437:
0438: return fr.getLine();
0439: }
0440:
0441: return 0;
0442: }
0443:
0444: public String getCallStackMethod(int i) {
0445: if (i < stack.length) {
0446: StackFrame fr = frame(i);
0447:
0448: return fr.getMethodInfo().getName();
0449: }
0450:
0451: return null;
0452: }
0453:
0454: /**
0455: * Returns the this pointer of the callee from the stack.
0456: */
0457: public int getCalleeThis(MethodInfo mi) {
0458: return top().getCalleeThis(mi);
0459: }
0460:
0461: /**
0462: * Returns the this pointer of the callee from the stack.
0463: */
0464: public int getCalleeThis(int size) {
0465: return top().getCalleeThis(size);
0466: }
0467:
0468: public boolean isCalleeThis(Reference r) {
0469: if ((stack.length == 0) || (r == null)) {
0470: return false;
0471: }
0472:
0473: Instruction pc = getPC();
0474:
0475: if (pc == null) {
0476: return false;
0477: }
0478:
0479: if (!(pc instanceof InvokeInstruction)) {
0480: return false;
0481: }
0482:
0483: if (pc instanceof INVOKESTATIC) {
0484: return false;
0485: }
0486:
0487: InvokeInstruction i = (InvokeInstruction) pc;
0488:
0489: return getCalleeThis(Types.getArgumentsSize(i.signature) + 1) == ((ElementInfo) r)
0490: .getIndex();
0491: }
0492:
0493: public char getCharLocal(String lname) {
0494: return (char) getLocalVariable(lname);
0495: }
0496:
0497: public char getCharLocal(int lindex) {
0498: return (char) getLocalVariable(lindex);
0499: }
0500:
0501: public char getCharLocal(int fr, String lname) {
0502: return (char) getLocalVariable(fr, lname);
0503: }
0504:
0505: public char getCharLocal(int fr, int lindex) {
0506: return (char) getLocalVariable(fr, lindex);
0507: }
0508:
0509: public char getCharReturnValue() {
0510: return (char) peek();
0511: }
0512:
0513: /**
0514: * Returns the class information.
0515: */
0516: public ClassInfo getClassInfo() {
0517: return threadData.ci;
0518: }
0519:
0520: public double getDoubleLocal(String lname) {
0521: return Types.longToDouble(getLongLocalVariable(lname));
0522: }
0523:
0524: public double getDoubleLocal(int lindex) {
0525: return Types.longToDouble(getLongLocalVariable(lindex));
0526: }
0527:
0528: public double getDoubleLocal(int fr, String lname) {
0529: return Types.longToDouble(getLongLocalVariable(fr, lname));
0530: }
0531:
0532: public double getDoubleLocal(int fr, int lindex) {
0533: return Types.longToDouble(getLongLocalVariable(fr, lindex));
0534: }
0535:
0536: public double getDoubleReturnValue() {
0537: return Types.longToDouble(longPeek());
0538: }
0539:
0540: /**
0541: * An enabled thread is either running, notified, or interrupted.
0542: */
0543: public boolean isEnabled() {
0544: boolean isEnabled = (threadData.status == RUNNING)
0545: || (threadData.status == SYNC_RUNNING)
0546: || (threadData.status == INTERRUPTED)
0547: || (threadData.status == NOTIFIED);
0548: return isEnabled;
0549: }
0550:
0551: public float getFloatLocal(String lname) {
0552: return Types.intToFloat(getLocalVariable(lname));
0553: }
0554:
0555: public float getFloatLocal(int lindex) {
0556: return Types.intToFloat(getLocalVariable(lindex));
0557: }
0558:
0559: public float getFloatLocal(int fr, String lname) {
0560: return Types.intToFloat(getLocalVariable(fr, lname));
0561: }
0562:
0563: public float getFloatLocal(int fr, int lindex) {
0564: return Types.intToFloat(getLocalVariable(fr, lindex));
0565: }
0566:
0567: public float getFloatReturnValue() {
0568: return Types.intToFloat(peek());
0569: }
0570:
0571: public int getIntLocal(String lname) {
0572: return getLocalVariable(lname);
0573: }
0574:
0575: public int getIntLocal(int lindex) {
0576: return getLocalVariable(lindex);
0577: }
0578:
0579: public int getIntLocal(int fr, String lname) {
0580: return getLocalVariable(fr, lname);
0581: }
0582:
0583: public int getIntLocal(int fr, int lindex) {
0584: return getLocalVariable(fr, lindex);
0585: }
0586:
0587: public int getIntReturnValue() {
0588: return peek();
0589: }
0590:
0591: public boolean isInterrupted(boolean resetStatus) {
0592: boolean ret = (getStatus() == INTERRUPTED);
0593:
0594: if (resetStatus) {
0595: // <2do> pcm is that true? check the specs
0596: setStatus(RUNNING);
0597: }
0598:
0599: return ret;
0600: }
0601:
0602: /**
0603: * return our internal thread number (order of creation)
0604: */
0605: public int getIndex() {
0606: return index;
0607: }
0608:
0609: /**
0610: * Returns the line number of the program counter of the top stack frame.
0611: */
0612: public int getLine() {
0613: if (stack.length == 0)
0614: return -1;
0615:
0616: return top().getLine();
0617: }
0618:
0619: /**
0620: * Returns the line the thread is at.
0621: */
0622: public int getLine(int idx) {
0623: return frame(idx).getLine();
0624: }
0625:
0626: public String[] getLocalNames() {
0627: return top().getLocalVariableNames();
0628: }
0629:
0630: public String[] getLocalNames(int fr) {
0631: return frame(fr).getLocalVariableNames();
0632: }
0633:
0634: /**
0635: * Sets the value of a local variable.
0636: */
0637: public void setLocalVariable(int idx, int v, boolean ref) {
0638: topClone().setLocalVariable(idx, v, ref);
0639: }
0640:
0641: /**
0642: * Returns the value of a local variable in a particular frame.
0643: */
0644: public int getLocalVariable(int fr, int idx) {
0645: return frame(fr).getLocalVariable(idx);
0646: }
0647:
0648: /**
0649: * Returns the value of a local variable.
0650: */
0651: public int getLocalVariable(int idx) {
0652: return top().getLocalVariable(idx);
0653: }
0654:
0655: /**
0656: * Gets the value of a local variable from its name and frame.
0657: */
0658: public int getLocalVariable(int fr, String name) {
0659: return frame(fr).getLocalVariable(name);
0660: }
0661:
0662: /**
0663: * Gets the value of a local variable from its name.
0664: */
0665: public int getLocalVariable(String name) {
0666: return top().getLocalVariable(name);
0667: }
0668:
0669: /**
0670: * Checks if a local variable is a reference.
0671: */
0672: public boolean isLocalVariableRef(int idx) {
0673: return top().isLocalVariableRef(idx);
0674: }
0675:
0676: /**
0677: * Gets the type associated with a local variable.
0678: */
0679: public String getLocalVariableType(int fr, String name) {
0680: return frame(fr).getLocalVariableType(name);
0681: }
0682:
0683: /**
0684: * Gets the type associated with a local variable.
0685: */
0686: public String getLocalVariableType(String name) {
0687: return top().getLocalVariableType(name);
0688: }
0689:
0690: /**
0691: * Sets the number of locks held at the time of a wait.
0692: */
0693: public void setLockCount(int l) {
0694: if (threadData.lockCount != l) {
0695: threadDataClone().lockCount = l;
0696: }
0697: }
0698:
0699: /**
0700: * Returns the number of locks in the last wait.
0701: */
0702: public int getLockCount() {
0703: return threadData.lockCount;
0704: }
0705:
0706: public LinkedList getLockedObjects() {
0707: return lockedObjects;
0708: }
0709:
0710: public int[] getLockedObjectReferences() {
0711: int[] a = new int[lockedObjects.size()];
0712: int i = 0;
0713: for (Iterator it = lockedObjects.iterator(); it.hasNext();) {
0714: a[i++] = ((ElementInfo) it.next()).getIndex();
0715: }
0716:
0717: return a;
0718: }
0719:
0720: public long getLongLocal(String lname) {
0721: return getLongLocalVariable(lname);
0722: }
0723:
0724: public long getLongLocal(int lindex) {
0725: return getLongLocalVariable(lindex);
0726: }
0727:
0728: public long getLongLocal(int fr, String lname) {
0729: return getLongLocalVariable(fr, lname);
0730: }
0731:
0732: public long getLongLocal(int fr, int lindex) {
0733: return getLongLocalVariable(fr, lindex);
0734: }
0735:
0736: /**
0737: * Sets the value of a long local variable.
0738: */
0739: public void setLongLocalVariable(int idx, long v) {
0740: topClone().setLongLocalVariable(idx, v);
0741: }
0742:
0743: /**
0744: * Returns the value of a long local variable.
0745: */
0746: public long getLongLocalVariable(int fr, int idx) {
0747: return frame(fr).getLongLocalVariable(idx);
0748: }
0749:
0750: /**
0751: * Returns the value of a long local variable.
0752: */
0753: public long getLongLocalVariable(int idx) {
0754: return top().getLongLocalVariable(idx);
0755: }
0756:
0757: /**
0758: * Gets the value of a long local variable from its name.
0759: */
0760: public long getLongLocalVariable(int fr, String name) {
0761: return frame(fr).getLongLocalVariable(name);
0762: }
0763:
0764: /**
0765: * Gets the value of a long local variable from its name.
0766: */
0767: public long getLongLocalVariable(String name) {
0768: return top().getLongLocalVariable(name);
0769: }
0770:
0771: public long getLongReturnValue() {
0772: return longPeek();
0773: }
0774:
0775: /**
0776: * Returns the current method in the top stack frame.
0777: */
0778: public MethodInfo getMethod() {
0779: if (stack.length > 0) {
0780: return top().getMethodInfo();
0781: } else {
0782: return null;
0783: }
0784: }
0785:
0786: public boolean isInCtor() {
0787: // <2do> - hmm, if we don't do this the whole stack, we miss factored
0788: // init funcs
0789: MethodInfo mi = getMethod();
0790: return mi.isCtor();
0791: }
0792:
0793: /**
0794: * Returns the method info of a specific stack frame.
0795: */
0796: public MethodInfo getMethod(int idx) {
0797: if (stack.length > 0) {
0798: return frame(idx).getMethodInfo();
0799: } else {
0800: return null;
0801: }
0802: }
0803:
0804: public String getName() {
0805: return threadData.name;
0806: }
0807:
0808: /**
0809: * Checks if the thread is waiting to execute a nondeterministic choice,
0810: * due to the use of Verify.random... calls.
0811: *
0812: * <?> pcm - this is not called anywhere, but is part of the 'iThreadInfo'
0813: * interface. We clean this up when we remove the interface
0814: */
0815: public boolean isNonDeterministic() {
0816: if (getPC() == null) {
0817: return false;
0818: }
0819:
0820: return !getPC().isDeterministic(list.ks.ss, list.ks, this );
0821: }
0822:
0823: public Reference getObjectLocal(String lname) {
0824: return list.ks.da.get(getLocalVariable(lname));
0825: }
0826:
0827: public Reference getObjectLocal(int lindex) {
0828: return list.ks.da.get(getLocalVariable(lindex));
0829: }
0830:
0831: public Reference getObjectLocal(int fr, String lname) {
0832: return list.ks.da.get(getLocalVariable(fr, lname));
0833: }
0834:
0835: public Reference getObjectLocal(int fr, int lindex) {
0836: return list.ks.da.get(getLocalVariable(fr, lindex));
0837: }
0838:
0839: /**
0840: * Returns the object reference.
0841: */
0842: public int getObjectReference() {
0843: return threadData.objref;
0844: }
0845:
0846: public Reference getObjectReturnValue() {
0847: return list.ks.da.get(peek());
0848: }
0849:
0850: public Object getOperandAttr() {
0851: return top().getOperandAttr();
0852: }
0853:
0854: public Object getOperandAttr(int opStackOffset) {
0855: return top().getOperandAttr(opStackOffset);
0856: }
0857:
0858: public void setOperandAttr(Object attr) {
0859: top().setOperandAttr(attr);
0860: }
0861:
0862: /**
0863: * Checks if the top operand is a reference.
0864: */
0865: public boolean isOperandRef() {
0866: return top().isOperandRef();
0867: }
0868:
0869: /**
0870: * Checks if an operand is a reference.
0871: */
0872: public boolean isOperandRef(int idx) {
0873: return top().isOperandRef(idx);
0874: }
0875:
0876: /**
0877: * Sets the program counter of the top stack frame.
0878: */
0879: public void setPC(Instruction pc) {
0880: topClone().setPC(pc);
0881: }
0882:
0883: /**
0884: * Returns the program counter of a stack frame.
0885: */
0886: public Instruction getPC(int i) {
0887: return frame(i).getPC();
0888: }
0889:
0890: /**
0891: * Returns the program counter of the top stack frame.
0892: */
0893: public Instruction getPC() {
0894: if (stack.length == 0) {
0895: return null;
0896: }
0897:
0898: return top().getPC();
0899: }
0900:
0901: public ExceptionInfo getPendingException() {
0902: return pendingException;
0903: }
0904:
0905: /**
0906: * Returns true if it is possible to execute the next instruction
0907: * of this thread. This function is used by the scheduler to determine
0908: * which threads can be executed.
0909: *
0910: * <?> pcm - watch out, it's not just used from Scheduler, but also from
0911: * within ThreadInfo itself
0912: */
0913: public boolean isRunnable() {
0914: if (!isEnabled()) {
0915: // this filters out waits
0916: return false;
0917: }
0918:
0919: // this is for newly created threads with synchronized run() methods
0920: if (threadData.status == SYNC_RUNNING) {
0921: int sync = (threadData.target != -1) ? threadData.target
0922: : threadData.objref;
0923: ElementInfo ei = list.ks.da.get(sync);
0924:
0925: if ((ei != null) && !ei.canLock(this )) {
0926: return false;
0927: }
0928: }
0929:
0930: Instruction pc = getPC();
0931:
0932: if (pc == null) {
0933: return false;
0934: }
0935:
0936: // the instruction needs to be executable as well
0937: // pcm - for now, this is about insns which might require a lock in order to be
0938: // executable (invokeX,monitorEnter)
0939: return pc.isExecutable(list.ks.ss, list.ks, this );
0940: }
0941:
0942: public short getShortLocal(String lname) {
0943: return (short) getLocalVariable(lname);
0944: }
0945:
0946: public short getShortLocal(int lindex) {
0947: return (short) getLocalVariable(lindex);
0948: }
0949:
0950: public short getShortLocal(int fr, String lname) {
0951: return (short) getLocalVariable(fr, lname);
0952: }
0953:
0954: public short getShortLocal(int fr, int lindex) {
0955: return (short) getLocalVariable(fr, lindex);
0956: }
0957:
0958: public short getShortReturnValue() {
0959: return (short) peek();
0960: }
0961:
0962: /**
0963: * get the current stack trace of this thread
0964: * this is called during creation of a Throwable, hence we should skip
0965: * all throwable ctors in here
0966: * <2do> this is only a partial solution,since we don't catch exceptions
0967: * in Throwable ctors yet
0968: */
0969: public String getStackTrace() {
0970: StringBuffer sb = new StringBuffer(256);
0971:
0972: for (int i = stack.length - 1; i >= 0; i--) {
0973: StackFrame sf = frame(i);
0974: MethodInfo mi = sf.getMethodInfo();
0975:
0976: if (mi.isCtor()) {
0977: ClassInfo ci = mi.getClassInfo();
0978: if (ci.instanceOf("java.lang.Throwable")) {
0979: continue;
0980: }
0981: }
0982:
0983: sb.append(frame(i).getStackTrace());
0984: sb.append("\n");
0985: }
0986:
0987: return sb.toString();
0988: }
0989:
0990: /**
0991: * Updates the status of the thread.
0992: */
0993: public void setStatus(int s) {
0994: if (threadData.status != s) {
0995:
0996: if ((s == RUNNING) || (s == SYNC_RUNNING)) {
0997: JVM.getVM().notifyThreadStarted(this );
0998: } else if (s == TERMINATED) {
0999: JVM.getVM().notifyThreadTerminated(this );
1000: }
1001:
1002: threadDataClone().status = s;
1003: }
1004: }
1005:
1006: /**
1007: * Returns the current status of the thread.
1008: */
1009: public int getStatus() {
1010: return threadData.status;
1011: }
1012:
1013: /**
1014: * Returns the information necessary to store.
1015: *
1016: * <2do> pcm - not clear to me how lower stack frames can contribute to
1017: * a different threadinfo state hash - only the current one can be changed
1018: * by the executing method
1019: */
1020: public int[] getStoringData() {
1021: int length = stack.length;
1022:
1023: int[] data = new int[length + 2];
1024: data[0] = getThreadDataIndex();
1025: data[1] = length;
1026:
1027: if (anyChanged) {
1028: if (lowestChanged > 0) {
1029: System.arraycopy(this .data, 2, data, 2, lowestChanged);
1030: }
1031:
1032: for (int i = lowestChanged, j = i + 2; i < length; i++, j++) {
1033: data[j] = getStackFrameIndex(i);
1034: }
1035: } else if (length > 0) {
1036: System.arraycopy(this .data, 2, data, 2, length);
1037: }
1038:
1039: anyChanged = false;
1040: hasChanged = new BitSet();
1041: lowestChanged = -1;
1042:
1043: this .data = data;
1044:
1045: return data;
1046: }
1047:
1048: public String getStringLocal(String lname) {
1049: return list.ks.da.get(getLocalVariable(lname)).asString();
1050: }
1051:
1052: public String getStringLocal(int lindex) {
1053: return list.ks.da.get(getLocalVariable(lindex)).asString();
1054: }
1055:
1056: public String getStringLocal(int fr, String lname) {
1057: return list.ks.da.get(getLocalVariable(fr, lname)).asString();
1058: }
1059:
1060: public String getStringLocal(int fr, int lindex) {
1061: return list.ks.da.get(getLocalVariable(fr, lindex)).asString();
1062: }
1063:
1064: public String getStringReturnValue() {
1065: return list.ks.da.get(peek()).asString();
1066: }
1067:
1068: /**
1069: * Sets the target of the thread.
1070: */
1071: public void setTarget(int t) {
1072: if (threadData.target != t) {
1073: threadDataClone().target = t;
1074: }
1075: }
1076:
1077: /**
1078: * Returns the object reference of the target.
1079: */
1080: public int getTarget() {
1081: return threadData.target;
1082: }
1083:
1084: /**
1085: * Returns the pointer to the object reference of the executing method
1086: */
1087: public int getThis() {
1088: return top().getThis();
1089: }
1090:
1091: public boolean isThis(Reference r) {
1092: if (r == null) {
1093: return false;
1094: }
1095:
1096: if (stack.length == 0) {
1097: return false;
1098: }
1099:
1100: return getMethod().isStatic() ? false : ((ElementInfo) r)
1101: .getIndex() == getLocalVariable(0);
1102: }
1103:
1104: public boolean atInvoke(String mname) {
1105: if (stack.length == 0) {
1106: return false;
1107: }
1108:
1109: Instruction pc = getPC();
1110:
1111: if (!(pc instanceof InvokeInstruction)) {
1112: return false;
1113: }
1114:
1115: InvokeInstruction i = (InvokeInstruction) pc;
1116:
1117: return mname.equals(i.cname + "." + i.mname);
1118: }
1119:
1120: public boolean atLabel(String label) {
1121: return Labels.isAt(label, this );
1122: }
1123:
1124: public boolean atMethod(String mname) {
1125: if (stack.length == 0) {
1126: return false;
1127: }
1128:
1129: return getMethod().getCompleteName().equals(mname);
1130: }
1131:
1132: public boolean atPosition(int position) {
1133: if (stack.length == 0) {
1134: return false;
1135: }
1136:
1137: Instruction pc = getPC();
1138:
1139: if (pc == null) {
1140: return false;
1141: }
1142:
1143: return pc.getPosition() == position;
1144: }
1145:
1146: public boolean atReturn() {
1147: if (stack.length == 0) {
1148: return false;
1149: }
1150:
1151: Instruction pc = getPC();
1152:
1153: if (pc == null) {
1154: return false;
1155: }
1156:
1157: return pc instanceof ReturnInstruction;
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,
1270: String fileName, int line) {
1271: DynamicArea da = DynamicArea.getHeap();
1272:
1273: ClassInfo ci = ClassInfo
1274: .getClassInfo("java.lang.StackTraceElement");
1275: int sRef = da.newObject(ci, this );
1276:
1277: ElementInfo sei = da.get(sRef);
1278: sei.setReferenceField("clsName", da.newString(clsName, this ));
1279: sei.setReferenceField("mthName", da.newString(mthName, this ));
1280: sei.setReferenceField("fileName", da.newString(fileName, this ));
1281: sei.setIntField("line", line);
1282:
1283: return sRef;
1284: }
1285:
1286: public int getStackTrace(int objref) {
1287: DynamicArea da = DynamicArea.getHeap();
1288: int stackDepth = countStackFrames();
1289: int i, j = 0;
1290: int aRef;
1291: ElementInfo aei;
1292:
1293: // are we executing in a native method? If yes, it's not on the stack
1294: MethodInfo nativeMth = env.getMethodInfo();
1295: if (nativeMth != null) {
1296: aRef = da.newArray("Ljava/lang/StackTraceElement",
1297: stackDepth + 1, this );
1298: aei = da.get(aRef);
1299:
1300: aei.setElement(j++, createStackTraceElement(nativeMth
1301: .getClassInfo().getName(), nativeMth.getName(),
1302: nativeMth.getClassInfo().getSourceFileName(), -1));
1303: } else {
1304: aRef = da.newArray("Ljava/lang/StackTraceElement",
1305: stackDepth, this );
1306: aei = da.get(aRef);
1307: }
1308:
1309: for (i = stackDepth - 1; i >= 0; i--, j++) {
1310: aei.setElement(j, createStackTraceElement(
1311: getCallStackClass(i), getCallStackMethod(i),
1312: getCallStackFile(i), getCallStackLine(i)));
1313: }
1314:
1315: return aRef;
1316: }
1317:
1318: void print(PrintWriter pw, String s) {
1319: if (pw != null) {
1320: pw.print(s);
1321: } else {
1322: vm.print(s);
1323: }
1324: }
1325:
1326: public void printStackTrace(int objRef) {
1327: printStackTrace(null, objRef);
1328: }
1329:
1330: public void printPendingExceptionOn(PrintWriter pw) {
1331: if (pendingException != null) {
1332: printStackTrace(pw, pendingException
1333: .getExceptionReference());
1334: }
1335: }
1336:
1337: public void printStackTrace(PrintWriter pw, int objRef) {
1338: // 'env' usage is not ideal, since we don't know from what context we are called, and
1339: // hence the MJIEnv calling context might not be set (no Method or ClassInfo)
1340: // on the other hand, we don't want to re-implement all the MJIEnv accessor methods
1341: print(pw, env.getClassInfo(objRef).getName());
1342:
1343: int msgRef = env.getReferenceField(objRef, "detailMessage");
1344: if (msgRef != MJIEnv.NULL) {
1345: print(pw, ": ");
1346: print(pw, env.getStringObject(msgRef));
1347: }
1348: print(pw, "\n");
1349:
1350: int aRef = env.getReferenceField(objRef, "stackTrace"); // StackTrace[]
1351: if (aRef != MJIEnv.NULL) {
1352: int len = env.getArrayLength(aRef);
1353: for (int i = 0; i < len; i++) {
1354: int sRef = env.getReferenceArrayElement(aRef, i);
1355: String clsName = env.getStringObject(env
1356: .getReferenceField(sRef, "clsName"));
1357: String mthName = env.getStringObject(env
1358: .getReferenceField(sRef, "mthName"));
1359: String fileName = env.getStringObject(env
1360: .getReferenceField(sRef, "fileName"));
1361: int line = env.getIntField(sRef, "line");
1362:
1363: print(pw, "\tat ");
1364: print(pw, clsName);
1365: print(pw, ".");
1366: print(pw, mthName);
1367: print(pw, "(");
1368: print(pw, fileName);
1369: print(pw, ":");
1370:
1371: if (line < 0) {
1372: print(pw, "native");
1373: } else {
1374: print(pw, Integer.toString(line));
1375: }
1376:
1377: print(pw, ")");
1378: print(pw, "\n");
1379: }
1380: }
1381: }
1382:
1383: // <2do> - not yet functional, fix free calls!!
1384: void callThrowableCtor(ClassInfo ci, int objRef, int msgRef) {
1385: MethodInfo mi = ci
1386: .getMethod("<init>(Ljava/lang/String;)", true);
1387: if (mi != null) {
1388: push(objRef, true);
1389: push(msgRef, true);
1390: executeMethod(mi);
1391: }
1392: }
1393:
1394: /**
1395: * Creates an exception and throws it.
1396: */
1397: public Instruction createAndThrowException(ClassInfo ci,
1398: String details) {
1399: DynamicArea da = DynamicArea.getHeap();
1400: int objref = da.newObject(ci, this );
1401: int msgref = -1;
1402:
1403: ElementInfo ei = da.get(objref);
1404:
1405: // <2do> pcm - this is not correct! We have to call a propper ctor
1406: // for the Throwable (for now, we just explicitly set the details)
1407: if (details != null) {
1408: msgref = da.newString(details, this );
1409: ei.setReferenceField("detailMessage",
1410: "java.lang.Throwable", msgref);
1411: }
1412:
1413: return throwException(objref);
1414: }
1415:
1416: /**
1417: * Creates an exception and throws it.
1418: */
1419: public Instruction createAndThrowException(String cname) {
1420: return createAndThrowException(ClassInfo.getClassInfo(cname),
1421: null);
1422: }
1423:
1424: public Instruction createAndThrowException(String cname,
1425: String details) {
1426: return createAndThrowException(ClassInfo.getClassInfo(cname),
1427: details);
1428: }
1429:
1430: /**
1431: * Duplicates a value on the top stack frame.
1432: */
1433: public void dup() {
1434: topClone().dup();
1435: }
1436:
1437: /**
1438: * Duplicates a long value on the top stack frame.
1439: */
1440: public void dup2() {
1441: topClone().dup2();
1442: }
1443:
1444: /**
1445: * Duplicates a long value on the top stack frame.
1446: */
1447: public void dup2_x1() {
1448: topClone().dup2_x1();
1449: }
1450:
1451: /**
1452: * Duplicates a long value on the top stack frame.
1453: */
1454: public void dup2_x2() {
1455: topClone().dup2_x2();
1456: }
1457:
1458: /**
1459: * Duplicates a value on the top stack frame.
1460: */
1461: public void dup_x1() {
1462: topClone().dup_x1();
1463: }
1464:
1465: /**
1466: * Duplicates a value on the top stack frame.
1467: */
1468: public void dup_x2() {
1469: topClone().dup_x2();
1470: }
1471:
1472: /**
1473: * Execute next instruction.
1474: */
1475: public Instruction executeInstruction() {
1476: // this is for threads with synchronized run() methods
1477: // (where we have to grab the lock as soon as we start to execute, no
1478: // matter what the insn is)
1479: if (threadData.status == SYNC_RUNNING) {
1480: int sync = (threadData.target != -1) ? threadData.target
1481: : threadData.objref;
1482: ElementInfo ei = list.ks.da.get(sync);
1483: // gets unlocked when we return from run();
1484: ei.lock(this );
1485: setStatus(RUNNING);
1486: }
1487:
1488: Instruction pc = getPC();
1489:
1490: CoverageManager.incInstruction(pc, index); // <2do> should be a listener!
1491:
1492: TrailInfo trail = list.ks.ss.trail();
1493: Step step = new Step(getMethod().getClassInfo()
1494: .getSourceFileName(), getLine(), pc);
1495: trail.addStep(step);
1496:
1497: if (pc.isFirstInstruction() && getMethod().isAtomic()) {
1498: list.ks.setAtomic();
1499: }
1500:
1501: //System.out.println("@ " + pc.getMethod().getCompleteName() + " " + pc.getPosition() + " : " + pc);
1502: // execute the next bytecode
1503: Instruction nextPc = pc.execute(list.ks.ss, list.ks, this );
1504:
1505: // we did not return from the last frame stack
1506: if (stack.length != 0) {
1507: setPC(nextPc);
1508: }
1509:
1510: // here we have our bytecode exec observation point
1511: // (note we have to do this after we have set the pc, since a listener
1512: // might come back to do checks like isRunnable)
1513: vm.notifyInstructionExecuted(this , pc, nextPc);
1514:
1515: return nextPc;
1516: }
1517:
1518: /**
1519: * Executes a method call. It executes the whole method as one atomic step and
1520: * returns when the call is over Arguments have to be already on the stack
1521: *
1522: * This is our entry point for calling methods without corresponding
1523: * INVOKE insns (e.g. <clinit>(), finalize() or method executions from native code
1524: */
1525: public void executeMethod(MethodInfo mi) {
1526: int depth = countStackFrames();
1527:
1528: mi.execute(this , true);
1529:
1530: KernelState ks = list.ks;
1531: SystemState ss = ks.ss;
1532:
1533: while (depth < countStackFrames()) {
1534: Instruction pc = executeInstruction();
1535:
1536: if (ss.violatedAssertion) {
1537: break;
1538: }
1539:
1540: if (pc == null) { // might be a thread in static init
1541: break;
1542: }
1543:
1544: if (!pc.isExecutable(ss, ks, this )) {
1545: throw new BlockedAtomicException();
1546: }
1547: }
1548: }
1549:
1550: /**
1551: * Executes next step.
1552: * @return false if intermediate step (due to Nondeterminism or Buchi observable)
1553: */
1554: public boolean executeStep() throws JPFException {
1555: current = this ;
1556:
1557: if (porInEffect) {
1558: return executePorStep();
1559: } else {
1560: return executeAtomicLinesStep();
1561: }
1562: }
1563:
1564: // we just got our last stack frame popped, so it's time to close down
1565: public void finish() {
1566: setStatus(TERMINATED);
1567:
1568: // need to own the lock before we can notify
1569: int objref = getObjectReference();
1570: ElementInfo ei = list.ks.da.get(objref);
1571:
1572: ei.lock(this );
1573: ei.notifiesAll();
1574: ei.unlock(this );
1575:
1576: // stack is gone, so reachability might change
1577: list.ks.ss.activateGC();
1578:
1579: //list.remove(index);
1580: }
1581:
1582: public void hash(HashData hd) {
1583: threadData.hash(hd);
1584: atomicData.hash(hd);
1585:
1586: for (int i = 0, l = stack.length; i < l; i++) {
1587: frame(i).hash(hd);
1588: }
1589: }
1590:
1591: public int hashCode() {
1592: HashData hd = new HashData();
1593:
1594: hash(hd);
1595:
1596: return hd.getValue();
1597: }
1598:
1599: public void interrupt() {
1600: if (getStatus() != WAITING) {
1601: return;
1602: }
1603:
1604: setStatus(INTERRUPTED);
1605: }
1606:
1607: /**
1608: * Called when a lock is acquired. Updates the information
1609: * related to the locks.
1610: */
1611: public void lock(Ref ref) {
1612: }
1613:
1614: public void log() {
1615: Debug.println(Debug.MESSAGE, "TH#" + index + " #"
1616: + threadData.target + " #" + threadData.objref + " "
1617: + threadData.status);
1618:
1619: for (int i = 0; i < stack.length; i++) {
1620: frame(i).log(i);
1621: }
1622: }
1623:
1624: /**
1625: * Peeks the top long value from the top stack frame.
1626: */
1627: public long longPeek() {
1628: return top().longPeek();
1629: }
1630:
1631: /**
1632: * Peeks a long value from the top stack frame.
1633: */
1634: public long longPeek(int n) {
1635: return top().longPeek(n);
1636: }
1637:
1638: /**
1639: * Pops the top long value from the top stack frame.
1640: */
1641: public long longPop() {
1642: return topClone().longPop();
1643: }
1644:
1645: /**
1646: * Pushes a long value of the top stack frame.
1647: */
1648: public void longPush(long v) {
1649: topClone().longPush(v);
1650: }
1651:
1652: /**
1653: * mark all objects during gc phase1 which are reachable from this threads
1654: * root set (Thread object, Runnable, stack)
1655: * @aspects: gc
1656: */
1657: void markRoots() {
1658: DynamicArea heap = DynamicArea.getHeap();
1659:
1660: // 1. mark the Thread object itself
1661: heap.markThreadRoot(threadData.objref, index);
1662:
1663: // 2. and its runnable
1664: if (threadData.target != -1) {
1665: heap.markThreadRoot(threadData.target, index);
1666: }
1667:
1668: // 3. now all references on the stack
1669: for (int i = 0, l = stack.length; i < l; i++) {
1670: frame(i).markThreadRoots(index);
1671: }
1672: }
1673:
1674: /**
1675: * Adds a new stack frame for a new called method.
1676: *
1677: * <2do> - turn this into a real stack - don't reallocate
1678: */
1679: public void pushFrame(StackFrame frame) {
1680: atomicData.inSameMethod = false;
1681:
1682: int depth = stack.length;
1683: StackFrame[] n = new StackFrame[depth + 1];
1684: System.arraycopy(stack, 0, n, 0, depth);
1685: stack = n;
1686:
1687: stack[depth] = frame;
1688:
1689: hasChanged.set(depth);
1690: anyChanged = true;
1691: list.ks.data = null;
1692:
1693: if ((lowestChanged == -1) || (lowestChanged > depth)) {
1694: lowestChanged = depth;
1695: }
1696: }
1697:
1698: public ElementInfo objectAtBlockedSynchronized() {
1699: if (stack.length == 0) {
1700: return null;
1701: }
1702:
1703: Instruction pc = getPC();
1704:
1705: if (pc == null) {
1706: return null;
1707: }
1708:
1709: if (pc instanceof InvokeInstruction) {
1710: if (!getMethod().canEnter(this )) {
1711: return getMethod().getBlockedObject(this , true);
1712: }
1713: }
1714:
1715: if (pc instanceof MONITORENTER) {
1716: if (!pc.isExecutable(list.ks.ss, list.ks, this )) {
1717: return list.ks.da.get(peek());
1718: }
1719: }
1720:
1721: return null;
1722: }
1723:
1724: /**
1725: * Peeks the top value from the top stack frame.
1726: */
1727: public int peek() {
1728: if (stack.length > 0) {
1729: return top().peek();
1730: } else {
1731: // <?> not really sure what to do here, but if the stack is gone, so is the thread
1732: return -1;
1733: }
1734: }
1735:
1736: /**
1737: * Peeks a int value from the top stack frame.
1738: */
1739: public int peek(int n) {
1740: if (stack.length > 0) {
1741: return top().peek(n);
1742: } else {
1743: // <?> see peek()
1744: return -1;
1745: }
1746: }
1747:
1748: /**
1749: * Pops the top value from the top stack frame.
1750: */
1751: public int pop() {
1752: if (stack.length > 0) {
1753: return topClone().pop();
1754: } else {
1755: // <?> see peek()
1756: return -1;
1757: }
1758: }
1759:
1760: /**
1761: * Pops a set of values from the top stack frame.
1762: */
1763: public void pop(int n) {
1764: if (stack.length > 0) {
1765: topClone().pop(n);
1766: }
1767: }
1768:
1769: /**
1770: * Removes a stack frame.
1771: */
1772: public boolean popFrame() {
1773: int last = stack.length - 1;
1774: StackFrame sf = stack[last];
1775:
1776: if (getMethod().isAtomic()) {
1777: list.ks.clearAtomic();
1778: }
1779:
1780: if (sf.hasAnyRef()) {
1781: ((SystemState) JVM.getVM().getSystemState()).activateGC();
1782: }
1783:
1784: StackFrame[] n = new StackFrame[last];
1785: System.arraycopy(stack, 0, n, 0, last);
1786: stack = n;
1787:
1788: if (last == 0) {
1789: atomicData.inSameMethod = false;
1790: finish();
1791: } else {
1792: atomicData.inSameMethod = (getMethod() == atomicData.currentMethod);
1793: }
1794:
1795: hasChanged.set(last);
1796: anyChanged = true;
1797: list.ks.data = null;
1798:
1799: if ((lowestChanged == -1) || (lowestChanged > last)) {
1800: lowestChanged = last;
1801: }
1802:
1803: return (last > 0);
1804: }
1805:
1806: public void printInternalErrorTrace(Throwable e) {
1807: String msg = e.getMessage();
1808:
1809: if (msg != null) {
1810: Debug.println(Debug.ERROR, "exception "
1811: + e.getClass().getName() + ": " + msg);
1812: } else {
1813: Debug.println(Debug.ERROR, "exception "
1814: + e.getClass().getName());
1815: }
1816:
1817: printStackTrace();
1818:
1819: if (msg != null) {
1820: Debug.println(Debug.ERROR, "exception "
1821: + e.getClass().getName() + ": " + msg);
1822: } else {
1823: Debug.println(Debug.ERROR, "exception "
1824: + e.getClass().getName());
1825: }
1826:
1827: printStackContent();
1828: }
1829:
1830: /**
1831: * Prints the content of the stack.
1832: */
1833: public void printStackContent() {
1834: for (int i = stack.length - 1; i >= 0; i--) {
1835: frame(i).printStackContent();
1836: }
1837: }
1838:
1839: /**
1840: * Prints the trace of the stack.
1841: */
1842: public void printStackTrace() {
1843: for (int i = stack.length - 1; i >= 0; i--) {
1844: frame(i).printStackTrace();
1845: }
1846: }
1847:
1848: /**
1849: * Pushes a value on the top stack frame.
1850: */
1851: public void push(int v, boolean ref) {
1852: if (stack.length > 0) { // otherwise we don't have anything to push onto
1853: topClone().push(v, ref);
1854: }
1855: }
1856:
1857: /**
1858: * Removes the arguments of a method call.
1859: */
1860: public void removeArguments(MethodInfo mi) {
1861: int i = mi.getArgumentsSize();
1862:
1863: if (i != 0) {
1864: pop(i);
1865: }
1866: }
1867:
1868: /**
1869: * Swaps two entry on the stack.
1870: */
1871: public void swap() {
1872: topClone().swap();
1873: }
1874:
1875: /**
1876: * Throws an exception throught the stack frames.
1877: */
1878: public Instruction throwException(int objref) {
1879: DynamicArea da = DynamicArea.getHeap();
1880: ElementInfo ei = da.get(objref);
1881: ClassInfo ci = ei.getClassInfo();
1882: MethodInfo mi;
1883: Instruction insn;
1884: int nFrames = countStackFrames();
1885: int i, j;
1886:
1887: //System.out.println("## ---- got: " + ci.getName());
1888:
1889: // we need to store the stack trace in the exception object before
1890: // we start to unwind the stack looking for a handler. Unfortunately,
1891: // the stack dump is accessible for the application, so we have to
1892: // create it in JPF object land
1893: int stRef = getStackTrace(objref);
1894: ei
1895: .setReferenceField("stackTrace", "java.lang.Throwable",
1896: stRef);
1897:
1898: // but we still keep this in JPF itself too, so that it's more accessible
1899: // for post-mortem 'debugging', and preserves as much JPF execution
1900: // state as possible (e.g. prevents subsequent GC)
1901: pendingException = new ExceptionInfo(this , ei);
1902:
1903: vm.notifyExceptionThrown(this , ei);
1904:
1905: if (!haltOnThrow) {
1906: for (j = 0; j < nFrames; j++) {
1907: mi = getMethod();
1908: insn = getPC();
1909:
1910: ExceptionHandler[] exceptions = mi.getExceptions();
1911: //System.out.println("## unwinding to: " + mi.getClassInfo().getName() + "." + mi.getUniqueName());
1912: // this is the point where we can check for
1913: // "articifial" stack frames. There is no corresponding
1914: // INVOKE instruction in the frame underneath
1915: if ((j == 0) || (insn instanceof InvokeInstruction)) {
1916: int p = insn.getPosition();
1917:
1918: if (exceptions != null) {
1919: // checks the exception catched in order
1920: for (i = 0; i < exceptions.length; i++) {
1921: ExceptionHandler eh = exceptions[i];
1922:
1923: // if it falls in the right range
1924: if ((p >= eh.getBegin())
1925: && (p <= eh.getEnd())) {
1926: String en = eh.getName();
1927: //System.out.println("## checking: " + ci.getName() + " handler: " + en + " depth: " + stack.length);
1928:
1929: // checks if this type of exception is caught here
1930: if ((en == null) || ci.instanceOf(en)) {
1931: //System.out.println("## handle");
1932: // clears all the operand stack
1933: clearOperandStack();
1934:
1935: // pushes the exception on the stack instead
1936: push(objref, true);
1937:
1938: // jumps to the exception handler
1939: Instruction startOfHandlerBlock = mi
1940: .getInstructionAt(eh
1941: .getHandler());
1942: setPC(startOfHandlerBlock); // set! we might be in a isDeterministic / isRunnable
1943:
1944: pendingException = null; // handled, no need to keep it
1945:
1946: return startOfHandlerBlock;
1947: }
1948: }
1949: }
1950: }
1951:
1952: if ("<clinit>".equals(mi.getName())) {
1953: //System.out.println("## bail");
1954: // we are done here, nobody can handle this - <clinits> don't nest, there is no calling
1955: // context but we should maybe wrap it up into an ExceptionInInitializerError (even though
1956: // that makes it harder to read, and the indirection is not buying us anything)
1957: break;
1958: }
1959:
1960: } else { // ! (insn instanceof InvokeInstruction)
1961: }
1962:
1963: mi.leave(this );
1964:
1965: // remove a frame
1966: popFrame();
1967: }
1968:
1969: // we keep the thread alive to ease post mortem debugging
1970: // <2do> really just required if we check for uncaught exceptions,
1971: // but we always do
1972: //finish(); // toast this thread
1973: }
1974:
1975: //System.out.println("## unhandled!");
1976:
1977: // Ok, I finally made my peace wuth UncaughtException - we can be called from various places,
1978: // including the VM (<clinit>, finalizer) and we can't rely on that all these locations check
1979: // for pc == null. Even if they would, at this point there is nothing to do anymore, get to the
1980: // NoUncaughtProperty reporting as quickly as possible, since chances are we would be even
1981: // obfuscating the problem
1982: NoUncaughtExceptionsProperty.setExceptionInfo(pendingException);
1983: throw new UncaughtException(this , objref);
1984: }
1985:
1986: /**
1987: * Called when a lock is released. Updates the information
1988: * related to the locks.
1989: */
1990: public void unlock(Ref ref) {
1991: }
1992:
1993: protected void setStackFrameIndex(int i, int idx) {
1994: if (hasChanged.get(i) || ((i + 2) >= data.length)
1995: || (data[i + 2] != idx)) {
1996: stack[i] = (StackFrame) stackFramePool.getObject(idx);
1997: }
1998: }
1999:
2000: protected int getStackFrameIndex(int i) {
2001: if (hasChanged.get(i)) {
2002: HashPool.PoolEntry e = stackFramePool.getEntry(stack[i]);
2003:
2004: stack[i] = (StackFrame) e.getObject();
2005:
2006: return e.getIndex();
2007: } else {
2008: return data[i + 2];
2009: }
2010: }
2011:
2012: protected void setThreadDataIndex(int idx) {
2013: if (tdIndex == idx) {
2014: return;
2015: }
2016:
2017: tdIndex = idx;
2018: threadData = (ThreadData) threadDataPool.getObject(idx);
2019: }
2020:
2021: protected int getThreadDataIndex() {
2022: if (tdIndex != -1) {
2023: return tdIndex;
2024: }
2025:
2026: HashPool.PoolEntry e = threadDataPool.getEntry(threadData);
2027: threadData = (ThreadData) e.getObject();
2028:
2029: return tdIndex = e.getIndex();
2030: }
2031:
2032: /**
2033: * Executes a step where lines are atomic.
2034: * @return false if intermediate step (due to Nondeterminism or Buchi observable)
2035: */
2036: protected boolean executeAtomicLinesStep() throws JPFException {
2037: atomicData.line = getLine();
2038: atomicData.currentMethod = getMethod();
2039: atomicData.inSameMethod = true;
2040:
2041: int[] lines = atomicData.currentMethod.getLineNumbers();
2042:
2043: while (true) {
2044: Instruction pc = executeInstruction();
2045:
2046: if (list.ks.ss.violatedAssertion) {
2047: break;
2048: }
2049:
2050: if (pc == null) {
2051: break;
2052: }
2053:
2054: if (pc.isObservable()) {
2055: list.ks.ss.trail().setAnnotation(
2056: "observable instruction");
2057: return false;
2058: }
2059:
2060: if (list.ks.ss.isIgnored()) {
2061: throw new IgnoreIfException();
2062: }
2063:
2064: if (!pc.isDeterministic(list.ks.ss, list.ks, this )) {
2065: return false;
2066: }
2067:
2068: if (list.ks.atomicLevel > 0) {
2069: if (!isRunnable()) {
2070: throw new BlockedAtomicException();
2071: }
2072:
2073: continue; // we are still atomic, loop
2074: }
2075:
2076: if (!isRunnable()) {
2077: break;
2078: }
2079:
2080: // <?> pcm - how do we treat methods without line number tables?
2081: // Apparently, AspectJ does this, and I would assume the same for many
2082: // bytecode (re)writers
2083: if (!atomicData.inSameMethod
2084: || (lines == null)
2085: || (atomicData.line != lines[pc.getOffset()] && !(pc instanceof ReturnInstruction))) {
2086: atomicData.currentMethod = null;
2087: atomicData.line = -1;
2088:
2089: break;
2090: }
2091: }
2092:
2093: return true;
2094: }
2095:
2096: /**
2097: * execute a step using on-the-fly partial order reduction
2098: */
2099: protected boolean executePorStep() throws JPFException {
2100:
2101: while (true) {
2102: Instruction pc = executeInstruction();
2103:
2104: if (list.ks.ss.violatedAssertion) {
2105: break;
2106: }
2107:
2108: if (pc == null) {
2109: break;
2110: }
2111:
2112: if (pc.isObservable()) {
2113: list.ks.ss.trail().setAnnotation(
2114: "observable instruction");
2115: return false;
2116: }
2117:
2118: if (list.ks.ss.isIgnored()) {
2119: throw new IgnoreIfException();
2120: }
2121:
2122: if (!pc.isDeterministic(list.ks.ss, list.ks, this )) {
2123: return false;
2124: }
2125:
2126: if (list.ks.atomicLevel > 0) {
2127: // <2do> this is dangerous with Object.wait(J) from an atomic
2128: // section in a lib method (like Thread.join()) !
2129: if (!isRunnable()) {
2130: throw new BlockedAtomicException();
2131: }
2132: continue; // we are still atomic, loop
2133: }
2134:
2135: // this will catch MONITOR_ENTER/EXIT, wait, sync run, if they can't exec
2136: if (!isRunnable()) {
2137: return true;
2138: }
2139:
2140: // this will filter out all insns which might alter the state differently
2141: // depending on the scheduling sequence
2142: // Thread.start : always
2143: // sync invoke, MonitorEnter/Exit : other runnable threads
2144: // field / array access : other runnable threads & multi-thread reachable
2145: // runnable wait/notify ??
2146: if (yield
2147: || pc.isSchedulingRelevant(list.ks.ss, list.ks,
2148: this )) {
2149: yield = false;
2150: break;
2151: }
2152: }
2153:
2154: return true;
2155: }
2156:
2157: /**
2158: * request a reschedule no matter what the next insn is
2159: * (can be used by listeners who directly modify thread states)
2160: */
2161: public void yield() {
2162: yield = true;
2163: }
2164:
2165: public boolean hasOtherRunnables() {
2166: return list.hasOtherRunnablesThan(index);
2167: }
2168:
2169: /**
2170: * Returns a specific stack frame.
2171: */
2172: protected StackFrame frame(int idx) {
2173: if (idx < 0) {
2174: idx += (stack.length - 1);
2175: }
2176:
2177: return stack[idx];
2178: }
2179:
2180: /**
2181: * Returns a clone of a specific stack frame.
2182: */
2183: protected StackFrame frameClone(int i) {
2184: if (i < 0) {
2185: i += (stack.length - 1);
2186: }
2187:
2188: if (hasChanged.get(i)) {
2189: return stack[i];
2190: }
2191:
2192: hasChanged.set(i);
2193: anyChanged = true;
2194: list.ks.data = null;
2195:
2196: if ((lowestChanged == -1) || (lowestChanged > i)) {
2197: lowestChanged = i;
2198: }
2199:
2200: return stack[i] = (StackFrame) stack[i].clone();
2201: }
2202:
2203: /**
2204: * Returns a clone of the thread data.
2205: */
2206: protected ThreadData threadDataClone() {
2207: if (tdIndex == -1) {
2208: return threadData;
2209: }
2210:
2211: tdIndex = -1;
2212: list.ks.data = null;
2213:
2214: return threadData = (ThreadData) threadData.clone();
2215: }
2216:
2217: /**
2218: * Returns the top stack frame.
2219: */
2220: public StackFrame top() {
2221: if (stack.length > 0) {
2222: return stack[stack.length - 1];
2223: } else {
2224: return null;
2225: }
2226: }
2227:
2228: /**
2229: * Returns a clone of the top stack frame.
2230: */
2231: protected StackFrame topClone() {
2232: int i = stack.length - 1;
2233:
2234: if (hasChanged.get(i)) {
2235: return stack[i];
2236: }
2237:
2238: hasChanged.set(i);
2239: anyChanged = true;
2240: list.ks.data = null;
2241:
2242: if ((lowestChanged == -1) || (lowestChanged > i)) {
2243: lowestChanged = i;
2244: }
2245:
2246: return stack[i] = (StackFrame) stack[i].clone();
2247: }
2248:
2249: void setDaemon(boolean isDaemon) {
2250: threadDataClone().isDaemon = isDaemon;
2251: }
2252:
2253: boolean isDaemon() {
2254: return threadData.isDaemon;
2255: }
2256:
2257: MJIEnv getMJIEnv() {
2258: return env;
2259: }
2260:
2261: void setName(String newName) {
2262: threadDataClone().name = newName;
2263:
2264: // see 'setPriority()', only that it's more serious here, because the
2265: // java.lang.Thread name is stored as a char[]
2266: }
2267:
2268: void setPriority(int newPrio) {
2269: if (threadData.priority != newPrio) {
2270: threadDataClone().priority = newPrio;
2271:
2272: // note that we don't update the java.lang.Thread object, but
2273: // use our threadData value (which works because the object
2274: // values are just used directly from the Thread ctors (from where we pull
2275: // it out in our ThreadInfo ctor), and henceforth only via our intercepted
2276: // native getters
2277: }
2278: }
2279:
2280: int getPriority() {
2281: return threadData.priority;
2282: }
2283:
2284: /**
2285: * this is the method that factorizes common Thread object initialization
2286: * (get's called by all ctors).
2287: * BEWARE - it's hidden magic (undocumented), and should be replaced by our
2288: * own Thread impl at some point
2289: */
2290: void init(int rGroup, int rRunnable, int rName, long stackSize,
2291: boolean setPriority) {
2292: DynamicArea da = JVM.getVM().getDynamicArea();
2293: ElementInfo ei = da.get(rName);
2294:
2295: ThreadData td = threadDataClone();
2296: threadData.name = ei.asString();
2297: threadData.target = rRunnable;
2298:
2299: // stackSize and setPriority are only used by native subsystems
2300: }
2301:
2302: /**
2303: * did we call the current method directly, i.e. no via a INVOKE bytecode insn?
2304: */
2305: public boolean wasDirectCall() {
2306: return top().isDirectCall();
2307: }
2308: }
|