[analyzer][solver] Introduce reasoning for not equal to operator

[manas]

Summary

With this patch, the solver can infer results for not equal to operator
over Ranges as well. This also fixes the issue of comparison between
different types, by first converting the RangeSets to resulting type,
which then can be used for comparisons.

[manas]

Closing this as this is mistakenly a duplicate of existing differential D112621.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/ImmutableSet.h"
 #include "llvm/ADT/STLExtras.h"
-#include "llvm/ADT/StringExtras.h"
 #include "llvm/ADT/SmallSet.h"
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/Compiler.h"
 #include "llvm/Support/raw_ostream.h"
 #include <algorithm>
 #include <iterator>
 
 using namespace clang;
 using namespace ento;
 
RangeSet VisitBinaryOperator(const BinarySymExprTy *Sym) {
     // in here.
     QualType ResultType = Sym->getType();
     return VisitBinaryOperator(inferAs(Sym->getLHS(), ResultType),
                                Sym->getOpcode(),
                                inferAs(Sym->getRHS(), ResultType), ResultType);
   }
 
   RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op,
-                               RangeSet RHS, QualType T) {
-    switch (Op) {
-    case BO_Or:
-      return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
-    case BO_And:
-      return VisitBinaryOperator<BO_And>(LHS, RHS, T);
-    case BO_Rem:
-      return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
-    default:
-      return infer(T);
-    }
-  }
+                               RangeSet RHS, QualType T);
 
   //===----------------------------------------------------------------------===//
   //                         Ranges and operators
   //===----------------------------------------------------------------------===//
 
   /// Return a rough approximation of the given range set.
   ///
   /// For the range set:
private:
   ProgramStateRef State;
 };
 
 //===----------------------------------------------------------------------===//
 //               Range-based reasoning about symbolic operations
 //===----------------------------------------------------------------------===//
 
 template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(RangeSet LHS,
+                                                           RangeSet RHS,
+                                                           QualType T) {
+
+  // We must check for empty RangeSets. This gets done via VisitBinaryOperator
+  // for other operators, but BO_NE is handled specifically.
+  if (LHS.isEmpty() || RHS.isEmpty()) {
+    return RangeFactory.getEmptySet();
+  }
+
+  APSIntType ResultType = ValueFactory.getAPSIntType(T);
+
+  RangeSet ConvertedLHS = RangeFactory.getEmptySet();
+  RangeSet ConvertedRHS = RangeFactory.getEmptySet();
+
+  // Convert each Range inside the RangeSet to given type. This will make it
+  // possible to have comparisons between different APSInts.
+  for (auto LRange : LHS) {
+    auto ConvertedLRange = convert(LRange, ResultType);
+
+    // If any of the converted Range is not bounded within the limits of the
+    // type, then we must not compare the APSInt values. Hence, we have no
+    // option other than to infer results via type.
+    if (!ConvertedLRange) {
+      return infer(T);
+    }
+
+    ConvertedLHS = RangeFactory.add(ConvertedLHS, ConvertedLRange.getValue());
+  }
+
+  for (auto RRange : RHS) {
+    auto ConvertedRRange = convert(RRange, ResultType);
+
+    if (!ConvertedRRange) {
+      return infer(T);
+    }
+
+    ConvertedRHS = RangeFactory.add(ConvertedRHS, ConvertedRRange.getValue());
+  }
+
+  // When both the Ranges are non-overlapping then all possible pairs of (x, y)
+  // in ConvertedLHS, ConvertedRHS respectively, will satisfy expression
+  // (x != y).
+  if ((ConvertedLHS.getMaxValue() < ConvertedRHS.getMinValue()) ||
+      (ConvertedLHS.getMinValue() > ConvertedRHS.getMaxValue())) {
+    return getTrueRange(T);
+  }
+
+  // If both Ranges contain only one Point which is equal, then the expression
+  // will always return true.
+  if ((ConvertedLHS.getMinValue() == ConvertedRHS.getMaxValue()) &&
+      (ConvertedLHS.getMaxValue() == ConvertedRHS.getMaxValue()) &&
+      (ConvertedLHS.getMinValue() == ConvertedRHS.getMinValue())) {
+    return getFalseRange(T);
+  }
+
+  // In all other cases, the resulting range cannot be deduced.
+  return infer(T);
+}
+
+template <>
 RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS,
                                                            QualType T) {
   APSIntType ResultType = ValueFactory.getAPSIntType(T);
   llvm::APSInt Zero = ResultType.getZeroValue();
 
   bool IsLHSPositiveOrZero = LHS.From() >= Zero;
   bool IsRHSPositiveOrZero = RHS.From() >= Zero;
 
if (IsLHSPositiveOrZero && IsRHSPositiveOrZero) {
     Min = LHS.To() < RHS.From() ? LHS.From() : Zero;
   }
 
   // Nevertheless, the symmetrical range for RHS is a conservative estimate
   // for any sign of either LHS, or RHS.
   return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};
 }
 
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator(RangeSet LHS,
+                                                    BinaryOperator::Opcode Op,
+                                                    RangeSet RHS, QualType T) {
+  switch (Op) {
+  case BO_NE:
+    return VisitBinaryOperator<BO_NE>(LHS, RHS, T);
+  case BO_Or:
+    return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
+  case BO_And:
+    return VisitBinaryOperator<BO_And>(LHS, RHS, T);
+  case BO_Rem:
+    return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
+  default:
+    return infer(T);
+  }
+}
+
 //===----------------------------------------------------------------------===//
 //                  Constraint manager implementation details
 //===----------------------------------------------------------------------===//
 
 class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
       : RangedConstraintManager(EE, SVB), F(getBasicVals()) {}
LLVM_NODISCARD Optional<bool> interpreteAsBool(RangeSet Constraint) {
     return llvm::None;
   }
 
   ProgramStateRef State;
   SValBuilder &Builder;
   RangeSet::Factory &RangeFactory;
 };
 
-
 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) {
     EquivalenceClass Class = ClassToSymbolSet.first;
     State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);

clang/test/Analysis/constant-folding.c

void testRemainderRules(unsigned int a, unsigned int b, int c, int d) {
 
   // Check that we work correctly when minimal unsigned value from a range is
   // equal to the signed minimum for the same bit width.
   unsigned int x = INT_MIN;
   if (a >= x && a <= x + 10) {
     clang_analyzer_eval((b % a) < x + 10); // expected-warning{{TRUE}}
   }
 }
+
+void testDisequalityRules(unsigned int u1, unsigned int u2, int s1, int s2) {
+  // Checks when ranges are not overlapping
+  if (u1 <= 10 && u2 >= 20) {
+    // u1: [0,10], u2: [20,UINT_MAX]
+    clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{TRUE}}
+  }
+
+  if (s1 <= INT_MIN + 10 && s2 >= INT_MAX - 10) {
+    // s1: [INT_MIN,INT_MIN + 10], s2: [INT_MAX - 10,INT_MAX]
+    clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{FALSE}}
+  }
+
+  // Checks when ranges are completely overlapping and have more than one point
+  if (u1 >= 20 && u1 <= 50 && u2 >= 20 && u2 <= 50) {
+    // u1: [20,50], u2: [20,50]
+    clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{UNKNOWN}}
+  }
+
+  if (s1 >= -20 && s1 <= 20 && s2 >= -20 && s2 <= 20) {
+    // s1: [-20,20], s2: [-20,20]
+    clang_analyzer_eval((s1 != s2) != 0); // expected-warning{{UNKNOWN}}
+  }
+
+  // Checks when ranges are partially overlapping
+  if (u1 >= 100 && u1 <= 200 && u2 >= 150 && u2 <= 300) {
+    // u1: [100,200], u2: [150,300]
+    clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{UNKNOWN}}
+  }
+
+  if (s1 >= -80 && s1 <= -50 && s2 >= -100 && s2 <= -75) {
+    // s1: [-80,-50], s2: [-100,-75]
+    clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{UNKNOWN}}
+  }
+
+  // Checks for ranges which are subset of one-another
+  if (u1 >= 500 && u1 <= 1000 && u2 >= 750 && u2 <= 1000) {
+    // u1: [500,1000], u2: [750,1000]
+    clang_analyzer_eval((u1 != u2) == 0); // expected-warning{{UNKNOWN}}
+  }
+
+  if (s1 >= -1000 && s1 <= -500 && s2 <= -500 && s2 >= -750) {
+    // s1: [-1000,-500], s2: [-500,-750]
+    clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{UNKNOWN}}
+  }
+
+  // Checks for comparison between different types
+  if (u1 <= 255 && s1 <= 0) {
+    // u1: [0, 255], s1: [INT_MIN, 0]
+    clang_analyzer_eval((u1 != s1) == 0); // expected-warning{{UNKNOWN}}
+  }
+}