diff --git a/rust/ql/lib/codeql/rust/internal/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/TypeInference.qll index bcc18342c007..338135a63c87 100644 --- a/rust/ql/lib/codeql/rust/internal/TypeInference.qll +++ b/rust/ql/lib/codeql/rust/internal/TypeInference.qll @@ -901,14 +901,14 @@ private predicate assocFunctionInfo( /** * Holds if function `f` with the name `name` and the arity `arity` exists in - * blanket implementation `impl` of `trait`, and the type at position + * blanket (like) implementation `impl` of `trait`, and the type at position * `pos` is `t`. * * `blanketPath` points to the type `blanketTypeParam` inside `t`, which * is the type parameter used in the blanket implementation. */ pragma[nomagic] -private predicate functionInfoBlanket( +private predicate functionInfoBlanketLike( Function f, string name, int arity, ImplItemNode impl, Trait trait, FunctionPosition pos, AssocFunctionType t, TypePath blanketPath, TypeParam blanketTypeParam ) { @@ -1027,19 +1027,20 @@ private module MethodResolution { /** * Holds if method `m` with the name `name` and the arity `arity` exists in - * blanket implementation `impl` of `trait`, and the type of the `self` + * blanket (like) implementation `impl` of `trait`, and the type of the `self` * parameter is `selfType`. * * `blanketPath` points to the type `blanketTypeParam` inside `selfType`, which * is the type parameter used in the blanket implementation. */ pragma[nomagic] - private predicate methodInfoBlanket( + private predicate methodInfoBlanketLike( Method m, string name, int arity, ImplItemNode impl, Trait trait, AssocFunctionType selfType, TypePath blanketPath, TypeParam blanketTypeParam ) { exists(FunctionPosition pos | - functionInfoBlanket(m, name, arity, impl, trait, pos, selfType, blanketPath, blanketTypeParam) and + functionInfoBlanketLike(m, name, arity, impl, trait, pos, selfType, blanketPath, + blanketTypeParam) and pos.isSelf() ) } @@ -1113,8 +1114,8 @@ private module MethodResolution { } /** - * Holds if method call `mc` may target a method in blanket implementation `i` - * with `self` parameter having type `selfType`. + * Holds if method call `mc` may target a method in blanket (like) implementation + * `impl` with `self` parameter having type `selfType`. * * `blanketPath` points to the type `blanketTypeParam` inside `selfType`, which * is the type parameter used in the blanket implementation. @@ -1125,13 +1126,13 @@ private module MethodResolution { */ bindingset[mc] pragma[inline_late] - private predicate methodCallBlanketCandidate( + private predicate methodCallBlanketLikeCandidate( MethodCall mc, Method m, ImplItemNode impl, AssocFunctionType self, TypePath blanketPath, TypeParam blanketTypeParam ) { exists(string name, int arity | mc.hasNameAndArity(name, arity) and - methodInfoBlanket(m, name, arity, impl, _, self, blanketPath, blanketTypeParam) + methodInfoBlanketLike(m, name, arity, impl, _, self, blanketPath, blanketTypeParam) | methodCallVisibleImplTraitCandidate(mc, impl) or @@ -1216,6 +1217,23 @@ private module MethodResolution { borrow), i, _) } + /** + * Holds if the method inside blanket-like implementation `impl` with matching name + * and arity can be ruled out as a target of this call, either because the candidate + * receiver type represented by `derefChain` and `borrow` is incompatible with the `self` + * parameter type, or because the blanket constraint is not satisfied. + */ + pragma[nomagic] + private predicate hasIncompatibleBlanketLikeTarget( + ImplItemNode impl, string derefChain, boolean borrow + ) { + ReceiverIsNotInstantiationOfBlanketLikeSelfParam::argIsNotInstantiationOf(MkMethodCallCand(this, + derefChain, borrow), impl, _) + or + ReceiverSatisfiesBlanketLikeConstraint::dissatisfiesBlanketConstraint(MkMethodCallCand(this, + derefChain, borrow), impl) + } + /** * Same as `getACandidateReceiverTypeAt`, but with traits substituted in for types * with trait bounds. @@ -1234,11 +1252,10 @@ private module MethodResolution { isComplexRootStripped(strippedTypePath, result) } - bindingset[strippedTypePath, strippedType, derefChain, borrow] - private predicate hasNoCompatibleTargetCheck( + bindingset[derefChain, borrow, strippedTypePath, strippedType] + private predicate hasNoCompatibleNonBlanketLikeTargetCheck( string derefChain, boolean borrow, TypePath strippedTypePath, Type strippedType ) { - // todo: also check that all blanket implementation candidates are incompatible forall(ImplOrTraitItemNode i | methodCallNonBlanketCandidate(this, _, i, _, strippedTypePath, strippedType) | @@ -1246,6 +1263,30 @@ private module MethodResolution { ) } + bindingset[derefChain, borrow, strippedTypePath, strippedType] + private predicate hasNoCompatibleTargetCheck( + string derefChain, boolean borrow, TypePath strippedTypePath, Type strippedType + ) { + this.hasNoCompatibleNonBlanketLikeTargetCheck(derefChain, borrow, strippedTypePath, + strippedType) and + forall(ImplItemNode i | methodCallBlanketLikeCandidate(this, _, i, _, _, _) | + this.hasIncompatibleBlanketLikeTarget(i, derefChain, borrow) + ) + } + + bindingset[derefChain, borrow, strippedTypePath, strippedType] + private predicate hasNoCompatibleNonBlanketTargetCheck( + string derefChain, boolean borrow, TypePath strippedTypePath, Type strippedType + ) { + this.hasNoCompatibleNonBlanketLikeTargetCheck(derefChain, borrow, strippedTypePath, + strippedType) and + forall(ImplItemNode i | + methodCallBlanketLikeCandidate(this, _, i, _, _, _) and not i.isBlanketImplementation() + | + this.hasIncompatibleBlanketLikeTarget(i, derefChain, borrow) + ) + } + /** * Holds if the candidate receiver type represented by `derefChain` does not * have a matching method target. @@ -1256,7 +1297,7 @@ private module MethodResolution { this.supportsAutoDerefAndBorrow() or // needed for the `hasNoCompatibleTarget` check in - // `SatisfiesBlanketConstraintInput::hasBlanketCandidate` + // `ReceiverSatisfiesBlanketLikeConstraintInput::hasBlanketCandidate` derefChain = "" ) and exists(TypePath strippedTypePath, Type strippedType | @@ -1266,6 +1307,26 @@ private module MethodResolution { ) } + /** + * Holds if the candidate receiver type represented by `derefChain` does not have + * a matching non-blanket method target. + */ + pragma[nomagic] + predicate hasNoCompatibleNonBlanketTargetNoBorrow(string derefChain) { + ( + this.supportsAutoDerefAndBorrow() + or + // needed for the `hasNoCompatibleTarget` check in + // `ReceiverSatisfiesBlanketLikeConstraintInput::hasBlanketCandidate` + derefChain = "" + ) and + exists(TypePath strippedTypePath, Type strippedType | + not derefChain.matches("%.ref") and // no need to try a borrow if the last thing we did was a deref + strippedType = this.getComplexStrippedType(derefChain, false, strippedTypePath) and + this.hasNoCompatibleNonBlanketTargetCheck(derefChain, false, strippedTypePath, strippedType) + ) + } + /** * Holds if the candidate receiver type represented by `derefChain`, followed * by a borrow, does not have a matching method target. @@ -1275,7 +1336,21 @@ private module MethodResolution { exists(TypePath strippedTypePath, Type strippedType | this.hasNoCompatibleTargetNoBorrow(derefChain) and strippedType = this.getComplexStrippedType(derefChain, true, strippedTypePath) and - this.hasNoCompatibleTargetCheck(derefChain, true, strippedTypePath, strippedType) + this.hasNoCompatibleNonBlanketLikeTargetCheck(derefChain, true, strippedTypePath, + strippedType) + ) + } + + /** + * Holds if the candidate receiver type represented by `derefChain`, followed + * by a borrow, does not have a matching non-blanket method target. + */ + pragma[nomagic] + predicate hasNoCompatibleNonBlanketTargetBorrow(string derefChain) { + exists(TypePath strippedTypePath, Type strippedType | + this.hasNoCompatibleTargetNoBorrow(derefChain) and + strippedType = this.getComplexStrippedType(derefChain, true, strippedTypePath) and + this.hasNoCompatibleNonBlanketTargetCheck(derefChain, true, strippedTypePath, strippedType) ) } @@ -1470,11 +1545,11 @@ private module MethodResolution { } pragma[nomagic] - predicate hasNoCompatibleTarget() { - mc_.hasNoCompatibleTargetBorrow(derefChain) and + predicate hasNoCompatibleNonBlanketTarget() { + mc_.hasNoCompatibleNonBlanketTargetBorrow(derefChain) and borrow = true or - mc_.hasNoCompatibleTargetNoBorrow(derefChain) and + mc_.hasNoCompatibleNonBlanketTargetNoBorrow(derefChain) and borrow = false } @@ -1555,20 +1630,20 @@ private module MethodResolution { Location getLocation() { result = mc_.getLocation() } } - private module ReceiverSatisfiesBlanketConstraintInput implements + private module ReceiverSatisfiesBlanketLikeConstraintInput implements BlanketImplementation::SatisfiesBlanketConstraintInputSig { pragma[nomagic] predicate hasBlanketCandidate( MethodCallCand mcc, ImplItemNode impl, TypePath blanketPath, TypeParam blanketTypeParam ) { - exists(MethodCall mc, string name, int arity | - mcc.hasSignature(mc, _, _, name, arity) and - methodCallBlanketCandidate(mc, _, impl, _, blanketPath, blanketTypeParam) and + exists(MethodCall mc | + mc = mcc.getMethodCall() and + methodCallBlanketLikeCandidate(mc, _, impl, _, blanketPath, blanketTypeParam) and // Only apply blanket implementations when no other implementations are possible; // this is to account for codebases that use the (unstable) specialization feature // (https://rust-lang.github.io/rfcs/1210-impl-specialization.html) - mcc.hasNoCompatibleTarget() + (mcc.hasNoCompatibleNonBlanketTarget() or not impl.isBlanketImplementation()) | mcc.hasNoBorrow() or @@ -1577,9 +1652,9 @@ private module MethodResolution { } } - private module ReceiverSatisfiesBlanketConstraint = + private module ReceiverSatisfiesBlanketLikeConstraint = BlanketImplementation::SatisfiesBlanketConstraint; + ReceiverSatisfiesBlanketLikeConstraintInput>; /** * A configuration for matching the type of a receiver against the type of @@ -1600,8 +1675,8 @@ private module MethodResolution { | methodCallNonBlanketCandidate(mc, m, i, selfType, strippedTypePath, strippedType) or - methodCallBlanketCandidate(mc, m, i, selfType, _, _) and - ReceiverSatisfiesBlanketConstraint::satisfiesBlanketConstraint(mcc, i) + methodCallBlanketLikeCandidate(mc, m, i, selfType, _, _) and + ReceiverSatisfiesBlanketLikeConstraint::satisfiesBlanketConstraint(mcc, i) ) } @@ -1626,6 +1701,30 @@ private module MethodResolution { private module ReceiverIsInstantiationOfSelfParam = ArgIsInstantiationOf; + /** + * A configuration for anti-matching the type of a receiver against the type of + * a `self` parameter belonging to a blanket (like) implementation. + */ + private module ReceiverIsNotInstantiationOfBlanketLikeSelfParamInput implements + IsInstantiationOfInputSig + { + pragma[nomagic] + predicate potentialInstantiationOf( + MethodCallCand mcc, TypeAbstraction abs, AssocFunctionType constraint + ) { + methodCallBlanketLikeCandidate(mcc.getMethodCall(), _, abs, constraint, _, _) and + if abs.(Impl).hasTrait() + then + // inherent methods take precedence over trait methods, so only allow + // trait methods when there are no matching inherent methods + mcc.hasNoInherentTarget() + else any() + } + } + + private module ReceiverIsNotInstantiationOfBlanketLikeSelfParam = + ArgIsInstantiationOf; + /** * A configuration for matching the type qualifier of a method call * against the type being implemented in an `impl` block. For example, @@ -1679,10 +1778,6 @@ private module MethodResolution { ReceiverIsInstantiationOfSelfParamInput::potentialInstantiationOf0(mcc, abs, constraint) and abs = any(Impl i | not i.hasTrait()) } - - predicate relevantConstraint(AssocFunctionType constraint) { - methodInfo(_, _, _, _, constraint, _, _) - } } private module ReceiverIsNotInstantiationOfInherentSelfParam = @@ -1948,18 +2043,18 @@ private module NonMethodResolution { } pragma[nomagic] - private predicate functionInfoBlanketRelevantPos( + private predicate functionInfoBlanketLikeRelevantPos( NonMethodFunction f, string name, int arity, ImplItemNode impl, Trait trait, FunctionPosition pos, AssocFunctionType t, TypePath blanketPath, TypeParam blanketTypeParam ) { - functionInfoBlanket(f, name, arity, impl, trait, pos, t, blanketPath, blanketTypeParam) and + functionInfoBlanketLike(f, name, arity, impl, trait, pos, t, blanketPath, blanketTypeParam) and ( if pos.isReturn() then // We only check that the context of the call provides relevant type information // when no argument can not exists(FunctionPosition pos0 | - functionInfoBlanket(f, name, arity, impl, trait, pos0, _, _, _) and + functionInfoBlanketLike(f, name, arity, impl, trait, pos0, _, _, _) and not pos0.isReturn() ) else any() @@ -1967,10 +2062,10 @@ private module NonMethodResolution { } pragma[nomagic] - private predicate blanketCallTraitCandidate(Element fc, Trait trait) { + private predicate blanketLikeCallTraitCandidate(Element fc, Trait trait) { exists(string name, int arity | fc.(NonMethodCall).hasNameAndArity(name, arity) and - functionInfoBlanketRelevantPos(_, name, arity, _, trait, _, _, _, _) + functionInfoBlanketLikeRelevantPos(_, name, arity, _, trait, _, _, _, _) | not fc.(Call).hasTrait() or @@ -1978,7 +2073,7 @@ private module NonMethodResolution { ) } - private module BlanketTraitIsVisible = TraitIsVisible; + private module BlanketTraitIsVisible = TraitIsVisible; /** A (potential) non-method call, `f(x)`. */ final class NonMethodCall extends CallExpr { @@ -2037,13 +2132,13 @@ private module NonMethodResolution { } pragma[nomagic] - predicate resolveCallTargetBlanketCandidate( + predicate resolveCallTargetBlanketLikeCandidate( ImplItemNode impl, FunctionPosition pos, TypePath blanketPath, TypeParam blanketTypeParam ) { exists(string name, int arity, Trait trait, AssocFunctionType t | this.hasNameAndArity(name, arity) and exists(this.getTypeAt(pos, blanketPath)) and - functionInfoBlanketRelevantPos(_, name, arity, impl, trait, pos, t, blanketPath, + functionInfoBlanketLikeRelevantPos(_, name, arity, impl, trait, pos, t, blanketPath, blanketTypeParam) and BlanketTraitIsVisible::traitIsVisible(this, trait) ) @@ -2080,7 +2175,7 @@ private module NonMethodResolution { private newtype TCallAndBlanketPos = MkCallAndBlanketPos(NonMethodCall fc, FunctionPosition pos) { - fc.resolveCallTargetBlanketCandidate(_, pos, _, _) + fc.resolveCallTargetBlanketLikeCandidate(_, pos, _, _) } /** A call tagged with a position. */ @@ -2106,7 +2201,7 @@ private module NonMethodResolution { ) { exists(NonMethodCall fc, FunctionPosition pos | fcp = MkCallAndBlanketPos(fc, pos) and - fc.resolveCallTargetBlanketCandidate(impl, pos, blanketPath, blanketTypeParam) + fc.resolveCallTargetBlanketLikeCandidate(impl, pos, blanketPath, blanketTypeParam) ) } } @@ -2129,12 +2224,12 @@ private module NonMethodResolution { exists(FunctionPosition pos | ArgSatisfiesBlanketConstraint::satisfiesBlanketConstraint(fcp, abs) and fcp = MkCallAndBlanketPos(_, pos) and - functionInfoBlanketRelevantPos(_, _, _, abs, _, pos, constraint, _, _) + functionInfoBlanketLikeRelevantPos(_, _, _, abs, _, pos, constraint, _, _) ) } predicate relevantConstraint(AssocFunctionType constraint) { - functionInfoBlanketRelevantPos(_, _, _, _, _, _, constraint, _, _) + functionInfoBlanketLikeRelevantPos(_, _, _, _, _, _, constraint, _, _) } } diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll index 8f2483c3f684..b88424caa349 100644 --- a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll +++ b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll @@ -132,4 +132,17 @@ module SatisfiesBlanketConstraint< SatisfiesBlanketConstraint::satisfiesConstraintType(ato, TTrait(traitBound), _, _) ) } + + /** + * Holds if the argument type `at` does _not_ satisfy the first non-trivial blanket + * constraint of `impl`. + */ + pragma[nomagic] + predicate dissatisfiesBlanketConstraint(ArgumentType at, ImplItemNode impl) { + exists(ArgumentTypeAndBlanketOffset ato, Trait traitBound | + ato = MkArgumentTypeAndBlanketOffset(at, _) and + SatisfiesBlanketConstraintInput::relevantConstraint(ato, impl, traitBound) and + SatisfiesBlanketConstraint::dissatisfiesConstraint(ato, TTrait(traitBound)) + ) + } } diff --git a/rust/ql/test/library-tests/type-inference/blanket_impl.rs b/rust/ql/test/library-tests/type-inference/blanket_impl.rs index 12449efe7d28..49fcd8af0a64 100644 --- a/rust/ql/test/library-tests/type-inference/blanket_impl.rs +++ b/rust/ql/test/library-tests/type-inference/blanket_impl.rs @@ -184,6 +184,85 @@ mod extension_trait_blanket_impl { } } +mod blanket_like_impl { + #[derive(Debug, Copy, Clone)] + struct S1; + + #[derive(Debug, Copy, Clone)] + struct S2; + + trait MyTrait1 { + // MyTrait1::m1 + fn m1(self); + } + + trait MyTrait2 { + // MyTrait2::m2 + fn m2(self); + } + + trait MyTrait3 { + // MyTrait3::m3 + fn m3(self); + } + + trait MyTrait4a { + // MyTrait4a::m4 + fn m4(self); + } + + trait MyTrait4b { + // MyTrait4b::m4 + fn m4(self); + } + + impl MyTrait1 for S1 { + // S1::m1 + fn m1(self) {} + } + + impl MyTrait3 for S1 { + // S1::m3 + fn m3(self) {} + } + + impl MyTrait2 for &T { + // MyTrait2Ref::m2 + fn m2(self) { + self.m1() // $ target=MyTrait1::m1 + } + } + + impl MyTrait2 for &&S1 { + // MyTrait2RefRefS1::m2 + fn m2(self) { + self.m1() // $ MISSING: target=S1::m1 + } + } + + impl MyTrait4a for T { + // MyTrait4aBlanket::m4 + fn m4(self) { + self.m3() // $ target=MyTrait3::m3 + } + } + + impl MyTrait4b for &T { + // MyTrait4bRef::m4 + fn m4(self) {} + } + + pub fn test_basic_blanket() { + let x1 = S1.m1(); // $ target=S1::m1 + let x2 = (&S1).m2(); // $ target=MyTrait2Ref::m2 + let x3 = (&&S1).m2(); // $ target=MyTrait2RefRefS1::m2 + let x4 = S1.m4(); // $ target=MyTrait4aBlanket::m4 + let x5 = (&S1).m4(); // $ target=MyTrait4bRef::m4 + let x6 = S2.m4(); // $ target=MyTrait4bRef::m4 + let x7 = (&S2).m4(); // $ target=MyTrait4bRef::m4 + } +} + pub mod sql_exec { // a highly simplified model of `MySqlConnection.execute` in SQLx 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 170651621c84..76b4afc482f9 100644 --- a/rust/ql/test/library-tests/type-inference/type-inference.expected +++ b/rust/ql/test/library-tests/type-inference/type-inference.expected @@ -207,46 +207,94 @@ inferType | blanket_impl.rs:183:22:183:34 | my_other_flag | | blanket_impl.rs:160:5:162:5 | MyOtherFlag | | blanket_impl.rs:183:22:183:56 | my_other_flag.try_read_flag_twice() | | {EXTERNAL LOCATION} | Option | | blanket_impl.rs:183:22:183:56 | my_other_flag.try_read_flag_twice() | T | {EXTERNAL LOCATION} | bool | -| blanket_impl.rs:193:21:193:25 | SelfParam | | file://:0:0:0:0 | & | -| blanket_impl.rs:193:21:193:25 | SelfParam | &T | blanket_impl.rs:192:5:195:5 | Self [trait Executor] | -| blanket_impl.rs:194:24:194:28 | SelfParam | | file://:0:0:0:0 | & | -| blanket_impl.rs:194:24:194:28 | SelfParam | &T | blanket_impl.rs:192:5:195:5 | Self [trait Executor] | -| blanket_impl.rs:194:31:194:35 | query | | blanket_impl.rs:194:21:194:21 | E | -| blanket_impl.rs:198:21:198:25 | SelfParam | | file://:0:0:0:0 | & | -| blanket_impl.rs:198:21:198:25 | SelfParam | &T | blanket_impl.rs:197:10:197:22 | T | -| blanket_impl.rs:199:22:199:41 | "Executor::execute1\\n" | | file://:0:0:0:0 | & | -| blanket_impl.rs:199:22:199:41 | "Executor::execute1\\n" | &T | {EXTERNAL LOCATION} | str | -| blanket_impl.rs:199:22:199:41 | FormatArgsExpr | | {EXTERNAL LOCATION} | Arguments | -| blanket_impl.rs:199:22:199:41 | MacroExpr | | {EXTERNAL LOCATION} | Arguments | -| blanket_impl.rs:202:24:202:28 | SelfParam | | file://:0:0:0:0 | & | -| blanket_impl.rs:202:24:202:28 | SelfParam | &T | blanket_impl.rs:197:10:197:22 | T | -| blanket_impl.rs:202:31:202:36 | _query | | blanket_impl.rs:202:21:202:21 | E | -| blanket_impl.rs:203:22:203:41 | "Executor::execute2\\n" | | file://:0:0:0:0 | & | -| blanket_impl.rs:203:22:203:41 | "Executor::execute2\\n" | &T | {EXTERNAL LOCATION} | str | -| blanket_impl.rs:203:22:203:41 | FormatArgsExpr | | {EXTERNAL LOCATION} | Arguments | -| blanket_impl.rs:203:22:203:41 | MacroExpr | | {EXTERNAL LOCATION} | Arguments | -| blanket_impl.rs:212:13:212:13 | c | | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:212:17:212:34 | MySqlConnection {...} | | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:214:9:214:9 | c | | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:215:35:215:36 | &c | | file://:0:0:0:0 | & | -| blanket_impl.rs:215:35:215:36 | &c | &T | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:215:36:215:36 | c | | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:217:9:217:9 | c | | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:217:20:217:40 | "SELECT * FROM users" | | file://:0:0:0:0 | & | -| blanket_impl.rs:217:20:217:40 | "SELECT * FROM users" | &T | {EXTERNAL LOCATION} | str | -| blanket_impl.rs:218:9:218:9 | c | | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:218:28:218:48 | "SELECT * FROM users" | | file://:0:0:0:0 | & | -| blanket_impl.rs:218:28:218:48 | "SELECT * FROM users" | &T | {EXTERNAL LOCATION} | str | -| blanket_impl.rs:219:35:219:36 | &c | | file://:0:0:0:0 | & | -| blanket_impl.rs:219:35:219:36 | &c | &T | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:219:36:219:36 | c | | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:219:39:219:59 | "SELECT * FROM users" | | file://:0:0:0:0 | & | -| blanket_impl.rs:219:39:219:59 | "SELECT * FROM users" | &T | {EXTERNAL LOCATION} | str | -| blanket_impl.rs:220:43:220:44 | &c | | file://:0:0:0:0 | & | -| blanket_impl.rs:220:43:220:44 | &c | &T | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:220:44:220:44 | c | | blanket_impl.rs:207:5:207:29 | MySqlConnection | -| blanket_impl.rs:220:47:220:67 | "SELECT * FROM users" | | file://:0:0:0:0 | & | -| blanket_impl.rs:220:47:220:67 | "SELECT * FROM users" | &T | {EXTERNAL LOCATION} | str | +| blanket_impl.rs:196:15:196:18 | SelfParam | | blanket_impl.rs:194:5:197:5 | Self [trait MyTrait1] | +| blanket_impl.rs:201:15:201:18 | SelfParam | | blanket_impl.rs:199:5:202:5 | Self [trait MyTrait2] | +| blanket_impl.rs:206:15:206:18 | SelfParam | | blanket_impl.rs:204:5:207:5 | Self [trait MyTrait3] | +| blanket_impl.rs:211:15:211:18 | SelfParam | | blanket_impl.rs:209:5:212:5 | Self [trait MyTrait4a] | +| blanket_impl.rs:216:15:216:18 | SelfParam | | blanket_impl.rs:214:5:217:5 | Self [trait MyTrait4b] | +| blanket_impl.rs:221:15:221:18 | SelfParam | | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:226:15:226:18 | SelfParam | | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:231:15:231:18 | SelfParam | | file://:0:0:0:0 | & | +| blanket_impl.rs:231:15:231:18 | SelfParam | &T | blanket_impl.rs:229:10:229:27 | T | +| blanket_impl.rs:232:13:232:16 | self | | file://:0:0:0:0 | & | +| blanket_impl.rs:232:13:232:16 | self | &T | blanket_impl.rs:229:10:229:27 | T | +| blanket_impl.rs:238:15:238:18 | SelfParam | | file://:0:0:0:0 | & | +| blanket_impl.rs:238:15:238:18 | SelfParam | &T | file://:0:0:0:0 | & | +| blanket_impl.rs:238:15:238:18 | SelfParam | &T.&T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:239:13:239:16 | self | | file://:0:0:0:0 | & | +| blanket_impl.rs:239:13:239:16 | self | &T | file://:0:0:0:0 | & | +| blanket_impl.rs:239:13:239:16 | self | &T.&T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:245:15:245:18 | SelfParam | | blanket_impl.rs:243:10:243:20 | T | +| blanket_impl.rs:246:13:246:16 | self | | blanket_impl.rs:243:10:243:20 | T | +| blanket_impl.rs:252:15:252:18 | SelfParam | | file://:0:0:0:0 | & | +| blanket_impl.rs:252:15:252:18 | SelfParam | &T | blanket_impl.rs:250:10:250:10 | T | +| blanket_impl.rs:256:18:256:19 | S1 | | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:257:18:257:22 | (...) | | file://:0:0:0:0 | & | +| blanket_impl.rs:257:18:257:22 | (...) | &T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:257:19:257:21 | &S1 | | file://:0:0:0:0 | & | +| blanket_impl.rs:257:19:257:21 | &S1 | &T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:257:20:257:21 | S1 | | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:258:18:258:23 | (...) | | file://:0:0:0:0 | & | +| blanket_impl.rs:258:18:258:23 | (...) | &T | file://:0:0:0:0 | & | +| blanket_impl.rs:258:18:258:23 | (...) | &T.&T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:258:19:258:22 | &... | | file://:0:0:0:0 | & | +| blanket_impl.rs:258:19:258:22 | &... | &T | file://:0:0:0:0 | & | +| blanket_impl.rs:258:19:258:22 | &... | &T.&T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:258:20:258:22 | &S1 | | file://:0:0:0:0 | & | +| blanket_impl.rs:258:20:258:22 | &S1 | &T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:258:21:258:22 | S1 | | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:259:18:259:19 | S1 | | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:260:18:260:22 | (...) | | file://:0:0:0:0 | & | +| blanket_impl.rs:260:18:260:22 | (...) | &T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:260:19:260:21 | &S1 | | file://:0:0:0:0 | & | +| blanket_impl.rs:260:19:260:21 | &S1 | &T | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:260:20:260:21 | S1 | | blanket_impl.rs:188:5:189:14 | S1 | +| blanket_impl.rs:261:18:261:19 | S2 | | blanket_impl.rs:191:5:192:14 | S2 | +| blanket_impl.rs:262:18:262:22 | (...) | | file://:0:0:0:0 | & | +| blanket_impl.rs:262:18:262:22 | (...) | &T | blanket_impl.rs:191:5:192:14 | S2 | +| blanket_impl.rs:262:19:262:21 | &S2 | | file://:0:0:0:0 | & | +| blanket_impl.rs:262:19:262:21 | &S2 | &T | blanket_impl.rs:191:5:192:14 | S2 | +| blanket_impl.rs:262:20:262:21 | S2 | | blanket_impl.rs:191:5:192:14 | S2 | +| blanket_impl.rs:272:21:272:25 | SelfParam | | file://:0:0:0:0 | & | +| blanket_impl.rs:272:21:272:25 | SelfParam | &T | blanket_impl.rs:271:5:274:5 | Self [trait Executor] | +| blanket_impl.rs:273:24:273:28 | SelfParam | | file://:0:0:0:0 | & | +| blanket_impl.rs:273:24:273:28 | SelfParam | &T | blanket_impl.rs:271:5:274:5 | Self [trait Executor] | +| blanket_impl.rs:273:31:273:35 | query | | blanket_impl.rs:273:21:273:21 | E | +| blanket_impl.rs:277:21:277:25 | SelfParam | | file://:0:0:0:0 | & | +| blanket_impl.rs:277:21:277:25 | SelfParam | &T | blanket_impl.rs:276:10:276:22 | T | +| blanket_impl.rs:278:22:278:41 | "Executor::execute1\\n" | | file://:0:0:0:0 | & | +| blanket_impl.rs:278:22:278:41 | "Executor::execute1\\n" | &T | {EXTERNAL LOCATION} | str | +| blanket_impl.rs:278:22:278:41 | FormatArgsExpr | | {EXTERNAL LOCATION} | Arguments | +| blanket_impl.rs:278:22:278:41 | MacroExpr | | {EXTERNAL LOCATION} | Arguments | +| blanket_impl.rs:281:24:281:28 | SelfParam | | file://:0:0:0:0 | & | +| blanket_impl.rs:281:24:281:28 | SelfParam | &T | blanket_impl.rs:276:10:276:22 | T | +| blanket_impl.rs:281:31:281:36 | _query | | blanket_impl.rs:281:21:281:21 | E | +| blanket_impl.rs:282:22:282:41 | "Executor::execute2\\n" | | file://:0:0:0:0 | & | +| blanket_impl.rs:282:22:282:41 | "Executor::execute2\\n" | &T | {EXTERNAL LOCATION} | str | +| blanket_impl.rs:282:22:282:41 | FormatArgsExpr | | {EXTERNAL LOCATION} | Arguments | +| blanket_impl.rs:282:22:282:41 | MacroExpr | | {EXTERNAL LOCATION} | Arguments | +| blanket_impl.rs:291:13:291:13 | c | | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:291:17:291:34 | MySqlConnection {...} | | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:293:9:293:9 | c | | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:294:35:294:36 | &c | | file://:0:0:0:0 | & | +| blanket_impl.rs:294:35:294:36 | &c | &T | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:294:36:294:36 | c | | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:296:9:296:9 | c | | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:296:20:296:40 | "SELECT * FROM users" | | file://:0:0:0:0 | & | +| blanket_impl.rs:296:20:296:40 | "SELECT * FROM users" | &T | {EXTERNAL LOCATION} | str | +| blanket_impl.rs:297:9:297:9 | c | | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:297:28:297:48 | "SELECT * FROM users" | | file://:0:0:0:0 | & | +| blanket_impl.rs:297:28:297:48 | "SELECT * FROM users" | &T | {EXTERNAL LOCATION} | str | +| blanket_impl.rs:298:35:298:36 | &c | | file://:0:0:0:0 | & | +| blanket_impl.rs:298:35:298:36 | &c | &T | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:298:36:298:36 | c | | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:298:39:298:59 | "SELECT * FROM users" | | file://:0:0:0:0 | & | +| blanket_impl.rs:298:39:298:59 | "SELECT * FROM users" | &T | {EXTERNAL LOCATION} | str | +| blanket_impl.rs:299:43:299:44 | &c | | file://:0:0:0:0 | & | +| blanket_impl.rs:299:43:299:44 | &c | &T | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:299:44:299:44 | c | | blanket_impl.rs:286:5:286:29 | MySqlConnection | +| blanket_impl.rs:299:47:299:67 | "SELECT * FROM users" | | file://:0:0:0:0 | & | +| blanket_impl.rs:299:47:299:67 | "SELECT * FROM users" | &T | {EXTERNAL LOCATION} | str | | closure.rs:6:13:6:22 | my_closure | | {EXTERNAL LOCATION} | dyn FnOnce | | closure.rs:6:13:6:22 | my_closure | dyn(Args) | file://:0:0:0:0 | (T_2) | | closure.rs:6:13:6:22 | my_closure | dyn(Args).0(2) | {EXTERNAL LOCATION} | bool | diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index ff9ccf3c192b..94f227c3a9ad 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -704,14 +704,26 @@ module Make1 Input1> { /** * Holds if `app` is _not_ a possible instantiation of `constraint`. + * + * This is an approximation of `not isInstantiationOf(app, abs, constraint)`, but + * defined without a negative occurrence of `isInstantiationOf`. + * + * Due to the approximation, both `isInstantiationOf` and `isNotInstantiationOf` + * can hold for the same values. For example, if `app` has two different types `t1` + * and `t2` at the same type path, and `t1` satisfies `constraint` while `t2` does + * not, then both `isInstantiationOf` and `isNotInstantiationOf` will hold. + * + * Dually, if `app` does not have a type at a required type path, then neither + * `isInstantiationOf` nor `isNotInstantiationOf` will hold. */ pragma[nomagic] predicate isNotInstantiationOf(App app, TypeAbstraction abs, Constraint constraint) { // `app` and `constraint` differ on a concrete type - exists(Type t, TypePath path | + exists(Type t, Type t2, TypePath path | t = resolveTypeAt(app, abs, constraint, path) and not t = abs.getATypeParameter() and - app.getTypeAt(path) != t + app.getTypeAt(path) = t2 and + t2 != t ) } } @@ -793,7 +805,7 @@ module Make1 Input1> { } /** - * Holds if its possible for a type with `conditionRoot` at the root to + * Holds if it's possible for a type with `conditionRoot` at the root to * satisfy a constraint with `constraintRoot` at the root through `abs`, * `condition`, and `constraint`. */ @@ -997,6 +1009,42 @@ module Make1 Input1> { ) } + /** + * Holds if `tt` does not satisfy `constraint`. + * + * 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) | + ( + not useUniversalConditions() + or + exists(countConstraintImplementations(type, constraint)) + or + forall(TypeAbstraction abs, TypeMention condition, TypeMention constraintMention | + conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and + resolveTypeMentionRoot(condition) = abs.getATypeParameter() + | + not constraint = resolveTypeMentionRoot(constraintMention) + ) + ) and + ( + countConstraintImplementations(type, constraint) = 0 + or + not rootTypesSatisfaction(type, constraint, _, _, _) + or + multipleConstraintImplementations(type, constraint) and + forex(TypeAbstraction abs, TypeMention condition | + rootTypesSatisfaction(type, constraint, abs, condition, _) + | + IsInstantiationOf::isNotInstantiationOf(tt, + abs, condition) + ) + ) + ) + } + pragma[nomagic] private predicate satisfiesConstraintTypeMention0( HasTypeTree tt, Type constraint, TypeAbstraction abs, TypeMention sub, TypePath path, Type t @@ -1038,6 +1086,29 @@ module Make1 Input1> { hasTypeConstraint(tt, constraint, constraint) and t = tt.getTypeAt(path) } + + /** + * Holds if the type tree at `tt` does _not_ satisfy the constraint `constraint`. + * + * This is an approximation of `not satisfiesConstraintType(tt, constraint, _, _)`, + * but defined without a negative occurrence of `satisfiesConstraintType`. + * + * Due to the approximation, both `satisfiesConstraintType` and `dissatisfiesConstraint` + * can hold for the same values. For example, if `tt` has two different types `t1` + * and `t2`, and `t1` satisfies `constraint` while `t2` does not, then both + * `satisfiesConstraintType` and `dissatisfiesConstraint` will hold. + * + * Dually, if `tt` does not have a type, then neither `satisfiesConstraintType` nor + * `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 + ) + } } /** Provides the input to `MatchingWithEnvironment`. */