[Prev][Next][Index][Thread]
Re: Formal semantics for C
On 29-Dec-2001, Corky Cartwright <cork@rice.edu> wrote:
>
> The "unsafe-operations-yield-undefined semantics" for C is
> deterministic; it collapses all unsafe computations into the "bottom"
> element of the semantic domain (cpo) of program values.
Any deterministic semantics for C does not correctly reflect the C standard.
C has several different kinds of "unsafe" operations. You can handle
operations which have "undefined behaviour" in the manner you describe
above, but that doesn't work for operations which have "unspecified
behaviour"; you need nondeterminism in the semantics to handle those.
> If you use a non-determinstic semantics where unsafe operations yield
> the set of all possible states, then you cannot use such a semantics
> justify any interesting static program analysis. [...]
> Such a semantics is "honest" in modeling the
> catastrophic consequences of unsafe operations, but I don't how it
> can be used to produce any positive results from the perspective
> of program analysis.
It's true that such a semantics is not directly useful for the purpose
of program optimization, but it's not completely uninteresting -- you can
use such a semantics to analyse when programs have undefined behaviour.
Analyses used for program optimization will assume that the program
does not have undefined behaviour, and so will use a simpler semantics.
But the non-deterministic semantics where unsafe operations yield the
set of all possible states is still useful, in a fairly trivial sense,
for justifying the optimizations applied as a result of analyses using the
simpler semantics.
--
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.
References: