RequirementMachine: Record property rule IDs in property bags

For homotopy reduction to properly deal with rewrite rules
introduced by property map construction, we need to keep
track of the original property rules when recording properties
in property bags.

For now, this doesn't even attempt to handle unification or
conflicts; we only record the first rule for each kind of
property on a fixed key.

This isn't actually used for anything yet, except a new
verify pass that runs after property map construction.

Author: slavapestov

lib/AST/RequirementMachine/PropertyMap.cpp

@@ -190,7 +190,9 @@ void PropertyBag::copyPropertiesFrom(const PropertyBag *next,
   // Conformances and the layout constraint, if any, can be copied over
   // unmodified.
   ConformsTo = next->ConformsTo;
+  ConformsToRules = next->ConformsToRules;
   Layout = next->Layout;
+  LayoutRule = next->LayoutRule;
 
   // If the property bag of V has superclass or concrete type
   // substitutions {X1, ..., Xn}, then the property bag of
@@ -200,14 +202,33 @@ void PropertyBag::copyPropertiesFrom(const PropertyBag *next,
   if (next->Superclass) {
     Superclass = next->Superclass->prependPrefixToConcreteSubstitutions(
         prefix, ctx);
+    SuperclassRule = next->SuperclassRule;
   }
 
   if (next->ConcreteType) {
     ConcreteType = next->ConcreteType->prependPrefixToConcreteSubstitutions(
         prefix, ctx);
+    ConcreteTypeRule = next->ConcreteTypeRule;
   }
 }
 
+void PropertyBag::verify(const RewriteSystem &system) const {
+#ifndef NDEBUG
+  assert(ConformsTo.size() == ConformsToRules.size());
+  for (unsigned i : indices(ConformsTo)) {
+    auto symbol = system.getRule(ConformsToRules[i]).getLHS().back();
+    assert(symbol.getKind() == Symbol::Kind::Protocol);
+    assert(symbol.getProtocol() == ConformsTo[i]);
+  }
+
+  // FIXME: Once unification introduces new rules, add asserts requiring
+  // that the layout, superclass and concrete type symbols match, as above
+  assert(!Layout.isNull() == LayoutRule.hasValue());
+  assert(Superclass.hasValue() == SuperclassRule.hasValue());
+  assert(ConcreteType.hasValue() == ConcreteTypeRule.hasValue());
+#endif
+}
+
 PropertyMap::~PropertyMap() {
   Trie.updateHistograms(Context.PropertyTrieHistogram,
                         Context.PropertyTrieRootHistogram);
@@ -289,11 +310,12 @@ void PropertyMap::clear() {
 /// Record a protocol conformance, layout or superclass constraint on the given
 /// key. Must be called in monotonically non-decreasing key order.
 void PropertyMap::addProperty(
-    Term key, Symbol property,
+    Term key, Symbol property, unsigned ruleID,
     SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules) {
   assert(property.isProperty());
+  assert(*System.getRule(ruleID).isPropertyRule() == property);
   auto *props = getOrCreateProperties(key);
-  props->addProperty(property, Context,
+  props->addProperty(property, ruleID, Context,
                      inducedRules, Debug.contains(DebugFlags::ConcreteUnification));
 }
 
@@ -314,11 +336,17 @@ PropertyMap::buildPropertyMap(unsigned maxIterations,
                               unsigned maxDepth) {
   clear();
 
+  struct Property {
+    Term key;
+    Symbol symbol;
+    unsigned ruleID;
+  };
+
   // PropertyMap::addRule() requires that shorter rules are added
   // before longer rules, so that it can perform lookups on suffixes and call
   // PropertyBag::copyPropertiesFrom(). However, we don't have to perform a
   // full sort by term order here; a bucket sort by term length suffices.
-  SmallVector<std::vector<std::pair<Term, Symbol>>, 4> properties;
+  SmallVector<std::vector<Property>, 4> properties;
 
   for (const auto &rule : System.getRules()) {
     if (rule.isSimplified())
@@ -336,16 +364,18 @@ PropertyMap::buildPropertyMap(unsigned maxIterations,
     unsigned length = rhs.size();
     if (length >= properties.size())
       properties.resize(length + 1);
-    properties[length].emplace_back(rhs, *property);
+
+    unsigned ruleID = System.getRuleID(rule);
+    properties[length].push_back({rhs, *property, ruleID});
   }
 
   // Merging multiple superclass or concrete type rules can induce new rules
   // to unify concrete type constructor arguments.
   SmallVector<std::pair<MutableTerm, MutableTerm>, 3> inducedRules;
 
   for (const auto &bucket : properties) {
-    for (auto pair : bucket) {
-      addProperty(pair.first, pair.second, inducedRules);
+    for (auto property : bucket) {
+      addProperty(property.key, property.symbol, property.ruleID, inducedRules);
     }
   }
 
@@ -371,6 +401,9 @@ PropertyMap::buildPropertyMap(unsigned maxIterations,
     }
   }
 
+  // Check invariants of the constructed property map.
+  verify();
+
   if (System.getRules().size() > maxIterations)
     return std::make_pair(CompletionResult::MaxIterations, addedNewRules);
 
@@ -385,4 +418,11 @@ void PropertyMap::dump(llvm::raw_ostream &out) const {
     out << "\n";
   }
   out << "}\n";
+}
+
+void PropertyMap::verify() const {
+#ifndef NDEBUG
+  for (const auto &props : Entries)
+    props->verify(System);
+#endif
 }

lib/AST/RequirementMachine/PropertyMap.h

@@ -41,7 +41,6 @@ enum class RequirementKind : unsigned;
 namespace rewriting {
 
 class MutableTerm;
-class RewriteContext;
 class Term;
 
 /// Stores a convenient representation of all "property-like" rewrite rules of
@@ -55,26 +54,39 @@ class PropertyBag {
   /// All protocols this type conforms to.
   llvm::TinyPtrVector<const ProtocolDecl *> ConformsTo;
 
+  /// The corresponding protocol conformance rules.
+  llvm::SmallVector<unsigned, 1> ConformsToRules;
+
   /// The most specific layout constraint this type satisfies.
   LayoutConstraint Layout;
 
+  /// The corresponding layout rule for the above.
+  Optional<unsigned> LayoutRule;
+
   /// The most specific superclass constraint this type satisfies.
   Optional<Symbol> Superclass;
 
+  /// The corresponding superclass rule for the above.
+  Optional<unsigned> SuperclassRule;
+
   /// All concrete conformances of Superclass to the protocols in the
   /// ConformsTo list.
   llvm::TinyPtrVector<ProtocolConformance *> SuperclassConformances;
 
   /// The most specific concrete type constraint this type satisfies.
   Optional<Symbol> ConcreteType;
 
+  /// The corresponding layout rule for the above.
+  Optional<unsigned> ConcreteTypeRule;
+
   /// All concrete conformances of ConcreteType to the protocols in the
   /// ConformsTo list.
   llvm::TinyPtrVector<ProtocolConformance *> ConcreteConformances;
 
   explicit PropertyBag(Term key) : Key(key) {}
 
   void addProperty(Symbol property,
+                   unsigned ruleID,
                    RewriteContext &ctx,
                    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules,
                    bool debug);
@@ -128,6 +140,8 @@ class PropertyBag {
   getConformsToExcludingSuperclassConformances() const;
 
   MutableTerm getPrefixAfterStrippingKey(const MutableTerm &lookupTerm) const;
+
+  void verify(const RewriteSystem &system) const;
 };
 
 /// Stores all rewrite rules of the form T.[p] => T, where [p] is a property
@@ -171,7 +185,7 @@ class PropertyMap {
 
 private:
   void clear();
-  void addProperty(Term key, Symbol property,
+  void addProperty(Term key, Symbol property, unsigned ruleID,
                    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules);
 
   void computeConcreteTypeInDomainMap();
@@ -188,6 +202,8 @@ class PropertyMap {
   MutableTerm computeConstraintTermForTypeWitness(
       Term key, CanType concreteType, CanType typeWitness,
       const MutableTerm &subjectType, ArrayRef<Term> substitutions) const;
+
+  void verify() const;
 };
 
 } // end namespace rewriting

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -309,19 +309,21 @@ static Symbol unifySuperclasses(
 }
 
 void PropertyBag::addProperty(
-    Symbol property, RewriteContext &ctx,
+    Symbol property, unsigned ruleID, RewriteContext &ctx,
     SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules,
     bool debug) {
 
   switch (property.getKind()) {
   case Symbol::Kind::Protocol:
     ConformsTo.push_back(property.getProtocol());
+    ConformsToRules.push_back(ruleID);
     return;
 
   case Symbol::Kind::Layout:
-    if (!Layout)
+    if (!Layout) {
       Layout = property.getLayoutConstraint();
-    else
+      LayoutRule = ruleID;
+    } else
       Layout = Layout.merge(property.getLayoutConstraint());
 
     return;
@@ -334,6 +336,7 @@ void PropertyBag::addProperty(
                                      ctx, inducedRules, debug);
     } else {
       Superclass = property;
+      SuperclassRule = ruleID;
     }
 
     return;
@@ -345,6 +348,7 @@ void PropertyBag::addProperty(
                                 ctx, inducedRules, debug);
     } else {
       ConcreteType = property;
+      ConcreteTypeRule = ruleID;
     }
 
     return;