[dataflow] Make SAT solver deterministic

[sammccall]

Summary

The SAT solver imported its constraints by iterating over an unordered DenseSet.
The path taken, and ultimately the runtime, the specific solution found, and
whether it would time out or complete could depend on the iteration order.

Instead, have the caller specify an ordered collection of constraints.
If this is built in a deterministic way, the system can have deterministic
behavior.
(The main alternative is to sort the constraints by value, but this option
is simpler today).

A lot of nondeterminism still appears to be remain in the framework, so today
the solver's inputs themselves are not deterministic yet.

[xazax.hun]

Is there a measurable perf cost for this determinism?

[sammccall]

In D153584#4443796, @xazax.hun wrote:

Is there a measurable perf cost for this determinism?

I'm going to say no...
All the extra cost is paid in addTransitiveFlowConditionConstraints. (We were building a set, now we're building a set + vector. The sat solver is actually doing *less* work now). I can't measure any difference in that function's runtime, and it's cheap enough to be trivial anyway.

On all of ClangAnalysisFlowSensitiveTests (release+asserts), with this patch:

• total time is 7.5s
• clang parsing is 6.1s (81%)
• sat solving in DataflowAnalysisContext is 75ms (1.0%)
• addTransitiveFlowConditionConstraints is 2.5ms (0.033%)

even if 100% of addTransitiveFlowConditionConstraints was added by this patch, it's still negligible compared to actual sat solving. These are toy examples, but sat solving scales worse almost by definition.

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

 #include "clang/AST/TypeOrdering.h"
 #include "clang/Analysis/FlowSensitive/Arena.h"
 #include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
+#include "llvm/ADT/SetVector.h"
 #include "llvm/Support/Compiler.h"
 #include <cassert>
 #include <memory>
 #include <optional>
 #include <type_traits>
 #include <utility>
 #include <vector>
 
private:
   /// context.
   llvm::DenseSet<const FieldDecl *> getReferencedFields(QualType Type);
 
   /// 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::DenseSet<BoolValue *> &Constraints,
+      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::DenseSet<BoolValue *> Constraints);
+  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::DenseSet<BoolValue *> Constraints) {
+  bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) {
     return querySolver(std::move(Constraints)).getStatus() ==
            Solver::Result::Status::Unsatisfiable;
   }
 
   std::unique_ptr<Solver> S;
   std::unique_ptr<Arena> A;
 
   // Maps from program declarations and statements to storage locations that are

clang/include/clang/Analysis/FlowSensitive/DebugSupport.h

 /// Atomic booleans appearing in the boolean value `Constraints` are assigned to
 /// labels either specified in `AtomNames` or created by default rules as B0,
 /// B1, ...
 ///
 /// Requirements:
 ///
 ///   Names assigned to atoms should not be repeated in `AtomNames`.
 std::string debugString(
-    const llvm::DenseSet<BoolValue *> &Constraints,
+    const llvm::ArrayRef<BoolValue *> Constraints,
     llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
 
 /// Returns a string representation for `Constraints` - a collection of boolean
 /// formulas and the `Result` of satisfiability checking.
 ///
 /// Atomic booleans appearing in `Constraints` and `Result` are assigned to
 /// labels either specified in `AtomNames` or created by default rules as B0,
 /// B1, ...
 ///
 /// Requirements:
 ///
 ///   Names assigned to atoms should not be repeated in `AtomNames`.
 std::string debugString(
     ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
     llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-inline std::string debugString(
-    const llvm::DenseSet<BoolValue *> &Constraints,
-    const Solver::Result &Result,
-    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}) {
-  std::vector<BoolValue *> ConstraintsVec(Constraints.begin(),
-                                          Constraints.end());
-  return debugString(ConstraintsVec, Result, std::move(AtomNames));
-}
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_

clang/include/clang/Analysis/FlowSensitive/Solver.h

 //  dataflow analyses.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 
 #include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
+#include "llvm/Support/Compiler.h"
 #include <optional>
+#include <vector>
 
 namespace clang {
 namespace dataflow {
 
 /// An interface for a SAT solver that can be used by dataflow analyses.
 class Solver {
 public:
   struct Result {
public:
   virtual ~Solver() = default;
 
   /// Checks if the conjunction of `Vals` is satisfiable and returns the
   /// corresponding result.
   ///
   /// Requirements:
   ///
   ///  All elements in `Vals` must not be null.
-  virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0;
+  virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0;
+
+  LLVM_DEPRECATED("Pass ArrayRef for determinism", "")
+  virtual Result solve(llvm::DenseSet<BoolValue *> Vals) {
+    return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end())));
+  }
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H

clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h

 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseSet.h"
+#include "llvm/ADT/ArrayRef.h"
 #include <limits>
 
 namespace clang {
 namespace dataflow {
 
 /// A SAT solver that is an implementation of Algorithm D from Knuth's The Art
 /// of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is based on
 /// the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, keeps references to a
public:
 
   // `Work` specifies a computational limit on the solver. Units of "work"
   // roughly correspond to attempts to assign a value to a single
   // variable. Since the algorithm is exponential in the number of variables,
   // this is the most direct (abstract) unit to target.
   explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
       : MaxIterations(WorkLimit) {}
 
-  Result solve(llvm::DenseSet<BoolValue *> Vals) override;
+  Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

 //===----------------------------------------------------------------------===//
 
 #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "clang/Analysis/FlowSensitive/Logger.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/SetOperations.h"
+#include "llvm/ADT/SetVector.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/Debug.h"
 #include "llvm/Support/FileSystem.h"
 #include "llvm/Support/Path.h"
 #include <cassert>
 #include <memory>
 #include <utility>
 
DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
   FlowConditionDeps[&Token].insert(&FirstToken);
   FlowConditionDeps[&Token].insert(&SecondToken);
   addFlowConditionConstraint(
       Token, arena().makeOr(FirstToken, SecondToken));
   return Token;
 }
 
 Solver::Result
-DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
+DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) {
   Constraints.insert(&arena().makeLiteral(true));
-  Constraints.insert(
-      &arena().makeNot(arena().makeLiteral(false)));
-  return S->solve(std::move(Constraints));
+  Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
+  return S->solve(Constraints.getArrayRef());
 }
 
 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
                                                    BoolValue &Val) {
   // Returns true if and only if truth assignment of the flow condition implies
   // that `Val` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
   // to show that assuming `Val` is false makes the constraints induced by the
   // flow condition unsatisfiable.
-  llvm::DenseSet<BoolValue *> Constraints = {&Token,
-                                             &arena().makeNot(Val)};
+  llvm::SetVector<BoolValue *> Constraints;
+  Constraints.insert(&Token);
+  Constraints.insert(&arena().makeNot(Val));
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
 bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
   // Returns true if and only if we cannot prove that the flow condition can
   // ever be false.
-  llvm::DenseSet<BoolValue *> Constraints = {
-      &arena().makeNot(Token)};
+  llvm::SetVector<BoolValue *> Constraints;
+  Constraints.insert(&arena().makeNot(Token));
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
 bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
                                                    BoolValue &Val2) {
-  llvm::DenseSet<BoolValue *> Constraints = {
-      &arena().makeNot(arena().makeEquals(Val1, Val2))};
-  return isUnsatisfiable(Constraints);
+  llvm::SetVector<BoolValue*> Constraints;
+  Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));
+  return isUnsatisfiable(std::move(Constraints));
 }
 
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
-    AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
+    AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
     llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
   auto Res = VisitedTokens.insert(&Token);
   if (!Res.second)
     return;
 
   auto ConstraintsIt = FlowConditionConstraints.find(&Token);
   if (ConstraintsIt == FlowConditionConstraints.end()) {
     Constraints.insert(&Token);
for (AtomicBoolValue *DepToken : DepsIt->second) {
       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
                                             VisitedTokens);
     }
   }
 }
 
 void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
                                                 llvm::raw_ostream &OS) {
-  llvm::DenseSet<BoolValue *> Constraints = {&Token};
+  llvm::SetVector<BoolValue *> Constraints;
+  Constraints.insert(&Token);
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
 
   llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
       {&arena().makeLiteral(false), "False"},
       {&arena().makeLiteral(true), "True"}};
-  OS << debugString(Constraints, AtomNames);
+  OS << debugString(Constraints.getArrayRef(), AtomNames);
 }
 
 const ControlFlowContext *
 DataflowAnalysisContext::getControlFlowContext(const FunctionDecl *F) {
   // Canonicalize the key:
   F = F->getDefinition();
   if (F == nullptr)
     return nullptr;

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

std::string debugString(const BoolValue &B, size_t Depth = 0) {
     }
     default:
       llvm_unreachable("Unhandled value kind");
     }
     auto Indent = Depth * 4;
     return formatv("{0}", fmt_pad(S, Indent, 0));
   }
 
-  std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) {
-    std::vector<std::string> ConstraintsStrings;
-    ConstraintsStrings.reserve(Constraints.size());
-    for (BoolValue *Constraint : Constraints) {
-      ConstraintsStrings.push_back(debugString(*Constraint));
-    }
-    llvm::sort(ConstraintsStrings);
-
+  std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) {
     std::string Result;
-    for (const std::string &S : ConstraintsStrings) {
-      Result += S;
+    for (const BoolValue *S : Constraints) {
+      Result += debugString(*S);
       Result += '\n';
     }
     return Result;
   }
 
   /// Returns a string representation of a set of boolean `Constraints` and the
   /// `Result` of satisfiability checking on the `Constraints`.
   std::string debugString(ArrayRef<BoolValue *> &Constraints,

 
 std::string
 debugString(const BoolValue &B,
             llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
   return DebugStringGenerator(std::move(AtomNames)).debugString(B);
 }
 
 std::string
-debugString(const llvm::DenseSet<BoolValue *> &Constraints,
+debugString(llvm::ArrayRef<BoolValue *> Constraints,
             llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
   return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
 }
 
 std::string
 debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
             llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
   return DebugStringGenerator(std::move(AtomNames))
       .debugString(Constraints, Result);
 }
 
 } // namespace dataflow
 } // namespace clang

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

 #include <cstdint>
 #include <iterator>
 #include <queue>
 #include <vector>
 
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/STLExtras.h"
 
 namespace clang {
 namespace dataflow {
 
 // `WatchedLiteralsSolver` is an implementation of Algorithm D from Knuth's
struct BooleanFormula {
   /// Returns the literals of clause `C`.
   llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const {
     return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C));
   }
 };
 
 /// Converts the conjunction of `Vals` into a formula in conjunctive normal
 /// form where each clause has at least one and at most three literals.
-BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
+BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) {
   // The general strategy of the algorithm implemented below is to map each
   // of the sub-values in `Vals` to a unique variable and use these variables in
   // the resulting CNF expression to avoid exponential blow up. The number of
   // literals in the resulting formula is guaranteed to be linear in the number
   // of sub-values in `Vals`.
 
   // Map each sub-value in `Vals` to a unique variable.
   llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
class WatchedLiteralsSolverImpl {
   /// element at index 1.
   std::vector<Assignment> VarAssignments;
 
   /// A set of unassigned variables that appear in watched literals in
   /// `Formula`. The vector is guaranteed to contain unique elements.
   std::vector<Variable> ActiveVars;
 
 public:
-  explicit WatchedLiteralsSolverImpl(const llvm::DenseSet<BoolValue *> &Vals)
+  explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals)
       : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
         LevelStates(Formula.LargestVar + 1) {
     assert(!Vals.empty());
 
     // Initialize the state at the root level to a decision so that in
     // `reverseForcedMoves` we don't have to check that `Level >= 0` on each
     // iteration.
     LevelStates[0] = State::Decision;
for (Literal Lit : watchedLiterals()) {
       if (ActiveVarsSet.contains(Var))
         continue;
       return false;
     }
     return true;
   }
 };
 
-Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) {
+Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) {
   if (Vals.empty())
     return Solver::Result::Satisfiable({{}});
   auto [Res, Iterations] =
       WatchedLiteralsSolverImpl(Vals).solve(MaxIterations);
   MaxIterations = Iterations;
   return Res;
 }
 
 } // namespace dataflow
 } // namespace clang

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

auto Expected = R"((or
     (or
         True
         B1)))";
   EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
               StrEq(Expected));
 }
 
 TEST(ConstraintSetDebugStringTest, Empty) {
-  llvm::DenseSet<BoolValue *> Constraints;
+  llvm::ArrayRef<BoolValue *> Constraints;
   EXPECT_THAT(debugString(Constraints), StrEq(""));
 }
 
 TEST(ConstraintSetDebugStringTest, Simple) {
   ConstraintContext Ctx;
-  llvm::DenseSet<BoolValue *> Constraints;
+  std::vector<BoolValue *> Constraints;
   auto X = cast<AtomicBoolValue>(Ctx.atom());
   auto Y = cast<AtomicBoolValue>(Ctx.atom());
-  Constraints.insert(Ctx.disj(X, Y));
-  Constraints.insert(Ctx.disj(X, Ctx.neg(Y)));
+  Constraints.push_back(Ctx.disj(X, Y));
+  Constraints.push_back(Ctx.disj(X, Ctx.neg(Y)));
 
   auto Expected = R"((or
     X
-    (not
-        Y))
+    Y)
 (or
     X
-    Y)
+    (not
+        Y))
 )";
   EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),
               StrEq(Expected));
 }
 
 Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
-  llvm::DenseSet<BoolValue *> ConstraintsSet(Constraints.begin(),
-                                             Constraints.end());
-  return WatchedLiteralsSolver().solve(std::move(ConstraintsSet));
+  return WatchedLiteralsSolver().solve(std::move(Constraints));
 }
 
 TEST(SATCheckDebugStringTest, AtomicBoolean) {
   // B0
   ConstraintContext Ctx;
   std::vector<BoolValue *> Constraints({Ctx.atom()});
   auto Result = CheckSAT(Constraints);
 

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

 using testing::AnyOf;
 using testing::IsEmpty;
 using testing::Optional;
 using testing::Pair;
 using testing::UnorderedElementsAre;
 
 // Checks if the conjunction of `Vals` is satisfiable and returns the
 // corresponding result.
-Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
-  return WatchedLiteralsSolver().solve(std::move(Vals));
+Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
+  return WatchedLiteralsSolver().solve(Vals);
 }
 
 void expectUnsatisfiable(Solver::Result Result) {
   EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
   EXPECT_FALSE(Result.getSolution().has_value());
 }
 
 template <typename Matcher>