Abstract
A Herbrand equality between expressions in a program is an equality which holds relative to the Herbrand interpretation of operators. We show that the problem of checking validity of positive Boolean combinations of Herbrand equalities at a given program point is decidable – even in presence of disequality guards. This result vastly extends the reach of classical methods for global value numbering which cannot deal with disjunctions and are always based on an abstraction of conditional branching with non-deterministic choice. In order to introduce our analysis technique in a simpler scenario we also give an alternative proof that in the classic setting, where all guards are ignored, conjunctions of Herbrand equalities can be checked in polynomial time. As an application of our method, we show how to derive all valid Herbrand constants in programs with disequality guards. Finally, we present a PSPACE lower bound and show that in presence of equality guards instead of disequality guards, it is undecidable to check whether a given Herbrand equality holds or not.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
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)
Briggs, P., Cooper, K.D., Simpson, L.T.: Value Numbering. Software- Practice and Experience 27(6), 701–724 (1997)
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)
Duffy, D.: Principles of Automated Theorem Proving. Wiley, Chichester (1991)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, New York (1978)
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: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 212–227. 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)
Kam, J.B., Ullman, J.D.: Monotone data flow analysis frameworks. Technical Report 169, Department of Electrical Engineering, Princeton University, Princeton, NJ (1975)
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)
Müller-Olm, M., Rüthing, O.: The Complexity of Constant Propagation. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 190–205. Springer, Heidelberg (2001)
Müller-Olm, M., Seidl, H.: Polynomial Constants are Decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 4–19. Springer, Heidelberg (2002)
Müller-Olm, M., Seidl, H.: A Note on Karr’s Algorithm. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016–1028. Springer, Heidelberg (2004)
Müller-Olm, M., Seidl, H.: Computing Polynomial Program Invariants. Information Processing Letters (IPL) 91(5), 233–244 (2004)
Müller-Olm, M., Seidl, H.: Precise Interprocedural Analysis through Linear Algebra. In: 31st ACM Symp. on Principles of Programming Languages (POPL), pp. 330–341 (2004)
Reif, J.H., Lewis, R.: Symbolic Evaluation and the Gobal Value Graph. In: 4th ACMSymp. 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)
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., Rüthing, O., Seidl, H. (2005). Checking Herbrand Equalities and Beyond. In: Cousot, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2005. Lecture Notes in Computer Science, vol 3385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30579-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-30579-8_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24297-0
Online ISBN: 978-3-540-30579-8
eBook Packages: Computer ScienceComputer Science (R0)