gov.nasa.jpf.vm

Class SystemState

java.lang.Object

gov.nasa.jpf.vm.SystemState

public class SystemState
extends java.lang.Object

the class that encapsulates not only the current execution state of the VM (the KernelState), but also the part of it's history that is required by VM to backtrack, plus some potential annotations that can be used to control the search (i.e. forward/backtrack calls)

Field Summary

Fields

Modifier and Type	Field and Description
KernelState	ks current execution state of the VM (stored separately by VM)
protected int	nAdvancedCGs
Transition	trail
UncaughtException	uncaughtException uncaught exception in current transition

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	SystemState()
	SystemState(Config config, VM vm) Creates a new system state.

Method Summary

Modifier and Type	Method and Description
void	activateGC()
protected void	advance(VM vm, ChoiceGenerator<?> cg)
protected void	advanceAllCascadedParents(VM vm, ChoiceGenerator<?> cg)
protected boolean	advanceCascadedParent(VM vm, ChoiceGenerator<?> cg)
protected boolean	advanceCurCg(VM vm)
void	backtrackTo(java.lang.Object backtrackData)
boolean	breakTransition()
void	checkGC() check if number of allocations since last GC exceed the maxAllocGC threshold, perform on-the-fly GC if yes.
void	clearAtomic()
void	decAtomic()
void	executeNextTransition(VM vm) enter all instructions that constitute the next transition.
protected boolean	extendTransition() check if we can extend the current transition without state storing/matching This is useful for non-cascaded single choice CGs that do not cause rescheduling.
boolean	gcIfNeeded()
java.lang.Object	getBacktrackData()
ChoiceGenerator<?>	getChoiceGenerator() answer the ChoiceGenerator that is used in the current transition
ChoiceGenerator<?>	getChoiceGenerator(java.lang.String id)
ChoiceGenerator<?>[]	getChoiceGenerators() return the whole stack of CGs of the current path
<T extends ChoiceGenerator<?>> T[]	getChoiceGeneratorsOfType(java.lang.Class<T> cgType)
ChoiceGenerator<?>	getCurrentChoiceGenerator(ChoiceGenerator<?> cgPrev)
ChoiceGenerator<?>	getCurrentChoiceGenerator(java.lang.String id)
<T extends ChoiceGenerator<?>> T	getCurrentChoiceGenerator(java.lang.String id, java.lang.Class<T> cgType)
<T> ChoiceGenerator<T>	getCurrentChoiceGeneratorForChoiceType(java.lang.String id, java.lang.Class<T> choiceType)
<T extends ChoiceGenerator<?>> T	getCurrentChoiceGeneratorOfType(java.lang.Class<T> cgType)
ChoiceGenerator<?>[]	getCurrentChoiceGenerators()
ThreadChoiceGenerator	getCurrentSchedulingPoint() this returns the most recently registered ThreadChoiceGenerator that is also a scheduling point, or 'null' if there is none in the list of current CGs
Heap	getHeap()
int	getId()
<T extends ChoiceGenerator<?>> T	getInsnChoiceGeneratorOfType(java.lang.Class<T> cgType, Instruction insn, ChoiceGenerator<?> cgPrev)
KernelState	getKernelState()
ChoiceGenerator<?>	getLastChoiceGeneratorInThread(ThreadInfo ti)
<T> ChoiceGenerator<T>	getLastChoiceGeneratorOfChoiceType(java.lang.String id, java.lang.Class<T> choiceType)
<T extends ChoiceGenerator<?>> T	getLastChoiceGeneratorOfType(java.lang.Class<T> cgType)
ChoiceGenerator<?>	getNextChoiceGenerator()
java.lang.Object	getRestoreData()
ClosedMemento	getRestorer(java.lang.Object key)
boolean	getRetainAttributes()
int	getThreadCount()
Transition	getTrail()
UncaughtException	getUncaughtException()
boolean	hasRestorer(java.lang.Object key)
void	incAtomic() use those with extreme care, it overrides scheduling choices
boolean	initializeNextTransition(VM vm) reset the SystemState and initialize the next CG.
boolean	isAtomic()
boolean	isBlockedInAtomicSection()
boolean	isBoring()
boolean	isForced()
boolean	isIgnored()
boolean	isInitState()
boolean	isInteresting()
protected void	notifyChoiceGeneratorSet(VM vm, ChoiceGenerator<?> cg)
void	putRestorer(java.lang.Object key, ClosedMemento restorer) call the provided restorer each time we get back to this state
void	recordSteps(boolean cond)
void	removeAllNextChoiceGenerators() remove the whole chain of currently registered nextCGs
void	removeNextChoiceGenerator() remove the current 'nextCg' Note this has to be called in a loop if all cascaded CGs have to be removed
void	restoreTo(java.lang.Object backtrackData)
void	retainAttributes(boolean b)
void	setBlockedInAtomicSection()
void	setBoring(boolean b)
protected void	setExecThread(VM vm)
void	setForced(boolean b)
void	setId(int newId)
void	setIgnored(boolean b) this can be called anywhere from within a transition, to revert it and go on with the next choice.
void	setInteresting(boolean b)
void	setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg, java.lang.String failMsg)
boolean	setNextChoiceGenerator(ChoiceGenerator<?> cg) set the ChoiceGenerator to be used in the next transition
void	setStartThread(ThreadInfo ti)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

ks

public KernelState ks

current execution state of the VM (stored separately by VM)

trail

public Transition trail

uncaughtException

public UncaughtException uncaughtException

uncaught exception in current transition

nAdvancedCGs

protected int nAdvancedCGs

Constructor Detail

SystemState

public SystemState(Config config,
                   VM vm)

Creates a new system state.

SystemState

protected SystemState()

Method Detail

setStartThread

public void setStartThread(ThreadInfo ti)

getId

public int getId()

setId

public void setId(int newId)

recordSteps

public void recordSteps(boolean cond)

incAtomic

public void incAtomic()

use those with extreme care, it overrides scheduling choices

decAtomic

public void decAtomic()

clearAtomic

public void clearAtomic()

isAtomic

public boolean isAtomic()

isBlockedInAtomicSection

public boolean isBlockedInAtomicSection()

setBlockedInAtomicSection

public void setBlockedInAtomicSection()

getTrail

public Transition getTrail()

getKernelState

public KernelState getKernelState()

getHeap

public Heap getHeap()

getChoiceGenerator

public ChoiceGenerator<?> getChoiceGenerator()

answer the ChoiceGenerator that is used in the current transition

getChoiceGenerator

public ChoiceGenerator<?> getChoiceGenerator(java.lang.String id)

getChoiceGenerators

public ChoiceGenerator<?>[] getChoiceGenerators()

return the whole stack of CGs of the current path

getLastChoiceGeneratorInThread

public ChoiceGenerator<?> getLastChoiceGeneratorInThread(ThreadInfo ti)

getChoiceGeneratorsOfType

public <T extends ChoiceGenerator<?>> T[] getChoiceGeneratorsOfType(java.lang.Class<T> cgType)

getLastChoiceGeneratorOfType

public <T extends ChoiceGenerator<?>> T getLastChoiceGeneratorOfType(java.lang.Class<T> cgType)

getLastChoiceGeneratorOfChoiceType

public <T> ChoiceGenerator<T> getLastChoiceGeneratorOfChoiceType(java.lang.String id,
                                                                 java.lang.Class<T> choiceType)

getCurrentChoiceGeneratorOfType

public <T extends ChoiceGenerator<?>> T getCurrentChoiceGeneratorOfType(java.lang.Class<T> cgType)

getCurrentChoiceGenerator

public <T extends ChoiceGenerator<?>> T getCurrentChoiceGenerator(java.lang.String id,
                                                                  java.lang.Class<T> cgType)

getCurrentChoiceGeneratorForChoiceType

public <T> ChoiceGenerator<T> getCurrentChoiceGeneratorForChoiceType(java.lang.String id,
                                                                     java.lang.Class<T> choiceType)

getCurrentChoiceGenerator

public ChoiceGenerator<?> getCurrentChoiceGenerator(java.lang.String id)

getCurrentChoiceGenerator

public ChoiceGenerator<?> getCurrentChoiceGenerator(ChoiceGenerator<?> cgPrev)

getCurrentSchedulingPoint

public ThreadChoiceGenerator getCurrentSchedulingPoint()

this returns the most recently registered ThreadChoiceGenerator that is also a scheduling point, or 'null' if there is none in the list of current CGs

getCurrentChoiceGenerators

public ChoiceGenerator<?>[] getCurrentChoiceGenerators()

getInsnChoiceGeneratorOfType

public <T extends ChoiceGenerator<?>> T getInsnChoiceGeneratorOfType(java.lang.Class<T> cgType,
                                                                     Instruction insn,
                                                                     ChoiceGenerator<?> cgPrev)

getNextChoiceGenerator

public ChoiceGenerator<?> getNextChoiceGenerator()

setNextChoiceGenerator

public boolean setNextChoiceGenerator(ChoiceGenerator<?> cg)

set the ChoiceGenerator to be used in the next transition

Returns:

true if there is a nextCg set after registration and listener notification

setMandatoryNextChoiceGenerator

public void setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg,
                                            java.lang.String failMsg)

removeNextChoiceGenerator

public void removeNextChoiceGenerator()

remove the current 'nextCg' Note this has to be called in a loop if all cascaded CGs have to be removed

removeAllNextChoiceGenerators

public void removeAllNextChoiceGenerators()

remove the whole chain of currently registered nextCGs

getBacktrackData

public java.lang.Object getBacktrackData()

backtrackTo

public void backtrackTo(java.lang.Object backtrackData)

getRestoreData

public java.lang.Object getRestoreData()

restoreTo

public void restoreTo(java.lang.Object backtrackData)

retainAttributes

public void retainAttributes(boolean b)

getRetainAttributes

public boolean getRetainAttributes()

setIgnored

public void setIgnored(boolean b)

this can be called anywhere from within a transition, to revert it and go on with the next choice. This is mostly used explicitly in the app via Verify.ignoreIf(..) calling setIgnored() also breaks the current transition, i.e. no further instructions are executed within this step

isIgnored

public boolean isIgnored()

setForced

public void setForced(boolean b)

isForced

public boolean isForced()

setInteresting

public void setInteresting(boolean b)

isInteresting

public boolean isInteresting()

setBoring

public void setBoring(boolean b)

isBoring

public boolean isBoring()

isInitState

public boolean isInitState()

getThreadCount

public int getThreadCount()

getUncaughtException

public UncaughtException getUncaughtException()

activateGC

public void activateGC()

hasRestorer

public boolean hasRestorer(java.lang.Object key)

getRestorer

public ClosedMemento getRestorer(java.lang.Object key)

putRestorer

public void putRestorer(java.lang.Object key,
                        ClosedMemento restorer)

call the provided restorer each time we get back to this state

Parameters:

key - usually the object this restorer encapsulates

restorer - the ClosedMemento that restores the state of the object it encapsulates once we backtrack/restore this program state Note that restorers are called in the order of registration, but in general it is not a good idea to depend on order since restorers can be set from different locations (listeners, peers, instructions)

gcIfNeeded

public boolean gcIfNeeded()

checkGC

public void checkGC()

check if number of allocations since last GC exceed the maxAllocGC threshold, perform on-the-fly GC if yes. This is aimed at avoiding a lot of short-living garbage in long transitions, which slows down the heap exponentially

initializeNextTransition

public boolean initializeNextTransition(VM vm)

reset the SystemState and initialize the next CG. This gets called *before* the restorer computes the KernelState snapshot, i.e. it is *not* allowed to change anything in the program state. The reason for splitting CG initialization from transition execution is to avoid KernelState storage in case the initialization does not produce a next choice and we have to backtrack.

Returns:

'true' if there is a next choice, i.e. a next transition to enter. 'false' if there is no next choice and the system has to backtrack

See Also:

VM.forward()

executeNextTransition

public void executeNextTransition(VM vm)

enter all instructions that constitute the next transition. Note this gets called *after* storing the KernelState, i.e. is allowed to modify thread states and fields

See Also:

VM.forward()

extendTransition

protected boolean extendTransition()

check if we can extend the current transition without state storing/matching This is useful for non-cascaded single choice CGs that do not cause rescheduling. Such CGs are never backtracked to anyways (they are processed on their first advance). NOTE: this is on top of CG type specific optimizations that are controlled by cg.break_single_choice (unset by default). If the respective CG creator is single choice aware it might not create / register a CG in the first place and we never get here. This is only called if somebody did create and register a CG note also that we don't eliminate BreakGenerators since their only purpose in life is to explicitly cause transition breaks. We don't want to override the override here.

setExecThread

protected void setExecThread(VM vm)

advance

protected void advance(VM vm,
                       ChoiceGenerator<?> cg)

advanceAllCascadedParents

protected void advanceAllCascadedParents(VM vm,
                                         ChoiceGenerator<?> cg)

advanceCascadedParent

protected boolean advanceCascadedParent(VM vm,
                                        ChoiceGenerator<?> cg)

advanceCurCg

protected boolean advanceCurCg(VM vm)

notifyChoiceGeneratorSet

protected void notifyChoiceGeneratorSet(VM vm,
                                        ChoiceGenerator<?> cg)

breakTransition

public boolean breakTransition()