[analyzer] Introduce range-based reasoning for subtraction operator

[manas]

Summary

Add logic for computing rangesets for symbolic subtraction operator and
add test cases.

[vsavchenko]

Hey Manas! Great job, you put this together real quick!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1490

Maybe you can include this as yet another condition in the next if statement? Their bodies are identical.

clang/test/Analysis/constant-folding.c

399

Maybe you can check (a - b) > 5 && (a - b) < UINT_MAX - 9 to cover the whole range?

405

This is also Min and Max overflowing on the positive side.

[manas]

Thanks Valeriy.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1490

True. I wanted to optimize the following if condition as it looks quite ugly right now! Although, I will concatenate these conditions for now and work on the optimization later.

clang/test/Analysis/constant-folding.c

399

That's true! I never thought of putting them together. Makes more sense.

405

I missed it! I will add another case for only Max overflowing on positive side and will keep this test as well.

[manas]

Merge conditionals with similar block and add test for one overflow on Tmax-side

[manas]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1494

@vsavchenko one thing crossed my mind is that, shouldn't I compare From and To values with llvm::APSInt Zero = ValueFactory.getAPSIntType(T).getZeroValue() instead of literal 0?

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1494

Yes! Thanks for noticing this (the same goes to the other patch as well)

[manas]

Replace literal-value 0 with APSInt Zero

[manas]

Remove redundant getAPSIntType calls

[manas]

Here is the proof using Z3: https://gist.github.com/weirdsmiley/8a35a0e1f55f310e3566cbd47555491a

[manas]

In D105273#2891921, @manas wrote:

Here is the proof using Z3: https://gist.github.com/weirdsmiley/8a35a0e1f55f310e3566cbd47555491a

I have updated the proof for Sub.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode 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);
     case BO_Add:
       return VisitBinaryOperator<BO_Add>(LHS, RHS, T);
+    case BO_Sub:
+      return VisitBinaryOperator<BO_Sub>(LHS, RHS, T);
     default:
       return infer(T);
     }
   }
 
   //===----------------------------------------------------------------------===//
   //                         Ranges and operators
   //===----------------------------------------------------------------------===//
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Add>(Range LHS,
   }
 
   // When both boundary values overflow from different sides then rangeset is
   // [Tmin, Tmax] because the entire rangeset is already covered and overflow
   // from opposite sides ensure already computed points to be reached again.
   return {RangeFactory, Tmin, Tmax};
 }
 
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Sub>(Range LHS,
+                                                            Range RHS,
+                                                            QualType T) {
+  APSIntType ResultType = ValueFactory.getAPSIntType(T);
+  const llvm::APSInt &Tmin = ValueFactory.getMinValue(ResultType);
+  const llvm::APSInt &Tmax = ValueFactory.getMaxValue(ResultType);
+
+  llvm::APSInt Min, Max;
+  bool HasMinOverflowed, HasMaxOverflowed;
+
+  // Based on their signedness, compute values for Min and Max, and also store
+  // whether those values have overflowed or not.
+  if (ResultType.isUnsigned()) {
+    Min = llvm::APSInt(LHS.From().usub_ov(RHS.To(), HasMinOverflowed), true);
+    Max = llvm::APSInt(LHS.To().usub_ov(RHS.From(), HasMaxOverflowed), true);
+  } else {
+    Min = llvm::APSInt(LHS.From().ssub_ov(RHS.To(), HasMinOverflowed), false);
+    Max = llvm::APSInt(LHS.To().ssub_ov(RHS.From(), HasMaxOverflowed), false);
+  }
+
+  // If no overflow occured then the range [Min, Max] is correct
+  if (!HasMinOverflowed && !HasMaxOverflowed) {
+    return {RangeFactory, ValueFactory.getValue(Min),
+            ValueFactory.getValue(Max)};
+  }
+
+  // In case of only one overflow, the two possibilities are:
+  //  1. The overflowing value overlaps the other boundary value, in which case,
+  //     the range is entire range set [Tmin, Tmax]
+  //  2. The values do not get overlapped, which results in segmented ranges
+  //     [Tmin, Max] U [Min, Tmax]
+  if (HasMinOverflowed ^ HasMaxOverflowed) {
+    if (Min > Max) {
+      RangeSet Result(RangeFactory, Tmin, ValueFactory.getValue(Max));
+      return RangeFactory.add(Result,
+                              {RangeFactory, ValueFactory.getValue(Min), Tmax});
+    }
+    return {RangeFactory, Tmin, Tmax};
+  }
+
+  // Consider, two unsigned values a, b, and we know that:
+  //    0 <= a, b <= Tmax
+  // Hence, (a - b) > Tmax can never occur mathematically. So, (a - b) will
+  // never overflow from Tmax-side.
+  // Now, Min and Max can only overflow from Tmin-side (or Zero-side) and hence
+  // the resulting range should be [Min, Max].
+  if (ResultType.isUnsigned()) {
+    return {RangeFactory, ValueFactory.getValue(Min),
+            ValueFactory.getValue(Max)};
+  }
+
+  // If both boundary values overflow on the same side then rangeset is
+  // [Min, Max]
+  if (((LHS.From() >= 0 && RHS.From() < 0) &&
+       (LHS.To() >= 0 && RHS.To() < 0)) ||
+      ((LHS.From() <= 0 && RHS.From() > 0) &&
+       (LHS.To() <= 0 && RHS.To() > 0))) {
+    return {RangeFactory, ValueFactory.getValue(Min),
+            ValueFactory.getValue(Max)};
+  }
+
+  // When both boundary values overflow from different sides then rangeset is
+  // [Tmin, Tmax] because the entire rangeset is already covered and overflow
+  // from opposite sides ensure already computed points to be reached again.
+  return {RangeFactory, Tmin, Tmax};
+}
+
 //===----------------------------------------------------------------------===//
 //                  Constraint manager implementation details
 //===----------------------------------------------------------------------===//
 
 static SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
   SValBuilder &SVB = State->getStateManager().getSValBuilder();
   SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
   return SimplifiedVal.getAsSymbol();

clang/test/Analysis/constant-folding.c

if (c >= HALF_INT_MAX - 10 && c <= HALF_INT_MAX + 10 &&
     // The resulting range for (c + d) will be:
     //   [INT_MIN, INT_MIN + 18] U [INT_MAX - 21, INT_MAX]
     clang_analyzer_eval((c + d) <= INT_MIN + 18); // expected-warning{{UNKNOWN}}
     clang_analyzer_eval((c + d) >= INT_MAX - 21); // expected-warning{{UNKNOWN}}
     clang_analyzer_eval((c + d) == INT_MIN + 19); // expected-warning{{FALSE}}
     clang_analyzer_eval((c + d) == INT_MAX - 22); // expected-warning{{FALSE}}
   }
 }
+
+void testSubtractionRules(unsigned int a, unsigned int b, int c, int d) {
+  // Checks when Max overflows but encompasses entire rangeset
+  if (c <= 0 && d <= 0) {
+    // (c - d) = [INT_MIN, INT_MAX]
+    clang_analyzer_eval((c - d) <= 0); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval((c - d) >= 0); // expected-warning{{UNKNOWN}}
+  }
+
+  // Checks when both limits overflow from the opposite ends
+  if (c >= INT_MIN + 40 && c <= INT_MAX - 40 && d >= -50 && d <= 50) {
+    // (c - d) = [INT_MIN, INT_MAX]
+    clang_analyzer_eval((c - d) <= 0); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval((c - d) >= 0); // expected-warning{{UNKNOWN}}
+  }
+
+  // Checks for non-overflowing ranges
+  if (a >= 10 && a <= 40 && b >= 5 && b <= 10) {
+    // (a - b) = [0, 35]
+    clang_analyzer_eval((a - b) <= 35); // expected-warning{{TRUE}}
+  }
+
+  if (c >= -10 && c <= 10 && d >= -20 && d <= 20) {
+    // (c - d) = [-30, 30]
+    clang_analyzer_eval((c - d) >= -30); // expected-warning{{TRUE}}
+    clang_analyzer_eval((c - d) <= 30); // expected-warning{{TRUE}}
+  }
+
+  // Check when Min overflows from lower bounded side
+  if (a <= 10 && b <= 10) {
+    // (a - b) = [0, 10] U [UINT_MAX - 9, UINT_MAX]
+    clang_analyzer_eval((a - b) != 11); // expected-warning{{TRUE}}
+    clang_analyzer_eval((a - b) != UINT_MAX - 10); // expected-warning{{TRUE}}
+  }
+
+  if (c <= 10 && d >= -30 && d <= 30) {
+    // (c - d) = [INT_MIN, 40] U [INT_MAX - 29, INT_MAX]
+    clang_analyzer_eval((c - d) != INT_MAX - 30); // expected-warning{{TRUE}}
+    clang_analyzer_eval((c - d) != 41); // expected-warning{{TRUE}}
+  }
+
+  // Checks when Max overflows from the upper bound side
+  if (a >= UINT_MAX - 10 && b >= UINT_MAX - 5) {
+    // (a - b) = [0, 5] U [UINT_MAX - 9, UINT_MAX]
+    clang_analyzer_eval((a - b) != 6); // expected-warning{{TRUE}}
+    clang_analyzer_eval((a - b) != UINT_MAX - 10); // expected-warning{{TRUE}}
+    clang_analyzer_eval((a - b) <= 5); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval((a - b) >= UINT_MAX - 9); // expected-warning{{UNKNOWN}}
+  }
+
+  if (c >= INT_MAX - 5 && d >= INT_MAX - 5) {
+    // (c - d) = [-5, 5]
+    clang_analyzer_eval((c - d) < -5 ); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c - d) > 5 ); // expected-warning{{FALSE}}
+  }
+
+  // Checks for Min and Max overflowing from same end
+  if (a <= 50 && b >= 60 && b <= 100) {
+    // (a - b) = [UINT_MAX - 99, UINT_MAX - 9]
+    clang_analyzer_eval((a - b) > UINT_MAX - 9); // expected-warning{{FALSE}}
+    clang_analyzer_eval((a - b) < UINT_MAX - 99); // expected-warning{{FALSE}}
+  }
+
+  if (c <= INT_MIN + 50 && d >= INT_MIN + 60 && d <= INT_MIN + 100) {
+    // (c - d) = [-100, -10]
+    clang_analyzer_eval((c - d) > -10); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c - d) < -100); // expected-warning{{FALSE}}
+  }
+
+  if (c >= INT_MAX - 50 && d >= INT_MIN + 70 && d <= INT_MIN + 90) {
+    // (c - d) = [-141, -71]
+    clang_analyzer_eval((c - d) < -141); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c - d) > -71); // expected-warning{{FALSE}}
+  }
+}