Abstract
In this paper, we study the problem of solving integer range constraints that arise in many static program analysis problems. In particular, we present the first polynomial time algorithm for a general class of integer range constraints. In contrast with abstract interpretation techniques based on widenings and narrowings, our algorithm computes, in polynomial time, the optimal solution of the arising fixpoint equations. Our result implies that “precise” range analysis can be performed in polynomial time without widening and narrowing operations.
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
Apt, K.R.: The essence of constraint propagation. Theoretical Computer Science 221(1-2), 179–210 (1999)
Apt, K.R.: The role of commutativity in constraint propagation algorithms. ACM Transactions on Programming Languages and Systems 22(6), 1002–1036 (2000)
Aspvall, B., Shiloach, Y.: A polynomial time algorithm for solving systems of linear inequalities with two variables per inequality. SIAM Journal on Computing 9(4), 827–845 (1980)
Benhamou, F., Older, W.J.: Applying interval arithmetic to real, integer, and Boolean constraints. Journal of Logic Programming 32(1), 1–24 (1997)
Bledsoe, W.W.: The Sup-Inf method in Presburger arithmetic. Technical report, University of Texas Math Dept. (December 1974)
Blume, W., Eigenmann, R.: The range test: A dependence test for symbolic, non-linear expressions. In: Supercomputing 1994, IEEE Computer Society, Los Alamitos (1994)
Blume, W., Eigenmann, R.: Symbolic range propagation. In: Proceedings of the 9th International Symposium on Parallel Processing IPPS 1995, Los Alamitos, CA, USA, April 1995, pp. 357–363. IEEE Computer Society Press, Los Alamitos (1995)
Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 30–43. Springer, Heidelberg (1996)
Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: SIGPLAN 1993 Conference on Programming Language Design and Implementation, pp. 46–55 (1993)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the 2nd International Symposium on Programming, pp. 106–130 (1976)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, pp. 234–252 (1977)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM Symposium on Principles of Programming Languages, pp. 84–97 (1978)
Fecht, C., Seidl, H.: A faster solver for general systems of equations. Science of Computer Programming 35(2-3), 137–161 (1999)
Gupta, R.: A fresh look at optimizing array bound checking. In: Proceedings of the Conference on Programming Language Design and Implementation, pp. 272–282 (1990)
Gupta, R.: Optimizing array bound checks using flow analysis. ACM Letters on Programming Languages and Systems 1(4), 135–150 (1994)
Heintze, N., Jaffar, J.: A decision procedure for a class of Herbrand set constraints. In: Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS), June 1990, pp. 42–51 (1990)
Hickey, T.J.: Analytic constraint solving and interval arithmetic. In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POLP 2000), N.Y., January 19-21, pp. 338–351 (2000)
Hickey, T.J., van Emden, M.H., Wu, H.: A unified framework for interval constraints and interval arithmetic. In: Principles and Practice of Constraint Programming, pp. 250–264 (1998)
Ignizio, J.P., Cavalier, T.M.: Introduction to Linear Programming. Prentice-Hall, Englewood Cliffs (1994)
Kam, J.B., Ullman, J.D.: Global data flow analysis and iterative algorithms. Journal of the ACM 23(1), 158–171 (1976)
Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations, pp. 85–103. Plenum Press, New York (1975)
Kildall, G.A.: A unified approach to global program optimization. In: Conference Record of the ACM Symposium on Principles of Programming Languages. ACM SIGACT and SIGPLAN, pp. 194–206 (1973)
Matijasevič, Y.V.: On recursive unsolvability of Hilbert’s Tenth Problem. In: Suppes, P., et al. (eds.) Logic, Methodology and Philosophy of Science IV. Studies in Logic and the Foundations of Mathematics, vol. 74, pp. 89–110. North-Holland, Amsterdam (1973)
Moore, R.E.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1963)
Nelson, G.: An n logn algorithm for the two-variable-per-constraint linear programming satisfiability problem. Technical Report STAN-CS-78-689, Stanford University (1978)
Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center (1981)
Older, W.J., Velino, A.: Constraint arithmetic on real intervals. In: Benhamou, F., Colmerauer, A. (eds.) Constraint Logic Programming: Selected Research, pp. 175–196. MIT Press, Cambridge (1993)
Paek, Y., Hoeflinger, J., Padua, D.A.: Efficient and precise array access analysis. ACM Transactions on Programming Languages and Systems 24(1), 65–109 (2002)
Pratt, V.R.: Two easy theories whose combination is hard (1977) (unpublished manuscript)
Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM 35(8), 102–114 (1992)
Pugh, W.: Constraint-based array dependence analysis. ACM Transactions on Programming Languages and Systems 20(3), 635–678 (1998)
Seater, R., Wonnacott, D.: Polynomial time array dataflow analysis. In: Languages and Compilers for Parallel Computing, LCPC (2001)
Shostak, R.: Deciding linear inequalities by computing loop residues. Journal of the ACM 28(4), 769–779 (1981)
Suzuki, N., Ishihata, K.: Implementation of an array bound checker. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, January 17-19. ACM SIGACT-SIGPLAN, pp. 132–143 (1977)
Wagner, D., Foster, J.S., Brewer, E.A., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Symposium on Network and Distributed Systems Security (NDSS 2000), San Diego, CA, February 2000. Internet Society, pp. 3–17 (2000)
Wolper, P., Boigelot, B.: An automata-theoretic approach to presburger arithmetic constraints. In: Static Analysis Symposium, pp. 21–32 (1995)
Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17-19, pp. 249–257 (1998)
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
Su, Z., Wagner, D. (2004). A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive