Combinations of abstract domains for logic programming: open product and generic pattern construction

Citation
A. Cortesi et al., Combinations of abstract domains for logic programming: open product and generic pattern construction, SCI COMP PR, 38(1-3), 2000, pp. 27-71
Citations number
61
Categorie Soggetti
Computer Science & Engineering
Journal title
SCIENCE OF COMPUTER PROGRAMMING
ISSN journal
01676423 → ACNP
Volume
38
Issue
1-3
Year of publication
2000
Pages
27 - 71
Database
ISI
SICI code
0167-6423(200008)38:1-3<27:COADFL>2.0.ZU;2-S
Abstract
Abstract interpretation is a systematic methodology to design static progra m analysis which has been studied extensively in the logic programming comm unity, because of the potential for optimizations in logic programming comp ilers and the sophistication of the analyses which require conceptual suppo rt. With the emergence of efficient generic abstract interpretation algorit hms for logic programming, the main burden in building an analysis is the a bstract domain which gives a safe approximation of the concrete domain of c omputation. However, accurate abstract domains for logic programming are of ten complex not only because of the relational nature of logic programming languages and of their typical interprocedural control-flow, but also becau se of the variety of analyses to perform, their interdependence, and the ne ed to maintain structural information. The purpose of this paper is to prop ose conceptual and software support for the design of abstract domains. It contains two main contributions: the notion of open product and a generic p attern domain. The open product is a new, language independent, way of comb ining abstract domains allowing each combined domain to benefit from inform ation from the other components through the notions of queries and open ope rations. It provides a framework to approximate Cousots' reduced product, w hile reusing existing implementations and providing methodological guidance on how to build domains for interaction and composition. It is orthogonal and complementary to Granger's product which improves the direct product by a decreasing iteration sequence based on refinements but lets the domains interact only after the individual operations. The generic pattern domain P at(R) automatically upgrades a domain D with structural information yieldin g a more accurate domain Pat(D) without additional design or implementation cost. 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 exper imentally and were used to design very complex abstract domains such as PBT (OPos x OMode x OPS) which would be very difficult to design otherwise. On this last domain, designers need only contribute about 20% (about 3400 line s) of the complete system (about 17,700 lines). (C) 2000 Published by Elsev ier Science B.V. All rights reserved.