Python: Add type-tracking consistency query

[RasmusWL]

Like Ruby we need to exclude nodes related to post-update

(created as draft to ensure I didn't overlook anything important)

[RasmusWL]

@yoff I would like your input in regards to the match exclusions (specifically the ones from adf5a4b). The internal match tests had quite a few failures not found when running against dataflow/match/ tests. I think that indicates we should expand the dataflow match tests.

I looked at constructs such as case ("foo" | "bar") as thing: and found it strange that the flow was "foo" | "bar" -> "foo" and not the other way around 🤷 Having some tests would at least highlight why the modeling is working the way it is 😊

internal match consistency failures

unreachableNode
| motivation.py:42:15:42:28 | ControlFlowNode for MatchAsPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:42:16:42:22 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:42:28:42:28 | ControlFlowNode for l | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:42:38:42:51 | ControlFlowNode for MatchAsPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:42:39:42:45 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:42:51:42:51 | ControlFlowNode for r | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:44:18:44:32 | ControlFlowNode for MatchAsPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:44:19:44:25 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:44:31:44:32 | ControlFlowNode for op | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:46:15:46:51 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:46:16:46:30 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:46:16:46:38 | ControlFlowNode for MatchAsPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:46:35:46:38 | ControlFlowNode for left | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:46:59:46:97 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:46:60:46:74 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:46:60:46:83 | ControlFlowNode for MatchAsPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:46:79:46:83 | ControlFlowNode for right | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:48:15:48:40 | ControlFlowNode for MatchAsPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:48:16:48:30 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:48:36:48:40 | ControlFlowNode for value | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:55:15:55:21 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:57:15:57:21 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:57:61:57:67 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:65:15:65:23 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| motivation.py:113:26:113:42 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| tutorial.py:48:18:48:52 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| tutorial.py:53:17:53:66 | ControlFlowNode for MatchAsPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| tutorial.py:53:18:53:52 | ControlFlowNode for MatchOrPattern | Unreachable node in step of kind simpleLocalSmallStep. |
| tutorial.py:53:58:53:66 | ControlFlowNode for direction | Unreachable node in step of kind simpleLocalSmallStep. |

[yoff]

I had to read what is actually being tested, and it seems that all local sources should be excluded?
I had a look at the first case in 5d21251 where the code is

@expects(2)
def test_sequence_pattern_tuple():
    match (NONSOURCE, SOURCE):
        case (x, y):   <--- consistency failure here (for x, y and their two match-patterns)
            SINK_F(x)
            SINK(y) #$ flow="SOURCE, l:-3 -> y"

and here it seems that the pattern for x is only the target of a read step and so should indeed be excluded. I would have expected flow from that pattern to the variable x via matchCaptureFlowStep, though...

[RasmusWL]

I had to read what is actually being tested, and it seems that all local sources should be excluded?

For anyone following along, the check is implemented here:

codeql/shared/typetracking/codeql/typetracking/internal/TypeTrackingImpl.qll

Lines 44 to 51 in 5a348a5

	query predicate unreachableNode(Node n, string msg) {
	not ConsistencyChecksInput::unreachableNodeExclude(n) and
	exists(string kind |
	stepEntry(n, kind) and
	not flowsTo(_, n) and
	msg = "Unreachable node in step of kind " + kind + "."
	)
	}

I don't understand your question though. I don't think unreachableNode will have any results for LocalSourceNodes, since that would require that not flowsTo(_, n) holds. Consider that flowsTo(_, n) holds when:

• nonStandardFlowsTo(localSource, n) holds
• which is the case when localSource.flowsTo(n) holds
• which is forwarded to Cached::hasLocalSource
• which holds when source = sink

So there will be no n where the following can hold: n instanceof LocalSourceNode and not flowsTo(_, n)

[yoff]

So there will be no n where the following can hold: n instanceof LocalSourceNode and not flowsTo(_, n)

Ah, right, because all LocalSourceNodes flow to themselves.

[RasmusWL]

Ah, right, because all LocalSourceNodes flow to themselves.

exactly

[yoff]

Ok, so there is probably something to investigate here, but I do not see a reason to block this PR..

[yoff]

LGTM