[analyzer][solver] Track symbol equivalence

[vsavchenko]

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.

[vsavchenko]

Fix incorrect comment

[xazax.hun]

I only checked the test cases and the comments so far and it looks very useful and promising. I really hope that the performance will be ok :) I'll look at the actual code changes later.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

425

I found the mention of union confusing here. Especially since merging means intersection in terms of the ranges. I think I know what you meant but some additional clarification is welcome.

[vsavchenko]

I really hope that the performance will be ok :)

I had a test run for one of the earlier implementations of this and it looks like it adds 1-2% to the execution time. And of course I will attach more info on that later.

Additionally, I have a couple of disappeared FPs concerning reference counting, that I still need to figure out.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

425

Gotcha, I guess I'll add parallels with the Union-Find data structure in the implementation and make it more transparent.

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

452

Assignment operator is currently the only thing that makes this class mutable (by allowing to change the ID after the class is constructed). Given that we want to put it into the program state, i don't think we want it to be mutable. Can we remove this operator?

537

Do i understand correctly that this isn't used yet and it's for the later patches?

1436

This makes me slightly worry about nondeterminism: height may depend on things like numeric values of pointers. I guess at the end of the day this will only manifest in choosing a different representative for the merged class, so it shouldn't be too bad, but i'd still rather double-check.

1661–1663

Ok, this turned out to be much scarier than i expected. At least, can we somehow assert that our data structures remain internally consistent after these operations? I.e., things like "a symbol points to an equivalence class iff it belongs to the set of members of that class", etc.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

452

Sure, that's a good point!

537

Not exactly, it is used in two symmetric cases:

1. We assumed a condition and we try to understand if what we assumed is an equality operation
2. We try understand something about a symbol and we want to understand if it is an equality operation

So, in the first case, the branch covering IsEquality == false does nothing and is designed for the later patches.

The second case, however, does work right now. If we see an equality operation where operands are known to be a part of the same class, we can tell for sure the result of the comparison. This way a == b is true and a != b is false. You can find this logic in getRangeForEqualities.

1436

I agree, but as you pointed out correctly, it affects only which ID is used for the class. Other ID is cease to exist after this function. ID is used other than for comparison only for trivial classes, which is not going to happen because it is guaranteed to be non-trivial after the merge. The only thing that it might affect is the ordering in the map, but we already have a problem with that as we use pointers for keys.

1661–1663

Assertion like this might cost us double of what we have in this function right now.

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

537

Ok, makes sense!

1661–1663

Sounds pretty amazing and worth every microsecond.

[vsavchenko]

Fix review remarks

[NoQ]

🎉!

I vaguely remember that we talked offline about a few nasty test cases that with casts and overflows, would it make sense to add them? Like, even if they don't pass yet, they may prove valuable.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1472

"lose"!

1487

"I am the solver!!!"

I guess what you're trying to say is that every time there's an infeasible state here, technically one of the infer() functions had a chance to prevent it (not necessarily easily).

[vsavchenko]

Fix comments and add a test for downcasts

[vsavchenko]

Rebase

[xazax.hun]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

506

Does the semantics if this differ from llvm::APInt::isNullValue?

1254

Sorry, but I am a bit confused here.

Does haveEqualConstraints have anything to do with equivalence classes?

I.e., what if I have two symbols with the same constraints (but those two symbols were never compared).

void f(int a, int b) {
  int c = clamp(a, 5, 10);
  int d = clamp(b, 5, 10);
}

In the code above if analyzer understands clamp, the range for c and d will be the same. Even though we never really compared them.
I would expect haveEqualConstraints to return true, even if they do not belong to the same equivalence class.

Do I miss something?

1380

So we basically do a conversion to Symbol -> Ranges from Class -> Ranges.
I wonder if it is possible to get rid of this conversion in the future to get some performance benefits.
We could either make all code work with both kind of range maps or have something like (Symbol + Class) -> Ranges to avoid conversion.
What do you think?

I am not opposed to this code at the moment, I just wonder if there is a relatively low hanging fruit for some performance gains in the future.

[xazax.hun]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1254

Never mind, I misunderstood this function. It operates on program states not on symbols.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

506

Good catch!

1254

Nothing to be sorry about, I'm happy to clarify!

haveEqualConstraints is here for our join heuristic that helps removing duplicating paths.

1380

This is here only for a very specific mode - when we double check found warnings with Z3. That mode needs constraints assigned to symbols, so here we construct such a set on-the-fly. So, we store ALL of the ranges in the map Class -> Ranges and construct Symbol -> Ranges on very special occasions.

[vsavchenko]

Get rid of 'isZero'

[xazax.hun]

Thanks, LGTM!

[martong]

Hi Valery,

Together with @steakhal we have found a serious issue.
The below code crashes if you compile with -DEXPENSIVE_CHECKS.
The analyzer goes on an unfeasible path, the State has a contradiction.

We think that getRange(Sym("a != b") should return a set that does not contain 0.
https://github.com/llvm/llvm-project/blob/e63b488f2755f91e8147fd678ed525cf6ba007cc/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp#L2064
Currently that goes down to infer(QualType("int")) which results a RangeSet[INT_MIN, INT_MAX].
Stach trace attached.

// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core \
// RUN:   -analyzer-checker=debug.ExprInspection \
// RUN:   -triple x86_64-unknown-linux \
// RUN:   -verify

// expected-no-diagnostics

void f(int a, int b) {
  int c = b - a;
  if (c <= 0)
    return;
  // c > 0
  // b - a > 0
  // b > a
  if (a != b)
    return;
  // a == b
  // This is an unfeasible path, the State has a contradiction.
  if (c < 0) // crash here
    ;
}

#0  (anonymous namespace)::SymbolicRangeInferrer::inferRange<clang::ento::SymExpr const*> (BV=..., F=..., State=..., Origin=0x55b9979bed08) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:715
#1  0x00007fa2314dddc9 in (anonymous namespace)::RangeConstraintManager::getRange (this=0x55b99791ab10, State=..., Sym=0x55b9979bed08) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2012
#2  0x00007fa2314de1e9 in (anonymous namespace)::RangeConstraintManager::assumeSymEQ (this=0x55b99791ab10, St=..., Sym=0x55b9979bed08, Int=..., Adjustment=...) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2064
#3  0x00007fa23150470d in clang::ento::RangedConstraintManager::assumeSymUnsupported (this=0x55b99791ab10, State=..., Sym=0x55b9979bed08, Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp:136
#4  0x00007fa2315353a9 in clang::ento::SimpleConstraintManager::assumeAux (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:62
#5  0x00007fa23153518b in clang::ento::SimpleConstraintManager::assume (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:46
#6  0x00007fa2315350e5 in clang::ento::SimpleConstraintManager::assume (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:41
#7  0x00007fa2313d39b3 in clang::ento::ConstraintManager::assumeDual (this=0x55b99791ab10, State=..., Cond=...) at ../../git/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:105
#8  0x00007fa2313d3bfc in clang::ento::ProgramState::assume (this=0x55b9979beef8, Cond=...) at ../../git/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:681
#9  0x00007fa231436b8a in clang::ento::ExprEngine::evalEagerlyAssumeBinOpBifurcation (this=0x7fffdf9ce9d0, Dst=..., Src=..., Ex=0x55b9979893f0) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/ExprEngine.cpp:3058

[vsavchenko]

In D82445#2284680, @martong wrote:

Hi Valery,

Together with @steakhal we have found a serious issue.
The below code crashes if you compile with -DEXPENSIVE_CHECKS.
The analyzer goes on an unfeasible path, the State has a contradiction.

We think that getRange(Sym("a != b") should return a set that does not contain 0.
https://github.com/llvm/llvm-project/blob/e63b488f2755f91e8147fd678ed525cf6ba007cc/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp#L2064
Currently that goes down to infer(QualType("int")) which results a RangeSet[INT_MIN, INT_MAX].
Stach trace attached.

// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core \
// RUN:   -analyzer-checker=debug.ExprInspection \
// RUN:   -triple x86_64-unknown-linux \
// RUN:   -verify

// expected-no-diagnostics

void f(int a, int b) {
  int c = b - a;
  if (c <= 0)
    return;
  // c > 0
  // b - a > 0
  // b > a
  if (a != b)
    return;
  // a == b
  // This is an unfeasible path, the State has a contradiction.
  if (c < 0) // crash here
    ;
}

#0  (anonymous namespace)::SymbolicRangeInferrer::inferRange<clang::ento::SymExpr const*> (BV=..., F=..., State=..., Origin=0x55b9979bed08) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:715
#1  0x00007fa2314dddc9 in (anonymous namespace)::RangeConstraintManager::getRange (this=0x55b99791ab10, State=..., Sym=0x55b9979bed08) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2012
#2  0x00007fa2314de1e9 in (anonymous namespace)::RangeConstraintManager::assumeSymEQ (this=0x55b99791ab10, St=..., Sym=0x55b9979bed08, Int=..., Adjustment=...) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2064
#3  0x00007fa23150470d in clang::ento::RangedConstraintManager::assumeSymUnsupported (this=0x55b99791ab10, State=..., Sym=0x55b9979bed08, Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp:136
#4  0x00007fa2315353a9 in clang::ento::SimpleConstraintManager::assumeAux (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:62
#5  0x00007fa23153518b in clang::ento::SimpleConstraintManager::assume (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:46
#6  0x00007fa2315350e5 in clang::ento::SimpleConstraintManager::assume (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:41
#7  0x00007fa2313d39b3 in clang::ento::ConstraintManager::assumeDual (this=0x55b99791ab10, State=..., Cond=...) at ../../git/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:105
#8  0x00007fa2313d3bfc in clang::ento::ProgramState::assume (this=0x55b9979beef8, Cond=...) at ../../git/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:681
#9  0x00007fa231436b8a in clang::ento::ExprEngine::evalEagerlyAssumeBinOpBifurcation (this=0x7fffdf9ce9d0, Dst=..., Src=..., Ex=0x55b9979893f0) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/ExprEngine.cpp:3058

Hi Gabor,

I'll take a look at this problem ASAP!

Thanks for such a thorough analysis of the issue!

[martong]

We came up with a quick fix, let us know what you think:
https://reviews.llvm.org/D88019

clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h

 };
 
 /// The bug visitor will walk all the nodes in a path and collect all the
 /// constraints. When it reaches the root node, will create a refutation
 /// manager and check if the constraints are satisfiable
 class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
 private:
   /// Holds the constraints in a given path
-  ConstraintRangeTy Constraints;
+  ConstraintMap Constraints;
 
 public:
   FalsePositiveRefutationBRVisitor();
 
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
   PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
                                    BugReporterContext &BRC,
                                    PathSensitiveBugReport &BR) override;
 
   void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
                        PathSensitiveBugReport &BR) override;
   void addConstraints(const ExplodedNode *N,
                       bool OverwriteConstraintsOnExistingSyms);
 };
 
-
 /// The visitor detects NoteTags and displays the event notes they contain.
 class TagVisitor : public BugReporterVisitor {
 public:
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
   PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
                                    BugReporterContext &BRC,
                                    PathSensitiveBugReport &R) override;
 };
 
 } // namespace ento
 
 } // namespace clang
 
 #endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_BUGREPORTERVISITORS_H

clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

public:
 
   void print(raw_ostream &os) const;
 
   bool operator==(const RangeSet &other) const {
     return ranges == other.ranges;
   }
 };
 
-class ConstraintRange {};
-using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;
-
-template <>
-struct ProgramStateTrait<ConstraintRange>
-    : public ProgramStatePartialTrait<ConstraintRangeTy> {
-  static void *GDMIndex();
-};
+using ConstraintMap = llvm::ImmutableMap<SymbolRef, RangeSet>;
+ConstraintMap getConstraintMap(ProgramStateRef State);
 
 class RangedConstraintManager : public SimpleConstraintManager {
 public:
   RangedConstraintManager(ExprEngine *EE, SValBuilder &SB)
       : SimpleConstraintManager(EE, SB) {}
 
   ~RangedConstraintManager() override;
 
protected:
   //===------------------------------------------------------------------===//
 private:
   static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
 };
 
 } // namespace ento
 } // namespace clang
 
+REGISTER_FACTORY_WITH_PROGRAMSTATE(ConstraintMap)
+
 #endif

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC,
   return nullptr;
 }
 
 //===----------------------------------------------------------------------===//
 // Implementation of FalsePositiveRefutationBRVisitor.
 //===----------------------------------------------------------------------===//
 
 FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
-    : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
+    : Constraints(ConstraintMap::Factory().getEmptyMap()) {}
 
 void FalsePositiveRefutationBRVisitor::finalizeVisitor(
     BugReporterContext &BRC, const ExplodedNode *EndPathNode,
     PathSensitiveBugReport &BR) {
   // Collect new constraints
   addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
 
   // Create a refutation manager
void FalsePositiveRefutationBRVisitor::finalizeVisitor(
 
   if (!IsSAT.getValue())
     BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
 }
 
 void FalsePositiveRefutationBRVisitor::addConstraints(
     const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
   // Collect new constraints
-  const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
-  ConstraintRangeTy::Factory &CF =
-      N->getState()->get_context<ConstraintRange>();
+  ConstraintMap NewCs = getConstraintMap(N->getState());
+  ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
 
   // Add constraints if we don't have them yet
   for (auto const &C : NewCs) {
     const SymbolRef &Sym = C.first;
     if (!Constraints.contains(Sym)) {
       // This symbol is new, just add the constraint.
       Constraints = CF.add(Constraints, Sym, C.second);
     } else if (OverwriteConstraintsOnExistingSyms) {

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

else
       os << ", ";
 
     os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
        << ']';
   }
   os << " }";
 }
 
+REGISTER_SET_FACTORY_WITH_PROGRAMSTATE(SymbolSet, SymbolRef)
+
+namespace {
+class EquivalenceClass;
+} // end anonymous namespace
+
+REGISTER_MAP_WITH_PROGRAMSTATE(ClassMap, SymbolRef, EquivalenceClass)
+REGISTER_MAP_WITH_PROGRAMSTATE(ClassMembers, EquivalenceClass, SymbolSet)
+REGISTER_MAP_WITH_PROGRAMSTATE(ConstraintRange, EquivalenceClass, RangeSet)
+
 namespace {
+/// This class encapsulates a set of symbols equal to each other.
+///
+/// The main idea of the approach requiring such classes is in narrowing
+/// and sharing constraints between symbols within the class.  Also we can
+/// conclude that there is no practical need in storing constraints for
+/// every member of the class separately.
+///
+/// Main terminology:
+///
+///   * "Equivalence class" is an object of this class, which can be efficiently
+///     compared to other classes.  It represents the whole class without
+///     storing the actual in it.  The members of the class however can be
+///     retrieved from the state.
+///
+///   * "Class members" are the symbols corresponding to the class.  This means
+///     that A == B for every member symbols A and B from the class.  Members of
+///     each class are stored in the state.
+///
+///   * "Trivial class" is a class that has and ever had only one same symbol.
+///
+///   * "Merge operation" merges two classes into one.  It is the main operation
+///     to produce non-trivial classes.
+///     If, at some point, we can assume that two symbols from two distinct
+///     classes are equal, we can merge these classes.
+class EquivalenceClass : public llvm::FoldingSetNode {
+public:
+  /// Find equivalence class for the given symbol in the given state.
+  LLVM_NODISCARD static inline EquivalenceClass find(ProgramStateRef State,
+                                                     SymbolRef Sym);
+
+  /// Merge classes for the given symbols and return a new state.
+  LLVM_NODISCARD static inline ProgramStateRef
+  merge(BasicValueFactory &BV, RangeSet::Factory &F, ProgramStateRef State,
+        SymbolRef First, SymbolRef Second);
+  // Merge this class with the given class and return a new state.
+  LLVM_NODISCARD inline ProgramStateRef merge(BasicValueFactory &BV,
+                                              RangeSet::Factory &F,
+                                              ProgramStateRef State,
+                                              EquivalenceClass Other);
+
+  /// Return a set of class members for the given state.
+  LLVM_NODISCARD inline SymbolSet getClassMembers(ProgramStateRef State);
+  /// Return true if the current class is trivial in the given state.
+  LLVM_NODISCARD inline bool isTrivial(ProgramStateRef State);
+  /// Return true if the current class is trivial and its only member is dead.
+  LLVM_NODISCARD inline bool isTriviallyDead(ProgramStateRef State,
+                                             SymbolReaper &Reaper);
+
+  /// Check equivalence data for consistency.
+  LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool
+  isClassDataConsistent(ProgramStateRef State);
+
+  LLVM_NODISCARD QualType getType() const {
+    return getRepresentativeSymbol()->getType();
+  }
+
+  EquivalenceClass() = delete;
+  EquivalenceClass(const EquivalenceClass &) = default;
+  EquivalenceClass &operator=(const EquivalenceClass &) = delete;
+  EquivalenceClass(EquivalenceClass &&) = default;
+  EquivalenceClass &operator=(EquivalenceClass &&) = delete;
+
+  bool operator==(const EquivalenceClass &Other) const {
+    return ID == Other.ID;
+  }
+  bool operator<(const EquivalenceClass &Other) const { return ID < Other.ID; }
+  bool operator!=(const EquivalenceClass &Other) const {
+    return !operator==(Other);
+  }
+
+  static void Profile(llvm::FoldingSetNodeID &ID, uintptr_t CID) {
+    ID.AddInteger(CID);
+  }
+
+  void Profile(llvm::FoldingSetNodeID &ID) const { Profile(ID, this->ID); }
+
+private:
+  /* implicit */ EquivalenceClass(SymbolRef Sym)
+      : ID(reinterpret_cast<uintptr_t>(Sym)) {}
+
+  /// This function is intended to be used ONLY within the class.
+  /// The fact that ID is a pointer to a symbol is an implementation detail
+  /// and should stay that way.
+  /// In the current implementation, we use it to retrieve the only member
+  /// of the trivial class.
+  SymbolRef getRepresentativeSymbol() const {
+    return reinterpret_cast<SymbolRef>(ID);
+  }
+  static inline SymbolSet::Factory &getMembersFactory(ProgramStateRef State);
+
+  inline ProgramStateRef mergeImpl(BasicValueFactory &BV, RangeSet::Factory &F,
+                                   ProgramStateRef State, SymbolSet Members,
+                                   EquivalenceClass Other,
+                                   SymbolSet OtherMembers);
+
+  /// This is a unique identifier of the class.
+  uintptr_t ID;
+};
+
+inline bool isZero(const llvm::APSInt &Int) {
+  APSIntType Type(Int);
+  return Int == Type.getZeroValue();
+}
+
+//===----------------------------------------------------------------------===//
+//                             Constraint functions
+//===----------------------------------------------------------------------===//
+
+LLVM_NODISCARD inline ProgramStateRef setConstraint(ProgramStateRef State,
+                                                    EquivalenceClass Class,
+                                                    RangeSet Constraint) {
+  return State->set<ConstraintRange>(Class, Constraint);
+}
+
+LLVM_NODISCARD inline ProgramStateRef
+setConstraint(ProgramStateRef State, SymbolRef Sym, RangeSet Constraint) {
+  return setConstraint(State, EquivalenceClass::find(State, Sym), Constraint);
+}
+
+LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
+                                                    EquivalenceClass Class) {
+  return State->get<ConstraintRange>(Class);
+}
+
+LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
+                                                    SymbolRef Sym) {
+  return getConstraint(State, EquivalenceClass::find(State, Sym));
+}
+
+//===----------------------------------------------------------------------===//
+//                       Equality/diseqiality abstraction
+//===----------------------------------------------------------------------===//
+
+/// A small helper structure representing symbolic equality.
+///
+/// Equality check can have different forms (like a == b or a - b) and this
+/// class encapsulates those away if the only thing the user wants to check -
+/// whether it's equality/diseqiality or not and have an easy access to the
+/// compared symbols.
+struct EqualityInfo {
+public:
+  SymbolRef Left, Right;
+  // true for equality and false for disequality.
+  bool IsEquality = true;
+
+  void invert() { IsEquality = !IsEquality; }
+  /// Extract equality information from the given symbol and the constants.
+  ///
+  /// This function assumes the following expression Sym + Adjustment != Int.
+  /// It is a default because the most widespread case of the equality check
+  /// is (A == B) + 0 != 0.
+  static Optional<EqualityInfo> extract(SymbolRef Sym, const llvm::APSInt &Int,
+                                        const llvm::APSInt &Adjustment) {
+    // As of now, the only equality form supported is Sym + 0 != 0.
+    if (!isZero(Int) || !isZero(Adjustment))
+      return llvm::None;
+
+    return extract(Sym);
+  }
+  /// Extract equality information from the given symbol.
+  static Optional<EqualityInfo> extract(SymbolRef Sym) {
+    return EqualityExtractor().Visit(Sym);
+  }
+
+private:
+  class EqualityExtractor
+      : public SymExprVisitor<EqualityExtractor, Optional<EqualityInfo>> {
+  public:
+    Optional<EqualityInfo> VisitSymSymExpr(const SymSymExpr *Sym) const {
+      switch (Sym->getOpcode()) {
+      case BO_Sub:
+        // This case is: A - B != 0 -> disequality check.
+        return EqualityInfo{Sym->getLHS(), Sym->getRHS(), false};
+      case BO_EQ:
+        // This case is: A == B != 0 -> equality check.
+        return EqualityInfo{Sym->getLHS(), Sym->getRHS(), true};
+      case BO_NE:
+        // This case is: A != B != 0 -> diseqiality check.
+        return EqualityInfo{Sym->getLHS(), Sym->getRHS(), false};
+      default:
+        return llvm::None;
+      }
+    }
+  };
+};
 
 //===----------------------------------------------------------------------===//
 //                            Intersection functions
 //===----------------------------------------------------------------------===//
 
 template <class SecondTy, class... RestTy>
 LLVM_NODISCARD inline RangeSet intersect(BasicValueFactory &BV,
                                          RangeSet::Factory &F, RangeSet Head,
RangeSet inferAs(SymbolRef Sym, QualType DestType) {
     }
     // Otherwise, let's simply infer from the destination type.
     // We couldn't figure out nothing else about that expression.
     return infer(DestType);
   }
 
   RangeSet infer(SymbolRef Sym) {
     if (Optional<RangeSet> ConstraintBasedRange = intersect(
-            ValueFactory, RangeFactory, State->get<ConstraintRange>(Sym),
+            ValueFactory, RangeFactory, getConstraint(State, Sym),
             // If Sym is a difference of symbols A - B, then maybe we have range
             // set stored for B - A.
             //
             // If we have range set stored for both A - B and B - A then
             // calculate the effective range set by intersecting the range set
             // for A - B and the negated range set of B - A.
-            getRangeForInvertedSub(Sym)))
+            getRangeForInvertedSub(Sym), getRangeForEqualities(Sym))) {
       return *ConstraintBasedRange;
+    }
 
     // If Sym is a comparison expression (except <=>),
     // find any other comparisons with the same operands.
     // See function description.
     if (Optional<RangeSet> CmpRangeSet = getRangeForComparisonSymbol(Sym))
       return *CmpRangeSet;
 
     return Visit(Sym);
if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
         if (!T->isUnsignedIntegerOrEnumerationType() &&
             !T->isSignedIntegerOrEnumerationType())
           return llvm::None;
 
         SymbolManager &SymMgr = State->getSymbolManager();
         SymbolRef NegatedSym =
             SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), T);
 
-        if (const RangeSet *NegatedRange =
-                State->get<ConstraintRange>(NegatedSym)) {
+        if (const RangeSet *NegatedRange = getConstraint(State, NegatedSym)) {
           return NegatedRange->Negate(ValueFactory, RangeFactory);
         }
       }
     }
     return llvm::None;
   }
 
   // Returns ranges only for binary comparison operators (except <=>)
Optional<RangeSet> getRangeForComparisonSymbol(SymbolRef Sym) {
 
     // Loop goes through all of the columns exept the last one ('UnknownX2').
     // We treat `UnknownX2` column separately at the end of the loop body.
     for (size_t i = 0; i < CmpOpTable.getCmpOpCount(); ++i) {
 
       // Let's find an expression e.g. (x < y).
       BinaryOperatorKind QueriedOP = OperatorRelationsTable::getOpFromIndex(i);
       const SymSymExpr *SymSym = SymMgr.getSymSymExpr(LHS, QueriedOP, RHS, T);
-      const RangeSet *QueriedRangeSet = State->get<ConstraintRange>(SymSym);
+      const RangeSet *QueriedRangeSet = getConstraint(State, SymSym);
 
       // If ranges were not previously found,
       // try to find a reversed expression (y > x).
       if (!QueriedRangeSet) {
         const BinaryOperatorKind ROP =
             BinaryOperator::reverseComparisonOp(QueriedOP);
         SymSym = SymMgr.getSymSymExpr(RHS, ROP, LHS, T);
-        QueriedRangeSet = State->get<ConstraintRange>(SymSym);
+        QueriedRangeSet = getConstraint(State, SymSym);
       }
 
       if (!QueriedRangeSet || QueriedRangeSet->isEmpty())
         continue;
 
       const llvm::APSInt *ConcreteValue = QueriedRangeSet->getConcreteValue();
       const bool isInFalseBranch =
           ConcreteValue ? (*ConcreteValue == 0) : false;
for (size_t i = 0; i < CmpOpTable.getCmpOpCount(); ++i) {
 
       return (BranchState == OperatorRelationsTable::True) ? getTrueRange(T)
                                                            : getFalseRange(T);
     }
 
     return llvm::None;
   }
 
+  Optional<RangeSet> getRangeForEqualities(SymbolRef Sym) {
+    Optional<EqualityInfo> Equality = EqualityInfo::extract(Sym);
+
+    if (!Equality)
+      return llvm::None;
+
+    EquivalenceClass LHS = EquivalenceClass::find(State, Equality->Left);
+    EquivalenceClass RHS = EquivalenceClass::find(State, Equality->Right);
+
+    if (LHS != RHS)
+      // Can't really say anything at this point.
+      // We can add more logic here if we track disequalities as well.
+      return llvm::None;
+
+    // At this point, operands of the equality operation are known to be equal.
+    if (Equality->IsEquality) {
+      return getTrueRange(Sym->getType());
+    }
+    return getFalseRange(Sym->getType());
+  }
+
   RangeSet getTrueRange(QualType T) {
     RangeSet TypeRange = infer(T);
     return assumeNonZero(TypeRange, T);
   }
 
   RangeSet getFalseRange(QualType T) {
     const llvm::APSInt &Zero = ValueFactory.getValue(0, T);
     return RangeSet(RangeFactory, Zero);
RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
       : RangedConstraintManager(EE, SVB) {}
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
 
   bool haveEqualConstraints(ProgramStateRef S1,
                             ProgramStateRef S2) const override {
-    return S1->get<ConstraintRange>() == S2->get<ConstraintRange>();
+    // NOTE: ClassMembers are as simple as back pointers for ClassMap,
+    //       so comparing constraint ranges and class maps should be
+    //       sufficient.
+    return S1->get<ConstraintRange>() == S2->get<ConstraintRange>() &&
+           S1->get<ClassMap>() == S2->get<ClassMap>();
   }
 
   bool canReasonAbout(SVal X) const override;
 
   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
 
   const llvm::APSInt *getSymVal(ProgramStateRef State,
                                 SymbolRef Sym) const override;
RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymLERange(llvm::function_ref<RangeSet()> RS,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
+
+  //===------------------------------------------------------------------===//
+  // Equality tracking implementation
+  //===------------------------------------------------------------------===//
+
+  ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym,
+                          const llvm::APSInt &Int,
+                          const llvm::APSInt &Adjustment) {
+    if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
+      // Extract function assumes that we gave it Sym + Adjustment != Int,
+      // so the result should be opposite.
+      Equality->invert();
+      return track(State, *Equality);
+    }
+
+    return State;
+  }
+
+  ProgramStateRef trackNE(ProgramStateRef State, SymbolRef Sym,
+                          const llvm::APSInt &Int,
+                          const llvm::APSInt &Adjustment) {
+    if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
+      return track(State, *Equality);
+    }
+
+    return State;
+  }
+
+  ProgramStateRef track(ProgramStateRef State, EqualityInfo ToTrack) {
+    if (ToTrack.IsEquality) {
+      return trackEquality(State, ToTrack.Left, ToTrack.Right);
+    }
+    return trackDisequality(State, ToTrack.Left, ToTrack.Right);
+  }
+
+  ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS,
+                                   SymbolRef RHS) {
+    // TODO: track inequalities
+    return State;
+  }
+
+  ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS,
+                                SymbolRef RHS);
 };
 
 } // end anonymous namespace
 
 std::unique_ptr<ConstraintManager>
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr,
                                    ExprEngine *Eng) {
   return std::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
 
+ConstraintMap ento::getConstraintMap(ProgramStateRef State) {
+  ConstraintMap::Factory &F = State->get_context<ConstraintMap>();
+  ConstraintMap Result = F.getEmptyMap();
+
+  ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+  for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
+    EquivalenceClass Class = ClassConstraint.first;
+    SymbolSet ClassMembers = Class.getClassMembers(State);
+    assert(!ClassMembers.isEmpty() &&
+           "Class must always have at least one member!");
+
+    SymbolRef Representative = *ClassMembers.begin();
+    Result = F.add(Result, Representative, ClassConstraint.second);
+  }
+
+  return Result;
+}
+
+//===----------------------------------------------------------------------===//
+//                     EqualityClass implementation details
+//===----------------------------------------------------------------------===//
+
+inline EquivalenceClass EquivalenceClass::find(ProgramStateRef State,
+                                               SymbolRef Sym) {
+  // We store far from all Symbol -> Class mappings
+  if (const EquivalenceClass *NontrivialClass = State->get<ClassMap>(Sym))
+    return *NontrivialClass;
+
+  // This is a trivial class of Sym.
+  return Sym;
+}
+
+inline ProgramStateRef EquivalenceClass::merge(BasicValueFactory &BV,
+                                               RangeSet::Factory &F,
+                                               ProgramStateRef State,
+                                               SymbolRef First,
+                                               SymbolRef Second) {
+  EquivalenceClass FirstClass = find(State, First);
+  EquivalenceClass SecondClass = find(State, Second);
+
+  return FirstClass.merge(BV, F, State, SecondClass);
+}
+
+inline ProgramStateRef EquivalenceClass::merge(BasicValueFactory &BV,
+                                               RangeSet::Factory &F,
+                                               ProgramStateRef State,
+                                               EquivalenceClass Other) {
+  // It is already the same class.
+  if (*this == Other)
+    return State;
+
+  // FIXME: As of now, we support only equivalence classes of the same type.
+  //        This limitation is connected to the lack of explicit casts in
+  //        our symbolic expression model.
+  //
+  //        That means that for `int x` and `char y` we don't distinguish
+  //        between these two very different cases:
+  //          * `x == y`
+  //          * `(char)x == y`
+  //
+  //        The moment we introduce symbolic casts, this restriction can be
+  //        lifted.
+  if (getType() != Other.getType())
+    return State;
+
+  SymbolSet Members = getClassMembers(State);
+  SymbolSet OtherMembers = Other.getClassMembers(State);
+
+  // We estimate the size of the class by the height of tree containing
+  // its members.  Merging is not a trivial operation, so it's easier to
+  // merge the smaller class into the bigger one.
+  if (Members.getHeight() >= OtherMembers.getHeight()) {
+    return mergeImpl(BV, F, State, Members, Other, OtherMembers);
+  } else {
+    return Other.mergeImpl(BV, F, State, OtherMembers, *this, Members);
+  }
+}
+
+inline ProgramStateRef
+EquivalenceClass::mergeImpl(BasicValueFactory &ValueFactory,
+                            RangeSet::Factory &RangeFactory,
+                            ProgramStateRef State, SymbolSet MyMembers,
+                            EquivalenceClass Other, SymbolSet OtherMembers) {
+  // Essentially what we try to recreate here is some kind of union-find
+  // data structure.  It does have certain limitations due to persistence
+  // and the need to remove elements from classes.
+  //
+  // In this setting, EquialityClass object is the representative of the class
+  // or the parent element.  ClassMap is a mapping of class members to their
+  // parent. Unlike the union-find structure, they all point directly to the
+  // class representative because we don't have an opportunity to actually do
+  // path compression when dealing with immutability.  This means that we
+  // compress paths every time we do merges.  It also means that we lose
+  // the main amortized complexity benefit from the original data structure.
+  ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+  ConstraintRangeTy::Factory &CRF = State->get_context<ConstraintRange>();
+
+  // 1. If the merged classes have any constraints associated with them, we
+  //    need to transfer them to the class we have left.
+  //
+  // Intersection here makes perfect sense because both of these constraints
+  // must hold for the whole new class.
+  if (Optional<RangeSet> NewClassConstraint =
+          intersect(ValueFactory, RangeFactory, getConstraint(State, *this),
+                    getConstraint(State, Other))) {
+    // NOTE: Essentially, NewClassConstraint should NEVER be infeasible because
+    //       range inferrer shouldn't generate ranges incompatible with
+    //       equivalence classes. However, at the moment, due to imperfections
+    //       in the solver, it is possible and the merge function can also
+    //       return infeasible states aka null states.
+    if (NewClassConstraint->isEmpty())
+      // Infeasible state
+      return nullptr;
+
+    // No need in tracking constraints of a now-dissolved class.
+    Constraints = CRF.remove(Constraints, Other);
+    // Assign new constraints for this class.
+    Constraints = CRF.add(Constraints, *this, *NewClassConstraint);
+
+    State = State->set<ConstraintRange>(Constraints);
+  }
+
+  // 2. Get ALL equivalence-related maps
+  ClassMapTy Classes = State->get<ClassMap>();
+  ClassMapTy::Factory &CF = State->get_context<ClassMap>();
+
+  ClassMembersTy Members = State->get<ClassMembers>();
+  ClassMembersTy::Factory &MF = State->get_context<ClassMembers>();
+
+  SymbolSet::Factory &F = getMembersFactory(State);
+
+  // 2. Merge members of the Other class into the current class.
+  SymbolSet NewClassMembers = MyMembers;
+  for (SymbolRef Sym : OtherMembers) {
+    NewClassMembers = F.add(NewClassMembers, Sym);
+    // *this is now the class for all these new symbols.
+    Classes = CF.add(Classes, Sym, *this);
+  }
+
+  // 3. Adjust member mapping.
+  //
+  // No need in tracking members of a now-dissolved class.
+  Members = MF.remove(Members, Other);
+  // Now only the current class is mapped to all the symbols.
+  Members = MF.add(Members, *this, NewClassMembers);
+
+  // 4. Update the state
+  State = State->set<ClassMap>(Classes);
+  State = State->set<ClassMembers>(Members);
+
+  return State;
+}
+
+inline SymbolSet::Factory &
+EquivalenceClass::getMembersFactory(ProgramStateRef State) {
+  return State->get_context<SymbolSet>();
+}
+
+SymbolSet EquivalenceClass::getClassMembers(ProgramStateRef State) {
+  if (const SymbolSet *Members = State->get<ClassMembers>(*this))
+    return *Members;
+
+  // This class is trivial, so we need to construct a set
+  // with just that one symbol from the class.
+  SymbolSet::Factory &F = getMembersFactory(State);
+  return F.add(F.getEmptySet(), getRepresentativeSymbol());
+}
+
+bool EquivalenceClass::isTrivial(ProgramStateRef State) {
+  return State->get<ClassMembers>(*this) == nullptr;
+}
+
+bool EquivalenceClass::isTriviallyDead(ProgramStateRef State,
+                                       SymbolReaper &Reaper) {
+  return isTrivial(State) && Reaper.isDead(getRepresentativeSymbol());
+}
+
+bool EquivalenceClass::isClassDataConsistent(ProgramStateRef State) {
+  ClassMembersTy Members = State->get<ClassMembers>();
+
+  for (std::pair<EquivalenceClass, SymbolSet> ClassMembersPair : Members) {
+    for (SymbolRef Member : ClassMembersPair.second) {
+      // Every member of the class should have a mapping back to the class.
+      if (find(State, Member) == ClassMembersPair.first) {
+        continue;
+      }
+
+      return false;
+    }
+  }
+
+  return true;
+}
+
 //===----------------------------------------------------------------------===//
 //                    RangeConstraintManager implementation
 //===----------------------------------------------------------------------===//
 
 bool RangeConstraintManager::canReasonAbout(SVal X) const {
   Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
   if (SymVal && SymVal->isExpression()) {
     const SymExpr *SE = SymVal->getSymbol();
if (SymVal && SymVal->isExpression()) {
     return false;
   }
 
   return true;
 }
 
 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
                                                     SymbolRef Sym) {
-  const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
+  const RangeSet *Ranges = getConstraint(State, Sym);
 
   // If we don't have any information about this symbol, it's underconstrained.
   if (!Ranges)
     return ConditionTruthVal();
 
   // If we have a concrete value, see if it's zero.
   if (const llvm::APSInt *Value = Ranges->getConcreteValue())
     return *Value == 0;
 
   BasicValueFactory &BV = getBasicVals();
   APSIntType IntType = BV.getAPSIntType(Sym->getType());
   llvm::APSInt Zero = IntType.getZeroValue();
 
   // Check if zero is in the set of possible values.
   if (Ranges->Intersect(BV, F, Zero, Zero).isEmpty())
     return false;
 
   // Zero is a possible value, but it is not the /only/ possible value.
   return ConditionTruthVal();
 }
 
 const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
                                                       SymbolRef Sym) const {
-  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym);
+  const RangeSet *T = getConstraint(St, Sym);
   return T ? T->getConcreteValue() : nullptr;
 }
 
 //===----------------------------------------------------------------------===//
 //                Remove dead symbols from existing constraints
 //===----------------------------------------------------------------------===//
 
 /// Scan all symbols referenced by the constraints. If the symbol is not alive
 /// as marked in LSymbols, mark it as dead in DSymbols.
 ProgramStateRef
 RangeConstraintManager::removeDeadBindings(ProgramStateRef State,
                                            SymbolReaper &SymReaper) {
-  bool Changed = false;
-  ConstraintRangeTy CR = State->get<ConstraintRange>();
-  ConstraintRangeTy::Factory &CRFactory = State->get_context<ConstraintRange>();
+  ClassMembersTy ClassMembersMap = State->get<ClassMembers>();
+  ClassMembersTy NewClassMembersMap = ClassMembersMap;
+  ClassMembersTy::Factory &EMFactory = State->get_context<ClassMembers>();
+  SymbolSet::Factory &SetFactory = State->get_context<SymbolSet>();
+
+  ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+  ConstraintRangeTy NewConstraints = Constraints;
+  ConstraintRangeTy::Factory &ConstraintFactory =
+      State->get_context<ConstraintRange>();
+
+  ClassMapTy Map = State->get<ClassMap>();
+  ClassMapTy NewMap = Map;
+  ClassMapTy::Factory &ClassFactory = State->get_context<ClassMap>();
+
+  bool ClassMapChanged = false;
+  bool MembersMapChanged = false;
+  bool ConstraintMapChanged = false;
+
+  // 1. Let's see if dead symbols are trivial and have associated constraints.
+  for (std::pair<EquivalenceClass, RangeSet> ClassConstraintPair :
+       Constraints) {
+    EquivalenceClass Class = ClassConstraintPair.first;
+    if (Class.isTriviallyDead(State, SymReaper)) {
+      // If this class is trivial, we can remove its constraints right away.
+      Constraints = ConstraintFactory.remove(Constraints, Class);
+      ConstraintMapChanged = true;
+    }
+  }
+
+  // 2. We don't need to track classes for dead symbols.
+  for (std::pair<SymbolRef, EquivalenceClass> SymbolClassPair : Map) {
+    SymbolRef Sym = SymbolClassPair.first;
 
-  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
-    SymbolRef Sym = I.getKey();
     if (SymReaper.isDead(Sym)) {
-      Changed = true;
-      CR = CRFactory.remove(CR, Sym);
+      ClassMapChanged = true;
+      NewMap = ClassFactory.remove(NewMap, Sym);
     }
   }
 
-  return Changed ? State->set<ConstraintRange>(CR) : State;
+  // 3. Remove dead members from classes and remove dead non-trivial classes
+  //    and their constraints.
+  for (std::pair<EquivalenceClass, SymbolSet> ClassMembersPair :
+       ClassMembersMap) {
+    SymbolSet LiveMembers = ClassMembersPair.second;
+    bool MembersChanged = false;
+
+    for (SymbolRef Member : ClassMembersPair.second) {
+      if (SymReaper.isDead(Member)) {
+        MembersChanged = true;
+        LiveMembers = SetFactory.remove(LiveMembers, Member);
+      }
+    }
+
+    // Check if the class changed.
+    if (!MembersChanged)
+      continue;
+
+    MembersMapChanged = true;
+
+    if (LiveMembers.isEmpty()) {
+      // The class is dead now, we need to wipe it out of the members map...
+      NewClassMembersMap =
+          EMFactory.remove(NewClassMembersMap, ClassMembersPair.first);
+
+      // ...and remove all of its constraints.
+      Constraints =
+          ConstraintFactory.remove(Constraints, ClassMembersPair.first);
+      ConstraintMapChanged = true;
+    } else {
+      // We need to change the members associated with the class.
+      NewClassMembersMap = EMFactory.add(NewClassMembersMap,
+                                         ClassMembersPair.first, LiveMembers);
+    }
+  }
+
+  // 4. Update the state with new maps.
+  //
+  // Here we try to be humble and update a map only if it really changed.
+  if (ClassMapChanged)
+    State = State->set<ClassMap>(NewMap);
+
+  if (MembersMapChanged)
+    State = State->set<ClassMembers>(NewClassMembersMap);
+
+  if (ConstraintMapChanged)
+    State = State->set<ConstraintRange>(Constraints);
+
+  assert(EquivalenceClass::isClassDataConsistent(State));
+
+  return State;
 }
 
 RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
                                           SymbolRef Sym) {
   return SymbolicRangeInferrer::inferRange(getBasicVals(), F, State, Sym);
 }
 
 //===------------------------------------------------------------------------===
RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
     return St;
 
   llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
 
   RangeSet New = getRange(St, Sym).Delete(getBasicVals(), F, Point);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+
+  if (New.isEmpty())
+    // this is infeasible assumption
+    return nullptr;
+
+  ProgramStateRef NewState = setConstraint(St, Sym, New);
+  return trackNE(NewState, Sym, Int, Adjustment);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
     return nullptr;
 
   // [Int-Adjustment, Int-Adjustment]
   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
   RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+
+  if (New.isEmpty())
+    // this is infeasible assumption
+    return nullptr;
+
+  ProgramStateRef NewState = setConstraint(St, Sym, New);
+  return trackEQ(NewState, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St,
                                                SymbolRef Sym,
                                                const llvm::APSInt &Int,
                                                const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St,
   return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
 }
 
 RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
                                                SymbolRef Sym,
                                                const llvm::APSInt &Int,
                                                const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
   return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
 }
 
 RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St,
                                                SymbolRef Sym,
                                                const llvm::APSInt &Int,
                                                const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St,
   return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGERange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
 }
 
-RangeSet RangeConstraintManager::getSymLERange(
-      llvm::function_ref<RangeSet()> RS,
+RangeSet
+RangeConstraintManager::getSymLERange(llvm::function_ref<RangeSet()> RS,
                                       const llvm::APSInt &Int,
                                       const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
     return F.getEmptySet();
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
RangeSet RangeConstraintManager::getSymLERange(ProgramStateRef St,
   return getSymLERange([&] { return getRange(St, Sym); }, Int, Adjustment);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   RangeSet New = getSymLERange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
 }
 
 ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGERange(State, Sym, From, Adjustment);
   if (New.isEmpty())
     return nullptr;
   RangeSet Out = getSymLERange([&] { return New; }, To, Adjustment);
-  return Out.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, Out);
+  return Out.isEmpty() ? nullptr : setConstraint(State, Sym, Out);
 }
 
 ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
   RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment);
   RangeSet New(RangeLT.addRange(F, RangeGT));
-  return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
+  return New.isEmpty() ? nullptr : setConstraint(State, Sym, New);
+}
+
+ProgramStateRef RangeConstraintManager::trackEquality(ProgramStateRef State,
+                                                      SymbolRef LHS,
+                                                      SymbolRef RHS) {
+  return EquivalenceClass::merge(getBasicVals(), F, State, LHS, RHS);
 }
 
 //===----------------------------------------------------------------------===//
 // Pretty-printing.
 //===----------------------------------------------------------------------===//
 
 void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State,
                                        const char *NL, unsigned int Space,
                                        bool IsDot) const {
   ConstraintRangeTy Constraints = State->get<ConstraintRange>();
 
   Indent(Out, Space, IsDot) << "\"constraints\": ";
   if (Constraints.isEmpty()) {
     Out << "null," << NL;
     return;
   }
 
   ++Space;
   Out << '[' << NL;
-  for (ConstraintRangeTy::iterator I = Constraints.begin();
-       I != Constraints.end(); ++I) {
-    Indent(Out, Space, IsDot)
-        << "{ \"symbol\": \"" << I.getKey() << "\", \"range\": \"";
-    I.getData().print(Out);
-    Out << "\" }";
-
-    if (std::next(I) != Constraints.end())
+  bool First = true;
+  for (std::pair<EquivalenceClass, RangeSet> P : Constraints) {
+    SymbolSet ClassMembers = P.first.getClassMembers(State);
+
+    // We can print the same constraint for every class member.
+    for (SymbolRef ClassMember : ClassMembers) {
+      if (First) {
+        First = false;
+      } else {
         Out << ',';
         Out << NL;
       }
+      Indent(Out, Space, IsDot)
+          << "{ \"symbol\": \"" << ClassMember << "\", \"range\": \"";
+      P.second.print(Out);
+      Out << "\" }";
+    }
+  }
+  Out << NL;
 
   --Space;
   Indent(Out, Space, IsDot) << "]," << NL;
 }

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

if (isa<SymbolData>(Sym)) {
     if (BinaryOperator::isComparisonOp(op) && op != BO_Cmp) {
       if (!Assumption)
         op = BinaryOperator::negateComparisonOp(op);
 
       return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
     }
 
   } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
+    BinaryOperator::Opcode Op = SSE->getOpcode();
+    assert(BinaryOperator::isComparisonOp(Op));
+
+    // We convert equality operations for pointers only.
+    if (Loc::isLocType(SSE->getLHS()->getType()) &&
+        Loc::isLocType(SSE->getRHS()->getType())) {
       // Translate "a != b" to "(b - a) != 0".
       // We invert the order of the operands as a heuristic for how loop
       // conditions are usually written ("begin != end") as compared to length
       // calculations ("end - begin"). The more correct thing to do would be to
       // canonicalize "a - b" and "b - a", which would allow us to treat
       // "a != b" and "b != a" the same.
-    SymbolManager &SymMgr = getSymbolManager();
-    BinaryOperator::Opcode Op = SSE->getOpcode();
-    assert(BinaryOperator::isComparisonOp(Op));
 
-    // For now, we only support comparing pointers.
-    if (Loc::isLocType(SSE->getLHS()->getType()) &&
-        Loc::isLocType(SSE->getRHS()->getType())) {
+      SymbolManager &SymMgr = getSymbolManager();
       QualType DiffTy = SymMgr.getContext().getPointerDiffType();
       SymbolRef Subtraction =
           SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
 
       const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
       Op = BinaryOperator::reverseComparisonOp(Op);
       if (!Assumption)
         Op = BinaryOperator::negateComparisonOp(Op);
       return assumeSymRel(State, Subtraction, Op, Zero);
     }
+
+    if (BinaryOperator::isEqualityOp(Op)) {
+      SymbolManager &SymMgr = getSymbolManager();
+
+      QualType ExprType = SSE->getType();
+      SymbolRef CanonicalEquality =
+          SymMgr.getSymSymExpr(SSE->getLHS(), BO_EQ, SSE->getRHS(), ExprType);
+
+      bool WasEqual = SSE->getOpcode() == BO_EQ;
+      bool IsExpectedEqual = WasEqual == Assumption;
+
+      const llvm::APSInt &Zero = getBasicVals().getValue(0, ExprType);
+
+      if (IsExpectedEqual) {
+        return assumeSymNE(State, CanonicalEquality, Zero, Zero);
+      }
+
+      return assumeSymEQ(State, CanonicalEquality, Zero, Zero);
+    }
   }
 
   // If we get here, there's nothing else we can do but treat the symbol as
   // opaque.
   return assumeSymUnsupported(State, Sym, Assumption);
 }
 
 ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
if (Op == BO_Add || Op == BO_Sub) {
       // This should happen /after/ promotion, in case the value being
       // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
       if (Op == BO_Sub)
         Adjustment = -Adjustment;
     }
   }
 }
 
-void *ProgramStateTrait<ConstraintRange>::GDMIndex() {
-  static int Index;
-  return &Index;
-}
-
 } // end of namespace ento
 
 } // end of namespace clang

clang/test/Analysis/equality_tracking.c

+// RUN: %clang_analyze_cc1 -verify %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false
+
+#define NULL (void *)0
+
+#define UCHAR_MAX (unsigned char)(~0U)
+#define CHAR_MAX (char)(UCHAR_MAX & (UCHAR_MAX >> 1))
+#define CHAR_MIN (char)(UCHAR_MAX & ~(UCHAR_MAX >> 1))
+
+void clang_analyzer_eval(int);
+void clang_analyzer_warnIfReached();
+
+int getInt();
+
+void zeroImpliesEquality(int a, int b) {
+  clang_analyzer_eval((a - b) == 0); // expected-warning{{UNKNOWN}}
+  if ((a - b) == 0) {
+    clang_analyzer_eval(b != a);    // expected-warning{{FALSE}}
+    clang_analyzer_eval(b == a);    // expected-warning{{TRUE}}
+    clang_analyzer_eval(!(a != b)); // expected-warning{{TRUE}}
+    clang_analyzer_eval(!(b == a)); // expected-warning{{FALSE}}
+    return;
+  }
+  clang_analyzer_eval((a - b) == 0); // expected-warning{{FALSE}}
+  // FIXME: we should track disequality information as well
+  clang_analyzer_eval(b == a); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b != a); // expected-warning{{UNKNOWN}}
+}
+
+void zeroImpliesReversedEqual(int a, int b) {
+  clang_analyzer_eval((b - a) == 0); // expected-warning{{UNKNOWN}}
+  if ((b - a) == 0) {
+    clang_analyzer_eval(b != a); // expected-warning{{FALSE}}
+    clang_analyzer_eval(b == a); // expected-warning{{TRUE}}
+    return;
+  }
+  clang_analyzer_eval((b - a) == 0); // expected-warning{{FALSE}}
+  // FIXME: we should track disequality information as well
+  clang_analyzer_eval(b == a); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(b != a); // expected-warning{{UNKNOWN}}
+}
+
+void canonicalEqual(int a, int b) {
+  clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
+  if (a == b) {
+    clang_analyzer_eval(b == a); // expected-warning{{TRUE}}
+    return;
+  }
+  clang_analyzer_eval(a == b); // expected-warning{{FALSE}}
+  clang_analyzer_eval(b == a); // expected-warning{{FALSE}}
+}
+
+void test(int a, int b, int c, int d) {
+  if (a == b && c == d) {
+    if (a == 0 && b == d) {
+      clang_analyzer_eval(c == 0); // expected-warning{{TRUE}}
+    }
+    c = 10;
+    if (b == d) {
+      clang_analyzer_eval(c == 10); // expected-warning{{TRUE}}
+      clang_analyzer_eval(d == 10); // expected-warning{{UNKNOWN}}
+                                    // expected-warning@-1{{FALSE}}
+      clang_analyzer_eval(b == a);  // expected-warning{{TRUE}}
+      clang_analyzer_eval(a == d);  // expected-warning{{TRUE}}
+
+      b = getInt();
+      clang_analyzer_eval(a == d); // expected-warning{{TRUE}}
+      clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
+    }
+  }
+
+  if (a != b && b == c) {
+    if (c == 42) {
+      clang_analyzer_eval(b == 42); // expected-warning{{TRUE}}
+      // FIXME: we should track disequality information as well
+      clang_analyzer_eval(a != 42); // expected-warning{{UNKNOWN}}
+    }
+  }
+}
+
+void testIntersection(int a, int b, int c) {
+  if (a < 42 && b > 15 && c >= 25 && c <= 30) {
+    if (a != b)
+      return;
+
+    clang_analyzer_eval(a > 15);  // expected-warning{{TRUE}}
+    clang_analyzer_eval(b < 42);  // expected-warning{{TRUE}}
+    clang_analyzer_eval(a <= 30); // expected-warning{{UNKNOWN}}
+
+    if (c == b) {
+      // For all equal symbols, we should track the minimal common range.
+      //
+      // Also, it should be noted that c is dead at this point, but the
+      // constraint initially associated with c is still around.
+      clang_analyzer_eval(a >= 25 && a <= 30); // expected-warning{{TRUE}}
+      clang_analyzer_eval(b >= 25 && b <= 30); // expected-warning{{TRUE}}
+    }
+  }
+}
+
+void testPromotion(int a, char b) {
+  if (b > 10) {
+    if (a == b) {
+      // FIXME: support transferring char ranges onto equal int symbols
+      //        when char is promoted to int
+      clang_analyzer_eval(a > 10);        // expected-warning{{UNKNOWN}}
+      clang_analyzer_eval(a <= CHAR_MAX); // expected-warning{{UNKNOWN}}
+    }
+  }
+}
+
+void testPromotionOnlyTypes(int a, char b) {
+  if (a == b) {
+    // FIXME: support transferring char ranges onto equal int symbols
+    //        when char is promoted to int
+    clang_analyzer_eval(a <= CHAR_MAX); // expected-warning{{UNKNOWN}}
+  }
+}
+
+void testDowncast(int a, unsigned char b) {
+  if (a <= -10) {
+    if ((unsigned char)a == b) {
+      // Even though ranges for a and b do not intersect,
+      // ranges for (unsigned char)a and b do.
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+    }
+    if (a == b) {
+      // FIXME: This case on the other hand is different, it shouldn't be
+      //        reachable.  However, the corrent symbolic information available
+      //        to the solver doesn't allow it to distinguish this expression
+      //        from the previous one.
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+    }
+  }
+}
+
+void testPointers(int *a, int *b, int *c, int *d) {
+  if (a == b && c == d) {
+    if (a == NULL && b == d) {
+      clang_analyzer_eval(c == NULL); // expected-warning{{TRUE}}
+    }
+  }
+
+  if (a != b && b == c) {
+    if (c == NULL) {
+      // FIXME: we should track disequality information as well
+      clang_analyzer_eval(a != NULL); // expected-warning{{UNKNOWN}}
+    }
+  }
+}
+
+void avoidInfeasibleConstraintsForClasses(int a, int b) {
+  if (a >= 0 && a <= 10 && b >= 20 && b <= 50) {
+    if ((b - a) == 0) {
+      clang_analyzer_warnIfReached(); // no warning
+    }
+    if (a == b) {
+      clang_analyzer_warnIfReached(); // no warning
+    }
+    if (a != b) {
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+    } else {
+      clang_analyzer_warnIfReached(); // no warning
+    }
+  }
+}