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 () |
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.
<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. |
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.
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. |
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.