RequirementMachine: Minimization understands 'relations' among layout requirements

A superclass requirement 'T : C' implies a layout requirement
'T : AnyObject' (if the class is @objc) or 'T : _NativeObject'
(if the class is not @objc).

In the latter case, there might already be a 'T : AnyObject'
requirement, in which case the type parameter 'T' is subject
to two layout requirements:

    T : AnyObject
    T : _NativeObject

The second requirement implies the first however. To encode this
in the world of rewrite loops, we the notion of a 'relation'
between property symbols, and a 'Relation' rewrite step.

Here, the relation is that _NativeObject < AnyObject. Once this
relation is recorded, the Relation rewrite step will transform

    T.[layout: _NativeObject].[layout: AnyObject]

into

    T.[layout: _NativeObject]

and vice versa.

This rewrite step allows us to construct a rewrite loop which
makes the first rewrite rule redundant via the second.

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -97,6 +97,7 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::Relation:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
@@ -220,6 +221,7 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::Relation:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
@@ -321,6 +323,7 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::Relation:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:

lib/AST/RequirementMachine/MinimalConformances.cpp

@@ -137,6 +137,7 @@ void RewriteLoop::findProtocolConformanceRules(
       case RewriteStep::AdjustConcreteType:
       case RewriteStep::Shift:
       case RewriteStep::Decompose:
+      case RewriteStep::Relation:
       case RewriteStep::ConcreteConformance:
       case RewriteStep::SuperclassConformance:
       case RewriteStep::ConcreteTypeWitness:

lib/AST/RequirementMachine/PropertyMap.cpp

@@ -319,7 +319,7 @@ Optional<unsigned> PropertyMap::addProperty(
   assert(*System.getRule(ruleID).isPropertyRule() == property);
   auto *props = getOrCreateProperties(key);
   bool debug = Debug.contains(DebugFlags::ConcreteUnification);
-  return props->addProperty(property, ruleID, Context,
+  return props->addProperty(property, ruleID, System,
                             inducedRules, debug);
 }
 

lib/AST/RequirementMachine/PropertyMap.h

@@ -103,7 +103,7 @@ class PropertyBag {
 
   Optional<unsigned> addProperty(Symbol property,
                                  unsigned ruleID,
-                                 RewriteContext &ctx,
+                                 RewriteSystem &system,
                                  SmallVectorImpl<InducedRule> &inducedRules,
                                  bool debug);
   void copyPropertiesFrom(const PropertyBag *next,

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -37,6 +37,82 @@
 using namespace swift;
 using namespace rewriting;
 
+unsigned RewriteSystem::recordRelation(Symbol lhs, Symbol rhs) {
+  auto key = std::make_pair(lhs, rhs);
+  auto found = RelationMap.find(key);
+  if (found != RelationMap.end())
+    return found->second;
+
+  unsigned index = Relations.size();
+  Relations.push_back(key);
+  auto inserted = RelationMap.insert(std::make_pair(key, index));
+  assert(inserted.second);
+  (void) inserted;
+
+  return index;
+}
+
+RewriteSystem::Relation
+RewriteSystem::getRelation(unsigned index) const {
+  return Relations[index];
+}
+
+/// Given two property rules (T.[p1] => T) and (T.[p2] => T) where [p1] < [p2],
+/// record a rewrite loop that makes the second rule redundant from the first.
+static void recordRelation(unsigned lhsRuleID, unsigned rhsRuleID,
+                           RewriteSystem &system,
+                           SmallVectorImpl<InducedRule> &inducedRules,
+                           bool debug) {
+  const auto &lhsRule = system.getRule(lhsRuleID);
+  const auto &rhsRule = system.getRule(rhsRuleID);
+
+  auto lhsProperty = lhsRule.getLHS().back();
+  auto rhsProperty = rhsRule.getLHS().back();
+
+  assert(lhsProperty.isProperty());
+  assert(rhsProperty.isProperty());
+  assert(lhsProperty.getKind() == rhsProperty.getKind());
+
+  if (debug) {
+    llvm::dbgs() << "%% Recording relation: ";
+    llvm::dbgs() << lhsRule.getLHS() << " < " << rhsProperty << "\n";
+  }
+
+  unsigned relationID = system.recordRelation(lhsProperty, rhsProperty);
+
+  /// Build the following rewrite path:
+  ///
+  ///   (T => T.[p1]).[p2] ⊗ T.Relation([p1].[p2] => [p1]) ⊗ (T.[p1] => T).
+  ///
+  RewritePath path;
+
+  /// Starting from T.[p2], the LHS rule in reverse to get T.[p1].[p2].
+  path.add(RewriteStep::forRewriteRule(/*startOffset=*/0,
+                                       /*endOffset=*/1,
+                                       /*ruleID=*/lhsRuleID,
+                                       /*inverse=*/true));
+
+  /// T.Relation([p1].[p2] => [p1]).
+  path.add(RewriteStep::forRelation(relationID, /*inverse=*/false));
+
+  /// (T.[p1] => T).
+  path.add(RewriteStep::forRewriteRule(/*startOffset=*/0,
+                                       /*endOffset=*/0,
+                                       /*ruleID=*/lhsRuleID,
+                                       /*inverse=*/false));
+
+  /// Add the rule (T.[p2] => T) with the above rewrite path.
+  ///
+  /// Since a rule (T.[p2] => T) *already exists*, both sides of the new
+  /// rule will simplify down to T, and the rewrite path will become a loop.
+  ///
+  /// This loop encodes the fact that (T.[p1] => T) makes (T.[p2] => T)
+  /// redundant.
+  inducedRules.emplace_back(MutableTerm(rhsRule.getLHS()),
+                            MutableTerm(rhsRule.getRHS()),
+                            path);
+}
+
 /// This method takes a concrete type that was derived from a concrete type
 /// produced by RewriteSystemBuilder::getConcreteSubstitutionSchema(),
 /// either by extracting a structural sub-component or performing a (Swift AST)
@@ -310,7 +386,7 @@ static std::pair<Symbol, bool> unifySuperclasses(
 /// Returns the old conflicting rule ID if there was a conflict,
 /// otherwise returns None.
 Optional<unsigned> PropertyBag::addProperty(
-    Symbol property, unsigned ruleID, RewriteContext &ctx,
+    Symbol property, unsigned ruleID, RewriteSystem &system,
     SmallVectorImpl<InducedRule> &inducedRules,
     bool debug) {
 
@@ -320,18 +396,41 @@ Optional<unsigned> PropertyBag::addProperty(
     ConformsToRules.push_back(ruleID);
     return None;
 
-  case Symbol::Kind::Layout:
+  case Symbol::Kind::Layout: {
+    auto newLayout = property.getLayoutConstraint();
+
     if (!Layout) {
-      Layout = property.getLayoutConstraint();
+      // If we haven't seen a layout requirement before, just record it.
+      Layout = newLayout;
       LayoutRule = ruleID;
     } else {
+      // Otherwise, compute the intersection.
       assert(LayoutRule.hasValue());
-      Layout = Layout.merge(property.getLayoutConstraint());
-      if (!Layout->isKnownLayout())
+      auto mergedLayout = Layout.merge(property.getLayoutConstraint());
+
+      // If the intersection is invalid, we have a conflict.
+      if (!mergedLayout->isKnownLayout())
         return LayoutRule;
+
+      // If the intersection is equal to the existing layout requirement,
+      // the new layout requirement is redundant.
+      if (mergedLayout == Layout) {
+        recordRelation(*LayoutRule, ruleID, system, inducedRules, debug);
+
+      // If the intersection is equal to the new layout requirement, the
+      // existing layout requirement is redundant.
+      } else if (mergedLayout == newLayout) {
+        recordRelation(ruleID, *LayoutRule, system, inducedRules, debug);
+        LayoutRule = ruleID;
+      } else {
+        llvm::errs() << "Arbitrary intersection of layout requirements is "
+                     << "supported yet\n";
+        abort();
+      }
     }
 
     return None;
+  }
 
   case Symbol::Kind::Superclass: {
     // FIXME: Also handle superclass vs concrete
@@ -342,7 +441,8 @@ Optional<unsigned> PropertyBag::addProperty(
     } else {
       assert(SuperclassRule.hasValue());
       auto pair = unifySuperclasses(*Superclass, property,
-                                    ctx, inducedRules, debug);
+                                    system.getRewriteContext(),
+                                    inducedRules, debug);
       Superclass = pair.first;
       bool conflict = pair.second;
       if (conflict)
@@ -359,7 +459,8 @@ Optional<unsigned> PropertyBag::addProperty(
     } else {
       assert(ConcreteTypeRule.hasValue());
       bool conflict = unifyConcreteTypes(*ConcreteType, property,
-                                         ctx, inducedRules, debug);
+                                         system.getRewriteContext(),
+                                         inducedRules, debug);
       if (conflict)
         return ConcreteTypeRule;
     }

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -64,6 +64,19 @@ void RewriteStep::dump(llvm::raw_ostream &out,
     out << Arg << ")";
     break;
   }
+  case Relation: {
+    evaluator.applyRelation(*this, system);
+
+    auto relation = system.getRelation(Arg);
+    out << "Relation(";
+    if (Inverse) {
+      out << relation.second << " > " << relation.first;
+    } else {
+      out << relation.first << " < " << relation.second;
+    }
+    out << ")";
+    break;
+  }
   case ConcreteConformance: {
     evaluator.applyConcreteConformance(*this, system);
 
@@ -280,6 +293,41 @@ void RewritePathEvaluator::applyShift(const RewriteStep &step,
   }
 }
 
+void RewritePathEvaluator::applyRelation(const RewriteStep &step,
+                                         const RewriteSystem &system) {
+  assert(step.Kind == RewriteStep::Relation);
+
+  auto relation = system.getRelation(step.Arg);
+  auto &term = getCurrentTerm();
+
+  if (!step.Inverse) {
+    // Given a term T.[p1].[p2].U where |U| == EndOffset, build the
+    // term T.[p1].U.
+
+    auto lhsProperty = *(term.end() - step.EndOffset - 2);
+    auto rhsProperty = *(term.end() - step.EndOffset - 1);
+    assert(lhsProperty == relation.first);
+    assert(rhsProperty == relation.second);
+
+    MutableTerm result(term.begin(), term.end() - step.EndOffset - 1);
+    result.append(term.end() - step.EndOffset, term.end());
+
+    term = result;
+  } else {
+    // Given a term T.[p1].U where |U| == EndOffset, build the
+    // term T.[p1].[p2].U.
+
+    auto lhsProperty = *(term.end() - step.EndOffset - 1);
+    assert(lhsProperty == relation.first);
+
+    MutableTerm result(term.begin(), term.end() - step.EndOffset);
+    result.add(relation.second);
+    result.append(term.end() - step.EndOffset, term.end());
+
+    term = result;
+  }
+}
+
 void RewritePathEvaluator::applyDecompose(const RewriteStep &step,
                                           const RewriteSystem &system) {
   assert(step.Kind == RewriteStep::Decompose);
@@ -623,6 +671,10 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
     applyDecompose(step, system);
     break;
 
+  case RewriteStep::Relation:
+    applyRelation(step, system);
+    break;
+
   case RewriteStep::ConcreteConformance:
   case RewriteStep::SuperclassConformance:
     applyConcreteConformance(step, system);

lib/AST/RequirementMachine/RewriteLoop.h

@@ -87,6 +87,19 @@ struct RewriteStep {
     /// *** Rewrite step kinds introduced by the property map ***
     ///
 
+    /// If not inverted: the top of the primary stack must be a term T.[p1].[p2]
+    /// ending in a pair of property symbols [p1] and [p2], where [p1] < [p2].
+    /// The symbol [p2] is dropped, leaving behind the term T.[p1].
+    ///
+    /// If inverted: the top of the primary stack must be a term T.[p1]
+    /// ending in a property symbol [p1]. The rewrite system must have a
+    /// recorded relation for the pair ([p1], [p2]). The symbol [p2] is added
+    /// to the end of the term, leaving behind the term T.[p1].[p2].
+    ///
+    /// The Arg field stores the result of calling
+    /// RewriteSystem::recordRelation().
+    Relation,
+
     /// If not inverted: the top of the primary stack must be a term ending in
     /// a concrete type symbol [concrete: C] followed by a protocol symbol [P].
     /// These two symbols are combined into a single concrete conformance
@@ -196,6 +209,11 @@ struct RewriteStep {
                        /*arg=*/numSubstitutions, inverse);
   }
 
+  static RewriteStep forRelation(unsigned relationID, bool inverse) {
+    return RewriteStep(Relation, /*startOffset=*/0, /*endOffset=*/0,
+                       /*arg=*/relationID, inverse);
+  }
+
   static RewriteStep forConcreteConformance(bool inverse) {
     return RewriteStep(ConcreteConformance, /*startOffset=*/0, /*endOffset=*/0,
                        /*arg=*/0, inverse);
@@ -402,6 +420,9 @@ struct RewritePathEvaluator {
   void applyShift(const RewriteStep &step,
                   const RewriteSystem &system);
 
+  void applyRelation(const RewriteStep &step,
+                     const RewriteSystem &system);
+
   void applyDecompose(const RewriteStep &step,
                       const RewriteSystem &system);
 

lib/AST/RequirementMachine/RewriteSystem.h

@@ -325,6 +325,17 @@ class RewriteSystem final {
   //////////////////////////////////////////////////////////////////////////////
 
 public:
+  /// The left hand side is known to be smaller than the right hand side.
+  using Relation = std::pair<Symbol, Symbol>;
+
+private:
+  llvm::DenseMap<Relation, unsigned> RelationMap;
+  std::vector<Relation> Relations;
+
+public:
+  unsigned recordRelation(Symbol lhs, Symbol rhs);
+  Relation getRelation(unsigned index) const;
+
   /// A type witness has a subject type, stored in LHS, which takes the form:
   ///
   /// T.[concrete: C : P].[P:X]

test/Generics/superclass_and_layout_requirement.swift

@@ -2,8 +2,14 @@
 
 class C {}
 
-// CHECK: superclass_and_layout_requirement.(file).P@
+// CHECK: superclass_and_layout_requirement.(file).P1@
 // CHECK: Requirement signature: <Self where Self.T : C>
-protocol P {
+protocol P1 {
   associatedtype T : C
 }
+
+// CHECK: superclass_and_layout_requirement.(file).P2@
+// CHECK: Requirement signature: <Self where Self.T : C>
+protocol P2 {
+  associatedtype T where T : C, T : AnyObject
+}