Expose DataflowAnalysisContext.querySolver().

[bazuzi]

Summary

This allows for use of the same solver used by the DAC for additional solving post-analysis and thus shared use of MaxIterations in WatchedLiteralsSolver.

[ymandel]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

179–182

nit: Given that these are options of Solver::Result, I think you can just delete these lines.

[bazuzi]

Updated function comment to remove unnecessary repetition and include newly-discovered caveat re: flow conditions.

[sammccall]

Thanks!

As discussed offline, I had some concerns about whether there were any cases where it was safe to use formulas separate from the FC that might constrain them.
But we found some: these are formulas produced by the downstream analysis that have known structure.

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

184

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.

184

this should be ArrayRef<BoolValue*> now... sorry for the churn

[bazuzi]

Rebase on main to pull in change from DenseSet to SetVector.

[sammccall]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

184

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)

[bazuzi]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

184

HEAD says SetVector, so updated to that. Is there another change coming that makes it ArrayRef?

184

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.

[gribozavr2]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

184

@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.

[sammccall]

LG as is, sorry for the noise!

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

184

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.

184

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.

[bazuzi]

It looks like D153485 changes the context for the last few comments significantly. What's the appetite for adding yet another child commit to the chain D153485 is in that exposes the solver directly? Instead of committing this and having D153485 make a breaking change to expose the solver directly if that's better in the new context.

[sammccall]

In D153805#4464487, @bazuzi wrote:

It looks like D153485 changes the context for the last few comments significantly. What's the appetite for adding yet another child commit to the chain D153485 is in that exposes the solver directly? Instead of committing this and having D153485 make a breaking change to expose the solver directly if that's better in the new context.

Yeah, that's fewer steps but more stuff stacked on top.
I don't feel strongly - happy to make that change later if you'd like to have this available now.

[bazuzi]

Since the timeline for being able to use this is dependent not only on commits but integrates as well, lets go ahead with this then.

Can someone commit it for me when we're ready?

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

public:
   /// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
   /// returns null.
   const ControlFlowContext *getControlFlowContext(const FunctionDecl *F);
 
   const Options &getOptions() { return Opts; }
 
   Arena &arena() { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);
+
 private:
   friend class Environment;
 
   struct NullableQualTypeDenseMapInfo : private llvm::DenseMapInfo<QualType> {
     static QualType getEmptyKey() {
       // Allow a NULL `QualType` by using a different value as the empty key.
       return QualType::getFromOpaquePtr(reinterpret_cast<Type *>(1));
     }
private:
   /// Adds all constraints of the flow condition identified by `Token` and all
   /// of its transitive dependencies to `Constraints`. `VisitedTokens` is used
   /// to track tokens of flow conditions that were already visited by recursive
   /// calls.
   void addTransitiveFlowConditionConstraints(
       AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
       llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) {
     return querySolver(std::move(Constraints)).getStatus() ==
            Solver::Result::Status::Unsatisfiable;
   }
 
   std::unique_ptr<Solver> S;