RequirementMachine: Add two more completion termination checks for concrete type requirements

The concrete nesting limit, which defaults to 30, catches
things like A == G<A>. However, with something like
A == (A, A), you end up with an exponential problem size
before you hit the limit.

Add two new limits.

The first is the total size of the concrete type, counting
all leaves, which defaults to 4000. It can be set with the
-requirement-machine-max-concrete-size= frontend flag.

The second avoids an assertion in addTypeDifference() which
can be hit if a certain counter overflows before any other
limit is breached. This also defaults to 4000 and can be set
with the -requirement-machine-max-type-differences= frontend flag.

include/swift/AST/DiagnosticsSema.def

@@ -3441,7 +3441,7 @@ WARNING(associated_type_override_typealias,none,
 
 ERROR(requirement_machine_completion_failed,none,
       "cannot build rewrite system for %select{generic signature|protocol}0; "
-      "%select{%error|rule count|rule length|concrete nesting}1 limit exceeded",
+      "%select{%error|rule count|rule length|concrete type nesting|concrete type size|concrete type difference}1 limit exceeded",
       (unsigned, unsigned))
 NOTE(requirement_machine_completion_rule,none,
      "failed rewrite rule is %0", (StringRef))

include/swift/Basic/LangOptions.h

@@ -580,10 +580,18 @@ namespace swift {
     /// algorithm.
     unsigned RequirementMachineMaxRuleLength = 12;
 
-    /// Maximum concrete type nesting depth for requirement machine property map
-    /// algorithm.
+    /// Maximum concrete type nesting depth (when type is viewed as a tree) for
+    /// requirement machine property map algorithm.
     unsigned RequirementMachineMaxConcreteNesting = 30;
 
+    /// Maximum concrete type size (total number of nodes in the type tree) for
+    /// requirement machine property map algorithm.
+    unsigned RequirementMachineMaxConcreteSize = 4000;
+
+    /// Maximum number of "type difference" structures for the requirement machine
+    /// property map algorithm.
+    unsigned RequirementMachineMaxTypeDifferences = 4000;
+
     /// Maximum number of attempts to make when splitting concrete equivalence
     /// classes.
     unsigned RequirementMachineMaxSplitConcreteEquivClassAttempts = 2;

include/swift/Option/FrontendOptions.td

@@ -451,6 +451,14 @@ def requirement_machine_max_concrete_nesting : Joined<["-"], "requirement-machin
   Flags<[FrontendOption, HelpHidden, DoesNotAffectIncrementalBuild]>,
   HelpText<"Set the maximum concrete type nesting depth before giving up">;
 
+def requirement_machine_max_concrete_size : Joined<["-"], "requirement-machine-max-concrete-size=">,
+  Flags<[FrontendOption, HelpHidden, DoesNotAffectIncrementalBuild]>,
+  HelpText<"Set the maximum concrete type total size before giving up">;
+
+def requirement_machine_max_type_differences : Joined<["-"], "requirement-machine-max-type-differences=">,
+  Flags<[FrontendOption, HelpHidden, DoesNotAffectIncrementalBuild]>,
+  HelpText<"Set the maximum number of type difference structures allocated before giving up">;
+
 def requirement_machine_max_split_concrete_equiv_class_attempts : Joined<["-"], "requirement-machine-max-split-concrete-equiv-class-attempts=">,
   Flags<[FrontendOption, HelpHidden, DoesNotAffectIncrementalBuild]>,
   HelpText<"Set the maximum concrete number of attempts at splitting "

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -291,8 +291,8 @@ RewriteSystem::findRuleToDelete(EliminationPredicate isRedundantRuleFn) {
     {
       // If both are concrete type requirements, prefer to eliminate the
       // one with the more deeply nested type.
-      unsigned ruleNesting = rule.getNesting();
-      unsigned otherRuleNesting = otherRule.getNesting();
+      unsigned ruleNesting = rule.getNestingAndSize().first;
+      unsigned otherRuleNesting = otherRule.getNestingAndSize().first;
 
       if (ruleNesting != otherRuleNesting) {
         if (ruleNesting > otherRuleNesting)

lib/AST/RequirementMachine/RequirementMachine.cpp

@@ -212,6 +212,8 @@ RequirementMachine::RequirementMachine(RewriteContext &ctx)
   MaxRuleCount = langOpts.RequirementMachineMaxRuleCount;
   MaxRuleLength = langOpts.RequirementMachineMaxRuleLength;
   MaxConcreteNesting = langOpts.RequirementMachineMaxConcreteNesting;
+  MaxConcreteSize = langOpts.RequirementMachineMaxConcreteSize;
+  MaxTypeDifferences = langOpts.RequirementMachineMaxTypeDifferences;
   Stats = ctx.getASTContext().Stats;
 
   if (Stats)
@@ -247,6 +249,18 @@ void RequirementMachine::checkCompletionResult(CompletionResult result) const {
       out << "Rewrite system exceeded concrete type nesting depth limit\n";
       dump(out);
     });
+
+  case CompletionResult::MaxConcreteSize:
+    ABORT([&](auto &out) {
+      out << "Rewrite system exceeded concrete type size limit\n";
+      dump(out);
+    });
+
+  case CompletionResult::MaxTypeDifferences:
+    ABORT([&](auto &out) {
+      out << "Rewrite system exceeded concrete type difference limit\n";
+      dump(out);
+    });
   }
 }
 
@@ -496,16 +510,26 @@ RequirementMachine::computeCompletion(RewriteSystem::ValidityPolicy policy) {
           return std::make_pair(CompletionResult::MaxRuleLength,
                                 ruleCount + i);
         }
-        if (newRule.getNesting() > MaxConcreteNesting + System.getDeepestInitialRule()) {
+        auto nestingAndSize = newRule.getNestingAndSize();
+        if (nestingAndSize.first > MaxConcreteNesting + System.getMaxNestingOfInitialRule()) {
           return std::make_pair(CompletionResult::MaxConcreteNesting,
                                 ruleCount + i);
         }
+        if (nestingAndSize.second > MaxConcreteSize + System.getMaxSizeOfInitialRule()) {
+          return std::make_pair(CompletionResult::MaxConcreteSize,
+                                ruleCount + i);
+        }
       }
 
       if (System.getLocalRules().size() > MaxRuleCount) {
         return std::make_pair(CompletionResult::MaxRuleCount,
                               System.getRules().size() - 1);
       }
+
+      if (System.getTypeDifferenceCount() > MaxTypeDifferences) {
+        return std::make_pair(CompletionResult::MaxTypeDifferences,
+                              System.getRules().size() - 1);
+      }
     }
   }
 

lib/AST/RequirementMachine/RequirementMachine.h

@@ -68,6 +68,8 @@ class RequirementMachine final {
   unsigned MaxRuleCount;
   unsigned MaxRuleLength;
   unsigned MaxConcreteNesting;
+  unsigned MaxConcreteSize;
+  unsigned MaxTypeDifferences;
 
   UnifiedStatsReporter *Stats;
 

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -34,7 +34,8 @@ RewriteSystem::RewriteSystem(RewriteContext &ctx)
   Frozen = 0;
   RecordLoops = 0;
   LongestInitialRule = 0;
-  DeepestInitialRule = 0;
+  MaxNestingOfInitialRule = 0;
+  MaxSizeOfInitialRule = 0;
 }
 
 RewriteSystem::~RewriteSystem() {
@@ -90,7 +91,12 @@ void RewriteSystem::initialize(
 
   for (const auto &rule : getLocalRules()) {
     LongestInitialRule = std::max(LongestInitialRule, rule.getDepth());
-    DeepestInitialRule = std::max(DeepestInitialRule, rule.getNesting());
+
+    auto nestingAndSize = rule.getNestingAndSize();
+    MaxNestingOfInitialRule = std::max(MaxNestingOfInitialRule,
+                                      nestingAndSize.first);
+    MaxSizeOfInitialRule = std::max(MaxSizeOfInitialRule,
+                                    nestingAndSize.second);
   }
 }
 

lib/AST/RequirementMachine/RewriteSystem.h

@@ -50,7 +50,13 @@ enum class CompletionResult {
   MaxRuleLength,
 
   /// Maximum concrete type nesting depth exceeded.
-  MaxConcreteNesting
+  MaxConcreteNesting,
+
+  /// Maximum concrete type size exceeded.
+  MaxConcreteSize,
+
+  /// Maximum type difference count exceeded.
+  MaxTypeDifferences,
 };
 
 /// A term rewrite system for working with types in a generic signature.
@@ -107,13 +113,16 @@ class RewriteSystem final {
   /// identities among rewrite rules discovered while resolving critical pairs.
   unsigned RecordLoops : 1;
 
-  /// The length of the longest initial rule, used for the MaxRuleLength
-  /// completion non-termination heuristic.
+  /// The length of the longest initial rule, for the MaxRuleLength limit.
   unsigned LongestInitialRule : 16;
 
-  /// The most deeply nested concrete type appearing in an initial rule, used
-  /// for the MaxConcreteNesting completion non-termination heuristic.
-  unsigned DeepestInitialRule : 16;
+  /// The most deeply nested concrete type appearing in an initial rule,
+  /// for the MaxConcreteNesting limit.
+  unsigned MaxNestingOfInitialRule : 16;
+
+  /// The largest concrete type by total tree node count that appears in an
+  /// initial rule, for the MaxConcreteSize limit.
+  unsigned MaxSizeOfInitialRule : 16;
 
 public:
   explicit RewriteSystem(RewriteContext &ctx);
@@ -143,8 +152,12 @@ public:
     return LongestInitialRule;
   }
 
-  unsigned getDeepestInitialRule() const {
-    return DeepestInitialRule;
+  unsigned getMaxNestingOfInitialRule() const {
+    return MaxNestingOfInitialRule;
+  }
+
+  unsigned getMaxSizeOfInitialRule() const {
+    return MaxSizeOfInitialRule;
   }
 
   ArrayRef<const ProtocolDecl *> getProtocols() const {
@@ -311,6 +324,10 @@ public:
                              std::optional<unsigned> &lhsDifferenceID,
                              std::optional<unsigned> &rhsDifferenceID);
 
+  unsigned getTypeDifferenceCount() const {
+    return Differences.size();
+  }
+
   const TypeDifference &getTypeDifference(unsigned index) const;
 
   void processTypeDifference(const TypeDifference &difference,

lib/AST/RequirementMachine/Rule.cpp

@@ -221,7 +221,12 @@ bool Rule::isDerivedFromConcreteProtocolTypeAliasRule() const {
   return true;
 }
 
-/// Returns the length of the left hand side.
+/// Returns the maximum among the length of the left-hand side,
+/// and the length of any substitution terms that appear in a
+/// property symbol at the end of the left-hand side.
+///
+/// This is a measure of the complexity of the rule, which stops
+/// completion from running forever.
 unsigned Rule::getDepth() const {
   auto result = LHS.size();
 
@@ -234,26 +239,30 @@ unsigned Rule::getDepth() const {
   return result;
 }
 
-/// Returns the nesting depth of the concrete symbol at the end of the
-/// left hand side, or 0 if there isn't one.
-unsigned Rule::getNesting() const {
+/// Returns the complexity of the concrete type in the property symbol
+/// at the end of the left-hand side, if there is one.
+///
+/// This is a measure of the complexity of the rule, which stops
+/// completion from running forever.
+std::pair<unsigned, unsigned>
+Rule::getNestingAndSize() const {
   if (LHS.back().hasSubstitutions()) {
     auto type = LHS.back().getConcreteType();
 
     struct Walker : TypeWalker {
       unsigned Nesting = 0;
       unsigned MaxNesting = 0;
+      unsigned Size = 0;
 
       Action walkToTypePre(Type ty) override {
+        ++Size;
         ++Nesting;
-        MaxNesting = std::max(Nesting, MaxNesting);
-
+        MaxNesting = std::max(MaxNesting, Nesting);
         return Action::Continue;
       }
 
       Action walkToTypePost(Type ty) override {
         --Nesting;
-
         return Action::Continue;
       }
     };
@@ -261,10 +270,10 @@ unsigned Rule::getNesting() const {
     Walker walker;
     type.walk(walker);
 
-    return walker.MaxNesting;
+    return std::make_pair(walker.MaxNesting, walker.Size);
   }
 
-  return 0;
+  return std::make_pair(0, 0);
 }
 
 /// Linear order on rules; compares LHS followed by RHS.

lib/AST/RequirementMachine/Rule.h

@@ -224,7 +224,7 @@ public:
 
   unsigned getDepth() const;
 
-  unsigned getNesting() const;
+  std::pair<unsigned, unsigned> getNestingAndSize() const;
 
   std::optional<int> compare(const Rule &other, RewriteContext &ctx) const;
 

lib/Frontend/CompilerInvocation.cpp

@@ -1769,6 +1769,28 @@ static bool ParseLangArgs(LangOptions &Opts, ArgList &Args,
     }
   }
 
+  if (const Arg *A = Args.getLastArg(OPT_requirement_machine_max_concrete_size)) {
+    unsigned limit;
+    if (StringRef(A->getValue()).getAsInteger(10, limit)) {
+      Diags.diagnose(SourceLoc(), diag::error_invalid_arg_value,
+                     A->getAsString(Args), A->getValue());
+      HadError = true;
+    } else {
+      Opts.RequirementMachineMaxConcreteSize = limit;
+    }
+  }
+
+  if (const Arg *A = Args.getLastArg(OPT_requirement_machine_max_type_differences)) {
+    unsigned limit;
+    if (StringRef(A->getValue()).getAsInteger(10, limit)) {
+      Diags.diagnose(SourceLoc(), diag::error_invalid_arg_value,
+                     A->getAsString(Args), A->getValue());
+      HadError = true;
+    } else {
+      Opts.RequirementMachineMaxTypeDifferences = limit;
+    }
+  }
+
   if (const Arg *A = Args.getLastArg(OPT_requirement_machine_max_split_concrete_equiv_class_attempts)) {
     unsigned limit;
     if (StringRef(A->getValue()).getAsInteger(10, limit)) {

test/Constraints/same_types.swift

@@ -284,7 +284,7 @@ protocol P2 {
 // CHECK-LABEL: same_types.(file).structuralSameTypeRecursive1@
 // CHECK-NEXT: Generic signature: <T, U>
 
-// expected-error@+2 {{cannot build rewrite system for generic signature; concrete nesting limit exceeded}}
+// expected-error@+2 {{cannot build rewrite system for generic signature; concrete type nesting limit exceeded}}
 // expected-note@+1 {{τ_0_0.[P2:Assoc1].[concrete: ((((((((((((((((((((((((((((((((τ_0_0.[P2:Assoc1], τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1), τ_0_1)] => τ_0_0.[P2:Assoc1]}}
 func structuralSameTypeRecursive1<T: P2, U>(_: T, _: U)
   where T.Assoc1 == Tuple2<T.Assoc1, U>

test/Generics/infinite_concrete_type.swift

@@ -2,8 +2,8 @@
 
 class G<T> {}
 
-protocol P1 { // expected-error {{cannot build rewrite system for protocol; concrete nesting limit exceeded}}
-// expected-note@-1 {{failed rewrite rule is [P1:A].[concrete: G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<[P1].A>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>] => [P1:A]}}
+protocol P1 { // expected-error {{cannot build rewrite system for protocol; concrete type difference limit exceeded}}
+// expected-note@-1 {{failed rewrite rule is [P1:B].[superclass: G<G<G<G<G<G<G<G<G<G<G<G<G<[P1].A>>>>>>>>>>>>>] => [P1:B]}}
   associatedtype A where A == G<B>
   associatedtype B where B == G<A>
 }

test/Generics/non_confluent.swift

@@ -52,3 +52,64 @@ protocol P3 : P3Base where T == S<U> {
 // expected-error@-1 {{cannot build rewrite system for protocol; rule length limit exceeded}}
 // expected-note@-2 {{failed rewrite rule is [P3:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[concrete: S<S<S<S<S<S<S<S<S<S<S<S<S<S<[P3:U]>>>>>>>>>>>>>>] => [P3:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T]}}
 }
+
+protocol Exponential {
+// expected-error@-1 {{cannot build rewrite system for protocol; concrete type size limit exceeded}}
+// expected-note@-2 {{failed rewrite rule is }}
+  associatedtype A where A == (A, A)
+}
+
+class Base<T> {}
+
+class Derived<T, U> : Base<(T, U)> {}
+
+protocol TooManyDifferences {
+// expected-error@-1 {{cannot build rewrite system for protocol; concrete type difference limit exceeded}}
+// expected-note@-2 {{failed rewrite rule is }}
+  associatedtype A1 where A1: Derived<B, C>, A2: Base<B>, A1 == A2
+  associatedtype A2
+  associatedtype B
+  associatedtype C
+}
+
+protocol M0 {
+// expected-error@-1 {{cannot build rewrite system for protocol; rule length limit exceeded}}
+// expected-note@-2 {{failed rewrite rule is }}
+  associatedtype A: M0
+  associatedtype B: M0
+  associatedtype C: M0
+    where A.B == Self, C.A == B.C  // expected-error *{{is not a member type}}
+}
+
+protocol M1 {
+// expected-error@-1 {{cannot build rewrite system for protocol; rule length limit exceeded}}
+// expected-note@-2 {{failed rewrite rule is }}
+  associatedtype A: M1
+  associatedtype B: M1
+  associatedtype C: M1
+    where C.A.C == A, A.B.A == A  // expected-error *{{is not a member type}}
+}
+
+protocol M2 {
+// expected-error@-1 {{cannot build rewrite system for protocol; rule length limit exceeded}}
+// expected-note@-2 {{failed rewrite rule is }}
+  associatedtype A: M2
+  associatedtype B: M2
+  associatedtype C: M2
+    where B.A == A.B, C.A == A, A.C == A  // expected-error *{{is not a member type}}
+}
+
+// FIXME: This should be rejected
+protocol M3 {
+  associatedtype A: M3
+  associatedtype B: M3
+    where A.A.A == A, A.B.B.A == B.B
+}
+
+protocol M4 {
+// expected-error@-1 {{cannot build rewrite system for protocol; rule length limit exceeded}}
+// expected-note@-2 {{failed rewrite rule is }}
+  associatedtype A: M4
+  associatedtype B: M4
+    where B.A.A == A.A.B, A.B.A == A.A  // expected-error *{{is not a member type}}
+}

test/Generics/rdar90402519.swift

@@ -23,5 +23,5 @@ protocol P1 : P0 where C == G1<I> {
 }
 
 protocol P2 : P1 where C == G2<I> {}
-// expected-error@-1 {{cannot build rewrite system for protocol; concrete nesting limit exceeded}}
-// expected-note@-2 {{failed rewrite rule is [P2:I].[concrete: G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<[P2:I]>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>] => [P2:I]}}
+// expected-error@-1 {{cannot build rewrite system for protocol; concrete type difference limit exceeded}}
+// expected-note@-2 {{failed rewrite rule is [P2:I].[concrete: G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<G<[P2:I]>>>>>>>>>>>>>>>>>>>>>>>>>> : Escapable] => [P2:I]}}

test/attr/attr_specialize.swift

@@ -53,7 +53,7 @@ class G<T> {
   @_specialize(where T == T) // expected-error{{too few generic parameters are specified in '_specialize' attribute (got 0, but expected 1)}}
   // expected-note@-1 {{missing constraint for 'T' in '_specialize' attribute}}
   @_specialize(where T == S<T>)
-  // expected-error@-1 {{cannot build rewrite system for generic signature; concrete nesting limit exceeded}}
+  // expected-error@-1 {{cannot build rewrite system for generic signature; concrete type nesting limit exceeded}}
   // expected-note@-2 {{failed rewrite rule is τ_0_0.[concrete: S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<τ_0_0>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>] => τ_0_0}}
   // expected-error@-3 {{too few generic parameters are specified in '_specialize' attribute (got 0, but expected 1)}}
   // expected-note@-4 {{missing constraint for 'T' in '_specialize' attribute}}

test/decl/protocol/req/recursion.swift

@@ -5,13 +5,13 @@ protocol SomeProtocol {
 }
 
 extension SomeProtocol where T == Optional<T> { }
-// expected-error@-1 {{cannot build rewrite system for generic signature; concrete nesting limit exceeded}}
+// expected-error@-1 {{cannot build rewrite system for generic signature; concrete type nesting limit exceeded}}
 // expected-note@-2 {{failed rewrite rule is τ_0_0.[SomeProtocol:T].[concrete: Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<Optional<τ_0_0.[SomeProtocol:T]>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>] => τ_0_0.[SomeProtocol:T]}}
 
 // rdar://problem/19840527
 
 class X<T> where T == X {
-// expected-error@-1 {{cannot build rewrite system for generic signature; concrete nesting limit exceeded}}
+// expected-error@-1 {{cannot build rewrite system for generic signature; concrete type nesting limit exceeded}}
 // expected-note@-2 {{failed rewrite rule is τ_0_0.[concrete: X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<X<τ_0_0>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>] => τ_0_0}}
 // expected-error@-3 {{generic class 'X' has self-referential generic requirements}}
     var type: T { return Swift.type(of: self) } // expected-error{{cannot convert return expression of type 'X<T>.Type' to return type 'T'}}