[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#789004, @baloghadamsoftware wrote:

> Now I can improve `SValBuilder` to compare `{conj_X}+n` to `conj_X}+m`, but I am not sure if it helps to simplify `compare()` much. How to handle cases where I have to compare `{conj_X}+n` to `{conj_Y}+m`, an we have a range `[k..k]` for `{conj_X}-{conj_Y}` in the constraint manager. I still need to decompose the two expressions, retrieve the single length range and adjust one of the sides of the comparison. I think I should not add such complicated code (i.e. retrieving single length range from the constrain manager) to `SValBuilder`.


`SValBuilder` simplifies the symbolic expressions to a certain "canonical" form - collapses `($x op N) op M` to single-op expressions, reorders `N op $x` to `$x op N`, unpacks `!$x` into `$x == 0`, etc.), and `ConstraintManager` makes assumptions over such "canonical" symbolic expressions (but unable to handle non-canonical symbolic expressions).

I propose to canonicalize `($x + N) == ($y + M)` to `($x - $y) == (M - N)` in `SValBuilder`, and then `ConstraintManager` should be able to assume over it, as long as it has a range for `($x - $y)`. `ConstraintManager` would also need an update to support reversing the range when he only has a range for `($y - $x)` but not for `($x - $y)`.


https://reviews.llvm.org/D32642