An Inter-Procedural Algorithm for Variable Width Analysis

• Douglas do Couto Teixeira UFMG
• Fernando Magno Quintão Pereira UFMG

Abstract

During this project we have developed an inter-procedural range analysis algorithm that scales up to programs with millions of assembly instructions. Contrary to many previous techniques, we handle comparisons between variables without resorting to expensive algorithms. We achieve path sensitiveness by using Bodik’s Extended Static Single Assignment form as the intermediate representation. We show that by processing the strongly connected components that constitute the graph of dependences between variables in topological order we not only gain in time, but also in precision. We have implemented our technique in LLVM, an industrial strength compiler, and have been able to process over 4 million assembly instructions in a few seconds.

References

Bodik, R., Gupta, R., and Sarkar, V. (2000). ABCD: eliminating array bounds checks on demand. In PLDI, pages 321–333. ACM.

Cong, J., Fan, Y., Han, G., Lin, Y., Xu, J., Zhang, Z., and Cheng, X. (18-21 Jan. 2005). Bitwidth-aware scheduling and binding in high-level synthesis. Design Automation Conference, 2005. Proceedings of the ASP-DAC 2005. Asia and South Pacific, 2:856–861.

Cousot, P. and Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238–252. ACM.

Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N., and Zadeck, F. K. (1991). Efficiently computing static single assignment form and the control dependence graph. TOPLAS, 13(4):451–490.

Ferrante, J., Ottenstein, K. J., and Warren, J. D. (1987). The program dependence graph and its use in optimization. TOPLAS, 9(3):319–349.

Gawlitza, T., Leroux, J., Reineke, J., Seidl, H., Sutre, G., and Wilhelm, R. (2009). Polynomial precise interval analysis revisited. Efficient Algorithms, 1:422 – 437.

Henning, J. L. (2006). Spec cpu2006 benchmark descriptions. SIGARCH Comput. Archit. News, 34(4):1–17.

Lattner, C. and Adve, V. S. (2004). LLVM: A compilation framework for lifelong program analysis & transformation. In CGO, pages 75–88. IEEE.

Mahlke, S., Ravindran, R., Schlansker, M., Schreiber, R., and Sherwood, T. (2001). Bitwidth cognizant architecture synthesis of custom hardware accelerators. ComputerAided Design of Integrated Circuits and Systems, IEEE Transactions on, 20(11):1355–1371.

Oh, H., Heo, K., Lee, W., Lee, W., and Yi, K. (2012). Design and implementation of sparse global analyses for c-like languages. In PLDI, page to appear. ACM.

Patterson, J. R. C. (1995). Accurate static branch prediction by value range propagation. In PLDI, pages 67–78. ACM.

Simon, A. (2008). Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities. Springer, 1th edition.

Souza, M. R. S., Guillon, C., Pereira, F. M. Q., and da Silva Bigonha, M. A. (2011). Dynamic elimination of overflow tests in a trace compiler. In CC, pages 2–21.

Stephenson, M., Babb, J., and Amarasinghe, S. (2000). Bitwidth analysis with application to silicon compilation. In PLDI, pages 108–120. ACM.

Su, Z. and Wagner, D. (2005). A class of polynomially solvable range constraints for interval analysis without widenings. Theoretical Computeter Science, 345(1):122–138.

Teixeira, D. and Pereira, F. M. Q. (2011). The design and implementation of a noniterative range analysis algorithm on a production compiler. In SBLP, pages 45–59. SBC.

Wagner, D., Foster, J. S., Brewer, E. A., and Aiken, A. (2000). A first step towards automated detection of buffer overrun vulnerabilities. In NDSS, pages 3–17. ACM.