sammccall created this revision.
Herald added subscribers: martong, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
sammccall requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Instead of meaningless "V7", use the name "B3 <https://reviews.llvm.org/B3>:1"
for the flow condition
of the first analysis of basic block 3.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D153488
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
Index: clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
+++ clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
@@ -154,6 +154,8 @@
std::vector<std::pair<const CFGBlock *, unsigned>> Iters;
// Number of times each CFG block has been seen.
llvm::DenseMap<const CFGBlock *, unsigned> BlockIters;
+ // Labels assigned to SAT atoms.
+ llvm::DenseMap<Atom, std::string> AtomNames;
// The messages logged in the current context but not yet written.
std::string ContextLogs;
// The number of elements we have visited within the current CFG block.
@@ -245,6 +247,9 @@
void recordState(TypeErasedDataflowAnalysisState &State) override {
unsigned Block = Iters.back().first->getBlockID();
unsigned Iter = Iters.back().second;
+ AtomNames.try_emplace(State.Env.getFlowConditionToken(),
+ iterID(Block, Iter));
+
JOS->attributeObject(elementIterID(Block, Iter, ElementIndex), [&] {
JOS->attribute("block", blockID(Block));
JOS->attribute("iter", Iter);
@@ -266,7 +271,17 @@
{
std::string BuiltinLattice;
llvm::raw_string_ostream BuiltinLatticeS(BuiltinLattice);
- State.Env.dump(BuiltinLatticeS);
+ State.Env.dump(BuiltinLatticeS,
+ [&](llvm::raw_ostream &OS, const Formula &F) {
+ if (F.kind() == Formula::AtomRef) {
+ if (auto It = AtomNames.find(F.atom());
+ It != AtomNames.end()) {
+ OS << It->second;
+ return true;
+ }
+ }
+ return false;
+ });
JOS->attribute("builtinLattice", BuiltinLattice);
}
});
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -898,7 +898,9 @@
return flowConditionImplies(Val.formula());
}
-void Environment::dump(raw_ostream &OS) const {
+void Environment::dump(
+ raw_ostream &OS,
+ llvm::function_ref<Formula::DelegatePrinter> Delegate) const {
// FIXME: add printing for remaining fields and allow caller to decide what
// fields are printed.
OS << "DeclToLoc:\n";
@@ -914,8 +916,8 @@
OS << " [" << L << ", " << V << ": " << *V << "]\n";
}
- OS << "FlowConditionToken:\n";
- DACtx->dumpFlowCondition(FlowConditionToken, OS);
+ OS << "Flow condition:\n";
+ DACtx->dumpFlowCondition(FlowConditionToken, OS, Delegate);
}
void Environment::dump() const {
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -189,8 +189,9 @@
}
}
-void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
- llvm::raw_ostream &OS) {
+void DataflowAnalysisContext::dumpFlowCondition(
+ Atom Token, llvm::raw_ostream &OS,
+ llvm::function_ref<Formula::DelegatePrinter> OuterDelegate) {
llvm::DenseSet<const Formula *> Constraints = {&arena().makeAtomRef(Token)};
llvm::DenseSet<Atom> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
@@ -199,6 +200,8 @@
auto &True = arena().makeLiteral(true);
auto &False = arena().makeLiteral(false);
auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) {
+ if (OuterDelegate(OS, F))
+ return true;
if (&F == &True) {
OS << "True";
return true;
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -548,7 +548,9 @@
Arena &arena() const { return DACtx->arena(); }
LLVM_DUMP_METHOD void dump() const;
- LLVM_DUMP_METHOD void dump(raw_ostream &OS) const;
+ LLVM_DUMP_METHOD void
+ dump(raw_ostream &OS,
+ llvm::function_ref<Formula::DelegatePrinter> = nullptr) const;
private:
/// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -161,8 +161,9 @@
/// `Val2` imposed by the flow condition.
bool equivalentFormulas(const Formula &Val1, const Formula &Val2);
- LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token,
- llvm::raw_ostream &OS = llvm::dbgs());
+ LLVM_DUMP_METHOD void
+ dumpFlowCondition(Atom Token, llvm::raw_ostream &OS = llvm::dbgs(),
+ llvm::function_ref<Formula::DelegatePrinter> = nullptr);
/// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
/// returns null.
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
