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

[Chris Hathhorn <hathhorn@gmail.com>]

Hi,

I'm the one who (very) recently added this negative zero check to kcc,
mostly in the interest of making it as pedantic as possible. I'll
confess that I'm not terribly confident in my interpretation of the
standard, but let me attempt to defend myself a bit.

> -------- Original Message --------
> From:   Pascal Cuoq <pascal.cuoq@gmail.com>
> To:     John Regehr <regehr@cs.utah.edu>
>
> I do think that 6.2.6.2:4  could be better phrased
> with respect with 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]”.

FWIW, the wording in the error is something like "potential negative zero."

>
> 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
>  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
>  is without effects.

I thought what immediately follows that in 6.2.6.2:2 seemed like the
most relevant part: "Which of these applies is implementation-defined,
as is whether the value with sign bit 1 and all value bits zero (for
the first two), or with sign bit and all value bits 1 (for ones'
complement), is a trap representation or a normal value."

This seems to be pretty explicit about the potential for "sign bit 1
and all value bits zero" to be a trap representation on two's
complement implementations (but I guess it's never actually a negative
zero, as you point out). What am I missing?

> From: John Regehr <regehr@cs.utah.edu>
> Date: Fri, Jun 27, 2014 at 12:04 PM
> To: csmith-bugs@flux.utah.edu
> There is roughly one of these in existence as far as I know and I doubt that
> its authors are interested in fuzzing it.
>
> John

But yeah, I'm definitely sympathetic with this, and kcc currently does
attempt to flag other negative zeros as well (I justify this because,
it seems to me, e.g., ~0 will be the same bit pattern on any
implementation, and on ones' complement it's a potential negative
zero). Sorry for any false positives, though, I didn't realize people
were actually using recent versions of the tool. I'll try to work on
usability in the near future.

Chris