Merge pull request #42017 from slavapestov/rqm-rule-length-heuristic

RequirementMachine: Tweak rule limit non-termination heuristic

Author: slavapestov

lib/AST/RequirementMachine/KnuthBendix.cpp

@@ -398,7 +398,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
         continue;
 
       // Check if the new rule is too long.
-      if (Rules.back().getDepth() > maxRuleLength)
+      if (Rules.back().getDepth() > maxRuleLength + getLongestInitialRule())
         return std::make_pair(CompletionResult::MaxRuleLength, Rules.size() - 1);
     }
 

lib/AST/RequirementMachine/RequirementMachine.cpp

@@ -301,7 +301,7 @@ RequirementMachine::computeCompletion(RewriteSystem::ValidityPolicy policy) {
       // Check new rules added by the property map against configured limits.
       for (unsigned i = 0; i < rulesAdded; ++i) {
         const auto &newRule = System.getRule(ruleCount + i);
-        if (newRule.getDepth() > MaxRuleLength) {
+        if (newRule.getDepth() > MaxRuleLength + System.getLongestInitialRule()) {
           return std::make_pair(CompletionResult::MaxRuleLength,
                                 ruleCount + i);
         }

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -30,6 +30,7 @@ RewriteSystem::RewriteSystem(RewriteContext &ctx)
   Complete = 0;
   Minimized = 0;
   RecordLoops = 0;
+  LongestInitialRule = 0;
 }
 
 RewriteSystem::~RewriteSystem() {
@@ -85,6 +86,10 @@ void RewriteSystem::initialize(
   addRules(std::move(importedRules),
            std::move(permanentRules),
            std::move(requirementRules));
+
+  for (const auto &rule : getLocalRules()) {
+    LongestInitialRule = std::max(LongestInitialRule, rule.getDepth());
+  }
 }
 
 /// Reduce a term by applying all rewrite rules until fixed point.

lib/AST/RequirementMachine/RewriteSystem.h

@@ -106,6 +106,10 @@ 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.
+  unsigned LongestInitialRule : 16;
+
 public:
   explicit RewriteSystem(RewriteContext &ctx);
   ~RewriteSystem();
@@ -131,6 +135,10 @@ class RewriteSystem final {
                   std::vector<std::pair<MutableTerm, MutableTerm>> &&permanentRules,
                   std::vector<std::tuple<MutableTerm, MutableTerm, Optional<unsigned>>> &&requirementRules);
 
+  unsigned getLongestInitialRule() const {
+    return LongestInitialRule;
+  }
+
   ArrayRef<const ProtocolDecl *> getProtocols() const {
     return Protos;
   }

test/Generics/non_confluent.swift

@@ -1,14 +1,14 @@
 // RUN: %target-typecheck-verify-swift -requirement-machine-protocol-signatures=on -requirement-machine-inferred-signatures=on
 
 protocol ABA // expected-error {{cannot build rewrite system for protocol; rule length limit exceeded}}
-// expected-note@-1 {{failed rewrite rule is [ABA:A].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:A] => [ABA:A].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B]}}
+// expected-note@-1 {{failed rewrite rule is [ABA:A].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:A] => [ABA:A].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B].[ABA:B]}}
     where A.B == A.B.A { // expected-error *{{is not a member type}}
   associatedtype A : ABA
   associatedtype B : ABA
 }
 
 protocol Undecidable // expected-error {{cannot build rewrite system for protocol; rule length limit exceeded}}
-// expected-note@-1 {{failed rewrite rule is [Undecidable:A].[Undecidable:B].[Undecidable:D].[Undecidable:C].[Undecidable:C].[Undecidable:C].[Undecidable:E].[Undecidable:B].[Undecidable:A].[Undecidable:A].[Undecidable:E].[Undecidable:C].[Undecidable:E] => [Undecidable:A].[Undecidable:B].[Undecidable:D].[Undecidable:C].[Undecidable:C].[Undecidable:C].[Undecidable:E].[Undecidable:B].[Undecidable:A].[Undecidable:A].[Undecidable:E].[Undecidable:C]}}
+// expected-note@-1 {{failed rewrite rule is [Undecidable:A].[Undecidable:C].[Undecidable:C].[Undecidable:C].[Undecidable:D].[Undecidable:C].[Undecidable:E].[Undecidable:E].[Undecidable:B].[Undecidable:B].[Undecidable:A].[Undecidable:B].[Undecidable:C].[Undecidable:C].[Undecidable:C].[Undecidable:D].[Undecidable:D] => [Undecidable:A].[Undecidable:C].[Undecidable:C].[Undecidable:C].[Undecidable:D].[Undecidable:C].[Undecidable:C].[Undecidable:C].[Undecidable:C].[Undecidable:D].[Undecidable:D].[Undecidable:E].[Undecidable:A].[Undecidable:B]}}
     where A.C == C.A, // expected-error *{{is not a member type}}
           A.D == D.A, // expected-error *{{is not a member type}}
           B.C == C.B, // expected-error *{{is not a member type}}
@@ -33,19 +33,19 @@ protocol P2 {
 
 func foo<T : P1 & P2>(_: T) {}
 // expected-error@-1 {{cannot build rewrite system for generic signature; rule length limit exceeded}}
-// expected-note@-2 {{failed rewrite rule is τ_0_0.[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P2] => τ_0_0.[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T]}}
+// expected-note@-2 {{failed rewrite rule is τ_0_0.[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].[P2] => τ_0_0.[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]}}
 
 extension P1 where Self : P2 {}
 // expected-error@-1 {{cannot build rewrite system for generic signature; rule length limit exceeded}}
-// expected-note@-2 {{failed rewrite rule is τ_0_0.[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P2] => τ_0_0.[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T].[P1:T]}}
+// expected-note@-2 {{failed rewrite rule is τ_0_0.[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].[P2] => τ_0_0.[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]}}
 
 struct S<U : P1> : P1 {
   typealias T = S<S<U>>
 }
 
 protocol P3 {
 // 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].[concrete: 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]}}
+// 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]}}
 
   associatedtype T : P1 where T == S<U>
 // expected-error@-1 {{type 'Self.U' does not conform to protocol 'P1'}}

test/Generics/opaque_archetype_concrete_requirement_recursive_rejected.swift

@@ -31,5 +31,5 @@ protocol HasRecursiveP {
 
 extension HasRecursiveP where T == DefinesRecursiveP.T {}
 // expected-error@-1 {{cannot build rewrite system for generic signature; rule length limit exceeded}}
-// expected-note@-2 {{failed rewrite rule is τ_0_0.[HasRecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[concrete: (((((((((@_opaqueReturnTypeOf("$s56opaque_archetype_concrete_requirement_recursive_rejected17DefinesRecursivePV1tQrvp", 0) __.T).T).T).T).T).T).T).T).T).T] => τ_0_0.[HasRecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T]}}
+// expected-note@-2 {{failed rewrite rule is τ_0_0.[HasRecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[concrete: ((((((((((((@_opaqueReturnTypeOf("$s56opaque_archetype_concrete_requirement_recursive_rejected17DefinesRecursivePV1tQrvp", 0) __.T).T).T).T).T).T).T).T).T).T).T).T).T] => τ_0_0.[HasRecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T].[RecursiveP:T]}}
 

test/Generics/sr16024.swift

@@ -0,0 +1,7 @@
+// RUN: %target-swift-frontend -typecheck %s -requirement-machine-protocol-signatures=on
+
+// The rule length limit (12 by default) is relative to the longest initial rule.
+
+protocol P {
+  associatedtype T : P where T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T.T == Self
+}

validation-test/compiler_crashers_2_fixed/sr9584.swift

@@ -10,7 +10,7 @@ protocol P {
 extension S: P where N: P {
   static func f<X: P>(_ x: X) -> S<X.A> where A == X, X.A == N {
   // expected-error@-1 {{cannot build rewrite system for generic signature; rule length limit exceeded}}
-  // expected-note@-2 {{failed rewrite rule is τ_0_0.[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[concrete: S<S<S<S<S<S<S<S<S<S<S<S<τ_0_0>>>>>>>>>>>>] => τ_0_0.[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A] [subst↓]}}
+  // expected-note@-2 {{failed rewrite rule is τ_0_0.[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[concrete: S<S<S<S<S<S<S<S<S<S<S<S<S<S<τ_0_0>>>>>>>>>>>>>>] => τ_0_0.[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A].[P:A] [subst↓]}}
   // expected-error@-3 {{'A' is not a member type of type 'X'}}
   // expected-error@-4 {{'A' is not a member type of type 'X'}}
     return S<X.A>()