This is the mail archive of the mailing list for the GCC project.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

Re: [PATCH] Improve PR30911 and PR31023, Ada and VRP

> This improves PR31023 by not folding comparisons as sign-changing
> just because we convert from a integral sub-type to its base-type
> as this also results in comparisons in a sub-type (similar to
> arithmetic in sub-types) and eventually constants that are not in
> the range of their types min/max value.

Thanks for your work in this area.

> With this fixed we can remove most of the range checking code
> that Ada emits for the testcase in PR30911 if we pre-seed
> parameter value-ranges in VRP with their types range.  This
> should be immune against other bugs in fold and safe as Ada
> ensures parameters are in range by checking code at the caller
> site.

The latter assertion is not true for GNAT and, consequently, you cannot 
pre-seed parameter ranges like that.

Here's an excerpt of a discussion we had internally a couple of years ago:

Bob Duff (Ada specialist)
"For example:

    Uninitialized : Range_Type; -- could be invalid
    B : Boolean;
    if not Uninitialized'Valid then
        B := Foo (Uninitialized);

 I think the call to Foo MUST either return False or raise an exception.
 Because we know Uninitialized is invalid at that point, and 13.9.1(10) says
 a value in Range_Type'Base but not in Range_Type is not supposed to be
 equal to 1 or 2.  (Of course, Uninitialized'Valid might be True, in which
 case the call to Foo won't happen.)"

Eric B.
"Can the behaviour of the program, assumed valid, really depend on the value 
of B, even though we are *sure* that it is computed from a value that is not 
valid?  Clearly that would be very problematic because that would mean you 
cannot "contain" data invalidity, i.e. it can percolate throughout the whole 

Bob D.
"I'm not sure what you mean by percolate, here.  If the call to Foo didn't
raise an exception, then B has the valid value False."

Eric B.
"Every single procedure must be prepared to receive and handle invalid values, 
even though it doesn't contain any sources of them.  In other words, it 
essentially cannot trust its own specification."

Robert Dewar
"That's right. For instance if you have:

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

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

Ada 95 *requires* that you do a subscript check here, a wild
store is improper, and that subscript check must NOT be eliminated.

So that's absolutely right, the spec says

   If M is valid it is in the range 1 .. 10

but it does NOT say that M is valid, and the procedure
MUST behave correctly (no erroneous behavior allowed)
if M is invalid."

Bob D.
"That's our choice.  We choose to allow the invalid value to percolate into
Foo as a parameter; therefore we cannot assume that the parameter is valid
when inside Foo.
The reason I like the "check early" model is that it makes such proofs
easier -- e.g. we can then prove that formal parameters are always valid.
But that's not what GNAT does."

Robert D.
"And it would require quite inefficient code to do this with any
reasonable level of effort, since real value tracking is not available
to us for this purpose."

Bob D.
"Again, this is true in GNAT, because we CHOOSE not to do a range check when
passing uninit vars to procedure R.  If we did such a check, then we could
eliminate the subscript check on Q(M) inside R."

Eric Botcazou

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]