IFSM: add AST-loop OR-branch to irqlChangesBetween for intra-function loop and re-entrant cases

The `irqlChangesBetween` predicate previously decided whether an
IRQL-changing call sits between a save and a restore using only
source-line position via the `anchorLineForCall` mechanism. This
correctly handles cross-function and acyclic in-function cases but
trivially fails on loops where the restore is textually above the save
(the bracketing line range is empty), even though at runtime the
loop back-edge means each iteration's restore is preceded by every
IRQL-changing call in the loop body.

This change adds a second disjunct to `irqlChangesBetween` that uses
AST-loop containment (`Loop.getStmt().getAChild*()`): when the save,
restore, and an IRQL-changing call all share a loop body in their
common enclosing function, the predicate fires. Combining the two
branches with OR is strictly additive and cannot regress any existing
true positive.

CFG-based reachability was rejected for two reasons documented during
investigation: BasicBlock CFG forward-reach is truncated in the
extracted DBs we test against, and ControlFlowNode forward reach
breaks at `if (call(...))` boundaries (the canonical IFSM pattern).
AST-loop containment sidesteps both issues by relying on a densely
populated AST relation that reflects the syntactic loop body.

Documents the residual limitation: the upstream IRQL analysis library
does not consistently bind `getPotentialExitIrqlAtCfn` at the
argument expression of `KeSaveFloatingPointState` when the call is
inside a loop body, so the `irqlSource != irqlSink` filter still
rejects the loop case before `irqlChangesBetween` is consulted.
Recovering this true positive requires improvements to the IRQL
analysis library, not just to this query. `driver_utility_loop_bad`
is retained in `driver_snippet.c` as a documented known false
negative so any future improvement to the IRQL library will be
detected via SARIF diff.

Refreshes `IrqlFloatStateMismatch.qhelp`, regenerates the rendered
`IrqlFloatStateMismatch.md`, refreshes the in-tree
`IrqlFloatStateMismatch.sarif` (rule-help text), and bumps
`@query-version` from v5 to v6.

Local test diff: +0/-0 (loop FN does not fire due to upstream
binding limitation; no existing TP is regressed).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: NateD-MSFT

src/drivers/general/queries/IrqlFloatStateMismatch/IrqlFloatStateMismatch.md

@@ -56,9 +56,9 @@ Correct example
 ## Semmle-specific notes
 **Wrapper / common-caller pattern.** The query reasons about IRQL-changing calls between save and restore not only when both calls share an enclosing function, but also when they sit inside one-level helper wrappers that are called from a common caller (for example, thin `save_fp_helper` / `restore_fp_helper` functions that simply forward to `KeSaveFloatingPointState` / `KeRestoreFloatingPointState`). In those cases the intermediate IRQL transition is searched in the common caller (or in either helper's enclosing function for the asymmetric case where one side is a helper and the other is direct).
 
-**Remaining limitations.** The position-based filter still does not detect:
+**Remaining limitations.** Despite the source-position and AST-loop branches, the predicate still does not detect:
 
 * **IRQL changes performed deep inside helper bodies.** If the helper function itself raises or lowers the IRQL after the save (or before the restore), the change is not visible from the common caller's source-position view, and no intermediate IRQL change is found. Annotating the helper with `_IRQL_raises_` or `_IRQL_saves_global_` makes its IRQL behavior visible without body inspection.
 * **Indirect calls.** IRQL changes performed by an indirect call (function pointer or dispatch-table call) between save and restore are not detected, because the predicate only inspects the static call target.
-* **Loops where the restore is textually before the save.** The filter compares source line numbers; in a loop body whose first statement is the restore and last statement is the save (with the IRQL change after the save), the line range becomes empty and no intermediate IRQL change is seen.
+* **Loops where the restore is textually before the save.** The AST-loop branch of `irqlChangesBetween` correctly recognises that all three calls (save, restore, and an IRQL-changing call) sit inside the same loop body and would fire on this pattern. However, the upstream IRQL analysis library used to compute the IRQL at the save and restore sites does not consistently bind a value at the argument expression of `KeSaveFloatingPointState` when the call is inside a loop body, so the `irqlSource != irqlSink` filter rejects these cases before `irqlChangesBetween` is consulted. Recovering this true positive requires improvements to the IRQL analysis library and not just to this query.
 * **Wrapper chains longer than one level.** Only one level of wrapping is currently modelled (the helper is called directly from the common caller). Multi-level wrappers require the same annotation hint described above, or a direct call site.

src/drivers/general/queries/IrqlFloatStateMismatch/IrqlFloatStateMismatch.qhelp

@@ -75,8 +75,8 @@
 			where one side is a helper and the other is direct).
 		</p>
 		<p>
-			<b>Remaining limitations.</b> The position-based filter still does
-			not detect:
+			<b>Remaining limitations.</b> Despite the source-position and
+			AST-loop branches, the predicate still does not detect:
 		</p>
 		<ul>
 			<li>
@@ -96,11 +96,18 @@
 			</li>
 			<li>
 				<b>Loops where the restore is textually before the save.</b>
-				The filter compares source line numbers; in a loop body
-				whose first statement is the restore and last statement is
-				the save (with the IRQL change after the save), the line
-				range becomes empty and no intermediate IRQL change is
-				seen.
+				The AST-loop branch of <code>irqlChangesBetween</code>
+				correctly recognises that all three calls (save, restore,
+				and an IRQL-changing call) sit inside the same loop body and
+				would fire on this pattern. However, the upstream IRQL
+				analysis library used to compute the IRQL at the save and
+				restore sites does not consistently bind a value at the
+				argument expression of <code>KeSaveFloatingPointState</code>
+				when the call is inside a loop body, so the
+				<code>irqlSource != irqlSink</code> filter rejects these
+				cases before <code>irqlChangesBetween</code> is consulted.
+				Recovering this true positive requires improvements to the
+				IRQL analysis library and not just to this query.
 			</li>
 			<li>
 				<b>Wrapper chains longer than one level.</b> Only one level

src/drivers/general/queries/IrqlFloatStateMismatch/IrqlFloatStateMismatch.ql

@@ -17,7 +17,7 @@
  * @tags correctness
  *       ca_ported
  * @scope domainspecific
- * @query-version v5
+ * @query-version v6
  */
 
 import cpp
@@ -101,30 +101,66 @@ private int anchorLineForCall(Function f, FunctionCall fc) {
 }
 
 /**
- * Holds if there is an IRQL-changing call in some function `f` whose
- * source line lies between the save anchor and the restore anchor in
- * `f`. The anchor mechanism (see `anchorLineForCall`) lets `f` be:
+ * Holds if there is an IRQL-changing call between `saveCall` and
+ * `restoreCall` in some function `f`. This predicate is a sanity filter
+ * applied on top of the dataflow result: dataflow has already shown the
+ * floating-point buffer flows from `saveCall` to `restoreCall`, and this
+ * predicate ensures there is at least one IRQL transition that could
+ * actually run between them.  Without it the query would emit the pure
+ * may-analysis artifact where two save / restore sites are compared at
+ * different hypothetical entry IRQLs but no IRQL transition can happen
+ * between them at runtime.
  *
- *   - the enclosing function of both `saveCall` and `restoreCall`
- *     (the original same-function case),
- *   - the common caller that calls thin save / restore helper
- *     wrappers,
- *   - the enclosing function of one of the two calls when the other
- *     is in a one-level helper called from it (asymmetric case).
+ * Two complementary disjuncts cooperate:
  *
- * The dataflow library has already established that the floating-
- * point buffer flows from `saveCall` to `restoreCall`; this predicate
- * is purely a sanity filter to suppress the pure may-analysis
- * artifact where two save / restore sites are compared at different
- * hypothetical entry IRQLs but no IRQL transition can actually happen
- * at runtime between them.
+ *  1. **Source-position branch.** For some `f`, an IRQL-changing call
+ *     `mid` in `f` lies on a source line bracketed by the anchor lines
+ *     of `saveCall` and `restoreCall` (see `anchorLineForCall`).  The
+ *     anchor mechanism lets `f` be the directly enclosing function of
+ *     both calls or a one-level wrapper / common caller, which covers
+ *     the cross-function case that intra-procedural CFG cannot reach.
  *
- * The position-based check (rather than a CFG-reachability check) is
- * required because the cpp control-flow graph in some extracted
- * databases does not transitively connect calls across statement
- * boundaries, which would silently eliminate true positives.
+ *  2. **AST-loop branch.** All three calls (`saveCall`, `restoreCall`,
+ *     `mid`) sit inside the body of the same loop in their common
+ *     enclosing function.  The loop back-edge means that at runtime
+ *     each iteration's `restoreCall` can be preceded by the previous
+ *     iteration's `saveCall` with `mid` between them, so an
+ *     IRQL-changing `mid` anywhere in the loop body is a real
+ *     transition between save and restore even when `restoreCall` is
+ *     textually above `saveCall`.  Source-line position alone cannot
+ *     express this: when the restore is textually earlier than the
+ *     save the bracketing line range is empty and branch (1) trivially
+ *     fails.
+ *
+ * The two branches are disjoint in spirit: branch (1) handles
+ * cross-function and acyclic in-function cases; branch (2) handles
+ * intra-function loops and re-entrant patterns.  Combining them is
+ * strictly additive (can only enable more findings, never suppress one
+ * that branch (1) would have flagged), so existing true positives are
+ * preserved.
+ *
+ * Why not full intra-procedural CFG reachability instead of branch (1)?
+ * The cpp control-flow graph in some extracted databases does not
+ * transitively connect calls across certain statement boundaries (in
+ * particular, forward reachability across `if (call(...))` conditions
+ * is unreliable in our extracted DBs), which would silently eliminate
+ * true positives that branch (1) catches via source-line bracketing.
+ * AST-loop containment in branch (2) sidesteps this by relying on the
+ * AST `Loop.getStmt().getAChild*()` relation, which is densely
+ * populated and reflects the syntactic loop body directly.
+ *
+ * Caveat: branch (2) cooperates with `irqlSource != irqlSink` only when
+ * the IRQL-analysis library binds `getPotentialExitIrqlAtCfn` at the
+ * argument expression of `KeSaveFloatingPointState`. In our current
+ * extracted DBs that binding is not always produced for `save` calls
+ * inside loop bodies, so some real-world loop true positives may
+ * still be filtered out by the upstream IRQL filter even when this
+ * predicate fires; recovering those will require improvements to
+ * the IRQL analysis library itself.
  */
 predicate irqlChangesBetween(FunctionCall saveCall, FunctionCall restoreCall) {
+  // Branch 1: source-line bracketing in a function `f` that anchors
+  // both calls (directly enclosing or one-level wrapper / common caller).
   exists(Function f, int saveLine, int restoreLine, FunctionCall mid |
     saveLine = anchorLineForCall(f, saveCall) and
     restoreLine = anchorLineForCall(f, restoreCall) and
@@ -135,6 +171,23 @@ predicate irqlChangesBetween(FunctionCall saveCall, FunctionCall restoreCall) {
     mid != saveCall and
     mid != restoreCall
   )
+  or
+  // Branch 2: all three calls live inside the body of the same loop in
+  // their shared enclosing function. The loop back-edge makes any
+  // IRQL-changing call in the body a real transition between save and
+  // restore on a subsequent iteration, even when source-line position
+  // would put restore before save.
+  exists(Function f, Loop l, FunctionCall mid |
+    f = saveCall.getEnclosingFunction() and
+    f = restoreCall.getEnclosingFunction() and
+    f = mid.getEnclosingFunction() and
+    isIrqlChangingCall(mid) and
+    mid != saveCall and
+    mid != restoreCall and
+    l.getStmt().getAChild*() = saveCall.getEnclosingStmt() and
+    l.getStmt().getAChild*() = restoreCall.getEnclosingStmt() and
+    l.getStmt().getAChild*() = mid.getEnclosingStmt()
+  )
 }
 
 from