Deriving Pre-conditions for Array Bound Check Elimination

  • Wei-Ngan Chin
  • Siau-Cheng Khoo
  • Dana N. Xu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2053)


We present a high-level approach to array bound check optimization that is neither hampered by recursive functions, nor disabled by the presence of partially redundant checks. Our approach combines a forward analysis to infer precise contextual constraint at designated program points, and a backward method for deriving a safety pre-condition for each bound check. Both analyses are formulated with the help of a practical constraint solver based on Presburger formulae; resulting in an accurate and fully automatable optimization. The derived pre-conditions are also used to guide bound check specialization, for the purpose of eliminating partially redundant checks.


Logic Program Recursive Function Recursive Call Contextual Constraint Call Site 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A.V. Aho, R. Sethi, and J.D. Ullman. Compilers, Principles, Techniques, and Tools. Addison-Wesley, 1986.Google Scholar
  2. [2]
    F. Benoy and A. King. Inferring argument size relationships with CLP(R). In Logic Programming Synthesis and Transformation, Springer-Verlag, August 1997.Google Scholar
  3. [3]
    R. Bodik, R. Gupta, and V. Sarkar. ABCD: Eliminating array bounds checks on demand. In ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 321–333, 2000.Google Scholar
  4. [4]
    W.N. Chin and S.C. Khoo. Calculating sized types. In 2000 ACM Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 62–72, Boston, Massachusetts, United States, January 2000.Google Scholar
  5. [5]
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Symposium on Principles of Programming Languages, pages 84–96. ACM Press, 1978.Google Scholar
  6. [6]
    F. Fioravanti, A. Pettorossi, and M. Proietti. Rules and stratigies for contextual specialization of constraint logic programs. Electronic Notes in Theoretical Computer Science, 30(2), 1990.Google Scholar
  7. [7]
    R. Gupta. A fresh look at optimizing array bound checking. In ACM SIGPLAN Conf. on Program Lang. Design and Impl., pages 272–282, New York, June 1990.Google Scholar
  8. [8]
    R. Gupta. Optimizing array bound checks using flow analysis. ACM Letters Program Lang. Syst., 2(1-4):135–150, Mar-Dec 1994.CrossRefGoogle Scholar
  9. [9]
    N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer Academic Pub., 1993.Google Scholar
  10. [10]
    N. Halbwachs. About synchronous programming and abstract interpretation. Science of Computer Programming, Special Issue on SAS’94, 31(1), May 1998.Google Scholar
  11. [11]
    N. Halbwachs, Y.E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, 1997.CrossRefGoogle Scholar
  12. [12]
    W. H. Harrison. Compiler analysis for the value ranges for variables. IEEE TOSE, SE-3(3):243–250, May 1977.Google Scholar
  13. [13]
    P. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The Omega Library Version 1.1.0 Interface Guide. Technical report, University of Maryland, College Park, November 1996. Scholar
  14. [14]
    A. King, K. Shen, and F. Benoy. Lower-bound time-complexity analysis of logic programs. In Jan Maluszynski, editor, International Symposium on Logic Programming, pages 261–276. MIT Press, November 1997.Google Scholar
  15. [15]
    P Kolte and M Wolfe. Elimination of redundant array subscript range checks. In ACM Conference on Programming Language Design and Implementation, pages 270–278. ACM Press, June 1995.Google Scholar
  16. [16]
    L. Lafave and J. Gallagher. Constraint-based partial evaluation of rewritingbased functional logic programs. In Program Synthesis and Transformation, LOPSTR’ 97, pages 70–82, LNCS 1463, 1997.Google Scholar
  17. [17]
    V. Markstein, J. Cooke, and P. Markstein. Optimization of range checking. In ACM SIGPLAN Symp. on Compiler Construction, pages 114–119, June 1982.Google Scholar
  18. [18]
    S.P. Midkiff, J.E. Moreira, and M. Snir. Optimizing bounds checking in Java programs. IBM Systems Journal, 37(3):409–453, 1998.CrossRefGoogle Scholar
  19. [19]
    G. Necula. Proof-carrying code. In ACM Principles of Programming Languages, pages 106–119, 1997.Google Scholar
  20. [20]
    G Necula and P. Lee. The design and implementation of a certifying compiler. In ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 333–344, 1998.Google Scholar
  21. [21]
    L. Plumer. Termination proofs for logic programs. In Lecture Notes in Artificial Intelligence, volume 446. Springer Verlag, 1990.Google Scholar
  22. [22]
    W. Pugh. The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of ACM, 8:102–114, 1992.CrossRefGoogle Scholar
  23. [23]
    R. Rugina and M. Rinard. Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 182–195. ACM Press, June 2000.Google Scholar
  24. [24]
    N. Suzuki and K. Ishihata. Implementation of array bound checker. In ACM Principles of Programming Languages, pages 132–143, 1977.Google Scholar
  25. [25]
    J.D. Ullman and A. Van Gelder. Efficient tests for top-down termination of logical rules. Journal of ACM, 35(2):345–373, 1988.CrossRefGoogle Scholar
  26. [26]
    H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In ACM Conference on Programming Language Design and Implementation, pages 249–257. ACM Press, June 1998.Google Scholar
  27. [27]
    Z. Xu, B.P. Miller, and T. Reps. Safety checking of machine code. In ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 70–82. ACM Press, June 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Wei-Ngan Chin
    • 1
  • Siau-Cheng Khoo
    • 1
  • Dana N. Xu
    • 1
  1. 1.School of ComputingNational University of SingaporeSingapore

Personalised recommendations