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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to