This is the mail archive of the
mailing list for the GCC project.
Re: changing "configure" to default to "gcc -g -O2 -fwrapv ..."
- From: Robert Dewar <dewar at adacore dot com>
- To: Geert Bosch <bosch at adacore dot com>
- Cc: Daniel Berlin <dberlin at dberlin dot org>, Richard Guenther <richard dot guenther at gmail dot com>, Paul Eggert <eggert at cs dot ucla dot edu>, autoconf-patches at gnu dot org, bug-gnulib at gnu dot org, gcc at gcc dot gnu dot org
- Date: Mon, 01 Jan 2007 12:25:23 -0500
- Subject: Re: changing "configure" to default to "gcc -g -O2 -fwrapv ..."
- References: <200612300047.kBU0lFwk014817@localhost.localdomain> <firstname.lastname@example.org> <10612302258.AA24598@vlsi1.ultra.nyu.edu> <email@example.com> <firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org> <22C62FE7-259E-43F7-9DB5-5F3A9CF574E2@adacore.com>
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)
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