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.

Author: slavapestov

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 @@ class RewriteSystem final {
     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 @@ class RewriteSystem final {
                              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,37 +239,41 @@ 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;
       }
     };
 
     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 @@ class Rule final {
 
   unsigned getDepth() const;
 
-  unsigned getNesting() const;
+  std::pair<unsigned, unsigned> getNestingAndSize() const;
 
   std::optional<int> compare(const Rule &other, RewriteContext &ctx) const;