wyt created this revision.
Herald added subscribers: martong, tschuett, xazax.hun.
Herald added a project: All.
wyt requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D129546
Files:
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
@@ -220,6 +220,49 @@
/// `Name` must be unique in `ASTCtx`.
const ValueDecl *findValueDecl(ASTContext &ASTCtx, llvm::StringRef Name);
+/// Utility class for creating boolean values.
+class BoolValueManager {
+public:
+ // Creates an atomic boolean value.
+ BoolValue *atom() {
+ Vals.push_back(std::make_unique<AtomicBoolValue>());
+ return Vals.back().get();
+ }
+
+ // Creates a boolean conjunction value.
+ BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ Vals.push_back(
+ std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
+ return Vals.back().get();
+ }
+
+ // Creates a boolean disjunction value.
+ BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ Vals.push_back(
+ std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
+ return Vals.back().get();
+ }
+
+ // Creates a boolean negation value.
+ BoolValue *neg(BoolValue *SubVal) {
+ Vals.push_back(std::make_unique<NegationValue>(*SubVal));
+ return Vals.back().get();
+ }
+
+ // Creates a boolean implication value.
+ BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ return disj(neg(LeftSubVal), RightSubVal);
+ }
+
+ // Creates a boolean biconditional value.
+ BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ return conj(impl(LeftSubVal, RightSubVal), impl(RightSubVal, LeftSubVal));
+ }
+
+private:
+ std::vector<std::unique_ptr<BoolValue>> Vals;
+};
+
} // namespace test
} // namespace dataflow
} // namespace clang
Index: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -7,6 +7,7 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "TestingSupport.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "gmock/gmock.h"
@@ -34,42 +35,6 @@
return WatchedLiteralsSolver().solve(std::move(Vals));
}
- // Creates an atomic boolean value.
- BoolValue *atom() {
- Vals.push_back(std::make_unique<AtomicBoolValue>());
- return Vals.back().get();
- }
-
- // Creates a boolean conjunction value.
- BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
- }
-
- // Creates a boolean disjunction value.
- BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
- }
-
- // Creates a boolean negation value.
- BoolValue *neg(BoolValue *SubVal) {
- Vals.push_back(std::make_unique<NegationValue>(*SubVal));
- return Vals.back().get();
- }
-
- // Creates a boolean implication value.
- BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- return disj(neg(LeftSubVal), RightSubVal);
- }
-
- // Creates a boolean biconditional value.
- BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- return conj(impl(LeftSubVal, RightSubVal), impl(RightSubVal, LeftSubVal));
- }
-
void expectUnsatisfiable(Solver::Result Result) {
EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
EXPECT_FALSE(Result.getSolution().has_value());
@@ -81,12 +46,11 @@
EXPECT_THAT(Result.getSolution(), Optional(Solution));
}
-private:
- std::vector<std::unique_ptr<BoolValue>> Vals;
+ test::BoolValueManager Bools;
};
TEST_F(SolverTest, Var) {
- auto X = atom();
+ auto X = Bools.atom();
// X
expectSatisfiable(
@@ -95,8 +59,8 @@
}
TEST_F(SolverTest, NegatedVar) {
- auto X = atom();
- auto NotX = neg(X);
+ auto X = Bools.atom();
+ auto NotX = Bools.neg(X);
// !X
expectSatisfiable(
@@ -105,17 +69,17 @@
}
TEST_F(SolverTest, UnitConflict) {
- auto X = atom();
- auto NotX = neg(X);
+ auto X = Bools.atom();
+ auto NotX = Bools.neg(X);
// X ^ !X
expectUnsatisfiable(solve({X, NotX}));
}
TEST_F(SolverTest, DistinctVars) {
- auto X = atom();
- auto Y = atom();
- auto NotY = neg(Y);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto NotY = Bools.neg(Y);
// X ^ !Y
expectSatisfiable(
@@ -125,59 +89,59 @@
}
TEST_F(SolverTest, DoubleNegation) {
- auto X = atom();
- auto NotX = neg(X);
- auto NotNotX = neg(NotX);
+ auto X = Bools.atom();
+ auto NotX = Bools.neg(X);
+ auto NotNotX = Bools.neg(NotX);
// !!X ^ !X
expectUnsatisfiable(solve({NotNotX, NotX}));
}
TEST_F(SolverTest, NegatedDisjunction) {
- auto X = atom();
- auto Y = atom();
- auto XOrY = disj(X, Y);
- auto NotXOrY = neg(XOrY);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto XOrY = Bools.disj(X, Y);
+ auto NotXOrY = Bools.neg(XOrY);
// !(X v Y) ^ (X v Y)
expectUnsatisfiable(solve({NotXOrY, XOrY}));
}
TEST_F(SolverTest, NegatedConjunction) {
- auto X = atom();
- auto Y = atom();
- auto XAndY = conj(X, Y);
- auto NotXAndY = neg(XAndY);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto XAndY = Bools.conj(X, Y);
+ auto NotXAndY = Bools.neg(XAndY);
// !(X ^ Y) ^ (X ^ Y)
expectUnsatisfiable(solve({NotXAndY, XAndY}));
}
TEST_F(SolverTest, DisjunctionSameVars) {
- auto X = atom();
- auto NotX = neg(X);
- auto XOrNotX = disj(X, NotX);
+ auto X = Bools.atom();
+ auto NotX = Bools.neg(X);
+ auto XOrNotX = Bools.disj(X, NotX);
// X v !X
expectSatisfiable(solve({XOrNotX}), _);
}
TEST_F(SolverTest, ConjunctionSameVarsConflict) {
- auto X = atom();
- auto NotX = neg(X);
- auto XAndNotX = conj(X, NotX);
+ auto X = Bools.atom();
+ auto NotX = Bools.neg(X);
+ auto XAndNotX = Bools.conj(X, NotX);
// X ^ !X
expectUnsatisfiable(solve({XAndNotX}));
}
TEST_F(SolverTest, PureVar) {
- auto X = atom();
- auto Y = atom();
- auto NotX = neg(X);
- auto NotXOrY = disj(NotX, Y);
- auto NotY = neg(Y);
- auto NotXOrNotY = disj(NotX, NotY);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto NotX = Bools.neg(X);
+ auto NotXOrY = Bools.disj(NotX, Y);
+ auto NotY = Bools.neg(Y);
+ auto NotXOrNotY = Bools.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
expectSatisfiable(
@@ -187,13 +151,13 @@
}
TEST_F(SolverTest, MustAssumeVarIsFalse) {
- auto X = atom();
- auto Y = atom();
- auto XOrY = disj(X, Y);
- auto NotX = neg(X);
- auto NotXOrY = disj(NotX, Y);
- auto NotY = neg(Y);
- auto NotXOrNotY = disj(NotX, NotY);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto XOrY = Bools.disj(X, Y);
+ auto NotX = Bools.neg(X);
+ auto NotXOrY = Bools.disj(NotX, Y);
+ auto NotY = Bools.neg(Y);
+ auto NotXOrNotY = Bools.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
expectSatisfiable(
@@ -203,31 +167,31 @@
}
TEST_F(SolverTest, DeepConflict) {
- auto X = atom();
- auto Y = atom();
- auto XOrY = disj(X, Y);
- auto NotX = neg(X);
- auto NotXOrY = disj(NotX, Y);
- auto NotY = neg(Y);
- auto NotXOrNotY = disj(NotX, NotY);
- auto XOrNotY = disj(X, NotY);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto XOrY = Bools.disj(X, Y);
+ auto NotX = Bools.neg(X);
+ auto NotXOrY = Bools.disj(NotX, Y);
+ auto NotY = Bools.neg(Y);
+ auto NotXOrNotY = Bools.disj(NotX, NotY);
+ auto XOrNotY = Bools.disj(X, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
}
TEST_F(SolverTest, IffSameVars) {
- auto X = atom();
- auto XEqX = iff(X, X);
+ auto X = Bools.atom();
+ auto XEqX = Bools.iff(X, X);
// X <=> X
expectSatisfiable(solve({XEqX}), _);
}
TEST_F(SolverTest, IffDistinctVars) {
- auto X = atom();
- auto Y = atom();
- auto XEqY = iff(X, Y);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto XEqY = Bools.iff(X, Y);
// X <=> Y
expectSatisfiable(
@@ -241,9 +205,9 @@
}
TEST_F(SolverTest, IffWithUnits) {
- auto X = atom();
- auto Y = atom();
- auto XEqY = iff(X, Y);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto XEqY = Bools.iff(X, Y);
// (X <=> Y) ^ X ^ Y
expectSatisfiable(
@@ -253,58 +217,60 @@
}
TEST_F(SolverTest, IffWithUnitsConflict) {
- auto X = atom();
- auto Y = atom();
- auto XEqY = iff(X, Y);
- auto NotY = neg(Y);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto XEqY = Bools.iff(X, Y);
+ auto NotY = Bools.neg(Y);
// (X <=> Y) ^ X !Y
expectUnsatisfiable(solve({XEqY, X, NotY}));
}
TEST_F(SolverTest, IffTransitiveConflict) {
- auto X = atom();
- auto Y = atom();
- auto Z = atom();
- auto XEqY = iff(X, Y);
- auto YEqZ = iff(Y, Z);
- auto NotX = neg(X);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto Z = Bools.atom();
+ auto XEqY = Bools.iff(X, Y);
+ auto YEqZ = Bools.iff(Y, Z);
+ auto NotX = Bools.neg(X);
// (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
}
TEST_F(SolverTest, DeMorgan) {
- auto X = atom();
- auto Y = atom();
- auto Z = atom();
- auto W = atom();
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto Z = Bools.atom();
+ auto W = Bools.atom();
// !(X v Y) <=> !X ^ !Y
- auto A = iff(neg(disj(X, Y)), conj(neg(X), neg(Y)));
+ auto A = Bools.iff(Bools.neg(Bools.disj(X, Y)),
+ Bools.conj(Bools.neg(X), Bools.neg(Y)));
// !(Z ^ W) <=> !Z v !W
- auto B = iff(neg(conj(Z, W)), disj(neg(Z), neg(W)));
+ auto B = Bools.iff(Bools.neg(Bools.conj(Z, W)),
+ Bools.disj(Bools.neg(Z), Bools.neg(W)));
// A ^ B
expectSatisfiable(solve({A, B}), _);
}
TEST_F(SolverTest, RespectsAdditionalConstraints) {
- auto X = atom();
- auto Y = atom();
- auto XEqY = iff(X, Y);
- auto NotY = neg(Y);
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto XEqY = Bools.iff(X, Y);
+ auto NotY = Bools.neg(Y);
// (X <=> Y) ^ X ^ !Y
expectUnsatisfiable(solve({XEqY, X, NotY}));
}
TEST_F(SolverTest, ImplicationConflict) {
- auto X = atom();
- auto Y = atom();
- auto *XImplY = impl(X, Y);
- auto *XAndNotY = conj(X, neg(Y));
+ auto X = Bools.atom();
+ auto Y = Bools.atom();
+ auto *XImplY = Bools.impl(X, Y);
+ auto *XAndNotY = Bools.conj(X, Bools.neg(Y));
// X => Y ^ X ^ !Y
expectUnsatisfiable(solve({XImplY, XAndNotY}));
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
