Differential methods in logic program analysis

AbstractProgram analysis based on abstract interpretation has proven very useful in compilation of constraint and logic programming languages. Unfortunately, the traditional goal-dependent framework is inherently imprecise. This is because it handles call and return in such a way that dataflow information may be re-asserted unnecessarily, leading to a loss of precision for many description domains. For a few specific domains, the literature contains proposals to overcome the problem, and some implementations use various unpublished tricks that sometimes avoid the precision loss. The purpose of this paper is to map the landscape of goal-dependent, goal-independent, and combined approaches to generic analysis of logic programs. This includes formalising existing methods and tricks in a way that is independent of specific description domains. Moreover, we suggest new methods for overcoming the loss of precision — altogether eight different semantics are considered and compared. We provide theoretical results determining the relative accuracy of the approaches. These show that two of our new semantics are uniformly more accurate than existing approaches. Experiments that we have performed (for two description domains) with implementations of the eight different approaches enable a discussion of their relative runtime performances. We discuss the expected effect on other domains as well and conclude that our new methods can be trusted to yield significantly more accurate analysis for a small extra implementation effort, without compromising the efficiency of analysis