1753f127fSDimitry Andric //===- DebugSupport.cpp -----------------------------------------*- C++ -*-===// 2753f127fSDimitry Andric // 3753f127fSDimitry Andric // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4753f127fSDimitry Andric // See https://llvm.org/LICENSE.txt for license information. 5753f127fSDimitry Andric // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6753f127fSDimitry Andric // 7753f127fSDimitry Andric //===----------------------------------------------------------------------===// 8753f127fSDimitry Andric // 9753f127fSDimitry Andric // This file defines functions which generate more readable forms of data 10753f127fSDimitry Andric // structures used in the dataflow analyses, for debugging purposes. 11753f127fSDimitry Andric // 12753f127fSDimitry Andric //===----------------------------------------------------------------------===// 13753f127fSDimitry Andric 14753f127fSDimitry Andric #include <utility> 15753f127fSDimitry Andric 16753f127fSDimitry Andric #include "clang/Analysis/FlowSensitive/DebugSupport.h" 17753f127fSDimitry Andric #include "clang/Analysis/FlowSensitive/Solver.h" 18753f127fSDimitry Andric #include "clang/Analysis/FlowSensitive/Value.h" 19753f127fSDimitry Andric #include "llvm/ADT/DenseMap.h" 20*fcaf7f86SDimitry Andric #include "llvm/ADT/STLExtras.h" 21753f127fSDimitry Andric #include "llvm/ADT/StringSet.h" 22753f127fSDimitry Andric #include "llvm/Support/ErrorHandling.h" 23753f127fSDimitry Andric #include "llvm/Support/FormatAdapters.h" 24753f127fSDimitry Andric #include "llvm/Support/FormatCommon.h" 25753f127fSDimitry Andric #include "llvm/Support/FormatVariadic.h" 26753f127fSDimitry Andric 27753f127fSDimitry Andric namespace clang { 28753f127fSDimitry Andric namespace dataflow { 29753f127fSDimitry Andric 30753f127fSDimitry Andric using llvm::AlignStyle; 31753f127fSDimitry Andric using llvm::fmt_pad; 32753f127fSDimitry Andric using llvm::formatv; 33753f127fSDimitry Andric 34*fcaf7f86SDimitry Andric std::string debugString(Solver::Result::Assignment Assignment) { 35*fcaf7f86SDimitry Andric switch (Assignment) { 36*fcaf7f86SDimitry Andric case Solver::Result::Assignment::AssignedFalse: 37*fcaf7f86SDimitry Andric return "False"; 38*fcaf7f86SDimitry Andric case Solver::Result::Assignment::AssignedTrue: 39*fcaf7f86SDimitry Andric return "True"; 40*fcaf7f86SDimitry Andric } 41*fcaf7f86SDimitry Andric llvm_unreachable("Booleans can only be assigned true/false"); 42*fcaf7f86SDimitry Andric } 43*fcaf7f86SDimitry Andric 44*fcaf7f86SDimitry Andric std::string debugString(Solver::Result::Status Status) { 45*fcaf7f86SDimitry Andric switch (Status) { 46*fcaf7f86SDimitry Andric case Solver::Result::Status::Satisfiable: 47*fcaf7f86SDimitry Andric return "Satisfiable"; 48*fcaf7f86SDimitry Andric case Solver::Result::Status::Unsatisfiable: 49*fcaf7f86SDimitry Andric return "Unsatisfiable"; 50*fcaf7f86SDimitry Andric case Solver::Result::Status::TimedOut: 51*fcaf7f86SDimitry Andric return "TimedOut"; 52*fcaf7f86SDimitry Andric } 53*fcaf7f86SDimitry Andric llvm_unreachable("Unhandled SAT check result status"); 54*fcaf7f86SDimitry Andric } 55*fcaf7f86SDimitry Andric 56753f127fSDimitry Andric namespace { 57753f127fSDimitry Andric 58753f127fSDimitry Andric class DebugStringGenerator { 59753f127fSDimitry Andric public: 60753f127fSDimitry Andric explicit DebugStringGenerator( 61753f127fSDimitry Andric llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg) 62753f127fSDimitry Andric : Counter(0), AtomNames(std::move(AtomNamesArg)) { 63753f127fSDimitry Andric #ifndef NDEBUG 64753f127fSDimitry Andric llvm::StringSet<> Names; 65753f127fSDimitry Andric for (auto &N : AtomNames) { 66753f127fSDimitry Andric assert(Names.insert(N.second).second && 67753f127fSDimitry Andric "The same name must not assigned to different atoms"); 68753f127fSDimitry Andric } 69753f127fSDimitry Andric #endif 70753f127fSDimitry Andric } 71753f127fSDimitry Andric 72753f127fSDimitry Andric /// Returns a string representation of a boolean value `B`. 73753f127fSDimitry Andric std::string debugString(const BoolValue &B, size_t Depth = 0) { 74753f127fSDimitry Andric std::string S; 75753f127fSDimitry Andric switch (B.getKind()) { 76753f127fSDimitry Andric case Value::Kind::AtomicBool: { 77753f127fSDimitry Andric S = getAtomName(&cast<AtomicBoolValue>(B)); 78753f127fSDimitry Andric break; 79753f127fSDimitry Andric } 80753f127fSDimitry Andric case Value::Kind::Conjunction: { 81753f127fSDimitry Andric auto &C = cast<ConjunctionValue>(B); 82753f127fSDimitry Andric auto L = debugString(C.getLeftSubValue(), Depth + 1); 83753f127fSDimitry Andric auto R = debugString(C.getRightSubValue(), Depth + 1); 84753f127fSDimitry Andric S = formatv("(and\n{0}\n{1})", L, R); 85753f127fSDimitry Andric break; 86753f127fSDimitry Andric } 87753f127fSDimitry Andric case Value::Kind::Disjunction: { 88753f127fSDimitry Andric auto &D = cast<DisjunctionValue>(B); 89753f127fSDimitry Andric auto L = debugString(D.getLeftSubValue(), Depth + 1); 90753f127fSDimitry Andric auto R = debugString(D.getRightSubValue(), Depth + 1); 91753f127fSDimitry Andric S = formatv("(or\n{0}\n{1})", L, R); 92753f127fSDimitry Andric break; 93753f127fSDimitry Andric } 94753f127fSDimitry Andric case Value::Kind::Negation: { 95753f127fSDimitry Andric auto &N = cast<NegationValue>(B); 96753f127fSDimitry Andric S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1)); 97753f127fSDimitry Andric break; 98753f127fSDimitry Andric } 99753f127fSDimitry Andric default: 100753f127fSDimitry Andric llvm_unreachable("Unhandled value kind"); 101753f127fSDimitry Andric } 102753f127fSDimitry Andric auto Indent = Depth * 4; 103753f127fSDimitry Andric return formatv("{0}", fmt_pad(S, Indent, 0)); 104753f127fSDimitry Andric } 105753f127fSDimitry Andric 106*fcaf7f86SDimitry Andric std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) { 107*fcaf7f86SDimitry Andric std::vector<std::string> ConstraintsStrings; 108*fcaf7f86SDimitry Andric ConstraintsStrings.reserve(Constraints.size()); 109*fcaf7f86SDimitry Andric for (BoolValue *Constraint : Constraints) { 110*fcaf7f86SDimitry Andric ConstraintsStrings.push_back(debugString(*Constraint)); 111*fcaf7f86SDimitry Andric } 112*fcaf7f86SDimitry Andric llvm::sort(ConstraintsStrings); 113*fcaf7f86SDimitry Andric 114*fcaf7f86SDimitry Andric std::string Result; 115*fcaf7f86SDimitry Andric for (const std::string &S : ConstraintsStrings) { 116*fcaf7f86SDimitry Andric Result += S; 117*fcaf7f86SDimitry Andric Result += '\n'; 118*fcaf7f86SDimitry Andric } 119*fcaf7f86SDimitry Andric return Result; 120*fcaf7f86SDimitry Andric } 121*fcaf7f86SDimitry Andric 122753f127fSDimitry Andric /// Returns a string representation of a set of boolean `Constraints` and the 123753f127fSDimitry Andric /// `Result` of satisfiability checking on the `Constraints`. 124*fcaf7f86SDimitry Andric std::string debugString(ArrayRef<BoolValue *> &Constraints, 125753f127fSDimitry Andric const Solver::Result &Result) { 126753f127fSDimitry Andric auto Template = R"( 127753f127fSDimitry Andric Constraints 128753f127fSDimitry Andric ------------ 129753f127fSDimitry Andric {0:$[ 130753f127fSDimitry Andric 131753f127fSDimitry Andric ]} 132753f127fSDimitry Andric ------------ 133753f127fSDimitry Andric {1}. 134753f127fSDimitry Andric {2} 135753f127fSDimitry Andric )"; 136753f127fSDimitry Andric 137753f127fSDimitry Andric std::vector<std::string> ConstraintsStrings; 138753f127fSDimitry Andric ConstraintsStrings.reserve(Constraints.size()); 139753f127fSDimitry Andric for (auto &Constraint : Constraints) { 140753f127fSDimitry Andric ConstraintsStrings.push_back(debugString(*Constraint)); 141753f127fSDimitry Andric } 142753f127fSDimitry Andric 143*fcaf7f86SDimitry Andric auto StatusString = clang::dataflow::debugString(Result.getStatus()); 144753f127fSDimitry Andric auto Solution = Result.getSolution(); 145*fcaf7f86SDimitry Andric auto SolutionString = Solution ? "\n" + debugString(Solution.value()) : ""; 146753f127fSDimitry Andric 147753f127fSDimitry Andric return formatv( 148753f127fSDimitry Andric Template, 149753f127fSDimitry Andric llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()), 150753f127fSDimitry Andric StatusString, SolutionString); 151753f127fSDimitry Andric } 152753f127fSDimitry Andric 153753f127fSDimitry Andric private: 154753f127fSDimitry Andric /// Returns a string representation of a truth assignment to atom booleans. 155753f127fSDimitry Andric std::string debugString( 156753f127fSDimitry Andric const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> 157753f127fSDimitry Andric &AtomAssignments) { 158753f127fSDimitry Andric size_t MaxNameLength = 0; 159753f127fSDimitry Andric for (auto &AtomName : AtomNames) { 160753f127fSDimitry Andric MaxNameLength = std::max(MaxNameLength, AtomName.second.size()); 161753f127fSDimitry Andric } 162753f127fSDimitry Andric 163753f127fSDimitry Andric std::vector<std::string> Lines; 164753f127fSDimitry Andric for (auto &AtomAssignment : AtomAssignments) { 165753f127fSDimitry Andric auto Line = formatv("{0} = {1}", 166753f127fSDimitry Andric fmt_align(getAtomName(AtomAssignment.first), 167753f127fSDimitry Andric AlignStyle::Left, MaxNameLength), 168*fcaf7f86SDimitry Andric clang::dataflow::debugString(AtomAssignment.second)); 169753f127fSDimitry Andric Lines.push_back(Line); 170753f127fSDimitry Andric } 171*fcaf7f86SDimitry Andric llvm::sort(Lines); 172753f127fSDimitry Andric 173753f127fSDimitry Andric return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end())); 174753f127fSDimitry Andric } 175753f127fSDimitry Andric 176753f127fSDimitry Andric /// Returns the name assigned to `Atom`, either user-specified or created by 177753f127fSDimitry Andric /// default rules (B0, B1, ...). 178753f127fSDimitry Andric std::string getAtomName(const AtomicBoolValue *Atom) { 179753f127fSDimitry Andric auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter)); 180753f127fSDimitry Andric if (Entry.second) { 181753f127fSDimitry Andric Counter++; 182753f127fSDimitry Andric } 183753f127fSDimitry Andric return Entry.first->second; 184753f127fSDimitry Andric } 185753f127fSDimitry Andric 186753f127fSDimitry Andric // Keep track of number of atoms without a user-specified name, used to assign 187753f127fSDimitry Andric // non-repeating default names to such atoms. 188753f127fSDimitry Andric size_t Counter; 189753f127fSDimitry Andric 190753f127fSDimitry Andric // Keep track of names assigned to atoms. 191753f127fSDimitry Andric llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames; 192753f127fSDimitry Andric }; 193753f127fSDimitry Andric 194753f127fSDimitry Andric } // namespace 195753f127fSDimitry Andric 196753f127fSDimitry Andric std::string 197753f127fSDimitry Andric debugString(const BoolValue &B, 198753f127fSDimitry Andric llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 199753f127fSDimitry Andric return DebugStringGenerator(std::move(AtomNames)).debugString(B); 200753f127fSDimitry Andric } 201753f127fSDimitry Andric 202753f127fSDimitry Andric std::string 203*fcaf7f86SDimitry Andric debugString(const llvm::DenseSet<BoolValue *> &Constraints, 204*fcaf7f86SDimitry Andric llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 205*fcaf7f86SDimitry Andric return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints); 206*fcaf7f86SDimitry Andric } 207*fcaf7f86SDimitry Andric 208*fcaf7f86SDimitry Andric std::string 209*fcaf7f86SDimitry Andric debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, 210753f127fSDimitry Andric llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 211753f127fSDimitry Andric return DebugStringGenerator(std::move(AtomNames)) 212753f127fSDimitry Andric .debugString(Constraints, Result); 213753f127fSDimitry Andric } 214753f127fSDimitry Andric 215753f127fSDimitry Andric } // namespace dataflow 216753f127fSDimitry Andric } // namespace clang 217