Merge pull request #41631 from slavapestov/rqm-abstract-signatures-on-by-default

RequirementMachine: Enable -requirement-machine-abstract-signatures=verify by default

Author: slavapestov

lib/AST/RequirementMachine/InterfaceType.cpp

@@ -263,10 +263,13 @@ getTypeForSymbolRange(const Symbol *begin, const Symbol *end, Type root,
       unsigned index = GenericParamKey(genericParam).findIndexIn(genericParams);
 
       if (index == genericParams.size()) {
-        llvm::errs() << "Invalid generic parameter: " << genericParam << "\n";
-        llvm::errs() << "Valid generic parameters are";
+        llvm::errs() << "Cannot build interface type for term "
+                     << MutableTerm(begin, end) << "\n";
+        llvm::errs() << "Invalid generic parameter: "
+                     << Type(genericParam) << "\n";
+        llvm::errs() << "Valid generic parameters: ";
         for (auto *otherParam : genericParams)
-          llvm::errs() << " " << Type(otherParam);
+          llvm::errs() << " " << otherParam->getCanonicalType();
         llvm::errs() << "\n";
         abort();
       }

lib/AST/RequirementMachine/KnuthBendix.cpp

@@ -212,8 +212,56 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
       return false;
     }
 
-    // Add the pair (XV, TY).
-    pairs.emplace_back(xv, ty, path);
+    // If Y == UW for some W, then the critical pair is (XV, TUW),
+    // and we have
+    // - lhs == (TU -> X)
+    // - rhs == (UV -> UW).
+    //
+    // We explicitly apply the rewrite step (TU = X) to the rewrite path,
+    // transforming the critical pair to (XV, XW).
+    //
+    // In particular, if T == X, U == [P] for some protocol P, and
+    // V == W.[p] for some property symbol p, then we in fact have a pair
+    // of property rules:
+    //
+    // - lhs == (T.[P] => T)
+    // - rhs == ([P].W.[p] => [P].W)
+    //
+    // Without this hack, the critical pair would be:
+    //
+    // (T.w.[p] => T.[P].w)
+    //
+    // With this hack, the critical pair becomes:
+    //
+    // (T.w.[p] => T.w)
+    //
+    // This ensures that the newly-added rule is itself a property rule;
+    // otherwise, this would only be the case if addRule() reduced T.[P].w
+    // into T.w without immediately reducing some subterm of T first.
+    //
+    // While completion will eventually simplify all such rules down into
+    // property rules, their existance in the first place breaks subtle
+    // invariants in the minimal conformances algorithm, which expects
+    // homotopy generators describing redundant protocol conformance rules
+    // to have a certain structure.
+    if (lhs.getLHS().size() <= ty.size() &&
+        std::equal(lhs.getLHS().begin(),
+                   lhs.getLHS().end(),
+                   ty.begin())) {
+      unsigned endOffset = ty.size() - lhs.getLHS().size();
+      path.add(RewriteStep::forRewriteRule(/*startOffset=*/0,
+                                           endOffset,
+                                           getRuleID(lhs),
+                                           /*inverse=*/false));
+
+      // Compute the term XW.
+      MutableTerm xw(lhs.getRHS());
+      xw.append(ty.end() - endOffset, ty.end());
+
+      pairs.emplace_back(xv, xw, path);
+    } else {
+      pairs.emplace_back(xv, ty, path);
+    }
   }
 
   return true;
@@ -244,12 +292,14 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
   // adding new rules in the property map's concrete type unification procedure.
   Complete = 1;
 
-  bool again = false;
+  unsigned ruleCount;
 
   std::vector<CriticalPair> resolvedCriticalPairs;
   std::vector<RewriteLoop> resolvedLoops;
 
   do {
+    ruleCount = Rules.size();
+
     // For every rule, looking for other rules that overlap with this rule.
     for (unsigned i = 0, e = Rules.size(); i < e; ++i) {
       const auto &lhs = getRule(i);
@@ -335,9 +385,10 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
       }
     }
 
+    assert(ruleCount == Rules.size());
+
     simplifyLeftHandSides();
 
-    again = false;
     for (const auto &pair : resolvedCriticalPairs) {
       // Check if we've already done too much work.
       if (Rules.size() > maxRuleCount)
@@ -349,8 +400,6 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
       // Check if the new rule is too long.
       if (Rules.back().getDepth() > maxRuleLength)
         return std::make_pair(CompletionResult::MaxRuleLength, Rules.size() - 1);
-
-      again = true;
     }
 
     for (const auto &loop : resolvedLoops) {
@@ -362,7 +411,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxRuleCount,
 
     simplifyRightHandSides();
     simplifyLeftHandSideSubstitutions(/*map=*/nullptr);
-  } while (again);
+  } while (Rules.size() > ruleCount);
 
   return std::make_pair(CompletionResult::Success, 0);
 }

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -563,6 +563,10 @@ void RewriteSystem::simplifyRightHandSides() {
 
     unsigned newRuleID = Rules.size();
 
+    if (Debug.contains(DebugFlags::Add)) {
+      llvm::dbgs() << "## RHS simplification adds a rule " << lhs << " => " << rhs << "\n\n";
+    }
+
     // Add a new rule with the simplified right hand side.
     Rules.emplace_back(lhs, Term::get(rhs, Context));
     auto oldRuleID = Trie.insert(lhs.begin(), lhs.end(), newRuleID);
@@ -655,10 +659,7 @@ void RewriteSystem::verifyRewriteRules(ValidityPolicy policy) const {
         ASSERT_RULE(symbol.getKind() != Symbol::Kind::GenericParam);
       }
 
-      // Completion can produce rules like [P:T].[Q].[R] => [P:T].[Q]
-      // which are immediately simplified away.
-      if (!rule.isLHSSimplified() &&
-          index != 0 && index != lhs.size() - 1) {
+      if (index != 0 && index != lhs.size() - 1) {
         ASSERT_RULE(symbol.getKind() != Symbol::Kind::Protocol);
       }
     }
@@ -689,9 +690,10 @@ void RewriteSystem::verifyRewriteRules(ValidityPolicy policy) const {
         ASSERT_RULE(symbol.getKind() != Symbol::Kind::GenericParam);
       }
 
-      // Completion can produce rules like [P:T].[Q].[R] => [P:T].[Q]
+      // Completion can produce rules like [P:T].[Q:R] => [P:T].[Q]
       // which are immediately simplified away.
-      if (!rule.isRHSSimplified() && index != 0) {
+      if (!rule.isRHSSimplified() &&
+          index != 0) {
         ASSERT_RULE(symbol.getKind() != Symbol::Kind::Protocol);
       }
     }

lib/Frontend/CompilerInvocation.cpp

@@ -914,6 +914,7 @@ static bool ParseLangArgs(LangOptions &Opts, ArgList &Args,
       Args.hasArg(OPT_disable_subst_sil_function_types);
 
   Opts.RequirementMachineProtocolSignatures = RequirementMachineMode::Verify;
+  Opts.RequirementMachineAbstractSignatures = RequirementMachineMode::Verify;
 
   if (auto A = Args.getLastArg(OPT_requirement_machine_protocol_signatures_EQ)) {
     auto value = llvm::StringSwitch<Optional<RequirementMachineMode>>(A->getValue())

stdlib/cmake/modules/SwiftSource.cmake

@@ -465,12 +465,6 @@ function(_compile_swift_files
     endif()
   endif()
 
-  # The standard library and overlays are built with the Requirement Machine enabled.
-  if(SWIFTFILE_IS_STDLIB)
-    list(APPEND swift_flags "-Xfrontend" "-requirement-machine-protocol-signatures=verify")
-    list(APPEND swift_flags "-Xfrontend" "-requirement-machine-abstract-signatures=verify")
-  endif()
-
   # The standard library and overlays are built resiliently when SWIFT_STDLIB_STABLE_ABI=On.
   if(SWIFTFILE_IS_STDLIB AND SWIFT_STDLIB_STABLE_ABI)
     list(APPEND swift_flags "-enable-library-evolution")

test/Generics/simplify_rhs_elimination_order.swift

@@ -0,0 +1,37 @@
+// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-protocol-signatures=on -requirement-machine-inferred-signatures=on 2>&1 | %FileCheck %s
+
+public protocol P1 {
+  associatedtype T
+}
+
+public protocol P2 : P1 {}
+
+public protocol P3 : P2 {}
+
+public protocol Q1 {}
+
+public protocol Q2 : Q1 {}
+
+public protocol Q3 : Q1 {}
+
+public protocol R {
+  associatedtype U: Q2, Q3
+}
+
+struct G<X: P3, Y: R> where X.T == Y.U {
+  // CHECK-LABEL: .G.Nested0@
+  // CHECK-NEXT: <X, Y, Z where X : P3, Y : R, X.[P1]T == Y.[R]U>
+  struct Nested0<Z> {}
+
+  // CHECK-LABEL: .G.Nested1@
+  // CHECK-NEXT: <X, Y, Z where X : P3, Y : R, X.[P1]T == Y.[R]U>
+  struct Nested1<Z> where X.T : Q1 {}
+
+  // CHECK-LABEL: .G.Nested2@
+  // CHECK-NEXT: <X, Y, Z where X : P3, Y : R, X.[P1]T == Y.[R]U>
+  struct Nested2<Z> where X.T : Q2 {}
+
+  // CHECK-LABEL: .G.Nested3@
+  // CHECK-NEXT: <X, Y, Z where X : P3, Y : R, X.[P1]T == Y.[R]U>
+  struct Nested3<Z> where X.T : Q3 {}
+}