maxjhandsome
/
llvm-project
forked from OSchip/llvm-project
1
0
Fork 0
Code Issues Pull Requests Packages Releases Wiki Activity

Revert "[clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`." 

This reverts commit 19e21887eb. I
accidentally landed the non-final version of the patch that used
decomposition declarations (not yet usable in LLVM/Clang source).
This commit is contained in:
Dmitri Gribenko 2022-07-07 21:37:26 +02:00
parent 65cac0ed92
commit 63fac424e6
4 changed files with 50 additions and 171 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
View File

@ -271,18 +271,17 @@ private:
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

62
clang/include/clang/Analysis/FlowSensitive/Solver.h
View File

@ -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 @@ public:
/// 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;
};

65
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
View File

@ -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 @@ public:
// 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 @@ public:
++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 @@ private:
}
}
/// 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 @@ private:
};
Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) {
return Vals.empty() ? Solver::Result::Satisfiable({{}})
return Vals.empty() ? WatchedLiteralsSolver::Result::Satisfiable
: WatchedLiteralsSolverImpl(Vals).solve();
}

81
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
View File

@ -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 @@ protected:
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