From 632de855a0420bf6ea56fc8b4727c64a9823a485 Mon Sep 17 00:00:00 2001 From: Wei Yi Tee Date: Tue, 12 Jul 2022 18:47:18 +0000 Subject: [PATCH] [clang][dataflow] Refactor boolean creation as a test utility. Differential Revision: https://reviews.llvm.org/D129546 --- .../Analysis/FlowSensitive/SolverTest.cpp | 299 ++++++++++----------- .../Analysis/FlowSensitive/TestingSupport.h | 57 +++- 2 files changed, 189 insertions(+), 167 deletions(-) diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp index cfce7a0..e950d6b 100644 --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -6,87 +6,47 @@ // //===----------------------------------------------------------------------===// +#include + +#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 -#include -#include 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 Vals) { - return WatchedLiteralsSolver().solve(std::move(Vals)); - } - - // Creates an atomic boolean value. - BoolValue *atom() { - Vals.push_back(std::make_unique()); - return Vals.back().get(); - } - - // Creates a boolean conjunction value. - BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) { - Vals.push_back( - std::make_unique(*LeftSubVal, *RightSubVal)); - return Vals.back().get(); - } - - // Creates a boolean disjunction value. - BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) { - Vals.push_back( - std::make_unique(*LeftSubVal, *RightSubVal)); - return Vals.back().get(); - } - - // Creates a boolean negation value. - BoolValue *neg(BoolValue *SubVal) { - Vals.push_back(std::make_unique(*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 - void expectSatisfiable(Solver::Result Result, Matcher Solution) { - EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable); - EXPECT_THAT(Result.getSolution(), Optional(Solution)); - } - -private: - std::vector> 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 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 +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 3d873ec..debff04 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 +#include +#include +#include +#include +#include + #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 -#include -#include -#include -#include 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()); + return Vals.back().get(); + } + + // Creates a boolean conjunction value. + BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) { + Vals.push_back( + std::make_unique(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); + } + + // Creates a boolean disjunction value. + BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) { + Vals.push_back( + std::make_unique(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); + } + + // Creates a boolean negation value. + BoolValue *neg(BoolValue *SubVal) { + Vals.push_back(std::make_unique(*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> Vals; +}; + } // namespace test } // namespace dataflow } // namespace clang -- 2.7.4