Devel August 2018

devel@sel4.systems

29 participants
33 discussions

Re: [seL4] Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 13 Aug '18

13 Aug '18

Hi, I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf loader. The function stuck is memcpy. I have added prints and I am not progressing after the last memcpy call in unpack_elf_to_paddr(). All kinds of input appreciated. Function under review: *static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)* /* Parse size/length headers. */ dest_vaddr = elf_getProgramHeaderVaddr(elf, i); data_size = elf_getProgramHeaderFileSize(elf, i); data_offset = elf_getProgramHeaderOffset(elf, i); /* Load data into memory. */ * memcpy((char *)dest_vaddr + phys_virt_offset,* * (char *)elf + data_offset, data_size);* * printf("loaded data into memory \n"); -----> Stuck Here !* } } *Can anyone give me a clue on whatsoever to check here ? **It worked perfectly in spike simulation.* *RISCV FPGA configuration* - It supports IMAFD. It has already booted linux. Kernel is loaded at physical address 80 million. *Snap shot* ELF-loader started on paddr=[80200000..8060dc17] elfFile->e_phnum = 1 elfFile->e_phnum = 1 elfFile->e_phnum = 1 elfFile->e_phnum = 1 ELF-loading image 'kernel' paddr=[c0000000..c002dfff] vaddr=[ffffffff80000000..ffffffff8002dfff] virt_entry=ffffffff80000000 elf file is valid image is aligned phy range valiidngetting size of image elfFile->e_phnum = 1 elfFile->e_phnum = 1 memset each segment in the elf file loading each segment in the elf file 2d018 elfFile->e_phnum = 1 loading data into memory char *)dest_vaddr + phys_virt_offset = ffffffffc0000000 (char *)elf + data_offset, = ffffffff8020a694 ----- ? -- regards, Sathya

2 2

Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 13 Aug '18

13 Aug '18

2 1

Paging in SEL4
by Sathya Narayanan N 10 Aug '18

10 Aug '18

Hi Experts, Could some one help me in understanding the paging in SEL4 ? the MMU architecture ? Is there any material to understand ? -- regards, Sathya

4 4

compile error aarch64 platform hikey
by Thad Seeberger 10 Aug '18

10 Aug '18

I really want to target zcu102 but i../init-build.sh -DPLATFORM=zynqmp unsupported platform so I decided to target another A53 target I dont know if this is the proper way to get started on this. ../init-build.sh -DPLATFORM=hikey -DAARCH64=1 ninja [maddthad@localhost build-zcu102]$ ccache /usr/lib64/ccache/aarch64-linux-gnu-gcc --sysroot=/home/maddthad/sel4/sel4test/build-zcu102 -DHAVE_AUTOCONF -I../tools/seL4/elfloader-tool/include -I../tools/seL4/elfloader-tool/include/plat/hikey -I../tools/seL4/elfloader-tool/include/arch-arm -I../tools/seL4/elfloader-tool/include/arch-arm/64 -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv8-a -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv8-a/64 -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/sel4test/apps/sel4test-driver/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -I../projects/util_libs/libcpio/include -march=armv8-a+crc -D__KERNEL_64__ -D_XOPEN_SOURCE=700 -ffreestanding -Wall -Werror -W -Wextra -mgeneral-regs-only -fpic -fno-pie -MD -MT elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -MF elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj.d -o elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -c ../tools/seL4/elfloader-tool/src/string.c ../tools/seL4/elfloader-tool/src/string.c:97:29: error: expected ‘;’, ‘,’ or ‘)’ before ‘dest’ void *memcpy(void *restrict dest, const void *restrict src, size_t n) gcc ver: COLLECT_GCC=/usr/bin/aarch64-linux-gnu-gcc COLLECT_LTO_WRAPPER=/usr/libexec/gcc/aarch64-linux-gnu/4.8.5/lto-wrapper Target: aarch64-linux-gnu gcc version 4.8.5 20150623 (Red Hat 4.8.5-16) (GCC) thx Thad

3 3

Re: [seL4] Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 09 Aug '18

09 Aug '18

> > Hi, > > I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf > loader. > > The function stuck is memcpy. I have added prints and I am not progressing > after the last memcpy call in unpack_elf_to_paddr(). All kinds of input > appreciated. > > > Function under review: > *static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)* > > /* Parse size/length headers. */ > dest_vaddr = elf_getProgramHeaderVaddr(elf, i); > data_size = elf_getProgramHeaderFileSize(elf, i); > data_offset = elf_getProgramHeaderOffset(elf, i); > > /* Load data into memory. */ > > * memcpy((char *)dest_vaddr + phys_virt_offset,* > * (char *)elf + data_offset, data_size);* > * printf("loaded data into memory \n"); -----> Stuck Here > !* > } > > } > > *Can anyone give me a clue on whatsoever to check here ? **It worked > perfectly in spike simulation.* > > *RISCV FPGA configuration* - It supports IMAFD. It has already booted > linux. Kernel is loaded at physical address 80 million. > -- regards, Sathya

1 0

sel4 thread creation problem
by Leonid Meyerovich 08 Aug '18

08 Aug '18

Hello, My platform is ARM (zynqmp), seL4 v8. I have created a timer in simple initial thread: int err; seL4_timer_t timer; vka_object_t ntfn_object; ntfn_object.cptr = 0; err = vka_alloc_notification(&_env.vka, &ntfn_object); assert(err == 0); err = sel4platsupport_init_default_timer(&_env.vka, &_env.vspace, &_env.simple, ntfn_object.cptr, &timer); err = ltimer_set_timeout(&timer.ltimer, NS_IN_MS * 20, TIMEOUT_PERIODIC); assert(err == 0); int count = 0; int count_s = 0; while (1) { /* Handle the timer interrupt */ seL4_Word badge; seL4_Wait(ntfn_object.cptr, &badge); printf("time_thread: badge=%lx\n", badge); sel4platsupport_handle_timer_irq(&timer, badge); count++; if ((count / 50) * 50 == count) { count_s++; printf("-----------------timer=%d %d\n", count, count_s); } } It works fine (I am not sure why TIMESTAMP timer interrupt coming every ~40 sec, but it's not an issue right now) Now I am trying to move all this timer code into a new thread, which I have created in the same vspace // create thread void initSleep(env_t penv) //seL4_BootInfo *info) { _penv = penv; vka_object_t tcb_object = {0}; int error = vka_alloc_tcb(&penv->vka, &tcb_object); seL4_CPtr cspace_cap; cspace_cap = simple_get_cnode(&penv->simple); seL4_CPtr pd_cap; pd_cap = simple_get_pd(&penv->simple); seL4_CPtr ipc_page; seL4_Word ipc_buffer = (seL4_Word)vspace_new_ipc_buffer(&penv->vspace, &ipc_page); error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page); error = seL4_TCB_SetPriority(tcb_object.cptr, simple_get_tcb(&penv->simple), seL4_MaxPrio); seL4_UserContext regs = { .pc = (seL4_Word)time_thread, .sp = (seL4_Word)thread_time_stack }; error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs); error = seL4_TCB_Resume(tcb_object.cptr); } And this is thread function static void time_thread(void) { _tick_number = 0; int count_s = 0; init_timer(); while (1) { /* Handle the timer interrupt */ seL4_Word badge; seL4_Wait(timer_ntfn_object.cptr, &badge); printf("time_thread: badge=%lx\n", badge); sel4platsupport_handle_timer_irq(&timer, badge); _tick_number++; if ((_tick_number / 50) * 50 == _tick_number) { count_s++; printf("-----------------timer=%lu %d\n", _tick_number, count_s); } } The system crashed: setup_irq@timer.c:81 Setting up IRQ 8000000000000000 <<seL4(CPU 0) [handleInvocation/281 T0xff8000001200 "child of: 'rootserver'" @42195c]: Invocation of invalid cap #48762580.>> Here is dump: /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/functions.h:23 421938: d53bd066 mrs x6, tpidrro_el0 setup_irq(): /home/lm/sel4vm/libs/libsel4platsupport/src/timer.c:85 error = seL4_IRQHandler_SetNotification(irq->handler_path.capPtr, irq->badged_ntfn_path.capPtr); 42193c: f85c8340 ldur x0, [x26,#-56] arm_sys_send_recv(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:165 register seL4_Word msg1 asm("x3") = *in_out_mr1; 421940: d2800003 mov x3, #0x0 // #0 seL4_SetCap(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/arch/functions.h:59 421944: f901e8c1 str x1, [x6,#976] arm_sys_send_recv(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:166 register seL4_Word msg2 asm("x4") = *in_out_mr2; 421948: d2800004 mov x4, #0x0 // #0 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:167 register seL4_Word msg3 asm("x5") = *in_out_mr3; 42194c: d2800005 mov x5, #0x0 // #0 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:170 register seL4_Word scno asm("x7") = sys; 421950: 92800007 mov x7, #0xffffffffffffffff // #-1 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:161 register seL4_Word info asm("x1") = info_arg; 421954: d2941001 mov x1, #0xa080 // #41088 421958: f2a00021 movk x1, #0x1, lsl #16 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:171 asm volatile ( 42195c: d4000002 hvc #0x0 seL4_MessageInfo_get_label(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/shared_types_gen.h:49 I suspect that my thread initialization is not right, can somebody see any problem? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 3

Re: [seL4] camkes-project error
by talos 08 Aug '18

08 Aug '18

Hi I changed it to: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-none-eabi- -DCAMKES_APP=adder -DSIMULATE=1 -Dc_std=gnu99 and it worked for ninja build. But when started simulation by ./simulate the error is: qemu-system-arm: -kernel images/capdl-loader-image-arm-imx6: unsupported machine type Use -machine help to list supported machines How could I choose the machine type? Thanks! Sincerely

3 2

Combined Ada and C project with Kbuild
by Noah Kennedy 08 Aug '18

08 Aug '18

I'm currently working on a project that is using the old Kbuild system. The project has been primarily implemented in C, however we would like to integrate some Ada code into the project. I am familiar with how to use gcc and makefiles to build polyglot projects on linux, however, I have no idea how to do so with the Kbuild system, as I cannot find out how to build anything other than .c or .h files with the makefile. How would I go about adding ada code to the project? Is there any way for me to build .ads and .adb, or .a files with the makefile?

2 1

camkes-project error
by talos 07 Aug '18

07 Aug '18

Hi, When I followed this tutorial: https://sel4.systems/Info/CAmkES/GettingStarted.pml The error is: /home/talos/camkes-project/build/arm/imx31/simple/src/echo/generated/camkes.o: In function `post_main': /home/talos/camkes-project/build/arm/imx31/simple/src/echo/generated/camkes.c:601: undefined reference to `component_control_main' collect2: error: ld returned 1 exit status /home/talos/camkes-project/build/arm/imx31/simple/camkes-gen.mk:630: recipe for target 'echo.instance.bin' failed make[1]: *** [echo.instance.bin] Error 1 tools/common/project.mk:333: recipe for target 'simple' failed make: *** [simple] Error 2 But when I followed this tutorial: https://docs.sel4.systems/CAmkES/ the error is: [230/232] Building C object elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj FAILED: /usr/bin/arm-none-eabi-gcc --sysroot=/home/talos/camkes-project/build -DHAVE_AUTOCONF -I../tools/seL4/elfloader-tool/include -I../tools/seL4/elfloader-tool/include/plat/imx6 -I../tools/seL4/elfloader-tool/include/arch-arm -I../tools/seL4/elfloader-tool/include/arch-arm/32 -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv7-a -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv7-a/32 -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -I../projects/util_libs/libcpio/include -march=armv7-a -marm -D__KERNEL_32__ -g -D_XOPEN_SOURCE=700 -ffreestanding -Wall -Werror -W -Wextra -fno-pic -fno-pie -MD -MT elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -MF elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj.d -o elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -c ../tools/seL4/elfloader-tool/src/string.c ../tools/seL4/elfloader-tool/src/string.c:97:29: error: expected ';', ',' or ')' before 'dest' void *memcpy(void *restrict dest, const void *restrict src, size_t n) ^ ninja: build stopped: subcommand failed. I used Ubuntu 16.04 x86_64 Thanks

3 2

How to write safe C code for free?
by Wean Irdeh 05 Aug '18

05 Aug '18

Hello. I'm a poor person looking for an advice. I know this is the right place since all of you have huge expertise in formal verification. I'm not a smart person (maybe I'm stupid), but I'm interested in open source contribution using C language. Is there any solution to write C code free from undefined behavior and vulnerability without paying for any tools?

3 2

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel August 2018