clang  16.0.0git
DebugSupport.cpp
Go to the documentation of this file.
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 
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) {
38  return "Integer";
40  return "Reference";
42  return "Pointer";
44  return "Struct";
46  return "AtomicBool";
48  return "Conjunction";
50  return "Disjunction";
52  return "Negation";
54  return "Implication";
56  return "Biconditional";
57  }
58  llvm_unreachable("Unhandled value kind");
59 }
60 
62  switch (Assignment) {
64  return "False";
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) {
74  return "Satisfiable";
76  return "Unsatisfiable";
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()) {
104  S = getAtomName(&cast<AtomicBoolValue>(B));
105  break;
106  }
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  }
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  }
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  }
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 
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.
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 
239  llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
240  return DebugStringGenerator(std::move(AtomNames)).debugString(B);
241 }
242 
245  llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
246  return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
247 }
248 
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
max
__DEVICE__ int max(int __a, int __b)
Definition: __clang_cuda_math.h:196
clang::dataflow::Solver::Result::Status::Unsatisfiable
@ Unsatisfiable
Indicates that there is no satisfying assignment for a boolean formula.
string
string(SUBSTRING ${CMAKE_CURRENT_BINARY_DIR} 0 ${PATH_LIB_START} PATH_HEAD) string(SUBSTRING $
Definition: CMakeLists.txt:22
AttributeLangSupport::C
@ C
Definition: SemaDeclAttr.cpp:55
clang::dataflow::Solver::Result::Status
Status
Definition: Solver.h:29
clang::dataflow::Solver::Result::Status::TimedOut
@ TimedOut
Indicates that the solver gave up trying to find a satisfying assignment for a boolean formula.
clang::prec::Assignment
@ Assignment
Definition: OperatorPrecedence.h:29
clang::dataflow::Value::Kind::Disjunction
@ Disjunction
DebugSupport.h
Solver.h
clang::dataflow::Value::Kind::Reference
@ Reference
Depth
int Depth
Definition: ASTDiff.cpp:191
clang::dataflow::Value::Kind::Integer
@ Integer
clang::dataflow::Value::Kind
Kind
Definition: Value.h:34
llvm::DenseSet
Definition: Sema.h:77
Line
const AnnotatedLine * Line
Definition: UsingDeclarationsSorter.cpp:68
clang::dataflow::Value::Kind::Conjunction
@ Conjunction
clang::dataflow::Value::Kind::Negation
@ Negation
clang::dataflow::BoolValue
Models a boolean.
Definition: Value.h:80
clang::Indent
raw_ostream & Indent(raw_ostream &Out, const unsigned int Space, bool IsDot)
Definition: JsonSupport.h:21
clang::dataflow::Value::Kind::Pointer
@ Pointer
llvm::ArrayRef
Definition: LLVM.h:34
clang::dataflow::Solver::Result::Assignment::AssignedTrue
@ AssignedTrue
clang::dataflow::debugString
llvm::StringRef debugString(Value::Kind Kind)
Returns a string representation of a value kind.
Definition: DebugSupport.cpp:35
clang::ObjCPropertyAttribute::Kind
Kind
Definition: DeclObjCCommon.h:22
std
Definition: Format.h:4321
clang::dataflow::Solver::Result::Assignment
Assignment
A boolean value is set to true or false in a truth assignment.
Definition: Solver.h:44
clang
Definition: CalledOnceCheck.h:17
clang::dataflow::Value::Kind::AtomicBool
@ AtomicBool
clang::dataflow::Solver::Result::Status::Satisfiable
@ Satisfiable
Indicates that there exists a satisfying assignment for a boolean formula.
clang::dataflow::Solver::Result::Assignment::AssignedFalse
@ AssignedFalse
clang::dataflow::Value::Kind::Struct
@ Struct
clang::dataflow::Solver::Result
Definition: Solver.h:28
clang::dataflow::Value::Kind::Implication
@ Implication
Value.h
clang::dataflow::Value::Kind::Biconditional
@ Biconditional