[PATCH] D135397: [clang][dataflow] Add support for a Top value in boolean formulas.

[Gábor Horváth via Phabricator via cfe-commits]

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