From 16613d173ff92ad99e621c1acd127de7f996d060 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Thu, 12 Mar 2026 10:39:22 +0100 Subject: [PATCH 1/3] Rust: Add type inference test --- .../type-inference/overloading.rs | 72 +++++++++ .../type-inference/type-inference.expected | 146 ++++++++++++++++++ 2 files changed, 218 insertions(+) diff --git a/rust/ql/test/library-tests/type-inference/overloading.rs b/rust/ql/test/library-tests/type-inference/overloading.rs index 94b5a8b69e41..e0f3dbf69540 100644 --- a/rust/ql/test/library-tests/type-inference/overloading.rs +++ b/rust/ql/test/library-tests/type-inference/overloading.rs @@ -449,3 +449,75 @@ mod inherent_before_trait { } } } + +mod trait_bound_impl_overlap { + trait MyTrait { + fn f(&self) -> T; + } + + trait MyTrait2 { + type Output; + + fn f(&self, x: T) -> Self::Output; + } + + struct S(T); + + impl MyTrait for S { + fn f(&self) -> i32 { + 0 + } + } + + impl MyTrait for S { + fn f(&self) -> i64 { + 0 + } + } + + impl MyTrait2> for S { + type Output = i32; + + fn f(&self, x: S) -> Self::Output { + 0 + } + } + + impl MyTrait2> for S { + type Output = >>::Output; + + fn f(&self, x: S) -> Self::Output { + 0 + } + } + + impl MyTrait2> for S { + type Output = i64; + + fn f(&self, x: S) -> Self::Output { + 0 + } + } + + fn call_f>(x: T2) -> T1 { + x.f() // $ target=f + } + + fn call_f2>(x: T1, y: T2) -> T2::Output { + y.f(x) // $ target=f + } + + fn test() { + let x = S(0); + let y = call_f(x); // $ target=call_f type=y:i32 $ SPURIOUS: type=y:i64 + let z: i32 = y; + + let x = S(0); + let y = call_f::(x); // $ target=call_f type=y:i32 + + let x = S(0); + let y = call_f2(S(0i32), x); // $ target=call_f2 type=y:i32 $ SPURIOUS: type=y:i64 + let x = S(0); + let y = call_f2(S(0i64), x); // $ target=call_f2 type=y:i64 $ SPURIOUS: type=y:i32 + } +} 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 feba4891a664..b71bcf643924 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -4079,6 +4079,51 @@ inferCertainType | overloading.rs:448:13:448:16 | self | | {EXTERNAL LOCATION} | & | | overloading.rs:448:13:448:16 | self | TRef | overloading.rs:405:5:405:19 | S | | overloading.rs:448:13:448:16 | self | TRef.T | {EXTERNAL LOCATION} | i64 | +| overloading.rs:455:14:455:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:455:14:455:18 | SelfParam | TRef | overloading.rs:454:5:456:5 | Self [trait MyTrait] | +| overloading.rs:461:14:461:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:461:14:461:18 | SelfParam | TRef | overloading.rs:458:5:462:5 | Self [trait MyTrait2] | +| overloading.rs:461:21:461:21 | x | | overloading.rs:458:20:458:27 | T | +| overloading.rs:467:14:467:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:467:14:467:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:467:14:467:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:467:28:469:9 | { ... } | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:473:14:473:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:473:14:473:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:473:14:473:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:473:28:475:9 | { ... } | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:481:14:481:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:481:14:481:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:481:14:481:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:481:21:481:21 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:481:21:481:21 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:481:48:483:9 | { ... } | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:489:14:489:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:489:14:489:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:489:14:489:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:489:21:489:21 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:489:21:489:21 | x | T | {EXTERNAL LOCATION} | i64 | +| overloading.rs:489:48:491:9 | { ... } | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:497:14:497:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:497:14:497:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:497:14:497:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:497:21:497:21 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:497:21:497:21 | x | T | {EXTERNAL LOCATION} | bool | +| overloading.rs:497:49:499:9 | { ... } | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:502:36:502:36 | x | | overloading.rs:502:19:502:33 | T2 | +| overloading.rs:502:49:504:5 | { ... } | | overloading.rs:502:15:502:16 | T1 | +| overloading.rs:503:9:503:9 | x | | overloading.rs:502:19:502:33 | T2 | +| overloading.rs:506:38:506:38 | x | | overloading.rs:506:16:506:17 | T1 | +| overloading.rs:506:45:506:45 | y | | overloading.rs:506:20:506:35 | T2 | +| overloading.rs:506:66:508:5 | { ... } | | overloading.rs:506:20:506:35 | T2::Output[MyTrait2] | +| overloading.rs:507:9:507:9 | y | | overloading.rs:506:20:506:35 | T2 | +| overloading.rs:507:13:507:13 | x | | overloading.rs:506:16:506:17 | T1 | +| overloading.rs:510:15:522:5 | { ... } | | {EXTERNAL LOCATION} | () | +| overloading.rs:513:13:513:13 | z | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:516:13:516:13 | y | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:516:17:516:35 | call_f::<...>(...) | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:519:27:519:30 | 0i32 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:521:27:521:30 | 0i64 | | {EXTERNAL LOCATION} | i64 | | pattern_matching.rs:13:26:133:1 | { ... } | | {EXTERNAL LOCATION} | Option | | pattern_matching.rs:13:26:133:1 | { ... } | T | {EXTERNAL LOCATION} | () | | pattern_matching.rs:15:5:18:5 | if ... {...} | | {EXTERNAL LOCATION} | () | @@ -12830,6 +12875,107 @@ inferType | overloading.rs:448:13:448:16 | self | TRef | overloading.rs:405:5:405:19 | S | | overloading.rs:448:13:448:16 | self | TRef.T | {EXTERNAL LOCATION} | i64 | | overloading.rs:448:13:448:22 | self.bar() | | {EXTERNAL LOCATION} | () | +| overloading.rs:455:14:455:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:455:14:455:18 | SelfParam | TRef | overloading.rs:454:5:456:5 | Self [trait MyTrait] | +| overloading.rs:461:14:461:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:461:14:461:18 | SelfParam | TRef | overloading.rs:458:5:462:5 | Self [trait MyTrait2] | +| overloading.rs:461:21:461:21 | x | | overloading.rs:458:20:458:27 | T | +| overloading.rs:467:14:467:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:467:14:467:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:467:14:467:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:467:28:469:9 | { ... } | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:468:13:468:13 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:473:14:473:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:473:14:473:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:473:14:473:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:473:28:475:9 | { ... } | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:474:13:474:13 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:474:13:474:13 | 0 | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:481:14:481:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:481:14:481:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:481:14:481:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:481:21:481:21 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:481:21:481:21 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:481:48:483:9 | { ... } | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:482:13:482:13 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:489:14:489:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:489:14:489:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:489:14:489:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:489:21:489:21 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:489:21:489:21 | x | T | {EXTERNAL LOCATION} | i64 | +| overloading.rs:489:48:491:9 | { ... } | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:490:13:490:13 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:490:13:490:13 | 0 | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:497:14:497:18 | SelfParam | | {EXTERNAL LOCATION} | & | +| overloading.rs:497:14:497:18 | SelfParam | TRef | overloading.rs:464:5:464:19 | S | +| overloading.rs:497:14:497:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:497:21:497:21 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:497:21:497:21 | x | T | {EXTERNAL LOCATION} | bool | +| overloading.rs:497:49:499:9 | { ... } | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:498:13:498:13 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:498:13:498:13 | 0 | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:502:36:502:36 | x | | overloading.rs:502:19:502:33 | T2 | +| overloading.rs:502:49:504:5 | { ... } | | overloading.rs:502:15:502:16 | T1 | +| overloading.rs:503:9:503:9 | x | | overloading.rs:502:19:502:33 | T2 | +| overloading.rs:503:9:503:13 | x.f() | | overloading.rs:502:15:502:16 | T1 | +| overloading.rs:506:38:506:38 | x | | overloading.rs:506:16:506:17 | T1 | +| overloading.rs:506:45:506:45 | y | | overloading.rs:506:20:506:35 | T2 | +| overloading.rs:506:66:508:5 | { ... } | | overloading.rs:506:20:506:35 | T2::Output[MyTrait2] | +| overloading.rs:507:9:507:9 | y | | overloading.rs:506:20:506:35 | T2 | +| overloading.rs:507:9:507:14 | y.f(...) | | overloading.rs:506:20:506:35 | T2::Output[MyTrait2] | +| overloading.rs:507:13:507:13 | x | | overloading.rs:506:16:506:17 | T1 | +| overloading.rs:510:15:522:5 | { ... } | | {EXTERNAL LOCATION} | () | +| overloading.rs:511:13:511:13 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:511:13:511:13 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:511:17:511:20 | S(...) | | overloading.rs:464:5:464:19 | S | +| overloading.rs:511:17:511:20 | S(...) | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:511:19:511:19 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:512:13:512:13 | y | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:512:13:512:13 | y | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:512:17:512:25 | call_f(...) | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:512:17:512:25 | call_f(...) | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:512:24:512:24 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:512:24:512:24 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:513:13:513:13 | z | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:513:22:513:22 | y | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:513:22:513:22 | y | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:515:13:515:13 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:515:13:515:13 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:515:17:515:20 | S(...) | | overloading.rs:464:5:464:19 | S | +| overloading.rs:515:17:515:20 | S(...) | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:515:19:515:19 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:516:13:516:13 | y | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:516:17:516:35 | call_f::<...>(...) | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:516:34:516:34 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:516:34:516:34 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:518:13:518:13 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:518:13:518:13 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:518:17:518:20 | S(...) | | overloading.rs:464:5:464:19 | S | +| overloading.rs:518:17:518:20 | S(...) | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:518:19:518:19 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:519:13:519:13 | y | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:519:13:519:13 | y | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:519:17:519:35 | call_f2(...) | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:519:17:519:35 | call_f2(...) | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:519:25:519:31 | S(...) | | overloading.rs:464:5:464:19 | S | +| overloading.rs:519:25:519:31 | S(...) | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:519:27:519:30 | 0i32 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:519:34:519:34 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:519:34:519:34 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:520:13:520:13 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:520:13:520:13 | x | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:520:17:520:20 | S(...) | | overloading.rs:464:5:464:19 | S | +| overloading.rs:520:17:520:20 | S(...) | T | {EXTERNAL LOCATION} | i32 | +| overloading.rs:520:19:520:19 | 0 | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:521:13:521:13 | y | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:521:13:521:13 | y | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:521:17:521:35 | call_f2(...) | | {EXTERNAL LOCATION} | i32 | +| overloading.rs:521:17:521:35 | call_f2(...) | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:521:25:521:31 | S(...) | | overloading.rs:464:5:464:19 | S | +| overloading.rs:521:25:521:31 | S(...) | T | {EXTERNAL LOCATION} | i64 | +| overloading.rs:521:27:521:30 | 0i64 | | {EXTERNAL LOCATION} | i64 | +| overloading.rs:521:34:521:34 | x | | overloading.rs:464:5:464:19 | S | +| overloading.rs:521:34:521:34 | x | T | {EXTERNAL LOCATION} | i32 | | pattern_matching.rs:13:26:133:1 | { ... } | | {EXTERNAL LOCATION} | Option | | pattern_matching.rs:13:26:133:1 | { ... } | T | {EXTERNAL LOCATION} | () | | pattern_matching.rs:14:9:14:13 | value | | {EXTERNAL LOCATION} | Option | From ca0fe444f7bf5882fd28601f42b8703c7b80ba75 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Thu, 12 Mar 2026 11:50:46 +0100 Subject: [PATCH 2/3] Rust: Only infer types from trait bounds when their implementation is unambiguous --- .../typeinference/BlanketImplementation.qll | 4 +- .../typeinference/FunctionOverloading.qll | 17 +- .../rust/internal/typeinference/Type.qll | 12 +- .../internal/typeinference/TypeInference.qll | 59 +++-- .../internal/typeinference/TypeMention.qll | 65 ++--- .../type-inference/overloading.rs | 6 +- .../type-inference/type-inference.expected | 27 +-- .../typeinference/internal/TypeInference.qll | 222 +++++++++++++----- 8 files changed, 257 insertions(+), 155 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll index db1402280d4d..97dbf2d8f3a9 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll @@ -103,7 +103,7 @@ module SatisfiesBlanketConstraint< } private module SatisfiesBlanketConstraintInput implements - SatisfiesConstraintInputSig + SatisfiesTypeInputSig { pragma[nomagic] additional predicate relevantConstraint( @@ -123,7 +123,7 @@ module SatisfiesBlanketConstraint< } private module SatisfiesBlanketConstraint = - SatisfiesConstraint; + SatisfiesType; /** * Holds if the argument type `at` satisfies the first non-trivial blanket diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll index 6e4cc6e2c2e8..f2e17d249704 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll @@ -14,13 +14,13 @@ private import TypeInference private import FunctionType pragma[nomagic] -private Type resolveNonTypeParameterTypeAt(TypeMention tm, TypePath path) { +private Type resolveNonTypeParameterTypeAt(PreTypeMention tm, TypePath path) { result = tm.getTypeAt(path) and not result instanceof TypeParameter } bindingset[t1, t2] -private predicate typeMentionEqual(TypeMention t1, TypeMention t2) { +private predicate typeMentionEqual(PreTypeMention t1, PreTypeMention t2) { forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type | resolveNonTypeParameterTypeAt(t2, path) = type ) @@ -28,7 +28,7 @@ private predicate typeMentionEqual(TypeMention t1, TypeMention t2) { pragma[nomagic] private predicate implSiblingCandidate( - Impl impl, TraitItemNode trait, Type rootType, TypeMention selfTy + Impl impl, TraitItemNode trait, Type rootType, PreTypeMention selfTy ) { trait = impl.(ImplItemNode).resolveTraitTy() and selfTy = impl.getSelfTy() and @@ -52,7 +52,7 @@ pragma[inline] private predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) { impl1 != impl2 and ( - exists(Type rootType, TypeMention selfTy1, TypeMention selfTy2 | + exists(Type rootType, PreTypeMention selfTy1, PreTypeMention selfTy2 | implSiblingCandidate(impl1, trait, rootType, selfTy1) and implSiblingCandidate(impl2, trait, rootType, selfTy2) and // In principle the second conjunct below should be superflous, but we still @@ -76,6 +76,15 @@ private predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) { pragma[nomagic] private predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) } +pragma[nomagic] +predicate implHasAmbigousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) { + exists(ImplItemNode impl2 | + implSiblings(trait, impl, impl2) and + resolveNonTypeParameterTypeAt(impl.getTraitPath(), path) != + resolveNonTypeParameterTypeAt(impl2.getTraitPath(), path) + ) +} + /** * Holds if `f` is a function declared inside `trait`, and the type of `f` at * `pos` and `path` is `traitTp`, which is a type parameter of `trait`. diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/Type.qll b/rust/ql/lib/codeql/rust/internal/typeinference/Type.qll index 05b6557522af..9ae79f2d58c9 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/Type.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/Type.qll @@ -439,11 +439,11 @@ class TypeParamTypeParameter extends TypeParameter, TTypeParamTypeParameter { */ class AssociatedTypeTypeParameter extends TypeParameter, TAssociatedTypeTypeParameter { private Trait trait; - private TypeAlias typeAlias; + private AssocType typeAlias; AssociatedTypeTypeParameter() { this = TAssociatedTypeTypeParameter(trait, typeAlias) } - TypeAlias getTypeAlias() { result = typeAlias } + AssocType getTypeAlias() { result = typeAlias } /** Gets the trait that contains this associated type declaration. */ TraitItemNode getTrait() { result = trait } @@ -457,7 +457,13 @@ class AssociatedTypeTypeParameter extends TypeParameter, TAssociatedTypeTypePara override ItemNode getDeclaringItem() { result = trait } override string toString() { - result = typeAlias.getName().getText() + "[" + trait.getName().toString() + "]" + exists(string fromString, TraitItemNode trait2 | + result = typeAlias.getName().getText() + "[" + trait.getName() + fromString + "]" and + trait2 = typeAlias.getTrait() and + if trait = trait2 + then fromString = "" + else fromString = " (inherited from " + trait2.getName() + ")" + ) } override Location getLocation() { result = typeAlias.getLocation() } diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll index c194531a0781..798ee76c7be9 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll @@ -41,6 +41,12 @@ private module Input implements InputSig1, InputSig2 { class TypeAbstraction = TA::TypeAbstraction; + predicate typeAbstractionHasAmbigousConstraintAt( + TypeAbstraction abs, Type constraint, TypePath path + ) { + FunctionOverloading::implHasAmbigousSiblingAt(abs, constraint.(TraitType).getTrait(), path) + } + class TypeArgumentPosition extends TTypeArgumentPosition { int asMethodTypeArgumentPosition() { this = TMethodTypeArgumentPosition(result) } @@ -127,17 +133,15 @@ private module Input implements InputSig1, InputSig2 { PreTypeMention getABaseTypeMention(Type t) { none() } - Type getATypeParameterConstraint(TypeParameter tp, TypePath path) { - exists(TypeMention tm | result = tm.getTypeAt(path) | - tm = tp.(TypeParamTypeParameter).getTypeParam().getATypeBound().getTypeRepr() or - tm = tp.(SelfTypeParameter).getTrait() or - tm = - tp.(ImplTraitTypeTypeParameter) - .getImplTraitTypeRepr() - .getTypeBoundList() - .getABound() - .getTypeRepr() - ) + PreTypeMention getATypeParameterConstraint(TypeParameter tp) { + result = tp.(TypeParamTypeParameter).getTypeParam().getATypeBound().getTypeRepr() or + result = tp.(SelfTypeParameter).getTrait() or + result = + tp.(ImplTraitTypeTypeParameter) + .getImplTraitTypeRepr() + .getTypeBoundList() + .getABound() + .getTypeRepr() } /** @@ -1170,7 +1174,7 @@ private module ContextTyping { or exists(TypeParameter mid | assocFunctionMentionsTypeParameterAtNonRetPos(i, f, mid) and - tp = getATypeParameterConstraint(mid, _) + tp = getATypeParameterConstraint(mid).getTypeAt(_) ) } @@ -2544,8 +2548,7 @@ private module AssocFunctionResolution { Location getLocation() { result = afc.getLocation() } } - private module CallSatisfiesDerefConstraintInput implements - SatisfiesConstraintInputSig + private module CallSatisfiesDerefConstraintInput implements SatisfiesTypeInputSig { pragma[nomagic] predicate relevantConstraint(CallDerefCand mc, Type constraint) { @@ -2555,7 +2558,7 @@ private module AssocFunctionResolution { } private module CallSatisfiesDerefConstraint = - SatisfiesConstraint; + SatisfiesType; pragma[nomagic] private AssociatedTypeTypeParameter getDerefTargetTypeParameter() { @@ -3586,7 +3589,7 @@ final private class AwaitTarget extends Expr { Type getTypeAt(TypePath path) { result = inferType(this, path) } } -private module AwaitSatisfiesConstraintInput implements SatisfiesConstraintInputSig { +private module AwaitSatisfiesTypeInput implements SatisfiesTypeInputSig { pragma[nomagic] predicate relevantConstraint(AwaitTarget term, Type constraint) { exists(term) and @@ -3594,13 +3597,12 @@ private module AwaitSatisfiesConstraintInput implements SatisfiesConstraintInput } } -private module AwaitSatisfiesConstraint = - SatisfiesConstraint; +private module AwaitSatisfiesType = SatisfiesType; pragma[nomagic] private Type inferAwaitExprType(AstNode n, TypePath path) { exists(TypePath exprPath | - AwaitSatisfiesConstraint::satisfiesConstraintType(n.(AwaitExpr).getExpr(), _, exprPath, result) and + AwaitSatisfiesType::satisfiesConstraintType(n.(AwaitExpr).getExpr(), _, exprPath, result) and exprPath.isCons(getFutureOutputTypeParameter(), path) ) } @@ -3779,9 +3781,7 @@ final private class ForIterableExpr extends Expr { Type getTypeAt(TypePath path) { result = inferType(this, path) } } -private module ForIterableSatisfiesConstraintInput implements - SatisfiesConstraintInputSig -{ +private module ForIterableSatisfiesTypeInput implements SatisfiesTypeInputSig { predicate relevantConstraint(ForIterableExpr term, Type constraint) { exists(term) and exists(Trait t | t = constraint.(TraitType).getTrait() | @@ -3802,15 +3802,15 @@ private AssociatedTypeTypeParameter getIntoIteratorItemTypeParameter() { result = getAssociatedTypeTypeParameter(any(IntoIteratorTrait t).getItemType()) } -private module ForIterableSatisfiesConstraint = - SatisfiesConstraint; +private module ForIterableSatisfiesType = + SatisfiesType; pragma[nomagic] private Type inferForLoopExprType(AstNode n, TypePath path) { // type of iterable -> type of pattern (loop variable) exists(ForExpr fe, TypePath exprPath, AssociatedTypeTypeParameter tp | n = fe.getPat() and - ForIterableSatisfiesConstraint::satisfiesConstraintType(fe.getIterable(), _, exprPath, result) and + ForIterableSatisfiesType::satisfiesConstraintType(fe.getIterable(), _, exprPath, result) and exprPath.isCons(tp, path) | tp = getIntoIteratorItemTypeParameter() @@ -3836,8 +3836,7 @@ final private class InvokedClosureExpr extends Expr { CallExpr getCall() { result = call } } -private module InvokedClosureSatisfiesConstraintInput implements - SatisfiesConstraintInputSig +private module InvokedClosureSatisfiesTypeInput implements SatisfiesTypeInputSig { predicate relevantConstraint(InvokedClosureExpr term, Type constraint) { exists(term) and @@ -3845,12 +3844,12 @@ private module InvokedClosureSatisfiesConstraintInput implements } } -private module InvokedClosureSatisfiesConstraint = - SatisfiesConstraint; +private module InvokedClosureSatisfiesType = + SatisfiesType; /** Gets the type of `ce` when viewed as an implementation of `FnOnce`. */ private Type invokedClosureFnTypeAt(InvokedClosureExpr ce, TypePath path) { - InvokedClosureSatisfiesConstraint::satisfiesConstraintType(ce, _, path, result) + InvokedClosureSatisfiesType::satisfiesConstraintType(ce, _, path, result) } /** diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll index dcb3fc0b0f49..e6c01b7659c1 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll @@ -205,6 +205,13 @@ private module MkTypeMention::...` + exists(PathTypeRepr typeRepr, PathTypeRepr traitRepr | + pathTypeAsTraitAssoc(_, typeRepr, traitRepr, _, _) and + this = traitRepr.getPath() and + result = typeRepr.getPath() + ) } pragma[nomagic] @@ -696,6 +703,16 @@ private module PreTypeMention = MkTypeMention; class PreTypeMention = PreTypeMention::TypeMention; +private class TraitOrTmTrait extends AstNode { + Type getTypeAt(TypePath path) { + pathTypeAsTraitAssoc(_, _, this, _, _) and + result = this.(PreTypeMention).getTypeAt(path) + or + result = TTrait(this) and + path.isEmpty() + } +} + /** * Holds if `path` accesses an associated type `alias` from `trait` on a * concrete type given by `tm`. @@ -705,7 +722,7 @@ class PreTypeMention = PreTypeMention::TypeMention; * when `path` is of the form `Self::AssocType`. */ private predicate pathConcreteTypeAssocType( - Path path, PreTypeMention tm, TraitItemNode trait, AstNode implOrTmTrait, TypeAlias alias + Path path, PreTypeMention tm, TraitItemNode trait, TraitOrTmTrait traitOrTmTrait, TypeAlias alias ) { exists(Path qualifier | qualifier = path.getQualifier() and @@ -714,30 +731,32 @@ private predicate pathConcreteTypeAssocType( // path of the form `::AssocType` // ^^^ tm ^^^^^^^^^ name exists(string name | - pathTypeAsTraitAssoc(path, tm, implOrTmTrait, trait, name) and + pathTypeAsTraitAssoc(path, tm, traitOrTmTrait, trait, name) and getTraitAssocType(trait, name) = alias ) or // path of the form `Self::AssocType` within an `impl` block // tm ^^^^ ^^^^^^^^^ name - implOrTmTrait = - any(ImplItemNode impl | - alias = resolvePath(path) and - qualifier = impl.getASelfPath() and - tm = impl.(Impl).getSelfTy() and - trait.getAnAssocItem() = alias - ) + exists(ImplItemNode impl | + alias = resolvePath(path) and + qualifier = impl.getASelfPath() and + tm = impl.(Impl).getSelfTy() and + trait.getAnAssocItem() = alias and + traitOrTmTrait = trait + ) ) } -private module PathSatisfiesConstraintInput implements SatisfiesConstraintInputSig { - predicate relevantConstraint(PreTypeMention tm, Type constraint) { - pathConcreteTypeAssocType(_, tm, constraint.(TraitType).getTrait(), _, _) +private module PathSatisfiesConstraintInput implements + SatisfiesConstraintInputSig +{ + predicate relevantConstraint(PreTypeMention tm, TraitOrTmTrait constraint) { + pathConcreteTypeAssocType(_, tm, _, constraint, _) } } private module PathSatisfiesConstraint = - SatisfiesConstraint; + SatisfiesConstraint; /** * Gets the type of `path` at `typePath` when `path` accesses an associated type @@ -745,26 +764,12 @@ private module PathSatisfiesConstraint = */ private Type getPathConcreteAssocTypeAt(Path path, TypePath typePath) { exists( - PreTypeMention tm, ImplItemNode impl, TraitItemNode trait, TraitType t, AstNode implOrTmTrait, + PreTypeMention tm, ImplItemNode impl, TraitItemNode trait, TraitOrTmTrait traitOrTmTrait, TypeAlias alias, TypePath path0 | - pathConcreteTypeAssocType(path, tm, trait, implOrTmTrait, alias) and - t = TTrait(trait) and - PathSatisfiesConstraint::satisfiesConstraintTypeThrough(tm, impl, t, path0, result) and + pathConcreteTypeAssocType(path, tm, trait, traitOrTmTrait, alias) and + PathSatisfiesConstraint::satisfiesConstraintTypeThrough(tm, impl, traitOrTmTrait, path0, result) and path0.isCons(TAssociatedTypeTypeParameter(trait, alias), typePath) - | - implOrTmTrait instanceof Impl - or - // When `path` is of the form `::AssocType` we need to check - // that `impl` is not more specific than the mentioned trait - implOrTmTrait = - any(PreTypeMention tmTrait | - not exists(TypePath path1, Type t1 | - t1 = impl.getTraitPath().(PreTypeMention).getTypeAt(path1) and - not t1 instanceof TypeParameter and - t1 != tmTrait.getTypeAt(path1) - ) - ) ) } diff --git a/rust/ql/test/library-tests/type-inference/overloading.rs b/rust/ql/test/library-tests/type-inference/overloading.rs index e0f3dbf69540..854338fcaf4c 100644 --- a/rust/ql/test/library-tests/type-inference/overloading.rs +++ b/rust/ql/test/library-tests/type-inference/overloading.rs @@ -509,15 +509,15 @@ mod trait_bound_impl_overlap { fn test() { let x = S(0); - let y = call_f(x); // $ target=call_f type=y:i32 $ SPURIOUS: type=y:i64 + let y = call_f(x); // $ target=call_f type=y:i32 let z: i32 = y; let x = S(0); let y = call_f::(x); // $ target=call_f type=y:i32 let x = S(0); - let y = call_f2(S(0i32), x); // $ target=call_f2 type=y:i32 $ SPURIOUS: type=y:i64 + let y = call_f2(S(0i32), x); // $ target=call_f2 $ MISSING: type=y:i32 let x = S(0); - let y = call_f2(S(0i64), x); // $ target=call_f2 type=y:i64 $ SPURIOUS: type=y:i32 + let y = call_f2(S(0i64), x); // $ target=call_f2 $ MISSING: type=y:i64 } } 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 b71bcf643924..9d917c6143fa 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -209,15 +209,15 @@ inferCertainType | associated_types.rs:454:24:454:28 | SelfParam | TRef | associated_types.rs:452:5:455:5 | Self [trait Subtrait] | | associated_types.rs:463:23:463:27 | SelfParam | | {EXTERNAL LOCATION} | & | | associated_types.rs:463:23:463:27 | SelfParam | TRef | associated_types.rs:457:5:467:5 | Self [trait Subtrait2] | -| associated_types.rs:463:30:463:31 | c1 | | associated_types.rs:20:5:20:16 | Output[Subtrait2] | -| associated_types.rs:463:48:463:49 | c2 | | associated_types.rs:20:5:20:16 | Output[Subtrait2] | +| associated_types.rs:463:30:463:31 | c1 | | associated_types.rs:20:5:20:16 | Output[Subtrait2 (inherited from GetSet)] | +| associated_types.rs:463:48:463:49 | c2 | | associated_types.rs:20:5:20:16 | Output[Subtrait2 (inherited from GetSet)] | | associated_types.rs:463:66:466:9 | { ... } | | {EXTERNAL LOCATION} | () | | associated_types.rs:464:13:464:16 | self | | {EXTERNAL LOCATION} | & | | associated_types.rs:464:13:464:16 | self | TRef | associated_types.rs:457:5:467:5 | Self [trait Subtrait2] | -| associated_types.rs:464:22:464:23 | c1 | | associated_types.rs:20:5:20:16 | Output[Subtrait2] | +| associated_types.rs:464:22:464:23 | c1 | | associated_types.rs:20:5:20:16 | Output[Subtrait2 (inherited from GetSet)] | | associated_types.rs:465:13:465:16 | self | | {EXTERNAL LOCATION} | & | | associated_types.rs:465:13:465:16 | self | TRef | associated_types.rs:457:5:467:5 | Self [trait Subtrait2] | -| associated_types.rs:465:22:465:23 | c2 | | associated_types.rs:20:5:20:16 | Output[Subtrait2] | +| associated_types.rs:465:22:465:23 | c2 | | associated_types.rs:20:5:20:16 | Output[Subtrait2 (inherited from GetSet)] | | associated_types.rs:474:16:474:20 | SelfParam | | {EXTERNAL LOCATION} | & | | associated_types.rs:474:16:474:20 | SelfParam | TRef | associated_types.rs:469:5:469:24 | MyType | | associated_types.rs:474:16:474:20 | SelfParam | TRef.T | associated_types.rs:471:10:471:16 | T | @@ -5441,17 +5441,17 @@ inferType | associated_types.rs:454:24:454:28 | SelfParam | TRef | associated_types.rs:452:5:455:5 | Self [trait Subtrait] | | associated_types.rs:463:23:463:27 | SelfParam | | {EXTERNAL LOCATION} | & | | associated_types.rs:463:23:463:27 | SelfParam | TRef | associated_types.rs:457:5:467:5 | Self [trait Subtrait2] | -| associated_types.rs:463:30:463:31 | c1 | | associated_types.rs:20:5:20:16 | Output[Subtrait2] | -| associated_types.rs:463:48:463:49 | c2 | | associated_types.rs:20:5:20:16 | Output[Subtrait2] | +| associated_types.rs:463:30:463:31 | c1 | | associated_types.rs:20:5:20:16 | Output[Subtrait2 (inherited from GetSet)] | +| associated_types.rs:463:48:463:49 | c2 | | associated_types.rs:20:5:20:16 | Output[Subtrait2 (inherited from GetSet)] | | associated_types.rs:463:66:466:9 | { ... } | | {EXTERNAL LOCATION} | () | | associated_types.rs:464:13:464:16 | self | | {EXTERNAL LOCATION} | & | | associated_types.rs:464:13:464:16 | self | TRef | associated_types.rs:457:5:467:5 | Self [trait Subtrait2] | | associated_types.rs:464:13:464:24 | self.set(...) | | {EXTERNAL LOCATION} | () | -| associated_types.rs:464:22:464:23 | c1 | | associated_types.rs:20:5:20:16 | Output[Subtrait2] | +| associated_types.rs:464:22:464:23 | c1 | | associated_types.rs:20:5:20:16 | Output[Subtrait2 (inherited from GetSet)] | | associated_types.rs:465:13:465:16 | self | | {EXTERNAL LOCATION} | & | | associated_types.rs:465:13:465:16 | self | TRef | associated_types.rs:457:5:467:5 | Self [trait Subtrait2] | | associated_types.rs:465:13:465:24 | self.set(...) | | {EXTERNAL LOCATION} | () | -| associated_types.rs:465:22:465:23 | c2 | | associated_types.rs:20:5:20:16 | Output[Subtrait2] | +| associated_types.rs:465:22:465:23 | c2 | | associated_types.rs:20:5:20:16 | Output[Subtrait2 (inherited from GetSet)] | | associated_types.rs:474:16:474:20 | SelfParam | | {EXTERNAL LOCATION} | & | | associated_types.rs:474:16:474:20 | SelfParam | TRef | associated_types.rs:469:5:469:24 | MyType | | associated_types.rs:474:16:474:20 | SelfParam | TRef.T | associated_types.rs:471:10:471:16 | T | @@ -12931,14 +12931,11 @@ inferType | overloading.rs:511:17:511:20 | S(...) | T | {EXTERNAL LOCATION} | i32 | | overloading.rs:511:19:511:19 | 0 | | {EXTERNAL LOCATION} | i32 | | overloading.rs:512:13:512:13 | y | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:512:13:512:13 | y | | {EXTERNAL LOCATION} | i64 | | overloading.rs:512:17:512:25 | call_f(...) | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:512:17:512:25 | call_f(...) | | {EXTERNAL LOCATION} | i64 | | overloading.rs:512:24:512:24 | x | | overloading.rs:464:5:464:19 | S | | overloading.rs:512:24:512:24 | x | T | {EXTERNAL LOCATION} | i32 | | overloading.rs:513:13:513:13 | z | | {EXTERNAL LOCATION} | i32 | | overloading.rs:513:22:513:22 | y | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:513:22:513:22 | y | | {EXTERNAL LOCATION} | i64 | | overloading.rs:515:13:515:13 | x | | overloading.rs:464:5:464:19 | S | | overloading.rs:515:13:515:13 | x | T | {EXTERNAL LOCATION} | i32 | | overloading.rs:515:17:515:20 | S(...) | | overloading.rs:464:5:464:19 | S | @@ -12953,10 +12950,6 @@ inferType | overloading.rs:518:17:518:20 | S(...) | | overloading.rs:464:5:464:19 | S | | overloading.rs:518:17:518:20 | S(...) | T | {EXTERNAL LOCATION} | i32 | | overloading.rs:518:19:518:19 | 0 | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:519:13:519:13 | y | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:519:13:519:13 | y | | {EXTERNAL LOCATION} | i64 | -| overloading.rs:519:17:519:35 | call_f2(...) | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:519:17:519:35 | call_f2(...) | | {EXTERNAL LOCATION} | i64 | | overloading.rs:519:25:519:31 | S(...) | | overloading.rs:464:5:464:19 | S | | overloading.rs:519:25:519:31 | S(...) | T | {EXTERNAL LOCATION} | i32 | | overloading.rs:519:27:519:30 | 0i32 | | {EXTERNAL LOCATION} | i32 | @@ -12967,10 +12960,6 @@ inferType | overloading.rs:520:17:520:20 | S(...) | | overloading.rs:464:5:464:19 | S | | overloading.rs:520:17:520:20 | S(...) | T | {EXTERNAL LOCATION} | i32 | | overloading.rs:520:19:520:19 | 0 | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:521:13:521:13 | y | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:521:13:521:13 | y | | {EXTERNAL LOCATION} | i64 | -| overloading.rs:521:17:521:35 | call_f2(...) | | {EXTERNAL LOCATION} | i32 | -| overloading.rs:521:17:521:35 | call_f2(...) | | {EXTERNAL LOCATION} | i64 | | overloading.rs:521:25:521:31 | S(...) | | overloading.rs:464:5:464:19 | S | | overloading.rs:521:25:521:31 | S(...) | T | {EXTERNAL LOCATION} | i64 | | overloading.rs:521:27:521:30 | 0i64 | | {EXTERNAL LOCATION} | i64 | diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index c33c49e7a168..701ed1e0441f 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -336,7 +336,7 @@ module Make1 Input1> { * ``` * the type parameter `T` has the constraint `IComparable`. */ - Type getATypeParameterConstraint(TypeParameter tp, TypePath path); + TypeMention getATypeParameterConstraint(TypeParameter tp); /** * Holds if @@ -385,6 +385,35 @@ module Make1 Input1> { predicate conditionSatisfiesConstraint( TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive ); + + /** + * Holds if the constraint belonging to `abs` with root type `constraint` is + * ambigous at `path`, meaning that there is _some_ other abstraction `abs2` + * with a structurally identical condition and root constraint type `constraint`, + * and where the constraints differ at `path`. + * + * Example: + * + * ```rust + * trait Trait { } + * + * impl Trait for Foo { ... } + * // ^^^ `abs` + * // ^^^^^ `constraint` + * // ^^^^^^ `condition` + * + * impl Trait for Foo { } + * // ^^^ `abs2` + * // ^^^^^ `constraint` + * // ^^^^^^ `condition2` + * ``` + * + * In the above, `abs` and `abs2` have structurally identical conditions, + * `condition` and `condition2`, and they differ at the path `"TTrait"`. + */ + predicate typeAbstractionHasAmbigousConstraintAt( + TypeAbstraction abs, Type constraint, TypePath path + ); } module Make2 Input2> { @@ -820,38 +849,43 @@ module Make1 Input1> { private import BaseTypes - signature module SatisfiesConstraintInputSig { + /** Provides the input to `SatisfiesConstraint`. */ + signature module SatisfiesConstraintInputSig { /** Holds if it is relevant to know if `term` satisfies `constraint`. */ - predicate relevantConstraint(HasTypeTree term, Type constraint); + predicate relevantConstraint(Term term, Constraint constraint); } module SatisfiesConstraint< - HasTypeTreeSig HasTypeTree, SatisfiesConstraintInputSig Input> + HasTypeTreeSig Term, HasTypeTreeSig Constraint, + SatisfiesConstraintInputSig Input> { private import Input pragma[nomagic] - private Type getTypeAt(HasTypeTree term, TypePath path) { + private Type getTypeAt(Term term, TypePath path) { relevantConstraint(term, _) and result = term.getTypeAt(path) } /** Holds if the type tree has the type `type` and should satisfy `constraint`. */ pragma[nomagic] - private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) { + private predicate hasTypeConstraint( + Term term, Type type, Constraint constraint, Type constraintRoot + ) { type = getTypeAt(term, TypePath::nil()) and - relevantConstraint(term, constraint) + relevantConstraint(term, constraint) and + constraintRoot = constraint.getTypeAt(TypePath::nil()) } - private module IsInstantiationOfInput implements - IsInstantiationOfInputSig + private module TermIsInstantiationOfConditionInput implements + IsInstantiationOfInputSig { - predicate potentialInstantiationOf(HasTypeTree tt, TypeAbstraction abs, TypeMention cond) { - exists(Type constraint, Type type | - hasTypeConstraint(tt, type, constraint) and - rootTypesSatisfaction(type, constraint, abs, cond, _) and + predicate potentialInstantiationOf(Term tt, TypeAbstraction abs, TypeMention cond) { + exists(Constraint constraint, Type type, Type constraintRoot | + hasTypeConstraint(tt, type, constraint, constraintRoot) and + rootTypesSatisfaction(type, constraintRoot, abs, cond, _) and // We only need to check instantiations where there are multiple candidates. - multipleConstraintImplementations(type, constraint) + multipleConstraintImplementations(type, constraintRoot) ) } @@ -860,18 +894,18 @@ module Make1 Input1> { } } - private module SatisfiesConstraintIsInstantiationOf = - IsInstantiationOf; + private module TermIsInstantiationOfCondition = + IsInstantiationOf; /** * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`. */ pragma[nomagic] private predicate hasConstraintMention( - HasTypeTree tt, TypeAbstraction abs, TypeMention condition, Type constraint, - TypeMention constraintMention + Term tt, TypeAbstraction abs, TypeMention condition, Constraint constraint, + Type constraintRoot, TypeMention constraintMention ) { - exists(Type type | hasTypeConstraint(tt, type, constraint) | + exists(Type type | hasTypeConstraint(tt, type, constraint, constraintRoot) | // TODO: Handle universal conditions properly, which means checking type parameter constraints // Also remember to update logic in `hasNotConstraintMention` // @@ -880,23 +914,23 @@ module Make1 Input1> { // getTypeMentionRoot(condition) = abs.getATypeParameter() and // constraint = getTypeMentionRoot(constraintMention) // or - countConstraintImplementations(type, constraint) > 0 and - rootTypesSatisfaction(type, constraint, abs, condition, constraintMention) and + countConstraintImplementations(type, constraintRoot) > 0 and + rootTypesSatisfaction(type, constraintRoot, abs, condition, constraintMention) and // When there are multiple ways the type could implement the // constraint we need to find the right implementation, which is the // one where the type instantiates the precondition. - if multipleConstraintImplementations(type, constraint) - then SatisfiesConstraintIsInstantiationOf::isInstantiationOf(tt, abs, condition) + if multipleConstraintImplementations(type, constraintRoot) + then TermIsInstantiationOfCondition::isInstantiationOf(tt, abs, condition) else any() ) } pragma[nomagic] private predicate isNotInstantiationOf( - HasTypeTree tt, TypeAbstraction abs, TypeMention condition, Type root + Term tt, TypeAbstraction abs, TypeMention condition, Type root ) { exists(TypePath path | - SatisfiesConstraintIsInstantiationOf::isNotInstantiationOf(tt, abs, condition, path) and + TermIsInstantiationOfCondition::isNotInstantiationOf(tt, abs, condition, path) and path.isCons(root.getATypeParameter(), _) ) } @@ -907,8 +941,8 @@ module Make1 Input1> { * This predicate is an approximation of `not hasConstraintMention(tt, constraint)`. */ pragma[nomagic] - private predicate hasNotConstraintMention(HasTypeTree tt, Type constraint) { - exists(Type type | hasTypeConstraint(tt, type, constraint) | + private predicate hasNotConstraintMention(Term tt, Constraint constraint, Type constraintRoot) { + exists(Type type | hasTypeConstraint(tt, type, constraint, constraintRoot) | // TODO: Handle universal conditions properly, which means taking type parameter constraints into account // ( // exists(countConstraintImplementations(type, constraint)) @@ -921,13 +955,13 @@ module Make1 Input1> { // ) // ) and ( - countConstraintImplementations(type, constraint) = 0 + countConstraintImplementations(type, constraintRoot) = 0 or - not rootTypesSatisfaction(type, constraint, _, _, _) + not rootTypesSatisfaction(type, constraintRoot, _, _, _) or - multipleConstraintImplementations(type, constraint) and + multipleConstraintImplementations(type, constraintRoot) and forex(TypeAbstraction abs, TypeMention condition | - rootTypesSatisfaction(type, constraint, abs, condition, _) + rootTypesSatisfaction(type, constraintRoot, abs, condition, _) | isNotInstantiationOf(tt, abs, condition, type) ) @@ -937,21 +971,44 @@ module Make1 Input1> { pragma[nomagic] private predicate satisfiesConstraintTypeMention0( - HasTypeTree tt, Type constraint, TypeAbstraction abs, TypeMention sub, TypePath path, Type t + Term tt, Constraint constraint, Type constraintRoot, TypeMention constraintMention, + TypeAbstraction abs, TypeMention sub, TypePath path, Type t + ) { + hasConstraintMention(tt, abs, sub, constraint, constraintRoot, constraintMention) and + conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) + } + + pragma[nomagic] + private predicate satisfiesConstraintTypeMention1( + Term tt, Constraint constraint, Type constraintRoot, TypeAbstraction abs, TypeMention sub, + TypePath path, Type t ) { exists(TypeMention constraintMention | - hasConstraintMention(tt, abs, sub, constraint, constraintMention) and - conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) + satisfiesConstraintTypeMention0(tt, constraint, constraintRoot, constraintMention, abs, + sub, path, t) + | + if typeAbstractionHasAmbigousConstraintAt(abs, constraintRoot, path.getAPrefix()) + then + // When the constraint is not uniquely satisfied, we check that the satisfying + // abstraction is not more specific than the constraint to be satisfied. For example, + // if the constraint is `MyTrait` and there is both `impl MyTrait for ...` and + // `impl MyTrait for ...`, then the latter will be filtered away + not exists(TypePath path1, Type t1 | + conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path1, t1) and + not t1 instanceof TypeParameter and + t1 != constraint.getTypeAt(path1) + ) + else any() ) } pragma[inline] private predicate satisfiesConstraintTypeMentionInline( - HasTypeTree tt, TypeAbstraction abs, Type constraint, TypePath path, + Term tt, Constraint constraint, Type constraintRoot, TypeAbstraction abs, TypePath path, TypePath pathToTypeParamInSub ) { exists(TypeMention sub, TypeParameter tp | - satisfiesConstraintTypeMention0(tt, constraint, abs, sub, path, tp) and + satisfiesConstraintTypeMention1(tt, constraint, constraintRoot, abs, sub, path, tp) and tp = abs.getATypeParameter() and sub.getTypeAt(pathToTypeParamInSub) = tp ) @@ -959,30 +1016,34 @@ module Make1 Input1> { pragma[nomagic] private predicate satisfiesConstraintTypeMention( - HasTypeTree tt, Type constraint, TypePath path, TypePath pathToTypeParamInSub + Term tt, Constraint constraint, TypePath path, TypePath pathToTypeParamInSub ) { - satisfiesConstraintTypeMentionInline(tt, _, constraint, path, pathToTypeParamInSub) + satisfiesConstraintTypeMentionInline(tt, constraint, _, _, path, pathToTypeParamInSub) } pragma[nomagic] private predicate satisfiesConstraintTypeMentionThrough( - HasTypeTree tt, TypeAbstraction abs, Type constraint, TypePath path, + Term tt, TypeAbstraction abs, Constraint constraint, Type constraintRoot, TypePath path, TypePath pathToTypeParamInSub ) { - satisfiesConstraintTypeMentionInline(tt, abs, constraint, path, pathToTypeParamInSub) + satisfiesConstraintTypeMentionInline(tt, constraint, constraintRoot, abs, path, + pathToTypeParamInSub) } pragma[inline] private predicate satisfiesConstraintTypeNonTypeParamInline( - HasTypeTree tt, TypeAbstraction abs, Type constraint, TypePath path, Type t + Term tt, TypeAbstraction abs, Constraint constraint, Type constraintRoot, TypePath path, + Type t ) { - satisfiesConstraintTypeMention0(tt, constraint, abs, _, path, t) and + satisfiesConstraintTypeMention1(tt, constraint, constraintRoot, abs, _, path, t) and not t = abs.getATypeParameter() } pragma[nomagic] - private predicate hasTypeConstraint(HasTypeTree term, Type constraint) { - hasTypeConstraint(term, constraint, constraint) + private predicate hasTypeConstraint(Term term, Constraint constraint) { + exists(Type constraintRoot | + hasTypeConstraint(term, constraintRoot, constraint, constraintRoot) + ) } /** @@ -990,8 +1051,8 @@ module Make1 Input1> { * with the type `t` at `path`. */ pragma[nomagic] - predicate satisfiesConstraintType(HasTypeTree tt, Type constraint, TypePath path, Type t) { - satisfiesConstraintTypeNonTypeParamInline(tt, _, constraint, path, t) + predicate satisfiesConstraintType(Term tt, Constraint constraint, TypePath path, Type t) { + satisfiesConstraintTypeNonTypeParamInline(tt, _, constraint, _, path, t) or exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix | satisfiesConstraintTypeMention(tt, constraint, prefix0, pathToTypeParamInSub) and @@ -1009,12 +1070,13 @@ module Make1 Input1> { */ pragma[nomagic] predicate satisfiesConstraintTypeThrough( - HasTypeTree tt, TypeAbstraction abs, Type constraint, TypePath path, Type t + Term tt, TypeAbstraction abs, Constraint constraint, TypePath path, Type t ) { - satisfiesConstraintTypeNonTypeParamInline(tt, abs, constraint, path, t) + satisfiesConstraintTypeNonTypeParamInline(tt, abs, constraint, _, path, t) or exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix | - satisfiesConstraintTypeMentionThrough(tt, abs, constraint, prefix0, pathToTypeParamInSub) and + satisfiesConstraintTypeMentionThrough(tt, abs, constraint, _, prefix0, + pathToTypeParamInSub) and getTypeAt(tt, pathToTypeParamInSub.appendInverse(suffix)) = t and path = prefix0.append(suffix) ) @@ -1035,15 +1097,47 @@ module Make1 Input1> { * `dissatisfiesConstraint` will hold. */ pragma[nomagic] - predicate dissatisfiesConstraint(HasTypeTree tt, Type constraint) { - hasNotConstraintMention(tt, constraint) and - exists(Type t | - hasTypeConstraint(tt, t, constraint) and - t != constraint + predicate dissatisfiesConstraint(Term tt, Constraint constraint) { + hasNotConstraintMention(tt, constraint, _) and + exists(Type t, Type constraintRoot | + hasTypeConstraint(tt, t, constraint, constraintRoot) and // todo + t != constraintRoot ) } } + /** Provides the input to `SatisfiesType`. */ + signature module SatisfiesTypeInputSig { + /** Holds if it is relevant to know if `term` satisfies `constraint`. */ + predicate relevantConstraint(Term term, Type constraint); + } + + /** + * A helper module wrapping `SatisfiesConstraint` where the constraint is simply a type. + */ + module SatisfiesType Input> { + private import Input + + final private class TypeFinal = Type; + + private class TypeAsTypeTree extends TypeFinal { + Type getTypeAt(TypePath path) { + result = this and + path.isEmpty() + } + } + + private module SatisfiesConstraintInput implements + SatisfiesConstraintInputSig + { + predicate relevantConstraint(Term term, TypeAsTypeTree constraint) { + Input::relevantConstraint(term, constraint) + } + } + + import SatisfiesConstraint + } + /** Provides the input to `MatchingWithEnvironment`. */ signature module MatchingWithEnvironmentInputSig { /** @@ -1266,7 +1360,7 @@ module Make1 Input1> { private module AccessConstraint { predicate relevantAccessConstraint( Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath path, - Type constraint + TypeMention constraint ) { target = a.getTarget(e) and typeParameterConstraintHasTypeParameter(target, apos, path, constraint, _, _) @@ -1294,7 +1388,7 @@ module Make1 Input1> { } /** Gets the constraint that this relevant access should satisfy. */ - Type getConstraint(Declaration target) { + TypeMention getConstraint(Declaration target) { relevantAccessConstraint(a, e, target, apos, path, result) } @@ -1306,20 +1400,20 @@ module Make1 Input1> { } private module SatisfiesConstraintInput implements - SatisfiesConstraintInputSig + SatisfiesConstraintInputSig { - predicate relevantConstraint(RelevantAccess at, Type constraint) { + predicate relevantConstraint(RelevantAccess at, TypeMention constraint) { constraint = at.getConstraint(_) } } predicate satisfiesConstraintType( Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix, - Type constraint, TypePath path, Type t + TypeMention constraint, TypePath path, Type t ) { exists(RelevantAccess ra | ra = MkRelevantAccess(a, apos, e, prefix) and - SatisfiesConstraint::satisfiesConstraintType(ra, + SatisfiesConstraint::satisfiesConstraintType(ra, constraint, path, t) and constraint = ra.getConstraint(target) ) @@ -1429,17 +1523,17 @@ module Make1 Input1> { */ pragma[nomagic] private predicate typeParameterConstraintHasTypeParameter( - Declaration target, AccessPosition apos, TypePath pathToConstrained, Type constraint, + Declaration target, AccessPosition apos, TypePath pathToConstrained, TypeMention constraint, TypePath pathToTp, TypeParameter tp ) { exists(DeclarationPosition dpos, TypeParameter constrainedTp | accessDeclarationPositionMatch(apos, dpos) and constrainedTp = target.getTypeParameter(_) and tp = target.getTypeParameter(_) and - tp = getATypeParameterConstraint(constrainedTp, pathToTp) and + tp = constraint.getTypeAt(pathToTp) and constrainedTp != tp and constrainedTp = target.getDeclaredType(dpos, pathToConstrained) and - constraint = getATypeParameterConstraint(constrainedTp, TypePath::nil()) + constraint = getATypeParameterConstraint(constrainedTp) ) } @@ -1448,7 +1542,7 @@ module Make1 Input1> { Access a, AccessEnvironment e, Declaration target, TypePath path, Type t, TypeParameter tp ) { not exists(getTypeArgument(a, target, tp, _)) and - exists(Type constraint, AccessPosition apos, TypePath pathToTp, TypePath pathToTp2 | + 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, pathToTp.appendInverse(path), t) From 902e9532467730f353316277f6490d80043cfe24 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Tue, 17 Mar 2026 09:45:42 +0100 Subject: [PATCH 3/3] wip --- .../typeinference/FunctionOverloading.qll | 144 ++++++++++-------- .../internal/typeinference/TypeInference.qll | 3 +- .../internal/typeinference/TypeMention.qll | 14 +- .../typeinference/internal/TypeInference.qll | 83 +++++++--- 4 files changed, 158 insertions(+), 86 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll index f2e17d249704..9a8cefdbee7a 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll @@ -13,78 +13,98 @@ private import TypeMention private import TypeInference private import FunctionType -pragma[nomagic] -private Type resolveNonTypeParameterTypeAt(PreTypeMention tm, TypePath path) { - result = tm.getTypeAt(path) and - not result instanceof TypeParameter -} +signature Type resolveTypeMentionAtSig(AstNode tm, TypePath path); -bindingset[t1, t2] -private predicate typeMentionEqual(PreTypeMention t1, PreTypeMention t2) { - forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type | - resolveNonTypeParameterTypeAt(t2, path) = type - ) -} +private module MkSiblingImpls { + pragma[nomagic] + private Type resolveNonTypeParameterTypeAt(AstNode tm, TypePath path) { + result = resolveTypeMentionAt(tm, path) and + not result instanceof TypeParameter + } -pragma[nomagic] -private predicate implSiblingCandidate( - Impl impl, TraitItemNode trait, Type rootType, PreTypeMention selfTy -) { - trait = impl.(ImplItemNode).resolveTraitTy() and - selfTy = impl.getSelfTy() and - rootType = selfTy.getType() -} + bindingset[t1, t2] + private predicate typeMentionEqual(AstNode t1, AstNode t2) { + forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type | + resolveNonTypeParameterTypeAt(t2, path) = type + ) + } -pragma[nomagic] -private predicate blanketImplSiblingCandidate(ImplItemNode impl, Trait trait) { - impl.isBlanketImplementation() and - trait = impl.resolveTraitTy() -} + pragma[nomagic] + private predicate implSiblingCandidate( + Impl impl, TraitItemNode trait, Type rootType, AstNode selfTy + ) { + trait = impl.(ImplItemNode).resolveTraitTy() and + selfTy = impl.getSelfTy() and + rootType = resolveTypeMentionAt(selfTy, TypePath::nil()) + } -/** - * Holds if `impl1` and `impl2` are a sibling implementations of `trait`. We - * consider implementations to be siblings if they implement the same trait for - * the same type. In that case `Self` is the same type in both implementations, - * and method calls to the implementations cannot be resolved unambiguously - * based only on the receiver type. - */ -pragma[inline] -private predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) { - impl1 != impl2 and - ( - exists(Type rootType, PreTypeMention selfTy1, PreTypeMention selfTy2 | - implSiblingCandidate(impl1, trait, rootType, selfTy1) and - implSiblingCandidate(impl2, trait, rootType, selfTy2) and - // In principle the second conjunct below should be superflous, but we still - // have ill-formed type mentions for types that we don't understand. For - // those checking both directions restricts further. Note also that we check - // syntactic equality, whereas equality up to renaming would be more - // correct. - typeMentionEqual(selfTy1, selfTy2) and - typeMentionEqual(selfTy2, selfTy1) + pragma[nomagic] + private predicate blanketImplSiblingCandidate(ImplItemNode impl, Trait trait) { + impl.isBlanketImplementation() and + trait = impl.resolveTraitTy() + } + + /** + * Holds if `impl1` and `impl2` are a sibling implementations of `trait`. We + * consider implementations to be siblings if they implement the same trait for + * the same type. In that case `Self` is the same type in both implementations, + * and method calls to the implementations cannot be resolved unambiguously + * based only on the receiver type. + */ + pragma[inline] + predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) { + impl1 != impl2 and + ( + exists(Type rootType, AstNode selfTy1, AstNode selfTy2 | + implSiblingCandidate(impl1, trait, rootType, selfTy1) and + implSiblingCandidate(impl2, trait, rootType, selfTy2) and + // In principle the second conjunct below should be superflous, but we still + // have ill-formed type mentions for types that we don't understand. For + // those checking both directions restricts further. Note also that we check + // syntactic equality, whereas equality up to renaming would be more + // correct. + typeMentionEqual(selfTy1, selfTy2) and + typeMentionEqual(selfTy2, selfTy1) + ) + or + blanketImplSiblingCandidate(impl1, trait) and + blanketImplSiblingCandidate(impl2, trait) ) - or - blanketImplSiblingCandidate(impl1, trait) and - blanketImplSiblingCandidate(impl2, trait) - ) + } + + /** + * Holds if `impl` is an implementation of `trait` and if another implementation + * exists for the same type. + */ + pragma[nomagic] + predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) } + + pragma[nomagic] + predicate implHasAmbigousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) { + exists(ImplItemNode impl2, Type t | + implSiblings(trait, impl, impl2) and + t = resolveNonTypeParameterTypeAt(impl.getTraitPath(), path) and + t != resolveNonTypeParameterTypeAt(impl2.getTraitPath(), path) + ) + } } -/** - * Holds if `impl` is an implementation of `trait` and if another implementation - * exists for the same type. - */ -pragma[nomagic] -private predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) } +private Type resolvePreTypeMention(AstNode tm, TypePath path) { + result = tm.(PreTypeMention).getTypeAt(path) +} -pragma[nomagic] -predicate implHasAmbigousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) { - exists(ImplItemNode impl2 | - implSiblings(trait, impl, impl2) and - resolveNonTypeParameterTypeAt(impl.getTraitPath(), path) != - resolveNonTypeParameterTypeAt(impl2.getTraitPath(), path) - ) +private module PreSiblingImpls = MkSiblingImpls; + +predicate preImplHasAmbigousSiblingAt = PreSiblingImpls::implHasAmbigousSiblingAt/3; + +private Type resolveTypeMention(AstNode tm, TypePath path) { + result = tm.(TypeMention).getTypeAt(path) } +private module SiblingImpls = MkSiblingImpls; + +import SiblingImpls + /** * Holds if `f` is a function declared inside `trait`, and the type of `f` at * `pos` and `path` is `traitTp`, which is a type parameter of `trait`. diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll index 798ee76c7be9..1bdcb3b0ab1f 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll @@ -2827,6 +2827,7 @@ private module FunctionCallMatchingInput implements MatchingWithEnvironmentInput } abstract class Access extends ContextTyping::ContextTypedCallCand { + // Access() { this = Debug::getRelevantLocatable() } abstract AstNode getNodeAt(FunctionPosition pos); bindingset[derefChainBorrow] @@ -4125,7 +4126,7 @@ private module Debug { exists(string filepath, int startline, int startcolumn, int endline, int endcolumn | result.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and filepath.matches("%/main.rs") and - startline = 103 + startline = 1751 ) } diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll index e6c01b7659c1..7de2ba0d3414 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll @@ -7,6 +7,7 @@ private import Type private import TypeAbstraction private import TypeInference private import AssociatedType +private import FunctionOverloading bindingset[trait, name] pragma[inline_late] @@ -717,9 +718,9 @@ private class TraitOrTmTrait extends AstNode { * Holds if `path` accesses an associated type `alias` from `trait` on a * concrete type given by `tm`. * - * `implOrTmTrait` is either the mention that resolves to `trait` when `path` - * is of the form `::AssocType`, or the enclosing `impl` block - * when `path` is of the form `Self::AssocType`. + * `traitOrTmTrait` is either the mention that resolves to `trait` when `path` + * is of the form `::AssocType`, or the trait being implemented + * when `path` is of the form `Self::AssocType` within an `impl` block. */ private predicate pathConcreteTypeAssocType( Path path, PreTypeMention tm, TraitItemNode trait, TraitOrTmTrait traitOrTmTrait, TypeAlias alias @@ -730,6 +731,7 @@ private predicate pathConcreteTypeAssocType( | // path of the form `::AssocType` // ^^^ tm ^^^^^^^^^ name + // ^^^^^ traitOrTmTrait exists(string name | pathTypeAsTraitAssoc(path, tm, traitOrTmTrait, trait, name) and getTraitAssocType(trait, name) = alias @@ -753,6 +755,12 @@ private module PathSatisfiesConstraintInput implements predicate relevantConstraint(PreTypeMention tm, TraitOrTmTrait constraint) { pathConcreteTypeAssocType(_, tm, _, constraint, _) } + + predicate typeAbstractionHasAmbigousConstraintAtOverride( + TypeAbstraction abs, Type constraint, TypePath path + ) { + preImplHasAmbigousSiblingAt(abs, constraint.(TraitType).getTrait(), path) + } } private module PathSatisfiesConstraint = diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 701ed1e0441f..8e4c19681cff 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -853,6 +853,14 @@ module Make1 Input1> { signature module SatisfiesConstraintInputSig { /** Holds if it is relevant to know if `term` satisfies `constraint`. */ predicate relevantConstraint(Term term, Constraint constraint); + + default Type foo(Term term, TypeParameter tp, TypePath path) { none() } + + default predicate typeAbstractionHasAmbigousConstraintAtOverride( + TypeAbstraction abs, Type constraint, TypePath path + ) { + typeAbstractionHasAmbigousConstraintAt(abs, constraint, path) + } } module SatisfiesConstraint< @@ -978,25 +986,56 @@ module Make1 Input1> { conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t) } + pragma[nomagic] + private predicate satisfiesConstraintTypeMention01( + Term tt, Constraint constraint, TypeAbstraction abs, TypePath prefix, TypeParameter tp + ) { + exists(Type constraintRoot | + satisfiesConstraintTypeMention0(tt, constraint, constraintRoot, _, abs, _, _, _) and + typeAbstractionHasAmbigousConstraintAtOverride(abs, constraintRoot, _) and + tp = constraint.getTypeAt(prefix) + ) + } + + bindingset[abs, path, t] + pragma[inline_late] + private predicate conditionSatisfiesConstraintTypeAtFilter( + TypeAbstraction abs, TypePath path, Type t + ) { + conditionSatisfiesConstraintTypeAt(abs, _, _, path, t) + } + + pragma[nomagic] + private Type getConstraintType(Term tt, Constraint constraint, TypePath path) { + exists(TypeAbstraction abs, TypePath prefix, TypeParameter tp, TypePath suffix | + satisfiesConstraintTypeMention01(tt, constraint, abs, prefix, tp) and + result = foo(tt, tp, suffix) and + path = prefix.append(suffix) and + conditionSatisfiesConstraintTypeAtFilter(abs, path, result) + ) + } + pragma[nomagic] private predicate satisfiesConstraintTypeMention1( - Term tt, Constraint constraint, Type constraintRoot, TypeAbstraction abs, TypeMention sub, - TypePath path, Type t + Term tt, Constraint constraint, TypeAbstraction abs, TypeMention sub, TypePath path, Type t ) { - exists(TypeMention constraintMention | + exists(Type constraintRoot, TypeMention constraintMention | satisfiesConstraintTypeMention0(tt, constraint, constraintRoot, constraintMention, abs, sub, path, t) | - if typeAbstractionHasAmbigousConstraintAt(abs, constraintRoot, path.getAPrefix()) + if typeAbstractionHasAmbigousConstraintAtOverride(abs, constraintRoot, path.getAPrefix()) then // When the constraint is not uniquely satisfied, we check that the satisfying // abstraction is not more specific than the constraint to be satisfied. For example, // if the constraint is `MyTrait` and there is both `impl MyTrait for ...` and // `impl MyTrait for ...`, then the latter will be filtered away - not exists(TypePath path1, Type t1 | + forall(TypePath path1, Type t1 | conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path1, t1) and - not t1 instanceof TypeParameter and - t1 != constraint.getTypeAt(path1) + not t1 instanceof TypeParameter + | + not t1 != constraint.getTypeAt(path1) + or + t1 = getConstraintType(tt, constraint, path1) ) else any() ) @@ -1004,11 +1043,11 @@ module Make1 Input1> { pragma[inline] private predicate satisfiesConstraintTypeMentionInline( - Term tt, Constraint constraint, Type constraintRoot, TypeAbstraction abs, TypePath path, + Term tt, Constraint constraint, TypeAbstraction abs, TypePath path, TypePath pathToTypeParamInSub ) { exists(TypeMention sub, TypeParameter tp | - satisfiesConstraintTypeMention1(tt, constraint, constraintRoot, abs, sub, path, tp) and + satisfiesConstraintTypeMention1(tt, constraint, abs, sub, path, tp) and tp = abs.getATypeParameter() and sub.getTypeAt(pathToTypeParamInSub) = tp ) @@ -1018,24 +1057,22 @@ module Make1 Input1> { private predicate satisfiesConstraintTypeMention( Term tt, Constraint constraint, TypePath path, TypePath pathToTypeParamInSub ) { - satisfiesConstraintTypeMentionInline(tt, constraint, _, _, path, pathToTypeParamInSub) + satisfiesConstraintTypeMentionInline(tt, constraint, _, path, pathToTypeParamInSub) } pragma[nomagic] private predicate satisfiesConstraintTypeMentionThrough( - Term tt, TypeAbstraction abs, Constraint constraint, Type constraintRoot, TypePath path, + Term tt, TypeAbstraction abs, Constraint constraint, TypePath path, TypePath pathToTypeParamInSub ) { - satisfiesConstraintTypeMentionInline(tt, constraint, constraintRoot, abs, path, - pathToTypeParamInSub) + satisfiesConstraintTypeMentionInline(tt, constraint, abs, path, pathToTypeParamInSub) } pragma[inline] private predicate satisfiesConstraintTypeNonTypeParamInline( - Term tt, TypeAbstraction abs, Constraint constraint, Type constraintRoot, TypePath path, - Type t + Term tt, TypeAbstraction abs, Constraint constraint, TypePath path, Type t ) { - satisfiesConstraintTypeMention1(tt, constraint, constraintRoot, abs, _, path, t) and + satisfiesConstraintTypeMention1(tt, constraint, abs, _, path, t) and not t = abs.getATypeParameter() } @@ -1052,7 +1089,7 @@ module Make1 Input1> { */ pragma[nomagic] predicate satisfiesConstraintType(Term tt, Constraint constraint, TypePath path, Type t) { - satisfiesConstraintTypeNonTypeParamInline(tt, _, constraint, _, path, t) + satisfiesConstraintTypeNonTypeParamInline(tt, _, constraint, path, t) or exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix | satisfiesConstraintTypeMention(tt, constraint, prefix0, pathToTypeParamInSub) and @@ -1072,11 +1109,10 @@ module Make1 Input1> { predicate satisfiesConstraintTypeThrough( Term tt, TypeAbstraction abs, Constraint constraint, TypePath path, Type t ) { - satisfiesConstraintTypeNonTypeParamInline(tt, abs, constraint, _, path, t) + satisfiesConstraintTypeNonTypeParamInline(tt, abs, constraint, path, t) or exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix | - satisfiesConstraintTypeMentionThrough(tt, abs, constraint, _, prefix0, - pathToTypeParamInSub) and + satisfiesConstraintTypeMentionThrough(tt, abs, constraint, prefix0, pathToTypeParamInSub) and getTypeAt(tt, pathToTypeParamInSub.appendInverse(suffix)) = t and path = prefix0.append(suffix) ) @@ -1405,6 +1441,13 @@ module Make1 Input1> { predicate relevantConstraint(RelevantAccess at, TypeMention constraint) { constraint = at.getConstraint(_) } + + Type foo(RelevantAccess at, TypeParameter tp, TypePath path) { + exists(Access a, AccessEnvironment e, Declaration target | + at = MkRelevantAccess(a, _, e, _) and + typeMatch(a, e, target, path, result, tp) + ) + } } predicate satisfiesConstraintType(