gov.nasa.jpf.listener

Class ExecTracker

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.ExecTracker

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class ExecTracker
extends ListenerAdapter

Listener tool to monitor JPF execution. This class can be used as a drop-in replacement for JPF, which is called by ExecTracker. ExecTracker is mostly a VMListener of 'instructionExecuted' and a SearchListener of 'stateAdvanced' and 'statehBacktracked' NOTE - the ExecTracker is machine type agnostic

Constructor Summary

Constructors

Constructor and Description
ExecTracker(Config config)

Method Summary

Modifier and Type	Method and Description
void	choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) the next choice was requested from a previously registered ChoiceGenerator NOTE - this notification happens before the KernelState is stored, i.e.
void	exceptionThrown(VM vm, ThreadInfo ti, ElementInfo ei) exception was thrown
void	gcEnd(VM vm) VMListener interface
void	instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)
void	objectExposed(VM vm, ThreadInfo currentThread, ElementInfo fieldOwnerObject, ElementInfo exposedObject) object becomes reachable through a shared reference 'sharedObject' is the (already shared) owner of the field to which the (yet unshared) 'exposedObject' reference got assigned
void	objectShared(VM vm, ThreadInfo currentThread, ElementInfo sharedObject) object fields accessed by more than one live thread
void	searchFinished(Search search) we're done, either with or without a preceeding error
void	searchStarted(Search search) we get this after we enter the search loop, but BEFORE the first forward
void	stateAdvanced(Search search) got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set
void	stateBacktracked(Search search) state was backtracked one step
void	stateProcessed(Search search) state is fully explored
void	stateRestored(Search search) SearchListener interface
void	threadStarted(VM vm, ThreadInfo ti) new Thread entered run() method
void	threadTerminated(VM vm, ThreadInfo ti) Thread exited run() method

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, exceptionBailout, exceptionHandled, executeInstruction, gcBegin, loadClass, methodEntered, methodExited, objectCreated, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishFinished, publishProbe, publishPropertyViolation, publishStart, publishTransition, searchConstraintHit, searchProbed, statePurged, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadWaiting, vmInitialized

Methods inherited from class java.lang.Object

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

Constructor Detail

ExecTracker

public ExecTracker(Config config)

Method Detail

stateRestored

public void stateRestored(Search search)

SearchListener interface

Specified by:

stateRestored in interface SearchListener

Overrides:

stateRestored in class ListenerAdapter

searchStarted

public void searchStarted(Search search)

Description copied from interface: SearchListener

we get this after we enter the search loop, but BEFORE the first forward

Specified by:

searchStarted in interface SearchListener

Overrides:

searchStarted in class ListenerAdapter

stateAdvanced

public void stateAdvanced(Search search)

Description copied from interface: SearchListener

got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set

Specified by:

stateAdvanced in interface SearchListener

Overrides:

stateAdvanced in class ListenerAdapter

stateProcessed

public void stateProcessed(Search search)

Description copied from interface: SearchListener

state is fully explored

Specified by:

stateProcessed in interface SearchListener

Overrides:

stateProcessed in class ListenerAdapter

stateBacktracked

public void stateBacktracked(Search search)

Description copied from interface: SearchListener

state was backtracked one step

Specified by:

stateBacktracked in interface SearchListener

Overrides:

stateBacktracked in class ListenerAdapter

searchFinished

public void searchFinished(Search search)

Description copied from interface: SearchListener

we're done, either with or without a preceeding error

Specified by:

searchFinished in interface SearchListener

Overrides:

searchFinished in class ListenerAdapter

gcEnd

public void gcEnd(VM vm)

VMListener interface

Specified by:

gcEnd in interface VMListener

Overrides:

gcEnd in class ListenerAdapter

instructionExecuted

public void instructionExecuted(VM vm,
                                ThreadInfo ti,
                                Instruction nextInsn,
                                Instruction executedInsn)

Description copied from interface: VMListener

VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)

Specified by:

instructionExecuted in interface VMListener

Overrides:

instructionExecuted in class ListenerAdapter

threadStarted

public void threadStarted(VM vm,
                          ThreadInfo ti)

Description copied from interface: VMListener

new Thread entered run() method

Specified by:

threadStarted in interface VMListener

Overrides:

threadStarted in class ListenerAdapter

threadTerminated

public void threadTerminated(VM vm,
                             ThreadInfo ti)

Description copied from interface: VMListener

Thread exited run() method

Specified by:

threadTerminated in interface VMListener

Overrides:

threadTerminated in class ListenerAdapter

exceptionThrown

public void exceptionThrown(VM vm,
                            ThreadInfo ti,
                            ElementInfo ei)

Description copied from interface: VMListener

exception was thrown

Specified by:

exceptionThrown in interface VMListener

Overrides:

exceptionThrown in class ListenerAdapter

choiceGeneratorAdvanced

public void choiceGeneratorAdvanced(VM vm,
                                    ChoiceGenerator<?> currentCG)

Description copied from interface: VMListener

the next choice was requested from a previously registered ChoiceGenerator NOTE - this notification happens before the KernelState is stored, i.e. listeners are NOT allowed to alter the KernelState (e.g. by changing field values or thread states)

Specified by:

choiceGeneratorAdvanced in interface VMListener

Overrides:

choiceGeneratorAdvanced in class ListenerAdapter

objectExposed

public void objectExposed(VM vm,
                          ThreadInfo currentThread,
                          ElementInfo fieldOwnerObject,
                          ElementInfo exposedObject)

Description copied from interface: VMListener

object becomes reachable through a shared reference 'sharedObject' is the (already shared) owner of the field to which the (yet unshared) 'exposedObject' reference got assigned

Specified by:

objectExposed in interface VMListener

Overrides:

objectExposed in class ListenerAdapter

objectShared

public void objectShared(VM vm,
                         ThreadInfo currentThread,
                         ElementInfo sharedObject)

Description copied from interface: VMListener

object fields accessed by more than one live thread

Specified by:

objectShared in interface VMListener

Overrides:

objectShared in class ListenerAdapter