diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h --- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h +++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h @@ -23,6 +23,13 @@ namespace clang { namespace dataflow { + +/// Returns a string representation of a boolean assignment to true or false. +std::string debugString(Solver::Result::Assignment Assignment); + +/// Returns a string representation of the result status of a SAT check. +std::string debugString(Solver::Result::Status Status); + /// Returns a string representation for the boolean value `B`. /// /// Atomic booleans appearing in the boolean value `B` are assigned to labels diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -30,6 +30,28 @@ 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 { @@ -101,7 +123,7 @@ ConstraintsStrings.push_back(debugString(*Constraint)); } - auto StatusString = debugString(Result.getStatus()); + auto StatusString = clang::dataflow::debugString(Result.getStatus()); auto Solution = Result.getSolution(); auto SolutionString = Solution ? "\n" + debugString(Solution.value()) : ""; @@ -126,7 +148,7 @@ 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()); @@ -134,30 +156,6 @@ 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) {