Tech Report CS-93-13

Conceptual and Software Support for Abstract Domain Design: Generic Structural Domain and Open Product

A. Cortesi, B. Le Charlier and P. Van Hentenryck

April 1993

Abstract:

Abstract interpretation is a systematic methodology to design static program analysis which has been studied extensively in the logic programming community. With the emergence of efficient generic abstract interpretation algorithms for logic programming, the main burden in building an analysis is the abstract domain which gives a safe approximation of the concrete domain of computation. However, accurate abstract domains for logic programming are often complex and complicated. The purpose of this paper is to propose conceptual and software support for the design of abstract domains. It contains two main contributions: a generic pattern domain and the notion of open product of domains. {\em The generic pattern domain} {\tt Pat($\Re$)} automatically upgrades a domain $\Re$ (e.g. {\tt Prop}), with structural information yielding a more accurate domain (e.g. {\tt Pat(Prop)\/}) while abstracting away structural information from the designer. The {\em open product} is a new way of combining abstract domains allowing each combined domain to benefit from information from the other components through the notions of queries and open operations. The open product is general-purpose and can be used for other programming paradigms as well. The two contributions are orthogonal and can be combined in various ways to obtain sophisticated domains while imposing minimal requirements on the designer. Both contributions are characterized theoretically and experimentally and were used to design very complex abstract domains such as {\tt OPAT(OProp$\otimes$OMode$\otimes$OPS)} which would be very difficult to design otherwise. On this last domain, designers need only contribute about 20% (about 3,400 lines) of the complete system (about 17,700 lines).

(complete text in pdf or gzipped postscript)