--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package gov.nasa.jpf.vm;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.JPFConfigException;
+import gov.nasa.jpf.JPFException;
+import gov.nasa.jpf.JPFListenerException;
+import gov.nasa.jpf.jvm.ClassFile;
+import gov.nasa.jpf.vm.FinalizerThreadInfo;
+import gov.nasa.jpf.search.Search;
+import gov.nasa.jpf.util.IntTable;
+import gov.nasa.jpf.util.JPFLogger;
+import gov.nasa.jpf.util.Misc;
+import gov.nasa.jpf.util.Predicate;
+
+import java.io.PrintWriter;
+import java.nio.ByteOrder;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Map;
+
+
+/**
+ * This class represents the virtual machine. The virtual machine is able to
+ * move backward and forward one transition at a time.
+ */
+public abstract class VM {
+
+ /**
+ * this is a debugging aid to control compilation of expensive consistency checks
+ * (we don't control these with class-wise assertion enabling since we do use
+ * unconditional assertions for mandatory consistency checks)
+ */
+ public static final boolean CHECK_CONSISTENCY = false;
+
+ protected static final String[] EMPTY_ARGS = new String[0];
+
+ protected static JPFLogger log = JPF.getLogger("vm");
+
+ /**
+ * our execution context
+ */
+ protected JPF jpf;
+
+ /**
+ * The number of errors saved so far.
+ * Used to generate the name of the error trail file.
+ */
+ protected static int error_id;
+
+ /**
+ * <2do> - this is a hack to be removed once there are no static references
+ * anymore
+ */
+ protected static VM vm;
+
+ static {
+ initStaticFields();
+ }
+
+ protected SystemState ss;
+
+ protected FunctionObjectFactory funcObjFactory = new FunctionObjectFactory();
+
+ // <2do> - if you are confused about the various pieces of state and its
+ // storage/backtrack structures, I'm with you. It's mainly an attempt to
+ // separate non-policy VM state (objects), policy VM state (Scheduler)
+ // and general JPF execution state, with special support for stack oriented
+ // state restoration (backtracking).
+ // this needs to be cleaned up and the principle reinstated
+
+
+ protected Path path; /** execution path to current state */
+ protected StringBuilder out; /** buffer to store output along path execution */
+
+ /**
+ * various caches for VMListener state acquisition. NOTE - these are only
+ * valid during notification
+ *
+ * <2do> get rid of the 'lasts' in favor of queries on the insn, the executing
+ * thread, and the VM. This is superfluous work to for every notification
+ * (even if there are no listeners using it) that can easily lead to inconsistencies
+ */
+ protected Transition lastTrailInfo;
+
+ protected boolean isTraceReplay; // can be set by listeners to indicate this is a replay
+
+ /** the repository we use to find out if we already have seen a state */
+ protected StateSet stateSet;
+
+ /** this was the last stateId - note this is also used for stateless model checking */
+ protected int newStateId;
+
+ /** the structure responsible for storing and restoring backtrack info */
+ protected Backtracker backtracker;
+
+ /** optional serializer/restorer to support backtracker */
+ protected StateRestorer<?> restorer;
+
+ /** optional serializer to support stateSet */
+ protected StateSerializer serializer;
+
+ /** potential execution listeners. We keep them in a simple array to avoid
+ creating objects on each notification */
+ protected VMListener[] listeners = new VMListener[0];
+
+ /** did we get a new transition */
+ protected boolean transitionOccurred;
+
+ /** how we model execution time */
+ protected TimeModel timeModel;
+
+ /** ThreadChoiceGenerator management related to data races and shared objects */
+ protected Scheduler scheduler;
+
+
+ protected Config config; // that's for the options we use only once
+
+ // VM options we use frequently
+ protected boolean runGc;
+ protected boolean treeOutput;
+ protected boolean pathOutput;
+ protected boolean indentOutput;
+ protected boolean processFinalizers;
+
+ // <2do> there are probably many places where this should be used
+ protected boolean isBigEndian;
+
+ protected boolean initialized;
+
+ //thread filters
+ protected Predicate<ThreadInfo> userliveNonDaemonPredicate;
+ protected Predicate<ThreadInfo> timedoutRunnablePredicate;
+ protected Predicate<ThreadInfo> alivePredicate;
+ protected Predicate<ThreadInfo> userTimedoutRunnablePredicate;
+
+ // a list of actions to be run post GC. This is a bit redundant to VMListener,
+ // but in addition to avoid the per-instruction execution overhead of a VMListener
+ // we want a (internal) mechanism that is on-demand only, i.e. processed
+ // actions are removed from the list
+ protected ArrayList<Runnable> postGcActions = new ArrayList<Runnable>();
+
+ /**
+ * be prepared this might throw JPFConfigExceptions
+ */
+ public VM (JPF jpf, Config conf) {
+ this.jpf = jpf; // so that we know who instantiated us
+
+ // <2do> that's really a bad hack and should be removed once we
+ // have cleaned up the reference chains
+ vm = this;
+
+ config = conf;
+
+ runGc = config.getBoolean("vm.gc", true);
+
+ treeOutput = config.getBoolean("vm.tree_output", true);
+ // we have to defer setting pathOutput until we have a reporter registered
+ indentOutput = config.getBoolean("vm.indent_output",false);
+
+ processFinalizers = config.getBoolean("vm.process_finalizers", false);
+
+ isBigEndian = getPlatformEndianness(config);
+ initialized = false;
+
+ initTimeModel(config);
+
+ initSubsystems(config);
+ initFields(config);
+
+ // set predicates used to query from threadlist
+ userliveNonDaemonPredicate = new Predicate<ThreadInfo>() {
+ @Override
+ public boolean isTrue (ThreadInfo ti) {
+ return (!ti.isDaemon() && !ti.isTerminated() && !ti.isSystemThread());
+ }
+ };
+
+ timedoutRunnablePredicate = new Predicate<ThreadInfo>() {
+ @Override
+ public boolean isTrue (ThreadInfo ti) {
+ return (ti.isTimeoutRunnable());
+ }
+ };
+
+ userTimedoutRunnablePredicate = new Predicate<ThreadInfo>() {
+ @Override
+ public boolean isTrue (ThreadInfo ti) {
+ return (ti.isTimeoutRunnable() && !ti.isSystemThread());
+ }
+ };
+
+ alivePredicate = new Predicate<ThreadInfo>() {
+ @Override
+ public boolean isTrue (ThreadInfo ti) {
+ return (ti.isAlive());
+ }
+ };
+ }
+
+ /**
+ * just here for unit test mockups, don't use as implicit base ctor in
+ * VM derived classes
+ */
+ protected VM (){}
+
+ public JPF getJPF() {
+ return jpf;
+ }
+
+ public void initFields (Config config) {
+ path = new Path("fix-this!");
+ out = null;
+
+ ss = new SystemState(config, this);
+
+ stateSet = config.getInstance("vm.storage.class", StateSet.class);
+ if (stateSet != null) stateSet.attach(this);
+ backtracker = config.getEssentialInstance("vm.backtracker.class", Backtracker.class);
+ backtracker.attach(this);
+
+ scheduler = config.getEssentialInstance("vm.scheduler.class", Scheduler.class);
+
+ newStateId = -1;
+ }
+
+ protected void initSubsystems (Config config) {
+ ClassLoaderInfo.init(config);
+ ClassInfo.init(config);
+ ThreadInfo.init(config);
+ ElementInfo.init(config);
+ MethodInfo.init(config);
+ NativePeer.init(config);
+ ChoiceGeneratorBase.init(config);
+
+ // peer classes get initialized upon NativePeer creation
+ }
+
+ protected void initTimeModel (Config config){
+ Class<?>[] argTypes = { VM.class, Config.class };
+ Object[] args = { this, config };
+ timeModel = config.getEssentialInstance("vm.time.class", TimeModel.class, argTypes, args);
+ }
+
+ /**
+ * called after the JPF run is finished. Shouldn't be public, but is called by JPF
+ */
+ public void cleanUp(){
+ // nothing yet
+ }
+
+ protected boolean getPlatformEndianness (Config config){
+ String endianness = config.getString("vm.endian");
+ if (endianness == null) {
+ return ByteOrder.nativeOrder() == ByteOrder.BIG_ENDIAN;
+ } else if (endianness.equalsIgnoreCase("big")) {
+ return true;
+ } else if (endianness.equalsIgnoreCase("little")) {
+ return false;
+ } else {
+ config.exception("illegal vm.endian value: " + endianness);
+ return false; // doesn't matter
+ }
+ }
+
+ public boolean isBigEndianPlatform(){
+ return isBigEndian;
+ }
+
+ public boolean finalizersEnabled() {
+ return processFinalizers;
+ }
+
+ public boolean isInitialized() {
+ return initialized;
+ }
+
+ public boolean isSingleProcess() {
+ return true;
+ }
+
+ /**
+ * do we see our model classes? Some of them cannot be used from the standard CLASSPATH, because they
+ * are tightly coupled with the JPF core (e.g. java.lang.Class, java.lang.Thread,
+ * java.lang.StackTraceElement etc.)
+ * Our strategy here is kind of lame - we just look into java.lang.Class if we find the 'uniqueId' field
+ * (that's a true '42')
+ */
+ static boolean checkSystemClassCompatibility (SystemClassLoaderInfo systemLoader) {
+ ClassInfo ci = systemLoader.getClassClassInfo();
+ return ci.checkIfValidClassClassInfo();
+ }
+
+ static boolean isValidClassName (String clsName) {
+ if ( !clsName.matches("[a-zA-Z_$][a-zA-Z_$0-9.]*")) {
+ return false;
+ }
+
+ // well, those two could be part of valid class names, but
+ // in all likeliness somebody specified a filename instead of
+ // a classname
+ if (clsName.endsWith(".java")) {
+ return false;
+ }
+ if (clsName.endsWith(".class")) {
+ return false;
+ }
+
+ return true;
+ }
+
+ //--- ThreadInfo factory methods
+ protected ThreadInfo createMainThreadInfo (int id, ApplicationContext appCtx){
+ ThreadInfo tiMain = new ThreadInfo( this, id, appCtx);
+ ThreadInfo.currentThread = tiMain; // we still need this for listeners that process startup class loading events
+ registerThread(tiMain);
+
+ return tiMain;
+ }
+
+ protected ThreadInfo createThreadInfo (int objRef, int groupRef, int runnableRef, int nameRef){
+ ThreadInfo tiCurrent = ThreadInfo.getCurrentThread();
+ ThreadInfo tiNew = new ThreadInfo( this, objRef, groupRef, runnableRef, nameRef, tiCurrent);
+
+ // note that we have to register here so that subsequent native peer calls can use the objRef
+ // to lookup the ThreadInfo. This is a bit premature since the thread is not runnable yet,
+ // but chances are it will be started soon, so we don't waste another data structure to do the mapping
+ registerThread( tiNew);
+
+ return tiNew;
+ }
+
+ // created if the option "vm.process_finalizers" is set to true
+ protected ThreadInfo createFinalizerThreadInfo (int id, ApplicationContext appCtx){
+ FinalizerThreadInfo finalizerTi = new FinalizerThreadInfo( this, appCtx, id);
+ registerThread(finalizerTi);
+
+ return finalizerTi;
+ }
+
+ /**
+ * the minimal set of system classes we need for initialization
+ */
+ protected List<String> getStartupSystemClassNames() {
+ ArrayList<String> startupClasses = new ArrayList<String>(64);
+
+ // bare essentials
+ startupClasses.add("java.lang.Object");
+ startupClasses.add("java.lang.Class");
+ startupClasses.add("java.lang.ClassLoader");
+
+ // the builtin types (and their arrays)
+ startupClasses.add("boolean");
+ startupClasses.add("[Z");
+ startupClasses.add("byte");
+ startupClasses.add("[B");
+ startupClasses.add("char");
+ startupClasses.add("[C");
+ startupClasses.add("short");
+ startupClasses.add("[S");
+ startupClasses.add("int");
+ startupClasses.add("[I");
+ startupClasses.add("long");
+ startupClasses.add("[J");
+ startupClasses.add("float");
+ startupClasses.add("[F");
+ startupClasses.add("double");
+ startupClasses.add("[D");
+ startupClasses.add("void");
+
+ // the box types
+ startupClasses.add("java.lang.Boolean");
+ startupClasses.add("java.lang.Character");
+ startupClasses.add("java.lang.Short");
+ startupClasses.add("java.lang.Integer");
+ startupClasses.add("java.lang.Long");
+ startupClasses.add("java.lang.Float");
+ startupClasses.add("java.lang.Double");
+ startupClasses.add("java.lang.Byte");
+
+ // the cache for box types
+ startupClasses.add("gov.nasa.jpf.BoxObjectCaches");
+
+ // standard system classes
+ startupClasses.add("java.lang.String");
+ startupClasses.add("java.lang.Thread");
+ startupClasses.add("java.lang.ThreadGroup");
+ startupClasses.add("java.lang.Thread$State");
+ startupClasses.add("java.lang.Thread$Permit");
+ startupClasses.add("java.io.PrintStream");
+ startupClasses.add("java.io.InputStream");
+ startupClasses.add("java.lang.System");
+ startupClasses.add("java.lang.ref.Reference");
+ startupClasses.add("java.lang.ref.WeakReference");
+ startupClasses.add("java.lang.Enum");
+ startupClasses.add("gov.nasa.jpf.FinalizerThread");
+
+ // we could be more fancy and use wildcard patterns and the current classpath
+ // to specify extra classes, but this could be VERY expensive. Projected use
+ // is mostly to avoid static init of single classes during the search
+ String[] extraStartupClasses = config.getStringArray("vm.extra_startup_classes");
+ if (extraStartupClasses != null) {
+ for (String extraCls : extraStartupClasses) {
+ startupClasses.add(extraCls);
+ }
+ }
+
+ // the main class has to be handled separately since it might be VM specific
+
+ return startupClasses;
+ }
+
+ /**
+ * return a list of ClassInfos for essential system types
+ *
+ * If system classes are not found, or are not valid JPF model classes, we throw
+ * a JPFConfigException and exit
+ *
+ * returned ClassInfos are not yet registered in Statics and don't have class objects
+ */
+ protected List<ClassInfo> getStartupSystemClassInfos (SystemClassLoaderInfo sysCl, ThreadInfo tiMain){
+ LinkedList<ClassInfo> list = new LinkedList<ClassInfo>();
+
+ try {
+ for (String clsName : getStartupSystemClassNames()) {
+ ClassInfo ci = sysCl.getResolvedClassInfo(clsName);
+ ci.registerStartupClass( tiMain, list); // takes care of superclasses and interfaces
+ }
+ } catch (ClassInfoException e){
+ e.printStackTrace();
+ throw new JPFConfigException("cannot load system class " + e.getFailedClass());
+ }
+
+ return list;
+ }
+
+ /**
+ * this adds the application main class and its supers to the list of startup classes
+ */
+ protected ClassInfo getMainClassInfo (SystemClassLoaderInfo sysCl, String mainClassName, ThreadInfo tiMain, List<ClassInfo> list){
+ try {
+ ClassInfo ciMain = sysCl.getResolvedClassInfo(mainClassName);
+ ciMain.registerStartupClass(tiMain, list); // this might add a couple more
+
+ return ciMain;
+
+ } catch (ClassInfoException e){
+ throw new JPFConfigException("cannot load application class " + e.getFailedClass());
+ }
+ }
+
+ /*
+ * these are called when creating ApplicationContexts and can be overridden by concrete VM types
+ */
+ protected SystemClassLoaderInfo createSystemClassLoaderInfo (int appId) {
+ Class<?>[] argTypes = { VM.class, int.class };
+
+ Object[] args = { this, Integer.valueOf(appId)};
+ SystemClassLoaderInfo sysCli = config.getEssentialInstance("vm.classloader.class", SystemClassLoaderInfo.class, argTypes, args);
+ return sysCli;
+ }
+
+ protected void createSystemClassLoaderObject (SystemClassLoaderInfo sysCl, ThreadInfo tiMain) {
+ Heap heap = getHeap();
+
+ // create ClassLoader object for the ClassLoader type defined by this SystemClassLoaderInfo
+ // NOTE - this requires the SystemClassLoaderInfo cache to be initialized
+ ClassInfo ciCl = sysCl.getClassLoaderClassInfo();
+ ElementInfo ei = heap.newObject( ciCl, tiMain);
+ //ei.setReferenceField("parent", MJIEnv.NULL);
+ heap.registerPinDown(ei.getObjectRef());
+
+ sysCl.setClassLoaderObject(ei);
+ }
+
+ protected void pushMainEntryArgs (MethodInfo miMain, String[] args, ThreadInfo tiMain, DirectCallStackFrame frame){
+ String sig = miMain.getSignature();
+ Heap heap = getHeap();
+
+ if (sig.contains("([Ljava/lang/String;)")){
+ ElementInfo eiArgs = heap.newArray("Ljava/lang/String;", args.length, tiMain);
+ for (int i = 0; i < args.length; i++) {
+ ElementInfo eiArg = heap.newString(args[i], tiMain);
+ eiArgs.setReferenceElement(i, eiArg.getObjectRef());
+ }
+ frame.setReferenceArgument( 0, eiArgs.getObjectRef(), null);
+
+ } else if (sig.contains("(Ljava/lang/String;)")){
+ if (args.length > 1){
+ ElementInfo eiArg = heap.newString(args[0], tiMain);
+ frame.setReferenceArgument( 0, eiArg.getObjectRef(), null);
+ } else {
+ frame.setReferenceArgument( 0, MJIEnv.NULL, null);
+ }
+
+ } else if (!sig.contains("()")){
+ throw new JPFException("unsupported main entry signature: " + miMain.getFullName());
+ }
+ }
+
+ protected void pushMainEntry (MethodInfo miMain, String[] args, ThreadInfo tiMain) {
+ DirectCallStackFrame frame = miMain.createDirectCallStackFrame(tiMain, 0);
+ pushMainEntryArgs( miMain, args, tiMain, frame);
+ tiMain.pushFrame(frame);
+ }
+
+ protected MethodInfo getMainEntryMethodInfo (String mthName, ClassInfo ciMain) {
+ MethodInfo miMain = ciMain.getMethod(mthName, true);
+
+ //--- do some sanity checks if this is a valid entry method
+ if (miMain == null || !miMain.isStatic()) {
+ throw new JPFConfigException("no static entry method: " + ciMain.getName() + '.' + mthName);
+ }
+
+ return miMain;
+ }
+
+ protected void pushClinits (List<ClassInfo> startupClasses, ThreadInfo tiMain) {
+ for (ClassInfo ci : startupClasses){
+ MethodInfo mi = ci.getMethod("<clinit>()V", false);
+ if (mi != null) {
+ DirectCallStackFrame frame = mi.createDirectCallStackFrame(tiMain, 0);
+ tiMain.pushFrame(frame);
+ } else {
+ ci.setInitialized();
+ }
+ }
+ }
+
+ /**
+ * this is the main initialization point that sets up startup objects threads and callstacks.
+ * If this returns false VM initialization cannot proceed and JPF will terminate
+ */
+ public abstract boolean initialize ();
+
+ /**
+ * create and initialize the main thread for the given ApplicationContext.
+ * This is called from VM.initialize() implementations, the caller has to handle exceptions that should be reported
+ * differently (JPFConfigException, ClassInfoException)
+ */
+ protected ThreadInfo initializeMainThread (ApplicationContext appCtx, int tid){
+ SystemClassLoaderInfo sysCl = appCtx.sysCl;
+
+ ThreadInfo tiMain = createMainThreadInfo(tid, appCtx);
+ List<ClassInfo> startupClasses = getStartupSystemClassInfos(sysCl, tiMain);
+ ClassInfo ciMain = getMainClassInfo(sysCl, appCtx.mainClassName, tiMain, startupClasses);
+
+ if (!checkSystemClassCompatibility( sysCl)){
+ throw new JPFConfigException("non-JPF system classes, check classpath");
+ }
+
+ // create essential objects (we can't call ctors yet)
+ createSystemClassLoaderObject(sysCl, tiMain);
+ for (ClassInfo ci : startupClasses) {
+ ci.createAndLinkStartupClassObject(tiMain);
+ }
+ tiMain.createMainThreadObject(sysCl);
+ registerThread(tiMain);
+
+ // note that StackFrames have to be pushed in reverse order
+ MethodInfo miMain = getMainEntryMethodInfo(appCtx.mainEntry, ciMain);
+ appCtx.setEntryMethod(miMain);
+ pushMainEntry(miMain, appCtx.args, tiMain);
+ Collections.reverse(startupClasses);
+ pushClinits(startupClasses, tiMain);
+
+ registerThreadListCleanup(sysCl.getThreadClassInfo());
+
+ return tiMain;
+ }
+
+ protected void initializeFinalizerThread (ApplicationContext appCtx, int tid) {
+ if(processFinalizers) {
+ ApplicationContext app = getCurrentApplicationContext();
+ FinalizerThreadInfo finalizerTi = app.getFinalizerThread();
+
+ finalizerTi = (FinalizerThreadInfo) createFinalizerThreadInfo(tid, app);
+ finalizerTi.createFinalizerThreadObject(app.getSystemClassLoader());
+
+ appCtx.setFinalizerThread(finalizerTi);
+ }
+ }
+
+ protected void registerThreadListCleanup (ClassInfo ciThread){
+ assert ciThread != null : "java.lang.Thread not loaded yet";
+
+ ciThread.addReleaseAction( new ReleaseAction(){
+ @Override
+ public void release (ElementInfo ei) {
+ ThreadList tl = getThreadList();
+ int objRef = ei.getObjectRef();
+ ThreadInfo ti = tl.getThreadInfoForObjRef(objRef);
+ if (tl.remove(ti)){
+ vm.getKernelState().changed();
+ }
+ }
+ });
+ }
+
+
+ /**
+ * override this if the concrete VM needs a special root CG
+ */
+ protected void setRootCG(){
+ scheduler.setRootCG();
+ }
+
+ protected void initSystemState (ThreadInfo mainThread){
+ ss.setStartThread(mainThread);
+
+ ss.recordSteps(hasToRecordSteps());
+
+ if (!pathOutput) { // don't override if explicitly requested
+ pathOutput = hasToRecordPathOutput();
+ }
+
+ setRootCG(); // this has to be guaranteed to register a CG
+ if (!hasNextChoiceGenerator()){
+ throw new JPFException("scheduler failed to set ROOT choice generator: " + scheduler);
+ }
+
+ transitionOccurred = true;
+ }
+
+ public void addPostGcAction (Runnable r){
+ postGcActions.add(r);
+ }
+
+ /**
+ * to be called from the Heap after GC is completed (i.e. only live objects remain)
+ */
+ public void processPostGcActions(){
+ if (!postGcActions.isEmpty()){
+ for (Runnable r : postGcActions){
+ r.run();
+ }
+
+ postGcActions.clear();
+ }
+ }
+
+ public void addListener (VMListener newListener) {
+ log.info("VMListener added: ", newListener);
+ listeners = Misc.appendElement(listeners, newListener);
+ }
+
+ public boolean hasListenerOfType (Class<?> listenerCls) {
+ return Misc.hasElementOfType(listeners, listenerCls);
+ }
+
+ public <T> T getNextListenerOfType(Class<T> type, T prev){
+ return Misc.getNextElementOfType(listeners, type, prev);
+ }
+
+ public void removeListener (VMListener removeListener) {
+ listeners = Misc.removeElement(listeners, removeListener);
+ }
+
+ public void setTraceReplay (boolean isReplay) {
+ isTraceReplay = isReplay;
+ }
+
+ public boolean isTraceReplay() {
+ return isTraceReplay;
+ }
+
+ public boolean hasToRecordSteps() {
+ // we have to record if there either is a reporter that has
+ // a 'trace' topic, or there is an explicit request
+ return jpf.getReporter().hasToReportTrace()
+ || config.getBoolean("vm.store_steps");
+ }
+
+ public void recordSteps( boolean cond) {
+ // <2do> not ideal - it might be already too late when this is called
+
+ config.setProperty("vm.store_steps", cond ? "true" : "false");
+
+ if (ss != null){
+ ss.recordSteps(cond);
+ }
+ }
+
+ public boolean hasToRecordPathOutput() {
+ if (config.getBoolean("vm.path_output")){ // explicitly requested
+ return true;
+ } else {
+ return jpf.getReporter().hasToReportOutput(); // implicilty required
+ }
+ }
+
+ //--- VM listener notifications
+
+ /*
+ * while some of these can be called from various places, the calls that happen from within Instruction.execute() should
+ * happen right before return since listeners might do things such as ThreadInfo.createAndThrowException(..), i.e. cause
+ * side effects that would violate consistency requirements of successive operations (e.g. by assuming we are still executing
+ * in the same StackFrame - after throwing an exception)
+ */
+
+ protected void notifyVMInitialized () {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].vmInitialized(this);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during vmInitialized() notification", t);
+ }
+ }
+
+ protected void notifyChoiceGeneratorRegistered (ChoiceGenerator<?>cg, ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].choiceGeneratorRegistered(this, cg, ti, ti.getPC());
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during choiceGeneratorRegistered() notification", t);
+ }
+ }
+
+ protected void notifyChoiceGeneratorSet (ChoiceGenerator<?>cg) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].choiceGeneratorSet(this, cg);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during choiceGeneratorSet() notification", t);
+ }
+ }
+
+ protected void notifyChoiceGeneratorAdvanced (ChoiceGenerator<?>cg) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].choiceGeneratorAdvanced(this, cg);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during choiceGeneratorAdvanced() notification", t);
+ }
+ }
+
+ protected void notifyChoiceGeneratorProcessed (ChoiceGenerator<?>cg) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].choiceGeneratorProcessed(this, cg);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during choiceGeneratorProcessed() notification", t);
+ }
+ }
+
+ protected void notifyExecuteInstruction (ThreadInfo ti, Instruction insn) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].executeInstruction(this, ti, insn);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during executeInstruction() notification", t);
+ }
+ }
+
+ protected void notifyInstructionExecuted (ThreadInfo ti, Instruction insn, Instruction nextInsn) {
+ try {
+ //listener.instructionExecuted(this);
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].instructionExecuted(this, ti, nextInsn, insn);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during instructionExecuted() notification", t);
+ }
+ }
+
+ protected void notifyThreadStarted (ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].threadStarted(this, ti);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during threadStarted() notification", t);
+ }
+ }
+
+ // NOTE: the supplied ThreadInfo does NOT have to be the running thread, as this
+ // notification can occur as a result of a lock operation in the current thread
+ protected void notifyThreadBlocked (ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].threadBlocked(this, ti, ti.getLockObject());
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during threadBlocked() notification", t);
+ }
+ }
+
+ protected void notifyThreadWaiting (ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].threadWaiting(this, ti);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during threadWaiting() notification", t);
+ }
+ }
+
+ protected void notifyThreadNotified (ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].threadNotified(this, ti);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during threadNotified() notification", t);
+ }
+ }
+
+ protected void notifyThreadInterrupted (ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].threadInterrupted(this, ti);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during threadInterrupted() notification", t);
+ }
+ }
+
+ protected void notifyThreadTerminated (ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].threadTerminated(this, ti);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during threadTerminated() notification", t);
+ }
+ }
+
+ protected void notifyThreadScheduled (ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].threadScheduled(this, ti);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during threadScheduled() notification", t);
+ }
+ }
+
+ protected void notifyLoadClass (ClassFile cf){
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].loadClass(this, cf);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during classLoaded() notification", t);
+ }
+ }
+
+ protected void notifyClassLoaded(ClassInfo ci) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].classLoaded(this, ci);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during classLoaded() notification", t);
+ }
+ }
+
+ protected void notifyObjectCreated(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectCreated(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectCreated() notification", t);
+ }
+ }
+
+ protected void notifyObjectReleased(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectReleased(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectReleased() notification", t);
+ }
+ }
+
+ protected void notifyObjectLocked(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectLocked(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectLocked() notification", t);
+ }
+ }
+
+ protected void notifyObjectUnlocked(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectUnlocked(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectUnlocked() notification", t);
+ }
+ }
+
+ protected void notifyObjectWait(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectWait(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectWait() notification", t);
+ }
+ }
+
+ protected void notifyObjectExposed(ThreadInfo ti, ElementInfo eiShared, ElementInfo eiExposed) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectExposed(this, ti, eiShared, eiExposed);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectExposed() notification", t);
+ }
+ }
+
+ protected void notifyObjectShared(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectShared(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectShared() notification", t);
+ }
+ }
+
+ protected void notifyObjectNotifies(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectNotify(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectNotifies() notification", t);
+ }
+ }
+
+ protected void notifyObjectNotifiesAll(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].objectNotifyAll(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during objectNotifiesAll() notification", t);
+ }
+ }
+
+ protected void notifyGCBegin() {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].gcBegin(this);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during gcBegin() notification", t);
+ }
+ }
+
+ protected void notifyGCEnd() {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].gcEnd(this);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during gcEnd() notification", t);
+ }
+ }
+
+ protected void notifyExceptionThrown(ThreadInfo ti, ElementInfo ei) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].exceptionThrown(this, ti, ei);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during exceptionThrown() notification", t);
+ }
+ }
+
+ protected void notifyExceptionBailout(ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].exceptionBailout(this, ti);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during exceptionBailout() notification", t);
+ }
+ }
+
+ protected void notifyExceptionHandled(ThreadInfo ti) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].exceptionHandled(this, ti);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during exceptionHandled() notification", t);
+ }
+ }
+
+ protected void notifyMethodEntered(ThreadInfo ti, MethodInfo mi) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].methodEntered(this, ti, mi);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during methodEntered() notification", t);
+ }
+ }
+
+ protected void notifyMethodExited(ThreadInfo ti, MethodInfo mi) {
+ try {
+ for (int i = 0; i < listeners.length; i++) {
+ listeners[i].methodExited(this, ti, mi);
+ }
+ } catch (UncaughtException x) {
+ throw x;
+ } catch (JPF.ExitException x) {
+ throw x;
+ } catch (Throwable t) {
+ throw new JPFListenerException("exception during methodExited() notification", t);
+ }
+ }
+
+ // VMListener acquisition
+ public String getThreadName () {
+ ThreadInfo ti = ThreadInfo.getCurrentThread();
+
+ return ti.getName();
+ }
+
+ // VMListener acquisition
+ public Instruction getInstruction () {
+ ThreadInfo ti = ThreadInfo.getCurrentThread();
+ return ti.getPC();
+ }
+
+ /**
+ * note this is gone after backtracking or starting the next exception
+ */
+ public ExceptionInfo getPendingException () {
+ ThreadInfo ti = ThreadInfo.getCurrentThread();
+
+ if (ti != null){
+ return ti.getPendingException();
+ } else {
+ return null;
+ }
+ }
+
+ public Step getLastStep () {
+ Transition trail = ss.getTrail();
+ if (trail != null) {
+ return trail.getLastStep();
+ }
+
+ return null;
+ }
+
+ public Transition getLastTransition () {
+ if (path.size() == 0) {
+ return null;
+ }
+ return path.get(path.size() - 1);
+ }
+
+ public ClassInfo getClassInfo (int objref) {
+ if (objref != MJIEnv.NULL) {
+ return getElementInfo(objref).getClassInfo();
+ } else {
+ return null;
+ }
+ }
+
+ /**
+ * NOTE: only use this locally, since the path is getting modified by the VM
+ *
+ * The path only contains all states when queried from a stateAdvanced() notification.
+ * If this is called from an instructionExecuted() (or other VMListener), and you need
+ * the ongoing transition in it, you have to call updatePath() first
+ */
+ public Path getPath () {
+ return path;
+ }
+
+ /**
+ * this is the ongoing transition. Note that it is not yet stored in the path
+ * if this is called from a VMListener notification
+ */
+ public Transition getCurrentTransition() {
+ return ss.getTrail();
+ }
+
+ /**
+ * use that one if you have to store the path for subsequent use
+ *
+ * NOTE: without a prior call to updatePath(), this does NOT contain the
+ * ongoing transition. See getPath() for usage from a VMListener
+ */
+ public Path getClonedPath () {
+ return path.clone();
+ }
+
+ public int getPathLength () {
+ return path.size();
+ }
+
+ public ThreadList getThreadList () {
+ return getKernelState().getThreadList();
+ }
+
+ public ClassLoaderList getClassLoaderList() {
+ return getKernelState().getClassLoaderList();
+ }
+
+
+ /**
+ * Bundles up the state of the system for export
+ */
+ public RestorableVMState getRestorableState () {
+ return new RestorableVMState(this);
+ }
+
+ /**
+ * Gets the system state.
+ */
+ public SystemState getSystemState () {
+ return ss;
+ }
+
+ public KernelState getKernelState () {
+ return ss.getKernelState();
+ }
+
+ public void kernelStateChanged(){
+ ss.getKernelState().changed();
+ }
+
+ public Config getConfig() {
+ return config;
+ }
+
+ public Backtracker getBacktracker() {
+ return backtracker;
+ }
+
+ @SuppressWarnings("unchecked")
+ public <T> StateRestorer<T> getRestorer() {
+ if (restorer == null) {
+ if (serializer instanceof StateRestorer) {
+ restorer = (StateRestorer<?>) serializer;
+ } else if (stateSet instanceof StateRestorer) {
+ restorer = (StateRestorer<?>) stateSet;
+ } else {
+ // config read only if serializer is not also a restorer
+ restorer = config.getInstance("vm.restorer.class", StateRestorer.class);
+ }
+ restorer.attach(this);
+ }
+
+ return (StateRestorer<T>) restorer;
+ }
+
+ public StateSerializer getSerializer() {
+ if (serializer == null) {
+ serializer = config.getEssentialInstance("vm.serializer.class",
+ StateSerializer.class);
+ serializer.attach(this);
+ }
+ return serializer;
+ }
+
+ public void setSerializer (StateSerializer newSerializer){
+ serializer = newSerializer;
+ serializer.attach(this);
+ }
+
+ /**
+ * Returns the stateSet if states are being matched.
+ */
+ public StateSet getStateSet() {
+ return stateSet;
+ }
+
+ public Scheduler getScheduler(){
+ return scheduler;
+ }
+
+ public FunctionObjectFactory getFunctionObjectFacotry() {
+ return funcObjFactory;
+ }
+
+ /**
+ * return the last registered SystemState's ChoiceGenerator object
+ * NOTE: there might be more than one ChoiceGenerator associated with the
+ * current transition (ChoiceGenerators can be cascaded)
+ */
+ public ChoiceGenerator<?> getChoiceGenerator () {
+ return ss.getChoiceGenerator();
+ }
+
+ public ChoiceGenerator<?> getNextChoiceGenerator() {
+ return ss.getNextChoiceGenerator();
+ }
+
+ public boolean hasNextChoiceGenerator(){
+ return (ss.getNextChoiceGenerator() != null);
+ }
+
+ public boolean setNextChoiceGenerator (ChoiceGenerator<?> cg){
+ return ss.setNextChoiceGenerator(cg);
+ }
+
+ public void setMandatoryNextChoiceGenerator (ChoiceGenerator<?> cg, String failMsg){
+ ss.setMandatoryNextChoiceGenerator(cg, failMsg);
+ }
+
+ /**
+ * return the latest registered ChoiceGenerator used in this transition
+ * that matches the provided 'id' and is of 'cgType'.
+ *
+ * This should be the main getter for clients that are cascade aware
+ */
+ public <T extends ChoiceGenerator<?>> T getCurrentChoiceGenerator (String id, Class<T> cgType) {
+ return ss.getCurrentChoiceGenerator(id,cgType);
+ }
+
+ /**
+ * returns all ChoiceGenerators in current path
+ */
+ public ChoiceGenerator<?>[] getChoiceGenerators() {
+ return ss.getChoiceGenerators();
+ }
+
+ public <T extends ChoiceGenerator<?>> T[] getChoiceGeneratorsOfType (Class<T> cgType) {
+ return ss.getChoiceGeneratorsOfType(cgType);
+ }
+
+ public <T extends ChoiceGenerator<?>> T getLastChoiceGeneratorOfType (Class<T> cgType){
+ return ss.getLastChoiceGeneratorOfType(cgType);
+ }
+
+ public ChoiceGenerator<?> getLastChoiceGeneratorInThread (ThreadInfo ti){
+ return ss.getLastChoiceGeneratorInThread(ti);
+ }
+
+ public void print (String s) {
+ if (treeOutput) {
+ System.out.print(s);
+ }
+
+ if (pathOutput) {
+ appendOutput(s);
+ }
+ }
+
+ public void println (String s) {
+ if (treeOutput) {
+ if (indentOutput){
+ StringBuilder indent = new StringBuilder();
+ int i;
+ for (i = 0;i<=path.size();i++) {
+ indent.append('|').append(i);
+ }
+ indent.append("|").append(s);
+ System.out.println(indent);
+ }
+ else {
+ System.out.println(s);
+ }
+ }
+
+ if (pathOutput) {
+ appendOutput(s);
+ appendOutput('\n');
+ }
+ }
+
+ public void print (boolean b) {
+ if (treeOutput) {
+ System.out.print(b);
+ }
+
+ if (pathOutput) {
+ appendOutput(Boolean.toString(b));
+ }
+ }
+
+ public void print (char c) {
+ if (treeOutput) {
+ System.out.print(c);
+ }
+
+ if (pathOutput) {
+ appendOutput(c);
+ }
+ }
+
+ public void print (int i) {
+ if (treeOutput) {
+ System.out.print(i);
+ }
+
+ if (pathOutput) {
+ appendOutput(Integer.toString(i));
+ }
+ }
+
+ public void print (long l) {
+ if (treeOutput) {
+ System.out.print(l);
+ }
+
+ if (pathOutput) {
+ appendOutput(Long.toString(l));
+ }
+ }
+
+ public void print (double d) {
+ if (treeOutput) {
+ System.out.print(d);
+ }
+
+ if (pathOutput) {
+ appendOutput(Double.toString(d));
+ }
+ }
+
+ public void print (float f) {
+ if (treeOutput) {
+ System.out.print(f);
+ }
+
+ if (pathOutput) {
+ appendOutput(Float.toString(f));
+ }
+ }
+
+ public void println () {
+ if (treeOutput) {
+ System.out.println();
+ }
+
+ if (pathOutput) {
+ appendOutput('\n');
+ }
+ }
+
+
+ void appendOutput (String s) {
+ if (out == null) {
+ out = new StringBuilder();
+ }
+ out.append(s);
+ }
+
+ void appendOutput (char c) {
+ if (out == null) {
+ out = new StringBuilder();
+ }
+ out.append(c);
+ }
+
+ /**
+ * get the pending output (not yet stored in the path)
+ */
+ public String getPendingOutput() {
+ if (out != null && out.length() > 0){
+ return out.toString();
+ } else {
+ return null;
+ }
+ }
+
+ /**
+ * this is here so that we can intercept it in subclassed VMs
+ */
+ public Instruction handleException (ThreadInfo ti, int xObjRef){
+ ti = null; // Get rid of IDE warning
+ xObjRef = 0;
+ return null;
+ }
+
+ public void storeTrace (String fileName, String comment, boolean verbose) {
+ ChoicePoint.storeTrace(fileName, getSUTName(), comment,
+ ss.getChoiceGenerators(), verbose);
+ }
+
+ public void storePathOutput () {
+ pathOutput = true;
+ }
+
+ private void printCG (ChoiceGenerator<?> cg, int n){
+ ChoiceGenerator cgPrev = cg.getPreviousChoiceGenerator();
+ if (cgPrev != null){
+ printCG( cgPrev, --n);
+ }
+
+ System.out.printf("[%d] ", n);
+ System.out.println(cg);
+ }
+
+ // for debugging purposes
+ public void printChoiceGeneratorStack(){
+ ChoiceGenerator<?> cg = getChoiceGenerator();
+ if (cg != null){
+ int n = cg.getNumberOfParents();
+ printCG(cg, n);
+ }
+ }
+
+ public ThreadInfo[] getLiveThreads () {
+ return getThreadList().getThreads();
+ }
+
+ /**
+ * print call stacks of all live threads
+ * this is also used for debugging purposes, so we can't move it to the Reporter system
+ * (it's also using a bit too many internals for that)
+ */
+ public void printLiveThreadStatus (PrintWriter pw) {
+ int nThreads = ss.getThreadCount();
+ ThreadInfo[] threads = getThreadList().getThreads();
+ int n=0;
+
+ for (int i = 0; i < nThreads; i++) {
+ ThreadInfo ti = threads[i];
+
+ if (ti.getStackDepth() > 0){
+ n++;
+ //pw.print("Thread: ");
+ //pw.print(tiMain.getName());
+ pw.println(ti.getStateDescription());
+
+ List<ElementInfo> locks = ti.getLockedObjects();
+ if (!locks.isEmpty()) {
+ pw.print(" owned locks:");
+ boolean first = true;
+ for (ElementInfo e : locks) {
+ if (first) {
+ first = false;
+ } else {
+ pw.print(",");
+ }
+ pw.print(e);
+ }
+ pw.println();
+ }
+
+ ElementInfo ei = ti.getLockObject();
+ if (ei != null) {
+ if (ti.getState() == ThreadInfo.State.WAITING) {
+ pw.print( " waiting on: ");
+ } else {
+ pw.print( " blocked on: ");
+ }
+ pw.println(ei);
+ }
+
+ pw.println(" call stack:");
+ for (StackFrame frame : ti){
+ if (!frame.isDirectCallFrame()) {
+ pw.print("\tat ");
+ pw.println(frame.getStackTraceInfo());
+ }
+ }
+
+ pw.println();
+ }
+ }
+
+ if (n==0) {
+ pw.println("no live threads");
+ }
+ }
+
+ // just a debugging aid
+ public void dumpThreadStates () {
+ java.io.PrintWriter pw = new java.io.PrintWriter(System.out, true);
+ printLiveThreadStatus(pw);
+ pw.flush();
+ }
+
+ /**
+ * Moves one step backward. This method and forward() are the main methods
+ * used by the search object.
+ * Note this is called with the state that caused the backtrack still being on
+ * the stack, so we have to remove that one first (i.e. popping two states
+ * and restoring the second one)
+ */
+ public boolean backtrack () {
+ transitionOccurred = false;
+
+ boolean success = backtracker.backtrack();
+ if (success) {
+ if (CHECK_CONSISTENCY) checkConsistency(false);
+
+ // restore the path
+ path.removeLast();
+ lastTrailInfo = path.getLast();
+
+ return true;
+
+ } else {
+ return false;
+ }
+ }
+
+ /**
+ * store the current SystemState's Trail in our path, after updating it
+ * with whatever annotations the VM wants to add.
+ * This is supposed to be called after each transition we want to keep
+ */
+ public void updatePath () {
+ Transition t = ss.getTrail();
+ Transition tLast = path.getLast();
+
+ // NOTE: don't add the transition twice, this is public and might get called
+ // from listeners, so the transition object might get changed
+
+ if (tLast != t) {
+ // <2do> we should probably store the output directly in the TrailInfo,
+ // but this might not be our only annotation in the future
+
+ // did we have output during the last transition? If yes, add it
+ if ((out != null) && (out.length() > 0)) {
+ t.setOutput( out.toString());
+ out.setLength(0);
+ }
+
+ path.add(t);
+ }
+ }
+
+ /**
+ * advance the program state
+ *
+ * forward() and backtrack() are the two primary interfaces towards the Search
+ * driver. note that the caller still has to check if there is a next state,
+ * and if the executed instruction sequence led into a new or already visited state
+ *
+ * @return 'true' if there was an un-executed sequence out of the current state,
+ * 'false' if it was completely explored
+ *
+ */
+ public boolean forward () {
+
+ // the reason we split up CG initialization and transition execution
+ // is that program state storage is not required if the CG initialization
+ // does not produce a new choice since we have to backtrack in that case
+ // anyways. This can be caused by complete enumeration of CGs and/or by
+ // CG listener intervention (i.e. not just after backtracking). For a large
+ // number of matched or end states and ignored transitions this can be a
+ // huge saving.
+ // The downside is that CG notifications are NOT allowed anymore to change the
+ // KernelState (modify fields or thread states) since those changes would
+ // happen before storing the KernelState, and hence would make backtracking
+ // inconsistent. This is advisable anyways since all program state changes
+ // should take place during transitions, but the real snag is that this
+ // cannot be easily enforced.
+
+ // actually, it hasn't occurred yet, but will
+ transitionOccurred = ss.initializeNextTransition(this);
+
+ if (transitionOccurred){
+ if (CHECK_CONSISTENCY) {
+ checkConsistency(true); // don't push an inconsistent state
+ }
+
+ backtracker.pushKernelState();
+
+ // cache this before we enter (and increment) the next insn(s)
+ lastTrailInfo = path.getLast();
+
+ try {
+ ss.executeNextTransition(vm);
+
+ } catch (UncaughtException e) {
+ // we don't pass this up since it means there were insns executed and we are
+ // in a consistent state
+ } // every other exception goes upwards
+
+ backtracker.pushSystemState();
+ updatePath();
+
+ if (!isIgnoredState()) {
+ // if this is ignored we are going to backtrack anyways
+ // matching states out of ignored transitions is also not a good idea
+ // because this transition is usually incomplete
+
+ if (runGc && !hasPendingException()) {
+ if(ss.gcIfNeeded()) {
+ processFinalizers();
+ }
+ }
+
+ if (stateSet != null) {
+ newStateId = stateSet.size();
+ int id = stateSet.addCurrent();
+ ss.setId(id);
+
+ } else { // this is 'state-less' model checking, i.e. we don't match states
+ ss.setId(++newStateId); // but we still should have states numbered in case listeners use the id
+ }
+ }
+
+ return true;
+
+ } else {
+
+ return false; // no transition occurred
+ }
+ }
+
+ /**
+ * Prints the current stack trace. Just for debugging purposes
+ */
+ public void printCurrentStackTrace () {
+ ThreadInfo th = ThreadInfo.getCurrentThread();
+
+ if (th != null) {
+ th.printStackTrace();
+ }
+ }
+
+
+ public void restoreState (RestorableVMState state) {
+ if (state.path == null) {
+ throw new JPFException("tried to restore partial VMState: " + state);
+ }
+ backtracker.restoreState(state.getBkState());
+ path = state.path.clone();
+ }
+
+ public void activateGC () {
+ ss.activateGC();
+ }
+
+
+ //--- various state attribute getters and setters (mostly forwarding to SystemState)
+
+ public void retainStateAttributes (boolean isRetained){
+ ss.retainAttributes(isRetained);
+ }
+
+ public void forceState () {
+ ss.setForced(true);
+ }
+
+ /**
+ * override the state matching - ignore this state, no matter if we changed
+ * the heap or stacks.
+ * use this with care, since it prunes whole search subtrees
+ */
+ public void ignoreState (boolean cond) {
+ ss.setIgnored(cond);
+ }
+
+ public void ignoreState(){
+ ignoreState(true);
+ }
+
+ /**
+ * imperatively break the transition to enable state matching
+ */
+ public void breakTransition (String reason) {
+ ThreadInfo ti = ThreadInfo.getCurrentThread();
+ ti.breakTransition(reason);
+ }
+
+ public boolean transitionOccurred(){
+ return transitionOccurred;
+ }
+
+ /**
+ * answers if the current state already has been visited. This is mainly
+ * used by the searches (to control backtracking), but could also be useful
+ * for observers to build up search graphs (based on the state ids)
+ *
+ * this returns true if no state has been produced yet, and false if
+ * no transition occurred after a forward call
+ */
+ public boolean isNewState() {
+
+ if (!transitionOccurred){
+ return false;
+ }
+
+ if (stateSet != null) {
+ if (ss.isForced()){
+ return true;
+ } else if (ss.isIgnored()){
+ return false;
+ } else {
+ return (newStateId == ss.getId());
+ }
+
+ } else { // stateless model checking - each transition leads to a new state
+ return true;
+ }
+ }
+
+ /**
+ * We made this to be overriden by Single/MultiprcessesVM implementations,
+ * since for MultiprcessesVM one can decide when to terminate (after the
+ * the termination of all processes or only one process).
+ * todo - that needs to be specified through the properties file
+ */
+ public abstract boolean isEndState ();
+
+ public boolean isVisitedState(){
+ return !isNewState();
+ }
+
+ public boolean isIgnoredState(){
+ return ss.isIgnored();
+ }
+
+ public boolean isInterestingState () {
+ return ss.isInteresting();
+ }
+
+ public boolean isBoringState () {
+ return ss.isBoring();
+ }
+
+ public boolean hasPendingException () {
+ return (getPendingException() != null);
+ }
+
+ public abstract boolean isDeadlocked ();
+
+ public Exception getException () {
+ return ss.getUncaughtException();
+ }
+
+
+
+ /**
+ * get the numeric id for the current state
+ * Note: this can be called several times (by the search and observers) for
+ * every forward()/backtrack(), so we want to cache things a bit
+ */
+ public int getStateId() {
+ return ss.getId();
+ }
+
+ public int getStateCount() {
+ return newStateId;
+ }
+
+
+ /**
+ * <2do> this is a band aid to bundle all these legacy reference chains
+ * from JPFs past. The goal is to replace them with proper accessors (normally
+ * through ThreadInfo, MJIEnv or VM, which all act as facades) wherever possible,
+ * and use VM.getVM() where there is no access to such a facade. Once this
+ * has been completed, we can start refactoring the users of VM.getVM() to
+ * get access to a suitable facade.
+ */
+ public static VM getVM () {
+ return vm;
+ }
+
+ /**
+ * not ideal to have this here since it is kind of a backlink, but it's not
+ * any better if listeners have to dig this out from JPF
+ * Note - this isn't set during initialization, since the VM object is created first
+ */
+ public Search getSearch() {
+ return jpf.getSearch();
+ }
+
+ /**
+ * pushClinit all our static fields. Called from <clinit> and reset
+ */
+ static void initStaticFields () {
+ error_id = 0;
+ }
+
+ /**
+ * given an object reference, it returns the ApplicationContext of the process to which
+ * this object belongs
+ */
+ public abstract ApplicationContext getCurrentApplicationContext();
+ public abstract ApplicationContext getApplicationContext(int objRef);
+ public abstract ApplicationContext[] getApplicationContexts();
+ public abstract String getSUTName();
+ public abstract String getSUTDescription();
+
+ public abstract int getNumberOfApplications();
+
+ public Heap getHeap() {
+ return ss.getHeap();
+ }
+
+ public ElementInfo getElementInfo(int objref){
+ return ss.getHeap().get(objref);
+ }
+
+ public ElementInfo getModifiableElementInfo(int objref){
+ return ss.getHeap().getModifiable(objref);
+ }
+
+
+ public ThreadInfo getCurrentThread () {
+ return ThreadInfo.currentThread;
+ }
+
+ public void registerClassLoader(ClassLoaderInfo cl) {
+ this.getKernelState().addClassLoader(cl);
+ }
+
+ public int registerThread (ThreadInfo ti){
+ getKernelState().changed();
+ return getThreadList().add(ti);
+ }
+
+ /**
+ * Returns the ClassLoader with the given globalId
+ */
+ protected ClassLoaderInfo getClassLoader(int gid) {
+ return ss.ks.getClassLoader(gid);
+ }
+
+ /**
+ * <2do> this is where we will hook in a better time model
+ */
+ public long currentTimeMillis () {
+ return timeModel.currentTimeMillis();
+ }
+
+ /**
+ * <2do> this is where we will hook in a better time model
+ */
+ public long nanoTime() {
+ return timeModel.nanoTime();
+ }
+
+ public void resetNextCG() {
+ if (ss.nextCg != null) {
+ ss.nextCg.reset();
+ }
+ }
+
+ /**
+ * only for debugging, this is expensive
+ *
+ * If this is a store (forward) this is called before the state is stored.
+ *
+ * If this is a restore (visited forward or backtrack), this is called after
+ * the state got restored
+ */
+ public void checkConsistency(boolean isStateStore) {
+ getThreadList().checkConsistency( isStateStore);
+ getHeap().checkConsistency( isStateStore);
+ }
+
+ public abstract void terminateProcess (ThreadInfo ti);
+
+ // this is invoked by the heap (see GenericHeap.newInternString()) upon creating
+ // the very first intern string
+ public abstract Map<Integer,IntTable<String>> getInitialInternStringsMap();
+
+ // ---------- Predicates used to query threads from ThreadList ---------- //
+
+ public abstract Predicate<ThreadInfo> getRunnablePredicate();
+
+ public abstract Predicate<ThreadInfo> getDaemonRunnablePredicate();
+
+ public abstract Predicate<ThreadInfo> getAppTimedoutRunnablePredicate();
+
+ public Predicate<ThreadInfo> getUserTimedoutRunnablePredicate () {
+ return userTimedoutRunnablePredicate;
+ }
+
+ public Predicate<ThreadInfo> getUserLiveNonDaemonPredicate() {
+ return userliveNonDaemonPredicate;
+ }
+
+ public Predicate<ThreadInfo> getTimedoutRunnablePredicate () {
+ return timedoutRunnablePredicate;
+ }
+
+ public Predicate<ThreadInfo> getAlivePredicate () {
+ return alivePredicate;
+ }
+
+
+ // ---------- Methods for handling finalizers ---------- //
+
+ public FinalizerThreadInfo getFinalizerThread() {
+ return getCurrentApplicationContext().getFinalizerThread();
+ }
+
+ abstract void updateFinalizerQueues();
+
+ public void processFinalizers() {
+ if(processFinalizers) {
+ updateFinalizerQueues();
+ ChoiceGenerator<?> cg = getNextChoiceGenerator();
+ if(cg==null || (cg.isSchedulingPoint() && !cg.isCascaded())) {
+ getFinalizerThread().scheduleFinalizer();
+ }
+ }
+ }
+}
projects / jpf-core.git / blobdiff