Don't include arg -> param edges in PathGraph::edges where arg is not reachable #7526
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ot reachable This avoids lots of missing-node warnings from `codeql bqrs interpret` as it discards the nodes that occur in the `edges` relation but not `nodes`. The problem arises because subpaths introduced two variants of `reach`, one of which is more restrictive than simply `reach(succ) and succ = pred.getASuccessor()`, so it no longer suffices to just check that the successor is reachable.
hvitved
reviewed
Jan 6, 2022
| @@ -3416,7 +3416,7 @@ private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1 | ||
| */ | ||
| module PathGraph { | ||
| /** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */ | ||
| query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(b) } | ||
| query predicate edges(PathNode a, PathNode b) { a.getASuccessor() = b and reach(a) and reach(b) } |
There was a problem hiding this comment.
I wonder if we shouldn't restrict sub path nodes to those that can reach a sink as well. I.e., redefine retReach as
predicate retReach(PathNode n) {
exists(PathNodeMid out |
subpaths(_, _, n, out) and
reach(out)
)
or
exists(PathNode mid |
retReach(mid) and
n.getASuccessor() = mid and
not subpaths(_, mid, _, _)
)
}@aschackmull : What do you think?
There was a problem hiding this comment.
That makes sense, although I think I'd prefer
predicate retReach(PathNode n) {
exists(PathNodeMid out |
subpaths(_, _, n, out)
|
directReach(out) or retReach(out)
)
or
exists(PathNode mid |
retReach(mid) and
n.getASuccessor() = mid and
not subpaths(_, mid, _, _)
)
}to avoid making it mutually recursive with reach.
There was a problem hiding this comment.
We might also want to restrict the final subpaths relation if we want to get rid of the Skipping subpaths tuple with missing node warnings.
There was a problem hiding this comment.
Yes, we should certainly also restrict subpaths.
|
The changes to the |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
This avoids lots of missing-node warnings from
codeql bqrs interpretas it discards the nodes that occur in theedgesrelation but notnodes. The problem arises because subpaths introduced two variants ofreach, one of which is more restrictive than simplyreach(succ) and succ = pred.getASuccessor(), so it no longer suffices to just check that the successor is reachable.Suggestions re: the best way to test this welcome.
The text was updated successfully, but these errors were encountered: