[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

Reverted in https://reviews.llvm.org/rL307853


Repository:
  rL LLVM

https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

Reverted in https://reviews.llvm.org/rL307853


Repository:
  rL LLVM

https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Matt Morehouse via Phabricator via cfe-commits]

morehouse added a comment.

r307833 is causing the sanitizer-x86_64-linux-fast buildbot 
 to 
fail during clang regression tests with the following error:

  clang: 
/mnt/b/sanitizer-buildbot3/sanitizer-x86_64-linux-fast/build/llvm/tools/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp:55:
 virtual clang::ento::ProgramStateRef 
clang::ento::RangedConstraintManager::assumeSym(clang::ento::ProgramStateRef, 
clang::ento::SymbolRef, bool): Assertion 
`Loc::isLocType(SSE->getLHS()->getType())' failed.

Could you please revert and/or fix this revision?


Repository:
  rL LLVM

https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rL307833: [analyzer] Support generating and reasoning over 
more symbolic constraint types (authored by ddcc).

Changed prior to commit:
  https://reviews.llvm.org/D28953?vs=106084=106284#toc

Repository:
  rL LLVM

https://reviews.llvm.org/D28953

Files:
  cfe/trunk/include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp
  cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  cfe/trunk/test/Analysis/analyzer_test.py
  cfe/trunk/test/Analysis/bitwise-ops.c
  cfe/trunk/test/Analysis/bool-assignment.c
  cfe/trunk/test/Analysis/conditional-path-notes.c
  cfe/trunk/test/Analysis/explain-svals.cpp
  cfe/trunk/test/Analysis/plist-macros-z3.cpp
  cfe/trunk/test/Analysis/plist-macros.cpp
  cfe/trunk/test/Analysis/range_casts.c
  cfe/trunk/test/Analysis/std-c-library-functions.c

Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -1034,31 +1034,39 @@
 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
 ProgramStateRef State, SymbolRef Sym, const llvm::APSInt ,
 const llvm::APSInt , bool InRange) {
+  ASTContext  = getBasicVals().getContext();
+  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
+  // but the former is not available in Clang. Instead, extend the APSInt
+  // directly.
+  bool isBoolTy = From.getBitWidth() == 1 && getAPSIntType(From).isNull();
+
   QualType RetTy;
   // The expression may be casted, so we cannot call getZ3DataExpr() directly
   Z3Expr Exp = getZ3Expr(Sym, );
-
-  assert((getAPSIntType(From) == getAPSIntType(To)) &&
- "Range values have different types!");
-  QualType RTy = getAPSIntType(From);
-  bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
-  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
-  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+  QualType RTy = isBoolTy ? Ctx.BoolTy : getAPSIntType(From);
+  Z3Expr FromExp =
+  isBoolTy ? Z3Expr::fromAPSInt(From.extend(Ctx.getTypeSize(Ctx.BoolTy)))
+   : Z3Expr::fromAPSInt(From);
 
   // Construct single (in)equality
   if (From == To)
 return assumeZ3Expr(State, Sym,
 getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
  FromExp, RTy, nullptr));
 
+  assert((getAPSIntType(From) == getAPSIntType(To)) &&
+ "Range values have different types!");
+
+  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
   // Construct two (in)equalities, and a logical and/or
   Z3Expr LHS =
   getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
   Z3Expr RHS =
   getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
   return assumeZ3Expr(
   State, Sym,
-  Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
+  Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+RetTy->isSignedIntegerOrEnumerationType()));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
@@ -1406,6 +1414,7 @@
QualType , QualType ) const {
   ASTContext  = getBasicVals().getContext();
 
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Perform type conversion
   if (LTy->isIntegralOrEnumerationType() &&
   RTy->isIntegralOrEnumerationType()) {
@@ -1468,10 +1477,10 @@
 void Z3ConstraintManager::doIntTypeConversion(T , QualType , T ,
   QualType ) const {
   ASTContext  = getBasicVals().getContext();
-
   uint64_t LBitWidth = Ctx.getTypeSize(LTy);
   uint64_t RBitWidth = Ctx.getTypeSize(RTy);
 
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Always perform integer promotion before checking type equality.
   // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
   if (LTy->isPromotableIntegerType()) {
Index: cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp
===
--- cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ cfe/trunk/lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -100,7 +100,7 @@
 
   if (T->isNullPtrType())
 return makeZeroVal(T);
-  
+
   if (!SymbolManager::canSymbolicate(T))
 return UnknownVal();
 
@@ -354,17 +354,14 @@
BinaryOperator::Opcode Op,
NonLoc LHS, NonLoc RHS,
QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-return UnknownVal();
-
   const SymExpr *symLHS = LHS.getAsSymExpr();
   const SymExpr *symRHS = RHS.getAsSymExpr();
   // 

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 106084.
ddcc added a comment.

Split plist-macros.cpp, and update analyzer_test.py to support tests that 
require not z3


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/analyzer_test.py
  test/Analysis/bitwise-ops.c
  test/Analysis/bool-assignment.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/plist-macros-z3.cpp
  test/Analysis/plist-macros.cpp
  test/Analysis/range_casts.c
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/range_casts.c
===
--- test/Analysis/range_casts.c
+++ test/Analysis/range_casts.c
@@ -67,8 +67,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1 == 0)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -87,8 +87,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1L == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -117,8 +117,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1UL == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
Index: test/Analysis/plist-macros.cpp
===
--- test/Analysis/plist-macros.cpp
+++ test/Analysis/plist-macros.cpp
@@ -1,7 +1,7 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
-
+// REQUIRES: !z3
 
 typedef __typeof(sizeof(int)) size_t;
 void *malloc(size_t);
@@ -11,13 +11,13 @@
   y++;
   y--;
   mallocmemory
-  y++; 
+  y++;
   y++;
   delete x; // expected-warning {{Memory allocated by malloc() should be deallocated by free(), not 'delete'}}
 }
 
 void macroIsFirstInFunction(int y) {
-  mallocmemory 
+  mallocmemory
   y++; // expected-warning {{Potential leak of memory pointed to by 'x'}}
 }
 
@@ -39,7 +39,7 @@
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
-#define macroWithArg(mp) mp==0 
+#define macroWithArg(mp) mp==0
 int macroWithArgInExpression(int *p, int y) {;
   y++;
   if (macroWithArg(p))
@@ -85,6 +85,7 @@
 void test2(int *p) {
   CALL_FN(p);
 }
+
 // CHECK:  diagnostics
 // CHECK-NEXT:  
 // CHECK-NEXT:   
@@ -636,6 +637,69 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line36
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Artem Dergachev via Phabricator via cfe-commits]

NoQ accepted this revision.
NoQ added a comment.
This revision is now accepted and ready to land.

This looks great, thank you very much.




Comment at: test/Analysis/plist-macros.cpp:2
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix 
-analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix 
-analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config 
path-diagnostics-alternate=ture %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s

ddcc wrote:
> NoQ wrote:
> > > `path-diagnostics-alternate=ture`
> > 
> > Ouch. Thanks for fixing this.
> > 
> > Maybe it'd be great to implement an option that enables validating analyzer 
> > config option values, and turn this option on in `%clang_analyze_cc1`.
> I agree that'd be useful, but I think that it should be a separate future 
> patch.
Sure sure.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

I've also uploaded the results to https://dcddcc.com/csa


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

I tested the following software, both before and after applying this patch, 
using RangeConstraintManager.

Software, Version, Compile Time (before), Bugs Reported (before), Compile Time 
(after), Bugs Reported (after)
openssl, 1.1.0f, 11 min, 126, 12 min, 126
sqlite, 3.18.2, 31 min, 86, 31 min, 82
wireshark, 2.2.7, 105 min, 109, 119 min, 108

For sqlite, the differences of four reported bugs all appear to be false 
positives, but for wireshark, the one difference appears to be a false negative.




Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:363
   // instead of generating an Unknown value and propagate the taint info to it.
-  const unsigned MaxComp = 1; // 10 28X
 

NoQ wrote:
> ddcc wrote:
> > zaks.anna wrote:
> > > Reducing the MaxComp is going to regress taint analysis..
> > > 
> > > > I've updated this revision to account for the recent SVal 
> > > > simplification commit by @NoQ, 
> > > 
> > > Which commit introduced the regression?
> > > 
> > > > but now there is an exponential blowup problem that prevents testcase 
> > > > PR24184.cpp from terminating, 
> > > 
> > > What triggers the regression? Removing the if statement above? Does the 
> > > regression only effect the Z3 "mode" (I am guessing not since you said 
> > > "due to an interaction between Simplifier::VisitNonLocSymbolVal() and 
> > > SValBuilder::makeSymExprValNN()")? 
> > > 
> > > Reducing the MaxComp is going to regress taint analysis..
> > 
> > I think the original intention was to increase `MaxComp`, not decrease it, 
> > but I will restore the original value here.
> > 
> > > What triggers the regression? Removing the if statement above? Does the 
> > > regression only effect the Z3 "mode"
> > 
> > No, the regression isn't specifically due to this code, but with @NoQ 's 
> > patch for `SVal` simplification (rL300178), and this commit extending it to 
> > handle `SymbolCast` and `IntSymExpr`, the cast of `ST *` used in the loop 
> > of case 3 of PR24184.cpp becomes "simplified" (inlined) repeatedly on each 
> > recursive iteration through `Simplifier::VisitNonLocSymbolVal()` -> 
> > `SValBuilder::makeSymExprValNN()`, causing a big slowdown in runtime 
> > performance.
> > 
> > The naive way to prevent it is to drop `MaxComp` (but this isn't 
> > reasonable, since it needs to be absurdly low, e.g. `10`). Alternatively, 
> > simplification for `SymbolCast` can be dropped from this commit (but it 
> > will eliminate some of the other analysis improvements), or, most likely, 
> > introduce another parameter to reduce recursion between these two functions.
> We talked a bit and we're pretty much fine with reduce `MaxComp` to 10 if 
> it's worth it in terms of performance.
Just to clarify, the current change from 100 to 10 in 
`simplifySVal::SimplyVisitNonLocSymbolVal` resolves the problem; the value of 
`MaxComp` here is unchanged.



Comment at: test/Analysis/plist-macros.cpp:2
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix 
-analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix 
-analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config 
path-diagnostics-alternate=ture %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s

NoQ wrote:
> > `path-diagnostics-alternate=ture`
> 
> Ouch. Thanks for fixing this.
> 
> Maybe it'd be great to implement an option that enables validating analyzer 
> config option values, and turn this option on in `%clang_analyze_cc1`.
I agree that'd be useful, but I think that it should be a separate future patch.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 105913.
ddcc marked an inline comment as done.
ddcc added a comment.

Drop duplicate code


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/bitwise-ops.c
  test/Analysis/bool-assignment.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/plist-macros.cpp
  test/Analysis/range_casts.c
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/range_casts.c
===
--- test/Analysis/range_casts.c
+++ test/Analysis/range_casts.c
@@ -67,8 +67,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1 == 0)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -87,8 +87,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1L == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -117,8 +117,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1UL == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
Index: test/Analysis/plist-macros.cpp
===
--- test/Analysis/plist-macros.cpp
+++ test/Analysis/plist-macros.cpp
@@ -1,5 +1,5 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
 
 
@@ -85,6 +85,7 @@
 void test2(int *p) {
   CALL_FN(p);
 }
+
 // CHECK:  diagnostics
 // CHECK-NEXT:  
 // CHECK-NEXT:   
@@ -636,6 +637,69 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line36
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col25
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT:
+// CHECK-NEXT:  
+// CHECK-NEXT:  depth0
+// CHECK-NEXT:  extended_message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT:  message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindcontrol
+// CHECK-NEXT:  edges
+// CHECK-NEXT:   
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

Because this patch affects the default behavior, i think it's necessary to 
understand the performance impact on a large codebase. I may lend a hand 
eventually, but if you're in a hurry you could probably at least run an 
overnight analysis over llvm and sqlite with range constraint manager and see 
how performance changes with this patch, and ideally also if we get new reports 
or lose old reports.

In https://reviews.llvm.org/D28953#785679, @ddcc wrote:

> I forgot to mention that the only remaining (Z3) test failure is on 
> `plist-macros.cpp`; there is a `Assuming condition is true` path note that 
> only appears with the RangeConstraintManager but not with 
> Z3ConstraintManager, and I can't `#ifdef` it because the annotations are 
> checked by `FileCheck`.


This test case could be separated into a different file if nothing else helps.




Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:363
   // instead of generating an Unknown value and propagate the taint info to it.
-  const unsigned MaxComp = 1; // 10 28X
 

ddcc wrote:
> zaks.anna wrote:
> > Reducing the MaxComp is going to regress taint analysis..
> > 
> > > I've updated this revision to account for the recent SVal simplification 
> > > commit by @NoQ, 
> > 
> > Which commit introduced the regression?
> > 
> > > but now there is an exponential blowup problem that prevents testcase 
> > > PR24184.cpp from terminating, 
> > 
> > What triggers the regression? Removing the if statement above? Does the 
> > regression only effect the Z3 "mode" (I am guessing not since you said "due 
> > to an interaction between Simplifier::VisitNonLocSymbolVal() and 
> > SValBuilder::makeSymExprValNN()")? 
> > 
> > Reducing the MaxComp is going to regress taint analysis..
> 
> I think the original intention was to increase `MaxComp`, not decrease it, 
> but I will restore the original value here.
> 
> > What triggers the regression? Removing the if statement above? Does the 
> > regression only effect the Z3 "mode"
> 
> No, the regression isn't specifically due to this code, but with @NoQ 's 
> patch for `SVal` simplification (rL300178), and this commit extending it to 
> handle `SymbolCast` and `IntSymExpr`, the cast of `ST *` used in the loop of 
> case 3 of PR24184.cpp becomes "simplified" (inlined) repeatedly on each 
> recursive iteration through `Simplifier::VisitNonLocSymbolVal()` -> 
> `SValBuilder::makeSymExprValNN()`, causing a big slowdown in runtime 
> performance.
> 
> The naive way to prevent it is to drop `MaxComp` (but this isn't reasonable, 
> since it needs to be absurdly low, e.g. `10`). Alternatively, simplification 
> for `SymbolCast` can be dropped from this commit (but it will eliminate some 
> of the other analysis improvements), or, most likely, introduce another 
> parameter to reduce recursion between these two functions.
We talked a bit and we're pretty much fine with reduce `MaxComp` to 10 if it's 
worth it in terms of performance.



Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:997-1003
   if (SymbolRef Sym = V.getAsSymbol())
 return state->getConstraintManager().getSymVal(state, Sym);
 
-  // FIXME: Add support for SymExprs.
+  if (Optional NV = V.getAs())
+if (SymbolRef Sym = NV->getAsSymExpr())
+  return state->getConstraintManager().getSymVal(state, Sym);
+

These two ifs are completely identical (apart from the fact that the one you 
added ignores symbolic region values due to explicit NonLoc cast). In fact 
`getAsSymbol()` (with its optional argument equal to `false`) and 
`getAsSymExpr()` are equivalent; we need to refactor this API.

I believe that the FIXME should in fact be addressed in 
`RangeConstraintManager`, in which currently `getSymVal()` works for atomic 
symbols only. Or, alternatively, we should stick `simplifySVal()` here - i 
think i'd have a look at this soon.

In any case, i suggest removing this change for now, unless i missed anything 
and it does in fact have an effect.



Comment at: test/Analysis/plist-macros.cpp:2
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix 
-analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix 
-analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config 
path-diagnostics-alternate=ture %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s

> `path-diagnostics-alternate=ture`

Ouch. Thanks for fixing this.

Maybe it'd be great to implement an option that enables validating analyzer 
config option values, and turn this option on in `%clang_analyze_cc1`.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

ping


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

I forgot to mention that the only remaining test failure is on 
`plist-macros.cpp`; there is a `Assuming condition is true` path note that only 
appears with the RangeConstraintManager but not with Z3ConstraintManager, and I 
can't `#ifdef` it because the annotations are checked by `FileCheck`.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 103239.
ddcc added a comment.

Rebase, decrease simplification complexity


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/bitwise-ops.c
  test/Analysis/bool-assignment.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/plist-macros.cpp
  test/Analysis/range_casts.c
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/range_casts.c
===
--- test/Analysis/range_casts.c
+++ test/Analysis/range_casts.c
@@ -67,8 +67,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1 == 0)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -87,8 +87,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1L == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -117,8 +117,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1UL == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
Index: test/Analysis/plist-macros.cpp
===
--- test/Analysis/plist-macros.cpp
+++ test/Analysis/plist-macros.cpp
@@ -1,5 +1,5 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
 
 
@@ -85,6 +85,7 @@
 void test2(int *p) {
   CALL_FN(p);
 }
+
 // CHECK:  diagnostics
 // CHECK-NEXT:  
 // CHECK-NEXT:   
@@ -636,6 +637,69 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line36
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col25
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT:
+// CHECK-NEXT:  
+// CHECK-NEXT:  depth0
+// CHECK-NEXT:  extended_message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT:  message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindcontrol
+// CHECK-NEXT:  edges
+// CHECK-NEXT:   
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// 

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

> Can we drop computing these for some expressions that we know the 
> RangeConstraintManager will not utilize?

It's possible, though I'm not sure what the actual limitations of the 
RangeConstraintManager are, since there are a lot of intermediate steps that 
attempt to transform unsupported expressions into supported ones.

> We could implement the TODO described below and possibly also lower the 
> MaxComp value. This means that instead of keeping a complex expression and 
> constraints on every symbol used in that expression, we would conjure a new 
> symbol and associate a new constrain derived from the expression with it. 
> (Would this strategy also work for the Z3 case?)

I think it's feasible, but would probably require some more to code to handle 
`SymbolConjured` (right now all `SymbolData` are treated as variables).

> Would it help to decrease 100 to 10 here?

Yes, changing it to 10 eliminates the excessive recursion; combined runtime 
drops to 282 sec on the testcases (~8 sec for Range only, ~271 sec for Z3 only; 
doesn't sum due to separate executions). This appears to be the most 
straightforward solution.

> (2) With RangeConstraintManager, simplification is not entirely idempotent: 
> we may simplify a symbol further when one of its sub-symbols gets constrained 
> to a constant in a new state. However, apart from that, we might be able to 
> avoid re-simplifying the same symbol by caching results based on the (symbol, 
> state's constraint data) pair. Probably it may work with Z3 as well.

Yeah, that would also fix this issue. In general, I think there's plenty of 
room for improvements from caching, especially for queries to e.g. 
`getSymVal()`.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

Hmm, curious, having a look. A couple of blind guesses before i actually 
understand what's going on:

(1) The `simplifySVal()` code has its own complexity threshold:

  1060 SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
  1061   // Simplification is much more costly than computing complexity.
  1062   // For high complexity, it may be not worth it.
  1063   if (V.getSymbol()->computeComplexity() > 100)
  1064 return V;
  1065   return Visit(V.getSymbol());
  1066 }

Would it help to decrease `100` to `10` here?

(2) With RangeConstraintManager, simplification is not entirely idempotent: we 
may simplify a symbol further when one of its sub-symbols gets constrained to a 
constant in a new state. However, apart from that, we might be able to avoid 
re-simplifying the same symbol by caching results based on the (symbol, state's 
constraint data) pair. Probably it may work with Z3 as well.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Anna Zaks via Phabricator via cfe-commits]

zaks.anna added inline comments.



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:356
QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-return UnknownVal();

ddcc wrote:
> zaks.anna wrote:
> > I am concerned that removing the guard will regress performance in the 
> > vanilla case. (Note that Z3 support as well as taint are not on by default.)
> > 
> > I am curious how much of the regression you've measured could be gained 
> > back if we make this conditional.
> To clarify, the changes made in this patch aren't specific to Z3 support, 
> especially simplifying `SymbolCast` and `IntSymExpr`. With the exception of 
> `PR24184.cpp` and `plist-macros.cpp`, all testcases pass with both the 
> default and Z3 constraint managers. However, creating additional constraints 
> does have performance overhead, and it may be useful to consider the 
> parameters for gating this functionality.
> 
> On a combined execution (Range + Z3) through the testcases, except the two 
> mentioned above, the runtime is 327 sec with this patch applied, and 195 sec 
> without this patch applied. On a separate execution through the testcases 
> with only the Z3 constraint manager, I get runtimes 320 and 191, respectively.
> 
> For testing purposes, I also tried the following code, which has combined 
> runtime 311 sec, but loses the accuracy improvements with the Range 
> constraint manager on `bitwise-ops.c`, `conditional-path-notes.c`, 
> `explain-svals.cpp`, and `std-c-library-functions.c`.
> 
> ```
> ConstraintManager  = getStateManager().getConstraintManager();
> if (!State->isTainted(RHS) && !State->isTainted(LHS) && !CM.isZ3())
> ```
Thanks for the explanation!

Regressing the current default behavior is my main concern. By looking at the 
numbers you provided before (Pre-commit and Post-Commit for 
RangeConstraintManager), it seems that this patch will introduce a performance 
regression of about 20%, which is large. But you are pointing out that there 
are improvements to the modeling as well and those are captured by the updated 
tests.

Here are a couple of ideas that came into mind on gaining back performance for 
the RangeConstraintManager case: 
 - Can we drop computing these for some expressions that we know the 
RangeConstraintManager will not utilize?
 - We could implement the TODO described below and possibly also lower the 
MaxComp value. This means that instead of keeping a complex expression and 
constraints on every symbol used in that expression, we would conjure a new 
symbol and associate a new constrain derived from the expression with it. 
(Would this strategy also work for the Z3 case?)

I have to point out that this code is currently only used by taint analysis, 
which is experimental and the current MaxComp value is targeted at that. We 
would probably need to refine the strategy here if we want to apply this logic 
to a general case. It's possible that different MaxComp should be used for 
different cases.

It would be valuable to run this on real code and measure how the number of 
reports we get differs depending on these values.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added inline comments.



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:356
QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-return UnknownVal();

zaks.anna wrote:
> I am concerned that removing the guard will regress performance in the 
> vanilla case. (Note that Z3 support as well as taint are not on by default.)
> 
> I am curious how much of the regression you've measured could be gained back 
> if we make this conditional.
To clarify, the changes made in this patch aren't specific to Z3 support, 
especially simplifying `SymbolCast` and `IntSymExpr`. With the exception of 
`PR24184.cpp` and `plist-macros.cpp`, all testcases pass with both the default 
and Z3 constraint managers. However, creating additional constraints does have 
performance overhead, and it may be useful to consider the parameters for 
gating this functionality.

On a combined execution (Range + Z3) through the testcases, except the two 
mentioned above, the runtime is 327 sec with this patch applied, and 195 sec 
without this patch applied. On a separate execution through the testcases with 
only the Z3 constraint manager, I get runtimes 320 and 191, respectively.

For testing purposes, I also tried the following code, which has combined 
runtime 311 sec, but loses the accuracy improvements with the Range constraint 
manager on `bitwise-ops.c`, `conditional-path-notes.c`, `explain-svals.cpp`, 
and `std-c-library-functions.c`.

```
ConstraintManager  = getStateManager().getConstraintManager();
if (!State->isTainted(RHS) && !State->isTainted(LHS) && !CM.isZ3())
```



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:363
   // instead of generating an Unknown value and propagate the taint info to it.
-  const unsigned MaxComp = 1; // 10 28X
 

zaks.anna wrote:
> Reducing the MaxComp is going to regress taint analysis..
> 
> > I've updated this revision to account for the recent SVal simplification 
> > commit by @NoQ, 
> 
> Which commit introduced the regression?
> 
> > but now there is an exponential blowup problem that prevents testcase 
> > PR24184.cpp from terminating, 
> 
> What triggers the regression? Removing the if statement above? Does the 
> regression only effect the Z3 "mode" (I am guessing not since you said "due 
> to an interaction between Simplifier::VisitNonLocSymbolVal() and 
> SValBuilder::makeSymExprValNN()")? 
> 
> Reducing the MaxComp is going to regress taint analysis..

I think the original intention was to increase `MaxComp`, not decrease it, but 
I will restore the original value here.

> What triggers the regression? Removing the if statement above? Does the 
> regression only effect the Z3 "mode"

No, the regression isn't specifically due to this code, but with @NoQ 's patch 
for `SVal` simplification (rL300178), and this commit extending it to handle 
`SymbolCast` and `IntSymExpr`, the cast of `ST *` used in the loop of case 3 of 
PR24184.cpp becomes "simplified" (inlined) repeatedly on each recursive 
iteration through `Simplifier::VisitNonLocSymbolVal()` -> 
`SValBuilder::makeSymExprValNN()`, causing a big slowdown in runtime 
performance.

The naive way to prevent it is to drop `MaxComp` (but this isn't reasonable, 
since it needs to be absurdly low, e.g. `10`). Alternatively, simplification 
for `SymbolCast` can be dropped from this commit (but it will eliminate some of 
the other analysis improvements), or, most likely, introduce another parameter 
to reduce recursion between these two functions.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Anna Zaks via Phabricator via cfe-commits]

zaks.anna added inline comments.



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:356
QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-return UnknownVal();

I am concerned that removing the guard will regress performance in the vanilla 
case. (Note that Z3 support as well as taint are not on by default.)

I am curious how much of the regression you've measured could be gained back if 
we make this conditional.



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:363
   // instead of generating an Unknown value and propagate the taint info to it.
-  const unsigned MaxComp = 1; // 10 28X
 

Reducing the MaxComp is going to regress taint analysis..

> I've updated this revision to account for the recent SVal simplification 
> commit by @NoQ, 

Which commit introduced the regression?

> but now there is an exponential blowup problem that prevents testcase 
> PR24184.cpp from terminating, 

What triggers the regression? Removing the if statement above? Does the 
regression only effect the Z3 "mode" (I am guessing not since you said "due to 
an interaction between Simplifier::VisitNonLocSymbolVal() and 
SValBuilder::makeSymExprValNN()")? 



https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 99521.
ddcc added a comment.

Fix typo in SymbolCast simplification


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/bitwise-ops.c
  test/Analysis/bool-assignment.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/plist-macros.cpp
  test/Analysis/range_casts.c
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/range_casts.c
===
--- test/Analysis/range_casts.c
+++ test/Analysis/range_casts.c
@@ -67,8 +67,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1 == 0)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -87,8 +87,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1L == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -117,8 +117,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1UL == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
Index: test/Analysis/plist-macros.cpp
===
--- test/Analysis/plist-macros.cpp
+++ test/Analysis/plist-macros.cpp
@@ -1,5 +1,5 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
 
 
@@ -85,6 +85,7 @@
 void test2(int *p) {
   CALL_FN(p);
 }
+
 // CHECK:  diagnostics
 // CHECK-NEXT:  
 // CHECK-NEXT:   
@@ -636,6 +637,69 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line36
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col25
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT:
+// CHECK-NEXT:  
+// CHECK-NEXT:  depth0
+// CHECK-NEXT:  extended_message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT:  message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindcontrol
+// CHECK-NEXT:  edges
+// CHECK-NEXT:   
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:  

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

I've updated this revision to account for the recent SVal simplification commit 
by @NoQ, but now there is an exponential recursion problem that prevents 
testcase `PR24184.cpp` from terminating, due to an interaction between 
`Simplifier::VisitNonLocSymbolVal()` and `SValBuilder::makeSymExprValNN()`. I'm 
not quite sure what the best way to resolve this is; from some blind testing, I 
ended up needing to set `MaxComp` to `10` to force termination in a reasonable 
amount of time, but this restricts its usefulness for other constraints.


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 99392.
ddcc added a comment.

Address SVal simplification from https://reviews.llvm.org/D31886


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/bitwise-ops.c
  test/Analysis/bool-assignment.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/plist-macros.cpp
  test/Analysis/range_casts.c
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/range_casts.c
===
--- test/Analysis/range_casts.c
+++ test/Analysis/range_casts.c
@@ -67,8 +67,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1 == 0)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -87,8 +87,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1L == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
@@ -117,8 +117,8 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
-clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1UL == 0L)
+clang_analyzer_warnIfReached(); // no-warning
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
Index: test/Analysis/plist-macros.cpp
===
--- test/Analysis/plist-macros.cpp
+++ test/Analysis/plist-macros.cpp
@@ -1,5 +1,5 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
 
 
@@ -636,6 +636,69 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line36
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  line36
+// CHECK-NEXT:  col25
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT:
+// CHECK-NEXT:  
+// CHECK-NEXT:  depth0
+// CHECK-NEXT:  extended_message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT:  message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindcontrol
+// CHECK-NEXT:  edges
+// CHECK-NEXT:   
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line36
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 98545.
ddcc added a comment.

Rebase


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  test/Analysis/bitwise-ops.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/explain-svals.cpp
===
--- test/Analysis/explain-svals.cpp
+++ test/Analysis/explain-svals.cpp
@@ -69,7 +69,7 @@
   static int stat;
   clang_analyzer_explain(x + 1); // expected-warning-re^\(argument 'x'\) \+ 1$
   clang_analyzer_explain(1 + y); // expected-warning-re^\(argument 'y'\) \+ 1$
-  clang_analyzer_explain(x + y); // expected-warning-re^unknown value$
+  clang_analyzer_explain(x + y); // expected-warning-re^\(argument 'x'\) \+ \(argument 'y'\)$
   clang_analyzer_explain(z); // expected-warning-re^undefined value$
   clang_analyzer_explain(); // expected-warning-re^pointer to local variable 'z'$
   clang_analyzer_explain(stat); // expected-warning-re^signed 32-bit integer '0'$
Index: test/Analysis/conditional-path-notes.c
===
--- test/Analysis/conditional-path-notes.c
+++ test/Analysis/conditional-path-notes.c
@@ -77,7 +77,8 @@
 
 void testNonDiagnosableBranchArithmetic(int a, int b) {
   if (a - b) {
-// expected-note@-1 {{Taking true branch}}
+// expected-note@-1 {{Assuming the condition is true}}
+// expected-note@-2 {{Taking true branch}}
 *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
 // expected-note@-1 {{Dereference of null pointer}}
   }
@@ -1573,12 +1574,75 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line79
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line79
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  line79
+// CHECK-NEXT:  col11
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT:
+// CHECK-NEXT:  
+// CHECK-NEXT:  depth0
+// CHECK-NEXT:  extended_message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT:  message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindcontrol
+// CHECK-NEXT:  edges
+// CHECK-NEXT:   
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT: end
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
@@ -1594,25 +1658,25 @@
 // CHECK-NEXT: start
 // CHECK-NEXT:  
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
 // 

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

It's been a while since I looked at the code, but I don't believe that all of 
the new constraints are necessarily unsupported by the current range constraint 
manager. Rather, they were just not being generated by the SimpleSValBuilder. 
The changes pass the testsuite for both the Range and Z3 constraint managers, 
without any special testcase handling that is Z3 specific.

Here are some runtime performance numbers on the testsuite:

Pre-Commit
RangeConstraintManager: 8.24s
Z3ConstraintManager: 247.29s

Post-Commit
RangeConstraintManager: 10.23s
Z3ConstraintManager: 250.35s

And for memory usage (max RSS):

Pre-Commit
edges-new.mm (RangeConstraintManager): 42688k
edges-new.mm (Z3ConstraintManager): 52916k
malloc-plist.c (RangeConstraintManager): 39812k
malloc-plist.c (Z3ConstraintManager): 50544k

Post-Commit
edges-new.mm (RangeConstraintManager): 43032k
edges-new.mm (Z3ConstraintManager): 52956k
malloc-plist.c (RangeConstraintManager): 40204k
malloc-plist.c (Z3ConstraintManager): 50364k


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

Do you have a benchmark how this affects the performance and memory usage when 
the old constraint manager is used? I wonder if most of people are using the 
old one, it might make no sense to generate symbolic expressions that can not 
be solved anyway.
Maybe the analyzer could only generate these symbolic expressions when Z3 is 
used?


https://reviews.llvm.org/D28953



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 93589.
ddcc added a comment.

Rebase


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  test/Analysis/bitwise-ops.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/explain-svals.cpp
===
--- test/Analysis/explain-svals.cpp
+++ test/Analysis/explain-svals.cpp
@@ -69,7 +69,7 @@
   static int stat;
   clang_analyzer_explain(x + 1); // expected-warning-re^\(argument 'x'\) \+ 1$
   clang_analyzer_explain(1 + y); // expected-warning-re^\(argument 'y'\) \+ 1$
-  clang_analyzer_explain(x + y); // expected-warning-re^unknown value$
+  clang_analyzer_explain(x + y); // expected-warning-re^\(argument 'x'\) \+ \(argument 'y'\)$
   clang_analyzer_explain(z); // expected-warning-re^undefined value$
   clang_analyzer_explain(); // expected-warning-re^pointer to local variable 'z'$
   clang_analyzer_explain(stat); // expected-warning-re^signed 32-bit integer '0'$
Index: test/Analysis/conditional-path-notes.c
===
--- test/Analysis/conditional-path-notes.c
+++ test/Analysis/conditional-path-notes.c
@@ -77,7 +77,8 @@
 
 void testNonDiagnosableBranchArithmetic(int a, int b) {
   if (a - b) {
-// expected-note@-1 {{Taking true branch}}
+// expected-note@-1 {{Assuming the condition is true}}
+// expected-note@-2 {{Taking true branch}}
 *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
 // expected-note@-1 {{Dereference of null pointer}}
   }
@@ -1573,12 +1574,75 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line79
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line79
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  line79
+// CHECK-NEXT:  col11
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT:
+// CHECK-NEXT:  
+// CHECK-NEXT:  depth0
+// CHECK-NEXT:  extended_message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT:  message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindcontrol
+// CHECK-NEXT:  edges
+// CHECK-NEXT:   
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT: end
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
@@ -1594,25 +1658,25 @@
 // CHECK-NEXT: start
 // CHECK-NEXT:  
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
 // 

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 85314.
ddcc added a comment.

Rebase


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  test/Analysis/bitwise-ops.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/explain-svals.cpp
===
--- test/Analysis/explain-svals.cpp
+++ test/Analysis/explain-svals.cpp
@@ -69,7 +69,7 @@
   static int stat;
   clang_analyzer_explain(x + 1); // expected-warning-re^\(argument 'x'\) \+ 1$
   clang_analyzer_explain(1 + y); // expected-warning-re^\(argument 'y'\) \+ 1$
-  clang_analyzer_explain(x + y); // expected-warning-re^unknown value$
+  clang_analyzer_explain(x + y); // expected-warning-re^\(argument 'x'\) \+ \(argument 'y'\)$
   clang_analyzer_explain(z); // expected-warning-re^undefined value$
   clang_analyzer_explain(); // expected-warning-re^pointer to local variable 'z'$
   clang_analyzer_explain(stat); // expected-warning-re^signed 32-bit integer '0'$
Index: test/Analysis/conditional-path-notes.c
===
--- test/Analysis/conditional-path-notes.c
+++ test/Analysis/conditional-path-notes.c
@@ -77,7 +77,8 @@
 
 void testNonDiagnosableBranchArithmetic(int a, int b) {
   if (a - b) {
-// expected-note@-1 {{Taking true branch}}
+// expected-note@-1 {{Assuming the condition is true}}
+// expected-note@-2 {{Taking true branch}}
 *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
 // expected-note@-1 {{Dereference of null pointer}}
   }
@@ -1573,12 +1574,75 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line79
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line79
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  line79
+// CHECK-NEXT:  col11
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT:
+// CHECK-NEXT:  
+// CHECK-NEXT:  depth0
+// CHECK-NEXT:  extended_message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT:  message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindcontrol
+// CHECK-NEXT:  edges
+// CHECK-NEXT:   
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT: end
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
@@ -1594,25 +1658,25 @@
 // CHECK-NEXT: start
 // CHECK-NEXT:  
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
 // 

[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 85139.
ddcc added a comment.

Fix rebase


https://reviews.llvm.org/D28953

Files:
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  test/Analysis/bitwise-ops.c
  test/Analysis/conditional-path-notes.c
  test/Analysis/explain-svals.cpp
  test/Analysis/std-c-library-functions.c

Index: test/Analysis/std-c-library-functions.c
===
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
Index: test/Analysis/explain-svals.cpp
===
--- test/Analysis/explain-svals.cpp
+++ test/Analysis/explain-svals.cpp
@@ -69,7 +69,7 @@
   static int stat;
   clang_analyzer_explain(x + 1); // expected-warning-re^\(argument 'x'\) \+ 1$
   clang_analyzer_explain(1 + y); // expected-warning-re^\(argument 'y'\) \+ 1$
-  clang_analyzer_explain(x + y); // expected-warning-re^unknown value$
+  clang_analyzer_explain(x + y); // expected-warning-re^\(argument 'x'\) \+ \(argument 'y'\)$
   clang_analyzer_explain(z); // expected-warning-re^undefined value$
   clang_analyzer_explain(); // expected-warning-re^pointer to local variable 'z'$
   clang_analyzer_explain(stat); // expected-warning-re^signed 32-bit integer '0'$
Index: test/Analysis/conditional-path-notes.c
===
--- test/Analysis/conditional-path-notes.c
+++ test/Analysis/conditional-path-notes.c
@@ -77,7 +77,8 @@
 
 void testNonDiagnosableBranchArithmetic(int a, int b) {
   if (a - b) {
-// expected-note@-1 {{Taking true branch}}
+// expected-note@-1 {{Assuming the condition is true}}
+// expected-note@-2 {{Taking true branch}}
 *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
 // expected-note@-1 {{Dereference of null pointer}}
   }
@@ -1573,12 +1574,75 @@
 // CHECK-NEXT: end
 // CHECK-NEXT:  
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT:   
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindevent
+// CHECK-NEXT:  location
+// CHECK-NEXT:  
+// CHECK-NEXT:   line79
+// CHECK-NEXT:   col7
+// CHECK-NEXT:   file0
+// CHECK-NEXT:  
+// CHECK-NEXT:  ranges
+// CHECK-NEXT:  
+// CHECK-NEXT:
+// CHECK-NEXT: 
+// CHECK-NEXT:  line79
+// CHECK-NEXT:  col7
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  line79
+// CHECK-NEXT:  col11
+// CHECK-NEXT:  file0
+// CHECK-NEXT: 
+// CHECK-NEXT:
+// CHECK-NEXT:  
+// CHECK-NEXT:  depth0
+// CHECK-NEXT:  extended_message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT:  message
+// CHECK-NEXT:  Assuming the condition is true
+// CHECK-NEXT: 
+// CHECK-NEXT: 
+// CHECK-NEXT:  kindcontrol
+// CHECK-NEXT:  edges
+// CHECK-NEXT:   
+// CHECK-NEXT:
+// CHECK-NEXT: start
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:   
+// CHECK-NEXT:line79
+// CHECK-NEXT:col7
+// CHECK-NEXT:file0
+// CHECK-NEXT:   
+// CHECK-NEXT:  
+// CHECK-NEXT: end
+// CHECK-NEXT:  
+// CHECK-NEXT:   
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
@@ -1594,25 +1658,25 @@
 // CHECK-NEXT: start
 // CHECK-NEXT:  
 // CHECK-NEXT:   
-// CHECK-NEXT:line81
+// CHECK-NEXT:line82
 // CHECK-NEXT:col5
 // CHECK-NEXT:file0
 // CHECK-NEXT:   
 //