2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPFException;
22 import gov.nasa.jpf.util.TypeSpecMatcher;
23 import gov.nasa.jpf.vm.choice.BreakGenerator;
25 import java.io.PrintWriter;
26 import java.util.LinkedHashMap;
30 * the class that encapsulates not only the current execution state of the VM
31 * (the KernelState), but also the part of it's history that is required
32 * by VM to backtrack, plus some potential annotations that can be used to
33 * control the search (i.e. forward/backtrack calls)
35 public class SystemState {
38 * instances of this class are used to store the SystemState parts which are
39 * subject to backtracking/state resetting. At some point, we might have
40 * stripped SystemState down enough to just store the SystemState itself
41 * (so far, we don't change it's identity, there is only one)
42 * the KernelState is still stored separately (which seems to be another
45 * NOTE: this gets stored at the end of a transition, i.e. if we need a value
46 * to be restored to it's transition entry state (like atomicLevel), we have
47 * to do that explicitly. Alternatively we could create the Memento before
48 * we start to enter the step, but then we have to update the nextCg in the
49 * snapshot, since it's only set at the transition end (required for
50 * restore(), i.e. HeuristicSearches)
52 * NOTE: the plain Memento doesn't deep copy the CGs, which means it can
53 * only be used for depth first search, where the parent CG states are always
54 * current if we encounter an error. If general state restoration is
55 * required (where the parent CGs might have been changed at the time we
56 * restore), we have to use a RestorableMemento
57 * <2do> this separation is error prone and fragile. It depends on correct
58 * ChoiceGenerator deepCopy() implementations and a separate state acquisition
59 * for restorable states. Currently, the gate for this is VM.getRestorableState(),
60 * but this could be bypassed.
62 static class Memento {
63 ChoiceGenerator<?> curCg; // the ChoiceGenerator for the current transition
64 ChoiceGenerator<?> nextCg;
67 ThreadInfo execThread;
68 int id; // the state id
69 LinkedHashMap<Object,ClosedMemento> restorers;
71 static protected ChoiceGenerator<?> cloneCG( ChoiceGenerator<?> cg){
74 return cg.deepClone();
75 } catch (CloneNotSupportedException cnsx){
76 throw new JPFException("clone failed: " + cg);
83 Memento (SystemState ss) {
87 atomicLevel = ss.entryAtomicLevel; // store the value we had when we started the transition
89 execThread = ss.execThread;
91 // we can just copy the reference since it is re-created in each transition
92 restorers = ss.restorers;
96 * this one is used to restore to a state which will re-enter with the next choice
97 * of the same CG, i.e. nextCG is reset
99 void backtrack (SystemState ss) {
100 ss.nextCg = null; // this is important - the nextCG will be set by the next Transition
103 ss.atomicLevel = atomicLevel;
105 ss.execThread = execThread;
107 if (restorers != null){
108 for (ClosedMemento r : restorers.values()){
114 void restore (SystemState ss) {
115 throw new JPFException("can't restore a SystemState.Memento that was created for backtracking");
121 ss.atomicLevel = atomicLevel;
123 ss.execThread = execThread;
129 * a Memento that can be restored, not just backtracked to. Be aware this can
130 * be a lot more expensive since it has to deep copy CGs so that we have
131 * the state of the parent CGs restored properly
133 static class RestorableMemento extends Memento {
134 RestorableMemento (SystemState ss){
137 nextCg = cloneCG(nextCg);
138 curCg = cloneCG( curCg);
142 void backtrack (SystemState ss){
144 ss.curCg = cloneCG(curCg);
148 * this one is used if we restore and then advance, i.e. it might change the CG on
149 * the next advance (if nextCg was set)
152 void restore (SystemState ss) {
153 // if we don't clone them on restore, it means we can only restore this memento once
154 ss.nextCg = cloneCG(nextCg);
155 ss.curCg = cloneCG(curCg);
157 ss.atomicLevel = atomicLevel;
159 ss.execThread = execThread;
161 if (restorers != null){
162 for (ClosedMemento r : restorers.values()){
169 int id; /** the state id */
171 ChoiceGenerator<?> nextCg; // the ChoiceGenerator for the next transition
172 ChoiceGenerator<?> curCg; // the ChoiceGenerator used in the current transition
173 ThreadInfo execThread; // currently executing thread, reset by ThreadChoiceGenerators
175 // on-demand list of optional restorers that run if we backtrack to this state
176 // this is reset before each transition
177 LinkedHashMap<Object,ClosedMemento> restorers;
180 /** current execution state of the VM (stored separately by VM) */
181 public KernelState ks;
183 public Transition trail; /** trace information */
185 //--- attributes that can be explicitly set for a state
187 boolean retainAttributes; // as long as this is set, we don't reset attributes
189 //--- ignored and isNewState are imperative
190 boolean isIgnored; // treat this as a matched state, i.e. backtrack
191 boolean isForced; // treat this as a new state
193 //--- those are hints (e.g. for HeuristicSearches)
194 boolean isInteresting;
197 boolean isBlockedInAtomicSection;
199 /** uncaught exception in current transition */
200 public UncaughtException uncaughtException;
202 /** set to true if garbage collection is necessary */
203 boolean GCNeeded = false;
205 // this is an optimization - long transitions can cause a lot of short-living
206 // garbage, which in turn can slow down the system considerably (heap size)
207 // by setting 'nAllocGCThreshold', we can do sync. on-the-fly gc when the
208 // number of new allocs within a single transition exceeds this value
212 /** NOTE: this has changed its meaning again. Now it once more is an
213 * optimization that can be used by applications calling Verify.begin/endAtomic(),
214 * but be aware of that it now reports a deadlock property violation in
215 * case of a blocking op inside an atomic section
216 * Data CGs however are now allowed to be inside atomic sections
218 * BEWARE - It is in the nature of atomic sections that they might loose paths that
219 * are relevant. This is esp. true for Thread.start() within AS if the starter
220 * runs to completion without further scheduling points (DiningPhil problem).
223 int entryAtomicLevel;
225 /** do we want executed insns to be recorded */
228 /** CG types for which we extend transitions if the CG has only non-rescheduling single choices */
229 TypeSpecMatcher extendTransitions;
232 * Creates a new system state.
234 public SystemState (Config config, VM vm) {
235 ks = new KernelState(config);
236 id = StateSet.UNKNOWN_ID;
238 Class<?>[] argTypes = { Config.class, VM.class, SystemState.class };
240 // we can't yet initialize the trail until we have the start thread
242 maxAllocGC = config.getInt("vm.max_alloc_gc", Integer.MAX_VALUE);
243 if (maxAllocGC <= 0){
244 maxAllocGC = Integer.MAX_VALUE;
247 extendTransitions = TypeSpecMatcher.create(config.getStringArray("vm.extend_transitions"));
248 // recordSteps is set later by VM, first we need a reporter (which requires the VM)
251 protected SystemState() {
252 // just for unit test mockups
255 public void setStartThread (ThreadInfo ti) {
257 trail = new Transition(nextCg, execThread);
260 public int getId () {
264 public void setId (int newId) {
266 trail.setStateId(newId);
269 nextCg.setStateId(newId);
273 public void recordSteps (boolean cond) {
278 * use those with extreme care, it overrides scheduling choices
280 public void incAtomic () {
284 public void decAtomic () {
285 if (atomicLevel > 0) {
289 public void clearAtomic() {
293 public boolean isAtomic () {
294 return (atomicLevel > 0);
297 public boolean isBlockedInAtomicSection() {
298 return isBlockedInAtomicSection;
301 public void setBlockedInAtomicSection() {
302 isBlockedInAtomicSection = true;
305 public Transition getTrail() {
309 public KernelState getKernelState() {
313 public Heap getHeap() {
317 //--- these are the various choice generator retrievers
320 * answer the ChoiceGenerator that is used in the current transition
322 public ChoiceGenerator<?> getChoiceGenerator () {
326 public ChoiceGenerator<?> getChoiceGenerator (String id) {
327 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getPreviousChoiceGenerator()){
328 if (id.equals(cg.getId())){
337 * return the whole stack of CGs of the current path
339 public ChoiceGenerator<?>[] getChoiceGenerators () {
341 return curCg.getAll();
347 public ChoiceGenerator<?> getLastChoiceGeneratorInThread (ThreadInfo ti){
348 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getPreviousChoiceGenerator()){
349 if (cg.getThreadInfo() == ti){
358 public <T extends ChoiceGenerator<?>> T[] getChoiceGeneratorsOfType (Class<T> cgType) {
360 return curCg.getAllOfType(cgType);
367 public <T extends ChoiceGenerator<?>> T getLastChoiceGeneratorOfType (Class<T> cgType) {
368 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getPreviousChoiceGenerator()){
369 if (cgType.isAssignableFrom(cg.getClass())) {
377 public <T> ChoiceGenerator<T> getLastChoiceGeneratorOfChoiceType (String id, Class<T> choiceType){
378 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getPreviousChoiceGenerator()){
379 if ((id == null || id.equals(cg.getId())) && choiceType.isAssignableFrom(cg.getChoiceType())) {
380 return (ChoiceGenerator<T>)cg;
388 public <T extends ChoiceGenerator<?>> T getCurrentChoiceGeneratorOfType (Class<T> cgType) {
389 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getCascadedParent()){
390 if (cgType.isAssignableFrom(cg.getClass())){
398 public <T extends ChoiceGenerator<?>> T getCurrentChoiceGenerator (String id, Class<T> cgType) {
399 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getCascadedParent()){
400 if (id.equals(cg.getId()) && cgType.isAssignableFrom(cg.getClass())){
408 public <T> ChoiceGenerator<T> getCurrentChoiceGeneratorForChoiceType (String id, Class<T> choiceType){
409 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getCascadedParent()){
410 if ((id == null || id.equals(cg.getId())) && choiceType.isAssignableFrom(cg.getChoiceType())){
411 return (ChoiceGenerator<T>)cg;
419 public ChoiceGenerator<?> getCurrentChoiceGenerator (String id) {
420 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getCascadedParent()){
421 if (id.equals(cg.getId())){
429 public ChoiceGenerator<?> getCurrentChoiceGenerator (ChoiceGenerator<?> cgPrev) {
433 return cgPrev.getCascadedParent();
438 * this returns the most recently registered ThreadChoiceGenerator that is
439 * also a scheduling point, or 'null' if there is none in the list of current CGs
441 public ThreadChoiceGenerator getCurrentSchedulingPoint () {
442 for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getCascadedParent()){
443 if (cg instanceof ThreadChoiceGenerator){
444 ThreadChoiceGenerator tcg = (ThreadChoiceGenerator)cg;
445 if (tcg.isSchedulingPoint()){
454 public ChoiceGenerator<?>[] getCurrentChoiceGenerators () {
455 return curCg.getCascade();
459 public <T extends ChoiceGenerator<?>> T getInsnChoiceGeneratorOfType (Class<T> cgType, Instruction insn, ChoiceGenerator<?> cgPrev){
460 ChoiceGenerator<?> cg = cgPrev != null ? cgPrev.getPreviousChoiceGenerator() : curCg;
462 if (cg != null && cg.getInsn() == insn && cgType.isAssignableFrom(cg.getClass())){
469 public ChoiceGenerator<?> getNextChoiceGenerator () {
474 * set the ChoiceGenerator to be used in the next transition
475 * @return true if there is a nextCg set after registration and listener notification
477 public boolean setNextChoiceGenerator (ChoiceGenerator<?> cg) {
479 // if this transition is already marked as ignored, we are not allowed
480 // to set nextCg because 'isIgnored' results in a shortcut backtrack that
481 // is not handed back to the Search (its solely in VM forward)
486 // first, check if we have to randomize it. Note this might change the CG
487 // instance since some algorithmic CG types need to be transformed into
488 // explicit choice lists
489 if (ChoiceGeneratorBase.useRandomization()) {
493 // set its context (thread and insn)
494 cg.setContext(execThread);
496 // do we already have a nextCG, which means this one is a cascaded CG
497 if (nextCg != null) {
498 cg.setPreviousChoiceGenerator(nextCg);
499 nextCg.setCascaded(); // note the last registered CG is NOT set cascaded
502 cg.setPreviousChoiceGenerator(curCg);
507 execThread.getVM().notifyChoiceGeneratorRegistered(cg, execThread); // <2do> we need a better way to get the vm
510 // a choiceGeneratorRegistered listener might have removed this CG
511 return (nextCg != null);
514 public void setMandatoryNextChoiceGenerator (ChoiceGenerator<?> cg, String failMsg){
515 if (!setNextChoiceGenerator(cg)){
516 throw new JPFException(failMsg);
521 * remove the current 'nextCg'
522 * Note this has to be called in a loop if all cascaded CGs have to be removed
524 public void removeNextChoiceGenerator (){
526 nextCg = nextCg.getPreviousChoiceGenerator();
531 * remove the whole chain of currently registered nextCGs
533 public void removeAllNextChoiceGenerators(){
534 while (nextCg != null){
535 nextCg = nextCg.getPreviousChoiceGenerator();
540 public Object getBacktrackData () {
541 return new Memento(this);
544 public void backtrackTo (Object backtrackData) {
545 ((Memento) backtrackData).backtrack( this);
548 public Object getRestoreData(){
549 return new RestorableMemento(this);
552 public void restoreTo (Object backtrackData) {
553 ((Memento) backtrackData).restore( this);
556 public void retainAttributes (boolean b){
557 retainAttributes = b;
560 public boolean getRetainAttributes() {
561 return retainAttributes;
565 * this can be called anywhere from within a transition, to revert it and
566 * go on with the next choice. This is mostly used explicitly in the app
567 * via Verify.ignoreIf(..)
569 * calling setIgnored() also breaks the current transition, i.e. no further
570 * instructions are executed within this step
572 public void setIgnored (boolean b) {
576 isForced = false; // mutually exclusive
580 public boolean isIgnored () {
584 public void setForced (boolean b){
588 isIgnored = false; // mutually exclusive
592 public boolean isForced () {
596 public void setInteresting (boolean b) {
604 public boolean isInteresting () {
605 return isInteresting;
608 public void setBoring (boolean b) {
612 isInteresting = false;
616 public boolean isBoring () {
620 public boolean isInitState () {
621 return (id == StateSet.UNKNOWN_ID);
624 public int getThreadCount () {
625 return ks.threads.length();
628 public UncaughtException getUncaughtException () {
629 return uncaughtException;
632 public void activateGC () {
636 public boolean hasRestorer (Object key){
637 if (restorers != null){
638 return restorers.containsKey(key);
644 public ClosedMemento getRestorer( Object key){
645 if (restorers != null){
646 return restorers.get(key);
653 * call the provided restorer each time we get back to this state
655 * @param key usually the object this restorer encapsulates
656 * @param restorer the ClosedMemento that restores the state of the object
657 * it encapsulates once we backtrack/restore this program state
659 * Note that restorers are called in the order of registration, but in
660 * general it is not a good idea to depend on order since restorers can
661 * be set from different locations (listeners, peers, instructions)
663 public void putRestorer (Object key, ClosedMemento restorer){
664 if (restorers == null){
665 restorers = new LinkedHashMap<Object,ClosedMemento>();
668 // we only support one restorer per target for now
669 restorers.put(key,restorer);
672 public boolean gcIfNeeded () {
673 boolean needed = false;
685 * check if number of allocations since last GC exceed the maxAllocGC
686 * threshold, perform on-the-fly GC if yes. This is aimed at avoiding a lot
687 * of short-living garbage in long transitions, which slows down the heap
690 public void checkGC () {
691 if (nAlloc++ > maxAllocGC){
697 void dumpThreadCG (ThreadChoiceGenerator cg) {
698 PrintWriter pw = new PrintWriter(System.out, true);
704 * reset the SystemState and initialize the next CG. This gets called
705 * *before* the restorer computes the KernelState snapshot, i.e. it is *not*
706 * allowed to change anything in the program state. The reason for splitting
707 * CG initialization from transition execution is to avoid KernelState storage
708 * in case the initialization does not produce a next choice and we have to
713 * @return 'true' if there is a next choice, i.e. a next transition to enter.
714 * 'false' if there is no next choice and the system has to backtrack
716 public boolean initializeNextTransition(VM vm) {
718 // set this before any choiceGeneratorSet or choiceGeneratorAdvanced
719 // notification (which can override it)
720 if (!retainAttributes){
723 isInteresting = false;
729 // 'nextCg' got set at the end of the previous transition (or a preceding
730 // choiceGeneratorSet() notification).
731 // Be aware of that 'nextCg' is only the *last* CG that was registered, i.e.
732 // there can be any number of CGs between the previous 'curCg' and 'nextCg'
733 // that were registered for the same insn.
734 while (nextCg != null) {
738 // these are hooks that can be used to do context specific CG initialization
740 notifyChoiceGeneratorSet(vm, curCg);
743 assert (curCg != null) : "transition without choice generator";
745 return advanceCurCg(vm);
749 * enter all instructions that constitute the next transition.
751 * Note this gets called *after* storing the KernelState, i.e. is allowed to
752 * modify thread states and fields
756 public void executeNextTransition (VM vm){
757 // do we have a thread context switch? (this sets execThread)
760 assert execThread.isRunnable() : "next transition thread not runnable: " + execThread.getStateDescription();
762 trail = new Transition(curCg, execThread);
763 entryAtomicLevel = atomicLevel; // store before we start to enter
765 execThread.executeTransition(this);
769 * check if we can extend the current transition without state storing/matching
770 * This is useful for non-cascaded single choice CGs that do not cause
771 * rescheduling. Such CGs are never backtracked to anyways (they are processed
772 * on their first advance).
774 * NOTE: this is on top of CG type specific optimizations that are controlled
775 * by cg.break_single_choice (unset by default). If the respective CG creator
776 * is single choice aware it might not create / register a CG in the first
777 * place and we never get here. This is only called if somebody did create
780 * note also that we don't eliminate BreakGenerators since their only purpose
781 * in life is to explicitly cause transition breaks. We don't want to override
784 protected boolean extendTransition (){
785 ChoiceGenerator<?> ncg = nextCg;
787 if (CheckExtendTransition.isMarked(ncg) ||
788 ((extendTransitions != null) && extendTransitions.matches(ncg.getClass()))){
789 if (ncg.getTotalNumberOfChoices() == 1 && !ncg.isCascaded()){
790 if (ncg instanceof ThreadChoiceGenerator){
791 if ((ncg instanceof BreakGenerator) || !((ThreadChoiceGenerator) ncg).contains(execThread)){
796 initializeNextTransition(execThread.getVM());
805 protected void setExecThread( VM vm){
806 ThreadChoiceGenerator tcg = getCurrentSchedulingPoint();
808 ThreadInfo tiNext = tcg.getNextChoice();
809 if (tiNext != execThread) {
810 vm.notifyThreadScheduled(tiNext);
815 if (execThread.isTimeoutWaiting()) {
816 execThread.setTimedOut();
821 // the number of advanced choice generators in this step
822 protected int nAdvancedCGs;
824 protected void advance( VM vm, ChoiceGenerator<?> cg){
826 if (cg.hasMoreChoices()){
829 vm.notifyChoiceGeneratorAdvanced(cg);
832 // this seems redundant, but the CG or the listener might actually skip choices,
833 // in which case we can't execute the next transition.
834 // NOTE - this causes backtracking
835 // <2do> it's debatable if we should treat this as a processed CG
836 if (cg.getNextChoice() != null){
843 vm.notifyChoiceGeneratorProcessed(cg);
849 protected void advanceAllCascadedParents( VM vm, ChoiceGenerator<?> cg){
850 ChoiceGenerator<?> parent = cg.getCascadedParent();
852 advanceAllCascadedParents(vm, parent);
857 protected boolean advanceCascadedParent (VM vm, ChoiceGenerator<?> cg){
858 if (cg.hasMoreChoices()){
863 vm.notifyChoiceGeneratorProcessed(cg);
865 ChoiceGenerator<?> parent = cg.getCascadedParent();
867 if (advanceCascadedParent(vm,parent)){
877 protected boolean advanceCurCg (VM vm){
880 ChoiceGenerator<?> cg = curCg;
881 ChoiceGenerator<?> parent = cg.getCascadedParent();
883 if (cg.hasMoreChoices()){
884 // check if this is the first time, for which we also have to advance our parents
885 if (parent != null && parent.getProcessedNumberOfChoices() == 0){
886 advanceAllCascadedParents(vm,parent);
890 } else { // this one is done, but how about our parents
891 vm.notifyChoiceGeneratorProcessed(cg);
894 if (advanceCascadedParent(vm,parent)){
901 return (nAdvancedCGs > 0);
906 protected void notifyChoiceGeneratorSet (VM vm, ChoiceGenerator<?> cg){
907 ChoiceGenerator<?> parent = cg.getCascadedParent();
908 if (parent != null) {
909 notifyChoiceGeneratorSet(vm, parent);
911 vm.notifyChoiceGeneratorSet(cg); // notify top down
915 // this is called on every executeInstruction from the running thread
916 public boolean breakTransition () {
917 return ((nextCg != null) || isIgnored);
920 void recordExecutionStep (Instruction pc) {
921 // this can require a lot of memory, so we should only store
922 // executed insns if we have to
924 Step step = new Step(pc);
925 trail.addStep( step);
927 trail.incStepCount();
931 // the three primitive ops used from within VM.forward()