gribozavr created this revision.
Herald added subscribers: martong, tschuett, mgrang, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
gribozavr requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Start by dumping the flow condition.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D130398
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
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
@@ -188,6 +188,31 @@
StrEq(Expected));
}
+TEST(ConstraintSetDebugStringTest, Empty) {
+ llvm::DenseSet<BoolValue *> Constraints;
+ EXPECT_THAT(debugString(Constraints), StrEq(""));
+}
+
+TEST(ConstraintSetDebugStringTest, Simple) {
+ ConstraintContext Ctx;
+ llvm::DenseSet<BoolValue *> Constraints;
+ auto X = cast<AtomicBoolValue>(Ctx.atom());
+ auto Y = cast<AtomicBoolValue>(Ctx.atom());
+ Constraints.insert(Ctx.disj(X, Y));
+ Constraints.insert(Ctx.disj(X, Ctx.neg(Y)));
+
+ auto Expected = R"((or
+ X
+ (not
+ Y))
+(or
+ X
+ Y)
+)";
+ EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),
+ StrEq(Expected));
+}
+
Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
llvm::DenseSet<BoolValue *> ConstraintsSet(Constraints.begin(),
Constraints.end());
Index: clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/STLExtras.h"
#include "llvm/ADT/StringSet.h"
#include "llvm/Support/ErrorHandling.h"
#include "llvm/Support/FormatAdapters.h"
@@ -30,6 +31,30 @@
using llvm::fmt_pad;
using llvm::formatv;
+/// 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");
+}
+
namespace {
class DebugStringGenerator {
@@ -80,9 +105,25 @@
return formatv("{0}", fmt_pad(S, Indent, 0));
}
+ std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) {
+ std::vector<std::string> ConstraintsStrings;
+ ConstraintsStrings.reserve(Constraints.size());
+ for (BoolValue *Constraint : Constraints) {
+ ConstraintsStrings.push_back(debugString(*Constraint));
+ }
+ llvm::sort(ConstraintsStrings);
+
+ std::string Result;
+ for (const std::string &S : ConstraintsStrings) {
+ Result += S;
+ Result += '\n';
+ }
+ return Result;
+ }
+
/// 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,
+ std::string debugString(ArrayRef<BoolValue *> Constraints,
const Solver::Result &Result) {
auto Template = R"(
Constraints
@@ -101,7 +142,7 @@
ConstraintsStrings.push_back(debugString(*Constraint));
}
- auto StatusString = debugString(Result.getStatus());
+ auto StatusString = clang::dataflow::debugString(Result.getStatus());
auto Solution = Result.getSolution();
auto SolutionString = Solution ? "\n" + debugString(Solution.value()) : "";
@@ -126,38 +167,14 @@
auto Line = formatv("{0} = {1}",
fmt_align(getAtomName(AtomAssignment.first),
AlignStyle::Left, MaxNameLength),
- debugString(AtomAssignment.second));
+ clang::dataflow::debugString(AtomAssignment.second));
Lines.push_back(Line);
}
- llvm::sort(Lines.begin(), Lines.end());
+ llvm::sort(Lines);
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) {
@@ -185,8 +202,13 @@
}
std::string
-debugString(const std::vector<BoolValue *> &Constraints,
- const Solver::Result &Result,
+debugString(const llvm::DenseSet<BoolValue *> &Constraints,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
+ return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
+}
+
+std::string
+debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
return DebugStringGenerator(std::move(AtomNames))
.debugString(Constraints, Result);
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -15,10 +15,8 @@
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/AST/Decl.h"
#include "clang/AST/DeclCXX.h"
-#include "clang/AST/ExprCXX.h"
#include "clang/AST/Type.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
-#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/DenseSet.h"
@@ -512,5 +510,9 @@
return DACtx->flowConditionImplies(*FlowConditionToken, Val);
}
+void Environment::dump() const {
+ DACtx->dumpFlowCondition(*FlowConditionToken);
+}
+
} // namespace dataflow
} // namespace clang
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -14,7 +14,9 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/AST/ExprCXX.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/Support/Debug.h"
#include <cassert>
#include <memory>
#include <utility>
@@ -293,6 +295,17 @@
return substituteBoolValue(*ConstraintsIT->second, SubstitutionsCache);
}
+void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token) {
+ llvm::DenseSet<BoolValue *> Constraints = {&Token};
+ llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+ addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
+
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
+ {&getBoolLiteralValue(false), "False"},
+ {&getBoolLiteralValue(true), "True"}};
+ llvm::dbgs() << debugString(Constraints, AtomNames);
+}
+
} // 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
@@ -23,6 +23,13 @@
namespace clang {
namespace dataflow {
+
+/// Returns a string representation of a boolean assignment to true or false.
+std::string debugString(Solver::Result::Assignment Assignment);
+
+/// Returns a string representation of the result status of a SAT check.
+std::string debugString(Solver::Result::Status Status);
+
/// Returns a string representation for the boolean value `B`.
///
/// Atomic booleans appearing in the boolean value `B` are assigned to labels
@@ -35,6 +42,20 @@
const BoolValue &B,
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+/// Returns a string representation for `Constraints` - a collection of boolean
+/// formulas.
+///
+/// Atomic booleans appearing in the boolean value `Constraints` 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 llvm::DenseSet<BoolValue *> &Constraints,
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+
/// Returns a string representation for `Constraints` - a collection of boolean
/// formulas and the `Result` of satisfiability checking.
///
@@ -46,7 +67,7 @@
///
/// Names assigned to atoms should not be repeated in `AtomNames`.
std::string debugString(
- const std::vector<BoolValue *> &Constraints, const Solver::Result &Result,
+ ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
inline std::string debugString(
const llvm::DenseSet<BoolValue *> &Constraints,
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -19,7 +19,6 @@
#include "clang/AST/DeclBase.h"
#include "clang/AST/Expr.h"
#include "clang/AST/Type.h"
-#include "clang/AST/TypeOrdering.h"
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
@@ -325,6 +324,8 @@
/// imply that `Val` is true.
bool flowConditionImplies(BoolValue &Val) const;
+ LLVM_DUMP_METHOD void dump() const;
+
private:
/// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
/// return null.
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -23,6 +23,7 @@
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/DenseSet.h"
+#include "llvm/Support/Compiler.h"
#include <cassert>
#include <memory>
#include <type_traits>
@@ -251,6 +252,8 @@
/// `Val2` imposed by the flow condition.
bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
+ LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token);
+
private:
struct NullableQualTypeDenseMapInfo : private llvm::DenseMapInfo<QualType> {
static QualType getEmptyKey() {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
