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

[Jordan Rose]

Author: jrose
Date: Fri Mar 22 20:21:23 2013
New Revision: 177803

URL: http://llvm.org/viewvc/llvm-project?rev=177803&view=rev
Log:
[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>

Modified:
    cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
    cfe/trunk/test/Analysis/ptr-arith.c

Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp?rev=177803&r1=177802&r2=177803&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp Fri Mar 22 20:21:23 2013
@@ -50,7 +50,7 @@ bool SimpleConstraintManager::canReasonA
     }
 
     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:
       }
 
     } 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);
+      SymbolManager &SymMgr = getSymbolManager();
+      BinaryOperator::Opcode Op = SSE->getOpcode();
+      assert(BinaryOperator::isComparisonOp(Op));
 
-        Assumption ^= (SSE->getOpcode() == BO_EQ);
-        return assumeAuxForSymbol(state, Subtraction, Assumption);
-      }
+      // 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

Modified: cfe/trunk/test/Analysis/ptr-arith.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/ptr-arith.c?rev=177803&r1=177802&r2=177803&view=diff
==============================================================================
--- cfe/trunk/test/Analysis/ptr-arith.c (original)
+++ cfe/trunk/test/Analysis/ptr-arith.c Fri Mar 22 20:21:23 2013
@@ -204,6 +204,50 @@ void zero_implies_equal(int *lhs, int *r
   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
 //-------------------------------