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

[Artem Dergachev via Phabricator via cfe-commits]

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