Merge pull request #20723 from paldepind/rust/ti-inheritance

Rust: Make impl blocks only give rise to direct trait implementation
This commit is contained in:
Tom Hvitved
2025-11-17 13:36:05 +01:00
committed by GitHub
8 changed files with 90 additions and 93 deletions

View File

@@ -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()
)
)
}
}
@@ -3616,10 +3620,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) {

View File

@@ -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)
}
@@ -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)
)
)
}
@@ -125,32 +124,34 @@ Type getAssocFunctionTypeAt(Function f, ImplOrTraitItemNode i, FunctionPosition
*
* ```rust
* trait T1 {
* fn m1(self); // self1
* fn m1(self); // T1::m1
*
* fn m2(self) { ... } // self2
* fn m2(self) { ... } // T1::m2
* }
*
* trait T2 : T1 {
* fn m3(self); // self3
* fn m3(self); // T2::m3
* }
*
* impl T1 for X {
* fn m1(self) { ... } // X::m1
* }
*
* impl T2 for X {
* fn m1(self) { ... } // self4
*
* fn m3(self) { ... } // self5
* fn m3(self) { ... } // X::m3
* }
* ```
*
* 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
* -------- | --------------- | ------ | ----
* `T1::m1` | `trait T1` | `self` | `T1`
* `T1::m1` | `trait T2` | `self` | `T2`
* `T1::m2` | `trait T1` | `self` | `T1`
* `T1::m2` | `trait T2` | `self` | `T2`
* `T1::m2` | `impl T1 for X` | `self` | `X`
* `T2::m3` | `trait T2` | `self` | `T2`
* `X::m1` | `impl T1 for X` | `self` | `X`
* `X::m3` | `impl T2 for X` | `self` | `X`
*/
class AssocFunctionType extends MkAssocFunctionType {
/**
@@ -158,7 +159,7 @@ class AssocFunctionType extends MkAssocFunctionType {
* 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)
}
/**

View File

@@ -1,2 +0,0 @@
multipleCallTargets
| main.rs:389:14:389:30 | ... .lt(...) |

View File

@@ -1,2 +0,0 @@
multipleCallTargets
| test.rs:31:22:31:72 | ... .read_to_string(...) |

View File

@@ -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:2553:13:2553:31 | ...::from(...) |
| main.rs:2554:13:2554:31 | ...::from(...) |
| main.rs:2555:13:2555:31 | ...::from(...) |

View File

@@ -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
S5(true).m(); // $ target=MyTrait1::m
S5::m(&S5(true)); // $ target=MyTrait1::m
}

View File

@@ -5443,7 +5443,6 @@ inferType
| main.rs:2595:42:2595:42 | 3 | | {EXTERNAL LOCATION} | i32 |
| main.rs:2596:9:2596:26 | for ... in ... { ... } | | file://:0:0:0:0 | () |
| main.rs:2596:13:2596:13 | u | | {EXTERNAL LOCATION} | u16 |
| main.rs:2596:13:2596:13 | u | | file://:0:0:0:0 | & |
| main.rs:2596:18:2596:23 | vals4a | | {EXTERNAL LOCATION} | Vec |
| main.rs:2596:18:2596:23 | vals4a | A | {EXTERNAL LOCATION} | Global |
| main.rs:2596:18:2596:23 | vals4a | T | {EXTERNAL LOCATION} | u16 |
@@ -5473,7 +5472,6 @@ inferType
| main.rs:2602:9:2602:25 | for ... in ... { ... } | | file://:0:0:0:0 | () |
| main.rs:2602:13:2602:13 | u | | {EXTERNAL LOCATION} | i32 |
| main.rs:2602:13:2602:13 | u | | {EXTERNAL LOCATION} | u32 |
| main.rs:2602:13:2602:13 | u | | file://:0:0:0:0 | & |
| main.rs:2602:18:2602:22 | vals5 | | {EXTERNAL LOCATION} | Vec |
| main.rs:2602:18:2602:22 | vals5 | A | {EXTERNAL LOCATION} | Global |
| main.rs:2602:18:2602:22 | vals5 | T | {EXTERNAL LOCATION} | i32 |
@@ -5514,7 +5512,6 @@ inferType
| main.rs:2608:20:2608:22 | 1u8 | | {EXTERNAL LOCATION} | u8 |
| main.rs:2609:9:2609:25 | for ... in ... { ... } | | file://:0:0:0:0 | () |
| main.rs:2609:13:2609:13 | u | | {EXTERNAL LOCATION} | u8 |
| main.rs:2609:13:2609:13 | u | | file://:0:0:0:0 | & |
| main.rs:2609:18:2609:22 | vals7 | | {EXTERNAL LOCATION} | Vec |
| main.rs:2609:18:2609:22 | vals7 | A | {EXTERNAL LOCATION} | Global |
| main.rs:2609:18:2609:22 | vals7 | T | {EXTERNAL LOCATION} | u8 |

View File

@@ -449,7 +449,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* - `abs` is a type abstraction that introduces type variables that are
* free in `condition` and `constraint`,
* - and for every instantiation of the type parameters from `abs` the
* resulting `condition` satisifies the constraint given by `constraint`.
* resulting `condition` satisfies the constraint given by `constraint`.
* - `transitive` corresponds to whether any further constraints satisfied
* through `constraint` should also apply to `condition`.
*
* Example in C#:
* ```csharp
@@ -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
);
}
@@ -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)
}
@@ -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,