diff options
Diffstat (limited to 'contrib/llvm-project/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp')
| -rw-r--r-- | contrib/llvm-project/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp | 208 |
1 files changed, 15 insertions, 193 deletions
diff --git a/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp index d4886f154b33..f8a049adea5e 100644 --- a/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -16,22 +16,12 @@ #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: @@ -46,26 +36,19 @@ llvm::StringRef debugString(Value::Kind Kind) { return "AtomicBool"; case Value::Kind::TopBool: return "TopBool"; - case Value::Kind::Conjunction: - return "Conjunction"; - case Value::Kind::Disjunction: - return "Disjunction"; - case Value::Kind::Negation: - return "Negation"; - case Value::Kind::Implication: - return "Implication"; - case Value::Kind::Biconditional: - return "Biconditional"; + case Value::Kind::FormulaBool: + return "FormulaBool"; } llvm_unreachable("Unhandled value kind"); } -llvm::StringRef debugString(Solver::Result::Assignment Assignment) { +llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, + Solver::Result::Assignment Assignment) { switch (Assignment) { case Solver::Result::Assignment::AssignedFalse: - return "False"; + return OS << "False"; case Solver::Result::Assignment::AssignedTrue: - return "True"; + return OS << "True"; } llvm_unreachable("Booleans can only be assigned true/false"); } @@ -82,177 +65,16 @@ llvm::StringRef debugString(Solver::Result::Status Status) { llvm_unreachable("Unhandled SAT check result status"); } -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 different 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::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::DenseSet<BoolValue *> &Constraints) { - std::vector<std::string> ConstraintsStrings; - ConstraintsStrings.reserve(Constraints.size()); - for (BoolValue *Constraint : Constraints) { - ConstraintsStrings.push_back(debugString(*Constraint)); - } - llvm::sort(ConstraintsStrings); - - std::string Result; - for (const std::string &S : ConstraintsStrings) { - Result += S; - Result += '\n'; - } - return Result; +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"; } - - /// 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())); - } - - /// 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(const llvm::DenseSet<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); + return OS; } } // namespace dataflow |
