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

[Gábor Horváth via Phabricator via cfe-commits]

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: clang/include/clang/Analysis/FlowSensitive/Solver.h:39
+
+  virtual ~Solver() {}
+
----------------
`= default`? To make this trivially destructible.


================
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
----------------
Shouldn't we make this function variadic (or taking a container) instead of having multiple overloads?


================
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());
----------------
Switch on the kind instead? That way `DisjunctionValue` and `ConjunctionValue` could be handled by the same case.


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:241
+  for (BoolValue *Val : Vals)
+    UnprocessedSubVals.push(Val);
+  while (!UnprocessedSubVals.empty()) {
----------------
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.


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


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D120289