[cfe-commits] r66899 - in /cfe/trunk: lib/Analysis/GRExprEngine.cpp test/Analysis/misc-ps-eager-assume.m

[Ted Kremenek]

Author: kremenek
Date: Fri Mar 13 11:32:54 2009
New Revision: 66899

URL: http://llvm.org/viewvc/llvm-project?rev=66899&view=rev
Log:
Add a hack in the analyzer to recover some path-sensitivity at branch
conditions. Currently the analyzer does not reason well about
promotions/truncations of symbolic values, so at branch conditions when we see:

  if (condition)
  
and condition is something like a 'short' or 'char', essentially ignore the
promotion to 'int' so that we track constraints on the original symbolic value.
We only ignore the casts if the underlying type has the same or fewer bits as
the converted type.

This fixes:

<rdar://problem/6619921>


Modified:
    cfe/trunk/lib/Analysis/GRExprEngine.cpp
    cfe/trunk/test/Analysis/misc-ps-eager-assume.m

Modified: cfe/trunk/lib/Analysis/GRExprEngine.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/GRExprEngine.cpp?rev=66899&r1=66898&r2=66899&view=diff

==============================================================================
--- cfe/trunk/lib/Analysis/GRExprEngine.cpp (original)
+++ cfe/trunk/lib/Analysis/GRExprEngine.cpp Fri Mar 13 11:32:54 2009
@@ -540,6 +540,45 @@
   }
 }
 
+/// RecoverCastedSymbol - A helper function for ProcessBranch that is used
+/// to try to recover some path-sensitivity for casts of symbolic
+/// integers that promote their values (which are currently not tracked well).
+/// This function returns the SVal bound to Condition->IgnoreCasts if all the
+//  cast(s) did was sign-extend the original value.
+static SVal RecoverCastedSymbol(GRStateManager& StateMgr, const GRState* state,
+                                Stmt* Condition, ASTContext& Ctx) {
+
+  Expr *Ex = dyn_cast<Expr>(Condition);
+  if (!Ex)
+    return UnknownVal();
+
+  uint64_t bits = 0;
+  bool bitsInit = false;
+    
+  while (CastExpr *CE = dyn_cast<CastExpr>(Ex)) {
+    QualType T = CE->getType();
+
+    if (!T->isIntegerType())
+      return UnknownVal();
+    
+    uint64_t newBits = Ctx.getTypeSize(T);
+    if (!bitsInit || newBits < bits) {
+      bitsInit = true;
+      bits = newBits;
+    }
+      
+    Ex = CE->getSubExpr();
+  }
+
+  // We reached a non-cast.  Is it a symbolic value?
+  QualType T = Ex->getType();
+
+  if (!bitsInit || !T->isIntegerType() || Ctx.getTypeSize(T) > bits)
+    return UnknownVal();
+  
+  return StateMgr.GetSVal(state, Ex);
+}
+
 void GRExprEngine::ProcessBranch(Stmt* Condition, Stmt* Term,
                                  BranchNodeBuilder& builder) {
   
@@ -563,10 +602,28 @@
     default:
       break;
 
-    case SVal::UnknownKind:
+    case SVal::UnknownKind: {
+      if (Expr *Ex = dyn_cast<Expr>(Condition)) {
+          if (Ex->getType()->isIntegerType()) {
+          // Try to recover some path-sensitivity.  Right now casts of symbolic
+          // integers that promote their values are currently not tracked well.
+          // If 'Condition' is such an expression, try and recover the
+          // underlying value and use that instead.
+          SVal recovered = RecoverCastedSymbol(getStateManager(),
+                                               builder.getState(), Condition,
+                                               getContext());
+            
+          if (!recovered.isUnknown()) {
+            V = recovered;
+            break;
+          }
+        }
+      }
+    
       builder.generateNode(MarkBranch(PrevState, Term, true), true);
       builder.generateNode(MarkBranch(PrevState, Term, false), false);
       return;
+    }
       
     case SVal::UndefinedKind: {      
       NodeTy* N = builder.generateNode(PrevState, true);

Modified: cfe/trunk/test/Analysis/misc-ps-eager-assume.m
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/misc-ps-eager-assume.m?rev=66899&r1=66898&r2=66899&view=diff

==============================================================================
--- cfe/trunk/test/Analysis/misc-ps-eager-assume.m (original)
+++ cfe/trunk/test/Analysis/misc-ps-eager-assume.m Fri Mar 13 11:32:54 2009
@@ -1,5 +1,34 @@
 // RUN: clang -analyze -checker-cfref --analyzer-store=region -analyzer-constraints=range --verify -fblocks %s -analyzer-eagerly-assume
 
+// Delta-reduced header stuff (needed for test cases).
+typedef signed char BOOL;
+typedef unsigned int NSUInteger;
+typedef struct _NSZone NSZone;
+ at class NSInvocation, NSMethodSignature, NSCoder, NSString, NSEnumerator;
+ at protocol NSObject  - (BOOL)isEqual:(id)object;
+- (oneway void)release;
+ at end  @protocol NSCopying  - (id)copyWithZone:(NSZone *)zone;
+ at end  @protocol NSMutableCopying  - (id)mutableCopyWithZone:(NSZone *)zone;
+ at end  @protocol NSCoding  - (void)encodeWithCoder:(NSCoder *)aCoder;
+ at end    @interface NSObject <NSObject> {}
++ (id)alloc;
+ at end  typedef struct {}
+NSFastEnumerationState;
+ at protocol NSFastEnumeration  - (NSUInteger)countByEnumeratingWithState:(NSFastEnumerationState *)state objects:(id *)stackbuf count:(NSUInteger)len;
+ at end      @interface NSArray : NSObject <NSCopying, NSMutableCopying, NSCoding, NSFastEnumeration>  - (NSUInteger)count;
+ at end    @interface NSMutableArray : NSArray  - (void)addObject:(id)anObject;
+- (BOOL)isEqualToString:(NSString *)aString;
+ at end        @interface NSAutoreleasePool : NSObject {}
+- (void)drain;
+- (id)init;
+ at end
+
+// This test case tests that (x != 0) is eagerly evaluated before stored to
+// 'y'.  This test case complements recoverCastedSymbol (see below) because
+// the symbolic expression is stored to 'y' (which is a short instead of an
+// int).  recoverCastedSymbol() only recovers path-sensitivity when the
+// symbolic expression is literally the branch condition.
+//
 void handle_assign_of_condition(int x) {
   // The cast to 'short' causes us to lose symbolic constraint.
   short y = (x != 0);
@@ -12,3 +41,23 @@
   }
 }
 
+// From <rdar://problem/6619921>
+//
+// In this test case, 'needsAnArray' is a signed char.  The analyzer tracks
+// a symbolic value for this variable, but in the branch condition it is
+// promoted to 'int'.  Currently the analyzer doesn't reason well about
+// promotions of symbolic values, so this test case tests the logic in
+// 'recoverCastedSymbol()' (GRExprEngine.cpp) to test that we recover
+// path-sensitivity and use the symbol for 'needsAnArray' in the branch
+// condition.
+//
+void handle_symbolic_cast_in_condition(void) {
+  NSAutoreleasePool* pool = [[NSAutoreleasePool alloc] init];
+
+  BOOL needsAnArray = [@"aString" isEqualToString:@"anotherString"];
+  NSMutableArray* array = needsAnArray ? [[NSMutableArray alloc] init] : 0;
+  if(needsAnArray)
+    [array release];
+
+  [pool drain];
+}