1*12c85518Srobert //===- DebugSupport.cpp -----------------------------------------*- C++ -*-===//
2*12c85518Srobert //
3*12c85518Srobert // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4*12c85518Srobert // See https://llvm.org/LICENSE.txt for license information.
5*12c85518Srobert // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6*12c85518Srobert //
7*12c85518Srobert //===----------------------------------------------------------------------===//
8*12c85518Srobert //
9*12c85518Srobert // This file defines functions which generate more readable forms of data
10*12c85518Srobert // structures used in the dataflow analyses, for debugging purposes.
11*12c85518Srobert //
12*12c85518Srobert //===----------------------------------------------------------------------===//
13*12c85518Srobert
14*12c85518Srobert #include <utility>
15*12c85518Srobert
16*12c85518Srobert #include "clang/Analysis/FlowSensitive/DebugSupport.h"
17*12c85518Srobert #include "clang/Analysis/FlowSensitive/Solver.h"
18*12c85518Srobert #include "clang/Analysis/FlowSensitive/Value.h"
19*12c85518Srobert #include "llvm/ADT/DenseMap.h"
20*12c85518Srobert #include "llvm/ADT/STLExtras.h"
21*12c85518Srobert #include "llvm/ADT/StringRef.h"
22*12c85518Srobert #include "llvm/ADT/StringSet.h"
23*12c85518Srobert #include "llvm/Support/ErrorHandling.h"
24*12c85518Srobert #include "llvm/Support/FormatAdapters.h"
25*12c85518Srobert #include "llvm/Support/FormatCommon.h"
26*12c85518Srobert #include "llvm/Support/FormatVariadic.h"
27*12c85518Srobert
28*12c85518Srobert namespace clang {
29*12c85518Srobert namespace dataflow {
30*12c85518Srobert
31*12c85518Srobert using llvm::AlignStyle;
32*12c85518Srobert using llvm::fmt_pad;
33*12c85518Srobert using llvm::formatv;
34*12c85518Srobert
debugString(Value::Kind Kind)35*12c85518Srobert llvm::StringRef debugString(Value::Kind Kind) {
36*12c85518Srobert switch (Kind) {
37*12c85518Srobert case Value::Kind::Integer:
38*12c85518Srobert return "Integer";
39*12c85518Srobert case Value::Kind::Reference:
40*12c85518Srobert return "Reference";
41*12c85518Srobert case Value::Kind::Pointer:
42*12c85518Srobert return "Pointer";
43*12c85518Srobert case Value::Kind::Struct:
44*12c85518Srobert return "Struct";
45*12c85518Srobert case Value::Kind::AtomicBool:
46*12c85518Srobert return "AtomicBool";
47*12c85518Srobert case Value::Kind::TopBool:
48*12c85518Srobert return "TopBool";
49*12c85518Srobert case Value::Kind::Conjunction:
50*12c85518Srobert return "Conjunction";
51*12c85518Srobert case Value::Kind::Disjunction:
52*12c85518Srobert return "Disjunction";
53*12c85518Srobert case Value::Kind::Negation:
54*12c85518Srobert return "Negation";
55*12c85518Srobert case Value::Kind::Implication:
56*12c85518Srobert return "Implication";
57*12c85518Srobert case Value::Kind::Biconditional:
58*12c85518Srobert return "Biconditional";
59*12c85518Srobert }
60*12c85518Srobert llvm_unreachable("Unhandled value kind");
61*12c85518Srobert }
62*12c85518Srobert
debugString(Solver::Result::Assignment Assignment)63*12c85518Srobert llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
64*12c85518Srobert switch (Assignment) {
65*12c85518Srobert case Solver::Result::Assignment::AssignedFalse:
66*12c85518Srobert return "False";
67*12c85518Srobert case Solver::Result::Assignment::AssignedTrue:
68*12c85518Srobert return "True";
69*12c85518Srobert }
70*12c85518Srobert llvm_unreachable("Booleans can only be assigned true/false");
71*12c85518Srobert }
72*12c85518Srobert
debugString(Solver::Result::Status Status)73*12c85518Srobert llvm::StringRef debugString(Solver::Result::Status Status) {
74*12c85518Srobert switch (Status) {
75*12c85518Srobert case Solver::Result::Status::Satisfiable:
76*12c85518Srobert return "Satisfiable";
77*12c85518Srobert case Solver::Result::Status::Unsatisfiable:
78*12c85518Srobert return "Unsatisfiable";
79*12c85518Srobert case Solver::Result::Status::TimedOut:
80*12c85518Srobert return "TimedOut";
81*12c85518Srobert }
82*12c85518Srobert llvm_unreachable("Unhandled SAT check result status");
83*12c85518Srobert }
84*12c85518Srobert
85*12c85518Srobert namespace {
86*12c85518Srobert
87*12c85518Srobert class DebugStringGenerator {
88*12c85518Srobert public:
DebugStringGenerator(llvm::DenseMap<const AtomicBoolValue *,std::string> AtomNamesArg)89*12c85518Srobert explicit DebugStringGenerator(
90*12c85518Srobert llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
91*12c85518Srobert : Counter(0), AtomNames(std::move(AtomNamesArg)) {
92*12c85518Srobert #ifndef NDEBUG
93*12c85518Srobert llvm::StringSet<> Names;
94*12c85518Srobert for (auto &N : AtomNames) {
95*12c85518Srobert assert(Names.insert(N.second).second &&
96*12c85518Srobert "The same name must not assigned to different atoms");
97*12c85518Srobert }
98*12c85518Srobert #endif
99*12c85518Srobert }
100*12c85518Srobert
101*12c85518Srobert /// Returns a string representation of a boolean value `B`.
debugString(const BoolValue & B,size_t Depth=0)102*12c85518Srobert std::string debugString(const BoolValue &B, size_t Depth = 0) {
103*12c85518Srobert std::string S;
104*12c85518Srobert switch (B.getKind()) {
105*12c85518Srobert case Value::Kind::AtomicBool: {
106*12c85518Srobert S = getAtomName(&cast<AtomicBoolValue>(B));
107*12c85518Srobert break;
108*12c85518Srobert }
109*12c85518Srobert case Value::Kind::Conjunction: {
110*12c85518Srobert auto &C = cast<ConjunctionValue>(B);
111*12c85518Srobert auto L = debugString(C.getLeftSubValue(), Depth + 1);
112*12c85518Srobert auto R = debugString(C.getRightSubValue(), Depth + 1);
113*12c85518Srobert S = formatv("(and\n{0}\n{1})", L, R);
114*12c85518Srobert break;
115*12c85518Srobert }
116*12c85518Srobert case Value::Kind::Disjunction: {
117*12c85518Srobert auto &D = cast<DisjunctionValue>(B);
118*12c85518Srobert auto L = debugString(D.getLeftSubValue(), Depth + 1);
119*12c85518Srobert auto R = debugString(D.getRightSubValue(), Depth + 1);
120*12c85518Srobert S = formatv("(or\n{0}\n{1})", L, R);
121*12c85518Srobert break;
122*12c85518Srobert }
123*12c85518Srobert case Value::Kind::Negation: {
124*12c85518Srobert auto &N = cast<NegationValue>(B);
125*12c85518Srobert S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
126*12c85518Srobert break;
127*12c85518Srobert }
128*12c85518Srobert case Value::Kind::Implication: {
129*12c85518Srobert auto &IV = cast<ImplicationValue>(B);
130*12c85518Srobert auto L = debugString(IV.getLeftSubValue(), Depth + 1);
131*12c85518Srobert auto R = debugString(IV.getRightSubValue(), Depth + 1);
132*12c85518Srobert S = formatv("(=>\n{0}\n{1})", L, R);
133*12c85518Srobert break;
134*12c85518Srobert }
135*12c85518Srobert case Value::Kind::Biconditional: {
136*12c85518Srobert auto &BV = cast<BiconditionalValue>(B);
137*12c85518Srobert auto L = debugString(BV.getLeftSubValue(), Depth + 1);
138*12c85518Srobert auto R = debugString(BV.getRightSubValue(), Depth + 1);
139*12c85518Srobert S = formatv("(=\n{0}\n{1})", L, R);
140*12c85518Srobert break;
141*12c85518Srobert }
142*12c85518Srobert default:
143*12c85518Srobert llvm_unreachable("Unhandled value kind");
144*12c85518Srobert }
145*12c85518Srobert auto Indent = Depth * 4;
146*12c85518Srobert return formatv("{0}", fmt_pad(S, Indent, 0));
147*12c85518Srobert }
148*12c85518Srobert
debugString(const llvm::DenseSet<BoolValue * > & Constraints)149*12c85518Srobert std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) {
150*12c85518Srobert std::vector<std::string> ConstraintsStrings;
151*12c85518Srobert ConstraintsStrings.reserve(Constraints.size());
152*12c85518Srobert for (BoolValue *Constraint : Constraints) {
153*12c85518Srobert ConstraintsStrings.push_back(debugString(*Constraint));
154*12c85518Srobert }
155*12c85518Srobert llvm::sort(ConstraintsStrings);
156*12c85518Srobert
157*12c85518Srobert std::string Result;
158*12c85518Srobert for (const std::string &S : ConstraintsStrings) {
159*12c85518Srobert Result += S;
160*12c85518Srobert Result += '\n';
161*12c85518Srobert }
162*12c85518Srobert return Result;
163*12c85518Srobert }
164*12c85518Srobert
165*12c85518Srobert /// Returns a string representation of a set of boolean `Constraints` and the
166*12c85518Srobert /// `Result` of satisfiability checking on the `Constraints`.
debugString(ArrayRef<BoolValue * > & Constraints,const Solver::Result & Result)167*12c85518Srobert std::string debugString(ArrayRef<BoolValue *> &Constraints,
168*12c85518Srobert const Solver::Result &Result) {
169*12c85518Srobert auto Template = R"(
170*12c85518Srobert Constraints
171*12c85518Srobert ------------
172*12c85518Srobert {0:$[
173*12c85518Srobert
174*12c85518Srobert ]}
175*12c85518Srobert ------------
176*12c85518Srobert {1}.
177*12c85518Srobert {2}
178*12c85518Srobert )";
179*12c85518Srobert
180*12c85518Srobert std::vector<std::string> ConstraintsStrings;
181*12c85518Srobert ConstraintsStrings.reserve(Constraints.size());
182*12c85518Srobert for (auto &Constraint : Constraints) {
183*12c85518Srobert ConstraintsStrings.push_back(debugString(*Constraint));
184*12c85518Srobert }
185*12c85518Srobert
186*12c85518Srobert auto StatusString = clang::dataflow::debugString(Result.getStatus());
187*12c85518Srobert auto Solution = Result.getSolution();
188*12c85518Srobert auto SolutionString = Solution ? "\n" + debugString(*Solution) : "";
189*12c85518Srobert
190*12c85518Srobert return formatv(
191*12c85518Srobert Template,
192*12c85518Srobert llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
193*12c85518Srobert StatusString, SolutionString);
194*12c85518Srobert }
195*12c85518Srobert
196*12c85518Srobert private:
197*12c85518Srobert /// Returns a string representation of a truth assignment to atom booleans.
debugString(const llvm::DenseMap<AtomicBoolValue *,Solver::Result::Assignment> & AtomAssignments)198*12c85518Srobert std::string debugString(
199*12c85518Srobert const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
200*12c85518Srobert &AtomAssignments) {
201*12c85518Srobert size_t MaxNameLength = 0;
202*12c85518Srobert for (auto &AtomName : AtomNames) {
203*12c85518Srobert MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
204*12c85518Srobert }
205*12c85518Srobert
206*12c85518Srobert std::vector<std::string> Lines;
207*12c85518Srobert for (auto &AtomAssignment : AtomAssignments) {
208*12c85518Srobert auto Line = formatv("{0} = {1}",
209*12c85518Srobert fmt_align(getAtomName(AtomAssignment.first),
210*12c85518Srobert AlignStyle::Left, MaxNameLength),
211*12c85518Srobert clang::dataflow::debugString(AtomAssignment.second));
212*12c85518Srobert Lines.push_back(Line);
213*12c85518Srobert }
214*12c85518Srobert llvm::sort(Lines);
215*12c85518Srobert
216*12c85518Srobert return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
217*12c85518Srobert }
218*12c85518Srobert
219*12c85518Srobert /// Returns the name assigned to `Atom`, either user-specified or created by
220*12c85518Srobert /// default rules (B0, B1, ...).
getAtomName(const AtomicBoolValue * Atom)221*12c85518Srobert std::string getAtomName(const AtomicBoolValue *Atom) {
222*12c85518Srobert auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
223*12c85518Srobert if (Entry.second) {
224*12c85518Srobert Counter++;
225*12c85518Srobert }
226*12c85518Srobert return Entry.first->second;
227*12c85518Srobert }
228*12c85518Srobert
229*12c85518Srobert // Keep track of number of atoms without a user-specified name, used to assign
230*12c85518Srobert // non-repeating default names to such atoms.
231*12c85518Srobert size_t Counter;
232*12c85518Srobert
233*12c85518Srobert // Keep track of names assigned to atoms.
234*12c85518Srobert llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
235*12c85518Srobert };
236*12c85518Srobert
237*12c85518Srobert } // namespace
238*12c85518Srobert
239*12c85518Srobert std::string
debugString(const BoolValue & B,llvm::DenseMap<const AtomicBoolValue *,std::string> AtomNames)240*12c85518Srobert debugString(const BoolValue &B,
241*12c85518Srobert llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
242*12c85518Srobert return DebugStringGenerator(std::move(AtomNames)).debugString(B);
243*12c85518Srobert }
244*12c85518Srobert
245*12c85518Srobert std::string
debugString(const llvm::DenseSet<BoolValue * > & Constraints,llvm::DenseMap<const AtomicBoolValue *,std::string> AtomNames)246*12c85518Srobert debugString(const llvm::DenseSet<BoolValue *> &Constraints,
247*12c85518Srobert llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
248*12c85518Srobert return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
249*12c85518Srobert }
250*12c85518Srobert
251*12c85518Srobert std::string
debugString(ArrayRef<BoolValue * > Constraints,const Solver::Result & Result,llvm::DenseMap<const AtomicBoolValue *,std::string> AtomNames)252*12c85518Srobert debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
253*12c85518Srobert llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
254*12c85518Srobert return DebugStringGenerator(std::move(AtomNames))
255*12c85518Srobert .debugString(Constraints, Result);
256*12c85518Srobert }
257*12c85518Srobert
258*12c85518Srobert } // namespace dataflow
259*12c85518Srobert } // namespace clang
260