heros.solver

Class BiDiIDESolver<N,D,M,V,I extends InterproceduralCFG<N,M>>

java.lang.Object

heros.solver.BiDiIDESolver<N,D,M,V,I>

Type Parameters:

N - see IFDSSolver

D - A data-flow abstraction that must implement the LinkedNode interface such that data-flow values can be linked to form reportable paths.

M - see IFDSSolver

I - see IFDSSolver

Direct Known Subclasses:

BiDiIFDSSolver

public class BiDiIDESolver<N,D,M,V,I extends InterproceduralCFG<N,M>>
extends java.lang.Object

This is a special IFDS solver that solves the analysis problem inside out, i.e., from further down the call stack to further up the call stack. This can be useful, for instance, for taint analysis problems that track flows in two directions. The solver is instantiated with two analyses, one to be computed forward and one to be computed backward. Both analysis problems must be unbalanced, i.e., must return true for SolverConfiguration.followReturnsPastSeeds(). The solver then executes both analyses in lockstep, i.e., when one of the analyses reaches an unbalanced return edge (signified by a ZERO source value) then the solver pauses this analysis until the other analysis reaches the same unbalanced return (if ever). The result is that the analyses will never diverge, i.e., will ultimately always only propagate into contexts in which both their computed paths are realizable at the same time. This solver requires data-flow abstractions that implement the LinkedNode interface such that data-flow values can be linked to form reportable paths.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
class	BiDiIDESolver.AbstractionWithSourceStmt This is an augmented abstraction propagated by the BiDiIDESolver.SingleDirectionSolver.
protected class	BiDiIDESolver.SingleDirectionSolver This is a modified IFDS solver that is capable of pausing and unpausing return-flow edges.

Field Summary

Fields

Modifier and Type	Field and Description
protected BiDiIDESolver.SingleDirectionSolver	bwSolver
protected BiDiIDESolver.SingleDirectionSolver	fwSolver

Constructor Summary

Constructors

Constructor and Description
BiDiIDESolver(IDETabulationProblem<N,D,M,V,I> forwardProblem, IDETabulationProblem<N,D,M,V,I> backwardProblem) Instantiates a BiDiIDESolver with the associated forward and backward problem.

Method Summary

Modifier and Type	Method and Description
protected BiDiIDESolver.SingleDirectionSolver	createSingleDirectionSolver(IDETabulationProblem<N,BiDiIDESolver.AbstractionWithSourceStmt,M,V,I> problem, java.lang.String debugName) Creates a solver to be used for each single analysis direction.
void	solve()

Methods inherited from class java.lang.Object

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

Field Detail

fwSolver

protected BiDiIDESolver.SingleDirectionSolver fwSolver

bwSolver

protected BiDiIDESolver.SingleDirectionSolver bwSolver

Constructor Detail

BiDiIDESolver

public BiDiIDESolver(IDETabulationProblem<N,D,M,V,I> forwardProblem,
                     IDETabulationProblem<N,D,M,V,I> backwardProblem)

Instantiates a BiDiIDESolver with the associated forward and backward problem.

Method Detail

solve

public void solve()

createSingleDirectionSolver

protected BiDiIDESolver.SingleDirectionSolver createSingleDirectionSolver(IDETabulationProblem<N,BiDiIDESolver.AbstractionWithSourceStmt,M,V,I> problem,
                                                                          java.lang.String debugName)

Creates a solver to be used for each single analysis direction.