sammccall created this revision.
Herald added subscribers: martong, mgrang, xazax.hun.
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.
This is the first step in untangling the two current jobs of BoolValue:
- BoolValue will model C++ booleans e.g. held in StorageLocations. this
includes describing uncertainty (e.g. "top" is a Value concern)
- Formula describes analysis-level assertions in terms of SAT atoms.
These can still be linked together: a BoolValue may have a corresponding
SAT atom which is constrained by formulas.
For now, BoolValue is left intact, Formula is just the input type to the
SAT solver, and we build formulas as needed to invoke the solver.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D153366
Files:
clang/include/clang/Analysis/FlowSensitive/Arena.h
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
clang/include/clang/Analysis/FlowSensitive/Formula.h
clang/include/clang/Analysis/FlowSensitive/Solver.h
clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
clang/lib/Analysis/FlowSensitive/Arena.cpp
clang/lib/Analysis/FlowSensitive/CMakeLists.txt
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Formula.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
Index: clang/unittests/Analysis/FlowSensitive/TestingSupport.h
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -42,6 +42,7 @@
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringMap.h"
#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
#include "llvm/Support/Errc.h"
#include "llvm/Support/Error.h"
#include "llvm/Testing/Annotations/Annotations.h"
@@ -404,55 +405,51 @@
/// Creates and owns constraints which are boolean values.
class ConstraintContext {
-public:
- // Creates an atomic boolean value.
- BoolValue *atom() {
- Vals.push_back(std::make_unique<AtomicBoolValue>());
- return Vals.back().get();
+ unsigned NextAtom;
+ llvm::BumpPtrAllocator A;
+
+ const Formula *make(Formula::Kind K, llvm::ArrayRef<const Formula *> Operands) {
+ return &Formula::create(A, K, Operands);
}
+public:
+#if 0 // XXX
// Creates an instance of the Top boolean value.
BoolValue *top() {
Vals.push_back(std::make_unique<TopBoolValue>());
return Vals.back().get();
}
+#endif
+
+ // Creates a reference to a fresh atomic variable.
+ const Formula *atom() {
+ return &Formula::create(A, Formula::AtomRef, {}, ++NextAtom);
+ }
// Creates a boolean conjunction value.
- BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ const Formula *conj(const Formula *LeftSubVal, const Formula *RightSubVal) {
+ return make(Formula::And, {LeftSubVal, RightSubVal});
}
// Creates a boolean disjunction value.
- BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ const Formula*disj(const Formula*LeftSubVal, const Formula*RightSubVal) {
+ return make(Formula::Or, {LeftSubVal, RightSubVal});
}
// Creates a boolean negation value.
- BoolValue *neg(BoolValue *SubVal) {
- Vals.push_back(std::make_unique<NegationValue>(*SubVal));
- return Vals.back().get();
+ const Formula *neg(const Formula *SubVal) {
+ return make(Formula::Not, {SubVal});
}
// Creates a boolean implication value.
- BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ const Formula *impl(const Formula *LeftSubVal, const Formula *RightSubVal) {
+ return make(Formula::Implies, {LeftSubVal, RightSubVal});
}
// Creates a boolean biconditional value.
- BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ const Formula *iff(const Formula *LeftSubVal, const Formula *RightSubVal) {
+ return make(Formula::Equal, {LeftSubVal, RightSubVal});
}
-
-private:
- std::vector<std::unique_ptr<BoolValue>> Vals;
};
} // namespace test
Index: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -30,19 +30,23 @@
// Checks if the conjunction of `Vals` is satisfiable and returns the
// corresponding result.
-Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
+Solver::Result solve(llvm::DenseSet<const Formula *> Vals) {
return WatchedLiteralsSolver().solve(std::move(Vals));
}
-void expectUnsatisfiable(Solver::Result Result) {
- EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
- EXPECT_FALSE(Result.getSolution().has_value());
+MATCHER(unsat, "") {
+ return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
}
-
-template <typename Matcher>
-void expectSatisfiable(Solver::Result Result, Matcher Solution) {
- EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
- EXPECT_THAT(Result.getSolution(), Optional(Solution));
+MATCHER_P(sat, SolutionMatcher,
+ "is satisfiable, where solution " +
+ (testing::DescribeMatcher<
+ llvm::DenseMap<Atom, Solver::Result::Assignment>>(
+ SolutionMatcher))) {
+ if (arg.getStatus() != Solver::Result::Status::Satisfiable)
+ return false;
+ auto Solution = *arg.getSolution();
+ return testing::ExplainMatchResult(SolutionMatcher, Solution,
+ result_listener);
}
TEST(SolverTest, Var) {
@@ -50,9 +54,9 @@
auto X = Ctx.atom();
// X
- expectSatisfiable(
- solve({X}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({X}),
+ sat(UnorderedElementsAre(
+ Pair(X->atom(), Solver::Result::Assignment::AssignedTrue))));
}
TEST(SolverTest, NegatedVar) {
@@ -61,9 +65,9 @@
auto NotX = Ctx.neg(X);
// !X
- expectSatisfiable(
- solve({NotX}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
+ EXPECT_THAT(solve({NotX}),
+ sat(UnorderedElementsAre(
+ Pair(X->atom(), Solver::Result::Assignment::AssignedFalse))));
}
TEST(SolverTest, UnitConflict) {
@@ -72,7 +76,7 @@
auto NotX = Ctx.neg(X);
// X ^ !X
- expectUnsatisfiable(solve({X, NotX}));
+ EXPECT_THAT(solve({X, NotX}), unsat());
}
TEST(SolverTest, DistinctVars) {
@@ -82,36 +86,10 @@
auto NotY = Ctx.neg(Y);
// X ^ !Y
- expectSatisfiable(
- solve({X, NotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedFalse)));
-}
-
-TEST(SolverTest, Top) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
-
- // X. Since Top is anonymous, we do not get any results in the solution.
- expectSatisfiable(solve({X}), IsEmpty());
-}
-
-TEST(SolverTest, NegatedTop) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
-
- // !X
- expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
-}
-
-TEST(SolverTest, DistinctTops) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
- auto Y = Ctx.top();
- auto NotY = Ctx.neg(Y);
-
- // X ^ !Y
- expectSatisfiable(solve({X, NotY}), IsEmpty());
+ EXPECT_THAT(solve({X, NotY}),
+ sat(UnorderedElementsAre(
+ Pair(X->atom(), Solver::Result::Assignment::AssignedTrue),
+ Pair(Y->atom(), Solver::Result::Assignment::AssignedFalse))));
}
TEST(SolverTest, DoubleNegation) {
@@ -121,7 +99,7 @@
auto NotNotX = Ctx.neg(NotX);
// !!X ^ !X
- expectUnsatisfiable(solve({NotNotX, NotX}));
+ EXPECT_THAT(solve({NotNotX, NotX}), unsat());
}
TEST(SolverTest, NegatedDisjunction) {
@@ -132,7 +110,7 @@
auto NotXOrY = Ctx.neg(XOrY);
// !(X v Y) ^ (X v Y)
- expectUnsatisfiable(solve({NotXOrY, XOrY}));
+ EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
}
TEST(SolverTest, NegatedConjunction) {
@@ -143,7 +121,7 @@
auto NotXAndY = Ctx.neg(XAndY);
// !(X ^ Y) ^ (X ^ Y)
- expectUnsatisfiable(solve({NotXAndY, XAndY}));
+ EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
}
TEST(SolverTest, DisjunctionSameVarWithNegation) {
@@ -153,7 +131,7 @@
auto XOrNotX = Ctx.disj(X, NotX);
// X v !X
- expectSatisfiable(solve({XOrNotX}), _);
+ EXPECT_THAT(solve({XOrNotX}), sat(_));
}
TEST(SolverTest, DisjunctionSameVar) {
@@ -162,7 +140,7 @@
auto XOrX = Ctx.disj(X, X);
// X v X
- expectSatisfiable(solve({XOrX}), _);
+ EXPECT_THAT(solve({XOrX}), sat(_));
}
TEST(SolverTest, ConjunctionSameVarsConflict) {
@@ -172,7 +150,7 @@
auto XAndNotX = Ctx.conj(X, NotX);
// X ^ !X
- expectUnsatisfiable(solve({XAndNotX}));
+ EXPECT_THAT(solve({XAndNotX}), unsat());
}
TEST(SolverTest, ConjunctionSameVar) {
@@ -181,7 +159,7 @@
auto XAndX = Ctx.conj(X, X);
// X ^ X
- expectSatisfiable(solve({XAndX}), _);
+ EXPECT_THAT(solve({XAndX}), sat(_));
}
TEST(SolverTest, PureVar) {
@@ -194,10 +172,10 @@
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
- expectSatisfiable(
- solve({NotXOrY, NotXOrNotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, _)));
+ EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
+ sat(UnorderedElementsAre(
+ Pair(X->atom(), Solver::Result::Assignment::AssignedFalse),
+ Pair(Y->atom(), _))));
}
TEST(SolverTest, MustAssumeVarIsFalse) {
@@ -211,10 +189,10 @@
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
- expectSatisfiable(
- solve({XOrY, NotXOrY, NotXOrNotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
+ sat(UnorderedElementsAre(
+ Pair(X->atom(), Solver::Result::Assignment::AssignedFalse),
+ Pair(Y->atom(), Solver::Result::Assignment::AssignedTrue))));
}
TEST(SolverTest, DeepConflict) {
@@ -229,7 +207,7 @@
auto XOrNotY = Ctx.disj(X, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
- expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
+ EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
}
TEST(SolverTest, IffIsEquivalentToDNF) {
@@ -243,7 +221,7 @@
auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
// !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
- expectUnsatisfiable(solve({NotEquivalent}));
+ EXPECT_THAT(solve({NotEquivalent}), unsat());
}
TEST(SolverTest, IffSameVars) {
@@ -252,7 +230,7 @@
auto XEqX = Ctx.iff(X, X);
// X <=> X
- expectSatisfiable(solve({XEqX}), _);
+ EXPECT_THAT(solve({XEqX}), sat(_));
}
TEST(SolverTest, IffDistinctVars) {
@@ -262,14 +240,15 @@
auto XEqY = Ctx.iff(X, Y);
// X <=> Y
- expectSatisfiable(
+ EXPECT_THAT(
solve({XEqY}),
- AnyOf(UnorderedElementsAre(
- Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)),
- UnorderedElementsAre(
- Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, Solver::Result::Assignment::AssignedFalse))));
+ sat(AnyOf(
+ UnorderedElementsAre(
+ Pair(X->atom(), Solver::Result::Assignment::AssignedTrue),
+ Pair(Y->atom(), Solver::Result::Assignment::AssignedTrue)),
+ UnorderedElementsAre(
+ Pair(X->atom(), Solver::Result::Assignment::AssignedFalse),
+ Pair(Y->atom(), Solver::Result::Assignment::AssignedFalse)))));
}
TEST(SolverTest, IffWithUnits) {
@@ -279,10 +258,10 @@
auto XEqY = Ctx.iff(X, Y);
// (X <=> Y) ^ X ^ Y
- expectSatisfiable(
- solve({XEqY, X, Y}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({XEqY, X, Y}),
+ sat(UnorderedElementsAre(
+ Pair(X->atom(), Solver::Result::Assignment::AssignedTrue),
+ Pair(Y->atom(), Solver::Result::Assignment::AssignedTrue))));
}
TEST(SolverTest, IffWithUnitsConflict) {
@@ -293,7 +272,7 @@
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X !Y
- expectUnsatisfiable(solve({XEqY, X, NotY}));
+ EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
}
TEST(SolverTest, IffTransitiveConflict) {
@@ -306,7 +285,7 @@
auto NotX = Ctx.neg(X);
// (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
- expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
+ EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat());
}
TEST(SolverTest, DeMorgan) {
@@ -323,7 +302,7 @@
auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
// A ^ B
- expectSatisfiable(solve({A, B}), _);
+ EXPECT_THAT(solve({A, B}), sat(_));
}
TEST(SolverTest, RespectsAdditionalConstraints) {
@@ -334,7 +313,7 @@
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X ^ !Y
- expectUnsatisfiable(solve({XEqY, X, NotY}));
+ EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
}
TEST(SolverTest, ImplicationIsEquivalentToDNF) {
@@ -346,7 +325,7 @@
auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
// !((X => Y) <=> (!X v Y))
- expectUnsatisfiable(solve({NotEquivalent}));
+ EXPECT_THAT(solve({NotEquivalent}), unsat());
}
TEST(SolverTest, ImplicationConflict) {
@@ -357,7 +336,7 @@
auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
// X => Y ^ X ^ !Y
- expectUnsatisfiable(solve({XImplY, XAndNotY}));
+ EXPECT_THAT(solve({XImplY, XAndNotY}), unsat());
}
TEST(SolverTest, LowTimeoutResultsInTimedOut) {
Index: clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -20,6 +20,7 @@
using test::ConstraintContext;
using testing::StrEq;
+ #if 0
TEST(BoolValueDebugStringTest, AtomicBoolean) {
// B0
@@ -449,4 +450,5 @@
{OtherIntEqZero, "OtherIntEqZero"}}),
StrEq(Expected));
}
+ #endif
} // namespace
Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -17,8 +17,8 @@
#include <queue>
#include <vector>
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/DenseSet.h"
@@ -122,10 +122,10 @@
/// Stores the variable identifier and value location for atomic booleans in
/// the formula.
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+ llvm::DenseMap<Variable, Atom> Atomics;
explicit BooleanFormula(Variable LargestVar,
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
+ llvm::DenseMap<Variable, Atom> Atomics)
: LargestVar(LargestVar), Atomics(std::move(Atomics)) {
Clauses.push_back(0);
ClauseStarts.push_back(0);
@@ -177,7 +177,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<BoolValue *> &Vals) {
+BooleanFormula buildBooleanFormula(const llvm::DenseSet<const Formula *> &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
@@ -185,90 +185,58 @@
// of sub-values in `Vals`.
// Map each sub-value in `Vals` to a unique variable.
- llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
+ llvm::DenseMap<const Formula *, Variable> SubValsToVar;
// Store variable identifiers and value location of atomic booleans.
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+ llvm::DenseMap<Variable, Atom> Atomics;
Variable NextVar = 1;
{
- std::queue<BoolValue *> UnprocessedSubVals;
- for (BoolValue *Val : Vals)
+ std::queue<const Formula *> UnprocessedSubVals;
+ for (const Formula *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
Variable Var = NextVar;
- BoolValue *Val = UnprocessedSubVals.front();
+ const Formula *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
if (!SubValsToVar.try_emplace(Val, Var).second)
continue;
++NextVar;
- // Visit the sub-values of `Val`.
- switch (Val->getKind()) {
- case Value::Kind::Conjunction: {
- auto *C = cast<ConjunctionValue>(Val);
- UnprocessedSubVals.push(&C->getLeftSubValue());
- UnprocessedSubVals.push(&C->getRightSubValue());
- break;
- }
- case Value::Kind::Disjunction: {
- auto *D = cast<DisjunctionValue>(Val);
- UnprocessedSubVals.push(&D->getLeftSubValue());
- UnprocessedSubVals.push(&D->getRightSubValue());
- break;
- }
- case Value::Kind::Negation: {
- auto *N = cast<NegationValue>(Val);
- UnprocessedSubVals.push(&N->getSubVal());
- break;
- }
- case Value::Kind::Implication: {
- auto *I = cast<ImplicationValue>(Val);
- UnprocessedSubVals.push(&I->getLeftSubValue());
- UnprocessedSubVals.push(&I->getRightSubValue());
- break;
- }
- case Value::Kind::Biconditional: {
- auto *B = cast<BiconditionalValue>(Val);
- UnprocessedSubVals.push(&B->getLeftSubValue());
- UnprocessedSubVals.push(&B->getRightSubValue());
- break;
- }
+ for (const Formula *F : Val->operands())
+ UnprocessedSubVals.push(F);
+ if (Val->kind() == Formula::AtomRef)
+ Atomics[Var] = Val->atom();
+#if 0 // XXX
case Value::Kind::TopBool:
// Nothing more to do. This `TopBool` instance has already been mapped
// to a fresh solver variable (`NextVar`, above) and is thereafter
// anonymous. The solver never sees `Top`.
break;
- case Value::Kind::AtomicBool: {
- Atomics[Var] = cast<AtomicBoolValue>(Val);
- break;
- }
- default:
- llvm_unreachable("buildBooleanFormula: unhandled value kind");
- }
+#endif
}
}
- auto GetVar = [&SubValsToVar](const BoolValue *Val) {
+ auto GetVar = [&SubValsToVar](const Formula *Val) {
auto ValIt = SubValsToVar.find(Val);
assert(ValIt != SubValsToVar.end());
return ValIt->second;
};
- BooleanFormula Formula(NextVar - 1, std::move(Atomics));
+ BooleanFormula Form(NextVar - 1, std::move(Atomics));
std::vector<bool> ProcessedSubVals(NextVar, false);
// Add a conjunct for each variable that represents a top-level conjunction
// value in `Vals`.
- for (BoolValue *Val : Vals)
- Formula.addClause(posLit(GetVar(Val)));
+ for (const Formula *Val : Vals)
+ Form.addClause(posLit(GetVar(Val)));
// Add conjuncts that represent the mapping between newly-created variables
// and their corresponding sub-values.
- std::queue<BoolValue *> UnprocessedSubVals;
- for (BoolValue *Val : Vals)
+ std::queue<const Formula *> UnprocessedSubVals;
+ for (const Formula *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
- const BoolValue *Val = UnprocessedSubVals.front();
+ const Formula *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
const Variable Var = GetVar(Val);
@@ -276,117 +244,107 @@
continue;
ProcessedSubVals[Var] = true;
- if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
- const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
- const Variable RightSubVar = GetVar(&C->getRightSubValue());
+ switch (Val->kind()) {
+ case Formula::AtomRef:
+ break;
+ case Formula::And: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
- if (LeftSubVar == RightSubVar) {
+ if (LHS == RHS) {
// `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
// already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
-
- // Visit a sub-value of `Val` (pick any, they are identical).
- UnprocessedSubVals.push(&C->getLeftSubValue());
+ Form.addClause(negLit(Var), posLit(LHS));
+ Form.addClause(posLit(Var), negLit(LHS));
} else {
// `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
// which is already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(negLit(Var), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&C->getLeftSubValue());
- UnprocessedSubVals.push(&C->getRightSubValue());
+ Form.addClause(negLit(Var), posLit(LHS));
+ Form.addClause(negLit(Var), posLit(RHS));
+ Form.addClause(posLit(Var), negLit(LHS), negLit(RHS));
}
- } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
- const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
- const Variable RightSubVar = GetVar(&D->getRightSubValue());
+ break;
+ }
+ case Formula::Or: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
- if (LeftSubVar == RightSubVar) {
+ if (LHS == RHS) {
// `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
// already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
-
- // Visit a sub-value of `Val` (pick any, they are identical).
- UnprocessedSubVals.push(&D->getLeftSubValue());
+ Form.addClause(negLit(Var), posLit(LHS));
+ Form.addClause(posLit(Var), negLit(LHS));
} else {
- // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
- // which is already in conjunctive normal form. Below we add each of the
- // conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&D->getLeftSubValue());
- UnprocessedSubVals.push(&D->getRightSubValue());
+ // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v
+ // !B)` which is already in conjunctive normal form. Below we add each
+ // of the conjuncts of the latter expression to the result.
+ Form.addClause(negLit(Var), posLit(LHS), posLit(RHS));
+ Form.addClause(posLit(Var), negLit(LHS));
+ Form.addClause(posLit(Var), negLit(RHS));
}
- } else if (auto *N = dyn_cast<NegationValue>(Val)) {
- const Variable SubVar = GetVar(&N->getSubVal());
-
- // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in
- // conjunctive normal form. Below we add each of the conjuncts of the
- // latter expression to the result.
- Formula.addClause(negLit(Var), negLit(SubVar));
- Formula.addClause(posLit(Var), posLit(SubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&N->getSubVal());
- } else if (auto *I = dyn_cast<ImplicationValue>(Val)) {
- const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
- const Variable RightSubVar = GetVar(&I->getRightSubValue());
+ break;
+ }
+ case Formula::Not: {
+ const Variable Operand = GetVar(Val->operands()[0]);
+
+ // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is
+ // already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ Form.addClause(negLit(Var), negLit(Operand));
+ Form.addClause(posLit(Var), posLit(Operand));
+ break;
+ }
+ case Formula::Implies: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
// `X <=> (A => B)` is equivalent to
// `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
- // conjunctive normal form. Below we add each of the conjuncts of the
- // latter expression to the result.
- Formula.addClause(posLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(RightSubVar));
- Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&I->getLeftSubValue());
- UnprocessedSubVals.push(&I->getRightSubValue());
- } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) {
- const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
- const Variable RightSubVar = GetVar(&B->getRightSubValue());
-
- if (LeftSubVar == RightSubVar) {
+ // conjunctive normal form. Below we add each of the conjuncts of
+ // the latter expression to the result.
+ Form.addClause(posLit(Var), posLit(LHS));
+ Form.addClause(posLit(Var), negLit(RHS));
+ Form.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+ break;
+ }
+ case Formula::Equal: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
+
+ if (LHS == RHS) {
// `X <=> (A <=> A)` is equvalent to `X` which is already in
// conjunctive normal form. Below we add each of the conjuncts of the
// latter expression to the result.
- Formula.addClause(posLit(Var));
+ Form.addClause(posLit(Var));
// No need to visit the sub-values of `Val`.
- } else {
- // `X <=> (A <=> B)` is equivalent to
- // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is
- // already in conjunctive normal form. Below we add each of the conjuncts
- // of the latter expression to the result.
- Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
- Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));
- Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&B->getLeftSubValue());
- UnprocessedSubVals.push(&B->getRightSubValue());
+ continue;
}
+ // `X <=> (A <=> B)` is equivalent to
+ // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which
+ // is already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ Form.addClause(posLit(Var), posLit(LHS), posLit(RHS));
+ Form.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+ Form.addClause(negLit(Var), posLit(LHS), negLit(RHS));
+ Form.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+ break;
+ }
}
+ for (const Formula *Child : Val->operands())
+ UnprocessedSubVals.push(Child);
}
- return Formula;
+ return Form;
}
class WatchedLiteralsSolverImpl {
/// A boolean formula in conjunctive normal form that the solver will attempt
/// to prove satisfiable. The formula will be modified in the process.
- BooleanFormula Formula;
+ BooleanFormula Form;
/// The search for a satisfying assignment of the variables in `Formula` will
/// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
@@ -438,9 +396,10 @@
std::vector<Variable> ActiveVars;
public:
- explicit WatchedLiteralsSolverImpl(const llvm::DenseSet<BoolValue *> &Vals)
- : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
- LevelStates(Formula.LargestVar + 1) {
+ explicit WatchedLiteralsSolverImpl(
+ const llvm::DenseSet<const Formula *> &Vals)
+ : Form(buildBooleanFormula(Vals)), LevelVars(Form.LargestVar + 1),
+ LevelStates(Form.LargestVar + 1) {
assert(!Vals.empty());
// Initialize the state at the root level to a decision so that in
@@ -449,10 +408,10 @@
LevelStates[0] = State::Decision;
// Initialize all variables as unassigned.
- VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
+ VarAssignments.resize(Form.LargestVar + 1, Assignment::Unassigned);
// Initialize the active variables.
- for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
+ for (Variable Var = Form.LargestVar; Var != NullVar; --Var) {
if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
ActiveVars.push_back(Var);
}
@@ -556,10 +515,9 @@
private:
/// Returns a satisfying truth assignment to the atomic values in the boolean
/// formula.
- llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
- buildSolution() {
- llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution;
- for (auto &Atomic : Formula.Atomics) {
+ llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
+ llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
+ for (auto &Atomic : Form.Atomics) {
// A variable may have a definite true/false assignment, or it may be
// unassigned indicating its truth value does not affect the result of
// the formula. Unassigned variables are assigned to true as a default.
@@ -595,24 +553,24 @@
const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
? negLit(Var)
: posLit(Var);
- ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
- Formula.WatchedHead[FalseLit] = NullClause;
+ ClauseID FalseLitWatcher = Form.WatchedHead[FalseLit];
+ Form.WatchedHead[FalseLit] = NullClause;
while (FalseLitWatcher != NullClause) {
- const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
+ const ClauseID NextFalseLitWatcher = Form.NextWatched[FalseLitWatcher];
// Pick the first non-false literal as the new watched literal.
- const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
+ const size_t FalseLitWatcherStart = Form.ClauseStarts[FalseLitWatcher];
size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
- while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
+ while (isCurrentlyFalse(Form.Clauses[NewWatchedLitIdx]))
++NewWatchedLitIdx;
- const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];
+ const Literal NewWatchedLit = Form.Clauses[NewWatchedLitIdx];
const Variable NewWatchedLitVar = var(NewWatchedLit);
// Swap the old watched literal for the new one in `FalseLitWatcher` to
// maintain the invariant that the watched literal is at the beginning of
// the clause.
- Formula.Clauses[NewWatchedLitIdx] = FalseLit;
- Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+ Form.Clauses[NewWatchedLitIdx] = FalseLit;
+ Form.Clauses[FalseLitWatcherStart] = NewWatchedLit;
// If the new watched literal isn't watched by any other clause and its
// variable isn't assigned we need to add it to the active variables.
@@ -620,8 +578,8 @@
VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
ActiveVars.push_back(NewWatchedLitVar);
- Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
- Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+ Form.NextWatched[FalseLitWatcher] = Form.WatchedHead[NewWatchedLit];
+ Form.WatchedHead[NewWatchedLit] = FalseLitWatcher;
// Go to the next clause that watches `FalseLit`.
FalseLitWatcher = NextFalseLitWatcher;
@@ -631,10 +589,10 @@
/// Returns true if and only if one of the clauses that watch `Lit` is a unit
/// clause.
bool watchedByUnitClause(Literal Lit) const {
- for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
+ for (ClauseID LitWatcher = Form.WatchedHead[Lit];
LitWatcher != NullClause;
- LitWatcher = Formula.NextWatched[LitWatcher]) {
- llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);
+ LitWatcher = Form.NextWatched[LitWatcher]) {
+ llvm::ArrayRef<Literal> Clause = Form.clauseLiterals(LitWatcher);
// Assert the invariant that the watched literal is always the first one
// in the clause.
@@ -664,7 +622,7 @@
/// Returns true if and only if `Lit` is watched by a clause in `Formula`.
bool isWatched(Literal Lit) const {
- return Formula.WatchedHead[Lit] != NullClause;
+ return Form.WatchedHead[Lit] != NullClause;
}
/// Returns an assignment for an unassigned variable.
@@ -677,8 +635,8 @@
/// Returns a set of all watched literals.
llvm::DenseSet<Literal> watchedLiterals() const {
llvm::DenseSet<Literal> WatchedLiterals;
- for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
- if (Formula.WatchedHead[Lit] == NullClause)
+ for (Literal Lit = 2; Lit < Form.WatchedHead.size(); Lit++) {
+ if (Form.WatchedHead[Lit] == NullClause)
continue;
WatchedLiterals.insert(Lit);
}
@@ -718,7 +676,8 @@
}
};
-Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) {
+Solver::Result
+WatchedLiteralsSolver::solve(const llvm::DenseSet<const Formula *> &Vals) {
if (Vals.empty())
return Solver::Result::Satisfiable({{}});
auto [Res, Iterations] =
Index: clang/lib/Analysis/FlowSensitive/Formula.cpp
===================================================================
--- /dev/null
+++ clang/lib/Analysis/FlowSensitive/Formula.cpp
@@ -0,0 +1,61 @@
+//===- Formula.cpp ----------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/ErrorHandling.h"
+#include <cassert>
+
+namespace clang::dataflow {
+
+Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
+ ArrayRef<const Formula *> Operands, unsigned Value) {
+ assert(Operands.size() == numOperands(K));
+ if (Value != 0)
+ assert(hasValue(K));
+ void *Mem = Alloc.Allocate(sizeof(Formula) +
+ Operands.size() * sizeof(Operands.front()),
+ alignof(Formula));
+ Formula *Result = new (Mem) Formula();
+ Result->FormulaKind = K;
+ Result->Value = Value;
+ llvm::copy(Operands, reinterpret_cast<const Formula **>(Result + 1));
+ return *Result;
+}
+
+void Formula::print(llvm::raw_ostream &OS,
+ llvm::function_ref<DelegatePrinter> Delegate) const {
+ if (Delegate && Delegate(OS, *this))
+ return;
+
+ switch (kind()) {
+ case Formula::AtomRef:
+ OS << atom();
+ return;
+ case Formula::Not:
+ OS << "!" << operands()[0];
+ return;
+ case Formula::And:
+ OS << "(" << operands()[0] << " & " << operands()[1] << ")";
+ return;
+ case Formula::Or:
+ OS << "(" << operands()[0] << " | " << operands()[1] << ")";
+ return;
+ case Formula::Implies:
+ OS << "(" << operands()[0] << " => " << operands()[1] << ")";
+ return;
+ case Formula::Equal:
+ OS << "(" << operands()[0] << " = " << operands()[1] << ")";
+ return;
+ }
+ llvm_unreachable("unhandled Formula kind");
+}
+
+} // namespace clang::dataflow
\ No newline at end of file
Index: clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -16,22 +16,12 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/STLExtras.h"
#include "llvm/ADT/StringRef.h"
-#include "llvm/ADT/StringSet.h"
#include "llvm/Support/ErrorHandling.h"
-#include "llvm/Support/FormatAdapters.h"
-#include "llvm/Support/FormatCommon.h"
-#include "llvm/Support/FormatVariadic.h"
namespace clang {
namespace dataflow {
-using llvm::AlignStyle;
-using llvm::fmt_pad;
-using llvm::formatv;
-
llvm::StringRef debugString(Value::Kind Kind) {
switch (Kind) {
case Value::Kind::Integer:
@@ -60,12 +50,13 @@
llvm_unreachable("Unhandled value kind");
}
-llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
+ Solver::Result::Assignment Assignment) {
switch (Assignment) {
case Solver::Result::Assignment::AssignedFalse:
- return "False";
+ return OS << "False";
case Solver::Result::Assignment::AssignedTrue:
- return "True";
+ return OS << "True";
}
llvm_unreachable("Booleans can only be assigned true/false");
}
@@ -82,181 +73,16 @@
llvm_unreachable("Unhandled SAT check result status");
}
-namespace {
-
-class DebugStringGenerator {
-public:
- explicit DebugStringGenerator(
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
- : Counter(0), AtomNames(std::move(AtomNamesArg)) {
-#ifndef NDEBUG
- llvm::StringSet<> Names;
- for (auto &N : AtomNames) {
- assert(Names.insert(N.second).second &&
- "The same name must not assigned to different atoms");
- }
-#endif
- }
-
- /// Returns a string representation of a boolean value `B`.
- std::string debugString(const BoolValue &B, size_t Depth = 0) {
- std::string S;
- switch (B.getKind()) {
- case Value::Kind::AtomicBool: {
- S = getAtomName(&cast<AtomicBoolValue>(B));
- break;
- }
- case Value::Kind::TopBool: {
- S = "top";
- break;
- }
- case Value::Kind::Conjunction: {
- auto &C = cast<ConjunctionValue>(B);
- auto L = debugString(C.getLeftSubValue(), Depth + 1);
- auto R = debugString(C.getRightSubValue(), Depth + 1);
- S = formatv("(and\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Disjunction: {
- auto &D = cast<DisjunctionValue>(B);
- auto L = debugString(D.getLeftSubValue(), Depth + 1);
- auto R = debugString(D.getRightSubValue(), Depth + 1);
- S = formatv("(or\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Negation: {
- auto &N = cast<NegationValue>(B);
- S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
- break;
- }
- case Value::Kind::Implication: {
- auto &IV = cast<ImplicationValue>(B);
- auto L = debugString(IV.getLeftSubValue(), Depth + 1);
- auto R = debugString(IV.getRightSubValue(), Depth + 1);
- S = formatv("(=>\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Biconditional: {
- auto &BV = cast<BiconditionalValue>(B);
- auto L = debugString(BV.getLeftSubValue(), Depth + 1);
- auto R = debugString(BV.getRightSubValue(), Depth + 1);
- S = formatv("(=\n{0}\n{1})", L, R);
- break;
- }
- 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 Result;
- for (const std::string &S : ConstraintsStrings) {
- Result += S;
- Result += '\n';
- }
- return Result;
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
+ OS << debugString(R.getStatus()) << "\n";
+ if (auto Solution = R.getSolution()) {
+ std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
+ Solution->begin(), Solution->end()};
+ llvm::sort(Sorted);
+ for (const auto &Entry : Sorted)
+ OS << Entry.first << " = " << Entry.second << "\n";
}
-
- /// 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,
- const Solver::Result &Result) {
- auto Template = R"(
-Constraints
-------------
-{0:$[
-
-]}
-------------
-{1}.
-{2}
-)";
-
- std::vector<std::string> ConstraintsStrings;
- ConstraintsStrings.reserve(Constraints.size());
- for (auto &Constraint : Constraints) {
- ConstraintsStrings.push_back(debugString(*Constraint));
- }
-
- auto StatusString = clang::dataflow::debugString(Result.getStatus());
- auto Solution = Result.getSolution();
- auto SolutionString = Solution ? "\n" + debugString(*Solution) : "";
-
- return formatv(
- Template,
- llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
- StatusString, SolutionString);
- }
-
-private:
- /// Returns a string representation of a truth assignment to atom booleans.
- std::string debugString(
- const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
- &AtomAssignments) {
- size_t MaxNameLength = 0;
- for (auto &AtomName : AtomNames) {
- MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
- }
-
- std::vector<std::string> Lines;
- for (auto &AtomAssignment : AtomAssignments) {
- auto Line = formatv("{0} = {1}",
- fmt_align(getAtomName(AtomAssignment.first),
- AlignStyle::Left, MaxNameLength),
- clang::dataflow::debugString(AtomAssignment.second));
- Lines.push_back(Line);
- }
- llvm::sort(Lines);
-
- return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
- }
-
- /// Returns the name assigned to `Atom`, either user-specified or created by
- /// default rules (B0, B1, ...).
- std::string getAtomName(const AtomicBoolValue *Atom) {
- auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
- if (Entry.second) {
- Counter++;
- }
- return Entry.first->second;
- }
-
- // Keep track of number of atoms without a user-specified name, used to assign
- // non-repeating default names to such atoms.
- size_t Counter;
-
- // Keep track of names assigned to atoms.
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
-};
-
-} // namespace
-
-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,
- 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);
+ return OS;
}
} // namespace dataflow
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -22,6 +22,7 @@
#include "llvm/Support/Debug.h"
#include "llvm/Support/FileSystem.h"
#include "llvm/Support/Path.h"
+#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <memory>
#include <utility>
@@ -129,7 +130,10 @@
Constraints.insert(&arena().makeLiteral(true));
Constraints.insert(
&arena().makeNot(arena().makeLiteral(false)));
- return S->solve(std::move(Constraints));
+ llvm::DenseSet<const Formula *> Formulas;
+ for (const BoolValue * Constraint : Constraints)
+ Formulas.insert(&arena().getFormula(*Constraint));
+ return S->solve(Formulas);
}
bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
@@ -190,14 +194,35 @@
void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
llvm::raw_ostream &OS) {
+ // TODO: accumulate formulas directly instead
llvm::DenseSet<BoolValue *> Constraints = {&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);
+ // TODO: have formulas know about true/false directly instead
+ auto &True = arena().getFormula(arena().makeLiteral(true));
+ auto &False = arena().getFormula(arena().makeLiteral(false));
+ auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) {
+ if (&F == &True) {
+ OS << "True";
+ return true;
+ }
+ if (&F == &False) {
+ OS << "False";
+ return true;
+ }
+ return false;
+ };
+
+ std::vector<std::string> Lines;
+ for (const auto *Constraint : Constraints) {
+ Lines.emplace_back();
+ llvm::raw_string_ostream LineOS(Lines.back());
+ arena().getFormula(*Constraint).print(LineOS, Delegate);
+ }
+ llvm::sort(Lines);
+ for (const auto &Line : Lines)
+ OS << Line << "\n";
}
const ControlFlowContext *
Index: clang/lib/Analysis/FlowSensitive/CMakeLists.txt
===================================================================
--- clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,6 +3,7 @@
ControlFlowContext.cpp
DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
+ Formula.cpp
HTMLLogger.cpp
Logger.cpp
Transfer.cpp
Index: clang/lib/Analysis/FlowSensitive/Arena.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -76,4 +76,50 @@
return *It->second;
}
+const Formula &Arena::getFormula(const BoolValue &B) {
+ auto It = ValToFormula.find(&B);
+ if (It != ValToFormula.end())
+ return *It->second;
+ Formula &F = [&]() -> Formula & {
+ switch (B.getKind()) {
+ case Value::Kind::Integer:
+ case Value::Kind::Reference:
+ case Value::Kind::Pointer:
+ case Value::Kind::Struct:
+ llvm_unreachable("not a boolean");
+ case Value::Kind::TopBool:
+ case Value::Kind::AtomicBool:
+ // TODO: assign atom numbers on creation rather than in getFormula(), so
+ // they will be deterministic and maybe even meaningful.
+ return Formula::create(Alloc, Formula::AtomRef, {},
+ static_cast<unsigned>(makeAtom()));
+ case Value::Kind::Conjunction:
+ return Formula::create(
+ Alloc, Formula::And,
+ {&getFormula(cast<ConjunctionValue>(B).getLeftSubValue()),
+ &getFormula(cast<ConjunctionValue>(B).getRightSubValue())});
+ case Value::Kind::Disjunction:
+ return Formula::create(
+ Alloc, Formula::Or,
+ {&getFormula(cast<DisjunctionValue>(B).getLeftSubValue()),
+ &getFormula(cast<DisjunctionValue>(B).getRightSubValue())});
+ case Value::Kind::Negation:
+ return Formula::create(Alloc, Formula::Not,
+ {&getFormula(cast<NegationValue>(B).getSubVal())});
+ case Value::Kind::Implication:
+ return Formula::create(
+ Alloc, Formula::Implies,
+ {&getFormula(cast<ImplicationValue>(B).getLeftSubValue()),
+ &getFormula(cast<ImplicationValue>(B).getRightSubValue())});
+ case Value::Kind::Biconditional:
+ return Formula::create(
+ Alloc, Formula::Equal,
+ {&getFormula(cast<BiconditionalValue>(B).getLeftSubValue()),
+ &getFormula(cast<BiconditionalValue>(B).getRightSubValue())});
+ }
+ }();
+ ValToFormula.try_emplace(&B, &F);
+ return F;
+}
+
} // namespace clang::dataflow
Index: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -14,8 +14,8 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseSet.h"
#include <limits>
@@ -46,7 +46,7 @@
explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
: MaxIterations(WorkLimit) {}
- Result solve(llvm::DenseSet<BoolValue *> Vals) override;
+ Result solve(const llvm::DenseSet<const Formula *> &Vals) override;
};
} // namespace dataflow
Index: clang/include/clang/Analysis/FlowSensitive/Solver.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/Solver.h
+++ clang/include/clang/Analysis/FlowSensitive/Solver.h
@@ -14,7 +14,7 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
-#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/DenseSet.h"
#include <optional>
@@ -45,8 +45,7 @@
/// Constructs a result indicating that the queried boolean formula is
/// satisfiable. The result will hold a solution found by the solver.
- static Result
- Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
+ static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) {
return Result(Status::Satisfiable, std::move(Solution));
}
@@ -64,19 +63,17 @@
/// Returns a truth assignment to boolean values that satisfies the queried
/// boolean formula if available. Otherwise, an empty optional is returned.
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
- getSolution() const {
+ std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const {
return Solution;
}
private:
- Result(
- enum Status SATCheckStatus,
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
+ Result(enum Status SATCheckStatus,
+ std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
: SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
Status SATCheckStatus;
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
+ std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
};
virtual ~Solver() = default;
@@ -87,9 +84,12 @@
/// Requirements:
///
/// All elements in `Vals` must not be null.
- virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0;
+ virtual Result solve(const llvm::DenseSet<const Formula *> &Vals) = 0;
};
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
+
} // namespace dataflow
} // namespace clang
Index: clang/include/clang/Analysis/FlowSensitive/Formula.h
===================================================================
--- /dev/null
+++ clang/include/clang/Analysis/FlowSensitive/Formula.h
@@ -0,0 +1,129 @@
+//===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
+
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/DenseMapInfo.h"
+#include "llvm/ADT/STLFunctionalExtras.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/raw_ostream.h"
+#include <cassert>
+#include <type_traits>
+
+namespace clang::dataflow {
+class Formula;
+
+/// Identifies an atomic boolean variable such as "V1".
+///
+/// This often represents an assertion that is interesting to the analysis but
+/// cannot immediately be proven true or false. For example:
+/// - V1 may mean "the program reaches this point",
+/// - V2 may mean "the parameter was null"
+///
+/// We can use these variables in formulas to describe relationships we know
+/// to be true: "if the parameter was null, the program reaches this point".
+/// We also express hypotheses as formulas, and use a SAT solver to check
+/// whether they are consistent with the known facts.
+enum class Atom : unsigned {};
+
+/// A boolean expression such as "true" or "V1 & !V2".
+/// Expressions may refer to boolean atomic variables, identified by number.
+///
+/// (Formulas are always expressions in terms of boolean variables rather than
+/// e.g. integers because our underlying model is SAT rather than e.g. SMT).
+///
+/// Simple formulas such as "true" and "V1" are self-contained.
+/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
+/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
+/// trailing objects.
+class alignas(Formula *) Formula {
+public:
+ enum Kind : unsigned {
+ /// A reference to an atomic boolean variable.
+ /// We name these e.g. "V3", where 3 == atom identity == value().
+ AtomRef,
+ // FIXME: add const true/false rather than modeling them as variables
+
+ Not, /// True if its only operand is false
+
+ // These kinds connect two operands LHS and RHS
+ And, /// True if LHS and RHS are both true
+ Or, /// True if either LHS or RHS is true
+ Implies, /// True if LHS is false or RHS is true
+ Equal, /// True if LHS and RHS have the same truth value
+ };
+ Kind kind() const { return FormulaKind; }
+
+ Atom atom() const {
+ assert(kind() == AtomRef);
+ return static_cast<Atom>(Value);
+ }
+
+ ArrayRef<const Formula *> operands() const {
+ return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
+ numOperands(kind()));
+ }
+
+ // A function that can optionally override the printing of formulas.
+ using DelegatePrinter = bool(llvm::raw_ostream &OS, const Formula &);
+ void print(llvm::raw_ostream &OS,
+ llvm::function_ref<DelegatePrinter> = nullptr) const;
+
+ static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
+ ArrayRef<const Formula *> Operands,
+ unsigned Value = 0);
+
+private:
+ Formula() = default;
+ Formula(const Formula &) = delete;
+ Formula &operator=(const Formula &) = delete;
+
+ static unsigned numOperands(Kind K) {
+ switch (K) {
+ case AtomRef:
+ return 0;
+ case Not:
+ return 1;
+ case And:
+ case Or:
+ case Implies:
+ case Equal:
+ return 2;
+ }
+ }
+
+ Kind FormulaKind;
+ unsigned Value;
+};
+
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
+ return OS << 'V' << static_cast<unsigned>(A);
+}
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
+ F.print(OS);
+ return OS;
+}
+
+} // namespace clang::dataflow
+namespace llvm {
+template <> struct DenseMapInfo<clang::dataflow::Atom> {
+ using Atom = clang::dataflow::Atom;
+ using Underlying = std::underlying_type_t<Atom>;
+
+ static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
+ static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
+ static unsigned getHashValue(const Atom &Val) {
+ return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
+ }
+ static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
+};
+} // namespace llvm
+#endif
Index: clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
@@ -19,7 +19,6 @@
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringRef.h"
namespace clang {
@@ -28,60 +27,9 @@
/// Returns a string representation of a value kind.
llvm::StringRef debugString(Value::Kind Kind);
-/// Returns a string representation of a boolean assignment to true or false.
-llvm::StringRef debugString(Solver::Result::Assignment Assignment);
-
/// Returns a string representation of the result status of a SAT check.
llvm::StringRef debugString(Solver::Result::Status Status);
-/// Returns a string representation for the boolean value `B`.
-///
-/// Atomic booleans appearing in the boolean value `B` 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 BoolValue &B,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas.
-///
-/// 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,
- 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
Index: clang/include/clang/Analysis/FlowSensitive/Arena.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -8,6 +8,7 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include <vector>
@@ -104,7 +105,17 @@
return create<AtomicBoolValue>();
}
+ /// Gets the boolean formula equivalent of a BoolValue.
+ /// Each unique Top values is translated to an Atom.
+ /// TODO: migrate to storing Formula directly in Values instead.
+ const Formula &getFormula(const BoolValue &);
+
+ /// Returns a new atomic boolean variable, distinct from any other.
+ Atom makeAtom() { return static_cast<Atom>(++NextAtom); };
+
private:
+ llvm::BumpPtrAllocator Alloc;
+
// Storage for the state of a program.
std::vector<std::unique_ptr<StorageLocation>> Locs;
std::vector<std::unique_ptr<Value>> Vals;
@@ -122,6 +133,9 @@
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
BiconditionalVals;
+ llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
+ unsigned NextAtom = 0;
+
AtomicBoolValue &TrueVal;
AtomicBoolValue &FalseVal;
};
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
