Author: Dmitri Gribenko Date: 2022-07-23T01:21:20+02:00 New Revision: ee6aba85aa48d03a931ba989ea2c1584b468588a
URL: https://github.com/llvm/llvm-project/commit/ee6aba85aa48d03a931ba989ea2c1584b468588a DIFF: https://github.com/llvm/llvm-project/commit/ee6aba85aa48d03a931ba989ea2c1584b468588a.diff LOG: [clang][dataflow] Expose stringification functions for SAT solver enums Reviewed By: ymandel Differential Revision: https://reviews.llvm.org/D130399 Added: Modified: clang/include/clang/Analysis/FlowSensitive/DebugSupport.h clang/lib/Analysis/FlowSensitive/DebugSupport.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h index 3b854850907b..74367d29b2a0 100644 --- 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 index 1d699a9c9804..f4217fd04c49 100644 --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -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 @@ Constraints 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 @@ Constraints 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) { _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
