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
