Abstract
We describe data structures and algorithms for performing a path-sensitive program analysis to discover equivalences of expressions involving linear arithmetic or uninterpreted functions. We assume that conditionals are abstracted as boolean variables, which may be repeated to reflect equivalent conditionals. We introduce free conditional expression diagrams (FCEDs), which extend binary decision diagrams (BDDs) with internal nodes corresponding to linear arithmetic operators or uninterpreted functions. FCEDs can represent values of expressions in a program involving conditionals and linear arithmetic (or uninterpreted functions). We show how to construct them easily from a program, and give a randomized linear time algorithm (or quadratic time for uninterpreted functions) for comparing FCEDs for equality. FCEDs are compact due to maximal representation sharing for portions of the program with independent conditionals. They inherit from BDDs the precise reasoning about boolean expressions needed to handle dependent conditionals.
This research was supported in part by the National Science Foundation Grant CCR-0081588, and gifts from Microsoft Research. The information presented here does not necessarily reflect the position or the policy of the Government and no official endorsement should be inferred.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: 15th Annual ACM Symposium on POPL, pp. 1–11. ACM, New York (1988)
Andersen, H., Hulgaard, H.: Boolean expression diagrams. In: 12th Annual IEEE Symposium on Logic in Computer Science, June 1997, pp. 88–98. IEEE, Los Alamitos (1997)
Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic Decision Diagrams and Their Applications. In: IEEE /ACM International Conference on CAD, November 1993, pp. 188–191. ACM/IEEE (1993)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of the ACM SIGPLAN 2000 Conference on PLDI, May 2001, ACM, New York (2001)
Blum, M., Chandra, A., Wegman, M.: Equivalence of free boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters 10, 80–82 (1980)
Bryant, R., Chen, Y.: Verification of Arithmetic Circuits with Binary Moment Diagrams. In: 32nd ACM/IEEE Design Automation Conference (June 1995)
Bryant, R.E.: Binary decision diagrams and beyond: Enabling technologies for formal verification. In: International Conference on Computer Aided Design, November 1995, pp. 236–245. IEEE Computer Society Press, Los Alamitos (1995)
Clarke, E.M., Fujita, M., Zhao, X.: Hybrid decision diagrams overcoming the limitations of MTBDDs and BMDs. In: International Conference on Computer Aided Design, November 1995, pp. 159–163. IEEE Computer Society Press, Los Alamitos (1995)
Clarke, E.M., McMillan, K.L., Znao, X., Fujiia, M., Yang, J.: Spectral transforms for large boolean functions with applications to technology mapping. In: Proceedings of the 30th ACM/IEEE Design Automation Conference, June 1993, pp. 54–60 (1993)
Corella, F., Zhou, Z., Song, X., Langevin, M., Cerny, E.: Multiway decision graphs for automated hardware verification. Formal Methods in System Design: An International Journal 10(1), 7–46 (1997)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Annual ACM Symposium on Principles of Programming Languages, pp. 234–252 (1977)
Darwiche, A.: A compiler for deterministic decomposable negation normal form. In: Proceedings of the Fourteenth Conference on Innovative Applications of Artificial Intelligence, July 2002, pp. 627–634. AAAI Press, Menlo Park (2002)
Darwiche, A., Huang, J.: Testing equivalence probabilistically. Technical Report D-23, Computer Science Department, UCLA (June 2002)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8), 453–457 (1975)
Fujita, M., McGeer, P.C.: Introduction to the special issue on multi-terminal binary decision diagrams. Formal Methods in System Design 10(2/3) (April 1997)
Gargi, K.: A sparse algorithm for predicated global value numbering. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, June 17-19, vol. 37(5), pp. 45–56. ACM Press, New York (2002)
Gergov, J., Meinel, C.: Efficient boolean manipulation with OBDDs can be extended to FBDDs. IEEE Trans. on Computers 43(10), 1197–1209 (1994)
Gulwani, S., Necula, G.C.: Discovering affine equalities using random interpretation. In: 30th Annual ACM Symposium on POPL, January 2003, ACM, New York (2003)
Gulwani, S., Necula, G.C.: Global value numbering using random interpretation. In: 31st Annual ACM Symposium on POPL, January 2004, ACM, New York (2004)
Gulwani, S., Necula, G.C.: Path-sensitive analysis for linear arithmetic and uninterpreted functions. Technical Report UCB//CSD-04-1325, UC-Berkeley (2004)
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)
Karr, M.: Affine relationships among variables of a program. In: Acta Informatica, pp. 133–151. Springer, Heidelberg (1976)
Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)
Necula, G.C.: Translation validation for an optimizing compiler. In: Proceedings of the ACM SIGPLAN ’00 Conference on PLDI, June 2000, pp. 83–94. ACM, New York (2000)
Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: 15th Annual ACM Symposium on Principles of Programming Languages, pp. 12–27. ACM, New York (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)
Schwartz, J.T.: Fast probabilistic algorithms for verification of polynomial identities. JACM 27(4), 701–717 (1980)
Weise, D., Crew, R.F., Ernst, M., Steensgaard, B.: Value dependence graphs: representation without taxation. In: 21st Annual ACM Symposium on POPL, January 1994, ACM, New York (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gulwani, S., Necula, G.C. (2004). Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions. In: Giacobazzi, R. (eds) Static Analysis. SAS 2004. Lecture Notes in Computer Science, vol 3148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27864-1_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-27864-1_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22791-5
Online ISBN: 978-3-540-27864-1
eBook Packages: Springer Book Archive