ymandel marked 5 inline comments as done.
ymandel added inline comments.
================
Comment at:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:157
+ TopValue &createTop() {
+ return takeOwnership(std::make_unique<TopValue>());
+ }
----------------
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.
================
Comment at: clang/include/clang/Analysis/FlowSensitive/Value.h:100
+public:
+ explicit TopBoolValue() : BoolValue(Kind::TopBool) {}
+
----------------
sgatev wrote:
> `explicit` seems unnecessary.
agreed. looks like a copy-paste error on my part.
================
Comment at:
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp:1220
+ (void)0;
+ /*[[p2]]*/
+ }
----------------
sgatev wrote:
> Why do we need to check two code points here and in the test below? It's not
> obvious what the difference between `p1` and `p2` is.
added comments to both tests to explain motivation. The second one is actually
a regression test since my original version had a bug in its handling of
lvalues *not* in rvalue position.
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
