From f454cc4dfeafa1eeae8d299632c7f29b6fd740f5 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 17 Jul 2025 10:46:29 +1000 Subject: [PATCH] sel4test: make instructions linear As #221 points out, copy/pasting the previous instructions linearly without closely reading the text will lead to an error state (wrong directory). Reorganise the code blocks so that they can be copy/pasted and run step by step without running into errors. This also makes the initial example more concrete. Fixes #221 Signed-off-by: Gerwin Klein --- Hardware/index.md | 2 +- projects/sel4test/index.md | 46 +++++++++++++++++++++----------------- 2 files changed, 27 insertions(+), 21 deletions(-) diff --git a/Hardware/index.md b/Hardware/index.md index 713398fc7b..e0ff1f037b 100644 --- a/Hardware/index.md +++ b/Hardware/index.md @@ -150,7 +150,7 @@ seL4 supports PC99-style Intel Architecture Platforms. Running seL4 in a simulator is a quick way to test it out and iteratively develop software. Note that feature support is then limited by the simulator. See the QEMU [Arm](qemu-arm-virt.html) and [RISCV](qemu-riscv-virt.html) targets -and the [simulation instructions for sel4test](../projects/sel4test/#running-it) +and the [simulation instructions for sel4test](../projects/sel4test/) for x86 for how to run seL4 using QEMU. Some hardware platforms support the `SIMULATION=1` option --- this will be marked on the respective platform page and will generally be good enough to run most of the seL4 test suite, but QEMU diff --git a/projects/sel4test/index.md b/projects/sel4test/index.md index 09b2a2eed9..06df5c9cec 100644 --- a/projects/sel4test/index.md +++ b/projects/sel4test/index.md @@ -63,16 +63,26 @@ which ones these are and their corresponding CMake configuration arguments, see the [Supported Platforms](../../Hardware) page. To start a build with a specific configuration we can create a new subdirectory -from the project root and initialise it with `init-build`: +from the project root and initialise it with `init-build`. In the example below +we are using `ia32` as the platform, building in release mode, and with +simulation support switched on. ```bash # create build directory mkdir build cd build # configure build directory +../init-build.sh -DPLATFORM=ia32 -DRELEASE=TRUE -DSIMULATION=TRUE +``` + +The general more form of the last command is + +```sh ../init-build.sh -DPLATFORM= -DRELEASE=[TRUE|FALSE] -DSIMULATION=[TRUE|FALSE] ``` +See below for the full list of [available options](#configuration-options). + This configures your build directory with the necessary CMake configuration for your chosen platform. @@ -102,28 +112,23 @@ ninja ### IA32 Example -We will now build seL4test for IA32, to run on the QEMU simulator. +If you have followed the example instructions above, and `ninja` has completed +successfully, the build will have produced boot images in the `images/` +directory and a `simulate` script. It was produced, because we passed +`-DSIMULATION=TRUE` to CMake. The option is available for hardware platforms +that are marked as "Simulation target: yes" on their platform info page (e.g. +for [IA32](../../Hardware/IA32.md)). -Passing `-DSIMULATION=TRUE` to CMake produces a script to simulate our release -IA32 build. The following commands will configure our CMake build: - -```bash -mkdir ia32_build -cd ia32_build -../init-build.sh -DPLATFORM=ia32 -DRELEASE=TRUE -DSIMULATION=TRUE -``` - -Build it: - -```bash -ninja -``` - -Executing the following commands will run QEMU and point it towards the image we +Executing the `simulate` script will run QEMU and point it towards the image we just built: ```bash ./simulate +``` + +It should produce output such as the following + +``` ... ELF-loading userland images from boot modules: size=0x1dd000 v_entry=0x806716f v_start=0x8048000 v_end=0x8225000 p_start=0x21f000 p_end=0x3fc000 @@ -143,8 +148,9 @@ Test BIND0003 passed ... ``` -To exit QEMU, press `Ctrl-a`, then `x`. The text `All is well in the -universe` indicates a successful build. +To exit QEMU, press `Ctrl-a`, then `x`. In `DEBUG` configurations, there will be +error messages printed for negative tests. These are expected. The text `All is +well in the universe` at the end indicates a successful run. ## Testing a Customised Kernel