================
@@ -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 <ransform : 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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
