Skip to content

Rust: Make impl blocks only give rise to direct trait implementation #20723

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Rust: Make impl blocks only give rise to direct trait implementation #20723

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
978e42e
Rust: Make impl blocks only give rise to direct trait implementation
paldepind Oct 30, 2025
6184952
Rust: Accept changes to expected files
paldepind Nov 3, 2025
9a3892c
Rust: Improvements to docs from review comments
paldepind Nov 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 40 additions & 36 deletions rust/ql/lib/codeql/rust/internal/TypeInference.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,48 +179,52 @@ private module Input2 implements InputSig2 {
* inference module for more information.
*/
predicate conditionSatisfiesConstraint(
TypeAbstraction abs, TypeMention condition, TypeMention constraint
TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive
) {
// `impl` blocks implementing traits
transitive = false and
exists(Impl impl |
abs = impl and
condition = impl.getSelfTy() and
constraint = impl.getTrait()
)
or
// supertraits
exists(Trait trait |
abs = trait and
condition = trait and
constraint = trait.getATypeBound().getTypeRepr()
)
or
// trait bounds on type parameters
exists(TypeParam param |
abs = param.getATypeBound() and
condition = param and
constraint = abs.(TypeBound).getTypeRepr()
)
or
// the implicit `Self` type parameter satisfies the trait
exists(SelfTypeParameterMention self |
abs = self and
condition = self and
constraint = self.getTrait()
)
or
exists(ImplTraitTypeRepr impl |
abs = impl and
condition = impl and
constraint = impl.getTypeBoundList().getABound().getTypeRepr()
)
or
// a `dyn Trait` type implements `Trait`. See the comment on
// `DynTypeBoundListMention` for further details.
exists(DynTraitTypeRepr object |
abs = object and
condition = object.getTypeBoundList() and
constraint = object.getTrait()
transitive = true and
(
// supertraits
exists(Trait trait |
abs = trait and
condition = trait and
constraint = trait.getATypeBound().getTypeRepr()
)
or
// trait bounds on type parameters
exists(TypeParam param |
abs = param.getATypeBound() and
condition = param and
constraint = abs.(TypeBound).getTypeRepr()
)
or
// the implicit `Self` type parameter satisfies the trait
exists(SelfTypeParameterMention self |
abs = self and
condition = self and
constraint = self.getTrait()
)
or
exists(ImplTraitTypeRepr impl |
abs = impl and
condition = impl and
constraint = impl.getTypeBoundList().getABound().getTypeRepr()
)
or
// a `dyn Trait` type implements `Trait`. See the comment on
// `DynTypeBoundListMention` for further details.
exists(DynTraitTypeRepr object |
abs = object and
condition = object.getTypeBoundList() and
constraint = object.getTrait()
)
)
}
}
Expand Down Expand Up @@ -3362,10 +3366,10 @@ private module Debug {
}

predicate debugConditionSatisfiesConstraint(
TypeAbstraction abs, TypeMention condition, TypeMention constraint
TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive
) {
abs = getRelevantLocatable() and
Input2::conditionSatisfiesConstraint(abs, condition, constraint)
Input2::conditionSatisfiesConstraint(abs, condition, constraint, transitive)
}

predicate debugInferShorthandSelfType(ShorthandSelfParameterMention self, TypePath path, Type t) {
Expand Down
67 changes: 34 additions & 33 deletions rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,16 +72,24 @@ module FunctionPositionMatchingInput {
}

private newtype TAssocFunctionType =
/** An associated function `f` that should be specialized for `i` at `pos`. */
MkAssocFunctionType(Function f, ImplOrTraitItemNode i, FunctionPosition pos) {
f = i.getASuccessor(_) and exists(pos.getTypeMention(f))
/** An associated function `f` in `parent` should be specialized for `i` at `pos`. */
MkAssocFunctionType(
ImplOrTraitItemNode parent, Function f, ImplOrTraitItemNode i, FunctionPosition pos
) {
parent.getAnAssocItem() = f and
i.getASuccessor(_) = f and
// When `f` is not directly in `i`, the `parent` should be satisfiable
// through `i`. This ensures that `parent` is either a supertrait of `i` or
// `i` in an `impl` block implementing `parent`.
(parent = i or BaseTypes::rootTypesSatisfaction(_, TTrait(parent), i, _, _)) and
exists(pos.getTypeMention(f))
}

bindingset[condition, constraint, tp]
bindingset[abs, constraint, tp]
private Type getTraitConstraintTypeAt(
TypeMention condition, TypeMention constraint, TypeParameter tp, TypePath path
TypeAbstraction abs, TypeMention constraint, TypeParameter tp, TypePath path
) {
BaseTypes::conditionSatisfiesConstraintTypeAt(_, condition, constraint,
BaseTypes::conditionSatisfiesConstraintTypeAt(abs, _, constraint,
TypePath::singleton(tp).appendInverse(path), result)
}

Expand All @@ -91,28 +99,19 @@ private Type getTraitConstraintTypeAt(
*/
pragma[nomagic]
Type getAssocFunctionTypeAt(Function f, ImplOrTraitItemNode i, FunctionPosition pos, TypePath path) {
exists(MkAssocFunctionType(f, i, pos)) and
(
exists(ImplOrTraitItemNode parent | exists(MkAssocFunctionType(parent, f, i, pos)) |
// No specialization needed when the function is directly in the trait or
// impl block or the declared type is not a type parameter
(i.getAnAssocItem() = f or not result instanceof TypeParameter) and
(parent = i or not result instanceof TypeParameter) and
result = pos.getTypeMention(f).resolveTypeAt(path)
or
not i.getAnAssocItem() = f and
exists(TypePath prefix, TypePath suffix, TypeParameter tp |
exists(TypePath prefix, TypePath suffix, TypeParameter tp, TypeMention constraint |
BaseTypes::rootTypesSatisfaction(_, TTrait(parent), i, _, constraint) and
path = prefix.append(suffix) and
tp = pos.getTypeMention(f).resolveTypeAt(prefix)
|
tp = pos.getTypeMention(f).resolveTypeAt(prefix) and
if tp = TSelfTypeParameter(_)
then result = resolveImplOrTraitType(i, suffix)
else
exists(TraitItemNode trait, TypeMention condition, TypeMention constraint |
trait.getAnAssocItem() = f and
BaseTypes::rootTypesSatisfaction(_, TTrait(trait), _, condition, constraint) and
result = getTraitConstraintTypeAt(condition, constraint, tp, suffix)
|
condition = i.(Trait) or condition = i.(Impl).getSelfTy()
)
else result = getTraitConstraintTypeAt(i, constraint, tp, suffix)
)
)
}
Expand All @@ -134,31 +133,33 @@ Type getAssocFunctionTypeAt(Function f, ImplOrTraitItemNode i, FunctionPosition
* fn m3(self); // self3
* }
*
* impl T2 for X {
* impl T1 for X {
* fn m1(self) { ... } // self4
* }
*
* impl T2 for X {
* fn m3(self) { ... } // self5
* }
* ```
*
* param | `impl` or trait | type
* ------- | --------------- | ----
* `self1` | `trait T1` | `T1`
* `self1` | `trait T2` | `T2`
* `self2` | `trait T1` | `T1`
* `self2` | `trait T2` | `T2`
* `self2` | `impl T2 for X` | `X`
* `self3` | `trait T2` | `T2`
* `self4` | `impl T2 for X` | `X`
* `self5` | `impl T2 for X` | `X`
* f | `impl` or trait | pos | type
* ---- | --------------- | ------ | ----
* `m1` | `trait T1` | `self` | `T1`
* `m1` | `trait T2` | `self` | `T2`
* `m2` | `trait T1` | `self` | `T1`
* `m2` | `trait T2` | `self` | `T2`
* `m2` | `impl T1 for X` | `self` | `X`
* `m3` | `trait T2` | `self` | `T2`
* `m4` | `impl T2 for X` | `self` | `X`
* `m5` | `impl T2 for X` | `self` | `X`
Copy link

Copilot AI Nov 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The documentation table references functions m4 and m5 that don't exist in the example code. Based on the example, line 153 should reference m1 (from the impl T1 for X block) and line 154 should reference m3 (from the impl T2 for X block).

Suggested change
* `m4` | `impl T2 for X` | `self` | `X`
* `m5` | `impl T2 for X` | `self` | `X`
* `m1` | `impl T1 for X` | `self` | `X`
* `m3` | `impl T2 for X` | `self` | `X`

Copilot uses AI. Check for mistakes.
*/
class AssocFunctionType extends MkAssocFunctionType {
/**
* Holds if this function type applies to the function `f` at position `pos`,
* when viewed as a member of the `impl` or trait item `i`.
*/
predicate appliesTo(Function f, ImplOrTraitItemNode i, FunctionPosition pos) {
this = MkAssocFunctionType(f, i, pos)
this = MkAssocFunctionType(_, f, i, pos)
}

/**
Expand Down
2 changes: 0 additions & 2 deletions rust/ql/test/library-tests/dataflow/models/CONSISTENCY/PathResolutionConsistency.expected
View file
Open in desktop

This file was deleted.

2 changes: 0 additions & 2 deletions .../test/library-tests/dataflow/sources/stdin/CONSISTENCY/PathResolutionConsistency.expected
View file
Open in desktop

This file was deleted.

3 changes: 0 additions & 3 deletions rust/ql/test/library-tests/type-inference/CONSISTENCY/PathResolutionConsistency.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,7 @@ multipleCallTargets
| dereference.rs:184:17:184:30 | ... .foo() |
| dereference.rs:186:17:186:25 | S.bar(...) |
| dereference.rs:187:17:187:29 | S.bar(...) |
| main.rs:589:9:589:14 | S4.m() |
| main.rs:590:9:590:18 | ...::m(...) |
| main.rs:591:9:591:20 | ... .m() |
| main.rs:592:9:592:24 | ...::m(...) |
| main.rs:2524:13:2524:31 | ...::from(...) |
| main.rs:2525:13:2525:31 | ...::from(...) |
| main.rs:2526:13:2526:31 | ...::from(...) |
Expand Down
6 changes: 3 additions & 3 deletions rust/ql/test/library-tests/type-inference/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -586,10 +586,10 @@ mod impl_overlap {
println!("{:?}", w.m(x)); // $ target=S3<T>::m
println!("{:?}", S3::m(&w, x)); // $ target=S3<T>::m

S4.m(); // $ target=<S4_as_MyTrait1>::m $ SPURIOUS: target=MyTrait1::m
S4.m(); // $ target=<S4_as_MyTrait1>::m
S4::m(&S4); // $ target=<S4_as_MyTrait1>::m $ SPURIOUS: target=MyTrait1::m
S5(0i32).m(); // $ target=<S5<i32>_as_MyTrait1>::m $ SPURIOUS: target=MyTrait1::m
S5::m(&S5(0i32)); // $ target=<S5<i32>_as_MyTrait1>::m $ SPURIOUS: target=MyTrait1::m
S5(0i32).m(); // $ target=<S5<i32>_as_MyTrait1>::m
S5::m(&S5(0i32)); // $ target=<S5<i32>_as_MyTrait1>::m
Copy link
Contributor Author

@paldepind paldepind Nov 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure why the second test did not get fixed, especially since it looks a lot like the fourth test. I'm guessing something more might be needed here, as the AssocFunctionType looked fine when I eval'ed it.

S5(true).m(); // $ target=MyTrait1::m
S5::m(&S5(true)); // $ target=MyTrait1::m
}
Expand Down
3 changes: 0 additions & 3 deletions rust/ql/test/library-tests/type-inference/type-inference.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5719,7 +5719,6 @@ inferType
| main.rs:2566:42:2566:42 | 3 | | {EXTERNAL LOCATION} | i32 |
| main.rs:2567:9:2567:26 | for ... in ... { ... } | | file://:0:0:0:0 | () |
| main.rs:2567:13:2567:13 | u | | {EXTERNAL LOCATION} | u16 |
| main.rs:2567:13:2567:13 | u | | file://:0:0:0:0 | & |
| main.rs:2567:18:2567:23 | vals4a | | {EXTERNAL LOCATION} | Vec |
| main.rs:2567:18:2567:23 | vals4a | A | {EXTERNAL LOCATION} | Global |
| main.rs:2567:18:2567:23 | vals4a | T | {EXTERNAL LOCATION} | u16 |
Expand Down Expand Up @@ -5749,7 +5748,6 @@ inferType
| main.rs:2573:9:2573:25 | for ... in ... { ... } | | file://:0:0:0:0 | () |
| main.rs:2573:13:2573:13 | u | | {EXTERNAL LOCATION} | i32 |
| main.rs:2573:13:2573:13 | u | | {EXTERNAL LOCATION} | u32 |
| main.rs:2573:13:2573:13 | u | | file://:0:0:0:0 | & |
| main.rs:2573:18:2573:22 | vals5 | | {EXTERNAL LOCATION} | Vec |
| main.rs:2573:18:2573:22 | vals5 | A | {EXTERNAL LOCATION} | Global |
| main.rs:2573:18:2573:22 | vals5 | T | {EXTERNAL LOCATION} | i32 |
Expand Down Expand Up @@ -5790,7 +5788,6 @@ inferType
| main.rs:2579:20:2579:22 | 1u8 | | {EXTERNAL LOCATION} | u8 |
| main.rs:2580:9:2580:25 | for ... in ... { ... } | | file://:0:0:0:0 | () |
| main.rs:2580:13:2580:13 | u | | {EXTERNAL LOCATION} | u8 |
| main.rs:2580:13:2580:13 | u | | file://:0:0:0:0 | & |
| main.rs:2580:18:2580:22 | vals7 | | {EXTERNAL LOCATION} | Vec |
| main.rs:2580:18:2580:22 | vals7 | A | {EXTERNAL LOCATION} | Global |
| main.rs:2580:18:2580:22 | vals7 | T | {EXTERNAL LOCATION} | u8 |
Expand Down
12 changes: 7 additions & 5 deletions shared/typeinference/codeql/typeinference/internal/TypeInference.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -450,6 +450,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* free in `condition` and `constraint`,
* - and for every instantiation of the type parameters from `abs` the
* resulting `condition` satisifies the constraint given by `constraint`.
* - `transitive` corresponds to wether any further constraints satisifed
Copy link

Copilot AI Nov 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Corrected spelling of 'wether' to 'whether' and 'satisifed' to 'satisfied'.

Suggested change
* - `transitive` corresponds to wether any further constraints satisifed
* - `transitive` corresponds to whether any further constraints satisfied

Copilot uses AI. Check for mistakes.
* through `constraint` also applies to `condition`.
*
* Example in C#:
* ```csharp
Expand Down Expand Up @@ -487,7 +489,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* should be empty.
*/
predicate conditionSatisfiesConstraint(
TypeAbstraction abs, TypeMention condition, TypeMention constraint
TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive
);
}

Expand Down Expand Up @@ -754,13 +756,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
private predicate typeCondition(
Type type, TypeAbstraction abs, TypeMentionTypeTree condition
) {
conditionSatisfiesConstraint(abs, condition, _) and
conditionSatisfiesConstraint(abs, condition, _, _) and
type = resolveTypeMentionRoot(condition)
}

pragma[nomagic]
private predicate typeConstraint(Type type, TypeMentionTypeTree constraint) {
conditionSatisfiesConstraint(_, _, constraint) and
conditionSatisfiesConstraint(_, _, constraint, _) and
type = resolveTypeMentionRoot(constraint)
}

Expand All @@ -781,12 +783,12 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
TypeAbstraction abs, TypeMention condition, TypeMention constraint, TypePath path, Type t
) {
// base case
conditionSatisfiesConstraint(abs, condition, constraint) and
conditionSatisfiesConstraint(abs, condition, constraint, _) and
constraint.resolveTypeAt(path) = t
or
// recursive case
exists(TypeAbstraction midAbs, TypeMention midConstraint, TypeMention midCondition |
conditionSatisfiesConstraint(abs, condition, midConstraint) and
conditionSatisfiesConstraint(abs, condition, midConstraint, true) and
// NOTE: `midAbs` describe the free type variables in `midCondition`, hence
// we use that for instantiation check.
IsInstantiationOf<TypeMentionTypeTree, TypeMentionTypeTree, IsInstantiationOfInput>::isInstantiationOf(midConstraint,
Expand Down
Loading