[dataflow] HTMLLogger: meaningful names for flow condition variables

[sammccall]

Summary

Instead of meaningless "V7", use the name "B3:1" for the flow condition
of the first analysis of basic block 3.

[xazax.hun]

Should we have some documentation or tooltip explaining the users what the meaning of those names are?

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

public:
   /// identified by `Token` are always true.
   bool flowConditionIsTautology(Atom Token);
 
   /// Returns true if `Val1` is equivalent to `Val2`.
   /// Note: This function doesn't take into account constraints on `Val1` and
   /// `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.
   const ControlFlowContext *getControlFlowContext(const FunctionDecl *F);
 
   const Options &getOptions() { return Opts; }
 
   Arena &arena() { return *A; }

clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h

public:
   bool canDescend(unsigned MaxDepth, const DeclContext *Callee) const;
 
   /// Returns the `DataflowAnalysisContext` used by the environment.
   DataflowAnalysisContext &getDataflowAnalysisContext() const { return *DACtx; }
 
   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
   /// return null.
   ///
   /// Recursively initializes storage locations and values until it sees a
   /// self-referential pointer or reference type. `Visited` is used to track
   /// which types appeared in the reference/pointer chain in order to avoid

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
   if (DepsIt != FlowConditionDeps.end()) {
     for (Atom DepToken : DepsIt->second) {
       addTransitiveFlowConditionConstraints(DepToken, Constraints,
                                             VisitedTokens);
     }
   }
 }
 
-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);
 
   // TODO: have formulas know about true/false directly instead
   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;
     }
     if (&F == &False) {
       OS << "False";
       return true;
     }

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

 
 bool Environment::flowConditionImplies(const Formula &Val) const {
   return DACtx->flowConditionImplies(FlowConditionToken, Val);
 }
 bool Environment::flowConditionImplies(BoolValue &Val) const {
   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";
   for (auto [D, L] : DeclToLoc)
     OS << "  [" << D->getNameAsString() << ", " << L << "]\n";
 
   OS << "ExprToLoc:\n";
   for (auto [E, L] : ExprToLoc)
     OS << "  [" << E << ", " << L << "]\n";
 
   OS << "LocToVal:\n";
   for (auto [L, V] : LocToVal) {
     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 {
   dump(llvm::dbgs());
 }
 
 AggregateStorageLocation *
 getImplicitObjectLocation(const CXXMemberCallExpr &MCE,

clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp

class HTMLLogger : public Logger {
   std::unique_ptr<llvm::raw_ostream> OS;
   std::optional<llvm::json::OStream> JOS;
 
   const ControlFlowContext *CFG;
   // Timeline of iterations of CFG block visitation.
   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.
   unsigned ElementIndex;
 
 public:
   explicit HTMLLogger(StreamFactory Streams) : Streams(std::move(Streams)) {}
   void beginAnalysis(const ControlFlowContext &CFG,
public:
   // FIXME: this dump is fairly opaque. We should show:
   //  - values associated with the current Stmt
   //  - values associated with its children
   //  - meaningful names for values
   //  - which boolean values are implied true/false by the flow condition
   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);
       JOS->attribute("element", ElementIndex);
 
       // If this state immediately follows an Expr, show its built-in model.
       if (ElementIndex > 0) {
         auto S =
             Iters.back().first->Elements[ElementIndex - 1].getAs<CFGStmt>();
         if (const Expr *E = S ? llvm::dyn_cast<Expr>(S->getStmt()) : nullptr)
           if (auto *Loc = State.Env.getStorageLocation(*E, SkipPast::None))
             JOS->attributeObject(
                 "value", [&] { ModelDumper(*JOS, State.Env).dump(*Loc); });
       }
       if (!ContextLogs.empty()) {
         JOS->attribute("logs", ContextLogs);
         ContextLogs.clear();
       }
       {
         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);
       }
     });
   }
   void blockConverged() override { logText("Block converged"); }
 
   void logText(llvm::StringRef S) override {
     ContextLogs.append(S.begin(), S.end());