Skip to content

RequirementMachine: Preliminary support for minimizing layout, superclass and concrete type requirements #39749

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Oct 14, 2021
Merged

RequirementMachine: Preliminary support for minimizing layout, superclass and concrete type requirements #39749

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
a6cd78e
RequirementMachine: Fix a typo in debug output and comment
slavapestov Oct 13, 2021
6441b8b
RequirementMachine: Extract some verification logic out of minimizeRe…
slavapestov Oct 13, 2021
11aecda
RequirementMachine: Only add a concrete type adjustment step if the s…
slavapestov Oct 13, 2021
5643972
RequirementMachine: Move some code from PropertyMap.cpp to RewriteCon…
slavapestov Oct 14, 2021
25718c7
RequirementMachine: Preliminary support for minimizing layout, superc…
slavapestov Oct 14, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
114 changes: 63 additions & 51 deletions lib/AST/RequirementMachine/HomotopyReduction.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -778,6 +778,9 @@ void RewriteSystem::minimizeRewriteSystem() {
loop.normalize(*this);
}

// Check invariants before homotopy reduction.
verifyHomotopyGenerators();

// First pass: Eliminate all redundant rules involving unresolved types.
performHomotopyReduction(/*firstPass=*/true,
/*redundantConformances=*/nullptr);
Expand All @@ -798,57 +801,10 @@ void RewriteSystem::minimizeRewriteSystem() {
performHomotopyReduction(/*firstPass=*/false,
/*redundantConformances=*/&redundantConformances);

// Assert if homotopy reduction failed to eliminate a redundant conformance,
// since this suggests a misunderstanding on my part.
for (unsigned ruleID : redundantConformances) {
const auto &rule = getRule(ruleID);
assert(rule.isProtocolConformanceRule() &&
"Redundant conformance is not a conformance rule?");

if (!rule.isRedundant()) {
llvm::errs() << "Homotopy reduction did not eliminate redundant "
<< "conformance?\n";
llvm::errs() << "(#" << ruleID << ") " << rule << "\n\n";
dump(llvm::errs());
abort();
}
}

// Assert if homotopy reduction failed to eliminate a rewrite rule which was
// deleted because either it's left hand side can be reduced by some other
// rule, or because it's right hand side can be reduced further.
for (const auto &rule : Rules) {
// Note that sometimes permanent rules can be simplified, but they can never
// be redundant.
if (rule.isPermanent()) {
if (rule.isRedundant()) {
llvm::errs() << "Permanent rule is redundant: " << rule << "\n\n";
dump(llvm::errs());
abort();
}

continue;
}

if (rule.isRedundant())
continue;

// Simplified rules should be redundant.
if (rule.isSimplified()) {
llvm::errs() << "Simplified rule is not redundant: " << rule << "\n\n";
dump(llvm::errs());
abort();
}

// Rules with unresolved name symbols (other than permanent rules for
// associated type introduction) should be redundant.
if (rule.getLHS().containsUnresolvedSymbols() ||
rule.getRHS().containsUnresolvedSymbols()) {
llvm::errs() << "Unresolved rule is not redundant: " << rule << "\n\n";
dump(llvm::errs());
abort();
}
}
// Check invariants after homotopy reduction.
verifyHomotopyGenerators();
verifyRedundantConformances(redundantConformances);
verifyMinimizedRules();
}

/// Collect all non-permanent, non-redundant rules whose domain is equal to
Expand Down Expand Up @@ -897,4 +853,60 @@ void RewriteSystem::verifyHomotopyGenerators() const {
}
}
#endif
}

/// Assert if homotopy reduction failed to eliminate a redundant conformance,
/// since this suggests a misunderstanding on my part.
void RewriteSystem::verifyRedundantConformances(
llvm::DenseSet<unsigned> redundantConformances) const {
for (unsigned ruleID : redundantConformances) {
const auto &rule = getRule(ruleID);
assert(rule.isProtocolConformanceRule() &&
"Redundant conformance is not a conformance rule?");

if (!rule.isRedundant()) {
llvm::errs() << "Homotopy reduction did not eliminate redundant "
<< "conformance?\n";
llvm::errs() << "(#" << ruleID << ") " << rule << "\n\n";
dump(llvm::errs());
abort();
}
}
}

// Assert if homotopy reduction failed to eliminate a rewrite rule it was
// supposed to delete.
void RewriteSystem::verifyMinimizedRules() const {
for (const auto &rule : Rules) {
// Note that sometimes permanent rules can be simplified, but they can never
// be redundant.
if (rule.isPermanent()) {
if (rule.isRedundant()) {
llvm::errs() << "Permanent rule is redundant: " << rule << "\n\n";
dump(llvm::errs());
abort();
}

continue;
}

if (rule.isRedundant())
continue;

// Simplified rules should be redundant.
if (rule.isSimplified()) {
llvm::errs() << "Simplified rule is not redundant: " << rule << "\n\n";
dump(llvm::errs());
abort();
}

// Rules with unresolved name symbols (other than permanent rules for
// associated type introduction) should be redundant.
if (rule.getLHS().containsUnresolvedSymbols() ||
rule.getRHS().containsUnresolvedSymbols()) {
llvm::errs() << "Unresolved rule is not redundant: " << rule << "\n\n";
dump(llvm::errs());
abort();
}
}
}
147 changes: 20 additions & 127 deletions lib/AST/RequirementMachine/PropertyMap.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,53 +129,6 @@ void PropertyBag::dump(llvm::raw_ostream &out) const {
out << " }";
}

/// Concrete type terms are written in terms of generic parameter types that
/// have a depth of 0, and an index into an array of substitution terms.
///
/// See RewriteSystemBuilder::getConcreteSubstitutionSchema().
static unsigned getGenericParamIndex(Type type) {
auto *paramTy = type->castTo<GenericTypeParamType>();
assert(paramTy->getDepth() == 0);
return paramTy->getIndex();
}

/// Reverses the transformation performed by
/// RewriteSystemBuilder::getConcreteSubstitutionSchema().
static Type getTypeFromSubstitutionSchema(Type schema,
ArrayRef<Term> substitutions,
TypeArrayView<GenericTypeParamType> genericParams,
const MutableTerm &prefix,
const ProtocolGraph &protos,
RewriteContext &ctx) {
assert(!schema->isTypeParameter() && "Must have a concrete type here");

if (!schema->hasTypeParameter())
return schema;

return schema.transformRec([&](Type t) -> Optional<Type> {
if (t->is<GenericTypeParamType>()) {
auto index = getGenericParamIndex(t);
auto substitution = substitutions[index];

// Prepend the prefix of the lookup key to the substitution.
if (prefix.empty()) {
// Skip creation of a new MutableTerm in the case where the
// prefix is empty.
return ctx.getTypeForTerm(substitution, genericParams, protos);
} else {
// Otherwise build a new term by appending the substitution
// to the prefix.
MutableTerm result(prefix);
result.append(substitution);
return ctx.getTypeForTerm(result, genericParams, protos);
}
}

assert(!t->isTypeParameter());
return None;
});
}

/// Given a term \p lookupTerm whose suffix must equal this property bag's
/// key, return a new term with that suffix stripped off. Will be empty if
/// \p lookupTerm exactly equals the key.
Expand Down Expand Up @@ -205,10 +158,10 @@ Type PropertyBag::getSuperclassBound(
const ProtocolGraph &protos,
RewriteContext &ctx) const {
MutableTerm prefix = getPrefixAfterStrippingKey(lookupTerm);
return getTypeFromSubstitutionSchema(Superclass->getSuperclass(),
Superclass->getSubstitutions(),
genericParams, prefix,
protos, ctx);
return ctx.getTypeFromSubstitutionSchema(Superclass->getSuperclass(),
Superclass->getSubstitutions(),
genericParams, prefix,
protos);
}

/// Get the concrete type of the term represented by this property bag.
Expand All @@ -226,70 +179,10 @@ Type PropertyBag::getConcreteType(
const ProtocolGraph &protos,
RewriteContext &ctx) const {
MutableTerm prefix = getPrefixAfterStrippingKey(lookupTerm);
return getTypeFromSubstitutionSchema(ConcreteType->getConcreteType(),
ConcreteType->getSubstitutions(),
genericParams, prefix,
protos, ctx);
}

/// Computes the term corresponding to a member type access on a substitution.
///
/// The type witness is a type parameter of the form τ_0_n.X.Y.Z,
/// where 'n' is an index into the substitution array.
///
/// If the nth entry in the array is S, this will produce S.X.Y.Z.
///
/// There is a special behavior if the substitution is a term consisting of a
/// single protocol symbol [P]. If the innermost associated type in
/// \p typeWitness is [Q:Foo], the result will be [P:Foo], not [P].[Q:Foo] or
/// [Q:Foo].
static MutableTerm getRelativeTermForType(CanType typeWitness,
ArrayRef<Term> substitutions,
RewriteContext &ctx) {
MutableTerm result;

// Get the substitution S corresponding to τ_0_n.
unsigned index = getGenericParamIndex(typeWitness->getRootGenericParam());
result = MutableTerm(substitutions[index]);

// If the substitution is a term consisting of a single protocol symbol
// [P], save P for later.
const ProtocolDecl *proto = nullptr;
if (result.size() == 1 &&
result[0].getKind() == Symbol::Kind::Protocol) {
proto = result[0].getProtocol();
}

// Collect zero or more member type names in reverse order.
SmallVector<Symbol, 3> symbols;
while (auto memberType = dyn_cast<DependentMemberType>(typeWitness)) {
typeWitness = memberType.getBase();

auto *assocType = memberType->getAssocType();
assert(assocType != nullptr &&
"Conformance checking should not produce unresolved member types");

// If the substitution is a term consisting of a single protocol symbol [P],
// produce [P:Foo] instead of [P].[Q:Foo] or [Q:Foo].
const auto *thisProto = assocType->getProtocol();
if (proto && isa<GenericTypeParamType>(typeWitness)) {
thisProto = proto;

assert(result.size() == 1);
assert(result[0].getKind() == Symbol::Kind::Protocol);
assert(result[0].getProtocol() == proto);
result = MutableTerm();
}

symbols.push_back(Symbol::forAssociatedType(thisProto,
assocType->getName(), ctx));
}

// Add the member type names.
for (auto iter = symbols.rbegin(), end = symbols.rend(); iter != end; ++iter)
result.add(*iter);

return result;
return ctx.getTypeFromSubstitutionSchema(ConcreteType->getConcreteType(),
ConcreteType->getSubstitutions(),
genericParams, prefix,
protos);
}

/// This method takes a concrete type that was derived from a concrete type
Expand Down Expand Up @@ -327,7 +220,7 @@ remapConcreteSubstitutionSchema(CanType concreteType,
if (!t->isTypeParameter())
return None;

auto term = getRelativeTermForType(CanType(t), substitutions, ctx);
auto term = ctx.getRelativeTermForType(CanType(t), substitutions);

unsigned newIndex = result.size();
result.push_back(Term::get(term, ctx));
Expand Down Expand Up @@ -368,10 +261,10 @@ namespace {

if (firstAbstract && secondAbstract) {
// Both sides are type parameters; add a same-type requirement.
auto lhsTerm = getRelativeTermForType(CanType(firstType),
lhsSubstitutions, ctx);
auto rhsTerm = getRelativeTermForType(CanType(secondType),
rhsSubstitutions, ctx);
auto lhsTerm = ctx.getRelativeTermForType(CanType(firstType),
lhsSubstitutions);
auto rhsTerm = ctx.getRelativeTermForType(CanType(secondType),
rhsSubstitutions);
if (lhsTerm != rhsTerm) {
if (debug) {
llvm::dbgs() << "%% Induced rule " << lhsTerm
Expand All @@ -385,8 +278,8 @@ namespace {
if (firstAbstract && !secondAbstract) {
// A type parameter is equated with a concrete type; add a concrete
// type requirement.
auto subjectTerm = getRelativeTermForType(CanType(firstType),
lhsSubstitutions, ctx);
auto subjectTerm = ctx.getRelativeTermForType(CanType(firstType),
lhsSubstitutions);

SmallVector<Term, 3> result;
auto concreteType = remapConcreteSubstitutionSchema(CanType(secondType),
Expand All @@ -407,8 +300,8 @@ namespace {
if (!firstAbstract && secondAbstract) {
// A concrete type is equated with a type parameter; add a concrete
// type requirement.
auto subjectTerm = getRelativeTermForType(CanType(secondType),
rhsSubstitutions, ctx);
auto subjectTerm = ctx.getRelativeTermForType(CanType(secondType),
rhsSubstitutions);

SmallVector<Term, 3> result;
auto concreteType = remapConcreteSubstitutionSchema(CanType(firstType),
Expand Down Expand Up @@ -915,8 +808,8 @@ void PropertyMap::concretizeNestedTypesFromConcreteParent(
if (!t->isTypeParameter())
return None;

auto term = getRelativeTermForType(t->getCanonicalType(),
substitutions, Context);
auto term = Context.getRelativeTermForType(t->getCanonicalType(),
substitutions);
System.simplify(term);
return Context.getTypeForTerm(term, { }, Protos);
}));
Expand Down Expand Up @@ -998,7 +891,7 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
// where 'n' is an index into the substitution array.
//
// Add a rule T => S.X.Y...Z, where S is the nth substitution term.
return getRelativeTermForType(typeWitness, substitutions, Context);
return Context.getRelativeTermForType(typeWitness, substitutions);
}

// The type witness is a concrete type.
Expand Down
1 change: 0 additions & 1 deletion lib/AST/RequirementMachine/RequirementMachine.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -502,7 +502,6 @@ void RequirementMachine::computeCompletion(RewriteSystem::ValidityPolicy policy)

// Check invariants.
System.verifyRewriteRules(policy);
System.verifyHomotopyGenerators();

// Build the property map, which also performs concrete term
// unification; if this added any new rules, run the completion
Expand Down
Loading