#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"
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
//
//===----------------------------------------------------------------------===//
+#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;
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) {
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
#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"
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