Geert Bosch wrote:
As undefined execution can result in arbitrary badness,
this is really at odds with the increasing need for many
programs to be secure. Since it is almost impossible to
prove that programs do not have signed integer overflow,
That seems a bit pessimistic, given the work Praxis
has done in the area of proving SPARK programs exception
free. Potentially these same techniques could work with
programs written in a suitable subset of C (and for
highly secure programs, you would want to use such a
subset in any case).
Still, in practical terms, it is true that overflow
being undefined is unpleasant. In Ada terms, it would
have seemed better in the C standard to reign in the
effect of overflow, for instance, merely saying that
the result is an implementation defined value of the
type, or the program is terminated. Any other outcome
seems unreasonable, and in practice unlikely.
The important thing is to stop the optimizer from
reasoning arbitrary deeply from lack of overflow.
For example if we have
if (Password == Expected_Password)
delete_system_disk;
else
xxx
and the optimizer figures out that xxx will unconditionally
cause signed integer overflow (presumably due to some bug),
we don't want the optimizer saying
"hmm, if that check is false, the result is undefined, so
I can do anything I like, for anything I will choose to
call delete_system_disk, so I can legitimately remove
the check on the password being correct."
This kind of back propagation, while strictly allowed
by the standard, seems totally unaccpetable to me. The
trouble is (we have been through this in some detail in
the Ada standardization world), it is hard to define
exactly and formally what you mean by "this kind of
back propagation".
