Java > Open Source Codes > gov > nasa > jpf > jvm > JVM


1 //
2 // Copyright (C) 2005 United States Government as represented by the
3 // Administrator of the National Aeronautics and Space Administration
4 // (NASA). All Rights Reserved.
5 //
6 // This software is distributed under the NASA Open Source Agreement
7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9 // directory tree for the complete NOSA document.
10 //
11 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18 //
19 package gov.nasa.jpf.jvm;
20
21 import gov.nasa.jpf.BootstrapXMLTraceHandler;
22 import gov.nasa.jpf.Config;
23 import gov.nasa.jpf.JPF;
24 import gov.nasa.jpf.JPFException;
25 import gov.nasa.jpf.Path;
26 import gov.nasa.jpf.Transition;
27 import gov.nasa.jpf.VM;
28 import gov.nasa.jpf.VMState;
29 import gov.nasa.jpf.VMListener;
30 import gov.nasa.jpf.VMListenerMulticaster;
31 import gov.nasa.jpf.util.CoverageManager;
32 import gov.nasa.jpf.util.Debug;
33
34 import java.io.File ;
35 import java.io.FileReader ;
36 import java.io.FileNotFoundException ;
37 import java.io.PrintWriter ;
38 import java.io.Reader ;
39 import java.io.Writer ;
40
41 import java.util.HashSet ;
42 import java.util.Stack ;
43 import java.util.StringTokenizer ;
44
45 import org.xml.sax.InputSource ;
46 import org.xml.sax.XMLReader ;
47 import org.xml.sax.helpers.XMLReaderFactory ;
48
49 import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
50 import gov.nasa.jpf.jvm.bytecode.Instruction;
51 import gov.nasa.jpf.jvm.choice.IntIntervalGenerator;
52
53
54 /**
55  * This class represents the virtual machine. The virtual machine is able to
56  * move backward and forward one transition at a time.
57  */
58 public class JVM implements VM {
59   
60   /**
61    * The number of errors saved so far.
62    * Used to generate the name of the error trail file.
63    */
64   protected static int error_id;
65     
66   /**
67    * Contains the list of the positions which are observable.
68    */
69   public static HashSet observablePositions;
70   
71   /**
72    * Contains the list of the labels which are observable.
73    */
74   public static HashSet observableLabels;
75   
76   /**
77    * Contains the list of invoke instructions which are observable.
78    */
79   public static HashSet observableInvokes;
80   
81   /**
82    * Contains the list of methods whose return instruction are observable.
83    */
84   public static HashSet observableReturns;
85     
86   /**
87    * <2do> - this is a hack to be removed once there are no static references
88    * anymore
89    */
90   protected static JVM jvm;
91   
92   static {
93     initStaticFields();
94   }
95   
96   protected SystemState ss;
97   
98   // <2do> - if you are confused about the various pieces of state and its
99 // storage/backtrack structures, I'm with you. It's mainly an attempt to
100 // separate non-policy VM state (objects), policy VM state (Scheduler)
101 // and general JPF execution state, with special support for stack oriented
102 // state restoration (backtracking).
103 // this needs to be cleaned up and the principle re-instantiated
104
105   /** where we keep the saved KernelState data */
106   protected Stack stateStoringStack;
107   
108   /** that's mostly JPFs execution context (atomicity etc.) */
109   protected Stack stateBacktrackStack;
110   
111   /** and that adds the SystemState specifics (Scheduler) */
112   protected Stack backtrackStack;
113   
114   protected String mainClassName;
115   protected String [] args; /** main() arguments */
116   
117   protected Path path; /** execution path to current state */
118   protected StringBuffer out; /** buffer to store output along path execution */
119   
120   /*
121    * we keep those state restoring caches around so that we don't have
122    * to duplicate them if somebody asks for the state. They are private because
123    * using them just makes sense after a forward() / backtrack(). Let's hope
124    * JPF never gets multithreaded
125    */
126   private int[] ksStoringData;
127   private Object ksBacktrackData;
128   
129   /** do we want to override state matching */
130   private boolean ignoreState;
131   
132   /**
133    * various caches for VMListener state acqusition. NOTE - these are only
134    * valid during notification
135    */
136   TrailInfo lastTrailInfo;
137   ClassInfo lastClassInfo;
138   ThreadInfo lastThreadInfo;
139   Instruction lastInstruction;
140   Instruction nextInstruction;
141   ElementInfo lastElementInfo;
142     
143   /** the repository we use to find out if we already have seen a state */
144   StateSet stateSet;
145   
146   /** potential execution listeners */
147   VMListener listener;
148   
149   Config config; // that's for the options we use only once
150
151   // JVM options we use frequently
152 boolean runGc;
153   boolean checkFP;
154   boolean checkFPcompare;
155   boolean atomicLines;
156   boolean treeOutput;
157   boolean pathOutput;
158   boolean indentOutput;
159   
160   /**
161    * VM instances are another example of evil throw-up ctors, but this is
162    * justified by the fact that they are only created via (configured)
163    * reflection from within the safe confines of the JPF ctor - which
164    * shields clients against blowups
165    */
166   public JVM (Config conf) throws Config.Exception {
167     // <2do> that's really a bad hack and should be removed once we
168 // have cleaned up the reference chains
169 jvm = this;
170     
171     config = conf;
172     
173     runGc = config.getBoolean("vm.gc", true);
174     checkFP = config.getBoolean("vm.check_fp", false);
175     checkFPcompare = config.getBoolean("vm.check_fp_compare", true);
176     atomicLines = config.getBoolean("vm.por.atomic_lines", true);
177     treeOutput = config.getBoolean("vm.tree_output", true);
178     pathOutput = config.getBoolean("vm.path_output", false);
179     indentOutput = config.getBoolean("vm.indent_output",false);
180
181     initSubsystems(config);
182     initFields(config);
183   }
184     
185   public void initFields (Config config) throws Config.Exception {
186     ClassInfo ci;
187
188     // the scheduler is just a local object because it is cloned/changed
189 // when restoring SystemStates
190 // <2do> this is likely to be changed when scheduling is moved over to
191 // external choice generators
192 Scheduler scheduler = null;
193     
194     // so that we can hash/store states
195 stateSet = (StateSet) config.getInstance("vm.storage.class", StateSet.class);
196
197     String target = config.getTargetArg();
198     
199     if (target.endsWith(".xml")) {
200       if ((new File (target)).exists()) {
201         // we are replaying a stored path
202 Path replay = loadPath(target);
203         mainClassName = replay.getApplication();
204         // if we replay a path, we have to use a PathScheduler no matter what
205 scheduler = new PathScheduler(replay);
206         Debug.println( Debug.MESSAGE, "replay path: " + target);
207       } else {
208         Debug.println( Debug.ERROR, "tracefile " + target + " not found, exiting");
209         JPF.exit();
210       }
211     } else {
212       mainClassName = target;
213       scheduler = (Scheduler) config.getEssentialInstance("vm.scheduler.class", Scheduler.class);
214     }
215     
216     args = config.getTargetArgParameters();
217             
218     stateStoringStack = new Stack ();
219     stateBacktrackStack = new Stack ();
220     backtrackStack = new Stack ();
221     path = new Path(mainClassName);
222     out = null;
223     
224     ss = new SystemState(config, scheduler);
225     
226     // <2do> - unify this with POR step boundaries
227 if (config.getBoolean("vm.visible_asserts")) {
228       addObservable("invoke.gov.nasa.jpf.jvm.Verify.assertTrue(Z)V");
229     }
230     
231     addListeners(config);
232   }
233     
234   void addListeners (Config config) throws Config.Exception {
235     Object [] listeners = config.getInstances("vm.listener", VMListener.class);
236     if (listeners != null) {
237       for (int i=0; i<listeners.length; i++) {
238         addListener( (VMListener) listeners[i]);
239       }
240     }
241   }
242   
243   void initSubsystems (Config config) throws Config.Exception {
244     ClassInfo.init(config);
245     ThreadInfo.init(config);
246     DynamicArea.init(config);
247     StaticArea.init(config);
248     NativePeer.init(config);
249     CoverageManager.init(config);
250     TrailInfo.init(config);
251     Step.init(config);
252     FieldInstruction.init(config);
253     JPF_gov_nasa_jpf_jvm_Verify.init(config);
254   }
255   
256   /**
257    * do we see our model classes? Some of them cannot be used from the standard CLASSPATH, because they
258    * are tightly coupled with the JPF core (e.g. java.lang.Class, java.lang.Thread,
259    * java.lang.StackTraceElement etc.)
260    * Our strategy here is kind of lame - we just look into java.lang.Class, if we find the 'int cref' field
261    * (that's a true '42')
262    */
263   static boolean checkModelClassAccess () {
264     ClassInfo ci = ClassInfo.getClassInfo("java.lang.Class");
265     return (ci.getDeclaredInstanceField("cref") != null);
266   }
267
268   
269   /**
270    * load and initialize startup classes, return 'true' if successful.
271    *
272    * This loads a bunch of core library classes, initializes the main thread,
273    * and then all the required startup classes, but excludes the static init of
274    * the main class. Note that whatever gets executed in here should NOT contain
275    * any non-determinism, since we are not backtrackable yet, i.e.
276    * non-determinism in clinits should be constrained to the app class (and
277    * classes used by it)
278    */
279   public boolean initialize () {
280     // from here, we get into some bootstrapping process
281 // - first, we have to load class structures (fields, supers, interfaces..)
282 // - second, we have to create a thread (so that we have a stack)
283 // - third, we have to execute the clinit methods on this stack
284 // create static fields and monitor for system classes and app entry
285 loadStartupClasses();
286     
287     if (!checkModelClassAccess()) {
288       Debug.println(Debug.ERROR,
289             "error during VM runtime initialization: wrong model classes (check vm.[boot]classpath)");
290       return false;
291     }
292     
293     // create the thread for the main class
294 // note this is incomplete for Java 1.3 where Thread ctors rely on main's
295 // 'inheritableThreadLocals' being set to 'Collections.EMPTY_SET', which
296 // pulls in the whole Collections/Random smash, but we can't execute the
297 // Collections.<clinit> yet because there's no stack before we have a main
298 // thread. Let's hope none of the init classes creates threads in their <clinit>.
299 createMainThread();
300     
301     try {
302       // initializes the classes loaded
303 // this mainly makes sure the <clinit> methods get called, which is not
304 // possible before we have a thread stack.
305 // Note - this does not include the main class clinit (or any of its
306 // superclasses), since that has to be done from forward (i.e. backtrackable)
307 initializeStartupClasses();
308       
309       // those are the actions (in reverse order) we are taking next. Reverse,
310 // because they are initiated via the stack
311 prepareMain(config);
312       prepareMainClinit(config);
313     } catch (UncaughtException ux) {
314       // <2do> hmm - we really should handle UncaughtExceptions consistently
315 Debug.println(Debug.ERROR, "error during VM runtime initialization:");
316       Debug.println(Debug.ERROR, ux);
317       return false;
318     }
319     
320     return true;
321   }
322   
323   public void addListener (VMListener newListener) {
324     listener = VMListenerMulticaster.add(listener, newListener);
325   }
326
327   public void removeListener (VMListener removeListener) {
328     listener = VMListenerMulticaster.remove(listener,removeListener);
329   }
330   
331   void notifyInstructionExecuted (ThreadInfo ti, Instruction insn, Instruction nextInsn) {
332     lastThreadInfo = ti;
333     lastInstruction = insn;
334     nextInstruction = nextInsn;
335     if (listener != null) {
336       listener.instructionExecuted(this);
337     }
338     nextInstruction = null;
339     lastInstruction = null;
340     lastThreadInfo = null;
341   }
342   
343   void notifyThreadStarted (ThreadInfo ti) {
344     lastThreadInfo = ti;
345     if (listener != null) {
346       listener.threadStarted(this);
347     }
348     lastThreadInfo = null;
349   }
350   
351   void notifyThreadTerminated (ThreadInfo ti) {
352     lastThreadInfo = ti;
353     if (listener != null) {
354       listener.threadTerminated(this);
355     }
356     lastThreadInfo = null;
357   }
358   
359   void notifyClassLoaded (ClassInfo ci) {
360     lastClassInfo = ci;
361     if (listener != null) {
362       listener.classLoaded(this);
363     }
364     lastClassInfo = null;
365   }
366   
367   void notifyObjectCreated (ThreadInfo ti, ElementInfo ei) {
368     lastThreadInfo = ti;
369     lastElementInfo = ei;
370     if (listener != null) {
371       listener.objectCreated(this);
372     }
373     lastElementInfo = null;
374     lastThreadInfo = null;
375   }
376   
377   void notifyObjectReleased (ElementInfo ei) {
378     lastElementInfo = ei;
379     if (listener != null) {
380       listener.objectReleased(this);
381     }
382     lastElementInfo = null;
383   }
384   
385   void notifyGCBegin () {
386     if (listener != null) {
387       listener.gcBegin(this);
388     }
389   }
390   
391   void notifyGCEnd () {
392     if (listener != null) {
393       listener.gcEnd(this);
394     }
395   }
396   
397   void notifyExceptionThrown (ThreadInfo ti, ElementInfo ei) {
398     lastThreadInfo = ti;
399     lastElementInfo = ei;
400     if (listener != null) {
401       listener.exceptionThrown(this);
402     }
403     lastElementInfo = null;
404     lastThreadInfo = null;
405   }
406   
407   // VMListener acquisition
408 public int getThreadNumber () {
409     if (lastThreadInfo != null) {
410       return lastThreadInfo.getIndex();
411     } else {
412       return -1;
413     }
414   }
415   
416   // VMListener acquisition
417 public String getThreadName () {
418     ThreadInfo ti = ss.getRunningThread();
419     
420     return ti.getName();
421   }
422   
423   // VMListener acquisition
424 Instruction getInstruction () {
425     ThreadInfo ti = ss.getRunningThread();
426     return ti.getPC();
427   }
428
429   
430   public int getAbstractionNonDeterministicThreadCount () {
431     int n = 0;
432     int imax = ss.getThreadCount();
433     
434     for (int i = 0; i < imax; i++) {
435       ThreadInfo th = ss.getThreadInfo(i);
436       
437       if (th.isAbstractionNonDeterministic()) {
438         n++;
439       }
440     }
441     
442     return n;
443   }
444   
445   public int getAliveThreadCount () {
446     int n = 0;
447     int imax = ss.getThreadCount();
448     
449     for (int i = 0; i < imax; i++) {
450       ThreadInfo th = ss.getThreadInfo(i);
451       
452       if (th.isAlive()) {
453         n++;
454       }
455     }
456     
457     return n;
458   }
459   
460   public ExceptionInfo getPendingException () {
461     return ThreadInfo.current.getPendingException();
462   }
463   
464   public boolean isBoringState () {
465     return ss.getBoring();
466   }
467   
468   public Reference getClassReference (String name) {
469     if (ClassInfo.exists(name)) {
470       return ss.ks.sa.get(name);
471     }
472     
473     return null;
474   }
475   
476   public boolean hasPendingException () {
477     return (ThreadInfo.current.pendingException != null);
478   }
479   
480   public boolean isDeadlocked () {
481     int length = ss.getThreadCount();
482     boolean result = false;
483     
484     for (int i = 0; i < length; i++) {
485       ThreadInfo th = (ThreadInfo) ss.getThreadInfo(i);
486       
487       // if there's at least one runnable, we are not deadlocked
488 if (th.isRunnable()) {
489         return false;
490       }
491       
492       // if stack depth is 0, it's done
493 // otherwise we have a deadlock if we don't find any runnable
494 if (th.countStackFrames() != 0) {
495         result = true;
496       }
497     }
498     
499     return result;
500   }
501   
502   public boolean isEndState () {
503     // note this uses 'alive', not 'runnable', hence isEndStateProperty won't
504 // catch deadlocks - but that would be NoDeadlockProperty anyway
505 return ss.isEndState();
506   }
507   
508   public Exception getException () {
509     return ss.getUncaughtException();
510   }
511   
512   public boolean isInterestingState () {
513     return ss.getInteresting();
514   }
515     
516   public Step getLastStep () {
517     TrailInfo trail = ss.trail();
518     if (trail != null) {
519       return trail.getLastStep();
520     }
521     
522     return null;
523   }
524   
525   public Transition getLastTransition () {
526     if (path.length() == 0) {
527       return null;
528     }
529     return path.get(path.length() - 1);
530   }
531   
532   /**
533    * answer the ClassInfo that was loaded most recently
534    * part of the VMListener state acqusition (only valid from inside of
535    * notification)
536    */
537   public ClassInfo getLastClassInfo () {
538     return lastClassInfo;
539   }
540   
541   /**
542    * answer the ThreadInfo that was most recently started or finished
543    * part of the VMListener state acqusition (only valid from inside of
544    * notification)
545    */
546   public ThreadInfo getLastThreadInfo () {
547     return lastThreadInfo;
548   }
549   
550   /**
551    * answer the last executed Instruction
552    * part of the VMListener state acqusition (only valid from inside of
553    * notification)
554    */
555   public Instruction getLastInstruction () {
556     return lastInstruction;
557   }
558   
559   /**
560    * answer the next Instruction to execute in the current thread
561    * part of the VMListener state acqusition (only valid from inside of
562    * notification)
563    */
564   public Instruction getNextInstruction () {
565     return nextInstruction;
566   }
567   
568   /**
569    * answer the Object that was most recently created or collected
570    * part of the VMListener state acqusition (only valid from inside of
571    * notification)
572    */
573   public ElementInfo getLastElementInfo () {
574     return lastElementInfo;
575   }
576   
577   /**
578    * answer the ClassInfo that was loaded most recently
579    * part of the VMListener state acqusition
580    */
581   public ClassInfo getClassInfo () {
582     return lastClassInfo;
583   }
584   
585   public String getMainClassName () {
586     return mainClassName;
587   }
588   
589   public String [] getArgs () {
590     return args;
591   }
592   
593   public void setPath (Path p) {
594   }
595   
596   public Path getPath () {
597     return (Path) path.clone();
598   }
599   
600   public int getPathLength () {
601     return path.length();
602   }
603   
604   public Reference getReference (String name) {
605     // first of all I have to get to a class
606 StringTokenizer st = new StringTokenizer (name, ".");
607     StringBuffer sb = new StringBuffer ();
608     Reference r = null;
609     
610     while (st.hasMoreTokens()) {
611       sb.append(st.nextToken());
612       
613       if ((r = getClassReference(sb.toString())) != null) {
614         break;
615       }
616       
617       sb.append('.');
618     }
619     
620     if (r == null) {
621       throw new JPFException("invalid argument: " + name);
622     }
623     
624     // now walk thought the fields
625 while (st.hasMoreTokens()) {
626       r = r.getObjectField(st.nextToken(), sb.toString());
627     }
628     
629     return r;
630   }
631   
632   public VMState getRestorableForwardState () {
633     JVMState state = new JVMState();
634     state.makeForwardRestorable();
635     
636     return state;
637   }
638   
639   public int getRunnableThreadCount () {
640     return ss.getRunnableThreadCount();
641   }
642     
643   public boolean checkFP () {
644     return checkFP;
645   }
646   
647   public boolean checkNaN (double r) {
648     if (checkFP) {
649       return !(Double.isNaN(r) || Double.isInfinite(r));
650     } else {
651       return true;
652     }
653   }
654   
655   public boolean checkNaN (float r) {
656     if (checkFP) {
657       return !(Float.isNaN(r) || Float.isInfinite(r));
658     } else {
659       return true;
660     }
661   }
662   
663   public boolean checkNaNcompare (float r1, float r2) {
664     if (checkFPcompare) {
665       return !(Float.isNaN(r1) || Float.isNaN(r2) ||
666         (Float.isInfinite(r1) && Float.isInfinite(r2) && (r1 == r2)));
667     } else {
668       return true;
669     }
670   }
671   
672   public boolean checkNaNcompare (double r1, double r2) {
673     if (checkFPcompare) {
674       return !(Double.isNaN(r1) || Double.isNaN(r2) ||
675         (Double.isInfinite(r1) && Double.isInfinite(r2) && (r1 == r2)));
676     } else {
677       return true;
678     }
679   }
680   
681   /**
682    * Bundles up the state of the system for export
683    */
684   public VMState getState () {
685     return (new JVMState());
686   }
687   
688   /**
689    * Gets the system state.
690    */
691   public SystemState getSystemState () {
692     return ss;
693   }
694   
695   public KernelState getKernelState () {
696     return ss.ks;
697   }
698   
699   /**
700    * return the current SystemState's ChoiceGenerator object
701    */
702   public ChoiceGenerator getChoiceGenerator () {
703     return ss.getChoiceGenerator();
704   }
705
706   ///// <2do> that's probably not going to stay here - ChoiceGenerator creation will be revamped
707
708   // our const ChoiceGenerator ctor argtypes
709 protected final Class [] cgArgTypes = { Config.class, String .class };
710   // this is our cache for ChoiceGenerator ctor parameters
711 protected Object [] cgArgs = { null, null };
712   
713   // the built-in ones (boolean and int)
714 public BooleanChoiceGenerator createBooleanChoiceGenerator () {
715     BooleanChoiceGenerator gen = new BooleanChoiceGenerator(config, "boolean");
716     gen.advance(this); // that's not going to stay here
717 ss.setChoiceGenerator(gen);
718     return gen;
719   }
720
721   public IntChoiceGenerator createIntChoiceGenerator (int min, int max) {
722     IntIntervalGenerator gen = new IntIntervalGenerator(min,max);
723     gen.advance(this); // that's not going to stay here
724 ss.setChoiceGenerator(gen);
725     return gen;
726   }
727   
728   // the generic one
729 public ChoiceGenerator createChoiceGenerator (String id) {
730     ChoiceGenerator gen = null;
731     
732     cgArgs[0] = config;
733     cgArgs[1] = id; // good thing we are not multithreaded (other fields are const)
734
735     try {
736       String key = id + ".class";
737       gen = (ChoiceGenerator)config.getEssentialInstance(key, ChoiceGenerator.class,
738                                                          cgArgTypes, cgArgs);
739       gen.advance(this); // that's not going to stay here
740 ss.setChoiceGenerator(gen);
741     } catch (Config.Exception cex) {
742       // bail, nothing we can do to cover up
743 throw new JPFException(cex);
744     }
745
746     return gen;
747   }
748   
749   
750   public boolean isTerminated () {
751     return ss.ks.isTerminated();
752   }
753   
754   public void print (String s) {
755     if (treeOutput) {
756       System.out.print(s);
757     }
758     
759     if (pathOutput) {
760       appendOutput(s);
761     }
762   }
763
764   public void println (String s) {
765     if (treeOutput) {
766       if (indentOutput){
767         StringBuffer indent = new StringBuffer ();
768         int i;
769         for (i = 0;i<=path.length();i++) {
770           indent.append("|" + i);
771         }
772         System.out.println(indent + "|" +s);
773       }
774       else {
775         System.out.println(s);
776       }
777     }
778     
779     if (pathOutput) {
780       appendOutput(s);
781       appendOutput('\n');
782     }
783   }
784
785   public void print (boolean b) {
786     if (treeOutput) {
787       System.out.print(b);
788     }
789     
790     if (pathOutput) {
791       appendOutput(Boolean.toString(b));
792     }
793   }
794   
795   public void print (char c) {
796     if (treeOutput) {
797       System.out.print(c);
798     }
799     
800     if (pathOutput) {
801       appendOutput(c);
802     }
803   }
804   
805   public void print (int i) {
806     if (treeOutput) {
807       System.out.print(i);
808     }
809     
810     if (pathOutput) {
811       appendOutput(Integer.toString(i));
812     }
813   }
814
815   public void print (long l) {
816     if (treeOutput) {
817       System.out.print(l);
818     }
819     
820     if (pathOutput) {
821       appendOutput(Long.toString(l));
822     }
823   }
824
825   public void print (double d) {
826     if (treeOutput) {
827       System.out.print(d);
828     }
829     
830     if (pathOutput) {
831       appendOutput(Double.toString(d));
832     }
833   }
834
835   public void print (float f) {
836     if (treeOutput) {
837       System.out.print(f);
838     }
839     
840     if (pathOutput) {
841       appendOutput(Float.toString(f));
842     }
843   }
844
845   public void println () {
846     if (treeOutput) {
847       System.out.println();
848     }
849     
850     if (pathOutput) {
851       appendOutput('\n');
852     }
853   }
854
855   
856   void appendOutput (String s) {
857     if (out == null) {
858       out = new StringBuffer ();
859     }
860     out.append(s);
861   }
862   
863   void appendOutput (char c) {
864     if (out == null) {
865       out = new StringBuffer ();
866     }
867     out.append(c);
868   }
869   
870   /**
871    * JVM specific results
872    */
873   public void printResults (PrintWriter pw) {
874     if (config.getBoolean("vm.report.printStacks")) {
875       pw.println("------------------------------------ thread stacks");
876       printStackTraces(pw);
877       pw.println("------------------------------------ end thread stacks");
878     }
879   }
880   
881   public void printStackTraces (PrintWriter pw) {
882     int imax = ss.getThreadCount();
883     
884     for (int i = 0; i < imax; i++) {
885       ThreadInfo ti = ss.getThreadInfo(i);
886       String [] cs = ti.getCallStack();
887       
888       if (cs.length > 0) {
889         pw.print("Thread: ");
890         pw.println(ti.getName());
891         for (int j=cs.length-1; j >= 0; j--) {
892           pw.println(cs[j]);
893         }
894         pw.println();
895       }
896     }
897   }
898   
899   void backtrackKernelState () {
900     ksStoringData = (int[]) stateStoringStack.pop();
901     ksBacktrackData = stateBacktrackStack.pop();
902     
903     ss.ks.backtrackTo(new ArrayOffset(ksStoringData), ksBacktrackData);
904   }
905   
906   void backtrackSystemState () {
907     ss.backtrackTo(null, backtrackStack.pop());
908   }
909   
910   /**
911    * Moves one step backward. This method and forward() are the main methods
912    * used by the search object.
913    * Note this is called with the state that caused the backtrack still being on
914    * the stack, so we have to remove that one first (i.e. popping two states
915    * and restoring the second one)
916    */
917   public boolean backtrack () {
918     if (!backtrackStack.isEmpty()) {
919       // restore the KernelState
920 backtrackKernelState();
921       
922       // restore the SystemState
923 backtrackSystemState();
924       
925       // restore the path
926 path.removeLast();
927       lastTrailInfo = (TrailInfo) path.getLast();
928       
929       return ((ss.getId() != StateSet.UNKNOWN_ID) || (stateSet == null));
930     } else {
931       return false;
932     }
933   }
934   
935   private void cacheKernelState () {
936     ksStoringData = ss.ks.getStoringData();
937     ksBacktrackData = ss.ks.getBacktrackData();
938   }
939   
940   private void resetKernelStateCache () {
941     ksStoringData = null;
942     ksBacktrackData = null;
943   }
944   
945   private boolean tryAgain () {
946     backtrackKernelState();
947     ss.scheduleNext(this);
948     
949     // <2do> pcm - no prepareNext here (scheduler resetting?)
950 return forward();
951   }
952   
953   /**
954    * store the current SystemState's TrainInfo in our path, after updating it
955    * with whatever annotations the JVM wants to add.
956    * This is supposed to be called after each transition we want to keep
957    */
958   void updatePath () {
959     Transition t = ss.trail();
960     
961     // <2do> we should probably store the output directly in the TrailInfo,
962 // but this might not be our only annotation in the future
963
964     // did we have output during the last transition? If yes, add it
965 if ((out != null) && (out.length() > 0)) {
966       t.setOutput( out.toString());
967       out.setLength(0);
968     }
969     
970     path.add(t);
971   }
972   
973   /**
974    * try to advance the state
975    * forward() and backtrack() are the two primary interfaces towards the Search
976    * driver
977    * return 'true' if there was an un-executed sequence out of the current state,
978    * 'false' if it was completely explored
979    * note that the caller still has to check if there is a next state, and if
980    * the executed instruction sequence led into a new or already visited state
981    */
982   public boolean forward () {
983     boolean isNewState = true;
984     ignoreState = false;
985     
986     try {
987       // saves the current state for backtracking purposes of depth first
988 // searches and state observers. If there is a previously cached
989 // kernelstate, use that one
990 pushKernelState();
991       
992       // cache this before we execute (and increment) the next insn(s)
993 lastTrailInfo = (TrailInfo) path.getLast();
994       
995       // execute the instruction(s) to get to the next state
996 // this changes the SystemState (e.g. finds the next thread to run)
997 if (ss.nextSuccessor(this)) {
998         // runs the garbage collector (if necessary), which might change the
999 // KernelState (DynamicArea)
1000 // we need to do this before we hash the state to find out if it is
1001 // a new one
1002 // Note that we don't collect if there is a pending exception, since
1003 // we want to preserve as much state as possible for debug purposes
1004 if (runGc && !hasPendingException()) {
1005          ss.gcIfNeeded();
1006        }
1007        
1008        // moves the scheduler to the next position, which changes the SystemState
1009 ss.scheduleNext(this);
1010        
1011        // might change backtrack info due to SystemState checks
1012 ss.checkNext(this);
1013        
1014        // saves the backtrack information. Unfortunately, we cannot cache
1015 // this (except of the optional lock graph) because it is changed
1016 // by the subsequent operations (before we return from forward)
1017 pushSystemState();
1018                
1019        updatePath();
1020        
1021        // get ready for the next round (resets Scheduler)
1022 ss.prepareNext(this);
1023        
1024      } else { // state was completely explored, no transition ocurred
1025 popKernelState();
1026        return false;
1027      }
1028      
1029    } catch (BlockedAtomicException e) { // <2do> bad control flow
1030 return tryAgain();
1031    } catch (IgnoreIfException e) { // <2do> bad control flow
1032 return tryAgain();
1033// } catch (JPFException e) {
1034// throw e;
1035 } catch (UncaughtException e) {
1036      updatePath(); // or we loose the last transition
1037 // something blew up, so we definitely executed something (hence return true)
1038 return true;
1039    } catch (RuntimeException e) {
1040      throw new JPFException(e);
1041    }
1042    
1043    if (stateSet != null) {
1044      int id = stateSet.add(ss);
1045      ss.setId(id);
1046      isNewState = stateSet.isNewState(id);
1047    }
1048    
1049    // the idea is that search objects or observers can query the state
1050 // *after* forward/backtrack was called, and that all changes of the
1051 // System/KernelStates happen from *within* forward/backtrack, i.e. the
1052 // (expensive) getBacktrack/storingData operations can be cached and used
1053 // w/o re-computation in the next forward pushXState()
1054 cacheKernelState(); // for subsequent getState() and the next forward()
1055
1056    return true;
1057  }
1058  
1059  /**
1060   * load a previously stored path from a file
1061   * <2do> should be simplified to use the JVMXMLTraceHandler (no use to
1062   * have different trace formats for the same VM)
1063   */
1064  public Path loadPath (String fname) {
1065    try {
1066      Reader r = new FileReader (fname);
1067
1068      XMLReader parser = XMLReaderFactory.createXMLReader(
1069                                              "org.apache.xerces.parsers.SAXParser");
1070      BootstrapXMLTraceHandler handler = new BootstrapXMLTraceHandler();
1071      parser.setContentHandler(handler);
1072      parser.parse(new InputSource (r));
1073
1074      return handler.getPath();
1075    } catch (FileNotFoundException e) {
1076      throw new JPFException(fname + ": file not found");
1077    } catch (Throwable x) {
1078      throw new JPFException("cannot load path " + fname + " : " + x);
1079    }
1080  }
1081    
1082  public void popKernelState () {
1083    stateStoringStack.pop();
1084    stateBacktrackStack.pop();
1085  }
1086  
1087  public void printStatus () {
1088    Debug.println(Debug.ERROR, "Current status of the virtual machine:");
1089    printCurrentStackTrace();
1090    
1091    //if (options.print_errors) {
1092 Debug.println(Debug.ERROR, "Current execution path:");
1093      Debug.println(Debug.ERROR, getPath());
1094    //}
1095 }
1096  
1097  /**
1098   * Prints the current stack trace.
1099   */
1100  public void printCurrentStackTrace () {
1101    ThreadInfo th = ss.getRunningThread();
1102    
1103    if (th != null) {
1104      th.printStackTrace();
1105    }
1106  }
1107      
1108  /**
1109   * Saves the state of the system.
1110   */
1111  public void pushKernelState () {
1112    int[] ksSD;
1113    
1114    // do we need to recompute the cache?
1115 if (ksStoringData == null) {
1116      ksSD = ss.ks.getStoringData();
1117    } else {
1118      ksSD = ksStoringData;
1119    }
1120    
1121    stateStoringStack.push(ksSD);
1122    
1123    Object ksBD;
1124    
1125    if (ksBacktrackData == null) {
1126      ksBD = ss.ks.getBacktrackData();
1127    } else {
1128      ksBD = ksBacktrackData;
1129    }
1130    
1131    stateBacktrackStack.push(ksBD);
1132  }
1133  
1134  /**
1135   * Saves the backtracking information.
1136   */
1137  public void pushSystemState () {
1138    Object ssBD = ss.getBacktrackData();
1139    backtrackStack.push(ssBD);
1140  }
1141    
1142  public void restoreState (VMState st) {
1143    if (st instanceof JVMState) {
1144      JVMState state = (JVMState) st;
1145      
1146      if (state.path == null) {
1147        throw new JPFException("tried to restore partial VMState: " + st);
1148      }
1149      
1150      // NOTE - we have to clone all restored objects that are modified by
1151 // subsequent forward/backtrack operations, since they might be stored
1152 // globally, and used to reset to the same state several times
1153
1154      // NOTE ALSO - be aware of that the state might not have been obtained without
1155 // calling makeRestorable(), in which case the following fields would not
1156 // be initialized, and backtracking would not work
1157 // see VMState
1158 stateStoringStack = (state.stateStoringStack != null) ?
1159        (Stack )state.stateStoringStack.clone() : new Stack ();
1160      stateBacktrackStack = (state.stateBacktrackStack != null) ?
1161        (Stack )state.stateBacktrackStack.clone() : new Stack ();
1162      backtrackStack = (state.backtrackStack != null) ?
1163        (Stack )state.backtrackStack.clone() : new Stack ();
1164      
1165      // we are going to restore the system state via backtracking, so there's
1166 // no need to give it a scheduler here
1167 //ss = SystemState.newInstance((Scheduler) null);
1168
1169      ksStoringData = state.ksStoringData;
1170      ksBacktrackData = state.ksBacktrackData;
1171      
1172      ss.ks.backtrackTo(new ArrayOffset(ksStoringData), ksBacktrackData);
1173      ss.backtrackTo(null, state.ssBacktrackData);
1174      
1175      path = (Path)state.path.clone();
1176    } else {
1177      throw new JPFException("tried to restore illegal VMState: " + st);
1178    }
1179  }
1180  
1181  public void rewind () {
1182    ss.sch.initialize();
1183  }
1184  
1185  public void savePath (Path path, Writer w) {
1186    PrintWriter out = new PrintWriter (w);
1187    int length = path.length();
1188    
1189    TrailInfo.toXML(out, path);
1190  }
1191  
1192  /**
1193   * override the state matching - ignore this state, no matter if we changed
1194   * the heap or stacks.
1195   * use this with care, since it prunes whole search subtrees
1196   */
1197  public void setIgnoreState (boolean b) {
1198    ignoreState = b;
1199  }
1200  
1201  /**
1202   * answers if the current state already has been visited. This is mainly
1203   * used by the searches (to control backtracking), but could also be useful
1204   * for observers to build up search graphs (based on the state ids)
1205   */
1206  public boolean isNewState() {
1207    if (stateSet != null) {
1208      if (ignoreState){
1209        return false;
1210      } else {
1211        return stateSet.isNewState(ss.getId());
1212      }
1213    } else {
1214      return true;
1215    }
1216  }
1217  
1218  /**
1219   * get the numeric id for the current state
1220   * Note: this can be called several times (by the search and observers) for
1221   * every forward()/backtrack(), so we want to cache things a bit
1222   */
1223  public int getStateId() {
1224    return ss.getId();
1225  }
1226  
1227  // <2do> this will be obsolete at some point (too close to POR)
1228 public void addObservable (String observable) {
1229    if (observable.startsWith("invoke.")) {
1230      synchronized (observableInvokes) {
1231        observableInvokes.add(observable.substring(7));
1232      }
1233    } else if (observable.startsWith("return.")) {
1234      synchronized (observableReturns) {
1235        observableReturns.add(observable.substring(7));
1236      }
1237    } else if (observable.startsWith("position.")) {
1238      synchronized (observablePositions) {
1239        observablePositions.add(observable.substring(9));
1240      }
1241    } else if (observable.startsWith("label.")) {
1242      synchronized (observableLabels) {
1243        observableLabels.add(observable.substring(6));
1244      }
1245    } else {
1246      Debug.println(Debug.ERROR, "Unknown observable: " + observable);
1247    }
1248  }
1249  
1250  /**
1251   * be careful - everything that's executed from within here is not allowed
1252   * to depend on static class init having been done yet
1253   */
1254  protected ThreadInfo createMainThread () {
1255    ElementInfo ei;
1256    DynamicArea da = ss.ks.da;
1257    
1258    // first we need a group for this baby (happens to be called "main")
1259 int grpObjref = da.newObject(ClassInfo.getClassInfo("java.lang.ThreadGroup"),
1260                                 null);
1261    
1262    // since we can't call methods yet, we have to init explicitly (BAD)
1263 int grpName = da.newString("main", null);
1264    ei = da.get(grpObjref);
1265    ei.setReferenceField("name", grpName);
1266    ei.setIntField("maxPriority", java.lang.Thread.MAX_PRIORITY);
1267    
1268    int tObjref = da.newObject(ClassInfo.getClassInfo("java.lang.Thread"), null);
1269    
1270    ei = da.get(tObjref);
1271    ei.setReferenceField("group", grpObjref);
1272    ei.setReferenceField("name", da.newString("main", null));
1273    ei.setIntField("priority", Thread.NORM_PRIORITY);
1274    
1275    // we need to keep the attributes on the JPF side in sync here
1276 // <2do> factor out the Thread/ThreadInfo creation so that it's less
1277 // error prone (even so this is the only location it's required for)
1278 ThreadInfo ti = new ThreadInfo( this, tObjref);
1279    ti.setPriority(java.lang.Thread.NORM_PRIORITY);
1280    ti.setName("main");
1281    ti.setStatus(ThreadInfo.RUNNING);
1282    ss.ks.addThread(ti); // <2do> get rid of this ref chain
1283
1284    return ti;
1285  }
1286  
1287  public ThreadInfo createThread (int objRef) {
1288    ThreadInfo ti = new ThreadInfo( this, objRef);
1289    ss.ks.addThread(ti); // <2do> get rid of this ref chain
1290 return ti;
1291  }
1292  
1293  void prepareMainClinit(Config config) {
1294    StaticArea sa = getStaticArea();
1295    ClassInfo ci = ClassInfo.getClassInfo(mainClassName);
1296    
1297    // note we have to push the stackframes in reverse execution order
1298 // (i.e. MDC first), since we start to execute from the stack top
1299 while (!sa.containsClass(ci.getName())) {
1300      // make sure the thing is registered, but not yet initialized
1301 sa.newUninitializedClass(ci);
1302      
1303      MethodInfo mi = ci.getMethod("<clinit>()", false);
1304      ThreadInfo ti = ss.getThreadInfo(0);
1305      
1306      if (mi != null) {
1307        StackFrame frame = null;
1308        // might be MJI, in which case we have to create the code and the stackframe
1309 if (mi.isMJI()) {
1310          mi = mi.createNativeCallStub();
1311          frame = new StackFrame(mi, true, null);
1312          frame.push(ci.getClassObjectRef(), true);
1313        } else {
1314          frame = new StackFrame(mi, true, null);
1315        }
1316        
1317        if (config.getBoolean("vm.atomic_init")) {
1318          mi.setAtomic(true);
1319        }
1320        
1321        ti.pushFrame(frame);
1322      }
1323      
1324      ci = ci.getSuperClass();
1325    }
1326  }
1327  
1328  void prepareMain (Config config) {
1329    DynamicArea da = ss.ks.da;
1330    ClassInfo ci = ClassInfo.getClassInfo(mainClassName);
1331    MethodInfo mi = ci.getMethod("main([Ljava/lang/String;)", false);
1332    ThreadInfo ti = ss.getThreadInfo(0);
1333    
1334    if (mi == null) {
1335      throw new JPFException("no main() method in " + ci.getName());
1336    }
1337    
1338    ti.pushFrame(new StackFrame(mi, false, null));
1339    ti.setStatus(ThreadInfo.RUNNING);
1340    
1341    int argsObjref = da.newArray("Ljava/lang/String;", args.length, null);
1342    ElementInfo argsElement = ss.ks.da.get(argsObjref);
1343    
1344    for (int i = 0; i < args.length; i++) {
1345      int stringObjref = da.newString(args[i], null);
1346      argsElement.setElement(i, stringObjref);
1347    }
1348    ti.setLocalVariable(0, argsObjref, true);
1349  }
1350  
1351  protected void loadStartupClasses () {
1352    String [] classes = {
1353      "java.lang.Object",
1354        "java.lang.Class",
1355        "java.lang.String",
1356        "java.lang.ThreadGroup",
1357        "java.lang.Thread",
1358        "java.io.PrintStream",
1359        "java.lang.System",
1360        "gov.nasa.jpf.jvm.Verify",
1361        "byte", "[B",
1362        "char", "[C",
1363        "int", "[I",
1364        "long", "[J"
1365    };
1366    
1367    for (int i=0; i<classes.length; i++) {
1368      ClassInfo ci = ClassInfo.getClassInfo(classes[i]);
1369      ss.ks.sa.newStartupClass(ci);
1370    }
1371  }
1372  
1373  protected void initializeStartupClasses () {
1374    ss.ks.sa.initializeClasses();
1375  }
1376  
1377  protected void loadClass (ClassInfo ci) {
1378    StaticArea sa = getStaticArea();
1379    if (!sa.containsClass(ci.getName())) {
1380            sa.newClass(ci);
1381    }
1382  }
1383  
1384  static JVM getVM () {
1385    // <2do> remove this, no more static refs!
1386 return jvm;
1387  }
1388  
1389  /**
1390   * initialize all our static fields. Called from <clinit> and reset
1391   */
1392  static void initStaticFields () {
1393    error_id = 0;
1394    observableInvokes = new HashSet ();
1395    observableLabels = new HashSet ();
1396    observablePositions = new HashSet ();
1397    observableReturns = new HashSet ();
1398  }
1399  
1400  /**
1401   * return the 'heap' object, which is a global service
1402   */
1403  public DynamicArea getDynamicArea () {
1404    return ss.ks.da;
1405  }
1406    
1407  /**
1408   * same for "loaded classes", but be advised it will probably go away at some point
1409   */
1410  StaticArea getStaticArea () {
1411    return ss.ks.sa;
1412  }
1413  
1414  boolean finalizeObject (ElementInfo ei) {
1415    MethodInfo fin = ei.getClassInfo().getFinalizer();
1416    
1417    if (fin != null) {
1418      // <2do> not really - finalizers should run in their own thread
1419 ThreadInfo ti = ss.getRunningThread();
1420      
1421      // this is subtle - if this is not the last non-daemon, we have to finalize.
1422 // If it is, we don't. Instead of re-creating stack frames, we just flag
1423 // the object as not yet finalizable. For this purpose, it's a somewhat
1424 // braindead hack, but ultimately we need this anyway, since finalization
1425 // can make objects live again
1426 if (ti.countStackFrames() <= 0) {
1427        return false;
1428      }
1429      
1430      ti.push(ei.getThisReference(), true);
1431      ti.executeMethod(fin);
1432    }
1433    
1434    return true;
1435  }
1436  
1437  
1438  /**
1439   * VM state implementation. See the description of the VMState
1440   * interface for anticipated future API changes
1441   * NOTE - making JVMStates fully restorable is currently very
1442   * expensive and should only be done on a selective basis
1443   */
1444  class JVMState implements VMState {
1445    
1446    /**
1447     * snapshots of the current state restoration data
1448     * this is what we need to analyze the current state, but doesn't inlcude
1449     * the history (path and backtrack caches)
1450     */
1451    int[] ksStoringData;
1452    Object ksBacktrackData;
1453    Object ssBacktrackData;
1454    
1455    /** the set of last executed insns */
1456    TrailInfo lastTrailInfo;
1457    
1458    /* these are the icky parts - the history is kept as stacks inside the
1459     * JVM (for restoration reasons), hence we have to copy it if we want
1460     * to restore a state. Since this is really expensive, it has to be done
1461     * on demand, with varying degrees of information
1462     */
1463    Path path;
1464    
1465    Stack backtrackStack;
1466    Stack stateBacktrackStack;
1467    Stack stateStoringStack;
1468    
1469    JVMState () {
1470      ksStoringData = JVM.this.ksStoringData;
1471      ksBacktrackData = JVM.this.ksBacktrackData;
1472      
1473      
1474      // unfortunately we cannot cache the SystemState since it is changed
1475 // before we return from forward(), but after it got pushed on the
1476 // stateBacktrackStack
1477 ssBacktrackData = ss.getBacktrackData();
1478      
1479      lastTrailInfo = JVM.this.lastTrailInfo;
1480    }
1481    
1482    public Transition getLastTransition () {
1483      return lastTrailInfo;
1484    }
1485    
1486    // Beware - this is expensive. If this JVMState is not meant to be used
1487 // for state restoration (which is requested by makeRestorable()), stay
1488 // away from it. If you 'just' need to enumerate, keep track of the states
1489 // themselves (which would be required for graphical display anyway) and use
1490 // getLastTransition
1491 public Path getPath () {
1492      if (path == null) {
1493        path = JVM.this.getPath();
1494      }
1495      
1496      return path;
1497    }
1498    
1499    public int getThread () {
1500      return lastTrailInfo.getThread();
1501    }
1502    
1503    /**
1504     * this doesn't clone the backtracking info, i.e. we cannot backtrack
1505     * above this state again, only up to it
1506     */
1507    public void makeForwardRestorable () {
1508      path = JVM.this.getPath();
1509    }
1510    
1511    public boolean isForwardRestorable() {
1512      return (path != null);
1513    }
1514    
1515    /**
1516     * in addition to the path, we also have to copy the backtrack stacks
1517     * of the VM. This is overly expensive. DON'T DO UNLESS YOU HAVE TO!
1518     */
1519    public void makeRestorable () {
1520      path = JVM.this.getPath();
1521      stateBacktrackStack = (Stack )JVM.this.stateBacktrackStack.clone();
1522      stateStoringStack = (Stack )JVM.this.stateStoringStack.clone();
1523      backtrackStack = (Stack )JVM.this.backtrackStack.clone();
1524    }
1525    
1526    public boolean isRestorable () {
1527      return (stateBacktrackStack != null);
1528    }
1529  }
1530}
1531
1532
1533
1534
1535

A to Z: JavaDoc & Examples

---

Daily Java News & Articles

---

Open Source Projects

---

Open Source Codes

---

Free Computer Books

---

Remove Frame

---

Popular Tags