[PATCH] D32642: [Analyzer] Iterator Checker - Part 2: Increment, decrement operators and ahead-of-begin checks

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D32642#787913, @baloghadamsoftware wrote:

> I tried `SValBuilder::evalBinOp()` first but it did not help too much. It could decide only if I compared the same conjured symbols or different ones, but nothing more. It always gave me `UnknownVal`. Even if comparing ${conj_X} == ${conj_X} + n where n was a concrete integer. So I have to compare the symbol part and the concrete integer part separately.


In any case, it's not right to have two `SValBuilder`s. Your code simplifies symbolic expressions of numeric types, `SValBuilder` does the same thing, there's no need to duplicate. It would be much better to move the functionality you need (and already have implemented) directly to `SValBuilder`.

I'm sure that simplification `(($x + N) + M) ~> ($x + (M + N))` is already working in `SValBuilder`. I think it's totally worth it to add `(($x + M) == ($x + N)) ~> (M == N)` and `(($x + M) - ($x + N)) ~> M - N` into `SValBuilder` in case it's not already there, because the whole analyzer would immediately benefit from that, not just your checker.

Generally, i totally encourage you to modify the analyzer's core to fit your purposes, even if to reduce code duplication. It's not worth it to teach the core constraint manager how to work with user-defined types such as iterators, but it's definitely worth it to teach `SValBuilder` how to handle numeric-type symbols better.

In https://reviews.llvm.org/D32642#787913, @baloghadamsoftware wrote:

> If Z3 constraint solver is accepted and will be the default constraint manager, then I can somewhat simplify my code. That patch is under review for long and I am not sure whether it will be the default ever.


I don't expect Z3 to be on by default soon, however i'm only pointing to the changes in the mainline `SValBuilder` in that patch. Z3 doesn't replace `SValBuilder`, it only replaces the constraint manager. However, `SValBuilder` needs to provide accurate `SVal`s to Z3, which means that a lot of `UnknownVal`s need to go away. We're discussing if they should go away completely even if Z3 isn't on.

In https://reviews.llvm.org/D32642#787913, @baloghadamsoftware wrote:

> Waiting is not an option for us since we are a bit delayed with this checker. I have to bring them out of alpha until the end of the year.


While moving things out of alpha is pretty much the primary goal of any work we do, sacrificing quality defeats that purpose. We can only afford to enable things by default when we know they're ready. This checker is research-heavy and as such hard to plan. We need to understand the decisions and trade-offs that you made.


https://reviews.llvm.org/D32642