From 8c3e7fbae6f61f87000f1edd59bb2379abf3d7e0 Mon Sep 17 00:00:00 2001
From: Ted Kremenek <kremenek@apple.com>
Date: Tue, 16 Sep 2008 23:24:45 +0000
Subject: [PATCH] Minor pass-sensitivity improvement:   if we know that 'len !=
 0' and know that 'i == 0' then we know that   'i < len' must evaluate to true
 and cannot evaluate to false

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

diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp
index ca97f930dd..2edbd80341 100644
--- a/lib/Analysis/BasicConstraintManager.cpp
+++ b/lib/Analysis/BasicConstraintManager.cpp
@@ -228,6 +228,12 @@ BasicConstraintManager::AssumeSymInt(const GRState* St, bool Assumption,
     else
       return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
 
+  case BinaryOperator::LT:
+    if (Assumption)
+      return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
+    else
+      return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
+      
   case BinaryOperator::LE:
     if (Assumption)
       return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
@@ -302,15 +308,30 @@ const GRState*
 BasicConstraintManager::AssumeSymGE(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 = true;
+  // 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;
+
   return St;
 }
 
diff --git a/test/Analysis/null-deref-ps.c b/test/Analysis/null-deref-ps.c
index 06f67da45a..a6819cc48b 100644
--- a/test/Analysis/null-deref-ps.c
+++ b/test/Analysis/null-deref-ps.c
@@ -1,6 +1,7 @@
 // RUN: clang -checker-simple -verify %s
 
 #include<stdint.h>
+#include <assert.h>
 
 void f1(int *p) {  
   if (p) *p = 1;
@@ -87,3 +88,15 @@ int f8(int *p, int *q) {
     if (!q)
       *q = 1; // no-warning
 }
+
+int* qux();
+
+int f9(int len) {
+  assert (len != 0);
+  int *p = 0;
+
+  for (int i = 0; i < len; ++i)
+   p = foo(i);
+
+  return *p++; // no-warning
+}
-- 
2.40.0