John Regehrfun superoptimizer result from @hyperoptimizer, this occurs in ImageMagick
@hyperoptimizer here's what an LLM thought about how to generalize this transformation 🤖 🤖 🤖
void friend@regehr using > to denote “is more work than”,
reading this > doing the reasoning yourself > reading Steve's toot
@void_friend well, I read it and it seems broadly correct. I'm interested because I work on generalizing program rewrites and I'm suspecting that the synthesis part of that work is now wholly obsolete.
I Can't Believe It's Not Zero!@regehr @void_friend it's pretty good!
Can Lehmann@regehr @hyperoptimizer Is this intentional or did someone just choose epsilon too small/mistankenly forgot a type cast?
@CanLehmann @hyperoptimizer I don't know how to tell that, but I'll ask Zhengyang for a file:line so we can look (he's not here often)
@regehr @CanLehmann @hyperoptimizer likely it originates from some sort of type-generic code of some sort.
@steve @regehr @hyperoptimizer That would make sense, otherwise I would be surprised why it would be written like this.
Chandler CarruthDon't forget the glorious way of doing this thanks to C/C++: using scientific notation!
... hold up. This is checking |a - b| < 0.0, which is always false. Is there a typo or a bug in the checker, or did I misread something?
@steve @hyperoptimizer I don't think typo-- I'm cutting and pasting.
but we've seen Alive2 and Z3 bugs wrt FP....
@regehr @hyperoptimizer typo (or tool using the wrong formatter). From your godbolt link, the actual compare is `fcmp olt double %ext, 1.000000e-15`. So it's correct.
(i16 is always exactly representable as float, and so is their difference. Absolute value and extension to double are also exact, so no rounding error occurs. Therefore (double)abs((float)a - (float)b) < 1.0e-15 is equivalent to a - b < 1.0e-15 in exact arithmetic, and since a and b are integers that's a == b.)
Alexander Monakov@regehr @steve @hyperoptimizer but the godbolt link has
%cmp = fcmp olt double %ext, 1.000000e-15
which is reasonable, so 0.0000 shown in the screenshot is the result of printing with %f?
@amonakov @steve @hyperoptimizer ah.... the screenshot is Alive2's output, which may not be sufficiently careful about floats.
indeed the godbolt link is the correct code
@regehr with C-style formatters, IIRC, either of %.16e or %.17g will print differently two doubles that are different, whereas obviously %f does not.
(assuming a modicum of quality of the libc doing the printing)
@void_friend yeah I'll patch Alive2 for this thanks
@void_friend @regehr these days I would try to use zmij (https://github.com/vitaut/zmij/) or similar for a self-contained portable very fast option that prints exactly as many digits as necessary to differentiate doubles, and not depend on libc.
@steve @void_friend not sure I can get Nuno to buy into a new dependency, hoping I can do this with just LLVM's APFloat utils
@regehr @void_friend APFloat should probably have a toShortestString with no parameters, then you wouldn't need it (obviously, this is a larger project, though).
But note that zmij and swiftDtoa and a few of the others are basically zero-dependency single-file implementations, so you can just copy them and not introduce any new dependencies for your project.
@steve @void_friend nice thanks, I've not used any of those yet
@regehr If you are willing to accept base-2 exponents being printed instead of base-10 (the significand can be in base 10, e.g. 1.57p2 for π), you can make a function sufficient for regression tests with a call to frexp, a multiplication and a conversion to uint64_t. Always prints differently doubles that are different and the n-1 first digits are even correct!
If you want base-10 exponents, it's better to add a dependency than to try to reinvent it. Either you'll have to reinvent multiprecision integers or to reinvent extremely sophisticated shortcuts invented along the decades by extremely bright people. It is really difficult and the algorithms known today have refined the job of doing this conversion efficiently to a tour de force.
@void_friend it looks like LLVM's APFloat library has everything I might want here, except not printing the shortest lossless string. but I don't know that we care specifically about that.
Joe Groff (1M Context)