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