hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-16 16:53:25 +01:00
Code Issues Packages Projects Releases Wiki Activity

Address review comments

Browse Source
This commit is contained in:
Tom Hvitved
2025-10-28 11:48:45 +01:00
parent 0e885e9297
commit 409f7fb743
3 changed files with 21 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
rust/ql/lib/codeql/rust/internal/TypeInference.qll
View File

@@ -1230,7 +1230,7 @@ private module MethodResolution {
ReceiverIsNotInstantiationOfBlanketLikeSelfParam::argIsNotInstantiationOf(MkMethodCallCand(this,
derefChain, borrow), impl, _)
or
ReceiverSatisfiesBlanketLikeConstraint::satisfiesNotBlanketConstraint(MkMethodCallCand(this,
ReceiverSatisfiesBlanketLikeConstraint::dissatisfiesBlanketConstraint(MkMethodCallCand(this,
derefChain, borrow), impl)
}

4
rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll
View File

@@ -138,11 +138,11 @@ module SatisfiesBlanketConstraint<
* constraint of `impl`.
*/
pragma[nomagic]
predicate satisfiesNotBlanketConstraint(ArgumentType at, ImplItemNode impl) {
predicate dissatisfiesBlanketConstraint(ArgumentType at, ImplItemNode impl) {
exists(ArgumentTypeAndBlanketOffset ato, Trait traitBound |
ato = MkArgumentTypeAndBlanketOffset(at, _) and
SatisfiesBlanketConstraintInput::relevantConstraint(ato, impl, traitBound) and
SatisfiesBlanketConstraint::satisfiesNotConstraint(ato, TTrait(traitBound))
SatisfiesBlanketConstraint::dissatisfiesConstraint(ato, TTrait(traitBound))
)
}
}

28
shared/typeinference/codeql/typeinference/internal/TypeInference.qll
View File

@@ -705,10 +705,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
/**
* Holds if `app` is _not_ a possible instantiation of `constraint`.
*
* This is a monotonic approximation of `not isInstantiationOf(app, abs, constraint)`;
* if, for example, `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.
* 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.
@@ -1008,6 +1011,8 @@ module Make1<LocationSig Location, InputSig1<Location> 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) {
@@ -1085,16 +1090,19 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
/**
* Holds if the type tree at `tt` does _not_ satisfy the constraint `constraint`.
*
* This is a monotonic approximation of `not satisfiesConstraintType(tt, constraint, _, _)`;
* if, for example, `tt` has two different types `t1` and `t2`, and `t1` satisfies
* `constraint` while `t2` does not, then both `satisfiesConstraintType` and
* `satisfiesNotConstraint` will hold.
* 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
* `satisfiesNotConstraint` will hold.
* `dissatisfiesConstraint` will hold.
*/
pragma[nomagic]
predicate satisfiesNotConstraint(HasTypeTree tt, Type constraint) {
predicate dissatisfiesConstraint(HasTypeTree tt, Type constraint) {
hasNotConstraintMention(tt, constraint) and
exists(Type t |
hasTypeConstraint(tt, t, constraint) and