Re: [Caml-list] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: Text/Plain; charset=us-ascii, Size: 2454 bytes --]

From: "Johan Baltié" <johan.baltie@wanadoo.fr>

> Well, Ada does. The strong typing gives information to the compiler for it to
> deduce when range checking is not needed:
> 
> declare
>   subtype Index is Integer range 1..10;
>   type Arr is array (Index) of Integer;
>   a : Arr;
>   element : Integer;
>   j : Index := 1;
>   k : Integer := 11;
> begin
>   for i in a'Range loop
>     element := a(i); -- no range checking needed, i is in range by definition
>   end loop;
>   a(j); -- range checking not needed, j is within Index by definition
>   a(k); -- range checking needed due possibility of k being outside of Index
> exception
>   when Constraint_Error =>
>      -- process the out-of-range error from a(k)
> end;

This is similar to Pascal ranges.
The trouble is that typical code doesn't look like that, but rather

    let bubble_once arr =
      for i = 0 to Array.length arr - 2 do
        if arr.(i) > arr.(i+1) then begin
          let tmp = arr.(i) in
          arr.(i) <- arr.(i+1);
          arr.(i+1) <- tmp
        end
      done

or worse

    let bubble_one arr last =
      assert (last < Array.length arr);
      let swap i =
        let tmp = arr.(i) in
        arr.(i) <- arr.(i+1);
        arr.(i+1) <- tmp
      in
      for i = 0 to last - 1 do
        if arr.(i) < arr.(i+1) then swap i
      done

In the first case, that's not too difficult: you just have to know
that Array.length returns the length of an array, and do a bit of
arithmetic.

In the second case, you should propagate the information from the
assertion to the loop bound, and additionally treat swap as if it were
inlined (we know it is its only call context).  And it's fragile:
if you move "swap" out of the function, then it might be used on any
array, and you have to do the bound check.
By the way: if you forgot the assertion, would it be ok to have the
compiler insert it automagically and fail early?  As I see an
out-of-bound error as fatal, this would seem reasonnable to me, but
this should be somewhere in the semantics of the language.

There are lots of things you can do without real type inference, but
the real trouble is that what is a reasonable target is not clear...

    Jacques Garrigue
-------------------
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