[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: csmith-bugs@flux.utah.edu*Subject*: Re: [csmith-bugs] Undefined behavior in safe_math: Bitwise operation produces negative zero*From*: Chris Hathhorn <hathhorn@gmail.com>*Date*: Fri, 27 Jun 2014 21:53:03 -0500*Cc*: Grigore Rosu <grosu@illinois.edu>, sebastian.buchwald@kit.edu, Chucky Ellison <cme@freefour.com>, pascal.cuoq@gmail.com*Dkim-signature*: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=D4VywQV+DJ0Ov27VXE0MnZI3fj8qj/DF7J269yEoeFs=; b=CQ1DTIVcLAHq9EDTQMpQSEaz8536poR5YFVvk0GtokRTjrLYet/ngfuMJtnkL2U5au dApKNS2m75Skz1Qlm9S+ovwDFV5S5jqJ+NP46lTQ0ZalzBuu3IrLGWJORxGtEKfGGFKC yxhYq5AI6ghfU16ViKJ/T+UWuSARsOKJ99GBTDlm3ylUNauS0kmcW19FUPNcEqvM7JwT yCYm6VkFu0i6PtuhZtrqJSVkb0I4/ANIxRYlAbIhoGK4VVsn0MqOOgFtdWFqgr9VODPx X7RDIpsTwzmQHEIJyJz/3b1H85H9zOs0hPJ+munsgq4YqSfCdDMvLyD9L9+6jYNv7uw8 0e1g==*In-reply-to*: <CAKDQXVLJN5MzWGgNzMLU5S0Eq58R01+obANuyXutDg34UePG-w@mail.gmail.com>*List-archive*: </listarchives/csmith-bugs>*List-help*: <mailto:csmith-bugs-request@flux.utah.edu?subject=help>*List-id*: Csmith Bugs Mailing List <csmith-bugs.flux.utah.edu>*List-post*: <mailto:csmith-bugs@flux.utah.edu>*List-subscribe*: <http://www.flux.utah.edu/mailman/listinfo/csmith-bugs>, <mailto:csmith-bugs-request@flux.utah.edu?subject=subscribe>*List-unsubscribe*: <http://www.flux.utah.edu/mailman/options/csmith-bugs>, <mailto:csmith-bugs-request@flux.utah.edu?subject=unsubscribe>*References*: <53AD6A05.1050902@ira.uka.de> <53AD9612.6030606@cs.utah.edu> <CAKDQXVLJN5MzWGgNzMLU5S0Eq58R01+obANuyXutDg34UePG-w@mail.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

**Follow-Ups**:**Re: [csmith-bugs] Undefined behavior in safe_math: Bitwise operation produces negative zero***From:*John Regehr <regehr@cs.utah.edu>

**References**:**[csmith-bugs] Undefined behavior in safe_math: Bitwise operation produces negative zero***From:*Andreas Fried <s_fried@ira.uka.de>

**Re: [csmith-bugs] Undefined behavior in safe_math: Bitwise operation produces negative zero***From:*John Regehr <regehr@cs.utah.edu>

- Prev by Date:
**[csmith-bugs] Fwd: Re: negative zero and two's complement** - Next by Date:
**Re: [csmith-bugs] Undefined behavior in safe_math: Bitwise operation produces negative zero** - Previous by thread:
**Re: [csmith-bugs] Undefined behavior in safe_math: Bitwise operation produces negative zero** - Next by thread:
**Re: [csmith-bugs] Undefined behavior in safe_math: Bitwise operation produces negative zero** - Index(es):