Re: Ada subtypes and base types

[Laurent GUERBY <laurent at guerby dot net>]

On Tue, 2006-03-21 at 11:29 -0500, Diego Novillo wrote:
> On 03/21/06 03:25, Laurent GUERBY wrote:
> 
> > A casual read of tree-vrp.c showed that symbolic_range_p is mostly
> > used to do nothing, did I miss something? May be it's in another file.
> > 
> That's correct.  We mostly punt on symbolic ranges because they are
> fairly expensive to track.  We do try to use symbolic range information
> in some places like 'if (a_3 > b_10)'.  If b_10's range is [a_3, +INF]
> then we know the conditional is false.
> 
> Do you have anything specific in mind that you would like to track?  Any
> kind of heavy symbolic processing will likely be very expensive.  And
> VRP already is a hog.

The typical Ada check we'd want to remove is below. I suspect Java
and Pascal are similar (Java has only one variable bound IIRC,
the first is always zero).

procedure T is

   -- Natural means [0 .. 2**32-1]
   procedure P (X : in out String; N1, N2 : in Natural) is
      First : constant Natural := X'First;
      Last  : constant Natural := X'Last;
   begin
      for I in First + N1 .. Last - N2 loop
         X (I) := ' '; -- CHECK that I>=X'First and I<=X'Last
      end loop;
   end P;

   S : String := "123456";

begin
   P (S, 2, 1);
   if S /= "12   6" then
      raise Program_Error;
   end if;
end T;

The Ada front-end expanded codes look like (gcc -c -gnatdg t.adb) :

   procedure t__p (x : in out string; n1 : in natural; n2 : in natural) is
      subtype t__p__S1b is string (x'first(1) .. x'last(1));
      first : constant natural := {x'first};
      last : constant natural := {x'last};
      L_1 : label
   begin
      S2b : integer;
      S2b := first + n1;
      S3b : integer;
      S3b := last - n2;
      L_1 : for i in S2b .. S3b loop
         [constraint_error when not (integer(i) in x'first .. x'last) "index check failed"]
         x (i) := ' ';
      end loop L_1;
      return;
   end t__p;


So we know:

- First, Last, N1, N2 are locally constant
- N1 >= 0 
- N2 >= 0
- First + N1 didn't overflow
- Last - N2 didn't overflow

And within the loop body:

- I >= First + N1
- I <= Last - N2
- First + N1 <= Last - N2

We'd need to track enough to prove that the following are always true

- I >= First 
- I <= Last

So the FE generated check can be removed.

Looks like not very far from what you describe, but I'm not a specialist
of those issues.

Laurent