[clang] [Clang] Improve subsumption. (PR #132849)

[via cfe-commits]

================
@@ -2001,3 +1932,318 @@ NormalizedConstraint::getFoldExpandedConstraint() const {
          "getFoldExpandedConstraint called on non-fold-expanded constraint.");
   return cast<FoldExpandedConstraint *>(Constraint);
 }
+
+//
+//
+// ------------------------ Subsumption -----------------------------------
+//
+//
+
+template <> struct llvm::DenseMapInfo<llvm::FoldingSetNodeID> {
+
+  static FoldingSetNodeID getEmptyKey() {
+    FoldingSetNodeID ID;
+    ID.AddInteger(std::numeric_limits<unsigned>::max());
+    return ID;
+  }
+
+  static FoldingSetNodeID getTombstoneKey() {
+    FoldingSetNodeID ID;
+    for (unsigned I = 0; I < sizeof(ID) / sizeof(unsigned); ++I) {
+      ID.AddInteger(std::numeric_limits<unsigned>::max());
+    }
+    return ID;
+  }
+
+  static unsigned getHashValue(const FoldingSetNodeID &Val) {
+    return Val.ComputeHash();
+  }
+
+  static bool isEqual(const FoldingSetNodeID &LHS,
+                      const FoldingSetNodeID &RHS) {
+    return LHS == RHS;
+  }
+};
+
+SubsumptionChecker::SubsumptionChecker(Sema &SemaRef,
+                                       SubsumptionCallable Callable)
+    : SemaRef(SemaRef), Callable(Callable), NextID(1) {}
+
+uint16_t SubsumptionChecker::getNewLiteralId() {
+  assert((unsigned(NextID) + 1 < std::numeric_limits<uint16_t>::max()) &&
+         "too many constraints!");
+  return NextID++;
+}
+
+auto SubsumptionChecker::find(AtomicConstraint *Ori) -> Literal {
+  auto &Elems = AtomicMap[Ori->ConstraintExpr];
+  // C++ [temp.constr.order] p2
+  //   - an atomic constraint A subsumes another atomic constraint B
+  //     if and only if the A and B are identical [...]
+  //
+  // C++ [temp.constr.atomic] p2
+  //   Two atomic constraints are identical if they are formed from the
+  //   same expression and the targets of the parameter mappings are
+  //   equivalent according to the rules for expressions [...]
+
+  // Because subsumption of atomic constraints is an identity
+  // relationship that does not require further analysis
+  // We cache the results such that if an atomic constraint literal
+  // subsumes another, their literal will be the same
+
+  llvm::FoldingSetNodeID ID;
+  const auto &Mapping = Ori->ParameterMapping;
+  ID.AddBoolean(Mapping.has_value());
+  if (Mapping) {
+    for (unsigned I = 0, S = Mapping->size(); I < S; ++I) {
+      SemaRef.getASTContext()
+          .getCanonicalTemplateArgument((*Mapping)[I].getArgument())
+          .Profile(ID, SemaRef.getASTContext());
+    }
+  }
+  auto It = Elems.find(ID);
+  if (It == Elems.end()) {
+    It =
+        Elems
+            .insert({ID, MappedAtomicConstraint{Ori, Literal{getNewLiteralId(),
+                                                             Literal::Atomic}}})
+            .first;
+    ReverseMap[It->second.ID.Value] = Ori;
+  }
+  return It->getSecond().ID;
+}
+
+auto SubsumptionChecker::find(FoldExpandedConstraint *Ori) -> Literal {
+  auto &Elems = FoldMap[Ori->Pattern];
+
+  FoldExpendedConstraintKey K;
+  K.Kind = Ori->Kind;
+
+  auto It = llvm::find_if(Elems, [&K](const FoldExpendedConstraintKey &Other) {
+    return K.Kind == Other.Kind;
+  });
+  if (It == Elems.end()) {
+    K.ID = {getNewLiteralId(), Literal::FoldExpanded};
+    It = Elems.insert(Elems.end(), std::move(K));
+    ReverseMap[It->ID.Value] = Ori;
+  }
+  return It->ID;
+}
+
+auto SubsumptionChecker::CNF(const NormalizedConstraint &C) -> CNFFormula {
+  return SubsumptionChecker::Normalize<CNFFormula>(C, DNFFormula::Kind);
+}
+auto SubsumptionChecker::DNF(const NormalizedConstraint &C) -> DNFFormula {
+  return SubsumptionChecker::Normalize<DNFFormula>(C, DNFFormula::Kind);
+}
+
+///
+/// \brief SubsumptionChecker::Normalize
+///
+/// Normalize a formula to Conjunctive Normal Form or
+/// Disjunctive normal form.
+///
+/// Each Atomic (and Fold Expanded) constraint gets represented by
+/// a single id to reduce space.
+///
+/// To minimize risks of exponential blow up, if two atomic
+/// constraints subsumes each other (same constraint and mapping),
+/// they are represented by the same literal.
+///
+/// Redundant clauses (ie clauses that are fully subsumed) by other
+/// clauses in the same formula are removed.
+template <typename FormulaType>
+FormulaType SubsumptionChecker::Normalize(
+    const NormalizedConstraint &NC,
+    NormalizedConstraint::CompoundConstraintKind ParentKind) {
+  FormulaType Res;
+
+  bool ParentWillDoCrossProduct = ParentKind != FormulaType::Kind;
+
+  auto Add = [&, this](Clause C, bool RemoveRedundantClause) {
+    // Sort each clause and remove duplicates for faster comparision
+    // Both AddClauseToFormula and IsSuperSet require sorted, uniqued literals.
+    std::sort(C.begin(), C.end());
+    C.erase(std::unique(C.begin(), C.end()), C.end());
+
+    // Because the caller may produce the cross product of the clauses
+    // we need to be careful not to remove clauses that could be
+    // combined by the parent.
+    if (!ParentWillDoCrossProduct && RemoveRedundantClause)
+      AddNonRedundantClauseToFormula(Res, std::move(C));
+    else
+      AddUniqueClauseToFormula(Res, std::move(C));
+  };
+
+  if (NC.isAtomic())
+    return {{find(NC.getAtomicConstraint())}};
+
+  if (NC.isFoldExpanded())
+    return {{find(NC.getFoldExpandedConstraint())}};
+
+  FormulaType Left, Right;
+  SemaRef.runWithSufficientStackSpace(SourceLocation(), [&] {
+    Left = Normalize<FormulaType>(NC.getLHS(), NC.getCompoundKind());
+    Right = Normalize<FormulaType>(NC.getRHS(), NC.getCompoundKind());
+  });
+
+  if (NC.getCompoundKind() == FormulaType::Kind) {
+    Res = std::move(Left);
+    Res.reserve(Left.size() + Right.size());
+    std::for_each(std::make_move_iterator(Right.begin()),
+                  std::make_move_iterator(Right.end()), [&](Clause C) {
+                    Add(std::move(C),
+                        FormulaType::Kind ==
+                            NormalizedConstraint::CCK_Disjunction);
+                  });
+    return Res;
+  }
+
+  Res.reserve(Left.size() * Right.size());
+  for (const auto &LTransform : Left) {
+    for (const auto &RTransform : Right) {
+      Clause Combined;
+      Combined.reserve(LTransform.size() + RTransform.size());
+      std::copy(LTransform.begin(), LTransform.end(),
+                std::back_inserter(Combined));
+      std::copy(RTransform.begin(), RTransform.end(),
+                std::back_inserter(Combined));
+      Add(std::move(Combined),
+          FormulaType::Kind == NormalizedConstraint::CCK_Conjunction);
+    }
+  }
+  return Res;
+}
+
+// Remove redundant clauses.
+// This is fairly crude, but we expect the number of clauses to be
+// small-ish and the number of literals to be small
+void SubsumptionChecker::AddNonRedundantClauseToFormula(Formula &F, Clause C) {
+  bool Added = false;
+  for (auto &Other : F) {
+    // Forward subsume: nothing to do
+    if (IsSuperSet(Other, C))
+      return;
+    // Backward subsume: replace other clauses
+    if (IsSuperSet(C, Other)) {
+      Other = C;
+      Added = true;
+    }
+  }
+  if (!Added)
+    F.push_back(C);
+}
+
+void SubsumptionChecker::AddUniqueClauseToFormula(Formula &F, Clause C) {
+  for (auto &Other : F) {
+    if (llvm::equal(C, Other))
+      return;
+  }
+  F.push_back(C);
+}
+
+bool SubsumptionChecker::IsSuperSet(const Clause &A, const Clause &B) {
+  if (B.size() > A.size())
+    return false;
+  Clause::const_iterator At = A.begin();
+  Clause::const_iterator Bt = B.begin();
+  for (; At != A.end() && Bt != B.end();) {
----------------
Sirraide wrote:

```suggestion
  while (At != A.end() && Bt != B.end()) {
```

https://github.com/llvm/llvm-project/pull/132849