[analyzer] Also transform "a < b" to "(b - a) > 0" in the constraint manager.

We can support the full range of comparison operations between two locations
by canonicalizing them as subtraction, as in the previous commit.

This won't work (well) if either location includes an offset, or (again)
if the comparisons are not consistent about which region comes first.

<rdar://problem/13239003>

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@177803 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index d87c51fed358ed53ba9fcc7451f60d75d7ccb490..4ff248785a55825d3028134aed02c07da610f5bd 100644 (file)
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -50,7 +50,7 @@ bool SimpleConstraintManager::canReasonAbout(SVal X) const {
     }
 
     if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
-      if (SSE->getOpcode() == BO_EQ || SSE->getOpcode() == BO_NE)
+      if (BinaryOperator::isComparisonOp(SSE->getOpcode()))
         return true;
     }
 
@@ -180,26 +180,28 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
       }
 
     } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) {
-      BinaryOperator::Opcode Op = SSE->getOpcode();
-
       // Translate "a != b" to "(b - a) != 0".
       // We invert the order of the operands as a heuristic for how loop
       // conditions are usually written ("begin != end") as compared to length
       // calculations ("end - begin"). The more correct thing to do would be to
       // canonicalize "a - b" and "b - a", which would allow us to treat
       // "a != b" and "b != a" the same.
-      if (BinaryOperator::isEqualityOp(Op)) {
-        SymbolManager &SymMgr = getSymbolManager();
-
-        assert(Loc::isLocType(SSE->getLHS()->getType()));
-        assert(Loc::isLocType(SSE->getRHS()->getType()));
-        QualType DiffTy = SymMgr.getContext().getPointerDiffType();
-        SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
-                                                     SSE->getLHS(), DiffTy);
-
-        Assumption ^= (SSE->getOpcode() == BO_EQ);
-        return assumeAuxForSymbol(state, Subtraction, Assumption);
-      }
+      SymbolManager &SymMgr = getSymbolManager();
+      BinaryOperator::Opcode Op = SSE->getOpcode();
+      assert(BinaryOperator::isComparisonOp(Op));
+
+      // For now, we only support comparing pointers.
+      assert(Loc::isLocType(SSE->getLHS()->getType()));
+      assert(Loc::isLocType(SSE->getRHS()->getType()));
+      QualType DiffTy = SymMgr.getContext().getPointerDiffType();
+      SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
+                                                   SSE->getLHS(), DiffTy);
+
+      const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
+      Op = BinaryOperator::reverseComparisonOp(Op);
+      if (!Assumption)
+        Op = BinaryOperator::negateComparisonOp(Op);
+      return assumeSymRel(state, Subtraction, Op, Zero);
     }
 
     // If we get here, there's nothing else we can do but treat the symbol as

diff --git a/test/Analysis/ptr-arith.c b/test/Analysis/ptr-arith.c
index d9c5a0ff999442a05638a614a662e60688e1088e..35faff4a170978e1c7083b4f5b2c085a0db07da3 100644 (file)
--- a/test/Analysis/ptr-arith.c
+++ b/test/Analysis/ptr-arith.c
@@ -204,6 +204,50 @@ void zero_implies_equal(int *lhs, int *rhs) {
   clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
 }
 
+void comparisons_imply_size(int *lhs, int *rhs) {
+  clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
+
+  if (lhs > rhs) {
+    clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
+    return;
+  }
+
+  clang_analyzer_eval(lhs <= rhs); // expected-warning{{TRUE}}
+  clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
+
+  if (lhs >= rhs) {
+    clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{TRUE}}
+    return;
+  }
+
+  clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+  clang_analyzer_eval(lhs < rhs); // expected-warning{{TRUE}}
+  clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
+}
+
+void size_implies_comparison(int *lhs, int *rhs) {
+  clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
+
+  if ((rhs - lhs) < 0) {
+    clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+    return;
+  }
+
+  clang_analyzer_eval(lhs <= rhs); // expected-warning{{TRUE}}
+  clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
+
+  if ((rhs - lhs) <= 0) {
+    clang_analyzer_eval(lhs == rhs); // expected-warning{{TRUE}}
+    return;
+  }
+
+  clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+  clang_analyzer_eval(lhs < rhs); // expected-warning{{TRUE}}
+  clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
+}
+
 //-------------------------------
 // False positives
 //-------------------------------