Merge pull request #41043 from slavapestov/rqm-concrete-conformance-minimization-fixes

RequirementMachine: Fix some bugs with concrete conformance minimization

Author: slavapestov

include/swift/Basic/LangOptions.h

@@ -509,7 +509,7 @@ namespace swift {
 
     /// Maximum term length for requirement machine Knuth-Bendix completion
     /// algorithm.
-    unsigned RequirementMachineDepthLimit = 10;
+    unsigned RequirementMachineDepthLimit = 12;
 
     /// Enable the new experimental protocol requirement signature minimization
     /// algorithm.

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -481,18 +481,20 @@ void RewriteSystem::minimizeRewriteSystem() {
   propagateExplicitBits();
 
   // First pass:
-  // - Eliminate all simplified non-conformance rules.
+  // - Eliminate all LHS-simplified non-conformance rules.
+  // - Eliminate all RHS-simplified and substitution-simplified rules.
   // - Eliminate all rules with unresolved symbols.
   performHomotopyReduction([&](unsigned ruleID) -> bool {
     const auto &rule = getRule(ruleID);
 
-    if (rule.isSimplified() &&
+    if (rule.isLHSSimplified() &&
         !rule.isAnyConformanceRule())
       return true;
 
-    // Other rules involving unresolved name symbols are derived from an
-    // associated type introduction rule together with a conformance rule.
-    // They are eliminated in the first pass.
+    if (rule.isRHSSimplified() ||
+        rule.isSubstitutionSimplified())
+      return true;
+
     if (rule.getLHS().containsUnresolvedSymbols())
       return true;
 
@@ -692,20 +694,31 @@ void RewriteSystem::verifyMinimizedRules(
       continue;
     }
 
-    // Simplified rules should be redundant, unless they're protocol conformance
-    // rules, which unfortunately might no be redundant, because we try to keep
-    // them in the original protocol definition for compatibility with the
-    // GenericSignatureBuilder's minimization algorithm.
-    if (rule.isSimplified() &&
+    // LHS-simplified rules should be redundant, unless they're protocol
+    // conformance rules, which unfortunately might no be redundant, because
+    // we try to keep them in the original protocol definition for
+    // compatibility with the GenericSignatureBuilder's minimization algorithm.
+    if (rule.isLHSSimplified() &&
         !rule.isRedundant() &&
         !rule.isProtocolConformanceRule()) {
       llvm::errs() << "Simplified rule is not redundant: " << rule << "\n\n";
       dump(llvm::errs());
       abort();
     }
 
+    // RHS-simplified and substitution-simplified rules should be redundant.
+    if ((rule.isRHSSimplified() ||
+         rule.isSubstitutionSimplified()) &&
+        !rule.isRedundant()) {
+      llvm::errs() << "Simplified rule is not redundant: " << rule << "\n\n";
+      dump(llvm::errs());
+      abort();
+    }
+
     if (rule.isRedundant() &&
         rule.isAnyConformanceRule() &&
+        !rule.isRHSSimplified() &&
+        !rule.isSubstitutionSimplified() &&
         !rule.containsUnresolvedSymbols() &&
         !redundantConformances.count(ruleID)) {
       llvm::errs() << "Minimal conformance is redundant: " << rule << "\n\n";

lib/AST/RequirementMachine/KnuthBendix.cpp

@@ -337,8 +337,11 @@ void RewriteSystem::checkMergedAssociatedType(Term lhs, Term rhs) {
 /// where \p rhs begins at \p from, which must be an iterator pointing
 /// into \p lhs.
 ///
-/// The resulting pair is pushed onto \p result only if it is non-trivial,
-/// that is, the left hand side and right hand side are not equal.
+/// The resulting pair, together with a rewrite path relating them is
+/// pushed onto \p pairs only if it is non-trivial, that is, the left
+/// hand side and right hand side are not equal.
+///
+/// Otherwise, we record a rewrite loop in \p loops.
 ///
 /// Returns true if the pair was non-trivial, false if it was trivial.
 ///
@@ -372,9 +375,7 @@ void RewriteSystem::checkMergedAssociatedType(Term lhs, Term rhs) {
 bool
 RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
                                    const Rule &lhs, const Rule &rhs,
-                                   std::vector<std::pair<MutableTerm,
-                                                         MutableTerm>> &pairs,
-                                   std::vector<RewritePath> &paths,
+                                   std::vector<CriticalPair> &pairs,
                                    std::vector<RewriteLoop> &loops) const {
   auto end = lhs.getLHS().end();
   if (from + rhs.getLHS().size() < end) {
@@ -420,8 +421,7 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
     }
 
     // Add the pair (X, TYV).
-    pairs.emplace_back(x, tyv);
-    paths.push_back(path);
+    pairs.emplace_back(x, tyv, path);
   } else {
     // lhs == TU -> X, rhs == UV -> Y.
 
@@ -476,8 +476,7 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
     }
 
     // Add the pair (XV, TY).
-    pairs.emplace_back(xv, ty);
-    paths.push_back(path);
+    pairs.emplace_back(xv, ty, path);
   }
 
   return true;
@@ -508,15 +507,16 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
 
   bool again = false;
 
-  std::vector<std::pair<MutableTerm, MutableTerm>> resolvedCriticalPairs;
-  std::vector<RewritePath> resolvedPaths;
+  std::vector<CriticalPair> resolvedCriticalPairs;
   std::vector<RewriteLoop> resolvedLoops;
 
   do {
     // 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);
-      if (lhs.isSimplified())
+      if (lhs.isLHSSimplified() ||
+          lhs.isRHSSimplified() ||
+          lhs.isSubstitutionSimplified())
         continue;
 
       // Look up every suffix of this rule in the trie using findAll(). This
@@ -529,7 +529,9 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
       while (from < to) {
         Trie.findAll(from, to, [&](unsigned j) {
           const auto &rhs = getRule(j);
-          if (rhs.isSimplified())
+          if (rhs.isLHSSimplified() ||
+              rhs.isRHSSimplified() ||
+              rhs.isSubstitutionSimplified())
             return;
 
           if (from == lhs.getLHS().begin()) {
@@ -557,23 +559,21 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
           // Try to repair the confluence violation by adding a new rule.
           if (computeCriticalPair(from, lhs, rhs,
                                   resolvedCriticalPairs,
-                                  resolvedPaths,
                                   resolvedLoops)) {
             if (Debug.contains(DebugFlags::Completion)) {
               const auto &pair = resolvedCriticalPairs.back();
-              const auto &path = resolvedPaths.back();
 
               llvm::dbgs() << "$ Overlapping rules: (#" << i << ") ";
               llvm::dbgs() << lhs << "\n";
               llvm::dbgs() << "                -vs- (#" << j << ") ";
               llvm::dbgs() << rhs << ":\n";
               llvm::dbgs() << "$$ First term of critical pair is "
-                           << pair.first << "\n";
+                           << pair.LHS << "\n";
               llvm::dbgs() << "$$ Second term of critical pair is "
-                           << pair.second << "\n\n";
+                           << pair.RHS << "\n\n";
 
               llvm::dbgs() << "$$ Resolved via path: ";
-              path.dump(llvm::dbgs(), pair.first, *this);
+              pair.Path.dump(llvm::dbgs(), pair.LHS, *this);
               llvm::dbgs() << "\n\n";
             }
           } else {
@@ -598,18 +598,13 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
 
     simplifyLeftHandSides();
 
-    assert(resolvedCriticalPairs.size() == resolvedPaths.size());
-
     again = false;
-    for (unsigned index : indices(resolvedCriticalPairs)) {
-      const auto &pair = resolvedCriticalPairs[index];
-      const auto &path = resolvedPaths[index];
-
+    for (const auto &pair : resolvedCriticalPairs) {
       // Check if we've already done too much work.
       if (Rules.size() > maxIterations)
         return std::make_pair(CompletionResult::MaxIterations, steps);
 
-      if (!addRule(pair.first, pair.second, &path))
+      if (!addRule(pair.LHS, pair.RHS, &pair.Path))
         continue;
 
       // Check if the new rule is too long.
@@ -626,10 +621,10 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
     }
 
     resolvedCriticalPairs.clear();
-    resolvedPaths.clear();
     resolvedLoops.clear();
 
-    simplifyRightHandSidesAndSubstitutions();
+    simplifyRightHandSides();
+    simplifyLeftHandSideSubstitutions();
 
     // If the added rules merged any associated types, process the merges now
     // before we continue with the completion procedure. This is important