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 ++/--.


git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@69741 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 25 insertions, 1 deletions

diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp
index d00bfe640a..4b540e78d5 100644
--- a/lib/Analysis/GRExprEngine.cpp
+++ b/lib/Analysis/GRExprEngine.cpp
@@ -2674,9 +2674,33 @@ void GRExprEngine::VisitUnaryOperator(UnaryOperator* U, NodeTy* Pred,
       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);