Hi!
I am new to this list so please forgive me if this question has been asked before.
The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words.
An example of that would be file
kernel/libsel4/mode_include/64/sel4/shared_types.bf
which can be obtained (as part of an entire source tree, of course) via repo init -u https://github.com/seL4/sel4test-manifest.git followed by repo sync.
What I find curious is that these files do not adhere to (common) C syntax yet they are fed into GCC and GCC swallows them.
This file format appears to be an extension to GCC. I could not find any documentation on any such extension. I would be grateful if anyone could point me to some kind of documentation pertaining to it.
Regards Mike
Hi, Mike!
At 2019-05-13T14:21:41+0200, Mike Epoch wrote:
I am new to this list so please forgive me if this question has been asked before.
No worries; it's a low-traffic list.
The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words.
Yes. They're called "bitfields", and you can read more about them here:
https://ts.data61.csiro.au/publications/nictaabstracts/Cock_08.abstract.pml
Regards, Branden
Thanks a lot for answering.
I have to ask a follow-up question. How does the bitfields tool chime in with the rest of the build process?
Here is a build step that I have logged:
Den mån 13 maj 2019 kl 15:34 skrev G. Branden Robinson < g.branden.robinson@gmail.com>:
Hi, Mike!
At 2019-05-13T14:21:41+0200, Mike Epoch wrote:
I am new to this list so please forgive me if this question has been asked before.
No worries; it's a low-traffic list.
The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words.
Yes. They're called "bitfields", and you can read more about them here:
https://ts.data61.csiro.au/publications/nictaabstracts/Cock_08.abstract.pml
Regards, Branden
Thanks a lot for answering.
I have to ask a follow-up question. How does the bitfields tool chime in with the rest of the build process?
As an example of why I am asking, here is a build step that I have logged:
gcc --sysroot=/home/mb/seL4/build -I../kernel/include -I../kernel/include/64 -I../kernel/include/arch/riscv -I../kernel/include/arch/riscv/arch/64 -I../kernel/include/plat/spike -I../kernel/include/plat/spike/plat/64 -I../kernel/libsel4/include -I../kernel/libsel4/arch_include/riscv -I../kernel/libsel4/sel4_arch_include/riscv64 -I../kernel/libsel4/sel4_plat_include/spike -I../kernel/libsel4/mode_include/64 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel/kernel_bf_gen_target_1_pbf_temp.c
This command line invokes gcc and at its end there is "-c kernel/kernel_bf_gen_target_1_pbf_temp.c", where the ".c"-file is a bitfields file. GCC should complain about the file format yet it does not. How is this achieved? I guess there must be something that presents the bitfields file in C syntax to GCC. How is this achieved?
Regards Mike
Den mån 13 maj 2019 kl 16:42 skrev Mike Epoch <crypticusername1234@gmail.com
:
Thanks a lot for answering.
I have to ask a follow-up question. How does the bitfields tool chime in with the rest of the build process?
Here is a build step that I have logged:
Den mån 13 maj 2019 kl 15:34 skrev G. Branden Robinson < g.branden.robinson@gmail.com>:
Hi, Mike!
At 2019-05-13T14:21:41+0200, Mike Epoch wrote:
I am new to this list so please forgive me if this question has been asked before.
No worries; it's a low-traffic list.
The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words.
Yes. They're called "bitfields", and you can read more about them here:
https://ts.data61.csiro.au/publications/nictaabstracts/Cock_08.abstract.pml
Regards, Branden
Alrighty, I believe I get it now. GCC preprocessing is used to generate bitfield files. Then there is a Python utility that translates them to C code at appropriate points during the build process.
Den mån 13 maj 2019 kl 16:51 skrev Mike Epoch <crypticusername1234@gmail.com
:
Thanks a lot for answering.
I have to ask a follow-up question. How does the bitfields tool chime in with the rest of the build process?
As an example of why I am asking, here is a build step that I have logged:
gcc --sysroot=/home/mb/seL4/build -I../kernel/include -I../kernel/include/64 -I../kernel/include/arch/riscv -I../kernel/include/arch/riscv/arch/64 -I../kernel/include/plat/spike -I../kernel/include/plat/spike/plat/64 -I../kernel/libsel4/include -I../kernel/libsel4/arch_include/riscv -I../kernel/libsel4/sel4_arch_include/riscv64 -I../kernel/libsel4/sel4_plat_include/spike -I../kernel/libsel4/mode_include/64 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel/kernel_bf_gen_target_1_pbf_temp.c
This command line invokes gcc and at its end there is "-c kernel/kernel_bf_gen_target_1_pbf_temp.c", where the ".c"-file is a bitfields file. GCC should complain about the file format yet it does not. How is this achieved? I guess there must be something that presents the bitfields file in C syntax to GCC. How is this achieved?
Regards Mike
Den mån 13 maj 2019 kl 16:42 skrev Mike Epoch < crypticusername1234@gmail.com>:
Thanks a lot for answering.
I have to ask a follow-up question. How does the bitfields tool chime in with the rest of the build process?
Here is a build step that I have logged:
Den mån 13 maj 2019 kl 15:34 skrev G. Branden Robinson < g.branden.robinson@gmail.com>:
Hi, Mike!
At 2019-05-13T14:21:41+0200, Mike Epoch wrote:
I am new to this list so please forgive me if this question has been asked before.
No worries; it's a low-traffic list.
The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words.
Yes. They're called "bitfields", and you can read more about them here:
https://ts.data61.csiro.au/publications/nictaabstracts/Cock_08.abstract.pml
Regards, Branden
Yes, that’s right. The first step is something I’d like to remove again, extending the bitfield language instead, but that is something for the future.
Cheers, Gerwin
On 14 May 2019, at 17:49, Mike Epoch <crypticusername1234@gmail.commailto:crypticusername1234@gmail.com> wrote:
Alrighty, I believe I get it now. GCC preprocessing is used to generate bitfield files. Then there is a Python utility that translates them to C code at appropriate points during the build process.
Den mån 13 maj 2019 kl 16:51 skrev Mike Epoch <crypticusername1234@gmail.commailto:crypticusername1234@gmail.com>: Thanks a lot for answering.
I have to ask a follow-up question. How does the bitfields tool chime in with the rest of the build process?
As an example of why I am asking, here is a build step that I have logged:
gcc --sysroot=/home/mb/seL4/build -I../kernel/include -I../kernel/include/64 -I../kernel/include/arch/riscv -I../kernel/include/arch/riscv/arch/64 -I../kernel/include/plat/spike -I../kernel/include/plat/spike/plat/64 -I../kernel/libsel4/include -I../kernel/libsel4/arch_include/riscv -I../kernel/libsel4/sel4_arch_include/riscv64 -I../kernel/libsel4/sel4_plat_include/spike -I../kernel/libsel4/mode_include/64 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel/kernel_bf_gen_target_1_pbf_temp.c
This command line invokes gcc and at its end there is "-c kernel/kernel_bf_gen_target_1_pbf_temp.c", where the ".c"-file is a bitfields file. GCC should complain about the file format yet it does not. How is this achieved? I guess there must be something that presents the bitfields file in C syntax to GCC. How is this achieved?
Regards Mike
Den mån 13 maj 2019 kl 16:42 skrev Mike Epoch <crypticusername1234@gmail.commailto:crypticusername1234@gmail.com>: Thanks a lot for answering.
I have to ask a follow-up question. How does the bitfields tool chime in with the rest of the build process?
Here is a build step that I have logged:
Den mån 13 maj 2019 kl 15:34 skrev G. Branden Robinson <g.branden.robinson@gmail.commailto:g.branden.robinson@gmail.com>: Hi, Mike!
At 2019-05-13T14:21:41+0200, Mike Epoch wrote:
I am new to this list so please forgive me if this question has been asked before.
No worries; it's a low-traffic list.
The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words.
Yes. They're called "bitfields", and you can read more about them here:
https://ts.data61.csiro.au/publications/nictaabstracts/Cock_08.abstract.pml
Regards, Branden _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
G. Branden Robinson -
Klein, Gerwin (Data61, Kensington NSW) -
Mike Epoch