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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
