[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

[Sam McCall via Phabricator via cfe-commits]

sammccall added a comment.

LG as is, sorry for the noise!



================
Comment at: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
+
----------------
gribozavr2 wrote:
> sammccall wrote:
> > bazuzi wrote:
> > > bazuzi wrote:
> > > > sammccall wrote:
> > > > > sammccall wrote:
> > > > > > FWIW, I'd probably prefer exposing the solver object itself, having all capabilities exposed directly through DataflowAnalysisContext gives it this ugly "god object" quality and the places that we want to use it really just need arena + solver.
> > > > > this should be ArrayRef<BoolValue*> now... sorry for the churn
> > > > HEAD says SetVector, so updated to that. Is there another change coming that makes it ArrayRef?
> > > If all capabilities was more than 1 capability and this function didn't already exist, I'd me more inclined to agree. But requiring users to duplicate the body of this function seems worse to me than forwarding an API from a member.
> > > 
> > > I'm noticing as well that the body of this function adds true and !false constraints to the provided set, which I hadn't been doing when using a solver and for which I can find no documentation indicating that it's necessary. Either we should document why that's done and would need to expect users to know to do it if we expose the solver only directly, or we should remove that from this function.
> > I do think ArrayRef is the right signature here - SetVector is a slightly messy impl detail.
> > 
> > This would mean an unfortunate copy for now but that will go away, see D153485 (which is waiting on the Formula patch to land)
> @sammccall 
> While I'd normally agree, querySolver() incorporates the true and false literals into the formula, so it is actually a lot more useful than the raw solver object. Until we have a different representation of boolean literals, I think this patch is the better in terms of API design.
The public APIs for "set of constraints" are ArrayRef (on Solver::solve).
SetVector was how we maintained determinism while deduplicating inside DACtx, this function is SetVector specifically because it was private.

Nevertheless, let's go with this change as-is, the alternatives are complicated for now.
I'll try to simplify the API a bit once the prereqs are in place.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:183
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
+
----------------
sammccall wrote:
> gribozavr2 wrote:
> > sammccall wrote:
> > > bazuzi wrote:
> > > > bazuzi wrote:
> > > > > sammccall wrote:
> > > > > > sammccall wrote:
> > > > > > > FWIW, I'd probably prefer exposing the solver object itself, having all capabilities exposed directly through DataflowAnalysisContext gives it this ugly "god object" quality and the places that we want to use it really just need arena + solver.
> > > > > > this should be ArrayRef<BoolValue*> now... sorry for the churn
> > > > > HEAD says SetVector, so updated to that. Is there another change coming that makes it ArrayRef?
> > > > If all capabilities was more than 1 capability and this function didn't already exist, I'd me more inclined to agree. But requiring users to duplicate the body of this function seems worse to me than forwarding an API from a member.
> > > > 
> > > > I'm noticing as well that the body of this function adds true and !false constraints to the provided set, which I hadn't been doing when using a solver and for which I can find no documentation indicating that it's necessary. Either we should document why that's done and would need to expect users to know to do it if we expose the solver only directly, or we should remove that from this function.
> > > I do think ArrayRef is the right signature here - SetVector is a slightly messy impl detail.
> > > 
> > > This would mean an unfortunate copy for now but that will go away, see D153485 (which is waiting on the Formula patch to land)
> > @sammccall 
> > While I'd normally agree, querySolver() incorporates the true and false literals into the formula, so it is actually a lot more useful than the raw solver object. Until we have a different representation of boolean literals, I think this patch is the better in terms of API design.
> The public APIs for "set of constraints" are ArrayRef (on Solver::solve).
> SetVector was how we maintained determinism while deduplicating inside DACtx, this function is SetVector specifically because it was private.
> 
> Nevertheless, let's go with this change as-is, the alternatives are complicated for now.
> I'll try to simplify the API a bit once the prereqs are in place.
> Either we should document why that's done and would need to expect users to know to do it if we expose the solver only directly, or we should remove that from this function.

I'll just eliminate the requirement to do so at all, soon.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D153805/new/

https://reviews.llvm.org/D153805