[Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)

[Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)

Since the range-based constraint manager (default) is weak in handling comparisons where symbols are on both sides it is wise to rearrange them to have symbols only on the left side. Thus e.g. A + n >= B + m becomes A - B >= m - n which enables the constraint manager to store a range m - n .. MAX_VALUE for the symbolic expression A - B. This can be used later to check whether e.g. A + k == B + l can be true, which is also rearranged to A - B == l - k so the constraint manager can check whether l - k is in the range (thus greater than or equal to m - n).

The restriction in this version is the the rearrangement happens only if both the symbols and the concrete integers are within the range [min/4 .. max/4] where min and max are the minimal and maximal values of their type.

The rearrangement is not enabled by default. It has to be enabled by using -analyzer-config aggressive-relational-comparison-simplification=true.

Co-author of this patch is Artem Dergachev (NoQ).

Differential Revision: https://reviews.llvm.org/D41938

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@329780 91177308-0d34-0410-b5e6-96231b3b80d8