Alias Analysis by Means of a Model Checker

  • Vincenzo Martena
  • Pierluigi San Pietro
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2027)


We study the application of a standard model checker tool, Spin, to the well-known problem of computing a may-alias relation for a C program. A precise may-alias relation can significantly improve code optimization, but in general it may be computationally too expensive. We show that, at least in the case of intraprocedural alias analysis, a model checking tool has a great potential for precision and efficiency. For instance, we can easily deal, with good precision, with features such as pointer arithmetic, arrays, structures and dynamic memory allocation. At the very least, the great flexibility allowed in defining the may-alias relation, should make it easier to experiment and to examine the connections among the accuracy of an alias analysis and the optimizations available in the various compilation phases.


Model Checker Pointer Arithmetic Static Array Nondeterministic Choice Model Check Tool 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    M. Shapiro and S. Horwitz, The effects of the precision of pointer analysis, In P. Van Hentenryck, (ed.), 4th Intern. Static Analysis Symp., 1997, LNCS 1302, pp. 16–34. Springer-Verlag.CrossRefGoogle Scholar
  2. 2.
    S. Muchnick, Advanced Compiler Design and Implementation, Morgan Kaufmann, 1997.Google Scholar
  3. 3.
    D. Bacon S. Graham and O. Sharp, Compiler Transformations for High-Performance Computing, ACM Computing Surveys, Vol. 26, n. 4, 1994, 345–419.CrossRefGoogle Scholar
  4. 4.
    Joseph A. Fisher, Trace Scheduling: A Technique for Global Microcode Compaction, IEEE Transactions on Computers, 1981, Vol. 30, n. 7, 478–490.CrossRefGoogle Scholar
  5. 5.
    G. Ramalingam, The Undecibility of Aliasing, ACM TOPLAS, Vol. 16, n. 5, 1994, 1467–1471.CrossRefGoogle Scholar
  6. 6.
    S. Horwitz, Precise Flow-Insensitive May-Alias Analysis is NP-Hard, ACM TOPLAS, Vol. 19, n. 1, 1997, 1–6.CrossRefGoogle Scholar
  7. 7.
    W. A. Landi, Interprocedural Aliasing in the Presence of Pointers, Rutgers Univ., PhD Thesis, 1997.Google Scholar
  8. 8.
    G. Holzmann, Design and Validation of Computer Protocols, Prentice-Hall, Englewood Cliffs, New Jersey, 1991.Google Scholar
  9. 9.
    W. Landi and B. Ryder, A Safe Approximate Algorithm for Interprocedural Pointer Aliasing, Prog. Lang. Design and Impl. ACM SIGPLAN Not., 1992, 235–248.Google Scholar
  10. 10.
    D. Liang and M.J. Harrold, Equivalence Analysis: A General Technique to Improve the Efficiency of Data-flow Analyses in the Presence of Pointers, ACM TOPLAS, Vol. 24, n. 5, 1999, 39–46.Google Scholar
  11. 11.
    M. Garatti, S. Crespi Reghizzi, Backward Alias Analysis, Tech.Report, Dip. di Elettronica E Informazione, Poilitecnico di Milano, Sept. 2000.Google Scholar
  12. 12.
    B. Steensgaard, Points-to Analysis in Almost Linear Time, in Proc. 23rd SIGPLANSIGACT Symp. on Principles of Programming Languages, Jan,, 1996.pp. 32–41, ACM Press.Google Scholar
  13. 13.
    D. Liang and M.J. Harrold, Efficient Points-to Analysis for Whole-Program Analysis, Lectures Notes in Computer Science, 1687, 1999.Google Scholar
  14. 14.
    K. L. McMillan, Symbolic model checking-an approach to the state explosion problem, PhD thesis, Carnegie Mellon University, 1992.Google Scholar
  15. 15.
    Yong, S.H., Horwitz, S., and Reps, T., Pointer analysis for programs with structures and casting, Proc. of the ACM Conf. on Programming Language Design and Implementation, (Atlanta, GA, May 1–4, 1999), in ACM SIGPLAN Notices 34, 5 (May 1999), pp. 91–103.Google Scholar
  16. 16.
    M. Hind, M. Burke, P. Carini and J. Choi, Interprocedural Pointer Alias Analysis, ACM TOPLAS, Vol. 21, 4, 1999, 848–894.CrossRefGoogle Scholar
  17. 17.
    B. Steffen, Data Flow Analysis as Model Checking, Proc. Int. Conf. on Theoretical Aspects of Computer Software, (TACS 1991), Sendai (Japan), September 1991, pp. 346–365.Google Scholar
  18. 18.
    D.A. Schmidt and B. Steffen, Program analysis as model checking of abstract interpretations, G. Levi. (ed.), pages 351–380. Proc. 5th Static Analysis Symp., Pisa, September, 1998. Berlin: Springer-Verlag, 1998. Springer LNCS 1503.Google Scholar
  19. 19.
    Cousot, P. and Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL 1977, pp. 238–252.Google Scholar
  20. 20.
    Cousot, P. and Cousot, R., Temporal Abstract Interpretation, POPL 2000, pp.12–25.Google Scholar
  21. 21.
    Reps, T., Program analysis via graph reachability, Information and Software Technology 40, 11-12 (Nov./Dec. 1998), pp. 701–726.CrossRefGoogle Scholar
  22. 22.
    W. Pugh and D. Wonnacott, Constraint-Based Array Dependence Analysis, ACM TOPLAS, Vol. 20, n. 3, 1998, 635–678.CrossRefGoogle Scholar
  23. 23.
    Alain Deutsch, Interprocedural May-Alias Analysis for Pointers: Beyond k-limiting. In PLDI 1994, pp. 230–241. Jun 1994.Google Scholar
  24. 24.
    Wilhelm, R., Sagiv, M., and Reps, T., Shape analysis. In Proc. of CC 2000: 9th Int. Conf. on Compiler Construction, (Berlin, Ger., Mar. 27-Apr. 2, 2000).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Vincenzo Martena
    • 1
  • Pierluigi San Pietro
    • 1
  1. 1.Dipartimento di Elettronica e InformazionePolitecnico di MilanoMilanoItalia

Personalised recommendations