[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)
```

clang/include/clang/Analysis/FlowSensitive/SimplifyConstraints.h

@@ -0,0 +1,49 @@
+//===-- SimplifyConstraints.h -----------------------------------*- 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H
+
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "llvm/ADT/SetVector.h"
+
+namespace clang {
+namespace dataflow {
+
+/// Information on the way a set of constraints was simplified.
+struct SimplifyConstraintsInfo {
+  /// List of equivalence classes of atoms. For each equivalence class, the
+  /// original constraints imply that all atoms in it must be equivalent.
+  /// Simplification replaces all occurrences of atoms in an equivalence class
+  /// with a single representative atom from the class.
+  /// Does not contain equivalence classes with just one member or atoms
+  /// contained in `TrueAtoms` or `FalseAtoms`.
+  llvm::SmallVector<llvm::SmallVector<Atom>> EquivalentAtoms;
+  /// Atoms that the original constraints imply must be true.
+  /// Simplification replaces all occurrences of these atoms by a true literal
+  /// (which may enable additional simplifications).
+  llvm::SmallVector<Atom> TrueAtoms;
+  /// Atoms that the original constraints imply must be false.
+  /// Simplification replaces all occurrences of these atoms by a false literal
+  /// (which may enable additional simplifications).
+  llvm::SmallVector<Atom> FalseAtoms;
+};
+
+/// Simplifies a set of constraints (implicitly connected by "and") in a way
+/// that does not change satisfiability of the constraints. This does _not_ mean
+/// that the set of solutions is the same before and after simplification.
+/// `Info`, if non-null, will be populated with information about the
+/// simplifications that were made to the formula (e.g. to display to the user).
+void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,
+                         Arena &arena, SimplifyConstraintsInfo *Info = nullptr);
+
+} // namespace dataflow
+} // namespace clang
+
+#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H

clang/lib/Analysis/FlowSensitive/CMakeLists.txt

@@ -7,6 +7,7 @@ add_clang_library(clangAnalysisFlowSensitive
   HTMLLogger.cpp
   Logger.cpp
   RecordOps.cpp
+  SimplifyConstraints.cpp
   Transfer.cpp
   TypeErasedDataflowAnalysis.cpp
   Value.cpp

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";
   }

clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

@@ -961,7 +961,7 @@ void Environment::dump(raw_ostream &OS) const {
     OS << "  [" << L << ", " << V << ": " << *V << "]\n";
   }
 
-  OS << "FlowConditionToken:\n";
+  OS << "\n";
   DACtx->dumpFlowCondition(FlowConditionToken, OS);
 }
 

clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp

@@ -0,0 +1,179 @@
+//===-- SimplifyConstraints.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
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/SimplifyConstraints.h"
+#include "llvm/ADT/EquivalenceClasses.h"
+
+namespace clang {
+namespace dataflow {
+
+// Substitutes all occurrences of a given atom in `F` by a given formula and
+// returns the resulting formula.
+static const Formula &
+substitute(const Formula &F,
+           const llvm::DenseMap<Atom, const Formula *> &Substitutions,
+           Arena &arena) {
+  switch (F.kind()) {
+  case Formula::AtomRef:
+    if (auto iter = Substitutions.find(F.getAtom());
+        iter != Substitutions.end())
+      return *iter->second;
+    return F;
+  case Formula::Literal:
+    return F;
+  case Formula::Not:
+    return arena.makeNot(substitute(*F.operands()[0], Substitutions, arena));
+  case Formula::And:
+    return arena.makeAnd(substitute(*F.operands()[0], Substitutions, arena),
+                         substitute(*F.operands()[1], Substitutions, arena));
+  case Formula::Or:
+    return arena.makeOr(substitute(*F.operands()[0], Substitutions, arena),
+                        substitute(*F.operands()[1], Substitutions, arena));
+  case Formula::Implies:
+    return arena.makeImplies(
+        substitute(*F.operands()[0], Substitutions, arena),
+        substitute(*F.operands()[1], Substitutions, arena));
+  case Formula::Equal:
+    return arena.makeEquals(substitute(*F.operands()[0], Substitutions, arena),
+                            substitute(*F.operands()[1], Substitutions, arena));
+  }
+}
+
+// Returns the result of replacing atoms in `Atoms` with the leader of their
+// equivalence class in `EquivalentAtoms`.
+// Atoms that don't have an equivalence class in `EquivalentAtoms` are inserted
+// into it as single-member equivalence classes.
+static llvm::DenseSet<Atom>
+projectToLeaders(const llvm::DenseSet<Atom> &Atoms,
+                 llvm::EquivalenceClasses<Atom> &EquivalentAtoms) {
+  llvm::DenseSet<Atom> Result;
+
+  for (Atom Atom : Atoms)
+    Result.insert(EquivalentAtoms.getOrInsertLeaderValue(Atom));
+
+  return Result;
+}
+
+// Returns the atoms in the equivalence class for the leader identified by
+// `LeaderIt`.
+static llvm::SmallVector<Atom>
+atomsInEquivalenceClass(const llvm::EquivalenceClasses<Atom> &EquivalentAtoms,
+                        llvm::EquivalenceClasses<Atom>::iterator LeaderIt) {
+  llvm::SmallVector<Atom> Result;
+  for (auto MemberIt = EquivalentAtoms.member_begin(LeaderIt);
+       MemberIt != EquivalentAtoms.member_end(); ++MemberIt)
+    Result.push_back(*MemberIt);
+  return Result;
+}
+
+void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,
+                         Arena &arena, SimplifyConstraintsInfo *Info) {
+  auto contradiction = [&]() {
+    Constraints.clear();
+    Constraints.insert(&arena.makeLiteral(false));
+  };
+
+  llvm::EquivalenceClasses<Atom> EquivalentAtoms;
+  llvm::DenseSet<Atom> TrueAtoms;
+  llvm::DenseSet<Atom> FalseAtoms;
+
+  while (true) {
+    for (const auto *Constraint : Constraints) {
+      switch (Constraint->kind()) {
+      case Formula::AtomRef:
+        TrueAtoms.insert(Constraint->getAtom());
+        break;
+      case Formula::Not:
+        if (Constraint->operands()[0]->kind() == Formula::AtomRef)
+          FalseAtoms.insert(Constraint->operands()[0]->getAtom());
+        break;
+      case Formula::Equal: {
+        ArrayRef<const Formula *> operands = Constraint->operands();
+        if (operands[0]->kind() == Formula::AtomRef &&
+            operands[1]->kind() == Formula::AtomRef) {
+          EquivalentAtoms.unionSets(operands[0]->getAtom(),
+                                    operands[1]->getAtom());
+        }
+        break;
+      }
+      default:
+        break;
+      }
+    }
+
+    TrueAtoms = projectToLeaders(TrueAtoms, EquivalentAtoms);
+    FalseAtoms = projectToLeaders(FalseAtoms, EquivalentAtoms);
+
+    llvm::DenseMap<Atom, const Formula *> Substitutions;
+    for (auto It = EquivalentAtoms.begin(); It != EquivalentAtoms.end(); ++It) {
+      Atom TheAtom = It->getData();
+      Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom);
+      if (TrueAtoms.contains(Leader)) {
+        if (FalseAtoms.contains(Leader)) {
+          contradiction();
+          return;
+        }
+        Substitutions.insert({TheAtom, &arena.makeLiteral(true)});
+      } else if (FalseAtoms.contains(Leader)) {
+        Substitutions.insert({TheAtom, &arena.makeLiteral(false)});
+      } else if (TheAtom != Leader) {
+        Substitutions.insert({TheAtom, &arena.makeAtomRef(Leader)});
+      }
+    }
+
+    llvm::SetVector<const Formula *> NewConstraints;
+    for (const auto *Constraint : Constraints) {
+      const Formula &NewConstraint =
+          substitute(*Constraint, Substitutions, arena);
+      if (&NewConstraint == &arena.makeLiteral(true))
+        continue;
+      if (&NewConstraint == &arena.makeLiteral(false)) {
+        contradiction();
+        return;
+      }
+      if (NewConstraint.kind() == Formula::And) {
+        NewConstraints.insert(NewConstraint.operands()[0]);
+        NewConstraints.insert(NewConstraint.operands()[1]);
+        continue;
+      }
+      NewConstraints.insert(&NewConstraint);
+    }
+
+    if (NewConstraints == Constraints)
+      break;
+    Constraints = std::move(NewConstraints);
+  }
+
+  if (Info) {
+    for (auto It = EquivalentAtoms.begin(), End = EquivalentAtoms.end();
+         It != End; ++It) {
+      if (!It->isLeader())
+        continue;
+      Atom At = *EquivalentAtoms.findLeader(It);
+      if (TrueAtoms.contains(At) || FalseAtoms.contains(At))
+        continue;
+      llvm::SmallVector<Atom> Atoms =
+          atomsInEquivalenceClass(EquivalentAtoms, It);
+      if (Atoms.size() == 1)
+        continue;
+      std::sort(Atoms.begin(), Atoms.end());
+      Info->EquivalentAtoms.push_back(std::move(Atoms));
+    }
+    for (Atom At : TrueAtoms)
+      Info->TrueAtoms.append(atomsInEquivalenceClass(
+          EquivalentAtoms, EquivalentAtoms.findValue(At)));
+    std::sort(Info->TrueAtoms.begin(), Info->TrueAtoms.end());
+    for (Atom At : FalseAtoms)
+      Info->FalseAtoms.append(atomsInEquivalenceClass(
+          EquivalentAtoms, EquivalentAtoms.findValue(At)));
+    std::sort(Info->FalseAtoms.begin(), Info->FalseAtoms.end());
+  }
+}
+
+} // namespace dataflow
+} // namespace clang

clang/unittests/Analysis/FlowSensitive/CMakeLists.txt

@@ -17,6 +17,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
   MultiVarConstantPropagationTest.cpp
   RecordOpsTest.cpp
   SignAnalysisTest.cpp
+  SimplifyConstraintsTest.cpp
   SingleVarConstantPropagationTest.cpp
   SolverTest.cpp
   TestingSupport.cpp