[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation
Artem Dergachev via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Sat Jun 17 02:33:20 PDT 2017
NoQ added a comment.
Hmm, curious, having a look. A couple of blind guesses before i actually understand what's going on:
(1) The `simplifySVal()` code has its own complexity threshold:
1060 SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
1061 // Simplification is much more costly than computing complexity.
1062 // For high complexity, it may be not worth it.
1063 if (V.getSymbol()->computeComplexity() > 100)
1064 return V;
1065 return Visit(V.getSymbol());
1066 }
Would it help to decrease `100` to `10` here?
(2) With RangeConstraintManager, simplification is not entirely idempotent: we may simplify a symbol further when one of its sub-symbols gets constrained to a constant in a new state. However, apart from that, we might be able to avoid re-simplifying the same symbol by caching results based on the (symbol, state's constraint data) pair. Probably it may work with Z3 as well.
https://reviews.llvm.org/D28953
More information about the cfe-commits
mailing list