Gem #134 : Erroneous Execution - Part 3

by Bob Duff —AdaCore

Let's get started...

We showed how this:

X : Natural := ...;
Y : Integer := X + 1;
<b>if</b> Y > 0 <b>then</b>
    Put_Line (Y'Img);
<b>end</b> <b>if</b>;

can end up printing a negative number if checks are suppressed.

In fact, a good compiler will warn that "Y > 0" is necessarily True, so the code is silly, and you can fix it. But you can't count on that. Optimizers are capable of much more subtle reasoning, which might not produce a warning. For example, suppose we have a procedure:

<b>procedure</b> Print_If_Positive (Y : Integer) <b>is</b>
<b>begin</b>
    <b>if</b> Y > 0 <b>then</b>
        Put_Line (Y'Img);
    <b>end</b> <b>if</b>;
<b>end</b> Print_If_Positive;

It seems "obvious" that Print_If_Positive will never print a negative number. But in the presence of erroneousness, that reasoning doesn't work:

X : Natural := ...;
Y : Integer := X + 1;
Print_If_Positive (Y);

The optimizer might decide to inline the call, and then optimize as in the previous example.

Other language features that can cause erroneous execution include:

Shared variables (erroneous if multiple tasks fail to synchronize)
Address clauses
Unchecked_Conversion
Interface to other languages
Machine-code insertions
User-defined storage pools
Unchecked_Deallocation

A complete list can be found by looking up "erroneous" in the RM index, or by searching the RM. Every case of erroneous execution is documented under the heading "Erroneous Execution".

You should try to minimize the use of such features. When you need to use them, try to encapsulate them so you can reason about them locally. And be careful.

As for suppressing checks: Don't suppress unless you need the added efficiency and you have confidence that the checks won't fail. If you do suppress checks, run regression tests on a regular basis in both modes (suppressed and not suppressed).

The final part of this Gem series will explain the rationale behind the concept of erroneous execution in Ada.