[Clang] Improve subsumption. #132849
Merged
[Clang] Improve subsumption. #132849
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 redundant clauses.
This should minimize the risks of exponentially-large
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 redundant clauses (even naively)
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 llvm#122581
llvmbot
added
clang
|
@llvm/pr-subscribers-clang Author: cor3ntin (cor3ntin) ChangesThe main goal of this patch is to improve the
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 redundant clauses (even naively) 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 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 Patch is 34.06 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/132849.diff 4 Files Affected:
diff --git a/clang/docs/ReleaseNotes.rst b/clang/docs/ReleaseNotes.rst
index 2f15c90ab1583..05bde5c9cc1d1 100644
--- a/clang/docs/ReleaseNotes.rst
+++ b/clang/docs/ReleaseNotes.rst
@@ -358,6 +358,7 @@ 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 no longer crash when establishing subsumption between some constraint expressions. (#GH122581)
Bug Fixes to AST Handling
^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/clang/include/clang/Sema/SemaConcept.h b/clang/include/clang/Sema/SemaConcept.h
index 5c599a70532f6..87fee1678fb05 100644
--- a/clang/include/clang/Sema/SemaConcept.h
+++ b/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,102 +132,113 @@ 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);
+
+ llvm::FoldingSetNodeID ProfileForSubsumption() const;
};
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) requires 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 AddClauseToFormula(Formula &F, Clause C);
+ bool IsSuperSet(const Clause &A, const Clause &B);
+
+ Literal find(AtomicConstraint *);
+ Literal find(FoldExpandedConstraint *);
+
+ uint16_t getNewId();
+};
} // clang
diff --git a/clang/lib/Sema/SemaConcept.cpp b/clang/lib/Sema/SemaConcept.cpp
index 57dc4154a537f..b16dac9c08dec 100644
--- a/clang/lib/Sema/SemaConcept.cpp
+++ b/clang/lib/Sema/SemaConcept.cpp
@@ -1726,71 +1726,6 @@ bool FoldExpandedConstraint::AreCompatibleForSubsumption(
return false;
}
-NormalForm clang::makeCNF(const NormalizedConstraint &Normalized) {
- if (Normalized.isAtomic())
- return {{Normalized.getAtomicConstraint()}};
-
- else if (Normalized.isFoldExpanded())
- return {{Normalized.getFoldExpandedConstraint()}};
-
- NormalForm LCNF = makeCNF(Normalized.getLHS());
- NormalForm RCNF = makeCNF(Normalized.getRHS());
- if (Normalized.getCompoundKind() == NormalizedConstraint::CCK_Conjunction) {
- LCNF.reserve(LCNF.size() + RCNF.size());
- while (!RCNF.empty())
- LCNF.push_back(RCNF.pop_back_val());
- return LCNF;
- }
-
- // Disjunction
- NormalForm Res;
- Res.reserve(LCNF.size() * RCNF.size());
- for (auto &LDisjunction : LCNF)
- for (auto &RDisjunction : RCNF) {
- NormalForm::value_type Combined;
- Combined.reserve(LDisjunction.size() + RDisjunction.size());
- std::copy(LDisjunction.begin(), LDisjunction.end(),
- std::back_inserter(Combined));
- std::copy(RDisjunction.begin(), RDisjunction.end(),
- std::back_inserter(Combined));
- Res.emplace_back(Combined);
- }
- return Res;
-}
-
-NormalForm clang::makeDNF(const NormalizedConstraint &Normalized) {
- if (Normalized.isAtomic())
- return {{Normalized.getAtomicConstraint()}};
-
- else if (Normalized.isFoldExpanded())
- return {{Normalized.getFoldExpandedConstraint()}};
-
- NormalForm LDNF = makeDNF(Normalized.getLHS());
- NormalForm RDNF = makeDNF(Normalized.getRHS());
- if (Normalized.getCompoundKind() == NormalizedConstraint::CCK_Disjunction) {
- LDNF.reserve(LDNF.size() + RDNF.size());
- while (!RDNF.empty())
- LDNF.push_back(RDNF.pop_back_val());
- return LDNF;
- }
-
- // Conjunction
- NormalForm Res;
- Res.reserve(LDNF.size() * RDNF.size());
- for (auto &LConjunction : LDNF) {
- for (auto &RConjunction : RDNF) {
- NormalForm::value_type Combined;
- Combined.reserve(LConjunction.size() + RConjunction.size());
- std::copy(LConjunction.begin(), LConjunction.end(),
- std::back_inserter(Combined));
- std::copy(RConjunction.begin(), RConjunction.end(),
- std::back_inserter(Combined));
- Res.emplace_back(Combined);
- }
- }
- return Res;
-}
-
bool Sema::IsAtLeastAsConstrained(NamedDecl *D1,
MutableArrayRef<const Expr *> AC1,
NamedDecl *D2,
@@ -1842,18 +1777,21 @@ bool Sema::IsAtLeastAsConstrained(NamedDecl *D1,
}
}
- if (clang::subsumes(
- *this, D1, AC1, D2, AC2, Result,
- [this](const AtomicConstraint &A, const AtomicConstraint &B) {
- return A.subsumes(Context, B);
- }))
+ SubsumptionChecker SC(*this);
+ std::optional<bool> Subsumes = SC.Subsumes(D1, AC1, D2, AC2);
+ if (!Subsumes) {
+ // Normalization failed
return true;
- SubsumptionCache.try_emplace(Key, Result);
+ }
+ Result = *Subsumes;
+ SubsumptionCache.try_emplace(Key, *Subsumes);
return false;
}
-bool Sema::MaybeEmitAmbiguousAtomicConstraintsDiagnostic(NamedDecl *D1,
- ArrayRef<const Expr *> AC1, NamedDecl *D2, ArrayRef<const Expr *> AC2) {
+bool Sema::MaybeEmitAmbiguousAtomicConstraintsDiagnostic(
+ NamedDecl *D1, ArrayRef<const Expr *> AC1, NamedDecl *D2,
+ ArrayRef<const Expr *> AC2) {
+
if (isSFINAEContext())
// No need to work here because our notes would be discarded.
return false;
@@ -1861,32 +1799,27 @@ bool Sema::MaybeEmitAmbiguousAtomicConstraintsDiagnostic(NamedDecl *D1,
if (AC1.empty() || AC2.empty())
return false;
- auto NormalExprEvaluator =
- [this] (const AtomicConstraint &A, const AtomicConstraint &B) {
- return A.subsumes(Context, B);
- };
-
const Expr *AmbiguousAtomic1 = nullptr, *AmbiguousAtomic2 = nullptr;
- auto IdenticalExprEvaluator =
- [&] (const AtomicConstraint &A, const AtomicConstraint &B) {
- if (!A.hasMatchingParameterMapping(Context, B))
- return false;
- const Expr *EA = A.ConstraintExpr, *EB = B.ConstraintExpr;
- if (EA == EB)
- return true;
-
- // Not the same source level expression - are the expressions
- // identical?
- llvm::FoldingSetNodeID IDA, IDB;
- EA->Profile(IDA, Context, /*Canonical=*/true);
- EB->Profile(IDB, Context, /*Canonical=*/true);
- if (IDA != IDB)
- return false;
-
- AmbiguousAtomic1 = EA;
- AmbiguousAtomic2 = EB;
- return true;
- };
+ auto IdenticalExprEvaluator = [&](const AtomicConstraint &A,
+ const AtomicConstraint &B) {
+ if (!A.hasMatchingParameterMapping(Context, B))
+ return false;
+ const Expr *EA = A.ConstraintExpr, *EB = B.ConstraintExpr;
+ if (EA == EB)
+ return true;
+
+ // Not the same source level expression - are the expressions
+ // identical?
+ llvm::FoldingSetNodeID IDA, IDB;
+ EA->Profile(IDA, Context, /*Canonical=*/true);
+ EB->Profile(IDB, Context, /*Canonical=*/true);
+ if (IDA != IDB)
+ return false;
+
+ AmbiguousAtomic1 = EA;
+ AmbiguousAtomic2 = EB;
+ return true;
+ };
{
// The subsumption checks might cause diagnostics
@@ -1894,27 +1827,25 @@ bool Sema::MaybeEmitAmbiguousAtomicConstraintsDiagnostic(NamedDecl *D1,
auto *Normalized1 = getNormalizedAssociatedConstraints(D1, AC1);
if (!Normalized1)
return false;
- const NormalForm DNF1 = makeDNF(*Normalized1);
- const NormalForm CNF1 = makeCNF(*Normalized1);
auto *Normalized2 = getNormalizedAssociatedConstraints(D2, AC2);
if (!Normalized2)
return false;
- const NormalForm DNF2 = makeDNF(*Normalized2);
- const NormalForm CNF2 = makeCNF(*Normalized2);
-
- bool Is1AtLeastAs2Normally =
- clang::subsumes(DNF1, CNF2, NormalExprEvaluator);
- bool Is2AtLeastAs1Normally =
- clang::subsumes(DNF2, CNF1, NormalExprEvaluator);
- bool Is1AtLeastAs2 = clang::subsumes(DNF1, CNF2, IdenticalExprEvaluator);
- bool Is2AtLeastAs1 = clang::subsumes(DNF2, CNF1, IdenticalExprEvaluator);
+
+ SubsumptionChecker SC(*this);
+
+ bool Is1AtLeastAs2Normally = SC.Subsumes(Normalized1, Normalized2);
+ bool Is2AtLeastAs1Normally = SC.Subsumes(Normalized2, Normalized1);
+
+ SubsumptionChecker SC2(*this, IdenticalExprEvaluator);
+ bool Is1AtLeastAs2 = SC2.Subsumes(Normalized1, Normalized2);
+ bool Is2AtLeastAs1 = SC2.Subsumes(Normalized2, Normalized1);
+
if (Is1AtLeastAs2 == Is1AtLeastAs2Normally &&
Is2AtLeastAs1 == Is2AtLeastAs1Normally)
// Same result - no ambiguity was caused by identical atomic expressions.
return false;
}
-
// A different result! Some ambiguous atomic constraint(s) caused a difference
assert(AmbiguousAtomic1 && AmbiguousAtomic2);
@@ -2001,3 +1932,304 @@ NormalizedConstraint::getFoldExpandedConstraint() const {
"getFoldExpandedConstraint called on non-fold-expanded constraint.");
return cast<FoldExpandedConstraint *>(Constraint);
}
+
+//
+//
+// -------------------------------------------------------------------------
+//
+//
+
+/// \name 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 (size_t 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) {}
+
+auto SubsumptionChecker::getNewId() -> uint16_t {
+ 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()
+ .getCa...
[truncated]
|
shafik
reviewed
Mar 25, 2025
zyn0217
reviewed
Mar 25, 2025
|
✅ With the latest revision this PR passed the C/C++ code formatter. |
Removing redundant clauses while producing a cross products was unsound.
Comment on lines
+2004
to
+2012
| 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; | ||
| } |
There was a problem hiding this comment.
It would be nice if we can avoid the repeated map lookup (find and insert) with try_emplace. Does llvm have a utility like with_result_of so we can make the construction of MappedAtomicConstraint lazy and therefore write something like the following?
auto [It, Inserted] = Elems.try_emplace(ID, llvm::with_result_of([&] {
return MappedAtomicConstraint{Ori, Literal{getNewLiteralId(),
Literal::Atomic}};
}));
if (Inserted)
ReverseMap[It->second.ID.Value] = Ori;There was a problem hiding this comment.
That would be quite nice indeed, but that does not exist yet!
Comment on lines
+2157
to
+2171
| 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; | ||
| } |
There was a problem hiding this comment.
I think this repeated map lookup can be avoided without the need for with_result_of:
Suggested change
| 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; | |
| } | |
| auto [It, Inserted] = FoldSubsumptionCache.try_emplace({A, B}); | |
| if (Inserted) { | |
| // 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->second = DoesSubsume; | |
| } |
There was a problem hiding this comment.
This leads to a crash, I'm not sure why (we do similar things elsewhere) - but either way I'm not concerned about the double lookup here
There was a problem hiding this comment.
Oh right, subsumes can modify the iterator, that's why!
zyn0217
approved these changes
Mar 27, 2025
| static bool AreCompatibleForSubsumption(const FoldExpandedConstraint &A, | ||
| const FoldExpandedConstraint &B); | ||
|
|
||
| llvm::FoldingSetNodeID ProfileForSubsumption() const; |
There was a problem hiding this comment.
I think naming it Profile is enough? After all the class is not used for other purposes
(Just want to keep it consistent with other Profile functions)
There was a problem hiding this comment.
Oh, that's actually not used, I should get rid of it thanks!
There was a problem hiding this comment.
Do we want to retain the profiling information? Actually, should we be adding some time trace report support to this so users can track how much time is spent on subsumption in their headers?
There was a problem hiding this comment.
This was just a (poorly named) attempt to produce a cache key for atomic constraint generically (we do it in two places but both places do it differently) - i just forgot to cleanup after myself
Actually, should we be adding some time trace report support to this so users can track how much time is spent on subsumption in their headers?
Completely unrelated but it might be a good in a follow up. But what we should profile there is more "how much time is spent finding the most constraint candidate"
There was a problem hiding this comment.
This was just a (poorly named) attempt to produce a cache key for atomic constraint generically (we do it in two places but both places do it differently) - i just forgot to cleanup after myself
Ah, yeah, I think I figured that out after posting the comment. Removal makes sense to me now.
Completely unrelated but it might be a good in a follow up. But what we should profile there is more "how much time is spent finding the most constraint candidate"
Yeah, follow-up is fine by me. I think what would be interesting to profile is "how much time is spent determining whether a constraint is met when instantiating a template" and "how much time is spent checking each individual constraint".
| static bool AreCompatibleForSubsumption(const FoldExpandedConstraint &A, | ||
| const FoldExpandedConstraint &B); | ||
|
|
||
| llvm::FoldingSetNodeID ProfileForSubsumption() const; |
There was a problem hiding this comment.
Do we want to retain the profiling information? Actually, should we be adding some time trace report support to this so users can track how much time is spent on subsumption in their headers?
Comment on lines
+154
to
+155
| std::optional<bool> Subsumes(NamedDecl *DP, ArrayRef<const Expr *> P, | ||
| NamedDecl *DQ, ArrayRef<const Expr *> Q); |
There was a problem hiding this comment.
Can those be const NamedDecl *?
There was a problem hiding this comment.
Not in this patch (getAssociatedConstraints is not const because nothing in normalization is const, and so it goes pretty deep, even if it should theoretically be possible)
AaronBallman
approved these changes
Mar 27, 2025
| FormulaType Res; | ||
|
|
||
| auto Add = [&, this](Clause C) { | ||
| // Sort each clause and remove duplicates for faster comparisons |
There was a problem hiding this comment.
Suggested change
| // Sort each clause and remove duplicates for faster comparisons | |
| // Sort each clause and remove duplicates for faster comparisons. |
There was a problem hiding this comment.
Fixed here #133633
cor3ntin
added a commit
that referenced
this pull request
Mar 30, 2025
SchrodingerZhu
pushed a commit
to SchrodingerZhu/llvm-project
that referenced
this pull request
Mar 31, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The main goal of this patch is to improve the
performance of concept subsumption by
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