A symbolic constraint solving framework for analysis of logic programs

Interpretation of logic programs using symbolic constraints has attracted a lot of attention lately since such approaches can yield very elegant formulation of manY analyses. Moreover, the performance of an analysis that uses constraints to represent program properties and symbolic constraint solving techniques to infer them, can be largely insensitive to domain size. However, implementations of these techniques must balance the conflicting requirements of (a) providing efficient constraint solving algorithms for specific constraints, and (b) being general enough to deal with a large class of constraints. We overcome the apparent conflict by implementing the analysis and constraint solving operations in multiple layers such that the top most layer is completely generic. The lower layers become increasingly speciahzed for a particular analysis. Each layer provides a set of operations for the higher layer using the operations provided by the lower layers. Such layering enables us to choose the most efficient rdgorithms appropriate for that layer, independent of the other layers. The critical aspect of this framework is the identification of interfaces between the layers that enables us to modularize not only our algorithms and implementations, but also the proof efforts. Prototype implementation of our framework shows that it scales very well to large domains, and furthermore, compares favorably with existing implementations of other analysis methods.