Irql.qll: add loop-body AST fallback to getPotentialExitIrqlAtCfn

The recursive cascade in `getPotentialExitIrqlAtCfn` returns no value
for argument-expression CFNs of function calls reached via a loop
back-edge in some extracted databases.  When the cascade is empty,
downstream queries that consume the result either drop the relevant
finding (because their `irqlSource = getPotentialExitIrqlAtCfn(...)`
binding fails) or fire spuriously (because they treat empty as
out-of-range).  This is the upstream complement to the IFSM
`irqlChangesBetween` AST-loop OR-branch added in 39dd725.

Fix: rename the existing predicate body to a private
`getPotentialExitIrqlAtCfnRaw` helper and introduce a public wrapper
that returns Raw's bindings unchanged, plus -- only when Raw yields
no value at all -- a single-step AST-level fallback that returns the
cascade's IRQL at the closest source-line preceding sibling Stmt.
The fallback is restricted to CFNs whose enclosing Stmt sits inside
a loop body, which is the empirical failure mode and avoids
over-approximating on linear branching code.

Layering preserves existing semantics on every input where Raw binds:
the wrapper agrees with Raw setwise there, so no query that previously
bound correctly can regress.  The only behavioural change is to fill
in silence with one conservative value derived from textually-preceding
code in the loop body.

Internal callers inside Irql.qll that participated in the recursive
stratum (getIrqlLevel for the three save-globals classes and
functionExitIrql) are switched to call Raw directly so the wrapper's
negation does not cycle back through them.

Validation:

Local IFSM TestDB: the documented "known false negative"
`driver_utility_loop_bad` at driver_snippet.c:156 (a for-loop where
the restore is textually above the save) now fires as a true positive,
recovered exactly as the source comment block at lines 127-145
predicted would require improvements to the IRQL analysis library.
SARIF baseline updated to include the new finding.

Out-of-tree corpora (clean cache, --ram tuned per DB): for the five
queries that call this predicate and have non-zero baseline:

* IrqlFunctionNotAnnotated, IrqlInconsistentWithRequired,
  IrqlTooHigh, IrqlTooLow: identical findings before and after on
  both small corpora.
* KeSetEventIrql: one fewer finding on the larger of the two small
  corpora (a true false-positive suppression in a worker-thread
  routine where a release-spinlock immediately precedes a SetEvent
  inside a `for(;;)` loop body; the cascade was empty pre-fix and the
  KeSetEvent query treated empty as out-of-range, warning spuriously).
  The fallback walks back to the release sibling stmt, binds PASSIVE,
  and the warning is correctly silenced.

Sanity-check queries that do not call the predicate (IrqlNotUsed,
IrqlCancelRoutine) are unchanged, confirming the rename did not
perturb unrelated paths.

Performance: no measurable wall-time regression observed on either
small corpus.

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

Author: NateD-MSFT

src/drivers/general/queries/IrqlFloatStateMismatch/IrqlFloatStateMismatch.sarif

@@ -112,7 +112,7 @@
         "extensions": [
           {
             "name": "microsoft/windows-drivers",
-            "semanticVersion": "1.9.0+4cacaf0d92da0d47dab3a6bd6640729cf07eec99",
+            "semanticVersion": "1.9.0+39dd725fc01992bf14a42934229a3cc1fd7bf25b",
             "locations": [
               {
                 "uri": "file:///F:/source/repos/Windows-Driver-Developer-Supplemental-Tools/src/",
@@ -254,14 +254,14 @@
                 "text": ""
               },
               "level": "none",
-              "timeUtc": "2026-04-29T20:06:00.500637300Z",
+              "timeUtc": "2026-04-29T20:46:26.236012500Z",
               "descriptor": {
                 "id": "cli/file-coverage-baseline",
                 "index": 1
               },
               "properties": {
                 "attributes": {
-                  "durationMilliseconds": 197
+                  "durationMilliseconds": 233
                 },
                 "visibility": {
                   "statusPage": false,
@@ -274,7 +274,7 @@
                 "text": ""
               },
               "level": "none",
-              "timeUtc": "2026-04-29T20:06:00.504647400Z",
+              "timeUtc": "2026-04-29T20:46:26.241012400Z",
               "descriptor": {
                 "id": "cli/platform",
                 "index": 2
@@ -297,7 +297,7 @@
                 "markdown": "Internal telemetry for the C++ extractor.\n\nNo action needed."
               },
               "level": "note",
-              "timeUtc": "2026-04-29T20:06:43.926354300Z",
+              "timeUtc": "2026-04-29T20:47:05.794926800Z",
               "descriptor": {
                 "id": "cpp/extractor/summary",
                 "index": 3
@@ -350,6 +350,68 @@
         }
       ],
       "results": [
+        {
+          "ruleId": "cpp/drivers/irql-float-state-mismatch",
+          "ruleIndex": 0,
+          "rule": {
+            "id": "cpp/drivers/irql-float-state-mismatch",
+            "index": 0
+          },
+          "message": {
+            "text": "The irql level where the floating-point state was saved (0) does not match the irql level for the restore operation (1).\nThe irql level where the floating-point state was saved (2) does not match the irql level for the restore operation (1)."
+          },
+          "locations": [
+            {
+              "physicalLocation": {
+                "artifactLocation": {
+                  "uri": "driver/driver_snippet.c",
+                  "uriBaseId": "%SRCROOT%",
+                  "index": 0
+                },
+                "region": {
+                  "startLine": 156,
+                  "startColumn": 38,
+                  "endColumn": 46
+                }
+              }
+            }
+          ],
+          "partialFingerprints": {
+            "primaryLocationLineHash": "7203877b7e98c247:1",
+            "primaryLocationStartColumnFingerprint": "29"
+          }
+        },
+        {
+          "ruleId": "cpp/drivers/irql-float-state-mismatch",
+          "ruleIndex": 0,
+          "rule": {
+            "id": "cpp/drivers/irql-float-state-mismatch",
+            "index": 0
+          },
+          "message": {
+            "text": "The irql level where the floating-point state was saved (0) does not match the irql level for the restore operation (1).\nThe irql level where the floating-point state was saved (2) does not match the irql level for the restore operation (1)."
+          },
+          "locations": [
+            {
+              "physicalLocation": {
+                "artifactLocation": {
+                  "uri": "driver/driver_snippet.c",
+                  "uriBaseId": "%SRCROOT%",
+                  "index": 0
+                },
+                "region": {
+                  "startLine": 156,
+                  "startColumn": 37,
+                  "endColumn": 46
+                }
+              }
+            }
+          ],
+          "partialFingerprints": {
+            "primaryLocationLineHash": "7203877b7e98c247:1",
+            "primaryLocationStartColumnFingerprint": "28"
+          }
+        },
         {
           "ruleId": "cpp/drivers/irql-float-state-mismatch",
           "ruleIndex": 0,

src/drivers/libraries/Irql.qll

@@ -534,13 +534,13 @@
     * "the IRQL before the corresponding save global call."
     */
    int getIrqlLevel() {
-     result = any(getPotentialExitIrqlAtCfn(this.getMostRecentRaise().getAPredecessor()))
+     result = any(getPotentialExitIrqlAtCfnRaw(this.getMostRecentRaise().getAPredecessor()))
    }
- 
+
    int getIrqlLevelExplicit() {
      result = any(getExplicitExitIrqlAtCfn(this.getMostRecentRaise().getAPredecessor()))
    }
- 
+
    /** Returns the matching call to a function that saved the IRQL. */
    IrqlSaveCall getMostRecentRaise() {
      result =
@@ -614,7 +614,7 @@
     */
    int getIrqlLevel() {
      result =
-       any(getPotentialExitIrqlAtCfn(this.getMostRecentRaiseInterprocedural().getAPredecessor()))
+       any(getPotentialExitIrqlAtCfnRaw(this.getMostRecentRaiseInterprocedural().getAPredecessor()))
    }
 
    int getIrqlLevelExplicit() {
@@ -665,13 +665,13 @@
     * "the IRQL before the corresponding save global call."
     */
    int getIrqlLevel() {
-     result = any(getPotentialExitIrqlAtCfn(this.getMostRecentRaise().getAPredecessor()))
+     result = any(getPotentialExitIrqlAtCfnRaw(this.getMostRecentRaise().getAPredecessor()))
    }
- 
+
    int getIrqlLevelExplicit() {
      result = any(getExplicitExitIrqlAtCfn(this.getMostRecentRaise().getAPredecessor()))
    }
- 
+
    /**
     * Returns the matching call to a function that saved the IRQL to a global state.
     *
@@ -735,10 +735,17 @@
  /**
   * Pre-computed summary: the potential exit IRQL of function `f`,
   * computed once per function rather than re-discovered per call site.
+  *
+  * Calls the Raw cascade directly rather than the public wrapper so
+  * that this internal building block stays inside a single recursive
+  * stratum with the cascade.  The wrapper layers an AST-level fallback
+  * over Raw using a negation, which would otherwise cycle back through
+  * here.  Equivalent to the historical pre-wrapper behaviour because
+  * the wrapper agrees with Raw on every input where Raw binds.
   */
  pragma[nomagic]
  private int functionExitIrql(Function f) {
-   result = getPotentialExitIrqlAtCfn(getAnExitPointOfFunction(f))
+   result = getPotentialExitIrqlAtCfnRaw(getAnExitPointOfFunction(f))
  }
 
  /**
@@ -765,9 +772,38 @@
   * - If there are no prior CFNs and no calls to this function, then the IRQL is determined by annotations applied to this function.
   * - Failing all this, we set the IRQL to 0.
   *
+  * Layering note: this public predicate wraps the recursive cascade
+  * `getPotentialExitIrqlAtCfnRaw` with a single AST-level fallback
+  * (`astLevelExitIrqlFallback`) that activates only when the cascade
+  * yields no value at all.  The fallback walks one source-line step
+  * back to the closest preceding sibling Stmt and returns the cascade's
+  * IRQL there.  This recovers binding for argument-expression CFNs of
+  * function calls inside loop bodies, where the cpp CFG in some
+  * extracted databases is too sparse for the cascade's predecessor walk
+  * to converge.  The fallback is restricted to CFNs inside loop bodies
+  * (the empirical failure mode), keeping it from over-approximating on
+  * linear branching code where the cascade's silence may be hiding
+  * IRQL-changing work that an AST-level scan cannot see.  When the
+  * cascade already binds, this wrapper returns exactly the cascade's
+  * result set: the fallback never widens an existing binding.
+  *
   * Not implemented: _IRQL_limited_to_
   */
  int getPotentialExitIrqlAtCfn(ControlFlowNode cfn) {
+   result = getPotentialExitIrqlAtCfnRaw(cfn)
+   or
+   not exists(getPotentialExitIrqlAtCfnRaw(cfn)) and
+   result = astLevelExitIrqlFallback(cfn)
+ }
+
+ /**
+  * Internal recursive cascade for `getPotentialExitIrqlAtCfn`.  Behaves
+  * exactly like the historical `getPotentialExitIrqlAtCfn` did before
+  * the AST fallback wrapper was introduced.  Callers should use
+  * `getPotentialExitIrqlAtCfn` instead, which additionally consults
+  * `astLevelExitIrqlFallback` when this cascade yields no value.
+  */
+ private int getPotentialExitIrqlAtCfnRaw(ControlFlowNode cfn) {
    if cfn instanceof KeRaiseIrqlCall
    then result = cfn.(KeRaiseIrqlCall).getIrqlLevel()
    else
@@ -788,18 +824,18 @@
              if
                cfn instanceof FunctionCall and
                cfn.(FunctionCall).getTarget() instanceof IrqlRequiresSameAnnotatedFunction
-             then result = getPotentialExitIrqlAtCfn(cfn.getAPredecessor())
+             then result = getPotentialExitIrqlAtCfnRaw(cfn.getAPredecessor())
              else
                if cfn instanceof FunctionCall
                then result = functionExitIrql(cfn.(FunctionCall).getTarget())
                else
                  if exists(ControlFlowNode cfn2 | cfn2 = cfn.getAPredecessor())
-                 then result = getPotentialExitIrqlAtCfn(cfn.getAPredecessor())
+                 then result = getPotentialExitIrqlAtCfnRaw(cfn.getAPredecessor())
                  else
                    if exists(callerPredecessor(cfn.getControlFlowScope()))
                    then
                      result =
-                       getPotentialExitIrqlAtCfn(callerPredecessor(cfn.getControlFlowScope()))
+                       getPotentialExitIrqlAtCfnRaw(callerPredecessor(cfn.getControlFlowScope()))
                    else
                      if
                        cfn.getControlFlowScope() instanceof IrqlRestrictsFunction and
@@ -808,6 +844,44 @@
                      else result = 0
  }
 
+ /**
+  * AST-level fallback for `getPotentialExitIrqlAtCfn`.  Walks to the
+  * closest source-line preceding sibling Stmt of `cfn`'s enclosing Stmt
+  * (within the same parent Stmt) and returns the cascade's IRQL there.
+  * Yields no value when there is no preceding sibling at the same
+  * nesting level (e.g. `cfn` is the first stmt in its block) or when
+  * the cascade also yields no value at that sibling.
+  *
+  * Restricted to CFNs whose enclosing Stmt sits inside a loop body.  The
+  * cascade's CFG-predecessor walk is reliable on linear control flow but
+  * empirically can fail to bind on argument-expression CFNs of function
+  * calls reached via a loop back-edge; this fallback exists to recover
+  * binding for that specific case.  Restricting to loops avoids
+  * supplying coarse single-value approximations on linear code where the
+  * cascade's silence (when it does occur) often reflects branching that
+  * the AST-level scan cannot reason about (e.g. an if-stmt whose body
+  * raises and lowers IRQL).
+  *
+  * Consulted by `getPotentialExitIrqlAtCfn` only when the cascade
+  * returns no value at all, so this never widens an existing binding;
+  * it only fills in silence with a single conservative IRQL value
+  * derived from textually-preceding code in the loop body.
+  */
+ private int astLevelExitIrqlFallback(ControlFlowNode cfn) {
+   exists(Stmt cfnStmt, Stmt prev, Loop l |
+     cfnStmt = cfn.getEnclosingStmt() and
+     cfnStmt.getParent+() = l and
+     prev.getParentStmt() = cfnStmt.getParentStmt() and
+     prev.getLocation().getStartLine() < cfnStmt.getLocation().getStartLine() and
+     not exists(Stmt closer |
+       closer.getParentStmt() = cfnStmt.getParentStmt() and
+       closer.getLocation().getStartLine() < cfnStmt.getLocation().getStartLine() and
+       closer.getLocation().getStartLine() > prev.getLocation().getStartLine()
+     ) and
+     result = getPotentialExitIrqlAtCfnRaw(prev)
+   )
+ }
+
  /*
   * Similar to above, but only exit points where the Irql is explicit
   */