capdl-loader-app: Refactor two-phase build design #56
Conversation
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
The capdl_spec.c file is generated by capDL-tool and is compiled into the capdl-loader-app program to define the system that the loader will load. The file is supposed to only be a C-language representation of the capDL spec for a particular system. Currently, the header files required to compile this spec file introduces dependencies on a C library, and libraries from seL4/util_libs and seL4/sel4_libs including libsel4utils and libutils (and any libraries they depend on). The spec itself doesn't inherently require any type definitions other than what's provided by libsel4, and so it shouldn't require these additional dependencies. Signed-off-by: Kent McLeod <[email protected]>
Instead of ZF_LOG* framework functions, we introduce our own layering of functions that directly output to seL4_DebugPutChar() when the debug syscall is present and outputs nothing when it isn't. This implementation allows using a minimal amount of the muslc stdio implementation for string formatting and bypasses the need for malloc or any syscalls to be supported. This will make it easier to refactor capdl-loader-app to be more freestanding (minimal runtime dependencies) in upcoming commits. Signed-off-by: Kent McLeod <[email protected]>
Refactor the remainder of the implementation of capdl-loader-app to
remove seL4_libs dependencies. This is achieved by mostly using similar
basic constructions inline rather than relying on them being provided by
the external libs:
- Create inline definitions of seL4_ARCH_{invocation} for the arch being
built,
- implement get_frame_object_type() which returns the correct object
type for page sizes of the current architecture,
- provide a few macro definitions for basic definitions
- remove platsupport_serial_setup code as seL4_DebugPutchar() will be
used for any console output for this app. (The loader doesn't safely
handle accessing physical serial device untyped without potentially
conflicting with resource requests of the system being loaded.
- remove malloc initialization as it is no longer required.
Signed-off-by: Kent McLeod <[email protected]>
The capdl-loader-app has previously used a non-conventional CMake pattern for building. As the app is built with the capDL spec and ELF files for any program data the loader is required to load, the actual CMake target definitions are deferred until the targets for generating the capDL spec are known as well as the ELF targets. These are then used to declare a capdl-loader-app target. Instead this change uses a different approach: - It compiles and links the program code leaving the symbols for the capDL spec and CPIO archive containing the ELF files unresolved, while still producing a base object file "capdl-loader.o". - Later on, a complete image can be created by taking the CapDL C spec and an object file containing a CPIO archive of ELF files and compiling these with the "capdl-loader.o" file. This compilation can be done outside of a CMake build as only access to libsel4 and capdl-loader-app header files are required to compile the CapDL C spec. - The helpers.cmake file that declares BuildCapDLApplication now builds the rootimage from within a custom command that performs the external call to a compiler with the required include paths and input files. - the sel4runtime dependency is removed as the loader app doesn't require thread-local storage and basic entry point assembly code is provided by "entry.h" which sets up a stack and then directly calls main() as the kernel places the bootinfo pointer in the first argument register and this is all the capdl-loader program needs to bootstrap. - As there is only one thread in the loader app, use global allocation instead of thread-local allocation for thread variables such as the pointer for the seL4 IPC buffer used by libsel4. Signed-off-by: Kent McLeod <[email protected]>
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.
The capdl-loader-app has previously used a non-conventional CMake
pattern for building. As the app is built with the capDL spec and ELF
files for any program data the loader is required to load, the actual
CMake target definitions are deferred until the targets for generating
the capDL spec are known as well as the ELF targets. These are then
used to declare a capdl-loader-app target.
Instead this change uses a different approach:
capDL spec and CPIO archive containing the ELF files unresolved, while
still producing a base object file "capdl-loader.o".
and an object file containing a CPIO archive of ELF files and
compiling these with the "capdl-loader.o" file. This compilation can
be done outside of a CMake build as only access to libsel4 and
capdl-loader-app header files are required to compile the CapDL C
spec.
the rootimage from within a custom command that performs the external
call to a compiler with the required include paths and input files.
require thread-local storage and basic entry point assembly code is
provided by "entry.h" which sets up a stack and then directly calls
main() as the kernel places the bootinfo pointer in the first argument
register and this is all the capdl-loader program needs to bootstrap.
instead of thread-local allocation for thread variables such as the
pointer for the seL4 IPC buffer used by libsel4.