From: Ted Kremenek <kremenek@apple.com>
Date: Thu, 7 Aug 2008 22:30:22 +0000 (+0000)
Subject: Added AssumeSymGT, AssumeSymGE, AssumeSymLT, AssumeSymLE to add some minor improvemen... 
X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=2619be072ccc6a722278d1ec39b98eae068d3da3;p=clang

Added AssumeSymGT, AssumeSymGE, AssumeSymLT, AssumeSymLE to add some minor improvements to path-sensitivity.  Right now we basically treat 'x > y' and 'x < y' as implying 'x != y', but this restriction will only inevitably apply to our must rudimentary value tracking component (we'll implement more advanced value reasoning later).


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

diff --git a/include/clang/Analysis/PathSensitive/ValueState.h b/include/clang/Analysis/PathSensitive/ValueState.h
index 554e6f5f86..46f62e12eb 100644
--- a/include/clang/Analysis/PathSensitive/ValueState.h
+++ b/include/clang/Analysis/PathSensitive/ValueState.h
@@ -365,7 +365,6 @@ public:
   const ValueState* AddNE(const ValueState* St, SymbolID sym,
                           const llvm::APSInt& V);
   
-  
   bool isEqual(const ValueState* state, Expr* Ex, const llvm::APSInt& V);
   bool isEqual(const ValueState* state, Expr* Ex, uint64_t);
   
@@ -397,6 +396,9 @@ private:
   
   const ValueState* AssumeAux(const ValueState* St, NonLVal Cond,
                               bool Assumption, bool& isFeasible);
+    
+  const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,                                 
+                                 const SymIntConstraint& C, bool& isFeasible);
   
   const ValueState* AssumeSymNE(const ValueState* St, SymbolID sym,
                                 const llvm::APSInt& V, bool& isFeasible);
@@ -404,8 +406,17 @@ private:
   const ValueState* AssumeSymEQ(const ValueState* St, SymbolID sym,
                                 const llvm::APSInt& V, bool& isFeasible);
   
-  const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
-                                 const SymIntConstraint& C, bool& isFeasible);
+  const ValueState* AssumeSymLT(const ValueState* St, SymbolID sym,
+                                const llvm::APSInt& V, bool& isFeasible);
+  
+  const ValueState* AssumeSymLE(const ValueState* St, SymbolID sym,
+                                const llvm::APSInt& V, bool& isFeasible);
+  
+  const ValueState* AssumeSymGT(const ValueState* St, SymbolID sym,
+                                const llvm::APSInt& V, bool& isFeasible);
+  
+  const ValueState* AssumeSymGE(const ValueState* St, SymbolID sym,
+                                const llvm::APSInt& V, bool& isFeasible);
 };
   
 } // end clang namespace
diff --git a/lib/Analysis/ValueState.cpp b/lib/Analysis/ValueState.cpp
index 1cf695438b..ffc4c28f2c 100644
--- a/lib/Analysis/ValueState.cpp
+++ b/lib/Analysis/ValueState.cpp
@@ -435,9 +435,52 @@ const ValueState* ValueStateManager::AssumeAux(const ValueState* St, NonLVal Con
   }
 }
 
-const ValueState* ValueStateManager::AssumeSymNE(const ValueState* St,
-                                            SymbolID sym, const llvm::APSInt& V,
-                                            bool& isFeasible) {
+
+
+const ValueState* ValueStateManager::AssumeSymInt(const ValueState* St,
+                                             bool Assumption,
+                                             const SymIntConstraint& C,
+                                             bool& isFeasible) {
+  
+  switch (C.getOpcode()) {
+    default:
+      // No logic yet for other operators.
+      isFeasible = true;
+      return St;
+      
+    case BinaryOperator::EQ:
+      if (Assumption)
+        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+      else
+        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
+      
+    case BinaryOperator::NE:
+      if (Assumption)
+        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
+      else
+        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+      
+    case BinaryOperator::GE:
+      if (Assumption)
+        return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
+      else
+        return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
+      
+    case BinaryOperator::LE:
+      if (Assumption)
+        return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
+      else
+        return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);    
+  }
+}
+
+//===----------------------------------------------------------------------===//
+// FIXME: This should go into a plug-in constraint engine.
+//===----------------------------------------------------------------------===//
+
+const ValueState*
+ValueStateManager::AssumeSymNE(const ValueState* St, SymbolID sym,
+                               const llvm::APSInt& V, bool& isFeasible) {
   
   // First, determine if sym == X, where X != V.
   if (const llvm::APSInt* X = St->getSymVal(sym)) {
@@ -458,8 +501,9 @@ const ValueState* ValueStateManager::AssumeSymNE(const ValueState* St,
   return AddNE(St, sym, V);
 }
 
-const ValueState* ValueStateManager::AssumeSymEQ(const ValueState* St, SymbolID sym,
-                                            const llvm::APSInt& V, bool& isFeasible) {
+const ValueState*
+ValueStateManager::AssumeSymEQ(const ValueState* St, SymbolID sym,
+                               const llvm::APSInt& V, bool& isFeasible) {
   
   // First, determine if sym == X, where X != V.
   if (const llvm::APSInt* X = St->getSymVal(sym)) {
@@ -480,27 +524,51 @@ const ValueState* ValueStateManager::AssumeSymEQ(const ValueState* St, SymbolID
   return AddEQ(St, sym, V);
 }
 
-const ValueState* ValueStateManager::AssumeSymInt(const ValueState* St,
-                                             bool Assumption,
-                                             const SymIntConstraint& C,
-                                             bool& isFeasible) {
+const ValueState*
+ValueStateManager::AssumeSymLT(const ValueState* St, SymbolID sym,
+                               const llvm::APSInt& V, bool& isFeasible) {
   
-  switch (C.getOpcode()) {
-    default:
-      // No logic yet for other operators.
-      isFeasible = true;
-      return St;
-      
-    case BinaryOperator::EQ:
-      if (Assumption)
-        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
-      else
-        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
-      
-    case BinaryOperator::NE:
-      if (Assumption)
-        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
-      else
-        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+  // FIXME: For now have assuming x < y be the same as assuming sym != V;
+  return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const ValueState*
+ValueStateManager::AssumeSymGT(const ValueState* St, SymbolID sym,
+                               const llvm::APSInt& V, bool& isFeasible) {
+  
+  // FIXME: For now have assuming x > y be the same as assuming sym != V;
+  return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const ValueState*
+ValueStateManager::AssumeSymGE(const ValueState* 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).
+  
+  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+    isFeasible = *X >= V;
+    return St;
   }
+  
+  isFeasible = true;
+  return St;
 }
+
+const ValueState*
+ValueStateManager::AssumeSymLE(const ValueState* 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).
+    
+  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+    isFeasible = *X <= V;
+    return St;
+  }
+  
+  isFeasible = true;
+  return St;
+}
+