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

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

baloghadamsoftware created this revision.
baloghadamsoftware added reviewers: NoQ, dcoughlin.
Herald added subscribers: a.sidorin, szepet.

This patch is a "light" version of https://reviews.llvm.org/D35109:

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 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).


https://reviews.llvm.org/D41938

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  test/Analysis/svalbuilder-rearrange-comparisons.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D41938.129406.patch
Type: text/x-patch
Size: 46924 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20180111/d2f3baea/attachment-0001.bin>