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

[Ted Kremenek]

Author: kremenek
Date: Fri Sep 19 13:00:36 2008
New Revision: 56354

URL: http://llvm.org/viewvc/llvm-project?rev=56354&view=rev
Log:
Fixed logic error in BasicConstraintManager pointed out by Zhongxing Xu.

For checking if a symbol >= value, we need to check if symbol == value || symbol
> value. When checking symbol > value and we know that symbol != value, the path
is infeasible only if value == maximum integer.

For checking if a symbol <= value, we need to check if symbol == value || symbol
< value. When checking symbol < value and we know that symbol != value, the path
is infeasible only if value == minimum integer.

Updated test case exercising this logic: we only prune paths if the values are
unsigned.

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=56354&r1=56353&r2=56354&view=diff

==============================================================================
--- cfe/trunk/lib/Analysis/BasicConstraintManager.cpp (original)
+++ cfe/trunk/lib/Analysis/BasicConstraintManager.cpp Fri Sep 19 13:00:36 2008
@@ -320,24 +320,9 @@
     return St;
   }
 
-  // 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;
-
+  isFeasible = !isNotEqual(St, sym, V) || 
+               (V != llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned()));
+                
   return St;
 }
 
@@ -352,8 +337,10 @@
     isFeasible = *X <= V;
     return St;
   }
-
-  isFeasible = true;
+  
+  isFeasible = !isNotEqual(St, sym, V) || 
+               (V != llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned()));
+  
   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=56354&r1=56353&r2=56354&view=diff

==============================================================================
--- cfe/trunk/test/Analysis/null-deref-ps.c (original)
+++ cfe/trunk/test/Analysis/null-deref-ps.c Fri Sep 19 13:00:36 2008
@@ -91,21 +91,21 @@
 
 int* qux();
 
-int f9(int len) {
+int f9(unsigned len) {
   assert (len != 0);
   int *p = 0;
 
-  for (int i = 0; i < len; ++i)
+  for (unsigned i = 0; i < len; ++i)
    p = qux(i);
 
   return *p++; // no-warning
 }
 
-int f9b(int len) {
+int f9b(unsigned len) {
   assert (len > 0);  // note use of '>'
   int *p = 0;
 
-  for (int i = 0; i < len; ++i)
+  for (unsigned i = 0; i < len; ++i)
    p = qux(i);
 
   return *p++; // no-warning