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

Shared, Rust: Reuse hasTypeConstraint in potentialInstantiationOf and factor out multipleConstraintImplementations

Browse Source
This commit is contained in:
Simon Friis Vindum
2025-07-17 14:28:04 +02:00
parent bdcecdfc2c
commit 43b2977cb4
1 changed files with 18 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -796,6 +796,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
) )
} }
/**
* Holds if there is multiple ways in which a type with `conditionRoot` at
* the root can satisfy a constraint with `constraintRoot` at the root.
*/
predicate multipleConstraintImplementations(Type conditionRoot, Type constraintRoot) {
countConstraintImplementations(conditionRoot, constraintRoot) > 1
}
/** /**
* Holds if `baseMention` is a (transitive) base type mention of `sub`, * Holds if `baseMention` is a (transitive) base type mention of `sub`,
* and `t` is mentioned (implicitly) at `path` inside `baseMention`. For * and `t` is mentioned (implicitly) at `path` inside `baseMention`. For
@@ -902,14 +910,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
{ {
private import Input private import Input
/** Holds if the type tree has the type `type` and should satisfy `constraint`. */
pragma[nomagic]
private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) {
type = term.getTypeAt(TypePath::nil()) and
relevantConstraint(term, constraint)
}
private module IsInstantiationOfInput implements IsInstantiationOfInputSig<HasTypeTree> { private module IsInstantiationOfInput implements IsInstantiationOfInputSig<HasTypeTree> {
predicate potentialInstantiationOf(HasTypeTree tt, TypeAbstraction abs, TypeMention cond) { predicate potentialInstantiationOf(HasTypeTree tt, TypeAbstraction abs, TypeMention cond) {
exists(Type constraint, Type type | exists(Type constraint, Type type |
type = tt.getTypeAt(TypePath::nil()) and hasTypeConstraint(tt, type, constraint) and
relevantConstraint(tt, constraint) and
rootTypesSatisfaction(type, constraint, abs, cond, _) and rootTypesSatisfaction(type, constraint, abs, cond, _) and
// We only need to check instantiations where there are multiple candidates. // We only need to check instantiations where there are multiple candidates.
countConstraintImplementations(type, constraint) > 1 multipleConstraintImplementations(type, constraint)
) )
} }
@@ -918,13 +932,6 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
} }
} }
/** Holds if the type tree has the type `type` and should satisfy `constraint`. */
pragma[nomagic]
private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) {
type = term.getTypeAt(TypePath::nil()) and
relevantConstraint(term, constraint)
}
/** /**
* Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`. * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
*/ */
@@ -944,7 +951,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
// When there are multiple ways the type could implement the // When there are multiple ways the type could implement the
// constraint we need to find the right implementation, which is the // constraint we need to find the right implementation, which is the
// one where the type instantiates the precondition. // one where the type instantiates the precondition.
if countConstraintImplementations(type, constraint) > 1 if multipleConstraintImplementations(type, constraint)
then then
IsInstantiationOf<HasTypeTree, IsInstantiationOfInput>::isInstantiationOf(tt, abs, sub) IsInstantiationOf<HasTypeTree, IsInstantiationOfInput>::isInstantiationOf(tt, abs, sub)
else any() else any()