[clang][dataflow] Add DataflowEnvironment::dump()

[gribozavr]

Summary

Start by dumping the flow condition.

[gribozavr]

Moved some changes to a different revision

[gribozavr]

Reverted more changes broken out to separate revisions

[ymandel]

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

93–96

I thought there's join-strings function somewhere...

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

 #include "clang/AST/Decl.h"
 #include "clang/AST/Expr.h"
 #include "clang/AST/TypeOrdering.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #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>
 #include <utility>
 #include <vector>
 
 namespace clang {
 namespace dataflow {
public:
   /// identified by `Token` are always true.
   bool flowConditionIsTautology(AtomicBoolValue &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 equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
 
+  LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token);
+
 private:
   struct NullableQualTypeDenseMapInfo : private llvm::DenseMapInfo<QualType> {
     static QualType getEmptyKey() {
       // Allow a NULL `QualType` by using a different value as the empty key.
       return QualType::getFromOpaquePtr(reinterpret_cast<Type *>(1));
     }
 
     using DenseMapInfo::getHashValue;

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

 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWENVIRONMENT_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWENVIRONMENT_H
 
 #include "clang/AST/Decl.h"
 #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"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
 #include <memory>
 #include <type_traits>
public:
 
   /// Adds `Val` to the set of clauses that constitute the flow condition.
   void addToFlowCondition(BoolValue &Val);
 
   /// Returns true if and only if the clauses that constitute the flow condition
   /// 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.
   ///
   /// 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
   /// creating a cyclic dependency with self-referential pointers/references.

clang/include/clang/Analysis/FlowSensitive/DebugSupport.h

 #include <vector>
 
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 
 namespace clang {
 namespace dataflow {
+
 /// Returns a string representation for the boolean value `B`.
 ///
 /// Atomic booleans appearing in the boolean value `B` 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 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.
 ///
 /// Atomic booleans appearing in `Constraints` and `Result` are assigned to
 /// labels either specified in `AtomNames` or created by default rules as B0,
 /// B1, ...
 ///
 /// Requirements:
 ///

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

 //===-- DataflowAnalysisContext.cpp -----------------------------*- C++ -*-===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines a DataflowAnalysisContext class that owns objects that
 //  encompass the state of a program and stores context that is used during
 //  dataflow analysis.
 //
 //===----------------------------------------------------------------------===//
 
 #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>
 
 namespace clang {
 namespace dataflow {
 
 StorageLocation &
for (AtomicBoolValue *DepToken : DepsIT->second) {
       auto &NewDep = buildAndSubstituteFlowConditionWithCache(
           *DepToken, SubstitutionsCache);
       SubstitutionsCache[DepToken] = &NewDep;
     }
   }
   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
 
 using namespace clang;
 
 const Expr &clang::dataflow::ignoreCFGOmittedNodes(const Expr &E) {
   const Expr *Current = &E;
   if (auto *EWC = dyn_cast<ExprWithCleanups>(Current)) {

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

 //  that run over Control-Flow Graphs (CFGs) to keep track of the state of the
 //  program at given program points.
 //
 //===----------------------------------------------------------------------===//
 
 #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"
 #include "llvm/Support/Casting.h"
 #include "llvm/Support/ErrorHandling.h"
 #include <cassert>
 #include <memory>
 #include <utility>

 void Environment::addToFlowCondition(BoolValue &Val) {
   DACtx->addFlowConditionConstraint(*FlowConditionToken, Val);
 }
 
 bool Environment::flowConditionImplies(BoolValue &Val) const {
   return DACtx->flowConditionImplies(*FlowConditionToken, Val);
 }
 
+void Environment::dump() const {
+  DACtx->dumpFlowCondition(*FlowConditionToken);
+}
+
 } // namespace dataflow
 } // namespace clang

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

 //===----------------------------------------------------------------------===//
 
 #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/STLExtras.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 {
std::string debugString(const BoolValue &B, size_t Depth = 0) {
     }
     default:
       llvm_unreachable("Unhandled value kind");
     }
     auto Indent = Depth * 4;
     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,
                           const Solver::Result &Result) {
     auto Template = R"(
 Constraints
 ------------
 {0:$[
std::string debugString(
     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());
+    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:

 
 std::string
 debugString(const BoolValue &B,
             llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
   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(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

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

(and
         B0)
     (or
         True
         B1)))";
   EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
               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());
   return WatchedLiteralsSolver().solve(std::move(ConstraintsSet));
 }
 
 TEST(SATCheckDebugStringTest, AtomicBoolean) {
   // B0