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::Conjunction: { 110 auto &C = cast<ConjunctionValue>(B); 111 auto L = debugString(C.getLeftSubValue(), Depth + 1); 112 auto R = debugString(C.getRightSubValue(), Depth + 1); 113 S = formatv("(and\n{0}\n{1})", L, R); 114 break; 115 } 116 case Value::Kind::Disjunction: { 117 auto &D = cast<DisjunctionValue>(B); 118 auto L = debugString(D.getLeftSubValue(), Depth + 1); 119 auto R = debugString(D.getRightSubValue(), Depth + 1); 120 S = formatv("(or\n{0}\n{1})", L, R); 121 break; 122 } 123 case Value::Kind::Negation: { 124 auto &N = cast<NegationValue>(B); 125 S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1)); 126 break; 127 } 128 case Value::Kind::Implication: { 129 auto &IV = cast<ImplicationValue>(B); 130 auto L = debugString(IV.getLeftSubValue(), Depth + 1); 131 auto R = debugString(IV.getRightSubValue(), Depth + 1); 132 S = formatv("(=>\n{0}\n{1})", L, R); 133 break; 134 } 135 case Value::Kind::Biconditional: { 136 auto &BV = cast<BiconditionalValue>(B); 137 auto L = debugString(BV.getLeftSubValue(), Depth + 1); 138 auto R = debugString(BV.getRightSubValue(), Depth + 1); 139 S = formatv("(=\n{0}\n{1})", L, R); 140 break; 141 } 142 default: 143 llvm_unreachable("Unhandled value kind"); 144 } 145 auto Indent = Depth * 4; 146 return formatv("{0}", fmt_pad(S, Indent, 0)); 147 } 148 149 std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) { 150 std::vector<std::string> ConstraintsStrings; 151 ConstraintsStrings.reserve(Constraints.size()); 152 for (BoolValue *Constraint : Constraints) { 153 ConstraintsStrings.push_back(debugString(*Constraint)); 154 } 155 llvm::sort(ConstraintsStrings); 156 157 std::string Result; 158 for (const std::string &S : ConstraintsStrings) { 159 Result += S; 160 Result += '\n'; 161 } 162 return Result; 163 } 164 165 /// Returns a string representation of a set of boolean `Constraints` and the 166 /// `Result` of satisfiability checking on the `Constraints`. 167 std::string debugString(ArrayRef<BoolValue *> &Constraints, 168 const Solver::Result &Result) { 169 auto Template = R"( 170 Constraints 171 ------------ 172 {0:$[ 173 174 ]} 175 ------------ 176 {1}. 177 {2} 178 )"; 179 180 std::vector<std::string> ConstraintsStrings; 181 ConstraintsStrings.reserve(Constraints.size()); 182 for (auto &Constraint : Constraints) { 183 ConstraintsStrings.push_back(debugString(*Constraint)); 184 } 185 186 auto StatusString = clang::dataflow::debugString(Result.getStatus()); 187 auto Solution = Result.getSolution(); 188 auto SolutionString = Solution ? "\n" + debugString(*Solution) : ""; 189 190 return formatv( 191 Template, 192 llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()), 193 StatusString, SolutionString); 194 } 195 196 private: 197 /// Returns a string representation of a truth assignment to atom booleans. 198 std::string debugString( 199 const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> 200 &AtomAssignments) { 201 size_t MaxNameLength = 0; 202 for (auto &AtomName : AtomNames) { 203 MaxNameLength = std::max(MaxNameLength, AtomName.second.size()); 204 } 205 206 std::vector<std::string> Lines; 207 for (auto &AtomAssignment : AtomAssignments) { 208 auto Line = formatv("{0} = {1}", 209 fmt_align(getAtomName(AtomAssignment.first), 210 AlignStyle::Left, MaxNameLength), 211 clang::dataflow::debugString(AtomAssignment.second)); 212 Lines.push_back(Line); 213 } 214 llvm::sort(Lines); 215 216 return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end())); 217 } 218 219 /// Returns the name assigned to `Atom`, either user-specified or created by 220 /// default rules (B0, B1, ...). 221 std::string getAtomName(const AtomicBoolValue *Atom) { 222 auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter)); 223 if (Entry.second) { 224 Counter++; 225 } 226 return Entry.first->second; 227 } 228 229 // Keep track of number of atoms without a user-specified name, used to assign 230 // non-repeating default names to such atoms. 231 size_t Counter; 232 233 // Keep track of names assigned to atoms. 234 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames; 235 }; 236 237 } // namespace 238 239 std::string 240 debugString(const BoolValue &B, 241 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 242 return DebugStringGenerator(std::move(AtomNames)).debugString(B); 243 } 244 245 std::string 246 debugString(const llvm::DenseSet<BoolValue *> &Constraints, 247 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 248 return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints); 249 } 250 251 std::string 252 debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, 253 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { 254 return DebugStringGenerator(std::move(AtomNames)) 255 .debugString(Constraints, Result); 256 } 257 258 } // namespace dataflow 259 } // namespace clang 260