Improving abstract interpretations by combining domains

ABSTRACT

In this paper we consider static analyses based on abstract interpretation of logic programs over combined domains. It is known that analyses over combined domains potentially provide more information than obtainable by performing the independent abstract interpretations. However, the construction of a combined analysis often requires redefining the basic operations for the combined domain. We demonstrate for logic programs that in practice it is possible to obtain precision in a combined analysis without redefining the basic operations. We also propose a way of performing the combination which can be more precise than the straightforward application of the classical “reduced product” approach, while keeping the original components of the basic operations. The advantage of the approach is that proofs of correctness for the new domains are not required and implementations can be reused. We illustrate our results by showing that a combined sharing analysis—constructed from “old” proposals—compares well with other “new” proposals suggested in recent literature both from the point of view of efficiency and accuracy.

REFERENCES

• 1: Roberto Barbuti , Roberto Giacobazzi , Giorgio Levi, A general framework for semantics-based bottom-up abstract interpretation of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.133-181, Jan. 1993 [doi>10.1145/151646.151650]
• 2: Maurice Bruynooghe, A practical framework for the abstract interpretation of logic programs, Journal of Logic Programming, v.10 n.2, p.91-124, Feb. 1991 [doi>10.1016/0743-1066(91)80001-T]
• 3: Michael Codish , Dennis Dams , Eyal Yardeni, Bottom-up abstract interpretation of logic programs, Theoretical Computer Science, v.124 n.1, p.93-125, Feb. 14, 1994 [doi>10.1016/0304-3975(94)90055-8]
• 4: M. Codish, D. Dams, and E. Yardeni. Derivation and Safety of an Abstract Algorithm for Groundhess and Aliasing Analysis. In Eighth International Conference on Logic Programming, pages 79- 93, Paris, France, June 1991. MIT Press.
• 5: A. Cortesi and G. Fit@. Comparing and improving: Abstract domains for sharing analysis. Technical Report, Department of Mathematics, University of Padova.
• 6: A. Cortesi and G. Fil@. Freeness computation in abstract interpretation. Rapporto Interno 2, Dip. di Matematica Pura e Applicata, Universit~ di Padova, March 1992.
• 7: Agostino Cortesi , Gilberto Filé , William H. Winsborough, Comparison of Abstract Interpretations, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.521-532, July 13-17, 1992
• 8: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 9: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 10: Patrick Cousot , Rahida Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, v.13 n.2-3, p.103-179, July 1992 [doi>10.1016/0743-1066(92)90030-7]
• 11: S.K. Debray, Guest editor. Journal of Logic Programming, Special Issue: Abstract interpretation, 13(2 and 3). North-Holland, July 1992.
• 12: G. Janssens , M. Bruynooghe, Deriving descriptions of possible values of program variables by means of abstract interpretation, Journal of Logic Programming, v.13 n.2-3, p.205-258, July 1992 [doi>10.1016/0743-1066(92)90032-X]
• 13: M. Hermenegildo. Abstract Interpretation and its Applications: Notes for an Advanced Tutorial. 1992 Joint International Conference and Symposium on Logic Programming, University of Maryland, November 1992.
• 14: M. V. Hermenegildo , K. J. Greene, Prolog and its performance: exploiting independent and-parallelism, Logic programming, MIT Press, Cambridge, MA, 1990
• 15: K. Horiuchi. Less Abstract Semantics for Abstract Interpretation of FGHC Programs. In 1992 international Conference on Fifth Generation Computer Systems, pages 897-906, Tokyo, Japan, June 1992. ICOT.
• 16: Dean Jacobs , Anno Langen, Static analysis of logic programs for independent and parallelism, Journal of Logic Programming, v.13 n.2-3, p.291-314, July 1992 [doi>10.1016/0743-1066(92)90034-Z]
• 17: N. D. Jones and H. Sendergaard. A semanticbased framework for the abstract interpretation of Prolog. in S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 123-142. Ellis Horwood, Chichester, 1987.
• 18: K. Muthukumar and M. Hermenegildo. Combined determination of sharing and freeness of program variables through abstract interpretation. In Proceedings of the Eighth International Conference on Logic Programming, pages 49-63, Paris, France, june 1991. MIT Press.
• 19: K. Muthukumar and M. Gareia de la Banda and M. Hermenegildo. Sharing and freeness analysis of logic programs using abstract interpretation. Technical report, U. of Madrid (UPM), Facultad Informatica UPM, Madrid, Spain, November 1992.
• 20: K. Muthukumar , M. Hermenegildo, Compile-time derivation of variable dependency using abstract interpretation, Journal of Logic Programming, v.13 n.2-3, p.315-347, July 1992 [doi>10.1016/0743-1066(92)90035-2]
• 21: Flemming Nielson, Strictness analysis and denotational abstract interpretation, Information and Computation, v.76 n.1, p.29-92, January 1988 [doi>10.1016/0890-5401(88)90041-7]
• 22: It. Sendergaard. Semantics.based Analysis and Transformation of Logic Programs. PhD thesis, DIKU, University of Copenhagen, 1990.
• 23: H Sondergaard, An application of abstract interpretation of logic programs: occur check reduction, Proc. of the European symposium on programming on ESOP 86, p.327-338, March 1986, Saarbru:9Aicken, Germany
• 24: Renganathan Sundararajan , John S. Conery, An Abstract Interpretation Scheme for Groundedness, Freeness, and Sharing Analysis of Logic Programs, Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science, p.203-216, December 18-20, 1992

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Design, Languages, Theory