Skip to content

Rust: Use doublyBoundedFastTC in TraitIsVisible #20362

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
hvitved wants to merge 1 commit into from
Closed

Rust: Use doublyBoundedFastTC in TraitIsVisible #20362

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
54 changes: 43 additions & 11 deletions rust/ql/lib/codeql/rust/internal/PathResolution.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1425,24 +1425,56 @@ signature predicate relevantTraitVisibleSig(Element element, Trait trait);
* at a given element.
*/
module TraitIsVisible<relevantTraitVisibleSig/2 relevantTraitVisible> {
/** Holds if the trait might be looked up in `encl`. */
private predicate traitLookup(ItemNode encl, Element element, Trait trait) {
// lookup in immediately enclosing item
relevantTraitVisible(element, trait) and
encl.getADescendant() = element
private newtype TNode =
TTrait(Trait t) { relevantTraitVisible(_, t) } or
TItemNode(ItemNode i) or
TElement(Element e) { relevantTraitVisible(e, _) }

private predicate isTrait(TNode n) { n instanceof TTrait }

private predicate step(TNode n1, TNode n2) {
exists(Trait t1, ItemNode i2 |
n1 = TTrait(t1) and
n2 = TItemNode(i2) and
t1 = i2.getASuccessor(_, _)
Comment on lines +1436 to +1439
Copy link

Copilot AI Sep 4, 2025

Choose a reason for hiding this comment

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

The getASuccessor call is missing the required name parameter. Based on the context, this should be t1 = i2.getASuccessor(_, _) where the first underscore represents the name parameter.

Suggested change
exists(Trait t1, ItemNode i2 |
n1 = TTrait(t1) and
n2 = TItemNode(i2) and
t1 = i2.getASuccessor(_, _)
exists(Trait t1, ItemNode i2, string name |
n1 = TTrait(t1) and
n2 = TItemNode(i2) and
t1 = i2.getASuccessor(name, _)

Copilot uses AI. Check for mistakes.
)
or
// lookup in an outer scope, but only if the trait is not declared in inner scope
exists(ItemNode mid |
traitLookup(mid, element, trait) and
not trait = mid.getASuccessor(_, _) and
encl = getOuterScope(mid)
exists(ItemNode i1, ItemNode i2 |
n1 = TItemNode(i1) and
n2 = TItemNode(i2) and
i1 = getOuterScope(i2)
Copy link

Copilot AI Sep 4, 2025

Choose a reason for hiding this comment

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

The direction of the relationship appears reversed. Based on the original traitLookup logic, this should be i2 = getOuterScope(i1) to represent moving from an inner scope to an outer scope.

Suggested change
i1 = getOuterScope(i2)
i2 = getOuterScope(i1)

Copilot uses AI. Check for mistakes.
)
or
exists(ItemNode i1, Element e2 |
n1 = TItemNode(i1) and
n2 = TElement(e2) and
i1.getADescendant() = e2
)
}

private predicate isElement(TNode n) { n instanceof TElement }

private predicate traitIsVisibleTC(TNode trait, TNode element) =
doublyBoundedFastTC(step/2, isTrait/1, isElement/1)(trait, element)

pragma[nomagic]
private predicate relevantTraitVisibleLift(TNode trait, TElement element) {
exists(Trait t, Element e |
trait = TTrait(t) and
element = TElement(e) and
relevantTraitVisible(e, t)
)
}

/** Holds if the trait `trait` is visible at `element`. */
pragma[nomagic]
predicate traitIsVisible(Element element, Trait trait) {
exists(ItemNode encl | traitLookup(encl, element, trait) and trait = encl.getASuccessor(_, _))
exists(TNode t, TNode e |
traitIsVisibleTC(t, e) and
relevantTraitVisibleLift(t, e) and
t = TTrait(trait) and
e = TElement(element)
)
}
}

Expand Down