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