[clang][dataflow] Simplify flow conditions displayed in HTMLLogger. (#70848)

This can make the flow condition significantly easier to interpret; see
below
for an example.

I had hoped that adding the simplification as a preprocessing step
before the
SAT solver (in `DataflowAnalysisContext::querySolver()`) would also
speed up SAT
solving and maybe even eliminate SAT solver timeouts, but in my testing,
this
actually turns out to be a pessimization. It appears that these
simplifications
are easy enough for the SAT solver to perform itself.

Nevertheless, the improvement in debugging alone makes this a worthwhile
change.

Example of flow condition output with these changes:

```
Flow condition token: V37
Constraints:
(V16 = (((V15 & (V19 = V12)) & V22) & V25))
(V15 = ((V12 & ((V14 = V9) | (V14 = V4))) & (V13 = V14)))
True atoms: (V0, V1, V2, V5, V6, V7, V29, V30, V32, V34, V35, V37)
False atoms: (V3, V8, V17)
Equivalent atoms:
(V11, V15)

Flow condition constraints before simplification:
V37
((!V3 & !V8) & !V17)
(V37 = V34)
(V34 = (V29 & (V35 = V30)))
(V29 = (((V16 | V2) & V32) & (V30 = V32)))
(V16 = (((V15 & (V19 = V12)) & V22) & V25))
(V15 = V11)
(V11 = ((((V7 | V2) & V12) & ((V7 & (V14 = V9)) | (V2 & (V14 = V4)))) & (V13 = V14)))
(V2 = V1)
(V1 = V0)
V0
(V7 = V6)
(V6 = V5)
(V5 = V2)
```

1 files changed, 39 insertions, 1 deletions

diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 40de6cd..9c15c87 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -17,6 +17,7 @@
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Logger.h"
+#include "clang/Analysis/FlowSensitive/SimplifyConstraints.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/SetOperations.h"
 #include "llvm/ADT/SetVector.h"
@@ -205,13 +206,50 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
   }
 }
 
+static void printAtomList(const llvm::SmallVector<Atom> &Atoms,
+                          llvm::raw_ostream &OS) {
+  OS << "(";
+  for (size_t i = 0; i < Atoms.size(); ++i) {
+    OS << Atoms[i];
+    if (i + 1 < Atoms.size())
+      OS << ", ";
+  }
+  OS << ")\n";
+}
+
 void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
                                                 llvm::raw_ostream &OS) {
   llvm::SetVector<const Formula *> Constraints;
   Constraints.insert(&arena().makeAtomRef(Token));
   addTransitiveFlowConditionConstraints(Token, Constraints);
 
-  for (const auto *Constraint : Constraints) {
+  OS << "Flow condition token: " << Token << "\n";
+  SimplifyConstraintsInfo Info;
+  llvm::SetVector<const Formula *> OriginalConstraints = Constraints;
+  simplifyConstraints(Constraints, arena(), &Info);
+  if (!Constraints.empty()) {
+    OS << "Constraints:\n";
+    for (const auto *Constraint : Constraints) {
+      Constraint->print(OS);
+      OS << "\n";
+    }
+  }
+  if (!Info.TrueAtoms.empty()) {
+    OS << "True atoms: ";
+    printAtomList(Info.TrueAtoms, OS);
+  }
+  if (!Info.FalseAtoms.empty()) {
+    OS << "False atoms: ";
+    printAtomList(Info.FalseAtoms, OS);
+  }
+  if (!Info.EquivalentAtoms.empty()) {
+    OS << "Equivalent atoms:\n";
+    for (const llvm::SmallVector<Atom> Class : Info.EquivalentAtoms)
+      printAtomList(Class, OS);
+  }
+
+  OS << "\nFlow condition constraints before simplification:\n";
+  for (const auto *Constraint : OriginalConstraints) {
     Constraint->print(OS);
     OS << "\n";
   }