Writing a WPDS analysis

WPDS is the latest solver for distributive data-flow problems that has been implemented in PhASAR. WPDS is very similar to IDE. Basically, our WPDSSolver implementation is a specialization of the IDESolver. But instead of building an exploded super-graph using the user's flow- and edge function implementations a (weighted) pushdown system is build whose rules are drawn from the user's analysis description. Mathematically, IDE and WPDS are equally powerful but WPDS has some additional neat properties which we will not be able to discuss is this documentation. Each rule in the rule set of the pushdown system corresponds to an edge in the exploded super-graph. The analysis problem---encoded in a pushdown system---is then solved using a stack automaton that is obtained by the post* or pre* algorithm. We use a modified version of the WALi library for that task. The following variants of pushdown systems can be created in our implementation:

• WPDS
• EWPDS
• FWPDS
• SWPDS

In order to write a WPDS analysis one basically needs to write an IDE analysis. The WPDS analysis has its own problem interface WPDSProblem that can be used to encode an WPDS problem. In addition, an existing concrete IDEProblem can be easily transformed into a concrete WPDSProblem as both are distributive problems. Please refer to the WPDSLinearConstantAnalysis for the IDEProblem to WPDSProblem transformation.