[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement

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

baloghadamsoftware added a comment.

Let us summarize the possibilities:

1. Type extension approach. I tested it, all tests pass, and also in Devin's examples we do not infer narrower range than we should. (Wider do not matter.) I think this is the most complete solution and many checkers could benefit of it. There are also two possibilities here:

  a) If the symbols on both sides are equal, we do not extend the type, because of `assumeInbound()` in `ProgramState`, which first adds `MIN` to both the bound and the index. So e.g. `S-1<S` becomes `S+MIN-1<S+MIN`. However, `S+MIN-1==S+MAX`, so if we extend the type here, we get `0<MIN-MAX`, which is `0<2*MIN+1` which is `false`. So we leave the type so `0<MIN-MAX` becomes `0<1` which is `true`.

  b) We extend the type even in case the symbols on both sides are equal, but we fix `assumeInbound()` in `ProgramState` to add `(MAX+MIN)/2` instead of `MIN`. (Why is this normalization necessary?)

2. [MIN/4..MAX/4] approach. We loose the (probably rare) cases using large numbers, but for most checkers it is probably no problem.

3. We drop this patch, and do the workaround in the iterator checker. Although it adds some complexity and other checkers cannot benefit from the rearrangement, it solves the problem of the iterator checkers at the moment.

The rearrangement only for `==` and `!=` is not enough for the iterator checkers. Maybe it is enough for checking iterator range, but it does not remove the complexity from it. To check the cases were we are completely outside of the valid range we still have to manually separate symbol and concrete integer and also do the comparison manually. To invalidate iterators after operations on the container it does not help anything, there we have to deal with `<`, `<=`, `>` and `>=` as well.


https://reviews.llvm.org/D35109