[Clang] Improve subsumption. (#132849)

The main goal of this patch is to improve the
performance of concept subsumption by

- Making sure literal (atomic) clauses are de-duplicated (Whether 2
atomic constraint is established during the initial normal form
production).
 - Eagerly removing duplicated clauses.

This should minimize the risks of exponentially large formulas that can
be produced by a naive {C,D}NF transformation.

While at it, I restructured that part of the code to be a bit clearer.

Subsumption of fold expanded constraint is also cached.

---

Note that removing duplicated clauses seems to be necessary and
sufficient to have acceptable performance on anything that could be
construed as reasonable code.

Ultimately, the number of clauses is always going to be fairly small
(but $2^{fairly\ small}$ is quickly *fairly large*..).

I went too far in the rabbit hole of Tseitin transformations etc, which
was much faster but would then require to check satisfiabiliy to
establish subsumption between some constraints (although it was good
enough to pass all but ones of our tests...).

It doesn't help that the C++ standard has a very specific definition of
subsumption that is really more of an implication...

While that sort of musing is fascinating, it was ultimately a fool's
errand, at least until such time that there is more motivation for a SAT
solver in clang (clang-tidy can after all use z3!).

Here be dragons.

Fixes #122581

Author: cor3ntin

clang/docs/ReleaseNotes.rst

@@ -370,7 +370,8 @@ Bug Fixes to C++ Support
 - Fixed a Clang regression in C++20 mode where unresolved dependent call expressions were created inside non-dependent contexts (#GH122892)
 - Clang now emits the ``-Wunused-variable`` warning when some structured bindings are unused
   and the ``[[maybe_unused]]`` attribute is not applied. (#GH125810)
-- Clang now issues an error when placement new is used to modify a const-qualified variable 
+- Clang no longer crashes when establishing subsumption between some constraint expressions. (#GH122581)
+- Clang now issues an error when placement new is used to modify a const-qualified variable
   in a ``constexpr`` function. (#GH131432)
 
 Bug Fixes to AST Handling

clang/include/clang/Sema/SemaConcept.h

@@ -14,13 +14,14 @@
 #define LLVM_CLANG_SEMA_SEMACONCEPT_H
 #include "clang/AST/ASTConcept.h"
 #include "clang/AST/ASTContext.h"
-#include "clang/AST/Expr.h"
 #include "clang/AST/DeclTemplate.h"
+#include "clang/AST/Expr.h"
 #include "clang/Basic/SourceLocation.h"
+#include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/PointerUnion.h"
+#include "llvm/ADT/STLFunctionalExtras.h"
 #include "llvm/ADT/SmallVector.h"
 #include <optional>
-#include <string>
 #include <utility>
 
 namespace clang {
@@ -56,49 +57,10 @@ struct alignas(ConstraintAlignment) AtomicConstraint {
     }
     return true;
   }
-
-  bool subsumes(ASTContext &C, const AtomicConstraint &Other) const {
-    // 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 [...]
-
-    // We do not actually substitute the parameter mappings into the
-    // constraint expressions, therefore the constraint expressions are
-    // the originals, and comparing them will suffice.
-    if (ConstraintExpr != Other.ConstraintExpr)
-      return false;
-
-    // Check that the parameter lists are identical
-    return hasMatchingParameterMapping(C, Other);
-  }
 };
 
-struct alignas(ConstraintAlignment) FoldExpandedConstraint;
-
-using NormalFormConstraint =
-    llvm::PointerUnion<AtomicConstraint *, FoldExpandedConstraint *>;
-struct NormalizedConstraint;
-using NormalForm =
-    llvm::SmallVector<llvm::SmallVector<NormalFormConstraint, 2>, 4>;
-
-// A constraint is in conjunctive normal form when it is a conjunction of
-// clauses where each clause is a disjunction of atomic constraints. For atomic
-// constraints A, B, and C, the constraint A  ∧ (B  ∨ C) is in conjunctive
-// normal form.
-NormalForm makeCNF(const NormalizedConstraint &Normalized);
-
-// A constraint is in disjunctive normal form when it is a disjunction of
-// clauses where each clause is a conjunction of atomic constraints. For atomic
-// constraints A, B, and C, the disjunctive normal form of the constraint A
-//  ∧ (B  ∨ C) is (A  ∧ B)  ∨ (A  ∧ C).
-NormalForm makeDNF(const NormalizedConstraint &Normalized);
-
 struct alignas(ConstraintAlignment) NormalizedConstraintPair;
+struct alignas(ConstraintAlignment) FoldExpandedConstraint;
 
 /// \brief A normalized constraint, as defined in C++ [temp.constr.normal], is
 /// either an atomic constraint, a conjunction of normalized constraints or a
@@ -170,10 +132,6 @@ struct alignas(ConstraintAlignment) FoldExpandedConstraint {
                          const Expr *Pattern)
       : Kind(K), Constraint(std::move(C)), Pattern(Pattern) {};
 
-  template <typename AtomicSubsumptionEvaluator>
-  bool subsumes(const FoldExpandedConstraint &Other,
-                const AtomicSubsumptionEvaluator &E) const;
-
   static bool AreCompatibleForSubsumption(const FoldExpandedConstraint &A,
                                           const FoldExpandedConstraint &B);
 };
@@ -182,90 +140,102 @@ const NormalizedConstraint *getNormalizedAssociatedConstraints(
     Sema &S, NamedDecl *ConstrainedDecl,
     ArrayRef<const Expr *> AssociatedConstraints);
 
-template <typename AtomicSubsumptionEvaluator>
-bool subsumes(const NormalForm &PDNF, const NormalForm &QCNF,
-              const AtomicSubsumptionEvaluator &E) {
-  // C++ [temp.constr.order] p2
-  //   Then, P subsumes Q if and only if, for every disjunctive clause Pi in the
-  //   disjunctive normal form of P, Pi subsumes every conjunctive clause Qj in
-  //   the conjuctive normal form of Q, where [...]
-  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.
-      bool Found = false;
-      for (NormalFormConstraint Pia : Pi) {
-        for (NormalFormConstraint Qjb : Qj) {
-          if (isa<FoldExpandedConstraint *>(Pia) &&
-              isa<FoldExpandedConstraint *>(Qjb)) {
-            if (cast<FoldExpandedConstraint *>(Pia)->subsumes(
-                    *cast<FoldExpandedConstraint *>(Qjb), E)) {
-              Found = true;
-              break;
-            }
-          } else if (isa<AtomicConstraint *>(Pia) &&
-                     isa<AtomicConstraint *>(Qjb)) {
-            if (E(*cast<AtomicConstraint *>(Pia),
-                  *cast<AtomicConstraint *>(Qjb))) {
-              Found = true;
-              break;
-            }
-          }
-        }
-        if (Found)
-          break;
-      }
-      if (!Found)
-        return false;
-    }
-  }
-  return true;
-}
-
-template <typename AtomicSubsumptionEvaluator>
-bool subsumes(Sema &S, NamedDecl *DP, ArrayRef<const Expr *> P, NamedDecl *DQ,
-              ArrayRef<const Expr *> Q, bool &Subsumes,
-              const AtomicSubsumptionEvaluator &E) {
-  // C++ [temp.constr.order] p2
-  //   In order to determine if a constraint P subsumes a constraint Q, P is
-  //   transformed into disjunctive normal form, and Q is transformed into
-  //   conjunctive normal form. [...]
-  const NormalizedConstraint *PNormalized =
-      getNormalizedAssociatedConstraints(S, DP, P);
-  if (!PNormalized)
-    return true;
-  NormalForm PDNF = makeDNF(*PNormalized);
+/// \brief SubsumptionChecker establishes subsumption
+/// between two set of constraints.
+class SubsumptionChecker {
+public:
+  using SubsumptionCallable = llvm::function_ref<bool(
+      const AtomicConstraint &, const AtomicConstraint &)>;
 
-  const NormalizedConstraint *QNormalized =
-      getNormalizedAssociatedConstraints(S, DQ, Q);
-  if (!QNormalized)
-    return true;
-  NormalForm QCNF = makeCNF(*QNormalized);
-
-  Subsumes = subsumes(PDNF, QCNF, E);
-  return false;
-}
-
-template <typename AtomicSubsumptionEvaluator>
-bool FoldExpandedConstraint::subsumes(
-    const FoldExpandedConstraint &Other,
-    const AtomicSubsumptionEvaluator &E) const {
+  SubsumptionChecker(Sema &SemaRef, SubsumptionCallable Callable = {});
 
-  // [C++26] [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
+  std::optional<bool> Subsumes(NamedDecl *DP, ArrayRef<const Expr *> P,
+                               NamedDecl *DQ, ArrayRef<const Expr *> Q);
 
-  if (Kind != Other.Kind || !AreCompatibleForSubsumption(*this, Other))
-    return false;
+  bool Subsumes(const NormalizedConstraint *P, const NormalizedConstraint *Q);
 
-  NormalForm PDNF = makeDNF(this->Constraint);
-  NormalForm QCNF = makeCNF(Other.Constraint);
-  return clang::subsumes(PDNF, QCNF, E);
-}
+private:
+  Sema &SemaRef;
+  SubsumptionCallable Callable;
+
+  // Each Literal has a unique value that is enough to establish
+  // its identity.
+  // Some constraints (fold expended) require special subsumption
+  // handling logic beyond comparing values, so we store a flag
+  // to let us quickly dispatch to each kind of variable.
+  struct Literal {
+    enum Kind { Atomic, FoldExpanded };
+
+    unsigned Value : 16;
+    LLVM_PREFERRED_TYPE(Kind)
+    unsigned Kind : 1;
+
+    bool operator==(const Literal &Other) const { return Value == Other.Value; }
+    bool operator<(const Literal &Other) const { return Value < Other.Value; }
+  };
+  using Clause = llvm::SmallVector<Literal>;
+  using Formula = llvm::SmallVector<Clause, 5>;
+
+  struct CNFFormula : Formula {
+    static constexpr auto Kind = NormalizedConstraint::CCK_Conjunction;
+    using Formula::Formula;
+  };
+  struct DNFFormula : Formula {
+    static constexpr auto Kind = NormalizedConstraint::CCK_Disjunction;
+    using Formula::Formula;
+  };
+
+  struct MappedAtomicConstraint {
+    AtomicConstraint *Constraint;
+    Literal ID;
+  };
+
+  struct FoldExpendedConstraintKey {
+    FoldExpandedConstraint::FoldOperatorKind Kind;
+    AtomicConstraint *Constraint;
+    Literal ID;
+  };
+
+  llvm::DenseMap<const Expr *, llvm::SmallDenseMap<llvm::FoldingSetNodeID,
+                                                   MappedAtomicConstraint>>
+      AtomicMap;
+
+  llvm::DenseMap<const Expr *, std::vector<FoldExpendedConstraintKey>> FoldMap;
+
+  // A map from a literal to a corresponding associated constraint.
+  // We do not have enough bits left for a pointer union here :(
+  llvm::DenseMap<uint16_t, void *> ReverseMap;
+
+  // Fold expanded constraints ask us to recursively establish subsumption.
+  // This caches the result.
+  llvm::SmallDenseMap<
+      std::pair<const FoldExpandedConstraint *, const FoldExpandedConstraint *>,
+      bool>
+      FoldSubsumptionCache;
+
+  // Each <atomic, fold expanded constraint> is represented as a single ID.
+  // This is intentionally kept small we can't handle a large number of
+  // constraints anyway.
+  uint16_t NextID;
+
+  bool Subsumes(const DNFFormula &P, const CNFFormula &Q);
+  bool Subsumes(Literal A, Literal B);
+  bool Subsumes(const FoldExpandedConstraint *A,
+                const FoldExpandedConstraint *B);
+  bool DNFSubsumes(const Clause &P, const Clause &Q);
+
+  CNFFormula CNF(const NormalizedConstraint &C);
+  DNFFormula DNF(const NormalizedConstraint &C);
+
+  template <typename FormulaType>
+  FormulaType Normalize(const NormalizedConstraint &C);
+  void AddUniqueClauseToFormula(Formula &F, Clause C);
+
+  Literal find(AtomicConstraint *);
+  Literal find(FoldExpandedConstraint *);
+
+  uint16_t getNewLiteralId();
+};
 
 } // clang