[Prev][Next][Index][Thread]
Re: Formal semantics for C
On 27-Dec-2001, Corky Cartwright <cork@rice.edu> wrote:
>
> > Compiler optimization researchers perform non-trivial analyses of C
> > programs (e.g., a pointer alias analysis) by ducking the issue of unsafe
> > operations: the simply assume that unsafe operations are never executed.
>
> This is not "ducking the issue". On the contrary, this is an approach
> whose correctness can be proven from the semantics of C, as specified
> in the C standard or more formally in the works referred to earlier.
>
> Nonsense! These optimizations are incorrect (do not preserve the
> meaning of programs) because they presume programs never perform unsafe
> operation, but in fact they do.
No, they do preserve the meanings (denotational semantics) of such programs.
They may not necessarily preserve the *behaviour* of such programs,
but this only happens in cases where the *meaning* of the program is
the infinite set of all possible behaviours; in such cases, any
behaviour is valid, and substituting one behaviour for another
does not change the meaning of the program.
(I'm presuming here that by "unsafe operation", you mean
"operation whose behaviour is undefined according to the C standard".
If you mean something different, you'll need to explain.)
--
Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
Follow-Ups:
References: