Public Member Functions

com.google.security.zynamics.binnavi.API.reil.mono.MonotoneSolver< GraphNode, LatticeElement extends ILatticeElement< LatticeElement >, ObjectType, Lattice extends ILattice< LatticeElement, ObjectType > > Class Reference

List of all members.

Public Member Functions

 MonotoneSolver (final ILatticeGraph< GraphNode > graph, final Lattice lattice, final IStateVector< GraphNode, LatticeElement > startVector, final ITransformationProvider< GraphNode, LatticeElement > transformationProvider, final IGraphWalker< GraphNode, ObjectType > walker)
final IStateVector< GraphNode,
LatticeElement > 
solve ()

Detailed Description

The MonotoneSolver class is the base class of the monotone framework. Given a lattice, an instruction graph, an initial state vector, and some other objects the monotone framework tries to propagate information from node to node of the instruction graph until no further information can be deduced from the current program state and the transforming instructions.

Parameters:
<GraphNode> Type of the graph nodes in the given graph.
<Lattice> Type of the lattice the monotone framework is using.
<LatticeElement> Type of the elements of the lattice.
<ObjectType> Type of the additional value objects.

Constructor & Destructor Documentation

com.google.security.zynamics.binnavi.API.reil.mono.MonotoneSolver< GraphNode, LatticeElement extends ILatticeElement< LatticeElement >, ObjectType, Lattice extends ILattice< LatticeElement, ObjectType > >.MonotoneSolver ( final ILatticeGraph< GraphNode >  graph,
final Lattice  lattice,
final IStateVector< GraphNode, LatticeElement >  startVector,
final ITransformationProvider< GraphNode, LatticeElement >  transformationProvider,
final IGraphWalker< GraphNode, ObjectType >  walker 
)

Creates a new instance of a monotone solver.

Parameters:
graph Graph that is being worked on.
lattice Lattice structure that provides the method to merge states.
startVector Initial state vector.
transformationProvider Transforms the state vector during each step of the algorithm.
walker Specifies how to walk through the graph.

Member Function Documentation

final IStateVector<GraphNode, LatticeElement> com.google.security.zynamics.binnavi.API.reil.mono.MonotoneSolver< GraphNode, LatticeElement extends ILatticeElement< LatticeElement >, ObjectType, Lattice extends ILattice< LatticeElement, ObjectType > >.solve (  ) 

Run the actual code analysis.

Starting from the initial state vector, iterate the transformation until a fixpoint is reached.

Depending on your analysis, your transformations and the program you are analyzing, it is conceivable that this will iterate for a long while. If your lattice is infinite and not noetherian (e.g. doesn't fulfill the 'all ascending chains stabilize'), this might not terminate.

Returns:
The fixpoint state.