[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement

[Balogh, Ádám via Phabricator via cfe-commits]

baloghadamsoftware added a comment.

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

2. I will also try the modification on some real-world code with most of the checkers enabled and compare the results. This takes lot of time, so until then

3. I suggest to continue the review on the iterator checker patches where I put back the workaround, but I separate them from the rest of the code and mark them with a FIXME referring to this patch. Furthermore,

4. I remove the dependency from the "Constraint Manager Negates Difference" patch (https://reviews.llvm.org/D35110), so the workaround in the checker can be somewhat simplified if that one is accepted. It is not a real dependency, the negation can be used also in the case we create the symbol difference manually.

What is your opinion about this approach?


https://reviews.llvm.org/D35109