wyt created this revision. Herald added subscribers: martong, tschuett, xazax.hun. Herald added a reviewer: NoQ. Herald added a project: All. wyt requested review of this revision. Herald added a project: clang. Herald added a subscriber: cfe-commits.
Repository: rG LLVM Github Monorepo https://reviews.llvm.org/D129180 Files: 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
Index: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp =================================================================== --- clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -20,6 +20,12 @@ 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 @@ -64,6 +70,17 @@ 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; }; @@ -72,7 +89,9 @@ auto X = atom(); // X - EXPECT_EQ(solve({X}), Solver::Result::Satisfiable); + expectSatisfiable( + solve({X}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue))); } TEST_F(SolverTest, NegatedVar) { @@ -80,7 +99,9 @@ auto NotX = neg(X); // !X - EXPECT_EQ(solve({NotX}), Solver::Result::Satisfiable); + expectSatisfiable( + solve({NotX}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse))); } TEST_F(SolverTest, UnitConflict) { @@ -88,7 +109,7 @@ auto NotX = neg(X); // X ^ !X - EXPECT_EQ(solve({X, NotX}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({X, NotX})); } TEST_F(SolverTest, DistinctVars) { @@ -97,7 +118,10 @@ auto NotY = neg(Y); // X ^ !Y - EXPECT_EQ(solve({X, NotY}), Solver::Result::Satisfiable); + expectSatisfiable( + solve({X, NotY}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue), + Pair(Y, Solver::Result::Assignment::AssignedFalse))); } TEST_F(SolverTest, DoubleNegation) { @@ -106,7 +130,7 @@ auto NotNotX = neg(NotX); // !!X ^ !X - EXPECT_EQ(solve({NotNotX, NotX}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({NotNotX, NotX})); } TEST_F(SolverTest, NegatedDisjunction) { @@ -116,7 +140,7 @@ auto NotXOrY = neg(XOrY); // !(X v Y) ^ (X v Y) - EXPECT_EQ(solve({NotXOrY, XOrY}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({NotXOrY, XOrY})); } TEST_F(SolverTest, NegatedConjunction) { @@ -126,7 +150,7 @@ auto NotXAndY = neg(XAndY); // !(X ^ Y) ^ (X ^ Y) - EXPECT_EQ(solve({NotXAndY, XAndY}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({NotXAndY, XAndY})); } TEST_F(SolverTest, DisjunctionSameVars) { @@ -135,7 +159,7 @@ auto XOrNotX = disj(X, NotX); // X v !X - EXPECT_EQ(solve({XOrNotX}), Solver::Result::Satisfiable); + expectSatisfiable(solve({XOrNotX}), _); } TEST_F(SolverTest, ConjunctionSameVarsConflict) { @@ -144,7 +168,7 @@ auto XAndNotX = conj(X, NotX); // X ^ !X - EXPECT_EQ(solve({XAndNotX}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({XAndNotX})); } TEST_F(SolverTest, PureVar) { @@ -156,7 +180,10 @@ auto NotXOrNotY = disj(NotX, NotY); // (!X v Y) ^ (!X v !Y) - EXPECT_EQ(solve({NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable); + expectSatisfiable( + solve({NotXOrY, NotXOrNotY}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse), + Pair(Y, _))); } TEST_F(SolverTest, MustAssumeVarIsFalse) { @@ -169,7 +196,10 @@ auto NotXOrNotY = disj(NotX, NotY); // (X v Y) ^ (!X v Y) ^ (!X v !Y) - EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable); + expectSatisfiable( + solve({XOrY, NotXOrY, NotXOrNotY}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse), + Pair(Y, Solver::Result::Assignment::AssignedTrue))); } TEST_F(SolverTest, DeepConflict) { @@ -183,8 +213,7 @@ auto XOrNotY = disj(X, NotY); // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y) - EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), - Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY})); } TEST_F(SolverTest, IffSameVars) { @@ -192,7 +221,7 @@ auto XEqX = iff(X, X); // X <=> X - EXPECT_EQ(solve({XEqX}), Solver::Result::Satisfiable); + expectSatisfiable(solve({XEqX}), _); } TEST_F(SolverTest, IffDistinctVars) { @@ -201,7 +230,14 @@ auto XEqY = iff(X, Y); // X <=> Y - EXPECT_EQ(solve({XEqY}), Solver::Result::Satisfiable); + 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) { @@ -210,7 +246,10 @@ auto XEqY = iff(X, Y); // (X <=> Y) ^ X ^ Y - EXPECT_EQ(solve({XEqY, X, Y}), Solver::Result::Satisfiable); + expectSatisfiable( + solve({XEqY, X, Y}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue), + Pair(Y, Solver::Result::Assignment::AssignedTrue))); } TEST_F(SolverTest, IffWithUnitsConflict) { @@ -220,7 +259,7 @@ auto NotY = neg(Y); // (X <=> Y) ^ X !Y - EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({XEqY, X, NotY})); } TEST_F(SolverTest, IffTransitiveConflict) { @@ -232,7 +271,7 @@ auto NotX = neg(X); // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X - EXPECT_EQ(solve({XEqY, YEqZ, Z, NotX}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX})); } TEST_F(SolverTest, DeMorgan) { @@ -248,7 +287,7 @@ auto B = iff(neg(conj(Z, W)), disj(neg(Z), neg(W))); // A ^ B - EXPECT_EQ(solve({A, B}), Solver::Result::Satisfiable); + expectSatisfiable(solve({A, B}), _); } TEST_F(SolverTest, RespectsAdditionalConstraints) { @@ -258,7 +297,7 @@ auto NotY = neg(Y); // (X <=> Y) ^ X ^ !Y - EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({XEqY, X, NotY})); } TEST_F(SolverTest, ImplicationConflict) { @@ -268,7 +307,7 @@ auto *XAndNotY = conj(X, neg(Y)); // X => Y ^ X ^ !Y - EXPECT_EQ(solve({XImplY, XAndNotY}), Solver::Result::Unsatisfiable); + expectUnsatisfiable(solve({XImplY, XAndNotY})); } } // namespace Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp =================================================================== --- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp +++ clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp @@ -44,6 +44,9 @@ /// Boolean variables are represented as positive integers. using Variable = uint32_t; +/// Boolean variables can be unassigned, assigned true or assigned false +using Assignment = Solver::Result::Assignment; + /// A null boolean variable is used as a placeholder in various data structures /// and algorithms. static constexpr Variable NullVar = 0; @@ -120,7 +123,13 @@ /// clauses in the formula start from the element at index 1. std::vector<ClauseID> NextWatched; - explicit BooleanFormula(Variable LargestVar) : LargestVar(LargestVar) { + /// 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)) { Clauses.push_back(0); ClauseStarts.push_back(0); NextWatched.push_back(0); @@ -180,6 +189,8 @@ // 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; @@ -194,14 +205,30 @@ ++NextVar; // Visit the sub-values of `Val`. - if (auto *C = dyn_cast<ConjunctionValue>(Val)) { + switch (Val->getKind()) { + case Value::Kind::Conjunction: { + auto *C = cast<ConjunctionValue>(Val); UnprocessedSubVals.push(&C->getLeftSubValue()); UnprocessedSubVals.push(&C->getRightSubValue()); - } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) { + break; + } + case Value::Kind::Disjunction: { + auto *D = cast<DisjunctionValue>(Val); UnprocessedSubVals.push(&D->getLeftSubValue()); UnprocessedSubVals.push(&D->getRightSubValue()); - } else if (auto *N = dyn_cast<NegationValue>(Val)) { + break; + } + case Value::Kind::Negation: { + auto *N = cast<NegationValue>(Val); UnprocessedSubVals.push(&N->getSubVal()); + break; + } + case Value::Kind::AtomicBool: { + Atomics[NextVar - 1] = cast<AtomicBoolValue>(Val); + break; + } + default: + llvm_unreachable("buildBooleanFormula: unhandled value kind"); } } } @@ -212,7 +239,7 @@ return ValIt->second; }; - BooleanFormula Formula(NextVar - 1); + BooleanFormula Formula(NextVar - 1, std::move(Atomics)); std::vector<bool> ProcessedSubVals(NextVar, false); // Add a conjunct for each variable that represents a top-level conjunction @@ -316,12 +343,6 @@ /// 1. std::vector<State> LevelStates; - enum class Assignment : int8_t { - Unassigned = -1, - AssignedFalse = 0, - AssignedTrue = 1 - }; - /// Maps variables (indices of the vector) to their assignments (elements of /// the vector). /// @@ -383,7 +404,7 @@ // If the root level is reached, then all possible assignments lead to // a conflict. if (Level == 0) - return WatchedLiteralsSolver::Result::Unsatisfiable; + return WatchedLiteralsSolver::Result::Unsatisfiable(); // Otherwise, take the other branch at the most recent level where a // decision was made. @@ -440,10 +461,19 @@ ++I; } } - return WatchedLiteralsSolver::Result::Satisfiable; + return WatchedLiteralsSolver::Result::Satisfiable(buildValAssignment()); } private: + // Returns the truth assignment to the atomic values in the boolean formula. + llvm::DenseMap<AtomicBoolValue *, Assignment> buildValAssignment() { + llvm::DenseMap<AtomicBoolValue *, Assignment> ValAssignments; + for (auto [Var, Val] : Formula.Atomics) { + ValAssignments[Val] = VarAssignments[Var]; + } + return ValAssignments; + } + // Reverses forced moves until the most recent level where a decision was made // on the assignment of a variable. void reverseForcedMoves() { @@ -592,7 +622,7 @@ }; Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) { - return Vals.empty() ? WatchedLiteralsSolver::Result::Satisfiable + return Vals.empty() ? Solver::Result::Satisfiable({{}}) : WatchedLiteralsSolverImpl(Vals).solve(); } Index: clang/include/clang/Analysis/FlowSensitive/Solver.h =================================================================== --- clang/include/clang/Analysis/FlowSensitive/Solver.h +++ clang/include/clang/Analysis/FlowSensitive/Solver.h @@ -16,6 +16,7 @@ #include "clang/Analysis/FlowSensitive/Value.h" #include "llvm/ADT/DenseSet.h" +#include <optional> namespace clang { namespace dataflow { @@ -23,17 +24,57 @@ /// An interface for a SAT solver that can be used by dataflow analyses. class Solver { public: - enum class Result { - /// Indicates that there exists a satisfying assignment for a boolean + 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 can be unset or be set to true or false when processing + /// a boolean formula. + enum class Assignment : int8_t { + Unassigned = -1, + AssignedFalse = 0, + AssignedTrue = 1 + }; + + static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); } + + static Result TimedOut() { return Result(Status::TimedOut, {}); } + + static Result + Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) { + return Result(Status::Satisfiable, std::move(Solution)); + } + + /// Returns the status of satisfiability checking on the queried boolean /// formula. - Satisfiable, + Status getStatus() const { return Status; } - /// Indicates that there is no satisfying assignment for a boolean formula. - Unsatisfiable, + /// Returns a truth assignment to boolean values that satisfies the queried + /// boolean formula if available. Otherwise, an empty optional is returned. + std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> + getSolution() const { + return Solution; + } - /// Indicates that the solver gave up trying to find a satisfying assignment - /// for a boolean formula. - TimedOut, + private: + Result( + enum Status Status, + std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution) + : Status(Status), Solution(std::move(Solution)) {} + + Status Status; + std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution; }; virtual ~Solver() = default; @@ -44,9 +85,6 @@ /// 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; }; Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h =================================================================== --- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -260,16 +260,18 @@ llvm::DenseSet<AtomicBoolValue *> &VisitedTokens); /// Returns the result of satisfiability checking on `Constraints`. - /// Possible return values are: - /// - `Satisfiable`: There exists a satisfying assignment for `Constraints`. + //// Possible return values are: + /// - `Satisfiable` : There exists a satisfying assignment for `Constraints`, + /// the solution found by the solver will be returned. /// - `Unsatisfiable`: There is no satisfying assignment for `Constraints`. - /// - `TimedOut`: The solver gives up on finding a satisfying assignment. + /// - `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)) == Solver::Result::Unsatisfiable; + return querySolver(std::move(Constraints)).getStatus() == + Solver::Result::Status::Unsatisfiable; } /// Returns a boolean value as a result of substituting `Val` and its sub
_______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits