Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 12 additions & 2 deletions rust/ql/lib/codeql/rust/internal/PathResolution.qll
Original file line number Diff line number Diff line change
Expand Up @@ -607,6 +607,9 @@ class ImplItemNode extends ImplOrTraitItemNode instanceof Impl {
result = this.resolveTraitTy().getCanonicalPath(c)
}

pragma[nomagic]
private string getSelfCanonicalPath(Crate c) { result = this.resolveSelfTy().getCanonicalPath(c) }

pragma[nomagic]
private string getCanonicalPathTraitPart(Crate c) {
exists(Crate c2 |
Expand All @@ -621,7 +624,7 @@ class ImplItemNode extends ImplOrTraitItemNode instanceof Impl {
result = "<"
or
i = 1 and
result = this.resolveSelfTy().getCanonicalPath(c)
result = this.getSelfCanonicalPath(c)
or
if exists(this.getTraitPath())
then
Expand Down Expand Up @@ -985,6 +988,7 @@ private predicate sourceFileEdge(SourceFile f, string name, ItemNode item) {
}

/** Holds if `f` is available as `mod name;` inside `folder`. */
pragma[nomagic]
private predicate fileModule(SourceFile f, string name, Folder folder) {
exists(File file | file = f.getFile() |
file.getBaseName() = name + ".rs" and
Expand All @@ -999,6 +1003,12 @@ private predicate fileModule(SourceFile f, string name, Folder folder) {
)
}

bindingset[name, folder]
pragma[inline_late]
private predicate fileModuleInlineLate(SourceFile f, string name, Folder folder) {
fileModule(f, name, folder)
}

/**
* Gets the `Meta` of the module `m`'s [path attribute][1].
*
Expand Down Expand Up @@ -1081,7 +1091,7 @@ pragma[nomagic]
predicate fileImport(Module m, SourceFile f) {
exists(string name, Folder parent |
modImport0(m, name, _) and
fileModule(f, name, parent)
fileModuleInlineLate(f, name, parent)
|
// `m` is not inside a nested module
modImport0(m, name, parent) and
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -423,27 +423,23 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
)
}

/**
* Holds if `app` is a possible instantiation of `tm` at `path`. That is
* the type at `path` in `tm` is either a type parameter or equal to the
* type at the same path in `app`.
*/
bindingset[app, abs, tm, path]
private predicate satisfiesConcreteTypeAt(
App app, TypeAbstraction abs, TypeMention tm, TypePath path
pragma[nomagic]
private Type resolveNthTypeAt(
App app, TypeAbstraction abs, TypeMention tm, int i, TypePath path
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this not a "big" relation to nomagic? It joins all the apps with the paths of all related type mentions. I would've thought it should be late inlined or something of that sort?

) {
exists(Type t |
tm.resolveTypeAt(path) = t and
if t = abs.getATypeParameter() then any() else app.getTypeAt(path) = t
)
potentialInstantiationOf(app, abs, tm) and
path = getNthPath(tm, i) and
result = tm.resolveTypeAt(path)
}

pragma[nomagic]
private predicate satisfiesConcreteTypesFromIndex(
App app, TypeAbstraction abs, TypeMention tm, int i
) {
potentialInstantiationOf(app, abs, tm) and
satisfiesConcreteTypeAt(app, abs, tm, getNthPath(tm, i)) and
exists(Type t, TypePath path |
t = resolveNthTypeAt(app, abs, tm, i, path) and
if t = abs.getATypeParameter() then any() else app.getTypeAt(path) = t
) and
// Recurse unless we are at the first path
if i = 0 then any() else satisfiesConcreteTypesFromIndex(app, abs, tm, i - 1)
}
Expand All @@ -467,24 +463,34 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
* Gets the path to the `i`th occurrence of `tp` within `tm` per some
* arbitrary order, if any.
*/
pragma[nomagic]
private TypePath getNthTypeParameterPath(TypeMention tm, TypeParameter tp, int i) {
result =
rank[i + 1](TypePath path | tp = tm.resolveTypeAt(path) and relevantTypeMention(tm) | path)
}

pragma[nomagic]
private predicate typeParametersEqualFromIndexBase(
App app, TypeAbstraction abs, TypeMention tm, TypeParameter tp, TypePath path
) {
path = getNthTypeParameterPath(tm, tp, 0) and
satisfiesConcreteTypes(app, abs, tm) and
// no need to compute this predicate if there is only one path
exists(getNthTypeParameterPath(tm, tp, 1))
}

pragma[nomagic]
private predicate typeParametersEqualFromIndex(
App app, TypeAbstraction abs, TypeMention tm, TypeParameter tp, Type t, int i
) {
satisfiesConcreteTypes(app, abs, tm) and
exists(TypePath path |
path = getNthTypeParameterPath(tm, tp, i) and
t = app.getTypeAt(path) and
if i = 0
then
// no need to compute this predicate if there is only one path
exists(getNthTypeParameterPath(tm, tp, 1))
else typeParametersEqualFromIndex(app, abs, tm, tp, t, i - 1)
then typeParametersEqualFromIndexBase(app, abs, tm, tp, path)
else (
typeParametersEqualFromIndex(app, abs, tm, tp, t, i - 1) and
path = getNthTypeParameterPath(tm, tp, i)
)
)
}

Expand Down Expand Up @@ -1040,6 +1046,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
/**
* Holds if `at` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
*/
pragma[nomagic]
private predicate hasConstraintMention(
RelevantAccess at, TypeAbstraction abs, TypeMention sub, Type constraint,
TypeMention constraintMention
Expand All @@ -1063,6 +1070,30 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
)
}

pragma[nomagic]
predicate satisfiesConstraintTypeMention0(
RelevantAccess at, Access a, AccessPosition apos, TypePath prefix, Type constraint,
TypeAbstraction abs, TypeMention sub, TypePath path, Type t
) {
exists(TypeMention constraintMention |
at = MkRelevantAccess(a, apos, prefix) and
hasConstraintMention(at, abs, sub, constraint, constraintMention) and
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
)
}

pragma[nomagic]
predicate satisfiesConstraintTypeMention1(
RelevantAccess at, Access a, AccessPosition apos, TypePath prefix, Type constraint,
TypePath path, TypePath pathToTypeParamInSub
) {
exists(TypeAbstraction abs, TypeMention sub, TypeParameter tp |
satisfiesConstraintTypeMention0(at, a, apos, prefix, constraint, abs, sub, path, tp) and
tp = abs.getATypeParameter() and
sub.resolveTypeAt(pathToTypeParamInSub) = tp
)
}

/**
* Holds if the type at `a`, `apos`, and `path` satisfies the constraint
* `constraint` with the type `t` at `path`.
Expand All @@ -1071,22 +1102,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
predicate satisfiesConstraintTypeMention(
Access a, AccessPosition apos, TypePath prefix, Type constraint, TypePath path, Type t
) {
exists(TypeAbstraction abs |
satisfiesConstraintTypeMention0(_, a, apos, prefix, constraint, abs, _, path, t) and
not t = abs.getATypeParameter()
)
or
exists(
RelevantAccess at, TypeAbstraction abs, TypeMention sub, Type t0, TypePath prefix0,
TypeMention constraintMention
RelevantAccess at, TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix
|
at = MkRelevantAccess(a, apos, prefix) and
hasConstraintMention(at, abs, sub, constraint, constraintMention) and
conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, prefix0, t0)
|
not t0 = abs.getATypeParameter() and t = t0 and path = prefix0
or
t0 = abs.getATypeParameter() and
exists(TypePath path3, TypePath suffix |
sub.resolveTypeAt(path3) = t0 and
at.getTypeAt(path3.appendInverse(suffix)) = t and
path = prefix0.append(suffix)
)
satisfiesConstraintTypeMention1(at, a, apos, prefix, constraint, prefix0,
pathToTypeParamInSub) and
at.getTypeAt(pathToTypeParamInSub.appendInverse(suffix)) = t and
path = prefix0.append(suffix)
)
}
}
Expand Down Expand Up @@ -1289,14 +1316,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
exists(DeclarationPosition dpos | accessDeclarationPositionMatch(apos, dpos) |
// A suffix of `path` leads to a type parameter in the target
exists(Declaration target, TypePath prefix, TypeParameter tp, TypePath suffix |
tp = target.getDeclaredType(pragma[only_bind_into](dpos), prefix) and
tp = target.getDeclaredType(dpos, prefix) and
path = prefix.append(suffix) and
typeMatch(a, target, suffix, result, tp)
)
or
// `path` corresponds directly to a concrete type in the declaration
exists(Declaration target |
result = target.getDeclaredType(pragma[only_bind_into](dpos), path) and
result = target.getDeclaredType(dpos, path) and
target = a.getTarget() and
not result instanceof TypeParameter
)
Expand Down
Loading