diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h new file mode 100644 --- /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 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 --- /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 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 --- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt +++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt @@ -3,6 +3,7 @@ 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 --- /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 +#include +#include +#include +#include + +#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 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 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 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 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 clauseLiterals(ClauseID C) const { + return llvm::ArrayRef(&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 &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 SubValsToVar; + Variable NextVar = 1; + { + std::queue 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(Val)) { + UnprocessedSubVals.push(&C->getLeftSubValue()); + UnprocessedSubVals.push(&C->getRightSubValue()); + } else if (auto *D = dyn_cast(Val)) { + UnprocessedSubVals.push(&D->getLeftSubValue()); + UnprocessedSubVals.push(&D->getRightSubValue()); + } else if (auto *N = dyn_cast(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 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 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(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(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(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 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 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 VarAssignments; + + /// A set of unassigned variables that appear in watched literals in + /// `Formula`. The vector is guaranteed to contain unique elements. + std::vector ActiveVars; + +public: + explicit WatchedLiteralsSolverImpl(const llvm::DenseSet &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 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 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(VarAssignments[var(Lit)]) == + static_cast(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 watchedLiterals() const { + llvm::DenseSet 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 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 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 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 --- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt +++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt @@ -11,6 +11,7 @@ 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 --- /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 +#include +#include + +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 Vals) { + return WatchedLiteralsSolver().solve(std::move(Vals)); + } + + // Creates an atomic boolean value. + BoolValue *atom() { + Vals.push_back(std::make_unique()); + return Vals.back().get(); + } + + // Creates a boolean conjunction value. + BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) { + Vals.push_back( + std::make_unique(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); + } + + // Creates a boolean disjunction value. + BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) { + Vals.push_back( + std::make_unique(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); + } + + // Creates a boolean negation value. + BoolValue *neg(BoolValue *SubVal) { + Vals.push_back(std::make_unique(*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> 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