[cfe-commits] r56260 - in /cfe/trunk: lib/Analysis/BasicConstraintManager.cpp test/Analysis/null-deref-ps.c

[Ted Kremenek]

Author: kremenek
Date: Tue Sep 16 18:24:45 2008
New Revision: 56260

URL: http://llvm.org/viewvc/llvm-project?rev=56260&view=rev
Log:
Minor pass-sensitivity improvement:
  if we know that 'len != 0' and know that 'i == 0' then we know that
  'i < len' must evaluate to true and cannot evaluate to false

Modified:
    cfe/trunk/lib/Analysis/BasicConstraintManager.cpp
    cfe/trunk/test/Analysis/null-deref-ps.c

Modified: cfe/trunk/lib/Analysis/BasicConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/BasicConstraintManager.cpp?rev=56260&r1=56259&r2=56260&view=diff

==============================================================================
--- cfe/trunk/lib/Analysis/BasicConstraintManager.cpp (original)
+++ cfe/trunk/lib/Analysis/BasicConstraintManager.cpp Tue Sep 16 18:24:45 2008
@@ -228,6 +228,12 @@
     else
       return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
 
+  case BinaryOperator::LT:
+    if (Assumption)
+      return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
+    else
+      return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
+      
   case BinaryOperator::LE:
     if (Assumption)
       return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
@@ -302,15 +308,30 @@
 BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym,
                                     const llvm::APSInt& V, bool& isFeasible) {
 
-  // FIXME: Primitive logic for now.  Only reject a path if the value of
-  //  sym is a constant X and !(X >= V).
-
+  // Reject a path if the value of sym is a constant X and !(X >= V).
   if (const llvm::APSInt* X = getSymVal(St, sym)) {
     isFeasible = *X >= V;
     return St;
   }
 
-  isFeasible = true;
+  // sym is not a constant, but it might be not-equal to a constant.
+  // Observe: V >= sym is the same as sym <= V.
+  //  check: is sym != V?
+  //  check: is sym > V?
+  // if both are true, the path is infeasible.
+  
+  if (isNotEqual(St, sym, V)) {
+    // Is sym > V?
+    //
+    //  We're not doing heavy range analysis yet, so all we can accurately
+    //  reason about are the edge cases.
+    //
+    //  If V == 0, since we know that sym != V, we also know that sym > V.    
+    isFeasible = V != 0;
+  }
+  else
+    isFeasible = true;
+
   return St;
 }
 

Modified: cfe/trunk/test/Analysis/null-deref-ps.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/null-deref-ps.c?rev=56260&r1=56259&r2=56260&view=diff

==============================================================================
--- cfe/trunk/test/Analysis/null-deref-ps.c (original)
+++ cfe/trunk/test/Analysis/null-deref-ps.c Tue Sep 16 18:24:45 2008
@@ -1,6 +1,7 @@
 // RUN: clang -checker-simple -verify %s
 
 #include<stdint.h>
+#include <assert.h>
 
 void f1(int *p) {  
   if (p) *p = 1;
@@ -87,3 +88,15 @@
     if (!q)
       *q = 1; // no-warning
 }
+
+int* qux();
+
+int f9(int len) {
+  assert (len != 0);
+  int *p = 0;
+
+  for (int i = 0; i < len; ++i)
+   p = foo(i);
+
+  return *p++; // no-warning
+}