Re: [Camllist] Statically detecting arrays bound exceptions ?? (was: Universal Serializer)

Johan Baltié

Jacques Garrigue
 Johan Baltié

Jacques Garrigue
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Johan Baltié <johan.baltie@w...> 
Subject:  Re: [Camllist] Statically detecting arrays bound exceptions ?? (was: Universal Serializer) 
> 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 outofrange 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 camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners