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
