Skip to content

Commit 3ddf2f4

Browse files
hvitvedhvitved
committed
wip
1 parent f8ec5cc commit 3ddf2f4

File tree

4 files changed

+63
-130
lines changed

4 files changed

+63
-130
lines changed

‎rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ module SatisfiesBlanketConstraint<
134134
exists(ArgumentTypeAndBlanketOffset ato, Trait traitBound |
135135
ato = MkArgumentTypeAndBlanketOffset(at, _) and
136136
SatisfiesBlanketConstraintInput::relevantConstraint(ato, impl, traitBound) and
137-
SatisfiesBlanketConstraint::satisfiesConstraintType(ato, TTrait(traitBound), _, _)
137+
SatisfiesBlanketConstraint::satisfiesConstraint(ato, TTrait(traitBound), _, _)
138138
)
139139
or
140140
exists(TypeParam blanketTypeParam |

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2521,7 +2521,7 @@ private module AssocFunctionResolution {
25212521
) {
25222522
exists(CallDerefCand cdc, TypePath exprPath |
25232523
cdc = MkCallDerefCand(afc, selfPos, derefChain) and
2524-
CallSatisfiesDerefConstraint::satisfiesConstraintTypeThrough(cdc, impl, _, exprPath, result) and
2524+
CallSatisfiesDerefConstraint::satisfiesConstraintThrough(cdc, impl, _, exprPath, result) and
25252525
exprPath.isCons(getDerefTargetTypeParameter(), path)
25262526
)
25272527
}
@@ -3623,7 +3623,7 @@ private module AwaitSatisfiesType = SatisfiesType<AwaitTarget, AwaitSatisfiesTyp
36233623
pragma[nomagic]
36243624
private Type inferAwaitExprType(AstNode n, TypePath path) {
36253625
exists(TypePath exprPath |
3626-
AwaitSatisfiesType::satisfiesConstraintType(n.(AwaitExpr).getExpr(), _, exprPath, result) and
3626+
AwaitSatisfiesType::satisfiesConstraint(n.(AwaitExpr).getExpr(), _, exprPath, result) and
36273627
exprPath.isCons(getFutureOutputTypeParameter(), path)
36283628
)
36293629
}
@@ -3790,7 +3790,7 @@ private Type inferForLoopExprType(AstNode n, TypePath path) {
37903790
// type of iterable -> type of pattern (loop variable)
37913791
exists(ForExpr fe, TypePath exprPath, AssociatedTypeTypeParameter tp |
37923792
n = fe.getPat() and
3793-
ForIterableSatisfiesType::satisfiesConstraintType(fe.getIterable(), _, exprPath, result) and
3793+
ForIterableSatisfiesType::satisfiesConstraint(fe.getIterable(), _, exprPath, result) and
37943794
exprPath.isCons(tp, path)
37953795
|
37963796
tp = getIntoIteratorItemTypeParameter()

‎rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -769,7 +769,7 @@ private Type getPathConcreteAssocTypeAt(Path path, TypePath typePath) {
769769
TypeAlias alias, TypePath path0
770770
|
771771
pathConcreteTypeAssocType(path, tm, trait, traitOrTmTrait, alias) and
772-
PathSatisfiesConstraint::satisfiesConstraintTypeThrough(tm, impl, traitOrTmTrait, path0, result) and
772+
PathSatisfiesConstraint::satisfiesConstraintThrough(tm, impl, traitOrTmTrait, path0, result) and
773773
path0.isCons(TAssociatedTypeTypeParameter(trait, alias), typePath)
774774
)
775775
}

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

Lines changed: 58 additions & 125 deletions
Original file line numberDiff line numberDiff line change
@@ -1072,7 +1072,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10721072
}
10731073

10741074
pragma[nomagic]
1075-
private predicate satisfiesConstraintTypeMention1(
1075+
private predicate satisfiesConstraint0(
10761076
Term term, Constraint constraint, TypeAbstraction abs, TypeMention sub, TypePath path,
10771077
Type t
10781078
) {
@@ -1100,45 +1100,31 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11001100
}
11011101

11021102
pragma[inline]
1103-
private predicate satisfiesConstraintTypeMentionInline(
1104-
Term term, Constraint constraint, TypeAbstraction abs, TypePath path,
1103+
private predicate satisfiesConstraintInline(
1104+
Term term, Constraint constraint, TypeAbstraction abs, TypePath pathToTypeParamInConstraint,
11051105
TypePath pathToTypeParamInSub, TypeParameter tp
11061106
) {
11071107
exists(TypeMention sub |
1108-
// `impl<T> From<S<T>> for Option<T> {`
1109-
// ^^^^^^^^^ sub
1110-
// ^^^^^^^^^^ constraintMention
1111-
// ^ tp
1112-
// `pathToTypeParamInSub` = `T_option`.
1113-
// `path` = `T_From.T_S`.
1114-
// `constraint` = `trait From`.
1115-
//
1116-
satisfiesConstraintTypeMention1(term, constraint, abs, sub, path, tp) and
1108+
satisfiesConstraint0(term, constraint, abs, sub, pathToTypeParamInConstraint, tp) and
11171109
tp = abs.getATypeParameter() and
11181110
sub.getTypeAt(pathToTypeParamInSub) = tp
11191111
)
11201112
}
11211113

11221114
pragma[nomagic]
1123-
private predicate satisfiesConstraintTypeMention(
1124-
Term term, Constraint constraint, TypePath path, TypePath pathToTypeParamInSub
1125-
) {
1126-
satisfiesConstraintTypeMentionInline(term, constraint, _, path, pathToTypeParamInSub, _)
1127-
}
1128-
1129-
pragma[nomagic]
1130-
private predicate satisfiesConstraintTypeMentionThrough(
1131-
Term term, Constraint constraint, TypeAbstraction abs, TypePath path,
1115+
predicate satisfiesConstraint0(
1116+
Term term, Constraint constraint, TypePath pathToTypeParamInConstraint,
11321117
TypePath pathToTypeParamInSub
11331118
) {
1134-
satisfiesConstraintTypeMentionInline(term, constraint, abs, path, pathToTypeParamInSub, _)
1119+
satisfiesConstraintInline(term, constraint, _, pathToTypeParamInConstraint,
1120+
pathToTypeParamInSub, _)
11351121
}
11361122

11371123
pragma[inline]
1138-
private predicate satisfiesConstraintTypeNonTypeParamInline(
1124+
private predicate satisfiesConstraintNonTypeParamInline(
11391125
Term term, TypeAbstraction abs, Constraint constraint, TypePath path, Type t
11401126
) {
1141-
satisfiesConstraintTypeMention1(term, constraint, abs, _, path, t) and
1127+
satisfiesConstraint0(term, constraint, abs, _, path, t) and
11421128
not t = abs.getATypeParameter()
11431129
}
11441130

@@ -1154,11 +1140,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11541140
* with the type `t` at `path`.
11551141
*/
11561142
pragma[nomagic]
1157-
predicate satisfiesConstraintType(Term term, Constraint constraint, TypePath path, Type t) {
1158-
satisfiesConstraintTypeNonTypeParamInline(term, _, constraint, path, t)
1143+
predicate satisfiesConstraint(Term term, Constraint constraint, TypePath path, Type t) {
1144+
satisfiesConstraintNonTypeParamInline(term, _, constraint, path, t)
11591145
or
11601146
exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
1161-
satisfiesConstraintTypeMention(term, constraint, prefix0, pathToTypeParamInSub) and
1147+
satisfiesConstraint0(term, constraint, prefix0, pathToTypeParamInSub) and
11621148
getTypeAt(term, pathToTypeParamInSub.appendInverse(suffix)) = t and
11631149
path = prefix0.append(suffix)
11641150
)
@@ -1167,36 +1153,32 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11671153
t = getTypeAt(term, path)
11681154
}
11691155

1156+
pragma[nomagic]
1157+
private predicate satisfiesConstraintThrough0(
1158+
Term term, Constraint constraint, TypeAbstraction abs, TypePath pathToTypeParamInConstraint,
1159+
TypePath pathToTypeParamInSub
1160+
) {
1161+
satisfiesConstraintInline(term, constraint, abs, pathToTypeParamInConstraint,
1162+
pathToTypeParamInSub, _)
1163+
}
1164+
11701165
/**
11711166
* Holds if the type tree at `term` satisfies the constraint `constraint`
11721167
* through `abs` with the type `t` at `path`.
11731168
*/
11741169
pragma[nomagic]
1175-
predicate satisfiesConstraintTypeThrough(
1170+
predicate satisfiesConstraintThrough(
11761171
Term term, TypeAbstraction abs, Constraint constraint, TypePath path, Type t
11771172
) {
1178-
satisfiesConstraintTypeNonTypeParamInline(term, abs, constraint, path, t)
1173+
satisfiesConstraintNonTypeParamInline(term, abs, constraint, path, t)
11791174
or
11801175
exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
1181-
satisfiesConstraintTypeMentionThrough(term, constraint, abs, prefix0, pathToTypeParamInSub) and
1176+
satisfiesConstraintThrough0(term, constraint, abs, prefix0, pathToTypeParamInSub) and
11821177
getTypeAt(term, pathToTypeParamInSub.appendInverse(suffix)) = t and
11831178
path = prefix0.append(suffix)
11841179
)
11851180
}
11861181

1187-
pragma[nomagic]
1188-
predicate test(
1189-
// Term tt, TypePath pathToTypeParamInSub, TypeAbstraction abs, Type constraint,
1190-
// TypeParameter tp, TypePath path
1191-
Term term, Constraint constraint, TypeAbstraction abs, TypePath path,
1192-
TypePath pathToTypeParamInSub, TypeParameter tp
1193-
) {
1194-
// Term term, Constraint constraint, TypeAbstraction abs, TypePath path,
1195-
// TypePath pathToTypeParamInSub, TypeParameter tp
1196-
satisfiesConstraintTypeMentionInline(term, constraint, abs, path, pathToTypeParamInSub, tp)
1197-
// satisfiesConstraintTypeMentionInline(tt, abs, constraint, path, pathToTypeParamInSub, tp)
1198-
}
1199-
12001182
/**
12011183
* Holds if the type tree at `term` does _not_ satisfy the constraint `constraint`.
12021184
*
@@ -1579,38 +1561,38 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
15791561
SatisfiesTypeParameterConstraintInput>;
15801562

15811563
pragma[nomagic]
1582-
predicate satisfiesConstraintType(
1564+
predicate satisfiesConstraint(
15831565
Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
15841566
TypeMention constraint, TypePath path, Type t
15851567
) {
15861568
exists(RelevantAccess ra |
15871569
ra = MkRelevantAccess(a, apos, e, prefix) and
1588-
SatisfiesTypeParameterConstraint::satisfiesConstraintType(ra, constraint, path, t) and
1570+
SatisfiesTypeParameterConstraint::satisfiesConstraint(ra, constraint, path, t) and
15891571
constraint = ra.getConstraint(target)
15901572
)
15911573
}
15921574

1593-
predicate satisfiesConstraintTypeThrough(
1575+
predicate satisfiesConstraintThrough(
15941576
Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
15951577
TypeAbstraction abs, TypeMention constraint, TypePath path, Type t
15961578
) {
15971579
exists(RelevantAccess ra |
15981580
ra = MkRelevantAccess(a, apos, e, prefix) and
1599-
SatisfiesTypeParameterConstraint::satisfiesConstraintTypeThrough(ra, abs, constraint,
1600-
path, t) and
1581+
SatisfiesTypeParameterConstraint::satisfiesConstraintThrough(ra, abs, constraint, path,
1582+
t) and
16011583
constraint = ra.getConstraint(target)
16021584
)
16031585
}
16041586

1605-
predicate test(
1587+
predicate satisfiesConstraint0(
16061588
Access a, TypePath pathToTypeParamInSub, AccessEnvironment e, Declaration target,
1607-
AccessPosition apos, TypePath prefix, TypeAbstraction abs, TypeMention constraint,
1608-
TypeParameter tp, TypePath path
1589+
AccessPosition apos, TypePath prefix, TypeMention constraint,
1590+
TypePath pathToTypeParamInConstraint
16091591
) {
16101592
exists(RelevantAccess ra |
16111593
ra = MkRelevantAccess(a, apos, e, prefix) and
1612-
SatisfiesTypeParameterConstraint::test(ra, constraint, abs, path, pathToTypeParamInSub,
1613-
tp) and
1594+
SatisfiesTypeParameterConstraint::satisfiesConstraint0(ra, constraint,
1595+
pathToTypeParamInConstraint, pathToTypeParamInSub) and
16141596
constraint = ra.getConstraint(target)
16151597
)
16161598
}
@@ -1753,79 +1735,11 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
17531735
not exists(getTypeArgument(a, target, tp, _)) and
17541736
exists(TypeMention constraint, AccessPosition apos, TypePath pathToTp, TypePath pathToTp2 |
17551737
typeParameterConstraintHasTypeParameter(target, apos, pathToTp2, constraint, pathToTp, tp) and
1756-
AccessConstraint::satisfiesConstraintType(a, e, target, apos, pathToTp2, constraint,
1738+
AccessConstraint::satisfiesConstraint(a, e, target, apos, pathToTp2, constraint,
17571739
pathToTp.appendInverse(path), t)
17581740
)
17591741
}
17601742

1761-
pragma[nomagic]
1762-
private predicate test3(
1763-
Access a, AccessPosition apos, AccessEnvironment e, Declaration target, TypePath path,
1764-
Type t, TypeParameter tp
1765-
) {
1766-
// not exists(getTypeArgument(a, target, tp, _)) and
1767-
exists(
1768-
TypeAbstraction abs, TypeMention constraint, TypePath pathToTypeParamInSub,
1769-
TypePath pathToTp, TypePath pathToTp2, TypePath suffix, TypeParameter tp2, TypePath path3,
1770-
TypePath path4, TypePath prefix //, TypeMention constraint2, AccessPosition apos2,
1771-
|
1772-
// TypePath pathToTp3, TypePath pathToTp4, TypeAbstraction abs2
1773-
// a.getLocation().getStartLine() = 24 and
1774-
// tp = T
1775-
// pathToTp = Args.T0
1776-
// pathToTp2 = ""
1777-
// constraint = trait Fn
1778-
// directTypeMatch(a, e, target, suffix, t, tp) and
1779-
// typeParameterConstraintHasTypeParameter(target, apos2, pathToTp4, constraint2, pathToTp3,
1780-
// tp) and
1781-
// AccessConstraint::satisfiesConstraintTypeThrough(a, e, target, apos2, pathToTp4, abs2,
1782-
// constraint2, pathToTp3.appendInverse(suffix), t) and
1783-
typeMatch(a, e, target, suffix, t, tp) and
1784-
// typeConstraintBaseTypeMatch(a, e, target, path, t, tp) and
1785-
typeParameterConstraintHasTypeParameter(target, apos, pathToTp2, constraint, pathToTp, tp) and
1786-
AccessConstraint::test(a, pathToTypeParamInSub, e, target, apos, prefix, abs,
1787-
/*TODO*/ constraint, tp2, path4) and
1788-
pathToTp = path4.appendInverse(path3) and
1789-
path = prefix.append(pathToTypeParamInSub.append(path3).append(suffix))
1790-
// AccessConstraint::test(a, pathToTypeParamInSub, e, target, apos, _, /*TODO*/ constraint,
1791-
// tp) and
1792-
// path = pathToTypeParamInSub.append(suffix)
1793-
// satisfiesConstraintType(a, e, target, apos, pathToTp2, constraint, pathToTp.appendInverse(path), t)
1794-
)
1795-
}
1796-
1797-
pragma[nomagic]
1798-
private predicate test5(
1799-
Access a, AccessPosition apos, AccessEnvironment e, Declaration target, TypePath path,
1800-
Type t
1801-
) {
1802-
// not exists(getTypeArgument(a, target, tp, _)) and
1803-
exists(
1804-
TypeMention constraint, TypePath pathToTypeParamInSub, TypePath pathToT,
1805-
TypeParameter tp2, TypePath path4, TypePath prefix, TypeParameter constrainedTp,
1806-
TypePath suffix
1807-
|
1808-
// tp2 = Args[Fn]
1809-
// pathToTypeParamInSub = dyn(Args)
1810-
// path4 = Args
1811-
// prefix = ""
1812-
// constraint = trait FnMut
1813-
AccessConstraint::test(a, pathToTypeParamInSub, e, target, apos, prefix, /*TODO*/ _,
1814-
constraint, tp2, path4) and
1815-
typeParameterConstraintHasAny(target, apos, constrainedTp, _, constraint) and
1816-
constraint = getATypeParameterConstraint(constrainedTp) and
1817-
t = constraint.getTypeAt(pathToT) and
1818-
// constraint = getATypeParameterConstraint(constrainedTp, TypePath::nil()) and
1819-
not t instanceof TypeParameter and
1820-
pathToT = path4.appendInverse(suffix) and
1821-
path = prefix.append(pathToTypeParamInSub.append(suffix))
1822-
// AccessConstraint::test(a, pathToTypeParamInSub, e, target, apos, _, /*TODO*/ constraint,
1823-
// tp) and
1824-
// path = pathToTypeParamInSub.append(suffix)
1825-
// satisfiesConstraintType(a, e, target, apos, pathToTp2, constraint, pathToTp.appendInverse(path), t)
1826-
)
1827-
}
1828-
18291743
pragma[inline]
18301744
private predicate typeMatch(
18311745
Access a, AccessEnvironment e, Declaration target, TypePath path, Type t, TypeParameter tp
@@ -1900,9 +1814,28 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
19001814
)
19011815
)
19021816
or
1903-
test3(a, apos, e, _, path, result, _)
1904-
or
1905-
test5(a, apos, e, _, path, result)
1817+
exists(
1818+
Declaration target, TypeMention constraint, TypePath pathToTypeParamInSub,
1819+
TypePath pathToTypeParamInConstraint, TypePath prefix
1820+
|
1821+
AccessConstraint::satisfiesConstraint0(a, pathToTypeParamInSub, e, target, apos, prefix,
1822+
constraint, pathToTypeParamInConstraint)
1823+
|
1824+
exists(TypePath suffix |
1825+
result = constraint.getTypeAt(pathToTypeParamInConstraint.appendInverse(suffix)) and
1826+
not result instanceof TypeParameter and
1827+
path = prefix.append(pathToTypeParamInSub.append(suffix))
1828+
)
1829+
or
1830+
exists(TypeParameter tp, TypePath suffix, TypePath path3, TypePath pathToTp |
1831+
not exists(getTypeArgument(a, target, tp, _)) and
1832+
typeMatch(a, e, target, suffix, result, tp) and
1833+
typeParameterConstraintHasTypeParameter(target, apos, _, constraint, pathToTp, tp) and
1834+
tp = constraint.getTypeAt(pathToTp) and
1835+
pathToTp = pathToTypeParamInConstraint.appendInverse(path3) and
1836+
path = prefix.append(pathToTypeParamInSub.append(path3).append(suffix))
1837+
)
1838+
)
19061839
}
19071840
}
19081841

0 commit comments

Comments
 (0)