[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.
Herald added a subscriber: rnkovacs.

In https://reviews.llvm.org/D35109#943558, @baloghadamsoftware wrote:

> In https://reviews.llvm.org/D35109#937763, @NoQ wrote:
>
> > For the type extension approach, somebody simply needs to do the math and prove that it works soundly in all cases. Devin has been heroically coming up with counter-examples so far, but even if he doesn't find any, it doesn't mean that it works, so ideally we shouldn't make him do this. The thing about the MAX/4 approach is that the math is fairly obvious: it is clear that overflows or truncations never occur under these constraints, therefore school algebra rules apply. If the type extension approach is proven to be sound, and covers more cases than the MAX/4 approach, i'd gladly welcome it.
>
>
> I am sure that it covers more cases. My proposal is the following:
>
> 1. I will try to do the math. However, that is not enough, because some checkers (and checker utility functions exported into the core) are dependent on the overflow. So


I'm totally fine with assuming the MAX/4 constraint on checker side - extension math would still be better than the MAX/4 pattern-matching in core because extension math should be more useful on its own. Otherwise, i'm also fine with MAX/4 `>`/`<` under an off-by-default flag, if this is indeed blocking future reviews. I'm just really uncomfortable with huge manual checker-side symbolic computations, essentially declaring that checkers should make their own solvers. Analyzer progress is already slowed down dramatically by technical debt in a lot of places - we rarely have time to address it, but at least we shouldn't introduce much more. This doesn't, in my opinion, reduce the fascination of that whole thing you've constructed. It is wonderful.

> 3. I suggest to continue the review

I just tried to unblock your progress on the other iterator checker reviews a little bit. I should have done this earlier. My overall impression is that they would be going much easier than the first ones, because they are split in really small neat chunks.


https://reviews.llvm.org/D35109