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

[Stanislav Gatev via Phabricator via cfe-commits]

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 relevant information to the user. That could also be best effort, of course. It's certainly something I think we should provide at some point.



================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:159
+  /// Adds the 3-literal `L1 v L2 v L3` clause to the formula.
+  void addClause(Literal L1, Literal L2, Literal L3) {
+    // The literals are guaranteed to be distinct from properties of BoolValue
----------------
xazax.hun wrote:
> Shouldn't we make this function variadic (or taking a container) instead of having multiple overloads?
I'd like to avoid containers here to minimize allocations. I'd love to use a fold expression, but that's C++ 17. I opted for setting default values for the last two arguments.


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:213
+    // Visit the sub-values of `Val`.
+    if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+      UnprocessedSubVals.push(&C->getLeftSubValue());
----------------
xazax.hun wrote:
> Switch on the kind instead? That way `DisjunctionValue` and `ConjunctionValue` could be handled by the same case.
Unfortunately, I don't think we can handle them in the same case because they don't share a parent that represents a binary operation. Perhaps an improvement worth considering, as we discussed in one of the previous patches.


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:241
+  for (BoolValue *Val : Vals)
+    UnprocessedSubVals.push(Val);
+  while (!UnprocessedSubVals.empty()) {
----------------
xazax.hun wrote:
> While I get that this should be empty before this loop due to the loop condition at the previous use, but I find such code confusing. I'd prefer to either use a separate queue or have at least an assert to remind us that this one should be a clean container before the loop.
I agree that this would be an improvement. I opted for narrowing the scope of the first container and adding a second container for this operation.


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:355
+
+    LevelVars.resize(Formula.LargestVar + 1);
+
----------------
xazax.hun wrote:
> Shouldn't we call the right ctor directly in the initialization list instead of resizing a default constructed vector?
Makes complete sense. Updated.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D120289