kmeakin (Apr 06 2023 at 22:48): kmeakin (Apr 06 2023 at 22:48):Does cranelift have a concept of UB/poison like LLVM does?
Chris Fallin (Apr 06 2023 at 22:49):Nope, we've actually pretty explicitly chosen not to have UB
kmeakin (Apr 06 2023 at 22:50):I understand wasm requires things like division by zero to trap. But splitting the check for zero divisor and division into separate instructions in the IR could expose more optimisation opportunites. Would just have to modify the fronted to generate code that checks for UB and traps
Chris Fallin (Apr 06 2023 at 22:50):small asterisk around memory accesses -- if you access an invalid pointer, all bets are off
Chris Fallin (Apr 06 2023 at 22:50):There are a whole host of benefits we get by not having UB, and I've tried to hold the line on this as much as possible: verification is simpler and subtle correctness bugs from unexpected optimization assumptions just can't happen
Chris Fallin (Apr 06 2023 at 22:51):It's true that in some cases it will limit opportunities, but our goal is explicitly not to be LLVM
Chris Fallin (Apr 06 2023 at 22:52):(for a somewhat related discussion, see recent comments about pointer provenance on GitHub -- I argued to treat a pointer as an integer, and define an access to a pointer as valid as long as the integer value is valid, irrespective of its provenance; because the alternative, where certain kinds of derivations are UB, just causes so many broken assumptions that it's impossible to be really sure about optimization correctness)
Chris Fallin (Apr 06 2023 at 22:53):Fuzzing and other similar testing is another example of the benefits we get from UB: by giving one particular meaning to any given CLIF, we can test via equality of outputs, rather than some sort of refinement or one-possible-valid-behavior predicate
Chris Fallin (Apr 06 2023 at 22:54):every once in a while this comes up when someone sees an optimization opportunity; maybe I should write an RFC if it would help align everyone :-)
kmeakin (Apr 06 2023 at 22:55):Thank you. Would be interesting to see how far we can push perf without compromising on UB
kmeakin (Apr 06 2023 at 22:56):IIRC there was a paper where they disabled UB in LLVM and there was only a few % slowdown in most benchmarks
Chris Fallin (Apr 06 2023 at 22:56):I do suspect that there are ways to design abstractions that expose some of the optimization opportunities without UB, though. One way to see UB is under-capture of invariants in the IR's type system. So for example a "non-zero integer type" as the output of a "trap if divisor is 0" operator could then be fed into a non-trapping div
Chris Fallin (Apr 06 2023 at 22:56):ah, that's interesting, I haven't seen concrete numbers; that's not bad at all
kmeakin (Apr 06 2023 at 22:57):Chris Fallin said:
I do suspect that there are ways to design abstractions that expose some of the optimization opportunities without UB, though. One way to see UB is under-capture of invariants in the IR's type system. So for example a "non-zero integer type" as the output of a "trap if divisor is 0" operator could then be fed into a non-trapping div
Something like a refinement type system?
Chris Fallin (Apr 06 2023 at 22:59):Yeah, in the most general sense :-) I don't know if I would want something like fully general refinement predicates in CLIF
Chris Fallin (Apr 06 2023 at 23:00):though maybe actually at least integer-range refinements would make sense
Notification Bot (Apr 12 2023 at 19:07):kmeakin has marked this topic as resolved.
scottmcm (Apr 18 2023 at 18:49):kmeakin said:
IIRC there was a paper where they disabled UB in LLVM and there was only a few % slowdown in most benchmarks
Do you have a link, perchance? I'd be very interested to see how they did that.
Last updated: Nov 22 2024 at 16:03 UTC