baloghadamsoftware updated this revision to Diff 292755.
baloghadamsoftware added a comment.

Crash fixed and new tests added.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D77792/new/

https://reviews.llvm.org/D77792

Files:
  
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-manager-sym-sym.c

Index: clang/test/Analysis/constraint-manager-sym-sym.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/constraint-manager-sym-sym.c
@@ -0,0 +1,206 @@
+// RUN: %clang_analyze_cc1 -verify -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+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__))
+
+// Given [a1,a2] and [b1,b2] intervals.
+// Pin the [b1,b2] interval to eg. [5,10]
+// Choose the a1,a2 points from 0,2,5,7,10,12 where a1 < a2.
+// There will be 5+4+3+2+1 cases.
+
+// [0,2] and [5,10]
+void test_range1(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 2);
+  clang_analyzer_eval(l < r);  // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// [0,5] and [5,10]
+void test_range2(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 5);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,7] and [5,10]
+void test_range3(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,10] and [5,10]
+void test_range4(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,12] and [5,10]
+void test_range5(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,5] and [5,10] omitted because it is the same as the '[0,5] and [5,10]'
+
+// [2,7] and [5,10]
+void test_range7(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,10] and [5,10]
+void test_range8(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,12] and [5,10]
+void test_range9(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,7] and [5,10]
+void test_range10(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,10] and [5,10]
+void test_range11(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,12] and [5,10]
+void test_range12(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [7,10] and [5,10]
+void test_range13(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(7 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [7,12] and [5,10]
+void test_range14(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(7 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [10,12] and [5,10]
+void test_range15(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(7 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// {[0,1],[5,6]} and {[9,9],[11,42],[44,44]}
+void test_range16(int l, int r) {
+  assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));
+  assert((0 <= l && l <= 1) || (5 <= l && l <= 6));
+  clang_analyzer_eval(l < r);  // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// {[0,1],[5,10]} and {[9,9],[11,42],[44,44]}
+void test_range17(int l, int r) {
+  assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));
+  assert((0 <= l && l <= 1) || (5 <= l && l <= 10));
+
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}} expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}} expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}} expected-warning{{FALSE}}
+}
+
+// {[0,1],[20,20]} and {[9,9],[11,42],[44,44]}
+void test_range18(int l, int r) {
+  assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));
+  assert((0 <= l && l <= 1) || (20 <= l && l <= 20));
+
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}} expected-warning{{TRUE}} expected-warning{{FALSE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}} expected-warning{{FALSE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}} expected-warning{{TRUE}} expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}} expected-warning{{FALSE}}
+}
+
+
+#define INT_MIN (- (int)(((unsigned) 0 - 1) / 2) - 1)
+
+void test_difference1(int k, int l, int m, int n) {
+  assert(k - l > INT_MIN);
+  assert(k - l <= 10);
+  assert(l - k <= 0);
+  // This means that k - l is from [0..10], l - k is from [-10..0]
+  assert(m - n >= -20);
+  assert(n - m > 10);
+  // This means that m - n is from [-20..-11], n - m is from [11..20]
+  clang_analyzer_eval(k - l < n - m); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l - k < n - m); // expected-warning{{TRUE}}
+  clang_analyzer_eval(k - l < m - n); // expected-warning{{FALSE}}
+  clang_analyzer_eval(l - k < m - n); // expected-warning{{FALSE}}
+}
Index: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -43,7 +43,7 @@
     BinaryOperator::Opcode Op = SSE->getOpcode();
     assert(BinaryOperator::isComparisonOp(Op));
 
-    // We convert equality operations for pointers only.
+    // We support comparing pointers and... (TODO!!!)
     if (Loc::isLocType(SSE->getLHS()->getType()) &&
         Loc::isLocType(SSE->getRHS()->getType())) {
       // Translate "a != b" to "(b - a) != 0".
@@ -83,6 +83,15 @@
 
       return assumeSymEQ(State, CanonicalEquality, Zero, Zero);
     }
+
+    // We also support constrained symbols, which don't have any overlapping
+    // range intervals. Eg. {[0,1],[5,6]} < {[9,9],[11,42],[44,44]}
+    if (SSE->getLHS()->getType()->isIntegralOrEnumerationType() &&
+        SSE->getRHS()->getType()->isIntegralOrEnumerationType()) {
+      if (auto OptionalState = tryAssumeSymSymOp(State, Op, SSE->getLHS(),
+                                                 SSE->getRHS(), Assumption))
+        return OptionalState.getValue();
+    }
   }
 
   // If we get here, there's nothing else we can do but treat the symbol as
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -24,6 +24,45 @@
 using namespace clang;
 using namespace ento;
 
+RangeSet::CompareResult RangeSet::compare(const RangeSet &other) const {
+  if (isEmpty() || other.isEmpty())
+    return CompareResult::unknown;
+
+  const int LMaxRMin =
+      llvm::APSInt::compareValues(getMaxValue(), other.getMinValue());
+  const int LMinRMax =
+      llvm::APSInt::compareValues(getMinValue(), other.getMaxValue());
+
+  // {-1,0,1}x{-1,0,1} has 9 combinations, so we will enumerate all of them.
+  // Given [a0,a1] and [b0,b1] ranges.
+  // Assuming that a0 <= a1 and b0 <= b1 (since ranges...)
+  // Than we examine the 'a1 <? b0' and the 'a0 <? b1' comparisons.
+  // Eg. if a1 <? b0 is -1, that means that a1 < b0; zero for equality; etc.
+  // Solving these 9 inequality systems we draw some conclusion and find some
+  // impossible cases (which are not satisfiable with any valid ranges).
+  if (LMaxRMin == -1 && LMinRMax == -1)
+    return CompareResult::less;
+  if (LMaxRMin == -1 && LMinRMax == 0)
+    llvm_unreachable("Impossible.");
+  if (LMaxRMin == -1 && LMinRMax == 1)
+    llvm_unreachable("Impossible.");
+
+  if (LMaxRMin == 0 && LMinRMax == -1)
+    return CompareResult::less_equal;
+  if (LMaxRMin == 0 && LMinRMax == 0)
+    return CompareResult::identical;
+  if (LMaxRMin == 0 && LMinRMax == 1)
+    llvm_unreachable("Impossible.");
+
+  if (LMaxRMin == 1 && LMinRMax == -1)
+    return CompareResult::unknown;
+  if (LMaxRMin == 1 && LMinRMax == 0)
+    return CompareResult::greater_equal;
+  assert(LMaxRMin == 1 && LMinRMax == 1);
+  return CompareResult::greater;
+}
+
+
 // This class can be extended with other tables which will help to reason
 // about ranges more precisely.
 class OperatorRelationsTable {
@@ -1321,6 +1360,12 @@
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
+  Optional<ProgramStateRef> tryAssumeSymSymOp(ProgramStateRef State,
+                                              BinaryOperator::Opcode Op,
+                                              SymbolRef LHSSym,
+                                              SymbolRef RHSSym,
+                                              bool Assumption) override;
+
 private:
   RangeSet::Factory F;
 
@@ -1821,13 +1866,17 @@
       // FIXME: Handle <=> here.
       if (BinaryOperator::isEqualityOp(SSE->getOpcode()) ||
           BinaryOperator::isRelationalOp(SSE->getOpcode())) {
-        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
-        // We've recently started producing Loc <> NonLoc comparisons (that
-        // result from casts of one of the operands between eg. intptr_t and
-        // void *), but we can't reason about them yet.
+        // We handle Loc <> Loc comparisons.
         if (Loc::isLocType(SSE->getLHS()->getType())) {
           return Loc::isLocType(SSE->getRHS()->getType());
         }
+
+        // We can handle certain NonLoc <> NonLoc comparisons, when the
+        // corresponding RangeSets are non-overlapping.
+        // We've recently started producing Loc <> NonLoc comparisons (that
+        // result from casts of one of the operands between eg. intptr_t and
+        // void *), but we can't reason about them yet.
+        return true;
       }
     }
 
@@ -2241,6 +2290,64 @@
   return New.isEmpty() ? nullptr : setConstraint(State, Sym, New);
 }
 
+Optional<ProgramStateRef> RangeConstraintManager::tryAssumeSymSymOp(
+    ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,
+    SymbolRef RHSSym, bool Assumption) {
+  // FIXME: In C++20? replace with 'using RangeSet::CompareResult;'
+  using CR = RangeSet::CompareResult;
+  constexpr auto unknown = CR::unknown;
+  constexpr auto identical = CR::identical;
+  constexpr auto less = CR::less;
+  constexpr auto greater = CR::greater;
+  constexpr auto less_equal = CR::less_equal;
+  constexpr auto greater_equal = CR::greater_equal;
+
+  const auto InfeasibleState = Optional<ProgramStateRef>{nullptr};
+
+  const RangeSet LHSRange = getRange(State, LHSSym);
+  const RangeSet RHSRange = getRange(State, RHSSym);
+  const RangeSet::CompareResult Res = LHSRange.compare(RHSRange);
+
+  if (Res == unknown)
+    return llvm::None;
+
+  if (!Assumption)
+    Op = BinaryOperator::negateComparisonOp(Op);
+
+  switch (Op) {
+  case BO_LT:
+    if (Res == less)
+      return State;
+    if (Res == identical || Res == greater_equal || Res == greater)
+      return InfeasibleState;
+    assert(Res == less_equal);
+    return llvm::None;
+  case BO_GT:
+    if (Res == greater)
+      return State;
+    if (Res == identical || Res == less_equal || Res == less)
+      return InfeasibleState;
+    assert(Res == greater_equal);
+    return llvm::None;
+  case BO_LE:
+    if (Res == identical || Res == less_equal || Res == less)
+      return State;
+    if (Res == greater)
+      return InfeasibleState;
+    assert(Res == greater_equal);
+    return llvm::None;
+  case BO_GE:
+    if (Res == identical || Res == greater_equal || Res == greater)
+      return State;
+    if (Res == less)
+      return InfeasibleState;
+    assert(Res == less_equal);
+    return llvm::None;
+  default:
+    llvm_unreachable("Should not reach this with any other operators.");
+  }
+}
+
 //===----------------------------------------------------------------------===//
 // Pretty-printing.
 //===----------------------------------------------------------------------===//
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -107,6 +107,20 @@
     return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
   }
 
+  enum class CompareResult {
+    unknown,
+    identical,
+    less,
+    less_equal,
+    greater,
+    greater_equal
+  };
+
+  // 'a < b' is true if the maximum value of 'a' is still (strictly) less than
+  // the minimum value of 'b'. The same logic applies for <=,>,>=,== operators.
+  // If there is no clear relation between the two RangeSet returns unknown.
+  CompareResult compare(const RangeSet &other) const;
+
   /// Get a minimal value covered by the ranges in the set
   const llvm::APSInt &getMinValue() const;
   /// Get a maximal value covered by the ranges in the set
@@ -206,6 +220,10 @@
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
 
+  virtual Optional<ProgramStateRef>
+  tryAssumeSymSymOp(ProgramStateRef State, BinaryOperator::Opcode Op,
+                    SymbolRef LHSSym, SymbolRef RHSSym, bool Assumption) = 0;
+
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to