Let constraint manager inform checkers that some assumption logic has happend.

Add new states for symbolic regions tracked by malloc checker. This enables us
to do malloc checking more accurately. See test case.

Based on Lei Zhang's patch and discussion.


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

1 files changed, 28 insertions, 4 deletions

diff --git a/lib/Analysis/MallocChecker.cpp b/lib/Analysis/MallocChecker.cpp
index 2ed070a170..fab73ee7b1 100644
--- a/lib/Analysis/MallocChecker.cpp
+++ b/lib/Analysis/MallocChecker.cpp
@@ -23,13 +23,13 @@ using namespace clang;
 namespace {
 
 class RefState {
-  enum Kind { Allocated, Released, Escaped } K;
+  enum Kind { AllocateUnchecked, AllocateFailed, Released, Escaped } K;
   const Stmt *S;
 
 public:
   RefState(Kind k, const Stmt *s) : K(k), S(s) {}
 
-  bool isAllocated() const { return K == Allocated; }
+  bool isAllocated() const { return K == AllocateUnchecked; }
   bool isReleased() const { return K == Released; }
   bool isEscaped() const { return K == Escaped; }
 
@@ -37,7 +37,12 @@ public:
     return K == X.K && S == X.S;
   }
 
-  static RefState getAllocated(const Stmt *s) { return RefState(Allocated, s); }
+  static RefState getAllocateUnchecked(const Stmt *s) { 
+    return RefState(AllocateUnchecked, s); 
+  }
+  static RefState getAllocateFailed() {
+    return RefState(AllocateFailed, 0);
+  }
   static RefState getReleased(const Stmt *s) { return RefState(Released, s); }
   static RefState getEscaped(const Stmt *s) { return RefState(Escaped, s); }
 
@@ -62,6 +67,8 @@ public:
   void EvalDeadSymbols(CheckerContext &C,const Stmt *S,SymbolReaper &SymReaper);
   void EvalEndPath(GREndPathNodeBuilder &B, void *tag, GRExprEngine &Eng);
   void PreVisitReturnStmt(CheckerContext &C, const ReturnStmt *S);
+  const GRState *EvalAssume(const GRState *state, SVal Cond, bool Assumption);
+
 private:
   void MallocMem(CheckerContext &C, const CallExpr *CE);
   const GRState *MallocMemAux(CheckerContext &C, const CallExpr *CE,
@@ -74,6 +81,8 @@ private:
 };
 } // end anonymous namespace
 
+typedef llvm::ImmutableMap<SymbolRef, RefState> RegionStateTy;
+
 namespace clang {
   template <>
   struct GRStateTrait<RegionState> 
@@ -144,7 +153,7 @@ const GRState *MallocChecker::MallocMemAux(CheckerContext &C,
   SymbolRef Sym = RetVal.getAsLocSymbol();
   assert(Sym);
   // Set the symbol's state to Allocated.
-  return state->set<RegionState>(Sym, RefState::getAllocated(CE));
+  return state->set<RegionState>(Sym, RefState::getAllocateUnchecked(CE));
 }
 
 void MallocChecker::FreeMem(CheckerContext &C, const CallExpr *CE) {
@@ -298,3 +307,18 @@ void MallocChecker::PreVisitReturnStmt(CheckerContext &C, const ReturnStmt *S) {
 
   C.addTransition(state);
 }
+
+const GRState *MallocChecker::EvalAssume(const GRState *state, SVal Cond, 
+                                         bool Assumption) {
+  // If a symblic region is assumed to NULL, set its state to AllocateFailed.
+  // FIXME: should also check symbols assumed to non-null.
+
+  RegionStateTy RS = state->get<RegionState>();
+
+  for (RegionStateTy::iterator I = RS.begin(), E = RS.end(); I != E; ++I) {
+    if (state->getSymVal(I.getKey()))
+      state = state->set<RegionState>(I.getKey(),RefState::getAllocateFailed());
+  }
+
+  return state;
+}