Tech Report CS-93-05
Abstract Interpretation of Prolog Based on OLDT Resolution
Pascal Van Hentenryck, Oliver Degimbe, Baudouin Le Charlier and Laurent Michel
OLDT resolution as a basis for abstract interpretation is a recurring theme in logic programming and was proposed by many authors because of its completeness properties for various classes of programs. In addition, an interesting property of OLDT resolution for abstract interpretation is the very fine granularity it provides for the analysis. This comes from the fact that OLDT resolution associates with each input pair a set of output abstract substitutions, unlike most algorithms which store a single abstract substitution per input pair by using, say, least-upper-bound operation. However, despite its popularity, no experimental results are available on the accuracy and efficiency of OLDT resolution for abstract interpretation.
This paper is a systematic study of OLDT resolution for abstract interpretation from the semantic framework to an efficient fixpoint algorithm and its experimental evaluation. The semantic framework demonstrates that pure OLDT resolution is not an appropriate setting for abstract interpretation and proposes an appropriate foundation using the idea of output subsumption. The algorithmic framework presents an efficient fixpoint algorithm by successive refinements. The algorithm includes optimizations such as the caching of abstract operations, output subsumption, and the use of sophisticated dependencies to avoid redundant computations. Comprehensive experimental results on the accuracy and efficiency of the algorithm are presented, using a finite and infinite abstract domain. The algorithm is also compared to other algorithms, working at a coarser granularity. Choices and variations of the algorithm are also carefully studied, including the impact of caching, dependencies, output subsumption, widening, and generalization. The results shed new light on the usefulness of OLDT resolution for abstract interpretation and the impact of granularity in abstract interpretation of logic programs.