[analyzer] Introduce reasoning about symbolic remainder operator
authorValeriy Savchenko <vsavchenko@nitrogen.local>
Thu, 14 May 2020 14:07:54 +0000 (17:07 +0300)
committerValeriy Savchenko <vsavchenko@apple.com>
Thu, 28 May 2020 15:56:38 +0000 (18:56 +0300)
Summary:
New logic tries to narrow possible result values of the remainder operation
based on its operands and their ranges.  It also tries to be conservative
with negative operands because according to the standard the sign of
the result is implementation-defined.

rdar://problem/44978988

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

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
clang/test/Analysis/PR35418.cpp [new file with mode: 0644]
clang/test/Analysis/constant-folding.c
clang/test/Analysis/hangs.c
clang/test/Analysis/uninit-bug-first-iteration-init.c [new file with mode: 0644]

index b73c395..6f92b96 100644 (file)
@@ -433,6 +433,8 @@ private:
       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);
     }
@@ -496,6 +498,46 @@ private:
     return infer(T);
   }
 
+  /// Return a symmetrical range for the given range and type.
+  ///
+  /// If T is signed, return the smallest range [-x..x] that covers the original
+  /// range, or [-min(T), max(T)] if the aforementioned symmetric range doesn't
+  /// exist due to original range covering min(T)).
+  ///
+  /// If T is unsigned, return the smallest range [0..x] that covers the
+  /// original range.
+  Range getSymmetricalRange(Range Origin, QualType T) {
+    APSIntType RangeType = ValueFactory.getAPSIntType(T);
+
+    if (RangeType.isUnsigned()) {
+      return Range(ValueFactory.getMinValue(RangeType), Origin.To());
+    }
+
+    if (Origin.From().isMinSignedValue()) {
+      // If mini is a minimal signed value, absolute value of it is greater
+      // than the maximal signed value.  In order to avoid these
+      // complications, we simply return the whole range.
+      return {ValueFactory.getMinValue(RangeType),
+              ValueFactory.getMaxValue(RangeType)};
+    }
+
+    // At this point, we are sure that the type is signed and we can safely
+    // use unary - operator.
+    //
+    // While calculating absolute maximum, we can use the following formula
+    // because of these reasons:
+    //   * If From >= 0 then To >= From and To >= -From.
+    //     AbsMax == To == max(To, -From)
+    //   * If To <= 0 then -From >= -To and -From >= From.
+    //     AbsMax == -From == max(-From, To)
+    //   * Otherwise, From <= 0, To >= 0, and
+    //     AbsMax == max(abs(From), abs(To))
+    llvm::APSInt AbsMax = std::max(-Origin.From(), Origin.To());
+
+    // Intersection is guaranteed to be non-empty.
+    return {ValueFactory.getValue(-AbsMax), ValueFactory.getValue(AbsMax)};
+  }
+
   /// Return a range set subtracting zero from \p Domain.
   RangeSet assumeNonZero(RangeSet Domain, QualType T) {
     APSIntType IntType = ValueFactory.getAPSIntType(T);
@@ -635,6 +677,63 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_And>(Range LHS,
   return infer(T);
 }
 
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
+                                                            Range RHS,
+                                                            QualType T) {
+  llvm::APSInt Zero = ValueFactory.getAPSIntType(T).getZeroValue();
+
+  Range ConservativeRange = getSymmetricalRange(RHS, T);
+
+  llvm::APSInt Max = ConservativeRange.To();
+  llvm::APSInt Min = ConservativeRange.From();
+
+  if (Max == Zero) {
+    // It's an undefined behaviour to divide by 0 and it seems like we know
+    // for sure that RHS is 0.  Let's say that the resulting range is
+    // simply infeasible for that matter.
+    return RangeFactory.getEmptySet();
+  }
+
+  // At this point, our conservative range is closed.  The result, however,
+  // couldn't be greater than the RHS' maximal absolute value.  Because of
+  // this reason, we turn the range into open (or half-open in case of
+  // unsigned integers).
+  //
+  // While we operate on integer values, an open interval (a, b) can be easily
+  // represented by the closed interval [a + 1, b - 1].  And this is exactly
+  // what we do next.
+  //
+  // If we are dealing with unsigned case, we shouldn't move the lower bound.
+  if (Min.isSigned()) {
+    ++Min;
+  }
+  --Max;
+
+  bool IsLHSPositiveOrZero = LHS.From() >= Zero;
+  bool IsRHSPositiveOrZero = RHS.From() >= Zero;
+
+  // Remainder operator results with negative operands is implementation
+  // defined.  Positive cases are much easier to reason about though.
+  if (IsLHSPositiveOrZero && IsRHSPositiveOrZero) {
+    // If maximal value of LHS is less than maximal value of RHS,
+    // the result won't get greater than LHS.To().
+    Max = std::min(LHS.To(), Max);
+    // We want to check if it is a situation similar to the following:
+    //
+    // <------------|---[  LHS  ]--------[  RHS  ]----->
+    //  -INF        0                              +INF
+    //
+    // In this situation, we can conclude that (LHS / RHS) == 0 and
+    // (LHS % RHS) == LHS.
+    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)};
+}
+
 class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
index d9fe3af..2e269f6 100644 (file)
@@ -652,6 +652,11 @@ SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
         if (LHSValue == 0)
           return evalCastFromNonLoc(lhs, resultTy);
         return makeSymExprValNN(op, InputLHS, InputRHS, resultTy);
+      case BO_Rem:
+        // 0 % x == 0
+        if (LHSValue == 0)
+          return makeZeroVal(resultTy);
+        LLVM_FALLTHROUGH;
       default:
         return makeSymExprValNN(op, InputLHS, InputRHS, resultTy);
       }
diff --git a/clang/test/Analysis/PR35418.cpp b/clang/test/Analysis/PR35418.cpp
new file mode 100644 (file)
index 0000000..658da72
--- /dev/null
@@ -0,0 +1,28 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s
+
+// expected-no-diagnostics
+
+void halt() __attribute__((__noreturn__));
+void assert(int b) {
+  if (!b)
+    halt();
+}
+
+void decode(unsigned width) {
+  assert(width > 0);
+
+  int base;
+  bool inited = false;
+
+  int i = 0;
+
+  if (i % width == 0) {
+    base = 512;
+    inited = true;
+  }
+
+  base += 1; // no-warning
+
+  if (base >> 10)
+    assert(false);
+}
index b3320cc..08a7acc 100644 (file)
@@ -1,5 +1,9 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify -analyzer-config eagerly-assume=false %s
 
+#define UINT_MAX (~0U)
+#define INT_MAX (int)(UINT_MAX & (UINT_MAX >> 1))
+#define INT_MIN (int)(UINT_MAX & ~(UINT_MAX >> 1))
+
 void clang_analyzer_eval(int);
 
 // There should be no warnings unless otherwise indicated.
@@ -174,3 +178,76 @@ void testBitwiseRules(unsigned int a, int b, int c) {
     clang_analyzer_eval((a & 1) <= 1); // expected-warning{{TRUE}}
   }
 }
+
+void testRemainderRules(unsigned int a, unsigned int b, int c, int d) {
+  // Check that we know that remainder of zero divided by any number is still 0.
+  clang_analyzer_eval((0 % c) == 0); // expected-warning{{TRUE}}
+
+  clang_analyzer_eval((10 % a) <= 10); // expected-warning{{TRUE}}
+
+  if (a <= 30 && b <= 50) {
+    clang_analyzer_eval((40 % a) < 30); // expected-warning{{TRUE}}
+    clang_analyzer_eval((a % b) < 50);  // expected-warning{{TRUE}}
+    clang_analyzer_eval((b % a) < 30);  // expected-warning{{TRUE}}
+
+    if (a >= 10) {
+      // Even though it seems like a valid assumption, it is not.
+      // Check that we are not making this mistake.
+      clang_analyzer_eval((a % b) >= 10); // expected-warning{{UNKNOWN}}
+
+      // Check that we can we can infer when remainder is equal
+      // to the dividend.
+      clang_analyzer_eval((4 % a) == 4); // expected-warning{{TRUE}}
+      if (b < 7) {
+        clang_analyzer_eval((b % a) < 7); // expected-warning{{TRUE}}
+      }
+    }
+  }
+
+  if (c > -10) {
+    clang_analyzer_eval((d % c) < INT_MAX);     // expected-warning{{TRUE}}
+    clang_analyzer_eval((d % c) > INT_MIN + 1); // expected-warning{{TRUE}}
+  }
+
+  // Check that we can reason about signed integers when they are
+  // known to be positive.
+  if (c >= 10 && c <= 30 && d >= 20 && d <= 50) {
+    clang_analyzer_eval((5 % c) == 5);  // expected-warning{{TRUE}}
+    clang_analyzer_eval((c % d) <= 30); // expected-warning{{TRUE}}
+    clang_analyzer_eval((c % d) >= 0);  // expected-warning{{TRUE}}
+    clang_analyzer_eval((d % c) < 30);  // expected-warning{{TRUE}}
+    clang_analyzer_eval((d % c) >= 0);  // expected-warning{{TRUE}}
+  }
+
+  if (c >= -30 && c <= -10 && d >= -20 && d <= 50) {
+    // Test positive LHS with negative RHS.
+    clang_analyzer_eval((40 % c) < 30);  // expected-warning{{TRUE}}
+    clang_analyzer_eval((40 % c) > -30); // expected-warning{{TRUE}}
+
+    // Test negative LHS with possibly negative RHS.
+    clang_analyzer_eval((-10 % d) < 50);  // expected-warning{{TRUE}}
+    clang_analyzer_eval((-20 % d) > -50); // expected-warning{{TRUE}}
+
+    // Check that we don't make wrong assumptions
+    clang_analyzer_eval((-20 % d) > -20); // expected-warning{{UNKNOWN}}
+
+    // Check that we can reason about negative ranges...
+    clang_analyzer_eval((c % d) < 50); // expected-warning{{TRUE}}
+    /// ...both ways
+    clang_analyzer_eval((d % c) < 30); // expected-warning{{TRUE}}
+
+    if (a <= 10) {
+      // Result is unsigned.  This means that 'c' is casted to unsigned.
+      // We don't want to reason about ranges changing boundaries with
+      // conversions.
+      clang_analyzer_eval((a % c) < 30); // expected-warning{{UNKNOWN}}
+    }
+  }
+
+  // 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}}
+  }
+}
index b109bcb..ce719a1 100644 (file)
@@ -1,9 +1,16 @@
-// RUN: %clang_analyze_cc1 -analyzer-checker core -verify %s
-
-// expected-no-diagnostics
+// RUN: %clang_analyze_cc1 -verify %s \
+// RUN:   -analyzer-checker core,debug.ExprInspection
 
 // Stuff that used to hang.
 
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+                          unsigned int __line, __const char *__function)
+    __attribute__((__noreturn__));
+#define assert(expr) \
+  ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+void clang_analyzer_eval(int);
+
 int g();
 
 int f(int y) {
@@ -28,3 +35,186 @@ void produce_an_exponentially_exploding_symbol(int x, int y) {
   x += y; y += x + g();
   x += y; y += x + g();
 }
+
+void produce_an_exponentially_exploding_symbol_2(int x, int y) {
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  if (x > 1) {
+    if (x > 2) {
+      if (x > 3) {
+        if (x > 4) {
+          if (x > 5) {
+            if (x > 6) {
+              if (x > 7) {
+                if (x > 8) {
+                  if (x > 9) {
+                    if (x > 10) {
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+void produce_an_exponentially_exploding_symbol_3(int x, int y) {
+  assert(0 < x && x < 10);
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  x &= y;
+  y &= x & g();
+  clang_analyzer_eval(0 < x && x < 10); // expected-warning{{TRUE}}
+                                        // expected-warning@-1{{FALSE}}
+}
diff --git a/clang/test/Analysis/uninit-bug-first-iteration-init.c b/clang/test/Analysis/uninit-bug-first-iteration-init.c
new file mode 100644 (file)
index 0000000..a0fae29
--- /dev/null
@@ -0,0 +1,27 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s
+
+// rdar://problem/44978988
+// expected-no-diagnostics
+
+int foo();
+
+int gTotal;
+
+double bar(int start, int end) {
+  int i, cnt, processed, size;
+  double result, inc;
+
+  result = 0;
+  processed = start;
+  size = gTotal * 2;
+  cnt = (end - start + 1) * size;
+
+  for (i = 0; i < cnt; i += 2) {
+    if ((i % size) == 0) {
+      inc = foo();
+      processed++;
+    }
+    result += inc * inc; // no-warning
+  }
+  return result;
+}