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

ddcc added a comment. Reverted in https://reviews.llvm.org/rL307853 Repository: rL LLVM https://reviews.llvm.org/D28953 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

ddcc added a comment. Reverted in https://reviews.llvm.org/rL307853 Repository: rL LLVM https://reviews.llvm.org/D28953 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

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

This revision was automatically updated to reflect the committed changes. Closed by commit rL307833: [analyzer] Support generating and reasoning over more symbolic constraint types (authored by ddcc). Changed prior to commit: https://reviews.llvm.org/D28953?vs=106084=106284#toc Repository:

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

ddcc updated this revision to Diff 106084. ddcc added a comment. Split plist-macros.cpp, and update analyzer_test.py to support tests that require not z3 https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp

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

NoQ accepted this revision. NoQ added a comment. This revision is now accepted and ready to land. This looks great, thank you very much. Comment at: test/Analysis/plist-macros.cpp:2 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s

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

ddcc added a comment. I've also uploaded the results to https://dcddcc.com/csa https://reviews.llvm.org/D28953 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

ddcc added a comment. I tested the following software, both before and after applying this patch, using RangeConstraintManager. Software, Version, Compile Time (before), Bugs Reported (before), Compile Time (after), Bugs Reported (after) openssl, 1.1.0f, 11 min, 126, 12 min, 126 sqlite,

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

ddcc updated this revision to Diff 105913. ddcc marked an inline comment as done. ddcc added a comment. Drop duplicate code https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp

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

NoQ added a comment. Because this patch affects the default behavior, i think it's necessary to understand the performance impact on a large codebase. I may lend a hand eventually, but if you're in a hurry you could probably at least run an overnight analysis over llvm and sqlite with range

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

ddcc added a comment. ping https://reviews.llvm.org/D28953 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

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

ddcc updated this revision to Diff 103239. ddcc added a comment. Rebase, decrease simplification complexity https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

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

ddcc added a comment. > Can we drop computing these for some expressions that we know the > RangeConstraintManager will not utilize? It's possible, though I'm not sure what the actual limitations of the RangeConstraintManager are, since there are a lot of intermediate steps that attempt to

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

NoQ added a comment. Hmm, curious, having a look. A couple of blind guesses before i actually understand what's going on: (1) The `simplifySVal()` code has its own complexity threshold: 1060 SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) { 1061 // Simplification is much more

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

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

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

ddcc added inline comments. Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:356 QualType ResultTy) { - if (!State->isTainted(RHS) && !State->isTainted(LHS)) -return UnknownVal(); zaks.anna wrote: > I am concerned that

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

zaks.anna added inline comments. Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:356 QualType ResultTy) { - if (!State->isTainted(RHS) && !State->isTainted(LHS)) -return UnknownVal(); I am concerned that removing the

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

ddcc updated this revision to Diff 99521. ddcc added a comment. Fix typo in SymbolCast simplification https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

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

ddcc added a comment. I've updated this revision to account for the recent SVal simplification commit by @NoQ, but now there is an exponential recursion problem that prevents testcase `PR24184.cpp` from terminating, due to an interaction between `Simplifier::VisitNonLocSymbolVal()` and

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

ddcc updated this revision to Diff 99392. ddcc added a comment. Address SVal simplification from https://reviews.llvm.org/D31886 https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp

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

ddcc updated this revision to Diff 98545. ddcc added a comment. Rebase https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp test/Analysis/bitwise-ops.c

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

ddcc added a comment. It's been a while since I looked at the code, but I don't believe that all of the new constraints are necessarily unsupported by the current range constraint manager. Rather, they were just not being generated by the SimpleSValBuilder. The changes pass the testsuite for

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

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

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

ddcc updated this revision to Diff 93589. ddcc added a comment. Rebase https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp test/Analysis/bitwise-ops.c

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

ddcc updated this revision to Diff 85314. ddcc added a comment. Rebase https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp test/Analysis/bitwise-ops.c

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

ddcc updated this revision to Diff 85139. ddcc added a comment. Fix rebase https://reviews.llvm.org/D28953 Files: include/clang/StaticAnalyzer/Checkers/SValExplainer.h lib/StaticAnalyzer/Core/SValBuilder.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp test/Analysis/bitwise-ops.c