]> granicus.if.org Git - clang/commitdiff
Add experimental logic in GRExprEngine::EvalEagerlyAssume() to handle
authorTed Kremenek <kremenek@apple.com>
Wed, 25 Feb 2009 22:32:02 +0000 (22:32 +0000)
committerTed Kremenek <kremenek@apple.com>
Wed, 25 Feb 2009 22:32:02 +0000 (22:32 +0000)
expressions of the form: 'short x = (y != 10);' While we handle 'int x = (y !=
10)' lazily, the cast to another integer type currently loses the symbolic
constraint. Eager evaluation of the constraint causes the paths to bifurcate and
eagerly evaluate 'y != 10' to a constant of 1 or 0. This should address
<rdar://problem/6619921> until we have a better (more lazy approach) for
handling promotions/truncations of symbolic integer values.

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

Driver/AnalysisConsumer.cpp
include/clang/Analysis/PathSensitive/GRExprEngine.h
lib/Analysis/GRExprEngine.cpp
test/Analysis/misc-ps-eager-assume.m [new file with mode: 0644]

index fd74f7dcd1790dcdd7e87f3ea1ac5a6ded2ab612..860cf156b5a556e5fcc54445a3a8353d7ac7b96c 100644 (file)
@@ -152,6 +152,12 @@ PurgeDead("analyzer-purge-dead",
           llvm::cl::desc("Remove dead symbols, bindings, and constraints before"
                          " processing a statement."));
 
+static llvm::cl::opt<bool>
+EagerlyAssume("analyzer-eagerly-assume",
+          llvm::cl::init(false),
+              llvm::cl::desc("Eagerly assume the truth/falseness of some "
+                             "symbolic constraints."));
+
 static llvm::cl::opt<std::string>
 AnalyzeSpecificFunction("analyze-function",
                llvm::cl::desc("Run analysis on specific function"));
@@ -516,7 +522,7 @@ static void ActionGRExprEngine(AnalysisManager& mgr, GRTransferFuncs* tf,
   if (!L) return;
 
   GRExprEngine Eng(*mgr.getCFG(), *mgr.getCodeDecl(), mgr.getContext(), *L, mgr,
-                   PurgeDead,
+                   PurgeDead, EagerlyAssume,
                    mgr.getStoreManagerCreator(), 
                    mgr.getConstraintManagerCreator());
 
index 7f2b5f595b8c9e2e52cac49857d6b0ba5d0522e4..797b0ae0cd80c40f952de251268a1bfeac873506 100644 (file)
@@ -90,6 +90,15 @@ protected:
   //   destructor is called before the rest of the GRExprEngine is destroyed.
   GRBugReporter BR;
   
+  /// EargerlyAssume - A flag indicating how the engine should handle
+  //   expressions such as: 'x = (y != 0)'.  When this flag is true then
+  //   the subexpression 'y != 0' will be eagerly assumed to be true or false,
+  //   thus evaluating it to the integers 0 or 1 respectively.  The upside
+  //   is that this can increase analysis precision until we have a better way
+  //   to lazily evaluate such logic.  The downside is that it eagerly
+  //   bifurcates paths.
+  const bool EagerlyAssume;
+  
 public:
   typedef llvm::SmallPtrSet<NodeTy*,2> ErrorNodes;  
   typedef llvm::DenseMap<NodeTy*, Expr*> UndefArgsTy;
@@ -186,7 +195,7 @@ public:
 public:
   GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx, LiveVariables& L,
                BugReporterData& BRD,
-               bool purgeDead,
+               bool purgeDead, bool eagerlyAssume = true,
                StoreManagerCreator SMC = CreateBasicStoreManager,
                ConstraintManagerCreator CMC = CreateBasicConstraintManager);
 
@@ -606,6 +615,11 @@ protected:
   const GRState* CheckDivideZero(Expr* Ex, const GRState* St, NodeTy* Pred,
                                  SVal Denom);  
   
+  /// EvalEagerlyAssume - Given the nodes in 'Src', eagerly assume symbolic
+  ///  expressions of the form 'x != 0' and generate new nodes (stored in Dst)
+  ///  with those assumptions.
+  void EvalEagerlyAssume(NodeSet& Dst, NodeSet& Src);
+  
   SVal EvalCast(SVal X, QualType CastT) {
     if (X.isUnknownOrUndef())
       return X;
index d34e8a3ed3a17e0d584948b412805134452b4831..08c8d9bf01d0e6397c5239a6fa0e5dc8a0e60afd 100644 (file)
@@ -103,7 +103,7 @@ static inline Selector GetNullarySelector(const char* name, ASTContext& Ctx) {
 
 GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx,
                            LiveVariables& L, BugReporterData& BRD,
-                           bool purgeDead,
+                           bool purgeDead, bool eagerlyAssume,
                            StoreManagerCreator SMC,
                            ConstraintManagerCreator CMC)
   : CoreEngine(cfg, CD, Ctx, *this), 
@@ -116,7 +116,8 @@ GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx,
     NSExceptionII(NULL), NSExceptionInstanceRaiseSelectors(NULL),
     RaiseSel(GetNullarySelector("raise", G.getContext())), 
     PurgeDead(purgeDead),
-    BR(BRD, *this)  {}
+    BR(BRD, *this),
+    EagerlyAssume(eagerlyAssume) {}
 
 GRExprEngine::~GRExprEngine() {    
   BR.FlushReports();
@@ -262,7 +263,14 @@ void GRExprEngine::Visit(Stmt* S, NodeTy* Pred, NodeSet& Dst) {
         break;
       }
 
-      VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Dst);
+      if (EagerlyAssume && (B->isRelationalOp() || B->isEqualityOp())) {
+        NodeSet Tmp;
+        VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Tmp);
+        EvalEagerlyAssume(Dst, Tmp);        
+      }
+      else
+        VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Dst);
+
       break;
     }
 
@@ -1349,6 +1357,44 @@ void GRExprEngine::VisitCallRec(CallExpr* CE, NodeTy* Pred,
 // Transfer function: Objective-C ivar references.
 //===----------------------------------------------------------------------===//
 
+static std::pair<const void*,const void*> EagerlyAssumeTag(&EagerlyAssumeTag,0);
+
+void GRExprEngine::EvalEagerlyAssume(NodeSet &Dst, NodeSet &Src) {
+  for (NodeSet::iterator I=Src.begin(), E=Src.end(); I!=E; ++I) {
+    NodeTy *Pred = *I;
+    Stmt *S = cast<PostStmt>(Pred->getLocation()).getStmt();
+    const GRState* state = Pred->getState();    
+    SVal V = GetSVal(state, S);    
+    if (isa<nonloc::SymIntConstraintVal>(V)) {
+      // First assume that the condition is true.
+      bool isFeasible = false;
+      const GRState *stateTrue = Assume(state, V, true, isFeasible);
+      if (isFeasible) {
+        stateTrue = BindExpr(stateTrue, cast<Expr>(S),
+                             MakeConstantVal(1U, cast<Expr>(S)));        
+        Dst.Add(Builder->generateNode(PostStmtCustom(S, &EagerlyAssumeTag),
+                                      stateTrue, Pred));
+      }
+        
+      // Next, assume that the condition is false.
+      isFeasible = false;
+      const GRState *stateFalse = Assume(state, V, false, isFeasible);
+      if (isFeasible) {
+        stateFalse = BindExpr(stateFalse, cast<Expr>(S),
+                              MakeConstantVal(0U, cast<Expr>(S)));
+        Dst.Add(Builder->generateNode(PostStmtCustom(S, &EagerlyAssumeTag),
+                                      stateFalse, Pred));
+      }
+    }
+    else
+      Dst.Add(Pred);
+  }
+}
+
+//===----------------------------------------------------------------------===//
+// Transfer function: Objective-C ivar references.
+//===----------------------------------------------------------------------===//
+
 void GRExprEngine::VisitObjCIvarRefExpr(ObjCIvarRefExpr* Ex,
                                             NodeTy* Pred, NodeSet& Dst,
                                             bool asLValue) {
diff --git a/test/Analysis/misc-ps-eager-assume.m b/test/Analysis/misc-ps-eager-assume.m
new file mode 100644 (file)
index 0000000..48d5b8f
--- /dev/null
@@ -0,0 +1,14 @@
+// RUN: clang -analyze -checker-cfref --analyzer-store=region -analyzer-constraints=range --verify -fblocks %s -analyzer-eagerly-assume
+
+void handle_assign_of_condition(int x) {
+  // The cast to 'short' causes us to lose symbolic constraint.
+  short y = (x != 0);
+  char *p = 0;
+  if (y) {
+    // This should be infeasible.
+    if (!(x != 0)) {
+      *p = 1;  // no-warning
+    }
+  }
+}
+