Abstract Interpretation of Logic Programs Using Magic Transformations
Saumya Debray Raghu Ramakrishnan
Abstract
In dataflow analysis of logic programs, information must be propagated
according to the control strategy of the language under consideration.
However, for languages with top-down control flow, naive top-down dataflow
analyses may have problems guaranteeing completeness and/or termination.
What is required in the dataflow analysis
is a bottom-up fixpoint computation, guided by the
(possibly top-down) control strategy of the language.
This paper describes the
application of the Magic Templates algorithm, originally devised as a
technique for efficient bottom-up computation of logic programs, to
dataflow analysis of logic programs. It turns out that a direct application
of the Magic Templates algorithm can result in an undesirable loss in
precision, because connections between ``calling patterns'' and
the corresponding ``success patterns'' may be lost. We show how the
original Magic Templates algorithm can be modified to avoid this problem,
and prove that the resulting analysis algorithm is at least as precise
as any other abstract interpretation that uses the same abstract domain
and abstract operations.