From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA05947; Mon, 15 Jul 2002 10:23:25 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA05943 for ; Mon, 15 Jul 2002 10:23:25 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g6F8NNj01300; Mon, 15 Jul 2002 10:23:23 +0200 (MET DST) Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA05936; Mon, 15 Jul 2002 10:23:23 +0200 (MET DST) Date: Mon, 15 Jul 2002 10:23:23 +0200 From: Xavier Leroy To: Alessandro Baretta Cc: Ocaml Subject: Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer) Message-ID: <20020715102323.C5476@pauillac.inria.fr> References: <200207081952.PAA28813@hickory.cc.columbia.edu> <15657.61603.221054.289184@spike.artisan.com> <200207090442.AAA05638@hickory.cc.columbia.edu> <001f01c2271e$8037adf0$d100a8c0@warp> <3D2C5B77.6060303@ozemail.com.au> <200207102229.g6AMTKB22278@orchestra.cs.caltech.edu> <3D2ECE7F.5040108@ozemail.com.au> <20020714142540.A4150@gogol.zorgol> <3D317B70.4010605@baretta.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 1.0i In-Reply-To: <3D317B70.4010605@baretta.com>; from alex@baretta.com on Sun, Jul 14, 2002 at 03:24:00PM +0200 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > Of course, in the absence of some unusual > limitation on the expressive power of array creation and > indexing expression, the general problem of static detection > of array indexing errors is undecidable. Indeed. > I wonder if the compiler gurus at the INRIA know what kinds > of constraints imposed on the language would allow the > compiler to statically check array indexing. Well, for this purpose, array index expressions must be restricted to a sub-language where inequations between index expressions are decidable. A well-known such sub-language is Presburger arithmetic: index expressions are variables, constants, and sums and products of expressions. I don't know of any significantly more expressive sub-language that has the required decidability properties. > I can imagine a few applications, such as signal analysis, where the > program logic is simple enough that such a restricted language might > suffice, and come to the aid of the developer who presently uses > unsafe arrays for the sake of speed, but with no help from the > compiler at prooving that the program is correct with respect to > array indexing. Obligatory preliminary remark: the cost of run-time array bound checks is not that high, since on modern processors it is performed largely in parallel with the actual array access. On my tests, ocamlopt -unsafe is at best 25% faster than ocamlopt on array intensive programs. This said, the approach you outline was investigated in depth by Hongwei Xi in his work on Dependent ML: http://www.ececs.uc.edu/~hwxi/DML/DML.html It's an interesting reading. - Xavier Leroy ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners