Abstract
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.
Work partially supported by STMicroelectronics and by CNR-CESTIA.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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.
S. Muchnick, Advanced Compiler Design and Implementation, Morgan Kaufmann, 1997.
D. Bacon S. Graham and O. Sharp, Compiler Transformations for High-Performance Computing, ACM Computing Surveys, Vol. 26, n. 4, 1994, 345–419.
Joseph A. Fisher, Trace Scheduling: A Technique for Global Microcode Compaction, IEEE Transactions on Computers, 1981, Vol. 30, n. 7, 478–490.
G. Ramalingam, The Undecibility of Aliasing, ACM TOPLAS, Vol. 16, n. 5, 1994, 1467–1471.
S. Horwitz, Precise Flow-Insensitive May-Alias Analysis is NP-Hard, ACM TOPLAS, Vol. 19, n. 1, 1997, 1–6.
W. A. Landi, Interprocedural Aliasing in the Presence of Pointers, Rutgers Univ., PhD Thesis, 1997.
G. Holzmann, Design and Validation of Computer Protocols, Prentice-Hall, Englewood Cliffs, New Jersey, 1991.
W. Landi and B. Ryder, A Safe Approximate Algorithm for Interprocedural Pointer Aliasing, Prog. Lang. Design and Impl. ACM SIGPLAN Not., 1992, 235–248.
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.
M. Garatti, S. Crespi Reghizzi, Backward Alias Analysis, Tech.Report, Dip. di Elettronica E Informazione, Poilitecnico di Milano, Sept. 2000.
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.
D. Liang and M.J. Harrold, Efficient Points-to Analysis for Whole-Program Analysis, Lectures Notes in Computer Science, 1687, 1999.
K. L. McMillan, Symbolic model checking-an approach to the state explosion problem, PhD thesis, Carnegie Mellon University, 1992.
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.
M. Hind, M. Burke, P. Carini and J. Choi, Interprocedural Pointer Alias Analysis, ACM TOPLAS, Vol. 21, 4, 1999, 848–894.
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.
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.
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.
Cousot, P. and Cousot, R., Temporal Abstract Interpretation, POPL 2000, pp.12–25.
Reps, T., Program analysis via graph reachability, Information and Software Technology 40, 11-12 (Nov./Dec. 1998), pp. 701–726.
W. Pugh and D. Wonnacott, Constraint-Based Array Dependence Analysis, ACM TOPLAS, Vol. 20, n. 3, 1998, 635–678.
Alain Deutsch, Interprocedural May-Alias Analysis for Pointers: Beyond k-limiting. In PLDI 1994, pp. 230–241. Jun 1994.
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).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Martena, V., San Pietro, P. (2001). Alias Analysis by Means of a Model Checker. In: Wilhelm, R. (eds) Compiler Construction. CC 2001. Lecture Notes in Computer Science, vol 2027. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45306-7_2
Download citation
DOI: https://doi.org/10.1007/3-540-45306-7_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41861-0
Online ISBN: 978-3-540-45306-2
eBook Packages: Springer Book Archive