diff options
| author | Dimitry Andric <dim@FreeBSD.org> | 2022-07-24 15:03:44 +0000 |
|---|---|---|
| committer | Dimitry Andric <dim@FreeBSD.org> | 2022-07-24 15:03:44 +0000 |
| commit | 4b4fe385e49bd883fd183b5f21c1ea486c722e61 (patch) | |
| tree | c3d8fdb355c9c73e57723718c22103aaf7d15aa6 /clang/lib/Analysis/FlowSensitive/DebugSupport.cpp | |
| parent | 1f917f69ff07f09b6dbb670971f57f8efe718b84 (diff) | |
Diffstat (limited to 'clang/lib/Analysis/FlowSensitive/DebugSupport.cpp')
| -rw-r--r-- | clang/lib/Analysis/FlowSensitive/DebugSupport.cpp | 83 |
1 files changed, 51 insertions, 32 deletions
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp index 305d9d346089..309ff0682f50 100644 --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -17,6 +17,7 @@ #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/StringSet.h" #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/FormatAdapters.h" @@ -30,6 +31,28 @@ using llvm::AlignStyle; using llvm::fmt_pad; using llvm::formatv; +std::string 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"); +} + +std::string 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 { @@ -80,9 +103,25 @@ public: 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(const std::vector<BoolValue *> &Constraints, + std::string debugString(ArrayRef<BoolValue *> &Constraints, const Solver::Result &Result) { auto Template = R"( Constraints @@ -101,10 +140,9 @@ Constraints ConstraintsStrings.push_back(debugString(*Constraint)); } - auto StatusString = debugString(Result.getStatus()); + auto StatusString = clang::dataflow::debugString(Result.getStatus()); auto Solution = Result.getSolution(); - auto SolutionString = - Solution.hasValue() ? "\n" + debugString(Solution.value()) : ""; + auto SolutionString = Solution ? "\n" + debugString(Solution.value()) : ""; return formatv( Template, @@ -127,38 +165,14 @@ private: auto Line = formatv("{0} = {1}", fmt_align(getAtomName(AtomAssignment.first), AlignStyle::Left, MaxNameLength), - debugString(AtomAssignment.second)); + clang::dataflow::debugString(AtomAssignment.second)); Lines.push_back(Line); } - llvm::sort(Lines.begin(), Lines.end()); + llvm::sort(Lines); return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end())); } - /// Returns a string representation of a boolean assignment to true or false. - std::string 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"); - } - - /// Returns a string representation of the result status of a SAT check. - std::string 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"); - } - /// Returns the name assigned to `Atom`, either user-specified or created by /// default rules (B0, B1, ...). std::string getAtomName(const AtomicBoolValue *Atom) { @@ -186,8 +200,13 @@ debugString(const BoolValue &B, } std::string -debugString(const std::vector<BoolValue *> &Constraints, - const Solver::Result &Result, +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); |
