Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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
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
77 changes: 39 additions & 38 deletions rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll
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 @@ -125,40 +124,42 @@ 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 T2 for X {
* fn m1(self) { ... } // self4
* impl T1 for X {
* fn m1(self) { ... } // X::m1
* }
*
* fn m3(self) { ... } // self5
* impl T2 for X {
* 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 {
/**
* 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

This file was deleted.

This file was deleted.

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
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

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
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
Original file line number Diff line number Diff line change
Expand Up @@ -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` 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