[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 ___

[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?

[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

[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

[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

[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

[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.

[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

[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)

[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

[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)

[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

[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

[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

[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`

[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

[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

[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

[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

[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