Coverage adequacy (6/6) - #9
Merged
Merged
Conversation
This was referenced Oct 1, 2026
tobiaskaestner
added this pull request to stack #10
October 1, 2026 18:47
tobiaskaestner
force-pushed
the
tkaestner/6-coverage-adequacy
branch
3 times, most recently
from
October 2, 2026 15:07
a1b1c2f to
85a3119
Compare
A verifies link and a satisfies link are claims. A per-test coverage run (west twister --coverage-per-test) checks them against execution: do the own verifying tests of a requirement run the code that satisfies it? The new module adequacy.py has no Sphinx dependency. It ports Source, resolve_impl_symbols and the verdicts from traceability_app.py by Anas (zephyr collab-safety 0cc56a35003), close to the original: - The bodies of a symbol are z_impl_<sym>, z_vrfy_<sym>, a plain definition, or a header static inline, in kernel/, kernel.h, kernel/**/*.h and sys/**/*.h. A macro has no body. - The sources come from git show <sha>:<path> at the run commit. The sha comes from zephyr.sha beside the run, else from environment.zephyr_version. Without it, the working tree is read, and the directive warns. - The verdicts are true, partial, broken, unattributed, unresolved, no-impl and no-cov. The evidence is passing, failing, skipped, no-run or untested. The keys are the keys of zdocs. A requirement gets its cases through verifies and its symbols through satisfies (IMPL-<symbol>). Each twister case goes to its spec case by (suite, function). Its matrix key is built from (scenario, C function name). The module does not parse keys, because scenario names are prefixes of other scenario names. Two changes correct errors of the original: the file patterns use glob rules in both modes (fnmatch missed sys/slist.h), and zephyr.sha comes first. The new directive testcoverage (test_coverage.py, loaded by test_module) emits one adequacy need per requirement that the run can assess. The id is ADQ-<run>/<req> (testcoverage_id_prefix), and the link assesses goes to the requirement. The run name is the first tag on the run commit, else the name of the run directory, or :run:. The fields verdict, evidence, coverage_run, judged_symbols and symbol_hits are roles (testcoverage_need_fields). The directive sets a field only if the consumer declares it. :layout: sets the need layout. The page gets a run summary, a table of the verdicts and one section per verdict. Each need lists its bodies, the lines that each own test ran, and the other tests that ran the body. The run directory comes from ZDOCS_COVERAGE_OUT (coverage_output_dir), wired like ZDOCS_TWISTER_OUT. twister_reader gains split_case_name, taken out of parse_twister_results. On the safety docset (twister-out-cov-subset, mps2/an385, 9 scenarios): 49 requirements, 32 true, 16 unresolved (all macros), 1 no-impl. ZEP-SRS-5-5 reads true. Tests (Phase 4 order 002, part 1): a git tree built in tmp_path with one fixture for each verdict and each body form (z_impl, z_vrfy only reached, plain, header static inline, macro). A working tree that moved 20 lines after the commit is the control: the verdict follows the commit. Other tests cover the prefix trap of the scenario names, parameter values that share one key, the fallbacks for the commit and the run name, and a Sphinx build that checks needs.json and no warning. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Tobias Kaestner <tobias.kaestner@inovex.de>
resolve_impl_symbols() searched a fixed file set, IMPL_PATTERNS: the set of the original resolver (kernel/*.c, kernel/**/*.c, include/zephyr/kernel.h, include/zephyr/kernel/**/*.h, include/zephyr/sys/**/*.h). A symbol with its body in another file got the verdict unresolved. On the safety docset, 17 of 384 requirements are unresolved for this reason only, for example should_preempt() in kernel/include/kthread.h and k_is_user_context() in include/zephyr/syscall.h. The new setting testcoverage_impl_files holds the glob patterns. The default is IMPL_PATTERNS, so the verdicts do not change without it. The directive gives the set to load_coverage_run() and assess(), and the summary of the run lists it. Two changes follow from a wider set: * A header is any .h file, not only a file under include/. So in kernel/include/*.h only a static inline definition is a body, as in include/. * The matrix keeps the lines of every file in the set. keep_prefixes() adds the fixed start of each pattern to _KEEP (arch/**/*.c adds arch/). Without it, a body in arch/ is never covered. Unit tests: the default set, a wider set (kernel/include/*.h, lib/*.c), a narrower set, keep_prefixes(), the matrix with a wider set, and the directive with the setting in conf.py. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Tobias Kaestner <tobias.kaestner@inovex.de>
tobiaskaestner
force-pushed
the
tkaestner/6-coverage-adequacy
branch
from
October 2, 2026 15:10
85a3119 to
901cd62
Compare
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.
Part 6 of 6 of a stacked series. It is based on #8 (
tkaestner/5-incremental-rebuilds); review the commits below only.testcoverage: per requirement, do its own verifying tests run the codethat satisfies it? It reads a per-test coverage run (
west twister --coverage-per-test, keyZDOCS_COVERAGE_OUT) and the sources at the runcommit. It emits one
adequacyneed per requirement(
ADQ-<run>/<req>, linkassesses). The verdicts aretrue,partial,broken,unattributed,unresolved,no-implandno-cov. The methodis a port of Anas Nashif's
traceability_app.py(zephyr collab-safety).testcoverage_impl_files: the consumer sets the files that hold the bodies.The default is the set of the original.
Commits
Testing
python3 -m pytest sphinx/_extensions/_tests -q) at the head of this PR: 399 passed.The stack
🤖 Generated with Claude Code