[analyzer] Introduce reasoning about symbolic remainder operator

[vsavchenko]

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.

[vsavchenko]

Here is a proof in Z3:
https://gist.github.com/SavchenkoValeriy/559ca923b050f2c01e340c1be543b7e0

[vsavchenko]

Rebase

[vsavchenko]

Here is a short summary of the performance testing I conducted across a bunch of open-source projects:

	vim	git	tmux	redis	cmake	pytorch	bitcoin	protobuf
Time (before)	20m56s	18m41s	11m40s	1h15m34s	30m34s	6h35m18s	9m27s	6m03s
Time (after)	22m16s	19m58s	29m52s	1h17m32s	33m03s	9h46m41s	9m33s	6m03s
Delta	+6.4%	+6.9%	+155.8%	+2.6%	+8.1%	+48.4%	-1.1%	+0.1%

Time (before) was measured on a commit before any of my solver changes.

This shows that performance tweaks discussed in various TODOs are indeed required to reduce the hit.

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

459

(Origin.From() + 1).isMinSignedValue() is another sufficient condition(?)

462

You mean zero, right?

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

459

I'm sorry, I don't quite get what cases does this check cover. Can you please explain what you have in mind?

462

No, not always. It still can be signed at this point.

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

462

Ok, so i misunderstood. This function computes range of abs($x) aka |$x| given the range for $x, right?

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

462

I guess I should fix my comments (and maybe the name for this function).
This function finds absolute maximum, i.e. the value C: |$x| <= C and returns the range [-C, C] for signed $xs and [0, C] for unsigned $xs.

So this new range is guaranteed to include the original range.

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

459

Aha, ok, nvm, a different issue then: For range [INT_MIN + 1, INT_MAX], the correct answer should be `[INT_MIN + 1, INT_MAX] (which is [-C, C] for C = INT_MAX]) rather than [INT_MIN, INT_MAX].

[vsavchenko]

Fix code review remarks.

[xazax.hun]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

633

I wonder if we actually need this? I vaguely recall that we are doing a lot of simplifications during building symbolic expressions. I would be surprised if this identity is not handled there. (And in that case, probable this should be added there.) Or we might need a comment to explain why do we need this simplification at both places.

[ASDenysPetrov]

@vsavchenko
I've made some assumptions.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

459–469

I think you should swap if statements. I'll explain.
Let's consider the input is an uint8 range [42, 242] and you will return [0, 242] in the second if.
But if the input is an uint8 range [128, 242] you will return [0, 255] in the first if, because 128 is an equivalent of -128(INT8_MIN) in binary representation so the condition in the first if would be true.
What is the great difference between [42, 242] and [128, 242] to have different results? Or you've just missed this case?

P.S. I think your function's name doesn't fit its body, since absolute value is always positive (without sign) from its definition, but you output range may have negative values. You'd better write an explanation above the function and rename it.

481

As for me, the last reason fully covers previous special cases, so you can omit those ones, thus simplify the comment.

659

Extend the comment, please, why we should move bounds to zero at all.

684

Is it OK to return this rangeset in case when one of operands(or both) is negative, since this rangeset can vary from specific implementation?

[vsavchenko]

Move 0 % x case to SValBuilder

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

459–469

It is a valid point, I will add this test and change this behaviour!

The name is confusing indeed, maybe you have any ideas what would be more appropriate?

481

I really want to be clear about the first two cases to explain why this works for any sign of From and To

633

Yeah, we don't do it in SValBuilder, but it is definitely a better place for that particular case. I'll move it.

659

Good point!

684

Yes, it is a conservative range for any ranges because only the sign of the operation is specific to different implementations

[vsavchenko]

Fix code review remarks

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

459–469

@NoQ , @ASDenysPetrov what do you think about this name instead (i.e. getSymmetricalRange).

[vsavchenko]

Performance-wise, I've investigated huge slowdowns on tmux and pytorch.

• pytorch build produces a lot of warnings and simply trashed my terminal. I guess one time it had more troubles with displaying all that than the other. Here is a table with new times:

	pytorch
Time (before)	2h21m33s
Time (after)	2h19m23s
Delta	-1.5%

As you can see, these numbers are way smaller than the original ones.

• tmux is a much smaller project, so I decided to run it 20 times for each case.

After consistently shows slower runtimes, but the overall difference (for median times) is only +3%.

I believe that as of now we can submit these modifications as is and explore performance optimizations later if needed.

[NoQ]

Aha, so performance regressions on real code weren't real, that's a relief :)

I believe that as of now we can submit these modifications as is and explore performance optimizations later if needed.

I still encourage you to explore the tests we have from our previous attempts to simplify expressions recursively without memoization (test/Analysis/hangs.c). I'm asking because these aren't all that artificial: this kind of code was previously reported by a frustrated user as "the analyzer started hanging on my code". Like, please replace a bunch of +es with &/|/% and see if this causes your code to perform exponentially over the size of the program. If so, i'd rather have us hurry up and implement memoization.

The math in this patch looks great, thanks!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

461–462

I suggest not trying to express signed types and unsigned types in a single formula, the reader will have to unwrap it back into the two cases anyway in order to understand what's going on.

The following would imho be easier to read: "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".

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

461–462

That is a perfect explanation, thanks!

[NoQ]

In D80117#2059567, @NoQ wrote:

I believe that as of now we can submit these modifications as is and explore performance optimizations later if needed.

I still encourage you to explore the tests we have from our previous attempts to simplify expressions recursively without memoization (test/Analysis/hangs.c). I'm asking because these aren't all that artificial: this kind of code was previously reported by a frustrated user as "the analyzer started hanging on my code". Like, please replace a bunch of +es with &/|/% and see if this causes your code to perform exponentially over the size of the program. If so, i'd rather have us hurry up and implement memoization.

Ok, looks like my memories on this subject are heavily messed up. The actual problem that made us hang was solved by D47155. This is a dumb bug that would have been avoided if we had memoization but it doesn't require memoization to be avoided and it doesn't look like this code risks repeating that mistake.

Then, our experience with memoization in D47402 wasn't as good as i expected; it turned out that there are other exponential parts of the analysis in such cases that we still couldn't avoid. We should probably still do it (given how difficult it is now to identify these "other parts" that are exponential, i'd rather not add more such parts consciously) but i guess it's not that much of a blocker.

[vsavchenko]

Fix code review remarks

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

private:
 
   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);
     }
   }
 
   //===----------------------------------------------------------------------===//
   //                         Ranges and operators
   //===----------------------------------------------------------------------===//
RangeSet VisitBinaryOperator(RangeSet LHS, RangeSet RHS, QualType T) {
     return VisitBinaryOperator<Op>(*ConvertedCoarseLHS, *ConvertedCoarseRHS, T);
   }
 
   template <BinaryOperator::Opcode Op>
   RangeSet VisitBinaryOperator(Range LHS, Range RHS, QualType T) {
     return infer(T);
   }
 
+  Range makeAbsolute(Range Origin, QualType T) {
+    APSIntType RangeType = ValueFactory.getAPSIntType(T);
+
+    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)};
+    }
+
+    if (RangeType.isUnsigned()) {
+      return Range(ValueFactory.getMinValue(RangeType), Origin.To());
+    }
+
+    // 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);
     return Domain.Intersect(ValueFactory, RangeFactory,
                             ++IntType.getZeroValue(), --IntType.getZeroValue());
   }
 
   // FIXME: Once SValBuilder supports unary minus, we should use SValBuilder to
if (IsLHSPositiveOrZero || IsRHSPositiveOrZero) {
     return {RangeFactory, ValueFactory.getValue(Zero),
             ValueFactory.getValue(Max)};
   }
 
   // Nothing much else to do here.
   return infer(T);
 }
 
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
+                                                            Range RHS,
+                                                            QualType T) {
+  llvm::APSInt Zero = ValueFactory.getAPSIntType(T).getZeroValue();
+
+  Range ConservativeRange = makeAbsolute(RHS, T);
+
+  llvm::APSInt Max = ConservativeRange.To();
+  llvm::APSInt Min = ConservativeRange.From();
+
+  // 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).
+  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();
+  }
+
+  // Offset the boundaries towards zero.
+  //
+  // 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;
+  }
+
+  return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};
+}
+
 class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(SubEngine *SE, SValBuilder &SVB)
       : RangedConstraintManager(SE, SVB) {}
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
 
   bool haveEqualConstraints(ProgramStateRef S1,
                             ProgramStateRef S2) const override {
     return S1->get<ConstraintRange>() == S2->get<ConstraintRange>();
   }
 

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

case nonloc::ConcreteIntKind: {
         if (LHSValue.isAllOnesValue() && LHSValue.isSigned())
           return evalCastFromNonLoc(lhs, resultTy);
         LLVM_FALLTHROUGH;
       case BO_Shl:
         // 0<<a and 0>>a
         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);
       }
     }
     case nonloc::SymbolValKind: {
       // We only handle LHS as simple symbols or SymIntExprs.
       SymbolRef Sym = lhs.castAs<nonloc::SymbolVal>().getSymbol();
 

clang/test/Analysis/PR35418.cpp

+// 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);
+}

clang/test/Analysis/constant-folding.c

 // 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.
 
 void testComparisons (int a) {
   // Sema can already catch the simple comparison a==a,
   // since that's usually a logic error (and not path-dependent).
   int b = a;
void testBitwiseRules(unsigned int a, int b, int c) {
   if (a < 10) {
     clang_analyzer_eval((a | 20) >= 20); // expected-warning{{TRUE}}
   }
 
   if (a > 10) {
     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}}
+    }
+  }
+}

clang/test/Analysis/uninit-bug-first-iteration-init.c

+// 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;
+}