Re: [Smtcomp-discussion] FP demo track at SMT-COMP
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Schanda F. <flo...@al...> - 2015-06-11 07:48:42
|
> On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > > Is it too late to ask for a change in the FP standard? Fixing one > return > > value for e.g. (fp.min -0 +0) would make life simpler without losing > > much IMHO, given that the underspecified semantics can still be > encoded > > if someone really wants that. What do people think? > > Fixing one return value while existing IEEE-compliant implementations > return different values would be actively harmful in my opinion. Yes, to add my "industry" voice to this, please keep it as is, that is unspecified. ;) This leaves it up to the tool vendor to specify it, if they happen to know. For example - if I remember right the intel manuals also do not specify what the hardware does. Although, if I remember right, it seems to behave consistently in that it always returns the second (or first?) argument. But fp.min returning -0 and fp.max returning +0 seems an equally likely implementation choice. In fact, I will add some benchmarks to my own testsuite to make sure this behaviour exists. It might all sound a bit silly, but it would be easy enough to construct a program that exploits this behaviour (convert floats to array of bytes) and we would get unsound proofs because of it! Florian |