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 @@ -16,6 +16,7 @@ #include +#include "clang/Analysis/FlowSensitive/Solver.h" #include "clang/Analysis/FlowSensitive/Value.h" #include "llvm/ADT/DenseMap.h" @@ -30,6 +31,20 @@ llvm::DenseMap AtomNames); inline std::string debugString(BoolValue &B) { return debugString(B, {{}}); } +/// Returns a string representation for `Constraints` - a set of boolean +/// formulas and the `Result` of satisfiability checking. +/// +/// Atomic booleans appearing in `Constraints` and `Result` are assigned to +/// labels either specified in `AtomNames` or created by default rules as B0, +/// B1, ... +std::string +debugString(llvm::DenseSet &Constraints, Solver::Result &Result, + llvm::DenseMap AtomNames); +inline std::string debugString(llvm::DenseSet &Constraints, + Solver::Result &Result) { + return debugString(Constraints, Result, {{}}); +} + } // namespace dataflow } // namespace clang 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 @@ -11,18 +11,24 @@ // //===----------------------------------------------------------------------===// +#include + #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/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::fmt_repeat; using llvm::formatv; class DebugStringGenerator { @@ -70,7 +76,96 @@ return formatv("{0}", fmt_pad(S, Indent, 0)); } + /// Returns a string representation of a set of boolean `Constraints` and the + /// `Result` of satisfiability checking on the `Constraints`. + std::string debugString(llvm::DenseSet &Constraints, + Solver::Result &Result) { + auto Template = R"( +Constraints +------------ +{0:$[ + +]} +------------ +{1}.{2} +)"; + + std::vector ConstraintsStrings; + for (auto &Constraint : Constraints) { + ConstraintsStrings.push_back(debugString(*Constraint)); + } + llvm::sort(ConstraintsStrings.begin(), ConstraintsStrings.end()); + + auto StatusString = debugString(Result.getStatus()); + auto Solution = Result.getSolution(); + auto SolutionString = + Solution.hasValue() ? "\n" + debugString(Solution.getValue()) : ""; + + 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(llvm::DenseMap + &ValAssignments) { + size_t FirstColWidth = 6; + size_t SecondColWidth = 7; + + std::vector> LinesData; + LinesData.push_back({"Atom", "Value"}); + for (auto &ValAssignment : ValAssignments) { + auto Name = getAtomName(ValAssignment.first); + FirstColWidth = std::max(FirstColWidth, Name.size() + 2); + LinesData.push_back({Name, debugString(ValAssignment.second)}); + } + llvm::sort(std::next(LinesData.begin()), LinesData.end()); + + std::vector Lines; + auto Separator = formatv("+{0}+{1}+", fmt_repeat('-', FirstColWidth), + fmt_repeat('-', SecondColWidth)); + Lines.push_back(Separator); + for (auto &LineData : LinesData) { + auto Line = formatv( + "| {0} | {1} |", + fmt_align(LineData.first, AlignStyle::Left, FirstColWidth - 2), + fmt_align(LineData.second, AlignStyle::Left, SecondColWidth - 2)); + Lines.push_back(Line); + Lines.push_back(Separator); + } + + 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"; + default: + llvm_unreachable("Booleans can only be assigned true/false"); + } + } + + /// Returns a string representation of the result status of a SAT check. + std::string debugString(enum 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"; + default: + 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(AtomicBoolValue *Atom) { @@ -94,5 +189,11 @@ return DebugStringGenerator(Names).debugString(B); } +std::string debugString(llvm::DenseSet &Constraints, + Solver::Result &Result, + llvm::DenseMap Names) { + return DebugStringGenerator(Names).debugString(Constraints, Result); +} + } // namespace dataflow } // namespace clang diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp --- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp @@ -9,6 +9,7 @@ #include "clang/Analysis/FlowSensitive/DebugSupport.h" #include "TestingSupport.h" #include "clang/Analysis/FlowSensitive/Value.h" +#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h" #include "gmock/gmock.h" #include "gtest/gtest.h" @@ -185,4 +186,267 @@ StrEq(Expected)); } +class SATCheckDebugStringTest : public ::testing::Test { +protected: + Solver::Result CheckSAT(llvm::DenseSet Constraints) { + return WatchedLiteralsSolver().solve(std::move(Constraints)); + } + test::BoolValueManager Bools; +}; + +TEST_F(SATCheckDebugStringTest, AtomicBoolean) { + // B0 + llvm::DenseSet Constraints({Bools.atom()}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +(B0) +------------ +Satisfiable. ++------+-------+ +| Atom | Value | ++------+-------+ +| B0 | True | ++------+-------+ +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST_F(SATCheckDebugStringTest, AtomicBooleanAndNegation) { + // B0, !B0 + auto B0 = Bools.atom(); + llvm::DenseSet Constraints({B0, Bools.neg(B0)}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +(B0) + +(not + (B0)) +------------ +Unsatisfiable. +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST_F(SATCheckDebugStringTest, MultipleAtomicBooleans) { + // B0, B1 + llvm::DenseSet Constraints({Bools.atom(), Bools.atom()}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +(B0) + +(B1) +------------ +Satisfiable. ++------+-------+ +| Atom | Value | ++------+-------+ +| B0 | True | ++------+-------+ +| B1 | True | ++------+-------+ +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST_F(SATCheckDebugStringTest, Implication) { + // B0, B0 => B1 + auto B0 = Bools.atom(); + auto B1 = Bools.atom(); + auto Impl = Bools.disj(Bools.neg(B0), B1); + llvm::DenseSet Constraints({B0, Impl}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +(B0) + +(or + (not + (B0)) + (B1)) +------------ +Satisfiable. ++------+-------+ +| Atom | Value | ++------+-------+ +| B0 | True | ++------+-------+ +| B1 | True | ++------+-------+ +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST_F(SATCheckDebugStringTest, Iff) { + // B0, B0 <=> B1 + auto B0 = Bools.atom(); + auto B1 = Bools.atom(); + auto Iff = + Bools.conj(Bools.disj(Bools.neg(B0), B1), Bools.disj(B0, Bools.neg(B1))); + llvm::DenseSet Constraints({B0, Iff}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +(B0) + +(and + (or + (not + (B0)) + (B1)) + (or + (B0) + (not + (B1)))) +------------ +Satisfiable. ++------+-------+ +| Atom | Value | ++------+-------+ +| B0 | True | ++------+-------+ +| B1 | True | ++------+-------+ +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST_F(SATCheckDebugStringTest, Xor) { + // B0, XOR(B0, B1) + auto B0 = Bools.atom(); + auto B1 = Bools.atom(); + auto XOR = + Bools.disj(Bools.conj(B0, Bools.neg(B1)), Bools.conj(Bools.neg(B0), B1)); + llvm::DenseSet Constraints({B0, XOR}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +(B0) + +(or + (and + (B0) + (not + (B1))) + (and + (not + (B0)) + (B1))) +------------ +Satisfiable. ++------+-------+ +| Atom | Value | ++------+-------+ +| B0 | True | ++------+-------+ +| B1 | False | ++------+-------+ +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST_F(SATCheckDebugStringTest, ComplexBooleanWithNames) { + // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else) + auto Cond = cast(Bools.atom()); + auto Then = cast(Bools.atom()); + auto Else = cast(Bools.atom()); + auto B = Bools.disj( + Bools.conj(Cond, Bools.conj(Then, Bools.neg(Else))), + Bools.conj(Bools.neg(Cond), Bools.conj(Bools.neg(Then), Else))); + llvm::DenseSet Constraints({Cond, B}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +(Cond) + +(or + (and + (Cond) + (and + (Then) + (not + (Else)))) + (and + (not + (Cond)) + (and + (not + (Then)) + (Else)))) +------------ +Satisfiable. ++------+-------+ +| Atom | Value | ++------+-------+ +| Cond | True | ++------+-------+ +| Else | False | ++------+-------+ +| Then | True | ++------+-------+ +)"; + EXPECT_THAT(debugString(Constraints, Result, + {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}), + StrEq(Expected)); +} + +TEST_F(SATCheckDebugStringTest, ComplexBooleanWithLongNames) { + // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq + auto IntsAreEq = cast(Bools.atom()); + auto ThisIntEqZero = cast(Bools.atom()); + auto OtherIntEqZero = cast(Bools.atom()); + auto BothZeroImpliesEQ = Bools.disj( + Bools.neg(Bools.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq); + llvm::DenseSet Constraints( + {ThisIntEqZero, Bools.neg(IntsAreEq), BothZeroImpliesEQ}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +(ThisIntEqZero) + +(not + (IntsAreEq)) + +(or + (not + (and + (ThisIntEqZero) + (OtherIntEqZero))) + (IntsAreEq)) +------------ +Satisfiable. ++----------------+-------+ +| Atom | Value | ++----------------+-------+ +| IntsAreEq | False | ++----------------+-------+ +| OtherIntEqZero | False | ++----------------+-------+ +| ThisIntEqZero | True | ++----------------+-------+ +)"; + EXPECT_THAT(debugString(Constraints, Result, + {{IntsAreEq, "IntsAreEq"}, + {ThisIntEqZero, "ThisIntEqZero"}, + {OtherIntEqZero, "OtherIntEqZero"}}), + StrEq(Expected)); +} } // namespace