gov.nasa.jpf.vm

Class Verify

java.lang.Object

gov.nasa.jpf.vm.Verify

public class Verify
extends java.lang.Object

Verify is the programmatic interface of JPF that can be used from inside of applications. In order to enable programs to run outside of the JPF environment, we provide (mostly empty) bodies for the methods that are otherwise intercepted by the native peer class

Field Summary

Fields

Modifier and Type	Field and Description
static int	FINE
static int	FINER
static int	FINEST
static int	INFO
static int	NO_VALUE
static int	SEVERE
static int	WARNING

Constructor Summary

Constructors

Constructor and Description
Verify()

Method Summary

Modifier and Type	Method and Description
static void	addComment(java.lang.String s) Adds a comment to the error trace, which will be printed and saved.
static void	addElementAttribute(java.lang.Object arr, int idx, int val)
static void	addFieldAttribute(java.lang.Object o, java.lang.String fieldName, int val)
static void	addLocalAttribute(java.lang.String varName, int val)
static void	addObjectAttribute(java.lang.Object o, int val)
static void	assertTrue(boolean cond) Deprecated. use 'assert' directly
static void	assertTrue(java.lang.String s, boolean cond) Deprecated. use "assert cond : msg"
static void	atLabel(int label)
static void	atLabel(java.lang.String label)
static void	beginAtomic() Marks the beginning of an atomic block.
static void	boring(boolean cond)
static void	breakTransition(java.lang.String reason)
static int	breakTransition(java.lang.String reason, int min, int max) for testing and debugging purposes
static void	busyWait(long duration)
static <T> T	createFromJSON(java.lang.Class<T> clazz, java.lang.String json)
static long	currentTimeMillis()
static void	endAtomic() Marks the end of an atomic block.
static void	freezeSharedness(java.lang.Object o, boolean freeze)
static boolean	getBitInBitSet(int id, int bit)
static boolean	getBoolean() this is the new boolean choice generator.
static boolean	getBoolean(boolean falseFirst) new boolean choice generator that also tells jpf which value to use first by default in a search.
static int	getCounter(int id)
static double	getDouble(java.lang.String key) this is the API for double value choice generators.
static double	getDoubleFromList(double... values)
static int	getElementAttribute(java.lang.Object arr, int idx)
static int[]	getElementAttributes(java.lang.Object arr, int idx)
static int	getFieldAttribute(java.lang.Object o, java.lang.String fieldName)
static int[]	getFieldAttributes(java.lang.Object o, java.lang.String fieldName)
static float	getFloatFromList(float... values)
static int	getHeuristicSearchValue()
static int	getInt(int min, int max) Returns int nondeterministically between (and including) min and max.
static int	getInt(java.lang.String key) this is the API for int value choice generators.
static int	getIntFromList(int... values)
static int	getLocalAttribute(java.lang.String varName)
static int[]	getLocalAttributes(java.lang.String varName)
static long	getLongFromList(long... values)
static java.lang.Object	getObject(java.lang.String key)
static int	getObjectAttribute(java.lang.Object o)
static int[]	getObjectAttributes(java.lang.Object o)
static java.lang.String	getProperty(java.lang.String key)
static int	getValue(java.lang.String key)
static void	ignoreIf(boolean cond)
static int	incrementCounter(int id)
static void	instrumentPoint(java.lang.String label)
static void	instrumentPointDeep(java.lang.String label)
static void	instrumentPointDeepRecur(java.lang.String label, int depth)
static void	interesting(boolean cond)
static boolean	isCalledFromClass(java.lang.String refClsName)
static boolean	isRunningInJPF()
static boolean	isShared(java.lang.Object o)
static boolean	isTraceReplay()
static void	log(java.lang.String loggerId, int logLevel, java.lang.String msg)
static void	log(java.lang.String loggerId, int logLevel, java.lang.String format, java.lang.Object... args)
static void	log(java.lang.String loggerId, int logLevel, java.lang.String msg, java.lang.String arg)
static void	print(java.lang.String... args) this is to avoid StringBuilders
static void	print(java.lang.String s)
static void	print(java.lang.String s, boolean b)
static void	print(java.lang.String s, int i)
static void	println()
static void	println(java.lang.String s)
static void	printPathOutput(boolean cond, java.lang.String msg)
static void	printPathOutput(java.lang.String msg) simple debugging aids to imperatively print the current path output of the SUT (to be used with vm.path_output)
static void	putValue(java.lang.String key, int value)
static int	random(int max) Returns a random number between 0 and max inclusive.
static boolean	randomBool() Returns a random boolean value, true or false.
static java.lang.Object	randomObject(java.lang.String type)
static <T> T	readObjectFromFile(java.lang.Class<T> clazz, java.lang.String fileName)
static void	resetCounter(int id)
static void	resetHeuristicSearchValue()
static void	setBitInBitSet(int id, int bit, boolean value)
static void	setCounter(int id, int val)
static void	setElementAttribute(java.lang.Object arr, int idx, int val)
static void	setFieldAttribute(java.lang.Object o, java.lang.String fieldName, int val) note - these are mostly for debugging purposes (to see if attributes get propagated correctly, w/o having to write a listener), since attributes are supposed to be created at the native side, and hence can't be accessed from the application
static void	setHeuristicSearchValue(int n)
static void	setLocalAttribute(java.lang.String varName, int val)
static void	setObjectAttribute(java.lang.Object o, int val)
static void	setPeerClass(java.lang.Class<?> cls)
static void	setProperties(java.lang.String... p)
static void	setShared(java.lang.Object o, boolean isShared)
static void	storeTrace(java.lang.String fileName, java.lang.String comment)
static void	storeTraceAndTerminate(java.lang.String fileName, java.lang.String comment)
static void	storeTraceAndTerminateIf(boolean cond, java.lang.String fileName, java.lang.String comment)
static void	storeTraceIf(boolean cond, java.lang.String fileName, java.lang.String comment)
static void	terminateSearch()
static void	threadPrint(java.lang.String s)
static void	threadPrintln(java.lang.String s)
static boolean	vmIsMatchingStates() USE CAREFULLY - returns true if the virtual machine this code is running under is doing state matching.
static void	writeObjectToFile(java.lang.Object object, java.lang.String fileName)

Methods inherited from class java.lang.Object

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

Field Detail

NO_VALUE

public static final int NO_VALUE

See Also:

Constant Field Values

SEVERE

public static final int SEVERE

See Also:

Constant Field Values

WARNING

public static final int WARNING

See Also:

Constant Field Values

INFO

public static final int INFO

See Also:

Constant Field Values

FINE

public static final int FINE

See Also:

Constant Field Values

FINER

public static final int FINER

See Also:

Constant Field Values

FINEST

public static final int FINEST

See Also:

Constant Field Values

Constructor Detail

Verify

public Verify()

Method Detail

setPeerClass

public static void setPeerClass(java.lang.Class<?> cls)

getCounter

public static int getCounter(int id)

resetCounter

public static void resetCounter(int id)

setCounter

public static void setCounter(int id,
                              int val)

incrementCounter

public static int incrementCounter(int id)

putValue

public static void putValue(java.lang.String key,
                            int value)

getValue

public static int getValue(java.lang.String key)

setBitInBitSet

public static void setBitInBitSet(int id,
                                  int bit,
                                  boolean value)

getBitInBitSet

public static boolean getBitInBitSet(int id,
                                     int bit)

addComment

public static void addComment(java.lang.String s)

Adds a comment to the error trace, which will be printed and saved.

assertTrue

@Deprecated
public static void assertTrue(java.lang.String s,
                                          boolean cond)

Deprecated. use "assert cond : msg"

Backwards compatibility START

assertTrue

@Deprecated
public static void assertTrue(boolean cond)

Deprecated. use 'assert' directly

Checks that the condition is true.

atLabel

public static void atLabel(java.lang.String label)

atLabel

public static void atLabel(int label)

beginAtomic

public static void beginAtomic()

Marks the beginning of an atomic block. THIS IS EVIL, DON'T USE IT FOR OPTIMIZATION - THAT'S WHAT POR IS FOR! (it's mostly here to support model classes that need to execute atomic)

endAtomic

public static void endAtomic()

Marks the end of an atomic block. EVIL - see beginAtomic()

boring

public static void boring(boolean cond)

busyWait

public static void busyWait(long duration)

isCalledFromClass

public static boolean isCalledFromClass(java.lang.String refClsName)

ignoreIf

public static void ignoreIf(boolean cond)

instrumentPoint

public static void instrumentPoint(java.lang.String label)

instrumentPointDeep

public static void instrumentPointDeep(java.lang.String label)

instrumentPointDeepRecur

public static void instrumentPointDeepRecur(java.lang.String label,
                                            int depth)

interesting

public static void interesting(boolean cond)

breakTransition

public static void breakTransition(java.lang.String reason)

breakTransition

public static int breakTransition(java.lang.String reason,
                                  int min,
                                  int max)

for testing and debugging purposes

printPathOutput

public static void printPathOutput(java.lang.String msg)

simple debugging aids to imperatively print the current path output of the SUT (to be used with vm.path_output)

printPathOutput

public static void printPathOutput(boolean cond,
                                   java.lang.String msg)

threadPrint

public static void threadPrint(java.lang.String s)

threadPrintln

public static void threadPrintln(java.lang.String s)

print

public static void print(java.lang.String s)

println

public static void println(java.lang.String s)

print

public static void print(java.lang.String s,
                         int i)

print

public static void print(java.lang.String s,
                         boolean b)

println

public static void println()

print

public static void print(java.lang.String... args)

this is to avoid StringBuilders

setFieldAttribute

public static void setFieldAttribute(java.lang.Object o,
                                     java.lang.String fieldName,
                                     int val)

note - these are mostly for debugging purposes (to see if attributes get propagated correctly, w/o having to write a listener), since attributes are supposed to be created at the native side, and hence can't be accessed from the application

getFieldAttribute

public static int getFieldAttribute(java.lang.Object o,
                                    java.lang.String fieldName)

addFieldAttribute

public static void addFieldAttribute(java.lang.Object o,
                                     java.lang.String fieldName,
                                     int val)

getFieldAttributes

public static int[] getFieldAttributes(java.lang.Object o,
                                       java.lang.String fieldName)

setLocalAttribute

public static void setLocalAttribute(java.lang.String varName,
                                     int val)

getLocalAttribute

public static int getLocalAttribute(java.lang.String varName)

addLocalAttribute

public static void addLocalAttribute(java.lang.String varName,
                                     int val)

getLocalAttributes

public static int[] getLocalAttributes(java.lang.String varName)

setElementAttribute

public static void setElementAttribute(java.lang.Object arr,
                                       int idx,
                                       int val)

getElementAttribute

public static int getElementAttribute(java.lang.Object arr,
                                      int idx)

addElementAttribute

public static void addElementAttribute(java.lang.Object arr,
                                       int idx,
                                       int val)

getElementAttributes

public static int[] getElementAttributes(java.lang.Object arr,
                                         int idx)

setObjectAttribute

public static void setObjectAttribute(java.lang.Object o,
                                      int val)

getObjectAttribute

public static int getObjectAttribute(java.lang.Object o)

addObjectAttribute

public static void addObjectAttribute(java.lang.Object o,
                                      int val)

getObjectAttributes

public static int[] getObjectAttributes(java.lang.Object o)

getBoolean

public static boolean getBoolean()

this is the new boolean choice generator. Since there's no real heuristic involved with boolean values, we skip the id (it's a hardwired "boolean")

getBoolean

public static boolean getBoolean(boolean falseFirst)

new boolean choice generator that also tells jpf which value to use first by default in a search.

getInt

public static int getInt(int min,
                         int max)

Returns int nondeterministically between (and including) min and max.

getIntFromList

public static int getIntFromList(int... values)

getObject

public static java.lang.Object getObject(java.lang.String key)

getInt

public static int getInt(java.lang.String key)

this is the API for int value choice generators. 'id' is used to identify both the corresponding ChoiceGenerator subclass, and the application specific ctor parameters from the normal JPF configuration mechanism

getDouble

public static double getDouble(java.lang.String key)

this is the API for double value choice generators. 'id' is used to identify both the corresponding ChoiceGenerator subclass, and the application specific ctor parameters from the normal JPF configuration mechanism

getDoubleFromList

public static double getDoubleFromList(double... values)

getLongFromList

public static long getLongFromList(long... values)

getFloatFromList

public static float getFloatFromList(float... values)

random

public static int random(int max)

Returns a random number between 0 and max inclusive.

randomBool

public static boolean randomBool()

Returns a random boolean value, true or false. Note this gets handled by the native peer, and is just here to enable running instrumented applications w/o JPF

currentTimeMillis

public static long currentTimeMillis()

randomObject

public static java.lang.Object randomObject(java.lang.String type)

isRunningInJPF

public static boolean isRunningInJPF()

vmIsMatchingStates

public static boolean vmIsMatchingStates()

USE CAREFULLY - returns true if the virtual machine this code is running under is doing state matching. This can be used as a hint as to whether data structures (that are known to be correct!) should be configured to use a canonical representation. For example,

 Vector v = new Vector();
 v.add(obj1);
 if (Verify.getBoolean()) {
     v.addAll(eleventyBillionObjectCollection);
     v.setSize(1);
 }
 // compare states here
 

To the programmer, the states are (almost certainly) the same. To the VM, they could be different (capacity inside the Vector). For the sake of speed, Vector does not store things canonically, but this can cause (probably mild) state explosion if matching states. If you know whether states are being matched, you can choose the right structure--as long as those structures aren't what you're looking for bugs in!

storeTrace

public static void storeTrace(java.lang.String fileName,
                              java.lang.String comment)

storeTraceIf

public static void storeTraceIf(boolean cond,
                                java.lang.String fileName,
                                java.lang.String comment)

storeTraceAndTerminate

public static void storeTraceAndTerminate(java.lang.String fileName,
                                          java.lang.String comment)

storeTraceAndTerminateIf

public static void storeTraceAndTerminateIf(boolean cond,
                                            java.lang.String fileName,
                                            java.lang.String comment)

isTraceReplay

public static boolean isTraceReplay()

isShared

public static boolean isShared(java.lang.Object o)

setShared

public static void setShared(java.lang.Object o,
                             boolean isShared)

freezeSharedness

public static void freezeSharedness(java.lang.Object o,
                                    boolean freeze)

terminateSearch

public static void terminateSearch()

setHeuristicSearchValue

public static void setHeuristicSearchValue(int n)

resetHeuristicSearchValue

public static void resetHeuristicSearchValue()

getHeuristicSearchValue

public static int getHeuristicSearchValue()

setProperties

public static void setProperties(java.lang.String... p)

getProperty

public static java.lang.String getProperty(java.lang.String key)

createFromJSON

public static <T> T createFromJSON(java.lang.Class<T> clazz,
                                   java.lang.String json)

writeObjectToFile

public static void writeObjectToFile(java.lang.Object object,
                                     java.lang.String fileName)

readObjectFromFile

public static <T> T readObjectFromFile(java.lang.Class<T> clazz,
                                       java.lang.String fileName)

log

public static void log(java.lang.String loggerId,
                       int logLevel,
                       java.lang.String msg)

log

public static void log(java.lang.String loggerId,
                       int logLevel,
                       java.lang.String msg,
                       java.lang.String arg)

log

public static void log(java.lang.String loggerId,
                       int logLevel,
                       java.lang.String format,
                       java.lang.Object... args)