-
Notifications
You must be signed in to change notification settings - Fork 302
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[CombToArith] Fix coarsening of division by zero UB #6945
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! This will probably do for most practical cases. But I am unsure if we may not still be in trouble if we try to do 0 / 0
. Going by the specification of the arith dialect, any division by zero is (immediate) UB. Alive2 also confirms this if we compare a clang compilation of the b == 0 ? 0 : a/b
reference against a slightly massaged output of the integration test:
Transformation doesn't verify!
ERROR: Source is more defined than target
Example:
i8 %#0 = #x00 (0)
i8 %#1 = #x00 (0)
Source:
i1 %#5 = #x1 (1)
>> Jump to %#4
i8 %#7 = #x00 (0)
Target:
i1 %#3 = #x1 (1)
i8 %#4 = #x00 (0)
i8 %#5 = UB triggered!
For practical purposes, I tested it on both x86_64 and ARM64 and the test produced 0 even for zero divded by zero. This is not so surprising for ARM64. I would have expected a trap on x86_64 though, see #6726 . This could be a subtlety of the JIT engine and the way it handles UB. But maybe I've just messed something up, which wouldn't be surprising either. 😖
On a more general note, I do think we need to tinker with the HW/Comb specification to get a clean separation between undefined behavior, undefined values (undef, poison, frozen poison, X, you name it...) and the conditions which must/may/mustn't terminate a simulation.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
adbdb21
to
f443494
Compare
@fzi-hielscher Thanks for the detailed review! I've changed it to divide by 1 if the divisor is 0 originally. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice, thank you.
Fixes #6938