gov.nasa.jpf.symbc.veritesting.VeritestingUtil

Class SpfUtil

java.lang.Object

gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil

public class SpfUtil
extends java.lang.Object

This class provides some utility methods for SPF.

Field Summary

Fields

Modifier and Type	Field and Description
private static int	operandNum

Constructor Summary

Constructors

Constructor and Description
SpfUtil()

Method Summary

Modifier and Type	Method and Description
static gov.nasa.jpf.symbc.numeric.Expression	createSPFVariableForType(gov.nasa.jpf.vm.StackFrame sf, int variable, java.lang.String varType) This creates SPF constants depending on the type of the variable.
static void	emptyFolder(java.io.File folder)
static gov.nasa.jpf.symbc.numeric.Comparator	getComparator(gov.nasa.jpf.vm.Instruction instruction)
private static za.ac.sun.cs.green.expr.Expression	getFirstCond(Stmt stmt)
static gov.nasa.jpf.symbc.numeric.Comparator	getNegComparator(gov.nasa.jpf.vm.Instruction instruction)
static int	getOperandNumber(java.lang.String instruction) Returns number of operands depending on the if-bytecode instruction.
private static boolean	isBothSidesFeasible(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.symbc.numeric.Comparator cmp, gov.nasa.jpf.symbc.numeric.Comparator negCmp, gov.nasa.jpf.symbc.numeric.Expression op1, gov.nasa.jpf.symbc.numeric.Expression op2)
static boolean	isIncrementalSolver()
static boolean	isStackConsumingRegionEnd(gov.nasa.jpf.vm.ThreadInfo ti, StaticRegion region, gov.nasa.jpf.vm.Instruction ins)
static boolean	isSymCond(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction ins) Checks if the "if" condition is symbolic based on the the operands of the "if" bytecode instruction.
static boolean	isSymCond(gov.nasa.jpf.vm.ThreadInfo ti, Stmt stmt, SlotParamTable slotParamTable, gov.nasa.jpf.vm.Instruction ins) Checks if the "if" condition is symbolic by visiting the condition expression of the statement of the staticRegion
static void	maybeParseConstraint(gov.nasa.jpf.symbc.numeric.PathCondition pc)

Methods inherited from class java.lang.Object

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

Field Detail

operandNum

private static int operandNum

Constructor Detail

SpfUtil

public SpfUtil()

Method Detail

getOperandNumber

public static int getOperandNumber(java.lang.String instruction)

Returns number of operands depending on the if-bytecode instruction.

Parameters:

instruction"if" - bytecode instruction

Returns:

Number of operands.

Throws:

StaticRegionException

isSymCond

public static boolean isSymCond(gov.nasa.jpf.vm.ThreadInfo ti,
                                gov.nasa.jpf.vm.Instruction ins)

Checks if the "if" condition is symbolic based on the the operands of the "if" bytecode instruction.

Parameters:

ti - Current ThreadInfo object

ins - Current "if" bytecode instruction.

Returns:

True if the operand(s) of "if" condition is symbolic and false if it was concerete.

Throws:

StaticRegionException

isBothSidesFeasible

private static boolean isBothSidesFeasible(gov.nasa.jpf.vm.ThreadInfo ti,
                                           gov.nasa.jpf.symbc.numeric.Comparator cmp,
                                           gov.nasa.jpf.symbc.numeric.Comparator negCmp,
                                           gov.nasa.jpf.symbc.numeric.Expression op1,
                                           gov.nasa.jpf.symbc.numeric.Expression op2)

isSymCond

public static boolean isSymCond(gov.nasa.jpf.vm.ThreadInfo ti,
                                Stmt stmt,
                                SlotParamTable slotParamTable,
                                gov.nasa.jpf.vm.Instruction ins)
                         throws StaticRegionException

Checks if the "if" condition is symbolic by visiting the condition expression of the statement of the staticRegion

Parameters:

ti - Current ThreadInfo object

stmt - Statement of the static region.

Returns:

True if the operand(s) of "if" condition is symbolic and false if it was concerete.

Throws:

StaticRegionException

getFirstCond

private static za.ac.sun.cs.green.expr.Expression getFirstCond(Stmt stmt)

createSPFVariableForType

public static gov.nasa.jpf.symbc.numeric.Expression createSPFVariableForType(gov.nasa.jpf.vm.StackFrame sf,
                                                                             int variable,
                                                                             java.lang.String varType)
                                                                      throws StaticRegionException

This creates SPF constants depending on the type of the variable.

Parameters:

sf - Current Stack Frame

variable - Variable number for which we want to create the constant.

varType - The type of which the constant should be created in SPF.

Returns:

SPF constant expression..

Throws:

StaticRegionException

emptyFolder

public static void emptyFolder(java.io.File folder)

getComparator

public static gov.nasa.jpf.symbc.numeric.Comparator getComparator(gov.nasa.jpf.vm.Instruction instruction)

getNegComparator

public static gov.nasa.jpf.symbc.numeric.Comparator getNegComparator(gov.nasa.jpf.vm.Instruction instruction)

isStackConsumingRegionEnd

public static boolean isStackConsumingRegionEnd(gov.nasa.jpf.vm.ThreadInfo ti,
                                                StaticRegion region,
                                                gov.nasa.jpf.vm.Instruction ins)
                                         throws StaticRegionException

Throws:

StaticRegionException

isIncrementalSolver

public static boolean isIncrementalSolver()

maybeParseConstraint

public static void maybeParseConstraint(gov.nasa.jpf.symbc.numeric.PathCondition pc)
                                 throws StaticRegionException

Throws:

StaticRegionException