Re: array index checking optimizations?

Stephen Adams wrote:
>
> I am curious if there are any compilers out there that can detect that
> all the array references in the following program are safe, and thus
> no array indexes need to be checked.
>


Old references on interval analysis are:


\bibitem{CousotCousot76-1}
P.~Cousot and R.~Cousot.
\newblock Static determination of dynamic properties of programs.
\newblock In {\em Proceedings of the 2{$^{\rm\em nd}$} International
Symposium
    on Programming}, pages 106--130. Dunod, Paris, France, 1976.


\bibitem{CousotCousot77-1}
P.~Cousot and R.~Cousot.
\newblock Abstract interpretation: a unified lattice model for static
analysis
    of programs by construction or approximation of fixpoints.
\newblock In {\em Conference Record of the 4{$^{\rm\em th}$} Annual
ACM
    SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages
    238--252, Los Angeles, California, 1977. ACM Press, New York, New
York, {\sc usa}.


See a comparison of this old look at optimizing array bound checking
with:


@INPROCEEDINGS{rg90,
                AUTHOR = {Rajiv Gupta},
                TITLE = {A Fresh Look at Optimizing Array Bound
Checking},
                BOOKTITLE = {ACM SIGPLAN '90 Conference on Programming
Language Design and Implementation},
                YEAR = {1990},
                PAGES = {272-282},
                MONTH = {June}
}


(mentionned by Ksheerabdhi Krishna) in:


\bibitem{CousotCousot92-3}
P.~Cousot and R.~Cousot.
\newblock Abstract interpretation frameworks.
\newblock {\em Journal of Logic and Computation}, 2(4):511--547,
August 1992.


If interested in the implementation of this interval checking
by abstract interpretation, see:


@INCOLLECTION{Bourdoncle90-1,
      author = "Bourdoncle, F.",
      title = "Interprocedural Abstract Interpretation of Block
Structured Languages
                        with Nested Procedures, Aliasing and Recursivity",
      editor = "Deransart, P. and Ma{\l}uszy{\'n}ski, J.",
      booktitle = PROC # "International Workshop PLILP'90, " # PLILP,
      series = "Link{\"{o}}ping " # sweden # ", 20--22 " # aug # " 1990,
" # LNCS # 456,
      pages = "307--323",
      publisher = SPRINGER,
      year = "1990",
}


@ARTICLE{Bourdoncle92-1,
      author = "Bourdoncle, F.",
      title = "Abstract Interpretation by Dynamic Partitioning",
      journal = JFP,
      year = 1992,
      volume = 2,
      number = 4,
}


@PHDTHESIS{Bourdoncle92-2,
      author = "Bourdoncle, F.",
      title = "S\'emantiques des langages imp\'eratifs d'ordre
sup\'erieur et interpr\'etation
                        abstraite",
      school = "\'Ecole Polytechnique",
      type = "Th\`ese de doctorat de l'\'Ecole Polytechnique en
informatique",
      address = "Palaiseau, " # france,
      month = "13~" # nov,
      year = 1992,
}


@INCOLLECTION{Bourdoncle93-1,
      author = "Bourdoncle, F.",
      title = "Efficient Chaotic Iteration Strategies with Widenings",
      booktitle = PROC # FMPA,
      series = "Academgorodok, Novosibirsk, " # russia # ", " # LNCS #
"735",
      editor = "Bj\o rner, D. and Broy, M. and Pottosin, I.V.",
      pages = "128--141",
      publisher = SPRINGER,
      month = jun # " 28--" # jul # " 2,",
      year = 1993,
}


@INCOLLECTION{Bourdoncle93-2,
      author = "Bourdoncle, F.",
      title = "Abstract Debugging of Higher-Order Imperative Languages",
      booktitle = PROC # PLDI,
      pages = "46--55",
      publisher = ACMPress,
      year = 1993,
}


An implementation (called SYNTOX by Franc,ois Bourdoncle) is also
available
(for a subset of PASCAL), if you have a look at:


  http://www.ensmp.fr/~bourdonc
  http://www.ensmp.fr/~bourdonc/syntox.tar.z


If you write your example in Pascal included in a main program (i.e.
something has to be known about the bounds, and the possible calls), I
can try it with SYNTOX (which performs Abstract Debugging of full
programs).


Best regards,


--
Patrick COUSOT tel.: +33 1 44 32 20 64
ENS -- DMI fax.: +33 1 44 32 20 80
45 rue d'Ulm email: cousot@dmi.ens.fr
Patrick.Cousot@ens.fr
F-75230 Paris cedex 05 (France) URL: http://www.ens.fr/~cousot


--

Return to the comp.compilers page.
Search the comp.compilers archives again.