Abstract
We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, called Herbrand equalities, are therefore an ideal basis for truly machine-independent optimizations as they hold on every machine. Besides a general correctness theorem, covering arbitrary call-by-value parameters and local and global variables, we also obtain two new completeness results: one by constraining the analysis problem to Herbrand constants, and one by allowing side-effect-free functions only. Thus if we miss a constant/equality in these two scenarios, then there exists a separating interpretation of the operator symbols.
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
Alpern, B., Wegman, M., Zadeck, F.K.: Detecting Equality of Variables in Programs. In: 15th ACM Symp. on Principles of Programming Languages (POPL), pp. 1–11 (1988)
Apt, K.R., Plotkin, G.D.: Countable Nondeterminism and Random Assignment. Journal of the ACM 33(4), 724–767 (1986)
Click, C., Cooper, K.D.: Combining Analyses, Combining Optimizations. ACM Transactions on Programming Languages and Systems 17(2), 181–196 (1995)
Cocke, J., Schwartz, J.T.: Programming languages and their compilers. Courant Institute of Mathematical Sciences, NY (1970)
Cousot, P.: Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Electronic Notes in Theoretical Computer Science 6 (1997), www.elsevier.nl/locate/entcs/volume6.html
Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: 4th ACM Symp. on Principles of Programming Languages, POPL (1977)
Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Recursive Procedures. In: Neuhold, E. (ed.) IFIP Conf. on Formal Description of Programming Concepts, pp. 237–277. North-Holland, Amsterdam (1977)
Gargi, K.: A Sparse Algorithm for Predicated Global Value Numbering. In: ACM Conf. on Programming Language Design and Implementation (PLDI), pp. 45–56 (2002)
Gulwani, S., Necula, G.C.: A Polynomial-time Algorithm for Global Value Numbering. In: 11th Int. Static Analysis Symposium (SAS). Springer, Heidelberg (2004)
Gulwani, S., Necula, G.C.: Global Value Numbering Using Random Interpretation. In: 31st ACM Symp. on Principles of Programming Languages (POPL), pp. 342–352 (2004)
Kildall, G.A.: A Unified Approach to Global Program Optimization. In: First ACM Symp. on Principles of Programming Languages (POPL), pp. 194–206 (1973)
Knoop, J., Rüthing, O., Steffen, B.: Code Motion and Code Placement: Just Synonyms? In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 154–196. Springer, Heidelberg (1998)
Knoop, J., Steffen, B.: The Interprocedural Coincidence Theorem. In: Barahona, P., Porto, A., Moniz Pereira, L. (eds.) EPIA 1991. LNCS, vol. 541, pp. 125–140. Springer, Heidelberg (1991)
Muchnick, S.S., Jones, N.D. (eds.): Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs (1981)
Müller-Olm, M., Rüthing, O., Seidl, H.: Checking Herbrand Equalities and Beyond. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 79–96. Springer, Heidelberg (2005)
Müller-Olm, M., Seidl, H., Steffen, B.: Interprocedural Analysis for Free. Technical Report 790, Fachbereich Informatik, Universität Dortmund (2004)
Reif, J.H., Lewis, R.: Symbolic Evaluation and the Gobal Value Graph. In: 4th ACM Symp. on Principles of Programming Languages (POPL), pp. 104–118 (1977)
Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global Value Numbers and Redundant Computations. In: 15th ACM Symp. on Principles of Programming Languages (POPL), pp. 12–27 (1988)
Rüthing, O., Knoop, J., Steffen, B.: Detecting Equalities of Variables: Combining Efficiency with Precision. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 232–247. Springer, Heidelberg (1999)
Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis. In: [14] ch. 7, pp. 189–233
Steffen, B.: Optimal Run Time Optimization—Proved by a New Look at Abstract Interpretations. In: Ehrig, H., Levi, G., Montanari, U. (eds.) CAAP 1987 and TAPSOFT 1987. LNCS, vol. 249, pp. 52–68. Springer, Heidelberg (1987)
Steffen, B., Knoop, J., Rüthing, O.: The Value Flow Graph: A Program Representation for Optimal Program Transformations. In: Jones, N.D. (ed.) ESOP 1990. LNCS, vol. 432, pp. 389–405. Springer, Heidelberg (1990)
Steffen, B., Knoop, J., Rüthing, O.: Efficient Code Motion and an Adaption to Strength Reduction. In: Abramsky, S. (ed.) TAPSOFT 1991, CCPSD 1991, and ADC-Talks 1991. LNCS, vol. 494, pp. 394–415. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller-Olm, M., Seidl, H., Steffen, B. (2005). Interprocedural Herbrand Equalities. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)