Author: Dmitri Gribenko Date: 2022-07-07T21:50:52+02:00 New Revision: 63fac424e674bbd77f63e2c76cda9ae28552916a
URL: https://github.com/llvm/llvm-project/commit/63fac424e674bbd77f63e2c76cda9ae28552916a DIFF: https://github.com/llvm/llvm-project/commit/63fac424e674bbd77f63e2c76cda9ae28552916a.diff LOG: Revert "[clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`." This reverts commit 19e21887eb18aa019000c2384ea7f2c91d937489. I accidentally landed the non-final version of the patch that used decomposition declarations (not yet usable in LLVM/Clang source). Added: Modified: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h clang/include/clang/Analysis/FlowSensitive/Solver.h clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp clang/unittests/Analysis/FlowSensitive/SolverTest.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index 358ace0430f62..d87b9cc37b996 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -271,18 +271,17 @@ class DataflowAnalysisContext { AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints, llvm::DenseSet<AtomicBoolValue *> &VisitedTokens); - /// Returns the outcome of satisfiability checking on `Constraints`. - /// Possible outcomes are: - /// - `Satisfiable`: A satisfying assignment exists and is returned. - /// - `Unsatisfiable`: A satisfying assignment does not exist. - /// - `TimedOut`: The search for a satisfying assignment was not completed. + /// Returns the result of satisfiability checking on `Constraints`. + /// Possible return values are: + /// - `Satisfiable`: There exists a satisfying assignment for `Constraints`. + /// - `Unsatisfiable`: There is no satisfying assignment for `Constraints`. + /// - `TimedOut`: The solver gives up on finding a satisfying assignment. Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints); /// Returns true if the solver is able to prove that there is no satisfying /// assignment for `Constraints` bool isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) { - return querySolver(std::move(Constraints)).getStatus() == - Solver::Result::Status::Unsatisfiable; + return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable; } /// Returns a boolean value as a result of substituting `Val` and its sub diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h index b7a14f3484e42..6b685b9b3c9a7 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Solver.h +++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h @@ -15,9 +15,7 @@ #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H #include "clang/Analysis/FlowSensitive/Value.h" -#include "llvm/ADT/DenseMap.h" #include "llvm/ADT/DenseSet.h" -#include "llvm/ADT/Optional.h" namespace clang { namespace dataflow { @@ -25,58 +23,17 @@ namespace dataflow { /// An interface for a SAT solver that can be used by dataflow analyses. class Solver { public: - struct Result { - enum class Status { - /// Indicates that there exists a satisfying assignment for a boolean - /// formula. - Satisfiable, - - /// Indicates that there is no satisfying assignment for a boolean - /// formula. - Unsatisfiable, - - /// Indicates that the solver gave up trying to find a satisfying - /// assignment for a boolean formula. - TimedOut, - }; - - /// A boolean value is set to true or false in a truth assignment. - enum class Assignment : uint8_t { AssignedFalse = 0, AssignedTrue = 1 }; - - /// Constructs a result indicating that the queried boolean formula is - /// satisfiable. The result will hold a solution found by the solver. - static Result - Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) { - return Result(Status::Satisfiable, std::move(Solution)); - } - - /// Constructs a result indicating that the queried boolean formula is - /// unsatisfiable. - static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); } - - /// Constructs a result indicating that satisfiability checking on the - /// queried boolean formula was not completed. - static Result TimedOut() { return Result(Status::TimedOut, {}); } - - /// Returns the status of satisfiability checking on the queried boolean + enum class Result { + /// Indicates that there exists a satisfying assignment for a boolean /// formula. - Status getStatus() const { return Status; } + Satisfiable, - /// Returns a truth assignment to boolean values that satisfies the queried - /// boolean formula if available. Otherwise, an empty optional is returned. - llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> - getSolution() const { - return Solution; - } + /// Indicates that there is no satisfying assignment for a boolean formula. + Unsatisfiable, - private: - Result( - enum Status Status, - llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution) - : Status(Status), Solution(std::move(Solution)) {} - - Status Status; - llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution; + /// Indicates that the solver gave up trying to find a satisfying assignment + /// for a boolean formula. + TimedOut, }; virtual ~Solver() = default; @@ -87,6 +44,9 @@ class Solver { /// Requirements: /// /// All elements in `Vals` must not be null. + /// + /// FIXME: Consider returning a model in case the conjunction of `Vals` is + /// satisfiable so that it can be used to generate warning messages. virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0; }; diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp index 9b1b7a821405c..0e6e70d6d5d47 100644 --- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp +++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp @@ -120,13 +120,7 @@ struct BooleanFormula { /// clauses in the formula start from the element at index 1. std::vector<ClauseID> NextWatched; - /// Stores the variable identifier and value location for atomic booleans in - /// the formula. - llvm::DenseMap<Variable, AtomicBoolValue *> Atomics; - - explicit BooleanFormula(Variable LargestVar, - llvm::DenseMap<Variable, AtomicBoolValue *> Atomics) - : LargestVar(LargestVar), Atomics(std::move(Atomics)) { + explicit BooleanFormula(Variable LargestVar) : LargestVar(LargestVar) { Clauses.push_back(0); ClauseStarts.push_back(0); NextWatched.push_back(0); @@ -186,47 +180,28 @@ BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) { // Map each sub-value in `Vals` to a unique variable. llvm::DenseMap<BoolValue *, Variable> SubValsToVar; - // Store variable identifiers and value location of atomic booleans. - llvm::DenseMap<Variable, AtomicBoolValue *> Atomics; Variable NextVar = 1; { std::queue<BoolValue *> UnprocessedSubVals; for (BoolValue *Val : Vals) UnprocessedSubVals.push(Val); while (!UnprocessedSubVals.empty()) { - Variable Var = NextVar; BoolValue *Val = UnprocessedSubVals.front(); UnprocessedSubVals.pop(); - if (!SubValsToVar.try_emplace(Val, Var).second) + if (!SubValsToVar.try_emplace(Val, NextVar).second) continue; ++NextVar; // Visit the sub-values of `Val`. - switch (Val->getKind()) { - case Value::Kind::Conjunction: { - auto *C = cast<ConjunctionValue>(Val); + if (auto *C = dyn_cast<ConjunctionValue>(Val)) { UnprocessedSubVals.push(&C->getLeftSubValue()); UnprocessedSubVals.push(&C->getRightSubValue()); - break; - } - case Value::Kind::Disjunction: { - auto *D = cast<DisjunctionValue>(Val); + } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) { UnprocessedSubVals.push(&D->getLeftSubValue()); UnprocessedSubVals.push(&D->getRightSubValue()); - break; - } - case Value::Kind::Negation: { - auto *N = cast<NegationValue>(Val); + } else if (auto *N = dyn_cast<NegationValue>(Val)) { UnprocessedSubVals.push(&N->getSubVal()); - break; - } - case Value::Kind::AtomicBool: { - Atomics[Var] = cast<AtomicBoolValue>(Val); - break; - } - default: - llvm_unreachable("buildBooleanFormula: unhandled value kind"); } } } @@ -237,7 +212,7 @@ BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) { return ValIt->second; }; - BooleanFormula Formula(NextVar - 1, std::move(Atomics)); + BooleanFormula Formula(NextVar - 1); std::vector<bool> ProcessedSubVals(NextVar, false); // Add a conjunct for each variable that represents a top-level conjunction @@ -408,7 +383,7 @@ class WatchedLiteralsSolverImpl { // If the root level is reached, then all possible assignments lead to // a conflict. if (Level == 0) - return Solver::Result::Unsatisfiable(); + return WatchedLiteralsSolver::Result::Unsatisfiable; // Otherwise, take the other branch at the most recent level where a // decision was made. @@ -465,28 +440,12 @@ class WatchedLiteralsSolverImpl { ++I; } } - return Solver::Result::Satisfiable(buildSolution()); + return WatchedLiteralsSolver::Result::Satisfiable; } private: - /// Returns a satisfying truth assignment to the atomic values in the boolean - /// formula. - llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> - buildSolution() { - llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution; - for (auto [Var, Val] : Formula.Atomics) { - // A variable may have a definite true/false assignment, or it may be - // unassigned indicating its truth value does not affect the result of - // the formula. Unassigned variables are assigned to true as a default. - Solution[Val] = VarAssignments[Var] == Assignment::AssignedFalse - ? Solver::Result::Assignment::AssignedFalse - : Solver::Result::Assignment::AssignedTrue; - } - return Solution; - } - - /// Reverses forced moves until the most recent level where a decision was - /// made on the assignment of a variable. + // Reverses forced moves until the most recent level where a decision was made + // on the assignment of a variable. void reverseForcedMoves() { for (; LevelStates[Level] == State::Forced; --Level) { const Variable Var = LevelVars[Level]; @@ -500,7 +459,7 @@ class WatchedLiteralsSolverImpl { } } - /// Updates watched literals that are affected by a variable assignment. + // Updates watched literals that are affected by a variable assignment. void updateWatchedLiterals() { const Variable Var = LevelVars[Level]; @@ -633,7 +592,7 @@ class WatchedLiteralsSolverImpl { }; Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) { - return Vals.empty() ? Solver::Result::Satisfiable({{}}) + return Vals.empty() ? WatchedLiteralsSolver::Result::Satisfiable : WatchedLiteralsSolverImpl(Vals).solve(); } diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp index cfce7a09e1220..c5116b9edbe05 100644 --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -20,12 +20,6 @@ namespace { using namespace clang; using namespace dataflow; -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 @@ -70,17 +64,6 @@ class SolverTest : public ::testing::Test { 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; }; @@ -89,9 +72,7 @@ TEST_F(SolverTest, Var) { auto X = atom(); // X - expectSatisfiable( - solve({X}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue))); + EXPECT_EQ(solve({X}), Solver::Result::Satisfiable); } TEST_F(SolverTest, NegatedVar) { @@ -99,9 +80,7 @@ TEST_F(SolverTest, NegatedVar) { auto NotX = neg(X); // !X - expectSatisfiable( - solve({NotX}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse))); + EXPECT_EQ(solve({NotX}), Solver::Result::Satisfiable); } TEST_F(SolverTest, UnitConflict) { @@ -109,7 +88,7 @@ TEST_F(SolverTest, UnitConflict) { auto NotX = neg(X); // X ^ !X - expectUnsatisfiable(solve({X, NotX})); + EXPECT_EQ(solve({X, NotX}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, DistinctVars) { @@ -118,10 +97,7 @@ TEST_F(SolverTest, DistinctVars) { auto NotY = neg(Y); // X ^ !Y - expectSatisfiable( - solve({X, NotY}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue), - Pair(Y, Solver::Result::Assignment::AssignedFalse))); + EXPECT_EQ(solve({X, NotY}), Solver::Result::Satisfiable); } TEST_F(SolverTest, DoubleNegation) { @@ -130,7 +106,7 @@ TEST_F(SolverTest, DoubleNegation) { auto NotNotX = neg(NotX); // !!X ^ !X - expectUnsatisfiable(solve({NotNotX, NotX})); + EXPECT_EQ(solve({NotNotX, NotX}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, NegatedDisjunction) { @@ -140,7 +116,7 @@ TEST_F(SolverTest, NegatedDisjunction) { auto NotXOrY = neg(XOrY); // !(X v Y) ^ (X v Y) - expectUnsatisfiable(solve({NotXOrY, XOrY})); + EXPECT_EQ(solve({NotXOrY, XOrY}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, NegatedConjunction) { @@ -150,7 +126,7 @@ TEST_F(SolverTest, NegatedConjunction) { auto NotXAndY = neg(XAndY); // !(X ^ Y) ^ (X ^ Y) - expectUnsatisfiable(solve({NotXAndY, XAndY})); + EXPECT_EQ(solve({NotXAndY, XAndY}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, DisjunctionSameVars) { @@ -159,7 +135,7 @@ TEST_F(SolverTest, DisjunctionSameVars) { auto XOrNotX = disj(X, NotX); // X v !X - expectSatisfiable(solve({XOrNotX}), _); + EXPECT_EQ(solve({XOrNotX}), Solver::Result::Satisfiable); } TEST_F(SolverTest, ConjunctionSameVarsConflict) { @@ -168,7 +144,7 @@ TEST_F(SolverTest, ConjunctionSameVarsConflict) { auto XAndNotX = conj(X, NotX); // X ^ !X - expectUnsatisfiable(solve({XAndNotX})); + EXPECT_EQ(solve({XAndNotX}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, PureVar) { @@ -180,10 +156,7 @@ TEST_F(SolverTest, PureVar) { auto NotXOrNotY = disj(NotX, NotY); // (!X v Y) ^ (!X v !Y) - expectSatisfiable( - solve({NotXOrY, NotXOrNotY}), - UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse), - Pair(Y, _))); + EXPECT_EQ(solve({NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable); } TEST_F(SolverTest, MustAssumeVarIsFalse) { @@ -196,10 +169,7 @@ TEST_F(SolverTest, MustAssumeVarIsFalse) { auto NotXOrNotY = 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))); + EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable); } TEST_F(SolverTest, DeepConflict) { @@ -213,7 +183,8 @@ TEST_F(SolverTest, DeepConflict) { auto XOrNotY = disj(X, NotY); // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y) - expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY})); + EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), + Solver::Result::Unsatisfiable); } TEST_F(SolverTest, IffSameVars) { @@ -221,7 +192,7 @@ TEST_F(SolverTest, IffSameVars) { auto XEqX = iff(X, X); // X <=> X - expectSatisfiable(solve({XEqX}), _); + EXPECT_EQ(solve({XEqX}), Solver::Result::Satisfiable); } TEST_F(SolverTest, IffDistinctVars) { @@ -230,14 +201,7 @@ TEST_F(SolverTest, IffDistinctVars) { auto XEqY = 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)))); + EXPECT_EQ(solve({XEqY}), Solver::Result::Satisfiable); } TEST_F(SolverTest, IffWithUnits) { @@ -246,10 +210,7 @@ TEST_F(SolverTest, IffWithUnits) { auto XEqY = 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))); + EXPECT_EQ(solve({XEqY, X, Y}), Solver::Result::Satisfiable); } TEST_F(SolverTest, IffWithUnitsConflict) { @@ -259,7 +220,7 @@ TEST_F(SolverTest, IffWithUnitsConflict) { auto NotY = neg(Y); // (X <=> Y) ^ X !Y - expectUnsatisfiable(solve({XEqY, X, NotY})); + EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, IffTransitiveConflict) { @@ -271,7 +232,7 @@ TEST_F(SolverTest, IffTransitiveConflict) { auto NotX = neg(X); // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X - expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX})); + EXPECT_EQ(solve({XEqY, YEqZ, Z, NotX}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, DeMorgan) { @@ -287,7 +248,7 @@ TEST_F(SolverTest, DeMorgan) { auto B = iff(neg(conj(Z, W)), disj(neg(Z), neg(W))); // A ^ B - expectSatisfiable(solve({A, B}), _); + EXPECT_EQ(solve({A, B}), Solver::Result::Satisfiable); } TEST_F(SolverTest, RespectsAdditionalConstraints) { @@ -297,7 +258,7 @@ TEST_F(SolverTest, RespectsAdditionalConstraints) { auto NotY = neg(Y); // (X <=> Y) ^ X ^ !Y - expectUnsatisfiable(solve({XEqY, X, NotY})); + EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable); } TEST_F(SolverTest, ImplicationConflict) { @@ -307,7 +268,7 @@ TEST_F(SolverTest, ImplicationConflict) { auto *XAndNotY = conj(X, neg(Y)); // X => Y ^ X ^ !Y - expectUnsatisfiable(solve({XImplY, XAndNotY})); + EXPECT_EQ(solve({XImplY, XAndNotY}), Solver::Result::Unsatisfiable); } } // namespace _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits