de.rwth.dfa.jvm
Interface Abstraction

All Known Implementing Classes:

AbstractSSDependingAbstraction, CPAbstraction, CFPAbstraction, SSAbstraction, LVAbstraction

public interface Abstraction

An interface for describing an abstract model of JVM execution. It describes everything which is necessary to do data flow analysis on JVM byte code.

Version:

$Id: Abstraction.java,v 1.2 2002/09/17 06:53:53 mohnen Exp $

Author:

Markus Mohnen

Inner Class Summary

static class

Abstraction.Default Container class for default implementations of methods.

Field Summary

static int	DIRECTION_BACKWARD The constant DIRECTION_BACKWARD may be used as result of getDirection() to indicate backward control flow.
static int	DIRECTION_FORWARD The constant DIRECTION_FORWARD may be used as result of getDirection() to indicate forward control flow.
static int	QUANTIFIER_ALL The constant QUANTIFIER_ALL may be used as result of getQuantifier() to indicate universal quantification.
static int	QUANTIFIER_EXISTS The constant QUANTIFIER_EXISTS may be used as result of getQuantifier() to indicate existential quantification.

Method Summary

Function	getAbstract(de.fub.bytecode.generic.InstructionHandle ih) Returns the transfer function associated by this abstraction with an instruction in a method.
Function	getAbstract(InstructionHandleVector ihv) Returns the transfer function associated by this abstraction with a sequence of JVM instructions without jumps in a method.
int	getDirection() Returns the direction of control flow in this abstraction.
java.lang.Object	getInitialValue(de.fub.bytecode.generic.InstructionHandle ih, boolean isEntry) For a JVM instruction in a method, it returns the initial value of the computations.
java.lang.Object	getInitialValue(InstructionHandleVector ihs, boolean isEntry) For a sequence of JVM instructions without jumps in a method, it returns the initial value of the computations.
Lattice	getLattice() Returns the lattice used to do all computations.
int	getQuantifier() Returns the quantification of this abstraction.

Field Detail

DIRECTION_FORWARD

public static final int DIRECTION_FORWARD

The constant DIRECTION_FORWARD may be used as result of getDirection() to indicate forward control flow.

DIRECTION_BACKWARD

public static final int DIRECTION_BACKWARD

The constant DIRECTION_BACKWARD may be used as result of getDirection() to indicate backward control flow.

QUANTIFIER_ALL

public static final int QUANTIFIER_ALL

The constant QUANTIFIER_ALL may be used as result of getQuantifier() to indicate universal quantification.

QUANTIFIER_EXISTS

public static final int QUANTIFIER_EXISTS

The constant QUANTIFIER_EXISTS may be used as result of getQuantifier() to indicate existential quantification.

Method Detail

getLattice

public Lattice getLattice()

Returns the lattice used to do all computations.

Returns:

a Lattice value

getInitialValue

public java.lang.Object getInitialValue(de.fub.bytecode.generic.InstructionHandle ih,
                                        boolean isEntry)

For a JVM instruction in a method, it returns the initial value of the computations. It must be an element of the lattice of this abstraction.

In addition to the classes defined in the BCEL API, the instruction handle may also be an instance of ExceptionHeaderInstructionHandle. This pseudo instruction is inserted before the first real instruction of an exception handler. If the operand stack state of the real JVM execution is modeled by this abstraction, the pseudo instruction must be used to make the abstract value represent a state with a stack with only a non null reference to an exception as the only entry.

Parameters:

ih - an InstructionHandle value

isEntry - a boolean value: true if this instruction is an entry with respect to the direction of control flow.

Returns:

an Object value

getInitialValue

public java.lang.Object getInitialValue(InstructionHandleVector ihs,
                                        boolean isEntry)

For a sequence of JVM instructions without jumps in a method, it returns the initial value of the computations. It must be an element of the lattice of this abstraction.

Parameters:

ihs - an InstructionHandleVector value

isEntry - a boolean value: true if this instruction is an entry with respect to the direction of control flow.

Returns:

an Object value

See Also:

Abstraction.Default

getDirection

public int getDirection()

Returns the direction of control flow in this abstraction. For forward flow, the entry point of a method is considered to be the entry of the data flow analysis. For backward flow, the exit points are considerer as entries.

Returns:

an int value: Either DIRECTION_FORWARD or DIRECTION_BACKWARD.

getQuantifier

public int getQuantifier()

Returns the quantification of this abstraction. For universal quantification, the meet operation of the lattice is used to combine values at point where controls flows merge. For existential quantification, the join operation of the lattice is used.

Returns:

an int value: Either QUANTIFIER_ALL or QUANTIFIER_EXISTS.

getAbstract

public Function getAbstract(de.fub.bytecode.generic.InstructionHandle ih)

Returns the transfer function associated by this abstraction with an instruction in a method. It must be a endomorphism on the lattice used by this abstraction. Furthermore, it must be a monotone function! Otherwise, the computation may not terminate.

Parameters:

ih - an InstructionHandle value

Returns:

a Function value

getAbstract

public Function getAbstract(InstructionHandleVector ihv)

Returns the transfer function associated by this abstraction with a sequence of JVM instructions without jumps in a method. It must be a endomorphism on the lattice used by this abstraction. Furthermore, it must be a monotone function! Otherwise, the computation may not terminate.

Parameters:

ih - an InstructionHandle value

Returns:

a Function value

See Also:

Abstraction.Default