[PATCH] D153366: [dataflow] Add dedicated representation of boolean formulas

[Martin Böhme via Phabricator via cfe-commits]

mboehme added a comment.

High-level comment: I like the separation of concerns that this introduces.

Would you like me to review https://reviews.llvm.org/D153469 or should we wait for this patch to converge first?



================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:22
+namespace clang::dataflow {
+class Formula;
+
----------------
Put this right above the class definition below? (This is just needed for the `alignas(Formula *)`, right?)


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:38
+/// A boolean expression such as "true" or "V1 & !V2".
+/// Expressions may refer to boolean atomic variables, identified by number.
+///
----------------
Is this important to state? (It's an implementation detail of `Atom`, essentially?)


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:47
+/// trailing objects.
+class alignas(Formula *) Formula {
+public:
----------------
Do you need the `alignas` because the pointers to operands are stored as trailing objects? Can you add a short comment to that effect?


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:71
+  ArrayRef<const Formula *> operands() const {
+    return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
+                    numOperands(kind()));
----------------
Is this technically legal? (I've taken a look, but the definition of similar types makes my eyes glaze over.)

Why not use `TrailingObjects` instead? (I'm not really familiar with `TrailingObjects`, so there may be good reasons against it -- just asking because it seems like an obvious existing mechanism that could be used here.)


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:82
+                         ArrayRef<const Formula *> Operands,
+                         unsigned Value = 0);
+
----------------
This looks like an "internal" API -- it's really only intended for use by `Arena`, right?

Maybe add a comment indicating that it's not intended to be used directly?


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:104
+  Kind FormulaKind;
+  unsigned Value;
+};
----------------
Why not give this type `Atom`?


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:218
 
-  BooleanFormula Formula(NextVar - 1, std::move(Atomics));
+  BooleanFormula Form(NextVar - 1, std::move(Atomics));
   std::vector<bool> ProcessedSubVals(NextVar, false);
----------------
Now that we've added `Formula`, it's pretty confusing that we also have `BooleanFormula`.

I assume this is one of the renamings that you want to get to later? I guess `BooleanFormula` becomes something like `CnfFormula` (would like to do `3CnfFormula`, but you can't start with a digit... :( )


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153366