[csmith-bugs] Fwd: Re: Undefined behavior in safe_math: Bitwise operation produces negative zero

[John Regehr <regehr@cs.utah.edu>]

See below.

John


-------- Original Message --------
Subject: 	Re: [csmith-bugs] Undefined behavior in safe_math: Bitwise
operation produces negative zero
Date: 	Fri, 27 Jun 2014 16:40:49 +0200
From: 	Pascal Cuoq <pascal.cuoq@gmail.com>
To: 	John Regehr <regehr@cs.utah.edu>



Hello,


On Fri, Jun 27, 2014 at 3:52 PM, John Regehr <regehr@cs.utah.edu
<mailto:regehr@cs.utah.edu>> wrote:

    Hi Pascal, do you agree with this?


No, I don't.

I do think that 6.2.6.2:4 <http://6.2.6.2:4> could be better phrased
with respect with 6.2.6.2:2 <http://6.2.6.2:2>, the latter only defining
“negative zero” when it is “a normal value” (i.e. supported), and the
former referring to “negative zero” being a result when it is “not
support[ed]”.

Clearly, a “negative zero”, whether supported or not, is a bit pattern
with the sign bit set and for which the applicable formula in 6.2.6.2:2
<http://6.2.6.2:2> produces the mathematical zero:

— the corresponding value with sign bit 0 is negated (sign and magnitude);
— the sign bit has the value −(2M ) (two’s complement);
— the sign bit has the value −(2M − 1) (ones’ complement).

For two's complement, no bit pattern has this property, so 6.2.6.2:4
<http://6.2.6.2:4> is without effects. For the other representations,
negative zero can be either supported or not supported, and in the
latter case, bitwise operations that produce the bit pattern that would
correspond to a negative zero are undefined (this is a reasonable
precaution: since in this case arithmetic instructions do not produce
this bit pattern, they may not like to have it as input).

In other words, ~INT_MAX is INT_MIN, not negative zero, and KCC, only
supporting two's complement, is wrong to flag the production of negative
zero in an expression that produces INT_MIN. You don't need to change
your safe integer library unless you plan to support one's complement or
sign-magnitude representations.

Pascal