TOWARDS A TOOL KIT FOR THE AUTOMATIC-GENERATION OF INTERPROCEDURAL DATA-FLOW ANALYSES

Frameworks for interprocedural data how analysis (DFA) often have a fo undational character: designing concrete applications requires usually a deep understanding of the framework. Here, we reconsider interproce dural DFA from an application-oriented point of view, where all detail s irrelevant for application are hidden. In this view the underlying f ramework, which captures programs with mutually recursive procedures, global and local variables, formal value and reference parameters, red uces to a cookbook of (1) how to specify interprocedural DFAs and (2) how to prove them precise with respect to a program property of intere st. Thus only knowledge about the specification level is required. Mor eover, this presentation also yields the basis for a tool kit implemen tation: specification parameters and generic algorithms of the framewo rk become specification tools allowing concise specifications and comp utation tools processing them. A tool kit prototype has been implement ed within METAFrame, a programming environment for the construction an d verification of complex software systems. The benefits of the approa ch are demonstrated by a collection of practically relevant precise in terprocedural DFAs ranging from classical bit-vector problems such as available expressions and live variables to sophisticated and powerful optimizations like the optimal elimination of interprocedural partial redundancies.