[cfe-commits] r69741 - in /cfe/trunk: lib/Analysis/GRExprEngine.cpp test/Analysis/misc-ps.m

[Ted Kremenek]

Author: kremenek
Date: Tue Apr 21 17:38:05 2009
New Revision: 69741

URL: http://llvm.org/viewvc/llvm-project?rev=69741&view=rev
Log:
Fix: <rdar://problem/6777209> false Dereference of null pointer in loop: pointer increment/decrement preserves non-nullness

When the StoreManager doesn't reason well about pointer-arithmetic, propagate
the non-nullness constraint on a pointer value when performing pointer
arithmetic uisng ++/--.

Modified:
    cfe/trunk/lib/Analysis/GRExprEngine.cpp
    cfe/trunk/test/Analysis/misc-ps.m

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

==============================================================================
--- cfe/trunk/lib/Analysis/GRExprEngine.cpp (original)
+++ cfe/trunk/lib/Analysis/GRExprEngine.cpp Tue Apr 21 17:38:05 2009
@@ -2674,9 +2674,33 @@
       SVal Result = EvalBinOp(Op, V2, MakeConstantVal(1U, U), U->getType());    
       
       // Conjure a new symbol if necessary to recover precision.
-      if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result))
+      if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result)){
         Result = ValMgr.getConjuredSymbolVal(Ex,
                                              Builder->getCurrentBlockCount());
+        
+        // If the value is a location, ++/-- should always preserve
+        // non-nullness.  Check if the original value was non-null, and if so propagate
+        // that constraint.        
+        if (Loc::IsLocType(U->getType())) {
+          SVal Constraint = EvalBinOp(BinaryOperator::EQ, V2,
+                                      ValMgr.makeZeroVal(U->getType()),
+                                      getContext().IntTy);          
+          
+          bool isFeasible = false;
+          Assume(state, Constraint, true, isFeasible);
+          if (!isFeasible) {
+            // It isn't feasible for the original value to be null.
+            // Propagate this constraint.
+            Constraint = EvalBinOp(BinaryOperator::EQ, Result,
+                                   ValMgr.makeZeroVal(U->getType()),
+                                   getContext().IntTy);
+            
+            bool isFeasible = false;
+            state = Assume(state, Constraint, false, isFeasible);
+            assert(isFeasible && state);
+          }            
+        }        
+      }
       
       state = BindExpr(state, U, U->isPostfix() ? V2 : Result);
 

Modified: cfe/trunk/test/Analysis/misc-ps.m
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/misc-ps.m?rev=69741&r1=69740&r2=69741&view=diff

==============================================================================
--- cfe/trunk/test/Analysis/misc-ps.m (original)
+++ cfe/trunk/test/Analysis/misc-ps.m Tue Apr 21 17:38:05 2009
@@ -245,3 +245,18 @@
   *p = 1; // expected-warning{{Dereference of null pointer}}  
 }
 
+// For pointer arithmetic, --/++ should be treated as preserving non-nullness,
+// regardless of how well the underlying StoreManager reasons about pointer
+// arithmetic.
+// <rdar://problem/6777209>
+
+void rdar_6777209(char *p) {
+  if (p == 0)
+    return;
+  
+  ++p;
+  
+  // This branch should always be infeasible.
+  if (p == 0)
+    *p = 'c'; // no-warning
+}