Coverage Report

Created: 2022-07-16 07:03

/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
Line
Count
Source (jump to first uncovered line)
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/StringSet.h"
21
#include "llvm/Support/ErrorHandling.h"
22
#include "llvm/Support/FormatAdapters.h"
23
#include "llvm/Support/FormatCommon.h"
24
#include "llvm/Support/FormatVariadic.h"
25
26
namespace clang {
27
namespace dataflow {
28
29
using llvm::AlignStyle;
30
using llvm::fmt_pad;
31
using llvm::formatv;
32
33
namespace {
34
35
class DebugStringGenerator {
36
public:
37
  explicit DebugStringGenerator(
38
      llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
39
20
      : Counter(0), AtomNames(std::move(AtomNamesArg)) {
40
20
#ifndef NDEBUG
41
20
    llvm::StringSet<> Names;
42
27
    for (auto &N : AtomNames) {
43
27
      assert(Names.insert(N.second).second &&
44
27
             "The same name must not assigned to different atoms");
45
27
    }
46
20
#endif
47
20
  }
48
49
  /// Returns a string representation of a boolean value `B`.
50
118
  std::string debugString(const BoolValue &B, size_t Depth = 0) {
51
118
    std::string S;
52
118
    switch (B.getKind()) {
53
63
    case Value::Kind::AtomicBool: {
54
63
      S = getAtomName(&cast<AtomicBoolValue>(B));
55
63
      break;
56
0
    }
57
19
    case Value::Kind::Conjunction: {
58
19
      auto &C = cast<ConjunctionValue>(B);
59
19
      auto L = debugString(C.getLeftSubValue(), Depth + 1);
60
19
      auto R = debugString(C.getRightSubValue(), Depth + 1);
61
19
      S = formatv("(and\n{0}\n{1})", L, R);
62
19
      break;
63
0
    }
64
16
    case Value::Kind::Disjunction: {
65
16
      auto &D = cast<DisjunctionValue>(B);
66
16
      auto L = debugString(D.getLeftSubValue(), Depth + 1);
67
16
      auto R = debugString(D.getRightSubValue(), Depth + 1);
68
16
      S = formatv("(or\n{0}\n{1})", L, R);
69
16
      break;
70
0
    }
71
20
    case Value::Kind::Negation: {
72
20
      auto &N = cast<NegationValue>(B);
73
20
      S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
74
20
      break;
75
0
    }
76
0
    default:
77
0
      llvm_unreachable("Unhandled value kind");
78
118
    }
79
118
    auto Indent = Depth * 4;
80
118
    return formatv("{0}", fmt_pad(S, Indent, 0));
81
118
  }
82
83
  /// Returns a string representation of a set of boolean `Constraints` and the
84
  /// `Result` of satisfiability checking on the `Constraints`.
85
  std::string debugString(const std::vector<BoolValue *> &Constraints,
86
8
                          const Solver::Result &Result) {
87
8
    auto Template = R"(
88
8
Constraints
89
8
------------
90
8
{0:$[
91
8
92
8
]}
93
8
------------
94
8
{1}.
95
8
{2}
96
8
)";
97
98
8
    std::vector<std::string> ConstraintsStrings;
99
8
    ConstraintsStrings.reserve(Constraints.size());
100
16
    for (auto &Constraint : Constraints) {
101
16
      ConstraintsStrings.push_back(debugString(*Constraint));
102
16
    }
103
104
8
    auto StatusString = debugString(Result.getStatus());
105
8
    auto Solution = Result.getSolution();
106
8
    auto SolutionString = Solution ? 
"\n" + debugString(Solution.value())7
:
""1
;
107
108
8
    return formatv(
109
8
        Template,
110
8
        llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
111
8
        StatusString, SolutionString);
112
8
  }
113
114
private:
115
  /// Returns a string representation of a truth assignment to atom booleans.
116
  std::string debugString(
117
      const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
118
7
          &AtomAssignments) {
119
7
    size_t MaxNameLength = 0;
120
20
    for (auto &AtomName : AtomNames) {
121
20
      MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
122
20
    }
123
124
7
    std::vector<std::string> Lines;
125
15
    for (auto &AtomAssignment : AtomAssignments) {
126
15
      auto Line = formatv("{0} = {1}",
127
15
                          fmt_align(getAtomName(AtomAssignment.first),
128
15
                                    AlignStyle::Left, MaxNameLength),
129
15
                          debugString(AtomAssignment.second));
130
15
      Lines.push_back(Line);
131
15
    }
132
7
    llvm::sort(Lines.begin(), Lines.end());
133
134
7
    return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
135
7
  }
136
137
  /// Returns a string representation of a boolean assignment to true or false.
138
15
  std::string debugString(Solver::Result::Assignment Assignment) {
139
15
    switch (Assignment) {
140
4
    case Solver::Result::Assignment::AssignedFalse:
141
4
      return "False";
142
11
    case Solver::Result::Assignment::AssignedTrue:
143
11
      return "True";
144
15
    }
145
0
    llvm_unreachable("Booleans can only be assigned true/false");
146
0
  }
147
148
  /// Returns a string representation of the result status of a SAT check.
149
8
  std::string debugString(Solver::Result::Status Status) {
150
8
    switch (Status) {
151
7
    case Solver::Result::Status::Satisfiable:
152
7
      return "Satisfiable";
153
1
    case Solver::Result::Status::Unsatisfiable:
154
1
      return "Unsatisfiable";
155
0
    case Solver::Result::Status::TimedOut:
156
0
      return "TimedOut";
157
8
    }
158
0
    llvm_unreachable("Unhandled SAT check result status");
159
0
  }
160
161
  /// Returns the name assigned to `Atom`, either user-specified or created by
162
  /// default rules (B0, B1, ...).
163
78
  std::string getAtomName(const AtomicBoolValue *Atom) {
164
78
    auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
165
78
    if (Entry.second) {
166
30
      Counter++;
167
30
    }
168
78
    return Entry.first->second;
169
78
  }
170
171
  // Keep track of number of atoms without a user-specified name, used to assign
172
  // non-repeating default names to such atoms.
173
  size_t Counter;
174
175
  // Keep track of names assigned to atoms.
176
  llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
177
};
178
179
} // namespace
180
181
std::string
182
debugString(const BoolValue &B,
183
12
            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
184
12
  return DebugStringGenerator(std::move(AtomNames)).debugString(B);
185
12
}
186
187
std::string
188
debugString(const std::vector<BoolValue *> &Constraints,
189
            const Solver::Result &Result,
190
8
            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
191
8
  return DebugStringGenerator(std::move(AtomNames))
192
8
      .debugString(Constraints, Result);
193
8
}
194
195
} // namespace dataflow
196
} // namespace clang