[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. Closed by commit rG53dcd9efd16f: [clang][dataflow] Add SAT solver interface and implementation (authored by sgatev). Repository: rG LLVM Github Monorepo CHANGES

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

sgatev added a comment. > Are there plans to get a model/assignment of the variables from the solver? > That could be helpful for generating warning messages in the future :) Absolutely! That was only discussed briefly so far. One challenge would be distilling this model to present only

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

sgatev updated this revision to Diff 411400. sgatev marked 5 inline comments as done. sgatev added a comment. Address reviewers' comments. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D120289/new/ https://reviews.llvm.org/D120289 Files:

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

xazax.hun accepted this revision. xazax.hun added a comment. Overall, looks good to me. Some nits inline. Are there plans to get a model/assignment of the variables from the solver? That could be helpful for generating warning messages in the future :) Comment at:

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

xazax.hun added a comment. In D120289#3341008 , @sgatev wrote: > it seems tailored to the Z3 API. As far as I understand, there were downstream patches that used the same API with other SMT solvers. The authors did not upstream it because they did not

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

sgatev added a comment. In D120289#3338262 , @xazax.hun wrote: > In D120289#3338244 , @sgatev wrote: > >>> I wonder if it would make sense to have a SAT base class for the SMT API >>> and reuse that here? >> >>

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

xazax.hun added a comment. In D120289#3338244 , @sgatev wrote: >> I wonder if it would make sense to have a SAT base class for the SMT API and >> reuse that here? > > I think that on a high level we can either 1) integrate the SMT API types > deeply

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

sgatev added a comment. > Did you look into reusing existing SAT solvers like miniSAT? What was the > main reason for rolling our own instead of picking something up off the > shelves? Mainly to provide a lightweight out-of-the-box alternative. The solver interface is simple so one should be

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

xazax.hun added a comment. Note that, there are already precedents for Clang using solver tech from LLVM. E.g., the clang static analyzer's Z3-based refutation support is using the SMT API in LLVM, and there are experiments integrating yet another solver with the SA:

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

xazax.hun added a comment. Hi! Just a quick high level question. Did you look into reusing existing SAT solvers like miniSAT? What was the main reason for rolling our own instead of picking something up off the selves? Also, LLVM already has a SMT API

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

sgatev added inline comments. Comment at: clang/include/clang/Analysis/FlowSensitive/Solver.h:39 + /// All elements in `Vals` must be non-null. + virtual Result solve(llvm::DenseSet Vals) = 0; +}; ymandel wrote: > Which `Result` is expected if the `Solver`

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

sgatev updated this revision to Diff 410460. sgatev marked 6 inline comments as done. sgatev added a comment. Address reviewers' comments. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D120289/new/ https://reviews.llvm.org/D120289 Files:

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

ymandel accepted this revision. ymandel added inline comments. This revision is now accepted and ready to land. Comment at: clang/include/clang/Analysis/FlowSensitive/Solver.h:39 + /// All elements in `Vals` must be non-null. + virtual Result solve(llvm::DenseSet Vals) = 0;

[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

sgatev created this revision. sgatev added reviewers: ymandel, xazax.hun, gribozavr2. Herald added subscribers: tschuett, steakhal, mstorsjo, rnkovacs, mgorny. sgatev requested review of this revision. Herald added a project: clang. This is part of the implementation of the dataflow analysis