Skip to content

Commit 4cacaf0

Browse files
NateD-MSFTCopilot
andcommitted
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>
1 parent a76f855 commit 4cacaf0

14 files changed

Lines changed: 994 additions & 482 deletions

File tree

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

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -142,18 +142,23 @@ from
142142
FunctionCall saveCall, FunctionCall restoreCall
143143
where
144144
FloatStateFlow::flow(source, sink) and
145-
saveCall.getTarget().getName().matches("KeSaveFloatingPointState") and
145+
// FloatStateFlow's source/sink predicates already restrict the flow's
146+
// endpoints to be the first arguments of KeSaveFloatingPointState /
147+
// KeRestoreFloatingPointState. The two arg(0) equalities below
148+
// uniquely bind `saveCall` and `restoreCall` (each Expr has exactly
149+
// one parent FunctionCall), without re-stating the function-name
150+
// constraints.
146151
source.asIndirectExpr() = saveCall.getArgument(0) and
147-
restoreCall.getTarget().getName().matches("KeRestoreFloatingPointState") and
148152
sink.asIndirectExpr() = restoreCall.getArgument(0) and
149153
irqlSource = getPotentialExitIrqlAtCfn(source.asIndirectExpr()) and
150154
irqlSink = getPotentialExitIrqlAtCfn(sink.asIndirectExpr()) and
151155
irqlSink != irqlSource and
152-
// Only flag if there is an actual IRQL-changing call in the same function
153-
// between save and restore (in source order). If no IRQL-changing call
154-
// exists between them, the IRQL is invariant within a single invocation
155-
// and the mismatch is a may-analysis artifact from different hypothetical
156-
// entry IRQLs.
156+
// Only flag if there is an actual IRQL-changing call between the save
157+
// and the restore (in source order), in either the directly enclosing
158+
// function or a one-level wrapper / common-caller. If no IRQL-changing
159+
// call exists between them, the IRQL is invariant within a single
160+
// invocation and the mismatch is a may-analysis artifact from
161+
// different hypothetical entry IRQLs.
157162
irqlChangesBetween(saveCall, restoreCall)
158163
select sink.asIndirectExpr(),
159164
"The irql level where the floating-point state was saved (" + irqlSource +

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -83,8 +83,8 @@
8383
"level": "warning"
8484
},
8585
"help": {
86-
"text": "# Irql Float State Mismatch\nThe IRQL where the floating-point state was saved does not match the current IRQL (for this restore operation).\n\n\n## Recommendation\nThe IRQL at which the driver is executing when it restores a floating-point state is different than the IRQL at which it was executing when it saved the floating-point state. Because the IRQL at which the driver runs determines how the floating-point state is saved, the driver must be executing at the same IRQL when it calls the functions to save and to restore the floating-point state.\n\n\n## Example\nExample of incorrect code. Floating point state was saved at APC_LEVEL but restored at PASSIVE_LEVEL\n\n```c\n \n\t\t_IRQL_requires_(PASSIVE_LEVEL) \n\t\tvoid driver_utility_bad(void)\n\t\t{\n\t\t\tKIRQL oldIRQL;\n\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\t\t\t// running at APC level\n\t\t\tKFLOATING_SAVE FloatBuf;\n\t\t\tif (KeSaveFloatingPointState(&FloatBuf))\n\t\t\t{\n\t\t\t\tKeLowerIrql(oldIRQL); // lower back to PASSIVE_LEVEL\n\t\t\t\t// ...\n\t\t\t\tKeRestoreFloatingPointState(&FloatBuf);\n\t\t\t}\n\t\t}\n\t\t\n```\nCorrect example\n\n```c\n \n\t\t\t_IRQL_requires_(PASSIVE_LEVEL) \n\t\t\tvoid driver_utility_good(void)\n\t\t\t{\n\t\t\t\t// running at APC level\n\t\t\t\tKFLOATING_SAVE FloatBuf;\n\t\t\t\tKIRQL oldIRQL;\n\t\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\n\t\t\t\tif (KeSaveFloatingPointState(&FloatBuf))\n\t\t\t\t{\n\t\t\t\t\tKeLowerIrql(oldIRQL);\n\t\t\t\t\t// ...\n\t\t\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\t\t\t\t\tKeRestoreFloatingPointState(&FloatBuf);\n\t\t\t\t}\n\t\t\t}\n\t\t\n```\n\n## References\n* [ C28111 ](https://learn.microsoft.com/en-us/windows-hardware/drivers/devtest/28111-floating-point-irql-mismatch)\n\n## Semmle-specific notes\n**Known false negatives.** The query suppresses save / restore pairs when no IRQL-changing call sits between the save call and the restore call on a source line that lies textually within the enclosing function. This suppression eliminates a class of may-analysis false positives where the save and the restore are at the same IRQL within a single dynamic invocation but the IRQL inference reports different hypothetical entry IRQLs. The check has the following limitations:\n\n* **Cross-function save / restore.** When the save and the restore are routed through helper functions that wrap `KeSaveFloatingPointState` / `KeRestoreFloatingPointState`, and the IRQL change happens in the caller, no in-function intermediate call is found and the mismatch is silently suppressed.\n* **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.\n* **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.\nIf a real mismatch is being suppressed, eliminate the wrapper or add explicit `_IRQL_raises_` / `_IRQL_saves_global_` annotations to the helper so its IRQL behavior is visible without body inspection.\n\n",
87-
"markdown": "# Irql Float State Mismatch\nThe IRQL where the floating-point state was saved does not match the current IRQL (for this restore operation).\n\n\n## Recommendation\nThe IRQL at which the driver is executing when it restores a floating-point state is different than the IRQL at which it was executing when it saved the floating-point state. Because the IRQL at which the driver runs determines how the floating-point state is saved, the driver must be executing at the same IRQL when it calls the functions to save and to restore the floating-point state.\n\n\n## Example\nExample of incorrect code. Floating point state was saved at APC_LEVEL but restored at PASSIVE_LEVEL\n\n```c\n \n\t\t_IRQL_requires_(PASSIVE_LEVEL) \n\t\tvoid driver_utility_bad(void)\n\t\t{\n\t\t\tKIRQL oldIRQL;\n\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\t\t\t// running at APC level\n\t\t\tKFLOATING_SAVE FloatBuf;\n\t\t\tif (KeSaveFloatingPointState(&FloatBuf))\n\t\t\t{\n\t\t\t\tKeLowerIrql(oldIRQL); // lower back to PASSIVE_LEVEL\n\t\t\t\t// ...\n\t\t\t\tKeRestoreFloatingPointState(&FloatBuf);\n\t\t\t}\n\t\t}\n\t\t\n```\nCorrect example\n\n```c\n \n\t\t\t_IRQL_requires_(PASSIVE_LEVEL) \n\t\t\tvoid driver_utility_good(void)\n\t\t\t{\n\t\t\t\t// running at APC level\n\t\t\t\tKFLOATING_SAVE FloatBuf;\n\t\t\t\tKIRQL oldIRQL;\n\t\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\n\t\t\t\tif (KeSaveFloatingPointState(&FloatBuf))\n\t\t\t\t{\n\t\t\t\t\tKeLowerIrql(oldIRQL);\n\t\t\t\t\t// ...\n\t\t\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\t\t\t\t\tKeRestoreFloatingPointState(&FloatBuf);\n\t\t\t\t}\n\t\t\t}\n\t\t\n```\n\n## References\n* [ C28111 ](https://learn.microsoft.com/en-us/windows-hardware/drivers/devtest/28111-floating-point-irql-mismatch)\n\n## Semmle-specific notes\n**Known false negatives.** The query suppresses save / restore pairs when no IRQL-changing call sits between the save call and the restore call on a source line that lies textually within the enclosing function. This suppression eliminates a class of may-analysis false positives where the save and the restore are at the same IRQL within a single dynamic invocation but the IRQL inference reports different hypothetical entry IRQLs. The check has the following limitations:\n\n* **Cross-function save / restore.** When the save and the restore are routed through helper functions that wrap `KeSaveFloatingPointState` / `KeRestoreFloatingPointState`, and the IRQL change happens in the caller, no in-function intermediate call is found and the mismatch is silently suppressed.\n* **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.\n* **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.\nIf a real mismatch is being suppressed, eliminate the wrapper or add explicit `_IRQL_raises_` / `_IRQL_saves_global_` annotations to the helper so its IRQL behavior is visible without body inspection.\n\n"
86+
"text": "# Irql Float State Mismatch\nThe IRQL where the floating-point state was saved does not match the current IRQL (for this restore operation).\n\n\n## Recommendation\nThe IRQL at which the driver is executing when it restores a floating-point state is different than the IRQL at which it was executing when it saved the floating-point state. Because the IRQL at which the driver runs determines how the floating-point state is saved, the driver must be executing at the same IRQL when it calls the functions to save and to restore the floating-point state.\n\n\n## Example\nExample of incorrect code. Floating point state was saved at APC_LEVEL but restored at PASSIVE_LEVEL\n\n```c\n \n\t\t_IRQL_requires_(PASSIVE_LEVEL) \n\t\tvoid driver_utility_bad(void)\n\t\t{\n\t\t\tKIRQL oldIRQL;\n\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\t\t\t// running at APC level\n\t\t\tKFLOATING_SAVE FloatBuf;\n\t\t\tif (KeSaveFloatingPointState(&FloatBuf))\n\t\t\t{\n\t\t\t\tKeLowerIrql(oldIRQL); // lower back to PASSIVE_LEVEL\n\t\t\t\t// ...\n\t\t\t\tKeRestoreFloatingPointState(&FloatBuf);\n\t\t\t}\n\t\t}\n\t\t\n```\nCorrect example\n\n```c\n \n\t\t\t_IRQL_requires_(PASSIVE_LEVEL) \n\t\t\tvoid driver_utility_good(void)\n\t\t\t{\n\t\t\t\t// running at APC level\n\t\t\t\tKFLOATING_SAVE FloatBuf;\n\t\t\t\tKIRQL oldIRQL;\n\t\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\n\t\t\t\tif (KeSaveFloatingPointState(&FloatBuf))\n\t\t\t\t{\n\t\t\t\t\tKeLowerIrql(oldIRQL);\n\t\t\t\t\t// ...\n\t\t\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\t\t\t\t\tKeRestoreFloatingPointState(&FloatBuf);\n\t\t\t\t}\n\t\t\t}\n\t\t\n```\n\n## References\n* [ C28111 ](https://learn.microsoft.com/en-us/windows-hardware/drivers/devtest/28111-floating-point-irql-mismatch)\n\n## Semmle-specific notes\n**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).\n\n**Remaining limitations.** The position-based filter still does not detect:\n\n* **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.\n* **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.\n* **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.\n* **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.\n",
87+
"markdown": "# Irql Float State Mismatch\nThe IRQL where the floating-point state was saved does not match the current IRQL (for this restore operation).\n\n\n## Recommendation\nThe IRQL at which the driver is executing when it restores a floating-point state is different than the IRQL at which it was executing when it saved the floating-point state. Because the IRQL at which the driver runs determines how the floating-point state is saved, the driver must be executing at the same IRQL when it calls the functions to save and to restore the floating-point state.\n\n\n## Example\nExample of incorrect code. Floating point state was saved at APC_LEVEL but restored at PASSIVE_LEVEL\n\n```c\n \n\t\t_IRQL_requires_(PASSIVE_LEVEL) \n\t\tvoid driver_utility_bad(void)\n\t\t{\n\t\t\tKIRQL oldIRQL;\n\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\t\t\t// running at APC level\n\t\t\tKFLOATING_SAVE FloatBuf;\n\t\t\tif (KeSaveFloatingPointState(&FloatBuf))\n\t\t\t{\n\t\t\t\tKeLowerIrql(oldIRQL); // lower back to PASSIVE_LEVEL\n\t\t\t\t// ...\n\t\t\t\tKeRestoreFloatingPointState(&FloatBuf);\n\t\t\t}\n\t\t}\n\t\t\n```\nCorrect example\n\n```c\n \n\t\t\t_IRQL_requires_(PASSIVE_LEVEL) \n\t\t\tvoid driver_utility_good(void)\n\t\t\t{\n\t\t\t\t// running at APC level\n\t\t\t\tKFLOATING_SAVE FloatBuf;\n\t\t\t\tKIRQL oldIRQL;\n\t\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\n\t\t\t\tif (KeSaveFloatingPointState(&FloatBuf))\n\t\t\t\t{\n\t\t\t\t\tKeLowerIrql(oldIRQL);\n\t\t\t\t\t// ...\n\t\t\t\t\tKeRaiseIrql(APC_LEVEL, &oldIRQL);\n\t\t\t\t\tKeRestoreFloatingPointState(&FloatBuf);\n\t\t\t\t}\n\t\t\t}\n\t\t\n```\n\n## References\n* [ C28111 ](https://learn.microsoft.com/en-us/windows-hardware/drivers/devtest/28111-floating-point-irql-mismatch)\n\n## Semmle-specific notes\n**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).\n\n**Remaining limitations.** The position-based filter still does not detect:\n\n* **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.\n* **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.\n* **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.\n* **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.\n"
8888
},
8989
"properties": {
9090
"tags": [
@@ -112,7 +112,7 @@
112112
"extensions": [
113113
{
114114
"name": "microsoft/windows-drivers",
115-
"semanticVersion": "1.9.0+2515238ad8912d03a18aab75fcacace2a4f4d307",
115+
"semanticVersion": "1.9.0+a76f8551b47f01adada99ddc44a5ea4fa9839fca",
116116
"locations": [
117117
{
118118
"uri": "file:///F:/source/repos/Windows-Driver-Developer-Supplemental-Tools/src/",
@@ -254,14 +254,14 @@
254254
"text": ""
255255
},
256256
"level": "none",
257-
"timeUtc": "2026-04-28T23:26:00.575823400Z",
257+
"timeUtc": "2026-04-29T04:38:29.808991Z",
258258
"descriptor": {
259259
"id": "cli/file-coverage-baseline",
260260
"index": 1
261261
},
262262
"properties": {
263263
"attributes": {
264-
"durationMilliseconds": 288
264+
"durationMilliseconds": 253
265265
},
266266
"visibility": {
267267
"statusPage": false,
@@ -274,7 +274,7 @@
274274
"text": ""
275275
},
276276
"level": "none",
277-
"timeUtc": "2026-04-28T23:26:00.581682100Z",
277+
"timeUtc": "2026-04-29T04:38:29.815492900Z",
278278
"descriptor": {
279279
"id": "cli/platform",
280280
"index": 2
@@ -297,7 +297,7 @@
297297
"markdown": "Internal telemetry for the C++ extractor.\n\nNo action needed."
298298
},
299299
"level": "note",
300-
"timeUtc": "2026-04-28T23:26:39.590845200Z",
300+
"timeUtc": "2026-04-29T04:39:07.709847200Z",
301301
"descriptor": {
302302
"id": "cpp/extractor/summary",
303303
"index": 3
@@ -369,7 +369,7 @@
369369
"index": 0
370370
},
371371
"region": {
372-
"startLine": 112,
372+
"startLine": 111,
373373
"startColumn": 33,
374374
"endColumn": 36
375375
}

src/drivers/general/queries/IrqlFloatStateMismatch/driver_snippet.c

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -92,14 +92,13 @@ void driver_utility_nested_block_good(void)
9292
// =====================================================================
9393
// Adversarial: cross-function save / restore via thin wrappers.
9494
//
95-
// `irqlChangesBetween` requires `saveCall` and `restoreCall` to
96-
// share an enclosing function, so when the save and the restore
97-
// are routed through helper wrappers and the IRQL change happens
98-
// in the caller, the source-position filter never finds a `mid`
99-
// candidate. No finding is produced even though the IRQL at the
100-
// save (PASSIVE_LEVEL) differs from the IRQL at the restore
101-
// (DISPATCH_LEVEL). This is a known false negative of the
102-
// current intraprocedural filter.
95+
// `irqlChangesBetween` projects each call to an anchor line in either
96+
// the directly enclosing function or a one-level wrapper / common
97+
// caller, so when the save and the restore are routed through helper
98+
// wrappers and the IRQL change happens in the caller, the caller's
99+
// anchor lines bracket the `KeRaiseIrql` call and the mismatch is
100+
// flagged. The IRQL at the save (PASSIVE_LEVEL) differs from the IRQL
101+
// at the restore (DISPATCH_LEVEL) for this case.
103102
// =====================================================================
104103

105104
static void save_fp_helper(PKFLOATING_SAVE pfs)

src/drivers/general/queries/IrqlNotSaved/IrqlNotSaved.ql

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,10 +83,10 @@ module IrqlSaveParameterFlowConfigurationConfig implements DataFlow::ConfigSig {
8383
}
8484

8585
predicate isSink(DataFlow::Node sink) {
86-
// Only track flow to assignment targets or parametersnot every node
86+
// Only track flow to assignment targets or parameters, not every node.
8787
exists(Variable v | v.getAnAssignedValue() = sink.asExpr())
8888
or
89-
exists(sink.asParameter())
89+
sink.asParameter() instanceof Parameter
9090
}
9191
}
9292
module IrqlSaveParameterFlowConfiguration = DataFlow::Global<IrqlSaveParameterFlowConfigurationConfig>;

0 commit comments

Comments
 (0)