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

[Dominic Chen via Phabricator via cfe-commits]

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 transform unsupported expressions into supported ones.

> We could implement the TODO described below and possibly also lower the MaxComp value. This means that instead of keeping a complex expression and constraints on every symbol used in that expression, we would conjure a new symbol and associate a new constrain derived from the expression with it. (Would this strategy also work for the Z3 case?)

I think it's feasible, but would probably require some more to code to handle `SymbolConjured` (right now all `SymbolData` are treated as variables).

> Would it help to decrease 100 to 10 here?

Yes, changing it to 10 eliminates the excessive recursion; combined runtime drops to 282 sec on the testcases (~8 sec for Range only, ~271 sec for Z3 only; doesn't sum due to separate executions). This appears to be the most straightforward solution.

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

Yeah, that would also fix this issue. In general, I think there's plenty of room for improvements from caching, especially for queries to e.g. `getSymVal()`.


https://reviews.llvm.org/D28953