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

[via cfe-commits]

================
@@ -2001,3 +1932,260 @@ 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);
+}
+auto SubsumptionChecker::DNF(const NormalizedConstraint &C) -> DNFFormula {
+  return SubsumptionChecker::Normalize<DNFFormula>(C);
+}
+
+///
+/// \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.
+///
+template <typename FormulaType>
+FormulaType SubsumptionChecker::Normalize(const NormalizedConstraint &NC) {
+  FormulaType Res;
+
+  auto Add = [&, this](Clause C) {
+    // Sort each clause and remove duplicates for faster comparisons
+    std::sort(C.begin(), C.end());
+    C.erase(std::unique(C.begin(), C.end()), C.end());
+    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());
+    Right = Normalize<FormulaType>(NC.getRHS());
+  });
+
+  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()), Add);
+    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));
+    }
+  }
+  return Res;
+}
+
+void SubsumptionChecker::AddUniqueClauseToFormula(Formula &F, Clause C) {
+  for (auto &Other : F) {
+    if (llvm::equal(C, Other))
+      return;
+  }
+  F.push_back(C);
+}
+
+std::optional<bool> SubsumptionChecker::Subsumes(NamedDecl *DP,
+                                                 ArrayRef<const Expr *> P,
+                                                 NamedDecl *DQ,
+                                                 ArrayRef<const Expr *> Q) {
+  const NormalizedConstraint *PNormalized =
+      getNormalizedAssociatedConstraints(SemaRef, DP, P);
+  if (!PNormalized)
+    return std::nullopt;
+
+  const NormalizedConstraint *QNormalized =
+      getNormalizedAssociatedConstraints(SemaRef, DQ, Q);
+  if (!QNormalized)
+    return std::nullopt;
+
+  return Subsumes(PNormalized, QNormalized);
+}
+
+bool SubsumptionChecker::Subsumes(const NormalizedConstraint *P,
+                                  const NormalizedConstraint *Q) {
+
+  DNFFormula DNFP = DNF(*P);
+  CNFFormula CNFQ = CNF(*Q);
+  return Subsumes(DNFP, CNFQ);
+}
+
+bool SubsumptionChecker::Subsumes(const DNFFormula &PDNF,
+                                  const CNFFormula &QCNF) {
+  for (const auto &Pi : PDNF) {
+    for (const auto &Qj : QCNF) {
+      // C++ [temp.constr.order] p2
+      //   - [...] a disjunctive clause Pi subsumes a conjunctive clause Qj if
+      //     and only if there exists an atomic constraint Pia in Pi for which
+      //     there exists an atomic constraint, Qjb, in Qj such that Pia
+      //     subsumes Qjb.
+      if (!DNFSubsumes(Pi, Qj))
+        return false;
+    }
+  }
+  return true;
+}
+
+bool SubsumptionChecker::DNFSubsumes(const Clause &P, const Clause &Q) {
+
+  return llvm::any_of(P, [&](Literal LP) {
+    return llvm::any_of(Q, [this, LP](Literal LQ) { return Subsumes(LP, LQ); });
+  });
+}
+
+bool SubsumptionChecker::Subsumes(const FoldExpandedConstraint *A,
+                                  const FoldExpandedConstraint *B) {
+  std::pair<const FoldExpandedConstraint *, const FoldExpandedConstraint *> Key{
+      A, B};
+
+  auto It = FoldSubsumptionCache.find(Key);
+  if (It == FoldSubsumptionCache.end()) {
+    // C++ [temp.constr.order]
+    // a fold expanded constraint A subsumes another fold expanded
+    // constraint B if they are compatible for subsumption, have the same
+    // fold-operator, and the constraint of A subsumes that of B.
+    bool DoesSubsume =
+        A->Kind == B->Kind &&
+        FoldExpandedConstraint::AreCompatibleForSubsumption(*A, *B) &&
+        Subsumes(&A->Constraint, &B->Constraint);
+    It = FoldSubsumptionCache.try_emplace(std::move(Key), DoesSubsume).first;
+  }
----------------
cor3ntin wrote:

Oh right, subsumes can modify the iterator, that's why!

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