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

[Sam McCall via Phabricator via cfe-commits]

sammccall added a comment.

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

Similarly it'd be great to get high-level feedback there: whether the design of FormulaBoolValue is right, whether the changes to use Atom/Formula more pervasively seem sensible etc.
For the details, probably better to wait until this one is stable to avoid churn...

Thanks!



================
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()));
----------------
mboehme wrote:
> 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.)
> Is this technically legal?

Yeah, it's OK: similar types etc is not relevant because these pointers are not pointing to objects of different types: there's an object of type Formula at one address that has a lifetime that begins at the constructor (but it's trivially destructible and never destroyed), and then objects of type `Formula*` at higher addresses - these don't overlap, and are both part of the chunks of memory provided by malloc.

> Why not use TrailingObjects instead? 

TrailingObjects is complicated and ugly - it *can* work for this, but I don't think it's actually easier to understand. (Do a code search for "this + 1" in LLVM - this is often done "by hand" instead of with TrailingObjects for simple cases like this one).

e.g. here we have a little magic in create() and a little in operands(). TrailingObjects equally needs ~2 pieces of magic, they're *slightly* less scary, but they also don't relate directly to the memory layout, and I don't think you can have a meaningful understanding of what this is for without also thinking about the memory layout.

TrailingObjects shines when the pointer arithmetic gets complicated, though...


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:104
+  Kind FormulaKind;
+  unsigned Value;
+};
----------------
mboehme wrote:
> Why not give this type `Atom`?
I don't think it should always be Atom, even when it's used

see D153485 where I add a "Literal" formula and use value to distinguish true/false


================
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);
----------------
mboehme wrote:
> 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... :( )
Agree this is an unfortunate conflict and we should probably rename this local one.
(Just because it's more important that the public type gets the good name)

CNFFormula or just CNF SGTM.
I'll leave this open and do it as a followup if that's OK, the patch is noisy as is.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153366