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
28namespace clang {
29namespace dataflow {
30
31using llvm::AlignStyle;
32using llvm::fmt_pad;
33using llvm::formatv;
34
35llvm::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
63llvm::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
73llvm::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
85namespace {
86
87class DebugStringGenerator {
88public:
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"(
170Constraints
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
196private:
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
239std::string
240debugString(const BoolValue &B,
241            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
242  return DebugStringGenerator(std::move(AtomNames)).debugString(B);
243}
244
245std::string
246debugString(const llvm::DenseSet<BoolValue *> &Constraints,
247            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
248  return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
249}
250
251std::string
252debugString(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