Gem #133 : Erroneous Execution - Part 2

by Bob Duff —AdaCore

Let's get started...

The moral of the story was: Do not write erroneous programs.

Strictly speaking, that's wrong usage. "Erroneous" refers to a particular execution of a program, not to the program itself. It's possible to write a program that has erroneous behavior for some input data, but not for some other input data. Nonetheless, it's reasonable to use "erroneous program" to refer to a program that might have erroneous behavior. Just remember that "erroneous" is not a property of the program text, but a property of the program text plus its input, and even its timing.

Never deliberately write code that can cause erroneous execution. For example, I've seen people suppress Overflow_Checks, because they "know" the hardware does wrap-around (modular) arithmetic, and that's what they want. That's wrong reasoning. The RM doesn't say that overflow, when suppressed, will do what the hardware does. The RM says anything at all can happen.

If you suppress Overflow_Checks, you are telling the compiler to assume to assume that overflow will not happen. If overflow can happen, you are telling the compiler to assume a falsehood. In any mathematical system, if you assume "false", anything at all can be proven true, causing the whole house of cards to tumble. Optimizers can and do prove all sorts of amazing things when told to assume "false".

Never try to guess that the optimizer isn't smart enough to cause trouble. Optimizers are so complicated that even their authors can't accurately predict what they will do. For example:

X : Natural := ...;
Y : Integer := X + 1;

if Y > 0 then
    Put_Line (Y'Img);
end if;

The above will print some positive number, unless X is Integer'Last, in which case Constraint_Error will be raised. The optimizer is therefore allowed to deduce that when we get to the 'if', Y must be positive, so it can remove the 'if', transforming it to:

X : Natural := ...;
Y : Integer := X + 1;

Put_Line (Y'Img);

That's good: removing the 'if' probably makes it run faster, which is the optimizer's goal. But if checks are suppressed, the optimizer can still do the above transformation. The reasoning is now: "when we get to the 'if', either Y must be positive, or we must be erroneous". If the former, the 'if' can be removed because it's True. If the latter, anything can happen (it's erroneous!), so the 'if' can be removed in that case, too. "X + 1" might produce -2**31 (or it might not).

We end up with a program that says:

if Y > 0 then
    Put_Line (Y'Img);
end if;

and prints a negative number, which is a surprise.

Another possible behavior of the above code (with checks suppressed) is to raise Constraint_Error. "Hey, I asked for the checks to be suppressed. Why didn't the compiler suppress them?" Well, if the execution is erroneous, anything can happen, and raising an exception is one possible "anything". The purpose of suppressing checks is to make the program faster. Do not use pragma Suppress to suppress checks (in the sense of relying on not getting the exception). Compilers do not remove suppressed checks if they are free -- for example, imagine a machine that automatically traps on overflow.

Perhaps pragma Suppress should have been called something like Assume_Checks_Will_Not_Fail, since it doesn't (necessarily) suppress the checks.

To be continued in part 3