Re: Bug in AdaEd???

[agate!spool.mu.edu!olivea!news.bu.edu!inmet!spock!stt@ucbvax.Berkeley.EDU (Tucker Taft)]

In article <EACHUS.93Sep22160725@spectre.mitre.org> 
  eachus@spectre.mitre.org (Robert I. Eachus) writes:

>In article <1993Sep22.093656.20606@sei.cmu.edu> 
>  firth@sei.cmu.edu (Robert Firth) writes:
>
>   > Indeed a nasty example!  However, isn't the solution fairly simple:
>   > eliminate the variable Junk and rewrite the test as
>
>   > 	   if X*Y > 10_000 then ...
>
>   > As far as I can see, that has to work regardless of whether X*Y
>   > overflows.  Moreover, isn't it the obvious way to write the code?
>
>   That was where we started...I guess I should have used a larger
>number in the example.  Substitute 1_000_000 for 10_000 and compile
>your code on a 16-bit machine.  Do you see the problem?  The compiler
>is allowed to assume the expression is false in all cases without
>doing the check, and thus without raising NUMERIC_ERROR or
>CONSTRAINT_ERROR on the expression evaluation.  
> . . .

This thread is of course very timely as we work to finalize the definition
of Ada 9X, and in particular clause 11.6.

I suspect that this statement:

  "The compiler is allowed to assume the expression is false ..."

reflects the heart of the problem with RM83-11.6(7) (or with the typical 
interpretation of it).

The point of 11.6(7) was *not* to allow junk or wrong 
results to be produced, but rather to allow dead variables to
be removed, even if their computation might raise an exception.
Nowhere does 11.6 say a compiler may presume an expression is True that
in fact is not True.  If one interprets 11.6(7) to imply that, then
clearly something is wrong in 11.6(7) or its interpretation.

I think the way to resolve this problem is for the compiler to
treat an expression that fails a predefined check as having an
"undefined" value (equivalent to "bottom" in some languages).

This idea is explored further below.  You might as well stop
reading here if the rest is boring or obvious to you...

All types must be extended with an extra "undefined" value, including
Boolean (in the case of Boolean, "undefined" corresponds to the "Unknown"
of three-valued logic).  Hence, the expression "X*Y > My_Int'Base'Last" 
may *not* be replaced with simply "False."  There are two possible values 
of the expression, "False" or "Undefined/Unknown."  

One needs to define the composition rules for the various predefined
operations when one or more of the operands are undefined/unknown.
For Boolean, Undefined combines as follows:

    Undefined and True => Undefined
    Undefined and False => False
    Undefined or True => True
    Undefined or False => Undefined
    not Undefined => Undefined
    Undefined xor X => Undefined

For most other operations, if any operand is undefined, the
result is undefined.  One notable exception is:

    Undefined * 0 => 0

Hence, the only way to "consume" an undefined value in an expression
and not produce an undefined result are to "and" with False, "or" with True, 
or multiply by 0 (there might be some others -- those are the ones
that come to mind right now).  In any case, Undefined > Integer'Last, 
is Undefined, not False.

Another important way to "consume" an undefined result is with
an exception handler.  Hence:

    ... Undefined ...;
 exception
    when others =>
       S;

can be transformed to:

       S;

Now of course if the exception handler is more specific about the
exception it handles, then the transformation is a bit more involved,
but you get the idea (I hope).

Rules must also be developed for how "undefined" propagates out
of expressions into statements and sequences of statements.
The naive rule would be:

    Undefined; S; ==> Undefined;

That is, if a statement is Undefined, then so is a sequence of
statements starting with that statement.   However, it has generally
been agreed (in the ARG and for Ada 9X) that the sequence  
should not be interpreted strictly, but rather the partial ordering
implied by data dependences should control the legitimate reorderings.

Hence, a legal transformation of:

    X := Undefined; <sequence without ref to X>; Y := ... X ...;

is:

    <sequence without ref to X>; Y := ... Undefined ...;

and a legal transformation of:

    X := Undefined; <rest of program with no further uses of X>;

is:

    <rest of program with no further uses of X>;

In other words, the calculation of an undefined value can be moved
around (or eliminated) just like the calculation of a defined value.

The critical thing is that an undefined value must not be allowed
to make it into the external output of the program, either directly
or by controlling the result printed.  Before this happens,
an exception must be raised.

"If" statements are not the same as assignments, but can be treated that
way by making the following transformation:

   if Cond then
       S1;
   else
       S2;
   end if;

goes to:

   Path := Cond;
   S1(Path);
   S2(not Path);

With this transformation, it should become clear that
if Cond evaluates to "Undefined," then neither S1 nor S2 may be
allowed to execute normally.  The only thing which would allow the elimination
of the evaluation of Cond would be if both S1 and S2 were empty (possibly
due to elimination of dead code by the optimizer).

Since in all of the examples mentioned earlier in this thread,
S1 was not empty, we clearly have to evaluate Cond to determine
whether it evaluates to False or to Undefined, and if it evaluates
to Undefined, we can only "consume" the Undefined by executing the
appropriate exception handler.

So... The bottom line, is that with this proposed approach
to 11.6(7), the compiler may *not* assume an expression is False 
just because it would either be False or raise an exception.
It must go ahead and determine whether or not the expression
raises an exception (i.e. evaluates to "Undefined"), unless there
is no output dependent on the result (in these examples, there
clearly was output dependent on the result).
       
>					Robert I. Eachus

S. Tucker Taft
Ada 9X Mapping/Revision Team
Intermetrics, Inc.
Cambridge, MA  02138