1 //===- DebugSupport.cpp -----------------------------------------*- C++ -*-===// 2 // 3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4 // See https://llvm.org/LICENSE.txt for license information. 5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6 // 7 //===----------------------------------------------------------------------===// 8 // 9 // This file defines functions which generate more readable forms of data 10 // structures used in the dataflow analyses, for debugging purposes. 11 // 12 //===----------------------------------------------------------------------===// 13 14 #include <utility> 15 16 #include "clang/Analysis/FlowSensitive/DebugSupport.h" 17 #include "clang/Analysis/FlowSensitive/Solver.h" 18 #include "clang/Analysis/FlowSensitive/Value.h" 19 #include "llvm/ADT/DenseMap.h" 20 #include "llvm/ADT/STLExtras.h" 21 #include "llvm/ADT/StringSet.h" 22 #include "llvm/Support/ErrorHandling.h" 23 #include "llvm/Support/FormatAdapters.h" 24 #include "llvm/Support/FormatCommon.h" 25 #include "llvm/Support/FormatVariadic.h" 26 27 namespace clang { 28 namespace dataflow { 29 30 using llvm::AlignStyle; 31 using llvm::fmt_pad; 32 using llvm::formatv; 33 34 std::string debugString(Solver::Result::Assignment Assignment) { 35 switch (Assignment) { 36 case Solver::Result::Assignment::AssignedFalse: 37 return "False"; 38 case Solver::Result::Assignment::AssignedTrue: 39 return "True"; 40 } 41 llvm_unreachable("Booleans can only be assigned true/false"); 42 } 43 44 std::string debugString(Solver::Result::Status Status) { 45 switch (Status) { 46 case Solver::Result::Status::Satisfiable: 47 return "Satisfiable"; 48 case Solver::Result::Status::Unsatisfiable: 49 return "Unsatisfiable"; 50 case Solver::Result::Status::TimedOut: 51 return "TimedOut"; 52 } 53 llvm_unreachable("Unhandled SAT check result status"); 54 } 55 56 namespace { 57 58 class DebugStringGenerator { 59 public: 60 explicit DebugStringGenerator( 61 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg) 62 : Counter(0), AtomNames(std::move(AtomNamesArg)) { 63 #ifndef NDEBUG 64 llvm::StringSet<> Names; 65 for (auto &N : AtomNames) { 66 assert(Names.insert(N.second).second && 67 "The same name must not assigned to different atoms"); 68 } 69 #endif 70 } 71 72 /// Returns a string representation of a boolean value `B`. 73 std::string debugString(const BoolValue &B, size_t Depth = 0) { 74 std::string S; 75 switch (B.getKind()) { 76 case Value::Kind::AtomicBool: { 77 S = getAtomName(&cast<AtomicBoolValue>(B)); 78 break; 79 } 80 case Value::Kind::Conjunction: { 81 auto &C = cast<ConjunctionValue>(B); 82 auto L = debugString(C.getLeftSubValue(), Depth + 1); 83 auto R = debugString(C.getRightSubValue(), Depth + 1); 84 S = formatv("(and\n{0}\n{1})", L, R); 85 break; 86 } 87 case Value::Kind::Disjunction: { 88 auto &D = cast<DisjunctionValue>(B); 89 auto L = debugString(D.getLeftSubValue(), Depth + 1); 90 auto R = debugString(D.getRightSubValue(), Depth + 1); 91 S = formatv("(or\n{0}\n{1})", L, R); 92 break; 93 } 94 case Value::Kind::Negation: { 95 auto &N = cast<NegationValue>(B); 96 S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1)); 97 break; 98 } 99 default: 100 llvm_unreachable("Unhandled value kind"); 101 } 102 auto Indent = Depth * 4; 103 return formatv("{0}", fmt_pad(S, Indent, 0)); 104 } 105 106 std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) { 107 std::vector<std::string> ConstraintsStrings; 108 ConstraintsStrings.reserve(Constraints.size()); 109 for (BoolValue *Constraint : Constraints) { 110 ConstraintsStrings.push_back(debugString(*Constraint)); 111 } 112 llvm::sort(ConstraintsStrings); 113 114 std::string Result; 115 for (const std::string &S : ConstraintsStrings) { 116 Result += S; 117 Result += '\n'; 118 } 119 return Result; 120 } 121 122 /// Returns a string representation of a set of boolean `Constraints` and the 123 /// `Result` of satisfiability checking on the `Constraints`. 124 std::string debugString(ArrayRef<BoolValue *> &Constraints, 125 const Solver::Result &Result) { 126 auto Template = R"( 127 Constraints 128 ------------ 129 {0:$[ 130 131 ]} 132 ------------ 133 {1}. 134 {2} 135 )"; 136 137 std::vector<std::string> ConstraintsStrings; 138 ConstraintsStrings.reserve(Constraints.size()); 139 for (auto &Constraint : Constraints) { 140 ConstraintsStrings.push_back(debugString(*Constraint)); 141 } 142 143 auto StatusString = clang::dataflow::debugString(Result.getStatus()); 144 auto Solution = Result.getSolution(); 145 auto SolutionString = Solution ? "\n" + debugString(Solution.value()) : ""; 146 147 return formatv( 148 Template, 149 llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()), 150 StatusString, SolutionString); 151 } 152 153 private: 154 /// Returns a string representation of a truth assignment to atom booleans. 155 std::string debugString( 156 const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> 157 &AtomAssignments) { 158 size_t MaxNameLength = 0; 159 for (auto &AtomName : AtomNames) { 160 MaxNameLength = std::max(MaxNameLength, AtomName.second.size()); 161 } 162 163 std::vector<std::string> Lines; 164 for (auto &AtomAssignment : AtomAssignments) { 165 auto Line = formatv("{0} = {1}", 166 fmt_align(getAtomName(AtomAssignment.first), 167 AlignStyle::Left, MaxNameLength), 168 clang::dataflow::debugString(AtomAssignment.second)); 169 Lines.push_back(Line); 170 } 171 llvm::sort(Lines); 172 173 return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end())); 174 } 175 176 /// Returns the name assigned to `Atom`, either user-specified or created by 177 /// default rules (B0, B1, ...). 178 std::string getAtomName(const AtomicBoolValue *Atom) { 179 auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter)); 180 if (Entry.second) { 181 Counter++; 182 } 183 return Entry.first->second; 184 } 185 186 // Keep track of number of atoms without a user-specified name, used to assign 187 // non-repeating default names to such atoms. 188 size_t Counter; 189 190 // Keep track of names assigned to atoms. 191 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames; 192 }; 193 194 } // namespace 195 196 std::string 197 debugString(const BoolValue &B, 198 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 199 return DebugStringGenerator(std::move(AtomNames)).debugString(B); 200 } 201 202 std::string 203 debugString(const llvm::DenseSet<BoolValue *> &Constraints, 204 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 205 return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints); 206 } 207 208 std::string 209 debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, 210 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 211 return DebugStringGenerator(std::move(AtomNames)) 212 .debugString(Constraints, Result); 213 } 214 215 } // namespace dataflow 216 } // namespace clang 217