[clang] [llvm] [clang][dataflow] Make `SolverTest` a type-parameterized test. (PR #91455)
via cfe-commits
cfe-commits at lists.llvm.org
Wed May 8 03:30:12 PDT 2024
llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT-->
@llvm/pr-subscribers-clang
Author: None (martinboehme)
<details>
<summary>Changes</summary>
This allows the tests to be run against any implementation of `Solver` instead
of begin specific to `WatchedLiteralsSolver` as they currently are.
---
Full diff: https://github.com/llvm/llvm-project/pull/91455.diff
5 Files Affected:
- (modified) clang/docs/tools/clang-formatted-files.txt (+2-1)
- (modified) clang/unittests/Analysis/FlowSensitive/CMakeLists.txt (+1-1)
- (renamed) clang/unittests/Analysis/FlowSensitive/SolverTest.h (+94-72)
- (added) clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp (+26)
- (modified) llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn (+1-1)
``````````diff
diff --git a/clang/docs/tools/clang-formatted-files.txt b/clang/docs/tools/clang-formatted-files.txt
index 2252d0ccde96d..eaeadf2656b0b 100644
--- a/clang/docs/tools/clang-formatted-files.txt
+++ b/clang/docs/tools/clang-formatted-files.txt
@@ -632,11 +632,12 @@ clang/unittests/Analysis/FlowSensitive/MapLatticeTest.cpp
clang/unittests/Analysis/FlowSensitive/MatchSwitchTest.cpp
clang/unittests/Analysis/FlowSensitive/MultiVarConstantPropagationTest.cpp
clang/unittests/Analysis/FlowSensitive/SingleVarConstantPropagationTest.cpp
-clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+clang/unittests/Analysis/FlowSensitive/SolverTest.h
clang/unittests/Analysis/FlowSensitive/TestingSupport.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TestingSupportTest.cpp
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp
clang/unittests/AST/ASTImporterFixtures.cpp
clang/unittests/AST/ASTImporterFixtures.h
clang/unittests/AST/ASTImporterObjCTest.cpp
diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
index 94160d949637c..cfabb80576bc1 100644
--- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -19,7 +19,6 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
SignAnalysisTest.cpp
SimplifyConstraintsTest.cpp
SingleVarConstantPropagationTest.cpp
- SolverTest.cpp
TestingSupport.cpp
TestingSupportTest.cpp
TransferBranchTest.cpp
@@ -27,6 +26,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
TypeErasedDataflowAnalysisTest.cpp
UncheckedOptionalAccessModelTest.cpp
ValueTest.cpp
+ WatchedLiteralsSolverTest.cpp
)
clang_target_link_libraries(ClangAnalysisFlowSensitiveTests
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.h
similarity index 62%
rename from clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
rename to clang/unittests/Analysis/FlowSensitive/SolverTest.h
index 71f6da93594e3..b375344381213 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.h
@@ -1,4 +1,4 @@
-//===- unittests/Analysis/FlowSensitive/SolverTest.cpp --------------------===//
+//===--- SolverTest.h - Type-parameterized test for solvers ---------------===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
@@ -6,43 +6,53 @@
//
//===----------------------------------------------------------------------===//
-#include <utility>
+#ifndef LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_SOLVER_TEST_H_
+#define LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_SOLVER_TEST_H_
#include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Arena.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
-#include "clang/Basic/LLVM.h"
-#include "llvm/ADT/ArrayRef.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
-#include <vector>
+
+namespace clang::dataflow::test {
namespace {
-using namespace clang;
-using namespace dataflow;
+constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
+constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
-using test::ConstraintContext;
-using test::parseFormulas;
using testing::_;
using testing::AnyOf;
using testing::Pair;
using testing::UnorderedElementsAre;
-constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
-constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
+} // namespace
-// Checks if the conjunction of `Vals` is satisfiable and returns the
-// corresponding result.
-Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
- return WatchedLiteralsSolver().solve(Vals);
-}
+/// Type-parameterized test for implementations of the `Solver` interface.
+/// To use:
+/// 1. Implement a specialization of `createSolverWithLowTimeout()` for the
+/// solver you want to test.
+/// 2. Instantiate the test suite for the solver you want to test using
+/// `INSTANTIATE_TYPED_TEST_SUITE_P()`.
+/// See WatchedLiteralsSolverTest.cpp for an example.
+template <typename SolverT> class SolverTest : public ::testing::Test {
+protected:
+ // Checks if the conjunction of `Vals` is satisfiable and returns the
+ // corresponding result.
+ Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
+ return SolverT().solve(Vals);
+ }
+
+ // Create a specialization for the solver type to test.
+ SolverT createSolverWithLowTimeout();
+};
+
+TYPED_TEST_SUITE_P(SolverTest);
MATCHER(unsat, "") {
return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
}
+
MATCHER_P(sat, SolutionMatcher,
"is satisfiable, where solution " +
(testing::DescribeMatcher<
@@ -55,57 +65,57 @@ MATCHER_P(sat, SolutionMatcher,
result_listener);
}
-TEST(SolverTest, Var) {
+TYPED_TEST_P(SolverTest, Var) {
ConstraintContext Ctx;
auto X = Ctx.atom();
// X
- EXPECT_THAT(solve({X}),
+ EXPECT_THAT(this->solve({X}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
}
-TEST(SolverTest, NegatedVar) {
+TYPED_TEST_P(SolverTest, NegatedVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
// !X
- EXPECT_THAT(solve({NotX}),
+ EXPECT_THAT(this->solve({NotX}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
}
-TEST(SolverTest, UnitConflict) {
+TYPED_TEST_P(SolverTest, UnitConflict) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
// X ^ !X
- EXPECT_THAT(solve({X, NotX}), unsat());
+ EXPECT_THAT(this->solve({X, NotX}), unsat());
}
-TEST(SolverTest, DistinctVars) {
+TYPED_TEST_P(SolverTest, DistinctVars) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
auto NotY = Ctx.neg(Y);
// X ^ !Y
- EXPECT_THAT(solve({X, NotY}),
+ EXPECT_THAT(this->solve({X, NotY}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
Pair(Y->getAtom(), AssignedFalse))));
}
-TEST(SolverTest, DoubleNegation) {
+TYPED_TEST_P(SolverTest, DoubleNegation) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
auto NotNotX = Ctx.neg(NotX);
// !!X ^ !X
- EXPECT_THAT(solve({NotNotX, NotX}), unsat());
+ EXPECT_THAT(this->solve({NotNotX, NotX}), unsat());
}
-TEST(SolverTest, NegatedDisjunction) {
+TYPED_TEST_P(SolverTest, NegatedDisjunction) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -113,10 +123,10 @@ TEST(SolverTest, NegatedDisjunction) {
auto NotXOrY = Ctx.neg(XOrY);
// !(X v Y) ^ (X v Y)
- EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
+ EXPECT_THAT(this->solve({NotXOrY, XOrY}), unsat());
}
-TEST(SolverTest, NegatedConjunction) {
+TYPED_TEST_P(SolverTest, NegatedConjunction) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -124,48 +134,48 @@ TEST(SolverTest, NegatedConjunction) {
auto NotXAndY = Ctx.neg(XAndY);
// !(X ^ Y) ^ (X ^ Y)
- EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
+ EXPECT_THAT(this->solve({NotXAndY, XAndY}), unsat());
}
-TEST(SolverTest, DisjunctionSameVarWithNegation) {
+TYPED_TEST_P(SolverTest, DisjunctionSameVarWithNegation) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
auto XOrNotX = Ctx.disj(X, NotX);
// X v !X
- EXPECT_THAT(solve({XOrNotX}), sat(_));
+ EXPECT_THAT(this->solve({XOrNotX}), sat(_));
}
-TEST(SolverTest, DisjunctionSameVar) {
+TYPED_TEST_P(SolverTest, DisjunctionSameVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto XOrX = Ctx.disj(X, X);
// X v X
- EXPECT_THAT(solve({XOrX}), sat(_));
+ EXPECT_THAT(this->solve({XOrX}), sat(_));
}
-TEST(SolverTest, ConjunctionSameVarsConflict) {
+TYPED_TEST_P(SolverTest, ConjunctionSameVarsConflict) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto NotX = Ctx.neg(X);
auto XAndNotX = Ctx.conj(X, NotX);
// X ^ !X
- EXPECT_THAT(solve({XAndNotX}), unsat());
+ EXPECT_THAT(this->solve({XAndNotX}), unsat());
}
-TEST(SolverTest, ConjunctionSameVar) {
+TYPED_TEST_P(SolverTest, ConjunctionSameVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto XAndX = Ctx.conj(X, X);
// X ^ X
- EXPECT_THAT(solve({XAndX}), sat(_));
+ EXPECT_THAT(this->solve({XAndX}), sat(_));
}
-TEST(SolverTest, PureVar) {
+TYPED_TEST_P(SolverTest, PureVar) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -175,12 +185,12 @@ TEST(SolverTest, PureVar) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
- EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
+ EXPECT_THAT(this->solve({NotXOrY, NotXOrNotY}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
Pair(Y->getAtom(), _))));
}
-TEST(SolverTest, MustAssumeVarIsFalse) {
+TYPED_TEST_P(SolverTest, MustAssumeVarIsFalse) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -191,12 +201,12 @@ TEST(SolverTest, MustAssumeVarIsFalse) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
- EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
+ EXPECT_THAT(this->solve({XOrY, NotXOrY, NotXOrNotY}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
Pair(Y->getAtom(), AssignedTrue))));
}
-TEST(SolverTest, DeepConflict) {
+TYPED_TEST_P(SolverTest, DeepConflict) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -208,10 +218,10 @@ TEST(SolverTest, DeepConflict) {
auto XOrNotY = Ctx.disj(X, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
- EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
+ EXPECT_THAT(this->solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
}
-TEST(SolverTest, IffIsEquivalentToDNF) {
+TYPED_TEST_P(SolverTest, IffIsEquivalentToDNF) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -222,19 +232,19 @@ TEST(SolverTest, IffIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
// !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
- EXPECT_THAT(solve({NotEquivalent}), unsat());
+ EXPECT_THAT(this->solve({NotEquivalent}), unsat());
}
-TEST(SolverTest, IffSameVars) {
+TYPED_TEST_P(SolverTest, IffSameVars) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto XEqX = Ctx.iff(X, X);
// X <=> X
- EXPECT_THAT(solve({XEqX}), sat(_));
+ EXPECT_THAT(this->solve({XEqX}), sat(_));
}
-TEST(SolverTest, IffDistinctVars) {
+TYPED_TEST_P(SolverTest, IffDistinctVars) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
@@ -242,36 +252,36 @@ TEST(SolverTest, IffDistinctVars) {
// X <=> Y
EXPECT_THAT(
- solve({XEqY}),
+ this->solve({XEqY}),
sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
Pair(Y->getAtom(), AssignedTrue)),
UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
Pair(Y->getAtom(), AssignedFalse)))));
}
-TEST(SolverTest, IffWithUnits) {
+TYPED_TEST_P(SolverTest, IffWithUnits) {
ConstraintContext Ctx;
auto X = Ctx.atom();
auto Y = Ctx.atom();
auto XEqY = Ctx.iff(X, Y);
// (X <=> Y) ^ X ^ Y
- EXPECT_THAT(solve({XEqY, X, Y}),
+ EXPECT_THAT(this->solve({XEqY, X, Y}),
sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
Pair(Y->getAtom(), AssignedTrue))));
}
-TEST(SolverTest, IffWithUnitsConflict) {
+TYPED_TEST_P(SolverTest, IffWithUnitsConflict) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(V0 = V1)
V0
!V1
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, IffTransitiveConflict) {
+TYPED_TEST_P(SolverTest, IffTransitiveConflict) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(V0 = V1)
@@ -279,63 +289,63 @@ TEST(SolverTest, IffTransitiveConflict) {
V2
!V0
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, DeMorgan) {
+TYPED_TEST_P(SolverTest, DeMorgan) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(!(V0 | V1) = (!V0 & !V1))
(!(V2 & V3) = (!V2 | !V3))
)");
- EXPECT_THAT(solve(Constraints), sat(_));
+ EXPECT_THAT(this->solve(Constraints), sat(_));
}
-TEST(SolverTest, RespectsAdditionalConstraints) {
+TYPED_TEST_P(SolverTest, RespectsAdditionalConstraints) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(V0 = V1)
V0
!V1
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, ImplicationIsEquivalentToDNF) {
+TYPED_TEST_P(SolverTest, ImplicationIsEquivalentToDNF) {
Arena A;
auto Constraints = parseFormulas(A, R"(
!((V0 => V1) = (!V0 | V1))
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, ImplicationConflict) {
+TYPED_TEST_P(SolverTest, ImplicationConflict) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(V0 => V1)
(V0 & !V1)
)");
- EXPECT_THAT(solve(Constraints), unsat());
+ EXPECT_THAT(this->solve(Constraints), unsat());
}
-TEST(SolverTest, ReachedLimitsReflectsTimeouts) {
+TYPED_TEST_P(SolverTest, ReachedLimitsReflectsTimeouts) {
Arena A;
auto Constraints = parseFormulas(A, R"(
(!(V0 | V1) = (!V0 & !V1))
(!(V2 & V3) = (!V2 & !V3))
)");
- WatchedLiteralsSolver solver(10);
+ TypeParam solver = this->createSolverWithLowTimeout();
ASSERT_EQ(solver.solve(Constraints).getStatus(),
Solver::Result::Status::TimedOut);
EXPECT_TRUE(solver.reachedLimit());
}
-TEST(SolverTest, SimpleButLargeContradiction) {
+TYPED_TEST_P(SolverTest, SimpleButLargeContradiction) {
// This test ensures that the solver takes a short-cut on known
// contradictory inputs, without using max_iterations. At the time
// this test is added, formulas that are easily recognized to be
// contradictory at CNF construction time would lead to timeout.
- WatchedLiteralsSolver solver(10);
+ TypeParam solver = this->createSolverWithLowTimeout();
ConstraintContext Ctx;
auto first = Ctx.atom();
auto last = first;
@@ -358,4 +368,16 @@ TEST(SolverTest, SimpleButLargeContradiction) {
EXPECT_FALSE(solver.reachedLimit());
}
-} // namespace
+REGISTER_TYPED_TEST_SUITE_P(
+ SolverTest, Var, NegatedVar, UnitConflict, DistinctVars, DoubleNegation,
+ NegatedDisjunction, NegatedConjunction, DisjunctionSameVarWithNegation,
+ DisjunctionSameVar, ConjunctionSameVarsConflict, ConjunctionSameVar,
+ PureVar, MustAssumeVarIsFalse, DeepConflict, IffIsEquivalentToDNF,
+ IffSameVars, IffDistinctVars, IffWithUnits, IffWithUnitsConflict,
+ IffTransitiveConflict, DeMorgan, RespectsAdditionalConstraints,
+ ImplicationIsEquivalentToDNF, ImplicationConflict,
+ ReachedLimitsReflectsTimeouts, SimpleButLargeContradiction);
+
+} // namespace clang::dataflow::test
+
+#endif // LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_
diff --git a/clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp
new file mode 100644
index 0000000000000..d83ea403511af
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp
@@ -0,0 +1,26 @@
+//===- unittests/Analysis/FlowSensitive/SolverTest.cpp --------------------===//
+//
+// 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/WatchedLiteralsSolver.h"
+#include "SolverTest.h"
+
+namespace clang::dataflow::test {
+
+template <>
+WatchedLiteralsSolver
+SolverTest<WatchedLiteralsSolver>::createSolverWithLowTimeout() {
+ return WatchedLiteralsSolver(10);
+}
+
+namespace {
+
+INSTANTIATE_TYPED_TEST_SUITE_P(WatchedLiteralsSolverTest, SolverTest,
+ WatchedLiteralsSolver);
+
+} // namespace
+} // namespace clang::dataflow::test
diff --git a/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn b/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
index df5b4587bf1c1..e16ca31b81a8d 100644
--- a/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
+++ b/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
@@ -33,7 +33,6 @@ unittest("ClangAnalysisFlowSensitiveTests") {
"SignAnalysisTest.cpp",
"SimplifyConstraintsTest.cpp",
"SingleVarConstantPropagationTest.cpp",
- "SolverTest.cpp",
"TestingSupport.cpp",
"TestingSupportTest.cpp",
"TransferBranchTest.cpp",
@@ -41,5 +40,6 @@ unittest("ClangAnalysisFlowSensitiveTests") {
"TypeErasedDataflowAnalysisTest.cpp",
"UncheckedOptionalAccessModelTest.cpp",
"ValueTest.cpp",
+ "WatchedLiteralsSolverTest.cpp",
]
}
``````````
</details>
https://github.com/llvm/llvm-project/pull/91455
More information about the cfe-commits
mailing list