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::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"(
170 Constraints
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 
196 private:
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 
239 std::string
240 debugString(const BoolValue &B,
241             llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
242   return DebugStringGenerator(std::move(AtomNames)).debugString(B);
243 }
244 
245 std::string
246 debugString(const llvm::DenseSet<BoolValue *> &Constraints,
247             llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
248   return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
249 }
250 
251 std::string
252 debugString(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