Skip to content

Commit 9975f49

Browse files
NateD-MSFTCopilotCopilot
authored
Bring AI+test-driven perf optimizations into development. (#220)
* [AI] Initial stab at optimizing suppressions and IRQL. * [AI] Revise IRQL queries and libraries to reduce false positives. * Compress repetitive code and fix misplaced comments in IRQL queries Agent-Logs-Url: https://github.com/microsoft/Windows-Driver-Developer-Supplemental-Tools/sessions/8ab9c70a-a38a-46ec-9f14-f90475a0d87c Co-authored-by: NateD-MSFT <34494373+NateD-MSFT@users.noreply.github.com> * Optimize MultiplePagedCode.ql to avoid timeouts on large codebases The original query joined MacroInvocation x MacroInvocation and only filtered by macro name and PagedFunctionDeclaration after the join. On large codebases this could hit the analysis timeout because MacroInvocation.getEnclosingFunction() (cpp-all 7.0.0 Macro.qll:178) is built on getAnAffectedElement(), which materialises a join of inmacroexpansion and macrolocationbind whose size scales poorly with code volume regardless of how the receiver set is constrained. Changes: * src/drivers/libraries/Page.qll: add class PagedCodeMacro extends MacroInvocation. Pre-filters by macro name (PAGED_CODE / PAGED_CODE_LOCKED) and exposes getEnclosingPagedFunction() that uses getStmt().getEnclosingFunction() (built on the cheaper getAnExpandedElement()) and excludes FunctionTemplateInstantiation. * src/drivers/wdm/queries/MultiplePagedCode/MultiplePagedCode.ql: rewrite body as an asymmetric existential over PagedCodeMacro + Function so only the outer macro is in the from clause. Excluding FunctionTemplateInstantiation also fixes a latent FP: each template instantiation produces its own Function and its own MacroInvocation records with line attribution that can drift by +-1 across instantiations, which produced false 'multiple PAGED_CODE' reports in templated functions. Counting only source-level (uninstantiated) template MIs preserves real positives in templates while eliminating the spurious match. Verification: * Windows driver samples corpus: pre-existing single TP preserved on the same (file, line); wall time roughly halved. * Large representative codebase that previously timed out at the 2 h limit: now completes in ~2.5 minutes with no findings; spot-checked source files with multiple textual PAGED_CODE() calls confirm each invocation lives in a distinct function (constructor/destructor pairs, per-overload operators, etc.), so the empty result is correct. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Bump @query-version on queries changed since development branch Each of these queries has functional changes (new predicates, additional where-clause filters, refactored body) relative to the development branch but the @query-version metadata had not been incremented. Bumping the versions so downstream consumers can detect the behavioural change. * IrqlFloatStateMismatch.ql: v1 -> v2 * IrqlNotSaved.ql: v1 -> v2 * IrqlSetTooHigh.ql: v1 -> v2 * IrqlTooHigh.ql: v3 -> v4 * IrqlTooLow.ql: v4 -> v5 * MultiplePagedCode.ql: v1 -> v2 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Refine IrqlFloatStateMismatch suppression to be CFG-independent The v2 `irqlChangesBetween` predicate used `ControlFlowNode.getASuccessor+()` from a `DataFlow::Node.asIndirectExpr()` anchor. Indirect-expression nodes are synthetic and are not connected to the cpp control-flow graph, so `getASuccessor+()` from them returns the empty set in some extracted databases. As a result the predicate held for nothing on those databases and all true positives were silently suppressed. Replace the CFG reachability check with a same-function source-position check between the `KeSaveFloatingPointState` and `KeRestoreFloatingPointState` calls. The new predicate preserves the original intent of suppressing the `no-actual-irql-transition` false positive category while remaining well-defined regardless of how the control-flow graph is materialised. Bumps @query-version v2 -> v3. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Catch IrqlFloatStateMismatch through unannotated helper wrappers Driver code commonly wraps the IRQL primitives (KeRaiseIrql, KeLowerIrql, KfRaiseIrql, KfLowerIrql) in unannotated helper functions. When a floating-point save/restore pair has its IRQL transition performed inside such a helper, the previous filter -- which only inspected calls in the enclosing function -- discarded the finding as a may-analysis artifact and the true positive was lost. Extend `isIrqlChangingCall` with a transitive helper-detection pass: `isIrqlChangingFunction(f)` holds either when `f` is annotated as an IRQL-changing function or when its own body contains an IRQL-changing call (recursively). This is bounded by the call graph and behaves idempotently on cycles. Add two test snippets to driver_snippet.c that exercise the new logic: `driver_utility_helper_bad` (must fire -- IRQL changes via an unannotated helper) and `driver_utility_nested_block_good` (must not fire -- IRQL change inside a nested compound statement). Update the checked-in baseline SARIF to expect the additional helper finding. Bumps @query-version v3 -> v4. Out-of-tree corpus measurements showed no change in finding counts and only a small evaluation-time regression on the smallest databases (roughly +10 percent), with no measurable change on larger databases. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Add adversarial tests + document known false negatives in qhelp Empirically validated three review-flagged regressions on the optimization branch by adding adversarial test cases to the local test drivers and running the queries with and without the branch's changes: * IrqlTooHigh / IrqlTooLow isInConstantFalseBranch. The predicate intended to silence NDIS dead-branch macros is too lax: compound assignments (|=, &=, +=) extract as AssignOperation, and ++/-- as CrementOperation, so the predicate's ot exists AssignExpr guard considers them as no mutation; pass-by-reference helpers and globals reassigned in another function also bypass the check. Four adversarial cases per direction were added; the on-branch query reports 0 of them, while the pre-branch query reports all 4. * IrqlFloatStateMismatch cross-function save / restore. The new irqlChangesBetween filter requires the save and restore calls to share an enclosing function. A wrapper that thinly forwards to KeSaveFloatingPointState / KeRestoreFloatingPointState with the IRQL change happening in the caller is now silently missed; the pre-branch query flagged it correctly. * MultiplePagedCode template-instantiation exclusion. A C++ function template containing two PAGED_CODE() invocations produced one finding from the pre-branch query and zero from the on-branch query (the latter excludes every FunctionTemplateInstantiation when locating the enclosing function and, on this database, never sees a non-instantiation parent). Adversarial template test driver lives in the out-of-tree workspace. For each finding, the corresponding qhelp file gains a "Known false negatives" / "Lower-on-exit pattern" section describing the limitation in user-facing terms; the matching .md files were regenerated via codeql generate query-help. The IrqlSetTooHigh "lower-on-exit" exemption (heuristic risk) and the IrqlFloatStateMismatch indirect-call / loop-order limitations are also documented. The on-branch driver_snippet baselines remain +0/-0 because each adversarial case is, by construction, a missed positive. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Fix three false negatives surfaced by the prior review * IrqlTooHigh / IrqlTooLow isInConstantFalseBranch. Replaced the AssignExpr-only mutation guard with the broader Assignment superclass (covers =, |=, &=, +=, etc.) and added a CrementOperation check for ++ / --. Restricted the variable-access case to non-static LocalVariable instances and bailed out when the variable's address is taken anywhere in the database, so globals reassigned in another function and locals mutated through a pointer are no longer treated as "constantly false". The compile-time-constant-zero condition is preserved unchanged. IrqlTooHigh: v4 -> v5. IrqlTooLow: v5 -> v6. The four adversarial cases in each driver_snippet now produce findings; baseline TPs are preserved unchanged. * IrqlFloatStateMismatch cross-function wrappers. Replaced the same-enclosing-function constraint in irqlChangesBetween with an anchor-line predicate that lets the candidate function be either the enclosing function of the call directly, or the function that calls a one-level helper containing it. The predicate then looks for an IRQL-changing call in between the two anchor lines. This handles thin save/restore wrappers around the Ke*FloatingPointState primitives where the IRQL change happens in the common caller, and also the asymmetric case where one side is a wrapper and the other is direct. v4 -> v5. * MultiplePagedCode template-instantiation handling. Replaced the blanket ot result instanceof FunctionTemplateInstantiation exclusion with a projection back to the underlying TemplateFunction via getTemplate(). Page-segment heuristics are still checked on the concrete instantiation, but match keys are deduplicated to the source-level template, so a duplicate PAGED_CODE inside a templated function body is reported once at the source location regardless of how many instantiations the extractor produced. v2 -> v3. Validation (in-tree tests): * IrqlTooHigh: 4 baseline TPs preserved; 4 adversarial cases now flagged (compound assign, increment, by-reference helper, file-scope global). diff +0/-0 against the updated baseline. * IrqlTooLow: same shape; 2 + 4 = 6 findings. * IrqlFloatStateMismatch: 4 baseline TPs preserved; 1 adversarial cross-function case now flagged. 5 findings. * MultiplePagedCode: existing baseline TP preserved; diff +0/-0. Validation (out-of-tree C++ KMDF template database): * MultiplePagedCode now reports the templated duplicate at the source location (one finding), matching the pre-branch baseline instead of silently dropping it. qhelp updated for each query: the prior "Known false negatives" sections were rewritten to describe the now-handled scope and to keep the documented limitations that still apply (indirect calls, deeply-nested helper IRQL changes, multi-level wrapper chains, loop-restore-before-save). MD files regenerated via codeql generate query-help. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Fix MultiplePagedCode cross-file conflation FP The previous fix projected FunctionTemplateInstantiation back to its underlying TemplateFunction to deduplicate findings inside a templated function body. However, the cpp extractor sometimes consolidates two ODR-equivalent template definitions in different headers into a single TemplateFunction entity. When two driver-private headers each defined e.g. emplate<class T> Aggregator_SendProperty(...) containing one PAGED_CODE(), my projection collapsed both definitions to one match key and the query reported a spurious "duplicate" across the two unrelated functions. This change reverts the projection: getEnclosingPagedFunction() now returns the concrete Function produced by getStmt().getEnclosingFunction() (which can be a FunctionTemplateInstantiation for templated bodies). The query joins on enclosing-function identity AND requires the two PagedCodeMacro invocations and the enclosing function to all share the same file, so the cross-file conflation can no longer match. Same-file deduplication across template instantiations within a single TU still produces a single finding because the multiple (mi2, f) tuples project to one mi2 at the SARIF level. Validation: * In-tree MultiplePagedCode test: diff +0/-0 (the existing DispatchShutdown baseline TP is preserved). * Out-of-tree C++ KMDF template DB: still reports 1 finding for the templated duplicate PAGED_CODE, matching the pre-branch baseline. * Large representative codebase that previously surfaced the cross-file FP: now reports 0 findings (down from the spurious 1). v3 -> v4. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Pretty-print SARIF baselines compressed by #220 Agent-Logs-Url: https://github.com/microsoft/Windows-Driver-Developer-Supplemental-Tools/sessions/e23e0bbb-d5d4-4b2c-808b-de74c56ed9dc Co-authored-by: NateD-MSFT <34494373+NateD-MSFT@users.noreply.github.com> * Tidy up: indentation, ASCII-only comments, dedupe IFSM where, refresh SARIF baselines Style and consistency cleanups uncovered during the final code review, plus baseline regeneration so all checked-in SARIF baselines have consistent (2-space) pretty-printing and reflect the current CodeQL build's output: * Irql.qll - whenConditionIsFalseAtCallSite: realign the new "!= NULL" and "(arg & 0x1) <op> 0" or-branches to match the indentation of the pre-existing "Param != 0" / "Param == N" branches (one extra leading space each before this change). - isInConstantFalseBranch: indent the predicate body to match the surrounding 1-space-leading column convention used throughout the file. * Page.qll: replace "MacroInvocation x MacroInvocation" en-quad with ASCII "x" so the file is pure ASCII (matching the rest of the codebase). * IrqlSetTooHigh.ql: replace em-dash with "--" in the same-line rationale comment for the lower-on-exit exemption. * IrqlNotSaved.ql: - Replace em-dash in the "Only track flow to assignment targets or parameters" comment with a comma. - Rewrite the "exists(sink.asParameter())" idiom as "sink.asParameter() instanceof Parameter" for readability; behaviour is unchanged. * IrqlFloatStateMismatch.ql: - Drop the now-redundant getName().matches("KeSave...") / getName().matches("KeRestore...") constraints from the where clause: the FloatStateFlow source/sink predicates already enforce them, so saveCall and restoreCall are uniquely bound by their arg(0) equalities. Adds a short explanatory comment. - Refresh the comment on the irqlChangesBetween conjunct so it no longer says "in the same function": the predicate now also handles one-level wrapper / common-caller patterns. * Adversarial driver_snippet.c comments (IrqlTooHigh, IrqlTooLow, IrqlFloatStateMismatch): the original test headers described the pre-fix predicate behaviour ("under the current predicate they are not [flagged]" / "known false negative of the current intraprocedural filter"). Those statements no longer reflect reality: each adversarial case is now flagged by the corresponding query. Rewrote the headers to describe what the test now exercises (regression guards against the former FN classes). * SARIF baselines: regenerated all six against the current CodeQL build using the in-tree test runner, then pretty-printed with 2-space indent (matching the convention used by the majority of checked-in baselines under src/drivers/). MPC's baseline previously used a Jackson-style "key" : value formatting from the older CodeQL 2.11.5; the regenerated file uses the modern "key": value style consistent with the rest of the repo. Validation: in-tree test runner reports +0/-0 for IrqlTooHigh, IrqlTooLow, IrqlFloatStateMismatch, MultiplePagedCode, IrqlNotSaved, and IrqlSetTooHigh. No query semantics changed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * 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> * 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> * IrqlFloatStateMismatch: pragma[inline_late] on irqlChangesBetween The `irqlChangesBetween/2` predicate is the hottest single predicate in the IFSM query at HEAD (~109 s of CPU and 3.43 M result tuples in the 18-query suite measurement on the WDS sample database, accounting for roughly a quarter of the IFSM query's total cost). Without a planner hint, the predicate is materialized as a standalone relation over every `(FunctionCall, FunctionCall)` pair in the codebase that satisfies its constraints, and only then intersected with the ~25-row dataflow result set produced by `FloatStateFlow::flow`. With `pragma[inline_late]` plus the matching `bindingset[saveCall, restoreCall]`, the body is specialized at the single call site after the dataflow result has bound both arguments, so the predicate body is evaluated only on the small set of dataflow-derived pairs. Validation on the WDS sample database (single-query run, cold cache): - SARIF result count for cpp/drivers/irql-float-state-mismatch: 0 (matches the HEAD baseline of 0; correctness preserved) - `irqlChangesBetween` no longer appears as a discrete predicate in the evaluator log (it has been fully inlined into its call site) - New top single-query predicate: 28.9 s, vs 109 s for the standalone `irqlChangesBetween` in the baseline suite measurement This is a planner-hint change only. The predicate body is byte-for-byte unchanged, so the set of `(saveCall, restoreCall)` pairs the predicate admits (and therefore the set of `select` rows the query produces) is unchanged on every database. The `bindingset` is honest: the only caller (line 215) binds both arguments via the `FloatStateFlow::flow` result and the `asIndirectExpr` constraints in the same `where` clause. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * [AI] More IRQL correctness tweaks * [AI] Reduce verbosity of AI comments + other cleanup. * Refactor a Supression predicate into a class * Address a few more review comments --------- Signed-off-by: NateD-MSFT <34494373+NateD-MSFT@users.noreply.github.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent 219f97f commit 9975f49

30 files changed

Lines changed: 3667 additions & 1255 deletions

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,3 +52,13 @@ Correct example
5252

5353
## References
5454
* [ C28111 ](https://learn.microsoft.com/en-us/windows-hardware/drivers/devtest/28111-floating-point-irql-mismatch)
55+
56+
## Semmle-specific notes
57+
**Wrapper / common-caller pattern.** The query searches for IRQL-changing calls between save and restore in either their shared enclosing function, or — when one or both endpoints sit inside a thin one-level helper (e.g. `save_fp_helper` forwarding to `KeSaveFloatingPointState`) — in the common caller of those helpers.
58+
59+
**Known false negatives:**
60+
61+
* **IRQL changes deep inside helper bodies.** If a helper raises/lowers IRQL between its entry and the save/restore primitive it forwards to, that change isn't visible from the common caller. Annotate the helper with `_IRQL_raises_` / `_IRQL_saves_global_` to make its IRQL behavior visible without body inspection.
62+
* **Indirect calls.** IRQL changes via function pointer or dispatch-table dispatch are not recognized; the predicate inspects only the static call target.
63+
* **Loops where restore is textually before save.** The AST-loop branch of `irqlChangesBetween` correctly recognizes such patterns, but the upstream IRQL cascade does not always bind at `KeSaveFloatingPointState`'s argument expression inside loop bodies, so the `irqlSource != irqlSink` filter rejects them before this predicate fires. Recovering this case needs work in `Irql.qll`.
64+
* **Wrapper chains longer than one level.** Only one level of helper wrapping is modelled. Multi-level wrappers need the annotation hint above, or a direct call site.

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

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,4 +60,51 @@
6060
</a>
6161
</li>
6262
</references>
63+
<semmleNotes>
64+
<!-- === AI-generated === -->
65+
<p>
66+
<b>Wrapper / common-caller pattern.</b> The query searches for
67+
IRQL-changing calls between save and restore in either their
68+
shared enclosing function, or &#8212; when one or both endpoints
69+
sit inside a thin one-level helper (e.g.
70+
<code>save_fp_helper</code> forwarding to
71+
<code>KeSaveFloatingPointState</code>) &#8212; in the common
72+
caller of those helpers.
73+
</p>
74+
<p>
75+
<b>Known false negatives:</b>
76+
</p>
77+
<ul>
78+
<li>
79+
<b>IRQL changes deep inside helper bodies.</b> If a helper
80+
raises/lowers IRQL between its entry and the save/restore
81+
primitive it forwards to, that change isn't visible from
82+
the common caller. Annotate the helper with
83+
<code>_IRQL_raises_</code> /
84+
<code>_IRQL_saves_global_</code> to make its IRQL behavior
85+
visible without body inspection.
86+
</li>
87+
<li>
88+
<b>Indirect calls.</b> IRQL changes via function pointer or
89+
dispatch-table dispatch are not recognized; the predicate
90+
inspects only the static call target.
91+
</li>
92+
<li>
93+
<b>Loops where restore is textually before save.</b> The
94+
AST-loop branch of <code>irqlChangesBetween</code>
95+
correctly recognizes such patterns, but the upstream IRQL
96+
cascade does not always bind at
97+
<code>KeSaveFloatingPointState</code>'s argument expression
98+
inside loop bodies, so the
99+
<code>irqlSource != irqlSink</code> filter rejects them
100+
before this predicate fires. Recovering this case needs
101+
work in <code>Irql.qll</code>.
102+
</li>
103+
<li>
104+
<b>Wrapper chains longer than one level.</b> Only one level
105+
of helper wrapping is modelled. Multi-level wrappers need
106+
the annotation hint above, or a direct call site.
107+
</li>
108+
</ul>
109+
</semmleNotes>
63110
</qhelp>

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

Lines changed: 130 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
* @tags correctness
1818
* ca_ported
1919
* @scope domainspecific
20-
* @query-version v1
20+
* @query-version v6
2121
*/
2222

2323
import cpp
@@ -42,12 +42,139 @@ module FloatStateFlowConfig implements DataFlow::ConfigSig {
4242

4343
module FloatStateFlow = DataFlow::Global<FloatStateFlowConfig>;
4444

45-
from DataFlow::Node source, DataFlow::Node sink, int irqlSink, int irqlSource
45+
/**
46+
* --- AI-generated ---
47+
*
48+
* Gets a source line in `f` that anchors `fc` from `f`'s perspective:
49+
*
50+
* - If `fc`'s enclosing function is `f`, the anchor is `fc`'s own
51+
* start line.
52+
* - Otherwise, if `f` contains a call site whose static target is
53+
* `fc`'s enclosing function, the anchor is that call site's start
54+
* line. (One-level wrapper case.)
55+
*
56+
* This lets `irqlChangesBetween` reason about the relative source
57+
* position of the save and the restore in any function that either
58+
* directly contains the call or calls the helper that does.
59+
*/
60+
private int anchorLineForCall(Function f, FunctionCall fc) {
61+
f = fc.getEnclosingFunction() and
62+
result = fc.getLocation().getStartLine()
63+
or
64+
exists(FunctionCall site |
65+
site.getEnclosingFunction() = f and
66+
site.getTarget() = fc.getEnclosingFunction() and
67+
f != fc.getEnclosingFunction() and
68+
result = site.getLocation().getStartLine()
69+
)
70+
}
71+
72+
/**
73+
* --- AI-generated ---
74+
*
75+
* Holds if some IRQL-changing call could run between `saveCall` and
76+
* `restoreCall` at runtime. Used as a sanity filter on top of the
77+
* dataflow result: dataflow already paired save -> restore, but
78+
* without this filter we'd flag pairs whose hypothetical entry IRQLs
79+
* differ even though no actual IRQL transition runs between them.
80+
*
81+
* Two additive disjuncts:
82+
*
83+
* 1. **Source-position branch.** A `FunctionCall` `mid` syntactically
84+
* inside some `f` has `isIrqlChangingCall(mid)` and lies on a
85+
* source line bracketed by `anchorLineForCall(f, save/restoreCall)`.
86+
* Two cross-function reach mechanisms with different depth bounds
87+
* cooperate: `anchorLineForCall` walks at most one call-graph edge
88+
* (we need a concrete line in `f` to anchor each endpoint), but
89+
* `isIrqlChangingCall` is transitively recursive through
90+
* `isIrqlChangingFunction`, so `mid`'s target can chain through any
91+
* number of wrappers before reaching a primitive (`KeRaiseIrql`,
92+
* `_IRQL_raises_`, etc.).
93+
*
94+
* 2. **AST-loop branch.** All three calls share an enclosing loop body
95+
* in the same function. The back-edge makes any IRQL-changing call
96+
* in the loop a real transition between save and restore on a
97+
* subsequent iteration, including when restore is textually above
98+
* save (which makes branch 1's range empty).
99+
*
100+
* We use source-line bracketing rather than CFG reachability because
101+
* the extracted cpp CFG can drop forward edges across `if (call(...))`
102+
* and similar boundaries, silently losing TPs. The AST relation in
103+
* branch 2 is densely populated and avoids that gap.
104+
*
105+
* Caveat: `getPotentialExitIrqlAtCfn` doesn't always bind at save-call
106+
* argument expressions inside loop bodies in current extracted DBs, so
107+
* branch 2 can fire correctly while the upstream `irqlSource != irqlSink`
108+
* still filters it out. Recovering those needs work in `Irql.qll`.
109+
*
110+
* Performance: `pragma[inline_late]` + `bindingset[saveCall, restoreCall]`
111+
* specialize this per call site after dataflow has bound the endpoints,
112+
* turning a codebase-wide enumeration of (save, restore) pairs into a
113+
* per-pair check. Both annotations are planner hints; semantics unchanged.
114+
*
115+
* --- Human comments ---
116+
*
117+
* Branch (1) wound up like this for perf reasons as well; a transitive
118+
* check across all of the helper's internals gets expensive and in practice
119+
* if there are helper functions involved they're pretty shallow.
120+
*/
121+
bindingset[saveCall, restoreCall]
122+
pragma[inline_late]
123+
predicate irqlChangesBetween(FunctionCall saveCall, FunctionCall restoreCall) {
124+
// Branch 1: source-line bracketing in a function `f` that anchors
125+
// both calls (directly enclosing or one-level wrapper / common caller).
126+
exists(Function f, int saveLine, int restoreLine, FunctionCall mid |
127+
saveLine = anchorLineForCall(f, saveCall) and
128+
restoreLine = anchorLineForCall(f, restoreCall) and
129+
mid.getEnclosingFunction() = f and
130+
isIrqlChangingCall(mid) and
131+
mid.getLocation().getStartLine() >= saveLine and
132+
mid.getLocation().getStartLine() <= restoreLine and
133+
mid != saveCall and
134+
mid != restoreCall
135+
)
136+
or
137+
// Branch 2: all three calls live inside the body of the same loop in
138+
// their shared enclosing function. The loop back-edge makes any
139+
// IRQL-changing call in the body a real transition between save and
140+
// restore on a subsequent iteration, even when source-line position
141+
// would put restore before save.
142+
exists(Function f, Loop l, FunctionCall mid |
143+
f = saveCall.getEnclosingFunction() and
144+
f = restoreCall.getEnclosingFunction() and
145+
f = mid.getEnclosingFunction() and
146+
isIrqlChangingCall(mid) and
147+
mid != saveCall and
148+
mid != restoreCall and
149+
l.getStmt().getAChild*() = saveCall.getEnclosingStmt() and
150+
l.getStmt().getAChild*() = restoreCall.getEnclosingStmt() and
151+
l.getStmt().getAChild*() = mid.getEnclosingStmt()
152+
)
153+
}
154+
155+
from
156+
DataFlow::Node source, DataFlow::Node sink, int irqlSink, int irqlSource,
157+
FunctionCall saveCall, FunctionCall restoreCall
46158
where
47159
FloatStateFlow::flow(source, sink) and
160+
// FloatStateFlow's source/sink predicates already restrict the flow's
161+
// endpoints to be the first arguments of KeSaveFloatingPointState /
162+
// KeRestoreFloatingPointState. The two arg(0) equalities below
163+
// uniquely bind `saveCall` and `restoreCall` (each Expr has exactly
164+
// one parent FunctionCall), without re-stating the function-name
165+
// constraints.
166+
source.asIndirectExpr() = saveCall.getArgument(0) and
167+
sink.asIndirectExpr() = restoreCall.getArgument(0) and
48168
irqlSource = getPotentialExitIrqlAtCfn(source.asIndirectExpr()) and
49169
irqlSink = getPotentialExitIrqlAtCfn(sink.asIndirectExpr()) and
50-
irqlSink != irqlSource
170+
irqlSink != irqlSource and
171+
// Only flag if there is an actual IRQL-changing call between the save
172+
// and the restore (in source order), in either the directly enclosing
173+
// function or a one-level wrapper / common-caller. If no IRQL-changing
174+
// call exists between them, the IRQL is invariant within a single
175+
// invocation and the mismatch is a may-analysis artifact from
176+
// different hypothetical entry IRQLs.
177+
irqlChangesBetween(saveCall, restoreCall)
51178
select sink.asIndirectExpr(),
52179
"The irql level where the floating-point state was saved (" + irqlSource +
53180
") does not match the irql level for the restore operation (" + irqlSink + ")."

0 commit comments

Comments
 (0)