gov.nasa.jpf.symbc

Class VeritestingListener

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.symbc.VeritestingListener

All Implemented Interfaces:

gov.nasa.jpf.JPFListener, gov.nasa.jpf.Property, gov.nasa.jpf.report.PublisherExtension, gov.nasa.jpf.search.SearchListener, gov.nasa.jpf.util.Printable, gov.nasa.jpf.vm.VMListener, java.lang.Cloneable

public class VeritestingListener
extends gov.nasa.jpf.PropertyListenerAdapter
implements gov.nasa.jpf.report.PublisherExtension

This is the entry point to Java Ranger. Through this listener JR intercept symbolic branch instructions and attempt to path-merge them by summarizing them as a constraint to be added on the path condition. Main JR transformations happen in FixedPointWrapper, which iterates different transformations until a fixed point is reached. JR also implements the single-path cases (called in the implementation SPFCases) through StaticChoiceGenerator, which allows JR to explore unsummarized behaviors of the region. JR have two instances of the region, a Static Region, and a Dynamic Region, where the static one has no runtime information included, whereas the dynamic one is where instantiation time information is found. Initially, JR creates the Static Region representing the fragment of the code that is about to be executed, this is done through the JITAnalysis. All Static Regions encounter are cached into VeritestingMain.veriRegions HashMap. JR then applies different transformations on it using the FixedPointWrapper, to turn the static region into a dynamic one, and finally to turn the dynamic region into a constraint. Finally JR decides what would parts have not completely been summarized and creates a choice for them using StaticBranchChoiceGenerator.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	VeritestingListener.VeritestingMode

Field Summary

Fields

Modifier and Type	Field and Description
static long	cleanupTime
static java.lang.String	exclusionsFile
static boolean	initializeTime
private static int	instantiationLimit
static java.lang.String[]	interestingClassNames
static boolean	jitAnalysis
static java.lang.String	key
static int	maxStaticExplorationDepth
private static long	npaths
static long	parseTime
static boolean	performanceMode
static boolean	printRegionDigest
static int	recursiveDepth
static java.lang.StringBuilder	regionDigest
private static java.lang.String	regionDigestPrintName
java.lang.String[]	regionKeys
static long	regionSummaryParseTime
static VeritestingListener.VeritestingMode	runMode
private long	runStartTime
static boolean	simplify
static boolean	singlePathOptimization
static long	solverAllocTime
static int	solverCount
private static boolean	spfCasesHeuristicsOn
private static long	staticAnalysisDur
static StatisticManager	statisticManager
private static int	timeout_mins
private static int	timeoutReportingCounter
static long	totalSolverTime
static int	veritestingMode
static int	veritestRegionCount
private static int	veritestRegionExpectedCount
static long	z3Time

Constructor Summary

Constructors

Constructor and Description
VeritestingListener(gov.nasa.jpf.Config conf, gov.nasa.jpf.JPF jpf)

Method Summary

Modifier and Type	Method and Description
static gov.nasa.jpf.vm.Instruction	advanceSpf(gov.nasa.jpf.vm.Instruction ins, DynamicRegion dynRegion, boolean earlyReturnSetup) Steps SPF to the end of the region.
private static boolean	canSetPC(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion, java.lang.Integer choice) This method checks that the current PathCondition and after appending the summarized region is satisfiable.
void	choiceGeneratorProcessed(gov.nasa.jpf.vm.VM vm, gov.nasa.jpf.vm.ChoiceGenerator<?> processedCG)
void	choiceGeneratorRegistered(gov.nasa.jpf.vm.VM vm, gov.nasa.jpf.vm.ChoiceGenerator<?> nextCG, gov.nasa.jpf.vm.ThreadInfo currentThread, gov.nasa.jpf.vm.Instruction executedInstruction)
private static void	clearStack(gov.nasa.jpf.vm.StackFrame sf, gov.nasa.jpf.vm.Instruction ins) This pop up operands of the if instruction that begins the region.
private void	discoverRegions(gov.nasa.jpf.vm.ThreadInfo ti)
void	executeInstruction(gov.nasa.jpf.vm.VM vm, gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instructionToExecute) Listener's main method that checks every instruction for being a potential veritesting region.
private java.lang.String	getMetricsVector(long dynRunTime)
private boolean	isAllowedRegion(java.lang.String key)
private boolean	isNoVeritesting(gov.nasa.jpf.vm.StackFrame curr, boolean noVeritestingFlag)
private void	isRegionEndOk(gov.nasa.jpf.vm.ThreadInfo ti, StaticRegion staticRegion, gov.nasa.jpf.vm.Instruction instructionToExecute)
private java.lang.String	keyFromInstructionToExc(gov.nasa.jpf.vm.Instruction instructionToExecute)
gov.nasa.jpf.symbc.numeric.SymbolicInteger	makeSymbolicInteger(java.lang.String name)
private static void	populateArrayOutputs(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion)
private static void	populateFieldOutputs(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion)
private static void	populateSlots(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion) Populates SPF stack slot with the output of the veritesting region.
void	publishFinished(gov.nasa.jpf.report.Publisher publisher)
private static void	pushExpOnStack(DynamicRegion dynRegion, gov.nasa.jpf.vm.StackFrame sf, java.lang.String returnType, za.ac.sun.cs.green.expr.Expression var)
private static void	pushReturnOnStack(gov.nasa.jpf.vm.StackFrame sf, DynamicRegion dynRegion)
private DynamicRegion	runVeritesting(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instructionToExecute, StaticRegion staticRegion, java.lang.String key)
private void	runVeritestingWithSPF(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.VM vm, gov.nasa.jpf.vm.Instruction instructionToExecute, StaticRegion staticRegion, java.lang.String key)
private void	runVeritestingWrapper(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.VM vm, StaticRegion staticRegion, gov.nasa.jpf.vm.Instruction instructionToExecute)
static gov.nasa.jpf.vm.Instruction	setupSPF(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction ins, DynamicRegion dynRegion, java.lang.Integer choice) This populates the Output of the summarized region to SPF.
void	stateAdvanced(gov.nasa.jpf.search.Search search)
void	stateBacktracked(gov.nasa.jpf.search.Search search)
void	threadStarted(gov.nasa.jpf.vm.VM vm, gov.nasa.jpf.vm.ThreadInfo startedThread)
void	threadTerminated(gov.nasa.jpf.vm.VM vm, gov.nasa.jpf.vm.ThreadInfo terminatedThread)
private void	updateSkipRegions(java.lang.String message, java.lang.String key)
private void	writeRegionDigest()

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

check, choiceGeneratorAdvanced, choiceGeneratorSet, classLoaded, clone, exceptionBailout, exceptionHandled, exceptionThrown, gcBegin, gcEnd, instructionExecuted, loadClass, methodEntered, methodExited, objectCreated, objectExposed, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectShared, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishProbe, publishPropertyViolation, publishStart, publishTransition, reset, searchConstraintHit, searchFinished, searchProbed, searchStarted, stateProcessed, statePurged, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, 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

Methods inherited from interface gov.nasa.jpf.report.PublisherExtension

publishConstraintHit, publishProbe, publishPropertyViolation, publishStart, publishTransition

Field Detail

veritestingMode

public static int veritestingMode

runMode

public static VeritestingListener.VeritestingMode runMode

totalSolverTime

public static long totalSolverTime

z3Time

public static long z3Time

parseTime

public static long parseTime

regionSummaryParseTime

public static long regionSummaryParseTime

solverAllocTime

public static long solverAllocTime

cleanupTime

public static long cleanupTime

solverCount

public static int solverCount

maxStaticExplorationDepth

public static int maxStaticExplorationDepth

initializeTime

public static boolean initializeTime

veritestRegionCount

public static int veritestRegionCount

staticAnalysisDur

private static long staticAnalysisDur

key

public static java.lang.String key

runStartTime

private final long runStartTime

statisticManager

public static StatisticManager statisticManager

veritestRegionExpectedCount

private static int veritestRegionExpectedCount

instantiationLimit

private static int instantiationLimit

simplify

public static boolean simplify

jitAnalysis

public static boolean jitAnalysis

timeout_mins

private static int timeout_mins

timeoutReportingCounter

private static int timeoutReportingCounter

npaths

private static long npaths

recursiveDepth

public static int recursiveDepth

regionDigest

public static java.lang.StringBuilder regionDigest

printRegionDigest

public static boolean printRegionDigest

singlePathOptimization

public static boolean singlePathOptimization

regionDigestPrintName

private static java.lang.String regionDigestPrintName

spfCasesHeuristicsOn

private static boolean spfCasesHeuristicsOn

performanceMode

public static boolean performanceMode

exclusionsFile

public static java.lang.String exclusionsFile

interestingClassNames

public static java.lang.String[] interestingClassNames

regionKeys

public java.lang.String[] regionKeys

Constructor Detail

VeritestingListener

public VeritestingListener(gov.nasa.jpf.Config conf,
                           gov.nasa.jpf.JPF jpf)

Method Detail

makeSymbolicInteger

public gov.nasa.jpf.symbc.numeric.SymbolicInteger makeSymbolicInteger(java.lang.String name)

executeInstruction

public void executeInstruction(gov.nasa.jpf.vm.VM vm,
                               gov.nasa.jpf.vm.ThreadInfo ti,
                               gov.nasa.jpf.vm.Instruction instructionToExecute)

Listener's main method that checks every instruction for being a potential veritesting region.

Specified by:

executeInstruction in interface gov.nasa.jpf.vm.VMListener

Overrides:

executeInstruction in class gov.nasa.jpf.PropertyListenerAdapter

Parameters:

vm - Virtual Machine.

ti - Current running Thread.

instructionToExecute - instruction to be executed.

runVeritestingWrapper

private void runVeritestingWrapper(gov.nasa.jpf.vm.ThreadInfo ti,
                                   gov.nasa.jpf.vm.VM vm,
                                   StaticRegion staticRegion,
                                   gov.nasa.jpf.vm.Instruction instructionToExecute)
                            throws java.lang.Exception

Throws:

java.lang.Exception

isRegionEndOk

private void isRegionEndOk(gov.nasa.jpf.vm.ThreadInfo ti,
                           StaticRegion staticRegion,
                           gov.nasa.jpf.vm.Instruction instructionToExecute)
                    throws StaticRegionException

Throws:

StaticRegionException

keyFromInstructionToExc

private java.lang.String keyFromInstructionToExc(gov.nasa.jpf.vm.Instruction instructionToExecute)

discoverRegions

private void discoverRegions(gov.nasa.jpf.vm.ThreadInfo ti)

isNoVeritesting

private boolean isNoVeritesting(gov.nasa.jpf.vm.StackFrame curr,
                                boolean noVeritestingFlag)

isAllowedRegion

private boolean isAllowedRegion(java.lang.String key)

updateSkipRegions

private void updateSkipRegions(java.lang.String message,
                               java.lang.String key)

runVeritestingWithSPF

private void runVeritestingWithSPF(gov.nasa.jpf.vm.ThreadInfo ti,
                                   gov.nasa.jpf.vm.VM vm,
                                   gov.nasa.jpf.vm.Instruction instructionToExecute,
                                   StaticRegion staticRegion,
                                   java.lang.String key)
                            throws java.lang.Exception

Throws:

java.lang.Exception

threadTerminated

public void threadTerminated(gov.nasa.jpf.vm.VM vm,
                             gov.nasa.jpf.vm.ThreadInfo terminatedThread)

Specified by:

threadTerminated in interface gov.nasa.jpf.vm.VMListener

Overrides:

threadTerminated in class gov.nasa.jpf.PropertyListenerAdapter

threadStarted

public void threadStarted(gov.nasa.jpf.vm.VM vm,
                          gov.nasa.jpf.vm.ThreadInfo startedThread)

Specified by:

threadStarted in interface gov.nasa.jpf.vm.VMListener

Overrides:

threadStarted in class gov.nasa.jpf.PropertyListenerAdapter

choiceGeneratorRegistered

public void choiceGeneratorRegistered(gov.nasa.jpf.vm.VM vm,
                                      gov.nasa.jpf.vm.ChoiceGenerator<?> nextCG,
                                      gov.nasa.jpf.vm.ThreadInfo currentThread,
                                      gov.nasa.jpf.vm.Instruction executedInstruction)

Specified by:

choiceGeneratorRegistered in interface gov.nasa.jpf.vm.VMListener

Overrides:

choiceGeneratorRegistered in class gov.nasa.jpf.PropertyListenerAdapter

stateAdvanced

public void stateAdvanced(gov.nasa.jpf.search.Search search)

Specified by:

stateAdvanced in interface gov.nasa.jpf.search.SearchListener

Overrides:

stateAdvanced in class gov.nasa.jpf.PropertyListenerAdapter

stateBacktracked

public void stateBacktracked(gov.nasa.jpf.search.Search search)

Specified by:

stateBacktracked in interface gov.nasa.jpf.search.SearchListener

Overrides:

stateBacktracked in class gov.nasa.jpf.PropertyListenerAdapter

choiceGeneratorProcessed

public void choiceGeneratorProcessed(gov.nasa.jpf.vm.VM vm,
                                     gov.nasa.jpf.vm.ChoiceGenerator<?> processedCG)

Specified by:

choiceGeneratorProcessed in interface gov.nasa.jpf.vm.VMListener

Overrides:

choiceGeneratorProcessed in class gov.nasa.jpf.PropertyListenerAdapter

runVeritesting

private DynamicRegion runVeritesting(gov.nasa.jpf.vm.ThreadInfo ti,
                                     gov.nasa.jpf.vm.Instruction instructionToExecute,
                                     StaticRegion staticRegion,
                                     java.lang.String key)
                              throws java.lang.Exception

Throws:

java.lang.Exception

setupSPF

public static gov.nasa.jpf.vm.Instruction setupSPF(gov.nasa.jpf.vm.ThreadInfo ti,
                                                   gov.nasa.jpf.vm.Instruction ins,
                                                   DynamicRegion dynRegion,
                                                   java.lang.Integer choice)
                                            throws StaticRegionException

This populates the Output of the summarized region to SPF.

Parameters:

ti - Currently running thread.

ins - Branch instruction that indicates beginning of the region.

dynRegion - Dynamic region that has been summarized.

Throws:

StaticRegionException - Exception to indicate a problem while setting SPF.

pushReturnOnStack

private static void pushReturnOnStack(gov.nasa.jpf.vm.StackFrame sf,
                                      DynamicRegion dynRegion)
                               throws StaticRegionException

Throws:

StaticRegionException

pushExpOnStack

private static void pushExpOnStack(DynamicRegion dynRegion,
                                   gov.nasa.jpf.vm.StackFrame sf,
                                   java.lang.String returnType,
                                   za.ac.sun.cs.green.expr.Expression var)
                            throws StaticRegionException

Throws:

StaticRegionException

canSetPC

private static boolean canSetPC(gov.nasa.jpf.vm.ThreadInfo ti,
                                DynamicRegion dynRegion,
                                java.lang.Integer choice)
                         throws StaticRegionException

This method checks that the current PathCondition and after appending the summarized region is satisfiable.

Parameters:

ti - Currently running thread.

dynRegion - Finaly summary of the region, after all transformations has been successfully completed.

Returns:

PathCondition is still satisfiable or not.

Throws:

StaticRegionException - Exception to indicate a problem while checking SAT of the updated PathCondition.

clearStack

private static void clearStack(gov.nasa.jpf.vm.StackFrame sf,
                               gov.nasa.jpf.vm.Instruction ins)
                        throws StaticRegionException

This pop up operands of the if instruction that begins the region.

Parameters:

sf - Current StackFrame.

ins - Current executing instruction

Throws:

StaticRegionException - Exception to indicate a problem while clearning the stack.

populateSlots

private static void populateSlots(gov.nasa.jpf.vm.ThreadInfo ti,
                                  DynamicRegion dynRegion)

Populates SPF stack slot with the output of the veritesting region.

Parameters:

ti - Current executing thread.

dynRegion - Dynamic region that has been successfully transformed and summarized.

populateFieldOutputs

private static void populateFieldOutputs(gov.nasa.jpf.vm.ThreadInfo ti,
                                         DynamicRegion dynRegion)
                                  throws StaticRegionException

Throws:

StaticRegionException

populateArrayOutputs

private static void populateArrayOutputs(gov.nasa.jpf.vm.ThreadInfo ti,
                                         DynamicRegion dynRegion)
                                  throws StaticRegionException

Throws:

StaticRegionException

advanceSpf

public static gov.nasa.jpf.vm.Instruction advanceSpf(gov.nasa.jpf.vm.Instruction ins,
                                                     DynamicRegion dynRegion,
                                                     boolean earlyReturnSetup)

Steps SPF to the end of the region.

Parameters:

ins - Insturction to be executed.

dynRegion - Dynamic region that has been successfully transformed and summarized.

publishFinished

public void publishFinished(gov.nasa.jpf.report.Publisher publisher)

Specified by:

publishFinished in interface gov.nasa.jpf.report.PublisherExtension

Overrides:

publishFinished in class gov.nasa.jpf.PropertyListenerAdapter

writeRegionDigest

private void writeRegionDigest()

getMetricsVector

private java.lang.String getMetricsVector(long dynRunTime)