wyt created this revision.
Herald added subscribers: martong, tschuett, mgrang, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
wyt requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Depends On D129547 <https://reviews.llvm.org/D129547>
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D129548
Files:
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ 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<BoolValue *> Constraints) {
+ return WatchedLiteralsSolver().solve(std::move(Constraints));
+ }
+ test::BoolValueManager Bools;
+};
+
+TEST_F(SATCheckDebugStringTest, AtomicBoolean) {
+ // B0
+ llvm::DenseSet<BoolValue *> 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<BoolValue *> 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<BoolValue *> 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<BoolValue *> 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<BoolValue *> 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<BoolValue *> 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<AtomicBoolValue>(Bools.atom());
+ auto Then = cast<AtomicBoolValue>(Bools.atom());
+ auto Else = cast<AtomicBoolValue>(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<BoolValue *> 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<AtomicBoolValue>(Bools.atom());
+ auto ThisIntEqZero = cast<AtomicBoolValue>(Bools.atom());
+ auto OtherIntEqZero = cast<AtomicBoolValue>(Bools.atom());
+ auto BothZeroImpliesEQ = Bools.disj(
+ Bools.neg(Bools.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
+ llvm::DenseSet<BoolValue *> 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
Index: clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -11,18 +11,24 @@
//
//===----------------------------------------------------------------------===//
+#include <utility>
+
#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<BoolValue *> &Constraints,
+ Solver::Result &Result) {
+ auto Template = R"(
+Constraints
+------------
+{0:$[
+
+]}
+------------
+{1}.{2}
+)";
+
+ std::vector<std::string> 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<AtomicBoolValue *, Solver::Result::Assignment>
+ &ValAssignments) {
+ size_t FirstColWidth = 6;
+ size_t SecondColWidth = 7;
+
+ std::vector<std::pair<std::string, std::string>> 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<std::string> 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<BoolValue *> &Constraints,
+ Solver::Result &Result,
+ llvm::DenseMap<AtomicBoolValue *, std::string> Names) {
+ return DebugStringGenerator(Names).debugString(Constraints, Result);
+}
+
} // namespace dataflow
} // namespace clang
Index: clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
@@ -16,6 +16,7 @@
#include <string>
+#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseMap.h"
@@ -30,6 +31,20 @@
llvm::DenseMap<AtomicBoolValue *, std::string> 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<BoolValue *> &Constraints, Solver::Result &Result,
+ llvm::DenseMap<AtomicBoolValue *, std::string> AtomNames);
+inline std::string debugString(llvm::DenseSet<BoolValue *> &Constraints,
+ Solver::Result &Result) {
+ return debugString(Constraints, Result, {{}});
+}
+
} // namespace dataflow
} // namespace clang
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
