Merge pull request #6712 from hvitved/csharp/subsumption-perf-take2

C#: Speedup type subsumption calculation
This commit is contained in:
Tom Hvitved
2021-09-20 11:59:24 +02:00
committed by GitHub
2 changed files with 85 additions and 153 deletions

View File

@@ -17,7 +17,7 @@ module Gvn {
string getNameNested(Type t) {
if not t instanceof NestedType or t.(NestedType).getDeclaringType() instanceof GenericType
then result = t.getName()
else result = getNameNested(t.(NestedType).getDeclaringType()) + "." + t.getName()
else result = getNameNested(t.(NestedType).getDeclaringType()) + "+" + t.getName()
}
/**
@@ -326,79 +326,53 @@ module Gvn {
getTypeArgument(k, t, i) = TTypeParameterGvnType()
}
/**
* Hold if (non-type-parameters) `arg1` and `arg2` are unifiable, and both are
* the `i`th type argument of a compound type of kind `k`.
*/
pragma[nomagic]
private predicate unifiableNonTypeParameterTypeArguments(
CompoundTypeKind k, GvnTypeArgument arg1, GvnTypeArgument arg2, int i
) {
exists(int j |
arg1 = getNonTypeParameterTypeArgument(k, _, i) and
arg2 = getNonTypeParameterTypeArgument(k, _, j) and
i <= j and
j <= i
|
arg1 = arg2
or
unifiable(arg1, arg2)
)
}
/**
* Hold if `arg1` and `arg2` are unifiable, and both are the `i`th type argument
* of a compound type of kind `k`.
*
* `subsumes` indicates whether `arg1` in fact subsumes `arg2`.
*/
pragma[nomagic]
private predicate unifiableTypeArguments(
CompoundTypeKind k, GvnTypeArgument arg1, GvnTypeArgument arg2, int i
CompoundTypeKind k, GvnTypeArgument arg1, GvnTypeArgument arg2, int i, boolean subsumes
) {
unifiableNonTypeParameterTypeArguments(k, arg1, arg2, i)
or
exists(int j |
arg1 = TTypeParameterGvnType() and
typeArgumentIsTypeParameter(k, _, i) and
arg2 = getTypeArgument(k, _, j) and
i <= j and
j <= i
arg1 = getNonTypeParameterTypeArgument(k, _, pragma[only_bind_into](i)) and
arg2 = getNonTypeParameterTypeArgument(k, _, pragma[only_bind_into](i)) and
(
arg1 = arg2 and
subsumes = true
or
unifiable(arg1, arg2, subsumes)
)
or
exists(int j |
arg1 = getTypeArgument(k, _, i) and
typeArgumentIsTypeParameter(k, _, j) and
arg2 = TTypeParameterGvnType() and
i <= j and
j <= i
)
arg1 = TTypeParameterGvnType() and
typeArgumentIsTypeParameter(k, _, pragma[only_bind_into](i)) and
arg2 = getTypeArgument(k, _, pragma[only_bind_into](i)) and
subsumes = true
or
arg1 = getNonTypeParameterTypeArgument(k, _, pragma[only_bind_into](i)) and
typeArgumentIsTypeParameter(k, _, pragma[only_bind_into](i)) and
arg2 = TTypeParameterGvnType() and
subsumes = false
}
pragma[nomagic]
private predicate unifiableSingle0(
CompoundTypeKind k, ConstructedGvnType t2, GvnTypeArgument arg1, GvnTypeArgument arg2
CompoundTypeKind k, ConstructedGvnType t2, GvnTypeArgument arg1, GvnTypeArgument arg2,
boolean subsumes
) {
unifiableTypeArguments(k, arg1, arg2, 0) and
unifiableTypeArguments(k, arg1, arg2, 0, subsumes) and
arg2 = getTypeArgument(k, t2, 0) and
k.getNumberOfTypeParameters() = 1
}
/**
* Holds if the type arguments of types `t1` and `t2` are unifiable, `t1`
* and `t2` are of the same kind, and the number of type arguments is 1.
*/
private predicate unifiableSingle(ConstructedGvnType t1, ConstructedGvnType t2) {
exists(CompoundTypeKind k, GvnTypeArgument arg1, GvnTypeArgument arg2 |
unifiableSingle0(k, t2, arg1, arg2) and
arg1 = getTypeArgument(k, t1, 0)
)
}
pragma[nomagic]
private predicate unifiableMultiple01Aux0(
CompoundTypeKind k, ConstructedGvnType t2, GvnTypeArgument arg10, GvnTypeArgument arg21
CompoundTypeKind k, ConstructedGvnType t2, GvnTypeArgument arg10, GvnTypeArgument arg21,
boolean subsumes
) {
exists(GvnTypeArgument arg20 |
unifiableTypeArguments(k, arg10, arg20, 0) and
unifiableTypeArguments(k, arg10, arg20, 0, subsumes) and
arg20 = getTypeArgument(k, t2, 0) and
arg21 = getTypeArgument(k, t2, 1)
)
@@ -406,43 +380,24 @@ module Gvn {
pragma[nomagic]
private predicate unifiableMultiple01Aux1(
CompoundTypeKind k, ConstructedGvnType t1, GvnTypeArgument arg10, GvnTypeArgument arg21
CompoundTypeKind k, ConstructedGvnType t1, GvnTypeArgument arg10, GvnTypeArgument arg21,
boolean subsumes
) {
exists(GvnTypeArgument arg11 |
unifiableTypeArguments(k, arg11, arg21, 1) and
unifiableTypeArguments(k, arg11, arg21, 1, subsumes) and
arg10 = getTypeArgument(k, t1, 0) and
arg11 = getTypeArgument(k, t1, 1)
)
}
/**
* Holds if the first two type arguments of types `t1` and `t2` are unifiable,
* and both `t1` and `t2` are of kind `k`.
*/
private predicate unifiableMultiple01(
CompoundTypeKind k, ConstructedGvnType t1, ConstructedGvnType t2
) {
exists(GvnTypeArgument arg10, GvnTypeArgument arg21 |
unifiableMultiple01Aux0(k, t2, arg10, arg21) and
unifiableMultiple01Aux1(k, t1, arg10, arg21)
)
}
pragma[nomagic]
private predicate unifiableMultiple2Aux(
CompoundTypeKind k, ConstructedGvnType t2, int i, GvnTypeArgument arg1, GvnTypeArgument arg2
CompoundTypeKind k, ConstructedGvnType t2, int i, GvnTypeArgument arg1, boolean subsumes
) {
unifiableTypeArguments(k, arg1, arg2, i) and
arg2 = getTypeArgument(k, t2, i) and
i >= 2
}
private predicate unifiableMultiple2(
CompoundTypeKind k, ConstructedGvnType t1, ConstructedGvnType t2, int i
) {
exists(GvnTypeArgument arg1, GvnTypeArgument arg2 |
unifiableMultiple2Aux(k, t2, i, arg1, arg2) and
arg1 = getTypeArgument(k, t1, i)
exists(GvnTypeArgument arg2 |
unifiableTypeArguments(k, arg1, arg2, i, subsumes) and
arg2 = getTypeArgument(k, t2, i) and
i >= 2
)
}
@@ -452,43 +407,33 @@ module Gvn {
*/
pragma[nomagic]
private predicate unifiableMultiple(
CompoundTypeKind k, ConstructedGvnType t1, ConstructedGvnType t2, int i
CompoundTypeKind k, ConstructedGvnType t1, ConstructedGvnType t2, int i, boolean subsumes
) {
unifiableMultiple01(k, t1, t2) and i = 1
exists(GvnTypeArgument arg10, GvnTypeArgument arg21, boolean subsumes1, boolean subsumes2 |
unifiableMultiple01Aux0(k, t2, arg10, arg21, subsumes1) and
unifiableMultiple01Aux1(k, t1, arg10, arg21, subsumes2) and
subsumes = subsumes1.booleanAnd(subsumes2)
) and
i = 1
or
unifiableMultiple(k, t1, t2, i - 1) and
unifiableMultiple2(k, t1, t2, i)
}
private newtype TTypePath =
TTypePathNil() or
TTypePathCons(int head, TTypePath tail) { exists(getTypeAtCons(_, head, tail)) }
/**
* Gets the GVN inside GVN `t`, by following the path `path`, if any.
*/
private GvnType getTypeAt(GvnType t, TTypePath path) {
path = TTypePathNil() and
result = t
or
exists(ConstructedGvnTypeList l, int head, TTypePath tail |
t = TConstructedGvnType(l) and
path = TTypePathCons(head, tail) and
result = getTypeAtCons(l, head, tail)
exists(GvnTypeArgument arg1, boolean subsumes1, boolean subsumes2 |
unifiableMultiple(k, t1, t2, i - 1, subsumes1) and
unifiableMultiple2Aux(k, t2, i, arg1, subsumes2) and
arg1 = getTypeArgument(k, t1, i) and
subsumes = subsumes1.booleanAnd(subsumes2)
)
}
private GvnType getTypeAtCons(ConstructedGvnTypeList l, int head, TTypePath tail) {
result = getTypeAt(l.getArg(head), tail)
}
/**
* Gets the leaf GVN inside GVN `t`, by following the path `path`, if any.
*/
pragma[noinline]
private GvnType getLeafTypeAt(GvnType t, TTypePath path) {
result = getTypeAt(t, path) and
not result instanceof ConstructedGvnType
pragma[nomagic]
private predicate unifiable(ConstructedGvnType t1, ConstructedGvnType t2, boolean subsumes) {
exists(CompoundTypeKind k, GvnTypeArgument arg1, GvnTypeArgument arg2 |
unifiableSingle0(k, t2, arg1, arg2, subsumes) and
arg1 = getTypeArgument(k, t1, 0)
)
or
exists(CompoundTypeKind k |
unifiableMultiple(k, t1, t2, k.getNumberOfTypeParameters() - 1, subsumes)
)
}
cached
@@ -540,33 +485,20 @@ module Gvn {
}
/**
* Holds if GVNs `t1` and `t2` can be unified. That is, is it possible to
* Holds if GVNs `t1` and `t2` can be unified. That is, it is possible to
* replace all type parameters in `t1` and `t2` with some GVNs (possibly
* type parameters themselves) to make the two substituted terms equal.
*/
cached
predicate unifiable(ConstructedGvnType t1, ConstructedGvnType t2) {
unifiableSingle(t1, t2)
or
exists(CompoundTypeKind k | unifiableMultiple(k, t1, t2, k.getNumberOfTypeParameters() - 1))
}
predicate unifiable(ConstructedGvnType t1, ConstructedGvnType t2) { unifiable(t1, t2, _) }
/**
* Holds if GVN `t1` subsumes GVN `t2`. That is, is it possible to replace all
* Holds if GVN `t1` subsumes GVN `t2`. That is, it is possible to replace all
* type parameters in `t1` with some GVNs (possibly type parameters themselves)
* to make the two substituted terms equal.
*/
cached
predicate subsumes(ConstructedGvnType t1, ConstructedGvnType t2) {
unifiable(t1, t2) and // subsumption implies unification
forall(TTypePath path, GvnType leaf1 | leaf1 = getLeafTypeAt(t1, path) |
exists(GvnType child2 | child2 = getTypeAt(t2, path) |
leaf1 = TTypeParameterGvnType()
or
leaf1 = child2
)
)
}
predicate subsumes(ConstructedGvnType t1, ConstructedGvnType t2) { unifiable(t1, t2, true) }
}
import Cached

View File

@@ -32,21 +32,21 @@ edges
| Types.cs:74:9:74:9 | access to local variable d : D | Types.cs:16:30:16:30 | this : D |
| Types.cs:77:22:77:22 | a : C | Types.cs:79:18:79:25 | SSA def(b) : C |
| Types.cs:79:18:79:25 | SSA def(b) : C | Types.cs:80:18:80:18 | access to local variable b |
| Types.cs:90:22:90:22 | e : Types.E<D>.E2 | Types.cs:92:26:92:26 | access to parameter e : Types.E<D>.E2 |
| Types.cs:92:13:92:16 | [post] this access [field Field] : Types.E<D>.E2 | Types.cs:93:13:93:16 | this access [field Field] : Types.E<D>.E2 |
| Types.cs:92:26:92:26 | access to parameter e : Types.E<D>.E2 | Types.cs:92:13:92:16 | [post] this access [field Field] : Types.E<D>.E2 |
| Types.cs:93:13:93:16 | this access [field Field] : Types.E<D>.E2 | Types.cs:113:34:113:34 | this [field Field] : Types.E<D>.E2 |
| Types.cs:110:25:110:32 | object creation of type E2 : Types.E<D>.E2 | Types.cs:90:22:90:22 | e : Types.E<D>.E2 |
| Types.cs:113:34:113:34 | this [field Field] : Types.E<D>.E2 | Types.cs:115:22:115:25 | this access [field Field] : Types.E<D>.E2 |
| Types.cs:115:22:115:25 | this access [field Field] : Types.E<D>.E2 | Types.cs:115:22:115:31 | access to field Field |
| Types.cs:90:22:90:22 | e : Types+E<D>.E2 | Types.cs:92:26:92:26 | access to parameter e : Types+E<D>.E2 |
| Types.cs:92:13:92:16 | [post] this access [field Field] : Types+E<D>.E2 | Types.cs:93:13:93:16 | this access [field Field] : Types+E<D>.E2 |
| Types.cs:92:26:92:26 | access to parameter e : Types+E<D>.E2 | Types.cs:92:13:92:16 | [post] this access [field Field] : Types+E<D>.E2 |
| Types.cs:93:13:93:16 | this access [field Field] : Types+E<D>.E2 | Types.cs:113:34:113:34 | this [field Field] : Types+E<D>.E2 |
| Types.cs:110:25:110:32 | object creation of type E2 : Types+E<D>.E2 | Types.cs:90:22:90:22 | e : Types+E<D>.E2 |
| Types.cs:113:34:113:34 | this [field Field] : Types+E<D>.E2 | Types.cs:115:22:115:25 | this access [field Field] : Types+E<D>.E2 |
| Types.cs:115:22:115:25 | this access [field Field] : Types+E<D>.E2 | Types.cs:115:22:115:31 | access to field Field |
| Types.cs:120:25:120:31 | object creation of type A : A | Types.cs:122:30:122:30 | access to local variable a : A |
| Types.cs:121:26:121:33 | object creation of type E2 : Types.E<D>.E2 | Types.cs:123:30:123:31 | access to local variable e2 : Types.E<D>.E2 |
| Types.cs:121:26:121:33 | object creation of type E2 : Types+E<D>.E2 | Types.cs:123:30:123:31 | access to local variable e2 : Types+E<D>.E2 |
| Types.cs:122:30:122:30 | access to local variable a : A | Types.cs:122:22:122:31 | call to method Through |
| Types.cs:122:30:122:30 | access to local variable a : A | Types.cs:130:34:130:34 | x : A |
| Types.cs:123:30:123:31 | access to local variable e2 : Types.E<D>.E2 | Types.cs:123:22:123:32 | call to method Through |
| Types.cs:123:30:123:31 | access to local variable e2 : Types.E<D>.E2 | Types.cs:130:34:130:34 | x : Types.E<D>.E2 |
| Types.cs:123:30:123:31 | access to local variable e2 : Types+E<D>.E2 | Types.cs:123:22:123:32 | call to method Through |
| Types.cs:123:30:123:31 | access to local variable e2 : Types+E<D>.E2 | Types.cs:130:34:130:34 | x : Types+E<D>.E2 |
| Types.cs:130:34:130:34 | x : A | Types.cs:130:40:130:40 | access to parameter x : A |
| Types.cs:130:34:130:34 | x : Types.E<D>.E2 | Types.cs:130:40:130:40 | access to parameter x : Types.E<D>.E2 |
| Types.cs:130:34:130:34 | x : Types+E<D>.E2 | Types.cs:130:40:130:40 | access to parameter x : Types+E<D>.E2 |
| Types.cs:138:21:138:25 | this [field Field] : Object | Types.cs:138:32:138:35 | this access [field Field] : Object |
| Types.cs:138:32:138:35 | this access [field Field] : Object | Types.cs:153:30:153:30 | this [field Field] : Object |
| Types.cs:144:13:144:13 | [post] access to parameter c [field Field] : Object | Types.cs:145:13:145:13 | access to parameter c [field Field] : Object |
@@ -97,24 +97,24 @@ nodes
| Types.cs:77:22:77:22 | a : C | semmle.label | a : C |
| Types.cs:79:18:79:25 | SSA def(b) : C | semmle.label | SSA def(b) : C |
| Types.cs:80:18:80:18 | access to local variable b | semmle.label | access to local variable b |
| Types.cs:90:22:90:22 | e : Types.E<D>.E2 | semmle.label | e : Types.E<D>.E2 |
| Types.cs:92:13:92:16 | [post] this access [field Field] : Types.E<D>.E2 | semmle.label | [post] this access [field Field] : Types.E<D>.E2 |
| Types.cs:92:26:92:26 | access to parameter e : Types.E<D>.E2 | semmle.label | access to parameter e : Types.E<D>.E2 |
| Types.cs:93:13:93:16 | this access [field Field] : Types.E<D>.E2 | semmle.label | this access [field Field] : Types.E<D>.E2 |
| Types.cs:110:25:110:32 | object creation of type E2 : Types.E<D>.E2 | semmle.label | object creation of type E2 : Types.E<D>.E2 |
| Types.cs:113:34:113:34 | this [field Field] : Types.E<D>.E2 | semmle.label | this [field Field] : Types.E<D>.E2 |
| Types.cs:115:22:115:25 | this access [field Field] : Types.E<D>.E2 | semmle.label | this access [field Field] : Types.E<D>.E2 |
| Types.cs:90:22:90:22 | e : Types+E<D>.E2 | semmle.label | e : Types+E<D>.E2 |
| Types.cs:92:13:92:16 | [post] this access [field Field] : Types+E<D>.E2 | semmle.label | [post] this access [field Field] : Types+E<D>.E2 |
| Types.cs:92:26:92:26 | access to parameter e : Types+E<D>.E2 | semmle.label | access to parameter e : Types+E<D>.E2 |
| Types.cs:93:13:93:16 | this access [field Field] : Types+E<D>.E2 | semmle.label | this access [field Field] : Types+E<D>.E2 |
| Types.cs:110:25:110:32 | object creation of type E2 : Types+E<D>.E2 | semmle.label | object creation of type E2 : Types+E<D>.E2 |
| Types.cs:113:34:113:34 | this [field Field] : Types+E<D>.E2 | semmle.label | this [field Field] : Types+E<D>.E2 |
| Types.cs:115:22:115:25 | this access [field Field] : Types+E<D>.E2 | semmle.label | this access [field Field] : Types+E<D>.E2 |
| Types.cs:115:22:115:31 | access to field Field | semmle.label | access to field Field |
| Types.cs:120:25:120:31 | object creation of type A : A | semmle.label | object creation of type A : A |
| Types.cs:121:26:121:33 | object creation of type E2 : Types.E<D>.E2 | semmle.label | object creation of type E2 : Types.E<D>.E2 |
| Types.cs:121:26:121:33 | object creation of type E2 : Types+E<D>.E2 | semmle.label | object creation of type E2 : Types+E<D>.E2 |
| Types.cs:122:22:122:31 | call to method Through | semmle.label | call to method Through |
| Types.cs:122:30:122:30 | access to local variable a : A | semmle.label | access to local variable a : A |
| Types.cs:123:22:123:32 | call to method Through | semmle.label | call to method Through |
| Types.cs:123:30:123:31 | access to local variable e2 : Types.E<D>.E2 | semmle.label | access to local variable e2 : Types.E<D>.E2 |
| Types.cs:123:30:123:31 | access to local variable e2 : Types+E<D>.E2 | semmle.label | access to local variable e2 : Types+E<D>.E2 |
| Types.cs:130:34:130:34 | x : A | semmle.label | x : A |
| Types.cs:130:34:130:34 | x : Types.E<D>.E2 | semmle.label | x : Types.E<D>.E2 |
| Types.cs:130:34:130:34 | x : Types+E<D>.E2 | semmle.label | x : Types+E<D>.E2 |
| Types.cs:130:40:130:40 | access to parameter x : A | semmle.label | access to parameter x : A |
| Types.cs:130:40:130:40 | access to parameter x : Types.E<D>.E2 | semmle.label | access to parameter x : Types.E<D>.E2 |
| Types.cs:130:40:130:40 | access to parameter x : Types+E<D>.E2 | semmle.label | access to parameter x : Types+E<D>.E2 |
| Types.cs:138:21:138:25 | this [field Field] : Object | semmle.label | this [field Field] : Object |
| Types.cs:138:32:138:35 | this access [field Field] : Object | semmle.label | this access [field Field] : Object |
| Types.cs:144:13:144:13 | [post] access to parameter c [field Field] : Object | semmle.label | [post] access to parameter c [field Field] : Object |
@@ -125,7 +125,7 @@ nodes
| Types.cs:153:42:153:51 | access to field Field | semmle.label | access to field Field |
subpaths
| Types.cs:122:30:122:30 | access to local variable a : A | Types.cs:130:34:130:34 | x : A | Types.cs:130:40:130:40 | access to parameter x : A | Types.cs:122:22:122:31 | call to method Through : A |
| Types.cs:123:30:123:31 | access to local variable e2 : Types.E<D>.E2 | Types.cs:130:34:130:34 | x : Types.E<D>.E2 | Types.cs:130:40:130:40 | access to parameter x : Types.E<D>.E2 | Types.cs:123:22:123:32 | call to method Through : Types.E<D>.E2 |
| Types.cs:123:30:123:31 | access to local variable e2 : Types+E<D>.E2 | Types.cs:130:34:130:34 | x : Types+E<D>.E2 | Types.cs:130:40:130:40 | access to parameter x : Types+E<D>.E2 | Types.cs:123:22:123:32 | call to method Through : Types+E<D>.E2 |
#select
| Types.cs:23:12:23:18 | object creation of type C : C | Types.cs:23:12:23:18 | object creation of type C : C | Types.cs:50:18:50:18 | access to local variable c | $@ | Types.cs:50:18:50:18 | access to local variable c | access to local variable c |
| Types.cs:25:12:25:18 | object creation of type C : C | Types.cs:25:12:25:18 | object creation of type C : C | Types.cs:63:33:63:36 | (...) ... | $@ | Types.cs:63:33:63:36 | (...) ... | (...) ... |
@@ -141,7 +141,7 @@ subpaths
| Types.cs:39:12:39:18 | object creation of type D : D | Types.cs:39:12:39:18 | object creation of type D : D | Types.cs:69:52:69:52 | access to parameter x | $@ | Types.cs:69:52:69:52 | access to parameter x | access to parameter x |
| Types.cs:40:12:40:18 | object creation of type D : D | Types.cs:40:12:40:18 | object creation of type D : D | Types.cs:16:42:16:45 | this access | $@ | Types.cs:16:42:16:45 | this access | this access |
| Types.cs:43:20:43:23 | null : null | Types.cs:43:20:43:23 | null : null | Types.cs:44:14:44:14 | access to local variable o | $@ | Types.cs:44:14:44:14 | access to local variable o | access to local variable o |
| Types.cs:110:25:110:32 | object creation of type E2 : Types.E<D>.E2 | Types.cs:110:25:110:32 | object creation of type E2 : Types.E<D>.E2 | Types.cs:115:22:115:31 | access to field Field | $@ | Types.cs:115:22:115:31 | access to field Field | access to field Field |
| Types.cs:110:25:110:32 | object creation of type E2 : Types+E<D>.E2 | Types.cs:110:25:110:32 | object creation of type E2 : Types+E<D>.E2 | Types.cs:115:22:115:31 | access to field Field | $@ | Types.cs:115:22:115:31 | access to field Field | access to field Field |
| Types.cs:120:25:120:31 | object creation of type A : A | Types.cs:120:25:120:31 | object creation of type A : A | Types.cs:122:22:122:31 | call to method Through | $@ | Types.cs:122:22:122:31 | call to method Through | call to method Through |
| Types.cs:121:26:121:33 | object creation of type E2 : Types.E<D>.E2 | Types.cs:121:26:121:33 | object creation of type E2 : Types.E<D>.E2 | Types.cs:123:22:123:32 | call to method Through | $@ | Types.cs:123:22:123:32 | call to method Through | call to method Through |
| Types.cs:121:26:121:33 | object creation of type E2 : Types+E<D>.E2 | Types.cs:121:26:121:33 | object creation of type E2 : Types+E<D>.E2 | Types.cs:123:22:123:32 | call to method Through | $@ | Types.cs:123:22:123:32 | call to method Through | call to method Through |
| Types.cs:144:23:144:34 | object creation of type Object : Object | Types.cs:144:23:144:34 | object creation of type Object : Object | Types.cs:153:42:153:51 | access to field Field | $@ | Types.cs:153:42:153:51 | access to field Field | access to field Field |