Efficient and effective array bound checking

ABSTRACT

Array bound checking refers to determining whether all array references in a program are within their declared ranges. This checking is critical for software verification and validation because subscripting arrays beyond their declared sizes may produce unexpected results, security holes, or failures. It is available in most commercial compilers but current implementations are not as efficient and effective as one may have hoped: (1) the execution times of array bound checked programs are increased by a factor of up to 5, (2) the compilation times are increased, which is detrimental to development and debugging, (3) the related error messages do not usually carry information to locate the faulty references, and (4) the consistency between actual array sizes and formal array declarations is not often checked.This article presents two optimization techniques that deal with Points 1, 2, and 3, and a new algorithm to tackle Point 4, which is not addressed by the current literature. The first optimization technique is based on the elimination of redundant tests, to provide very accurate information about faulty references during development and testing phases. The second one is based on the insertion of unavoidable tests to provide the smallest possible slowdown during the production phase. The new algorithm ensures the absence of bound violations in every array access in the called procedure with respect to the array declarations in the calling procedure. Our experiments suggest that the optimization of array bound checking depends on several factors, not only the percentage of removed checks, usually considered as the best improvement measuring metrics. The debugging capability and compile-time and run-time performances of our techniques are better than current implementations. The execution times of SPEC95 CFP benchmarks with range checking added by PIPS, our Fortran research compiler, are slightly longer, less than 20%, than that of unchecked programs. More problems due to functional and data recursion would have to be solved to extend these results from Fortran to other languages such as C, C++, or Java, but the issues addressed in this article are nevertheless relevant.

REFERENCES

• 1: Aneesh Aggarwal , Keith H. Randall, Related field analysis, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.214-220, June 2001, Snowbird, Utah, United States
• 2: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 3: Frances Allen , Michael Burke , Philippe Charles , Ron Cytron , Jeanne Ferreant, An overview for the PTRAN analysis system for multiprocessing, Journal of Parallel and Distributed Computing, v.5 n.5, p.617-640, October 1988 [doi>10.1016/0743-7315(88)90015-9]
• 4: Tal Lev-Ami , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Putting static analysis to work for verification: A case study, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.26-38, August 21-24, 2000, Portland, Oregon, United States
• 5: Corinne Ancourt , François Irigoin, Scanning polyhedra with DO loops, Proceedings of the third ACM SIGPLAN symposium on Principles and practice of parallel programming, p.39-50, April 21-24, 1991, Williamsburg, Virginia, United States
• 6: Corinne Ancourt , Thi Viet Nga Nguyen, Array resizing for scientific code debugging, maintenance and reuse, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.32-37, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379656]
• 7: ANSI. 1983. Programming Language FORTRAN, ANSI X3.9-1978, ISO 1539-1980. American National Standard Institute, New York, NY.
• 8: Jonathan M. Asuru, Optimization of array subscript range checks, ACM Letters on Programming Languages and Systems (LOPLAS), v.1 n.2, p.109-118, June 1992 [doi>10.1145/151333.151392]
• 9: Todd M. Austin , Scott E. Breach , Gurindar S. Sohi, Efficient detection of all pointer and array access errors, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.290-301, June 20-24, 1994, Orlando, Florida, United States
• 10: Rastislav Bodík , Rajiv Gupta , Vivek Sarkar, ABCD: eliminating array bounds checks on demand, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.321-333, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: David Callahan , Ken Kennedy, Analysis of interprocedural side effects in a parallel programming environment, Journal of Parallel and Distributed Computing, v.5 n.5, p.517-550, October 1988 [doi>10.1016/0743-7315(88)90011-1]
• 12: Wei-Ngan Chin , Eak-Khoon Goh, A reexamination of “Optimization of array subscript range checks”, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.2, p.217-227, March 1995 [doi>10.1145/201059.201063]
• 13: Cousot, P. and Cousot, R. 1976. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming. 106--130.
• 14: Cousot, P. and Cousot, R. 1977. Static determination of dynamic properties of recursive programs. In Proceedings of the IFIP Conference on Formal Description of Programming Concepts. 237--277.
• 15: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 16: Béatrice Creusillet , François Irigoin, Interprocedural Array Region Analyses, Proceedings of the 8th International Workshop on Languages and Compilers for Parallel Computing, p.46-60, August 10-12, 1995
• 17: Béatrice Creusillet , François Irigoin, Exact versus Approximate Array Region Analyses, Proceedings of the 9th International Workshop on Languages and Compilers for Parallel Computing, p.86-100, August 08-10, 1996
• 18: Delzanno, G., Jung, G., and Podelski, A. 2000. Static analysis of array bounds as infinite-state model checking. Unpublished article.
• 19: Nurit Dor , Michael Rodeh , Shmuel Sagiv, Cleanness Checking of String Manipulations in C Programs via Integer Analysis, Proceedings of the 8th International Symposium on Static Analysis, p.194-212, July 16-18, 2001
• 20: Evelyn Duesterwald , Rajiv Gupta , Mary Lou Soffa, A practical data flow framework for array reference analysis and its use in optimizations, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.68-77, June 21-25, 1993, Albuquerque, New Mexico, United States
• 21: Jozo J. Dujmovic , Ivo Dujmovic, Evolution and evaluation of SPEC benchmarks, ACM SIGMETRICS Performance Evaluation Review, v.26 n.3, p.2-9, Dec. 1998 [doi>10.1145/306225.306228]
• 22: David Evans , David Larochelle, Improving Security Using Extensible Lightweight Static Analysis, IEEE Software, v.19 n.1, p.42-51, January 2002 [doi>10.1109/52.976940]
• 23: Feautrier, P. 1991. Dataflow analysis of array and scalar references. Int. J. Parall. Programm. 20, 1, 23--53.
• 24: Junjie Gu , Zhiyuan Li, Efficient Interprocedural Array Data-Flow Analysis for Automatic Program Parallelization, IEEE Transactions on Software Engineering, v.26 n.3, p.244-261, March 2000 [doi>10.1109/32.842950]
• 25: Manish Gupta , Sayak Mukhopadhyay , Navin Sinha, Automatic Parallelization of Recursive Procedures, International Journal of Parallel Programming, v.28 n.6, p.537-562, December 2000 [doi>10.1023/A:1007560600904]
• 26: Rajiv Gupta, A fresh look at optimizing array bound checking, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.272-282, June 1990, White Plains, New York, United States
• 27: Rajiv Gupta, Optimizing array bound checks using flow analysis, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.135-150, March–Dec. 1993 [doi>10.1145/176454.176507]
• 28: Mary W. Hall , Brian R. Murphy , Saman P. Amarasinghe , Shih-Wei Liao , Monica S. Lam, Interprocedural Analysis for Parallelization, Proceedings of the 8th International Workshop on Languages and Compilers for Parallel Computing, p.61-80, August 10-12, 1995
• 29: Harrison, W. H. 1977. Compiler analysis of the value ranges for variables. IEEE Trans. Softw. Eng. SE-3, 3 (May), 243--250.
• 30: Hasting, R. and Joyce, B. 1992. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Winter USENIX Conference. 125--136.
• 31: Michael Hind , Michael Burke , Paul Carini , Sam Midkiff, An empirical study of precise interprocedural array analysis, Scientific Programming, v.3 n.3, p.255-271, Fall 1994
• 32: Jay P. Hoeflinger , Yunheung Paek , Kwang Yi, Unified Interprocedural Parallelism Detection, International Journal of Parallel Programming, v.29 n.2, p.185-215, April 2001 [doi>10.1023/A:1007685003043]
• 33: François Irigoin , Pierre Jouvelot , Rémi Triolet, Semantical interprocedural parallelization: an overview of the PIPS project, Proceedings of the 5th international conference on Supercomputing, p.244-251, June 17-21, 1991, Cologne, West Germany [doi>10.1145/109025.109086]
• 34: Jones, R. W. M. and Kelly, P. H. J. 1997. Backwards-compatible bounds checking for arrays and pointers in C programs. In Proceedings of the Third International Workshop on Automated Debugging.
• 35: Karr, M. 1976. Affine relationship among variables of a program. Acta Informatica, 6, 133--151.
• 36: Priyadarshan Kolte , Michael Wolfe, Elimination of redundant array subscript range checks, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.270-278, June 18-21, 1995, La Jolla, California, United States
• 37: Sumant Kowshik , Dinakar Dhurjati , Vikram Adve, Ensuring code safety without runtime checks for real-time control systems, Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems, October 08-11, 2002, Grenoble, France [doi>10.1145/581630.581678]
• 38: Leservot, A. 1996. Analyses interprocédurales du flot des données. Ph.D. dissertation. Université Paris VI, Paris, France.
• 39: Yuan Lin , David A. Padua, Demand-Driven Interprocedural Array Property Analysis, Proceedings of the 12th International Workshop on Languages and Compilers for Parallel Computing, p.303-317, August 04-06, 1999
• 40: Manjunathaiah, M. and Nicole, D. A. 1997. Precise analysis of array usage in scientific programs. Sci. Programm. 6, 229--242.
• 41: Victoria Markstein , John Cocke , Peter Markstein, Optimization of range checking, ACM SIGPLAN Notices, v.17 n.6, p.114-119, June 1982
• 42: Dror E. Maydan , Saman P. Amarasinghe , Monica S. Lam, Array-data flow analysis and its use in array privatization, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.2-15, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158515]
• 43: S. P. Midkiff , J. E. Moreira , M. Snir, Optimizing array reference checking in Java programs, IBM Systems Journal, v.37 n.3, p.409-453, 1998
• 44: José E. Moreira , Samuel P. Midkiff , Manish Gupta, From flop to megaflops: Java for technical computing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.265-295, March 2000 [doi>10.1145/349214.349222]
• 45: José E. Moreira , Samuel P. Midkiff , Manish Gupta , Pedro V. Artigas , Peng Wu , George Almasi, The NINJA project, Communications of the ACM, v.44 n.10, p.102-109, Oct. 2001 [doi>10.1145/383845.383867]
• 46: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 47: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 48: Trung N. Nguyen , Junjie Gu , Zhiyuan Li, An Interprocedural Parallelizing Compiler and Its Support for Memory Hierarchy Research, Proceedings of the 8th International Workshop on Languages and Compilers for Parallel Computing, p.96-110, August 10-12, 1995
• 49: Nguyen, T. V. N. 2002. Efficient and effective software verifications for scientific applications using static analyses and code instrumentation. Ph.D. dissertation. Ecole des Mines de Paris, Paris, France.
• 50: Yunheung Paek , Jay Hoeflinger , David Padua, Efficient and precise array access analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.1, p.65-109, January 2002 [doi>10.1145/509705.509708]
• 51: Harish Patil , Charles Fischer, Low-cost, concurrent checking of pointer and array accesses in C programs, Software—Practice & Experience, v.27 n.1, p.87-110, Jan. 1997 [doi>10.1002/(SICI)1097-024X(199701)27:1<87::AID-SPE78>3.0.CO;2-P]
• 52: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 53: Feng Qian , Laurie J. Hendren , Clark Verbrugge, A Comprehensive Approach to Array Bounds Check Elimination for Java, Proceedings of the 11th International Conference on Compiler Construction, p.325-342, April 08-12, 2002
• 54: S. Richardson , M. Ganapathi, Interprocedual optimization: experimental results, Software—Practice & Experience, v.19 n.2, p.149-169, February 1989 [doi>10.1002/spe.4380190205]
• 55: Radu Rugina , Martin Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.182-195, June 18-21, 2000, Vancouver, British Columbia, Canada
• 56: Alexandeer Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986
• 57: B. Schwarz , W. Kirchgässner , R. Landwehr, An optimizer for Ada - design, experiences and results, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.175-184, June 20-24, 1988, Atlanta, Georgia, United States
• 58: Madalene Spezialetti , Rajiv Gupta, Loop Monotonic Statements, IEEE Transactions on Software Engineering, v.21 n.6, p.497-505, June 1995 [doi>10.1109/32.391376]
• 59: Joseph L. Steffen, Adding run-time checking to the portable C compiler, Software—Practice & Experience, v.22 n.4, p.305-316, April 1992 [doi>10.1002/spe.4380220403]
• 60: Norihisa Suzuki , Kiyoshi Ishihata, Implementation of an array bound checker, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.132-143, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512963]
• 61: Rémi Triolet , Paul Feautrier , François Irigoin, Automatic Parallelization of Fortran Programs in the Presence of Procedure Calls, Proceedings of the European Symposium on Programming, p.210-222, March 17-19, 1986
• 62: Peng Tu , David Padua, Gated SSA-based demand-driven symbolic analysis for parallelizing compilers, Proceedings of the 9th international conference on Supercomputing, p.414-423, July 03-07, 1995, Barcelona, Spain [doi>10.1145/224538.224648]
• 63: David A. Wagner , Eric A. Brewer, Static analysis and computer security: new techniques for software assurance, 2000
• 64: Welsh, J. 1978. Economic range checks in Pascal. Soft.---Pract. Exper. 8, 85--97.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Symbolic execution; Debugging aids
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers; Optimization

Keywords:
Array bound checking, interprocedural analysis