mirror of
https://github.com/github/codeql.git
synced 2026-04-26 17:25:19 +02:00
Rust: Infer argument types based on trait bounds on parameters
This commit is contained in:
Tom Hvitved
@@ -964,7 +964,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
/**
|
||||
* Holds if `term` does not satisfy `constraint`.
|
||||
*
|
||||
* This predicate is an approximation of `not hasConstraintMention(term, constraint)`.
|
||||
* This predicate is an approximation of `not hasConstraintMention(term, _, _, constraint, _, _)`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate hasNotConstraintMention(
|
||||
@@ -1072,7 +1072,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate satisfiesConstraintTypeMention1(
|
||||
private predicate satisfiesConstraint0(
|
||||
Term term, Constraint constraint, TypeAbstraction abs, TypeMention sub, TypePath path,
|
||||
Type t
|
||||
) {
|
||||
@@ -1100,37 +1100,55 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
}
|
||||
|
||||
pragma[inline]
|
||||
private predicate satisfiesConstraintTypeMentionInline(
|
||||
Term term, Constraint constraint, TypeAbstraction abs, TypePath path,
|
||||
TypePath pathToTypeParamInSub
|
||||
private predicate satisfiesConstraintInline(
|
||||
Term term, Constraint constraint, TypeAbstraction abs, TypePath pathToTypeParamInConstraint,
|
||||
TypePath pathToTypeParamInSub, TypeParameter tp
|
||||
) {
|
||||
exists(TypeMention sub, TypeParameter tp |
|
||||
satisfiesConstraintTypeMention1(term, constraint, abs, sub, path, tp) and
|
||||
exists(TypeMention sub |
|
||||
satisfiesConstraint0(term, constraint, abs, sub, pathToTypeParamInConstraint, tp) and
|
||||
tp = abs.getATypeParameter() and
|
||||
sub.getTypeAt(pathToTypeParamInSub) = tp
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `term` satisfies the constraint `constraint` with _some_ type
|
||||
* parameter at `pathToTypeParamInConstraint`, and the type parameter occurs
|
||||
* at `pathToTypeParamInSub` in a satisfying condition.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rust
|
||||
* struct MyThing<A> { ... }
|
||||
*
|
||||
* trait MyTrait<B> { ... }
|
||||
*
|
||||
* impl<T> MyTrait<T> for MyThing<T> { ... }
|
||||
*
|
||||
* fn foo<T: MyTrait<i32>>(x: T) { ... }
|
||||
*
|
||||
* let x = MyThing(Default::default());
|
||||
* foo(x);
|
||||
* ```
|
||||
*
|
||||
* At `term` = `foo(x)`, we have `constraint = MyTrait<i32>`, and because of the
|
||||
* `impl` block, `pathToTypeParamInConstraint` = `"B"`, and
|
||||
* `pathToTypeParamInSub` = `"A"`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate satisfiesConstraintTypeMention(
|
||||
Term term, Constraint constraint, TypePath path, TypePath pathToTypeParamInSub
|
||||
) {
|
||||
satisfiesConstraintTypeMentionInline(term, constraint, _, path, pathToTypeParamInSub)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate satisfiesConstraintTypeMentionThrough(
|
||||
Term term, Constraint constraint, TypeAbstraction abs, TypePath path,
|
||||
predicate satisfiesConstraintAtTypeParameter(
|
||||
Term term, Constraint constraint, TypePath pathToTypeParamInConstraint,
|
||||
TypePath pathToTypeParamInSub
|
||||
) {
|
||||
satisfiesConstraintTypeMentionInline(term, constraint, abs, path, pathToTypeParamInSub)
|
||||
satisfiesConstraintInline(term, constraint, _, pathToTypeParamInConstraint,
|
||||
pathToTypeParamInSub, _)
|
||||
}
|
||||
|
||||
pragma[inline]
|
||||
private predicate satisfiesConstraintTypeNonTypeParamInline(
|
||||
private predicate satisfiesConstraintNonTypeParamInline(
|
||||
Term term, TypeAbstraction abs, Constraint constraint, TypePath path, Type t
|
||||
) {
|
||||
satisfiesConstraintTypeMention1(term, constraint, abs, _, path, t) and
|
||||
satisfiesConstraint0(term, constraint, abs, _, path, t) and
|
||||
not t = abs.getATypeParameter()
|
||||
}
|
||||
|
||||
@@ -1142,15 +1160,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the type tree at `term` satisfies the constraint `constraint`
|
||||
* with the type `t` at `path`.
|
||||
* Holds if `term` satisfies the constraint `constraint` with the type `t` at `path`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate satisfiesConstraintType(Term term, Constraint constraint, TypePath path, Type t) {
|
||||
satisfiesConstraintTypeNonTypeParamInline(term, _, constraint, path, t)
|
||||
predicate satisfiesConstraint(Term term, Constraint constraint, TypePath path, Type t) {
|
||||
satisfiesConstraintNonTypeParamInline(term, _, constraint, path, t)
|
||||
or
|
||||
exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
|
||||
satisfiesConstraintTypeMention(term, constraint, prefix0, pathToTypeParamInSub) and
|
||||
satisfiesConstraintAtTypeParameter(term, constraint, prefix0, pathToTypeParamInSub) and
|
||||
getTypeAt(term, pathToTypeParamInSub.appendInverse(suffix)) = t and
|
||||
path = prefix0.append(suffix)
|
||||
)
|
||||
@@ -1159,25 +1176,34 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
t = getTypeAt(term, path)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate satisfiesConstraintThrough0(
|
||||
Term term, Constraint constraint, TypeAbstraction abs, TypePath pathToTypeParamInConstraint,
|
||||
TypePath pathToTypeParamInSub
|
||||
) {
|
||||
satisfiesConstraintInline(term, constraint, abs, pathToTypeParamInConstraint,
|
||||
pathToTypeParamInSub, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the type tree at `term` satisfies the constraint `constraint`
|
||||
* through `abs` with the type `t` at `path`.
|
||||
* Holds if `term` satisfies the constraint `constraint` through `abs` with
|
||||
* the type `t` at `path`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate satisfiesConstraintTypeThrough(
|
||||
predicate satisfiesConstraintThrough(
|
||||
Term term, TypeAbstraction abs, Constraint constraint, TypePath path, Type t
|
||||
) {
|
||||
satisfiesConstraintTypeNonTypeParamInline(term, abs, constraint, path, t)
|
||||
satisfiesConstraintNonTypeParamInline(term, abs, constraint, path, t)
|
||||
or
|
||||
exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
|
||||
satisfiesConstraintTypeMentionThrough(term, constraint, abs, prefix0, pathToTypeParamInSub) and
|
||||
satisfiesConstraintThrough0(term, constraint, abs, prefix0, pathToTypeParamInSub) and
|
||||
getTypeAt(term, pathToTypeParamInSub.appendInverse(suffix)) = t and
|
||||
path = prefix0.append(suffix)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the type tree at `term` does _not_ satisfy the constraint `constraint`.
|
||||
* Holds if `term` does _not_ satisfy the constraint `constraint`.
|
||||
*
|
||||
* This is an approximation of `not satisfiesConstraintType(term, constraint, _, _)`,
|
||||
* but defined without a negative occurrence of `satisfiesConstraintType`.
|
||||
@@ -1495,7 +1521,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
TypeMention constraint
|
||||
) {
|
||||
target = a.getTarget(e) and
|
||||
typeParameterConstraintHasTypeParameter(target, apos, path, constraint, _, _)
|
||||
typeParameterHasConstraint(target, apos, _, path, constraint)
|
||||
}
|
||||
|
||||
private newtype TRelevantAccess =
|
||||
@@ -1556,13 +1582,40 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
SatisfiesTypeParameterConstraintInput>;
|
||||
|
||||
pragma[nomagic]
|
||||
predicate satisfiesConstraintType(
|
||||
predicate satisfiesConstraintAtTypeParameter(
|
||||
Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
|
||||
TypeMention constraint, TypePath pathToTypeParamInConstraint,
|
||||
TypePath pathToTypeParamInSub
|
||||
) {
|
||||
exists(RelevantAccess ra |
|
||||
ra = MkRelevantAccess(a, apos, e, prefix) and
|
||||
SatisfiesTypeParameterConstraint::satisfiesConstraintAtTypeParameter(ra, constraint,
|
||||
pathToTypeParamInConstraint, pathToTypeParamInSub) and
|
||||
constraint = ra.getConstraint(target)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate satisfiesConstraint(
|
||||
Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
|
||||
TypeMention constraint, TypePath path, Type t
|
||||
) {
|
||||
exists(RelevantAccess ra |
|
||||
ra = MkRelevantAccess(a, apos, e, prefix) and
|
||||
SatisfiesTypeParameterConstraint::satisfiesConstraintType(ra, constraint, path, t) and
|
||||
SatisfiesTypeParameterConstraint::satisfiesConstraint(ra, constraint, path, t) and
|
||||
constraint = ra.getConstraint(target)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate satisfiesConstraintThrough(
|
||||
Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
|
||||
TypeAbstraction abs, TypeMention constraint, TypePath path, Type t
|
||||
) {
|
||||
exists(RelevantAccess ra |
|
||||
ra = MkRelevantAccess(a, apos, e, prefix) and
|
||||
SatisfiesTypeParameterConstraint::satisfiesConstraintThrough(ra, abs, constraint, path,
|
||||
t) and
|
||||
constraint = ra.getConstraint(target)
|
||||
)
|
||||
}
|
||||
@@ -1707,7 +1760,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
not exists(getTypeArgument(a, target, tp, _)) and
|
||||
exists(TypeMention constraint, AccessPosition apos, TypePath pathToTp, TypePath pathToTp2 |
|
||||
typeParameterConstraintHasTypeParameter(target, apos, pathToTp2, constraint, pathToTp, tp) and
|
||||
AccessConstraint::satisfiesConstraintType(a, e, target, apos, pathToTp2, constraint,
|
||||
AccessConstraint::satisfiesConstraint(a, e, target, apos, pathToTp2, constraint,
|
||||
pathToTp.appendInverse(path), t)
|
||||
)
|
||||
}
|
||||
@@ -1785,6 +1838,82 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
|
||||
not result instanceof TypeParameter
|
||||
)
|
||||
)
|
||||
or
|
||||
exists(
|
||||
Declaration target, TypePath prefix, TypeMention constraint,
|
||||
TypePath pathToTypeParamInConstraint, TypePath pathToTypeParamInSub
|
||||
|
|
||||
AccessConstraint::satisfiesConstraintAtTypeParameter(a, e, target, apos, prefix,
|
||||
constraint, pathToTypeParamInConstraint, pathToTypeParamInSub)
|
||||
|
|
||||
exists(TypePath suffix |
|
||||
/*
|
||||
* Example:
|
||||
*
|
||||
* ```rust
|
||||
* struct MyThing<A> { ... }
|
||||
*
|
||||
* trait MyTrait<B> { ... }
|
||||
*
|
||||
* impl<T> MyTrait<T> for MyThing<T> { ... }
|
||||
*
|
||||
* fn foo<T: MyTrait<i32>>(x: T) { ... }
|
||||
*
|
||||
* let x = MyThing(Default::default());
|
||||
* foo(x);
|
||||
* ```
|
||||
*
|
||||
* At `term` = `foo(x)`, we have
|
||||
* - `constraint = MyTrait<i32>`,
|
||||
* - `pathToTypeParamInConstraint` = `"B"`,
|
||||
* - `pathToTypeParamInSub` = `"A"`,
|
||||
* - `prefix` = `suffix` = `""`, and
|
||||
* - `result` = `i32`.
|
||||
*
|
||||
* That is, it allows us to infer that the type of `x` is `MyThing<i32>`.
|
||||
*/
|
||||
|
||||
result = constraint.getTypeAt(pathToTypeParamInConstraint.appendInverse(suffix)) and
|
||||
not result instanceof TypeParameter and
|
||||
path = prefix.append(pathToTypeParamInSub.append(suffix))
|
||||
)
|
||||
or
|
||||
exists(TypeParameter tp, TypePath suffix, TypePath mid, TypePath pathToTp |
|
||||
/*
|
||||
* Example:
|
||||
*
|
||||
* ```rust
|
||||
* struct MyThing<A> { ... }
|
||||
*
|
||||
* trait MyTrait<B> { ... }
|
||||
*
|
||||
* impl<T> MyTrait<T> for MyThing<T> { ... }
|
||||
*
|
||||
* fn bar<T1, T2: MyTrait<T1>>(x: T1, y: T2) {}
|
||||
*
|
||||
* let x : i32 = ...;
|
||||
* let y = MyThing(Default::default());
|
||||
* bar(x, y);
|
||||
* ```
|
||||
*
|
||||
* At `term` = `bar(x, y)`, we have
|
||||
* - `constraint = MyTrait<T1>`,
|
||||
* - `pathToTypeParamInConstraint` = `"B"`,
|
||||
* - `pathToTypeParamInSub` = `"A"`,
|
||||
* - `prefix` = `suffix` = `mid` = `""`,
|
||||
* - `tp = T1`,
|
||||
* - `pathToTp` = `"B"`, and
|
||||
* - `result` = `i32`.
|
||||
*
|
||||
* That is, it allows us to infer that the type of `y` is `MyThing<i32>`.
|
||||
*/
|
||||
|
||||
typeMatch(a, e, target, suffix, result, tp) and
|
||||
typeParameterConstraintHasTypeParameter(target, apos, _, constraint, pathToTp, tp) and
|
||||
pathToTp = pathToTypeParamInConstraint.appendInverse(mid) and
|
||||
path = prefix.append(pathToTypeParamInSub.append(mid).append(suffix))
|
||||
)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
Reference in New Issue
Block a user