[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2018-05-30 Thread George Karpenkov via Phabricator via cfe-commits
george.karpenkov requested changes to this revision.
george.karpenkov added a comment.
This revision now requires changes to proceed.

@ddcc so would be great if we could split this patch into smaller chunks.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2018-05-30 Thread George Karpenkov via Phabricator via cfe-commits
george.karpenkov added a comment.

> I can also split out the APSInt fix into a separate patch.

Yes please.

In general I really dislike arbitrary "complexity cutoffs", as they make 
further debugging hard and may lead to weird bugs: could you explain why is 
that required and can not be avoided?


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2018-05-30 Thread Dominic Chen via Phabricator via cfe-commits
ddcc added a comment.

In https://reviews.llvm.org/D35450#1116535, @george.karpenkov wrote:

> @ddcc Hi, are you still interested in landing the fixes associated with this 
> patch? I can take a look as I'm currently reviewing 
> https://reviews.llvm.org/D45517, but it is likely that the patch would need 
> to be changed substantially before it could land.


@george.karpenkov Yeah, I've got this and a couple of other patches still 
awaiting review. If it's easier, I can also split out the APSInt fix into a 
separate patch.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2018-05-30 Thread George Karpenkov via Phabricator via cfe-commits
george.karpenkov added a comment.
Herald added subscribers: a.sidorin, zzheng, rnkovacs, szepet.
Herald added a reviewer: george.karpenkov.

@ddcc Hi, are you still interested in landing the fixes associated with this 
patch? I can take a look as I'm currently reviewing 
https://reviews.llvm.org/D45517, but it is likely that the patch would need to 
be changed substantially before it could land.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-08-31 Thread Dominic Chen via Phabricator via cfe-commits
ddcc marked 5 inline comments as done.
ddcc added a comment.

All testcases pass, except the issue with `range_casts.c`. The cause is still 
the range intersection discussed in https://reviews.llvm.org/D35450#810469.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-08-31 Thread Dominic Chen via Phabricator via cfe-commits
ddcc updated this revision to Diff 113505.
ddcc added a comment.

Rebase, make complexity limits configurable


https://reviews.llvm.org/D35450

Files:
  include/clang/AST/Expr.h
  include/clang/Config/config.h.cmake
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  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/loop-unrolling.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,7 +67,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
+  if (index - 1 == 0)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -87,7 +87,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
+  if (index - 1L == 0L)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -117,7 +117,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
+  if (index - 1UL == 0L)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   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:   

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-08-28 Thread Anna Zaks via Phabricator via cfe-commits
zaks.anna added a comment.

> But I've never used the taint tracking mode, so I don't know what would be a 
> reasonable default for MaxComp.

that one is very experimental anyway. I'd just keep the functional changes to 
tain out of this patch and use the current default that taint uses.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-08-28 Thread Dominic Chen via Phabricator via cfe-commits
ddcc added inline comments.



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:364
   if (symLHS && symRHS &&
-  (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)
+  (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
 return makeNonLoc(symLHS, Op, symRHS, ResultTy);

zaks.anna wrote:
> ddcc wrote:
> > zaks.anna wrote:
> > > As a follow up to the previous version of this patch, I do not think we 
> > > should set the default complexity limit to 1.
> > > 
> > > What is the relation between this limit and the limit in 
> > > VisitNonLocSymbolVal? If they are related, would it be worthwhile turning 
> > > these into an analyzer option?
> > To clarify, the current version of this patch does not modify the `MaxComp` 
> > parameter.
> > 
> > My understanding is that `MaxComp` is the upper bound for building a new 
> > `NonLoc` symbol from two children, based on the sum of the number of child 
> > symbols (complexity) across both children.
> > 
> > In contrast, the limit in `VisitNonLocSymbolVal` (@NoQ, correct me if I'm 
> > wrong), is the upper bound for recursively evaluating and inlining a 
> > `NonLoc` symbol, triggered from `simplifySVal` by `evalBinOpNN`. Note that 
> > these two latter functions indirectly call each other recursively (through 
> > `evalBinOp`), causing the previous runtime blowup. Furthermore, each call 
> > to `computeComplexity`will re-iterate through all child symbols of the 
> > current symbol, but only the first complexity check at the root symbol is 
> > actually necessary, because by definition the complexity of a child symbol 
> > at each recursive call is monotonically decreasing.
> > 
> > I think it'd be useful to allow both to be configurable, but I don't see a 
> > direct relationship between the two.
> > To clarify, the current version of this patch does not modify the MaxComp 
> > parameter.
> 
> I know. Also, currently, it is only used in the unsupported taint tracking 
> mode and only for tainted symbols. I would like a different smaller default 
> for all expressions.
Ok. I can make both configurable as part of this patch, with a new default of 
10 for `VisitNonLocSymbolVal`. But I've never used the taint tracking mode, so 
I don't know what would be a reasonable default for `MaxComp`.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-08-27 Thread Anna Zaks via Phabricator via cfe-commits
zaks.anna added inline comments.



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:364
   if (symLHS && symRHS &&
-  (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)
+  (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
 return makeNonLoc(symLHS, Op, symRHS, ResultTy);

ddcc wrote:
> zaks.anna wrote:
> > As a follow up to the previous version of this patch, I do not think we 
> > should set the default complexity limit to 1.
> > 
> > What is the relation between this limit and the limit in 
> > VisitNonLocSymbolVal? If they are related, would it be worthwhile turning 
> > these into an analyzer option?
> To clarify, the current version of this patch does not modify the `MaxComp` 
> parameter.
> 
> My understanding is that `MaxComp` is the upper bound for building a new 
> `NonLoc` symbol from two children, based on the sum of the number of child 
> symbols (complexity) across both children.
> 
> In contrast, the limit in `VisitNonLocSymbolVal` (@NoQ, correct me if I'm 
> wrong), is the upper bound for recursively evaluating and inlining a `NonLoc` 
> symbol, triggered from `simplifySVal` by `evalBinOpNN`. Note that these two 
> latter functions indirectly call each other recursively (through 
> `evalBinOp`), causing the previous runtime blowup. Furthermore, each call to 
> `computeComplexity`will re-iterate through all child symbols of the current 
> symbol, but only the first complexity check at the root symbol is actually 
> necessary, because by definition the complexity of a child symbol at each 
> recursive call is monotonically decreasing.
> 
> I think it'd be useful to allow both to be configurable, but I don't see a 
> direct relationship between the two.
> To clarify, the current version of this patch does not modify the MaxComp 
> parameter.

I know. Also, currently, it is only used in the unsupported taint tracking mode 
and only for tainted symbols. I would like a different smaller default for all 
expressions.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-08-25 Thread Dominic Chen via Phabricator via cfe-commits
ddcc added inline comments.



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:364
   if (symLHS && symRHS &&
-  (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)
+  (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
 return makeNonLoc(symLHS, Op, symRHS, ResultTy);

zaks.anna wrote:
> As a follow up to the previous version of this patch, I do not think we 
> should set the default complexity limit to 1.
> 
> What is the relation between this limit and the limit in 
> VisitNonLocSymbolVal? If they are related, would it be worthwhile turning 
> these into an analyzer option?
To clarify, the current version of this patch does not modify the `MaxComp` 
parameter.

My understanding is that `MaxComp` is the upper bound for building a new 
`NonLoc` symbol from two children, based on the sum of the number of child 
symbols (complexity) across both children.

In contrast, the limit in `VisitNonLocSymbolVal` (@NoQ, correct me if I'm 
wrong), is the upper bound for recursively evaluating and inlining a `NonLoc` 
symbol, triggered from `simplifySVal` by `evalBinOpNN`. Note that these two 
latter functions indirectly call each other recursively (through `evalBinOp`), 
causing the previous runtime blowup. Furthermore, each call to 
`computeComplexity`will re-iterate through all child symbols of the current 
symbol, but only the first complexity check at the root symbol is actually 
necessary, because by definition the complexity of a child symbol at each 
recursive call is monotonically decreasing.

I think it'd be useful to allow both to be configurable, but I don't see a 
direct relationship between the two.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-08-25 Thread Anna Zaks via Phabricator via cfe-commits
zaks.anna added inline comments.



Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:364
   if (symLHS && symRHS &&
-  (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)
+  (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
 return makeNonLoc(symLHS, Op, symRHS, ResultTy);

As a follow up to the previous version of this patch, I do not think we should 
set the default complexity limit to 1.

What is the relation between this limit and the limit in VisitNonLocSymbolVal? 
If they are related, would it be worthwhile turning these into an analyzer 
option?


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-08-05 Thread Dominic Chen via Phabricator via cfe-commits
ddcc added a comment.

@NoQ ping


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-18 Thread Dominic Chen via Phabricator via cfe-commits
ddcc updated this revision to Diff 107190.
ddcc added a comment.

Minor style fix


https://reviews.llvm.org/D35450

Files:
  include/clang/AST/Expr.h
  include/clang/Config/config.h.cmake
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  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/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,7 +67,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
+  if (index - 1 == 0)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -87,7 +87,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
+  if (index - 1L == 0L)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -117,7 +117,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
+  if (index - 1UL == 0L)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   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:  line36
+// 

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-17 Thread Dominic Chen via Phabricator via cfe-commits
ddcc added a comment.

As an update, after fixing the typo and updating the tests, the assertion in 
`range_casts.c` is no longer triggered and everything seems fine now.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-17 Thread Dominic Chen via Phabricator via cfe-commits
ddcc updated this revision to Diff 106896.
ddcc added a comment.

Fix tests after typo fix


https://reviews.llvm.org/D35450

Files:
  include/clang/AST/Expr.h
  include/clang/Config/config.h.cmake
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  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/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,7 +67,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
+  if (index - 1 == 0)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -87,7 +87,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
+  if (index - 1L == 0L)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -117,7 +117,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
+  if (index - 1UL == 0L)
 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   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:  line36
+// 

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-17 Thread Dominic Chen via Phabricator via cfe-commits
ddcc added a comment.

> Is diff 1 the original diff from https://reviews.llvm.org/D28953? It was ok 
> to reopen it, but the new revision is also fine.

No, diff 1 is already different; it contains most of the bugfixes. I couldn't 
find any way to reopen the previous review, and `arc diff` wouldn't let me 
update a closed review.

> Regarding 1-bit bools: did you notice https://reviews.llvm.org/D32328 and 
> https://reviews.llvm.org/D35041, do they accidentally help?

I did see those changes, but I think they're a little different. The test 
failures I ran into were cases where the input is a 1-bit APSInt, and 
attempting to retrieve the type for that gives a null QualType.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-17 Thread Dominic Chen via Phabricator via cfe-commits
ddcc updated this revision to Diff 106883.
ddcc added a comment.

Fix typo


https://reviews.llvm.org/D35450

Files:
  include/clang/AST/Expr.h
  include/clang/Config/config.h.cmake
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  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: 

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-17 Thread Artem Dergachev via Phabricator via cfe-commits
NoQ added a comment.

I'd have a look soon.

Is diff 1 the original diff from https://reviews.llvm.org/D28953? It was ok to 
reopen it, but the new revision is also fine.

Regarding 1-bit bools: did you notice https://reviews.llvm.org/D32328 and 
https://reviews.llvm.org/D35041, do they accidentally help?




Comment at: include/clang/AST/Expr.h:3096
+  static bool isCommutativeOp(Opcode Opc) {
+return Opc == BO_Mul || Opc == BO_Add || (Opc >= BO_EQ && Opc == BO_Or);
+  }

There seems to be a typo somewhere around the last comparison.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-15 Thread Dominic Chen via Phabricator via cfe-commits
ddcc added a comment.

Compared with https://reviews.llvm.org/D28953, this revision fixes the test 
failure with `PR3991.m` with RangeConstraintManager, and a few other failures 
with Z3ConstraintManager. However, there's one remaining test failure in 
`range_casts.c` that I'm not sure how to resolve. For reference, this is the 
simplified code snippet from that testcase:

  void f15(long foo) {
unsigned index = -1;
if (index < foo) index = foo;
unsigned int tmp = index + 1;
if (tmp == 0)
  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
else
  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  }

In debug mode, an assertion about the system being over-constrained is thrown 
from `ConstraintManager.h`. This is because the new 
`Simplifier::VisitSymbolCast` function will attempt to evaluate the cast 
`(unsigned int) (reg_$0)`, which is suppressed by the call to 
`haveSameType()` in `SimpleSValBuilder::evalCastFromNonLoc` 
(https://reviews.llvm.org/D28955 fixes this, but only for Z3ConstraintManager), 
generating just the symbol `reg_$0`. Subsequently, the analyzer will 
attempt to evaluate the expression `((reg_$0) + 1U) == 0U` with the 
range `reg_$0 : { [4294967296, 9223372036854775807] }`, or `[UINT_MAX 
+ 1, LONG_MAX]`. However, in the case where the assumption is true, 
RangeConstraintManager takes the intersection of the previous range with 
`[UINT_MAX, UINT_MAX]` and produces the empty set, and likewise where the 
assumption is false, the intersection with `[UINT_MAX - 1, 0]` again produces 
the empty set. As a result, both program states are NULL, triggering the 
assertion.

I'm now somewhat inclined to drop the addition of 
`Simplified::VisitSymbolCast()` and those associated testsuite changes, because 
ignoring type casts is clearly incorrect and will introduce both false 
negatives and false positives.


https://reviews.llvm.org/D35450



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


[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-15 Thread Dominic Chen via Phabricator via cfe-commits
ddcc updated this revision to Diff 106758.
ddcc added a comment.

Modify Z3RangeConstraintManager::fixAPSInt() and add Expr::isCommutativeOp()


https://reviews.llvm.org/D35450

Files:
  include/clang/AST/Expr.h
  include/clang/Config/config.h.cmake
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  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
+// 

[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types

2017-07-15 Thread Dominic Chen via Phabricator via cfe-commits
ddcc created this revision.

Generate more IntSymExpr constraints, perform SVal simplification for 
IntSymExpr and SymbolCast constraints, and create fully symbolic SymExprs


https://reviews.llvm.org/D35450

Files:
  include/clang/Config/config.h.cmake
  include/clang/StaticAnalyzer/Checkers/SValExplainer.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  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