Skip to content

Commit a367388

Browse files
paldepindpaldepind
committed
Shared: Refactor type inference and expose SatisfiesConstraint module
1 parent 93c891a commit a367388

File tree

1 file changed

+103
-87
lines changed

1 file changed

+103
-87
lines changed

‎shared/typeinference/codeql/typeinference/internal/TypeInference.qll‎

Lines changed: 103 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -866,6 +866,101 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
866866

867867
private import BaseTypes
868868

869+
signature module SatisfiesConstraintSig<HasTypeTreeSig TypeTree> {
870+
/** Holds if it is relevant to know if `term` satisfies `constraint`. */
871+
predicate relevantConstraint(TypeTree term, Type constraint);
872+
}
873+
874+
module SatisfiesConstraint<HasTypeTreeSig TypeTree, SatisfiesConstraintSig<TypeTree> Input> {
875+
import Input
876+
877+
private module IsInstantiationOfInput implements IsInstantiationOfInputSig<TypeTree> {
878+
predicate potentialInstantiationOf(TypeTree tt, TypeAbstraction abs, TypeMention cond) {
879+
exists(Type constraint, Type type |
880+
type = tt.getTypeAt(TypePath::nil()) and
881+
relevantConstraint(tt, constraint) and
882+
rootTypesSatisfaction(type, constraint, abs, cond, _) and
883+
// We only need to check instantiations where there are multiple candidates.
884+
countConstraintImplementations(type, constraint) > 1
885+
)
886+
}
887+
888+
predicate relevantTypeMention(TypeMention constraint) {
889+
rootTypesSatisfaction(_, _, _, constraint, _)
890+
}
891+
}
892+
893+
/** Holds if the type tree has the type `type` and should satisfy `constraint`. */
894+
private predicate hasTypeConstraint(TypeTree term, Type type, Type constraint) {
895+
type = term.getTypeAt(TypePath::nil()) and
896+
relevantConstraint(term, constraint)
897+
}
898+
899+
/**
900+
* Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
901+
*/
902+
pragma[nomagic]
903+
private predicate hasConstraintMention(
904+
TypeTree tt, TypeAbstraction abs, TypeMention sub, Type constraint,
905+
TypeMention constraintMention
906+
) {
907+
exists(Type type | hasTypeConstraint(tt, type, constraint) |
908+
not exists(countConstraintImplementations(type, constraint)) and
909+
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, _, _) and
910+
resolveTypeMentionRoot(sub) = abs.getATypeParameter() and
911+
constraint = resolveTypeMentionRoot(constraintMention)
912+
or
913+
countConstraintImplementations(type, constraint) > 0 and
914+
rootTypesSatisfaction(type, constraint, abs, sub, constraintMention) and
915+
// When there are multiple ways the type could implement the
916+
// constraint we need to find the right implementation, which is the
917+
// one where the type instantiates the precondition.
918+
if countConstraintImplementations(type, constraint) > 1
919+
then IsInstantiationOf<TypeTree, IsInstantiationOfInput>::isInstantiationOf(tt, abs, sub)
920+
else any()
921+
)
922+
}
923+
924+
pragma[nomagic]
925+
private predicate satisfiesConstraintTypeMention0(
926+
TypeTree tt, Type constraint, TypeAbstraction abs, TypeMention sub, TypePath path, Type t
927+
) {
928+
exists(TypeMention constraintMention |
929+
hasConstraintMention(tt, abs, sub, constraint, constraintMention) and
930+
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
931+
)
932+
}
933+
934+
pragma[nomagic]
935+
private predicate satisfiesConstraintTypeMention1(
936+
TypeTree tt, Type constraint, TypePath path, TypePath pathToTypeParamInSub
937+
) {
938+
exists(TypeAbstraction abs, TypeMention sub, TypeParameter tp |
939+
satisfiesConstraintTypeMention0(tt, constraint, abs, sub, path, tp) and
940+
tp = abs.getATypeParameter() and
941+
sub.resolveTypeAt(pathToTypeParamInSub) = tp
942+
)
943+
}
944+
945+
/**
946+
* Holds if the type tree at `tt` satisfies the constraint `constraint`
947+
* with the type `t` at `path`.
948+
*/
949+
pragma[nomagic]
950+
predicate satisfiesConstraintTypeMention(TypeTree tt, Type constraint, TypePath path, Type t) {
951+
exists(TypeAbstraction abs |
952+
satisfiesConstraintTypeMention0(tt, constraint, abs, _, path, t) and
953+
not t = abs.getATypeParameter()
954+
)
955+
or
956+
exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
957+
satisfiesConstraintTypeMention1(tt, constraint, prefix0, pathToTypeParamInSub) and
958+
tt.getTypeAt(pathToTypeParamInSub.appendInverse(suffix)) = t and
959+
path = prefix0.append(suffix)
960+
)
961+
}
962+
}
963+
869964
/** Provides the input to `Matching`. */
870965
signature module MatchingInputSig {
871966
/**
@@ -1129,11 +1224,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11291224
adjustedAccessType(a, apos, target, path.appendInverse(suffix), result)
11301225
}
11311226

1132-
/** Holds if this relevant access has the type `type` and should satisfy `constraint`. */
1133-
predicate hasTypeConstraint(Type type, Type constraint) {
1134-
adjustedAccessType(a, apos, target, path, type) and
1135-
relevantAccessConstraint(a, target, apos, path, constraint)
1136-
}
1227+
/** Holds if this relevant access should satisfy `constraint`. */
1228+
Type getConstraint() { relevantAccessConstraint(a, target, apos, path, result) }
11371229

11381230
string toString() {
11391231
result = a.toString() + ", " + apos.toString() + ", " + path.toString()
@@ -1142,94 +1234,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11421234
Location getLocation() { result = a.getLocation() }
11431235
}
11441236

1145-
private module IsInstantiationOfInput implements IsInstantiationOfInputSig<RelevantAccess> {
1146-
predicate potentialInstantiationOf(
1147-
RelevantAccess at, TypeAbstraction abs, TypeMention cond
1148-
) {
1149-
exists(Type constraint, Type type |
1150-
at.hasTypeConstraint(type, constraint) and
1151-
rootTypesSatisfaction(type, constraint, abs, cond, _) and
1152-
// We only need to check instantiations where there are multiple candidates.
1153-
countConstraintImplementations(type, constraint) > 1
1154-
)
1155-
}
1156-
1157-
predicate relevantTypeMention(TypeMention constraint) {
1158-
rootTypesSatisfaction(_, _, _, constraint, _)
1237+
private module SatisfiesConstraintInput implements SatisfiesConstraintSig<RelevantAccess> {
1238+
predicate relevantConstraint(RelevantAccess at, Type constraint) {
1239+
constraint = at.getConstraint()
11591240
}
11601241
}
11611242

1162-
/**
1163-
* Holds if `at` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
1164-
*/
1165-
pragma[nomagic]
1166-
private predicate hasConstraintMention(
1167-
RelevantAccess at, TypeAbstraction abs, TypeMention sub, Type constraint,
1168-
TypeMention constraintMention
1169-
) {
1170-
exists(Type type | at.hasTypeConstraint(type, constraint) |
1171-
not exists(countConstraintImplementations(type, constraint)) and
1172-
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, _, _) and
1173-
resolveTypeMentionRoot(sub) = abs.getATypeParameter() and
1174-
constraint = resolveTypeMentionRoot(constraintMention)
1175-
or
1176-
countConstraintImplementations(type, constraint) > 0 and
1177-
rootTypesSatisfaction(type, constraint, abs, sub, constraintMention) and
1178-
// When there are multiple ways the type could implement the
1179-
// constraint we need to find the right implementation, which is the
1180-
// one where the type instantiates the precondition.
1181-
if countConstraintImplementations(type, constraint) > 1
1182-
then
1183-
IsInstantiationOf<RelevantAccess, IsInstantiationOfInput>::isInstantiationOf(at, abs,
1184-
sub)
1185-
else any()
1186-
)
1187-
}
1188-
1189-
pragma[nomagic]
1190-
predicate satisfiesConstraintTypeMention0(
1191-
RelevantAccess at, Access a, AccessPosition apos, TypePath prefix, Type constraint,
1192-
TypeAbstraction abs, TypeMention sub, TypePath path, Type t
1193-
) {
1194-
exists(TypeMention constraintMention |
1195-
at = MkRelevantAccess(a, _, apos, prefix) and
1196-
hasConstraintMention(at, abs, sub, constraint, constraintMention) and
1197-
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
1198-
)
1199-
}
1200-
1201-
pragma[nomagic]
1202-
predicate satisfiesConstraintTypeMention1(
1203-
RelevantAccess at, Access a, AccessPosition apos, TypePath prefix, Type constraint,
1204-
TypePath path, TypePath pathToTypeParamInSub
1205-
) {
1206-
exists(TypeAbstraction abs, TypeMention sub, TypeParameter tp |
1207-
satisfiesConstraintTypeMention0(at, a, apos, prefix, constraint, abs, sub, path, tp) and
1208-
tp = abs.getATypeParameter() and
1209-
sub.resolveTypeAt(pathToTypeParamInSub) = tp
1210-
)
1211-
}
1212-
1213-
/**
1214-
* Holds if the type at `a`, `apos`, and `path` satisfies the constraint
1215-
* `constraint` with the type `t` at `path`.
1216-
*/
1217-
pragma[nomagic]
12181243
predicate satisfiesConstraintTypeMention(
12191244
Access a, AccessPosition apos, TypePath prefix, Type constraint, TypePath path, Type t
12201245
) {
1221-
exists(TypeAbstraction abs |
1222-
satisfiesConstraintTypeMention0(_, a, apos, prefix, constraint, abs, _, path, t) and
1223-
not t = abs.getATypeParameter()
1224-
)
1225-
or
1226-
exists(
1227-
RelevantAccess at, TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix
1228-
|
1229-
satisfiesConstraintTypeMention1(at, a, apos, prefix, constraint, prefix0,
1230-
pathToTypeParamInSub) and
1231-
at.getTypeAt(pathToTypeParamInSub.appendInverse(suffix)) = t and
1232-
path = prefix0.append(suffix)
1246+
exists(RelevantAccess at | at = MkRelevantAccess(a, _, apos, prefix) |
1247+
SatisfiesConstraint<RelevantAccess, SatisfiesConstraintInput>::satisfiesConstraintTypeMention(at,
1248+
constraint, path, t)
12331249
)
12341250
}
12351251
}

0 commit comments

Comments
 (0)