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

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

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