Skip to content

Commit 1ccea7f

Browse files
authored
Merge pull request #19829 from paldepind/rust/type-tree-constraint
Rust: Add `SatisfiesConstraintInput` module in shared type inference
2 parents 1f559b2 + 60c27f8 commit 1ccea7f

File tree

4 files changed

+130
-182
lines changed

4 files changed

+130
-182
lines changed

rust/ql/lib/codeql/rust/internal/PathResolution.qll

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1132,7 +1132,7 @@ pragma[nomagic]
11321132
private predicate crateDependencyEdge(SourceFileItemNode file, string name, CrateItemNode dep) {
11331133
exists(CrateItemNode c | dep = c.(Crate).getDependency(name) | file = c.getASourceFile())
11341134
or
1135-
// Give builtin files, such as `await.rs`, access to `std`
1135+
// Give builtin files access to `std`
11361136
file instanceof BuiltinSourceFile and
11371137
dep.getName() = name and
11381138
name = "std"
@@ -1501,7 +1501,7 @@ private predicate preludeEdge(SourceFile f, string name, ItemNode i) {
15011501
exists(Crate stdOrCore, ModuleLikeNode mod, ModuleItemNode prelude, ModuleItemNode rust |
15021502
f = any(Crate c0 | stdOrCore = c0.getDependency(_) or stdOrCore = c0).getASourceFile()
15031503
or
1504-
// Give builtin files, such as `await.rs`, access to the prelude
1504+
// Give builtin files access to the prelude
15051505
f instanceof BuiltinSourceFile
15061506
|
15071507
stdOrCore.getName() = ["std", "core"] and

rust/ql/lib/codeql/rust/internal/TypeInference.qll

Lines changed: 14 additions & 84 deletions
Original file line numberDiff line numberDiff line change
@@ -997,101 +997,31 @@ private AssociatedTypeTypeParameter getFutureOutputTypeParameter() {
997997
result.getTypeAlias() = any(FutureTrait ft).getOutputType()
998998
}
999999

1000-
/**
1001-
* A matching configuration for resolving types of `.await` expressions.
1002-
*/
1003-
private module AwaitExprMatchingInput implements MatchingInputSig {
1004-
private newtype TDeclarationPosition =
1005-
TSelfDeclarationPosition() or
1006-
TOutputPos()
1007-
1008-
class DeclarationPosition extends TDeclarationPosition {
1009-
predicate isSelf() { this = TSelfDeclarationPosition() }
1010-
1011-
predicate isOutput() { this = TOutputPos() }
1012-
1013-
string toString() {
1014-
this.isSelf() and
1015-
result = "self"
1016-
or
1017-
this.isOutput() and
1018-
result = "(output)"
1019-
}
1020-
}
1021-
1022-
private class BuiltinsAwaitFile extends File {
1023-
BuiltinsAwaitFile() {
1024-
this.getBaseName() = "await.rs" and
1025-
this.getParentContainer() instanceof Builtins::BuiltinsFolder
1026-
}
1027-
}
1028-
1029-
class Declaration extends Function {
1030-
Declaration() {
1031-
this.getFile() instanceof BuiltinsAwaitFile and
1032-
this.getName().getText() = "await_type_matching"
1033-
}
1034-
1035-
TypeParameter getTypeParameter(TypeParameterPosition ppos) {
1036-
typeParamMatchPosition(this.getGenericParamList().getATypeParam(), result, ppos)
1037-
}
1038-
1039-
Type getDeclaredType(DeclarationPosition dpos, TypePath path) {
1040-
dpos.isSelf() and
1041-
result = this.getParam(0).getTypeRepr().(TypeMention).resolveTypeAt(path)
1042-
or
1043-
dpos.isOutput() and
1044-
result = this.getRetType().getTypeRepr().(TypeMention).resolveTypeAt(path)
1045-
}
1046-
}
1047-
1048-
class AccessPosition = DeclarationPosition;
1049-
1050-
class Access extends AwaitExpr {
1051-
Type getTypeArgument(TypeArgumentPosition apos, TypePath path) { none() }
1052-
1053-
AstNode getNodeAt(AccessPosition apos) {
1054-
result = this.getExpr() and
1055-
apos.isSelf()
1056-
or
1057-
result = this and
1058-
apos.isOutput()
1059-
}
1060-
1061-
Type getInferredType(AccessPosition apos, TypePath path) {
1062-
result = inferType(this.getNodeAt(apos), path)
1063-
}
1064-
1065-
Declaration getTarget() { exists(this) and exists(result) }
1066-
}
1067-
1068-
predicate accessDeclarationPositionMatch(AccessPosition apos, DeclarationPosition dpos) {
1069-
apos = dpos
1070-
}
1071-
}
1072-
10731000
pragma[nomagic]
10741001
private TraitType inferAsyncBlockExprRootType(AsyncBlockExpr abe) {
10751002
// `typeEquality` handles the non-root case
10761003
exists(abe) and
10771004
result = getFutureTraitType()
10781005
}
10791006

1080-
private module AwaitExprMatching = Matching<AwaitExprMatchingInput>;
1007+
final class AwaitTarget extends Expr {
1008+
AwaitTarget() { this = any(AwaitExpr ae).getExpr() }
1009+
1010+
Type getTypeAt(TypePath path) { result = inferType(this, path) }
1011+
}
1012+
1013+
private module AwaitSatisfiesConstraintInput implements SatisfiesConstraintInputSig<AwaitTarget> {
1014+
predicate relevantConstraint(AwaitTarget term, Type constraint) {
1015+
exists(term) and
1016+
constraint.(TraitType).getTrait() instanceof FutureTrait
1017+
}
1018+
}
10811019

10821020
pragma[nomagic]
10831021
private Type inferAwaitExprType(AstNode n, TypePath path) {
1084-
exists(AwaitExprMatchingInput::Access a, AwaitExprMatchingInput::AccessPosition apos |
1085-
n = a.getNodeAt(apos) and
1086-
result = AwaitExprMatching::inferAccessType(a, apos, path)
1087-
)
1088-
or
1089-
// This case is needed for `async` functions and blocks, where we assign
1090-
// the type `Future<Output = T>` directly instead of `impl Future<Output = T>`
1091-
//
1092-
// TODO: It would be better if we could handle this in the shared library
10931022
exists(TypePath exprPath |
1094-
result = inferType(n.(AwaitExpr).getExpr(), exprPath) and
1023+
SatisfiesConstraint<AwaitTarget, AwaitSatisfiesConstraintInput>::satisfiesConstraintType(n.(AwaitExpr)
1024+
.getExpr(), _, exprPath, result) and
10951025
exprPath.isCons(getFutureOutputTypeParameter(), path)
10961026
)
10971027
}

rust/tools/builtins/await.rs

Lines changed: 0 additions & 7 deletions
This file was deleted.

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

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

867867
private import BaseTypes
868868

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

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-
}
1234+
/** Holds if this relevant access should satisfy `constraint`. */
1235+
Type getConstraint() { relevantAccessConstraint(a, target, apos, path, result) }
11371236

11381237
string toString() {
11391238
result = a.toString() + ", " + apos.toString() + ", " + path.toString()
@@ -1142,94 +1241,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11421241
Location getLocation() { result = a.getLocation() }
11431242
}
11441243

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-
)
1244+
private module SatisfiesConstraintInput implements
1245+
SatisfiesConstraintInputSig<RelevantAccess>
1246+
{
1247+
predicate relevantConstraint(RelevantAccess at, Type constraint) {
1248+
constraint = at.getConstraint()
11551249
}
1156-
1157-
predicate relevantTypeMention(TypeMention constraint) {
1158-
rootTypesSatisfaction(_, _, _, constraint, _)
1159-
}
1160-
}
1161-
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-
)
11871250
}
11881251

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]
1218-
predicate satisfiesConstraintTypeMention(
1252+
predicate satisfiesConstraintType(
12191253
Access a, AccessPosition apos, TypePath prefix, Type constraint, TypePath path, Type t
12201254
) {
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)
1255+
exists(RelevantAccess at | at = MkRelevantAccess(a, _, apos, prefix) |
1256+
SatisfiesConstraint<RelevantAccess, SatisfiesConstraintInput>::satisfiesConstraintType(at,
1257+
constraint, path, t)
12331258
)
12341259
}
12351260
}
@@ -1366,7 +1391,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13661391
accessDeclarationPositionMatch(apos, dpos) and
13671392
typeParameterConstraintHasTypeParameter(target, dpos, pathToTp2, _, constraint, pathToTp,
13681393
tp) and
1369-
AccessConstraint::satisfiesConstraintTypeMention(a, apos, pathToTp2, constraint,
1394+
AccessConstraint::satisfiesConstraintType(a, apos, pathToTp2, constraint,
13701395
pathToTp.appendInverse(path), t)
13711396
)
13721397
}

0 commit comments

Comments
 (0)