maxjhandsome
/
llvm-project
forked from OSchip/llvm-project
1
0
Fork 0
Code Issues Pull Requests Packages Releases Wiki Activity

[clang][dataflow] Expose stringification functions for SAT solver enums 

Reviewed By: ymandel

Differential Revision: https://reviews.llvm.org/D130399
This commit is contained in:
Dmitri Gribenko 2022-07-23 01:18:03 +02:00
parent b4722cc4c9
commit ee6aba85aa
2 changed files with 31 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
View File

@ -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

50
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
View File

@ -30,6 +30,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 {
@ -101,7 +123,7 @@ 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 ? "\n" + debugString(Solution.value()) : "";
@ -126,7 +148,7 @@ 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());
@ -134,30 +156,6 @@ private:
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) {