gov.nasa.jpf.listener

Class IdleFilter

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.IdleFilter

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener, java.lang.Cloneable

Direct Known Subclasses:

EndlessLoopDetector

public class IdleFilter
extends PropertyListenerAdapter

simple combined listener that checks if a thread seems to do idle loops that might starve other threads or JPF. The most classical case is a "busy wait" loop like for (long l=0; l<1000000; l++); which would give us a pretty long path. Even worse, things like while (true); would (just like in a normal VM) never terminate in JPF, even though people familiar with model checking would expect state matching. Only that without a transition break, JPF has no reason to match states, so we have to automatically add a break on the backjump. We shouldn't add one on every backjump though because that might cause a lot of overhead in programs that do terminate. IdleFilter has two options: idle.max_backjumps : sets the number of backjumps after which we break idle.action : what to do if max_backjumps are exceeded in the same thread on the same location and stackframe warn : only print warning for backjumps exceeding the max_backjumps break : break the transition to allow state matching prune : unconditionally prune the search jump : jump past the backjump (this is dangerous if the loop has side effects)

Constructor Summary

Constructors

Constructor and Description
IdleFilter(Config config)

Method Summary

Modifier and Type	Method and Description
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	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	threadTerminated(VM vm, ThreadInfo ti) Thread exited run() method

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

check, choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, clone, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, loadClass, methodEntered, methodExited, objectCreated, objectExposed, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectShared, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishFinished, publishProbe, publishPropertyViolation, publishStart, publishTransition, reset, searchConstraintHit, searchFinished, searchProbed, searchStarted, stateProcessed, statePurged, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadWaiting, vmInitialized

Methods inherited from class gov.nasa.jpf.GenericProperty

getErrorMessage, getExplanation, printOn

Methods inherited from class java.lang.Object

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

Constructor Detail

IdleFilter

public IdleFilter(Config config)

Method Detail

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 PropertyListenerAdapter

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 PropertyListenerAdapter

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 PropertyListenerAdapter

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 PropertyListenerAdapter