github · yoff · Sep 29, 2026 · Sep 29, 2026
@@ -204,7 +204,15 @@ class ControlFlowNode extends CfgImpl::ControlFlowNode {
   }
 
   /** Holds if this flow node strictly reaches `other`. */
-  predicate strictlyReaches(ControlFlowNode other) { this.getASuccessor+() = other }
+  overlay[caller?]
+  pragma[inline]
+  predicate strictlyReaches(ControlFlowNode other) {
+    this.getBasicBlock().strictlyReaches(other.getBasicBlock())
+    or
+    exists(BasicBlock block, int i, int j |
+      this = block.getNode(i) and other = block.getNode(j) and i < j
+    )
+  }
 }
 
 /**

@@ -0,0 +1,35 @@
+/**
+ * Inline-expectations test for node reachability in the shared CFG facade.
+ */
+
+import python
+import semmle.python.controlflow.internal.Cfg as Cfg
+import utils.test.InlineExpectationsTest
+
+private Cfg::NameNode caseNode(string caseId, string role) {
+  role = ["source", "destination"] and
+  result.isStore() and
+  result.getId() = "reachability_" + caseId + "_" + role
+}
+
+module StrictlyReachesTest implements TestSig {
+  string getARelevantTag() { result = ["reaches", "not-reaches"] }
+
+  predicate hasActualResult(Location location, string element, string tag, string value) {
+    exists(Cfg::NameNode source, Cfg::NameNode destination |
+      source = caseNode(value, "source") and
+      destination = caseNode(value, "destination") and
+      location = destination.getLocation() and
+      element = destination.toString() and
+      (
+        tag = "reaches" and
+        source.strictlyReaches(destination)
+        or
+        tag = "not-reaches" and
+        not source.strictlyReaches(destination)
+      )
+    )
+  }
+}
+
+import MakeTest<StrictlyReachesTest>
@@ -0,0 +1,60 @@
+def same_block_forward():
+    reachability_same_block_forward_source = 1
+    reachability_same_block_forward_destination = (  # $ reaches=same_block_forward
+        reachability_same_block_forward_source + 1
+    )
+    return reachability_same_block_forward_destination
+
+
+def same_block_reverse():
+    reachability_same_block_reverse_destination = 1  # $ not-reaches=same_block_reverse
+    reachability_same_block_reverse_source = reachability_same_block_reverse_destination + 1
+    return reachability_same_block_reverse_source
+
+
+def branch_left_to_join(condition):
+    if condition:
+        reachability_branch_left_to_join_source = 1
+    else:
+        fallback = 2
+    reachability_branch_left_to_join_destination = fallback  # $ reaches=branch_left_to_join
+    return reachability_branch_left_to_join_destination
+
+
+def branch_right_to_join(condition):
+    if condition:
+        fallback = 1
+    else:
+        reachability_branch_right_to_join_source = 2
+    reachability_branch_right_to_join_destination = fallback  # $ reaches=branch_right_to_join
+    return reachability_branch_right_to_join_destination
+
+
+def branch_siblings(condition):
+    if condition:
+        reachability_branch_siblings_source = 1
+    else:
+        reachability_branch_siblings_destination = 2  # $ not-reaches=branch_siblings
+
+
+def loop_backedge(condition):
+    while condition:
+        reachability_loop_backedge_destination = 1  # $ reaches=loop_backedge
+        reachability_loop_backedge_source = reachability_loop_backedge_destination + 1
+
+
+def loop_exit(condition):
+    while condition:
+        reachability_loop_exit_source = 1
+    reachability_loop_exit_destination = 2  # $ reaches=loop_exit
+    return reachability_loop_exit_destination
+
+
+def distinct_scope_source():
+    reachability_distinct_scopes_source = 1
+    return reachability_distinct_scopes_source
+
+
+def distinct_scope_destination():
+    reachability_distinct_scopes_destination = 2  # $ not-reaches=distinct_scopes
+    return reachability_distinct_scopes_destination