seL4
tool: Not failing if symbols aren't present for patching
Currently, the MicroKit tool fails if symbols it plans to patch (e.g. microkit_name or those referred to by setvar_vaddr) aren't present. One example of a case where this is inconvenient is when a PD never actually uses microkit_name , and so the linker might exclude microkit_name from the final binary. This happens in Rust PDs for which the compiler can prove that they never panic.
In Rust, there is no way to instruct the linker to include certain unused symbols in the final binary without using unstable features.
I think the best solution is for the tool to permit such symbols to be absent in the binary.
setvar_vaddr is optional, so is the only problematic variable microkit_name?
Having an option such as --no-elf-patching to the tool may be possible, but I would only want to do this if this is a problem across multiple/all systems programming languages.
Changing Microkit to work around a limitation in Rust seems weird.
This Rust scenario is just the specific reason why I've found myself wishing the tool had this slightly more general behavior.
I see the change I'm proposing as a slight generalization of the current behavior. From:
Patch each variable
To:
Patch each variable that actually exists in the binary
Making the tool more permissive in this way would simplify PD constructions by reducing the assumptions made about their structure.
But it seems there is only one assumption we are talking about here, and that is the existence of microkit_name, right?
I would find the behaviour of the tool weird if you had in your system description setvar_vaddr and then it didn't actually do that because of some control flow that is hidden from the user.
The tool derives, from the system description, a set of variables that it would patch for each PD. The assumption that I'm talking about is the assumption that all of these variables are present in the corresponding PD binaries.
I would find the behaviour of the tool weird if you had in your system description setvar_vaddr and then it didn't actually do that because of some control flow that is hidden from the user.
A case where I think that behavior would be nice is during development, before a PD developer has built out the PD to the point where the relevant variable is actually used.
A case where I think that behavior would be nice is during development, before a PD developer has built out the PD to the point where the relevant variable is actually used.
Then during development just omit setvar_vaddr?
The behaviour of the variable patching is I think very clear right now. You ask the tool to patch a variable, and it does it. If it can't patch the variable you get a clear error message.
This approach would remove that clear behaviour, and I am not convinced right now that it is beneficial to do that just because a compiler invalidates the assumption. It seems that you are working around the behaviour of a compiler. I do not think it is unreasonable for a compiler for a systems programming language to explicitly leave in a symbol at the request of its user.
I will continue thinking about the issue, I haven't reached a conclusion.
A case where I think that behavior would be nice is during development, before a PD developer has built out the PD to the point where the relevant variable is actually used.
Sure, but I also run into lots of cases where I change the variable name or mess up the variable name in the system file and forget to make the corresponding change in the code. Right now it gives me a clear error message instead of having a VM fault sometime during runtime because the tool couldn't find the variable and ignored the setvar_vaddr.
I'm going to close this issue as not planned since I don't think the behaviour you're asking for is intuitive and I think the better approach would be to omit the setvar_vaddr where ELF patching isn't possible.
ELF patching isn't a 100% solution for information flow from the system design to the code and for larger systems more tooling to handle this is needed for things that build on top of Microkit like LionsOS. We're working on this but have nothing ready for use yet so all I can say is that this general problem is being worked on and not ignored.