[PATCH] D83286: [analyzer][solver] Track symbol disequalities

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko created this revision.
vsavchenko added reviewers: NoQ, dcoughlin, ASDenysPetrov, xazax.hun, Szelethus.
Herald added subscribers: cfe-commits, martong, Charusso, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware.
Herald added a project: clang.

This commmit adds another relation that we can track separately from
range constraints.  Symbol disequality can help us understand that
two equivalence classes are not equal to each other.  We can generalize
this knowledge to classes because for every a,b,c, and d that
a == b, c == d, and b != c it is true that a != d.

As a result, we can reason about other equalities/disequalities of symbols
that we know nothing else about, i.e. no constraint ranges associated
with them.  However, we also benefit from the knowledge of disequal
symbols by following the rule:

  if a != b and b == C where C is a constant, a != C

This information can refine associated ranges for different classes
and reduce the number of false positives and paths to explore.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D83286

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/equality_tracking.c
  clang/test/Analysis/mutually_exclusive_null_fp.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D83286.275952.patch
Type: text/x-patch
Size: 24561 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200707/f0cd89fe/attachment-0001.bin>