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

Fri Jun 23 00:05:53 PDT 2023

mboehme added a comment.

In D153366#4441758 <https://reviews.llvm.org/D153366#4441758>, @sammccall wrote:

>> 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!

Will do!

================
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()));
----------------
sammccall wrote:
> 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...
> > 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.

Thanks for the explanation!

Is it worth putting a (condensed) version of this in a comment, or is this well-known enough that it's not worth it?

> > 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...

Again, thanks for the explanation. I don't have any experience with `TrailingObjects` except for using classes that are implemented using it, so thanks for filling me in.

================
Comment at: clang/include/clang/Analysis/FlowSensitive/Formula.h:104
+  Kind FormulaKind;
+  unsigned Value;
+};
----------------
sammccall wrote:
> 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
Ah, I understand now.

Maybe add a comment somewhere to explain this distinction? (If it had me scratching my head, it might do so for others too.)

================
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);
----------------
sammccall wrote:
> 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.
Yes, please do leave it open. This should happen later, just wanted to clarify that that's the plan.

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153366