[PATCH] D35450: [analyzer] Support generating and reasoning over more symbolic constraint types
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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