[analyzer][solver] Improve reasoning for not equal to operator
authorManas <manas18244@iiitd.ac.in>
Tue, 24 Jan 2023 20:59:05 +0000 (02:29 +0530)
committerManas <manas18244@iiitd.ac.in>
Tue, 24 Jan 2023 21:02:55 +0000 (02:32 +0530)
This patch fixes certain cases where solver was not able to infer
disequality due to overlapping of values in rangeset. This case was
casting from lower signed type to bigger unsigned type.

Reviewed By: steakhal

Differential Revision: https://reviews.llvm.org/D140086

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/constant-folding.c

index 3725e49..1017dff 100644 (file)
@@ -1622,7 +1622,33 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(RangeSet LHS,
   if (LHS.getAPSIntType() == RHS.getAPSIntType()) {
     if (intersect(RangeFactory, LHS, RHS).isEmpty())
       return getTrueRange(T);
+
   } else {
+    // We can only lose information if we are casting smaller signed type to
+    // bigger unsigned type. For e.g.,
+    //    LHS (unsigned short): [2, USHRT_MAX]
+    //    RHS   (signed short): [SHRT_MIN, 0]
+    //
+    // Casting RHS to LHS type will leave us with overlapping values
+    //    CastedRHS : [0, 0] U [SHRT_MAX + 1, USHRT_MAX]
+    //
+    // We can avoid this by checking if signed type's maximum value is lesser
+    // than unsigned type's minimum value.
+
+    // If both have different signs then only we can get more information.
+    if (LHS.isUnsigned() != RHS.isUnsigned()) {
+      if (LHS.isUnsigned() && (LHS.getBitWidth() >= RHS.getBitWidth())) {
+        if (RHS.getMaxValue().isNegative() ||
+            LHS.getAPSIntType().convert(RHS.getMaxValue()) < LHS.getMinValue())
+          return getTrueRange(T);
+
+      } else if (RHS.isUnsigned() && (LHS.getBitWidth() <= RHS.getBitWidth())) {
+        if (LHS.getMaxValue().isNegative() ||
+            RHS.getAPSIntType().convert(LHS.getMaxValue()) < RHS.getMinValue())
+          return getTrueRange(T);
+      }
+    }
+
     // Both RangeSets should be casted to bigger unsigned type.
     APSIntType CastingType(std::max(LHS.getBitWidth(), RHS.getBitWidth()),
                            LHS.isUnsigned() || RHS.isUnsigned());
@@ -2151,7 +2177,6 @@ private:
   RangeSet::Factory &RangeFactory;
 };
 
-
 bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
                                               const llvm::APSInt &Constraint) {
   llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
index f0598d4..620adcd 100644 (file)
@@ -303,7 +303,8 @@ void testDisequalityRules(unsigned int u1, unsigned int u2, unsigned int u3,
 
   if (s1 < 0 && s1 > -4 && u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
     // s1: [-3, -1], u1: [UINT_MAX - 3, UINT_MAX - 2]
-    clang_analyzer_eval(u1 != s1); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
+    clang_analyzer_eval(s1 != u1); // expected-warning{{TRUE}}
   }
 
   if (s1 < 1 && s1 > -6 && s1 != -4 && s1 != -3 &&
@@ -400,12 +401,10 @@ void testDisequalityRules(unsigned int u1, unsigned int u2, unsigned int u3,
     clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
   }
 
-  // FIXME: Casting smaller signed types to unsigned one may leave us with
-  // overlapping values, falsely indicating UNKNOWN, where it is possible to
-  // assert TRUE.
   if (uch > 1 && sch < 1) {
     // uch: [2, UCHAR_MAX], sch: [SCHAR_MIN, 0]
-    clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(uch != sch); // expected-warning{{TRUE}}
+    clang_analyzer_eval(sch != uch); // expected-warning{{TRUE}}
   }
 
   if (uch <= 1 && uch >= 1 && sch <= 1 && sch >= 1) {
@@ -419,10 +418,9 @@ void testDisequalityRules(unsigned int u1, unsigned int u2, unsigned int u3,
     clang_analyzer_eval(ush != ssh); // expected-warning{{UNKNOWN}}
   }
 
-  // FIXME: Casting leave us with overlapping values. Should be TRUE.
   if (ush > 1 && ssh < 1) {
     // ush: [2, USHRT_MAX], ssh: [SHRT_MIN, 0]
-    clang_analyzer_eval(ush != ssh); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(ush != ssh); // expected-warning{{TRUE}}
   }
 
   if (ush <= 1 && ush >= 1 && ssh <= 1 && ssh >= 1) {