From: Wei Yi Tee Date: Tue, 12 Jul 2022 18:38:52 +0000 (+0000) Subject: [clang][dataflow] Generate readable form of input and output of satisfiability checking. X-Git-Tag: upstream/15.0.7~1854 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=b8d83e8004e4b70fa81e8582eb9f8443a0f3758c;p=platform%2Fupstream%2Fllvm.git [clang][dataflow] Generate readable form of input and output of satisfiability checking. Differential Revision: https://reviews.llvm.org/D129548 --- diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h index 00f8972..ef903d8 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h +++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h @@ -15,7 +15,9 @@ #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_ #include +#include +#include "clang/Analysis/FlowSensitive/Solver.h" #include "clang/Analysis/FlowSensitive/Value.h" #include "llvm/ADT/DenseMap.h" @@ -33,6 +35,28 @@ std::string debugString( const BoolValue &B, llvm::DenseMap AtomNames = {{}}); +/// Returns a string representation for `Constraints` - a collection 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, ... +/// +/// Requirements: +/// +/// Names assigned to atoms should not be repeated in `AtomNames`. +std::string debugString( + const std::vector &Constraints, const Solver::Result &Result, + llvm::DenseMap AtomNames = {{}}); +inline std::string debugString( + const llvm::DenseSet &Constraints, + const Solver::Result &Result, + llvm::DenseMap AtomNames = {{}}) { + std::vector ConstraintsVec(Constraints.begin(), + Constraints.end()); + return debugString(ConstraintsVec, Result, std::move(AtomNames)); +} + } // namespace dataflow } // namespace clang diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp index 8426eda..052ab33 100644 --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -11,17 +11,22 @@ // //===----------------------------------------------------------------------===// +#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::formatv; @@ -75,7 +80,85 @@ public: 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(const std::vector &Constraints, + const Solver::Result &Result) { + auto Template = R"( +Constraints +------------ +{0:$[ + +]} +------------ +{1}. +{2} +)"; + + std::vector ConstraintsStrings; + ConstraintsStrings.reserve(Constraints.size()); + for (auto &Constraint : Constraints) { + ConstraintsStrings.push_back(debugString(*Constraint)); + } + + 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( + const llvm::DenseMap + &AtomAssignments) { + size_t MaxNameLength = 0; + for (auto &AtomName : AtomNames) { + MaxNameLength = std::max(MaxNameLength, AtomName.second.size()); + } + + std::vector Lines; + for (auto &AtomAssignment : AtomAssignments) { + auto Line = formatv("{0} = {1}", + fmt_align(getAtomName(AtomAssignment.first), + AlignStyle::Left, MaxNameLength), + debugString(AtomAssignment.second)); + Lines.push_back(Line); + } + llvm::sort(Lines.begin(), Lines.end()); + + 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) { @@ -102,5 +185,13 @@ debugString(const BoolValue &B, return DebugStringGenerator(std::move(AtomNames)).debugString(B); } +std::string +debugString(const std::vector &Constraints, + const Solver::Result &Result, + llvm::DenseMap AtomNames) { + return DebugStringGenerator(std::move(AtomNames)) + .debugString(Constraints, Result); +} + } // namespace dataflow } // namespace clang diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp index 3c12b6c..d59de0a 100644 --- 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" @@ -187,4 +188,242 @@ TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) { StrEq(Expected)); } +Solver::Result CheckSAT(std::vector Constraints) { + llvm::DenseSet ConstraintsSet(Constraints.begin(), + Constraints.end()); + return WatchedLiteralsSolver().solve(std::move(ConstraintsSet)); +} + +TEST(SATCheckDebugStringTest, AtomicBoolean) { + // B0 + ConstraintContext Ctx; + std::vector Constraints({Ctx.atom()}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 +------------ +Satisfiable. + +B0 = True +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) { + // B0, !B0 + ConstraintContext Ctx; + auto B0 = Ctx.atom(); + std::vector Constraints({B0, Ctx.neg(B0)}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +(not + B0) +------------ +Unsatisfiable. + +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) { + // B0, B1 + ConstraintContext Ctx; + std::vector Constraints({Ctx.atom(), Ctx.atom()}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +B1 +------------ +Satisfiable. + +B0 = True +B1 = True +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, Implication) { + // B0, B0 => B1 + ConstraintContext Ctx; + auto B0 = Ctx.atom(); + auto B1 = Ctx.atom(); + auto Impl = Ctx.disj(Ctx.neg(B0), B1); + std::vector Constraints({B0, Impl}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +(or + (not + B0) + B1) +------------ +Satisfiable. + +B0 = True +B1 = True +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, Iff) { + // B0, B0 <=> B1 + ConstraintContext Ctx; + auto B0 = Ctx.atom(); + auto B1 = Ctx.atom(); + auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1))); + std::vector Constraints({B0, Iff}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +(and + (or + (not + B0) + B1) + (or + B0 + (not + B1))) +------------ +Satisfiable. + +B0 = True +B1 = True +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, Xor) { + // B0, XOR(B0, B1) + ConstraintContext Ctx; + auto B0 = Ctx.atom(); + auto B1 = Ctx.atom(); + auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1)); + std::vector Constraints({B0, XOR}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +(or + (and + B0 + (not + B1)) + (and + (not + B0) + B1)) +------------ +Satisfiable. + +B0 = True +B1 = False +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) { + // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else) + ConstraintContext Ctx; + auto Cond = cast(Ctx.atom()); + auto Then = cast(Ctx.atom()); + auto Else = cast(Ctx.atom()); + auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))), + Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else))); + std::vector 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. + +Cond = True +Else = False +Then = True +)"; + EXPECT_THAT(debugString(Constraints, Result, + {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}), + StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) { + // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq + ConstraintContext Ctx; + auto IntsAreEq = cast(Ctx.atom()); + auto ThisIntEqZero = cast(Ctx.atom()); + auto OtherIntEqZero = cast(Ctx.atom()); + auto BothZeroImpliesEQ = + Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq); + std::vector Constraints( + {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +ThisIntEqZero + +(not + IntsAreEq) + +(or + (not + (and + ThisIntEqZero + OtherIntEqZero)) + IntsAreEq) +------------ +Satisfiable. + +IntsAreEq = False +OtherIntEqZero = False +ThisIntEqZero = True +)"; + EXPECT_THAT(debugString(Constraints, Result, + {{IntsAreEq, "IntsAreEq"}, + {ThisIntEqZero, "ThisIntEqZero"}, + {OtherIntEqZero, "OtherIntEqZero"}}), + StrEq(Expected)); +} } // namespace