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

[Ted Kremenek]

Author: kremenek
Date: Wed Dec  3 13:06:30 2008
New Revision: 60490

URL: http://llvm.org/viewvc/llvm-project?rev=60490&view=rev
Log:
BasicConstraintManager:
- Fix nonsensical logic in AssumeSymGE. When comparing 'sym >= constant' and the
  constant is the maximum integer value, add the constraint that 'sym ==
  constant' when the path is deemed feasible.  All other cases are feasible.
- Improve AssumeSymGT. When comparing 'sym > constant' and constant is the
  maximum integer value we know the path is infeasible.
- Add test case for this enhancement to AssumeSymGT.

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=60490&r1=60489&r2=60490&view=diff

==============================================================================
--- cfe/trunk/lib/Analysis/BasicConstraintManager.cpp (original)
+++ cfe/trunk/lib/Analysis/BasicConstraintManager.cpp Wed Dec  3 13:06:30 2008
@@ -328,6 +328,13 @@
 BasicConstraintManager::AssumeSymGT(const GRState* St, SymbolID sym,
                                     const llvm::APSInt& V, bool& isFeasible) {
 
+  // Is 'V' the largest possible value?
+  if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned())) {
+    // sym cannot be any value greater than 'V'.  This path is infeasible.
+    isFeasible = false;
+    return St;
+  }
+
   // FIXME: For now have assuming x > y be the same as assuming sym != V;
   return AssumeSymNE(St, sym, V, isFeasible);
 }
@@ -341,10 +348,23 @@
     isFeasible = *X >= V;
     return St;
   }
+  
+  // Sym is not a constant, but it is worth looking to see if V is the
+  // maximum integer value.
+  if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned())) {
+    // If we know that sym != V, then this condition is infeasible since
+    // there is no other value greater than V.    
+    isFeasible = !isNotEqual(St, sym, V);
+    
+    // If the path is still feasible then as a consequence we know that
+    // 'sym == V' because we cannot have 'sym > V' (no larger values).
+    // Add this constraint.
+    if (isFeasible)
+      return AddEQ(St, sym, V);
+  }
+  else
+    isFeasible = true;
 
-  isFeasible = !isNotEqual(St, sym, V) || 
-               (V != llvm::APSInt::getMaxValue(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=60490&r1=60489&r2=60490&view=diff

==============================================================================
--- cfe/trunk/test/Analysis/null-deref-ps.c (original)
+++ cfe/trunk/test/Analysis/null-deref-ps.c Wed Dec  3 13:06:30 2008
@@ -144,3 +144,12 @@
   }
 }
 
+void f11b(unsigned i) {
+  int *x = 0;
+  if (i <= ~(unsigned)0) {
+    // always true
+  } else {
+    *x = 42; // no-warning
+  }
+}
+