[PATCH] Improve PR30911 and PR31023, Ada and VRP

[Eric Botcazou]

> However I thought the plan was to use VIEW_CONVERT_EXPR to implement the
> check as this instead: 
>
>   Y = VIEW_CONVERT_EXPR(X, base_type);
>   if Y < 1 or Y > 10 then
>     raise_exception;
>   end if;
>   A(X);
>
> In which case VRP will not remove the check because VIEW_CONVERT_EXPR is
> a "VRP barrier".

That's right, for

procedure P is

    subtype X is integer range 1 .. 10;
    Q : array (X) of integer;

    procedure R (M : X) is
    begin
       Q (M) := 3;
    end;

   My_X : X;

begin
  R(My_X);
end;

the front-end generates

with interfaces;

procedure p is
   subtype p__x is integer range 1 .. 10;
   [type p__TqB is array (1 .. 10 range <>) of integer]
   freeze p__TqB []
   [subtype p__TqT is p__TqB (1 .. 10)]
   freeze p__TqT []
   q : array (1 .. 10) of integer;

   procedure p__r (m : p__x) is
   begin
      [constraint_error when
        not (interfaces__unsigned_32!(m) >= 1 and then
          interfaces__unsigned_32!(m) <= 10)
        "invalid data"]
      q (m) := 3;
      return;
   end p__r;

   my_x : p__x;
begin
   p__r (my_x);
   return;
end p;

and Gigi

P.R (m)
{
  interfaces__unsigned_32 D.182;
  interfaces__unsigned_32 D.183;
  <unnamed-signed:32> m.0;

  D.182 = VIEW_CONVERT_EXPR<interfaces__unsigned_32>(m);
  if (D.182 == 0)
    {
      goto <D.180>;
    }
  else
    {
      
    }
  D.183 = VIEW_CONVERT_EXPR<interfaces__unsigned_32>(m);
  if (D.183 > 10)
    {
      goto <D.180>;
    }
  else
    {
      goto <D.181>;
    }
  <D.180>:;
  __gnat_rcheck_06 ("p.adb", 8);
  <D.181>:;
  m.0 = (<unnamed-signed:32>) m;
  q[m.0]{lb: 1 sz: 4} = 3;
  return;
}

> If VIEW_CONVERT_EXPR was used for all checks that ensure that a bounded
> error does not turn into an unbounded error, then teaching VRP that
> variables are in the range of their types would not result in a bounded
> error escalating into an unbounded error.  In particular, assuming that
> parameters are in the range of their types would not result in the bounded
> error of them not being in range turning into an unbounded error.

Yes, this might be a valid (and subtle) reasoning: we would be entitled to 
remove all useless checks based on the assumption that the parameters are in 
the range of their types, except for the validity checks.  Since the latter 
checks are already specifically protected wrt VRP, we could teach VRP about 
these ranges, like Richard G. did and what gave him a clean ACATS.

> That said, it is not clear exactly what is allowed when there is a bounded
> error.  For example, the Ada reference manual seems to require that
> uninitialized values behave deterministically.  Suppose X is uninitialized
> (using it is then a bounded error).  In the following code
>   if X = 0 then
>     do_something_with_X;
>   end if;
> must X have the value 0 in do_something_with_X?
> [...]
> If the type of X had the range 0 .. 0, then allowing VRP to reason based on
> type ranges could likewise cause do_something_with_X to be executed in the
> case of the bounded error of X containing an out of range value, i.e. not 0.

Indeed, but my understanding is that do_something_with_X must be prepared for 
invalid values of X (i.e. non-null values) in any cases and behaves in a 
bounded way for them, so there would be no error escalation.

-- 
Eric Botcazou