# 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 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 simulate-debug
```

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
`simulate-debug`, 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/jtgans/shodan/sw/tock:$cdir:$cwd
Reading symbols from out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf...
add symbol table from file "out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf"
Reading symbols from out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf...
add symbol table from file "out/matcha/riscv32imc-unknown-none-elf/debug/matcha_platform"
Reading symbols from out/matcha/riscv32imc-unknown-none-elf/debug/matcha_platform...
add symbol table from file "out/matcha/riscv32imc-unknown-none-elf/debug/matcha_app"
Reading symbols from out/matcha/riscv32imc-unknown-none-elf/debug/matcha_app...
Remote debugging using localhost:3333
warning: multi-threaded target stopped without sending a thread-id, using first non-exited thread
0x20007b4a in tock_cells::map_cell::MapCell<kernel::callback::AppId>::is_some<kernel::callback::AppId> (self=0x10005af4 <matcha_platform::reset_handler::BUF>)
    at /usr/local/google/home/jtgans/shodan/sw/tock/libraries/tock-cells/src/map_cell.rs:47
47              self.occupied.get()
(gdb)
```

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

`kgdb.sh` will automatically load symbols on the seL4 side, based upon their
thread names, 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 <threadname>`, which
will automatically load them with the appropriate offsets.

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 you've setup your breakpoints using `sel4 break`, you'll need to tell
Renode to enable breakpoints as well with `sel4 breakpoints-enabled True`, and
then `continue`. For example, consider this debugging session:

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

(gdb) # Wait until 'rootserver' thread is set up in seL4
(gdb) sel4 wait-for-thread rootserver

(gdb) # rootserver thread is now the symbol "main" in the thread/program, so we
(gdb) # can break on stopped and associated symbols are loaded.
(gdb) sel4 break rootserver main

(gdb) # Enable extension breakpoints (it's disabled by default as it's pretty
(gdb) # performance-heavy as Renode has to break on every context-switch)
(gdb) sel4 breakpoints-enabled True
(gdb) c

(gdb) # We are in capdl-loader main() function, disable extension breakpoints
(gdb) sel4 breakpoints-enabled False

(gdb) # As we are in capdl-loader thread and proper symbols are loaded, all commands
(gdb) # like break are working correctly
(gdb) b init_system
(gdb) c
```

## 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/config/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 may be
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, not all symbols will 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 the break occurs, Renode will
instruct GDB to load the correct symbol table, and then symbols can be resolved
for later breakpoints, etc.

To set a breakpoint for a thread that is not the current context, use the `sel4
break <threadname> <symbol>` command. This will instruct Renode to load the
appropriate symbol table and break at the right place once that thread is
running. If, however, you need to set a breakpoint in the current thread
context, it's fine to use `break` as normal, since the symbols for the current
thread should be loaded.