The basic idea behind improving the quality of a monovariant control flow analysis such as 0CFAis the concept of polyvariant analyses such as Agesen’s Cartesian Product Algorithm (CPA) and Shivers’ n CFA. In this paper we develop a novel framework for polyvariant flow analysis based on Aiken-Wimmers constrained type theory. We develop instantiations of our framework to formalize various polyvariant algorithms, including nCFA and CPA. With our CPA formalization, we show the call-graph based termination condition for CPA will not always guarantee termination. We then develop a novel termination condition and prove it indeed leads to a terminating algorithm. Additionally, we show how data polymorphism can be modeled in the framework, by defining a simple extension to CPA that incorporates data polymorphism.
CITATION STYLE
Smith, S. F., & Wang, T. (2000). Polyvariant flow analysis with constrained types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1782, pp. 382–396). Springer Verlag. https://doi.org/10.1007/3-540-46425-5_25
Mendeley helps you to discover research relevant for your work.