| <!-- |
| Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) |
| |
| SPDX-License-Identifier: CC-BY-SA-4.0 |
| --> |
| |
| # CAmkES Debug Manual |
| |
| This document describes the structure and use of the CAmkES debug tool, which allows you to debug systems built on the CAmkES platform. |
| The [Usage](#usage) section describes how to debug a component built on CAmkES, as well as the current limitations of the tool. |
| The [Implementation](#implementation) section describes the internal implementation of the tool. |
| This document assumes some familiary with [CAmkES](https://github.com/seL4/camkes-tool/blob/master/docs/index.md) and the [seL4 microkernel](http://sel4.systems/). |
| If you are not familiar with them then you should read their documentation first. |
| |
| A working example app, [debug-simple](https://github.com/seL4/camkes/tree/master/apps/debug-simple), can be found in the camkes sample apps project. |
| |
| ## Usage |
| |
| This debug tool will provide an interface for you to debug components within CAmkES. Currently, the debug tool is only compatible with ia32. |
| |
| Configuring a component for remote debugging the following is required: |
| * Enable CAmkES preprocessing which is achieved by setting the CAMKES_CPP Kconfig setting. |
| * Ensure that CAPDL_LOADER_WRITEABLE_PAGES is also set to allow GDB to rewrite instructions for software breakpoints. |
| * Add `#include <camkes/gdb/adl.h>` which imports the DEBUG CPP macros used to easily modify existing components. |
| * Add `DEBUG_COMPONENT()` to the definition of your component. This creates connectors that the gdb server uses to modify the components state. |
| * Add `DEBUG_COMPOSITION(client, 3, "0x2f8:0x2ff")` under your assembly section. This adds additional assembly information that creates |
| the debug server and connects it to the serial hardware and your component to debug. 3 is the interrupt number of the serial port and "0x2f8:0x2ff" |
| refers to the hardware IOPort addresses. If you are debugging on hardware with a single serial port, you will need to stop your application and the |
| kernel from using it for output. |
| |
| ### Example CAmkES file |
| ```c |
| import <std_connector.camkes>; |
| #include <camkes/gdb/adl.h> |
| import "Simple.idl4"; |
| |
| component Client { |
| control; |
| uses Simple a; |
| /* This adds the required connector interfaces for the debug server to use */ |
| DEBUG_COMPONENT() |
| } |
| |
| component Echo { |
| provides Simple b; |
| } |
| |
| assembly { |
| composition { |
| component Echo echo; |
| component Client client; |
| connection seL4RPCCall simple(from client.a, to echo.b); |
| } |
| } |
| |
| /* This adds the assembly and configuration parts for the debug server to connect to `client` |
| and specifies the serial port settings. |
| */ |
| DEBUG_COMPOSITION(client, 3, "0x2f8:0x2ff") |
| ``` |
| |
| |
| ### Debugging |
| After you have built the image, you should be able to connect to the serial port via GDB. |
| The GDB connection will only be opened once there is a fault or breakpoint, so if you want |
| to inspect on startup you should set a code breakpoint within the component you are debugging. |
| This is achieved by using `camkes_software_breakpoint();` provided by `#include <camkes/debug.h>` |
| |
| ### Using GDB |
| Current functionality includes: |
| * reading memory and registers, backtrace, seeing variables. |
| * Writing memory and registers |
| * Software and hardware breakpoints can be set. |
| * Hardware watchpoints can be set on global variables. |
| |
| ### Using qemu |
| |
| It's possible to debug a system running in qemu. To do this, one must forward the output of the second serial port to the tcp port gdb is connected to (1234 by default). |
| We provide a script that runs the current image in the "images" directory on qemu, forwarding the first serial port to the terminal where the script is running, |
| and the second serial port to 127.0.0.1:1234. |
| |
| To debug with the script, run `tools/camkes/debug/debug_qeum` in one terminal, and run `gdb` in a second terminal, running both commands from the top level of this project. |
| |
| ```bash |
| qemu-system-i386 -nographic -m 512 -cpu Haswell \ |
| -kernel kernel-ia32-pc99 \ |
| -initrd capdl-loader-experimental-image-ia32-pc99 \ |
| -device isa-serial,chardev=ch0 \ |
| -device isa-serial,chardev=ch1 \ |
| -chardev file,path=/dev/tty,id=ch0 \ |
| -chardev socket,host=127.0.0.1,port=1234,id=ch1,server,wait |
| ``` |
| |
| ### Known issues / Limitations |
| * Currently only compatible with ia32 |
| * Watch points are not supported on stack variables |
| * Taking a backtrace should work the first time, but will crash the component, so that no more debugging can be done |
| |
| |
| ## Implementation |
| |
| The information below assumes you are familiar with the functionality of CAmkES. |
| |
| ### Architecture |
| |
| To enable debugging, a debug server component is created that can communicate with a remote GDB client over serial using the GDB remote serial protocol. |
| Currently it communicates over serial by having exclusive access to the serial device. Once a client attaches, the server interprets GDB commands from the |
| client and provides responses. To achieve this the GDB server component is connected to the debug target component using a seL4GDB rpc connection. This connection |
| allows the server to read and write memory and registers, as well as set hardware breakpoints and watchpoints. Additionally the target thread's fault handler endpoints |
| are all set to an endpoint that the GDB server waits on. When the target first faults, this results in seL4 sending a fault message to the GDB server, that then decodes this |
| message and sends the relevant serial packet to the remote GDB client. The remote GDB client can then interract with the debug target. |
| |
| ### Relevant files |
| |
| **include/builtin/gdb-delegate.camkes** - This defines the CAmkES ADL required to create the GDB components and connections. |
| |
| **libsel4camkes/include/camkes/gdb/idl.h** - Contains the CPP macros for more easily modifying a CAmkES project for debugging. |
| |
| **camkes/templates/component.debug.c** - Debug target implementation of the RPC interface for reading and writing, registers and memory. |
| |
| **camkes/templates/seL4GDB-from.template.c** - Template for the fault ep on the component side. This should just be generating a cap, since it is set manually later. |
| **camkes/templates/seL4GDB-to.template.c** - Template code for the GDB server fault handler. This decodes the fault type and uses the gdb server library code for handling. |
| |
| **libsel4camkes/src/gdb_server/[gdb.c|serial.c]** - GDB server and serial implementation can be found here. |
| **libsel4camkes/include/camkes/gdb/[gdb.h|serial.h|delegate_types.h]** - Header files for GDB server and serial interfaces. |
| |
| **camkes/templates/[seL4GDBMem-to.template.c|seL4GDBMem-from.template.c]** - Template code for a fault handler to check if memory is readable or writeable on the debug target. |
| |
| |