double rounding in x86

[Vaughan Pratt]

	When those values are stored to memory, if the destination
	format is double precision, those values *cannot* be stored
	bit-for-bit - they must be converted from extended precision to
	double precision.  It cannot be otherwise.

Does the standard itself say it cannot be otherwise?  If so then gcc
violates the standard in the following code:

		double w, x, y, z;
		...
		x = y + z;
		...(no further assignment to x)
		w = x - y;

One cannot deduce that the last line uses x rounded to double, since if
y + z is still in a register (and hence at extended precision) when the
last line is reached, gcc for the x86 is happy to treat x as synonymous
with y+z (very naughty), which makes w exactly 0 in this case.  Whether
y+z *is* still in a register can depend (at compile time) on code
*following* the last line, with the result that whether w is zero can
vary as you vary the following code (but not the values in y and z)!

This sort of compiler nondeterminism is very nasty quite apart from
questions of IEEE compliance.  Debugging under these conditions makes
one realize how dependent debugging is on the usual programmer's
understanding of the laws of causality in a program---one tears one's
hair out trying to figure out what is going on.

Vaughan Pratt