[clang] 53dcd9e - [clang][dataflow] Add SAT solver interface and implementation
Stanislav Gatev via cfe-commits
cfe-commits at lists.llvm.org
Fri Feb 25 06:48:28 PST 2022
Author: Stanislav Gatev
Date: 2022-02-25T14:46:52Z
New Revision: 53dcd9efd16fc881b01470767ac17c4b221f3e08
URL: https://github.com/llvm/llvm-project/commit/53dcd9efd16fc881b01470767ac17c4b221f3e08
DIFF: https://github.com/llvm/llvm-project/commit/53dcd9efd16fc881b01470767ac17c4b221f3e08.diff
LOG: [clang][dataflow] Add SAT solver interface and implementation
This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-dev.
Reviewed-by: ymandel, xazax.hun
Differential Revision: https://reviews.llvm.org/D120289
Added:
clang/include/clang/Analysis/FlowSensitive/Solver.h
clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
Modified:
clang/lib/Analysis/FlowSensitive/CMakeLists.txt
clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h
new file mode 100644
index 0000000000000..6b685b9b3c9a7
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h
@@ -0,0 +1,56 @@
+//===- Solver.h -------------------------------------------------*- C++ -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines an interface for a SAT solver that can be used by
+// dataflow analyses.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
+
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang {
+namespace dataflow {
+
+/// 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
+ /// 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,
+ };
+
+ virtual ~Solver() = default;
+
+ /// Checks if the conjunction of `Vals` is satisfiable and returns the
+ /// corresponding result.
+ ///
+ /// 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;
+};
+
+} // namespace dataflow
+} // namespace clang
+
+#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
new file mode 100644
index 0000000000000..702da97349da9
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -0,0 +1,37 @@
+//===- WatchedLiteralsSolver.h ----------------------------------*- C++ -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a SAT solver implementation that can be used by dataflow
+// analyses.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
+
+#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseSet.h"
+
+namespace clang {
+namespace dataflow {
+
+/// A SAT solver that is an implementation of Algorithm D from Knuth's The Art
+/// of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is based on
+/// the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, keeps references to a
+/// single "watched" literal per clause, and uses a set of "active" variables
+/// for unit propagation.
+class WatchedLiteralsSolver : public Solver {
+public:
+ Result solve(llvm::DenseSet<BoolValue *> Vals) override;
+};
+
+} // namespace dataflow
+} // namespace clang
+
+#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index 6ac9b97d7e989..d6a544ab154f0 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,6 +3,7 @@ add_clang_library(clangAnalysisFlowSensitive
DataflowEnvironment.cpp
Transfer.cpp
TypeErasedDataflowAnalysis.cpp
+ WatchedLiteralsSolver.cpp
LINK_LIBS
clangAnalysis
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
new file mode 100644
index 0000000000000..0e6e70d6d5d47
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -0,0 +1,600 @@
+//===- WatchedLiteralsSolver.cpp --------------------------------*- C++ -*-===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a SAT solver implementation that can be used by dataflow
+// analyses.
+//
+//===----------------------------------------------------------------------===//
+
+#include <cassert>
+#include <cstdint>
+#include <iterator>
+#include <queue>
+#include <vector>
+
+#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseSet.h"
+#include "llvm/ADT/STLExtras.h"
+
+namespace clang {
+namespace dataflow {
+
+// `WatchedLiteralsSolver` is an implementation of Algorithm D from Knuth's
+// The Art of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is
+// based on the backtracking DPLL algorithm [1], keeps references to a single
+// "watched" literal per clause, and uses a set of "active" variables to perform
+// unit propagation.
+//
+// The solver expects that its input is a boolean formula in conjunctive normal
+// form that consists of clauses of at least one literal. A literal is either a
+// boolean variable or its negation. Below we define types, data structures, and
+// utilities that are used to represent boolean formulas in conjunctive normal
+// form.
+//
+// [1] https://en.wikipedia.org/wiki/DPLL_algorithm
+
+/// Boolean variables are represented as positive integers.
+using Variable = uint32_t;
+
+/// A null boolean variable is used as a placeholder in various data structures
+/// and algorithms.
+static constexpr Variable NullVar = 0;
+
+/// Literals are represented as positive integers. Specifically, for a boolean
+/// variable `V` that is represented as the positive integer `I`, the positive
+/// literal `V` is represented as the integer `2*I` and the negative literal
+/// `!V` is represented as the integer `2*I+1`.
+using Literal = uint32_t;
+
+/// A null literal is used as a placeholder in various data structures and
+/// algorithms.
+static constexpr Literal NullLit = 0;
+
+/// Returns the positive literal `V`.
+static constexpr Literal posLit(Variable V) { return 2 * V; }
+
+/// Returns the negative literal `!V`.
+static constexpr Literal negLit(Variable V) { return 2 * V + 1; }
+
+/// Returns the negated literal `!L`.
+static constexpr Literal notLit(Literal L) { return L ^ 1; }
+
+/// Returns the variable of `L`.
+static constexpr Variable var(Literal L) { return L >> 1; }
+
+/// Clause identifiers are represented as positive integers.
+using ClauseID = uint32_t;
+
+/// A null clause identifier is used as a placeholder in various data structures
+/// and algorithms.
+static constexpr ClauseID NullClause = 0;
+
+/// A boolean formula in conjunctive normal form.
+struct BooleanFormula {
+ /// `LargestVar` is equal to the largest positive integer that represents a
+ /// variable in the formula.
+ const Variable LargestVar;
+
+ /// Literals of all clauses in the formula.
+ ///
+ /// The element at index 0 stands for the literal in the null clause. It is
+ /// set to 0 and isn't used. Literals of clauses in the formula start from the
+ /// element at index 1.
+ ///
+ /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of
+ /// `Clauses` will be `[0, L1, L2, L2, L3, L4]`.
+ std::vector<Literal> Clauses;
+
+ /// Start indices of clauses of the formula in `Clauses`.
+ ///
+ /// The element at index 0 stands for the start index of the null clause. It
+ /// is set to 0 and isn't used. Start indices of clauses in the formula start
+ /// from the element at index 1.
+ ///
+ /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of
+ /// `ClauseStarts` will be `[0, 1, 3]`. Note that the literals of the first
+ /// clause always start at index 1. The start index for the literals of the
+ /// second clause depends on the size of the first clause and so on.
+ std::vector<size_t> ClauseStarts;
+
+ /// Maps literals (indices of the vector) to clause identifiers (elements of
+ /// the vector) that watch the respective literals.
+ ///
+ /// For a given clause, its watched literal is always its first literal in
+ /// `Clauses`. This invariant is maintained when watched literals change.
+ std::vector<ClauseID> WatchedHead;
+
+ /// Maps clause identifiers (elements of the vector) to identifiers of other
+ /// clauses that watch the same literals, forming a set of linked lists.
+ ///
+ /// The element at index 0 stands for the identifier of the clause that
+ /// follows the null clause. It is set to 0 and isn't used. Identifiers of
+ /// clauses in the formula start from the element at index 1.
+ std::vector<ClauseID> NextWatched;
+
+ explicit BooleanFormula(Variable LargestVar) : LargestVar(LargestVar) {
+ Clauses.push_back(0);
+ ClauseStarts.push_back(0);
+ NextWatched.push_back(0);
+ const size_t NumLiterals = 2 * LargestVar + 1;
+ WatchedHead.resize(NumLiterals + 1, 0);
+ }
+
+ /// Adds the `L1 v L2 v L3` clause to the formula. If `L2` or `L3` are
+ /// `NullLit` they are respectively omitted from the clause.
+ ///
+ /// Requirements:
+ ///
+ /// `L1` must not be `NullLit`.
+ ///
+ /// All literals in the input that are not `NullLit` must be distinct.
+ void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) {
+ // The literals are guaranteed to be distinct from properties of BoolValue
+ // and the construction in `buildBooleanFormula`.
+ assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
+ (L2 != L3 || L2 == NullLit));
+
+ const ClauseID C = ClauseStarts.size();
+ const size_t S = Clauses.size();
+ ClauseStarts.push_back(S);
+
+ Clauses.push_back(L1);
+ if (L2 != NullLit)
+ Clauses.push_back(L2);
+ if (L3 != NullLit)
+ Clauses.push_back(L3);
+
+ // Designate the first literal as the "watched" literal of the clause.
+ NextWatched.push_back(WatchedHead[L1]);
+ WatchedHead[L1] = C;
+ }
+
+ /// Returns the number of literals in clause `C`.
+ size_t clauseSize(ClauseID C) const {
+ return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]
+ : ClauseStarts[C + 1] - ClauseStarts[C];
+ }
+
+ /// Returns the literals of clause `C`.
+ llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const {
+ return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C));
+ }
+};
+
+/// Converts the conjunction of `Vals` into a formula in conjunctive normal
+/// form where each clause has at least one and at most three literals.
+BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
+ // The general strategy of the algorithm implemented below is to map each
+ // of the sub-values in `Vals` to a unique variable and use these variables in
+ // the resulting CNF expression to avoid exponential blow up. The number of
+ // literals in the resulting formula is guaranteed to be linear in the number
+ // of sub-values in `Vals`.
+
+ // Map each sub-value in `Vals` to a unique variable.
+ llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
+ Variable NextVar = 1;
+ {
+ std::queue<BoolValue *> UnprocessedSubVals;
+ for (BoolValue *Val : Vals)
+ UnprocessedSubVals.push(Val);
+ while (!UnprocessedSubVals.empty()) {
+ BoolValue *Val = UnprocessedSubVals.front();
+ UnprocessedSubVals.pop();
+
+ if (!SubValsToVar.try_emplace(Val, NextVar).second)
+ continue;
+ ++NextVar;
+
+ // Visit the sub-values of `Val`.
+ if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+ UnprocessedSubVals.push(&C->getLeftSubValue());
+ UnprocessedSubVals.push(&C->getRightSubValue());
+ } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
+ UnprocessedSubVals.push(&D->getLeftSubValue());
+ UnprocessedSubVals.push(&D->getRightSubValue());
+ } else if (auto *N = dyn_cast<NegationValue>(Val)) {
+ UnprocessedSubVals.push(&N->getSubVal());
+ }
+ }
+ }
+
+ auto GetVar = [&SubValsToVar](const BoolValue *Val) {
+ auto ValIt = SubValsToVar.find(Val);
+ assert(ValIt != SubValsToVar.end());
+ return ValIt->second;
+ };
+
+ BooleanFormula Formula(NextVar - 1);
+ std::vector<bool> ProcessedSubVals(NextVar, false);
+
+ // Add a conjunct for each variable that represents a top-level conjunction
+ // value in `Vals`.
+ for (BoolValue *Val : Vals)
+ Formula.addClause(posLit(GetVar(Val)));
+
+ // Add conjuncts that represent the mapping between newly-created variables
+ // and their corresponding sub-values.
+ std::queue<BoolValue *> UnprocessedSubVals;
+ for (BoolValue *Val : Vals)
+ UnprocessedSubVals.push(Val);
+ while (!UnprocessedSubVals.empty()) {
+ const BoolValue *Val = UnprocessedSubVals.front();
+ UnprocessedSubVals.pop();
+ const Variable Var = GetVar(Val);
+
+ if (ProcessedSubVals[Var])
+ continue;
+ ProcessedSubVals[Var] = true;
+
+ if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+ const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
+ const Variable RightSubVar = GetVar(&C->getRightSubValue());
+
+ // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
+ // which is already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ Formula.addClause(negLit(Var), posLit(LeftSubVar));
+ Formula.addClause(negLit(Var), posLit(RightSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+
+ // Visit the sub-values of `Val`.
+ UnprocessedSubVals.push(&C->getLeftSubValue());
+ UnprocessedSubVals.push(&C->getRightSubValue());
+ } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
+ const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
+ const Variable RightSubVar = GetVar(&D->getRightSubValue());
+
+ // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
+ // which is already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar));
+ Formula.addClause(posLit(Var), negLit(RightSubVar));
+
+ // Visit the sub-values of `Val`.
+ UnprocessedSubVals.push(&D->getLeftSubValue());
+ UnprocessedSubVals.push(&D->getRightSubValue());
+ } else if (auto *N = dyn_cast<NegationValue>(Val)) {
+ const Variable SubVar = GetVar(&N->getSubVal());
+
+ // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in
+ // conjunctive normal form. Below we add each of the conjuncts of the
+ // latter expression to the result.
+ Formula.addClause(negLit(Var), negLit(SubVar));
+ Formula.addClause(posLit(Var), posLit(SubVar));
+
+ // Visit the sub-values of `Val`.
+ UnprocessedSubVals.push(&N->getSubVal());
+ }
+ }
+
+ return Formula;
+}
+
+class WatchedLiteralsSolverImpl {
+ /// A boolean formula in conjunctive normal form that the solver will attempt
+ /// to prove satisfiable. The formula will be modified in the process.
+ BooleanFormula Formula;
+
+ /// The search for a satisfying assignment of the variables in `Formula` will
+ /// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
+ /// (inclusive). The current level is stored in `Level`. At each level the
+ /// solver will assign a value to an unassigned variable. If this leads to a
+ /// consistent partial assignment, `Level` will be incremented. Otherwise, if
+ /// it results in a conflict, the solver will backtrack by decrementing
+ /// `Level` until it reaches the most recent level where a decision was made.
+ size_t Level = 0;
+
+ /// Maps levels (indices of the vector) to variables (elements of the vector)
+ /// that are assigned values at the respective levels.
+ ///
+ /// The element at index 0 isn't used. Variables start from the element at
+ /// index 1.
+ std::vector<Variable> LevelVars;
+
+ /// State of the solver at a particular level.
+ enum class State : uint8_t {
+ /// Indicates that the solver made a decision.
+ Decision = 0,
+
+ /// Indicates that the solver made a forced move.
+ Forced = 1,
+ };
+
+ /// State of the solver at a particular level. It keeps track of previous
+ /// decisions that the solver can refer to when backtracking.
+ ///
+ /// The element at index 0 isn't used. States start from the element at index
+ /// 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).
+ ///
+ /// The element at index 0 isn't used. Variable assignments start from the
+ /// element at index 1.
+ std::vector<Assignment> VarAssignments;
+
+ /// A set of unassigned variables that appear in watched literals in
+ /// `Formula`. The vector is guaranteed to contain unique elements.
+ std::vector<Variable> ActiveVars;
+
+public:
+ explicit WatchedLiteralsSolverImpl(const llvm::DenseSet<BoolValue *> &Vals)
+ : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
+ LevelStates(Formula.LargestVar + 1) {
+ assert(!Vals.empty());
+
+ // Initialize the state at the root level to a decision so that in
+ // `reverseForcedMoves` we don't have to check that `Level >= 0` on each
+ // iteration.
+ LevelStates[0] = State::Decision;
+
+ // Initialize all variables as unassigned.
+ VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
+
+ // Initialize the active variables.
+ for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
+ if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
+ ActiveVars.push_back(Var);
+ }
+ }
+
+ Solver::Result solve() && {
+ size_t I = 0;
+ while (I < ActiveVars.size()) {
+ // Assert that the following invariants hold:
+ // 1. All active variables are unassigned.
+ // 2. All active variables form watched literals.
+ // 3. Unassigned variables that form watched literals are active.
+ // FIXME: Consider replacing these with test cases that fail if the any
+ // of the invariants is broken. That might not be easy due to the
+ // transformations performed by `buildBooleanFormula`.
+ assert(activeVarsAreUnassigned());
+ assert(activeVarsFormWatchedLiterals());
+ assert(unassignedVarsFormingWatchedLiteralsAreActive());
+
+ const Variable ActiveVar = ActiveVars[I];
+
+ // Look for unit clauses that contain the active variable.
+ const bool unitPosLit = watchedByUnitClause(posLit(ActiveVar));
+ const bool unitNegLit = watchedByUnitClause(negLit(ActiveVar));
+ if (unitPosLit && unitNegLit) {
+ // We found a conflict!
+
+ // Backtrack and rewind the `Level` until the most recent non-forced
+ // assignment.
+ reverseForcedMoves();
+
+ // If the root level is reached, then all possible assignments lead to
+ // a conflict.
+ if (Level == 0)
+ return WatchedLiteralsSolver::Result::Unsatisfiable;
+
+ // Otherwise, take the other branch at the most recent level where a
+ // decision was made.
+ LevelStates[Level] = State::Forced;
+ const Variable Var = LevelVars[Level];
+ VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
+ ? Assignment::AssignedFalse
+ : Assignment::AssignedTrue;
+
+ updateWatchedLiterals();
+ } else if (unitPosLit || unitNegLit) {
+ // We found a unit clause! The value of its unassigned variable is
+ // forced.
+ ++Level;
+
+ LevelVars[Level] = ActiveVar;
+ LevelStates[Level] = State::Forced;
+ VarAssignments[ActiveVar] =
+ unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse;
+
+ // Remove the variable that was just assigned from the set of active
+ // variables.
+ if (I + 1 < ActiveVars.size()) {
+ // Replace the variable that was just assigned with the last active
+ // variable for efficient removal.
+ ActiveVars[I] = ActiveVars.back();
+ } else {
+ // This was the last active variable. Repeat the process from the
+ // beginning.
+ I = 0;
+ }
+ ActiveVars.pop_back();
+
+ updateWatchedLiterals();
+ } else if (I + 1 == ActiveVars.size()) {
+ // There are no remaining unit clauses in the formula! Make a decision
+ // for one of the active variables at the current level.
+ ++Level;
+
+ LevelVars[Level] = ActiveVar;
+ LevelStates[Level] = State::Decision;
+ VarAssignments[ActiveVar] = decideAssignment(ActiveVar);
+
+ // Remove the variable that was just assigned from the set of active
+ // variables.
+ ActiveVars.pop_back();
+
+ updateWatchedLiterals();
+
+ // This was the last active variable. Repeat the process from the
+ // beginning.
+ I = 0;
+ } else {
+ ++I;
+ }
+ }
+ return WatchedLiteralsSolver::Result::Satisfiable;
+ }
+
+private:
+ // 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];
+
+ VarAssignments[Var] = Assignment::Unassigned;
+
+ // If the variable that we pass through is watched then we add it to the
+ // active variables.
+ if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
+ ActiveVars.push_back(Var);
+ }
+ }
+
+ // Updates watched literals that are affected by a variable assignment.
+ void updateWatchedLiterals() {
+ const Variable Var = LevelVars[Level];
+
+ // Update the watched literals of clauses that currently watch the literal
+ // that falsifies `Var`.
+ const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
+ ? negLit(Var)
+ : posLit(Var);
+ ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
+ Formula.WatchedHead[FalseLit] = NullClause;
+ while (FalseLitWatcher != NullClause) {
+ const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
+
+ // Pick the first non-false literal as the new watched literal.
+ const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
+ size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
+ while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
+ ++NewWatchedLitIdx;
+ const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];
+ const Variable NewWatchedLitVar = var(NewWatchedLit);
+
+ // Swap the old watched literal for the new one in `FalseLitWatcher` to
+ // maintain the invariant that the watched literal is at the beginning of
+ // the clause.
+ Formula.Clauses[NewWatchedLitIdx] = FalseLit;
+ Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+
+ // If the new watched literal isn't watched by any other clause and its
+ // variable isn't assigned we need to add it to the active variables.
+ if (!isWatched(NewWatchedLit) && !isWatched(notLit(NewWatchedLit)) &&
+ VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
+ ActiveVars.push_back(NewWatchedLitVar);
+
+ Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
+ Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+
+ // Go to the next clause that watches `FalseLit`.
+ FalseLitWatcher = NextFalseLitWatcher;
+ }
+ }
+
+ /// Returns true if and only if one of the clauses that watch `Lit` is a unit
+ /// clause.
+ bool watchedByUnitClause(Literal Lit) const {
+ for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
+ LitWatcher != NullClause;
+ LitWatcher = Formula.NextWatched[LitWatcher]) {
+ llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);
+
+ // Assert the invariant that the watched literal is always the first one
+ // in the clause.
+ // FIXME: Consider replacing this with a test case that fails if the
+ // invariant is broken by `updateWatchedLiterals`. That might not be easy
+ // due to the transformations performed by `buildBooleanFormula`.
+ assert(Clause.front() == Lit);
+
+ if (isUnit(Clause))
+ return true;
+ }
+ return false;
+ }
+
+ /// Returns true if and only if `Clause` is a unit clause.
+ bool isUnit(llvm::ArrayRef<Literal> Clause) const {
+ return llvm::all_of(Clause.drop_front(),
+ [this](Literal L) { return isCurrentlyFalse(L); });
+ }
+
+ /// Returns true if and only if `Lit` evaluates to `false` in the current
+ /// partial assignment.
+ bool isCurrentlyFalse(Literal Lit) const {
+ return static_cast<int8_t>(VarAssignments[var(Lit)]) ==
+ static_cast<int8_t>(Lit & 1);
+ }
+
+ /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
+ bool isWatched(Literal Lit) const {
+ return Formula.WatchedHead[Lit] != NullClause;
+ }
+
+ /// Returns an assignment for an unassigned variable.
+ Assignment decideAssignment(Variable Var) const {
+ return !isWatched(posLit(Var)) || isWatched(negLit(Var))
+ ? Assignment::AssignedFalse
+ : Assignment::AssignedTrue;
+ }
+
+ /// Returns a set of all watched literals.
+ llvm::DenseSet<Literal> watchedLiterals() const {
+ llvm::DenseSet<Literal> WatchedLiterals;
+ for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
+ if (Formula.WatchedHead[Lit] == NullClause)
+ continue;
+ WatchedLiterals.insert(Lit);
+ }
+ return WatchedLiterals;
+ }
+
+ /// Returns true if and only if all active variables are unassigned.
+ bool activeVarsAreUnassigned() const {
+ return llvm::all_of(ActiveVars, [this](Variable Var) {
+ return VarAssignments[Var] == Assignment::Unassigned;
+ });
+ }
+
+ /// Returns true if and only if all active variables form watched literals.
+ bool activeVarsFormWatchedLiterals() const {
+ const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals();
+ return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {
+ return WatchedLiterals.contains(posLit(Var)) ||
+ WatchedLiterals.contains(negLit(Var));
+ });
+ }
+
+ /// Returns true if and only if all unassigned variables that are forming
+ /// watched literals are active.
+ bool unassignedVarsFormingWatchedLiteralsAreActive() const {
+ const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(),
+ ActiveVars.end());
+ for (Literal Lit : watchedLiterals()) {
+ const Variable Var = var(Lit);
+ if (VarAssignments[Var] != Assignment::Unassigned)
+ continue;
+ if (ActiveVarsSet.contains(Var))
+ continue;
+ return false;
+ }
+ return true;
+ }
+};
+
+Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) {
+ return Vals.empty() ? WatchedLiteralsSolver::Result::Satisfiable
+ : WatchedLiteralsSolverImpl(Vals).solve();
+}
+
+} // namespace dataflow
+} // namespace clang
diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
index 414f5c8810c78..81bab391cb1bd 100644
--- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -11,6 +11,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
TestingSupportTest.cpp
TransferTest.cpp
TypeErasedDataflowAnalysisTest.cpp
+ SolverTest.cpp
)
clang_target_link_libraries(ClangAnalysisFlowSensitiveTests
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
new file mode 100644
index 0000000000000..c5116b9edbe05
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -0,0 +1,274 @@
+//===- 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 "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>
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+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));
+ }
+
+private:
+ std::vector<std::unique_ptr<BoolValue>> Vals;
+};
+
+TEST_F(SolverTest, Var) {
+ auto X = atom();
+
+ // X
+ EXPECT_EQ(solve({X}), Solver::Result::Satisfiable);
+}
+
+TEST_F(SolverTest, NegatedVar) {
+ auto X = atom();
+ auto NotX = neg(X);
+
+ // !X
+ EXPECT_EQ(solve({NotX}), Solver::Result::Satisfiable);
+}
+
+TEST_F(SolverTest, UnitConflict) {
+ auto X = atom();
+ auto NotX = neg(X);
+
+ // X ^ !X
+ EXPECT_EQ(solve({X, NotX}), Solver::Result::Unsatisfiable);
+}
+
+TEST_F(SolverTest, DistinctVars) {
+ auto X = atom();
+ auto Y = atom();
+ auto NotY = neg(Y);
+
+ // X ^ !Y
+ EXPECT_EQ(solve({X, NotY}), Solver::Result::Satisfiable);
+}
+
+TEST_F(SolverTest, DoubleNegation) {
+ auto X = atom();
+ auto NotX = neg(X);
+ auto NotNotX = neg(NotX);
+
+ // !!X ^ !X
+ EXPECT_EQ(solve({NotNotX, NotX}), Solver::Result::Unsatisfiable);
+}
+
+TEST_F(SolverTest, NegatedDisjunction) {
+ auto X = atom();
+ auto Y = atom();
+ auto XOrY = disj(X, Y);
+ auto NotXOrY = neg(XOrY);
+
+ // !(X v Y) ^ (X v Y)
+ EXPECT_EQ(solve({NotXOrY, XOrY}), Solver::Result::Unsatisfiable);
+}
+
+TEST_F(SolverTest, NegatedConjunction) {
+ auto X = atom();
+ auto Y = atom();
+ auto XAndY = conj(X, Y);
+ auto NotXAndY = neg(XAndY);
+
+ // !(X ^ Y) ^ (X ^ Y)
+ EXPECT_EQ(solve({NotXAndY, XAndY}), Solver::Result::Unsatisfiable);
+}
+
+TEST_F(SolverTest, DisjunctionSameVars) {
+ auto X = atom();
+ auto NotX = neg(X);
+ auto XOrNotX = disj(X, NotX);
+
+ // X v !X
+ EXPECT_EQ(solve({XOrNotX}), Solver::Result::Satisfiable);
+}
+
+TEST_F(SolverTest, ConjunctionSameVarsConflict) {
+ auto X = atom();
+ auto NotX = neg(X);
+ auto XAndNotX = conj(X, NotX);
+
+ // X ^ !X
+ EXPECT_EQ(solve({XAndNotX}), Solver::Result::Unsatisfiable);
+}
+
+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);
+
+ // (!X v Y) ^ (!X v !Y)
+ EXPECT_EQ(solve({NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable);
+}
+
+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);
+
+ // (X v Y) ^ (!X v Y) ^ (!X v !Y)
+ EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable);
+}
+
+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);
+
+ // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
+ EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}),
+ Solver::Result::Unsatisfiable);
+}
+
+TEST_F(SolverTest, IffSameVars) {
+ auto X = atom();
+ auto XEqX = iff(X, X);
+
+ // X <=> X
+ EXPECT_EQ(solve({XEqX}), Solver::Result::Satisfiable);
+}
+
+TEST_F(SolverTest, IffDistinctVars) {
+ auto X = atom();
+ auto Y = atom();
+ auto XEqY = iff(X, Y);
+
+ // X <=> Y
+ EXPECT_EQ(solve({XEqY}), Solver::Result::Satisfiable);
+}
+
+TEST_F(SolverTest, IffWithUnits) {
+ auto X = atom();
+ auto Y = atom();
+ auto XEqY = iff(X, Y);
+
+ // (X <=> Y) ^ X ^ Y
+ EXPECT_EQ(solve({XEqY, X, Y}), Solver::Result::Satisfiable);
+}
+
+TEST_F(SolverTest, IffWithUnitsConflict) {
+ auto X = atom();
+ auto Y = atom();
+ auto XEqY = iff(X, Y);
+ auto NotY = neg(Y);
+
+ // (X <=> Y) ^ X !Y
+ EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable);
+}
+
+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);
+
+ // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
+ EXPECT_EQ(solve({XEqY, YEqZ, Z, NotX}), Solver::Result::Unsatisfiable);
+}
+
+TEST_F(SolverTest, DeMorgan) {
+ auto X = atom();
+ auto Y = atom();
+ auto Z = atom();
+ auto W = atom();
+
+ // !(X v Y) <=> !X ^ !Y
+ auto A = iff(neg(disj(X, Y)), conj(neg(X), neg(Y)));
+
+ // !(Z ^ W) <=> !Z v !W
+ auto B = iff(neg(conj(Z, W)), disj(neg(Z), neg(W)));
+
+ // A ^ B
+ EXPECT_EQ(solve({A, B}), Solver::Result::Satisfiable);
+}
+
+TEST_F(SolverTest, RespectsAdditionalConstraints) {
+ auto X = atom();
+ auto Y = atom();
+ auto XEqY = iff(X, Y);
+ auto NotY = neg(Y);
+
+ // (X <=> Y) ^ X ^ !Y
+ EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable);
+}
+
+TEST_F(SolverTest, ImplicationConflict) {
+ auto X = atom();
+ auto Y = atom();
+ auto *XImplY = impl(X, Y);
+ auto *XAndNotY = conj(X, neg(Y));
+
+ // X => Y ^ X ^ !Y
+ EXPECT_EQ(solve({XImplY, XAndNotY}), Solver::Result::Unsatisfiable);
+}
+
+} // namespace
More information about the cfe-commits
mailing list