Nothing Special   »   [go: up one dir, main page]

skip to main content
research-article
Open access

Fast interprocedural linear two-variable equalities

Published: 03 January 2012 Publication History

Abstract

In this article we provide an interprocedural analysis of linear two-variable equalities. The novel algorithm has a worst-case complexity of 𝒪(nk4), where k is the number of variables and n is the program size. Thus, it saves a factor of k4 in comparison to a related algorithm based on full linear algebra. We also indicate how the practical runtime can be further reduced significantly. The analysis can be applied, for example, for register coalescing, for identifying local variables and thus for interprocedurally observing stack pointer modifications as well as for an analysis of array index expressions, when analyzing low-level code.

References

[1]
Alpern, B., Wegman, M., and Zadeck, F. K. 1988. Detecting equality of variables in programs. In Proceedings of the 15th ACM Symposium on Principles of Programming Languages (POPL). ACM, New York, 1--11.
[2]
Fecht, C. and Seidl, H. 1998. Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems. Nord. J. Comput. 5, 4, 304--329.
[3]
George, L. and Appel, A. W. 1996. Iterated register coalescing. ACM Trans. Program. Lang. Syst. 18, 3, 300--324.
[4]
Gulwani, S. and Necula, G. C. 2004. A polynomial-time algorithm for global value numbering. In Proceedings of the 11th International Static Analysis Symposium (SAS). Lecture Notes in Computer Science, vol. 3148, Springer, Berlin, 212--227.
[5]
Horwitz, S., Reps, T. W., and Sagiv, M. 1995. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL). ACM, New York, 49--61.
[6]
Knoop, J. and Steffen, B. 1992. The interprocedural coincidence theorem. In Proceedings of the Compiler Construction Conference (CC). Lecture Notes in Computer Science, vol. 541, Springer, Berlin, 125--140.
[7]
Miné, A. 2001a. A new numerical abstract domain based on difference bound matrices. In Proceedings of the 2d Symposium on Programs as Data Objects (PADO II). Lecture Notes in Computer Science, vol. 2053, Springer, Berlin, 155--172.
[8]
Miné, A. 2001b. The octagon abstract domain. In Proceedings of the Workshop on Analysis, Slicing, and Transformation (AST). IEEE, Los Alamitos, CA, 310--319.
[9]
Müller-Olm, M., Rüthing, O., and Seidl, H. 2005. Checking Herbrand equalities and beyond. In Proceedings of the International Conference on Verification, Model-Checking and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 3385, Springer, Berlin, 79--96.
[10]
Müller-Olm, M. and Seidl, H. 2004. Precise interprocedural analysis through linear algebra. In Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL). ACM, New York, 330--341.
[11]
Müller-Olm, M., Seidl, H., and Steffen, B. 2005. Interprocedural Herbrand equalities. In Proceedings of the 14th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 3444, Springer, Berlin, 31--45.
[12]
Müller-Olm, M. and Seidl, H. 2007. Analysis of modular arithmetic. ACM Trans. Program. Lang. Syst. 29, 5.
[13]
Müller-Olm, M. and Seidl, H. 2008. Upper adjoints for fast inter-procedural variable equalities. In Proceedings of the 17th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 4960, Springer, Berlin.
[14]
Sagiv, S., Reps, T. W., and Horwitz, S. 1996. Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167, 1/2, 131--170.
[15]
Sankaranarayanan, S., Sipma, H., and Manna, Z. 2005. Scalable analysis of linear systems using mathematical programming. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 3385, Springer, Berlin, 25--41.
[16]
Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Application, Prentice Hall, Englewood Cliffs, NJ, 189--234.
[17]
Simon, A., King, A., and Howe, J. M. 2002. Two variables per linear inequality as an abstract domain. In Proceedings of the Conference on Logic Based Program Development and Transformation (LOPSTR). Lecture Notes in Computer Science, vol. 2664, Springer, Berlin, 71--89.
[18]
Steffen, B., Knoop, J., and Rüthing, O. 1990. The value flow graph: A program representation for optimal program transformations. In Proceedings of the 3rd European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 432, Springer, Berlin, 389--405.
[19]
Votum. 2010. http://www2.in.tum.de/votum.
[20]
Zucker, S. and Karhi, K. 1995. System V application binary interface: PowerPC processor supplement. http://refspecs.freestandards.org/elf/elfspec_ppc.pdf.

Cited By

View all

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 33, Issue 6
December 2011
145 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/2049706
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 January 2012
Accepted: 01 October 2011
Revised: 01 April 2011
Received: 01 January 2010
Published in TOPLAS Volume 33, Issue 6

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Abstract interpretation
  2. interprocedural analysis
  3. linear equalities
  4. linear two-variable equalities
  5. low-level code analysis
  6. static analysis
  7. summary functions
  8. variable differences

Qualifiers

  • Research-article
  • Research
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)78
  • Downloads (Last 6 weeks)12
Reflects downloads up to 17 Nov 2024

Other Metrics

Citations

Cited By

View all

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media