# How to Use GDB with Renode to Debug seL4 Threads with Symbols

## High-Level Usage

The method for debugging seL4 threads with Renode is relatively simple, and
involves the usual suspects of `m debug-simulation` (or `m simulate-debug`) and `kgdb.sh`, but the
interface through GDB has changed slightly. In general, a debugging session now
looks like the following:

On one terminal, start an instance of Renode:
```bash
source build/setup.sh
m debug-simulation
```

[Note `m debug-simulation` gives GDB
control before anything runs while `m simulate-debug` lets Renode run
until `kgdb.sh` is invoked and contacts GDB. The former is necessary to
debug issues in the boot process (bootstrap, kernel, rootserver).]

Once Renode has started and starts outputting green debug logs, in another
terminal start up GDB with:
```bash
kgdb.sh
```

At this point, GDB should connect to the running Renode instance started by
`debug-simulation`, and you'll see something equivalent to the following (output
is not exact -- symbol reading may differ):

```
ghost:~/$ kgdb.sh
Source directories searched: /usr/local/google/home/sleffler/shodan/sw/tock:$cdir:$cwd
Reading symbols from out/shodan_boot_rom/multihart_boot_rom/multihart_boot_rom.elf...
add symbol table from file "out/shodan_boot_rom/multihart_boot_rom/multihart_boot_rom.elf"
Reading symbols from out/shodan_boot_rom/multihart_boot_rom/multihart_boot_rom.elf...
Remote debugging using localhost:3333
warning: multi-threaded target stopped without sending a thread-id, using first non-exited thread
_reset_start () at /usr/local/google/home/sleffler/shodan/sw/multihart_boot_rom/multihart_boot_rom/rom_crt.S:29
29        li  x7, 0x0
Symbol autoswitching is now disabled
(gdb)
```

At this point, GDB has stopped the simulator, giving you a chance to set
breakpoints and examine the system.

`kgdb.sh` will load symbols on the seL4 side, based on their
thread / CAmkES component, so there is no need to manually find the associated symbol file
and load it with the correct offsets. It may be necessary to switch symbol
tables, which can easily be done using `sel4 switch-symbols <component>`, which
will automatically load the symbols for CAmkES `<component>` with the appropriate offsets
(a `<component>` is the lower-case version of the CAmkES name, e.g. the CAmkES component
`DebugConsole` translates to `debug_console`.)

In this environment, there are two sets of breakpoints that can be used:
standard GDB `break`-style breakpoints, and renode-side `sel4 break`
breakpoints. The former work within the currently executing thread and can be
used for "local" breaks inside of a thread, whereas the latter can be set in any
thread that was previously discovered by the Renode extension.

Once a breakpoint is setup using `sel4 break` one can just
`continue`. For example, consider this debugging session:

```
<assuming cpu1 is halted and GDB is waiting at a prompt>

(gdb) sel4 wait-for-thread rootserver

Thread 2 "matcha.cpu1" received signal SIGTRAP, Trace/breakpoint trap.
[Switching to Thread 2]
0xff814802 in ?? ()
(gdb) # Switch to the 'rootserver' thread's symbol table and set a breakpoint on main
(gdb) sel4 switch-symbols rootserver
Reading symbols from out/kata/riscv32-unknown-elf/debug/capdl-loader...
(gdb) sel4 break rootserver main
(gdb) c
Continuing.

Thread 2 "matcha.cpu1" received signal SIGTRAP, Trace/breakpoint trap.
kata_os_rootserver::main () at src/main.rs:164
164     pub fn main() {
(gdb)
(gdb) # As we are in capdl-loader thread and proper symbols are loaded, all commands
(gdb) # like break work as expected.
(gdb) b init_system
Breakpoint 1 at 0x4c632: file /usr/local/google/home/sleffler/shodan/kata/projects/kata/apps/system/components/kata-os-common/src/model/mod.rs, line 200.
(gdb) c
Continuing.

Thread 2 "matcha.cpu1" hit Breakpoint 1, model::KataOsModel::init_system (self=0x8e3cc8)
    at /usr/local/google/home/sleffler/shodan/kata/projects/kata/apps/system/components/kata-os-common/src/model/mod.rs:200
200             self.init_copy_region();
```

Note that symbol tables are per-component but breakpoints are
per-thread. The seL4 GDB extentions assume all threads in a component
share the same VSpace and hence the same symbol table. Beware also
that when symbol names are ambiguous you can specify fully-qualified
names; e.g. above `main` was expanded to `kata_os_rootserver::main` and
`init_system` to `model::KataOsModel::init_system`. Several well-known
special symbols are supported: `kernel` for the seL4 Kernel, `user`
for any thread running in user space, and `rootserver` for the first
seL4 thread that runs after boot.

## Temporary Breakpoints

In addition to regular GDB breakpoints the sel4 extentions support temporary
breakpoints. The syntax is `sel4 tbreak <threadname> [<symbol>]`. If `<symbol>`
is not specified GDB will stop on the next entry to `<threadname>`. This is
especially useful for stopping the next time you enter user space:

```
(gdb) sel4 thread
kernel
(gdb) sel4 tbreak user
(gdb) c
Continuing.
Thread 2 "matcha.cpu1" received signal SIGTRAP, Trace/breakpoint trap.
[Switching to Thread 2]
0xff80311c in ?? ()
```

or the kernel:

```
(gdb) sel4 tbreak kernel
(gdb) sel4 list-breakpoints
--------------------------
|Thread|Address|Temporary|
--------------------------
|kernel|any    |True     |
--------------------------
(gdb) c
Continuing.

Thread 2 "matcha.cpu1" received signal SIGTRAP, Trace/breakpoint trap.
0xff803000 in ?? ()
(gdb)
```

## Theory of Operation

The kgdb.sh / Renode symbol lookup mechanism is
composed of two parts: a custom Renode extension in
`sim/config/shodan_infrastructure/seL4Extensions.cs` and a custom GDB
extension in `sim/renode/tools/sel4_extensions/gdbscript.py`. `kgdb.sh`
is a simple bash script that starts GDB and connects to the appropriate
remote with the extension loaded.

The Renode extension tracks the VSpace setup for each thread and
translates virtual addresses to physical addresses. Without this work
symbols will be (almost always) incorrectly resolved because every VSpace
memory range starts at 0.

In addition, the extension provides commands to Renode to add debugging hooks to
an execution, all prefixed with the subcommand `seL4` (case matters at the
Renode prompt!). In our simulation config, Renode is configured to start the
seL4 extension on cpu1 using the `cpu1 CreateseL4` command.

The GDB extension provides a matching set of wrappers via the `sel4` command
prefix to examine the simulator state and take a look at threads in the system.

Both extensions provide built in help at their respective command lines, but
suffice it to say, the GDB extension is essentially just an automation mechanism
to load in symbols for the current thread context from disk when the Renode
extension detects a context switch.

During debugging, most symbols will not be loaded in GDB at the start, so it can
be helpful to use `sel4 wait-for-thread <threadname>` to tell Renode to break
execution upon entry of the given thread. When a break occurs the appropriate
symbols may be loaded with the `sel4 switch-symbols <threadname>` command or,
if `sel4 symbol-autoswitching true` is set then Renode will automatically switch
symbol tables based on the current thread. Symbol-autoswitching is disabled by
default because there GDB does not have a reliable way to synchronize the
cmdline with the runtime so repeatedly switching between threads can leave
GDB in a bad state where it will crash on an assert.

To set a breakpoint for a thread that is not the current context, the thread
needs to be entered at least once. After that symbols in that thread can be
resolved so the `sel4 break <threadname> <symbol>` command works. Beware that
if `<symbol>` is wrong (e.g. mis-typed) the error diagnostic will go to the
Renode console, not to the GDB cmdline. Note also that using regular GDB
breakpoints will generate complaints about not being able to set the breakpoints
when switching to a different thread. Best to use `sel4 break` in seL4 user
threads and limit GDB `break` to contexts like the kernel or multihart_boot_rom.

## Esoterica

The Renode extensions identify seL4 threads by intercepting
`seL4_DebugNameThread` system calls that assign a thread an ASCII
string. Typically this happens when the thread first starts up but
it can also happen otherwise; e.g. when the rootserver constructs
a thread it may assign a name. This means that a command like `sel4
wait-for-thread <threadname>` may stop GDB in an unexpected context (e.g.
the rootserver).

In order for the Renode extension to intercept `seL4_DebugNameThread`
system calls it must know the system call ID. Because seL4 does not
have a fixed ABI this number may change depending on how the system is
built and/or if the system source is modified. To deal with this the
system call ID is specified as an argument to the `CreateSeL4` Renode
directive; e.g. `monitor cpu1 CreateSeL4 0xffffffee`.  If you notice seL4
threads are not identified and simulations slow to a crawl then check
the setting--when there is a msimatch Renode will be single-stepping
execution waiting for threads to be entered for the first time (the
`sel4 ready` command may also be helpful in diagnosing this behaviour).