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

Wed Feb 23 11:15:03 PST 2022

sgatev added a comment.

In D120289#3338262 <https://reviews.llvm.org/D120289#3338262>, @xazax.hun wrote:

> In D120289#3338244 <https://reviews.llvm.org/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 into the dataflow framework and use that solver interface directly or 2) have a layer that translates from the dataflow `BoolValue` types to the SMT API types. At this point I'm not convinced that we should go for 1).
>
> Could you elaborate on what would be the main disadvantage of using 1)? (The advantage would be that we could very easily switch to Z3 any time.)

Let me clarify 1) because I see two options there as well:

1.a) We replace the `BoolValue` hierarchy in the dataflow framework with `SMTExprRef`.
This feels too committal. The dataflow interfaces are still not sufficiently developed and there isn't a clear benefit (e.g. performance) with this approach so I'd rather not couple them for now. There might also be benefits to having a structured representation (as opposed to using opaque values such as `SMTExprRef`) that we need to consider. I think this is a viable long-term option, though.

1.b) We add an `SMTExprRef` member to each boolean value (atom, conjunction, disjunction, and negation) in the dataflow framework.
I like this better than 1.a). The main disadvantage I see is that `SMTSolver` is a huge interface and on the surface it seems tailored to the Z3 API. >From that perspective it also feels more committal than necessary, given that we can make do with a simple one-method interface for now. I think this is a good long-term option if we think the SMT API is the most appropriate solver interface.

I find 2) least committal as it keeps the dataflow framework and the solver separate. For a simple integration with Z3 I can provide an implementation of `clang::dataflow::Solver` using the SMT API. That should boil down to translating dataflow types to SMT types.

What do you think about this? Any other options we should consider?

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D120289/new/

https://reviews.llvm.org/D120289