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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
