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