[analyzer][solver] Track symbol equivalence
authorValeriy Savchenko <vsavchenko@apple.com>
Wed, 24 Jun 2020 09:50:56 +0000 (12:50 +0300)
committerValeriy Savchenko <vsavchenko@apple.com>
Wed, 22 Jul 2020 10:02:39 +0000 (13:02 +0300)
commitb13d9878b8dcef4354ddfc86f382ca9b537e65aa
treefe1c57194700e65dc27e77075c332e877c17f7c3
parentf531c1c7c0d5850c824333518ff32708730d775b
[analyzer][solver] Track symbol equivalence

Summary:
For the most cases, we try to reason about symbol either based on the
information we know about that symbol in particular or about its
composite parts.  This is faster and eliminates costly brute force
searches through existing constraints.

However, we do want to support some cases that are widespread enough
and involve reasoning about different existing constraints at once.
These include:
  * resoning about 'a - b' based on what we know about 'b - a'
  * reasoning about 'a <= b' based on what we know about 'a > b' or 'a < b'

This commit expands on that part by tracking symbols known to be equal
while still avoiding brute force searches.  It changes the way we track
constraints for individual symbols.  If we know for a fact that 'a == b'
then there is no need in tracking constraints for both 'a' and 'b' especially
if these constraints are different.  This additional relationship makes
dead/live logic for constraints harder as we want to maintain as much
information on the equivalence class as possible, but we still won't
carry the information that we don't need anymore.

Differential Revision: https://reviews.llvm.org/D82445
clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
clang/test/Analysis/equality_tracking.c [new file with mode: 0644]