martinboehme wrote: > > Yes, significantly faster, and fewer SAT solver timeouts. > > The Clang Static Analyzer is going one step further. It is pruning the > analysis state really aggressively, it is relying on liveness analysis, and > whenever the value of a variable is dead (would not be read in future program > points), the corresponding symbols will be pruned from the state. For the > really deep path sensitive analysis the CSA is doing, it was really > beneficial performance-wise. On the other hand, this approach definitely > introduced complexity. The CSA is basically doing garbage collection to > figure out what part of the program state is unreachable (e.g., can we read a > value through some pointers?). Moreover, actually pruning the analysis state > is tricky. If we had `x < y` and `y < z` in our constraints, to correctly > prune `y`, we would need to have a new set of constraints like `x+1 < z`. > Simply dropping everything with `y` would lose information.
Thanks for the input from CSA! Yes, doing this more broadly would surely be a win -- but also much more difficult than for expression evaluation, which makes it easy to determine how long a value will be needed. Something to keep in mind for the future. By the way, we've also been discussing dropping clauses from the flow condition when we can prove we no longer need them. Do you happen to know any references to similar work, maybe in CSA? https://github.com/llvm/llvm-project/pull/82611 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
