[clang] 7a72ce9 - Revert "[dataflow] Add dedicated representation of boolean formulas"
Tom Weaver via cfe-commits
cfe-commits at lists.llvm.org
Tue Jul 4 06:07:19 PDT 2023
Author: Tom Weaver
Date: 2023-07-04T14:05:54+01:00
New Revision: 7a72ce98224be76d9328e65eee472381f7c8e7fe
URL: https://github.com/llvm/llvm-project/commit/7a72ce98224be76d9328e65eee472381f7c8e7fe
DIFF: https://github.com/llvm/llvm-project/commit/7a72ce98224be76d9328e65eee472381f7c8e7fe.diff
LOG: Revert "[dataflow] Add dedicated representation of boolean formulas"
This reverts commit 2fd614efc1bb9c27f1bc6c3096c60a7fe121e274.
Commit caused failures on the following two build bots:
http://45.33.8.238/win/80815/step_7.txt
https://lab.llvm.org/buildbot/#/builders/139/builds/44269
Added:
Modified:
clang/include/clang/Analysis/FlowSensitive/Arena.h
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
clang/include/clang/Analysis/FlowSensitive/Solver.h
clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
clang/lib/Analysis/FlowSensitive/Arena.cpp
clang/lib/Analysis/FlowSensitive/CMakeLists.txt
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
Removed:
clang/include/clang/Analysis/FlowSensitive/Formula.h
clang/lib/Analysis/FlowSensitive/Formula.cpp
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h
index b6c62e76246254..83b4ddeec02564 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -8,7 +8,6 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
-#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include <vector>
@@ -105,17 +104,7 @@ class Arena {
return create<AtomicBoolValue>();
}
- /// Gets the boolean formula equivalent of a BoolValue.
- /// Each unique Top values is translated to an Atom.
- /// TODO: migrate to storing Formula directly in Values instead.
- const Formula &getFormula(const BoolValue &);
-
- /// Returns a new atomic boolean variable, distinct from any other.
- Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
-
private:
- llvm::BumpPtrAllocator Alloc;
-
// Storage for the state of a program.
std::vector<std::unique_ptr<StorageLocation>> Locs;
std::vector<std::unique_ptr<Value>> Vals;
@@ -133,9 +122,6 @@ class Arena {
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
BiconditionalVals;
- llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
- unsigned NextAtom = 0;
-
AtomicBoolValue &TrueVal;
AtomicBoolValue &FalseVal;
};
diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
index 6b9f3681490af1..360786b02729f2 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
@@ -19,6 +19,7 @@
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringRef.h"
namespace clang {
@@ -27,9 +28,52 @@ namespace dataflow {
/// Returns a string representation of a value kind.
llvm::StringRef debugString(Value::Kind Kind);
+/// Returns a string representation of a boolean assignment to true or false.
+llvm::StringRef debugString(Solver::Result::Assignment Assignment);
+
/// Returns a string representation of the result status of a SAT check.
llvm::StringRef debugString(Solver::Result::Status Status);
+/// Returns a string representation for the boolean value `B`.
+///
+/// Atomic booleans appearing in the boolean value `B` are assigned to labels
+/// either specified in `AtomNames` or created by default rules as B0, B1, ...
+///
+/// Requirements:
+///
+/// Names assigned to atoms should not be repeated in `AtomNames`.
+std::string debugString(
+ const BoolValue &B,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+
+/// Returns a string representation for `Constraints` - a collection of boolean
+/// formulas.
+///
+/// Atomic booleans appearing in the boolean value `Constraints` are assigned to
+/// labels either specified in `AtomNames` or created by default rules as B0,
+/// B1, ...
+///
+/// Requirements:
+///
+/// Names assigned to atoms should not be repeated in `AtomNames`.
+std::string debugString(
+ const llvm::ArrayRef<BoolValue *> Constraints,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+
+/// Returns a string representation for `Constraints` - a collection of boolean
+/// formulas and the `Result` of satisfiability checking.
+///
+/// Atomic booleans appearing in `Constraints` and `Result` are assigned to
+/// labels either specified in `AtomNames` or created by default rules as B0,
+/// B1, ...
+///
+/// Requirements:
+///
+/// Names assigned to atoms should not be repeated in `AtomNames`.
+std::string debugString(
+ ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+
} // namespace dataflow
} // namespace clang
diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h
deleted file mode 100644
index 0c7b1ecd02b17c..00000000000000
--- a/clang/include/clang/Analysis/FlowSensitive/Formula.h
+++ /dev/null
@@ -1,137 +0,0 @@
-//===- Formula.h - Boolean formulas -----------------------------*- 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
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
-#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
-
-#include "clang/Basic/LLVM.h"
-#include "llvm/ADT/ArrayRef.h"
-#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/DenseMapInfo.h"
-#include "llvm/ADT/STLFunctionalExtras.h"
-#include "llvm/Support/Allocator.h"
-#include "llvm/Support/raw_ostream.h"
-#include <cassert>
-#include <string>
-#include <type_traits>
-
-namespace clang::dataflow {
-
-/// Identifies an atomic boolean variable such as "V1".
-///
-/// This often represents an assertion that is interesting to the analysis but
-/// cannot immediately be proven true or false. For example:
-/// - V1 may mean "the program reaches this point",
-/// - V2 may mean "the parameter was null"
-///
-/// We can use these variables in formulas to describe relationships we know
-/// to be true: "if the parameter was null, the program reaches this point".
-/// We also express hypotheses as formulas, and use a SAT solver to check
-/// whether they are consistent with the known facts.
-enum class Atom : unsigned {};
-
-/// A boolean expression such as "true" or "V1 & !V2".
-/// Expressions may refer to boolean atomic variables. These should take a
-/// consistent true/false value across the set of formulas being considered.
-///
-/// (Formulas are always expressions in terms of boolean variables rather than
-/// e.g. integers because our underlying model is SAT rather than e.g. SMT).
-///
-/// Simple formulas such as "true" and "V1" are self-contained.
-/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
-/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
-/// trailing objects.
-/// For this reason, Formulas are Arena-allocated and over-aligned.
-class Formula;
-class alignas(const Formula *) Formula {
-public:
- enum Kind : unsigned {
- /// A reference to an atomic boolean variable.
- /// We name these e.g. "V3", where 3 == atom identity == Value.
- AtomRef,
- // FIXME: add const true/false rather than modeling them as variables
-
- Not, /// True if its only operand is false
-
- // These kinds connect two operands LHS and RHS
- And, /// True if LHS and RHS are both true
- Or, /// True if either LHS or RHS is true
- Implies, /// True if LHS is false or RHS is true
- Equal, /// True if LHS and RHS have the same truth value
- };
- Kind kind() const { return FormulaKind; }
-
- Atom getAtom() const {
- assert(kind() == AtomRef);
- return static_cast<Atom>(Value);
- }
-
- ArrayRef<const Formula *> operands() const {
- return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
- numOperands(kind()));
- }
-
- using AtomNames = llvm::DenseMap<Atom, std::string>;
- // Produce a stable human-readable representation of this formula.
- // For example: (V3 | !(V1 & V2))
- // If AtomNames is provided, these override the default V0, V1... names.
- void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
-
- // Allocate Formulas using Arena rather than calling this function directly.
- static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
- ArrayRef<const Formula *> Operands,
- unsigned Value = 0);
-
-private:
- Formula() = default;
- Formula(const Formula &) = delete;
- Formula &operator=(const Formula &) = delete;
-
- static unsigned numOperands(Kind K) {
- switch (K) {
- case AtomRef:
- return 0;
- case Not:
- return 1;
- case And:
- case Or:
- case Implies:
- case Equal:
- return 2;
- }
- }
-
- Kind FormulaKind;
- // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
- unsigned Value;
-};
-
-// The default names of atoms are V0, V1 etc in order of creation.
-inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
- return OS << 'V' << static_cast<unsigned>(A);
-}
-inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
- F.print(OS);
- return OS;
-}
-
-} // namespace clang::dataflow
-namespace llvm {
-template <> struct DenseMapInfo<clang::dataflow::Atom> {
- using Atom = clang::dataflow::Atom;
- using Underlying = std::underlying_type_t<Atom>;
-
- static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
- static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
- static unsigned getHashValue(const Atom &Val) {
- return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
- }
- static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
-};
-} // namespace llvm
-#endif
diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h
index 079f6802f241ee..10964eab8c34cc 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Solver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h
@@ -14,10 +14,12 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
-#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Basic/LLVM.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseSet.h"
+#include "llvm/Support/Compiler.h"
#include <optional>
#include <vector>
@@ -47,7 +49,8 @@ class Solver {
/// 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<Atom, Assignment> Solution) {
+ static Result
+ Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
return Result(Status::Satisfiable, std::move(Solution));
}
@@ -65,17 +68,19 @@ class Solver {
/// 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<Atom, Assignment>> getSolution() const {
+ std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
+ getSolution() const {
return Solution;
}
private:
- Result(Status SATCheckStatus,
- std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
+ Result(
+ enum Status SATCheckStatus,
+ std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
: SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
Status SATCheckStatus;
- std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
+ std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
};
virtual ~Solver() = default;
@@ -86,11 +91,13 @@ class Solver {
/// Requirements:
///
/// All elements in `Vals` must not be null.
- virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0;
-};
+ virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0;
-llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
-llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
+ LLVM_DEPRECATED("Pass ArrayRef for determinism", "")
+ virtual Result solve(llvm::DenseSet<BoolValue *> Vals) {
+ return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end())));
+ }
+};
} // namespace dataflow
} // namespace clang
diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
index a0cdce93c9d470..b69cc01542c550 100644
--- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -14,8 +14,8 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
-#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/ArrayRef.h"
#include <limits>
@@ -46,7 +46,7 @@ class WatchedLiteralsSolver : public Solver {
explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
: MaxIterations(WorkLimit) {}
- Result solve(llvm::ArrayRef<const Formula *> Vals) override;
+ Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
};
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index e576affc6a41b5..cff6c45e185422 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -76,50 +76,4 @@ IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
return *It->second;
}
-const Formula &Arena::getFormula(const BoolValue &B) {
- auto It = ValToFormula.find(&B);
- if (It != ValToFormula.end())
- return *It->second;
- Formula &F = [&]() -> Formula & {
- switch (B.getKind()) {
- case Value::Kind::Integer:
- case Value::Kind::Reference:
- case Value::Kind::Pointer:
- case Value::Kind::Struct:
- llvm_unreachable("not a boolean");
- case Value::Kind::TopBool:
- case Value::Kind::AtomicBool:
- // TODO: assign atom numbers on creation rather than in getFormula(), so
- // they will be deterministic and maybe even meaningful.
- return Formula::create(Alloc, Formula::AtomRef, {},
- static_cast<unsigned>(makeAtom()));
- case Value::Kind::Conjunction:
- return Formula::create(
- Alloc, Formula::And,
- {&getFormula(cast<ConjunctionValue>(B).getLeftSubValue()),
- &getFormula(cast<ConjunctionValue>(B).getRightSubValue())});
- case Value::Kind::Disjunction:
- return Formula::create(
- Alloc, Formula::Or,
- {&getFormula(cast<DisjunctionValue>(B).getLeftSubValue()),
- &getFormula(cast<DisjunctionValue>(B).getRightSubValue())});
- case Value::Kind::Negation:
- return Formula::create(Alloc, Formula::Not,
- {&getFormula(cast<NegationValue>(B).getSubVal())});
- case Value::Kind::Implication:
- return Formula::create(
- Alloc, Formula::Implies,
- {&getFormula(cast<ImplicationValue>(B).getLeftSubValue()),
- &getFormula(cast<ImplicationValue>(B).getRightSubValue())});
- case Value::Kind::Biconditional:
- return Formula::create(
- Alloc, Formula::Equal,
- {&getFormula(cast<BiconditionalValue>(B).getLeftSubValue()),
- &getFormula(cast<BiconditionalValue>(B).getRightSubValue())});
- }
- }();
- ValToFormula.try_emplace(&B, &F);
- return F;
-}
-
} // namespace clang::dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index 171884afe8f4bf..d59bebf6a5a127 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,7 +3,6 @@ add_clang_library(clangAnalysisFlowSensitive
ControlFlowContext.cpp
DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
- Formula.cpp
HTMLLogger.cpp
Logger.cpp
RecordOps.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 42cc6d4c3d143e..37bcc8be958792 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -15,7 +15,6 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/AST/ExprCXX.h"
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Logger.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/SetOperations.h"
@@ -24,12 +23,9 @@
#include "llvm/Support/Debug.h"
#include "llvm/Support/FileSystem.h"
#include "llvm/Support/Path.h"
-#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <memory>
-#include <string>
#include <utility>
-#include <vector>
static llvm::cl::opt<std::string> DataflowLog(
"dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
@@ -133,10 +129,7 @@ Solver::Result
DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) {
Constraints.insert(&arena().makeLiteral(true));
Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
- std::vector<const Formula *> Formulas;
- for (const BoolValue *Constraint : Constraints)
- Formulas.push_back(&arena().getFormula(*Constraint));
- return S->solve(Formulas);
+ return S->solve(Constraints.getArrayRef());
}
bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
@@ -198,21 +191,15 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
llvm::raw_ostream &OS) {
- // TODO: accumulate formulas directly instead
llvm::SetVector<BoolValue *> Constraints;
Constraints.insert(&Token);
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- // TODO: have formulas know about true/false directly instead
- Atom True = arena().getFormula(arena().makeLiteral(true)).getAtom();
- Atom False = arena().getFormula(arena().makeLiteral(false)).getAtom();
- Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
-
- for (const auto *Constraint : Constraints) {
- arena().getFormula(*Constraint).print(OS, &Names);
- OS << "\n";
- }
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
+ {&arena().makeLiteral(false), "False"},
+ {&arena().makeLiteral(true), "True"}};
+ OS << debugString(Constraints.getArrayRef(), AtomNames);
}
const ControlFlowContext *
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
index 34e53249ba4d8b..25225ed6266fb8 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -16,12 +16,22 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/STLExtras.h"
#include "llvm/ADT/StringRef.h"
+#include "llvm/ADT/StringSet.h"
#include "llvm/Support/ErrorHandling.h"
+#include "llvm/Support/FormatAdapters.h"
+#include "llvm/Support/FormatCommon.h"
+#include "llvm/Support/FormatVariadic.h"
namespace clang {
namespace dataflow {
+using llvm::AlignStyle;
+using llvm::fmt_pad;
+using llvm::formatv;
+
llvm::StringRef debugString(Value::Kind Kind) {
switch (Kind) {
case Value::Kind::Integer:
@@ -50,13 +60,12 @@ llvm::StringRef debugString(Value::Kind Kind) {
llvm_unreachable("Unhandled value kind");
}
-llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
- Solver::Result::Assignment Assignment) {
+llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
switch (Assignment) {
case Solver::Result::Assignment::AssignedFalse:
- return OS << "False";
+ return "False";
case Solver::Result::Assignment::AssignedTrue:
- return OS << "True";
+ return "True";
}
llvm_unreachable("Booleans can only be assigned true/false");
}
@@ -73,16 +82,174 @@ llvm::StringRef debugString(Solver::Result::Status Status) {
llvm_unreachable("Unhandled SAT check result status");
}
-llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
- OS << debugString(R.getStatus()) << "\n";
- if (auto Solution = R.getSolution()) {
- std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
- Solution->begin(), Solution->end()};
- llvm::sort(Sorted);
- for (const auto &Entry : Sorted)
- OS << Entry.first << " = " << Entry.second << "\n";
+namespace {
+
+class DebugStringGenerator {
+public:
+ explicit DebugStringGenerator(
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
+ : Counter(0), AtomNames(std::move(AtomNamesArg)) {
+#ifndef NDEBUG
+ llvm::StringSet<> Names;
+ for (auto &N : AtomNames) {
+ assert(Names.insert(N.second).second &&
+ "The same name must not assigned to
diff erent atoms");
+ }
+#endif
+ }
+
+ /// Returns a string representation of a boolean value `B`.
+ std::string debugString(const BoolValue &B, size_t Depth = 0) {
+ std::string S;
+ switch (B.getKind()) {
+ case Value::Kind::AtomicBool: {
+ S = getAtomName(&cast<AtomicBoolValue>(B));
+ break;
+ }
+ case Value::Kind::TopBool: {
+ S = "top";
+ break;
+ }
+ case Value::Kind::Conjunction: {
+ auto &C = cast<ConjunctionValue>(B);
+ auto L = debugString(C.getLeftSubValue(), Depth + 1);
+ auto R = debugString(C.getRightSubValue(), Depth + 1);
+ S = formatv("(and\n{0}\n{1})", L, R);
+ break;
+ }
+ case Value::Kind::Disjunction: {
+ auto &D = cast<DisjunctionValue>(B);
+ auto L = debugString(D.getLeftSubValue(), Depth + 1);
+ auto R = debugString(D.getRightSubValue(), Depth + 1);
+ S = formatv("(or\n{0}\n{1})", L, R);
+ break;
+ }
+ case Value::Kind::Negation: {
+ auto &N = cast<NegationValue>(B);
+ S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
+ break;
+ }
+ case Value::Kind::Implication: {
+ auto &IV = cast<ImplicationValue>(B);
+ auto L = debugString(IV.getLeftSubValue(), Depth + 1);
+ auto R = debugString(IV.getRightSubValue(), Depth + 1);
+ S = formatv("(=>\n{0}\n{1})", L, R);
+ break;
+ }
+ case Value::Kind::Biconditional: {
+ auto &BV = cast<BiconditionalValue>(B);
+ auto L = debugString(BV.getLeftSubValue(), Depth + 1);
+ auto R = debugString(BV.getRightSubValue(), Depth + 1);
+ S = formatv("(=\n{0}\n{1})", L, R);
+ break;
+ }
+ default:
+ llvm_unreachable("Unhandled value kind");
+ }
+ auto Indent = Depth * 4;
+ return formatv("{0}", fmt_pad(S, Indent, 0));
+ }
+
+ std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) {
+ std::string Result;
+ for (const BoolValue *S : Constraints) {
+ Result += debugString(*S);
+ Result += '\n';
+ }
+ return Result;
+ }
+
+ /// Returns a string representation of a set of boolean `Constraints` and the
+ /// `Result` of satisfiability checking on the `Constraints`.
+ std::string debugString(ArrayRef<BoolValue *> &Constraints,
+ const Solver::Result &Result) {
+ auto Template = R"(
+Constraints
+------------
+{0:$[
+
+]}
+------------
+{1}.
+{2}
+)";
+
+ std::vector<std::string> ConstraintsStrings;
+ ConstraintsStrings.reserve(Constraints.size());
+ for (auto &Constraint : Constraints) {
+ ConstraintsStrings.push_back(debugString(*Constraint));
+ }
+
+ auto StatusString = clang::dataflow::debugString(Result.getStatus());
+ auto Solution = Result.getSolution();
+ auto SolutionString = Solution ? "\n" + debugString(*Solution) : "";
+
+ return formatv(
+ Template,
+ llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
+ StatusString, SolutionString);
+ }
+
+private:
+ /// Returns a string representation of a truth assignment to atom booleans.
+ std::string debugString(
+ const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
+ &AtomAssignments) {
+ size_t MaxNameLength = 0;
+ for (auto &AtomName : AtomNames) {
+ MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
+ }
+
+ std::vector<std::string> Lines;
+ for (auto &AtomAssignment : AtomAssignments) {
+ auto Line = formatv("{0} = {1}",
+ fmt_align(getAtomName(AtomAssignment.first),
+ AlignStyle::Left, MaxNameLength),
+ clang::dataflow::debugString(AtomAssignment.second));
+ Lines.push_back(Line);
+ }
+ llvm::sort(Lines);
+
+ return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
}
- return OS;
+
+ /// Returns the name assigned to `Atom`, either user-specified or created by
+ /// default rules (B0, B1, ...).
+ std::string getAtomName(const AtomicBoolValue *Atom) {
+ auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
+ if (Entry.second) {
+ Counter++;
+ }
+ return Entry.first->second;
+ }
+
+ // Keep track of number of atoms without a user-specified name, used to assign
+ // non-repeating default names to such atoms.
+ size_t Counter;
+
+ // Keep track of names assigned to atoms.
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
+};
+
+} // namespace
+
+std::string
+debugString(const BoolValue &B,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
+ return DebugStringGenerator(std::move(AtomNames)).debugString(B);
+}
+
+std::string
+debugString(llvm::ArrayRef<BoolValue *> Constraints,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
+ return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
+}
+
+std::string
+debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
+ return DebugStringGenerator(std::move(AtomNames))
+ .debugString(Constraints, Result);
}
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
deleted file mode 100644
index 504ad2fb7938af..00000000000000
--- a/clang/lib/Analysis/FlowSensitive/Formula.cpp
+++ /dev/null
@@ -1,82 +0,0 @@
-//===- Formula.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
-//
-//===----------------------------------------------------------------------===//
-
-#include "clang/Analysis/FlowSensitive/Formula.h"
-#include "clang/Basic/LLVM.h"
-#include "llvm/ADT/STLExtras.h"
-#include "llvm/ADT/StringRef.h"
-#include "llvm/Support/Allocator.h"
-#include "llvm/Support/ErrorHandling.h"
-#include <cassert>
-
-namespace clang::dataflow {
-
-Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
- ArrayRef<const Formula *> Operands, unsigned Value) {
- assert(Operands.size() == numOperands(K));
- if (Value != 0) // Currently, formulas have values or operands, not both.
- assert(numOperands(K) == 0);
- void *Mem = Alloc.Allocate(sizeof(Formula) +
- Operands.size() * sizeof(Operands.front()),
- alignof(Formula));
- Formula *Result = new (Mem) Formula();
- Result->FormulaKind = K;
- Result->Value = Value;
- // Operands are stored as `const Formula *`s after the formula itself.
- // We don't need to construct an object as pointers are trivial types.
- // Formula is alignas(const Formula *), so alignment is satisfied.
- llvm::copy(Operands, reinterpret_cast<const Formula **>(Result + 1));
- return *Result;
-}
-
-static llvm::StringLiteral sigil(Formula::Kind K) {
- switch (K) {
- case Formula::AtomRef:
- return "";
- case Formula::Not:
- return "!";
- case Formula::And:
- return " & ";
- case Formula::Or:
- return " | ";
- case Formula::Implies:
- return " => ";
- case Formula::Equal:
- return " = ";
- }
- llvm_unreachable("unhandled formula kind");
-}
-
-void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
- if (Names && kind() == AtomRef)
- if (auto It = Names->find(getAtom()); It != Names->end()) {
- OS << It->second;
- return;
- }
-
- switch (numOperands(kind())) {
- case 0:
- OS << getAtom();
- break;
- case 1:
- OS << sigil(kind());
- operands()[0]->print(OS, Names);
- break;
- case 2:
- OS << '(';
- operands()[0]->print(OS, Names);
- OS << sigil(kind());
- operands()[1]->print(OS, Names);
- OS << ')';
- break;
- default:
- llvm_unreachable("unhandled formula arity");
- }
-}
-
-} // namespace clang::dataflow
\ No newline at end of file
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index 037886d09c4f7d..db2e1d694457bf 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -17,8 +17,8 @@
#include <queue>
#include <vector>
-#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
@@ -79,7 +79,7 @@ using ClauseID = uint32_t;
static constexpr ClauseID NullClause = 0;
/// A boolean formula in conjunctive normal form.
-struct CNFFormula {
+struct BooleanFormula {
/// `LargestVar` is equal to the largest positive integer that represents a
/// variable in the formula.
const Variable LargestVar;
@@ -121,12 +121,12 @@ struct CNFFormula {
/// clauses in the formula start from the element at index 1.
std::vector<ClauseID> NextWatched;
- /// Stores the variable identifier and Atom for atomic booleans in the
- /// formula.
- llvm::DenseMap<Variable, Atom> Atomics;
+ /// Stores the variable identifier and value location for atomic booleans in
+ /// the formula.
+ llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
- explicit CNFFormula(Variable LargestVar,
- llvm::DenseMap<Variable, Atom> Atomics)
+ explicit BooleanFormula(Variable LargestVar,
+ llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
: LargestVar(LargestVar), Atomics(std::move(Atomics)) {
Clauses.push_back(0);
ClauseStarts.push_back(0);
@@ -144,8 +144,8 @@ struct CNFFormula {
///
/// 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 Formula
- // and the construction in `buildCNF`.
+ // 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));
@@ -178,59 +178,98 @@ struct CNFFormula {
/// Converts the conjunction of `Vals` into a formula in conjunctive normal
/// form where each clause has at least one and at most three literals.
-CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
+BooleanFormula buildBooleanFormula(const llvm::ArrayRef<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-formulas in `Vals`.
+ // of sub-values in `Vals`.
- // Map each sub-formula in `Vals` to a unique variable.
- llvm::DenseMap<const Formula *, Variable> SubValsToVar;
- // Store variable identifiers and Atom of atomic booleans.
- llvm::DenseMap<Variable, Atom> Atomics;
+ // 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<const Formula *> UnprocessedSubVals;
- for (const Formula *Val : Vals)
+ std::queue<BoolValue *> UnprocessedSubVals;
+ for (BoolValue *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
Variable Var = NextVar;
- const Formula *Val = UnprocessedSubVals.front();
+ BoolValue *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
if (!SubValsToVar.try_emplace(Val, Var).second)
continue;
++NextVar;
- for (const Formula *F : Val->operands())
- UnprocessedSubVals.push(F);
- if (Val->kind() == Formula::AtomRef)
- Atomics[Var] = Val->getAtom();
+ // Visit the sub-values of `Val`.
+ switch (Val->getKind()) {
+ case Value::Kind::Conjunction: {
+ auto *C = cast<ConjunctionValue>(Val);
+ UnprocessedSubVals.push(&C->getLeftSubValue());
+ UnprocessedSubVals.push(&C->getRightSubValue());
+ break;
+ }
+ case Value::Kind::Disjunction: {
+ auto *D = cast<DisjunctionValue>(Val);
+ UnprocessedSubVals.push(&D->getLeftSubValue());
+ UnprocessedSubVals.push(&D->getRightSubValue());
+ break;
+ }
+ case Value::Kind::Negation: {
+ auto *N = cast<NegationValue>(Val);
+ UnprocessedSubVals.push(&N->getSubVal());
+ break;
+ }
+ case Value::Kind::Implication: {
+ auto *I = cast<ImplicationValue>(Val);
+ UnprocessedSubVals.push(&I->getLeftSubValue());
+ UnprocessedSubVals.push(&I->getRightSubValue());
+ break;
+ }
+ case Value::Kind::Biconditional: {
+ auto *B = cast<BiconditionalValue>(Val);
+ UnprocessedSubVals.push(&B->getLeftSubValue());
+ UnprocessedSubVals.push(&B->getRightSubValue());
+ break;
+ }
+ case Value::Kind::TopBool:
+ // Nothing more to do. This `TopBool` instance has already been mapped
+ // to a fresh solver variable (`NextVar`, above) and is thereafter
+ // anonymous. The solver never sees `Top`.
+ break;
+ case Value::Kind::AtomicBool: {
+ Atomics[Var] = cast<AtomicBoolValue>(Val);
+ break;
+ }
+ default:
+ llvm_unreachable("buildBooleanFormula: unhandled value kind");
+ }
}
}
- auto GetVar = [&SubValsToVar](const Formula *Val) {
+ auto GetVar = [&SubValsToVar](const BoolValue *Val) {
auto ValIt = SubValsToVar.find(Val);
assert(ValIt != SubValsToVar.end());
return ValIt->second;
};
- CNFFormula CNF(NextVar - 1, std::move(Atomics));
+ BooleanFormula Formula(NextVar - 1, std::move(Atomics));
std::vector<bool> ProcessedSubVals(NextVar, false);
- // Add a conjunct for each variable that represents a top-level formula in
- // `Vals`.
- for (const Formula *Val : Vals)
- CNF.addClause(posLit(GetVar(Val)));
+ // 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-formulas.
- std::queue<const Formula *> UnprocessedSubVals;
- for (const Formula *Val : Vals)
+ // and their corresponding sub-values.
+ std::queue<BoolValue *> UnprocessedSubVals;
+ for (BoolValue *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
- const Formula *Val = UnprocessedSubVals.front();
+ const BoolValue *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
const Variable Var = GetVar(Val);
@@ -238,107 +277,117 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
continue;
ProcessedSubVals[Var] = true;
- switch (Val->kind()) {
- case Formula::AtomRef:
- break;
- case Formula::And: {
- const Variable LHS = GetVar(Val->operands()[0]);
- const Variable RHS = GetVar(Val->operands()[1]);
+ if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+ const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
+ const Variable RightSubVar = GetVar(&C->getRightSubValue());
- if (LHS == RHS) {
+ if (LeftSubVar == RightSubVar) {
// `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
// already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- CNF.addClause(negLit(Var), posLit(LHS));
- CNF.addClause(posLit(Var), negLit(LHS));
+ Formula.addClause(negLit(Var), posLit(LeftSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar));
+
+ // Visit a sub-value of `Val` (pick any, they are identical).
+ UnprocessedSubVals.push(&C->getLeftSubValue());
} else {
// `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.
- CNF.addClause(negLit(Var), posLit(LHS));
- CNF.addClause(negLit(Var), posLit(RHS));
- CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+ 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());
}
- break;
- }
- case Formula::Or: {
- const Variable LHS = GetVar(Val->operands()[0]);
- const Variable RHS = GetVar(Val->operands()[1]);
+ } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
+ const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
+ const Variable RightSubVar = GetVar(&D->getRightSubValue());
- if (LHS == RHS) {
+ if (LeftSubVar == RightSubVar) {
// `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
// already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- CNF.addClause(negLit(Var), posLit(LHS));
- CNF.addClause(posLit(Var), negLit(LHS));
+ Formula.addClause(negLit(Var), posLit(LeftSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar));
+
+ // Visit a sub-value of `Val` (pick any, they are identical).
+ UnprocessedSubVals.push(&D->getLeftSubValue());
} else {
- // `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.
- CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS));
- CNF.addClause(posLit(Var), negLit(LHS));
- CNF.addClause(posLit(Var), negLit(RHS));
+ // `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());
}
- break;
- }
- case Formula::Not: {
- const Variable Operand = GetVar(Val->operands()[0]);
-
- // `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.
- CNF.addClause(negLit(Var), negLit(Operand));
- CNF.addClause(posLit(Var), posLit(Operand));
- break;
- }
- case Formula::Implies: {
- const Variable LHS = GetVar(Val->operands()[0]);
- const Variable RHS = GetVar(Val->operands()[1]);
+ } 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());
+ } else if (auto *I = dyn_cast<ImplicationValue>(Val)) {
+ const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
+ const Variable RightSubVar = GetVar(&I->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.
- CNF.addClause(posLit(Var), posLit(LHS));
- CNF.addClause(posLit(Var), negLit(RHS));
- CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
- break;
- }
- case Formula::Equal: {
- const Variable LHS = GetVar(Val->operands()[0]);
- const Variable RHS = GetVar(Val->operands()[1]);
-
- if (LHS == RHS) {
+ // conjunctive normal form. Below we add each of the conjuncts of the
+ // latter expression to the result.
+ Formula.addClause(posLit(Var), posLit(LeftSubVar));
+ Formula.addClause(posLit(Var), negLit(RightSubVar));
+ Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
+
+ // Visit the sub-values of `Val`.
+ UnprocessedSubVals.push(&I->getLeftSubValue());
+ UnprocessedSubVals.push(&I->getRightSubValue());
+ } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) {
+ const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
+ const Variable RightSubVar = GetVar(&B->getRightSubValue());
+
+ if (LeftSubVar == RightSubVar) {
// `X <=> (A <=> A)` is equvalent to `X` which is already in
// conjunctive normal form. Below we add each of the conjuncts of the
// latter expression to the result.
- CNF.addClause(posLit(Var));
+ Formula.addClause(posLit(Var));
// No need to visit the sub-values of `Val`.
- continue;
+ } else {
+ // `X <=> (A <=> B)` is equivalent to
+ // `(X v A v B) ^ (X v !A v !B) ^ (!X v A 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(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
+ Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+ Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));
+ Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
+
+ // Visit the sub-values of `Val`.
+ UnprocessedSubVals.push(&B->getLeftSubValue());
+ UnprocessedSubVals.push(&B->getRightSubValue());
}
- // `X <=> (A <=> B)` is equivalent to
- // `(X v A v B) ^ (X v !A v !B) ^ (!X v A 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.
- CNF.addClause(posLit(Var), posLit(LHS), posLit(RHS));
- CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
- CNF.addClause(negLit(Var), posLit(LHS), negLit(RHS));
- CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
- break;
- }
}
- for (const Formula *Child : Val->operands())
- UnprocessedSubVals.push(Child);
}
- return CNF;
+ 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.
- CNFFormula CNF;
+ 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`
@@ -390,10 +439,9 @@ class WatchedLiteralsSolverImpl {
std::vector<Variable> ActiveVars;
public:
- explicit WatchedLiteralsSolverImpl(
- const llvm::ArrayRef<const Formula *> &Vals)
- : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
- LevelStates(CNF.LargestVar + 1) {
+ explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<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
@@ -402,10 +450,10 @@ class WatchedLiteralsSolverImpl {
LevelStates[0] = State::Decision;
// Initialize all variables as unassigned.
- VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);
+ VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
// Initialize the active variables.
- for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
+ for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
ActiveVars.push_back(Var);
}
@@ -426,7 +474,7 @@ class WatchedLiteralsSolverImpl {
// 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 `buildCNF`.
+ // transformations performed by `buildBooleanFormula`.
assert(activeVarsAreUnassigned());
assert(activeVarsFormWatchedLiterals());
assert(unassignedVarsFormingWatchedLiteralsAreActive());
@@ -507,10 +555,12 @@ class WatchedLiteralsSolverImpl {
}
private:
- /// Returns a satisfying truth assignment to the atoms in the boolean formula.
- llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
- llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
- for (auto &Atomic : CNF.Atomics) {
+ /// 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 &Atomic : 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.
@@ -546,24 +596,24 @@ class WatchedLiteralsSolverImpl {
const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
? negLit(Var)
: posLit(Var);
- ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];
- CNF.WatchedHead[FalseLit] = NullClause;
+ ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
+ Formula.WatchedHead[FalseLit] = NullClause;
while (FalseLitWatcher != NullClause) {
- const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];
+ const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
// Pick the first non-false literal as the new watched literal.
- const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];
+ const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
- while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
+ while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
++NewWatchedLitIdx;
- const Literal NewWatchedLit = CNF.Clauses[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.
- CNF.Clauses[NewWatchedLitIdx] = FalseLit;
- CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+ 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.
@@ -571,8 +621,8 @@ class WatchedLiteralsSolverImpl {
VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
ActiveVars.push_back(NewWatchedLitVar);
- CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];
- CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+ Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
+ Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
// Go to the next clause that watches `FalseLit`.
FalseLitWatcher = NextFalseLitWatcher;
@@ -582,15 +632,16 @@ class WatchedLiteralsSolverImpl {
/// 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 = CNF.WatchedHead[Lit]; LitWatcher != NullClause;
- LitWatcher = CNF.NextWatched[LitWatcher]) {
- llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
+ 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 `buildCNF`.
+ // due to the transformations performed by `buildBooleanFormula`.
assert(Clause.front() == Lit);
if (isUnit(Clause))
@@ -614,7 +665,7 @@ class WatchedLiteralsSolverImpl {
/// Returns true if and only if `Lit` is watched by a clause in `Formula`.
bool isWatched(Literal Lit) const {
- return CNF.WatchedHead[Lit] != NullClause;
+ return Formula.WatchedHead[Lit] != NullClause;
}
/// Returns an assignment for an unassigned variable.
@@ -627,8 +678,8 @@ class WatchedLiteralsSolverImpl {
/// Returns a set of all watched literals.
llvm::DenseSet<Literal> watchedLiterals() const {
llvm::DenseSet<Literal> WatchedLiterals;
- for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
- if (CNF.WatchedHead[Lit] == NullClause)
+ for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
+ if (Formula.WatchedHead[Lit] == NullClause)
continue;
WatchedLiterals.insert(Lit);
}
@@ -668,8 +719,7 @@ class WatchedLiteralsSolverImpl {
}
};
-Solver::Result
-WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
+Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) {
if (Vals.empty())
return Solver::Result::Satisfiable({{}});
auto [Res, Iterations] =
diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
index 53131723ff5cef..407abf58529a50 100644
--- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -7,7 +7,6 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Arena.h"
-#include "llvm/Support/ScopedPrinter.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -126,26 +125,5 @@ TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
EXPECT_NE(&XIffY1, &XIffZ);
}
-TEST_F(ArenaTest, ValueToFormula) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
- auto &XIffY = A.makeEquals(X, Y);
- auto &XOrNotY = A.makeOr(X, A.makeNot(Y));
- auto &Implies = A.makeImplies(XIffY, XOrNotY);
-
- EXPECT_EQ(llvm::to_string(A.getFormula(Implies)),
- "((V0 = V1) => (V0 | !V1))");
-}
-
-TEST_F(ArenaTest, ValueToFormulaCached) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
- auto &XIffY = A.makeEquals(X, Y);
-
- auto &Formula1 = A.getFormula(XIffY);
- auto &Formula2 = A.getFormula(XIffY);
- EXPECT_EQ(&Formula1, &Formula2);
-}
-
} // namespace
} // namespace clang::dataflow
diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
index 8ee56ae08b98a9..10fcd204c9ab07 100644
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -8,9 +8,8 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
-#include "llvm/Support/ScopedPrinter.h"
-#include "llvm/Support/raw_ostream.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -23,88 +22,429 @@ using test::ConstraintContext;
using testing::StrEq;
TEST(BoolValueDebugStringTest, AtomicBoolean) {
+ // B0
ConstraintContext Ctx;
auto B = Ctx.atom();
- auto Expected = "V0";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"(B0)";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
+}
+
+TEST(BoolValueDebugStringTest, Top) {
+ ConstraintContext Ctx;
+ auto B = Ctx.top();
+
+ auto Expected = R"(top)";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Negation) {
+ // !B0
ConstraintContext Ctx;
auto B = Ctx.neg(Ctx.atom());
- auto Expected = "!V0";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((not
+ B0))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Conjunction) {
+ // B0 ^ B1
ConstraintContext Ctx;
auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
- auto Expected = "(V0 & V1)";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((and
+ B0
+ B1))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Disjunction) {
+ // B0 v B1
ConstraintContext Ctx;
auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
- auto Expected = "(V0 | V1)";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((or
+ B0
+ B1))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Implication) {
+ // B0 => B1
ConstraintContext Ctx;
auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
- auto Expected = "(V0 => V1)";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((=>
+ B0
+ B1))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Iff) {
+ // B0 <=> B1
ConstraintContext Ctx;
auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
- auto Expected = "(V0 = V1)";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((=
+ B0
+ B1))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Xor) {
+ // (B0 ^ !B1) V (!B0 ^ B1)
ConstraintContext Ctx;
auto B0 = Ctx.atom();
auto B1 = Ctx.atom();
auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
- auto Expected = "((V0 & !V1) | (!V0 & V1))";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((or
+ (and
+ B0
+ (not
+ B1))
+ (and
+ (not
+ B0)
+ B1)))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, NestedBoolean) {
+ // B0 ^ (B1 v (B2 ^ (B3 v B4)))
ConstraintContext Ctx;
auto B = Ctx.conj(
Ctx.atom(),
Ctx.disj(Ctx.atom(),
Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
- auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((and
+ B0
+ (or
+ B1
+ (and
+ B2
+ (or
+ B3
+ B4)))))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
+}
+
+TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
+ // True
+ ConstraintContext Ctx;
+ auto True = cast<AtomicBoolValue>(Ctx.atom());
+ auto B = True;
+
+ auto Expected = R"(True)";
+ EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
+}
+
+TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
+ // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
+ ConstraintContext Ctx;
+ auto Cond = cast<AtomicBoolValue>(Ctx.atom());
+ auto Then = cast<AtomicBoolValue>(Ctx.atom());
+ auto Else = cast<AtomicBoolValue>(Ctx.atom());
+ auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
+ Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
+
+ auto Expected = R"((or
+ (and
+ Cond
+ (and
+ Then
+ (not
+ Else)))
+ (and
+ (not
+ Cond)
+ (and
+ (not
+ Then)
+ Else))))";
+ EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
+ StrEq(Expected));
}
TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
+ // (False && B0) v (True v B1)
ConstraintContext Ctx;
- auto True = Ctx.atom();
- auto False = Ctx.atom();
- Formula::AtomNames Names;
- Names[True->getAtom()] = "true";
- Names[False->getAtom()] = "false";
+ auto True = cast<AtomicBoolValue>(Ctx.atom());
+ auto False = cast<AtomicBoolValue>(Ctx.atom());
auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
- auto Expected = R"(((false & V2) | (true | V3)))";
- std::string Actual;
- llvm::raw_string_ostream OS(Actual);
- B->print(OS, &Names);
- EXPECT_THAT(Actual, StrEq(Expected));
+ auto Expected = R"((or
+ (and
+ False
+ B0)
+ (or
+ True
+ B1)))";
+ EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
+ StrEq(Expected));
+}
+
+TEST(ConstraintSetDebugStringTest, Empty) {
+ llvm::ArrayRef<BoolValue *> Constraints;
+ EXPECT_THAT(debugString(Constraints), StrEq(""));
+}
+
+TEST(ConstraintSetDebugStringTest, Simple) {
+ ConstraintContext Ctx;
+ std::vector<BoolValue *> Constraints;
+ auto X = cast<AtomicBoolValue>(Ctx.atom());
+ auto Y = cast<AtomicBoolValue>(Ctx.atom());
+ Constraints.push_back(Ctx.disj(X, Y));
+ Constraints.push_back(Ctx.disj(X, Ctx.neg(Y)));
+
+ auto Expected = R"((or
+ X
+ Y)
+(or
+ X
+ (not
+ Y))
+)";
+ EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),
+ StrEq(Expected));
+}
+
+Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
+ return WatchedLiteralsSolver().solve(std::move(Constraints));
+}
+
+TEST(SATCheckDebugStringTest, AtomicBoolean) {
+ // B0
+ ConstraintContext Ctx;
+ std::vector<BoolValue *> Constraints({Ctx.atom()});
+ auto Result = CheckSAT(Constraints);
+
+ auto Expected = R"(
+Constraints
+------------
+B0
+------------
+Satisfiable.
+
+B0 = True
+)";
+ EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
+ // B0, !B0
+ ConstraintContext Ctx;
+ auto B0 = Ctx.atom();
+ std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
+ auto Result = CheckSAT(Constraints);
+
+ auto Expected = R"(
+Constraints
+------------
+B0
+
+(not
+ B0)
+------------
+Unsatisfiable.
+
+)";
+ EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
+ // B0, B1
+ ConstraintContext Ctx;
+ std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
+ auto Result = CheckSAT(Constraints);
+
+ auto Expected = R"(
+Constraints
+------------
+B0
+
+B1
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+ EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, Implication) {
+ // B0, B0 => B1
+ ConstraintContext Ctx;
+ auto B0 = Ctx.atom();
+ auto B1 = Ctx.atom();
+ auto Impl = Ctx.disj(Ctx.neg(B0), B1);
+ std::vector<BoolValue *> Constraints({B0, Impl});
+ auto Result = CheckSAT(Constraints);
+
+ auto Expected = R"(
+Constraints
+------------
+B0
+
+(or
+ (not
+ B0)
+ B1)
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+ EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
}
+TEST(SATCheckDebugStringTest, Iff) {
+ // B0, B0 <=> B1
+ ConstraintContext Ctx;
+ auto B0 = Ctx.atom();
+ auto B1 = Ctx.atom();
+ auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
+ std::vector<BoolValue *> Constraints({B0, Iff});
+ auto Result = CheckSAT(Constraints);
+
+ auto Expected = R"(
+Constraints
+------------
+B0
+
+(and
+ (or
+ (not
+ B0)
+ B1)
+ (or
+ B0
+ (not
+ B1)))
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+ EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, Xor) {
+ // B0, XOR(B0, B1)
+ ConstraintContext Ctx;
+ auto B0 = Ctx.atom();
+ auto B1 = Ctx.atom();
+ auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
+ std::vector<BoolValue *> Constraints({B0, XOR});
+ auto Result = CheckSAT(Constraints);
+
+ auto Expected = R"(
+Constraints
+------------
+B0
+
+(or
+ (and
+ B0
+ (not
+ B1))
+ (and
+ (not
+ B0)
+ B1))
+------------
+Satisfiable.
+
+B0 = True
+B1 = False
+)";
+ EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
+ // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
+ ConstraintContext Ctx;
+ auto Cond = cast<AtomicBoolValue>(Ctx.atom());
+ auto Then = cast<AtomicBoolValue>(Ctx.atom());
+ auto Else = cast<AtomicBoolValue>(Ctx.atom());
+ auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
+ Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
+ std::vector<BoolValue *> Constraints({Cond, B});
+ auto Result = CheckSAT(Constraints);
+
+ auto Expected = R"(
+Constraints
+------------
+Cond
+
+(or
+ (and
+ Cond
+ (and
+ Then
+ (not
+ Else)))
+ (and
+ (not
+ Cond)
+ (and
+ (not
+ Then)
+ Else)))
+------------
+Satisfiable.
+
+Cond = True
+Else = False
+Then = True
+)";
+ EXPECT_THAT(debugString(Constraints, Result,
+ {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
+ StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
+ // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
+ ConstraintContext Ctx;
+ auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
+ auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
+ auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
+ auto BothZeroImpliesEQ =
+ Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
+ std::vector<BoolValue *> Constraints(
+ {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
+ auto Result = CheckSAT(Constraints);
+
+ auto Expected = R"(
+Constraints
+------------
+ThisIntEqZero
+
+(not
+ IntsAreEq)
+
+(or
+ (not
+ (and
+ ThisIntEqZero
+ OtherIntEqZero))
+ IntsAreEq)
+------------
+Satisfiable.
+
+IntsAreEq = False
+OtherIntEqZero = False
+ThisIntEqZero = True
+)";
+ EXPECT_THAT(debugString(Constraints, Result,
+ {{IntsAreEq, "IntsAreEq"},
+ {ThisIntEqZero, "ThisIntEqZero"},
+ {OtherIntEqZero, "OtherIntEqZero"}}),
+ StrEq(Expected));
+}
} // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index ba0a77a910d7c4..9999dd3a475f1b 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -9,10 +9,9 @@
#include <utility>
#include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
-#include "llvm/ADT/ArrayRef.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -24,31 +23,26 @@ using namespace dataflow;
using test::ConstraintContext;
using testing::_;
using testing::AnyOf;
+using testing::IsEmpty;
+using testing::Optional;
using testing::Pair;
using testing::UnorderedElementsAre;
-constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
-constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
-
// Checks if the conjunction of `Vals` is satisfiable and returns the
// corresponding result.
-Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
+Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
return WatchedLiteralsSolver().solve(Vals);
}
-MATCHER(unsat, "") {
- return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
+void expectUnsatisfiable(Solver::Result Result) {
+ EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
+ EXPECT_FALSE(Result.getSolution().has_value());
}
-MATCHER_P(sat, SolutionMatcher,
- "is satisfiable, where solution " +
- (testing::DescribeMatcher<
- llvm::DenseMap<Atom, Solver::Result::Assignment>>(
- SolutionMatcher))) {
- if (arg.getStatus() != Solver::Result::Status::Satisfiable)
- return false;
- auto Solution = *arg.getSolution();
- return testing::ExplainMatchResult(SolutionMatcher, Solution,
- result_listener);
+
+template <typename Matcher>
+void expectSatisfiable(Solver::Result Result, Matcher Solution) {
+ EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
+ EXPECT_THAT(Result.getSolution(), Optional(Solution));
}
TEST(SolverTest, Var) {
@@ -56,8 +50,9 @@ TEST(SolverTest, Var) {
auto X = Ctx.atom();
// X
- EXPECT_THAT(solve({X}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
+ expectSatisfiable(
+ solve({X}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
}
TEST(SolverTest, NegatedVar) {
@@ -66,8 +61,9 @@ TEST(SolverTest, NegatedVar) {
auto NotX = Ctx.neg(X);
// !X
- EXPECT_THAT(solve({NotX}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
+ expectSatisfiable(
+ solve({NotX}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
}
TEST(SolverTest, UnitConflict) {
@@ -76,7 +72,7 @@ TEST(SolverTest, UnitConflict) {
auto NotX = Ctx.neg(X);
// X ^ !X
- EXPECT_THAT(solve({X, NotX}), unsat());
+ expectUnsatisfiable(solve({X, NotX}));
}
TEST(SolverTest, DistinctVars) {
@@ -86,9 +82,36 @@ TEST(SolverTest, DistinctVars) {
auto NotY = Ctx.neg(Y);
// X ^ !Y
- EXPECT_THAT(solve({X, NotY}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
- Pair(Y->getAtom(), AssignedFalse))));
+ expectSatisfiable(
+ solve({X, NotY}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
+ Pair(Y, Solver::Result::Assignment::AssignedFalse)));
+}
+
+TEST(SolverTest, Top) {
+ ConstraintContext Ctx;
+ auto X = Ctx.top();
+
+ // X. Since Top is anonymous, we do not get any results in the solution.
+ expectSatisfiable(solve({X}), IsEmpty());
+}
+
+TEST(SolverTest, NegatedTop) {
+ ConstraintContext Ctx;
+ auto X = Ctx.top();
+
+ // !X
+ expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
+}
+
+TEST(SolverTest, DistinctTops) {
+ ConstraintContext Ctx;
+ auto X = Ctx.top();
+ auto Y = Ctx.top();
+ auto NotY = Ctx.neg(Y);
+
+ // X ^ !Y
+ expectSatisfiable(solve({X, NotY}), IsEmpty());
}
TEST(SolverTest, DoubleNegation) {
@@ -98,7 +121,7 @@ TEST(SolverTest, DoubleNegation) {
auto NotNotX = Ctx.neg(NotX);
// !!X ^ !X
- EXPECT_THAT(solve({NotNotX, NotX}), unsat());
+ expectUnsatisfiable(solve({NotNotX, NotX}));
}
TEST(SolverTest, NegatedDisjunction) {
@@ -109,7 +132,7 @@ TEST(SolverTest, NegatedDisjunction) {
auto NotXOrY = Ctx.neg(XOrY);
// !(X v Y) ^ (X v Y)
- EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
+ expectUnsatisfiable(solve({NotXOrY, XOrY}));
}
TEST(SolverTest, NegatedConjunction) {
@@ -120,7 +143,7 @@ TEST(SolverTest, NegatedConjunction) {
auto NotXAndY = Ctx.neg(XAndY);
// !(X ^ Y) ^ (X ^ Y)
- EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
+ expectUnsatisfiable(solve({NotXAndY, XAndY}));
}
TEST(SolverTest, DisjunctionSameVarWithNegation) {
@@ -130,7 +153,7 @@ TEST(SolverTest, DisjunctionSameVarWithNegation) {
auto XOrNotX = Ctx.disj(X, NotX);
// X v !X
- EXPECT_THAT(solve({XOrNotX}), sat(_));
+ expectSatisfiable(solve({XOrNotX}), _);
}
TEST(SolverTest, DisjunctionSameVar) {
@@ -139,7 +162,7 @@ TEST(SolverTest, DisjunctionSameVar) {
auto XOrX = Ctx.disj(X, X);
// X v X
- EXPECT_THAT(solve({XOrX}), sat(_));
+ expectSatisfiable(solve({XOrX}), _);
}
TEST(SolverTest, ConjunctionSameVarsConflict) {
@@ -149,7 +172,7 @@ TEST(SolverTest, ConjunctionSameVarsConflict) {
auto XAndNotX = Ctx.conj(X, NotX);
// X ^ !X
- EXPECT_THAT(solve({XAndNotX}), unsat());
+ expectUnsatisfiable(solve({XAndNotX}));
}
TEST(SolverTest, ConjunctionSameVar) {
@@ -158,7 +181,7 @@ TEST(SolverTest, ConjunctionSameVar) {
auto XAndX = Ctx.conj(X, X);
// X ^ X
- EXPECT_THAT(solve({XAndX}), sat(_));
+ expectSatisfiable(solve({XAndX}), _);
}
TEST(SolverTest, PureVar) {
@@ -171,9 +194,10 @@ TEST(SolverTest, PureVar) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
- EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
- Pair(Y->getAtom(), _))));
+ expectSatisfiable(
+ solve({NotXOrY, NotXOrNotY}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
+ Pair(Y, _)));
}
TEST(SolverTest, MustAssumeVarIsFalse) {
@@ -187,9 +211,10 @@ TEST(SolverTest, MustAssumeVarIsFalse) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
- EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
- Pair(Y->getAtom(), AssignedTrue))));
+ expectSatisfiable(
+ solve({XOrY, NotXOrY, NotXOrNotY}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
+ Pair(Y, Solver::Result::Assignment::AssignedTrue)));
}
TEST(SolverTest, DeepConflict) {
@@ -204,7 +229,7 @@ TEST(SolverTest, DeepConflict) {
auto XOrNotY = Ctx.disj(X, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
- EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
+ expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
}
TEST(SolverTest, IffIsEquivalentToDNF) {
@@ -218,7 +243,7 @@ TEST(SolverTest, IffIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
// !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
- EXPECT_THAT(solve({NotEquivalent}), unsat());
+ expectUnsatisfiable(solve({NotEquivalent}));
}
TEST(SolverTest, IffSameVars) {
@@ -227,7 +252,7 @@ TEST(SolverTest, IffSameVars) {
auto XEqX = Ctx.iff(X, X);
// X <=> X
- EXPECT_THAT(solve({XEqX}), sat(_));
+ expectSatisfiable(solve({XEqX}), _);
}
TEST(SolverTest, IffDistinctVars) {
@@ -237,12 +262,14 @@ TEST(SolverTest, IffDistinctVars) {
auto XEqY = Ctx.iff(X, Y);
// X <=> Y
- EXPECT_THAT(
+ expectSatisfiable(
solve({XEqY}),
- sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
- Pair(Y->getAtom(), AssignedTrue)),
- UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
- Pair(Y->getAtom(), AssignedFalse)))));
+ 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(SolverTest, IffWithUnits) {
@@ -252,9 +279,10 @@ TEST(SolverTest, IffWithUnits) {
auto XEqY = Ctx.iff(X, Y);
// (X <=> Y) ^ X ^ Y
- EXPECT_THAT(solve({XEqY, X, Y}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
- Pair(Y->getAtom(), AssignedTrue))));
+ expectSatisfiable(
+ solve({XEqY, X, Y}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
+ Pair(Y, Solver::Result::Assignment::AssignedTrue)));
}
TEST(SolverTest, IffWithUnitsConflict) {
@@ -265,7 +293,7 @@ TEST(SolverTest, IffWithUnitsConflict) {
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X !Y
- EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
+ expectUnsatisfiable(solve({XEqY, X, NotY}));
}
TEST(SolverTest, IffTransitiveConflict) {
@@ -278,7 +306,7 @@ TEST(SolverTest, IffTransitiveConflict) {
auto NotX = Ctx.neg(X);
// (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
- EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat());
+ expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
}
TEST(SolverTest, DeMorgan) {
@@ -295,7 +323,7 @@ TEST(SolverTest, DeMorgan) {
auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
// A ^ B
- EXPECT_THAT(solve({A, B}), sat(_));
+ expectSatisfiable(solve({A, B}), _);
}
TEST(SolverTest, RespectsAdditionalConstraints) {
@@ -306,7 +334,7 @@ TEST(SolverTest, RespectsAdditionalConstraints) {
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X ^ !Y
- EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
+ expectUnsatisfiable(solve({XEqY, X, NotY}));
}
TEST(SolverTest, ImplicationIsEquivalentToDNF) {
@@ -318,7 +346,7 @@ TEST(SolverTest, ImplicationIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
// !((X => Y) <=> (!X v Y))
- EXPECT_THAT(solve({NotEquivalent}), unsat());
+ expectUnsatisfiable(solve({NotEquivalent}));
}
TEST(SolverTest, ImplicationConflict) {
@@ -329,7 +357,7 @@ TEST(SolverTest, ImplicationConflict) {
auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
// X => Y ^ X ^ !Y
- EXPECT_THAT(solve({XImplY, XAndNotY}), unsat());
+ expectUnsatisfiable(solve({XImplY, XAndNotY}));
}
TEST(SolverTest, LowTimeoutResultsInTimedOut) {
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
index 93991d87d77f20..e258eb7e75f592 100644
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -43,7 +43,6 @@
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringMap.h"
#include "llvm/ADT/StringRef.h"
-#include "llvm/Support/Allocator.h"
#include "llvm/Support/Errc.h"
#include "llvm/Support/Error.h"
#include "llvm/Testing/Annotations/Annotations.h"
@@ -443,44 +442,55 @@ ValueT &getValueForDecl(ASTContext &ASTCtx, const Environment &Env,
/// Creates and owns constraints which are boolean values.
class ConstraintContext {
- unsigned NextAtom = 0;
- llvm::BumpPtrAllocator A;
-
- const Formula *make(Formula::Kind K,
- llvm::ArrayRef<const Formula *> Operands) {
- return &Formula::create(A, K, Operands);
+public:
+ // Creates an atomic boolean value.
+ BoolValue *atom() {
+ Vals.push_back(std::make_unique<AtomicBoolValue>());
+ return Vals.back().get();
}
-public:
- // Returns a reference to a fresh atomic variable.
- const Formula *atom() {
- return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
+ // Creates an instance of the Top boolean value.
+ BoolValue *top() {
+ Vals.push_back(std::make_unique<TopBoolValue>());
+ return Vals.back().get();
}
- // Creates a boolean conjunction.
- const Formula *conj(const Formula *LHS, const Formula *RHS) {
- return make(Formula::And, {LHS, RHS});
+ // 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.
- const Formula *disj(const Formula *LHS, const Formula *RHS) {
- return make(Formula::Or, {LHS, RHS});
+ // 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.
- const Formula *neg(const Formula *Operand) {
- return make(Formula::Not, {Operand});
+ // 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.
- const Formula *impl(const Formula *LHS, const Formula *RHS) {
- return make(Formula::Implies, {LHS, RHS});
+ // Creates a boolean implication value.
+ BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ Vals.push_back(
+ std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal));
+ return Vals.back().get();
}
- // Creates a boolean biconditional.
- const Formula *iff(const Formula *LHS, const Formula *RHS) {
- return make(Formula::Equal, {LHS, RHS});
+ // Creates a boolean biconditional value.
+ BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ Vals.push_back(
+ std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
+ return Vals.back().get();
}
+
+private:
+ std::vector<std::unique_ptr<BoolValue>> Vals;
};
} // namespace test
More information about the cfe-commits
mailing list