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