Shared: Ensure subpath-induced edges are handled properly

Argument-passing and flow-through edges are present in 'edges' in addition to 'subpaths', but the implementation didn't take this into account.
This commit is contained in:
Asger F
2024-12-16 13:21:43 +01:00
parent 0edb30638a
commit f2968f4e14
2 changed files with 10 additions and 5 deletions

View File

@@ -47,9 +47,10 @@ predicate reachableFromPropagate(Graph::PathNode node, string state, boolean cal
node.getNode().asExpr() = propagateCall(state) and call = false node.getNode().asExpr() = propagateCall(state) and call = false
or or
exists(Graph::PathNode prev | reachableFromPropagate(prev, state, call) | exists(Graph::PathNode prev | reachableFromPropagate(prev, state, call) |
Graph::edges(prev, node, _, _) Graph::edges(prev, node, _, _) and
not Graph::subpaths(prev, node, _, _) // argument-passing edges are handled separately
or or
Graph::subpaths(prev, _, _, node) // arg -> out Graph::subpaths(prev, _, _, node) // arg -> out (should be included in 'edges' but handle the case here for clarity)
) )
or or
exists(Graph::PathNode prev | exists(Graph::PathNode prev |

View File

@@ -935,11 +935,15 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
) )
} }
/** Gets a successor of `node` including subpath flow-through. */ /** Gets a successor of `node`, including subpath flow-through, but not enter or exit subpath steps. */
InputPathNode stepEx(InputPathNode node) { InputPathNode stepEx(InputPathNode node) {
step(node, result, _, _) step(node, result, _, _) and
not result = enterSubpathStep(node) and
not result = exitSubpathStep(node)
or or
subpathStep(node, _, _, result) // assuming the input is pruned properly, all subpaths have flow-through // Assuming the input is pruned properly, all subpaths have flow-through.
// This step should be in 'step' as well, but include it here for clarity as we rely on it.
subpathStep(node, _, _, result)
} }
InputPathNode enterSubpathStep(InputPathNode node) { subpathStep(node, result, _, _) } InputPathNode enterSubpathStep(InputPathNode node) { subpathStep(node, result, _, _) }