xazax.hun added inline comments.
================
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue &createTop() {
+ return takeOwnership(std::make_unique<TopValue>());
+ }
----------------
ymandel wrote:
> xazax.hun wrote:
> > gribozavr2 wrote:
> > > ymandel wrote:
> > > > 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?
> > > I see. Could you add some direct tests for the SAT solver with formulas
> > > that include Top to check the behavior we care about?
> > >
> > Given the discussion so far, it looks like having a singleton top has its
> > own problems. I'm fine with the current solution for now, let's see if the
> > overall approach works and we will see if this needs any further
> > optimization later. +1 to Dmitry, some unit tests like Top && Top generated
> > multiple times will not yield the same expression could be useful. If
> > someone in the future tries to introduce singleton Top, they will see those
> > tests fail and see why we did not have that in the first place and what
> > problems need to be solved to introduce it.
> I've added a test that direct creation of two Tops results in distinct values
> (by pointer) and inequivalent (per the solver), and some tests relating to
> the solver which will fail if you switch to a singleton Top. I didn't see
> much room for a `Top && Top` test, since that seems redundant with the
> simpler tests. I think the inequivalence tests satisfies Dmitri's concern
> with conjunctions involving Top, but, happy to add more if you disagree.
>
> I should note, though: `Top iff Top` is true when both Tops are identical
> values (pointer equality) but not when they are distinct values. This doesn't
> seem right to me -- I think we should have one answer for `Top iff Top` and I
> think it should be `false`. So, in some sense, even the current scheme
> suffers from the some of the drawbacks of the singleton scheme. I think this
> is ok for now, but it does seem to encourage improvement in further patches.
> I think we should have one answer for Top iff Top and I think it should be
> false.
I'd love to see this as a TODO comment.
================
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:527-528
+ auto *Prop2 = Val2.getProperty("has_value");
+ return Prop1 == Prop2 || (Prop1 != nullptr && Prop2 != nullptr &&
+ isTop(*Prop1) && isTop(*Prop2));
}
----------------
ymandel wrote:
> xazax.hun wrote:
> > I feel like this logic is repeated multiple times. I wonder if we should
> > define an `operator==` for `const BoolValue*`.
> Agreed. I want to wait until we settle on the representation and then we can
> consider this operator. But, if we end up with a singleton Top then I think
> we can hold off.
We ended up not going with a singleton Top, let's reconsider the overloaded
operator.
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
