[analyzer][solver][NFC] Refactor how we detect (dis)equalities

[vsavchenko]

Summary

This patch simplifies the way we deal with (dis)equalities.
Due to the symmetry between constraint handler and range inferrer,
we can have very similar implementations of logic handling
questions about (dis)equality and assumptions involving (dis)equality.

It also helps us to remove one more visitor, and removes uncertainty
that we got all the right places to put trackNE and trackEQ.

[martong]

LGTM!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

687

This is no longer a structure.

clang/test/Analysis/equality_tracking.c

223–235

Thanks, for the new test cases!

[vsavchenko]

Fix comments

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

687

Good catch!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

LLVM_NODISCARD ProgramStateRef setConstraints(ProgramStateRef State,
                                               ConstraintRangeTy Constraints) {
   return State->set<ConstraintRange>(Constraints);
 }
 
 //===----------------------------------------------------------------------===//
 //                       Equality/diseqiality abstraction
 //===----------------------------------------------------------------------===//
 
-/// A small helper structure representing symbolic equality.
+/// A small helper function for detecting symbolic (dis)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 (!Int.isNullValue() || !Adjustment.isNullValue())
-      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;
-      }
-    }
-  };
-};
+/// whether it's equality/diseqiality or not.
+///
+/// \returns true if assuming this Sym to be true means equality of operands
+///          false if it means disequality of operands
+///          None otherwise
+Optional<bool> meansEquality(const SymSymExpr *Sym) {
+    return false;
+    return true;
+    return false;
 
 //===----------------------------------------------------------------------===//
 //                            Intersection functions
 //===----------------------------------------------------------------------===//
 
 template <class SecondTy, class... RestTy>
 LLVM_NODISCARD inline RangeSet intersect(RangeSet::Factory &F, RangeSet Head,
                                          SecondTy Second, RestTy... Tail);
RangeSet VisitSymIntExpr(const SymIntExpr *Sym) {
     return VisitBinaryOperator(Sym);
   }
 
   RangeSet VisitIntSymExpr(const IntSymExpr *Sym) {
     return VisitBinaryOperator(Sym);
   }
 
   RangeSet VisitSymSymExpr(const SymSymExpr *Sym) {
-    return VisitBinaryOperator(Sym);
+    return intersect(
+        RangeFactory,
+        // If Sym is (dis)equality, we might have some information
+        // on that in our equality classes data structure.
+        getRangeForEqualities(Sym),
+        // And we should always check what we can get from the operands.
+        VisitBinaryOperator(Sym));
   }
 
 private:
   SymbolicRangeInferrer(RangeSet::Factory &F, ProgramStateRef S)
       : ValueFactory(F.getValueFactory()), RangeFactory(F), State(S) {}
 
   /// Infer range information from the given integer constant.
   ///
return intersect(
         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.
         getRangeForNegatedSub(Sym),
-        // If Sym is (dis)equality, we might have some information on that
-        // in our equality classes data structure.
-        getRangeForEqualities(Sym),
         // If Sym is a comparison expression (except <=>),
         // find any other comparisons with the same operands.
         // See function description.
         getRangeForComparisonSymbol(Sym),
         // Apart from the Sym itself, we can infer quite a lot if we look
         // into subexpressions of Sym.
         Visit(Sym));
   }
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);
+  Optional<RangeSet> getRangeForEqualities(const SymSymExpr *Sym) {
+    Optional<bool> Equality = meansEquality(Sym);
 
     if (!Equality)
       return llvm::None;
 
-    if (Optional<bool> AreEqual = EquivalenceClass::areEqual(
-            State, Equality->Left, Equality->Right)) {
-      if (*AreEqual == Equality->IsEquality) {
+    if (Optional<bool> AreEqual =
+            EquivalenceClass::areEqual(State, Sym->getLHS(), Sym->getRHS())) {
+      // Here we cover two cases at once:
+      //   * if Sym is equality and its operands are known to be equal -> true
+      //   * if Sym is disequality and its operands are disequal -> true
+      if (*AreEqual == *Equality) {
         return getTrueRange(Sym->getType());
       }
+      // Opposite combinations result in false.
       return getFalseRange(Sym->getType());
     }
 
     return llvm::None;
   }
 
   RangeSet getTrueRange(QualType T) {
     RangeSet TypeRange = infer(T);
assign(ProgramStateRef State, SValBuilder &Builder, RangeSet::Factory &F,
     if (!State || NewConstraint.isEmpty())
       return nullptr;
 
     ConstraintAssignor Assignor{State, Builder, F};
     return Assignor.assign(CoS, NewConstraint);
   }
 
   inline bool assignSymExprToConst(const SymExpr *Sym, Const Constraint);
+  inline bool assignSymSymExprToRangeSet(const SymSymExpr *Sym,
+                                         RangeSet Constraint);
 
 private:
   ConstraintAssignor(ProgramStateRef State, SValBuilder &Builder,
                      RangeSet::Factory &F)
       : State(State), Builder(Builder), RangeFactory(F) {}
   using Base = ConstraintAssignorBase<ConstraintAssignor>;
 
   /// Base method for handling new constraints for symbols.
if (const llvm::APSInt *Point = NewConstraint.getConcreteValue()) {
                                          "a state with infeasible constraints");
 
       return setConstraints(State, Constraints);
     }
 
     return setConstraint(State, Class, NewConstraint);
   }
 
+  ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS,
+                                   SymbolRef RHS) {
+    return EquivalenceClass::markDisequal(RangeFactory, State, LHS, RHS);
+  }
+
+  ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS,
+                                SymbolRef RHS) {
+    return EquivalenceClass::merge(RangeFactory, State, LHS, RHS);
+  }
+
+  LLVM_NODISCARD Optional<bool> interpreteAsBool(RangeSet Constraint) {
+    assert(!Constraint.isEmpty() && "Empty ranges shouldn't get here");
+
+    if (Constraint.getConcreteValue())
+      return !Constraint.getConcreteValue()->isNullValue();
+
+    APSIntType T{Constraint.getMinValue()};
+    Const Zero = T.getZeroValue();
+    if (!Constraint.contains(Zero))
+      return true;
+
+    return llvm::None;
+  }
+
   ProgramStateRef State;
   SValBuilder &Builder;
   RangeSet::Factory &RangeFactory;
 };
 
 //===----------------------------------------------------------------------===//
 //                  Constraint manager implementation details
 //===----------------------------------------------------------------------===//
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(RangeSet NewConstraint, ProgramStateRef State,
-                          SymbolRef Sym, const llvm::APSInt &Int,
-                          const llvm::APSInt &Adjustment) {
-    return track<true>(NewConstraint, State, Sym, Int, Adjustment);
-  }
-
-  ProgramStateRef trackNE(RangeSet NewConstraint, ProgramStateRef State,
-                          SymbolRef Sym, const llvm::APSInt &Int,
-                          const llvm::APSInt &Adjustment) {
-    return track<false>(NewConstraint, State, Sym, Int, Adjustment);
-  }
-
-  template <bool EQ>
-  ProgramStateRef track(RangeSet NewConstraint, ProgramStateRef State,
-                        SymbolRef Sym, const llvm::APSInt &Int,
-                        const llvm::APSInt &Adjustment) {
-    if (NewConstraint.isEmpty())
-      // This is an infeasible assumption.
-      return nullptr;
-
-    if (ProgramStateRef NewState = setRange(State, Sym, NewConstraint)) {
-      if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
-        // If the original assumption is not Sym + Adjustment !=/</> Int,
-        // we should invert IsEquality flag.
-        Equality->IsEquality = Equality->IsEquality != EQ;
-        return track(NewState, *Equality);
-      }
-
-      return NewState;
-    }
-
-    return nullptr;
-  }
-
-  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) {
-    return EquivalenceClass::markDisequal(F, State, LHS, RHS);
-  }
-
-  ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS,
-                                SymbolRef RHS) {
-    return EquivalenceClass::merge(F, State, LHS, RHS);
-  }
 };
 
 bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
                                               const llvm::APSInt &Constraint) {
   llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
   // Iterate over all equivalence classes and try to simplify them.
   ClassMembersTy Members = State->get<ClassMembers>();
   for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
     State = Class.simplify(Builder, RangeFactory, State);
     if (!State)
       return false;
   }
 
   return true;
 }
 
+bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym,
+                                                    RangeSet Constraint) {
+  Optional<bool> ConstraintAsBool = interpreteAsBool(Constraint);
+
+  if (!ConstraintAsBool)
+    return true;
+
+  if (Optional<bool> Equality = meansEquality(Sym)) {
+    // Here we cover two cases:
+    //   * if Sym is equality and the new constraint is true -> Sym's operands
+    //     should be marked as equal
+    //   * if Sym is disequality and the new constraint is false -> Sym's
+    //     operands should be also marked as equal
+    if (*Equality == *ConstraintAsBool) {
+      State = trackEquality(State, Sym->getLHS(), Sym->getRHS());
+    } else {
+      // Other combinations leave as with disequal operands.
+      State = trackDisequality(State, Sym->getLHS(), Sym->getRHS());
+    }
+
+    if (!State)
+      return false;
+  }
+
+  return true;
+}
+
 } // end anonymous namespace
 
 std::unique_ptr<ConstraintManager>
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr,
                                    ExprEngine *Eng) {
   return std::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
 
RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
   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);
   New = F.deletePoint(New, Point);
 
-  return trackNE(New, St, Sym, Int, Adjustment);
+  return setRange(St, Sym, New);
 }
 
 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);
   New = F.intersect(New, AdjInt);
 
-  return trackEQ(New, St, Sym, Int, Adjustment);
+  return setRange(St, Sym, New);
 }
 
 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 F.intersect(Result, 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 trackNE(New, St, Sym, Int, Adjustment);
+  return setRange(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 F.intersect(SymRange, 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 trackNE(New, St, Sym, Int, Adjustment);
+  return setRange(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);

clang/test/Analysis/equality_tracking.c

if (a != b) {
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
     return;
   }
   clang_analyzer_warnIfReached(); // no warning
   // a == b
   if (c < 0)
     ;
 }
+
+void implyDisequalityFromGT(int a, int b) {
+  if (a > b) {
+    clang_analyzer_eval(a == b); // expected-warning{{FALSE}}
+    clang_analyzer_eval(a != b); // expected-warning{{TRUE}}
+  }
+}
+
+void implyDisequalityFromLT(int a, int b) {
+  if (a < b) {
+    clang_analyzer_eval(a == b); // expected-warning{{FALSE}}
+    clang_analyzer_eval(a != b); // expected-warning{{TRUE}}
+  }
+}