[clang] 632de85 - [clang][dataflow] Refactor boolean creation as a test utility.
Wei Yi Tee via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 13 03:15:22 PDT 2022
Author: Wei Yi Tee
Date: 2022-07-13T10:15:06Z
New Revision: 632de855a0420bf6ea56fc8b4727c64a9823a485
URL: https://github.com/llvm/llvm-project/commit/632de855a0420bf6ea56fc8b4727c64a9823a485
DIFF: https://github.com/llvm/llvm-project/commit/632de855a0420bf6ea56fc8b4727c64a9823a485.diff
LOG: [clang][dataflow] Refactor boolean creation as a test utility.
Differential Revision: https://reviews.llvm.org/D129546
Added:
Modified:
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
Removed:
################################################################################
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index cfce7a09e1220..e950d6b91a5a0 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -6,87 +6,47 @@
//
//===----------------------------------------------------------------------===//
+#include <utility>
+
+#include "TestingSupport.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
-#include <memory>
-#include <utility>
-#include <vector>
namespace {
using namespace clang;
using namespace dataflow;
+using test::ConstraintContext;
using testing::_;
using testing::AnyOf;
using testing::Optional;
using testing::Pair;
using testing::UnorderedElementsAre;
-class SolverTest : public ::testing::Test {
-protected:
- // Checks if the conjunction of `Vals` is satisfiable and returns the
- // corresponding result.
- Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
- return WatchedLiteralsSolver().solve(std::move(Vals));
- }
-
- // 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());
- }
-
- template <typename Matcher>
- void expectSatisfiable(Solver::Result Result, Matcher Solution) {
- EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
- EXPECT_THAT(Result.getSolution(), Optional(Solution));
- }
-
-private:
- std::vector<std::unique_ptr<BoolValue>> Vals;
-};
-
-TEST_F(SolverTest, Var) {
- auto X = atom();
+// Checks if the conjunction of `Vals` is satisfiable and returns the
+// corresponding result.
+Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
+ return WatchedLiteralsSolver().solve(std::move(Vals));
+}
+
+void expectUnsatisfiable(Solver::Result Result) {
+ EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
+ EXPECT_FALSE(Result.getSolution().has_value());
+}
+
+template <typename Matcher>
+void expectSatisfiable(Solver::Result Result, Matcher Solution) {
+ EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
+ EXPECT_THAT(Result.getSolution(), Optional(Solution));
+}
+
+TEST(SolverTest, Var) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
// X
expectSatisfiable(
@@ -94,9 +54,10 @@ TEST_F(SolverTest, Var) {
UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
}
-TEST_F(SolverTest, NegatedVar) {
- auto X = atom();
- auto NotX = neg(X);
+TEST(SolverTest, NegatedVar) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto NotX = Ctx.neg(X);
// !X
expectSatisfiable(
@@ -104,18 +65,20 @@ TEST_F(SolverTest, NegatedVar) {
UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
}
-TEST_F(SolverTest, UnitConflict) {
- auto X = atom();
- auto NotX = neg(X);
+TEST(SolverTest, UnitConflict) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto NotX = Ctx.neg(X);
// X ^ !X
expectUnsatisfiable(solve({X, NotX}));
}
-TEST_F(SolverTest, DistinctVars) {
- auto X = atom();
- auto Y = atom();
- auto NotY = neg(Y);
+TEST(SolverTest, DistinctVars) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto NotY = Ctx.neg(Y);
// X ^ !Y
expectSatisfiable(
@@ -124,60 +87,66 @@ TEST_F(SolverTest, DistinctVars) {
Pair(Y, Solver::Result::Assignment::AssignedFalse)));
}
-TEST_F(SolverTest, DoubleNegation) {
- auto X = atom();
- auto NotX = neg(X);
- auto NotNotX = neg(NotX);
+TEST(SolverTest, DoubleNegation) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto NotX = Ctx.neg(X);
+ auto NotNotX = Ctx.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);
+TEST(SolverTest, NegatedDisjunction) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto XOrY = Ctx.disj(X, Y);
+ auto NotXOrY = Ctx.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);
+TEST(SolverTest, NegatedConjunction) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto XAndY = Ctx.conj(X, Y);
+ auto NotXAndY = Ctx.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);
+TEST(SolverTest, DisjunctionSameVars) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto NotX = Ctx.neg(X);
+ auto XOrNotX = Ctx.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);
+TEST(SolverTest, ConjunctionSameVarsConflict) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto NotX = Ctx.neg(X);
+ auto XAndNotX = Ctx.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);
+TEST(SolverTest, PureVar) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto NotX = Ctx.neg(X);
+ auto NotXOrY = Ctx.disj(NotX, Y);
+ auto NotY = Ctx.neg(Y);
+ auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
expectSatisfiable(
@@ -186,14 +155,15 @@ TEST_F(SolverTest, PureVar) {
Pair(Y, _)));
}
-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);
+TEST(SolverTest, MustAssumeVarIsFalse) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto XOrY = Ctx.disj(X, Y);
+ auto NotX = Ctx.neg(X);
+ auto NotXOrY = Ctx.disj(NotX, Y);
+ auto NotY = Ctx.neg(Y);
+ auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
expectSatisfiable(
@@ -202,32 +172,35 @@ TEST_F(SolverTest, MustAssumeVarIsFalse) {
Pair(Y, Solver::Result::Assignment::AssignedTrue)));
}
-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);
+TEST(SolverTest, DeepConflict) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto XOrY = Ctx.disj(X, Y);
+ auto NotX = Ctx.neg(X);
+ auto NotXOrY = Ctx.disj(NotX, Y);
+ auto NotY = Ctx.neg(Y);
+ auto NotXOrNotY = Ctx.disj(NotX, NotY);
+ auto XOrNotY = Ctx.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);
+TEST(SolverTest, IffSameVars) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto XEqX = Ctx.iff(X, X);
// X <=> X
expectSatisfiable(solve({XEqX}), _);
}
-TEST_F(SolverTest, IffDistinctVars) {
- auto X = atom();
- auto Y = atom();
- auto XEqY = iff(X, Y);
+TEST(SolverTest, IffDistinctVars) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto XEqY = Ctx.iff(X, Y);
// X <=> Y
expectSatisfiable(
@@ -240,10 +213,11 @@ TEST_F(SolverTest, IffDistinctVars) {
Pair(Y, Solver::Result::Assignment::AssignedFalse))));
}
-TEST_F(SolverTest, IffWithUnits) {
- auto X = atom();
- auto Y = atom();
- auto XEqY = iff(X, Y);
+TEST(SolverTest, IffWithUnits) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto XEqY = Ctx.iff(X, Y);
// (X <=> Y) ^ X ^ Y
expectSatisfiable(
@@ -252,59 +226,64 @@ TEST_F(SolverTest, IffWithUnits) {
Pair(Y, Solver::Result::Assignment::AssignedTrue)));
}
-TEST_F(SolverTest, IffWithUnitsConflict) {
- auto X = atom();
- auto Y = atom();
- auto XEqY = iff(X, Y);
- auto NotY = neg(Y);
+TEST(SolverTest, IffWithUnitsConflict) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto XEqY = Ctx.iff(X, Y);
+ auto NotY = Ctx.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);
+TEST(SolverTest, IffTransitiveConflict) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto Z = Ctx.atom();
+ auto XEqY = Ctx.iff(X, Y);
+ auto YEqZ = Ctx.iff(Y, Z);
+ auto NotX = Ctx.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();
+TEST(SolverTest, DeMorgan) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto Z = Ctx.atom();
+ auto W = Ctx.atom();
// !(X v Y) <=> !X ^ !Y
- auto A = iff(neg(disj(X, Y)), conj(neg(X), neg(Y)));
+ auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y)));
// !(Z ^ W) <=> !Z v !W
- auto B = iff(neg(conj(Z, W)), disj(neg(Z), neg(W)));
+ auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.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);
+TEST(SolverTest, RespectsAdditionalConstraints) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto XEqY = Ctx.iff(X, Y);
+ auto NotY = Ctx.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));
+TEST(SolverTest, ImplicationConflict) {
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto *XImplY = Ctx.impl(X, Y);
+ auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
// X => Y ^ X ^ !Y
expectUnsatisfiable(solve({XImplY, XAndNotY}));
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
index 3d873eceeba3f..debff04a3c068 100644
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -13,6 +13,13 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_
#define LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_
+#include <functional>
+#include <memory>
+#include <ostream>
+#include <string>
+#include <utility>
+#include <vector>
+
#include "clang/AST/ASTContext.h"
#include "clang/AST/Decl.h"
#include "clang/AST/Stmt.h"
@@ -30,17 +37,10 @@
#include "clang/Tooling/Tooling.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/StringMap.h"
#include "llvm/ADT/StringRef.h"
#include "llvm/Support/Errc.h"
#include "llvm/Support/Error.h"
-#include "llvm/Support/ErrorHandling.h"
#include "llvm/Testing/Support/Annotations.h"
-#include <functional>
-#include <memory>
-#include <ostream>
-#include <string>
-#include <utility>
namespace clang {
namespace dataflow {
@@ -220,6 +220,49 @@ llvm::Error checkDataflow(
/// `Name` must be unique in `ASTCtx`.
const ValueDecl *findValueDecl(ASTContext &ASTCtx, llvm::StringRef Name);
+/// 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();
+ }
+
+ // 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
More information about the cfe-commits
mailing list