Graeme Gange
Harald Søndergaard
Peter J. Stuckey
Skip Abstract Section
Abstract
The most commonly used integer types have fixed bit-width, making it possible for computations to “wrap around,” and many programs depend on this behaviour. Yet much work to date on program analysis and verification of integer computations treats integers as having infinite precision, and most analyses that do respect fixed width lose precision when overflow is possible. We present a novel integer interval abstract domain that correctly handles wrap-around. The analysis is signedness agnostic. By treating integers as strings of bits, only considering signedness for operations that treat them differently, we produce precise, correct results at a modest cost in execution time.
- Gogul Balakrishnan. 2007. WYSINWYX: What You See Is Not What You Execute. Ph.D. Dissertation. University of Wisconsin at Madison, Madison, WI. Google Scholar
Digital Library
- Gogul Balakrishnan and Thomas Reps. 2004. Analyzing memory accesses in x86 executables. In Compiler Construction: Proceedings of the 13th International Conference, E. Duesterwald (Ed.). Lecture Notes in Computer Science, Vol. 2985. Springer, 5--23.Google Scholar
- Sébastien Bardin, Philippe Herrmann, and Florian Perroud. 2010. An alternative to SAT-based approaches for bit-vectors. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’10), J. Esparza and R. Majumdar (Eds.). Lecture Notes in Computer Science, Vol. 6015. Springer, 84--98. Google ScholarDigital Library
- Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation: Complexity, Analysis, Transformation, T. Æ. Mogensen, D. A. Schmidt, and I. H. Sudborough (Eds.). Lecture Notes in Computer Science, Vol. 2566. Springer, 85--108. Google ScholarDigital Library
- Sandrine Blazy, Vincent Laporte, Andre Maroneze, and David Pichardie. 2013. Formal verification of a C value analysis based on abstract interpretation. In Static Analysis, F. Logozzo and M. Fähndrich (Eds.). Lecture Notes in Computer Science, Vol. 7935. Springer, 324--344.Google Scholar
- Jörg Brauer and Andy King. 2010. Automatic abstraction for intervals using boolean formulae. In Static Analysis, R. Cousot and M. Martel (Eds.). Lecture Notes in Computer Science, Vol. 6337. Springer, 167--183. Google ScholarDigital Library
- Zack Coker and Munawar Hafiz. 2013. Program transformations to fix C integers. In Proceedings of the 35th International Conference on Software Engineering (ICSE’13). IEEE, 792--801. Google ScholarDigital Library
- Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, and Westley Weimer. 2003. CCured in the real world. In Proceedings of ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI’03). ACM, New York, NY, 232--244. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1977. 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. ACM, New York, NY, 238--252. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Proceedings of the Sixth ACM Symposium on Principles of Programming Languages. ACM, New York, NY, 269--282. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1992. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In Proceedings of the International Symposium on Programming Language Implementation and Logic Programming, M. Bruynooghe and M. Wirsing (Eds.). Lecture Notes in Computer Science, Vol. 631. Springer, 269--295. Google ScholarDigital Library
- Will Dietz, Peng Li, John Regehr, and Vikram Adve. 2012. Understanding integer overflow in C/C++. In Proceedings of the 34th International Conference on Software Engineering. IEEE, 760--770. Google ScholarDigital Library
- Manuel Fähndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In FoVeOSS, B. Beckert and C. Marché (Eds.). Lecture Notes in Computer Science, Vol. 6528. Springer, 10--30. Google ScholarDigital Library
- Stephan Falke, Deepak Kapur, and Carsten Sinz. 2012. Termination analysis of imperative programs using bitvector arithmetic. In Verified Software: Theories, Tools, and Experiments, R. Joshi, P. Müller, and A. Podelski (Eds.). Lecture Notes in Computer Science, Vol. 7152. Springer, 261--277. Google ScholarDigital Library
- Stephan Falke, Florian Merz, and Carsten Sinz. 2013. LLBNC: Improved bounded model checking of C programs using LLVM. In Tools and Algorithms for the Construction and Analysis of Systems, N. Piterman and S. Smolka (Eds.). Lecture Notes in Computer Science, Vol. 7795. Springer, 623--626. Google ScholarDigital Library
- Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2013a. Abstract interpretation over non-lattice abstract domains. In Static Analysis, F. Logozzo and M. Fähndrich (Eds.). Lecture Notes in Computer Science, Vol. 7935. Springer, 6--24.Google Scholar
- Graeme Gange, Harald Søndergaard, Peter J. Stuckey, and Peter Schachte. 2013b. Solving difference constraints over modular arithmetic. In Automated Deduction, M. Bonacina (Ed.). Lecture Notes in Artificial Intelligence, Vol. 7898. Springer, 215--230. Google ScholarDigital Library
- Thomas Gawlitza, Jérôme Leroux, Jan Reineke, Helmut Seidl, Grégoire Sutre, and Reinhard Wilhelm. 2009. Polynomial precise interval analysis revisited. In Efficient Algorithms: Essays Dedicated to Kurt Mehlhorn on the Occasion of His 60th Birthday, S. Albers, H. Alt, and S. Näher (Eds.). Lecture Notes in Computer Science, Vol. 5760. Springer, 422--437. Google ScholarDigital Library
- Arnaud Gotlieb, Michel Leconte, and Bruno Marre. 2010. Constraint solving on modular integers. In Proceedings of the Ninth International Workshop on Constraint Modelling and Reformulation (ModRef’10).Google Scholar
- Philippe Granger. 1989. Static analysis of arithmetical congruences. International Journal of Computer Mathematics 30 (1989), 165--190.Google ScholarCross Ref
- Philippe Granger. 1991. Static analyses of linear congruence equalities among variables of a program. In Theory and Practice of Software Development. Lecture Notes in Computer Science, Vol. 493. Springer, 167--192. Google ScholarDigital Library
- Andy King and Harald Søndergaard. 2010. Automatic abstraction for congruences. In Verification, Model Checking and Abstract Interpretation, G. Barthe and M. Hermenegildo (Eds.). Lecture Notes in Computer Science, Vol. 5944. Springer, 197--213. Google ScholarDigital Library
- Michel Leconte and Bruno Berstel. 2006. Extending a CP solver with congruences as domains for program verification. In Proceedings of the 1st Workshop on Software Testing, Verification and Analysis (CSTVA’06), B. Blanc, A. Gotlieb, and C. Michel (Eds.). 22--33.Google Scholar
- Jérôme Leroux and Grégoire Sutre. 2007. Accelerated data-flow analysis. In Static Analysis, H. Riis Nielson and G. Filé (Eds.). Lecture Notes in Computer Science, Vol. 4634. Springer, 184--199. Google ScholarDigital Library
- Francesco Logozzo and Matthieu Martel. 2013. Automatic repair of overflowing expressions with abstract interpretation. In Semantics, Abstract Interpretation, and Reasoning about Programs, A. Banerjee, O. Danvy, K.-G. Doh, and J. Hatcliff (Eds.). Electronic Proceedings in Theoretical Computer Science, Vol. 129. 341--357.Google ScholarCross Ref
- Kim Marriott and Peter J. Stuckey. 1998. Programming with Constraints: An Introduction. MIT Press, Cambridge, MA.Google Scholar
- Laurant D. Michel and Pascal Van Hentenryck. 2012. Constraint satisfaction over bit-vectors. In Constraint Programming: Proceedings of the 2012 Conference, M. Milano (Ed.). Lecture Notes in Computer Science, Vol. 7514. Springer, 527--543. Google ScholarCross Ref
- Antoine Miné. 2006. The octagon abstract domain. Higher-Order and Symbolic Computation 19, 1, 31--100. Google ScholarDigital Library
- Tsuneo Nakanishi, Kazuki Joe, Constantine D. Polychronopoulos, and Akira Fukuda. 1999. The modulo interval: A simple and practical representation for program analysis. In Parallel Architecture and Compilation Techniques. IEEE, 91--96. DOI:http://dx.doi.org/10.1109/PACT.1999.807422 Google ScholarCross Ref
- Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2012. Signedness-agnostic program analysis: Precise integer bounds for low-level code. In Proceedings of the 10th Asian Symposium on Programming Languages and Systems (APLAS’12), R. Jhala and A. Igarashi (Eds.). Lecture Notes in Computer Science, Vol. 7705. Springer, 115--130.Google Scholar
- Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of Program Analysis. Springer, New York, NY. Google ScholarDigital Library
- John Regehr and Usit Duongsaa. 2006. Deriving abstract transfer functions for analyzing embedded software. In Proceedings of the 2006 SIGPLAN/SIGBED Conference on Language, Compilers, and Tool Support for Embedded Systems (LCTES’06). ACM Press, 34--43. Google ScholarDigital Library
- Thomas Reps, Gogul Balakrishnan, and Junghee Lim. 2006. Intermediate-representation recovery from low-level code. In Proceedings of the 2006 ACM SIGPLAN Conference on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, New York, NY, 100--111. Google ScholarDigital Library
- Raphael E. Rodrigues, Victor H. Sperle Campos, and Fernando M. Quintão Pereira. 2013. A fast and low-overhead technique to secure programs against integer overflows. In Proceedings of the 2013 IEEE/ACM International Symposium on Code Generation and Optimization (CGO’13). IEEE, 1--11. Google ScholarDigital Library
- Helmut Seidl, Reinhard Wilhelm, and Sebastian Hack. 2012. Compiler Design: Analysis and Transformation. Springer. Google ScholarDigital Library
- Rathijit Sen and Y. N. Srikant. 2007. Executable analysis using abstract interpretation with circular linear progressions. In Proceedings of the Fifth IEEE/ACM International Conference on Formal Methods and Models for Codesign. IEEE, 39--48. Google ScholarDigital Library
- Axel Simon and Andy King. 2007. Taming the wrapping of integer arithmetic. In Static Analysis, H. Riis Nielson and G. Filé (Eds.). Lecture Notes in Computer Science, Vol. 4634. Springer, 121--136. Google ScholarDigital Library
- Zhendong Su and David Wagner. 2004. A class of polynomially solvable range constraints for interval analysis without widenings and narrowings. In Tools and Algorithms for the Construction and Analysis of Systems, K. Jensen and A. Podelski (Eds.). Lecture Notes in Computer Science, Vol. 2988. Springer, 280--295.Google Scholar
- Douglas D. C. Teixera and Fernando M. Q. Pereira. 2011. The design and implementation of a non-iterative range analysis algorithm on a production compiler. In Proceedings of the 2011 Brazilian Symposium on Programming Languages.Google Scholar
- Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, and Armando Solar-Lezama. 2013. Towards optimization-safe systems: Analyzing the impact of undefined behavior. In Proceedings of the 24th ACM Symposium on Operating Systems Principles. ACM, New York, NY, 260--275. Google ScholarDigital Library
- Henry S. Warren Jr. 2003. Hacker’s Delight. Addison Wesley, New York, NY.Google Scholar
- Chao Zhang, Tielei Wang, Tao Wei, Yu Chen, and Wei Zou. 2010. IntPatch: Automatically fix integer-overflow-to-buffer-overflow vulnerability at compile-time. In Computer Security -- ESORICS 2010, D. Gritzalis, B. Preneel, and M. Theoharidou (Eds.). Lecture Notes in Computer Science, Vol. 6345. Springer, 71--86. Google ScholarDigital Library
- Chao Zhang, Wei Zou, Tielei Wang, Yu Chen, and Tao Wei. 2011. Using type analysis in compiler to mitigate integer-overflow-to-buffer-overflow threat. Journal of Computer Security 19, 6, 1083--1107. Google ScholarDigital Library
Index Terms
- Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss
Recommendations
A VLSI Residue Arithmetic Multiplier
Recently, residue arithmetic has received increased attention in the open literature. Using table lookup methods and high-speed memory, modular arithmetic has been demonstrated. However, the memory size limitation of ECL, bipolar, and high-speed MOS ...
The Use of Floating-Point and Interval Arithmetic in the Computation of Error Bounds
Three forms of interval floating-point arithmetic are defined in terms of absolute precision, relative precision, and combined absolute and relative precision. The absolute-precision form corresponds to the centered form of conventional rounded-interval ...
Analysis of modular arithmetic
Special Issue ESOP'05We consider integer arithmetic modulo a power of 2 as provided by mainstream programming languages like Java or standard implementations of C. The difficulty here is that, for w > 1, the ring Zm of integers modulo m = 2w has zero divisors and thus cannot be ...
Comments