[analyzer][solver] Track symbol disequalities

[vsavchenko]

Summary

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.

[vsavchenko]

Rebase

[NoQ]

This looks great to me but i'd very much rather have someone else have a look, just because of the nature of the problem (:

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1579

Nit: I think it's a bit messy to use getDisequalClasses() in some places but manual lookup in other places. Like, someone may change the function and believe that they changed the entire lookup mechanism but fail to notice that the function wasn't used consitently. I think this may be worth encapsulating.

1721

Parse error; missing "we"?

1914–1916

I actually wouldn't mind duplicating a direct assertion here, given that consistency checks are pretty complicated on their own :)

clang/test/Analysis/mutually_exclusive_null_fp.cpp

26

// no-warning please? These marks make tests a lot easier to understand when you break them 5 years later.

[ASDenysPetrov]

@vsavchenko

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

Did you take into account that e.g. a > b also is a disequality.

[vsavchenko]

In D83286#2138734, @ASDenysPetrov wrote:

Did you take into account that e.g. a > b also is a disequality.

It is a very good point! I didn't take them into account (yet?) because they make the implementation a bit harder.
Right now we can decide by the look of the assumption (or symbolic expression) if it's an equality/disequality check. Later on, if we see an expression that looks like equality/disequality, we can try to see what we know about its operands. So here we have a fairly easy table (2x2) of possible outcomes: if our current knowledge of the equality/disequality matches the current check - it's true, if it's opposite - it's false.

When it comes to things like a > b, we can consider it as disequality when we start tracking it because a > b -> a != b, but cannot in the second case because a != b -/-> a > b. As the result, this beautiful symmetry that I use is gone and we need to add more data into EqualityInfo so we support the one-sidedness of that implication.

It is not a big change, but I would prefer making it separately.

[vsavchenko]

Fix review remarks

[vsavchenko]

Introduction

I have some test results with execution times. Because the execution time varies from one execution to another, I've measured performance on master twice (I know that it's not very conclusive) to show that equivalence tracking doesn't affect performance of the analyzer. So, please, let's treat it more like a smoke test that everything stayed the same with a new functionality rather than a full-blown performance benchmarking.

Raw results

project	master run#1	master run#2	patch run#1
box2d	137.57s	156.36s	142.46s
cxxopts	26.74s	29.31s	27.01s
drogon	257.43s	265.88s	263.00s
duckdb	2251.08s	2297.60s	2258.06s
fmt	266.96s	293.06s	279.26s
libsoundio	33.89s	35.37s	36.48s
oatpp	171.58s	175.25s	172.92s
re2	84.12s	133.46s	87.24s
simbody	1405.25s	1374.38s	1365.58s
symengine	455.94s	487.50s	466.28s
termbox	20.91s	20.28s	20.88s
tinyexpr	11.91s	13.53s	12.58s
tinyspline	48.61s	49.01s	48.90s
tinyvm	27.77s	29.32s	28.70s
zstd	150.28s	152.86s	154.21s

Processed results

project	min delta	max delta	within range
box2d	-8.9%	3.6%
cxxopts	-7.8%	1.0%
drogon	-1.1%	2.2%
duckdb	-1.7%	0.3%
fmt	-4.7%	4.6%
libsoundio	3.1%	7.6%
oatpp	-1.3%	0.8%
re2	-34.6%	3.7%
simbody	-2.8%	-0.6%
symengine	-4.4%	2.3%
termbox	-0.1%	3.0%
tinyexpr	-7.0%	5.6%
tinyspline	-0.2%	0.6%
tinyvm	-2.1%	3.3%
zstd	0.9%	2.6%

Diff results

The only project that had any difference in terms of warnings was simbody:

--- Building project simbody
2020-07-08 07:53:32,956:INFO:main: Log file: /projects/simbody/ScanBuildResults/Logs/run_static_analyzer.log
2020-07-08 07:53:32,956:INFO:main: Output directory: /projects/simbody/ScanBuildResults
2020-07-08 07:54:03,447:INFO:main:   No local patches.
2020-07-08 08:16:18,536:INFO:main: Build complete (time: 1365.58). See the log for more details: /projects/simbody/ScanBuildResults/Logs/run_static_analyzer.log
2020-07-08 08:16:22,965:INFO:main: Number of bug reports (non-empty plist files) produced: 181
2020-07-08 08:16:29,197:INFO:main: REMOVED: [../SimTKmath/Optimizers/src/IpOpt/IpSymScaledMatrix.cpp] ../SimTKmath/Optimizers/src/IpOpt/IpSmartPtr.hpp#GetRawPtr:585:5, Memory error: Use of memory after it is freed
2020-07-08 08:16:29,197:INFO:main: REMOVED: [../SimTKmath/Optimizers/src/IpOpt/IpScaledMatrix.cpp] ../SimTKmath/Optimizers/src/IpOpt/IpSmartPtr.hpp#GetRawPtr:585:5, Memory error: Use of memory after it is freed
2020-07-08 08:16:29,197:INFO:main: TOTAL REPORTS: 1106
2020-07-08 08:16:29,197:INFO:main: TOTAL ADDED: 0
2020-07-08 08:16:29,197:INFO:main: TOTAL REMOVED: 2
2020-07-08 08:16:29,197:INFO:main: Warning: 2 differences in diagnostics.
2020-07-08 08:16:29,197:INFO:main: Error: Diffs found in strict mode (2).
2020-07-08 08:16:29,197:INFO:main: Diagnostic comparison complete (time: 6.23).
2020-07-08 08:16:29,197:INFO:main: Completed tests for project simbody (time: 1376.24).

These two warning are two FPs related to custom ref-counting pointers and the analyzer was able to figure out that the counters could not be 1 at some point.

[NoQ]

Data 👍

Maybe spend a few minutes remeasuring libsoundio more carefully, just in case? Also i really wish we had per-TU data of that kind, to see if any particular TUs have regressed significantly.

These two warning are two FPs related to custom ref-counting pointers and the analyzer was able to figure out that the counters could not be 1 at some point.

That's pretty amazing. I hate these false positives because there's often too little we can do.

[vsavchenko]

In D83286#2148787, @NoQ wrote:

Data 👍

Thanks 😊 These tables are already generated by a script and I plan to make it into a phabricator reporter, so it is easier to put all the data we need here.

Maybe spend a few minutes remeasuring libsoundio more carefully, just in case?

Sure, will do!

Also i really wish we had per-TU data of that kind, to see if any particular TUs have regressed significantly.

I think we even store all this information about the run, but it needs a bit of refactoring in CmpRuns.py to get it in a nice way. I think it's a good feature to put into my plan for the testing system.

[vsavchenko]

Maybe spend a few minutes remeasuring libsoundio more carefully, just in case?

Sure, will do!

It turns out that libsoundio has a problem similar to re2 and varies a lot in terms of the analysis time (probably we can even try to figure out some reasons behind it sometime in the future).
Here is the chart comparing 50 runs before and after:

[vsavchenko]

@xazax.hun You were interested in performance ⏫

These results here compare this patch together with D82445 against master.

[xazax.hun]

In D83286#2149912, @vsavchenko wrote:

@xazax.hun You were interested in performance ⏫

These results here compare this patch together with D82445 against master.

This is really great news, thanks!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 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)
 
+REGISTER_SET_FACTORY_WITH_PROGRAMSTATE(ClassSet, EquivalenceClass)
+REGISTER_MAP_WITH_PROGRAMSTATE(DisequalityMap, EquivalenceClass, ClassSet)
+
 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.
 ///
public:
   /// 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);
 
+  LLVM_NODISCARD static inline ProgramStateRef
+  markDisequal(BasicValueFactory &BV, RangeSet::Factory &F,
+               ProgramStateRef State, SymbolRef First, SymbolRef Second);
+  LLVM_NODISCARD static inline ProgramStateRef
+  markDisequal(BasicValueFactory &BV, RangeSet::Factory &F,
+               ProgramStateRef State, EquivalenceClass First,
+               EquivalenceClass Second);
+  LLVM_NODISCARD inline ProgramStateRef
+  markDisequal(BasicValueFactory &BV, RangeSet::Factory &F,
+               ProgramStateRef State, EquivalenceClass Other) const;
+  LLVM_NODISCARD static inline ClassSet
+  getDisequalClasses(ProgramStateRef State, SymbolRef Sym);
+  LLVM_NODISCARD inline ClassSet
+  getDisequalClasses(ProgramStateRef State) const;
+  LLVM_NODISCARD inline ClassSet
+  getDisequalClasses(DisequalityMapTy Map, ClassSet::Factory &Factory) const;
+
+  LLVM_NODISCARD static inline Optional<bool>
+  areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
+
   /// Check equivalence data for consistency.
   LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool
   isClassDataConsistent(ProgramStateRef State);
 
   LLVM_NODISCARD QualType getType() const {
     return getRepresentativeSymbol()->getType();
   }
 
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);
+  static inline void
+  addToDisequalityInfo(DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
+                       BasicValueFactory &BV, RangeSet::Factory &F,
+                       ProgramStateRef State, EquivalenceClass First,
+                       EquivalenceClass Second);
 
   /// This is a unique identifier of the class.
   uintptr_t ID;
 };
 
 //===----------------------------------------------------------------------===//
 //                             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));

 /// A little component aggregating all of the reasoning we have about
 /// the ranges of symbolic expressions.
 ///
 /// Even when we don't know the exact values of the operands, we still
 /// can get a pretty good estimate of the result's range.
 class SymbolicRangeInferrer
     : public SymExprVisitor<SymbolicRangeInferrer, RangeSet> {
 public:
+  template <class SourceType>
   static RangeSet inferRange(BasicValueFactory &BV, RangeSet::Factory &F,
-                             ProgramStateRef State, SymbolRef Sym) {
+                             ProgramStateRef State, SourceType Origin) {
     SymbolicRangeInferrer Inferrer(BV, F, State);
-    return Inferrer.infer(Sym);
+    return Inferrer.infer(Origin);
   }
 
   RangeSet VisitSymExpr(SymbolRef Sym) {
     // If we got to this function, the actual type of the symbolic
     // expression is not supported for advanced inference.
     // In this case, we simply backoff to the default "let's simply
     // infer the range from the expression's type".
     return infer(Sym->getType());
if (Optional<RangeSet> ConstraintBasedRange = intersect(
             // for A - B and the negated range set of B - A.
             getRangeForNegatedSub(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))
+    if (Optional<RangeSet> CmpRangeSet = getRangeForComparisonSymbol(Sym)) {
       return *CmpRangeSet;
+    }
 
     return Visit(Sym);
   }
 
+  RangeSet infer(EquivalenceClass Class) {
+    if (const RangeSet *AssociatedConstraint = getConstraint(State, Class))
+      return *AssociatedConstraint;
+
+    return infer(Class.getType());
+  }
+
   /// Infer range information solely from the type.
   RangeSet infer(QualType T) {
     // Lazily generate a new RangeSet representing all possible values for the
     // given symbol type.
     RangeSet Result(RangeFactory, ValueFactory.getMinValue(T),
                     ValueFactory.getMaxValue(T));
 
     // References are known to be non-zero.
private:
   }
 
   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) {
+    if (Optional<bool> AreEqual = EquivalenceClass::areEqual(
+            State, Equality->Left, Equality->Right)) {
+      if (*AreEqual == Equality->IsEquality) {
         return getTrueRange(Sym->getType());
       }
       return getFalseRange(Sym->getType());
     }
 
+    return llvm::None;
+  }
+
   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);
public:
   ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
 private:
   RangeSet::Factory F;
 
   RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
+  RangeSet getRange(ProgramStateRef State, EquivalenceClass Class);
 
   RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
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;
+    return EquivalenceClass::markDisequal(getBasicVals(), F, State, LHS, RHS);
   }
 
   ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS,
-                                SymbolRef RHS);
+                                SymbolRef RHS) {
+    return EquivalenceClass::merge(getBasicVals(), F, State, LHS, RHS);
+  }
+
+  LLVM_NODISCARD inline ProgramStateRef setConstraint(ProgramStateRef State,
+                                                      EquivalenceClass Class,
+                                                      RangeSet Constraint) {
+    ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+    ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>();
+
+    // Add new constraint.
+    Constraints = CF.add(Constraints, Class, Constraint);
+
+    // There is a chance that we might need to update constraints for the
+    // classes that are known to be disequal to Class.
+    //
+    // In order for this to be even possible, the new constraint should
+    // be simply a constant because we can't reason about range disequalities.
+    if (const llvm::APSInt *Point = Constraint.getConcreteValue())
+      for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
+        RangeSet UpdatedConstraint =
+            getRange(State, DisequalClass).Delete(getBasicVals(), F, *Point);
+        Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint);
+      }
+
+    return State->set<ConstraintRange>(Constraints);
+  }
+
+  LLVM_NODISCARD inline ProgramStateRef
+  setConstraint(ProgramStateRef State, SymbolRef Sym, RangeSet Constraint) {
+    return setConstraint(State, EquivalenceClass::find(State, Sym), Constraint);
+  }
 };
 
 } // end anonymous namespace
 
 std::unique_ptr<ConstraintManager>
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr,
                                    ExprEngine *Eng) {
   return std::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
if (Optional<RangeSet> NewClassConstraint =
     // 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>();
+  ClassMapTy::Factory &CMF = State->get_context<ClassMap>();
 
   ClassMembersTy Members = State->get<ClassMembers>();
   ClassMembersTy::Factory &MF = State->get_context<ClassMembers>();
 
+  DisequalityMapTy DisequalityInfo = State->get<DisequalityMap>();
+  DisequalityMapTy::Factory &DF = State->get_context<DisequalityMap>();
+
+  ClassSet::Factory &CF = State->get_context<ClassSet>();
   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);
+    Classes = CMF.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
+  // 4. Update disequality relations
+  ClassSet DisequalToOther = Other.getDisequalClasses(DisequalityInfo, CF);
+  if (!DisequalToOther.isEmpty()) {
+    ClassSet DisequalToThis = getDisequalClasses(DisequalityInfo, CF);
+    DisequalityInfo = DF.remove(DisequalityInfo, Other);
+
+    for (EquivalenceClass DisequalClass : DisequalToOther) {
+      DisequalToThis = CF.add(DisequalToThis, DisequalClass);
+
+      // Disequality is a symmetric relation meaning that if
+      // DisequalToOther not null then the set for DisequalClass is not
+      // empty and has at least Other.
+      ClassSet OriginalSetLinkedToOther =
+          *DisequalityInfo.lookup(DisequalClass);
+
+      // Other will be eliminated and we should replace it with the bigger
+      // united class.
+      ClassSet NewSet = CF.remove(OriginalSetLinkedToOther, Other);
+      NewSet = CF.add(NewSet, *this);
+
+      DisequalityInfo = DF.add(DisequalityInfo, DisequalClass, NewSet);
+    }
+
+    DisequalityInfo = DF.add(DisequalityInfo, *this, DisequalToThis);
+    State = State->set<DisequalityMap>(DisequalityInfo);
+  }
+
+  // 5. Update the state
   State = State->set<ClassMap>(Classes);
   State = State->set<ClassMembers>(Members);
 
   return State;
 }
 
 inline SymbolSet::Factory &
 EquivalenceClass::getMembersFactory(ProgramStateRef State) {
bool EquivalenceClass::isTrivial(ProgramStateRef State) {
   return State->get<ClassMembers>(*this) == nullptr;
 }
 
 bool EquivalenceClass::isTriviallyDead(ProgramStateRef State,
                                        SymbolReaper &Reaper) {
   return isTrivial(State) && Reaper.isDead(getRepresentativeSymbol());
 }
 
+inline ProgramStateRef EquivalenceClass::markDisequal(BasicValueFactory &VF,
+                                                      RangeSet::Factory &RF,
+                                                      ProgramStateRef State,
+                                                      SymbolRef First,
+                                                      SymbolRef Second) {
+  return markDisequal(VF, RF, State, find(State, First), find(State, Second));
+}
+
+inline ProgramStateRef EquivalenceClass::markDisequal(BasicValueFactory &VF,
+                                                      RangeSet::Factory &RF,
+                                                      ProgramStateRef State,
+                                                      EquivalenceClass First,
+                                                      EquivalenceClass Second) {
+  return First.markDisequal(VF, RF, State, Second);
+}
+
+inline ProgramStateRef
+EquivalenceClass::markDisequal(BasicValueFactory &VF, RangeSet::Factory &RF,
+                               ProgramStateRef State,
+                               EquivalenceClass Other) const {
+  // If we know that two classes are equal, we can only produce an infeasible
+  // state.
+  if (*this == Other) {
+    return nullptr;
+  }
+
+  DisequalityMapTy DisequalityInfo = State->get<DisequalityMap>();
+  ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+
+  // Disequality is a symmetric relation, so if we mark A as disequal to B,
+  // we should also mark B as disequalt to A.
+  addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, *this,
+                       Other);
+  addToDisequalityInfo(DisequalityInfo, Constraints, VF, RF, State, Other,
+                       *this);
+
+  State = State->set<DisequalityMap>(DisequalityInfo);
+  State = State->set<ConstraintRange>(Constraints);
+
+  return State;
+}
+
+inline void EquivalenceClass::addToDisequalityInfo(
+    DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
+    BasicValueFactory &VF, RangeSet::Factory &RF, ProgramStateRef State,
+    EquivalenceClass First, EquivalenceClass Second) {
+
+  // 1. Get all of the required factories.
+  DisequalityMapTy::Factory &F = State->get_context<DisequalityMap>();
+  ClassSet::Factory &CF = State->get_context<ClassSet>();
+  ConstraintRangeTy::Factory &CRF = State->get_context<ConstraintRange>();
+
+  // 2. Add Second to the set of classes disequal to First.
+  const ClassSet *CurrentSet = Info.lookup(First);
+  ClassSet NewSet = CurrentSet ? *CurrentSet : CF.getEmptySet();
+  NewSet = CF.add(NewSet, Second);
+
+  Info = F.add(Info, First, NewSet);
+
+  // 3. If Second is known to be a constant, we can delete this point
+  //    from the constraint asociated with First.
+  //
+  //    So, if Second == 10, it means that First != 10.
+  //    At the same time, the same logic does not apply to ranges.
+  if (const RangeSet *SecondConstraint = Constraints.lookup(Second))
+    if (const llvm::APSInt *Point = SecondConstraint->getConcreteValue()) {
+
+      RangeSet FirstConstraint = SymbolicRangeInferrer::inferRange(
+          VF, RF, State, First.getRepresentativeSymbol());
+
+      FirstConstraint = FirstConstraint.Delete(VF, RF, *Point);
+      Constraints = CRF.add(Constraints, First, FirstConstraint);
+    }
+}
+
+inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
+                                                 SymbolRef FirstSym,
+                                                 SymbolRef SecondSym) {
+  EquivalenceClass First = find(State, FirstSym);
+  EquivalenceClass Second = find(State, SecondSym);
+
+  // The same equivalence class => symbols are equal.
+  if (First == Second)
+    return true;
+
+  // Let's check if we know anything about these two classes being not equal to
+  // each other.
+  ClassSet DisequalToFirst = First.getDisequalClasses(State);
+  if (DisequalToFirst.contains(Second))
+    return false;
+
+  // It is not clear.
+  return llvm::None;
+}
+
+inline ClassSet EquivalenceClass::getDisequalClasses(ProgramStateRef State,
+                                                     SymbolRef Sym) {
+  return find(State, Sym).getDisequalClasses(State);
+}
+
+inline ClassSet
+EquivalenceClass::getDisequalClasses(ProgramStateRef State) const {
+  return getDisequalClasses(State->get<DisequalityMap>(),
+                            State->get_context<ClassSet>());
+}
+
+inline ClassSet
+EquivalenceClass::getDisequalClasses(DisequalityMapTy Map,
+                                     ClassSet::Factory &Factory) const {
+  if (const ClassSet *DisequalClasses = Map.lookup(*this))
+    return *DisequalClasses;
+
+  return Factory.getEmptySet();
+}
+
 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;
     }
   }
 
+  DisequalityMapTy Disequalities = State->get<DisequalityMap>();
+  for (std::pair<EquivalenceClass, ClassSet> DisequalityInfo : Disequalities) {
+    EquivalenceClass Class = DisequalityInfo.first;
+    ClassSet DisequalClasses = DisequalityInfo.second;
+
+    // There is no use in keeping empty sets in the map.
+    if (DisequalClasses.isEmpty())
+      return false;
+
+    // Disequality is symmetrical, i.e. for every Class A and B that A != B,
+    // B != A should also be true.
+    for (EquivalenceClass DisequalClass : DisequalClasses) {
+      const ClassSet *DisequalToDisequalClasses =
+          Disequalities.lookup(DisequalClass);
+
+      // It should be a set of at least one element: Class
+      if (!DisequalToDisequalClasses ||
+          !DisequalToDisequalClasses->contains(Class))
+        return false;
+    }
+  }
+
   return true;
 }
 
 //===----------------------------------------------------------------------===//
 //                    RangeConstraintManager implementation
 //===----------------------------------------------------------------------===//
 
 bool RangeConstraintManager::canReasonAbout(SVal X) const {
RangeConstraintManager::removeDeadBindings(ProgramStateRef State,
   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>();
 
+  DisequalityMapTy Disequalities = State->get<DisequalityMap>();
+  DisequalityMapTy::Factory &DisequalityFactory =
+      State->get_context<DisequalityMap>();
+  ClassSet::Factory &ClassSetFactory = State->get_context<ClassSet>();
+
   bool ClassMapChanged = false;
   bool MembersMapChanged = false;
   bool ConstraintMapChanged = false;
+  bool DisequalitiesChanged = false;
+
+  auto removeDeadClass = [&](EquivalenceClass Class) {
+    // Remove associated constraint ranges.
+    Constraints = ConstraintFactory.remove(Constraints, Class);
+    ConstraintMapChanged = true;
+
+    // Update disequality information to not hold any information on the
+    // removed class.
+    ClassSet DisequalClasses =
+        Class.getDisequalClasses(Disequalities, ClassSetFactory);
+    if (!DisequalClasses.isEmpty()) {
+      for (EquivalenceClass DisequalClass : DisequalClasses) {
+        ClassSet DisequalToDisequalSet =
+            DisequalClass.getDisequalClasses(Disequalities, ClassSetFactory);
+        // DisequalToDisequalSet is guaranteed to be non-empty for consistent
+        // disequality info.
+        assert(!DisequalToDisequalSet.isEmpty());
+        ClassSet NewSet = ClassSetFactory.remove(DisequalToDisequalSet, Class);
+
+        // No need in keeping an empty set.
+        if (NewSet.isEmpty()) {
+          Disequalities =
+              DisequalityFactory.remove(Disequalities, DisequalClass);
+        } else {
+          Disequalities =
+              DisequalityFactory.add(Disequalities, DisequalClass, NewSet);
+        }
+      }
+      // Remove the data for the class
+      Disequalities = DisequalityFactory.remove(Disequalities, Class);
+      DisequalitiesChanged = true;
+    }
+  };
 
   // 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;
+      removeDeadClass(Class);
     }
   }
 
   // 2. We don't need to track classes for dead symbols.
   for (std::pair<SymbolRef, EquivalenceClass> SymbolClassPair : Map) {
     SymbolRef Sym = SymbolClassPair.first;
 
     if (SymReaper.isDead(Sym)) {
       ClassMapChanged = true;
       NewMap = ClassFactory.remove(NewMap, Sym);
     }
   }
 
   // 3. Remove dead members from classes and remove dead non-trivial classes
   //    and their constraints.
   for (std::pair<EquivalenceClass, SymbolSet> ClassMembersPair :
        ClassMembersMap) {
+    EquivalenceClass Class = ClassMembersPair.first;
     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);
+      NewClassMembersMap = EMFactory.remove(NewClassMembersMap, Class);
 
       // ...and remove all of its constraints.
-      Constraints =
-          ConstraintFactory.remove(Constraints, ClassMembersPair.first);
-      ConstraintMapChanged = true;
+      removeDeadClass(Class);
     } else {
       // We need to change the members associated with the class.
-      NewClassMembersMap = EMFactory.add(NewClassMembersMap,
-                                         ClassMembersPair.first, LiveMembers);
+      NewClassMembersMap =
+          EMFactory.add(NewClassMembersMap, Class, 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);
 
+  if (DisequalitiesChanged)
+    State = State->set<DisequalityMap>(Disequalities);
+
   assert(EquivalenceClass::isClassDataConsistent(State));
 
   return State;
 }
 
 RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
                                           SymbolRef Sym) {
   return SymbolicRangeInferrer::inferRange(getBasicVals(), F, State, Sym);
 }
 
+RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
+                                          EquivalenceClass Class) {
+  return SymbolicRangeInferrer::inferRange(getBasicVals(), F, State, Class);
+}
+
 //===------------------------------------------------------------------------===
 // assumeSymX methods: protected interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
 // and (x, y) for open ranges. These ranges are modular, corresponding with
 // a common treatment of C integer overflow. This means that these methods
 // do not have to worry about overflow; RangeSet::Intersect can handle such a
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 : 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>();

clang/test/Analysis/equality_tracking.c

void zeroImpliesEquality(int a, int b) {
   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}}
+  clang_analyzer_eval(b == a);       // expected-warning{{FALSE}}
+  clang_analyzer_eval(b != a);       // expected-warning{{TRUE}}
 }
 
 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}}
+  clang_analyzer_eval(b == a);       // expected-warning{{FALSE}}
+  clang_analyzer_eval(b != a);       // expected-warning{{TRUE}}
 }
 
 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;
   }
if (b == d) {
       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}}
+      clang_analyzer_eval(a != 42); // expected-warning{{TRUE}}
     }
   }
 }
 
 void testIntersection(int a, int b, int c) {
   if (a < 42 && b > 15 && c >= 25 && c <= 30) {
     if (a != b)
       return;
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}}
+      clang_analyzer_eval(a != NULL); // expected-warning{{TRUE}}
+    }
+  }
+}
+
+void testDisequalitiesAfter(int a, int b, int c) {
+  if (a >= 10 && b <= 42) {
+    if (a == b && c == 15 && c != a) {
+      clang_analyzer_eval(b != c);  // expected-warning{{TRUE}}
+      clang_analyzer_eval(a != 15); // expected-warning{{TRUE}}
+      clang_analyzer_eval(b != 15); // expected-warning{{TRUE}}
+      clang_analyzer_eval(b >= 10); // expected-warning{{TRUE}}
+      clang_analyzer_eval(a <= 42); // expected-warning{{TRUE}}
+    }
+  }
+}
+
+void testDisequalitiesBefore(int a, int b, int c) {
+  if (a >= 10 && b <= 42 && c == 15) {
+    if (a == b && c != a) {
+      clang_analyzer_eval(b != c);  // expected-warning{{TRUE}}
+      clang_analyzer_eval(a != 15); // expected-warning{{TRUE}}
+      clang_analyzer_eval(b != 15); // expected-warning{{TRUE}}
+      clang_analyzer_eval(b >= 10); // expected-warning{{TRUE}}
+      clang_analyzer_eval(a <= 42); // expected-warning{{TRUE}}
     }
   }
 }
 
 void avoidInfeasibleConstraintsForClasses(int a, int b) {
   if (a >= 0 && a <= 10 && b >= 20 && b <= 50) {
     if ((b - a) == 0) {
       clang_analyzer_warnIfReached(); // no warning

clang/test/Analysis/mutually_exclusive_null_fp.cpp

+// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s
+
+// rdar://problem/56586853
+// expected-no-diagnostics
+
+struct Data {
+  int x;
+  Data *data;
+};
+
+int compare(Data &a, Data &b) {
+  Data *aData = a.data;
+  Data *bData = b.data;
+
+  // Covers the cases where both pointers are null as well as both pointing to the same buffer.
+  if (aData == bData)
+    return 0;
+
+  if (aData && !bData)
+    return 1;
+
+  if (!aData && bData)
+    return -1;
+
+  return compare(*aData, *bData); // no-warning
+}