| Issue |
204593
|
| Summary |
Add tiering or configuration of Solvers for Clang Dataflow Framework
|
| Labels |
clang:dataflow
|
| Assignees |
|
| Reporter |
jvoung
|
Currently, the CDF checkers default to WatchedLiteralsSolver, which is okay for simple problems but doesn't scale well to more complex problems (see reports like issue #69369).
Internally, we've been using tiers of solvers (a) start with WatchedLiteralsSolver for only a few iterations, and then (b) switch to a production-grade solver after that, and that has worked better. For (b), we could for example use Z3 w/ some limits set as well.
The default should be improved in the [diagnoseFunction](https://github.com/llvm/llvm-project/blob/3c33c36d925f5d278501fea55ef5a2e1f8f331ca/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h#L322) entry point, but we should also be able to take a custom solver (e.g., it is currently configurable though, e.g., [DataflowAnalysisContext](https://github.com/llvm/llvm-project/blob/3c33c36d925f5d278501fea55ef5a2e1f8f331ca/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h#L91) if you instead use the [runDataflowAnalysis](https://github.com/llvm/llvm-project/blob/3c33c36d925f5d278501fea55ef5a2e1f8f331ca/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h#L234) entry point)
![]()
_______________________________________________
llvm-bugs mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-bugs
