[clang][dataflow] Refactor boolean creation as a test utility.

[wyt]

Summary

Functionality for creating boolean values moved from SolverTest.cpp to BoolValueManager class in TestingSupport.h.

[gribozavr2]

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

223

224

ConstraintContext, to match other ~Context types whose purpose is to own things.

[wyt]

Address comments on renaming. Removed test fixture class, replacing TEST_F with TEST.

[sgatev]

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

263

#include <vector>

[wyt]

Address comments: add used import, remove unused imports.

[wyt]

Removed unused imports in SolverTest.cpp

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

 //===- 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/Solver.h"
+#include "TestingSupport.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>
 

 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::BoolValueManager Bools;
 };
 
 TEST_F(SolverTest, Var) {
-  auto X = atom();
+  auto X = Bools.atom();
 
   // X
   expectSatisfiable(
       solve({X}),
       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
 }
 
 TEST_F(SolverTest, NegatedVar) {
-  auto X = atom();
-  auto NotX = neg(X);
+  auto X = Bools.atom();
+  auto NotX = Bools.neg(X);
 
   // !X
   expectSatisfiable(
       solve({NotX}),
       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
 }
 
 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(
       solve({X, NotY}),
       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
                            Pair(Y, Solver::Result::Assignment::AssignedFalse)));
 }
 
 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(
       solve({NotXOrY, NotXOrNotY}),
       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
                            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);
+  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(
       solve({XOrY, NotXOrY, NotXOrNotY}),
       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
                            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);
+  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(
       solve({XEqY}),
       AnyOf(UnorderedElementsAre(
                 Pair(X, Solver::Result::Assignment::AssignedTrue),
                 Pair(Y, Solver::Result::Assignment::AssignedTrue)),
             UnorderedElementsAre(
                 Pair(X, Solver::Result::Assignment::AssignedFalse),
                 Pair(Y, Solver::Result::Assignment::AssignedFalse))));
 }
 
 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(
       solve({XEqY, X, Y}),
       UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
                            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);
+  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}));
 }
 
 } // namespace

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

 
 /// Returns the `ValueDecl` for the given identifier.
 ///
 /// Requirements:
 ///
 ///  `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
 
 #endif // LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_