Formal language, grammar and set-constraint-based program analysis by abstract interpretation
Patrick M. Cousot, Radhia Cousot · 1995
Grammar-based program analysis à la Jones and Muchnick and set-constraint-based program analysis à la Aiken and Heintze are static analysis techniques that have traditionally been seen as quite different from abstract-interpretation-based analyses, in particular because of their apparent non-iterative nature. For example, on page 18 of N. Heintze thesis, it is alleged that ``The finitary nature of abstract interpretation implies that there is a fundamental limitation on the accuracy of this approach to program analysis. There are decidable kinds of analysis that cannot be computed using abstract interpretation (even with widening and narrowing). The set-based analysis considered in this thesis is one example''. On the contrary, we show that grammar and set-constraint-based program analyses are similar abstract interpretations with iterative fixpoint computation using either a widening or a finitary grammar/set-constraints transformer or even a finite domain for each particular program. The understanding of grammar-based and set-constraint-based program analysis as a particular instance of abstract interpretation of a semantics has several advantages. First, the approximation process is formalized and not only explained using examples. Second, a domain of abstract properties is exhibited which is of general scope. Third, these analyses can be easily combined with other abstract-interpretation-based analyses, in particular for the analysis of numerical values. Fourth, they can be generalized to very powerful attribute-dependent and context-dependent analyses. Finally, a few misunderstandings may be removed.