wcet: name the op and byte offset in an unmodeled-op decline (#921) - #922
Merged
Conversation
gale got 9 of 31 functions declined with {name, reason, note} and nothing else
— the second-largest category, actionable only by hand-bisecting the object.
Adds optional `op` + `offset` to the decline record, additive so existing
consumers are unaffected.
`op` is derived from Debug, not a hand-maintained table (no mirror to drift).
`offset` comes from the REAL encoder, the same source WcetLoopBound uses, and
is OMITTED rather than estimated when it cannot be computed — a drifted offset
is worse than none.
CORRECTS A FALSE DOC CLAIM: the variant said it was 'never emitted in a released
build (the classifier is exhaustive with no wildcard)'. op_cost indeed has no
wildcard, but many arms return Unmodeled deliberately — exhaustive over variants
is not costed for every variant.
Threading it through function_wcet alone left op null in every REAL sidecar,
because the CLI goes through the composer; the unit path passed regardless. The
end-to-end run caught it, so the regression test is end-to-end and red-first
verified: reverting the composer patch reproduces gale's exact JSON and fails.
Measured, not assumed: i64.load reproduces (I64Ldr); i64.add / i64.ge_s /
i64.extend_i32_u come out BOUNDED because the selector expands them first.
clippy 0, 133 test suites green.
Refs #921, #778
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
The clippy and test-helper fixes were applied with a script AFTER the last `cargo fmt` run, so the formatter never saw them. Format caught it.
# Conflicts: # CHANGELOG.md
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.
Closes #921. Additive to
synth-wcet-v1;.textunchanged.{"status":"declined","name":"f","reason":"unmodeled-op", "note":"op not classified by the cycle model","op":"I64Ldr","offset":8}Both fields are optional and absent for every other reason, so existing consumers are unaffected.
Two design choices worth flagging
opis derived fromDebug, not a hand-written table. This repo keeps paying for hand-maintained mirrors that drift from what they mirror (thumb-2: i32.shl/shr_s/shr_u don't mask the shift amount mod 32 — amounts >=32 silently compile to 0 (VCR-SEL regression; Rocq ARM model masks like WASM so proof is vacuous) #682, Shelfware oracles: 57/130 differentials are unreferenced, and nothing distinguishes 'manual by design' from 'forgotten' #890). A newArmOpvariant is named correctly here for free, with no second source of truth.offsetcomes from the REAL encoder — the same source of truthWcetLoopBound::head_offsetuses, so a decline site and a loop head cross-reference in one disassembly. It is omitted, never estimated, when a preceding op is one the encoder refuses:estimate_arm_byte_sizeis not exact for every op, and a drifted offset sends the reader to the wrong instruction — worse than sending them nowhere.The doc comment was false
WcetDecline::UnmodeledOpclaimed it was "never emitted in a released build (the classifier is exhaustive with no wildcard)".op_costdoes have no wildcard arm — exhaustive in the compiler's sense — but many arms returnUnmodeleddeliberately: the i64 pseudo-ops and the whole MVE/Helium f32 family. Exhaustive over variants is not costed for every variant, and #921 is that difference showing up on the first real object. Corrected.Measured, not assumed
I nearly shipped "it'll be the i64 family, timestamps are 64-bit" as fact. Testing it:
i64.loadI64Ldri64.addi64.ge_si64.extend_i32_uThe selector expands most i64 ops before the WCET pass sees them. Which op @avrabe's object actually trips is what the new field answers — on their object, not by inference from mine.
What caught the bug in the fix
Threading the site through
function_wcetalone leftopnull in every real sidecar, because the CLI goes through the composer (wcet_compose). Unit tests on the patched path passed throughout. The end-to-end run found it, so the regression test is end-to-end too and red-first verified — reverting the composer patch reproduces the exact JSON from the issue and fails the test.The test also refuses to pass over an empty set: if
I64Ldrever becomes costed, it fails loudly rather than silently asserting nothing.clippy clean, 133 test suites green.