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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
