From d5a95a8099bddb5ef65e22760569e5ae20e3fb1e Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Wed, 10 Dec 2025 20:44:27 +0100 Subject: [PATCH] Rust: Strengthen `isNotInstantiationOf` uses --- .../codeql/rust/internal/TypeInference.qll | 20 +- .../internal/typeinference/FunctionType.qll | 6 +- .../test/library-tests/type-inference/main.rs | 2 +- .../type-inference/type-inference.expected | 186 ------------------ .../typeinference/internal/TypeInference.qll | 29 ++- 5 files changed, 40 insertions(+), 203 deletions(-) diff --git a/rust/ql/lib/codeql/rust/internal/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/TypeInference.qll index ed87b0c7104..b281889ef1d 100644 --- a/rust/ql/lib/codeql/rust/internal/TypeInference.qll +++ b/rust/ql/lib/codeql/rust/internal/TypeInference.qll @@ -1430,11 +1430,19 @@ private module MethodResolution { * Holds if the method inside `i` with matching name and arity can be ruled * out as a target of this call, because the candidate receiver type represented * by `derefChain` and `borrow` is incompatible with the `self` parameter type. + * + * The types are incompatible because they disagree on a concrete type somewhere + * inside `root`. */ pragma[nomagic] - private predicate hasIncompatibleTarget(ImplOrTraitItemNode i, string derefChain, boolean borrow) { - ReceiverIsInstantiationOfSelfParam::argIsNotInstantiationOf(MkMethodCallCand(this, derefChain, - borrow), i, _) + private predicate hasIncompatibleTarget( + ImplOrTraitItemNode i, string derefChain, boolean borrow, Type root + ) { + exists(TypePath path | + ReceiverIsInstantiationOfSelfParam::argIsNotInstantiationOf(MkMethodCallCand(this, + derefChain, borrow), i, _, path) and + path.isCons(root.getATypeParameter(), _) + ) } /** @@ -1448,7 +1456,7 @@ private module MethodResolution { ImplItemNode impl, string derefChain, boolean borrow ) { ReceiverIsNotInstantiationOfBlanketLikeSelfParam::argIsNotInstantiationOf(MkMethodCallCand(this, - derefChain, borrow), impl, _) + derefChain, borrow), impl, _, _) or ReceiverSatisfiesBlanketLikeConstraint::dissatisfiesBlanketConstraint(MkMethodCallCand(this, derefChain, borrow), impl) @@ -1479,7 +1487,7 @@ private module MethodResolution { forall(ImplOrTraitItemNode i | methodCallNonBlanketCandidate(this, _, i, _, strippedTypePath, strippedType) | - this.hasIncompatibleTarget(i, derefChain, borrow) + this.hasIncompatibleTarget(i, derefChain, borrow, strippedType) ) } @@ -1818,7 +1826,7 @@ private module MethodResolution { */ pragma[nomagic] private predicate hasIncompatibleInherentTarget(Impl impl) { - ReceiverIsNotInstantiationOfInherentSelfParam::argIsNotInstantiationOf(this, impl, _) + ReceiverIsNotInstantiationOfInherentSelfParam::argIsNotInstantiationOf(this, impl, _, _) } /** diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll index c219ef0eacc..a74ff762c58 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionType.qll @@ -256,8 +256,10 @@ module ArgIsInstantiationOf< ArgSubstIsInstantiationOf::isInstantiationOf(arg, i, constraint) } - predicate argIsNotInstantiationOf(Arg arg, ImplOrTraitItemNode i, AssocFunctionType constraint) { - ArgSubstIsInstantiationOf::isNotInstantiationOf(arg, i, constraint) + predicate argIsNotInstantiationOf( + Arg arg, ImplOrTraitItemNode i, AssocFunctionType constraint, TypePath path + ) { + ArgSubstIsInstantiationOf::isNotInstantiationOf(arg, i, constraint, path) } } diff --git a/rust/ql/test/library-tests/type-inference/main.rs b/rust/ql/test/library-tests/type-inference/main.rs index 4cc91bf6584..466733cf47c 100644 --- a/rust/ql/test/library-tests/type-inference/main.rs +++ b/rust/ql/test/library-tests/type-inference/main.rs @@ -3064,7 +3064,7 @@ mod literal_overlap { pub fn f() -> usize { let mut x = 0; - x = x.f(); // $ target=usizef $ SPURIOUS: target=i32f target=Reff + x = x.f(); // $ target=usizef $ SPURIOUS: target=i32f x } } 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 9aaad02aa43..14cc4577539 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -11013,203 +11013,17 @@ inferType | main.rs:3065:25:3069:5 | { ... } | | {EXTERNAL LOCATION} | usize | | main.rs:3066:17:3066:17 | x | | {EXTERNAL LOCATION} | i32 | | main.rs:3066:17:3066:17 | x | | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:17:3066:17 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | | main.rs:3066:21:3066:21 | 0 | | {EXTERNAL LOCATION} | i32 | | main.rs:3066:21:3066:21 | 0 | | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3066:21:3066:21 | 0 | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | | main.rs:3067:9:3067:9 | x | | {EXTERNAL LOCATION} | i32 | | main.rs:3067:9:3067:9 | x | | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:9:3067:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | | main.rs:3067:9:3067:17 | ... = ... | | {EXTERNAL LOCATION} | () | | main.rs:3067:13:3067:13 | x | | {EXTERNAL LOCATION} | i32 | | main.rs:3067:13:3067:13 | x | | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:13 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | | main.rs:3067:13:3067:17 | x.f() | | {EXTERNAL LOCATION} | i32 | | main.rs:3067:13:3067:17 | x.f() | | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3067:13:3067:17 | x.f() | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | | main.rs:3068:9:3068:9 | x | | {EXTERNAL LOCATION} | i32 | | main.rs:3068:9:3068:9 | x | | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | i32 | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | usize | -| main.rs:3068:9:3068:9 | x | TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef.TRef | {EXTERNAL LOCATION} | & | | main.rs:3077:11:3112:1 | { ... } | | {EXTERNAL LOCATION} | () | | main.rs:3078:5:3078:21 | ...::f(...) | | {EXTERNAL LOCATION} | () | | main.rs:3079:5:3079:20 | ...::f(...) | | main.rs:72:5:72:21 | Foo | diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index bf107c7d3f5..4bb348979c1 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -705,7 +705,8 @@ module Make1 Input1> { } /** - * Holds if `app` is _not_ a possible instantiation of `constraint`. + * Holds if `app` is _not_ a possible instantiation of `constraint`, because `app` + * and `constraint` differ on concrete types at `path`. * * This is an approximation of `not isInstantiationOf(app, abs, constraint)`, but * defined without a negative occurrence of `isInstantiationOf`. @@ -719,9 +720,11 @@ module Make1 Input1> { * `isInstantiationOf` nor `isNotInstantiationOf` will hold. */ pragma[nomagic] - predicate isNotInstantiationOf(App app, TypeAbstraction abs, Constraint constraint) { + predicate isNotInstantiationOf( + App app, TypeAbstraction abs, Constraint constraint, TypePath path + ) { // `app` and `constraint` differ on a concrete type - exists(Type t, Type t2, TypePath path | + exists(Type t, Type t2 | t = resolveTypeAt(app, abs, constraint, path) and not t = abs.getATypeParameter() and app.getTypeAt(path) = t2 and @@ -983,6 +986,9 @@ module Make1 Input1> { } } + private module SatisfiesConstraintIsInstantiationOf = + IsInstantiationOf; + /** * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`. */ @@ -1004,13 +1010,21 @@ module Make1 Input1> { // constraint we need to find the right implementation, which is the // one where the type instantiates the precondition. if multipleConstraintImplementations(type, constraint) - then - IsInstantiationOf::isInstantiationOf(tt, - abs, condition) + then SatisfiesConstraintIsInstantiationOf::isInstantiationOf(tt, abs, condition) else any() ) } + pragma[nomagic] + private predicate isNotInstantiationOf( + HasTypeTree tt, TypeAbstraction abs, TypeMention condition, Type root + ) { + exists(TypePath path | + SatisfiesConstraintIsInstantiationOf::isNotInstantiationOf(tt, abs, condition, path) and + path.isCons(root.getATypeParameter(), _) + ) + } + /** * Holds if `tt` does not satisfy `constraint`. * @@ -1040,8 +1054,7 @@ module Make1 Input1> { forex(TypeAbstraction abs, TypeMention condition | rootTypesSatisfaction(type, constraint, abs, condition, _) | - IsInstantiationOf::isNotInstantiationOf(tt, - abs, condition) + isNotInstantiationOf(tt, abs, condition, type) ) ) )