forked from OSchip/llvm-project
[clang][dataflow] Add DataflowEnvironment::dump()
Start by dumping the flow condition. Reviewed By: ymandel Differential Revision: https://reviews.llvm.org/D130398
This commit is contained in:
parent
1e4478bbea
commit
b5414b566a
|
@ -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 @@ public:
|
|||
/// `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() {
|
||||
|
|
|
@ -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 @@ public:
|
|||
/// 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.
|
||||
|
|
|
@ -42,6 +42,20 @@ std::string debugString(
|
|||
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.
|
||||
///
|
||||
|
|
|
@ -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 @@ BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache(
|
|||
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
|
||||
|
||||
|
|
|
@ -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 @@ bool Environment::flowConditionImplies(BoolValue &Val) const {
|
|||
return DACtx->flowConditionImplies(*FlowConditionToken, Val);
|
||||
}
|
||||
|
||||
void Environment::dump() const {
|
||||
DACtx->dumpFlowCondition(*FlowConditionToken);
|
||||
}
|
||||
|
||||
} // namespace dataflow
|
||||
} // namespace clang
|
||||
|
|
|
@ -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"
|
||||
|
@ -102,6 +103,22 @@ public:
|
|||
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(ArrayRef<BoolValue *> &Constraints,
|
||||
|
@ -151,7 +168,7 @@ private:
|
|||
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()));
|
||||
}
|
||||
|
@ -182,6 +199,12 @@ debugString(const BoolValue &B,
|
|||
return DebugStringGenerator(std::move(AtomNames)).debugString(B);
|
||||
}
|
||||
|
||||
std::string
|
||||
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) {
|
||||
|
|
|
@ -188,6 +188,31 @@ TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
|
|||
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());
|
||||
|
|
Loading…
Reference in New Issue