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/StringRef.h" 22 #include "llvm/ADT/StringSet.h" 23 #include "llvm/Support/ErrorHandling.h" 24 #include "llvm/Support/FormatAdapters.h" 25 #include "llvm/Support/FormatCommon.h" 26 #include "llvm/Support/FormatVariadic.h" 27 28 namespace clang { 29 namespace dataflow { 30 31 using llvm::AlignStyle; 32 using llvm::fmt_pad; 33 using llvm::formatv; 34 35 llvm::StringRef debugString(Value::Kind Kind) { 36 switch (Kind) { 37 case Value::Kind::Integer: 38 return "Integer"; 39 case Value::Kind::Reference: 40 return "Reference"; 41 case Value::Kind::Pointer: 42 return "Pointer"; 43 case Value::Kind::Struct: 44 return "Struct"; 45 case Value::Kind::AtomicBool: 46 return "AtomicBool"; 47 case Value::Kind::TopBool: 48 return "TopBool"; 49 case Value::Kind::Conjunction: 50 return "Conjunction"; 51 case Value::Kind::Disjunction: 52 return "Disjunction"; 53 case Value::Kind::Negation: 54 return "Negation"; 55 case Value::Kind::Implication: 56 return "Implication"; 57 case Value::Kind::Biconditional: 58 return "Biconditional"; 59 } 60 llvm_unreachable("Unhandled value kind"); 61 } 62 63 llvm::StringRef debugString(Solver::Result::Assignment Assignment) { 64 switch (Assignment) { 65 case Solver::Result::Assignment::AssignedFalse: 66 return "False"; 67 case Solver::Result::Assignment::AssignedTrue: 68 return "True"; 69 } 70 llvm_unreachable("Booleans can only be assigned true/false"); 71 } 72 73 llvm::StringRef debugString(Solver::Result::Status Status) { 74 switch (Status) { 75 case Solver::Result::Status::Satisfiable: 76 return "Satisfiable"; 77 case Solver::Result::Status::Unsatisfiable: 78 return "Unsatisfiable"; 79 case Solver::Result::Status::TimedOut: 80 return "TimedOut"; 81 } 82 llvm_unreachable("Unhandled SAT check result status"); 83 } 84 85 namespace { 86 87 class DebugStringGenerator { 88 public: 89 explicit DebugStringGenerator( 90 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg) 91 : Counter(0), AtomNames(std::move(AtomNamesArg)) { 92 #ifndef NDEBUG 93 llvm::StringSet<> Names; 94 for (auto &N : AtomNames) { 95 assert(Names.insert(N.second).second && 96 "The same name must not assigned to different atoms"); 97 } 98 #endif 99 } 100 101 /// Returns a string representation of a boolean value `B`. 102 std::string debugString(const BoolValue &B, size_t Depth = 0) { 103 std::string S; 104 switch (B.getKind()) { 105 case Value::Kind::AtomicBool: { 106 S = getAtomName(&cast<AtomicBoolValue>(B)); 107 break; 108 } 109 case Value::Kind::TopBool: { 110 S = "top"; 111 break; 112 } 113 case Value::Kind::Conjunction: { 114 auto &C = cast<ConjunctionValue>(B); 115 auto L = debugString(C.getLeftSubValue(), Depth + 1); 116 auto R = debugString(C.getRightSubValue(), Depth + 1); 117 S = formatv("(and\n{0}\n{1})", L, R); 118 break; 119 } 120 case Value::Kind::Disjunction: { 121 auto &D = cast<DisjunctionValue>(B); 122 auto L = debugString(D.getLeftSubValue(), Depth + 1); 123 auto R = debugString(D.getRightSubValue(), Depth + 1); 124 S = formatv("(or\n{0}\n{1})", L, R); 125 break; 126 } 127 case Value::Kind::Negation: { 128 auto &N = cast<NegationValue>(B); 129 S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1)); 130 break; 131 } 132 case Value::Kind::Implication: { 133 auto &IV = cast<ImplicationValue>(B); 134 auto L = debugString(IV.getLeftSubValue(), Depth + 1); 135 auto R = debugString(IV.getRightSubValue(), Depth + 1); 136 S = formatv("(=>\n{0}\n{1})", L, R); 137 break; 138 } 139 case Value::Kind::Biconditional: { 140 auto &BV = cast<BiconditionalValue>(B); 141 auto L = debugString(BV.getLeftSubValue(), Depth + 1); 142 auto R = debugString(BV.getRightSubValue(), Depth + 1); 143 S = formatv("(=\n{0}\n{1})", L, R); 144 break; 145 } 146 default: 147 llvm_unreachable("Unhandled value kind"); 148 } 149 auto Indent = Depth * 4; 150 return formatv("{0}", fmt_pad(S, Indent, 0)); 151 } 152 153 std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) { 154 std::string Result; 155 for (const BoolValue *S : Constraints) { 156 Result += debugString(*S); 157 Result += '\n'; 158 } 159 return Result; 160 } 161 162 /// Returns a string representation of a set of boolean `Constraints` and the 163 /// `Result` of satisfiability checking on the `Constraints`. 164 std::string debugString(ArrayRef<BoolValue *> &Constraints, 165 const Solver::Result &Result) { 166 auto Template = R"( 167 Constraints 168 ------------ 169 {0:$[ 170 171 ]} 172 ------------ 173 {1}. 174 {2} 175 )"; 176 177 std::vector<std::string> ConstraintsStrings; 178 ConstraintsStrings.reserve(Constraints.size()); 179 for (auto &Constraint : Constraints) { 180 ConstraintsStrings.push_back(debugString(*Constraint)); 181 } 182 183 auto StatusString = clang::dataflow::debugString(Result.getStatus()); 184 auto Solution = Result.getSolution(); 185 auto SolutionString = Solution ? "\n" + debugString(*Solution) : ""; 186 187 return formatv( 188 Template, 189 llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()), 190 StatusString, SolutionString); 191 } 192 193 private: 194 /// Returns a string representation of a truth assignment to atom booleans. 195 std::string debugString( 196 const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> 197 &AtomAssignments) { 198 size_t MaxNameLength = 0; 199 for (auto &AtomName : AtomNames) { 200 MaxNameLength = std::max(MaxNameLength, AtomName.second.size()); 201 } 202 203 std::vector<std::string> Lines; 204 for (auto &AtomAssignment : AtomAssignments) { 205 auto Line = formatv("{0} = {1}", 206 fmt_align(getAtomName(AtomAssignment.first), 207 AlignStyle::Left, MaxNameLength), 208 clang::dataflow::debugString(AtomAssignment.second)); 209 Lines.push_back(Line); 210 } 211 llvm::sort(Lines); 212 213 return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end())); 214 } 215 216 /// Returns the name assigned to `Atom`, either user-specified or created by 217 /// default rules (B0, B1, ...). 218 std::string getAtomName(const AtomicBoolValue *Atom) { 219 auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter)); 220 if (Entry.second) { 221 Counter++; 222 } 223 return Entry.first->second; 224 } 225 226 // Keep track of number of atoms without a user-specified name, used to assign 227 // non-repeating default names to such atoms. 228 size_t Counter; 229 230 // Keep track of names assigned to atoms. 231 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames; 232 }; 233 234 } // namespace 235 236 std::string 237 debugString(const BoolValue &B, 238 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 239 return DebugStringGenerator(std::move(AtomNames)).debugString(B); 240 } 241 242 std::string 243 debugString(llvm::ArrayRef<BoolValue *> Constraints, 244 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 245 return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints); 246 } 247 248 std::string 249 debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, 250 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 251 return DebugStringGenerator(std::move(AtomNames)) 252 .debugString(Constraints, Result); 253 } 254 255 } // namespace dataflow 256 } // namespace clang 257