[clang] b8d83e8 - [clang][dataflow] Generate readable form of input and output of satisfiability checking.
Wei Yi Tee via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 13 04:59:09 PDT 2022
Author: Wei Yi Tee
Date: 2022-07-13T11:58:51Z
New Revision: b8d83e8004e4b70fa81e8582eb9f8443a0f3758c
URL: https://github.com/llvm/llvm-project/commit/b8d83e8004e4b70fa81e8582eb9f8443a0f3758c
DIFF: https://github.com/llvm/llvm-project/commit/b8d83e8004e4b70fa81e8582eb9f8443a0f3758c.diff
LOG: [clang][dataflow] Generate readable form of input and output of satisfiability checking.
Differential Revision: https://reviews.llvm.org/D129548
Added:
Modified:
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
index 00f897255e771..ef903d807e12f 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 <string>
+#include <vector>
+#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<const AtomicBoolValue *, std::string> 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<BoolValue *> &Constraints, const Solver::Result &Result,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+inline std::string debugString(
+ const llvm::DenseSet<BoolValue *> &Constraints,
+ const Solver::Result &Result,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}) {
+ std::vector<BoolValue *> 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 8426eda5bebe6..052ab33b74a19 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -11,17 +11,22 @@
//
//===----------------------------------------------------------------------===//
+#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::formatv;
@@ -75,7 +80,85 @@ class DebugStringGenerator {
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<BoolValue *> &Constraints,
+ const Solver::Result &Result) {
+ auto Template = R"(
+Constraints
+------------
+{0:$[
+
+]}
+------------
+{1}.
+{2}
+)";
+
+ std::vector<std::string> 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<AtomicBoolValue *, Solver::Result::Assignment>
+ &AtomAssignments) {
+ size_t MaxNameLength = 0;
+ for (auto &AtomName : AtomNames) {
+ MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
+ }
+
+ std::vector<std::string> 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<BoolValue *> &Constraints,
+ const Solver::Result &Result,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> 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 3c12b6cede2b2..d59de0a343822 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<BoolValue *> Constraints) {
+ llvm::DenseSet<BoolValue *> ConstraintsSet(Constraints.begin(),
+ Constraints.end());
+ return WatchedLiteralsSolver().solve(std::move(ConstraintsSet));
+}
+
+TEST(SATCheckDebugStringTest, AtomicBoolean) {
+ // B0
+ ConstraintContext Ctx;
+ std::vector<BoolValue *> 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<BoolValue *> 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<BoolValue *> 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<BoolValue *> 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<BoolValue *> 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<BoolValue *> 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<AtomicBoolValue>(Ctx.atom());
+ auto Then = cast<AtomicBoolValue>(Ctx.atom());
+ auto Else = cast<AtomicBoolValue>(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<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.
+
+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<AtomicBoolValue>(Ctx.atom());
+ auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
+ auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
+ auto BothZeroImpliesEQ =
+ Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
+ std::vector<BoolValue *> 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
More information about the cfe-commits
mailing list