mirror of
https://github.com/llvm/llvm-project.git
synced 2025-05-07 22:46:06 +00:00
258 lines
8.0 KiB
C++
258 lines
8.0 KiB
C++
//===- DebugSupport.cpp -----------------------------------------*- C++ -*-===//
|
|
//
|
|
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
|
// See https://llvm.org/LICENSE.txt for license information.
|
|
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
|
//
|
|
//===----------------------------------------------------------------------===//
|
|
//
|
|
// This file defines functions which generate more readable forms of data
|
|
// structures used in the dataflow analyses, for debugging purposes.
|
|
//
|
|
//===----------------------------------------------------------------------===//
|
|
|
|
#include <utility>
|
|
|
|
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
|
|
#include "clang/Analysis/FlowSensitive/Solver.h"
|
|
#include "clang/Analysis/FlowSensitive/Value.h"
|
|
#include "llvm/ADT/DenseMap.h"
|
|
#include "llvm/ADT/STLExtras.h"
|
|
#include "llvm/ADT/StringRef.h"
|
|
#include "llvm/ADT/StringSet.h"
|
|
#include "llvm/Support/ErrorHandling.h"
|
|
#include "llvm/Support/FormatAdapters.h"
|
|
#include "llvm/Support/FormatCommon.h"
|
|
#include "llvm/Support/FormatVariadic.h"
|
|
|
|
namespace clang {
|
|
namespace dataflow {
|
|
|
|
using llvm::AlignStyle;
|
|
using llvm::fmt_pad;
|
|
using llvm::formatv;
|
|
|
|
llvm::StringRef debugString(Value::Kind Kind) {
|
|
switch (Kind) {
|
|
case Value::Kind::Integer:
|
|
return "Integer";
|
|
case Value::Kind::Reference:
|
|
return "Reference";
|
|
case Value::Kind::Pointer:
|
|
return "Pointer";
|
|
case Value::Kind::Struct:
|
|
return "Struct";
|
|
case Value::Kind::AtomicBool:
|
|
return "AtomicBool";
|
|
case Value::Kind::Conjunction:
|
|
return "Conjunction";
|
|
case Value::Kind::Disjunction:
|
|
return "Disjunction";
|
|
case Value::Kind::Negation:
|
|
return "Negation";
|
|
case Value::Kind::Implication:
|
|
return "Implication";
|
|
case Value::Kind::Biconditional:
|
|
return "Biconditional";
|
|
}
|
|
llvm_unreachable("Unhandled value kind");
|
|
}
|
|
|
|
llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
|
|
switch (Assignment) {
|
|
case Solver::Result::Assignment::AssignedFalse:
|
|
return "False";
|
|
case Solver::Result::Assignment::AssignedTrue:
|
|
return "True";
|
|
}
|
|
llvm_unreachable("Booleans can only be assigned true/false");
|
|
}
|
|
|
|
llvm::StringRef debugString(Solver::Result::Status Status) {
|
|
switch (Status) {
|
|
case Solver::Result::Status::Satisfiable:
|
|
return "Satisfiable";
|
|
case Solver::Result::Status::Unsatisfiable:
|
|
return "Unsatisfiable";
|
|
case Solver::Result::Status::TimedOut:
|
|
return "TimedOut";
|
|
}
|
|
llvm_unreachable("Unhandled SAT check result status");
|
|
}
|
|
|
|
namespace {
|
|
|
|
class DebugStringGenerator {
|
|
public:
|
|
explicit DebugStringGenerator(
|
|
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
|
|
: Counter(0), AtomNames(std::move(AtomNamesArg)) {
|
|
#ifndef NDEBUG
|
|
llvm::StringSet<> Names;
|
|
for (auto &N : AtomNames) {
|
|
assert(Names.insert(N.second).second &&
|
|
"The same name must not assigned to different atoms");
|
|
}
|
|
#endif
|
|
}
|
|
|
|
/// Returns a string representation of a boolean value `B`.
|
|
std::string debugString(const BoolValue &B, size_t Depth = 0) {
|
|
std::string S;
|
|
switch (B.getKind()) {
|
|
case Value::Kind::AtomicBool: {
|
|
S = getAtomName(&cast<AtomicBoolValue>(B));
|
|
break;
|
|
}
|
|
case Value::Kind::Conjunction: {
|
|
auto &C = cast<ConjunctionValue>(B);
|
|
auto L = debugString(C.getLeftSubValue(), Depth + 1);
|
|
auto R = debugString(C.getRightSubValue(), Depth + 1);
|
|
S = formatv("(and\n{0}\n{1})", L, R);
|
|
break;
|
|
}
|
|
case Value::Kind::Disjunction: {
|
|
auto &D = cast<DisjunctionValue>(B);
|
|
auto L = debugString(D.getLeftSubValue(), Depth + 1);
|
|
auto R = debugString(D.getRightSubValue(), Depth + 1);
|
|
S = formatv("(or\n{0}\n{1})", L, R);
|
|
break;
|
|
}
|
|
case Value::Kind::Negation: {
|
|
auto &N = cast<NegationValue>(B);
|
|
S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
|
|
break;
|
|
}
|
|
case Value::Kind::Implication: {
|
|
auto &IV = cast<ImplicationValue>(B);
|
|
auto L = debugString(IV.getLeftSubValue(), Depth + 1);
|
|
auto R = debugString(IV.getRightSubValue(), Depth + 1);
|
|
S = formatv("(=>\n{0}\n{1})", L, R);
|
|
break;
|
|
}
|
|
case Value::Kind::Biconditional: {
|
|
auto &BV = cast<BiconditionalValue>(B);
|
|
auto L = debugString(BV.getLeftSubValue(), Depth + 1);
|
|
auto R = debugString(BV.getRightSubValue(), Depth + 1);
|
|
S = formatv("(=\n{0}\n{1})", L, R);
|
|
break;
|
|
}
|
|
default:
|
|
llvm_unreachable("Unhandled value kind");
|
|
}
|
|
auto Indent = Depth * 4;
|
|
return formatv("{0}", fmt_pad(S, Indent, 0));
|
|
}
|
|
|
|
std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) {
|
|
std::vector<std::string> ConstraintsStrings;
|
|
ConstraintsStrings.reserve(Constraints.size());
|
|
for (BoolValue *Constraint : Constraints) {
|
|
ConstraintsStrings.push_back(debugString(*Constraint));
|
|
}
|
|
llvm::sort(ConstraintsStrings);
|
|
|
|
std::string Result;
|
|
for (const std::string &S : ConstraintsStrings) {
|
|
Result += S;
|
|
Result += '\n';
|
|
}
|
|
return Result;
|
|
}
|
|
|
|
/// Returns a string representation of a set of boolean `Constraints` and the
|
|
/// `Result` of satisfiability checking on the `Constraints`.
|
|
std::string debugString(ArrayRef<BoolValue *> &Constraints,
|
|
const Solver::Result &Result) {
|
|
auto Template = R"(
|
|
Constraints
|
|
------------
|
|
{0:$[
|
|
|
|
]}
|
|
------------
|
|
{1}.
|
|
{2}
|
|
)";
|
|
|
|
std::vector<std::string> ConstraintsStrings;
|
|
ConstraintsStrings.reserve(Constraints.size());
|
|
for (auto &Constraint : Constraints) {
|
|
ConstraintsStrings.push_back(debugString(*Constraint));
|
|
}
|
|
|
|
auto StatusString = clang::dataflow::debugString(Result.getStatus());
|
|
auto Solution = Result.getSolution();
|
|
auto SolutionString = Solution ? "\n" + debugString(Solution.value()) : "";
|
|
|
|
return formatv(
|
|
Template,
|
|
llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
|
|
StatusString, SolutionString);
|
|
}
|
|
|
|
private:
|
|
/// Returns a string representation of a truth assignment to atom booleans.
|
|
std::string debugString(
|
|
const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
|
|
&AtomAssignments) {
|
|
size_t MaxNameLength = 0;
|
|
for (auto &AtomName : AtomNames) {
|
|
MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
|
|
}
|
|
|
|
std::vector<std::string> Lines;
|
|
for (auto &AtomAssignment : AtomAssignments) {
|
|
auto Line = formatv("{0} = {1}",
|
|
fmt_align(getAtomName(AtomAssignment.first),
|
|
AlignStyle::Left, MaxNameLength),
|
|
clang::dataflow::debugString(AtomAssignment.second));
|
|
Lines.push_back(Line);
|
|
}
|
|
llvm::sort(Lines);
|
|
|
|
return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
|
|
}
|
|
|
|
/// Returns the name assigned to `Atom`, either user-specified or created by
|
|
/// default rules (B0, B1, ...).
|
|
std::string getAtomName(const AtomicBoolValue *Atom) {
|
|
auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
|
|
if (Entry.second) {
|
|
Counter++;
|
|
}
|
|
return Entry.first->second;
|
|
}
|
|
|
|
// Keep track of number of atoms without a user-specified name, used to assign
|
|
// non-repeating default names to such atoms.
|
|
size_t Counter;
|
|
|
|
// Keep track of names assigned to atoms.
|
|
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
|
|
};
|
|
|
|
} // namespace
|
|
|
|
std::string
|
|
debugString(const BoolValue &B,
|
|
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
|
|
return DebugStringGenerator(std::move(AtomNames)).debugString(B);
|
|
}
|
|
|
|
std::string
|
|
debugString(const llvm::DenseSet<BoolValue *> &Constraints,
|
|
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
|
|
return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
|
|
}
|
|
|
|
std::string
|
|
debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
|
|
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
|
|
return DebugStringGenerator(std::move(AtomNames))
|
|
.debugString(Constraints, Result);
|
|
}
|
|
|
|
} // namespace dataflow
|
|
} // namespace clang
|