Inconsistent phi value after select based on undef value

[FlashSheridan]

Inconsistent phi value after select based on undef value

[nunoplopes]

The issue may be in the Alive2 UI for values, especially those not marked “[based on undef value],” but %obit and %spec.select are each used only once (and the value for %spec.select (#x1) is not marked as based on undef value). If the display of %spec.select = #x1 is not relevant to Alive2’s assumption for the value’s sole use in the chosen counterexample, I’m misunderstanding the UI.

I understand the frustration. The issue is that it's quite expensive to mark things as based-on-undef. We use a cheap technique, but it cannot detect all cases. It's annoying, but I don't think we want to spend several minutes to print a counterexample.
Our hope was that we would remove undef from LLVM altogether. That's the main reason why I haven't invested much in making undef perfect in Alive2.

I hate to say this, but in the end this project is maintained by poorly paid academics, while the users are handsomely paid compiler developers. Moreover, companies are not willing to sponsor Alive2. While I try to fix most bugs that come our way, I prioritize the things that are useful for the majority of the users and for my own research. My priority is to remove undef from LLVM.

[regehr]

well... if Alive is happy with the transformation under the --disable-undef-input then maybe just call it good? there are certainly a number of things in the tree already that don't work when inputs are undef

also, this is a pretty big example to think about and I can't llvm-reduce it since you're providing both the src and tgt. can you llvm-reduce it under the criterion that Alive reports a value mismatch and post the results here?

[regehr]

I don't know if you are an llvm-reduce user but if not, this is the interestingness test that you want, but obv adjust the path

#!/bin/bash
timeout 1 $HOME/alive2-regehr/build/alive-tv $1 2>&1 | grep 'Value mismatch'

[nunoplopes]

The optimization is not correct for undef inputs. Each time an undef is used it can yield a different value.
Since %obit in tgt is undef, the select can return either of the operands each time it is used. I know the counterexample may look confusing because you get a value for the select and a different for the phi, but that's just how undef works!

[FlashSheridan]

The optimization is not correct for undef inputs.

Thanks for the explanation in the subsequent issue, which may have revealed an important bug in our code; but that’s not the point to this bug:

We’re not confident in what the expected behavior is. Alive2 notes, reasonably, that in both src and tgt, %obit is based on undef value. Thus the value of %spec.select might have been different, but Alive2 proclaimed it to be #x1.

Each time an undef is used it can yield a different value. Since %obit in tgt is undef, the select can return either of the operands each time it is used.

The issue may be in the Alive2 UI for values, especially those not marked “[based on undef value],” but %obit and %spec.select are each used only once (and the value for %spec.select (#x1) is not marked as based on undef value). If the display of %spec.select = #x1 is not relevant to Alive2’s assumption for the value’s sole use in the chosen counterexample, I’m misunderstanding the UI.

[FlashSheridan]

I quite understand your point (Matter Labs is hiring, and my wife is a professor). Alive2 has done a lot of good for the LLVM community and for our compiler, so we’d like to become a sponsor; please send me the details.
    We’ve now fixed our undef bug; I’m not sure where it would fit in your BugList.md. It’s our PR#385, and will become open source when we update our public repo, though the PR number may be transient.

[FlashSheridan]

…I haven't invested much in making undef perfect in Alive2.

That makes sense, and it’s no longer crucial for us, given the freeze fix plus using noundef where needed. I would suggest, for others still depending on undef, tweaking the UI (or perhaps the documentation) to make it clearer what the user can’t rely on when analyzing an unsoundness report involving undef — or perhaps just remove some of the output. (I don’t understand the reports well enough to submit a ReadMe PR.)