sammccall updated this revision to Diff 533022.
sammccall added a comment.
update tests
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D153366/new/
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,43 @@
/// 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 = 0;
+ llvm::BumpPtrAllocator A;
+
+ const Formula *make(Formula::Kind K, llvm::ArrayRef<const Formula *> Operands) {
+ return &Formula::create(A, K, Operands);
}
- // Creates an instance of the Top boolean value.
- BoolValue *top() {
- Vals.push_back(std::make_unique<TopBoolValue>());
- return Vals.back().get();
+public:
+ // 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
@@ -8,8 +8,11 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "TestingSupport.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/Support/ScopedPrinter.h"
+#include "llvm/Support/raw_ostream.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -22,431 +25,96 @@
using testing::StrEq;
TEST(BoolValueDebugStringTest, AtomicBoolean) {
- // B0
ConstraintContext Ctx;
auto B = Ctx.atom();
- auto Expected = R"(B0)";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, Top) {
- ConstraintContext Ctx;
- auto B = Ctx.top();
-
- auto Expected = R"(top)";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "V0";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Negation) {
- // !B0
ConstraintContext Ctx;
auto B = Ctx.neg(Ctx.atom());
- auto Expected = R"((not
- B0))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "!V0";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Conjunction) {
- // B0 ^ B1
ConstraintContext Ctx;
auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
- auto Expected = R"((and
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "(V0 & V1)";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Disjunction) {
- // B0 v B1
ConstraintContext Ctx;
auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
- auto Expected = R"((or
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "(V0 | V1)";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Implication) {
- // B0 => B1
ConstraintContext Ctx;
auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
- auto Expected = R"((=>
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "(V0 => V1)";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Iff) {
- // B0 <=> B1
ConstraintContext Ctx;
auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
- auto Expected = R"((=
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "(V0 = V1)";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Xor) {
- // (B0 ^ !B1) V (!B0 ^ B1)
ConstraintContext Ctx;
auto B0 = Ctx.atom();
auto B1 = Ctx.atom();
auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
- auto Expected = R"((or
- (and
- B0
- (not
- B1))
- (and
- (not
- B0)
- B1)))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "((V0 & !V1) | (!V0 & V1))";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, NestedBoolean) {
- // B0 ^ (B1 v (B2 ^ (B3 v B4)))
ConstraintContext Ctx;
auto B = Ctx.conj(
Ctx.atom(),
Ctx.disj(Ctx.atom(),
Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
- auto Expected = R"((and
- B0
- (or
- B1
- (and
- B2
- (or
- B3
- B4)))))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
- // True
- ConstraintContext Ctx;
- auto True = cast<AtomicBoolValue>(Ctx.atom());
- auto B = True;
-
- auto Expected = R"(True)";
- EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
- // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
- ConstraintContext Ctx;
- auto Cond = cast<AtomicBoolValue>(Ctx.atom());
- auto Then = cast<AtomicBoolValue>(Ctx.atom());
- auto Else = cast<AtomicBoolValue>(Ctx.atom());
- auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
- Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
-
- auto Expected = R"((or
- (and
- Cond
- (and
- Then
- (not
- Else)))
- (and
- (not
- Cond)
- (and
- (not
- Then)
- Else))))";
- EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
- StrEq(Expected));
+ auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
- // (False && B0) v (True v B1)
ConstraintContext Ctx;
- auto True = cast<AtomicBoolValue>(Ctx.atom());
- auto False = cast<AtomicBoolValue>(Ctx.atom());
+ auto True = Ctx.atom();
+ auto False = Ctx.atom();
+ 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;
+ };
auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
- auto Expected = R"((or
- (and
- False
- B0)
- (or
- True
- B1)))";
- EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
- StrEq(Expected));
-}
-
-TEST(ConstraintSetDebugStringTest, Empty) {
- llvm::DenseSet<BoolValue *> Constraints;
- EXPECT_THAT(debugString(Constraints), StrEq(""));
-}
-
-TEST(ConstraintSetDebugStringTest, Simple) {
- ConstraintContext Ctx;
- llvm::DenseSet<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)));
-
- auto Expected = R"((or
- X
- (not
- Y))
-(or
- X
- 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));
-}
-
-TEST(SATCheckDebugStringTest, AtomicBoolean) {
- // B0
- ConstraintContext Ctx;
- std::vector<BoolValue *> Constraints({Ctx.atom()});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-------------
-Satisfiable.
-
-B0 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
- // B0, !B0
- ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(not
- B0)
-------------
-Unsatisfiable.
-
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
- // B0, B1
- ConstraintContext Ctx;
- std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-B1
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, Implication) {
- // B0, B0 => B1
- ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- auto B1 = Ctx.atom();
- auto Impl = Ctx.disj(Ctx.neg(B0), B1);
- std::vector<BoolValue *> Constraints({B0, Impl});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
- (not
- B0)
- B1)
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+ auto Expected = R"(((False & V2) | (True | V3)))";
+ std::string Actual;
+ llvm::raw_string_ostream OS(Actual);
+ B->print(OS, Delegate);
+ EXPECT_THAT(Actual, StrEq(Expected));
}
-TEST(SATCheckDebugStringTest, Iff) {
- // B0, B0 <=> B1
- ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- auto B1 = Ctx.atom();
- auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
- std::vector<BoolValue *> Constraints({B0, Iff});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(and
- (or
- (not
- B0)
- B1)
- (or
- B0
- (not
- B1)))
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, Xor) {
- // B0, XOR(B0, B1)
- ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- auto B1 = Ctx.atom();
- auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
- std::vector<BoolValue *> Constraints({B0, XOR});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
- (and
- B0
- (not
- B1))
- (and
- (not
- B0)
- B1))
-------------
-Satisfiable.
-
-B0 = True
-B1 = False
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
- // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
- ConstraintContext Ctx;
- auto Cond = cast<AtomicBoolValue>(Ctx.atom());
- auto Then = cast<AtomicBoolValue>(Ctx.atom());
- auto Else = cast<AtomicBoolValue>(Ctx.atom());
- auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
- Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
- std::vector<BoolValue *> Constraints({Cond, B});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-Cond
-
-(or
- (and
- Cond
- (and
- Then
- (not
- Else)))
- (and
- (not
- Cond)
- (and
- (not
- Then)
- Else)))
-------------
-Satisfiable.
-
-Cond = True
-Else = False
-Then = True
-)";
- EXPECT_THAT(debugString(Constraints, Result,
- {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
- StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
- // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
- ConstraintContext Ctx;
- auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
- auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
- auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
- auto BothZeroImpliesEQ =
- Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
- std::vector<BoolValue *> Constraints(
- {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-ThisIntEqZero
-
-(not
- IntsAreEq)
-
-(or
- (not
- (and
- ThisIntEqZero
- OtherIntEqZero))
- IntsAreEq)
-------------
-Satisfiable.
-
-IntsAreEq = False
-OtherIntEqZero = False
-ThisIntEqZero = True
-)";
- EXPECT_THAT(debugString(Constraints, Result,
- {{IntsAreEq, "IntsAreEq"},
- {ThisIntEqZero, "ThisIntEqZero"},
- {OtherIntEqZero, "OtherIntEqZero"}}),
- StrEq(Expected));
-}
} // 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,77 @@
+//===- 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/ADT/StringRef.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;
+}
+
+static llvm::StringLiteral sigil(Formula::Kind K) {
+ switch (K) {
+ case Formula::AtomRef:
+ return "";
+ case Formula::Not:
+ return "!";
+ case Formula::And:
+ return " & ";
+ case Formula::Or:
+ return " | ";
+ case Formula::Implies:
+ return " => ";
+ case Formula::Equal:
+ return " = ";
+ }
+ llvm_unreachable("unhandled formula kind");
+}
+
+void Formula::print(llvm::raw_ostream &OS,
+ llvm::function_ref<DelegatePrinter> Delegate) const {
+ if (Delegate && Delegate(OS, *this))
+ return;
+
+ switch (numOperands(kind())) {
+ case 0:
+ OS << atom();
+ break;
+ case 1:
+ OS << sigil(kind());
+ operands()[0]->print(OS, Delegate);
+ break;
+ case 2:
+ OS << '(';
+ operands()[0]->print(OS, Delegate);
+ OS << sigil(kind());
+ operands()[1]->print(OS, Delegate);
+ OS << ')';
+ break;
+ default:
+ llvm_unreachable("unhandled formula arity");
+ }
+}
+
+} // 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,133 @@
+//===- 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 bool hasValue(Kind K) {
+ // Currently, formulas have either values or operands, not both.
+ return numOperands(K) == 0;
+ }
+ 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
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
