Skip to content

Commit 7848c04

Browse files
committed
[AI] Reduce verbosity of AI comments + other cleanup.
1 parent 9a8eba1 commit 7848c04

15 files changed

Lines changed: 246 additions & 294 deletions

File tree

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -54,11 +54,11 @@ Correct example
5454
* [ C28111 ](https://learn.microsoft.com/en-us/windows-hardware/drivers/devtest/28111-floating-point-irql-mismatch)
5555

5656
## Semmle-specific notes
57-
**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).
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.
5858

59-
**Remaining limitations.** Despite the source-position and AST-loop branches, the predicate still does not detect:
59+
**Known false negatives:**
6060

61-
* **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.
62-
* **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.
63-
* **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.
64-
* **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.
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: 30 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -61,60 +61,49 @@
6161
</li>
6262
</references>
6363
<semmleNotes>
64+
<!-- === AI-generated === -->
6465
<p>
65-
<b>Wrapper / common-caller pattern.</b> The query reasons about
66-
IRQL-changing calls between save and restore not only when both
67-
calls share an enclosing function, but also when they sit inside
68-
one-level helper wrappers that are called from a common caller
69-
(for example, thin <code>save_fp_helper</code> /
70-
<code>restore_fp_helper</code> functions that simply forward to
71-
<code>KeSaveFloatingPointState</code> /
72-
<code>KeRestoreFloatingPointState</code>). In those cases the
73-
intermediate IRQL transition is searched in the common caller
74-
(or in either helper's enclosing function for the asymmetric case
75-
where one side is a helper and the other is direct).
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.
7673
</p>
7774
<p>
78-
<b>Remaining limitations.</b> Despite the source-position and
79-
AST-loop branches, the predicate still does not detect:
75+
<b>Known false negatives:</b>
8076
</p>
8177
<ul>
8278
<li>
83-
<b>IRQL changes performed deep inside helper bodies.</b>
84-
If the helper function itself raises or lowers the IRQL after
85-
the save (or before the restore), the change is not visible
86-
from the common caller's source-position view, and no
87-
intermediate IRQL change is found. Annotating the helper with
88-
<code>_IRQL_raises_</code> or <code>_IRQL_saves_global_</code>
89-
makes its IRQL behavior visible without body inspection.
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.
9086
</li>
9187
<li>
92-
<b>Indirect calls.</b> IRQL changes performed by an indirect
93-
call (function pointer or dispatch-table call) between save
94-
and restore are not detected, because the predicate only
95-
inspects the static call target.
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.
9691
</li>
9792
<li>
98-
<b>Loops where the restore is textually before the save.</b>
99-
The AST-loop branch of <code>irqlChangesBetween</code>
100-
correctly recognises that all three calls (save, restore,
101-
and an IRQL-changing call) sit inside the same loop body and
102-
would fire on this pattern. However, the upstream IRQL
103-
analysis library used to compute the IRQL at the save and
104-
restore sites does not consistently bind a value at the
105-
argument expression of <code>KeSaveFloatingPointState</code>
106-
when the call is inside a loop body, so the
107-
<code>irqlSource != irqlSink</code> filter rejects these
108-
cases before <code>irqlChangesBetween</code> is consulted.
109-
Recovering this true positive requires improvements to the
110-
IRQL analysis library and not just to this query.
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>.
111102
</li>
112103
<li>
113104
<b>Wrapper chains longer than one level.</b> Only one level
114-
of wrapping is currently modelled (the helper is called
115-
directly from the common caller). Multi-level wrappers
116-
require the same annotation hint described above, or a
117-
direct call site.
105+
of helper wrapping is modelled. Multi-level wrappers need
106+
the annotation hint above, or a direct call site.
118107
</li>
119108
</ul>
120109
</semmleNotes>

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

Lines changed: 42 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,8 @@ module FloatStateFlowConfig implements DataFlow::ConfigSig {
4343
module FloatStateFlow = DataFlow::Global<FloatStateFlowConfig>;
4444

4545
/**
46+
* --- AI-generated ---
47+
*
4648
* Gets a source line in `f` that anchors `fc` from `f`'s perspective:
4749
*
4850
* - If `fc`'s enclosing function is `f`, the anchor is `fc`'s own
@@ -68,76 +70,53 @@ private int anchorLineForCall(Function f, FunctionCall fc) {
6870
}
6971

7072
/**
71-
* Holds if there is an IRQL-changing call between `saveCall` and
72-
* `restoreCall` in some function `f`. This predicate is a sanity filter
73-
* applied on top of the dataflow result: dataflow has already shown the
74-
* floating-point buffer flows from `saveCall` to `restoreCall`, and this
75-
* predicate ensures there is at least one IRQL transition that could
76-
* actually run between them. Without it the query would emit the pure
77-
* may-analysis artifact where two save / restore sites are compared at
78-
* different hypothetical entry IRQLs but no IRQL transition can happen
79-
* between them at runtime.
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.
8080
*
81-
* Two complementary disjuncts cooperate:
81+
* Two additive disjuncts:
8282
*
83-
* 1. **Source-position branch.** For some `f`, an IRQL-changing call
84-
* `mid` in `f` lies on a source line bracketed by the anchor lines
85-
* of `saveCall` and `restoreCall` (see `anchorLineForCall`). The
86-
* anchor mechanism lets `f` be the directly enclosing function of
87-
* both calls or a one-level wrapper / common caller, which covers
88-
* the cross-function case that intra-procedural CFG cannot reach.
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.).
8993
*
90-
* 2. **AST-loop branch.** All three calls (`saveCall`, `restoreCall`,
91-
* `mid`) sit inside the body of the same loop in their common
92-
* enclosing function. The loop back-edge means that at runtime
93-
* each iteration's `restoreCall` can be preceded by the previous
94-
* iteration's `saveCall` with `mid` between them, so an
95-
* IRQL-changing `mid` anywhere in the loop body is a real
96-
* transition between save and restore even when `restoreCall` is
97-
* textually above `saveCall`. Source-line position alone cannot
98-
* express this: when the restore is textually earlier than the
99-
* save the bracketing line range is empty and branch (1) trivially
100-
* fails.
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).
10199
*
102-
* The two branches are disjoint in spirit: branch (1) handles
103-
* cross-function and acyclic in-function cases; branch (2) handles
104-
* intra-function loops and re-entrant patterns. Combining them is
105-
* strictly additive (can only enable more findings, never suppress one
106-
* that branch (1) would have flagged), so existing true positives are
107-
* preserved.
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.
108104
*
109-
* Why not full intra-procedural CFG reachability instead of branch (1)?
110-
* The cpp control-flow graph in some extracted databases does not
111-
* transitively connect calls across certain statement boundaries (in
112-
* particular, forward reachability across `if (call(...))` conditions
113-
* is unreliable in our extracted DBs), which would silently eliminate
114-
* true positives that branch (1) catches via source-line bracketing.
115-
* AST-loop containment in branch (2) sidesteps this by relying on the
116-
* AST `Loop.getStmt().getAChild*()` relation, which is densely
117-
* populated and reflects the syntactic loop body directly.
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`.
118109
*
119-
* Caveat: branch (2) cooperates with `irqlSource != irqlSink` only when
120-
* the IRQL-analysis library binds `getPotentialExitIrqlAtCfn` at the
121-
* argument expression of `KeSaveFloatingPointState`. In our current
122-
* extracted DBs that binding is not always produced for `save` calls
123-
* inside loop bodies, so some real-world loop true positives may
124-
* still be filtered out by the upstream IRQL filter even when this
125-
* predicate fires; recovering those will require improvements to
126-
* the IRQL analysis library itself.
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.
127114
*
128-
* Performance note: `pragma[inline_late]` lets the planner specialize
129-
* this predicate at its call site after the dataflow result has bound
130-
* `saveCall` and `restoreCall`. Without it, the body would otherwise
131-
* be materialized over every (saveCall, restoreCall) pair in the
132-
* codebase that satisfies the constraints (millions of tuples on
133-
* large drivers), only to be intersected with a much smaller dataflow
134-
* result set afterwards. With it, the body is evaluated only for the
135-
* dataflow-derived pairs, turning a codebase-wide enumeration into a
136-
* per-pair check. The accompanying `bindingset` records the calling
137-
* convention required by `inline_late` (both arguments bound at the
138-
* call site, which is satisfied by the `from` clause below).
139-
* Semantics are unchanged — both annotations are planner hints, not
140-
* logical changes.
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.
141120
*/
142121
bindingset[saveCall, restoreCall]
143122
pragma[inline_late]

src/drivers/general/queries/IrqlSetTooHigh/IrqlSetTooHigh.md

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,5 @@ This query may provide false positives in cases where functions are not annotate
2828
2929
For information on how to annotate your functions with information about how they adjust the IRQL, see "IRQL annotations for drivers" in the references section.
3030
31-
**Lower-on-exit pattern: known false negative.** When a function has no `_IRQL_always_function_max_` but does carry an `_IRQL_raises_(R)` annotation, the query treats `R` as the implicit ceiling for the function body. A function annotated as both `_IRQL_requires_min_(M)` and `_IRQL_raises_(R)` with `M > R` is interpreted as a "lower IRQL on exit" pattern (for example a wrapper around a mutex or spin-lock release that runs at `DISPATCH_LEVEL` on entry and returns at `PASSIVE_LEVEL`). For these functions the implicit ceiling is suppressed entirely, because `R` describes the exit IRQL rather than a maximum.
32-
33-
This means that a buggy "lower-on-exit" function whose body raises the IRQL above `M` at some intermediate point will *not* be flagged. If the function actually has a maximum that should be enforced along the body, declare it explicitly with `_IRQL_always_function_max_(MAX)` so the query has a concrete ceiling to check against.
31+
**Lower-on-exit pattern: known false negative.** A function annotated `_IRQL_requires_min_(M)` + `_IRQL_raises_(R)` with `M > R` is treated as "raises only at exit" (e.g. a wrapper around a spin-lock or mutex release that enters at `DISPATCH_LEVEL` and returns at `PASSIVE_LEVEL`): the query suppresses the implicit ceiling so `R` is read as the exit IRQL rather than a body-wide maximum. Consequently a buggy lower-on-exit function whose body raises IRQL above `M` in the middle is not flagged. To enforce a body-wide maximum, declare it explicitly with `_IRQL_always_function_max_(MAX)`.
3432

src/drivers/general/queries/IrqlSetTooHigh/IrqlSetTooHigh.qhelp

Lines changed: 14 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -36,26 +36,21 @@
3636
<p>This query uses interprocedural data-flow analysis and can take a large amount of CPU time and memory to run.</p>
3737
<p>This query may provide false positives in cases where functions are not annotated with their expected IRQL ranges or behaviors.</p>
3838
<p>For information on how to annotate your functions with information about how they adjust the IRQL, see "IRQL annotations for drivers" in the references section.</p>
39+
<!-- === AI-generated === -->
3940
<p>
40-
<b>Lower-on-exit pattern: known false negative.</b> When a function has
41-
no <code>_IRQL_always_function_max_</code> but does carry an
42-
<code>_IRQL_raises_(R)</code> annotation, the query treats <code>R</code>
43-
as the implicit ceiling for the function body. A function annotated as
44-
both <code>_IRQL_requires_min_(M)</code> and
45-
<code>_IRQL_raises_(R)</code> with <code>M &gt; R</code> is interpreted
46-
as a "lower IRQL on exit" pattern (for example a wrapper around a mutex
47-
or spin-lock release that runs at <code>DISPATCH_LEVEL</code> on entry
48-
and returns at <code>PASSIVE_LEVEL</code>). For these functions the
49-
implicit ceiling is suppressed entirely, because <code>R</code> describes
50-
the exit IRQL rather than a maximum.
51-
</p>
52-
<p>
53-
This means that a buggy "lower-on-exit" function whose body raises the
54-
IRQL above <code>M</code> at some intermediate point will <i>not</i> be
55-
flagged. If the function actually has a maximum that should be enforced
56-
along the body, declare it explicitly with
57-
<code>_IRQL_always_function_max_(MAX)</code> so the query has a concrete
58-
ceiling to check against.
41+
<b>Lower-on-exit pattern: known false negative.</b> A function
42+
annotated <code>_IRQL_requires_min_(M)</code> +
43+
<code>_IRQL_raises_(R)</code> with <code>M &gt; R</code> is
44+
treated as "raises only at exit" (e.g. a wrapper around a
45+
spin-lock or mutex release that enters at
46+
<code>DISPATCH_LEVEL</code> and returns at
47+
<code>PASSIVE_LEVEL</code>): the query suppresses the
48+
implicit ceiling so <code>R</code> is read as the exit IRQL
49+
rather than a body-wide maximum. Consequently a buggy
50+
lower-on-exit function whose body raises IRQL above
51+
<code>M</code> in the middle is not flagged. To enforce a
52+
body-wide maximum, declare it explicitly with
53+
<code>_IRQL_always_function_max_(MAX)</code>.
5954
</p>
6055
</semmleNotes>
6156
</qhelp>

0 commit comments

Comments
 (0)