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.BootstrapXMLTraceHandler;
0022: import gov.nasa.jpf.Config;
0023: import gov.nasa.jpf.JPF;
0024: import gov.nasa.jpf.JPFException;
0025: import gov.nasa.jpf.Path;
0026: import gov.nasa.jpf.Transition;
0027: import gov.nasa.jpf.VM;
0028: import gov.nasa.jpf.VMState;
0029: import gov.nasa.jpf.VMListener;
0030: import gov.nasa.jpf.VMListenerMulticaster;
0031: import gov.nasa.jpf.util.CoverageManager;
0032: import gov.nasa.jpf.util.Debug;
0033:
0034: import java.io.File;
0035: import java.io.FileReader;
0036: import java.io.FileNotFoundException;
0037: import java.io.PrintWriter;
0038: import java.io.Reader;
0039: import java.io.Writer;
0040:
0041: import java.util.HashSet;
0042: import java.util.Stack;
0043: import java.util.StringTokenizer;
0044:
0045: import org.xml.sax.InputSource;
0046: import org.xml.sax.XMLReader;
0047: import org.xml.sax.helpers.XMLReaderFactory;
0048:
0049: import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
0050: import gov.nasa.jpf.jvm.bytecode.Instruction;
0051: import gov.nasa.jpf.jvm.choice.IntIntervalGenerator;
0052:
0053: /**
0054: * This class represents the virtual machine. The virtual machine is able to
0055: * move backward and forward one transition at a time.
0056: */
0057: public class JVM implements VM {
0058:
0059: /**
0060: * The number of errors saved so far.
0061: * Used to generate the name of the error trail file.
0062: */
0063: protected static int error_id;
0064:
0065: /**
0066: * Contains the list of the positions which are observable.
0067: */
0068: public static HashSet observablePositions;
0069:
0070: /**
0071: * Contains the list of the labels which are observable.
0072: */
0073: public static HashSet observableLabels;
0074:
0075: /**
0076: * Contains the list of invoke instructions which are observable.
0077: */
0078: public static HashSet observableInvokes;
0079:
0080: /**
0081: * Contains the list of methods whose return instruction are observable.
0082: */
0083: public static HashSet observableReturns;
0084:
0085: /**
0086: * <2do> - this is a hack to be removed once there are no static references
0087: * anymore
0088: */
0089: protected static JVM jvm;
0090:
0091: static {
0092: initStaticFields();
0093: }
0094:
0095: protected SystemState ss;
0096:
0097: // <2do> - if you are confused about the various pieces of state and its
0098: // storage/backtrack structures, I'm with you. It's mainly an attempt to
0099: // separate non-policy VM state (objects), policy VM state (Scheduler)
0100: // and general JPF execution state, with special support for stack oriented
0101: // state restoration (backtracking).
0102: // this needs to be cleaned up and the principle re-instantiated
0103:
0104: /** where we keep the saved KernelState data */
0105: protected Stack stateStoringStack;
0106:
0107: /** that's mostly JPFs execution context (atomicity etc.) */
0108: protected Stack stateBacktrackStack;
0109:
0110: /** and that adds the SystemState specifics (Scheduler) */
0111: protected Stack backtrackStack;
0112:
0113: protected String mainClassName;
0114: protected String[] args;
0115: /** main() arguments */
0116:
0117: protected Path path;
0118: /** execution path to current state */
0119: protected StringBuffer out;
0120: /** buffer to store output along path execution */
0121:
0122: /*
0123: * we keep those state restoring caches around so that we don't have
0124: * to duplicate them if somebody asks for the state. They are private because
0125: * using them just makes sense after a forward() / backtrack(). Let's hope
0126: * JPF never gets multithreaded
0127: */
0128: private int[] ksStoringData;
0129: private Object ksBacktrackData;
0130:
0131: /** do we want to override state matching */
0132: private boolean ignoreState;
0133:
0134: /**
0135: * various caches for VMListener state acqusition. NOTE - these are only
0136: * valid during notification
0137: */
0138: TrailInfo lastTrailInfo;
0139: ClassInfo lastClassInfo;
0140: ThreadInfo lastThreadInfo;
0141: Instruction lastInstruction;
0142: Instruction nextInstruction;
0143: ElementInfo lastElementInfo;
0144:
0145: /** the repository we use to find out if we already have seen a state */
0146: StateSet stateSet;
0147:
0148: /** potential execution listeners */
0149: VMListener listener;
0150:
0151: Config config; // that's for the options we use only once
0152:
0153: // JVM options we use frequently
0154: boolean runGc;
0155: boolean checkFP;
0156: boolean checkFPcompare;
0157: boolean atomicLines;
0158: boolean treeOutput;
0159: boolean pathOutput;
0160: boolean indentOutput;
0161:
0162: /**
0163: * VM instances are another example of evil throw-up ctors, but this is
0164: * justified by the fact that they are only created via (configured)
0165: * reflection from within the safe confines of the JPF ctor - which
0166: * shields clients against blowups
0167: */
0168: public JVM(Config conf) throws Config.Exception {
0169: // <2do> that's really a bad hack and should be removed once we
0170: // have cleaned up the reference chains
0171: jvm = this ;
0172:
0173: config = conf;
0174:
0175: runGc = config.getBoolean("vm.gc", true);
0176: checkFP = config.getBoolean("vm.check_fp", false);
0177: checkFPcompare = config.getBoolean("vm.check_fp_compare", true);
0178: atomicLines = config.getBoolean("vm.por.atomic_lines", true);
0179: treeOutput = config.getBoolean("vm.tree_output", true);
0180: pathOutput = config.getBoolean("vm.path_output", false);
0181: indentOutput = config.getBoolean("vm.indent_output", false);
0182:
0183: initSubsystems(config);
0184: initFields(config);
0185: }
0186:
0187: public void initFields(Config config) throws Config.Exception {
0188: ClassInfo ci;
0189:
0190: // the scheduler is just a local object because it is cloned/changed
0191: // when restoring SystemStates
0192: // <2do> this is likely to be changed when scheduling is moved over to
0193: // external choice generators
0194: Scheduler scheduler = null;
0195:
0196: // so that we can hash/store states
0197: stateSet = (StateSet) config.getInstance("vm.storage.class",
0198: StateSet.class);
0199:
0200: String target = config.getTargetArg();
0201:
0202: if (target.endsWith(".xml")) {
0203: if ((new File(target)).exists()) {
0204: // we are replaying a stored path
0205: Path replay = loadPath(target);
0206: mainClassName = replay.getApplication();
0207: // if we replay a path, we have to use a PathScheduler no matter what
0208: scheduler = new PathScheduler(replay);
0209: Debug.println(Debug.MESSAGE, "replay path: " + target);
0210: } else {
0211: Debug.println(Debug.ERROR, "tracefile " + target
0212: + " not found, exiting");
0213: JPF.exit();
0214: }
0215: } else {
0216: mainClassName = target;
0217: scheduler = (Scheduler) config.getEssentialInstance(
0218: "vm.scheduler.class", Scheduler.class);
0219: }
0220:
0221: args = config.getTargetArgParameters();
0222:
0223: stateStoringStack = new Stack();
0224: stateBacktrackStack = new Stack();
0225: backtrackStack = new Stack();
0226: path = new Path(mainClassName);
0227: out = null;
0228:
0229: ss = new SystemState(config, scheduler);
0230:
0231: // <2do> - unify this with POR step boundaries
0232: if (config.getBoolean("vm.visible_asserts")) {
0233: addObservable("invoke.gov.nasa.jpf.jvm.Verify.assertTrue(Z)V");
0234: }
0235:
0236: addListeners(config);
0237: }
0238:
0239: void addListeners(Config config) throws Config.Exception {
0240: Object[] listeners = config.getInstances("vm.listener",
0241: VMListener.class);
0242: if (listeners != null) {
0243: for (int i = 0; i < listeners.length; i++) {
0244: addListener((VMListener) listeners[i]);
0245: }
0246: }
0247: }
0248:
0249: void initSubsystems(Config config) throws Config.Exception {
0250: ClassInfo.init(config);
0251: ThreadInfo.init(config);
0252: DynamicArea.init(config);
0253: StaticArea.init(config);
0254: NativePeer.init(config);
0255: CoverageManager.init(config);
0256: TrailInfo.init(config);
0257: Step.init(config);
0258: FieldInstruction.init(config);
0259: JPF_gov_nasa_jpf_jvm_Verify.init(config);
0260: }
0261:
0262: /**
0263: * do we see our model classes? Some of them cannot be used from the standard CLASSPATH, because they
0264: * are tightly coupled with the JPF core (e.g. java.lang.Class, java.lang.Thread,
0265: * java.lang.StackTraceElement etc.)
0266: * Our strategy here is kind of lame - we just look into java.lang.Class, if we find the 'int cref' field
0267: * (that's a true '42')
0268: */
0269: static boolean checkModelClassAccess() {
0270: ClassInfo ci = ClassInfo.getClassInfo("java.lang.Class");
0271: return (ci.getDeclaredInstanceField("cref") != null);
0272: }
0273:
0274: /**
0275: * load and initialize startup classes, return 'true' if successful.
0276: *
0277: * This loads a bunch of core library classes, initializes the main thread,
0278: * and then all the required startup classes, but excludes the static init of
0279: * the main class. Note that whatever gets executed in here should NOT contain
0280: * any non-determinism, since we are not backtrackable yet, i.e.
0281: * non-determinism in clinits should be constrained to the app class (and
0282: * classes used by it)
0283: */
0284: public boolean initialize() {
0285: // from here, we get into some bootstrapping process
0286: // - first, we have to load class structures (fields, supers, interfaces..)
0287: // - second, we have to create a thread (so that we have a stack)
0288: // - third, we have to execute the clinit methods on this stack
0289: // create static fields and monitor for system classes and app entry
0290: loadStartupClasses();
0291:
0292: if (!checkModelClassAccess()) {
0293: Debug
0294: .println(
0295: Debug.ERROR,
0296: "error during VM runtime initialization: wrong model classes (check vm.[boot]classpath)");
0297: return false;
0298: }
0299:
0300: // create the thread for the main class
0301: // note this is incomplete for Java 1.3 where Thread ctors rely on main's
0302: // 'inheritableThreadLocals' being set to 'Collections.EMPTY_SET', which
0303: // pulls in the whole Collections/Random smash, but we can't execute the
0304: // Collections.<clinit> yet because there's no stack before we have a main
0305: // thread. Let's hope none of the init classes creates threads in their <clinit>.
0306: createMainThread();
0307:
0308: try {
0309: // initializes the classes loaded
0310: // this mainly makes sure the <clinit> methods get called, which is not
0311: // possible before we have a thread stack.
0312: // Note - this does not include the main class clinit (or any of its
0313: // superclasses), since that has to be done from forward (i.e. backtrackable)
0314: initializeStartupClasses();
0315:
0316: // those are the actions (in reverse order) we are taking next. Reverse,
0317: // because they are initiated via the stack
0318: prepareMain(config);
0319: prepareMainClinit(config);
0320: } catch (UncaughtException ux) {
0321: // <2do> hmm - we really should handle UncaughtExceptions consistently
0322: Debug.println(Debug.ERROR,
0323: "error during VM runtime initialization:");
0324: Debug.println(Debug.ERROR, ux);
0325: return false;
0326: }
0327:
0328: return true;
0329: }
0330:
0331: public void addListener(VMListener newListener) {
0332: listener = VMListenerMulticaster.add(listener, newListener);
0333: }
0334:
0335: public void removeListener(VMListener removeListener) {
0336: listener = VMListenerMulticaster.remove(listener,
0337: removeListener);
0338: }
0339:
0340: void notifyInstructionExecuted(ThreadInfo ti, Instruction insn,
0341: Instruction nextInsn) {
0342: lastThreadInfo = ti;
0343: lastInstruction = insn;
0344: nextInstruction = nextInsn;
0345: if (listener != null) {
0346: listener.instructionExecuted(this );
0347: }
0348: nextInstruction = null;
0349: lastInstruction = null;
0350: lastThreadInfo = null;
0351: }
0352:
0353: void notifyThreadStarted(ThreadInfo ti) {
0354: lastThreadInfo = ti;
0355: if (listener != null) {
0356: listener.threadStarted(this );
0357: }
0358: lastThreadInfo = null;
0359: }
0360:
0361: void notifyThreadTerminated(ThreadInfo ti) {
0362: lastThreadInfo = ti;
0363: if (listener != null) {
0364: listener.threadTerminated(this );
0365: }
0366: lastThreadInfo = null;
0367: }
0368:
0369: void notifyClassLoaded(ClassInfo ci) {
0370: lastClassInfo = ci;
0371: if (listener != null) {
0372: listener.classLoaded(this );
0373: }
0374: lastClassInfo = null;
0375: }
0376:
0377: void notifyObjectCreated(ThreadInfo ti, ElementInfo ei) {
0378: lastThreadInfo = ti;
0379: lastElementInfo = ei;
0380: if (listener != null) {
0381: listener.objectCreated(this );
0382: }
0383: lastElementInfo = null;
0384: lastThreadInfo = null;
0385: }
0386:
0387: void notifyObjectReleased(ElementInfo ei) {
0388: lastElementInfo = ei;
0389: if (listener != null) {
0390: listener.objectReleased(this );
0391: }
0392: lastElementInfo = null;
0393: }
0394:
0395: void notifyGCBegin() {
0396: if (listener != null) {
0397: listener.gcBegin(this );
0398: }
0399: }
0400:
0401: void notifyGCEnd() {
0402: if (listener != null) {
0403: listener.gcEnd(this );
0404: }
0405: }
0406:
0407: void notifyExceptionThrown(ThreadInfo ti, ElementInfo ei) {
0408: lastThreadInfo = ti;
0409: lastElementInfo = ei;
0410: if (listener != null) {
0411: listener.exceptionThrown(this );
0412: }
0413: lastElementInfo = null;
0414: lastThreadInfo = null;
0415: }
0416:
0417: // VMListener acquisition
0418: public int getThreadNumber() {
0419: if (lastThreadInfo != null) {
0420: return lastThreadInfo.getIndex();
0421: } else {
0422: return -1;
0423: }
0424: }
0425:
0426: // VMListener acquisition
0427: public String getThreadName() {
0428: ThreadInfo ti = ss.getRunningThread();
0429:
0430: return ti.getName();
0431: }
0432:
0433: // VMListener acquisition
0434: Instruction getInstruction() {
0435: ThreadInfo ti = ss.getRunningThread();
0436: return ti.getPC();
0437: }
0438:
0439: public int getAbstractionNonDeterministicThreadCount() {
0440: int n = 0;
0441: int imax = ss.getThreadCount();
0442:
0443: for (int i = 0; i < imax; i++) {
0444: ThreadInfo th = ss.getThreadInfo(i);
0445:
0446: if (th.isAbstractionNonDeterministic()) {
0447: n++;
0448: }
0449: }
0450:
0451: return n;
0452: }
0453:
0454: public int getAliveThreadCount() {
0455: int n = 0;
0456: int imax = ss.getThreadCount();
0457:
0458: for (int i = 0; i < imax; i++) {
0459: ThreadInfo th = ss.getThreadInfo(i);
0460:
0461: if (th.isAlive()) {
0462: n++;
0463: }
0464: }
0465:
0466: return n;
0467: }
0468:
0469: public ExceptionInfo getPendingException() {
0470: return ThreadInfo.current.getPendingException();
0471: }
0472:
0473: public boolean isBoringState() {
0474: return ss.getBoring();
0475: }
0476:
0477: public Reference getClassReference(String name) {
0478: if (ClassInfo.exists(name)) {
0479: return ss.ks.sa.get(name);
0480: }
0481:
0482: return null;
0483: }
0484:
0485: public boolean hasPendingException() {
0486: return (ThreadInfo.current.pendingException != null);
0487: }
0488:
0489: public boolean isDeadlocked() {
0490: int length = ss.getThreadCount();
0491: boolean result = false;
0492:
0493: for (int i = 0; i < length; i++) {
0494: ThreadInfo th = (ThreadInfo) ss.getThreadInfo(i);
0495:
0496: // if there's at least one runnable, we are not deadlocked
0497: if (th.isRunnable()) {
0498: return false;
0499: }
0500:
0501: // if stack depth is 0, it's done
0502: // otherwise we have a deadlock if we don't find any runnable
0503: if (th.countStackFrames() != 0) {
0504: result = true;
0505: }
0506: }
0507:
0508: return result;
0509: }
0510:
0511: public boolean isEndState() {
0512: // note this uses 'alive', not 'runnable', hence isEndStateProperty won't
0513: // catch deadlocks - but that would be NoDeadlockProperty anyway
0514: return ss.isEndState();
0515: }
0516:
0517: public Exception getException() {
0518: return ss.getUncaughtException();
0519: }
0520:
0521: public boolean isInterestingState() {
0522: return ss.getInteresting();
0523: }
0524:
0525: public Step getLastStep() {
0526: TrailInfo trail = ss.trail();
0527: if (trail != null) {
0528: return trail.getLastStep();
0529: }
0530:
0531: return null;
0532: }
0533:
0534: public Transition getLastTransition() {
0535: if (path.length() == 0) {
0536: return null;
0537: }
0538: return path.get(path.length() - 1);
0539: }
0540:
0541: /**
0542: * answer the ClassInfo that was loaded most recently
0543: * part of the VMListener state acqusition (only valid from inside of
0544: * notification)
0545: */
0546: public ClassInfo getLastClassInfo() {
0547: return lastClassInfo;
0548: }
0549:
0550: /**
0551: * answer the ThreadInfo that was most recently started or finished
0552: * part of the VMListener state acqusition (only valid from inside of
0553: * notification)
0554: */
0555: public ThreadInfo getLastThreadInfo() {
0556: return lastThreadInfo;
0557: }
0558:
0559: /**
0560: * answer the last executed Instruction
0561: * part of the VMListener state acqusition (only valid from inside of
0562: * notification)
0563: */
0564: public Instruction getLastInstruction() {
0565: return lastInstruction;
0566: }
0567:
0568: /**
0569: * answer the next Instruction to execute in the current thread
0570: * part of the VMListener state acqusition (only valid from inside of
0571: * notification)
0572: */
0573: public Instruction getNextInstruction() {
0574: return nextInstruction;
0575: }
0576:
0577: /**
0578: * answer the Object that was most recently created or collected
0579: * part of the VMListener state acqusition (only valid from inside of
0580: * notification)
0581: */
0582: public ElementInfo getLastElementInfo() {
0583: return lastElementInfo;
0584: }
0585:
0586: /**
0587: * answer the ClassInfo that was loaded most recently
0588: * part of the VMListener state acqusition
0589: */
0590: public ClassInfo getClassInfo() {
0591: return lastClassInfo;
0592: }
0593:
0594: public String getMainClassName() {
0595: return mainClassName;
0596: }
0597:
0598: public String[] getArgs() {
0599: return args;
0600: }
0601:
0602: public void setPath(Path p) {
0603: }
0604:
0605: public Path getPath() {
0606: return (Path) path.clone();
0607: }
0608:
0609: public int getPathLength() {
0610: return path.length();
0611: }
0612:
0613: public Reference getReference(String name) {
0614: // first of all I have to get to a class
0615: StringTokenizer st = new StringTokenizer(name, ".");
0616: StringBuffer sb = new StringBuffer();
0617: Reference r = null;
0618:
0619: while (st.hasMoreTokens()) {
0620: sb.append(st.nextToken());
0621:
0622: if ((r = getClassReference(sb.toString())) != null) {
0623: break;
0624: }
0625:
0626: sb.append('.');
0627: }
0628:
0629: if (r == null) {
0630: throw new JPFException("invalid argument: " + name);
0631: }
0632:
0633: // now walk thought the fields
0634: while (st.hasMoreTokens()) {
0635: r = r.getObjectField(st.nextToken(), sb.toString());
0636: }
0637:
0638: return r;
0639: }
0640:
0641: public VMState getRestorableForwardState() {
0642: JVMState state = new JVMState();
0643: state.makeForwardRestorable();
0644:
0645: return state;
0646: }
0647:
0648: public int getRunnableThreadCount() {
0649: return ss.getRunnableThreadCount();
0650: }
0651:
0652: public boolean checkFP() {
0653: return checkFP;
0654: }
0655:
0656: public boolean checkNaN(double r) {
0657: if (checkFP) {
0658: return !(Double.isNaN(r) || Double.isInfinite(r));
0659: } else {
0660: return true;
0661: }
0662: }
0663:
0664: public boolean checkNaN(float r) {
0665: if (checkFP) {
0666: return !(Float.isNaN(r) || Float.isInfinite(r));
0667: } else {
0668: return true;
0669: }
0670: }
0671:
0672: public boolean checkNaNcompare(float r1, float r2) {
0673: if (checkFPcompare) {
0674: return !(Float.isNaN(r1) || Float.isNaN(r2) || (Float
0675: .isInfinite(r1)
0676: && Float.isInfinite(r2) && (r1 == r2)));
0677: } else {
0678: return true;
0679: }
0680: }
0681:
0682: public boolean checkNaNcompare(double r1, double r2) {
0683: if (checkFPcompare) {
0684: return !(Double.isNaN(r1) || Double.isNaN(r2) || (Double
0685: .isInfinite(r1)
0686: && Double.isInfinite(r2) && (r1 == r2)));
0687: } else {
0688: return true;
0689: }
0690: }
0691:
0692: /**
0693: * Bundles up the state of the system for export
0694: */
0695: public VMState getState() {
0696: return (new JVMState());
0697: }
0698:
0699: /**
0700: * Gets the system state.
0701: */
0702: public SystemState getSystemState() {
0703: return ss;
0704: }
0705:
0706: public KernelState getKernelState() {
0707: return ss.ks;
0708: }
0709:
0710: /**
0711: * return the current SystemState's ChoiceGenerator object
0712: */
0713: public ChoiceGenerator getChoiceGenerator() {
0714: return ss.getChoiceGenerator();
0715: }
0716:
0717: ///// <2do> that's probably not going to stay here - ChoiceGenerator creation will be revamped
0718:
0719: // our const ChoiceGenerator ctor argtypes
0720: protected final Class[] cgArgTypes = { Config.class, String.class };
0721: // this is our cache for ChoiceGenerator ctor parameters
0722: protected Object[] cgArgs = { null, null };
0723:
0724: // the built-in ones (boolean and int)
0725: public BooleanChoiceGenerator createBooleanChoiceGenerator() {
0726: BooleanChoiceGenerator gen = new BooleanChoiceGenerator(config,
0727: "boolean");
0728: gen.advance(this ); // that's not going to stay here
0729: ss.setChoiceGenerator(gen);
0730: return gen;
0731: }
0732:
0733: public IntChoiceGenerator createIntChoiceGenerator(int min, int max) {
0734: IntIntervalGenerator gen = new IntIntervalGenerator(min, max);
0735: gen.advance(this ); // that's not going to stay here
0736: ss.setChoiceGenerator(gen);
0737: return gen;
0738: }
0739:
0740: // the generic one
0741: public ChoiceGenerator createChoiceGenerator(String id) {
0742: ChoiceGenerator gen = null;
0743:
0744: cgArgs[0] = config;
0745: cgArgs[1] = id; // good thing we are not multithreaded (other fields are const)
0746:
0747: try {
0748: String key = id + ".class";
0749: gen = (ChoiceGenerator) config.getEssentialInstance(key,
0750: ChoiceGenerator.class, cgArgTypes, cgArgs);
0751: gen.advance(this ); // that's not going to stay here
0752: ss.setChoiceGenerator(gen);
0753: } catch (Config.Exception cex) {
0754: // bail, nothing we can do to cover up
0755: throw new JPFException(cex);
0756: }
0757:
0758: return gen;
0759: }
0760:
0761: public boolean isTerminated() {
0762: return ss.ks.isTerminated();
0763: }
0764:
0765: public void print(String s) {
0766: if (treeOutput) {
0767: System.out.print(s);
0768: }
0769:
0770: if (pathOutput) {
0771: appendOutput(s);
0772: }
0773: }
0774:
0775: public void println(String s) {
0776: if (treeOutput) {
0777: if (indentOutput) {
0778: StringBuffer indent = new StringBuffer();
0779: int i;
0780: for (i = 0; i <= path.length(); i++) {
0781: indent.append("|" + i);
0782: }
0783: System.out.println(indent + "|" + s);
0784: } else {
0785: System.out.println(s);
0786: }
0787: }
0788:
0789: if (pathOutput) {
0790: appendOutput(s);
0791: appendOutput('\n');
0792: }
0793: }
0794:
0795: public void print(boolean b) {
0796: if (treeOutput) {
0797: System.out.print(b);
0798: }
0799:
0800: if (pathOutput) {
0801: appendOutput(Boolean.toString(b));
0802: }
0803: }
0804:
0805: public void print(char c) {
0806: if (treeOutput) {
0807: System.out.print(c);
0808: }
0809:
0810: if (pathOutput) {
0811: appendOutput(c);
0812: }
0813: }
0814:
0815: public void print(int i) {
0816: if (treeOutput) {
0817: System.out.print(i);
0818: }
0819:
0820: if (pathOutput) {
0821: appendOutput(Integer.toString(i));
0822: }
0823: }
0824:
0825: public void print(long l) {
0826: if (treeOutput) {
0827: System.out.print(l);
0828: }
0829:
0830: if (pathOutput) {
0831: appendOutput(Long.toString(l));
0832: }
0833: }
0834:
0835: public void print(double d) {
0836: if (treeOutput) {
0837: System.out.print(d);
0838: }
0839:
0840: if (pathOutput) {
0841: appendOutput(Double.toString(d));
0842: }
0843: }
0844:
0845: public void print(float f) {
0846: if (treeOutput) {
0847: System.out.print(f);
0848: }
0849:
0850: if (pathOutput) {
0851: appendOutput(Float.toString(f));
0852: }
0853: }
0854:
0855: public void println() {
0856: if (treeOutput) {
0857: System.out.println();
0858: }
0859:
0860: if (pathOutput) {
0861: appendOutput('\n');
0862: }
0863: }
0864:
0865: void appendOutput(String s) {
0866: if (out == null) {
0867: out = new StringBuffer();
0868: }
0869: out.append(s);
0870: }
0871:
0872: void appendOutput(char c) {
0873: if (out == null) {
0874: out = new StringBuffer();
0875: }
0876: out.append(c);
0877: }
0878:
0879: /**
0880: * JVM specific results
0881: */
0882: public void printResults(PrintWriter pw) {
0883: if (config.getBoolean("vm.report.printStacks")) {
0884: pw
0885: .println("------------------------------------ thread stacks");
0886: printStackTraces(pw);
0887: pw
0888: .println("------------------------------------ end thread stacks");
0889: }
0890: }
0891:
0892: public void printStackTraces(PrintWriter pw) {
0893: int imax = ss.getThreadCount();
0894:
0895: for (int i = 0; i < imax; i++) {
0896: ThreadInfo ti = ss.getThreadInfo(i);
0897: String[] cs = ti.getCallStack();
0898:
0899: if (cs.length > 0) {
0900: pw.print("Thread: ");
0901: pw.println(ti.getName());
0902: for (int j = cs.length - 1; j >= 0; j--) {
0903: pw.println(cs[j]);
0904: }
0905: pw.println();
0906: }
0907: }
0908: }
0909:
0910: void backtrackKernelState() {
0911: ksStoringData = (int[]) stateStoringStack.pop();
0912: ksBacktrackData = stateBacktrackStack.pop();
0913:
0914: ss.ks.backtrackTo(new ArrayOffset(ksStoringData),
0915: ksBacktrackData);
0916: }
0917:
0918: void backtrackSystemState() {
0919: ss.backtrackTo(null, backtrackStack.pop());
0920: }
0921:
0922: /**
0923: * Moves one step backward. This method and forward() are the main methods
0924: * used by the search object.
0925: * Note this is called with the state that caused the backtrack still being on
0926: * the stack, so we have to remove that one first (i.e. popping two states
0927: * and restoring the second one)
0928: */
0929: public boolean backtrack() {
0930: if (!backtrackStack.isEmpty()) {
0931: // restore the KernelState
0932: backtrackKernelState();
0933:
0934: // restore the SystemState
0935: backtrackSystemState();
0936:
0937: // restore the path
0938: path.removeLast();
0939: lastTrailInfo = (TrailInfo) path.getLast();
0940:
0941: return ((ss.getId() != StateSet.UNKNOWN_ID) || (stateSet == null));
0942: } else {
0943: return false;
0944: }
0945: }
0946:
0947: private void cacheKernelState() {
0948: ksStoringData = ss.ks.getStoringData();
0949: ksBacktrackData = ss.ks.getBacktrackData();
0950: }
0951:
0952: private void resetKernelStateCache() {
0953: ksStoringData = null;
0954: ksBacktrackData = null;
0955: }
0956:
0957: private boolean tryAgain() {
0958: backtrackKernelState();
0959: ss.scheduleNext(this );
0960:
0961: // <2do> pcm - no prepareNext here (scheduler resetting?)
0962: return forward();
0963: }
0964:
0965: /**
0966: * store the current SystemState's TrainInfo in our path, after updating it
0967: * with whatever annotations the JVM wants to add.
0968: * This is supposed to be called after each transition we want to keep
0969: */
0970: void updatePath() {
0971: Transition t = ss.trail();
0972:
0973: // <2do> we should probably store the output directly in the TrailInfo,
0974: // but this might not be our only annotation in the future
0975:
0976: // did we have output during the last transition? If yes, add it
0977: if ((out != null) && (out.length() > 0)) {
0978: t.setOutput(out.toString());
0979: out.setLength(0);
0980: }
0981:
0982: path.add(t);
0983: }
0984:
0985: /**
0986: * try to advance the state
0987: * forward() and backtrack() are the two primary interfaces towards the Search
0988: * driver
0989: * return 'true' if there was an un-executed sequence out of the current state,
0990: * 'false' if it was completely explored
0991: * note that the caller still has to check if there is a next state, and if
0992: * the executed instruction sequence led into a new or already visited state
0993: */
0994: public boolean forward() {
0995: boolean isNewState = true;
0996: ignoreState = false;
0997:
0998: try {
0999: // saves the current state for backtracking purposes of depth first
1000: // searches and state observers. If there is a previously cached
1001: // kernelstate, use that one
1002: pushKernelState();
1003:
1004: // cache this before we execute (and increment) the next insn(s)
1005: lastTrailInfo = (TrailInfo) path.getLast();
1006:
1007: // execute the instruction(s) to get to the next state
1008: // this changes the SystemState (e.g. finds the next thread to run)
1009: if (ss.nextSuccessor(this )) {
1010: // runs the garbage collector (if necessary), which might change the
1011: // KernelState (DynamicArea)
1012: // we need to do this before we hash the state to find out if it is
1013: // a new one
1014: // Note that we don't collect if there is a pending exception, since
1015: // we want to preserve as much state as possible for debug purposes
1016: if (runGc && !hasPendingException()) {
1017: ss.gcIfNeeded();
1018: }
1019:
1020: // moves the scheduler to the next position, which changes the SystemState
1021: ss.scheduleNext(this );
1022:
1023: // might change backtrack info due to SystemState checks
1024: ss.checkNext(this );
1025:
1026: // saves the backtrack information. Unfortunately, we cannot cache
1027: // this (except of the optional lock graph) because it is changed
1028: // by the subsequent operations (before we return from forward)
1029: pushSystemState();
1030:
1031: updatePath();
1032:
1033: // get ready for the next round (resets Scheduler)
1034: ss.prepareNext(this );
1035:
1036: } else { // state was completely explored, no transition ocurred
1037: popKernelState();
1038: return false;
1039: }
1040:
1041: } catch (BlockedAtomicException e) { // <2do> bad control flow
1042: return tryAgain();
1043: } catch (IgnoreIfException e) { // <2do> bad control flow
1044: return tryAgain();
1045: // } catch (JPFException e) {
1046: // throw e;
1047: } catch (UncaughtException e) {
1048: updatePath(); // or we loose the last transition
1049: // something blew up, so we definitely executed something (hence return true)
1050: return true;
1051: } catch (RuntimeException e) {
1052: throw new JPFException(e);
1053: }
1054:
1055: if (stateSet != null) {
1056: int id = stateSet.add(ss);
1057: ss.setId(id);
1058: isNewState = stateSet.isNewState(id);
1059: }
1060:
1061: // the idea is that search objects or observers can query the state
1062: // *after* forward/backtrack was called, and that all changes of the
1063: // System/KernelStates happen from *within* forward/backtrack, i.e. the
1064: // (expensive) getBacktrack/storingData operations can be cached and used
1065: // w/o re-computation in the next forward pushXState()
1066: cacheKernelState(); // for subsequent getState() and the next forward()
1067:
1068: return true;
1069: }
1070:
1071: /**
1072: * load a previously stored path from a file
1073: * <2do> should be simplified to use the JVMXMLTraceHandler (no use to
1074: * have different trace formats for the same VM)
1075: */
1076: public Path loadPath(String fname) {
1077: try {
1078: Reader r = new FileReader(fname);
1079:
1080: XMLReader parser = XMLReaderFactory
1081: .createXMLReader("org.apache.xerces.parsers.SAXParser");
1082: BootstrapXMLTraceHandler handler = new BootstrapXMLTraceHandler();
1083: parser.setContentHandler(handler);
1084: parser.parse(new InputSource(r));
1085:
1086: return handler.getPath();
1087: } catch (FileNotFoundException e) {
1088: throw new JPFException(fname + ": file not found");
1089: } catch (Throwable x) {
1090: throw new JPFException("cannot load path " + fname + " : "
1091: + x);
1092: }
1093: }
1094:
1095: public void popKernelState() {
1096: stateStoringStack.pop();
1097: stateBacktrackStack.pop();
1098: }
1099:
1100: public void printStatus() {
1101: Debug.println(Debug.ERROR,
1102: "Current status of the virtual machine:");
1103: printCurrentStackTrace();
1104:
1105: //if (options.print_errors) {
1106: Debug.println(Debug.ERROR, "Current execution path:");
1107: Debug.println(Debug.ERROR, getPath());
1108: //}
1109: }
1110:
1111: /**
1112: * Prints the current stack trace.
1113: */
1114: public void printCurrentStackTrace() {
1115: ThreadInfo th = ss.getRunningThread();
1116:
1117: if (th != null) {
1118: th.printStackTrace();
1119: }
1120: }
1121:
1122: /**
1123: * Saves the state of the system.
1124: */
1125: public void pushKernelState() {
1126: int[] ksSD;
1127:
1128: // do we need to recompute the cache?
1129: if (ksStoringData == null) {
1130: ksSD = ss.ks.getStoringData();
1131: } else {
1132: ksSD = ksStoringData;
1133: }
1134:
1135: stateStoringStack.push(ksSD);
1136:
1137: Object ksBD;
1138:
1139: if (ksBacktrackData == null) {
1140: ksBD = ss.ks.getBacktrackData();
1141: } else {
1142: ksBD = ksBacktrackData;
1143: }
1144:
1145: stateBacktrackStack.push(ksBD);
1146: }
1147:
1148: /**
1149: * Saves the backtracking information.
1150: */
1151: public void pushSystemState() {
1152: Object ssBD = ss.getBacktrackData();
1153: backtrackStack.push(ssBD);
1154: }
1155:
1156: public void restoreState(VMState st) {
1157: if (st instanceof JVMState) {
1158: JVMState state = (JVMState) st;
1159:
1160: if (state.path == null) {
1161: throw new JPFException(
1162: "tried to restore partial VMState: " + st);
1163: }
1164:
1165: // NOTE - we have to clone all restored objects that are modified by
1166: // subsequent forward/backtrack operations, since they might be stored
1167: // globally, and used to reset to the same state several times
1168:
1169: // NOTE ALSO - be aware of that the state might not have been obtained without
1170: // calling makeRestorable(), in which case the following fields would not
1171: // be initialized, and backtracking would not work
1172: // see VMState
1173: stateStoringStack = (state.stateStoringStack != null) ? (Stack) state.stateStoringStack
1174: .clone()
1175: : new Stack();
1176: stateBacktrackStack = (state.stateBacktrackStack != null) ? (Stack) state.stateBacktrackStack
1177: .clone()
1178: : new Stack();
1179: backtrackStack = (state.backtrackStack != null) ? (Stack) state.backtrackStack
1180: .clone()
1181: : new Stack();
1182:
1183: // we are going to restore the system state via backtracking, so there's
1184: // no need to give it a scheduler here
1185: //ss = SystemState.newInstance((Scheduler) null);
1186:
1187: ksStoringData = state.ksStoringData;
1188: ksBacktrackData = state.ksBacktrackData;
1189:
1190: ss.ks.backtrackTo(new ArrayOffset(ksStoringData),
1191: ksBacktrackData);
1192: ss.backtrackTo(null, state.ssBacktrackData);
1193:
1194: path = (Path) state.path.clone();
1195: } else {
1196: throw new JPFException("tried to restore illegal VMState: "
1197: + st);
1198: }
1199: }
1200:
1201: public void rewind() {
1202: ss.sch.initialize();
1203: }
1204:
1205: public void savePath(Path path, Writer w) {
1206: PrintWriter out = new PrintWriter(w);
1207: int length = path.length();
1208:
1209: TrailInfo.toXML(out, path);
1210: }
1211:
1212: /**
1213: * override the state matching - ignore this state, no matter if we changed
1214: * the heap or stacks.
1215: * use this with care, since it prunes whole search subtrees
1216: */
1217: public void setIgnoreState(boolean b) {
1218: ignoreState = b;
1219: }
1220:
1221: /**
1222: * answers if the current state already has been visited. This is mainly
1223: * used by the searches (to control backtracking), but could also be useful
1224: * for observers to build up search graphs (based on the state ids)
1225: */
1226: public boolean isNewState() {
1227: if (stateSet != null) {
1228: if (ignoreState) {
1229: return false;
1230: } else {
1231: return stateSet.isNewState(ss.getId());
1232: }
1233: } else {
1234: return true;
1235: }
1236: }
1237:
1238: /**
1239: * get the numeric id for the current state
1240: * Note: this can be called several times (by the search and observers) for
1241: * every forward()/backtrack(), so we want to cache things a bit
1242: */
1243: public int getStateId() {
1244: return ss.getId();
1245: }
1246:
1247: // <2do> this will be obsolete at some point (too close to POR)
1248: public void addObservable(String observable) {
1249: if (observable.startsWith("invoke.")) {
1250: synchronized (observableInvokes) {
1251: observableInvokes.add(observable.substring(7));
1252: }
1253: } else if (observable.startsWith("return.")) {
1254: synchronized (observableReturns) {
1255: observableReturns.add(observable.substring(7));
1256: }
1257: } else if (observable.startsWith("position.")) {
1258: synchronized (observablePositions) {
1259: observablePositions.add(observable.substring(9));
1260: }
1261: } else if (observable.startsWith("label.")) {
1262: synchronized (observableLabels) {
1263: observableLabels.add(observable.substring(6));
1264: }
1265: } else {
1266: Debug.println(Debug.ERROR, "Unknown observable: "
1267: + observable);
1268: }
1269: }
1270:
1271: /**
1272: * be careful - everything that's executed from within here is not allowed
1273: * to depend on static class init having been done yet
1274: */
1275: protected ThreadInfo createMainThread() {
1276: ElementInfo ei;
1277: DynamicArea da = ss.ks.da;
1278:
1279: // first we need a group for this baby (happens to be called "main")
1280: int grpObjref = da.newObject(ClassInfo
1281: .getClassInfo("java.lang.ThreadGroup"), null);
1282:
1283: // since we can't call methods yet, we have to init explicitly (BAD)
1284: int grpName = da.newString("main", null);
1285: ei = da.get(grpObjref);
1286: ei.setReferenceField("name", grpName);
1287: ei.setIntField("maxPriority", java.lang.Thread.MAX_PRIORITY);
1288:
1289: int tObjref = da.newObject(ClassInfo
1290: .getClassInfo("java.lang.Thread"), null);
1291:
1292: ei = da.get(tObjref);
1293: ei.setReferenceField("group", grpObjref);
1294: ei.setReferenceField("name", da.newString("main", null));
1295: ei.setIntField("priority", Thread.NORM_PRIORITY);
1296:
1297: // we need to keep the attributes on the JPF side in sync here
1298: // <2do> factor out the Thread/ThreadInfo creation so that it's less
1299: // error prone (even so this is the only location it's required for)
1300: ThreadInfo ti = new ThreadInfo(this , tObjref);
1301: ti.setPriority(java.lang.Thread.NORM_PRIORITY);
1302: ti.setName("main");
1303: ti.setStatus(ThreadInfo.RUNNING);
1304: ss.ks.addThread(ti); // <2do> get rid of this ref chain
1305:
1306: return ti;
1307: }
1308:
1309: public ThreadInfo createThread(int objRef) {
1310: ThreadInfo ti = new ThreadInfo(this , objRef);
1311: ss.ks.addThread(ti); // <2do> get rid of this ref chain
1312: return ti;
1313: }
1314:
1315: void prepareMainClinit(Config config) {
1316: StaticArea sa = getStaticArea();
1317: ClassInfo ci = ClassInfo.getClassInfo(mainClassName);
1318:
1319: // note we have to push the stackframes in reverse execution order
1320: // (i.e. MDC first), since we start to execute from the stack top
1321: while (!sa.containsClass(ci.getName())) {
1322: // make sure the thing is registered, but not yet initialized
1323: sa.newUninitializedClass(ci);
1324:
1325: MethodInfo mi = ci.getMethod("<clinit>()", false);
1326: ThreadInfo ti = ss.getThreadInfo(0);
1327:
1328: if (mi != null) {
1329: StackFrame frame = null;
1330: // might be MJI, in which case we have to create the code and the stackframe
1331: if (mi.isMJI()) {
1332: mi = mi.createNativeCallStub();
1333: frame = new StackFrame(mi, true, null);
1334: frame.push(ci.getClassObjectRef(), true);
1335: } else {
1336: frame = new StackFrame(mi, true, null);
1337: }
1338:
1339: if (config.getBoolean("vm.atomic_init")) {
1340: mi.setAtomic(true);
1341: }
1342:
1343: ti.pushFrame(frame);
1344: }
1345:
1346: ci = ci.getSuperClass();
1347: }
1348: }
1349:
1350: void prepareMain(Config config) {
1351: DynamicArea da = ss.ks.da;
1352: ClassInfo ci = ClassInfo.getClassInfo(mainClassName);
1353: MethodInfo mi = ci
1354: .getMethod("main([Ljava/lang/String;)", false);
1355: ThreadInfo ti = ss.getThreadInfo(0);
1356:
1357: if (mi == null) {
1358: throw new JPFException("no main() method in "
1359: + ci.getName());
1360: }
1361:
1362: ti.pushFrame(new StackFrame(mi, false, null));
1363: ti.setStatus(ThreadInfo.RUNNING);
1364:
1365: int argsObjref = da.newArray("Ljava/lang/String;", args.length,
1366: null);
1367: ElementInfo argsElement = ss.ks.da.get(argsObjref);
1368:
1369: for (int i = 0; i < args.length; i++) {
1370: int stringObjref = da.newString(args[i], null);
1371: argsElement.setElement(i, stringObjref);
1372: }
1373: ti.setLocalVariable(0, argsObjref, true);
1374: }
1375:
1376: protected void loadStartupClasses() {
1377: String[] classes = { "java.lang.Object", "java.lang.Class",
1378: "java.lang.String", "java.lang.ThreadGroup",
1379: "java.lang.Thread", "java.io.PrintStream",
1380: "java.lang.System", "gov.nasa.jpf.jvm.Verify", "byte",
1381: "[B", "char", "[C", "int", "[I", "long", "[J" };
1382:
1383: for (int i = 0; i < classes.length; i++) {
1384: ClassInfo ci = ClassInfo.getClassInfo(classes[i]);
1385: ss.ks.sa.newStartupClass(ci);
1386: }
1387: }
1388:
1389: protected void initializeStartupClasses() {
1390: ss.ks.sa.initializeClasses();
1391: }
1392:
1393: protected void loadClass(ClassInfo ci) {
1394: StaticArea sa = getStaticArea();
1395: if (!sa.containsClass(ci.getName())) {
1396: sa.newClass(ci);
1397: }
1398: }
1399:
1400: static JVM getVM() {
1401: // <2do> remove this, no more static refs!
1402: return jvm;
1403: }
1404:
1405: /**
1406: * initialize all our static fields. Called from <clinit> and reset
1407: */
1408: static void initStaticFields() {
1409: error_id = 0;
1410: observableInvokes = new HashSet();
1411: observableLabels = new HashSet();
1412: observablePositions = new HashSet();
1413: observableReturns = new HashSet();
1414: }
1415:
1416: /**
1417: * return the 'heap' object, which is a global service
1418: */
1419: public DynamicArea getDynamicArea() {
1420: return ss.ks.da;
1421: }
1422:
1423: /**
1424: * same for "loaded classes", but be advised it will probably go away at some point
1425: */
1426: StaticArea getStaticArea() {
1427: return ss.ks.sa;
1428: }
1429:
1430: boolean finalizeObject(ElementInfo ei) {
1431: MethodInfo fin = ei.getClassInfo().getFinalizer();
1432:
1433: if (fin != null) {
1434: // <2do> not really - finalizers should run in their own thread
1435: ThreadInfo ti = ss.getRunningThread();
1436:
1437: // this is subtle - if this is not the last non-daemon, we have to finalize.
1438: // If it is, we don't. Instead of re-creating stack frames, we just flag
1439: // the object as not yet finalizable. For this purpose, it's a somewhat
1440: // braindead hack, but ultimately we need this anyway, since finalization
1441: // can make objects live again
1442: if (ti.countStackFrames() <= 0) {
1443: return false;
1444: }
1445:
1446: ti.push(ei.getThisReference(), true);
1447: ti.executeMethod(fin);
1448: }
1449:
1450: return true;
1451: }
1452:
1453: /**
1454: * VM state implementation. See the description of the VMState
1455: * interface for anticipated future API changes
1456: * NOTE - making JVMStates fully restorable is currently very
1457: * expensive and should only be done on a selective basis
1458: */
1459: class JVMState implements VMState {
1460:
1461: /**
1462: * snapshots of the current state restoration data
1463: * this is what we need to analyze the current state, but doesn't inlcude
1464: * the history (path and backtrack caches)
1465: */
1466: int[] ksStoringData;
1467: Object ksBacktrackData;
1468: Object ssBacktrackData;
1469:
1470: /** the set of last executed insns */
1471: TrailInfo lastTrailInfo;
1472:
1473: /* these are the icky parts - the history is kept as stacks inside the
1474: * JVM (for restoration reasons), hence we have to copy it if we want
1475: * to restore a state. Since this is really expensive, it has to be done
1476: * on demand, with varying degrees of information
1477: */
1478: Path path;
1479:
1480: Stack backtrackStack;
1481: Stack stateBacktrackStack;
1482: Stack stateStoringStack;
1483:
1484: JVMState() {
1485: ksStoringData = JVM.this .ksStoringData;
1486: ksBacktrackData = JVM.this .ksBacktrackData;
1487:
1488: // unfortunately we cannot cache the SystemState since it is changed
1489: // before we return from forward(), but after it got pushed on the
1490: // stateBacktrackStack
1491: ssBacktrackData = ss.getBacktrackData();
1492:
1493: lastTrailInfo = JVM.this .lastTrailInfo;
1494: }
1495:
1496: public Transition getLastTransition() {
1497: return lastTrailInfo;
1498: }
1499:
1500: // Beware - this is expensive. If this JVMState is not meant to be used
1501: // for state restoration (which is requested by makeRestorable()), stay
1502: // away from it. If you 'just' need to enumerate, keep track of the states
1503: // themselves (which would be required for graphical display anyway) and use
1504: // getLastTransition
1505: public Path getPath() {
1506: if (path == null) {
1507: path = JVM.this .getPath();
1508: }
1509:
1510: return path;
1511: }
1512:
1513: public int getThread() {
1514: return lastTrailInfo.getThread();
1515: }
1516:
1517: /**
1518: * this doesn't clone the backtracking info, i.e. we cannot backtrack
1519: * above this state again, only up to it
1520: */
1521: public void makeForwardRestorable() {
1522: path = JVM.this .getPath();
1523: }
1524:
1525: public boolean isForwardRestorable() {
1526: return (path != null);
1527: }
1528:
1529: /**
1530: * in addition to the path, we also have to copy the backtrack stacks
1531: * of the VM. This is overly expensive. DON'T DO UNLESS YOU HAVE TO!
1532: */
1533: public void makeRestorable() {
1534: path = JVM.this .getPath();
1535: stateBacktrackStack = (Stack) JVM.this .stateBacktrackStack
1536: .clone();
1537: stateStoringStack = (Stack) JVM.this .stateStoringStack
1538: .clone();
1539: backtrackStack = (Stack) JVM.this .backtrackStack.clone();
1540: }
1541:
1542: public boolean isRestorable() {
1543: return (stateBacktrackStack != null);
1544: }
1545: }
1546: }
|