From 73abd133aeda75971212176b1b4f7f251976d7cf Mon Sep 17 00:00:00 2001
From: Ted Kremenek <kremenek@apple.com>
Date: Wed, 3 Dec 2008 18:56:12 +0000
Subject: [PATCH] BasicConstraintManager: - Fix nonsensical logic in
 AssumeSymLE. When comparing 'sym <= constant' and the   constant is the
 minimum integer value, add the constraint that 'sym ==   constant' when the
 path is deemed feasible.  All other cases are feasible. - Improve AssumeSymLT
 to address <rdar://problem/6407949>.  When comparing   'sym < constant' and
 constant is the minimum integer value we know the   path is infeasible. - Add
 test case for <rdar://problem/6407949>.

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@60489 91177308-0d34-0410-b5e6-96231b3b80d8
---
 lib/Analysis/BasicConstraintManager.cpp | 30 ++++++++++++++++++++-----
 test/Analysis/null-deref-ps.c           | 10 +++++++++
 2 files changed, 34 insertions(+), 6 deletions(-)

diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp
index 5ce95a1e56..c8065d1869 100644
--- a/lib/Analysis/BasicConstraintManager.cpp
+++ b/lib/Analysis/BasicConstraintManager.cpp
@@ -312,6 +312,13 @@ BasicConstraintManager::AssumeSymEQ(const GRState* St, SymbolID sym,
 const GRState*
 BasicConstraintManager::AssumeSymLT(const GRState* St, SymbolID sym,
                                     const llvm::APSInt& V, bool& isFeasible) {
+  
+  // Is 'V' the smallest possible value?
+  if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned())) {
+    // sym cannot be any value less 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);
@@ -345,17 +352,28 @@ const GRState*
 BasicConstraintManager::AssumeSymLE(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 = !isNotEqual(St, sym, V) || 
-               (V != llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned()));
-  
+  // Sym is not a constant, but it is worth looking to see if V is the
+  // minimum integer value.
+  if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned())) {
+    // If we know that sym != V, then this condition is infeasible since
+    // there is no other value less 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 smaller values).
+    // Add this constraint.
+    if (isFeasible)
+      return AddEQ(St, sym, V);
+  }
+  else
+    isFeasible = true;
+    
   return St;
 }
 
diff --git a/test/Analysis/null-deref-ps.c b/test/Analysis/null-deref-ps.c
index c9477566cb..eb6062b981 100644
--- a/test/Analysis/null-deref-ps.c
+++ b/test/Analysis/null-deref-ps.c
@@ -134,3 +134,13 @@ int* f10(int* p, signed char x, int y) {
   return p;
 }
 
+// Test case from <rdar://problem/6407949>
+void f11(unsigned i) {
+  int *x = 0;
+  if (i >= 0) {
+    // always true
+  } else {
+    *x = 42; // no-warning
+  }
+}
+
-- 
2.40.0