Type Domains for Abstract Interpretation : A critical study

Sammanfattning: Programming languages with dynamic typing such as Prolog do not require that the programmer declares the types of data or procedures. This flexibility, however, comes at a price. The lack of declarations makes it hard for a compiler to produce fast code since data must be assumed to be of any type.Abstract interpretation is a technique to automatically infer conservative approximations of program properties such as the types of program variables and procedure arguments. The properties of interest are described using an abstract domain. The abstract domains for type analysis investigated in this thesis are based on deterministic term grammars but differ in the representation of the term grammars and in the widening used, that is, the method used to ensure that the analysis terminates.One proposed representation of term grammars, type graphs, are shown to be exponentially larger than the term grammars they represent not only in the worst case but also in practice. One previously proposed widening for type graphs is shown to be impractically expensive and also no more precise than other more efficient methods. A novel implementation technique is proposed for another type graph widening that appears in the literature. The precision using this implementation technique is shown to be better than for the other investigated widenings. The performance, however, suffers from the problems inherent in the type graph representation unless some crucial modifications to the analyzer are made.To overcome the problems with the type graph representation a more compact representation of term grammars is proposed. A number of widenings using this representation are investigated and shown not to suffer from problems with huge term grammar representations. The precision obtained using these widenings are as good or better than the precision obtained using the original widening proposed for type graphs.Finally, two sets of benchmarks that have been used in the literature to investigate analysis methods are considered. It is shown that these benchmarks will give unrealistically good absolute precision and one set of benchmarks, the GAIA benchmarks, is shown to have further deficiencies that make it completely unsuitable for benchmarking purposes.