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

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

[Johan Baltié]

Ok as there were the two same comments on my post I do a single answer.

Here my first post:

>> What about defining type that are subranges of int ?
>> à la ADA...


Here the comments:
-----
>Then how do you make sure that the result of an arithmetic expression is
>still within that sub-range? For example, m.( i + j ) ?
>
>Cheers,
>Hao-yang Wang

-----

>as i said to john skaller, won't you then get index incrementation exceptions ?
>anyway, it's a trade-off.
>
>-- 
>Berke
>mayur_naik@my-deja.com writes:

-----

Now, as I am not an ADA guru I just show you my source:

http://groups.google.com/groups?hl=fr&lr=&ie=UTF-8&oe=UTF-8&frame=right&th=5c68b368acf1e99&seekm=00-04-194%40comp.compilers#link5

------------- BEGIN OF FOLLOWUP -------------

> Does any language or any machine provide some mechanism to:
>
> 1. index an array without checking its bounds
> 2. throw an exception if the index was actually out of range
> 3. allow the programmer to catch and handle the exception rather than
>    terminate the program

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;

--
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,
blaak@infomatch.com                            The Rhythm has my soul.

------------- END OF FOLLOWUP -------------

IMHO, the use of subtypes help to avoid a lot of bound check, maybe not all of
them, but I do not think that eliminating *all* the bounds check is useful.

Another point is that using subranges you're not allowed to do many errors as
when you are using bare int.

Ciao

Jo
-------------------
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

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

[Jacques Garrigue]

[-- 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

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

[Johan Baltié]

> 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).  

No it's not such a mess.
A subrange is  a type. As ocaml is a bit strong on is types it solves itself the
problem

     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

the {..} are my subranges types

bubble_one: a' {0..b'} array -> int -> unit
swap: {0..b'} -> unit

the "for" should be like in Ada, working with range types and no problem will
ever occur.

> 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.

If you move swap out of the function, in another one using another array, the
type will change and a warning/error/check will occur if the types are incompatible.


> [snipped]
>     Jacques Garrigue


Ciao

Jo
-------------------
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

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

[Jacques Garrigue]

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

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

> > 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).  
> 
> No it's not such a mess.  A subrange is a type. As ocaml is a bit
> strong on is types it solves itself the problem

OK, I should have been clearer about my basic assumption: I was
talking about what you can do _without_ modifying the typing.
Modifying the typing is a mess: if your bounds are no longer integers,
then how can you convert between them and integers, back and forth.
You could use subtyping in one direction, but there is no implicit
subtyping in ocaml, as this would badly break type inference.

> > 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.
> 
> If you move swap out of the function, in another one using another array, the
> type will change and a warning/error/check will occur if the types
> are incompatible.

No, I was just saying moving swap to the toplevel:
  let swap arr i = ....

Supposing you use the original plain type, you are in trouble.

But it looks like you're just asking for dependent types, no less...

I think this discussion started on efficiency considerations;
my belief is that you can already already optimize a lot, without
using fancy type systems. Such type systems are not only hard to
implement (and mix with an existing type system);  while they
certainly take bugs, they also get in your way when you get out of
their small understanding.

Cheers,

        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

Re: [Caml-list] Sub{range,type} (was: Statically detecting arrays bound exceptions ??)

[Johan Baltié]

> From: "Johan Baltié" <johan.baltie@wanadoo.fr>
> 
> > > 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).  
> > 
> > No it's not such a mess.  A subrange is a type. As ocaml is a bit
> > strong on is types it solves itself the problem
> 
> OK, I should have been clearer about my basic assumption: I was
> talking about what you can do _without_ modifying the typing.
> Modifying the typing is a mess: if your bounds are no longer integers,
> then how can you convert between them and integers, back and forth.
> You could use subtyping in one direction, but there is no implicit
> subtyping in ocaml, as this would badly break type inference.

*sigh* :,(
I was dreaming of that kind of stuff.

But I do not see why type inference reach an end with subtyping.
Can you elaborate on this ?
 
> > > 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.
> > 
> > If you move swap out of the function, in another one using another array, the
> > type will change and a warning/error/check will occur if the types
> > are incompatible.
> 
> No, I was just saying moving swap to the toplevel:
>   let swap arr i = ....
> 
> Supposing you use the original plain type, you are in trouble.
> 
> But it looks like you're just asking for dependent types, no less...

I did not know this name, and after a quick browse I can answer: "Yes" :)

 
> I think this discussion started on efficiency considerations;
> my belief is that you can already already optimize a lot, without
> using fancy type systems. 
Ok, I left the previous thread, cause I'm getting totally of topic.

> Such type systems are not only hard to
> implement (and mix with an existing type system);  while they
> certainly take bugs, they also get in your way when you get out of
> their small understanding.
With my new and small understanding of dependent type, it seems to me that Ada
types look a lot like this. It seems to add power to the type checker, so why
would this be a bad thing ? Did I miss something ?


The only problem that I see is that if you consider list type dependent of size,
this kind of type cannot staticaly determined (is it the point that break type
inference ?).

Ciao

Jo
-------------------
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

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

[Florian Hars]

Oleg wrote:
> On Monday 15 July 2002 04:39 am, Noel Welsh wrote:
> 
>>FiSH (ask Google; I'm feeling lazy)
> 
> Even Altavista doesn't support case-sensitive searches anymore.

Learn to use search engines intelligently: You know that *FiSH* (correct 
capitalization is FISh, so a case sensitive search wouldn't have bought 
you anything, anyway :-)) is a *language* with good *array* processing 
capabilities. So here we go:

http://www.google.com/search?q=fish+language+array

The first four results are relevant.

Yours, Florian Hars

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

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

[Michael Vanier]

http://www-staff.mcs.uts.edu.au/~cbj/FISh/

Mike

> From: Oleg <oleg_inconnu@myrealbox.com>
> Date: Mon, 15 Jul 2002 17:22:35 -0400
> 
> On Monday 15 July 2002 04:39 am, Noel Welsh wrote:
> > FiSH (ask
> > Google; I'm feeling lazy)
> 
> Even Altavista doesn't support case-sensitive searches anymore.
> 
> Oleg
-------------------
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

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

[Oleg]

On Monday 15 July 2002 04:39 am, Noel Welsh wrote:
> FiSH (ask
> Google; I'm feeling lazy)

Even Altavista doesn't support case-sensitive searches anymore.

Oleg
-------------------
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

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

[Noel Welsh]

--- Alessandro Baretta <alex@baretta.com> wrote:
> 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. 

I'm not a compiler guru from INRIA but I can point out
the languages SAC (Single Assignment C) and FiSH (ask
Google; I'm feeling lazy) that do array shape
inference.  Basically the type system for arrays in
augmented by their shape and shapes are inferred in a
similar way to types.  In addition to eliminating
bounds checks the compiler can do funky reordering
optimisations (because these are functional languages,
so evaluation order is not important) and produce code
faster than Fortran. Exciting stuff if you're into
numerical code.

Noel

__________________________________________________
Do You Yahoo!?
Yahoo! Autos - Get free new car price quotes
http://autos.yahoo.com
-------------------
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

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

[Xavier Leroy]

> 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

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

[Alessandro Baretta]

Berke Durak wrote:
> On Fri, Jul 12, 2002 at 10:41:35PM +1000, John Max Skaller wrote:
> [...]
> 
> Hey, wait a minute, how do you plan to statically detect bounds exceptions ?
> It's as undecidable as detecting infinite recursions.
> 
> 	let rec f () =
> 	   let a = [|1;2|] in
>        if compiler_is_gonna_say_that_there_is_gonna_be_a_bounds_error f then
>           a.(0)
>        else
>           a.(3)

If the compiler attempted to catch at least the most evident 
  bounds errors, it would very simply detect that your code 
contains an expression which, if evaluated, would raise a 
runtime bounds error. Hence, the compiler should simply 
reject the code. 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.

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. 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.

I have a feeling that most applications which would benefit 
from static checking of array indexing boil down to finite 
state automata. I'm pretty sure that a language based of 
FSAs could do static bounds checking.

Alex

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

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

[Berke Durak]

On Fri, Jul 12, 2002 at 10:41:35PM +1000, John Max Skaller wrote:
[...]
> Ocaml run time errors include array (and string) bounds exceptions and 
> infinite recursions:
> static type checking could detect the first, but not the second.

Hey, wait a minute, how do you plan to statically detect bounds exceptions ?
It's as undecidable as detecting infinite recursions.

	let rec f () =
	   let a = [|1;2|] in
       if compiler_is_gonna_say_that_there_is_gonna_be_a_bounds_error f then
          a.(0)
       else
          a.(3)
-- 
Berke Durak
-------------------
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