Static Analysis of Logic Programs Using CLP as a Meta-language

Huseyin Saglam, John Gallagher, Static Analysis of Logic Programs Using CLP as a Meta-language. CSTR-96-003, Department of Computer Science, University of Bristol. June 1996. PDF, 224 Kbytes.


The tools for analysing logic programs presented here support a systematic method for constructing static analyses. The basic approach and some implementation experiments were described in previous papers iteGallagher-Boulanger-Saglam-ILPS95, iteGallagher-WAILL, iteBoB94, iteBoBD94. Briefly, the method includes the following steps. First the functions and constants of the language of the program to be analysed are given an interpretation into a domain of values representing properties (a pre-interpretation of the language); second, abstract compilation with respect to the pre-interpretation transforms the program into a ``domain program"; third, (an approximation to) the standard model of the domain program is computed. In addition to these steps, various program transformations may be used to simulate goal-directed analysis and improve precision. The methods described in iteGallagher-Boulanger-Saglam-ILPS95 and iteGallagher-WAILL are extended by introducing constraint logic programs as the meta-language for describing pre-interpretations, rather than simple Datalog programs as before. Pre-interpretations with respect to arithmetic domains thus become possible. This implies that the domain program can be a constraint logic program of arbitrary complexity, and so the main practical concern is to compute reasonably precise approximate models of constraint logic programs. The flexibility of the approach is illustrated, showing how well-known approximations such as convex polyhedra can be combined with other constraints. A prototype implementation, with simplified handling of some operations on convex polyhedra, and some examples are included.

Bibtex entry.

Publication Admin