[AUTOMATED] feat(p2): cortexmpriv — fold the Cortex-M isCurrentModePrivileged() guard (DIV-99) - #357
Merged
Conversation
…ivileged() guard (DIV-99)
`ARMTHUMBinstructions.sinc` models every VERSION_7M (Cortex-M) special-register
move as a RUNTIME privilege test rather than as one operation:
b:1 = isCurrentModePrivileged();
if (!b) goto <notPriv>;
<the real effect>
<notPriv>
Twelve constructors do it — `mrs`/`msr` against ipsr, primask, basepri,
basepri_max, faultmask and control — so kuna, lowering the model literally, gives
EVERY MRS/MSR one extra basic block and two extra CFG edges that exist in no
source. A four-instruction `irq_disable`/`irq_restore` pair therefore lands four
phantom branches in the middle of an otherwise straight-line function; RIOT's
`thread_sleep` and NuttX's `nxsched_process_scheduler` score GED 24 and 26
against straight-line source for that reason alone. Upstream Ghidra shares the
defect; IDA and Binary Ninja model MRS/MSR as a plain intrinsic and score 6 and 0
on the same functions.
`p2_lift/kuna_cortexmpriv.rs` supplies a `<callotherfixup>` body for the user op
— the constant `1` — so the guard condition constant-folds, its block and edges
die, and the real effect survives untouched. The payload is synthesized in Rust
rather than added to a `.cspec`, so the vendored spec tree stays byte-identical
to upstream, and `architecture.rs (register_cortexmpriv_fixup)` installs it
between the cspec `<callotherfixup>` dispatch and `parse_inject_all` — only where
a local `.sla` can compile it, only on a language whose translator presents the
user op, and only when no compiler spec has already specialized it.
"The core is privileged" is a MODELLING JUDGEMENT, not a proof (Cortex-M Thread
mode can run unprivileged, and there those moves really do read as zero), so it
ships as `option cortexmpriv`, default off and ON in the `aggressive` preset —
which `auto` selects for anything under 500 KiB, i.e. essentially every Cortex-M
image. Because the architecture bootstraps at `load file`, before any `option`
line, the flag is read at the CONSUMPTION seam instead:
`decompile_drive.rs (is_injected_userop)`, the one live per-CALLOTHER predicate
that sees the applied options.
Measured over the 26 guard-bearing decbench binaries (46,747 function bodies,
`decompile-all --json --max-fn-seconds 120`, exactly as the benchmark runs it):
discovery identical on all 26 (nA == nB), errors identical
changed bodies 868
of which guarded 868 (ZERO non-guard collateral)
`cortexmpriv off` byte-identical to unmodified HEAD on all 46,747 bodies
plus 10 control binaries (4,148 bodies, one of them ARM with no MRS/MSR):
0 changed lines against HEAD at the shipped default.
The synthesized payload compiles at architecture bootstrap on all 15 ARM language
variants (LE and BE, v4 through v8-m), and is a measured no-op on AArch64 and
x86-64.
Gates: `make test` 675/675 PARITY OK (no re-pin), `make test-stages` 572/572
PARITY OK (568 -> 572, baseline re-recorded for the new stage test),
`make check-spec` green in lenient and strict mode, `kuna catalog --check` OK.
Catalog 125 -> 126 settables (transform tier 51 -> 52). Stages corpus 220 -> 221
files.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FvpHGrvHyKDNmLSPVnZw2G
…surement it rests on
The evidence half of the `cortexmpriv` change: the DIV-99 row in `docs/history.md` and
`docs/decbench/cortexmpriv-measurement.md`, the file it points at. Also moves
`register_cortexmpriv_fixup` below `init_userops_and_fixups` so it stops stealing that
function's doc comment (pure relocation, no code change).
Corpus-scale and bidirectional (`scripts.decbench.optsweep`, 90 Cortex-M slices over
O0 / O2 / O2-noinline, 31,044 functions scored in BOTH arms, one kuna binary invoked
exactly as decbench's `kuna_raw` backend does; baseline arm = the shipped branch
defaults, variant arm = `--option cortexmpriv off`, i.e. main HEAD):
to GED-perfect 93 off GED-perfect 0 (McNemar z = 9.64)
improved 336 worsened 98
aggregate GED 236,133 -> 230,129 -6,004
GED removed/added -7,033 / +1,029 6.8 : 1
Controls all clean: 30,600 unchanged bodies score identically, 0 slug-only diffs, and
the baseline arm agrees with the tree's published per-function verdict on
30,612/31,044 (98.6%). `betaflight` is 533 KB, so `auto` picks `reliable`, the preset
never reaches it, and its two arms are identical -- a control inside the sweep.
DecBench sample set: +2. Only 49 of the 250 sit on a guard-bearing binary; all 49
re-scored in both arms, four change, none regresses:
O0-riot-os-hello-world-thread_sleep 24 -> 0 FLIP
O0-nuttx-nuttx-nxsched_process_scheduler 26 -> 0 FLIP
O2-noinline-freertos-RTOSDemo-xFirstTimerHandler 84 -> 14
O0-nuttx-nuttx-nxsig_find_pendingsignal 18 -> 9
Neither flip was perfect on any metric before, so both are genuine `overall` gains.
Speed: flat, and the row says so with a null control rather than a bare number. The
same arm compared against itself on cf2.elf reads -4.81% at min-of-9, so nothing inside
+-5% at that rep count is signal on this box; the two min-of-21 readings (nuttx -0.7%,
chibios/ch.elf +0.2%) are the usable ones.
Stated plainly in both files: 98 of the 434 changed functions score WORSE on GED. That
is the metric, not lost recovery -- GED counts blocks and edges, so deleting phantom
blocks widens the node deficit wherever kuna's CFG is already smaller than the source's.
The 336 wins have a median source CFG of 4 nodes, the 98 losses a median of 11, and the
emitted `on` body is always the `off` body minus the guards.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FvpHGrvHyKDNmLSPVnZw2G
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
specs/Ghidra/Processors/ARM/data/languages/ARMTHUMBinstructions.sincmodels every Cortex-M (VERSION_7M) MRS/MSR asTwelve constructors, all inside
@if defined(VERSION_7M). kuna lowers that literally, so each MRS/MSR costs one basic block and two CFG edges that exist in no source. Ghidra shares the defect exactly (GED 26 on NuttXnxsched_process_scheduler); IDA and Binary Ninja model MRS/MSR as a plain intrinsic and score 6 and 0.How
A synthesized
<callotherfixup>for the ARM user opisCurrentModePrivilegedreturning the constant1, installed throughUserOpManage::manual_call_other_fixupat architecture bootstrap.specs/is untouched — that is the point of doing this as a fixup rather than a spec edit (git diff main...feat/cortexmpriv -- specs/is empty).The option is read at the CALLOTHER consumption gate (
decompile_drive::is_injected_userop), not at registration, because the payload is installed before anyoptionline is processed.Default OFF, in
AGGRESSIVE_OVERRIDES. "The core is privileged" is a modelling judgement, not a proof — Cortex-M Thread mode can run unprivileged — which is exactly what an option is for.Measured
Sample set: +2 overall-perfect, both verified individually through decbench's own
GEDMetric:O0-riot-os-hello-world-thread_sleepO0-nuttx-nuttx-nxsched_process_schedulerO0-nuttx-nuttx-nxsig_find_pendingsignalO2-noinline-freertos-RTOSDemo-xFirstTimerHandlerThe author explicitly corrected the brief here: it is +2, not +4 — the other two named cases improve but do not reach GED 0.
Corpus (the eight Cortex-M projects, the only population that can change; 90 slices / 31,044 functions in both arms): to GED-perfect 93, off GED-perfect 0 (McNemar z = 9.64), improved 336 / worsened 98, aggregate GED −6,004 (−7,033 removed against +1,029 added).
Zero collateral, measured not assumed: over the 26 guard-bearing binaries (46,747 bodies) discovery is identical on all 26 (same function set, same error count), and of 868 changed bodies all 868 are guard-bearing.
Speed flat, established with a null control rather than a bare number: running the identical harness off-vs-itself reads −4.8%, so anything inside ±5% at that rep count is noise. The two highest-rep readings are nuttx −0.7% and chibios +0.2% (both min-of-21). Off ARM the payload is never registered, so the cost is structurally zero.
Honest caveat carried in the DIV row: 98 of 434 changed functions score worse on GED (+1,029 against −7,033). That is the metric, not lost information.
Gates
make test— 675/675 PARITY OK (no re-pin; the datatest corpus has no Cortex-M bytechunk and cannot observe this)make test-stages— 574/574 PARITY OK with the new two-passtests/stages/kuna-cortexmpriv.xmlmake rust-test— green, 330 result blocks, 0 failuresmake check-spec— green in lenient and strict modekuna catalog --check— greenRebased onto
voidtailreturn(#356); all six hard-coded catalog counts reconciled to base+both (127 settables, tier 28/52/47, live 39, static rows 126, corpus 222 files) and the DIV renumbered 99. An independent adversarial review re-ran every gate in its own worktree and re-scored both flips: verdict ship.🤖 Generated with Claude Code
https://claude.ai/code/session_01FvpHGrvHyKDNmLSPVnZw2G