Author: martinboehme Date: 2024-05-08T16:12:53+02:00 New Revision: d6d613aaebc0ae503409ba7719a43b4a55e1ee70
URL: https://github.com/llvm/llvm-project/commit/d6d613aaebc0ae503409ba7719a43b4a55e1ee70 DIFF: https://github.com/llvm/llvm-project/commit/d6d613aaebc0ae503409ba7719a43b4a55e1ee70.diff LOG: [clang][dataflow] Make `SolverTest` a type-parameterized test. (#91455) This allows the tests to be run against any implementation of `Solver` instead of begin specific to `WatchedLiteralsSolver` as they currently are. Added: clang/unittests/Analysis/FlowSensitive/SolverTest.h clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp Modified: clang/docs/tools/clang-formatted-files.txt clang/unittests/Analysis/FlowSensitive/CMakeLists.txt llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn Removed: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp ################################################################################ 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..0a2514a2d7c12 --- /dev/null +++ b/clang/unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.cpp @@ -0,0 +1,26 @@ +//===- unittests/Analysis/FlowSensitive/WatchedLiteralsSolverTest.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", ] } _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
