Extract kernel object sizes from headers#456
Merged
Ivan-Velickovic merged 2 commits intomainfrom Mar 30, 2026
Merged
Conversation
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Ivan-Velickovic
force-pushed
the
object_sizes_from_kernel
branch
2 times, most recently
from
6aa3fc8 to
7ee449d
Compare
Many of these constants are architecture-dependent, but also slightly differ depending on how the kernel is configured. Rather than reproducing all the special combinations of kernel configurations that affect object size in the tool itself, just read from the source of truth. This should prevent bugs such as 7323d07. Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Ivan-Velickovic
force-pushed
the
object_sizes_from_kernel
branch
from
7ee449d to
113fc40
Compare
|
These sizes are exported as defines in libsel4/sel4_arch_include/*/sel4/sel4_arch/constants.h, but not in a usable format. Feel free to open a PR in seL4 to export this information properly instead of adding hacks like this. |
midnightveil
approved these changes
Mar 30, 2026
Contributor
midnightveil
left a comment
midnightveil
left a comment
There was a problem hiding this comment.
I hate having to do this but it seems fine.
Member
|
When/if someone is working on exporting these nicely from the seL4 build, please let me know. These would be nice to import into the verification as well. |
Collaborator
Author
|
@Indanz I agree that is a hack. @lsf37, I've opened seL4/seL4#1632. I can give it a go once I get feedback from people on how it should work. |
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
4 participants
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.
See commit messages for details.
Addresses #378, but ideally this would be an output of the kernel build itself since it is useful outside of Microkit.