ymandel added a comment.
Thanks for the thorough reviews! Agreed on all points, and will address.
================
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue &createTop() {
+ return takeOwnership(std::make_unique<TopValue>());
+ }
----------------
xazax.hun wrote:
> gribozavr2 wrote:
> > Should we be creating a new top every time, or should it be a singleton
> > like true and false?
> >
> > It seems like we explicitly don't care about its identity (or else it would
> > be isomorphic to AtomicBool).
> Good point, a singleton Top might actually simplify some parts of the code.
Good question. That was my initial implementation, but it ran into the problem
that the solver (in `buildBooleanFormula`) maps each unique (by pointer)
subexpression into a fresh SAT variable in . If we use a singleton Top, we need
to modify that algorithm appropriately. I'm open to suggestions, though,
because of the advantages of a singleton Top.
If we assume that a given `Top` is never actually shared in a boolean formula
(unlike other subexpressions, which may be shared), then we can use a singleton
and special case it in `buildBooleanFormula`. I think that's a good assumption,
but am not sure. Thoughts?
================
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:102
+ static bool classof(const Value *Val) { return Val->getKind() == Kind::Top; }
+};
+
----------------
gribozavr2 wrote:
> Since TopValue is a BoolValue, can we form say a ConjunctionValue where LHS
> or RHS is Top?
>
> What if we create such a conjunction twice? It seems like such conjunctions
> would incorrectly compare equal, even though each Top will be replaced with a
> unique fresh variable.
>
> Would it make sense to change our factory functions for boolean formulas to
> eagerly open Top?
>
> Then we wouldn't need a recursive walk in unpackValue().
They would only compare equal if we're using a singleton Top. In fact, that's
not quite right because we have no deep equality on formulas. But, the caching
mechanism would generate the same formula, so the point holds. In that case, we
would need to eagerly open the Top, because we would lose any way to
distinguish them. But, with different Top instances, this wouldn't be
necessary. Overall, it seems like "open top as soon as possible without killing
convergence" is probably our best heuristic, so this seems like a win. But, I'm
pretty sure there are places where it will prevent convergence (on its own --
`widen` will still handle it fine I believe).
Avoiding the recursive walk would be nice.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D135397/new/
https://reviews.llvm.org/D135397
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
