mirror of https://github.com/seL4/docs.git
292 lines
9.7 KiB
Markdown
292 lines
9.7 KiB
Markdown
---
|
|
redirect_from:
|
|
- /DebuggingGuide
|
|
SPDX-License-Identifier: CC-BY-SA-4.0
|
|
SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
|
|
---
|
|
|
|
# Debugging guide
|
|
|
|
This guide is for debugging the seL4 kernel itself, for instance during
|
|
development of new features. See [Debugging user
|
|
space](debugging-userspace.html) for how to debug user-level code on top of
|
|
seL4.
|
|
|
|
## Compiler Settings
|
|
|
|
Ensure that the build directory you are building in is not a release build. To
|
|
do so, check you build directory `CMakeCache.txt` file for the following lines:
|
|
|
|
- `CMAKE_BUILD_TYPE:STRING=Debug`
|
|
- `KernelDebugBuild:BOOL=ON`
|
|
|
|
Debug builds enable helpful features for debugging including:
|
|
|
|
- `printf` + a serial driver,
|
|
- `-g` is passed to the compiler,
|
|
- compile- and run-time asserts,
|
|
- the kernel will print out error messages when invocations fail.
|
|
|
|
## QEMU
|
|
|
|
[QEMU](http://www.qemu.org/) is a simulator that provides software emulation of
|
|
a hardware platform. It is useful for developing and debugging embedded software
|
|
when you do not have access to the target platform. Even if you do have the
|
|
target hardware, QEMU can shorten your edit-compile-debug cycle. Be aware that
|
|
it is not cycle-accurate and cannot emulate every device, so sometimes you have
|
|
no alternative than to debug on real hardware.
|
|
|
|
For the seL4 tutorials, a `simulate` script is always generated for use in the
|
|
build directory of a project. In most other projects, this script can be
|
|
generated by passing the flag `-DSIMULATION=1` to the `../init-build.sh`
|
|
invocation.
|
|
|
|
```bash
|
|
mkdir build_dir
|
|
cd build_dir
|
|
../init-build.sh -DSIMULATION=1
|
|
./simulate
|
|
```
|
|
|
|
If the platform does not support QEMU, the script will output
|
|
|
|
```bash
|
|
Unsupported platform or architecture for simulation
|
|
```
|
|
|
|
When simulating an seL4 system in QEMU, you should see output that is
|
|
directed to the (emulated) UART device on your terminal:
|
|
|
|
```log
|
|
ELF-loader started on CPU: ARM Ltd. ARMv6 Part: 0xb36 r1p3
|
|
paddr=[82000000..8225001f]
|
|
ELF-loading image 'kernel'
|
|
paddr=[80000000..80033fff]
|
|
vaddr=[f0000000..f0033fff]
|
|
virt_entry=f0000000
|
|
ELF-loading image 'sel4test-driver'
|
|
paddr=[80034000..8036efff]
|
|
vaddr=[10000..34afff]
|
|
virt_entry=1c880
|
|
Enabling MMU and paging
|
|
Jumping to kernel-image entry point...
|
|
|
|
Bootstrapping kernel
|
|
Switching to a safer, bigger stack...
|
|
seL4 Test
|
|
=========
|
|
...
|
|
```
|
|
|
|
To exit from QEMU, type the sequence Ctrl+"a", then "x". Note that you
|
|
can exit at any point; you do not need to wait for the system to finish
|
|
or reach some stable state. If you exit QEMU while a system is running,
|
|
it will simply be terminated.
|
|
|
|
QEMU has some powerful debugging features built in. You can type
|
|
Ctrl+"a", then "c" to switch to the QEMU monitor. From here you can
|
|
inspect CPU or device state, read and write memory, and single-step
|
|
execution. More information about this functionality is available in the
|
|
[QEMU documentation](https://qemu-project.gitlab.io/qemu/system/monitor.html).
|
|
|
|
When debugging an seL4 project, the QEMU debugger is inherently limited.
|
|
It has no understanding of your source code, so it is difficult to
|
|
relate what you are seeing back to the C code you compiled. It is
|
|
possible to get a richer debugging environment by connecting GDB to
|
|
QEMU.
|
|
|
|
### Using GDB with QEMU
|
|
|
|
[GDB](https://www.gnu.org/s/gdb/) is a debugger commonly used
|
|
in C application development. Though not as seamless as debugging a
|
|
native Linux application, it is possible to use GDB to debug within
|
|
QEMU's emulated environment.
|
|
|
|
Start QEMU with the extra options "-S" (pause execution on start) and
|
|
"-s" (start a GDB server on TCP port 1234):
|
|
|
|
```bash
|
|
./simulate --extra-qemu-args="-S -s"
|
|
```
|
|
|
|
In a separate terminal window, start your target platform's version of
|
|
GDB. You should either pass a binary of the seL4 kernel if you intend on
|
|
debugging seL4 itself or the user-space application if you intend on
|
|
debugging an application on seL4.
|
|
|
|
In this example we're going
|
|
to debug the seL4 kernel that has been built in debug mode:
|
|
|
|
```bash
|
|
${CROSS_COMPILER_PREFIX}gdb kernel/kernel.elf
|
|
```
|
|
|
|
Where `CROSS_COMPILER_PREFIX` is the prefix used for the toolchain for the
|
|
architecture you are debugging. For x86 this is blank, for other architectures
|
|
you can check the `CMakeCache.txt` file in the build directory for the variable
|
|
`CROSS_COMPILER_PREFIX`. In the following example, the prefix is
|
|
`arm-none-eabi-`:
|
|
|
|
```bash
|
|
CROSS_COMPILER_PREFIX:UNINITIALIZED=arm-none-eabi-
|
|
```
|
|
|
|
At the GDB prompt, enter "target remote :1234" to connect to the server
|
|
QEMU is hosting:
|
|
|
|
```gdb
|
|
Reading symbols from kernel/kernel.elf...done.
|
|
(gdb) target remote :1234
|
|
Remote debugging using :1234
|
|
0x82000000 in ?? ()
|
|
(gdb)
|
|
```
|
|
|
|
Suppose we want to halt when `kprintf` is called. Enter `break kprintf` at
|
|
the GDB prompt:
|
|
|
|
```gdb
|
|
(gdb) break kprintf
|
|
Breakpoint 1 at 0xf0011248: file kernel/src/machine/io.c, line 269.
|
|
```
|
|
|
|
We can now start QEMU running and wait until we hit the breakpoint. To
|
|
do this, type "cont" at the GDB prompt:
|
|
|
|
```gdb
|
|
(gdb) cont
|
|
Continuing.
|
|
|
|
Breakpoint 1, kprintf (format=0xf0428000 "") at kernel/src/machine/io.c:269
|
|
269 {
|
|
```
|
|
|
|
Note that some output has appeared in the other terminal window running
|
|
QEMU as it has partially executed. It may be surprising to see that some
|
|
printing somehow happened without our breakpoint triggering. The reason
|
|
for this is that output we're seeing is from the ELF loader that runs
|
|
prior to the kernel. GDB does not know the address of its print function
|
|
(as we only gave GDB the kernel's symbol table) and it is not looking to
|
|
break on its address. The breakpoint we have just hit is the first time
|
|
the ''kernel'' tried to print. Similarly, the breakpoint we have
|
|
configured will have no effect on user-space calls to `printf`.
|
|
|
|
Now that we are stopped at a breakpoint, all the standard GDB operations
|
|
are possible (inspect registers or the stack, single-step, continue
|
|
until function exit, ...). More information is available in the
|
|
[GDB manual](http://www.gnu.org/software/gdb/documentation/).
|
|
|
|
Be warned that if you are debugging the kernel's early boot steps,
|
|
something that may not be immediately obvious is that debugging across a
|
|
context in which page mappings change (e.g. switching page directories
|
|
or turning the MMU on/off) will confuse GDB and you may find breakpoints
|
|
triggering unexpectedly or being missed.
|
|
|
|
The process we have described is similar for x86, though if you are on
|
|
an x86 or x86_64 host you can simply use your platform's native GDB,
|
|
gdb.
|
|
|
|
#### User space debugging
|
|
|
|
The steps for debugging a user-space application on seL4 are identical to
|
|
the ones we have just seen, except that we pass GDB a symbol table for
|
|
user-space rather than the kernel. For example, using the same `sel4test`
|
|
environment we start QEMU in the same way but start GDB with the `sel4test`
|
|
binary:
|
|
|
|
```bash
|
|
${CROSS_COMPILER_PREFIX}gdb projects/sel4test/apps/sel4test-driver/sel4test-driver
|
|
```
|
|
|
|
After connecting to QEMU, we can instruct GDB to break on the user space
|
|
`printf` function:
|
|
|
|
```gdb
|
|
Reading symbols from projects/sel4test/apps/sel4test-driver/sel4test-driver.bin...done.
|
|
(gdb) target remote :1234
|
|
Remote debugging using :1234 0x82000000 in ?? ()
|
|
(gdb) break printf
|
|
Breakpoint 1 at 0x30870: file libs/libmuslc/src/stdio/printf.c, line 9.
|
|
(gdb)
|
|
```
|
|
|
|
Note that GDB has correctly identified the printf function in Musl C. We
|
|
now continue as before:
|
|
|
|
```gdb
|
|
(gdb) cont
|
|
Continuing.
|
|
|
|
Breakpoint 1, printf (fmt=0x363e8 "%s") at libs/libmuslc/src/stdio/printf.c:9
|
|
9 ret = vfprintf(stdout, fmt, ap);
|
|
(gdb)
|
|
```
|
|
|
|
If you examine the terminal window running QEMU at this point, you will
|
|
note that we see an extra bit of output from the kernel. The kernel's
|
|
print functionality is unaffected, but GDB has stopped execution the
|
|
first time user space called `printf`.
|
|
|
|
From here, the experience is essentially identical to debugging the
|
|
kernel. One small complication to be aware of is that debugging across a
|
|
context switch may be confusing. If you are single-stepping in GDB and
|
|
find execution suddenly diverted to an address where code is unknown,
|
|
check the address itself. It is usually easy to identify from the
|
|
address alone when execution is in kernel code or the exception vector
|
|
table. Unfortunately there is no easy way to continue until you're back
|
|
in user space, particularly if the kernel schedules a different thread
|
|
than the one you were debugging. Depending on the scenario you are
|
|
debugging, it may be simpler to modify your system setup to ensure only
|
|
one thread is running.
|
|
|
|
## Objdump
|
|
|
|
The `objdump` tool can be used to disassemble an ELF file, be it a kernel or an
|
|
application. This can be used to lookup the instruction where a fault occurred.
|
|
Make sure `-g` is passed to the compiler so that debug information is included
|
|
in the image.
|
|
|
|
Like gdb, the appropriate `objdump` from the toolchain must be called by
|
|
using `CROSS_COMPILER_PREFIX`.
|
|
|
|
For ARM, supposing that **arm-none-eabi-** is used as the
|
|
cross-compiler prefix.
|
|
|
|
```bash
|
|
arm-none-eabi-objdump -D binary_file_name > dump.s
|
|
```
|
|
|
|
For x86, on an x86 host:
|
|
|
|
```bash
|
|
objdump -D binary_file_name > dump.s
|
|
```
|
|
|
|
The file `dump.s` has the human-readable assembly instructions.
|
|
|
|
If you have symbols and want (C) source information in your disassembly
|
|
(and who doesn't!) then use the -S flag. for example:
|
|
|
|
```bash
|
|
${CROSS_COMPILER_PREFIX}objdump -DS binary_file_name
|
|
```
|
|
|
|
## Hardware debugging
|
|
|
|
For some platforms, seL4 supports hardware debugging.
|
|
See [Hardware debugging of user-space threads](debugging-userspace.html).
|
|
|
|
## In kernel debugging
|
|
|
|
seL4 does not currently have a kernel debugger. As a result, most of our
|
|
debugging is done with:
|
|
|
|
- `objdump` as described above,
|
|
- `printf`,
|
|
- `__builtin_return_address` (to figure out stack traces).
|
|
|
|
In the kernel, we provide `debug_printKernelEntryReason` found in
|
|
[debug.h](https://github.com/seL4/seL4/blob/master/include/api/debug.h)
|
|
which can be used at any point in the kernel to output the current
|
|
operation that the kernel is doing.
|