[PATCH] D153584: [dataflow] Make SAT solver deterministic

[Sam McCall via Phabricator via cfe-commits]

This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rGd85c233e4b05: [dataflow] Make SAT solver deterministic 
(authored by sammccall).

Changed prior to commit:
  https://reviews.llvm.org/D153584?vs=533740=534699#toc

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153584

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
  clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
  clang/include/clang/Analysis/FlowSensitive/Solver.h
  clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
  clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
  clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
  clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
  clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
  clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

Index: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -30,8 +30,8 @@
 
 // Checks if the conjunction of `Vals` is satisfiable and returns the
 // corresponding result.
-Solver::Result solve(llvm::DenseSet Vals) {
-  return WatchedLiteralsSolver().solve(std::move(Vals));
+Solver::Result solve(llvm::ArrayRef Vals) {
+  return WatchedLiteralsSolver().solve(Vals);
 }
 
 void expectUnsatisfiable(Solver::Result Result) {
Index: clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -187,34 +187,32 @@
 }
 
 TEST(ConstraintSetDebugStringTest, Empty) {
-  llvm::DenseSet Constraints;
+  llvm::ArrayRef Constraints;
   EXPECT_THAT(debugString(Constraints), StrEq(""));
 }
 
 TEST(ConstraintSetDebugStringTest, Simple) {
   ConstraintContext Ctx;
-  llvm::DenseSet Constraints;
+  std::vector Constraints;
   auto X = cast(Ctx.atom());
   auto Y = cast(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 Constraints) {
-  llvm::DenseSet ConstraintsSet(Constraints.begin(),
- Constraints.end());
-  return WatchedLiteralsSolver().solve(std::move(ConstraintsSet));
+  return WatchedLiteralsSolver().solve(std::move(Constraints));
 }
 
 TEST(SATCheckDebugStringTest, AtomicBoolean) {
Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
===
--- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -20,6 +20,7 @@
 #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"
@@ -177,7 +178,7 @@
 
 /// 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 ) {
+BooleanFormula buildBooleanFormula(const llvm::ArrayRef ) {
   // 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
@@ -438,7 +439,7 @@
   std::vector ActiveVars;
 
 public:
-  explicit WatchedLiteralsSolverImpl(const llvm::DenseSet )
+  explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef )
   : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
 LevelStates(Formula.LargestVar + 1) {
 assert(!Vals.empty());
@@ -718,7 +719,7 @@
   }
 };
 
-Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet Vals) {
+Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef Vals) {
   if (Vals.empty())
 return Solver::Result::Satisfiable({{}});
   auto [Res, Iterations] =
Index: clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
===
--- clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -150,17 +150,10 @@
 return 

[PATCH] D153584: [dataflow] Make SAT solver deterministic

[Sam McCall via Phabricator via cfe-commits]

sammccall added a comment.

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.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153584

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153584: [dataflow] Make SAT solver deterministic

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

xazax.hun added a comment.

Is there a measurable perf cost for this determinism?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D153584

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D153584: [dataflow] Make SAT solver deterministic

[Sam McCall via Phabricator via cfe-commits]

sammccall created this revision.
sammccall added reviewers: ymandel, xazax.hun.
Herald added subscribers: martong, mgrang.
Herald added a reviewer: NoQ.
Herald added a project: All.
sammccall requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

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.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D153584

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
  clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
  clang/include/clang/Analysis/FlowSensitive/Solver.h
  clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
  clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
  clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
  clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
  clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
  clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

Index: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -30,8 +30,8 @@
 
 // Checks if the conjunction of `Vals` is satisfiable and returns the
 // corresponding result.
-Solver::Result solve(llvm::DenseSet Vals) {
-  return WatchedLiteralsSolver().solve(std::move(Vals));
+Solver::Result solve(llvm::ArrayRef Vals) {
+  return WatchedLiteralsSolver().solve(Vals);
 }
 
 void expectUnsatisfiable(Solver::Result Result) {
Index: clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
===
--- clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -187,34 +187,32 @@
 }
 
 TEST(ConstraintSetDebugStringTest, Empty) {
-  llvm::DenseSet Constraints;
+  llvm::ArrayRef Constraints;
   EXPECT_THAT(debugString(Constraints), StrEq(""));
 }
 
 TEST(ConstraintSetDebugStringTest, Simple) {
   ConstraintContext Ctx;
-  llvm::DenseSet Constraints;
+  std::vector Constraints;
   auto X = cast(Ctx.atom());
   auto Y = cast(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 Constraints) {
-  llvm::DenseSet ConstraintsSet(Constraints.begin(),
- Constraints.end());
-  return WatchedLiteralsSolver().solve(std::move(ConstraintsSet));
+  return WatchedLiteralsSolver().solve(std::move(Constraints));
 }
 
 TEST(SATCheckDebugStringTest, AtomicBoolean) {
Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
===
--- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -20,6 +20,7 @@
 #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"
@@ -177,7 +178,7 @@
 
 /// 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 ) {
+BooleanFormula buildBooleanFormula(const llvm::ArrayRef ) {
   // 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
@@ -438,7 +439,7 @@
   std::vector ActiveVars;
 
 public:
-  explicit WatchedLiteralsSolverImpl(const llvm::DenseSet )
+  explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef )
   : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
 LevelStates(Formula.LargestVar + 1) {