[Analyzer][solver] Fix equivalence class invariant violation in removeDeadBindings

[martong]

Summary

There is an invariant in the range based solver for equivalence classes.
We don't store class->member associations for trivial classes in the
state (ClassMembers). This means any SymbolSet stored in ClassMembers
must have at least two members. This invariant is violated in
removeDeadBindings, because we remove a class from ClassMembers only
once it became empty.

Fixing this invariant violation implies that we must prepare for element
removals from an equivalence class. An element removal might result in
downgrading a non-trivial class to trivial, also the representative
symbol might be changed. If the representative symbol has changed then
we have to re-key constraints and the disequality info.

[martong]

Note1: This issue is not related to and does not fix https://bugs.llvm.org/show_bug.cgi?id=51109
Note2: I am about to measure any performance penalty induced by the extra bookkeeping we must do.

[vsavchenko]

Thanks for working on it, but it is a quite large change that I don't get the motivation for (it doesn't even fix the recently found bug).

Summary explains what the patch does, but for why it is done, it talks about an invariant that is not specified anywhere in the code. The invariant you are talking about in the summary is simply not true and was never intended to be true.

When I was implementing it, trivial class is a symbol that was never ever equal to anything else. The moment we make merge something into it, it stops being trivial, forever! Representative is an implementation detail and shouldn't be required to represent the actual information. What I'm saying is that representative can be long gone, but the class can still hold. If we use representative symbol for something other than its pointer or type after it's gone, the mistake is using representative in the first place, not the motivation to make it more complex and change representatives.

[martong]

Thanks for taking your time to take a look. And I accept your statements. Nevertheless, let me explain my motivation.

I thought that a class is trivial if it has only one member. And it seemed perfectly logical to not store equivalence classes with one member. I.e a equals to a does not hold any meaningful information it just takes precious memory. When we add a new constraint we take careful steps to avoid adding a new class with one member. However, when remove dead kicks in, suddenly we end up having classes stored with one member, which is a somewhat inconsistent design IMHO. Perhaps some better documentation could have helped.

[vsavchenko]

In D106136#2883100, @martong wrote:

Thanks for taking your time to take a look. And I accept your statements. Nevertheless, let me explain my motivation.

I thought that a class is trivial if it has only one member. And it seemed perfectly logical to not store equivalence classes with one member. I.e a equals to a does not hold any meaningful information it just takes precious memory. When we add a new constraint we take careful steps to avoid adding a new class with one member. However, when remove dead kicks in, suddenly we end up having classes stored with one member, which is a somewhat inconsistent design IMHO. Perhaps some better documentation could have helped.

Representative symbol gives its equivalence class an ID. We use this ID for everything, for comparing and for mapping. Since we live in a persistent world, we can't just change this ID at some point, it will basically mean that we want to replace a class with another class. So, all maps where this class participated (constraints, class, members, disequality) should remove the old class and add the new class. This is a huge burden. You need to carefully do all this, and bloat existing data structures.

Trivial class is an optimization for the vast majority of symbols that never get into any classes. We still need to associate constraints with those. This is where implicit Symbol to Class conversion comes in handy.

Now let's imagine that something else is merged into it. We are obliged to officially map the symbol to its class, and the class to its members. When this happens, it goes into the data structure FOREVER. And when in the future, with only one member, instead of keeping something that we already have from other versions of the data structure, you decide to remove the item from the class map, you actually use more memory when it was there! This is how persistent data structures work, different versions of the same data structure share data. And I'm not even talking here about the fact that you now need to replace the class with one ID with the class with another ID in every relationship.

You can probably measure memory footprint in your example and see it for yourself.

[martong]

In D106136#2883707, @vsavchenko wrote:

In D106136#2883100, @martong wrote:

Thanks for taking your time to take a look. And I accept your statements. Nevertheless, let me explain my motivation.

I thought that a class is trivial if it has only one member. And it seemed perfectly logical to not store equivalence classes with one member. I.e a equals to a does not hold any meaningful information it just takes precious memory. When we add a new constraint we take careful steps to avoid adding a new class with one member. However, when remove dead kicks in, suddenly we end up having classes stored with one member, which is a somewhat inconsistent design IMHO. Perhaps some better documentation could have helped.

Representative symbol gives its equivalence class an ID. We use this ID for everything, for comparing and for mapping. Since we live in a persistent world, we can't just change this ID at some point, it will basically mean that we want to replace a class with another class. So, all maps where this class participated (constraints, class, members, disequality) should remove the old class and add the new class. This is a huge burden. You need to carefully do all this, and bloat existing data structures.

Trivial class is an optimization for the vast majority of symbols that never get into any classes. We still need to associate constraints with those. This is where implicit Symbol to Class conversion comes in handy.

Now let's imagine that something else is merged into it. We are obliged to officially map the symbol to its class, and the class to its members. When this happens, it goes into the data structure FOREVER. And when in the future, with only one member, instead of keeping something that we already have from other versions of the data structure, you decide to remove the item from the class map, you actually use more memory when it was there! This is how persistent data structures work, different versions of the same data structure share data. And I'm not even talking here about the fact that you now need to replace the class with one ID with the class with another ID in every relationship.

You can probably measure memory footprint in your example and see it for yourself.

Yeah, makes sense. Thanks for taking more time for further explanations. Still, IMHO, the definition of a trivial class needs a clear written documentation in the code itself, so other developers can easier understand and maintain this code. I am going to create an NFC patch that summarizes this discussion in a comment attached to the isTrivial function.

[vsavchenko]

In D106136#2889610, @martong wrote:

In D106136#2883707, @vsavchenko wrote:

In D106136#2883100, @martong wrote:

Thanks for taking your time to take a look. And I accept your statements. Nevertheless, let me explain my motivation.

I thought that a class is trivial if it has only one member. And it seemed perfectly logical to not store equivalence classes with one member. I.e a equals to a does not hold any meaningful information it just takes precious memory. When we add a new constraint we take careful steps to avoid adding a new class with one member. However, when remove dead kicks in, suddenly we end up having classes stored with one member, which is a somewhat inconsistent design IMHO. Perhaps some better documentation could have helped.

Representative symbol gives its equivalence class an ID. We use this ID for everything, for comparing and for mapping. Since we live in a persistent world, we can't just change this ID at some point, it will basically mean that we want to replace a class with another class. So, all maps where this class participated (constraints, class, members, disequality) should remove the old class and add the new class. This is a huge burden. You need to carefully do all this, and bloat existing data structures.

Trivial class is an optimization for the vast majority of symbols that never get into any classes. We still need to associate constraints with those. This is where implicit Symbol to Class conversion comes in handy.

Now let's imagine that something else is merged into it. We are obliged to officially map the symbol to its class, and the class to its members. When this happens, it goes into the data structure FOREVER. And when in the future, with only one member, instead of keeping something that we already have from other versions of the data structure, you decide to remove the item from the class map, you actually use more memory when it was there! This is how persistent data structures work, different versions of the same data structure share data. And I'm not even talking here about the fact that you now need to replace the class with one ID with the class with another ID in every relationship.

You can probably measure memory footprint in your example and see it for yourself.

Yeah, makes sense. Thanks for taking more time for further explanations. Still, IMHO, the definition of a trivial class needs a clear written documentation in the code itself, so other developers can easier understand and maintain this code. I am going to create an NFC patch that summarizes this discussion in a comment attached to the isTrivial function.

That's a great idea! Thanks!

[martong]

Here it is: https://reviews.llvm.org/D106370

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

public:
   LLVM_NODISCARD static inline Optional<bool>
   areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
 
   /// Iterate over all symbols and try to simplify them.
   LLVM_NODISCARD ProgramStateRef simplify(SValBuilder &SVB,
                                           RangeSet::Factory &F,
                                           ProgramStateRef State);
 
+  /// Associate new members to the class. This may result in changing the
+  /// representative symbol or downgrading from non-trivial to trivial.
+  LLVM_NODISCARD ProgramStateRef setNewMembers(SymbolSet NewMembers,
+                                               ProgramStateRef State);
+
+  // Remove an already empty class amongs the constraints and the disequality
+  // info.
+  LLVM_NODISCARD static ProgramStateRef removeEmpty(ProgramStateRef State,
+                                                    EquivalenceClass Class);
+
   void dumpToStream(ProgramStateRef State, raw_ostream &os) const;
   LLVM_DUMP_METHOD void dump(ProgramStateRef State) const {
     dumpToStream(State, llvm::errs());
   }
 
   /// Check equivalence data for consistency.
   LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool
   isClassDataConsistent(ProgramStateRef State);
private:
   inline ProgramStateRef mergeImpl(RangeSet::Factory &F, ProgramStateRef State,
                                    SymbolSet Members, EquivalenceClass Other,
                                    SymbolSet OtherMembers);
   static inline bool
   addToDisequalityInfo(DisequalityMapTy &Info, ConstraintRangeTy &Constraints,
                        RangeSet::Factory &F, ProgramStateRef State,
                        EquivalenceClass First, EquivalenceClass Second);
 
+  /// Returns a new representative symbol if the old representative symbol is
+  /// not amongst the new members.
+  Optional<SymbolRef> isRepresentativeSymbolChanged(SymbolSet NewMembers,
+                                                    ProgramStateRef State);
+
+  // Re-key constraints with Old->New.
+  LLVM_NODISCARD static ProgramStateRef
+  replaceConstraints(ProgramStateRef State, const SymbolRef Old,
+                     const SymbolRef New);
+
+  // Re-key disequality info with Old->New.
+  LLVM_NODISCARD static ProgramStateRef
+  replaceDisequalityInfo(ProgramStateRef State, const SymbolRef Old,
+                         const SymbolRef New);
+
   /// This is a unique identifier of the class.
   uintptr_t ID;
 };
 
 //===----------------------------------------------------------------------===//
 //                             Constraint functions
 //===----------------------------------------------------------------------===//
 
if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
       State = merge(F, State, ClassOfSimplifiedSym);
       if (!State)
         return nullptr;
     }
   }
   return State;
 }
 
+LLVM_NODISCARD ProgramStateRef EquivalenceClass::replaceConstraints(
+    ProgramStateRef State, const SymbolRef Old, const SymbolRef New) {
+  assert(Old != New);
+
+  ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+  ConstraintRangeTy::Factory &ConstraintFactory =
+      State->get_context<ConstraintRange>();
+  if (const RangeSet *R = getConstraint(State, Old)) {
+    Constraints = ConstraintFactory.remove(Constraints, Old);
+    Constraints = ConstraintFactory.add(Constraints, New, *R);
+  }
+  State = State->set<ConstraintRange>(Constraints);
+  return State;
+}
+
+LLVM_NODISCARD ProgramStateRef EquivalenceClass::replaceDisequalityInfo(
+    ProgramStateRef State, const SymbolRef Old, const SymbolRef New) {
+  assert(Old != New);
+
+  ClassSet::Factory &CF = State->get_context<ClassSet>();
+  DisequalityMapTy::Factory &DF = State->get_context<DisequalityMap>();
+
+  DisequalityMapTy DisequalityInfo = State->get<DisequalityMap>();
+  ClassSet DisequalToOld =
+      EquivalenceClass(Old).getDisequalClasses(DisequalityInfo, CF);
+  if (!DisequalToOld.isEmpty()) {
+    DisequalityInfo = DF.remove(DisequalityInfo, Old);
+    DisequalityInfo = DF.add(DisequalityInfo, New, DisequalToOld);
+    for (EquivalenceClass DisEqClass : DisequalToOld) {
+      ClassSet ReverseSet = DisEqClass.getDisequalClasses(DisequalityInfo, CF);
+      if (!ReverseSet.isEmpty()) {
+        ReverseSet = CF.remove(ReverseSet, Old);
+        ReverseSet = CF.add(ReverseSet, New);
+        DisequalityInfo = DF.add(DisequalityInfo, DisEqClass, ReverseSet);
+      }
+    }
+    State = State->set<DisequalityMap>(DisequalityInfo);
+  }
+  return State;
+}
+
+Optional<SymbolRef>
+EquivalenceClass::isRepresentativeSymbolChanged(SymbolSet NewMembers,
+                                                ProgramStateRef State) {
+  assert(!NewMembers.isEmpty());
+  SymbolRef CurrentRepr = this->getRepresentativeSymbol();
+  // Existing representative is still good.
+  if (NewMembers.contains(CurrentRepr))
+    return None;
+  return *NewMembers.begin();
+}
+
+LLVM_NODISCARD ProgramStateRef
+EquivalenceClass::removeEmpty(ProgramStateRef State, EquivalenceClass Class) {
+  assert(State->get<ClassMembers>(Class) == nullptr);
+
+  ConstraintRangeTy::Factory &ConstraintFactory =
+      State->get_context<ConstraintRange>();
+  ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+
+  DisequalityMapTy Disequalities = State->get<DisequalityMap>();
+  DisequalityMapTy::Factory &DisequalityFactory =
+      State->get_context<DisequalityMap>();
+  ClassSet::Factory &ClassSetFactory = State->get_context<ClassSet>();
+
+  // Remove associated constraint ranges.
+  Constraints = ConstraintFactory.remove(Constraints, Class);
+
+  // 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);
+  }
+  State = State->set<ConstraintRange>(Constraints);
+  State = State->set<DisequalityMap>(Disequalities);
+  return State;
+}
+
+LLVM_NODISCARD ProgramStateRef
+EquivalenceClass::setNewMembers(SymbolSet NewMembers, ProgramStateRef State) {
+
+  assert(!this->isTrivial(State));
+  SymbolSet OldMembers = this->getClassMembers(State);
+  // Must have at least two members currently.
+  assert(OldMembers.getHeight() > 1);
+
+  ClassMembersTy::Factory &EMFactory = State->get_context<ClassMembers>();
+  ClassMapTy::Factory &CMF = State->get_context<ClassMap>();
+
+  ClassMembersTy ClassMembersMap = State->get<ClassMembers>();
+  ClassMapTy Classes = State->get<ClassMap>();
+
+  // Downgrade to trivial.
+  if (NewMembers.getHeight() <= 1) {
+    // Remove from ClassMap and ClassMembers.
+    ClassMembersMap = EMFactory.remove(ClassMembersMap, *this);
+    // Remove Old->Class relations.
+    for (SymbolRef Old : OldMembers)
+      Classes = CMF.remove(Classes, Old);
+  } else { // The Class is still nontrivial.
+    // Update fwd/backwd relations in ClassMap/ClassMembers.
+    ClassMembersMap = EMFactory.add(ClassMembersMap, *this, NewMembers);
+    // Remove Old->Class relations.
+    for (SymbolRef Old : OldMembers)
+      Classes = CMF.remove(Classes, Old);
+    // Add New->Class relations.
+    for (SymbolRef New : NewMembers)
+      Classes = CMF.add(Classes, New, *this);
+  }
+
+  State = State->set<ClassMap>(Classes);
+  State = State->set<ClassMembers>(ClassMembersMap);
+
+  if (NewMembers.getHeight() == 0) {
+    State = removeEmpty(State, *this);
+  } else if (Optional<SymbolRef> NewReprSym =
+                 this->isRepresentativeSymbolChanged(NewMembers, State)) {
+    SymbolRef OldReprSym = this->getRepresentativeSymbol();
+    State = replaceConstraints(State, OldReprSym, *NewReprSym);
+    State = replaceDisequalityInfo(State, OldReprSym, *NewReprSym);
+  }
+
+  return State;
+}
+
 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) {
+    // A class should have at least two members.
+    // A tree with height 0 has 0 element. A tree with height 1 has exactly 1
+    // element. A tree with height 2 can have 2 or 3 elements.
+    if (ClassMembersPair.second.getHeight() <= 1)
+      return false;
     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;
     }

 //===----------------------------------------------------------------------===//
 
 /// 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) {
   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>();
-
   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.
-      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);
+      State = EquivalenceClass::removeEmpty(State, Class);
     }
   }
 
   // 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;
 
+    assert(ClassMembersPair.second.getHeight() > 1);
     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, Class);
-
-      // ...and remove all of its constraints.
-      removeDeadClass(Class);
-    } else {
-      // We need to change the members associated with the class.
-      NewClassMembersMap =
-          EMFactory.add(NewClassMembersMap, Class, LiveMembers);
-    }
+    State = Class.setNewMembers(LiveMembers, State);
   }
 
-  // 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(F, State, Sym);

clang/test/Analysis/equivalence-classes-and-remove-dead.c

+// RUN: %clang_analyze_cc1 -verify %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false
+
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   2>&1 | FileCheck %s
+
+void clang_analyzer_eval(int);
+void clang_analyzer_warnIfReached();
+void clang_analyzer_printState();
+
+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}}
+
+    clang_analyzer_printState(); // At this point a, b, c are alive
+    // CHECK:      "constraints": [
+    // CHECK-NEXT:   { "symbol": "reg_$0<int a>", "range": "{ [16, 41] }" },
+    // CHECK-NEXT:   { "symbol": "reg_$1<int b>", "range": "{ [16, 41] }" },
+    // CHECK-NEXT:   { "symbol": "reg_$2<int c>", "range": "{ [25, 30] }" },
+    // CHECK-NEXT:   { "symbol": "(reg_$0<int a>) != (reg_$1<int b>)", "range": "{ [0, 0] }" }
+    // CHECK-NEXT: ],
+    // CHECK-NEXT: "equivalence_classes": [
+    // CHECK-NEXT:   [ "reg_$0<int a>", "reg_$1<int b>" ]
+    // CHECK-NEXT: ],
+    // CHECK-NEXT: "disequality_info": null,
+
+    if (c == b) {
+      // Also, it should be noted that c is dead at this point, but the
+      // constraint initially associated with c is still around.
+      clang_analyzer_printState(); // a, b are alive
+      // CHECK:      "constraints": [
+      // CHECK-NEXT:   { "symbol": "reg_$0<int a>", "range": "{ [25, 30] }" },
+      // CHECK-NEXT:   { "symbol": "reg_$1<int b>", "range": "{ [25, 30] }" },
+      // CHECK-NEXT:   { "symbol": "(reg_$0<int a>) != (reg_$1<int b>)", "range": "{ [0, 0] }" }
+      // CHECK-NEXT: ],
+      // CHECK-NEXT: "equivalence_classes": [
+      // CHECK-NEXT:   [ "reg_$0<int a>", "reg_$1<int b>" ]
+      // CHECK-NEXT: ],
+      // CHECK-NEXT: "disequality_info": null,
+      clang_analyzer_eval(a >= 25 && a <= 30); // expected-warning{{TRUE}}
+
+      clang_analyzer_printState(); // only b is alive
+      // CHECK:       "constraints": [
+      // CHECK-NEXT:    { "symbol": "reg_$1<int b>", "range": "{ [25, 30] }" }
+      // CHECK-NEXT:  ],
+      // CHECK-NEXT:  "equivalence_classes": null,
+      // CHECK-NEXT:  "disequality_info": null,
+      clang_analyzer_eval(b >= 25 && b <= 30); // expected-warning{{TRUE}}
+
+      clang_analyzer_printState(); // all died
+      // CHECK:       "constraints": null,
+      // CHECK-NEXT:  "equivalence_classes": null,
+      // CHECK-NEXT:  "disequality_info": null,
+    }
+  }
+}