From 978e42e7a4532ffeff38ffddbdc49fa5d9137aef Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 30 Oct 2025 15:50:03 +0100 Subject: [PATCH 1/3] Rust: Make impl blocks only give rise to direct trait implementation --- .../codeql/rust/internal/TypeInference.qll | 76 ++++++++++--------- .../internal/typeinference/FunctionType.qll | 67 ++++++++-------- .../test/library-tests/type-inference/main.rs | 6 +- .../type-inference/type-inference.expected | 3 - .../typeinference/internal/TypeInference.qll | 12 +-- 5 files changed, 84 insertions(+), 80 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/TypeInference.qll index 905175803a24..041357f555c3 100644 --- a/rust/ql/lib/codeql/rust/internal/TypeInference.qll +++ b/rust/ql/lib/codeql/rust/internal/TypeInference.qll @@ -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() + ) ) } } @@ -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) { diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll index 10c007a9d724..b3050e83bff5 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll @@ -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) ) ) } @@ -134,23 +133,25 @@ 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` */ 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) } /** diff --git a/rust/ql/test/library-tests/type-inference/main.rs b/rust/ql/test/library-tests/type-inference/main.rs index d99d178ba8d0..7b158d956638 100644 --- a/rust/ql/test/library-tests/type-inference/main.rs +++ b/rust/ql/test/library-tests/type-inference/main.rs @@ -586,10 +586,10 @@ mod impl_overlap { println!("{:?}", w.m(x)); // $ target=S3::m println!("{:?}", S3::m(&w, x)); // $ target=S3::m - S4.m(); // $ target=::m $ SPURIOUS: target=MyTrait1::m + S4.m(); // $ target=::m S4::m(&S4); // $ target=::m $ SPURIOUS: target=MyTrait1::m - S5(0i32).m(); // $ target=_as_MyTrait1>::m $ SPURIOUS: target=MyTrait1::m - S5::m(&S5(0i32)); // $ target=_as_MyTrait1>::m $ SPURIOUS: target=MyTrait1::m + S5(0i32).m(); // $ target=_as_MyTrait1>::m + S5::m(&S5(0i32)); // $ target=_as_MyTrait1>::m S5(true).m(); // $ target=MyTrait1::m S5::m(&S5(true)); // $ target=MyTrait1::m } diff --git a/rust/ql/test/library-tests/type-inference/type-inference.expected b/rust/ql/test/library-tests/type-inference/type-inference.expected index d9b5e5782abf..6d9c2825867c 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -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 | @@ -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 | @@ -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 | diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index a827ef3cd792..260f78344edf 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -450,6 +450,8 @@ module Make1 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 + * through `constraint` also applies to `condition`. * * Example in C#: * ```csharp @@ -487,7 +489,7 @@ module Make1 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 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 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::isInstantiationOf(midConstraint, From 6184952f00e6d0dfafef39dc6dc68b7ecc89eeac Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Mon, 3 Nov 2025 09:55:34 +0100 Subject: [PATCH 2/3] Rust: Accept changes to expected files --- .../models/CONSISTENCY/PathResolutionConsistency.expected | 2 -- .../stdin/CONSISTENCY/PathResolutionConsistency.expected | 2 -- .../CONSISTENCY/PathResolutionConsistency.expected | 3 --- 3 files changed, 7 deletions(-) delete mode 100644 rust/ql/test/library-tests/dataflow/models/CONSISTENCY/PathResolutionConsistency.expected delete mode 100644 rust/ql/test/library-tests/dataflow/sources/stdin/CONSISTENCY/PathResolutionConsistency.expected diff --git a/rust/ql/test/library-tests/dataflow/models/CONSISTENCY/PathResolutionConsistency.expected b/rust/ql/test/library-tests/dataflow/models/CONSISTENCY/PathResolutionConsistency.expected deleted file mode 100644 index 7db157837813..000000000000 --- a/rust/ql/test/library-tests/dataflow/models/CONSISTENCY/PathResolutionConsistency.expected +++ /dev/null @@ -1,2 +0,0 @@ -multipleCallTargets -| main.rs:389:14:389:30 | ... .lt(...) | diff --git a/rust/ql/test/library-tests/dataflow/sources/stdin/CONSISTENCY/PathResolutionConsistency.expected b/rust/ql/test/library-tests/dataflow/sources/stdin/CONSISTENCY/PathResolutionConsistency.expected deleted file mode 100644 index 535b3f339b48..000000000000 --- a/rust/ql/test/library-tests/dataflow/sources/stdin/CONSISTENCY/PathResolutionConsistency.expected +++ /dev/null @@ -1,2 +0,0 @@ -multipleCallTargets -| test.rs:31:22:31:72 | ... .read_to_string(...) | diff --git a/rust/ql/test/library-tests/type-inference/CONSISTENCY/PathResolutionConsistency.expected b/rust/ql/test/library-tests/type-inference/CONSISTENCY/PathResolutionConsistency.expected index e1585e2e0d34..8e88714f2b48 100644 --- a/rust/ql/test/library-tests/type-inference/CONSISTENCY/PathResolutionConsistency.expected +++ b/rust/ql/test/library-tests/type-inference/CONSISTENCY/PathResolutionConsistency.expected @@ -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(...) | From 9a3892cfd324aa7f136bec1f0a861e9cf5f5d395 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Mon, 3 Nov 2025 10:21:19 +0100 Subject: [PATCH 3/3] Rust: Improvements to docs from review comments --- .../internal/typeinference/FunctionType.qll | 30 +++++++++---------- .../typeinference/internal/TypeInference.qll | 4 +-- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll index b3050e83bff5..d52c1e092a5d 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll @@ -124,34 +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) { ... } // self4 + * fn m1(self) { ... } // X::m1 * } * * impl T2 for X { - * fn m3(self) { ... } // self5 + * fn m3(self) { ... } // X::m3 * } * ``` * - * 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` + * 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 { /** diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 260f78344edf..9b9d60abb678 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -449,8 +449,8 @@ module Make1 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`. - * - `transitive` corresponds to wether any further constraints satisifed + * 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#: