secc
/
seL4-microkit
mirror of https://github.com/seL4/microkit.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Initial public source code release of seL4 core platform

This commit is contained in:
Ben Leslie 2021-10-20 23:03:39 +00:00
commit 59f3d7ecea
93 changed files with 11904 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
.flake8 Normal file
View File

@ -0,0 +1,7 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
[flake8]
ignore = E501

7
.gitignore vendored Normal file
View File

@ -0,0 +1,7 @@
__pycache__
*-sdk-*/
build/
env/
release/
tmp_build/

22
LICENSE Normal file
View File

@ -0,0 +1,22 @@
Copyright 2021 Breakaway Consulting Pty. Ltd.
Redistribution and use in source and binary forms, with or without modification,
are permitted provided that the following conditions are met:
o Redistributions of source code must retain the above copyright notice, this list
of conditions and the following disclaimer.
o Redistributions in binary form must reproduce the above copyright notice, this
list of conditions and the following disclaimer in the documentation and/or
other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

140
README.md Normal file
View File

@ -0,0 +1,140 @@
# seL4 Core Platform
The purpose of the seL4 Core Platform (sel4cp) is to enable system designers to create static software systems based on the seL4 microkernel.
The seL4 Core Platform consists of three parts:
* seL4 Core Platform Library
* seL4 Core Platform initial task
* seL4 Core Platform tool
The seL4 Core Platform is distributed as a software development kit (SDK).
This repository is the source for the sel4cp SDK.
If you are *developing* sel4cp itself this is the repo you want!
If you are a system designer and want to *use* the sel4cp SDK please download a pre-built SDK.
The remainder of this README is for sel4cp developers.
## Developer system requirements
Development of sel4cp has primarily been performed on Ubuntu 18.04 LTS (x86_64).
This section attempts to list the packages or external development tools which are required during development.
At this stage it may be incomplete.
Please file an issue if additional packages are required.
* git
* make
* python3.9
* python3.9-venv
* musl-1.2.2
* ARM GCC compiler; 10.2-2020.11
On Ubuntu 18.04 there are no packages available for musl-1.2.2; it must be compiled from source.
On Ubuntu 18.04 Python 3.9 is available via the *deadsnakes* PPA: https://launchpad.net/~deadsnakes/+archive/ubuntu/ppa
To use this:
$ sudo add-apt-repository ppa:deadsnakes/ppa
$ sudo apt update
$ sudo apt install python3.9 python3.9-venv
Additonally, a number of Python libraries are needed.
These should be installed using `pip`.
$ python3.8 -m venv pyenv
$ ./pyenv/bin/pip install --upgrade pip setuptools wheel
$ ./pyenv/bin/pip install -r requirements.txt
Note: It is a high priority of the authors to ensure builds are self-contained and repeatable.
A high value is placed on using specifically versioned tools.
At this point in time this is not fully realised, however it is a high priority to enable this in the near future.
The ARM toolchain is available from:
https://developer.arm.com/tools-and-software/open-source-software/developer-tools/gnu-toolchain/gnu-a/downloads/10-2-2020-11
The specific version used for development is the x86_64-aarch64-none-elf version:
https://developer.arm.com/-/media/Files/downloads/gnu-a/10.2-2020.11/binrel/gcc-arm-10.2-2020.11-x86_64-aarch64-none-elf.tar.xz?revision=79f65c42-1a1b-43f2-acb7-a795c8427085&hash=61BBFB526E785D234C5D8718D9BA8E61
Note: There are no plans to support development of sel4cp on any platforms other than Linux x86_64.
## seL4 Version
The SDK includes a binary of the seL4 kernel.
During the SDK build process the kernel is build from source.
At this point in time there are some minor changes to the seL4 kernel required for seL4 Core Platform.
Please clone seL4 from:
git@github.com:BreakawayConsulting/seL4.git
The correct branch to use is `sel4cp-core-support`.
Testing has been performed using commit `c8ef493d038b81cc43f82c0190788e4b3bdb4d9d`.
## Building the SDK
$ ./env/bin/python build_sdk.py --sel4=<path to sel4>
## SDK Layout
The SDK is delivered as a `tar.gz` file.
The SDK top-level directory is `sel4cp-sdk-$VERSION`.
The directory layout underneath the top-level directory is:
```
bin/
bin/sel4cp
bsp/$board/$config/include/
bsp/$board/$config/include/sel4cp.h
bsp/$board/$config/lib/
bsp/$board/$config/lib/libsel4cp.a
bsp/$board/$config/lib/sel4cp.ld
bsp/$board/$config/elf
bsp/$board/$config/elf/loader.elf
bsp/$board/$config/elf/kernel.elf
bsp/$board/$config/elf/monitor.elf
```
The currently supported boards:
* tqma8xqp1gb
The currently supported configurations are:
* release
* debug
## Supported Boards
### tqma8xqp-1gb
The TQMa8Xx Embedded Module from TQ Group configured with the NXP i.MX8QXP SoC and 1GiB of DDR3 ECC memory.
https://www.tq-group.com/en/products/tq-embedded/arm-architecture/tqma8xx/
All testing has been performed with the module on the MBa8Xx carrier board which is included in the starter kit.
The provided board support should be at the module level and does not make any assumptions about the carrier board.
Note: There are different configured of the TQMa8Xx board which include different NXP SoCs and different memory configurations.
Such modules are not supported.
## Supported Configurations
## Release
In release configuration the loader, kernel and monitor do *not* perform any direct serial output.
## Debug
The debug configuration includes basic print output form the loader, kernel and monitor.

365
build_sdk.py Normal file
View File

@ -0,0 +1,365 @@
"""The SDK build script.
# Why Python (and not make, or something else)?
We call out to Make, but having this top-level driver script
is useful.
There are just a lot of things that are much easier in Python
than in make.
"""
from argparse import ArgumentParser
from os import popen, system
from shutil import copy
from pathlib import Path
from dataclasses import dataclass
from tarfile import open as tar_open, TarInfo
from typing import Dict, Union
NAME = "sel4cp"
VERSION = "1.2.6"
SEL4CP_EPOCH = 1616367257
KERNEL_CONFIG_TYPE = Union[bool, str]
KERNEL_OPTIONS = Dict[str, KERNEL_CONFIG_TYPE]
@dataclass
class BoardInfo:
name: str
gcc_cpu: str
kernel_options: KERNEL_CONFIG_TYPE
examples: Dict[str, Path]
@dataclass
class ConfigInfo:
name: str
debug: bool
kernel_options: KERNEL_CONFIG_TYPE
SUPPORTED_BOARDS = (
BoardInfo(
name="tqma8xqp1gb",
gcc_cpu="cortex-a35",
kernel_options = {
"KernelPlatform": "tqma8xqp1gb",
"KernelIsMCS": True,
"KernelArmExportPCNTUser": True,
},
examples = {
"ethernet": Path("example/tqma8xqp1gb/ethernet")
}
),)
SUPPORTED_CONFIGS = (
ConfigInfo(
name="release",
debug=False,
kernel_options = {},
),
ConfigInfo(
name="debug",
debug=True,
kernel_options = {
"KernelDebugBuild": True,
"KernelPrinting": True,
"KernelVerificationBuild": False
}
),
)
def tar_filter(tarinfo: TarInfo) -> TarInfo:
"""This is used to change the tarinfo when created the .tar.gz archive.
This ensures the tar file does not leak information from the build environment.
"""
# Force uid/gid
tarinfo.uid = tarinfo.gid = 0
tarinfo.uname = tarinfo.gname = "sel4cp"
# This is unlikely to be set, but force it anyway
tarinfo.pax_headers = {}
tarinfo.mtime = SEL4CP_EPOCH
assert tarinfo.isfile() or tarinfo.isdir()
# Set the permissions properly
if tarinfo.isdir():
tarinfo.mode = tarinfo.mode & ~0o777 | 0o557
if tarinfo.isfile():
if "/bin/" in tarinfo.name:
# Assume everything in bin should be executable.
tarinfo.mode = tarinfo.mode & ~0o777 | 0o755
else:
tarinfo.mode = tarinfo.mode & ~0o777 | 0o644
return tarinfo
def test_tool() -> None:
r = system(
"./env/bin/python -m unittest discover -s tool -v"
)
assert r == 0
def build_tool(tool_target: Path) -> None:
r = system(
"./env/bin/pyoxidizer build --release --path tool --target-triple x86_64-unknown-linux-musl"
)
assert r == 0
tool_output = "./tool/build/x86_64-unknown-linux-musl/release/install/sel4cp"
r = system(f"strip {tool_output}")
assert r == 0
copy(tool_output, tool_target)
def build_sel4(
sel4_dir: Path,
root_dir: Path,
build_dir: Path,
board: BoardInfo,
config: ConfigInfo,
) -> None:
"""Build seL4"""
build_dir = build_dir / board.name / config.name / "sel4"
build_dir.mkdir(exist_ok=True, parents=True)
sel4_install_dir = build_dir / "install"
sel4_build_dir = build_dir / "build"
sel4_install_dir.mkdir(exist_ok=True, parents=True)
sel4_build_dir.mkdir(exist_ok=True, parents=True)
print(f"Building sel4: {sel4_dir=} {root_dir=} {build_dir=} {board=} {config=}")
config_args = list(board.kernel_options.items()) + list(config.kernel_options.items())
config_strs = []
for arg, val in sorted(config_args):
if isinstance(val, bool):
str_val = "ON" if val else "OFF"
else:
str_val = str(val)
s = f"-D{arg}={str_val}"
config_strs.append(s)
config_str = " ".join(config_strs)
platform = board.name
cmd = (
f"cmake -GNinja -DCMAKE_INSTALL_PREFIX={sel4_install_dir.absolute()} "\
f" -DKernelPlatform={platform} {config_str} " \
f"-S {sel4_dir.absolute()} -B {sel4_build_dir.absolute()}")
r = system(cmd)
if r != 0:
raise Exception(f"Error configuring sel4: cmd={cmd}")
cmd = f"cmake --build {sel4_build_dir.absolute()}"
r = system(cmd)
if r != 0:
raise Exception(f"Error building sel4: cmd={cmd}")
cmd = f"cmake --install {sel4_build_dir.absolute()}"
r = system(cmd)
if r != 0:
raise Exception(f"Error installing sel4: cmd={cmd}")
elf = sel4_install_dir / "bin" / "kernel.elf"
dest = (
root_dir / "board" / board.name / config.name / "elf" / "sel4.elf"
)
dest.unlink(missing_ok=True)
copy(elf, dest)
# Make output read-only
dest.chmod(0o444)
include_dir = root_dir / "board" / board.name / config.name / "include"
for source in ("kernel_Config", "libsel4", "libsel4/sel4_Config", "libsel4/autoconf"):
source_dir = sel4_install_dir / source / "include"
for p in source_dir.rglob("*"):
if not p.is_file():
continue
rel = p.relative_to(source_dir)
dest = include_dir / rel
dest.parent.mkdir(exist_ok=True, parents=True)
dest.unlink(missing_ok=True)
copy(p, dest)
dest.chmod(0o444)
def build_elf_component(
component_name: str,
root_dir: Path,
build_dir: Path,
board: BoardInfo,
config: ConfigInfo,
) -> None:
"""Build a specific ELF component.
Right now this is either the loader or the monitor
"""
sel4_dir = root_dir / "board" / board.name / config.name
build_dir = build_dir / board.name / config.name / component_name
build_dir.mkdir(exist_ok=True, parents=True)
r = system(
f"BUILD_DIR={build_dir.absolute()} GCC_CPU={board.gcc_cpu} SEL4_SDK={sel4_dir.absolute()} make -C {component_name}"
)
if r != 0:
raise Exception(
f"Error building: {component_name} for board: {board.name} config: {config.name}"
)
elf = build_dir / f"{component_name}.elf"
dest = (
root_dir / "board" / board.name / config.name / "elf" / f"{component_name}.elf"
)
dest.unlink(missing_ok=True)
copy(elf, dest)
# Make output read-only
dest.chmod(0o444)
def build_doc(root_dir):
output = root_dir / "doc" / "sel4cp_user_manual.pdf"
r = system(f'pandoc docs/manual.md -o {output}')
assert r == 0
def build_lib_component(
component_name: str,
root_dir: Path,
build_dir: Path,
board: BoardInfo,
config: ConfigInfo,
) -> None:
"""Build a specific library component.
Right now this is just libsel4.a
"""
sel4_dir = root_dir / "board" / board.name / config.name
build_dir = build_dir / board.name / config.name / component_name
build_dir.mkdir(exist_ok=True, parents=True)
r = system(
f"BUILD_DIR={build_dir.absolute()} GCC_CPU={board.gcc_cpu} SEL4_SDK={sel4_dir.absolute()} make -C {component_name}"
)
if r != 0:
raise Exception(
f"Error building: {component_name} for board: {board.name} config: {config.name}"
)
lib = build_dir / f"{component_name}.a"
lib_dir = root_dir / "board" / board.name / config.name / "lib"
dest = lib_dir / f"{component_name}.a"
dest.unlink(missing_ok=True)
copy(lib, dest)
# Make output read-only
dest.chmod(0o444)
link_script = Path(component_name) / "sel4cp.ld"
dest = lib_dir / "sel4cp.ld"
dest.unlink(missing_ok=True)
copy(link_script, dest)
# Make output read-only
dest.chmod(0o444)
crt0 = build_dir / "crt0.o"
dest = lib_dir / "crt0.o"
dest.unlink(missing_ok=True)
copy(crt0, dest)
# Make output read-only
dest.chmod(0o444)
include_dir = root_dir / "board" / board.name / config.name / "include"
source_dir = Path(component_name) / "include"
for p in source_dir.rglob("*"):
if not p.is_file():
continue
rel = p.relative_to(source_dir)
dest = include_dir / rel
dest.parent.mkdir(exist_ok=True, parents=True)
dest.unlink(missing_ok=True)
copy(p, dest)
dest.chmod(0o444)
def main() -> None:
parser = ArgumentParser()
parser.add_argument("--sel4", type=Path, required=True)
args = parser.parse_args()
sel4_dir = args.sel4.expanduser()
if not sel4_dir.exists():
raise Exception(f"sel4_dir: {sel4_dir} does not exist")
root_dir = Path("release") / f"{NAME}-sdk-{VERSION}"
tar_file = Path("release") / f"{NAME}-sdk-{VERSION}.tar.gz"
source_tar_file = Path("release") / f"{NAME}-source-{VERSION}.tar.gz"
dir_structure = [
root_dir / "doc",
root_dir / "bin",
root_dir / "board",
]
for board in SUPPORTED_BOARDS:
board_dir = root_dir / "board" / board.name
dir_structure.append(board_dir)
for config in SUPPORTED_CONFIGS:
config_dir = board_dir / config.name
dir_structure.append(config_dir)
dir_structure += [
config_dir / "include",
config_dir / "lib",
config_dir / "elf",
]
for dr in dir_structure:
dr.mkdir(exist_ok=True, parents=True)
copy(Path("LICENSE"), root_dir)
tool_target = root_dir / "bin" / "sel4cp"
if not tool_target.exists():
test_tool()
build_tool(tool_target)
build_doc(root_dir)
build_dir = Path("build")
for board in SUPPORTED_BOARDS:
for config in SUPPORTED_CONFIGS:
build_sel4(sel4_dir, root_dir, build_dir, board, config)
build_elf_component("loader", root_dir, build_dir, board, config)
build_elf_component("monitor", root_dir, build_dir, board, config)
build_lib_component("libsel4cp", root_dir, build_dir, board, config)
# Setup the examples
for example, example_path in board.examples.items():
include_dir = root_dir / "board" / board.name / "example" / example
source_dir = example_path
for p in source_dir.rglob("*"):
if not p.is_file():
continue
rel = p.relative_to(source_dir)
dest = include_dir / rel
dest.parent.mkdir(exist_ok=True, parents=True)
dest.unlink(missing_ok=True)
copy(p, dest)
dest.chmod(0o444)
# At this point we create a tar.gz file
with tar_open(tar_file, "w:gz") as tar:
tar.add(root_dir, arcname=root_dir.name, filter=tar_filter)
# Build the source tar
process = popen("git ls-files")
filenames = [Path(fn.strip()) for fn in process.readlines()]
process.close()
source_prefix = Path(f"{NAME}-source-{VERSION}")
with tar_open(source_tar_file, "w:gz") as tar:
for filename in filenames:
tar.add(filename, arcname=source_prefix / filename, filter=tar_filter)
if __name__ == "__main__":
main()

41
docs/README.md Normal file
View File

@ -0,0 +1,41 @@
## Building the example
$ cd example
$ make
The output will be `hello.sysbin` which is, eventually, intended to by a file that can be directly loaded onto a board using the board's regular bootloader.
## Bootstrapping memory
In a perfect world, the newly propose [boot interface](https://sel4.discourse.group/t/pre-rfc-boot-interface/295/8) would already be in place.
This would allow for all the memory regions to be directly initialized by the loader.
However, pushing those changes will require significant time (and possibly reverification).
As such an alternative approach is required.
The initial images will need to be packed into the initial tasks image, and then the initial task (i.e. the platform runtime) will need to move memory about appropriately.
The root server ELF image will need to be manipulated appropriately to include a packed memory image (as well as other data structures).
## seL4 Core Platform Library
The header and source files for the library are in the `libsel4cp` directory.
To compile against the library you need flags such as:
-I$(LIBSEL4CP)/include -L$(LIBSEL4CP) -llibsel4cp
Where LIBSELCP variable refers to the `libsel4cp` directory.
Note: current state is that this is used in place.
Ftuture state is that this shall be merged with an seL4 SDK to simplify distribution and configuration.
### Functions
This section provides a brief summary of the functions made available in the seL4 Core Platform Library.
* `void sel4cp_dbg_putc(int c)`: Output a single character to the debug console.
* `void sel4cp_dbg_puts(const char *s)`: Output a string to the debug console.

605
docs/manual.md Normal file
View File

@ -0,0 +1,605 @@
---
title: seL4 Core Platform User Manual (v1.2-pre)
papersize:
- a4
fontsize:
- 11pt
geometry:
- margin=2cm
fontfamily:
- charter
header-includes:
- \usepackage{titlesec}
- \newcommand{\sectionbreak}{\clearpage}
subparagraph: yes
numbersections: yes
colorlinks: true
---
\maketitle
\thispagestyle{empty}
\clearpage
\tableofcontents
\pagenumbering{roman}
\clearpage
\pagenumbering{arabic}
\setcounter{page}{1}
# Introduction
seL4 Core Platform (sel4cp) is a small and simple operating system (OS) built on the seL4 microkernel.
sel4cp is designed for building system with a *static architecture*.
A static architecture is one where system resources are assigned up-front at system initialisation time.
## Purpose
The seL4 Core Platform is intended to:
* provide a small and simple OS for a wide range of IoT, cyberphysical and other embedded use cases;
* provide a reasonable degree of application portability appropriate for the targeted use cases;
* make seL4-based systems easy to develop and deploy within the target areas;
* leverage seL4's strong isolation properties to support a near-minimal *trusted computing base* (TCB);
* retain seL4's trademark performance for systems built with it;
* be, in principle, amenable to formal analysis of system safety and security properties (although such analysis is beyond the initial scope).
## Overview
An sel4cp system is built from a set of individual programs that are isolated from each other, and the system, in *protection domains*.
Protection domains can interact by calling *protected procedures* or sending *notifications*.
sel4cp is distributed as a software development kit (SDK).
The SDK includes the tools, libraries and binaries required to build an sel4cp system.
The sel4cp source is also available which allows you to customize or extend sel4cp and produce your own SDK.
To build an sel4cp system you will write some programs that use `libsel4cp`.
sel4cp programs are a little different to a typical progress on a Linux-like operating system.
Rather than a single `main` entry point, a program has three distinct entry points: `init`, `notified` and, optionally, `protected`.
The individual programs are combined to produce a single bootable *system image*.
The format of the image is suitable for loading by the target board's bootloader.
The sel4cp tool, which is provided as part of the SDK, is used to generate the system image.
The sel4cp tool takes a *system description* as input.
The system description is an XML file that specifies all the objects that make up the system.
*Note*: sel4cp does **not** impose any specific build system; you are free to choose the build system that works best for you.
\clearpage
## Document Structure
The [Concepts](#concepts) chapter describes the various concepts that make up sel4cp.
It is recommended that you familiarise yourself with these concepts before trying to build a system.
The [SDK](#sdk) chapter describes the software development kit, including its components and system requirements for use.
The [sel4cp tool](#tool) chapter describes the host system tool used for generating a firmware image from the system description.
The [libsel4cp](#libsel4cp) chapter describes the interfaces to the core platform library.
The [System Description Format](#sysdesc) chapter describes the format of the system description XML file.
The [Board Support Packages](#bsps) chapter describes each of the board support packages included in the SDK.
The [Rationale](#rationale) chapter documents the rationale for some of the key design choices of in sel4cp.
# Concepts {#concepts}
This chapter describes the key concepts provided by sel4cp.
As with any set of concepts there are words that take on special meanings.
This document attempts to clearly describe all of these terms, however as the concepts are inter-related it is sometimes necessary to use a term prior to its formal introduction.
* [system](#system)
* [protection domain (PD)](#pd)
* [channel](#chan)
* [memory region](#mr)
* [notification](#notification)
* [protected procedure](#pp)
## System {#system}
At the most basic level sel4cp provides the platform for running a *system* on a specific board.
As a *user* of sel4cp you use the platform to create a softare system that implements your use case.
The system is described in a declarative configuration file, and the sel4cp tool takes this system description as an input and produces an appropriate system image that can be loaded on the target board.
The key elements that make up a system are *protection domains*, *memory regions* and *channels*.
## Protection Domains {#pd}
A **protection domain** (PD) is the fundamental runtime abstraction in the seL4 platform.
It is analogous, but very different in detail, to a process on a UNIX system.
A PD provides a thread of control that executes within a fixed virtual address space.
The isolation provided by the virtual address space is enforced by the underlying hardware MMU.
The virtual address space for a PD has mappings for the PD's *program image* along with any memory regions that the PD can access.
The program image is an ELF file containing the code and data which implements the isolated component.
The platform supports a maximum of 63 protection domains.
### Entry points
Although a protection domain is somewhat analogous to a process, it has a considerably different program structure and life-cycle.
A process on a typical operating system will have a `main` function which is invoked by the system when the process is created.
When the `main` function returns the process is destroyed.
By comparison a protection domain has three entry points: `init`, `notify` and, optionally, `protected`.
When an seL4 Core Platform system is booted, all PDs in the system execute the `init` entry point.
The `notified` entry point will be invoked whenever the protection domain receives a *notification* on a *channel*.
The `protected` entry point is invoked when a PD's *protected procedure* is called by another PD.
A PD does not have to provide a protected procedure, therefore the `protected` entry point is optional.
These entry points are described in more detail in subsequent sections.
**Note:** The processing of `init` entry points is **not** synchronised across protection domains.
Specifically, it is possible for a high priority PD's `notified` or `protected` entry point to be called prior to the completion of a low priority PD's `init` entry point.
The overall computational model for an sel4cp system is a set of isolated components reacting to incoming events.
### Scheduling
The PD has a number of scheduling attrbites that are configured in the system description:
* priority (0 -- 254)
* period (microseconds)
* budget (microseconds)
The budget and period bound the fraction of CPU time that a PD can consume.
Specifically, the **budget** specifies the amount of time for which the PD is allowed to execute.
Once the PD has consumed its budget, it is no longer runnable until the budget is replenished; replenishment happens once every **period** and resets the budget to its initial value.
This means that the maximum fraction of CPU time the PD can consume is budget/period.
The budget cannot be larger than the period.
A budget that equals the period (aka. a "full" budget) behaves like a traditional time slice: After executing for a full period, the PD is preempted and put at the end of the scheduling queue of its priority. On other words, PDs with full budgets are scheduled round-robin with a time slice defined by the period.
The **priority** determines which of the runnable PDs to schedule. A PD is runnable if one of its entry points have been invoked and it has budget remaining in the current period.
Runnable PDs of the same priority are scheduled in a round-robin manner.
## Memory Regions {#mr}
A *memory region* is a contiguous range of physical memory.
A memory region may have a *fixed* physical address.
For memory regions without a fixed physical address the physical address is allocated as part of the build process.
Typically, memory regions with a fixed physical address represents memory-mapped device registers.
The size of a memory region must be a multiple of a supported page size.
The supported page sizes are architecture dependent.
For example, on AArch64 architectures, sel4cp support 4KiB and 2MiB pages.
The page size for a memory region may be specified explicitly in the system description.
If page size is not specified, the smallest supported page size is used.
*Note:* The page size also restricts the alignment of the memory region's physical address.
A fixed physical address must be a multiple of the specified page size.
A memory region can be *mapped* into one or more protection domains.
The mapping has a number of attributes, which include:
* the virtual address at which the region is mapped in the PD
* caching attributes (mostly relevant for device memory)
* permissions (read, write and execute)
**Note:** When a memory region is mapped into multiple protection
domains, the attributes used for different mapping may vary.
## Channels
A *channel* enables two protection domains to interact using protected procedures or notifications.
Each connects connects exactly two PDs; there are no multi-party channels.
When a channel is created between two PDs, a *channel identifier* is configured for each PD.
The *channel identifier* is used by the PD to reference the channel.
Each PD can refer to the channel with a different identifier.
For example if PDs **A** and **B** are connected by a channel, **A** may refer to the channel using an identifier of **37** while **B** may use **42** to refer to the same channel.
**Note:** There is no way for a PD to directly refer to another PD in the system.
PDs can only refer to other PDs indirectly if there is a channel between them.
In this case the channel identifier is effectively a proxy identifier for the other PD.
So, to extend the prior example, **A** can indirectly refer to **B** via the channel identifier **37**.
Similary, **B** can refer to **A** via the channel identifier **42**.
The system supports a maximum up 64 channels and interrupts per protection domain.
### Protected procedure
A protection domain may provide a *protected procedure* (PP) which can be invoked from another protection domain.
Up to 64 words of data may be passed as arguments when calling a protected procedure.
The protected procedure return value may also be up to 64 words.
When a protection domain calls a protected procedure, the procedure executes within the context of the providing protection domain.
A protected call is only possible if the callee has strictly higher priority than the caller.
Transitive calls are possible, and as such a PD may call a *protected procedure* in another PD from a `protected` entry point.
However the overall call graph between PDs forms a directed, acyclic graph.
It follows that a PD can not call itself, even indirectly.
For example, `A calls B calls C` is valid (subject to the priority constraint), while `A calls B calls A` is not valid.
When a protection domain is called, the `protected` entry point is invoked.
The control returns to the caller when the `protected` entry point returns.
The caller is blocked until the callee returns.
Protected procedures must execute in bounded time.
It is intended that future version of the platform will enforce this condition through static analysis.
In the present version the callee must trust the callee to conform.
In general, PPs are provided by services for use by clients that trust the protection domain to provide that service.
To call a PP, a PD calls `sel4cp_ppcall` passing the channel identifier and a *message* structure.
A *message* structure is returned from this function.
When a PD's protected procedure is invoked, the `protected` entry point is invoked with the channel identifier and message structure passed as arguments.
The `protected` entry point must return a message structure.
### Notification
A notification is a (binary) semaphore-like synchronisation mechanism.
A PD can *notify* another PD to indicate availability of data in a shared memory region if they share a channel.
To notify another PD, a PD calls `sel4cp_notify`, passing the channel identifier.
When a PD receives a notification, the `notified` entry point is invoked with the appropriate channel identifier passed as an argument.
Unlike protected procedures, notifications can be sent in either direction on a channel regardless of priority.
**Note:** Notifications provide a mechanism for synchronisation between PDs, however this is not a blocking operation.
If a PD notifies another PD, that PD will become scheduled to run (if it is not already), but the current PD does **not** block.
Of course, if the notified PD has a higher priority than the current PD, then the current PD will be preempted (but not blocked) by the other PD.
## Interrupts
Hardware interrupts can be used to notify a protection domain.
The system description specifies if a protection domain receives notifications for any hardware interrupt sources.
Each hardware interrupt is assigned a channel identifier.
In this way the protection domain can distinguish the hardware interrupt from other notifications.
A specific hardware interrupt can only be associated with at most one protection domain.
Although interrupts are the final concept to be described here, they are in some ways the most important.
Without interrupts a system would not do much after system initialisation.
sel4cp does not provides timers, nor any *sleep* API.
After initialisation, activity in the system is initiated by an interrupt causing a `notified` entry point to be invoked.
That notified function may in turn notify or call other protection domains that cause other system activity, but eventually all activity indirectly initiated from that interrupt will complete, at which point the system is inactive again until another interrupt occurs.
# SDK {#sdk}
sel4cp is distributed as a software development kit (SDK).
The SDK includes support for one or more *boards*.
Two *configurations* are supported for each board: *debug* and *release*.
The *debug* configuration includes a debug build of the seL4 kernel to allow console debug output using the kernel's UART driver.
The SDK contains:
* sel4cp user manual (this document)
* sel4cp tool
Additionally, for each supported board configuration the following are provided:
* `libsel4cp`
* `loader.elf`
* `kernel.elf`
* `monitor.elf`
For some boards there are also examples provided in the `examples` directory.
The sel4cp SDK does **not** provide, nor require, any specific build system.
The user is free to build their system using whatever build system is deemed most appropriate for their specific use case.
The sel4cp tool should be invoked by the system build process to transform a system description (and any referenced program images) into an image file which can be loaded by the target board's bootloader.
The ELF files provided as program images should be standard ELF files and have been linked against the provided libsel4cp.
## System Requirements
The sel4cp tool requires Linux x86_64.
The sel4cp tool is statically linked and should run on any Linux distribution.
The sel4cp tool does not depend on any additional system binaries.
# sel4cp tool {#tool}
The sel4cp tool is available in `bin/sel4cp`.
The sel4cp tool takes as input a system description.
The format of the system description is described in a subsequent chapter.
Usage:
sel4cp [-h] [-o OUTPUT] [-r REPORT] system
The path to the sytem description file must be provided.
In the case of errors, a diagnostic message shall be output to `stderr` and a non-zero code returned.
In the case of success, a loadable image file and a report shall be produced.
The output paths for these can be specified by `-o` and `-r` respectively.
The default output paths are `loader.img` and `report.txt`.
The loadable image will be a binary that can be loaded by the board's bootloader.
The report is a plain text file describing important information about the system.
The report can be useful when debugging potential system problems.
This report does not have a fixed format and may change between versions.
It is not intended to be machine readable.
# libsel4cp {#libsel4cp}
All program images should link against `libsel4cp.a`.
The library provides the C runtime for the protection domain, along with interfaces for the sel4cp APIs.
The component must provide the following functions:
void init(void);
void notified(sel4cp_channel ch);
Additionally, if the protection domain provides a protected procedure it must also implement:
sel4cp_msginfo protected(sel4cp_channel ch, sel4cp_msginfo msginfo);
`libsel4cp` provides the following functions:
sel4cp_msginfo sel4cp_ppcall(sel4cp_channel ch, sel4cp_msginfo msginfo);
void sel4cp_notify(sel4cp_channel ch);
sel4cp_msginfo sel4cp_msginfo_new(uint64_t label, uint16_t count);
uint64_t sel4cp_msginfo_get_label(sel4cp_msginfo msginfo);
void sel4cp_irq_ack(sel4cp_channel ch);
void sel4cp_mr_set(uint8_t mr, uint64_t value);
uint64_t sel4cp_mr_get(uint8_t mr);
## `void init(void)`
Every PD must expose an `init` entry point.
This is called by the system at boot time.
## `sel4cp_message protected(sel4cp_channel channel, sel4cp_message message)`
The `protected` entry point is optional.
This is called when another PD call `sel4cp_ppcall` on a channel shared with the PD.
The `channel` argument identifies the channel on which the PP was invoked.
Indirectly this identifies the PD performing the call.
Channel identifiers are specified in the system configuration.
**Note:** The channel argument is passed by the system and is unforgable.
The `message` argument is the argument passed to the PP and is provided by the calling PD.
The contents of the message is up to a pre-arranged protocol between the PDs.
The message contents are opaque to the system.
Note: The message is *copied* from the caller.
The returned `message` is the return value of the protected procedure.
As with arguments this is *copied* to the caller.
## `void notified(sel4cp_channel channel)`
The `notified` entry point is called by the system when a PD has received a notification on a channel.
`channel` identifies the channel which has been notified (and indirectly the PD that performed the notification).
**Note:** `channel` could identify an interrupt.
Channel identifiers are specified in the system configuration.
## `sel4cp_message sel4cp_ppcall(sel4cp_channel channel, sel4cp_message message)`
Performs a call to a protected procedure in a different PD.
The `channel` argument identifies the protected procedure to be called.
`message` is passed as argument to the protected procedure.
Channel identifiers are specified in the system configuration.
The protected procedure's return data is returned in the `sel4cp_message`.
## `void sel4cp_notify(sel4cp_channel channel)`
Notify the `channel`.
Channel identifiers are specified in the system configuration.
## `void sel4cp_irq_ack(sel4cp_channel ch)`
Acknowledge the interrupt identified by the specified channel.
## `sel4cp_message sel4cp_msginfo_new(uint64_t label, uint16_t count)`
Creates a new message structure.
The message can be passed to `sel4cp_ppcall` or returned from `protected`.
## `uint64_t sel4cp_msginfo_get_label(sel4cp_message message)`
Returns the label from a message.
## `uint64_t sel4cp_mr_get(uint8_t mr)`
Get a message register.
## `void sel4cp_mr_set(uint8_t mr, uint64_t)`
Set a message register.
# System Description Format {#sysdesc}
This section describes the format of the system description file.
This file is provided as the input to the `sel4cp` tool.
The system description file is an XML file.
The root element of the XML file is `system`.
Within the `system` root element the following child elements are supported:
* `protection_domain`
* `memory_region`
* `channel`
## `protection_domain`
The `protection_domain` element describes a protection domain.
It supports the following attributes:
* `name`: a unique name for the protection domain
* `pp`: (optional) indicates that the protection domain has a protected procedure; defaults to false.
* `priority`: the priority of the protection domain (integer 0 to 254).
* `budget`: (optional) the PD's budget in microseconds; defaults to 1,000.
* `period`: (optional) the PD's period in microseconds; must not be smaller than the budget; defaults to the budget.
Additionally, it supports the following child elements:
* `program_image`: (exactly one) describes the program image for the protection domain.
* `map`: (zero or more) describes mapping of memory regions into the protection domain.
* `irq`: (zero or more) describes hardware interrupt associations.
* `setvar`: (zero or more) describes variable rewriting.
The `program_image` element has a single `path` attribute describing the path to an ELF file.
The `map` element has the following attributes:
* `mr`: Identifies the memory region to map.
* `vaddr`: Identifies the virtual address at which to map the memory region.
* `perms`: Identifies the permissions with which to map the memory region. Can be a combination of `r` (read), `w` (write), and `x` (eXecute).
* `cached`: Determines if mapped with caching enabled or disabled. Defaults to `true`.
* `setvar_vaddr`: Specifies a symbol in the program image. This symbol will be rewritten with the virtual address of the memory region.
The `irq` element has the following attributes:
* `irq`: The hardware interrupt number.
* `id`: The channel identifier.
The `setvar` element has the following attributes:
* `symbol`: Name of a symbol in the ELF file.
* `region_paddr`: Name of an MR. The symbol's value shall be updated to this MRs physical address.
## `memory_region`
The `memory_region` element describes a memory region.
It supports the following attributes:
* `name`: a unique name for the memory region
* `size`: size of the memory region in bytes (must be a multiple of the page size)
* `page_size`: (optional) size of the pages used in the memory region; must be a supported page size if provided.
* `phys_addr`: (optional) the physical address for the start of the memory region.
The `memory_region` element does not support any child elements.
## `channel`
The `channel` element has exactly two `end` children elements for specifying the two PDs associated with the channel.
The `end` element has the following attributes:
* `pd`: Name of the protection domain for this end.
* `id`: Channel identifier in the context of the named protection domain.
The `id` is passed to the PD in the `notified` and `protected` entry points.
The `id` should be passed to the `sel4cp_notify` and `sel4cp_ppcall` functions.
# Board Support Packages {#bsps}
This chapter describes the board support packages that are available in the SDK.
## TQMa8XQP 1GB
The TQMa8XQP is a system-on-module designed by TQ-Systems GmbH.
The modules incorporates an NXP i.MX8X Quad Plus system-on-chip and 1GiB ECC memory.
TQ-Systems provide the MBa8Xx carrier board for development purposes.
The instructions provided assume the use of the MBa8Xx carrier board.
If you are using a different carrier board please refer to the appropriate documentation.
The MBa8Xx provides access to the TQMa8XQP UART via UART-USB bridge.
To access the UART connect a USB micro cable to port **X13**.
The UART-USB bridge supports 4 individual UARTs; the UART is connected to the 2nd port.
By default the SoM will autoboot using U-boot.
Hit any key during the boot process to stop the autoboot.
A new board will autoboot to Linux.
You will likely want to disable autoboot:
=> env set bootdelay -1
=> env save
The board can be reset by pressing switch **S4** (located next to the Ethernet port).
Alternatively, you can use the `reset` command from the U-Boot prompt.
During development the most convenient way to boot an sel4cp image is via network booting.
U-boot support booting via the *tftp* protocol.
To support this you'll want to configure the network.
U-Boot supports DHCP, however it is often more reliable to explicitly set an IP address.
For example:
=> env set ipaddr 10.1.1.2
=> env set netmask 255.255.255.0
=> env set serverip 10.1.1.1
=> env save
To use tftp you also need to set the file to load and the memory address to load it to:
=> env set bootfile loader.img
=> env set loadaddr 0x80280000
=> env save
The system image generated by the sel4cp tool is a raw binary file.
An example sequence of commands for booting is:
=> tftpboot
=> dcache flush
=> icache flush
=> go ${loadaddr}
Rather than typing these each time you can create a U-Boot script:
=> env set sel4cp 'tftpboot; dcache flush; icache flush; go ${loadaddr}'
=> env save
=> run sel4cp
When debugging is enabled the kernel will use the same UART as U-Boot.
# Rationale
This section describes the rationales driving the sel4cp design choices.
## Overview
The seL4 microkernel provides a set of powerful and flexible mechanisms that can be used for building almost arbitrary systems.
While minimising constraints on the nature of system designs and scope of deployments, this flexibility makes it challenging to design the best system for a particular use case, requiring extensive seL4 experience from developers.
The seL4 Core Platform addresses this challenge by constraining the
system architecture to one that provides enough features and power for
its target usage class (IoT, cyberphysical and other embedded systems
with a static architecture), enabling a much simpler set of developer-visible abstractions.
## Protection Domains
PDs are single-threaded to keep the programming model and implementations simple, and because this serves the needs of most present use cases in the target domains.
Extending the model to multithreaded applications (clients) is straightforward and can be done if needed.
Extending to multithreaded services is possible but requires additional infrastructure for which we see no need in the near future.
## Protected Procedure Priorities
The restriction of only calling to higher priority prevents deadlocks and reflects the notion that the callee operates on behalf of the caller, and it should not be possible to preempt execution of the callee unless the caller could be preempted as well.
This greatly simplifies reasoning about real-time properties in the system; in particular, it means that PPs can be used to implement *resource servers*, where shared resources are encapsulated in a component that ensures mutual exclusion, while avoiding unbounded priority inversions through the *immediate priority ceiling protocol*.
While it would be possible to achieve the same by allowing PPs between PDs of the same priority, this would be much harder to statically analyse for loop-freedom (and thus deadlock-freedom).
The drawback is that we waste a part of the priority space where a logical entity is split into multiple PDs, eg to separate out a particularly critical component to formally verify it, when the complete entity would be too complex for formal verification.
For the kinds of systems targeted by the seL4 Core Platform, this reduction of the usable priority space is unlikely to cause problems.
## Protected Procedure Argument Size
The limitation on the size of by-value arguments is forced by the (architecture-dependent) limits on the payload size of the underlying seL4 operations, as well as by efficiency considerations.
The protected procedure payload should be considered as analogous to function arguments in the C language; similar limitations exist in the C ABIs (Application Binary Interfaces) of various platforms.
## Limits
The limitation on the number of protection domains in the system is relatively arbitrary.
Based on experience with the system and the types of systems being built it is possible for this to be increased in the future.
The limitation on the number of channels for a protection domain is based on the size of the notification object in seL4.
Changing this to be large than 64 would most likely require changes to seL4.

48
example/tqma8xqp1gb/ethernet/Makefile Normal file
View File

@ -0,0 +1,48 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
ifeq ($(strip $(BUILD_DIR)),)
$(error BUILD_DIR must be specified)
endif
TOOLCHAIN := aarch64-none-elf
CPU := cortex-a35
CC := $(TOOLCHAIN)-gcc
LD := $(TOOLCHAIN)-ld
AS := $(TOOLCHAIN)-as
ETH_OBJS := eth.o
PASS_OBJS := pass.o
GPT_OBJS := gpt.o
BOARD_DIR := $(SEL4CP_SDK)/board/$(SEL4CP_BOARD)/$(SEL4CP_CONFIG)
IMAGES := eth.elf pass.elf gpt.elf
CFLAGS := -mcpu=$(CPU) -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall -Wno-unused-function -Werror -I$(BOARD_DIR)/include
LDFLAGS := -L$(BOARD_DIR)/lib
LIBS := -lsel4cp -Tsel4cp.ld
all: $(BUILD_DIR)/loader.img
$(BUILD_DIR)/%.o: %.c Makefile
$(CC) -c $(CFLAGS) $< -o $@
$(BUILD_DIR)/%.o: %.s Makefile
$(AS) -g3 -mcpu=$(CPU) $< -o $@
$(BUILD_DIR)/eth.elf: $(addprefix $(BUILD_DIR)/, $(ETH_OBJS))
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
$(BUILD_DIR)/pass.elf: $(addprefix $(BUILD_DIR)/, $(PASS_OBJS))
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
$(BUILD_DIR)/gpt.elf: $(addprefix $(BUILD_DIR)/, $(GPT_OBJS))
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
$(BUILD_DIR)/loader.img: $(addprefix $(BUILD_DIR)/, $(IMAGES)) ethernet.system
$(SEL4CP_SDK)/bin/sel4cp ethernet.system --search-path $(BUILD_DIR) --board $(SEL4CP_BOARD) --config $(SEL4CP_CONFIG) -o $@

1077
example/tqma8xqp1gb/ethernet/eth.c Normal file
View File

File diff suppressed because it is too large Load Diff

122
example/tqma8xqp1gb/ethernet/ethernet.system Normal file
View File

@ -0,0 +1,122 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="eth_outer_output" size="0x200_000" page_size="0x200_000" />
<memory_region name="eth_outer_input" size="0x200_000" page_size="0x200_000" />
<memory_region name="eth_inner_output" size="0x200_000" page_size="0x200_000" />
<memory_region name="eth_inner_input" size="0x200_000" page_size="0x200_000" />
<memory_region name="paddinga" size="0x2_000"/>
<memory_region name="ring_buffer_inner" size="0x1_000" />
<memory_region name="paddingb" size="0x2_000"/>
<memory_region name="ring_buffer_outer" size="0x1000" />
<memory_region name="packet_buffer_inner" size="0x200_000" page_size="0x200_000" />
<memory_region name="packet_buffer_outer" size="0x200_000" page_size="0x200_000" />
<!-- There are 11 GPTs in total.
6 GPTs are in the AMDA subsyste, and there are another 5 GPTs in the
LSIO subsystem.
It is likely that a dedicated GPT can be mapped directly where required, however
to demonstrate sharing a GPT, we use GPT0 in a GPT sharing protection domain.
-->
<memory_region name="lsio_gpt0_clk" size="0x1_000" phys_addr="0x5d540000" />
<memory_region name="lsio_gpt1_clk" size="0x1_000" phys_addr="0x5d550000" />
<memory_region name="lsio_gpt2_clk" size="0x1_000" phys_addr="0x5d560000" />
<memory_region name="lsio_gpt3_clk" size="0x1_000" phys_addr="0x5d570000" />
<memory_region name="lsio_gpt4_clk" size="0x1_000" phys_addr="0x5d580000" />
<memory_region name="lsio_gpt0" size="0x1_000" phys_addr="0x5d140000" />
<memory_region name="lsio_gpt1" size="0x1_000" phys_addr="0x5d150000" />
<memory_region name="lsio_gpt2" size="0x1_000" phys_addr="0x5d160000" />
<memory_region name="lsio_gpt3" size="0x1_000" phys_addr="0x5d170000" />
<memory_region name="lsio_gpt4" size="0x1_000" phys_addr="0x5d180000" />
<memory_region name="eth0" size="0x10_000" phys_addr="0x5b040000" />
<memory_region name="eth1" size="0x10_000" phys_addr="0x5b050000" />
<memory_region name="eth_clk" size="0x1_000" phys_addr="0x5b200000" />
<protection_domain name="gpt" priority="254" pp="true">
<program_image path="gpt.elf" />
<map mr="lsio_gpt0" vaddr="0x2_000_000" perms="rw" cached="false" setvar_vaddr="gpt_regs" />
<map mr="lsio_gpt0_clk" vaddr="0x2_200_000" perms="rw" cached="false" setvar_vaddr="gpt_regs_clk" />
<irq irq="112" id="3" />
</protection_domain>
<protection_domain name="eth_outer" priority="99" budget="1_000" period="100_000">
<program_image path="eth.elf" />
<map mr="ring_buffer_outer" vaddr="0x3_000_000" perms="rw" cached="false" setvar_vaddr="ring_buffer_vaddr" />
<map mr="packet_buffer_outer" vaddr="0x2_400_000" perms="rw" cached="true" setvar_vaddr="packet_buffer_vaddr" />
<map mr="eth0" vaddr="0x2_000_000" perms="rw" cached="false"/>
<map mr="eth_clk" vaddr="0x2_200_000" perms="rw" cached="false"/>
<map mr="eth_outer_output" vaddr="0x3_600_000" perms="rw" setvar_vaddr="output_buffer_vaddr" />
<map mr="eth_outer_input" vaddr="0x3_a00_000" perms="rw" setvar_vaddr="input_buffer_vaddr" />
<irq irq="290" id="3" /> <!-- ethernet interrupt -->
<setvar symbol="ring_buffer_paddr" region_paddr="ring_buffer_outer" />
<setvar symbol="packet_buffer_paddr" region_paddr="packet_buffer_outer" />
</protection_domain>
<protection_domain name="eth_inner" priority="99">
<program_image path="eth.elf" />
<map mr="ring_buffer_inner" vaddr="0x3000000" perms="rw" cached="false" setvar_vaddr="ring_buffer_vaddr" />
<map mr="packet_buffer_inner" vaddr="0x2400000" perms="rw" cached="true" setvar_vaddr="packet_buffer_vaddr" />
<map mr="eth1" vaddr="0x2000000" perms="rw" cached="false" />
<map mr="eth_clk" vaddr="0x2200000" perms="rw" cached="false" />
<map mr="eth_inner_output" vaddr="0x3600000" perms="rw" setvar_vaddr="output_buffer_vaddr" />
<map mr="eth_inner_input" vaddr="0x3a00000" perms="rw" setvar_vaddr="input_buffer_vaddr" />
<irq irq="294" id="3" />
<setvar symbol="ring_buffer_paddr" region_paddr="ring_buffer_inner" />
<setvar symbol="packet_buffer_paddr" region_paddr="packet_buffer_inner" />
</protection_domain>
<protection_domain name="pass" priority="100">
<program_image path="pass.elf" />
<map mr="eth_outer_output" vaddr="0x2000000" perms="rw" setvar_vaddr="outer_input_vaddr" />
<map mr="eth_outer_input" vaddr="0x2400000" perms="rw" setvar_vaddr="outer_output_vaddr"/>
<map mr="eth_inner_output" vaddr="0x2800000" perms="rw" setvar_vaddr="inner_input_vaddr"/>
<map mr="eth_inner_input" vaddr="0x2c00000" perms="rw" setvar_vaddr="inner_output_vaddr"/>
</protection_domain>
<channel>
<end pd="gpt" id="1" />
<end pd="pass" id="0" />
</channel>
<channel>
<end pd="eth_outer" id="1" />
<end pd="pass" id="1" />
</channel>
<channel>
<end pd="eth_outer" id="2" />
<end pd="pass" id="2" />
</channel>
<channel>
<end pd="eth_inner" id="1" />
<end pd="pass" id="3" />
</channel>
<channel>
<end pd="eth_inner" id="2" />
<end pd="pass" id="4" />
</channel>
</system>

42
example/tqma8xqp1gb/ethernet/foo.c Normal file
View File

@ -0,0 +1,42 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <sel4cp.h>
#define ECHO_CH 2
volatile uint64_t *shared_counter = (uint64_t *)(uintptr_t)0x1800000;
void
init(void)
{
sel4cp_dbg_puts("foo: foo protection domain init function running\n");
sel4cp_dbg_puts("foo: sending a notification\n");
*shared_counter = 0x37;
sel4cp_notify(ECHO_CH);
sel4cp_dbg_puts("foo: sent a notification\n");
}
void
notified(sel4cp_channel ch)
{
switch (ch) {
case ECHO_CH:
sel4cp_dbg_puts("foo: received notification on echo channel\n");
if (*shared_counter == 0x38) {
sel4cp_dbg_puts("foo: counter is expected value\n");
} else {
sel4cp_dbg_puts("foo: counter is unexpected value\n");
}
break;
default:
sel4cp_dbg_puts("foo: received notification on unexpected channel\n");
break;
/* ignore any other channels */
}
}

206
example/tqma8xqp1gb/ethernet/gpt.c Normal file
View File

@ -0,0 +1,206 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdbool.h>
#include <stdint.h>
#include <sel4cp.h>
#define IRQ_CH 3
uintptr_t gpt_regs;
uintptr_t gpt_regs_clk;
static volatile uint32_t *gpt;
static volatile uint32_t *lpcg;
static uint64_t timeouts[SEL4CP_MAX_CHANNELS];
static sel4cp_channel active_channel = -1;
static bool timeout_active;
static uint64_t current_timeout;
static uint32_t overflow_count;
static uint8_t pending_timeouts;
#define CR 0
#define PR 1
#define SR 2
#define IR 3
#define OCR1 4
#define OCR2 5
#define OCR3 6
#define ICR1 7
#define ICR2 8
#define CNT 9
static char
hexchar(unsigned int v)
{
return v < 10 ? '0' + v : ('a' - 10) + v;
}
static void
puthex32(uint32_t x)
{
char buffer[11];
buffer[0] = '0';
buffer[1] = 'x';
buffer[2] = hexchar((x >> 28) & 0xf);
buffer[3] = hexchar((x >> 24) & 0xf);
buffer[4] = hexchar((x >> 20) & 0xf);
buffer[5] = hexchar((x >> 16) & 0xf);
buffer[6] = hexchar((x >> 12) & 0xf);
buffer[7] = hexchar((x >> 8) & 0xf);
buffer[8] = hexchar((x >> 4) & 0xf);
buffer[9] = hexchar(x & 0xf);
buffer[10] = 0;
sel4cp_dbg_puts(buffer);
}
void
init(void)
{
sel4cp_dbg_puts(sel4cp_name);
sel4cp_dbg_puts(": gpt PD init function running\n");
gpt = (volatile uint32_t *) gpt_regs;
lpcg = (volatile uint32_t *) gpt_regs_clk;
sel4cp_dbg_puts("LPCG: ");
puthex32(lpcg[0]);
sel4cp_dbg_puts("\n");
uint32_t cr = (
(1 << 9) | // Free run mode
(1 << 6) | // Peripheral clocks
(1) // Enable
);
gpt[CR] = cr;
gpt[IR] = (
(1 << 5) // rollover interrupt
);
sel4cp_dbg_puts("CR: ");
puthex32(gpt[0]);
sel4cp_dbg_puts("\n");
sel4cp_dbg_puts("PR: ");
puthex32(gpt[1]);
sel4cp_dbg_puts("\n");
}
void
notified(sel4cp_channel ch)
{
switch (ch) {
case IRQ_CH: {
uint32_t sr = gpt[SR];
gpt[SR] = sr;
sel4cp_irq_ack(ch);
if (sr & (1 << 5)) {
overflow_count++;
/* FIXME: set the next timeout if required */
}
if (sr & 1) {
gpt[IR] &= ~1;
timeout_active = false;
sel4cp_channel sel4cp_current_channel = active_channel;
timeouts[sel4cp_current_channel] = 0;
/* FIXME: set the next timeout if any are available */
#if 0
sel4cp_dbg_puts("GPT: irq sr=");
puthex32(sr);
sel4cp_dbg_puts(" cnt=");
puthex32(gpt[0x24 / 4]);
sel4cp_dbg_puts("\n");
#endif
sel4cp_notify(sel4cp_current_channel);
}
if (pending_timeouts && !timeout_active) {
/* find next timeout */
uint64_t next_timeout = UINT64_MAX;
sel4cp_channel ch = -1;
for (unsigned i = 0; i < SEL4CP_MAX_CHANNELS; i++) {
if (timeouts[i] != 0 && timeouts[i] < next_timeout) {
next_timeout = timeouts[i];
ch = i;
}
}
/* FIXME: Is there a race here? -- Probably! Fix it later. */
if (ch != -1 && overflow_count == (next_timeout >> 32)) {
pending_timeouts--;
gpt[OCR1] = next_timeout;
gpt[IR] |= 1;
timeout_active = true;
current_timeout = next_timeout;
active_channel = ch;
}
}
break;
}
default:
sel4cp_dbg_puts("gpt: received notification on unexpected channel\n");
break;
}
}
static uint64_t get_ticks(void) {
/* FIXME: If an overflow interrupt happens in the middle here we are in trouble */
uint64_t overflow = overflow_count;
uint32_t sr1 = gpt[SR];
uint32_t cnt = gpt[CNT];
uint32_t sr2 = gpt[SR];
if ((sr2 & (1 << 5)) && (!(sr1 & (1 << 5)))) {
/* rolled-over during - 64-bit time must be the overflow */
cnt = gpt[CNT];
overflow++;
}
return (overflow << 32) | cnt;
}
seL4_MessageInfo_t
protected(sel4cp_channel ch, sel4cp_msginfo msginfo)
{
switch (sel4cp_msginfo_get_label(msginfo)) {
case 0:
seL4_SetMR(0, get_ticks());
return sel4cp_msginfo_new(0, 1);
case 1: {
/* FIXME: There is a race here, if there are higher priority
* protection domains it is possible arbitrary amount of time
* could elapse between any of these instructions. The code
* should be made robust against such a possibility.
*/
uint64_t rel_timeout = seL4_GetMR(0);
uint64_t cur_ticks = get_ticks();
uint64_t abs_timeout = cur_ticks + rel_timeout;
timeouts[ch] = abs_timeout;
if ((!timeout_active || abs_timeout < current_timeout) && (cur_ticks >> 32 == abs_timeout >> 32)) {
if (timeout_active) {
/* there current timeout is now treated as pending */
pending_timeouts++;
}
gpt[OCR1] = abs_timeout;
gpt[IR] |= 1;
timeout_active = true;
current_timeout = abs_timeout;
active_channel = ch;
} else {
pending_timeouts++;
}
#if 0
sel4cp_dbg_puts("GPT: set timeout ch = ");
puthex32(ch);
sel4cp_dbg_puts(" - " );
puthex32(timeout);
sel4cp_dbg_puts("\n");
#endif
return sel4cp_msginfo_new(0, 1);
}
}
return sel4cp_msginfo_new(0, 0);
}

284
example/tqma8xqp1gb/ethernet/pass.c Normal file
View File

@ -0,0 +1,284 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <sel4cp.h>
#define GPT_CH 0
#define OUTER_INPUT_CH 1
#define OUTER_OUTPUT_CH 2
#define INNER_INPUT_CH 3
#define INNER_OUTPUT_CH 4
#define BUFFER_SIZE (2 * 1024)
#define DATA_OFFSET 64
#define OUTER_INPUT outer_input_vaddr
#define OUTER_OUTPUT outer_output_vaddr
#define INNER_INPUT inner_input_vaddr
#define INNER_OUTPUT inner_output_vaddr
#define BUFFER_MAX 1024
unsigned outer_input_index = 0;
unsigned inner_input_index = 0;
unsigned outer_output_index = 0;
unsigned inner_output_index = 0;
uintptr_t outer_input_vaddr;
uintptr_t outer_output_vaddr;
uintptr_t inner_input_vaddr;
uintptr_t inner_output_vaddr;
struct buffer_descriptor {
uint16_t data_length;
uint16_t flags;
};
volatile uint64_t *shared_counter = (uint64_t *)(uintptr_t)0x1800000;
static char
hexchar(unsigned int v)
{
return v < 10 ? '0' + v : ('a' - 10) + v;
}
static void
puthex16(uint16_t x)
{
char buffer[7];
buffer[0] = '0';
buffer[1] = 'x';
buffer[2] = hexchar((x >> 12) & 0xf);
buffer[3] = hexchar((x >> 8) & 0xf);
buffer[4] = hexchar((x >> 4) & 0xf);
buffer[5] = hexchar(x & 0xf);
buffer[6] = 0;
sel4cp_dbg_puts(buffer);
}
static void
puthex32(uint32_t x)
{
char buffer[11];
buffer[0] = '0';
buffer[1] = 'x';
buffer[2] = hexchar((x >> 28) & 0xf);
buffer[3] = hexchar((x >> 24) & 0xf);
buffer[4] = hexchar((x >> 20) & 0xf);
buffer[5] = hexchar((x >> 16) & 0xf);
buffer[6] = hexchar((x >> 12) & 0xf);
buffer[7] = hexchar((x >> 8) & 0xf);
buffer[8] = hexchar((x >> 4) & 0xf);
buffer[9] = hexchar(x & 0xf);
buffer[10] = 0;
sel4cp_dbg_puts(buffer);
}
static void
puthex64(uint64_t x)
{
char buffer[19];
buffer[0] = '0';
buffer[1] = 'x';
buffer[2] = hexchar((x >> 60) & 0xf);
buffer[3] = hexchar((x >> 56) & 0xf);
buffer[4] = hexchar((x >> 52) & 0xf);
buffer[5] = hexchar((x >> 48) & 0xf);
buffer[6] = hexchar((x >> 44) & 0xf);
buffer[7] = hexchar((x >> 40) & 0xf);
buffer[8] = hexchar((x >> 36) & 0xf);
buffer[9] = hexchar((x >> 32) & 0xf);
buffer[10] = hexchar((x >> 28) & 0xf);
buffer[11] = hexchar((x >> 24) & 0xf);
buffer[12] = hexchar((x >> 20) & 0xf);
buffer[13] = hexchar((x >> 16) & 0xf);
buffer[14] = hexchar((x >> 12) & 0xf);
buffer[15] = hexchar((x >> 8) & 0xf);
buffer[16] = hexchar((x >> 4) & 0xf);
buffer[17] = hexchar(x & 0xf);
buffer[18] = 0;
sel4cp_dbg_puts(buffer);
}
static void
mycpy(volatile void *dst, volatile void *src, unsigned int length)
{
volatile uint64_t *d = dst;
volatile uint64_t *s = src;
int i = 0;
int l = length / 64;
if (length % 64) {
l++;
}
while (l) {
d[i] = s[i];
d[i + 1] = s[i + 1];
d[i + 2] = s[i + 2];
d[i + 3] = s[i + 3];
d[i + 4] = s[i + 4];
d[i + 5] = s[i + 5];
d[i + 6] = s[i + 6];
d[i + 7] = s[i + 7];
l--;
i += 8;
}
}
static void
dump_hex(const uint8_t *d, unsigned int length)
{
unsigned int i = 0;
while (length) {
puthex16(i);
sel4cp_dbg_puts(": ");
while (length) {
sel4cp_dbg_putc(hexchar((d[i] >> 4) & 0xf));
sel4cp_dbg_putc(hexchar(d[i] & 0xf));
length--;
i++;
if (i % 16 == 0) {
sel4cp_dbg_putc('\n');
break;
} else {
sel4cp_dbg_putc(' ');
}
}
}
if (i % 16) {
sel4cp_dbg_putc('\n');
}
}
#define GPT_CHANNEL 0
static inline uint64_t
gpt_ticks(void)
{
(void) sel4cp_ppcall(GPT_CHANNEL, sel4cp_msginfo_new(0, 0));
return sel4cp_mr_get(0);
}
static inline void
gpt_timer(uint64_t timeout)
{
sel4cp_mr_set(0, timeout);
(void) sel4cp_ppcall(GPT_CHANNEL, sel4cp_msginfo_new(1, 1));
}
void
init(void)
{
sel4cp_dbg_puts("pass protection domain init function running\n");
/* Example calling a PP */
sel4cp_dbg_puts("ticks: ");
puthex32(gpt_ticks());
sel4cp_dbg_puts("\n");
gpt_timer(0x1000000);
}
void
notified(sel4cp_channel ch)
{
switch (ch) {
case GPT_CH:
sel4cp_dbg_puts("tick! ticks=");
puthex64(gpt_ticks());
sel4cp_dbg_puts("\n");
gpt_timer(0x1000000);
case OUTER_INPUT_CH:
for (;;) {
volatile struct buffer_descriptor *bd = (void *)(uintptr_t)(OUTER_INPUT + (BUFFER_SIZE * outer_input_index));
volatile void *pkt = (void *)(uintptr_t)(OUTER_INPUT + (BUFFER_SIZE * outer_input_index) + DATA_OFFSET);
if (bd->flags == 0) {
break;
}
outer_input_index++;
if (outer_input_index == BUFFER_MAX) {
outer_input_index = 0;
}
volatile struct buffer_descriptor *obd = (void *)(uintptr_t)(INNER_OUTPUT + (BUFFER_SIZE * inner_output_index));
volatile void *opkt = (void *)(uintptr_t)(INNER_OUTPUT + (BUFFER_SIZE * inner_output_index) + DATA_OFFSET);
if (obd->flags == 1) {
sel4cp_dbg_puts("PASS: outer can't pass buffer (no space for inner)\n");
} else {
obd->data_length = bd->data_length;
mycpy(opkt, pkt, bd->data_length);
obd->flags = 1;
sel4cp_notify(INNER_OUTPUT_CH);
inner_output_index++;
if (inner_output_index == BUFFER_MAX) {
inner_output_index = 0;
}
}
bd->flags = 0;
}
break;
case OUTER_OUTPUT_CH:
sel4cp_dbg_puts("outer output\n");
break;
case INNER_INPUT_CH:
for (;;) {
volatile struct buffer_descriptor *bd = (void *)(uintptr_t)(INNER_INPUT + (BUFFER_SIZE * inner_input_index));
volatile void *pkt = (void *)(uintptr_t)(INNER_INPUT + (BUFFER_SIZE * inner_input_index) + DATA_OFFSET);
if (bd->flags == 0) {
break;
}
inner_input_index++;
if (inner_input_index == BUFFER_MAX) {
inner_input_index = 0;
}
volatile struct buffer_descriptor *obd = (void *)(uintptr_t)(OUTER_OUTPUT + (BUFFER_SIZE * outer_output_index));
volatile void *opkt = (void *)(uintptr_t)(OUTER_OUTPUT + (BUFFER_SIZE * outer_output_index) + DATA_OFFSET);
if (obd->flags == 1) {
sel4cp_dbg_puts("PASS: inner can't pass buffer (no space for outer)\n");
} else {
obd->data_length = bd->data_length;
mycpy(opkt, pkt, bd->data_length);
obd->flags = 1;
sel4cp_notify(OUTER_OUTPUT_CH);
outer_output_index++;
if (outer_output_index == BUFFER_MAX) {
outer_output_index = 0;
}
}
bd->flags = 0;
}
break;
case INNER_OUTPUT_CH:
sel4cp_dbg_puts("inner output\n");
break;
default:
sel4cp_dbg_puts("foo: received notification on unexpected channel\n");
break;
/* ignore any other channels */
}
}

2026
example/tqma8xqp1gb/ethernet/report.txt Normal file
View File

File diff suppressed because it is too large Load Diff

35
libsel4cp/Makefile Normal file
View File

@ -0,0 +1,35 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
ifeq ($(strip $(BUILD_DIR)),)
$(error BUILD_DIR must be specified)
endif
ifeq ($(strip $(GCC_CPU)),)
$(error GCC_CPU must be specified)
endif
TOOLCHAIN := aarch64-none-elf-
CFLAGS := -std=gnu11 -g3 -O3 -nostdlib -ffreestanding -mcpu=$(GCC_CPU) -Wall -Wno-maybe-uninitialized -Wno-unused-function -Werror -Iinclude -I$(SEL4_SDK)/include
LIBS := libsel4cp.a
OBJS := main.o dbg.o
OTHER_OBJS := crt0.o
$(BUILD_DIR)/%.o : src/%.S
$(TOOLCHAIN)gcc -x assembler-with-cpp -c -g3 -mcpu=$(GCC_CPU) $< -o $@
$(BUILD_DIR)/%.o : src/%.s
$(TOOLCHAIN)as -g3 -mcpu=$(GCC_CPU) $< -o $@
$(BUILD_DIR)/%.o : src/%.c
$(TOOLCHAIN)gcc -c $(CFLAGS) $< -o $@
LIB = $(addprefix $(BUILD_DIR)/, $(LIBS))
all: $(LIB) $(addprefix $(BUILD_DIR)/, $(OTHER_OBJS))
$(LIB): $(addprefix $(BUILD_DIR)/, $(OBJS))
$(TOOLCHAIN)ar -rv $@ $^

81
libsel4cp/include/sel4cp.h Normal file
View File

@ -0,0 +1,81 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/* seL4 Core Platform interface */
#pragma once
#include <stdint.h>
#define __thread
#include <sel4/sel4.h>
typedef unsigned int sel4cp_channel;
typedef seL4_MessageInfo_t sel4cp_msginfo;
#define BASE_OUTPUT_NOTIFICATION_CAP 10
#define BASE_ENDPOINT_CAP 74
#define BASE_IRQ_CAP 138
#define SEL4CP_MAX_CHANNELS 63
/* User provided functions */
void init(void);
void notified(sel4cp_channel ch);
sel4cp_msginfo protected(sel4cp_channel ch, sel4cp_msginfo msginfo);
extern char sel4cp_name[16];
/*
* Output a single character on the debug console.
*/
void sel4cp_dbg_putc(int c);
/*
* Output a NUL terminated string to the debug console.
*/
void sel4cp_dbg_puts(const char *s);
static inline void
sel4cp_notify(sel4cp_channel ch)
{
seL4_Signal(BASE_OUTPUT_NOTIFICATION_CAP + ch);
}
static inline void
sel4cp_irq_ack(sel4cp_channel ch)
{
seL4_IRQHandler_Ack(BASE_IRQ_CAP + ch);
}
static inline sel4cp_msginfo
sel4cp_ppcall(sel4cp_channel ch, sel4cp_msginfo msginfo)
{
return seL4_Call(BASE_ENDPOINT_CAP + ch, msginfo);
}
static inline sel4cp_msginfo
sel4cp_msginfo_new(uint64_t label, uint16_t count)
{
return seL4_MessageInfo_new(label, 0, 0, count);
}
static inline uint64_t
sel4cp_msginfo_get_label(sel4cp_msginfo msginfo)
{
return seL4_MessageInfo_get_label(msginfo);
}
static void
sel4cp_mr_set(uint8_t mr, uint64_t value)
{
seL4_SetMR(mr, value);
}
static uint64_t
sel4cp_mr_get(uint8_t mr)
{
return seL4_GetMR(mr);
}

61
libsel4cp/sel4cp.ld Normal file
View File

@ -0,0 +1,61 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
PHDRS
{
text PT_LOAD;
data PT_LOAD;
}
ENTRY(_start);
STARTUP(crt0.o);
SECTIONS
{
. = 0x200000;
.text :
{
_text = .;
*(.text.start)
*(.text*)
*(.rodata)
_text_end = .;
} :text
. = ALIGN(0x1000);
/* For some reason the ABI puts init array
* into writable memory, so we have to follow suit */
.init_array :
{
PROVIDE(__init_array_start = .);
KEEP (*(SORT(.init_array.*)))
KEEP (*(.init_array*))
PROVIDE(__init_array_end = .);
} :data
.data :
{
_data = .;
*(.data)
_data_end = .;
} :data
.bss :
{
_bss = .;
*(.bss)
*(COMMON)
. = ALIGN(4);
_bss_end = .;
} :data
. = ALIGN(0x1000);
.ipc_buffer (NOLOAD): {
__sel4_ipc_buffer_obj = .;
}
}

15
libsel4cp/src/crt0.s Normal file
View File

@ -0,0 +1,15 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
.extern main
.section ".text.start"
.global _start;
.type _start, %function;
_start:
ldr x1, =_stack + 0xff0
mov sp, x1
b main

41
libsel4cp/src/dbg.c Normal file
View File

@ -0,0 +1,41 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <sel4cp.h>
#define __thread
#include <sel4/sel4.h>
void
sel4cp_dbg_putc(int c)
{
#if defined(CONFIG_DEBUG_BUILD)
seL4_DebugPutChar(c);
#endif
}
void
sel4cp_dbg_puts(const char *s)
{
while (*s) {
sel4cp_dbg_putc(*s);
s++;
}
}
void
__assert_fail(const char *str, const char *file, int line, const char *function)
{
sel4cp_dbg_puts("assert failed: ");
sel4cp_dbg_puts(str);
sel4cp_dbg_puts(" ");
sel4cp_dbg_puts(file);
sel4cp_dbg_puts(" ");
sel4cp_dbg_puts(function);
sel4cp_dbg_puts("\n");
}

86
libsel4cp/src/main.c Normal file
View File

@ -0,0 +1,86 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdbool.h>
#include <stddef.h>
#include <stdint.h>
#define __thread
#include <sel4/sel4.h>
#include <sel4cp.h>
#define INPUT_CAP 1
#define REPLY_CAP 4
#define NOTIFICATION_BITS 57
char _stack[4096] __attribute__((__aligned__(16)));
char sel4cp_name[16];
extern seL4_IPCBuffer __sel4_ipc_buffer_obj;
seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj;
extern const void (*const __init_array_start []) (void);
extern const void (*const __init_array_end []) (void);
__attribute__((weak)) sel4cp_msginfo protected(sel4cp_channel ch, sel4cp_msginfo msginfo)
{
return seL4_MessageInfo_new(0, 0, 0, 0);
}
static void
run_init_funcs(void)
{
size_t count = __init_array_end - __init_array_start;
for (size_t i = 0; i < count; i++) {
__init_array_start[i]();
}
}
static void
handler_loop(void)
{
bool have_reply = false;
seL4_MessageInfo_t reply_tag;
for (;;) {
seL4_Word badge;
seL4_MessageInfo_t tag;
if (have_reply) {
tag = seL4_ReplyRecv(INPUT_CAP, reply_tag, &badge, REPLY_CAP);
} else {
tag = seL4_Recv(INPUT_CAP, &badge, REPLY_CAP);
}
uint64_t is_endpoint = badge >> 63;
if (is_endpoint) {
have_reply = true;
reply_tag = protected(badge & 0x3f, tag);
} else {
unsigned int idx = 0;
have_reply = false;
do {
if (badge & 1) {
notified(idx);
}
badge >>= 1;
idx++;
} while (badge != 0);
}
}
}
void
main(void)
{
run_init_funcs();
init();
handler_loop();
}

35
loader/Makefile Normal file
View File

@ -0,0 +1,35 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
ifeq ($(strip $(BUILD_DIR)),)
$(error BUILD_DIR must be specified)
endif
ifeq ($(strip $(GCC_CPU)),)
$(error GCC_CPU must be specified)
endif
TOOLCHAIN := aarch64-none-elf-
CFLAGS := -std=gnu11 -g3 -O3 -nostdlib -ffreestanding -mcpu=$(GCC_CPU) -Wall -Werror
PROGS := loader.elf
OBJECTS := loader.o crt0.o util64.o
LINKSCRIPT := loader.ld
$(BUILD_DIR)/%.o : src/%.S
$(TOOLCHAIN)gcc -x assembler-with-cpp -c -g3 -mcpu=$(GCC_CPU) $< -o $@
$(BUILD_DIR)/%.o : src/%.s
$(TOOLCHAIN)as -g3 -mcpu=$(GCC_CPU) $< -o $@
$(BUILD_DIR)/%.o : src/%.c
$(TOOLCHAIN)gcc -c $(CFLAGS) $< -o $@
OBJPROG = $(addprefix $(BUILD_DIR)/, $(PROGS))
all: $(OBJPROG)
$(OBJPROG): $(addprefix $(BUILD_DIR)/, $(OBJECTS))
$(TOOLCHAIN)ld -T$(LINKSCRIPT) $^ -o $@

43
loader/loader.ld Normal file
View File

@ -0,0 +1,43 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
PHDRS
{
/* all PT_LOAD AT (0x51fa0000) ; */
/* all PT_LOAD AT (0x80000) ; */
all PT_LOAD AT (0x80280000);
}
SECTIONS
{
/* . = 0x51fa0000; */
/* . = 0x80000; */
. = 0x80280000;
.text :
{
_text = .;
*(.text.start)
*(.text*)
*(.rodata)
_text_end = .;
} :all
.data :
{
_data = .;
*(.data)
_data_end = .;
} :all
.bss :
{
_bss = .;
*(.bss)
*(COMMON)
. = ALIGN(4);
_bss_end = .;
} :all
}

25
loader/src/crt0.s Normal file
View File

@ -0,0 +1,25 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
.extern main
.section ".text.start"
.global _start;
.type _start, %function;
_start:
mrs x0, mpidr_el1
and x0, x0,#0xFF // Check processor id
cbz x0, master // Hang for all non-primary CPU
proc_hang:
wfe
b proc_hang
master:
ldr x1, =_stack + 0xff0
mov sp, x1
b main

449
loader/src/loader.c Normal file
View File

@ -0,0 +1,449 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <strings.h>
_Static_assert(sizeof(uintptr_t) == 8 || sizeof(uintptr_t) == 4, "Expect uintptr_t to be 32-bit or 64-bit");
#if UINTPTR_MAX == 0xffffffffUL
#define WORD_SIZE 32
#else
#define WORD_SIZE 64
#endif
#if WORD_SIZE == 32
#define MAGIC 0x5e14dead
#else
#define MAGIC 0x5e14dead14de5ead
#endif
#define ALIGN(n) __attribute__((__aligned__(n)))
#define MASK(x) ((1U << x) - 1)
#define STACK_SIZE 4096
#define UART_BASE 0x5a070000
#define STAT 0x14
#define TRANSMIT 0x1c
#define STAT_TDRE (1 << 23)
#define UART_REG(x) ((volatile uint32_t *)(UART_BASE + (x)))
#define REGION_TYPE_DATA 1
#define REGION_TYPE_ZERO 2
#define FLAG_SEL4_HYP (1UL << 0)
enum el {
EL0 = 0,
EL1 = 1,
EL2 = 2,
EL3 = 3,
};
struct region {
uintptr_t load_addr;
uintptr_t size;
uintptr_t offset;
uintptr_t type;
};
struct loader_data {
uintptr_t magic;
uintptr_t flags;
uintptr_t kernel_entry;
uintptr_t ui_p_reg_start;
uintptr_t ui_p_reg_end;
uintptr_t pv_offset;
uintptr_t v_entry;
uintptr_t extra_device_addr_p;
uintptr_t extra_device_size;
uintptr_t num_regions;
struct region regions[];
};
typedef void (*sel4_entry)(
uintptr_t ui_p_reg_start,
uintptr_t ui_p_reg_end,
intptr_t pv_offset,
uintptr_t v_entry,
uintptr_t dtb_addr_p,
uintptr_t dtb_size,
uintptr_t extra_device_addr_p,
uintptr_t extra_device_size
);
void switch_to_el1(void);
void el1_mmu_enable(void);
char _stack[STACK_SIZE] ALIGN(16);
/* Paging structures for kernel mapping */
uint64_t boot_lvl0_upper[1 << 9] ALIGN(1 << 12);
uint64_t boot_lvl1_upper[1 << 9] ALIGN(1 << 12);
uint64_t boot_lvl2_upper[1 << 9] ALIGN(1 << 12);
/* Paging structures for identity mapping */
uint64_t boot_lvl0_lower[1 << 9] ALIGN(1 << 12);
uint64_t boot_lvl1_lower[1 << 9] ALIGN(1 << 12);
uintptr_t exception_register_state[32];
extern char _bss_end;
const struct loader_data *loader_data = (void *)&_bss_end;
static void
memcpy(void *dst, const void *src, size_t sz)
{
char *dst_ = dst;
const char *src_ = src;
while (sz-- > 0) {
*dst_++ = *src_++;
}
}
static void
putc(uint8_t ch)
{
while (!(*UART_REG(STAT) & STAT_TDRE)) { }
*UART_REG(TRANSMIT) = ch;
}
static void
puts(const char *s)
{
while (*s) {
putc(*s);
s++;
}
}
static char
hexchar(unsigned int v)
{
return v < 10 ? '0' + v : ('a' - 10) + v;
}
static void
puthex32(uint32_t val)
{
char buffer[8 + 3];
buffer[0] = '0';
buffer[1] = 'x';
buffer[8 + 3 - 1] = 0;
for (unsigned i = 8 + 1; i > 1; i--) {
buffer[i] = hexchar(val & 0xf);
val >>= 4;
}
puts(buffer);
}
static void
puthex64(uint64_t val)
{
char buffer[16 + 3];
buffer[0] = '0';
buffer[1] = 'x';
buffer[16 + 3 - 1] = 0;
for (unsigned i = 16 + 1; i > 1; i--) {
buffer[i] = hexchar(val & 0xf);
val >>= 4;
}
puts(buffer);
}
static void
puthex(uintptr_t val)
{
#if WORD_SIZE == 32
puthex32(val);
#else
puthex64(val);
#endif
}
/* Returns the current execption level */
static enum el
current_el(void)
{
/* See: C5.2.1 CurrentEL */
uint32_t val;
asm volatile("mrs %x0, CurrentEL" : "=r"(val) :: "cc");
/* bottom two bits are res0 */
return (enum el) val >> 2;
}
static char *
el_to_string(enum el el)
{
switch (el) {
case EL0: return "EL0";
case EL1: return "EL1";
case EL2: return "EL2";
case EL3: return "EL3";
}
return "<invalid el>";
}
static char *
ex_to_string(uintptr_t ex)
{
switch (ex) {
case 0: return "Synchronous EL1t";
case 1: return "IRQ EL1t";
case 2: return "FIQ EL1t";
case 3: return "SError EL1t";
case 4: return "Synchronous EL1h";
case 5: return "IRQ EL1h";
case 6: return "FIQ EL1h";
case 7: return "SError EL1h";
case 8: return "Synchronous 64-bit EL0";
case 9: return "IRQ 64-bit EL0";
case 10: return "FIQ 64-bit EL0";
case 11: return "SError 64-bit EL0";
case 12: return "Synchronous 32-bit EL0";
case 13: return "IRQ 32-bit EL0";
case 14: return "FIQ 32-bit EL0";
case 15: return "SError 32-bit EL0";
}
return "<invalid ex>";
}
static char *
ec_to_string(uintptr_t ec)
{
switch (ec) {
case 0: return "Unknown reason";
case 1: return "Trapped WFI or WFE instruction execution";
case 3: return "Trapped MCR or MRC access with (coproc==0b1111) this is not reported using EC 0b000000";
case 4: return "Trapped MCRR or MRRC access with (coproc==0b1111) this is not reported using EC 0b000000";
case 5: return "Trapped MCR or MRC access with (coproc==0b1110)";
case 6: return "Trapped LDC or STC access";
case 7: return "Access to SVC, Advanced SIMD or floating-point functionality trapped";
case 12: return "Trapped MRRC access with (coproc==0b1110)";
case 13: return "Branch Target Exception";
case 17: return "SVC instruction execution in AArch32 state";
case 21: return "SVC instruction execution in AArch64 state";
case 24: return "Trapped MSR, MRS or System instruction exuection in AArch64 state, this is not reported using EC 0xb000000, 0b000001 or 0b000111";
case 25: return "Access to SVE functionality trapped";
case 28: return "Exception from a Pointer Authentication instruction authentication failure";
case 32: return "Instruction Abort from a lower Exception level";
case 33: return "Instruction Abort taken without a change in Exception level";
case 34: return "PC alignment fault exception";
case 36: return "Data Abort from a lower Exception level";
case 37: return "Data Abort taken without a change in Exception level";
case 38: return "SP alignment faultr exception";
case 40: return "Trapped floating-point exception taken from AArch32 state";
case 44: return "Trapped floating-point exception taken from AArch64 state";
case 47: return "SError interrupt";
case 48: return "Breakpoint exception from a lower Exception level";
case 49: return "Breakpoint exception taken without a change in Exception level";
case 50: return "Software Step exception from a lower Exception level";
case 51: return "Software Step exception taken without a change in Exception level";
case 52: return "Watchpoint exception from a lower Exception level";
case 53: return "Watchpoint exception taken without a change in Exception level";
case 56: return "BKPT instruction execution in AArch32 state";
case 60: return "BRK instruction execution in AArch64 state";
}
return "<invalid EC>";
}
/*
* Print out the loader data structure.
*
* This doesn't *do anything*. It helps when
* debugging to verify that the data structures are
* being interpretted correctly by the loader.
*/
static void
print_flags(void)
{
if (loader_data->flags & FLAG_SEL4_HYP) {
puts(" seL4 configured as hypervisor\n");
}
}
static void
print_loader_data(void)
{
puts("INFO: Flags: ");
puthex64(loader_data->flags);
puts("\n");
print_flags();
puts("INFO: Kernel: entry: ");
puthex64(loader_data->kernel_entry);
puts("\n");
puts("INFO: Root server: physmem: ");
puthex64(loader_data->ui_p_reg_start);
puts(" -- ");
puthex64(loader_data->ui_p_reg_end);
puts("\nINFO: virtmem: ");
puthex64(loader_data->ui_p_reg_start - loader_data->pv_offset);
puts(" -- ");
puthex64(loader_data->ui_p_reg_end - loader_data->pv_offset);
puts("\nINFO: entry : ");
puthex64(loader_data->v_entry);
puts("\n");
for (uint32_t i = 0; i < loader_data->num_regions; i++) {
const struct region *r = &loader_data->regions[i];
puts("INFO: region: ");
puthex32(i);
puts(" addr: ");
puthex64(r->load_addr);
puts(" size: ");
puthex64(r->size);
puts(" offset: ");
puthex64(r->offset);
puts(" type: ");
puthex64(r->type);
puts("\n");
}
}
static void
copy_data(void)
{
const void *base = &loader_data->regions[loader_data->num_regions];
for (uint32_t i = 0; i < loader_data->num_regions; i++) {
const struct region *r = &loader_data->regions[i];
puts("INFO: copying region ");
puthex32(i);
puts("\n");
memcpy((void *)(uintptr_t)r->load_addr, base + r->offset, r->size);
}
}
static int
ensure_correct_el(void)
{
enum el el = current_el();
puts("INFO: CurrentEL=");
puts(el_to_string(el));
puts("\n");
if (el == EL0 || el == EL3) {
puts("ERROR: Unsupported initial exception level\n");
return 1;
}
if (loader_data->flags & FLAG_SEL4_HYP) {
if (el != EL2) {
puts("ERROR: seL4 configured as a hypervisor, but not in EL2\n");
}
} else {
if (el == EL2) {
/* seL4 relies on the timer to be set to a useful value */
puts("INFO: Resetting CNTVOFF\n");
asm volatile("msr cntvoff_el2, xzr");
puts("INFO: Dropping from EL2 to EL1\n");
switch_to_el1();
puts("INFO: CurrentEL=");
el = current_el();
puts(el_to_string(el));
puts("\n");
if (el == EL1) {
puts("INFO: Dropped to EL1 successfully\n");
} else {
puts("ERROR: Failed to switch to EL1\n");
return 1;
}
}
}
return 0;
}
static void
start_kernel(void)
{
((sel4_entry)(loader_data->kernel_entry))(
loader_data->ui_p_reg_start,
loader_data->ui_p_reg_end,
loader_data->pv_offset,
loader_data->v_entry,
0,
0,
loader_data->extra_device_addr_p,
loader_data->extra_device_size
);
}
int
main(void)
{
int r;
puts("INFO: altloader for seL4 starting\n");
/* Check that the loader magic number is set correctly */
if (loader_data->magic != MAGIC) {
puts("ERROR: mismatch on loader data structure magic number\n");
return 1;
}
print_loader_data();
/* past here we have trashed u-boot so any errors should go to the
* fail label; it's not possible to return to U-boot
*/
copy_data();
r = ensure_correct_el();
if (r != 0) {
goto fail;
}
puts("INFO: enabling MMU\n");
el1_mmu_enable();
puts("INFO: jumping to kernel\n");
start_kernel();
puts("ERROR: seL4 Loader: Error - KERNEL RETURNED\n");
fail:
/* Note: can't usefully return to U-Boot once we are here. */
/* IMPROVEMENT: use SMC SVC call to try and power-off / reboot system.
* or at least go to a WFI loop
*/
for (;;) {
}
}
void
exception_handler(uintptr_t ex, uintptr_t esr, uintptr_t far)
{
uintptr_t ec = (esr >> 26) & 0x3f;
puts("ERROR: loader trapped kernel exception: ");
puts(ex_to_string(ex));
puts(" ec=");
puts(ec_to_string(ec));
puts("(");
puthex32(ec);
puts(") il=");
puthex((esr >> 25) & 1);
puts(" iss=");
puthex(esr & MASK(24));
puts(" far=");
puthex(far);
puts("\n");
for (unsigned i = 0; i < 32; i++) {
puts("reg: ");
puthex32(i);
puts(": ");
puthex(exception_register_state[i]);
puts("\n");
}
for (;;) {
}
}

350
loader/src/util64.S Normal file
View File

@ -0,0 +1,350 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#define PSR_F_BIT 0x00000040
#define PSR_I_BIT 0x00000080
#define PSR_A_BIT 0x00000100
#define PSR_D_BIT 0x00000200
#define PSR_MODE_EL0t 0x00000000
#define PSR_MODE_EL1t 0x00000004
#define PSR_MODE_EL1h 0x00000005
#define PSR_MODE_EL2t 0x00000008
#define PSR_MODE_EL2h 0x00000009
#define PSR_MODE_SVC_32 0x00000013
#define MT_DEVICE_nGnRnE 0
#define MT_DEVICE_nGnRE 1
#define MT_DEVICE_GRE 2
#define MT_NORMAL_NC 3
#define MT_NORMAL 4
#define MAIR(_attr, _mt) ((_attr) << ((_mt) * 8))
#define TCR_T0SZ(x) ((64 - (x)))
#define TCR_T1SZ(x) ((64 - (x)) << 16)
#define TCR_TxSZ(x) (TCR_T0SZ(x) | TCR_T1SZ(x))
#define TCR_IRGN0_WBWC (1 << 8)
#define TCR_IRGN_NC ((0 << 8) | (0 << 24))
#define TCR_IRGN_WBWA ((1 << 8) | (1 << 24))
#define TCR_IRGN_WT ((2 << 8) | (2 << 24))
#define TCR_IRGN_WBnWA ((3 << 8) | (3 << 24))
#define TCR_IRGN_MASK ((3 << 8) | (3 << 24))
#define TCR_ORGN0_WBWC (1 << 10)
#define TCR_ORGN_NC ((0 << 10) | (0 << 26))
#define TCR_ORGN_WBWA ((1 << 10) | (1 << 26))
#define TCR_ORGN_WT ((2 << 10) | (2 << 26))
#define TCR_ORGN_WBnWA ((3 << 10) | (3 << 26))
#define TCR_ORGN_MASK ((3 << 10) | (3 << 26))
#define TCR_SH0_ISH (3 << 12)
#define TCR_SHARED ((3 << 12) | (3 << 28))
#define TCR_TG0_4K (0 << 14)
#define TCR_TG0_64K (1 << 14)
#define TCR_TG1_4K (2 << 30)
#define TCR_TG1_64K (3 << 30)
#define TCR_PS_4G (0 << 16)
#define TCR_PS_64G (1 << 16)
#define TCR_PS_1T (2 << 16)
#define TCR_PS_4T (3 << 16)
#define TCR_PS_16T (4 << 16)
#define TCR_PS_256T (5 << 16)
#define TCR_ASID16 (1 << 36)
/* Assembler Macros */
.macro dcache op
dsb sy
mrs x0, clidr_el1
and x3, x0, #0x7000000
lsr x3, x3, #23
cbz x3, finished_\op
mov x10, #0
loop1_\op:
add x2, x10, x10, lsr #1
lsr x1, x0, x2
and x1, x1, #7
cmp x1, #2
b.lt skip_\op
msr csselr_el1, x10
isb
mrs x1, ccsidr_el1
and x2, x1, #7
add x2, x2, #4
mov x4, #0x3ff
and x4, x4, x1, lsr #3
clz w5, w4
mov x7, #0x7fff
and x7, x7, x1, lsr #13
loop2_\op:
mov x9, x4
loop3_\op:
lsl x6, x9, x5
orr x11, x10, x6
lsl x6, x7, x2
orr x11, x11, x6
dc \op, x11
subs x9, x9, #1
b.ge loop3_\op
subs x7, x7, #1
b.ge loop2_\op
skip_\op:
add x10, x10, #2
cmp x3, x10
b.gt loop1_\op
finished_\op:
mov x10, #0
msr csselr_el1, x10
dsb sy
isb
.endm
/*
* Disable the MMU.
*
* Arguments:
* system control register for the appropriate exception level
* temporary register
*
* This clears bits 0, 2 and 12 in the control register
* which map to M (MMU disable), C (cache disable) and I (icache disable)
* bits.
*/
.macro disable_mmu sctlr tmp
mrs \tmp, \sctlr
bic \tmp, \tmp, #(1 << 0)
bic \tmp, \tmp, #(1 << 2)
bic \tmp, \tmp, #(1 << 12)
msr \sctlr, \tmp
isb
.endm
/*
* Enable the MMU.
*
* Arguments:
* system control register for the appropriate exception level
* temporary register
*
* This set bits 0, 2 and 12 in the control register
* which map to M (MMU enable), C (cache enable) and I (icache enable)
* bits.
*/
.macro enable_mmu sctlr tmp
mrs \tmp, \sctlr
orr \tmp, \tmp, #(1 << 0)
orr \tmp, \tmp, #(1 << 2)
orr \tmp, \tmp, #(1 << 12)
msr \sctlr, \tmp
isb
.endm
/* Standard function decorators. */
#define BEGIN_FUNC(_name) \
.global _name ; \
.type _name, %function ; \
_name:
#define END_FUNC(_name) \
.size _name, .-_name
/* Invalidate the D-cache */
BEGIN_FUNC(invalidate_dcache)
dcache isw
ret
END_FUNC(invalidate_dcache)
/* Flush the D-cache */
BEGIN_FUNC(flush_dcache)
dcache cisw
ret
END_FUNC(flush_dcache)
/* Invalidate the I-cache */
BEGIN_FUNC(invalidate_icache)
ic iallu
dsb nsh
isb
ret
END_FUNC(invalidate_icache)
/*
* Switch from to running in EL1 (assumes correctly running in EL2).
*/
BEGIN_FUNC(switch_to_el1)
/* push frame pointer and link register to the stack */
stp x29, x30, [sp, #-16]!
mov x29, sp
bl flush_dcache
/* Disable EL2 MMU (stage1) */
disable_mmu sctlr_el2, x9
bl invalidate_icache
/* Set execution state for EL1 to AArch64 -- disable virtualization */
mov x9, #(1 << 31)
msr hcr_el2, x9
/* Disable traps to EL2 */
/* FIXME: This enables the 'TZ' bit, which seems to be against the design */
mov x9, #0x33ff
msr cptr_el2, x9
msr hstr_el2, xzr
/* Since stage 2 addressing is disable, clear the base register */
msr vttbr_el2, xzr
/* Disable EL1 MMU (stage1) */
disable_mmu sctlr_el1 , x9
/* Set SPSR for EL2
* I => interrupts are masked
* F => fast interrupts are masked
* A => SError interrupts are masked
* D => debug exceptions are masked
* MODE_EL1h => return to EL1 on eret (using SP_EL1, not SP_EL0)
*/
mov x9, #(PSR_F_BIT | PSR_I_BIT | PSR_A_BIT | PSR_D_BIT | PSR_MODE_EL1h)
msr spsr_el2, x9
/* The same stack is reused */
ldp x29, x30, [sp], #16
mov x10, sp
msr sp_el1, x10
/* set ELR so that it's possible to perform ERET */
msr elr_el2, x30
eret
END_FUNC(switch_to_el1)
BEGIN_FUNC(el1_mmu_enable)
stp x29, x30, [sp, #-16]!
mov x29, sp
bl flush_dcache
/* Ensure I-cache, D-cache and mmu are disabled for EL1/Stage1 */
disable_mmu sctlr_el1, x8
/*
* Invalidate the local I-cache so that any instructions fetched
* speculatively are discarded.
*/
bl invalidate_icache
/*
* DEVICE_nGnRnE 000 00000000
* DEVICE_nGnRE 001 00000100
* DEVICE_GRE 010 00001100
* NORMAL_NC 011 01000100
* NORMAL 100 11111111
*/
ldr x5, =MAIR(0x00, MT_DEVICE_nGnRnE) | \
MAIR(0x04, MT_DEVICE_nGnRE) | \
MAIR(0x0c, MT_DEVICE_GRE) | \
MAIR(0x44, MT_NORMAL_NC) | \
MAIR(0xff, MT_NORMAL)
msr mair_el1, x5
ldr x10, =TCR_TxSZ(48) | TCR_IRGN_WBWA | TCR_ORGN_WBWA | TCR_TG0_4K | TCR_TG1_4K | TCR_ASID16 /*| TCR_SHARED*/
mrs x9, ID_AA64MMFR0_EL1
bfi x10, x9, #32, #3
msr tcr_el1, x10
/* Setup page tables */
adrp x8, boot_lvl0_lower
msr ttbr0_el1, x8
adrp x8, boot_lvl0_upper
msr ttbr1_el1, x8
isb
/* invalidate all TLB entries for EL1 */
tlbi vmalle1is
dsb ish
isb
enable_mmu sctlr_el1, x8
/* set up a vector table so that if the low-level kernel
* initialization code fails, we have some chance of finding
* out and printing reasonable diagnostics.
*/
adrp x8, arm_vector_table
msr vbar_el1, x8
ldp x29, x30, [sp], #16
ret
END_FUNC(el1_mmu_enable)
.extern exception_handler
.extern exception_register_state
.macro ventry id
.align 7
/* push some temp registers on the stack */
stp x2, x3, [sp, #-16]
adrp x2, exception_register_state
stp x0, x1, [x2]
mov x0, x2
ldp x2, x3, [sp, #-16]
stp x2, x3, [x0, #16 * 1]
stp x4, x5, [x0, #16 * 2]
stp x6, x7, [x0, #16 * 3]
stp x8, x9, [x0, #16 * 4]
stp x10, x11, [x0, #16 * 5]
stp x12, x13, [x0, #16 * 6]
stp x14, x15, [x0, #16 * 7]
stp x16, x17, [x0, #16 * 8]
stp x18, x19, [x0, #16 * 9]
stp x20, x21, [x0, #16 * 10]
stp x22, x23, [x0, #16 * 11]
stp x24, x25, [x0, #16 * 12]
stp x26, x27, [x0, #16 * 13]
stp x28, x29, [x0, #16 * 14]
mov x0, \id
mrs x1, ESR_EL1
mrs x2, FAR_EL1
b exception_handler
.endm
.align 12
BEGIN_FUNC(arm_vector_table)
ventry #0 // Synchronous EL1t
ventry #1 // IRQ EL1t
ventry #2 // FIQ EL1t
ventry #3 // SError EL1t
ventry #4 // Synchronous EL1h
ventry #5 // IRQ EL1h
ventry #6 // FIQ EL1h
ventry #7 // SError EL1h
ventry #8 // Synchronous 64-bit EL0
ventry #9 // IRQ 64-bit EL0
ventry #10 // FIQ 64-bit EL0
ventry #11 // SError 64-bit EL0
ventry #12 // Synchronous 32-bit EL0
ventry #13 // IRQ 32-bit EL0
ventry #14 // FIQ 32-bit EL0
ventry #15 // SError 32-bit EL0
END_FUNC(arm_vector_table)

35
monitor/Makefile Normal file
View File

@ -0,0 +1,35 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
ifeq ($(strip $(BUILD_DIR)),)
$(error BUILD_DIR must be specified)
endif
ifeq ($(strip $(GCC_CPU)),)
$(error GCC_CPU must be specified)
endif
TOOLCHAIN := aarch64-none-elf-
CFLAGS := -std=gnu11 -g3 -O3 -nostdlib -ffreestanding -mcpu=$(GCC_CPU) -Wall -Wno-maybe-uninitialized -Werror -I$(SEL4_SDK)/include
PROGS := monitor.elf
OBJECTS := main.o crt0.o debug.o util.o
LINKSCRIPT := monitor.ld
$(BUILD_DIR)/%.o : src/%.S
$(TOOLCHAIN)gcc -x assembler-with-cpp -c -g3 -mcpu=$(GCC_CPU) $< -o $@
$(BUILD_DIR)/%.o : src/%.s
$(TOOLCHAIN)as -g3 -mcpu=$(GCC_CPU) $< -o $@
$(BUILD_DIR)/%.o : src/%.c
$(TOOLCHAIN)gcc -c $(CFLAGS) $< -o $@
OBJPROG = $(addprefix $(BUILD_DIR)/, $(PROGS))
all: $(OBJPROG)
$(OBJPROG): $(addprefix $(BUILD_DIR)/, $(OBJECTS))
$(TOOLCHAIN)ld -T$(LINKSCRIPT) $^ -o $@

39
monitor/monitor.ld Normal file
View File

@ -0,0 +1,39 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
PHDRS
{
all PT_LOAD AT (0x08a000000);
}
SECTIONS
{
. = 0x08a000000;
.text :
{
_text = .;
*(.text.start)
*(.text*)
*(.rodata)
_text_end = .;
} :all
.data :
{
_data = .;
*(.data)
_data_end = .;
} :all
.bss :
{
_bss = .;
*(.bss)
*(COMMON)
. = ALIGN(4);
_bss_end = .;
} :all
}

15
monitor/src/crt0.s Normal file
View File

@ -0,0 +1,15 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
.extern main
.section ".text.start"
.global _start;
.type _start, %function;
_start:
ldr x1, =_stack + 0xff0
mov sp, x1
b main

156
monitor/src/debug.c Normal file
View File

@ -0,0 +1,156 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#define __thread
#include <sel4/sel4.h>
#include "util.h"
#include "debug.h"
void
dump_bootinfo(seL4_BootInfo *bi)
{
unsigned i;
puts("Bootinfo: ");
puthex64((uintptr_t)bi);
puts("\n");
puts("extraLen = ");
puthex64(bi->extraLen);
puts("\n");
puts("nodeID = ");
puthex64(bi->nodeID);
puts("\n");
puts("numNodes = ");
puthex64(bi->numNodes);
puts("\n");
puts("numIOPTLevels = ");
puthex64(bi->numIOPTLevels);
puts("\n");
puts("ipcBuffer* = ");
puthex64((uintptr_t)bi->ipcBuffer);
puts("\n");
puts("initThreadCNodeSizeBits = ");
puthex64(bi->initThreadCNodeSizeBits);
puts("\n");
puts("initThreadDomain = ");
puthex64(bi->initThreadDomain);
puts("\n");
puts("userImagePaging = ");
puthex64(bi->userImagePaging.start);
puts("..");
puthex64(bi->userImagePaging.end - 1);
puts("\n");
puts("schedcontrol = ");
puthex64(bi->schedcontrol.start);
puts("..");
puthex64(bi->schedcontrol.end - 1);
puts("\n");
puts("userImageFrames = ");
puthex64(bi->userImageFrames.start);
puts("..");
puthex64(bi->userImageFrames.end - 1);
puts("\n");
puts("untyped = ");
puthex64(bi->untyped.start);
puts("..");
puthex64(bi->untyped.end - 1);
puts("\n");
puts("empty = ");
puthex64(bi->empty.start);
puts("..");
puthex64(bi->empty.end - 1);
puts("\n");
puts("sharedFrames = ");
puthex64(bi->sharedFrames.start);
puts("..");
puthex64(bi->sharedFrames.end - 1);
puts("\n");
puts("ioSpaceCaps = ");
puthex64(bi->ioSpaceCaps.start);
puts("..");
puthex64(bi->ioSpaceCaps.end - 1);
puts("\n");
puts("extraBIPages = ");
puthex64(bi->extraBIPages.start);
puts("..");
puthex64(bi->extraBIPages.end - 1);
puts("\n");
#if 1
for (i = 0; i < bi->untyped.end - bi->untyped.start; i++) {
puts("untypedList[");
puthex32(i);
puts("] = slot: ");
puthex32(bi->untyped.start + i);
puts(", paddr: ");
puthex64(bi->untypedList[i].paddr);
puts(" - ");
puthex64(bi->untypedList[i].paddr + (1UL << bi->untypedList[i].sizeBits));
puts(" (");
puts(bi->untypedList[i].isDevice ? "device" : "normal");
puts(") bits: ");
puthex32(bi->untypedList[i].sizeBits);
puts("\n");
}
#endif
/* The extended printing over the individual untypes is good if you care
about the individual objects, but annoying if you want to focus on memory
regions. This coalesces thing before printing to summarize the regions.
This works best when the input is sorted! In practise untyped are sorted
by device/normal and then address, so coalescing works well, but not perfectly.
Good enough for debug.
Note: the 'gaps' we see are where the kernel is using the memory. For device
memory, this is the memory regions of the GIC. For regular memory that is
memory used for kernel and rootserver.
*/
#if 1
puts("\nUntyped Memory Ranges\n");
seL4_Word start = bi->untypedList[0].paddr;
seL4_Word end = start + (1ULL << bi->untypedList[0].sizeBits);
seL4_Word is_device = bi->untypedList[0].isDevice;
for (i = 1; i < bi->untyped.end - bi->untyped.start; i++) {
if (bi->untypedList[i].paddr != end || bi->untypedList[i].isDevice != is_device) {
puts(" paddr: ");
puthex64(start);
puts(" - ");
puthex64(end);
puts(" (");
puts(is_device ? "device" : "normal");
puts(")\n");
start = bi->untypedList[i].paddr;
end = start + (1ULL << bi->untypedList[i].sizeBits);
is_device = bi->untypedList[i].isDevice;
} else {
end += (1ULL << bi->untypedList[i].sizeBits);
}
}
puts(" paddr: ");
puthex64(start);
puts(" - ");
puthex64(end);
puts(" (");
puts(is_device ? "device" : "normal");
puts(")\n");
#endif
}

8
monitor/src/debug.h Normal file
View File

@ -0,0 +1,8 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
void dump_bootinfo(seL4_BootInfo *bi);

567
monitor/src/main.c Normal file
View File

@ -0,0 +1,567 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/*
* The seL4 Core Platform Monitor.
*
* The monitor is the initial task in a core platform system.
*
* The monitor fulfills two purposes:
*
* 1. creating the initial state of the system.
* 2. acting as the fault handler for for protection domains.
*
* Initialisation is performed by executing a number of kernel
* invocations to create and configure kernel objects.
*
* The specific invocations to make are configured by the build
* tool; the monitor simply reads a data structure to execute
* each invocation one at a time.
*
* The process occurs in a two step manner. The first bootstrap
* step execute the `bootstrap_invocations` only. The purpose
* of this bootstrap is to get the system to the point for the
* `system_invocations` is mapped into the monitors address space.
* Once this occurs it is possible for the monitor to switch to
* executing invocation from this second data structure.
*
* The motivation for this design is to keep both the initial
* task image and the initial CNode as small, fixed size entities.
*
* Fixed size allows both kernel and monitor to avoid unnecesary
* recompilation for different system configurations. Keeping things
* small optimizes overall memory usage.
*
*
*/
/*
* Why this you may ask? Well, the seL4 headers depend on
* a global `__sel4_ipc_buffer` which is a pointer to the
* thread's IPC buffer. Which is reasonable enough, passing
* that explicitly to every function would be annoying.
*
* The seL4 headers make this global a thread-local global,
* which is also reasonable, considering it applies to a
* specific thread! But, for our purposes we don't have threads!
*
* Thread local storage is painful and annoying to configure.
* We'd really rather NOT use thread local storage (especially
* consider we never have more than one thread in a Vspace)
*
* So, by defining __thread to be empty it means the variable
* becomes a true global rather than thread local storage
* variable, which means, we don't need to waste a bunch
* of effort and complexity on thread local storage implementation.
*/
#define __thread
#include <stdbool.h>
#include <stdint.h>
#include <sel4/sel4.h>
#include "util.h"
#include "debug.h"
#define MAX_PDS 64
#define MAX_NAME_LEN 16
#define MAX_TCBS 64
#define MAX_UNTYPED_REGIONS 256
/* Max words available for bootstrap invocations.
*
* Only a small number of syscalls is required to
* get to the point where the main syscalls data
* is mapped in, so we keep this small.
*
* FIXME: This can be smaller once compression is enabled.
*/
#define BOOTSTRAP_INVOCATION_DATA_SIZE 90
seL4_IPCBuffer *__sel4_ipc_buffer;
char _stack[4096];
static char pd_names[MAX_PDS][MAX_NAME_LEN];
seL4_Word fault_ep;
seL4_Word reply;
seL4_Word tcbs[MAX_TCBS];
struct region {
uintptr_t paddr;
uintptr_t size_bits;
uintptr_t is_device; /*FIXME: should back size_bits / is_device */
};
struct untyped_info {
seL4_Word cap_start;
seL4_Word cap_end;
struct region regions[MAX_UNTYPED_REGIONS];
};
seL4_Word bootstrap_invocation_count;
seL4_Word bootstrap_invocation_data[BOOTSTRAP_INVOCATION_DATA_SIZE];
seL4_Word system_invocation_count;
seL4_Word *system_invocation_data = (void*)0x80000000;
struct untyped_info untyped_info;
static char *
ec_to_string(uintptr_t ec)
{
switch (ec) {
case 0: return "Unknown reason";
case 1: return "Trapped WFI or WFE instruction execution";
case 3: return "Trapped MCR or MRC access with (coproc==0b1111) this is not reported using EC 0b000000";
case 4: return "Trapped MCRR or MRRC access with (coproc==0b1111) this is not reported using EC 0b000000";
case 5: return "Trapped MCR or MRC access with (coproc==0b1110)";
case 6: return "Trapped LDC or STC access";
case 7: return "Access to SVC, Advanced SIMD or floating-point functionality trapped";
case 12: return "Trapped MRRC access with (coproc==0b1110)";
case 13: return "Branch Target Exception";
case 17: return "SVC instruction execution in AArch32 state";
case 21: return "SVC instruction execution in AArch64 state";
case 24: return "Trapped MSR, MRS or System instruction exuection in AArch64 state, this is not reported using EC 0xb000000, 0b000001 or 0b000111";
case 25: return "Access to SVE functionality trapped";
case 28: return "Exception from a Pointer Authentication instruction authentication failure";
case 32: return "Instruction Abort from a lower Exception level";
case 33: return "Instruction Abort taken without a change in Exception level";
case 34: return "PC alignment fault exception";
case 36: return "Data Abort from a lower Exception level";
case 37: return "Data Abort taken without a change in Exception level";
case 38: return "SP alignment faultr exception";
case 40: return "Trapped floating-point exception taken from AArch32 state";
case 44: return "Trapped floating-point exception taken from AArch64 state";
case 47: return "SError interrupt";
case 48: return "Breakpoint exception from a lower Exception level";
case 49: return "Breakpoint exception taken without a change in Exception level";
case 50: return "Software Step exception from a lower Exception level";
case 51: return "Software Step exception taken without a change in Exception level";
case 52: return "Watchpoint exception from a lower Exception level";
case 53: return "Watchpoint exception taken without a change in Exception level";
case 56: return "BKPT instruction execution in AArch32 state";
case 60: return "BRK instruction execution in AArch64 state";
}
return "<invalid EC>";
}
static char *
data_abort_dfsc_to_string(uintptr_t dfsc)
{
switch(dfsc) {
case 0x00: return "address size fault, level 0";
case 0x01: return "address size fault, level 1";
case 0x02: return "address size fault, level 2";
case 0x03: return "address size fault, level 3";
case 0x04: return "translation fault, level 0";
case 0x05: return "translation fault, level 1";
case 0x06: return "translation fault, level 2";
case 0x07: return "translation fault, level 3";
case 0x09: return "access flag fault, level 1";
case 0x0a: return "access flag fault, level 2";
case 0x0b: return "access flag fault, level 3";
case 0x0d: return "permission fault, level 1";
case 0x0e: return "permission fault, level 2";
case 0x0f: return "permission fault, level 3";
case 0x10: return "synchronuos external abort";
case 0x11: return "synchronous tag check fault";
case 0x14: return "synchronous external abort, level 0";
case 0x15: return "synchronous external abort, level 1";
case 0x16: return "synchronous external abort, level 2";
case 0x17: return "synchronous external abort, level 3";
case 0x18: return "syncrhonous partity or ECC error";
case 0x1c: return "syncrhonous partity or ECC error, level 0";
case 0x1d: return "syncrhonous partity or ECC error, level 1";
case 0x1e: return "syncrhonous partity or ECC error, level 2";
case 0x1f: return "syncrhonous partity or ECC error, level 3";
case 0x21: return "alignment fault";
case 0x30: return "tlb conflict abort";
case 0x31: return "unsupported atomic hardware update fault";
}
return "<unexpected DFSC>";
}
static void
check_untypeds_match(seL4_BootInfo *bi)
{
/* Check that untypeds list generate from build matches the kernel */
if (untyped_info.cap_start != bi->untyped.start) {
puts("ERROR: cap start mismatch. Expected cap start: ");
puthex32(untyped_info.cap_start);
puts(" boot info cap start: ");
puthex32(bi->untyped.start);
puts("\n");
fail("cap start mismatch");
}
if (untyped_info.cap_end != bi->untyped.end) {
puts("ERROR: cap end mismatch. Expected cap end: ");
puthex32(untyped_info.cap_end);
puts(" boot info cap end: ");
puthex32(bi->untyped.end);
puts("\n");
fail("cap end mismatch");
}
for (unsigned i = 0; i < untyped_info.cap_end - untyped_info.cap_start; i++) {
if (untyped_info.regions[i].paddr != bi->untypedList[i].paddr) {
puts("ERROR: paddr mismatch for untyped region: ");
puthex32(i);
puts(" expected paddr: ");
puthex64(untyped_info.regions[i].paddr);
puts(" boot info paddr: ");
puthex64(bi->untypedList[i].paddr);
puts("\n");
fail("paddr mismatch");
}
if (untyped_info.regions[i].size_bits != bi->untypedList[i].sizeBits) {
fail("size_bits mismatch");
}
if (untyped_info.regions[i].is_device != bi->untypedList[i].isDevice) {
fail("is_device mismatch");
}
}
puts("INFO: untyped matches\n");
}
static unsigned
perform_invocation(seL4_Word *invocation_data, unsigned offset, unsigned idx)
{
seL4_MessageInfo_t tag, out_tag;
seL4_Error result;
seL4_Word mr0;
seL4_Word mr1;
seL4_Word mr2;
seL4_Word mr3;
seL4_Word service;
seL4_Word service_incr;
seL4_Word cmd = invocation_data[offset];
seL4_Word iterations = (cmd >> 32) + 1;
seL4_Word tag0 = cmd & 0xffffffffULL;
unsigned int cap_offset, cap_incr_offset, cap_count;
unsigned int mr_offset, mr_incr_offset, mr_count;
unsigned int next_offset;
tag.words[0] = tag0;
service = invocation_data[offset + 1];
cap_count = seL4_MessageInfo_get_extraCaps(tag);
mr_count = seL4_MessageInfo_get_length(tag);
#if 0
puts("Doing invocation: ");
puthex32(idx);
puts(" cap count: ");
puthex32(cap_count);
puts(" MR count: ");
puthex32(mr_count);
puts("\n");
#endif
cap_offset = offset + 2;
mr_offset = cap_offset + cap_count;
if (iterations > 1) {
service_incr = invocation_data[mr_offset + mr_count];
cap_incr_offset = mr_offset + mr_count + 1;
mr_incr_offset = cap_incr_offset + cap_count;
next_offset = mr_incr_offset + mr_count;
} else {
next_offset = mr_offset + mr_count;
}
if (seL4_MessageInfo_get_capsUnwrapped(tag) != 0) {
fail("kernel invocation should never have unwrapped caps");
}
for (unsigned i = 0; i < iterations; i++) {
/* Set all the caps */
seL4_Word call_service = service;
if (i > 0) {
call_service += service_incr * i;
}
for (unsigned j = 0; j < cap_count; j++) {
seL4_Word cap = invocation_data[cap_offset + j];
if (i > 0) {
cap += invocation_data[cap_incr_offset + j] * i;
}
seL4_SetCap(j, cap);
}
for (unsigned j = 0; j < mr_count; j++) {
seL4_Word mr = invocation_data[mr_offset + j];
if (i > 0) {
mr += invocation_data[mr_incr_offset + j] * i;
}
switch (j) {
case 0: mr0 = mr; break;
case 1: mr1 = mr; break;
case 2: mr2 = mr; break;
case 3: mr3 = mr; break;
default: seL4_SetMR(j, mr); break;
}
}
out_tag = seL4_CallWithMRs(call_service, tag, &mr0, &mr1, &mr2, &mr3);
result = (seL4_Error) seL4_MessageInfo_get_label(out_tag);
if (result != seL4_NoError) {
puts("ERROR: ");
puthex64(result);
puts(" ");
puts(sel4_strerror(result));
puts(" invocation idx: ");
puthex32(idx);
puts(".");
puthex32(i);
puts("\n");
fail("error calling");
}
#if 0
puts("Done invocation: ");
puthex32(idx);
puts(".");
puthex32(i);
puts("\n");
#endif
}
return next_offset;
}
static void
monitor(void)
{
for (;;) {
seL4_Word badge, label;
seL4_MessageInfo_t tag;
seL4_Error err;
tag = seL4_Recv(fault_ep, &badge, reply);
label = seL4_MessageInfo_get_label(tag);
seL4_Word tcb_cap = tcbs[badge];
puts("received message ");
puthex32(label);
puts(" badge: ");
puthex64(badge);
puts(" tcb cap: ");
puthex64(tcb_cap);
puts("\n");
if (badge < MAX_PDS && pd_names[badge][0] != 0) {
puts("faulting PD: ");
puts(pd_names[badge]);
puts("\n");
} else {
fail("unknown/invalid badge\n");
}
seL4_UserContext regs;
err = seL4_TCB_ReadRegisters(tcb_cap, false, 0, sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs);
if (err != seL4_NoError) {
fail("error reading registers");
}
// FIXME: Would be good to print the whole register set
puts("Registers: \n");
puts("pc : ");
puthex64(regs.pc);
puts("\n");
puts("spsr : ");
puthex64(regs.spsr);
puts("\n");
puts("x0 : ");
puthex64(regs.x0);
puts("\n");
puts("x1 : ");
puthex64(regs.x1);
puts("\n");
puts("x2 : ");
puthex64(regs.x2);
puts("\n");
puts("x3 : ");
puthex64(regs.x3);
puts("\n");
puts("x4 : ");
puthex64(regs.x4);
puts("\n");
puts("x5 : ");
puthex64(regs.x5);
puts("\n");
puts("x6 : ");
puthex64(regs.x6);
puts("\n");
puts("x7 : ");
puthex64(regs.x7);
puts("\n");
switch(label) {
case seL4_Fault_CapFault: {
seL4_Word ip = seL4_GetMR(seL4_CapFault_IP);
seL4_Word fault_addr = seL4_GetMR(seL4_CapFault_Addr);
seL4_Word in_recv_phase = seL4_GetMR(seL4_CapFault_InRecvPhase);
seL4_Word lookup_failure_type = seL4_GetMR(seL4_CapFault_LookupFailureType);
seL4_Word bits_left = seL4_GetMR(seL4_CapFault_BitsLeft);
seL4_Word depth_bits_found = seL4_GetMR(seL4_CapFault_DepthMismatch_BitsFound);
seL4_Word guard_found = seL4_GetMR(seL4_CapFault_GuardMismatch_GuardFound);
seL4_Word guard_bits_found = seL4_GetMR(seL4_CapFault_GuardMismatch_BitsFound);
puts("CapFault: ip=");
puthex64(ip);
puts(" fault_addr=");
puthex64(fault_addr);
puts(" in_recv_phase=");
puts(in_recv_phase == 0 ? "false" : "true");
puts(" lookup_failure_type=");
switch (lookup_failure_type) {
case seL4_NoFailure: puts("seL4_NoFailure"); break;
case seL4_InvalidRoot: puts("seL4_InvalidRoot"); break;
case seL4_MissingCapability: puts("seL4_MissingCapability"); break;
case seL4_DepthMismatch: puts("seL4_DepthMismatch"); break;
case seL4_GuardMismatch: puts("seL4_GuardMismatch"); break;
default: puthex64(lookup_failure_type);
}
if (
lookup_failure_type == seL4_MissingCapability ||
lookup_failure_type == seL4_DepthMismatch ||
lookup_failure_type == seL4_GuardMismatch) {
puts(" bits_left=");
puthex64(bits_left);
}
if (lookup_failure_type == seL4_DepthMismatch) {
puts(" depth_bits_found=");
puthex64(depth_bits_found);
}
if (lookup_failure_type == seL4_GuardMismatch) {
puts(" guard_found=");
puthex64(guard_found);
puts(" guard_bits_found=");
puthex64(guard_bits_found);
}
puts("\n");
break;
}
case seL4_Fault_UserException: {
puts("UserException\n");
break;
}
case seL4_Fault_VMFault: {
seL4_Word ip = seL4_GetMR(seL4_VMFault_IP);
seL4_Word fault_addr = seL4_GetMR(seL4_VMFault_Addr);
seL4_Word is_instruction = seL4_GetMR(seL4_VMFault_PrefetchFault);
seL4_Word fsr = seL4_GetMR(seL4_VMFault_FSR);
seL4_Word ec = fsr >> 26;
seL4_Word il = fsr >> 25 & 1;
seL4_Word iss = fsr & 0x1ffffffUL;
puts("VMFault: ip=");
puthex64(ip);
puts(" fault_addr=");
puthex64(fault_addr);
puts(" fsr=");
puthex64(fsr);
puts(" ");
puts(is_instruction ? "(instruction fault)" : "(data fault)");
puts("\n");
puts(" ec: ");
puthex32(ec);
puts(" ");
puts(ec_to_string(ec));
puts(" il: ");
puts(il ? "1" : "0");
puts(" iss: ");
puthex32(iss);
puts("\n");
if (ec == 0x24) {
/* FIXME: Note, this is not a complete decoding of the fault! Just some of the more
common fields!
*/
seL4_Word dfsc = iss & 0x3f;
bool ea = (iss >> 9) & 1;
bool cm = (iss >> 8) & 1;
bool s1ptw = (iss >> 7) & 1;
bool wnr = (iss >> 6) & 1;
puts(" dfsc = ");
puts(data_abort_dfsc_to_string(dfsc));
puts(" (");
puthex32(dfsc);
puts(")");
if (ea) {
puts(" -- external abort");
}
if (cm) {
puts(" -- cache maint");
}
if (s1ptw) {
puts(" -- stage 2 fault for stage 1 page table walk");
}
if (wnr) {
puts(" -- write not read");
}
puts("\n");
}
break;
}
default:
puts("Unknown fault\n");
break;
}
}
}
void
main(seL4_BootInfo *bi)
{
__sel4_ipc_buffer = bi->ipcBuffer;
puts("seL4 Core Platform Bootstrap\n");
#if 1
dump_bootinfo(bi);
#endif
check_untypeds_match(bi);
puts("INFO: Number of bootstrap invocations: ");
puthex32(bootstrap_invocation_count);
puts("\n");
puts("INFO: Number of system invocations: ");
puthex32(system_invocation_count);
puts("\n");
#if 0
{
puts("Doing the CNode dance\n");
uint32_t ident_cap1;
uint32_t ident_capX;
ident_cap1 = seL4_DebugCapIdentify(0x5);
ident_capX = seL4_DebugCapIdentify(12 << 12);
puts("cap1: ");
puthex32(ident_cap1);
puts("\ncapX: ");
puthex32(ident_capX);
puts("\n");
}
#endif
unsigned offset = 0;
for (unsigned idx = 0; idx < bootstrap_invocation_count; idx++) {
offset = perform_invocation(bootstrap_invocation_data, offset, idx);
}
puts("INFO: completed bootstrap invocations\n");
offset = 0;
for (unsigned idx = 0; idx < system_invocation_count; idx++) {
offset = perform_invocation(system_invocation_data, offset, idx);
}
puts("INFO: completed system invocations\n");
monitor();
}

88
monitor/src/util.c Normal file
View File

@ -0,0 +1,88 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include "util.h"
void
putc(uint8_t ch)
{
#if defined(CONFIG_DEBUG_BUILD)
seL4_DebugPutChar(ch);
#endif
}
void
puts(const char *s)
{
while (*s) {
putc(*s);
s++;
}
}
static char
hexchar(unsigned int v)
{
return v < 10 ? '0' + v : ('a' - 10) + v;
}
void
puthex32(uint32_t val)
{
char buffer[8 + 3];
buffer[0] = '0';
buffer[1] = 'x';
buffer[8 + 3 - 1] = 0;
for (unsigned i = 8 + 1; i > 1; i--) {
buffer[i] = hexchar(val & 0xf);
val >>= 4;
}
puts(buffer);
}
void
puthex64(uint64_t val)
{
char buffer[16 + 3];
buffer[0] = '0';
buffer[1] = 'x';
buffer[16 + 3 - 1] = 0;
for (unsigned i = 16 + 1; i > 1; i--) {
buffer[i] = hexchar(val & 0xf);
val >>= 4;
}
puts(buffer);
}
void
fail(char *s)
{
puts("FAIL: ");
puts(s);
puts("\n");
for (;;) {}
}
char*
sel4_strerror(seL4_Word err)
{
switch (err) {
case seL4_NoError: return "seL4_NoError";
case seL4_InvalidArgument: return "seL4_InvalidArgument";
case seL4_InvalidCapability: return "seL4_InvalidCapability";
case seL4_IllegalOperation: return "seL4_IllegalOperation";
case seL4_RangeError: return "seL4_RangeError";
case seL4_AlignmentError: return "seL4_AlignmentError";
case seL4_FailedLookup: return "seL4_FailedLookup";
case seL4_TruncatedMessage: return "seL4_TruncatedMessage";
case seL4_DeleteFirst: return "seL4_DeleteFirst";
case seL4_RevokeFirst: return "seL4_RevokeFirst";
case seL4_NotEnoughMemory: return "seL4_NotEnoughMemory";
}
return "<invalid seL4 error>";
}

16
monitor/src/util.h Normal file
View File

@ -0,0 +1,16 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <stdint.h>
#include <sel4/sel4.h>
void putc(uint8_t ch);
void puts(const char *s);
void puthex32(uint32_t val);
void puthex64(uint64_t val);
void fail(char *s);
char* sel4_strerror(seL4_Word err);

23
mypy.ini Normal file
View File

@ -0,0 +1,23 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
[mypy]
warn_unused_configs = True
disallow_any_unimported = True
disallow_any_expr = False
disallow_any_decorated = True
disallow_any_explicit = True
disallow_any_generics = True
disallow_subclassing_any = True
disallow_untyped_calls = True
disallow_untyped_defs = True
disallow_incomplete_defs = True
disallow_untyped_decorators = True
no_implicit_optional = True
warn_redundant_casts = True
warn_unused_ignores = True
warn_return_any = True
warn_unreachable = True
strict_equality = True

9
requirements.txt Normal file
View File

@ -0,0 +1,9 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
pyoxidizer==0.17.0
mypy==0.910
black==21.7b0
flake8==3.9.2

33
tests/capfault/Makefile Normal file
View File

@ -0,0 +1,33 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
LIBSEL4CP := ../../libsel4cp
TOOLCHAIN := aarch64-linux-gnu
PYTHON := python3.8
CPU := cortex-a35
CC := $(TOOLCHAIN)-gcc
LD := $(TOOLCHAIN)-ld
AS := $(TOOLCHAIN)-as
CAPFAULT_OBJS := capfault.o
IMAGES := capfault.elf
CFLAGS := -mcpu=$(CPU) -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall -Wno-unused-function -Werror -I$(SEL4_SDK)/include -I$(LIBSEL4CP)/include
LDFLAGS := -L$(LIBSEL4CP) -Tsel4cp.ld
LIBS := -lsel4cp
all: $(IMAGES)
%.o: %.c Makefile
$(CC) -c $(CFLAGS) $< -o $@
%.o: %.s Makefile
$(AS) -g3 -mcpu=$(CPU) $< -o $@
capfault.elf: $(CAPFAULT_OBJS)
$(LD) $(LDFLAGS) $(CAPFAULT_OBJS) $(LIBS) -o $@

8
tests/capfault/README.md Normal file
View File

@ -0,0 +1,8 @@
# Cap Fault Test
The purpose of the capfault test is to verify that the monitor will
correctly detect and output debug information in case a protection
domain generates a cap fault.
Note: This test is (currently) expected to be run manually, and
the output inspected to ensure cap fault debugging is output.

23
tests/capfault/capfault.c Normal file
View File

@ -0,0 +1,23 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <sel4cp.h>
#define ECHO_CH 2
volatile uint64_t *shared_counter = (uint64_t *)(uintptr_t)0x1800000;
void
init(void)
{
sel4cp_dbg_puts("capfault: forcing a cap fault by notifying invalid channel 10,000\n");
sel4cp_notify(10000);
}
void
notified(sel4cp_channel ch)
{
}

11
tests/capfault/capfault.system Normal file
View File

@ -0,0 +1,11 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="faulter" priority="250">
<program_image path="tests/capfault/capfault.elf" />
</protection_domain>
</system>

33
tests/overlapping_pages/Makefile Normal file
View File

@ -0,0 +1,33 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
LIBSEL4CP := ../../libsel4cp
TOOLCHAIN := aarch64-linux-gnu
PYTHON := python3.8
CPU := cortex-a35
CC := $(TOOLCHAIN)-gcc
LD := $(TOOLCHAIN)-ld
AS := $(TOOLCHAIN)-as
OVERLAPPING_PAGES_OBJS := overlapping_pages.o
IMAGES := overlapping_pages.elf
CFLAGS := -mcpu=$(CPU) -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall -Wno-unused-function -Werror -I$(SEL4_SDK)/include -I$(LIBSEL4CP)/include
LDFLAGS := -L$(LIBSEL4CP) -Tsel4cp.ld
LIBS := -lsel4cp
all: $(IMAGES)
%.o: %.c Makefile
$(CC) -c $(CFLAGS) $< -o $@
%.o: %.s Makefile
$(AS) -g3 -mcpu=$(CPU) $< -o $@
overlapping_pages.elf: $(OVERLAPPING_PAGES_OBJS)
$(LD) $(LDFLAGS) $(OVERLAPPING_PAGES_OBJS) $(LIBS) -o $@

3
tests/overlapping_pages/README.md Normal file
View File

@ -0,0 +1,3 @@
# Overlapping Pages Test
The purpose of this is to test that when a user attempts to create overlapping pages in the address space a build error occurs.

22
tests/overlapping_pages/overlapping_pages.c Normal file
View File

@ -0,0 +1,22 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <sel4cp.h>
volatile uint8_t *p;
volatile uint8_t *q;
void
init(void)
{
*p = 'A';
*q = 'Z';
}
void
notified(sel4cp_channel ch)
{
}

19
tests/overlapping_pages/overlapping_pages.system Normal file
View File

@ -0,0 +1,19 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="large0" size="0x200_000" page_size="0x200_000" />
<memory_region name="small0" size="0x1_000" page_size="0x1_000" />
<protection_domain name="simplemrs" priority="250">
<program_image path="tests/overlapping_pages/overlapping_pages.elf" />
<map mr="large0" vaddr="0x400000" perms="rw" cached="true" setvar_vaddr="p"/>
<map mr="small0" vaddr="0x500000" perms="rw" cached="true" setvar_vaddr="q"/>
</protection_domain>
</system>

33
tests/simplemrs/Makefile Normal file
View File

@ -0,0 +1,33 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
LIBSEL4CP := ../../libsel4cp
TOOLCHAIN := aarch64-linux-gnu
PYTHON := python3.8
CPU := cortex-a35
CC := $(TOOLCHAIN)-gcc
LD := $(TOOLCHAIN)-ld
AS := $(TOOLCHAIN)-as
SIMPLEMRS_OBJS := simplemrs.o
IMAGES := simplemrs.elf
CFLAGS := -mcpu=$(CPU) -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall -Wno-unused-function -Werror -I$(SEL4_SDK)/include -I$(LIBSEL4CP)/include
LDFLAGS := -L$(LIBSEL4CP) -Tsel4cp.ld
LIBS := -lsel4cp
all: $(IMAGES)
%.o: %.c Makefile
$(CC) -c $(CFLAGS) $< -o $@
%.o: %.s Makefile
$(AS) -g3 -mcpu=$(CPU) $< -o $@
simplemrs.elf: $(SIMPLEMRS_OBJS)
$(LD) $(LDFLAGS) $(SIMPLEMRS_OBJS) $(LIBS) -o $@

5
tests/simplemrs/README.md Normal file
View File

@ -0,0 +1,5 @@
# Simple Memory Region Tests
The purpose of this is to test very simple system with two MRs and a single PD.
It is a very simple smoke test.

22
tests/simplemrs/simplemrs.c Normal file
View File

@ -0,0 +1,22 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <sel4cp.h>
volatile uint8_t *p;
volatile uint8_t *q;
void
init(void)
{
*p = 'A';
*q = 'Z';
}
void
notified(sel4cp_channel ch)
{
}

19
tests/simplemrs/simplemrs.system Normal file
View File

@ -0,0 +1,19 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="large0" size="0x200_000" page_size="0x200_000" />
<memory_region name="small0" size="0x1_000" page_size="0x1_000" />
<protection_domain name="simplemrs" priority="250">
<program_image path="tests/simplemrs/simplemrs.elf" />
<map mr="large0" vaddr="0x400000" perms="rw" cached="true" setvar_vaddr="p"/>
<map mr="small0" vaddr="0x600000" perms="rw" cached="true" setvar_vaddr="q"/>
</protection_domain>
</system>

48
tool/pyoxidizer.bzl Normal file
View File

@ -0,0 +1,48 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
# PyOxidizer configuration file for generation sel4cp tool
def make_exe():
dist = default_python_distribution()
# Configure the policy
policy = dist.make_python_packaging_policy()
policy.extension_module_filter = "no-copyleft"
policy.include_test = False
policy.resources_location = "in-memory"
policy.resources_location_fallback = None
# Configure the config
python_config = dist.make_python_interpreter_config()
python_config.run_module = "sel4coreplat"
exe = dist.to_python_executable(name="sel4cp", packaging_policy=policy, config=python_config)
resources = exe.read_package_root(path="tool", packages=["sel4coreplat"])
exe.add_python_resources(resources)
return exe
def make_embedded_resources(exe):
return exe.to_embedded_resources()
def make_install(exe):
# Create an object that represents our installed application file layout.
files = FileManifest()
# Add the generated executable to our install layout in the root directory.
files.add_python_resource(".", exe)
return files
# Tell PyOxidizer about the build targets defined above.
register_target("exe", make_exe)
register_target("resources", make_embedded_resources, depends=["exe"], default_build_script=True)
register_target("install", make_install, depends=["exe"], default=True)
# Resolve whatever targets the invoker of this configuration file is requesting
# be resolved.
resolve_targets()

0
tool/sel4coreplat/__init__.py Normal file
View File

1670
tool/sel4coreplat/__main__.py Normal file
View File

File diff suppressed because it is too large Load Diff

76
tool/sel4coreplat/docs.md Normal file
View File

@ -0,0 +1,76 @@
# Description
## Emulating the kernel boot
1. Building the system requires knowledge of the untyped objects
that the kernel has. To achieve this we must emulate what the
kernel does during boot.the kernel boot
The inputs for emulating a kernel boot are the kernel ELF image,
the region of physical memory used by the initial task, and the
reserved region of physical memory.
### Determine physical memory region for initial task
1. We use the ELF file to tell us, we should allocate it.
2. It must be a single region.
## Things that need improvement
Right now the memory for the initial task region is determine by the ELF file.
This is dumb. It should be allocated.
We need a physical memory allocator for the platform.
The physical memory allocator should take into account:
1/ Kernel physical memory.
2/ Loader physical memory.
3/ Boot loader physical memory.
#
# Building the system has a problem:
#
# In order to accurately build the system it is necessary to know, in advance,
#
# 1/ the amount of memory to use for the 'invocation table' which is used by the
# monitor to setup the system.
#
# 2/ the size of the system CNode used to hold caps for the initial objects.
#
# However, it is also necessary to *build* the system actually know how many
# invocations are required to setup the system, or the number of caps required.
#
# The size of the invocation table or initial CNode can potentially change the
# number of invocations or caps required for the system!
#
# The approach taken to solve this is:
#
# 1/ At the beginning we start with the minimum possible sizes for the invocation
# table and system CNode.
#
# 2/ We build the system based on this assumption
#
# 3/ We check the number of invocations and caps required for the build system.
# If it fits in the current invocation table and system CNode, we reach a stopping
# condition.
# Otherwise we increase both the invocation table size and system cnode size
# to fit the required number of invocations and caps, we then repeat from step #2
#
# In almost all cases we'd expect to reach a stable point after two iterations
# of this process, however it is possible that increasing the size of the invocation
# table / system CNode creates a system that requires more invocations of caps
# resulting in another iteration.
#
# Note: invocation table size must be a multiple of page size, while system cnode
# size must be a power of two. This means they will, in most circumstances, be
# overallocated on the first iteration, so even a modest increase in invocations
# or caps will not required a subsequent increase.
#
# Note: the algorithm never decreases the size of the invocation table or
# system CNode. It is possible (I think!) although very unlikely that a larger
# invocation table or system CNode may result in fewer invocations or caps being
# required. If the sizes were decreased after an iteration it would be possible
# (although exceedingly unlikely) for the algorithm to never terminate as it bounces
# between to constantly increasing then decreasing sizes.
#

452
tool/sel4coreplat/elf.py Normal file
View File

@ -0,0 +1,452 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
from pathlib import Path
from struct import Struct, pack
from enum import IntEnum, IntFlag
from dataclasses import dataclass
from typing import List, Literal, Optional, Tuple
class ObjectFileType(IntEnum):
ET_NONE = 0
ET_REL = 1
ET_EXEC = 2
ET_DYN = 3
ET_CORE = 4
class ObjectFileClass(IntEnum):
ELFCLASS32 = 1
ELFCLASS64 = 2
class DataEncoding(IntEnum):
ELFDATA2LSB = 1
ELFDATA2MSB = 2
class OperatingSystemAbi(IntEnum):
ELFOSABI_SYSV = 0
ELFOSABI_HPUX = 1
ELFOSABI_STANDALINE = 255
class SegmentType(IntEnum):
PT_NULL = 0
PT_LOAD = 1
PT_DYNAMIC = 2
PT_INTERP = 3
PT_NOTE = 4
PT_SHLID = 5
PT_PHDR = 6
class SegmentAttributes(IntFlag):
PF_X = 0x1
PF_W = 0x2
PF_R = 0x4
class MachineType(IntEnum):
# NOTE: Obviously there are may more!
# This is all we support for now, and I don't
# feel like typing them all out!
EM_AARCH64 = 183
class ElfVersion(IntEnum):
EV_NONE = 0
EV_CURRENT = 1
ELF_MAGIC = b'\x7FELF'
# Note: header struct excludes first 5 bytes (magic + class)
ELF_HEADER32 = Struct("<BBBBxxxxxxxHHIIIIIHHHHHH")
ELF_HEADER32_FIELDS = (
"ident_data",
"ident_version",
"ident_osabi",
"ident_abiversion",
"type_",
"machine",
"version",
"entry",
"phoff",
"shoff",
"flags",
"ehsize",
"phentsize",
"phnum",
"shentsize",
"shnum",
"shstrndx",
)
ELF_PROGRAM_HEADER32 = Struct("<IIIIIIII")
ELF_PROGRAM_HEADER32_FIELDS = (
"type_",
"offset",
"vaddr",
"paddr",
"filesz",
"memsz",
"flags",
"align",
)
ELF_SECTION_HEADER32 = Struct("<IIIIIIIIII")
ELF_SECTION_HEADER32_FIELDS = (
"name",
"type_",
"flags",
"addr",
"offset",
"size",
"link",
"info",
"addralign",
"entsize",
)
ELF_HEADER64 = Struct("<BBBBxxxxxxxHHIQQQIHHHHHH")
ELF_HEADER64_FIELDS = (
"ident_data",
"ident_version",
"ident_osabi",
"ident_abiversion",
"type_",
"machine",
"version",
"entry",
"phoff",
"shoff",
"flags",
"ehsize",
"phentsize",
"phnum",
"shentsize",
"shnum",
"shstrndx",
)
ELF_PROGRAM_HEADER64 = Struct("<IIQQQQQQ")
ELF_PROGRAM_HEADER64_FIELDS = (
"type_",
"flags",
"offset",
"vaddr",
"paddr",
"filesz",
"memsz",
"align",
)
ELF_SECTION_HEADER64 = Struct("<IIQQQQIIQQ")
ELF_SECTION_HEADER64_FIELDS = (
"name",
"type_",
"flags",
"addr",
"offset",
"size",
"link",
"info",
"addralign",
"entsize",
)
ELF_SYMBOL64 = Struct("<IBBHQQ")
ELF_SYMBOL64_FIELDS = (
"name",
"info",
"other",
"shndx",
"value",
"size",
)
class InvalidElf(Exception):
pass
@dataclass
class ElfHeader:
ident_data: int
ident_version: int
ident_osabi: int
ident_abiversion: int
type_: int
machine: int
version: int
entry: int
phoff: int
shoff: int
flags: int
ehsize: int
phentsize: int
phnum: int
shentsize: int
shnum: int
shstrndx: int
@dataclass
class ElfProgramHeader:
type_: int
offset: int
vaddr: int
paddr: int
filesz: int
memsz: int
flags: int
align: int
@dataclass
class ElfSectionHeader:
name: int
type_: int
flags: int
addr: int
offset: int
size: int
link: int
info: int
addralign: int
entsize: int
@dataclass
class ElfSymbol:
name: int
info: int
other: int
shndx: int
value: int
size: int
class ElfSegment:
def __init__(self, phys_addr: int, virt_addr: int, data: bytearray, loadable: bool, attrs: SegmentAttributes) -> None:
self.data = data
self.phys_addr = phys_addr
self.virt_addr = virt_addr
self.loadable = loadable
self.attrs = attrs
def __repr__(self) -> str:
return f"<ElfSegment phys_addr=0x{self.phys_addr:x} virt_addr=0x{self.virt_addr:x} mem_size={self.mem_size}>"
# FIXME: Is this really useful?
@property
def mem_size(self) -> int:
return len(self.data)
@property
def is_writable(self) -> bool:
return (self.attrs & SegmentAttributes.PF_W) != 0
@property
def is_readable(self) -> bool:
return (self.attrs & SegmentAttributes.PF_R) != 0
@property
def is_executable(self) -> bool:
return (self.attrs & SegmentAttributes.PF_X) != 0
class ElfFile:
def __init__(self, word_size: Literal[32, 64] = 64) -> None:
self.segments: List[ElfSegment] = []
self._symbols: List[Tuple[str, ElfSymbol]] = []
self.word_size = word_size
self.entry: int = 0x0
@classmethod
def from_path(cls, path: Path) -> "ElfFile":
with path.open("rb") as f:
magic = f.read(4)
if magic != ELF_MAGIC:
raise InvalidElf("Incorrect magic")
class_ = f.read(1)[0]
if class_ == 1:
hdr_fmt = ELF_HEADER32
hdr_fields = ELF_HEADER32_FIELDS
ph_fmt = ELF_PROGRAM_HEADER32
ph_fields = ELF_PROGRAM_HEADER32_FIELDS
sh_fmt = ELF_SECTION_HEADER32
sh_fields = ELF_SECTION_HEADER32_FIELDS
elf = cls(word_size=32)
elif class_ == 2:
hdr_fmt = ELF_HEADER64
hdr_fields = ELF_HEADER64_FIELDS
ph_fmt = ELF_PROGRAM_HEADER64
ph_fields = ELF_PROGRAM_HEADER64_FIELDS
sh_fmt = ELF_SECTION_HEADER64
sh_fields = ELF_SECTION_HEADER64_FIELDS
sym_fmt = ELF_SYMBOL64
sym_fields = ELF_SYMBOL64_FIELDS
elf = cls(word_size=64)
else:
raise InvalidElf(f"Invalid class '{class_}'")
hdr_raw = f.read(hdr_fmt.size)
hdr: ElfHeader = ElfHeader(**dict(zip(hdr_fields, hdr_fmt.unpack(hdr_raw))))
elf.entry = hdr.entry
f.seek(hdr.phoff)
for idx in range(hdr.phnum):
f.seek(hdr.phoff + idx * hdr.phentsize)
phent_raw = f.read(hdr.phentsize)
phent = ElfProgramHeader(**dict(zip(ph_fields, ph_fmt.unpack_from(phent_raw))))
f.seek(phent.offset)
data = f.read(phent.filesz)
zeros = bytes(phent.memsz - phent.filesz)
elf.segments.append(ElfSegment(phent.paddr, phent.vaddr, bytearray(data + zeros), phent.type_ == 1, SegmentAttributes(phent.flags)))
# FIXME: Add support for sections and symbols
f.seek(hdr.shoff)
shents = []
symtab_shent: Optional[ElfSectionHeader] = None
for idx in range(hdr.shnum):
shent_raw = f.read(hdr.shentsize)
shent = ElfSectionHeader(**dict(zip(sh_fields, sh_fmt.unpack_from(shent_raw))))
shents.append(shent)
if shent.type_ == 3:
shstrtab_shent = shent
if shent.type_ == 2:
assert symtab_shent is None
symtab_shent = shent
if shstrtab_shent is None:
raise InvalidElf("Unable to find string table section")
f.seek(shstrtab_shent.offset)
assert symtab_shent is not None
f.seek(symtab_shent.offset)
_symtab = f.read(symtab_shent.size)
symtab_str = shents[symtab_shent.link]
f.seek(symtab_str.offset)
_symtab_str = f.read(symtab_str.size)
offset = 0
elf._symbols = []
while offset < len(_symtab):
sym = ElfSymbol(**dict(zip(sym_fields, sym_fmt.unpack_from(_symtab, offset))))
name = cls._get_string(_symtab_str, sym.name)
offset += sym_fmt.size
elf._symbols.append((name, sym))
return elf
def write(self, path: Path) -> None:
"""Note: This only supports writing out of program headers
and segments. It does *not* support writing out sections
at this point in time.
"""
with path.open("wb") as f:
ehsize = ELF_HEADER64.size + 5
phentsize = ELF_PROGRAM_HEADER64.size
header = ElfHeader(
ident_data=DataEncoding.ELFDATA2LSB,
ident_version=ElfVersion.EV_CURRENT,
ident_osabi=OperatingSystemAbi.ELFOSABI_STANDALINE,
ident_abiversion=0,
type_ = ObjectFileType.ET_EXEC,
machine=MachineType.EM_AARCH64,
version=ElfVersion.EV_CURRENT,
entry=self.entry,
phoff=ehsize,
shoff=0,
flags=0,
ehsize=ehsize,
phentsize=phentsize,
phnum=len(self.segments),
shentsize=0,
shnum=0,
shstrndx=0,
)
header_bytes = ELF_HEADER64.pack(*(getattr(header, field) for field in ELF_HEADER64_FIELDS))
f.write(ELF_MAGIC)
f.write(pack("<B", ObjectFileClass.ELFCLASS64))
f.write(header_bytes)
data_offset = ehsize + len(self.segments) * phentsize
for segment in self.segments:
pheader = ElfProgramHeader(
type_ = SegmentType.PT_LOAD,
offset = data_offset,
vaddr = segment.virt_addr,
paddr = segment.phys_addr,
filesz = segment.mem_size,
memsz = segment.mem_size,
# FIXME: Need to do something better with permissions in the future!
flags = SegmentAttributes.PF_R | SegmentAttributes.PF_W | SegmentAttributes.PF_X,
align = 1,
)
pheader_bytes = ELF_PROGRAM_HEADER64.pack(*(getattr(pheader, field) for field in ELF_PROGRAM_HEADER64_FIELDS))
f.write(pheader_bytes)
data_offset += len(segment.data)
for segment in self.segments:
f.write(segment.data)
def add_segment(self, segment: ElfSegment) -> None:
# TODO: Check that the segment doesn't overlap any existing
# segment
# TODO: We may want to keep segments in order.
self.segments.append(segment)
def get_data(self, vaddr: int, size: int) -> bytes:
for seg in self.segments:
if vaddr >= seg.virt_addr and vaddr + size <= seg.virt_addr + len(seg.data):
offset = vaddr - seg.virt_addr
return seg.data[offset:offset+size]
raise Exception(f"Unable to find data for vaddr=0x{vaddr:x} size=0x{size:x}")
def write_symbol(self, variable_name: str, data: bytes) -> None:
vaddr, size = self.find_symbol(variable_name)
for seg in self.segments:
if vaddr >= seg.virt_addr and vaddr + size <= seg.virt_addr + len(seg.data):
offset = vaddr - seg.virt_addr
assert len(data) <= size
seg.data[offset:offset+len(data)] = data
# def read(self, offset: int, size: int) -> bytes:
# self._f.seek(offset)
# return self._f.read(size)
# def _get_sh_string(self, idx: int) -> str:
# end_idx = self._shstrtab.find(0, idx)
# return self._shstrtab[idx:end_idx].decode("ascii")
@staticmethod
def _get_string(strtab: bytes, idx: int) -> str:
end_idx = strtab.find(0, idx)
return strtab[idx:end_idx].decode("utf8")
def find_symbol(self, variable_name: str) -> Tuple[int, int]:
found_sym = None
for name, sym in self._symbols:
if name == variable_name:
if found_sym is None:
found_sym = sym
else:
raise Exception(f"Multiple symbols with name {variable_name}")
if found_sym is None:
raise KeyError(f"No symbol named {variable_name} found")
# symbol_type = found_sym.info & 0xf
# symbol_binding = found_sym.info >> 4
#if symbol_type != 1:
# raise Exception(f"Unexpected symbol type {symbol_type}. Expect STT_OBJECT")
return found_sym.value, found_sym.size
def read_struct(self, variable_name: str, struct_: Struct) -> Tuple[int, ...]:
vaddr, size = self.find_symbol(variable_name)
return struct_.unpack_from(self.get_data(vaddr, size))

262
tool/sel4coreplat/loader.py Normal file
View File

@ -0,0 +1,262 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
from pathlib import Path
from struct import pack
from typing import Dict, List, Optional, Tuple, Union
from sel4coreplat.elf import ElfFile
from sel4coreplat.util import kb, mb, round_up, MemoryRegion
AARCH64_1GB_BLOCK_BITS = 30
AARCH64_2MB_BLOCK_BITS = 21
AARCH64_LVL0_BITS = 9
AARCH64_LVL1_BITS = 9
AARCH64_LVL2_BITS = 9
PAGE_TABLE_SIZE = 4096
def mask(x: int) -> int:
return ((1 << x) - 1)
def lvl0_index(addr: int) -> int:
return (((addr) >> (AARCH64_2MB_BLOCK_BITS + AARCH64_LVL2_BITS + AARCH64_LVL1_BITS)) & mask(AARCH64_LVL0_BITS))
def lvl1_index(addr: int) -> int:
return (((addr) >> (AARCH64_2MB_BLOCK_BITS + AARCH64_LVL2_BITS)) & mask(AARCH64_LVL1_BITS))
def lvl2_index(addr: int) -> int:
return (((addr) >> (AARCH64_2MB_BLOCK_BITS)) & mask(AARCH64_LVL2_BITS))
def lvl0_addr(addr: int) -> int:
bits = AARCH64_2MB_BLOCK_BITS + AARCH64_LVL2_BITS + AARCH64_LVL1_BITS
return (addr >> bits) << bits
def lvl1_addr(addr: int) -> int:
bits = AARCH64_2MB_BLOCK_BITS + AARCH64_LVL2_BITS
return (addr >> bits) << bits
def lvl2_addr(addr: int) -> int:
bits = AARCH64_2MB_BLOCK_BITS
return (addr >> bits) << bits
def _check_non_overlapping(regions: List[Tuple[int, bytes]]) -> None:
checked: List[Tuple[int, int]] = []
for base, data in regions:
end = base + len(data)
# Check that this does not overlap any checked regions
for b, e in checked:
if not (end <= b or base >= e):
raise Exception(f"Overlapping: {base:x}--{end:x} overlaps {b:x} -- {e:x}")
checked.append((base, end))
class Loader:
def __init__(self,
loader_elf_path: Path,
kernel_elf: ElfFile,
initial_task_elf: ElfFile,
reserved_region: MemoryRegion,
regions: List[Tuple[int, bytes]]
) -> None:
# Setup the pagetable data structures (directly embedded in the loader)
self._elf = ElfFile.from_path(loader_elf_path)
sz = self._elf.word_size
self._header_struct_fmt = "<IIIIIIIIII" if sz == 32 else "<QQQQqQQQQQ"
self._region_struct_fmt = "<IIII" if sz == 32 else "<QQQQ"
self._magic = 0x5e14dead if sz== 32 else 0x5e14dead14de5ead
for loader_segment in self._elf.segments:
if loader_segment.loadable:
break
else:
raise Exception("Didn't find loadable segment")
if loader_segment.virt_addr != self._elf.entry:
raise Exception("The loader entry point must be the first byte in the image")
self._image = loader_segment.data
self._regions: List[Tuple[int, Union[bytes, bytearray]]] = []
kernel_first_vaddr: Optional[int] = None
kernel_last_vaddr: Optional[int] = None
kernel_first_paddr: Optional[int] = None
kernel_p_v_offset: Optional[int] = None
for segment in kernel_elf.segments:
if segment.loadable:
# NOTE: For now we include any zeroes. We could optimize in the future
if kernel_first_vaddr is None or segment.virt_addr < kernel_first_vaddr:
kernel_first_vaddr = segment.virt_addr
if kernel_last_vaddr is None or segment.virt_addr + segment.mem_size > kernel_last_vaddr:
kernel_last_vaddr = round_up(segment.virt_addr + segment.mem_size, mb(2))
if kernel_first_paddr is None or segment.phys_addr < kernel_first_paddr:
kernel_first_paddr = segment.phys_addr
if kernel_p_v_offset is None:
kernel_p_v_offset = segment.virt_addr - segment.phys_addr
else:
if kernel_p_v_offset != segment.virt_addr - segment.phys_addr:
raise Exception("Kernel does not have constistent phys to virt offset")
self._regions.append((
segment.phys_addr,
segment.data
))
inittask_first_vaddr: Optional[int] = None
inittask_last_vaddr: Optional[int] = None
inittask_first_paddr: Optional[int] = None
inittask_p_v_offset: Optional[int] = None
assert kernel_first_paddr is not None
for segment in initial_task_elf.segments:
if segment.loadable:
if inittask_first_vaddr is None or segment.virt_addr < inittask_first_vaddr:
inittask_first_vaddr = segment.virt_addr
if inittask_last_vaddr is None or segment.virt_addr + segment.mem_size > inittask_last_vaddr:
inittask_last_vaddr = round_up(segment.virt_addr + segment.mem_size, kb(4))
if inittask_first_paddr is None or segment.phys_addr < kernel_first_paddr:
inittask_first_paddr = segment.phys_addr
if inittask_p_v_offset is None:
inittask_p_v_offset = segment.virt_addr - segment.phys_addr
else:
if inittask_p_v_offset != segment.virt_addr - segment.phys_addr:
raise Exception("Init task does not have constistent phys to virt offset")
# NOTE: For now we include any zeroes. We could optimize in the future
self._regions.append((
segment.phys_addr,
segment.data
))
# Determine the pagetable variables
assert kernel_first_vaddr is not None
assert kernel_first_paddr is not None
pagetable_vars = self._setup_pagetables(kernel_first_vaddr, kernel_first_paddr)
for var_name, var_data in pagetable_vars.items():
var_addr, var_size = self._elf.find_symbol(var_name)
offset = var_addr - loader_segment.virt_addr
assert var_size == len(var_data)
assert offset > 0
assert offset <= len(self._image)
self._image[offset:offset + var_size] = var_data
kernel_entry = kernel_elf.entry
assert inittask_first_paddr is not None
assert inittask_first_vaddr is not None
pv_offset = inittask_first_paddr - inittask_first_vaddr
ui_p_reg_start = inittask_first_paddr
assert inittask_last_vaddr is not None
assert inittask_p_v_offset is not None
ui_p_reg_end = inittask_last_vaddr - inittask_p_v_offset
assert(ui_p_reg_end > ui_p_reg_start)
v_entry = initial_task_elf.entry
extra_device_addr_p = reserved_region.base
extra_device_size = reserved_region.size
self._regions += regions
_check_non_overlapping(self._regions)
# FIXME: Should be a way to determine if seL4 needs hypervisor mode or not
flags = 0
self._header = (
self._magic,
flags,
kernel_entry,
ui_p_reg_start,
ui_p_reg_end,
pv_offset,
v_entry,
extra_device_addr_p,
extra_device_size,
len(self._regions)
)
def _setup_pagetables(self, first_vaddr: int, first_paddr: int) -> Dict[str, bytes]:
boot_lvl1_lower_addr, _ = self._elf.find_symbol("boot_lvl1_lower")
boot_lvl1_upper_addr, _ = self._elf.find_symbol("boot_lvl1_upper")
boot_lvl2_upper_addr, _ = self._elf.find_symbol("boot_lvl2_upper")
boot_lvl0_lower = bytearray(PAGE_TABLE_SIZE)
boot_lvl0_lower[:8] = pack("<Q", boot_lvl1_lower_addr | 3)
boot_lvl1_lower = bytearray(PAGE_TABLE_SIZE)
for i in range(512):
pt_entry = (
(i << AARCH64_1GB_BLOCK_BITS) |
(1 << 10) | # access flag
(0 << 2) | # strongly ordered memory
(1) # 1G block
)
boot_lvl1_lower[8*i:8*(i+1)] = pack("<Q", pt_entry)
boot_lvl0_upper = bytearray(PAGE_TABLE_SIZE)
ptentry = boot_lvl1_upper_addr | 3
idx = lvl0_index(first_vaddr)
boot_lvl0_upper[8 * idx:8 * (idx+1)] = pack("<Q", ptentry)
boot_lvl1_upper = bytearray(PAGE_TABLE_SIZE)
ptentry = boot_lvl2_upper_addr | 3
idx = lvl1_index(first_vaddr)
boot_lvl1_upper[8 * idx:8 * (idx+1)] = pack("<Q", ptentry)
boot_lvl2_upper = bytearray(PAGE_TABLE_SIZE)
for i in range(lvl2_index(first_vaddr), 512):
pt_entry = (
first_paddr |
(1 << 10) | # access flag
(3 << 8) | # make sure the shareability is the same as the kernel's
(4 << 2) | #MT_NORMAL memory
(1 << 0) # 2M block
)
first_paddr += (1 << AARCH64_2MB_BLOCK_BITS)
boot_lvl2_upper[8*i:8*(i+1)] = pack("<Q", pt_entry)
return {
"boot_lvl0_lower": boot_lvl0_lower,
"boot_lvl1_lower": boot_lvl1_lower,
"boot_lvl0_upper": boot_lvl0_upper,
"boot_lvl1_upper": boot_lvl1_upper,
"boot_lvl2_upper": boot_lvl2_upper,
}
def write_image(self, path: Path) -> None:
with path.open("wb") as f:
header_binary = pack(self._header_struct_fmt, *self._header)
offset = 0
for addr, data in self._regions:
header_binary += pack(self._region_struct_fmt, addr, len(data), offset, 1)
offset += len(data)
# Finally write everything out to a file.
f.write(self._image)
f.write(header_binary)
for _, data in self._regions:
f.write(data)

812
tool/sel4coreplat/sel4.py Normal file
View File

@ -0,0 +1,812 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
from dataclasses import dataclass, fields
from enum import IntEnum
from typing import List, Optional, Set, Tuple
from struct import pack, Struct
from sel4coreplat.util import MemoryRegion, DisjointMemoryRegion, lsb, round_down, round_up
from sel4coreplat.elf import ElfFile
SLOT_BITS = 5
SLOT_SIZE = 1 << SLOT_BITS
SEL4_TCB_SIZE = (1 << 11)
SEL4_ENDPOINT_SIZE = (1 << 4)
SEL4_NOTIFICATION_SIZE = (1 << 6)
SEL4_REPLY_SIZE = (1 << 5)
SEL4_PAGE_TABLE_SIZE = (1 << 12)
SEL4_PAGE_DIRECTORY_SIZE = (1 << 12)
SEL4_PAGE_UPPER_DIRECTORY_SIZE = (1 << 12)
SEL4_LARGE_PAGE_SIZE = (2 * 1024 * 1024)
SEL4_SMALL_PAGE_SIZE = (4 * 1024)
SEL4_VSPACE_SIZE = (4 * 1024)
SEL4_ASID_POOL_SIZE = (1 << 12)
# Kernel Objects:
SEL4_UNTYPED_OBJECT = 0
SEL4_TCB_OBJECT = 1
SEL4_ENDPOINT_OBJECT = 2
SEL4_NOTIFICATION_OBJECT = 3
SEL4_CNODE_OBJECT = 4
SEL4_SCHEDCONTEXT_OBJECT = 5
SEL4_REPLY_OBJECT = 6
SEL4_HUGE_PAGE_OBJECT = 7
SEL4_PAGE_UPPER_DIRECTORY_OBJECT = 8
SEL4_PAGE_GLOBAL_DIRECTORY_OBJECT = 9
SEL4_SMALL_PAGE_OBJECT = 10
SEL4_LARGE_PAGE_OBJECT = 11
SEL4_PAGE_TABLE_OBJECT = 12
SEL4_PAGE_DIRECTORY_OBJECT = 13
SEL4_VSPACE_OBJECT = SEL4_PAGE_GLOBAL_DIRECTORY_OBJECT
FIXED_OBJECT_SIZES = {
SEL4_TCB_OBJECT: SEL4_TCB_SIZE,
SEL4_ENDPOINT_OBJECT: SEL4_ENDPOINT_SIZE,
SEL4_NOTIFICATION_OBJECT: SEL4_NOTIFICATION_SIZE,
SEL4_REPLY_OBJECT: SEL4_REPLY_SIZE,
SEL4_VSPACE_OBJECT: SEL4_VSPACE_SIZE,
SEL4_PAGE_UPPER_DIRECTORY_OBJECT: SEL4_PAGE_UPPER_DIRECTORY_SIZE,
SEL4_PAGE_DIRECTORY_OBJECT: SEL4_PAGE_DIRECTORY_SIZE,
SEL4_PAGE_TABLE_OBJECT: SEL4_PAGE_TABLE_SIZE,
SEL4_LARGE_PAGE_OBJECT: SEL4_LARGE_PAGE_SIZE,
SEL4_SMALL_PAGE_OBJECT: SEL4_SMALL_PAGE_SIZE,
}
VARIABLE_SIZE_OBJECTS = {
SEL4_CNODE_OBJECT,
SEL4_UNTYPED_OBJECT,
SEL4_SCHEDCONTEXT_OBJECT,
}
SEL4_RIGHTS_WRITE = 1
SEL4_RIGHTS_READ = 2
SEL4_RIGHTS_GRANT = 4
SEL4_RIGHTS_GRANT_REPLY = 8
SEL4_RIGHTS_ALL = 0xf
SEL4_ARM_PAGE_CACHEABLE = 1
SEL4_ARM_PARITY_ENABLED = 2
SEL4_ARM_EXECUTE_NEVER = 4
SEL4_ARM_DEFAULT_VMATTRIBUTES = 3
SEL4_ARM_CACHE_I = 1
SEL4_ARM_CACHE_D = 2
SEL4_ARM_CACHE_ID = 3
# FIXME: There should be a better way of determining these, so they don't
# have to be hard coded
INIT_NULL_CAP_ADDRESS = 0
INIT_TCB_CAP_ADDRESS = 1
INIT_CNODE_CAP_ADDRESS = 2
INIT_VSPACE_CAP_ADDRESS = 3
IRQ_CONTROL_CAP_ADDRESS = 4 # Singleton
ASID_CONTROL_CAP_ADDRESS = 5 # Singleton
INIT_ASID_POOL_CAP_ADDRESS = 6
IO_PORT_CONTROL_CAP_ADDRESS = 7 # Null on this platform
IO_SPACE_CAP_ADDRESS = 8 # Null on this platform
BOOT_INFO_FRAME_CAP_ADDRESS = 9
INIT_THREAD_IPC_BUFFER_CAP_ADDRESS = 10
DOMAIN_CAP_ADDRESS = 11
SMMU_SID_CONTROL_CAP_ADDRESS = 12
SMMU_CB_CONTROL_CAP_ADDRESS = 13
INIT_THREAD_SC_CAP_ADDRESS = 14
def _get_n_paging(region: MemoryRegion, bits: int) -> int:
start = round_down(region.base, 1 << bits)
end = round_up(region.end, 1 << bits)
return (end - start) // (1 << bits)
def _get_arch_n_paging(region: MemoryRegion) -> int:
PT_INDEX_OFFSET = 12
PD_INDEX_OFFSET = (PT_INDEX_OFFSET + 9)
PUD_INDEX_OFFSET = (PD_INDEX_OFFSET + 9)
PGD_INDEX_OFFSET = (PUD_INDEX_OFFSET + 9)
return (
_get_n_paging(region, PGD_INDEX_OFFSET) +
_get_n_paging(region, PUD_INDEX_OFFSET) +
_get_n_paging(region, PD_INDEX_OFFSET)
)
def calculate_rootserver_size(initial_task_region: MemoryRegion) -> int:
# FIXME: These constants should ideally come from the config / kernel
# binary not be hard coded here.
# But they are constant so it isn't too bad.
# This is specifically for aarch64
slot_bits = 5 # seL4_SlotBits
root_cnode_bits = 12 # CONFIG_ROOT_CNODE_SIZE_BITS
tcb_bits = 11 # seL4_TCBBits
page_bits = 12 # seL4_PageBits
asid_pool_bits = 12 # seL4_ASIDPoolBits
vspace_bits = 12 #seL4_VSpaceBits
page_table_bits = 12 # seL4_PageTableBits
min_sched_context_bits = 8 # seL4_MinSchedContextBits
size = 0
size += 1 << (root_cnode_bits + slot_bits)
size += 1 << (tcb_bits)
size += 2 * (1 << page_bits)
size += 1 << asid_pool_bits
size += 1 << vspace_bits
size += _get_arch_n_paging(initial_task_region) * (1 << page_table_bits)
size += 1 <<min_sched_context_bits
return size
class Sel4Aarch64Regs:
"""
typedef struct seL4_UserContext_ {
/* frame registers */
seL4_Word pc, sp, spsr, x0, x1, x2, x3, x4, x5, x6, x7, x8, x16, x17, x18, x29, x30;
/* other integer registers */
seL4_Word x9, x10, x11, x12, x13, x14, x15, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28;
/* Thread ID registers */
seL4_Word tpidr_el0, tpidrro_el0;
} seL4_UserContext;
"""
# FIXME: This is pretty terrible, but for now... explicit better than implicit
# NOTE: We could optimize so that we can see how many register are actually set
# in a given set to reduce space
def __init__(self,
pc: Optional[int] = None,
sp: Optional[int] = None,
spsr: Optional[int] = None,
x0: Optional[int] = None,
x1: Optional[int] = None,
x2: Optional[int] = None,
x3: Optional[int] = None,
x4: Optional[int] = None,
x5: Optional[int] = None,
x6: Optional[int] = None,
x7: Optional[int] = None,
x8: Optional[int] = None,
x16: Optional[int] = None,
x17: Optional[int] = None,
x18: Optional[int] = None,
x29: Optional[int] = None,
x30: Optional[int] = None,
x9: Optional[int] = None,
x10: Optional[int] = None,
x11: Optional[int] = None,
x12: Optional[int] = None,
x13: Optional[int] = None,
x14: Optional[int] = None,
x15: Optional[int] = None,
x19: Optional[int] = None,
x20: Optional[int] = None,
x21: Optional[int] = None,
x22: Optional[int] = None,
x23: Optional[int] = None,
x24: Optional[int] = None,
x25: Optional[int] = None,
x26: Optional[int] = None,
x27: Optional[int] = None,
x28: Optional[int] = None,
tpidr_el0: Optional[int] = None,
tpidrro_el0: Optional[int] = None,
):
self.pc = pc
self.sp = sp
self.spsr = spsr
self.x0 = x0
self.x1 = x1
self.x2 = x2
self.x3 = x3
self.x4 = x4
self.x5 = x5
self.x6 = x6
self.x7 = x7
self.x8 = x8
self.x16 = x16
self.x17 = x17
self.x18 = x18
self.x29 = x29
self.x30 = x30
self.x9 = x9
self.x10 = x10
self.x11 = x11
self.x12 = x12
self.x13 = x13
self.x14 = x14
self.x15 = x15
self.x19 = x19
self.x20 = x20
self.x21 = x21
self.x22 = x22
self.x23 = x23
self.x24 = x24
self.x25 = x25
self.x26 = x26
self.x27 = x27
self.x28 = x28
self.tpidr_el0 = tpidr_el0
self.tpidrro_el0 = tpidrro_el0
def count(self) -> int:
# FIXME: Optimize when most are none
return len(self.as_tuple())
def as_tuple(self) -> Tuple[int, ...]:
raw = (
self.pc ,
self.sp ,
self.spsr ,
self.x0 ,
self.x1 ,
self.x2 ,
self.x3 ,
self.x4 ,
self.x5 ,
self.x6 ,
self.x7 ,
self.x8 ,
self.x16 ,
self.x17 ,
self.x18 ,
self.x29 ,
self.x30 ,
self.x9 ,
self.x10 ,
self.x11 ,
self.x12 ,
self.x13 ,
self.x14 ,
self.x15 ,
self.x19 ,
self.x20 ,
self.x21 ,
self.x22 ,
self.x23 ,
self.x24 ,
self.x25 ,
self.x26 ,
self.x27 ,
self.x28 ,
self.tpidr_el0 ,
self.tpidrro_el0,
)
return tuple(0 if x is None else x for x in raw)
class Sel4Label(IntEnum):
# Untyped
UntypedRetype = 1
# TCB
TCBReadRegisters = 2
TCBWriteRegisters = 3
TCBCopyRegisters = 4
TCBConfigure = 5
TCBSetPriority = 6
TCBSetMCPriority = 7
TCBSetSchedParams = 8
TCBSetTimeoutEndpoint = 9
TCBSetIPCBuffer = 10
TCBSetSpace = 11
TCBSuspend = 12
TCBResume = 13
TCBBindNotification = 14
TCBUnbindNotification = 15
TCBSetTLSBase = 16
# CNode
CNodeRevoke = 17
CNodeDelete = 18
CNodeCancelBadgedSends = 19
CNodeCopy = 20
CNodeMint = 21
CNodeMove = 22
CNodeMutate = 23
CNodeRotate = 24
# IRQ
IRQIssueIRQHandler = 25
IRQAckIRQ = 26
IRQSetIRQHandler = 27
IRQClearIRQHandler = 28
# Domain
DomainSetSet = 29
# Sched
SchedControlConfigureFlags = 30
SchedContextBind = 31
SchedContextUnbind = 32
SchedContextUnbindObject = 33
SchedContextConsume = 34
SchedContextYieldTo = 35
# ARM V Space
ARMVSpaceClean_Data = 36
ARMVSpaceInvalidate_Data = 37
ARMVSpaceCleanInvalidate_Data = 38
ARMVSpaceUnify_Instruction = 39
# ARM Page Upper Directory
ARMPageUpperDirectoryMap = 40
ARMPageUpperDirectoryUnmap = 41
ARMPageDirectoryMap = 42
ARMPageDirectoryUnmap = 43
# ARM Page table
ARMPageTableMap = 44
ARMPageTableUnmap = 45
# ARM Page
ARMPageMap = 46
ARMPageUnmap = 47
ARMPageClean_Data = 48
ARMPageInvalidate_Data = 49
ARMPageCleanInvalidate_Data = 50
ARMPageUnify_Instruction = 51
ARMPageGetAddress = 52
# ARM Asid
ARMASIDControlMakePool = 53
ARMASIDPoolAssign = 54
# ARM IRQ
ARMIRQIssueIRQHandlerTrigger = 55
### Invocations
class Sel4Invocation:
label: Sel4Label
_extra_caps: Tuple[str, ...]
_object_type: str
_method_name: str
def _generic_invocation(self, extra_caps: Tuple[int, ...], args: Tuple[int, ...]) -> bytes:
repeat_count = self._repeat_count if hasattr(self, "_repeat_count") else None
tag = self.message_info_new(self.label, 0, len(extra_caps), len(args))
if repeat_count:
tag |= ((repeat_count - 1) << 32)
fmt = "<QQ" + ("Q" * (0 + len(extra_caps) + len(args)))
all_args = (tag, self._service) + extra_caps + args
base = pack(fmt, *all_args)
if repeat_count:
repeat_incr = self._repeat_incr
extra_fmt = "<Q" + ("Q" * (0 + len(extra_caps) + len(args)))
service: int = repeat_incr.get(fields(self)[0].name, 0)
cap_args: Tuple[int, ...] = tuple(repeat_incr.get(f.name, 0) for f in fields(self)[1:] if f.name in self._extra_caps)
val_args: Tuple[int, ...] = tuple(repeat_incr.get(f.name, 0) for f in fields(self)[1:] if f.name not in self._extra_caps)
extra = pack(extra_fmt, *((service, ) + cap_args + val_args))
else:
extra = b''
return base + extra
@property
def _service(self) -> int:
v = getattr(self, fields(self)[0].name)
assert isinstance(v, int)
return v
@property
def _args(self) -> List[Tuple[str, int]]:
arg_names = [f.name for f in fields(self)[1:]]
return [(nm, getattr(self, nm)) for nm in arg_names]
@staticmethod
def message_info_new(label: Sel4Label, caps: int, extra_caps: int, length: int) -> int:
assert label < (1 << 50)
assert caps < 8
assert extra_caps < 4
assert length < 0x80
return label << 12 | caps << 9 | extra_caps << 7 | length
def _get_raw_invocation(self) -> bytes:
cap_args = tuple(val for nm, val in self._args if nm in self._extra_caps)
val_args = tuple(val for nm, val in self._args if nm not in self._extra_caps)
return self._generic_invocation(cap_args, val_args)
def repeat(self, count: int, **kwargs: int) -> None:
if count > 1:
field_names: Set[str] = {f.name for f in fields(self)}
assert len(kwargs) > 0
for nm in kwargs:
assert nm in field_names
self._repeat_count = count
self._repeat_incr = kwargs
@dataclass
class Sel4UntypedRetype(Sel4Invocation):
_object_type = "Untyped"
_method_name = "Retype"
_extra_caps = ("root", )
label = Sel4Label.UntypedRetype
untyped: int
object_type: int
size_bits: int
root: int
node_index: int
node_depth: int
node_offset: int
num_objects: int
@dataclass
class Sel4TcbSetSchedParams(Sel4Invocation):
_object_type = "TCB"
_method_name = "SetSchedParams"
_extra_caps = ("authority", "sched_context", "fault_ep")
label = Sel4Label.TCBSetSchedParams
tcb: int
authority: int
mcp: int
priority: int
sched_context: int
fault_ep: int
@dataclass
class Sel4TcbSetSpace(Sel4Invocation):
_object_type = "TCB"
_method_name = "SetSpace"
_extra_caps = ("fault_ep", "cspace_root", "vspace_root")
label = Sel4Label.TCBSetSpace
tcb: int
fault_ep: int
cspace_root: int
cspace_root_data: int
vspace_root: int
vspace_root_data: int
@dataclass
class Sel4TcbSetIpcBuffer(Sel4Invocation):
_object_type = "TCB"
_method_name = "SetIPCBuffer"
_extra_caps = ("buffer_frame", )
label = Sel4Label.TCBSetIPCBuffer
tcb: int
buffer: int
buffer_frame: int
@dataclass
class Sel4TcbResume(Sel4Invocation):
_object_type = "TCB"
_method_name = "Resume"
_extra_caps = ()
label = Sel4Label.TCBResume
tcb: int
@dataclass
class Sel4TcbWriteRegisters(Sel4Invocation):
_object_type = "TCB"
_method_name = "WriteRegisters"
_extra_caps = ()
label = Sel4Label.TCBWriteRegisters
tcb: int
resume: bool
arch_flags: int
regs: Sel4Aarch64Regs
def _get_raw_invocation(self) -> bytes:
params = (
self.arch_flags << 8 | 1 if self.resume else 0,
self.regs.count()
) + self.regs.as_tuple()
return self._generic_invocation((), params)
@dataclass
class Sel4TcbBindNotification(Sel4Invocation):
_object_type = "TCB"
_method_name = "BindNotification"
_extra_caps = ("notification", )
label = Sel4Label.TCBBindNotification
tcb: int
notification: int
@dataclass
class Sel4AsidPoolAssign(Sel4Invocation):
_object_type = "ASID Pool"
_method_name = "Assign"
_extra_caps = ("vspace", )
label = Sel4Label.ARMASIDPoolAssign
asid_pool: int
vspace: int
@dataclass
class Sel4IrqControlGet(Sel4Invocation):
_object_type = "IRQ Control"
_method_name = "Get"
_extra_caps = ("dest_root", )
label = Sel4Label.IRQIssueIRQHandler
irq_control: int
irq: int
dest_root: int
dest_index: int
dest_depth: int
@dataclass
class Sel4IrqHandlerSetNotification(Sel4Invocation):
_object_type = "IRQ Handler"
_method_name = "SetNotification"
_extra_caps = ("notification", )
label = Sel4Label.IRQSetIRQHandler
irq_handler: int
notification: int
@dataclass
class Sel4PageUpperDirectoryMap(Sel4Invocation):
_object_type = "Page Upper Directory"
_method_name = "Map"
_extra_caps = ("vspace", )
label = Sel4Label.ARMPageUpperDirectoryMap
page_upper_directory: int
vspace: int
vaddr: int
attr: int
@dataclass
class Sel4PageDirectoryMap(Sel4Invocation):
_object_type = "Page Directory"
_method_name = "Map"
_extra_caps = ("vspace", )
label = Sel4Label.ARMPageDirectoryMap
page_directory: int
vspace: int
vaddr: int
attr: int
@dataclass
class Sel4PageTableMap(Sel4Invocation):
_object_type = "Page Table"
_method_name = "Map"
_extra_caps = ("vspace", )
label = Sel4Label.ARMPageTableMap
page_table: int
vspace: int
vaddr: int
attr: int
@dataclass
class Sel4PageMap(Sel4Invocation):
_object_type = "Page"
_method_name = "Map"
_extra_caps = ("vspace", )
label = Sel4Label.ARMPageMap
page: int
vspace: int
vaddr: int
attr: int
rights: int
@dataclass
class Sel4CnodeMint(Sel4Invocation):
_object_type = "CNode"
_method_name = "Mint"
_extra_caps = ("src_root", )
label = Sel4Label.CNodeMint
cnode: int
dest_index: int
dest_depth: int
src_root: int
src_obj: int
src_depth: int
rights: int
badge: int
@dataclass
class Sel4CnodeMutate(Sel4Invocation):
_object_type = "CNode"
_method_name = "Mutate"
_extra_caps = ("src_root", )
label = Sel4Label.CNodeMutate
cnode: int
dest_index: int
dest_depth: int
src_root: int
src_obj: int
src_depth: int
badge: int
@dataclass
class Sel4SchedControlConfigureFlags(Sel4Invocation):
_object_type = "SchedControl"
_method_name = "ConfigureFlags"
_extra_caps = ("schedcontext", )
label = Sel4Label.SchedControlConfigureFlags
schedcontrol: int
schedcontext: int
budget: int
period: int
extra_refills: int
badge: int
flags: int
@dataclass(frozen=True, eq=True)
class UntypedObject:
cap: int
region: MemoryRegion
is_device: bool
@property
def base(self) -> int:
return self.region.base
@property
def size_bits(self) -> int:
return lsb(self.region.end - self.region.base)
@dataclass(frozen=True, eq=True)
class KernelBootInfo:
fixed_cap_count: int
schedcontrol_cap: int
paging_cap_count: int
page_cap_count: int
untyped_objects: List[UntypedObject]
first_available_cap: int
@dataclass(frozen=True, eq=True)
class KernelConfig:
word_size: int
minimum_page_size: int
paddr_user_device_top: int
kernel_frame_size: int
init_cnode_bits: int
cap_address_bits: int
fan_out_limit: int
def _kernel_device_addrs(kernel_elf: ElfFile) -> List[int]:
"""Extra the physical address of all kernel (only) devices"""
kernel_devices = []
kernel_frame_t = Struct("<QQII")
vaddr, size = kernel_elf.find_symbol("kernel_device_frames")
p_regs = kernel_elf.get_data(vaddr, size)
offset = 0
while offset < size:
paddr, pptr, xn, ua = kernel_frame_t.unpack_from(p_regs, offset)
if not ua:
kernel_devices.append(paddr)
offset += kernel_frame_t.size
return kernel_devices
def _kernel_phys_mem(kernel_elf: ElfFile) -> List[Tuple[int, int]]:
"""Extract a list of normal memory from the kernel elf file."""
phys_mem = []
p_region_t = Struct("<QQ")
vaddr, size = kernel_elf.find_symbol("avail_p_regs")
p_regs = kernel_elf.get_data(vaddr, size)
offset = 0
while offset < size:
start, end = p_region_t.unpack_from(p_regs, offset)
phys_mem.append((start, end))
offset += p_region_t.size
return phys_mem
def _kernel_self_mem(kernel_elf: ElfFile) -> Tuple[int, int]:
"""Return the physical memory range used by the kernel itself."""
base = kernel_elf.segments[0].phys_addr
ki_end_v, _= kernel_elf.find_symbol("ki_end")
ki_end_p = ki_end_v - kernel_elf.segments[0].virt_addr + base
return (base, ki_end_p)
def _kernel_boot_mem(kernel_elf: ElfFile) -> MemoryRegion:
base = kernel_elf.segments[0].phys_addr
ki_boot_end_v, _ = kernel_elf.find_symbol("ki_boot_end")
ki_boot_end_p = ki_boot_end_v - kernel_elf.segments[0].virt_addr + base
return MemoryRegion(base, ki_boot_end_p)
def _rootserver_max_size_bits() -> int:
slot_bits = 5 # seL4_SlotBits
root_cnode_bits = 12 # CONFIG_ROOT_CNODE_SIZE_BITS
vspace_bits = 12 #seL4_VSpaceBits
cnode_size_bits = root_cnode_bits + slot_bits
return max(cnode_size_bits, vspace_bits)
def emulate_kernel_boot(
kernel_config: KernelConfig,
kernel_elf: ElfFile,
initial_task_region: MemoryRegion,
reserved_region: MemoryRegion) -> KernelBootInfo:
"""Emulate what happens during a kernel boot, generating a
representation of the BootInfo struct."""
# Determine the untyped caps of the system
# This lets allocations happen correctly.
device_memory = DisjointMemoryRegion()
normal_memory = DisjointMemoryRegion()
# Start by allocating the entire physical address space
# as device memory.
device_memory.insert_region(0, kernel_config.paddr_user_device_top)
# Next, remove all the kernel devices.
# NOTE: There is an assumption each kernel device is one frame
# in size only. It's possible this assumption could break in the
# future.
for paddr in _kernel_device_addrs(kernel_elf):
device_memory.remove_region(paddr, paddr + kernel_config.kernel_frame_size)
# Remove all the actual physical memory from the device regions
# but add it all to the actual normal memory regions
for start, end in _kernel_phys_mem(kernel_elf):
device_memory.remove_region(start, end)
normal_memory.insert_region(start, end)
# Remove the kernel image itself
normal_memory.remove_region(*_kernel_self_mem(kernel_elf))
# but get the boot region, we'll add that back later
# FIXME: Why calcaultae it now if we add it back later?
boot_region = _kernel_boot_mem(kernel_elf)
# Remove the initial task region
normal_memory.remove_region(initial_task_region.base, initial_task_region.end)
# And the the reserved region
normal_memory.remove_region(reserved_region.base, reserved_region.end)
# Now, the tricky part! determine which memory is used for the initial task objects
initial_objects_size = calculate_rootserver_size(initial_task_region)
initial_objects_align = _rootserver_max_size_bits()
# Find an appropriate region of normal memory to allocate the objects
# from; this follows the same algorithm used within the kernel boot code
# (or at least we hope it does!)
for region in reversed(normal_memory._regions):
start = round_down(region.end - initial_objects_size, 1 << initial_objects_align)
if start >= region.base:
normal_memory.remove_region(start, start + initial_objects_size)
break
else:
raise Exception("Couldn't find appropriate region for initial task kernel objects")
fixed_cap_count = 0xf
sched_control_cap_count = 1
paging_cap_count = _get_arch_n_paging(initial_task_region)
page_cap_count = initial_task_region.size // kernel_config.minimum_page_size
first_untyped_cap = fixed_cap_count + paging_cap_count + sched_control_cap_count + page_cap_count
schedcontrol_cap = fixed_cap_count + paging_cap_count
device_regions = reserved_region.aligned_power_of_two_regions() + device_memory.aligned_power_of_two_regions()
normal_regions = boot_region.aligned_power_of_two_regions() + normal_memory.aligned_power_of_two_regions()
untyped_objects = []
for cap, r in enumerate(device_regions, first_untyped_cap):
untyped_objects.append(UntypedObject(cap, r, True))
for cap, r in enumerate(normal_regions, cap + 1):
untyped_objects.append(UntypedObject(cap, r, False))
return KernelBootInfo(
fixed_cap_count = fixed_cap_count,
paging_cap_count = paging_cap_count,
page_cap_count = page_cap_count,
schedcontrol_cap = schedcontrol_cap,
first_available_cap = first_untyped_cap + len(device_regions) + len(normal_regions),
untyped_objects = untyped_objects,
)

352
tool/sel4coreplat/sysxml.py Normal file
View File

@ -0,0 +1,352 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
from dataclasses import dataclass
from pathlib import Path
# See: https://stackoverflow.com/questions/6949395/is-there-a-way-to-get-a-line-number-from-an-elementtree-element
# Force use of Python elementtree to avoid overloading
import sys
sys.modules['_elementtree'] = None # type: ignore
import xml.etree.ElementTree as ET
from typing import Dict, Iterable, Optional, Set, Tuple
from sel4coreplat.util import str_to_bool, UserError
MIN_PAGE_SIZE = 0x1000 # FIXME: This shouldn't be here
class MissingAttribute(Exception):
def __init__(self, attribute_name: str, element: ET.Element):
super().__init__(f"Missing attribute: {attribute_name}")
self.attribute_name = attribute_name
self.element = element
def checked_lookup(el: ET.Element, attr: str) -> str:
try:
return el.attrib[attr]
except KeyError:
raise MissingAttribute(attr, el)
def _check_attrs(el: ET.Element, valid_keys: Iterable[str]) -> None:
for key in el.attrib:
if key not in valid_keys:
raise ValueError(f"invalid attribute '{key}'")
@dataclass(frozen=True, eq=True)
class PlatformDescription:
page_sizes: Tuple[int, ...]
class LineNumberingParser(ET.XMLParser):
def __init__(self, path: Path):
super().__init__()
self._path = path
def _start(self, *args, **kwargs): # type: ignore
element = super(self.__class__, self)._start(*args, **kwargs)
element._path = self._path
element._start_line_number = self.parser.CurrentLineNumber
element._start_column_number = self.parser.CurrentColumnNumber
element._loc_str = f"{element._path}:{element._start_line_number}.{element._start_column_number}"
return element
@dataclass(frozen=True, eq=True)
class SysMap:
mr: str
vaddr: int
perms: str # FIXME: should make this a better typed thing
cached: bool
element: Optional[ET.Element]
@dataclass(frozen=True, eq=True)
class SysIrq:
irq: int
id_: int
@dataclass(frozen=True, eq=True)
class SysSetVar:
symbol: str
region_paddr: Optional[str] = None
vaddr: Optional[int] = None
@dataclass(frozen=True, eq=True)
class ProtectionDomain:
name: str
priority: int
budget: int
period: int
pp: bool
program_image: Path
maps: Tuple[SysMap, ...]
irqs: Tuple[SysIrq, ...]
setvars: Tuple[SysSetVar, ...]
element: ET.Element
@dataclass(frozen=True, eq=True)
class SysMemoryRegion:
name: str
size: int
page_size: int
page_count: int
phys_addr: Optional[int]
@dataclass(frozen=True, eq=True)
class Channel:
pd_a: str
id_a: int
pd_b: str
id_b: int
element: ET.Element
class SystemDescription:
def __init__(
self,
memory_regions: Iterable[SysMemoryRegion],
protection_domains: Iterable[ProtectionDomain],
channels: Iterable[Channel]
) -> None:
self.memory_regions = tuple(memory_regions)
self.protection_domains = tuple(protection_domains)
self.channels = tuple(channels)
# Note: These could be dict comprehensions, but
# we want to perform duplicate checks as we
# build the data structure
self.pd_by_name: Dict[str, ProtectionDomain] = {}
self.mr_by_name: Dict[str, SysMemoryRegion] = {}
# Ensure there is at least one protection domain
if len(self.protection_domains) == 0:
raise UserError("At least one protection domain must be defined")
if len(self.protection_domains) > 63:
raise UserError(f"Too many protection domains ({len(self.protection_domains)}) defined. Maximum is 63.")
for pd in protection_domains:
if pd.name in self.pd_by_name:
raise UserError(f"Duplicate protection domain name '{pd.name}'.")
self.pd_by_name[pd.name] = pd
for mr in memory_regions:
if mr.name in self.mr_by_name:
raise UserError(f"Duplicate memory region name '{mr.name}'.")
self.mr_by_name[mr.name] = mr
# Ensure all CCs make senses
for cc in self.channels:
for pd_name in (cc.pd_a, cc.pd_b):
if pd_name not in self.pd_by_name:
raise UserError(f"Invalid pd name '{pd_name}'. on element '{cc.element.tag}': {cc.element._loc_str}") # type: ignore
# Ensure no duplicate IRQs
all_irqs = set()
for pd in self.protection_domains:
for sysirq in pd.irqs:
if sysirq.irq in all_irqs:
raise UserError(f"duplicate irq: {sysirq.irq} in protection domain: '{pd.name}' @ {pd.element._loc_str}") # type: ignore
all_irqs.add(sysirq.irq)
# Ensure no duplicate channel identifiers
ch_ids: Dict[str, Set[int]] = {pd_name: set() for pd_name in self.pd_by_name}
for pd in self.protection_domains:
for sysirq in pd.irqs:
if sysirq.id_ in ch_ids[pd.name]:
raise UserError(f"duplicate channel id: {sysirq.id_} in protection domain: '{pd.name}' @ {pd.element._loc_str}") # type: ignore
ch_ids[pd.name].add(sysirq.id_)
for cc in self.channels:
if cc.id_a in ch_ids[cc.pd_a]:
pd = self.pd_by_name[cc.pd_a]
raise UserError(f"duplicate channel id: {cc.id_a} in protection domain: '{pd.name}' @ {pd.element._loc_str}") # type: ignore
if cc.id_b in ch_ids[cc.pd_b]:
pd = self.pd_by_name[cc.pd_b]
raise UserError(f"duplicate channel id: {cc.id_b} in protection domain: '{pd.name}' @ {pd.element._loc_str}") # type: ignore
ch_ids[cc.pd_a].add(cc.id_a)
ch_ids[cc.pd_b].add(cc.id_b)
# Ensure that all maps are correct
for pd in self.protection_domains:
for map in pd.maps:
if map.mr not in self.mr_by_name:
raise UserError(f"Invalid memory region name '{map.mr}' on '{map.element.tag}' @ {map.element._loc_str}") # type: ignore
mr = self.mr_by_name[map.mr]
extra = map.vaddr % mr.page_size
if extra != 0:
raise UserError(f"Invalid vaddr alignment on '{map.element.tag}' @ {map.element._loc_str}") # type: ignore
# Note: Overlapping memory is checked in the build.
# Ensure all memory regions are used at least once. This only generates
# warnings, not errors
check_mrs = set(self.mr_by_name.keys())
for pd in self.protection_domains:
for m in pd.maps:
if m.mr in check_mrs:
check_mrs.remove(m.mr)
for mr_ in check_mrs:
print(f"WARNING: Unused memory region: {mr_}")
def xml2mr(mr_xml: ET.Element, plat_desc: PlatformDescription) -> SysMemoryRegion:
_check_attrs(mr_xml, ("name", "size", "page_size", "phys_addr"))
name = checked_lookup(mr_xml, "name")
size = int(checked_lookup(mr_xml, "size"), base=0)
page_size_str = mr_xml.attrib.get("page_size")
page_size = min(plat_desc.page_sizes) if page_size_str is None else int(page_size_str, base=0)
if page_size not in plat_desc.page_sizes:
raise ValueError(f"page size 0x{page_size:x} not supported")
if size % page_size != 0:
raise ValueError("size is not a multiple of the page size")
paddr_str = mr_xml.attrib.get("phys_addr")
paddr = None if paddr_str is None else int(paddr_str, base=0)
if paddr is not None and paddr % page_size != 0:
raise ValueError("phys_addr is not aligned to the page size")
page_count = size // page_size
return SysMemoryRegion(name, size, page_size, page_count, paddr)
def xml2pd(pd_xml: ET.Element) -> ProtectionDomain:
_check_attrs(pd_xml, ("name", "priority", "pp", "budget", "period"))
program_image: Optional[Path] = None
name = checked_lookup(pd_xml, "name")
priority = int(pd_xml.attrib.get("priority", "0"), base=0)
if priority < 0 or priority > 254:
raise ValueError("priority must be between 0 and 254")
budget = int(pd_xml.attrib.get("budget", "1000"), base=0)
period = int(pd_xml.attrib.get("period", str(budget)), base=0)
if budget > period:
raise ValueError(f"budget ({budget}) must be less than, or equal to, period ({period})")
pp = str_to_bool(pd_xml.attrib.get("pp", "false"))
maps = []
irqs = []
setvars = []
for child in pd_xml:
try:
if child.tag == "program_image":
_check_attrs(child, ("path", ))
if program_image is not None:
raise ValueError("program_image must only be specified once")
program_image = Path(checked_lookup(child, "path"))
elif child.tag == "map":
_check_attrs(child, ("mr", "vaddr", "perms", "cached", "setvar_vaddr"))
mr = checked_lookup(child, "mr")
vaddr = int(checked_lookup(child, "vaddr"), base=0)
perms = child.attrib.get("perms", "rw")
cached = str_to_bool(child.attrib.get("cached", "true"))
maps.append(SysMap(mr, vaddr, perms, cached, child))
setvar_vaddr = child.attrib.get("setvar_vaddr")
if setvar_vaddr:
setvars.append(SysSetVar(setvar_vaddr, vaddr=vaddr))
elif child.tag == "irq":
_check_attrs(child, ("irq", "id"))
irq = int(checked_lookup(child, "irq"), base=0)
id_ = int(checked_lookup(child, "id"), base=0)
irqs.append(SysIrq(irq, id_))
elif child.tag == "setvar":
_check_attrs(child, ("symbol", "region_paddr"))
symbol = checked_lookup(child, "symbol")
region_paddr = checked_lookup(child, "region_paddr")
setvars.append(SysSetVar(symbol, region_paddr=region_paddr))
else:
raise UserError(f"Invalid XML element '{child.tag}': {child._loc_str}") # type: ignore
except ValueError as e:
raise UserError(f"Error: {e} on element '{child.tag}': {child._loc_str}") # type: ignore
if program_image is None:
raise ValueError("program_image must be specified")
return ProtectionDomain(name, priority, budget, period, pp, program_image, tuple(maps), tuple(irqs), tuple(setvars), pd_xml)
def xml2channel(ch_xml: ET.Element) -> Channel:
_check_attrs(ch_xml, ())
ends = []
for child in ch_xml:
try:
if child.tag == "end":
_check_attrs(ch_xml, ("pd", "id"))
pd = checked_lookup(child, "pd")
id_ = int(checked_lookup(child, "id"))
if id_ >= 64:
raise ValueError("id must be < 64")
if id_ < 0:
raise ValueError("id must be >= 0")
ends.append((pd, id_))
else:
raise UserError(f"Invalid XML element '{child.tag}': {child._loc_str}") # type: ignore
except ValueError as e:
raise UserError(f"Error: {e} on element '{child.tag}': {child._loc_str}") # type: ignore
if len(ends) != 2:
raise ValueError("exactly two end elements must be specified")
return Channel(ends[0][0], ends[0][1], ends[1][0], ends[1][1], ch_xml)
def _check_no_text(el: ET.Element) -> None:
if not (el.text is None or el.text.strip() == ""):
raise UserError(f"Error: unexpected text found in element '{el.tag}' @ {el._loc_str}") # type: ignore
if not (el.tail is None or el.tail.strip() == ""):
raise UserError(f"Error: unexpected text found after element '{el.tag}' @ {el._loc_str}") # type: ignore
for child in el:
_check_no_text(child)
def xml2system(filename: Path, plat_desc: PlatformDescription) -> SystemDescription:
try:
tree = ET.parse(filename, parser=LineNumberingParser(filename))
except ET.ParseError as e:
line, column = e.position
raise UserError(f"XML parse error: {filename}:{line}.{column}")
root = tree.getroot()
memory_regions = []
protection_domains = []
channels = []
# Ensure there is no non-whitespace text
_check_no_text(root)
for child in root:
try:
if child.tag == "memory_region":
memory_regions.append(xml2mr(child, plat_desc))
elif child.tag == "protection_domain":
protection_domains.append(xml2pd(child))
elif child.tag == "channel":
channels.append(xml2channel(child))
else:
raise UserError(f"Invalid XML element '{child.tag}': {child._loc_str}") # type: ignore
except ValueError as e:
raise UserError(f"Error: {e} on element '{child.tag}': {child._loc_str}") # type: ignore
except MissingAttribute as e:
raise UserError(f"Error: Missing required attribute '{e.attribute_name}' on element '{e.element.tag}': {e.element._loc_str}") # type: ignore
return SystemDescription(
memory_regions=memory_regions,
protection_domains=protection_domains,
channels=channels,
)

154
tool/sel4coreplat/util.py Normal file
View File

@ -0,0 +1,154 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
from dataclasses import dataclass
from typing import List, Optional
class UserError(Exception):
pass
def kb(n: int) -> int:
return n * 1024
def mb(n: int) -> int:
return n * 1024 * 1024
def msb(x: int) -> int:
return x.bit_length() - 1
def lsb(x: int) -> int:
return msb(x & -x)
def round_up(n: int, x: int) -> int:
d, m = divmod(n, x)
return n if m == 0 else n + x - m
def round_down(n: int, x: int) -> int:
d, m = divmod(n, x)
return n if m == 0 else n - m
def mask_bits(n: int, bits: int) -> int:
"""mask out (set to zero) the lower bits from n"""
assert n > 0
return (n >> bits) << bits
def is_power_of_two(n: int) -> bool:
"""Return True if n is a power of two."""
assert n > 0
return n & (n - 1) == 0
def str_to_bool(s: str) -> bool:
if s.lower() == "true":
return True
elif s.lower() == "false":
return False
raise ValueError("invalid boolean value")
@dataclass
class MemoryRegion:
# Note: base is inclusive, end is exclusive
# MemoryRegion(1, 5) would have a size of 4
# and cover [1, 2, 3, 4]
base: int
end: int
def aligned_power_of_two_regions(self) -> List["MemoryRegion"]:
max_bits = 40
# Align
# find the first bit self
r = []
base = self.base
end = self.end
while base != end:
size = end - base
size_bits = msb(size)
if base == 0:
bits = size_bits
else:
bits = min(size_bits, lsb(base))
if bits > max_bits:
bits = max_bits
sz = 1 << bits
r.append(MemoryRegion(base, base + sz))
base += sz
return r
def __repr__(self) -> str:
return f"MemoryRegion(base=0x{self.base:x}, end=0x{self.end:x})"
@property
def size(self) -> int:
return self.end - self.base
class DisjointMemoryRegion:
def __init__(self) -> None:
self._regions: List[MemoryRegion] = []
self._check()
def _check(self) -> None:
# Ensure that regions are sorted and non-overlapping
last_end: Optional[int] = None
for region in self._regions:
if last_end is not None:
assert region.base >= last_end
last_end = region.end
def dump(self) -> None:
for region in self._regions:
print(f" {region.base:016x} - {region.end:016x}")
def insert_region(self, base: int, end: int) -> None:
# Find where it belongs
for idx, region in enumerate(self._regions):
if end < region.base:
break
else:
idx = len(self._regions)
# FIXME: Should extend here if adjacent rather than
# inserting now
self._regions.insert(idx, MemoryRegion(base, end))
self._check()
def remove_region(self, base: int, end: int) -> None:
for idx, region in enumerate(self._regions):
if base >= region.base and end <= region.end:
break
else:
raise Exception("Attempting to remove region that is not currently covered")
if region.base == base and region.end == end:
# Covers exactly, so just remove
del self._regions[idx]
elif region.base == base:
# Trim the start of the region
self._regions[idx] = MemoryRegion(end, region.end)
elif region.end == end:
# Trim end of the region
self._regions[idx] = MemoryRegion(region.base, base)
else:
# Splitting
self._regions[idx] = MemoryRegion(region.base, base)
self._regions.insert(idx + 1, MemoryRegion(end, region.end))
self._check()
def aligned_power_of_two_regions(self) -> List[MemoryRegion]:
r = []
for region in self._regions:
r += region.aligned_power_of_two_regions()
return r

146
tool/test/__init__.py Normal file
View File

@ -0,0 +1,146 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
from pathlib import Path
import unittest
from sel4coreplat.sysxml import xml2system, UserError, PlatformDescription
plat_desc = PlatformDescription(
page_sizes = [0x1_000, 0x200_000]
)
def _file(filename: str) -> Path:
return Path(__file__).parent / filename
class ExtendedTestCase(unittest.TestCase):
def assertStartsWith(self, v, check):
self.assertTrue(v.startswith(check), f"'{v}' does not start with '{check}'")
def _check_error(self, filename, message):
with self.assertRaises(UserError) as e:
xml2system(_file(filename), plat_desc)
self.assertStartsWith(str(e.exception), message)
def _check_missing(self, filename, attr, element):
expected_message = f"Error: Missing required attribute '{attr}' on element '{element}'"
self._check_error(filename, expected_message)
class MemoryRegionParseTests(ExtendedTestCase):
def test_malformed_size(self):
self._check_error("mr_malformed_size.xml", "Error: invalid literal for int() with base 0: '0x200_000sd' on element 'memory_region'")
def test_unsupported_page_size(self):
self._check_error("mr_unsupported_page_size.xml", "Error: page size 0x200001 not supported on element 'memory_region'")
def test_size_not_multiple_of_page_size(self):
self._check_error("mr_size_not_multiple_of_page_size.xml", "Error: size is not a multiple of the page size on element 'memory_region'")
def test_addr_not_aligned_to_page_size(self):
self._check_error("mr_addr_not_aligned_to_page_size.xml", "Error: phys_addr is not aligned to the page size on element 'memory_region'")
def test_missing_size(self):
self._check_missing("mr_missing_size.xml", "size", "memory_region")
def test_missing_name(self):
self._check_missing("mr_missing_name.xml", "name", "memory_region")
def test_invalid_attrs(self):
self._check_error("mr_invalid_attrs.xml", "Error: invalid attribute 'page_count' on element 'memory_region': ")
class ProtectionDomainParseTests(ExtendedTestCase):
def test_missing_name(self):
self._check_missing("pd_missing_name.xml", "name", "protection_domain")
def test_missing_path(self):
self._check_missing("pd_missing_path.xml", "path", "program_image")
def test_missing_mr(self):
self._check_missing("pd_missing_mr.xml", "mr", "map")
def test_missing_vaddr(self):
self._check_missing("pd_missing_vaddr.xml", "vaddr", "map")
def test_missing_irq(self):
self._check_missing("pd_missing_irq.xml", "irq", "irq")
def test_missing_id(self):
self._check_missing("pd_missing_id.xml", "id", "irq")
def test_missing_symbol(self):
self._check_missing("pd_missing_symbol.xml", "symbol", "setvar")
def test_missing_region_paddr(self):
self._check_missing("pd_missing_region_paddr.xml", "region_paddr", "setvar")
def test_duplicate_program_image(self):
self._check_error("pd_duplicate_program_image.xml", "Error: program_image must only be specified once on element 'program_image': ")
def test_invalid_attrs(self):
self._check_error("pd_invalid_attrs.xml", "Error: invalid attribute 'foo' on element 'protection_domain': ")
def test_program_image_invalid_attrs(self):
self._check_error("pd_program_image_invalid_attrs.xml", "Error: invalid attribute 'foo' on element 'program_image': ")
def test_budget_gt_period(self):
self._check_error("pd_budget_gt_period.xml", "Error: budget (1000) must be less than, or equal to, period (100) on element 'protection_domain':")
class ChannelParseTests(ExtendedTestCase):
def test_missing_pd(self):
self._check_missing("ch_missing_pd.xml", "pd", "end")
def test_missing_id(self):
self._check_missing("ch_missing_id.xml", "id", "end")
def test_id_greater_than_63(self):
self._check_error("ch_id_greater_than_63.xml", "Error: id must be < 64 on element 'end'")
def test_id_less_than_0(self):
self._check_error("ch_id_less_than_0.xml", "Error: id must be >= 0 on element 'end'")
def test_invalid_attrs(self):
self._check_error("ch_invalid_attrs.xml", "Error: invalid attribute 'foo' on element 'channel': ")
class SystemParseTests(ExtendedTestCase):
def test_duplicate_pd_names(self):
self._check_error("sys_duplicate_pd_name.xml", "Duplicate protection domain name 'test'.")
def test_duplicate_mr_names(self):
self._check_error("sys_duplicate_mr_name.xml", "Duplicate memory region name 'test'.")
def test_channel_invalid_pd(self):
self._check_error("sys_channel_invalid_pd.xml", "Invalid pd name 'invalidpd'. on element 'channel': ")
def test_duplicate_irq_number(self):
self._check_error("sys_duplicate_irq_number.xml", "duplicate irq: 112 in protection domain: 'test2' @ ")
def test_duplicate_irq_id(self):
self._check_error("sys_duplicate_irq_id.xml", "duplicate channel id: 3 in protection domain: 'test1' @")
def test_channel_duplicate_a_id(self):
self._check_error("sys_channel_duplicate_a_id.xml", "duplicate channel id: 5 in protection domain: 'test1' @")
def test_channel_duplicate_b_id(self):
self._check_error("sys_channel_duplicate_b_id.xml", "duplicate channel id: 5 in protection domain: 'test2' @")
def test_no_protection_domains(self):
self._check_error("sys_no_protection_domains.xml", "At least one protection domain must be defined")
def test_text_elements(self):
self._check_error("sys_text_elements.xml", "Error: unexpected text found in element 'system' @")
def test_map_invalid_mr(self):
self._check_error("sys_map_invalid_mr.xml", "Invalid memory region name 'foos' on 'map' @ ")
def test_map_not_aligned(self):
self._check_error("sys_map_not_aligned.xml", "Invalid vaddr alignment on 'map' @ ")
def test_too_many_pds(self):
self._check_error("sys_too_many_pds.xml", "Too many protection domains (64) defined. Maximum is 63.")

18
tool/test/ch_id_greater_than_63.xml Normal file
View File

@ -0,0 +1,18 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
</protection_domain>
<channel>
<end pd="test1" id="64"/>
<end pd="test2" id="5"/>
</channel>
</system>

18
tool/test/ch_id_less_than_0.xml Normal file
View File

@ -0,0 +1,18 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
</protection_domain>
<channel>
<end pd="test1" id="-1"/>
<end pd="test2" id="5"/>
</channel>
</system>

18
tool/test/ch_invalid_attrs.xml Normal file
View File

@ -0,0 +1,18 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
</protection_domain>
<channel foo="bar">
<end pd="test1" id="-1"/>
<end pd="test2" id="5"/>
</channel>
</system>

18
tool/test/ch_missing_id.xml Normal file
View File

@ -0,0 +1,18 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
</protection_domain>
<channel>
<end pd="test1"/>
<end pd="test2" id="5"/>
</channel>
</system>

18
tool/test/ch_missing_pd.xml Normal file
View File

@ -0,0 +1,18 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
</protection_domain>
<channel>
<end id="5"/>
<end pd="test2" id="5"/>
</channel>
</system>

9
tool/test/mr_addr_not_aligned_to_page_size.xml Normal file
View File

@ -0,0 +1,9 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="eth_outer_output" size="0x200_000" page_size="0x200_000" phys_addr="0x201_000" />
</system>

10
tool/test/mr_invalid_attrs.xml Normal file
View File

@ -0,0 +1,10 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="eth_outer_output" size="0x200_000" page_size="0x200_000" page_count="123" />
<protection_domain name="test"><program_image path="test" /></protection_domain>
</system>

9
tool/test/mr_malformed_size.xml Normal file
View File

@ -0,0 +1,9 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="eth_outer_output" size="0x200_000sd" page_size="0x200_000" />
</system>

9
tool/test/mr_missing_name.xml Normal file
View File

@ -0,0 +1,9 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region size="0x200_000" page_size="0x200_000" />
</system>

9
tool/test/mr_missing_size.xml Normal file
View File

@ -0,0 +1,9 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="eth_outer_output" page_size="0x200_000" />
</system>

9
tool/test/mr_size_not_multiple_of_page_size.xml Normal file
View File

@ -0,0 +1,9 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="eth_outer_output" size="0x200_001" page_size="0x200_000" />
</system>

9
tool/test/mr_unsupported_page_size.xml Normal file
View File

@ -0,0 +1,9 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="eth_outer_output" size="0x200_000" page_size="0x200_001" />
</system>

11
tool/test/pd_budget_gt_period.xml Normal file
View File

@ -0,0 +1,11 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test" budget="1000" period="100">
<program_image path="test" />
</protection_domain>
</system>

13
tool/test/pd_duplicate_program_image.xml Normal file
View File

@ -0,0 +1,13 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="test_mr" size="0x1_000" />
<protection_domain name="test">
<program_image path="test" />
<program_image path="test" />
</protection_domain>
</system>

11
tool/test/pd_invalid_attrs.xml Normal file
View File

@ -0,0 +1,11 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test" foo="bar">
<program_image path="test" />
</protection_domain>
</system>

12
tool/test/pd_missing_id.xml Normal file
View File

@ -0,0 +1,12 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test">
<program_image path="test" />
<irq irq="5" />
</protection_domain>
</system>

12
tool/test/pd_missing_irq.xml Normal file
View File

@ -0,0 +1,12 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test">
<program_image path="test" />
<irq id="37" />
</protection_domain>
</system>

13
tool/test/pd_missing_mr.xml Normal file
View File

@ -0,0 +1,13 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="test_mr" size="0x1_000" />
<protection_domain name="test">
<program_image path="test" />
<map vaddr="0x3_000_000" perms="rw" cached="false" />
</protection_domain>
</system>

11
tool/test/pd_missing_name.xml Normal file
View File

@ -0,0 +1,11 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain>
<program_image path="dummy.elf" />
</protection_domain>
</system>

11
tool/test/pd_missing_path.xml Normal file
View File

@ -0,0 +1,11 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test">
<program_image />
</protection_domain>
</system>

13
tool/test/pd_missing_region_paddr.xml Normal file
View File

@ -0,0 +1,13 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="test_mr" size="0x1_000" />
<protection_domain name="test">
<program_image path="test" />
<setvar symbol="foo" />
</protection_domain>
</system>

13
tool/test/pd_missing_symbol.xml Normal file
View File

@ -0,0 +1,13 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="test_mr" size="0x1_000" />
<protection_domain name="test">
<program_image path="test" />
<setvar region_paddr="test_mr" />
</protection_domain>
</system>

13
tool/test/pd_missing_vaddr.xml Normal file
View File

@ -0,0 +1,13 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="test_mr" size="0x1_000" />
<protection_domain name="test">
<program_image path="test" />
<map mr="test_mr" perms="rw" cached="false" />
</protection_domain>
</system>

11
tool/test/pd_program_image_invalid_attrs.xml Normal file
View File

@ -0,0 +1,11 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test">
<program_image path="test" foo="bar"/>
</protection_domain>
</system>

19
tool/test/sys_channel_duplicate_a_id.xml Normal file
View File

@ -0,0 +1,19 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
<irq irq="112" id="5" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
</protection_domain>
<channel>
<end pd="test1" id="5"/>
<end pd="test2" id="5"/>
</channel>
</system>

19
tool/test/sys_channel_duplicate_b_id.xml Normal file
View File

@ -0,0 +1,19 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
<irq irq="112" id="5" />
</protection_domain>
<channel>
<end pd="test1" id="4"/>
<end pd="test2" id="5"/>
</channel>
</system>

18
tool/test/sys_channel_invalid_pd.xml Normal file
View File

@ -0,0 +1,18 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
</protection_domain>
<channel>
<end pd="invalidpd" id="5"/>
<end pd="test2" id="5"/>
</channel>
</system>

13
tool/test/sys_duplicate_irq_id.xml Normal file
View File

@ -0,0 +1,13 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
<irq irq="111" id="3" />
<irq irq="112" id="3" />
</protection_domain>
</system>

16
tool/test/sys_duplicate_irq_number.xml Normal file
View File

@ -0,0 +1,16 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test1">
<program_image path="test" />
<irq irq="112" id="3" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
<irq irq="112" id="3" />
</protection_domain>
</system>

13
tool/test/sys_duplicate_mr_name.xml Normal file
View File

@ -0,0 +1,13 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="test" size="0x200_000" page_size="0x200_000" />
<memory_region name="test" size="0x200_000" page_size="0x200_000" />
<protection_domain name="test">
<program_image path="test" />
</protection_domain>
</system>

14
tool/test/sys_duplicate_pd_name.xml Normal file
View File

@ -0,0 +1,14 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test">
<program_image path="test" />
</protection_domain>
<protection_domain name="test">
<program_image path="test" />
</protection_domain>
</system>

17
tool/test/sys_map_invalid_mr.xml Normal file
View File

@ -0,0 +1,17 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="foo" size="0x1_000" />
<protection_domain name="test1">
<program_image path="test" />
<map mr="foo" vaddr="0x20_000" />
</protection_domain>
<protection_domain name="test2">
<program_image path="test" />
<map mr="foos" vaddr="0x20_000" />
</protection_domain>
</system>

13
tool/test/sys_map_not_aligned.xml Normal file
View File

@ -0,0 +1,13 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<memory_region name="foo" size="0x1_000" />
<protection_domain name="test1">
<program_image path="test" />
<map mr="foo" vaddr="0x20_001" />
</protection_domain>
</system>

8
tool/test/sys_no_protection_domains.xml Normal file
View File

@ -0,0 +1,8 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
</system>

12
tool/test/sys_text_elements.xml Normal file
View File

@ -0,0 +1,12 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
asdf
<protection_domain name="foo">
<program_image path="foo" />
</protection_domain>
</system>

72
tool/test/sys_too_many_pds.xml Normal file
View File

@ -0,0 +1,72 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="test00"><program_image path="foo" /></protection_domain>
<protection_domain name="test01"><program_image path="foo" /></protection_domain>
<protection_domain name="test02"><program_image path="foo" /></protection_domain>
<protection_domain name="test03"><program_image path="foo" /></protection_domain>
<protection_domain name="test04"><program_image path="foo" /></protection_domain>
<protection_domain name="test05"><program_image path="foo" /></protection_domain>
<protection_domain name="test06"><program_image path="foo" /></protection_domain>
<protection_domain name="test07"><program_image path="foo" /></protection_domain>
<protection_domain name="test08"><program_image path="foo" /></protection_domain>
<protection_domain name="test09"><program_image path="foo" /></protection_domain>
<protection_domain name="test10"><program_image path="foo" /></protection_domain>
<protection_domain name="test11"><program_image path="foo" /></protection_domain>
<protection_domain name="test12"><program_image path="foo" /></protection_domain>
<protection_domain name="test13"><program_image path="foo" /></protection_domain>
<protection_domain name="test14"><program_image path="foo" /></protection_domain>
<protection_domain name="test15"><program_image path="foo" /></protection_domain>
<protection_domain name="test16"><program_image path="foo" /></protection_domain>
<protection_domain name="test17"><program_image path="foo" /></protection_domain>
<protection_domain name="test18"><program_image path="foo" /></protection_domain>
<protection_domain name="test19"><program_image path="foo" /></protection_domain>
<protection_domain name="test20"><program_image path="foo" /></protection_domain>
<protection_domain name="test21"><program_image path="foo" /></protection_domain>
<protection_domain name="test22"><program_image path="foo" /></protection_domain>
<protection_domain name="test23"><program_image path="foo" /></protection_domain>
<protection_domain name="test24"><program_image path="foo" /></protection_domain>
<protection_domain name="test25"><program_image path="foo" /></protection_domain>
<protection_domain name="test26"><program_image path="foo" /></protection_domain>
<protection_domain name="test27"><program_image path="foo" /></protection_domain>
<protection_domain name="test28"><program_image path="foo" /></protection_domain>
<protection_domain name="test29"><program_image path="foo" /></protection_domain>
<protection_domain name="test30"><program_image path="foo" /></protection_domain>
<protection_domain name="test31"><program_image path="foo" /></protection_domain>
<protection_domain name="test32"><program_image path="foo" /></protection_domain>
<protection_domain name="test33"><program_image path="foo" /></protection_domain>
<protection_domain name="test34"><program_image path="foo" /></protection_domain>
<protection_domain name="test35"><program_image path="foo" /></protection_domain>
<protection_domain name="test36"><program_image path="foo" /></protection_domain>
<protection_domain name="test37"><program_image path="foo" /></protection_domain>
<protection_domain name="test38"><program_image path="foo" /></protection_domain>
<protection_domain name="test39"><program_image path="foo" /></protection_domain>
<protection_domain name="test40"><program_image path="foo" /></protection_domain>
<protection_domain name="test41"><program_image path="foo" /></protection_domain>
<protection_domain name="test42"><program_image path="foo" /></protection_domain>
<protection_domain name="test43"><program_image path="foo" /></protection_domain>
<protection_domain name="test44"><program_image path="foo" /></protection_domain>
<protection_domain name="test45"><program_image path="foo" /></protection_domain>
<protection_domain name="test46"><program_image path="foo" /></protection_domain>
<protection_domain name="test47"><program_image path="foo" /></protection_domain>
<protection_domain name="test48"><program_image path="foo" /></protection_domain>
<protection_domain name="test49"><program_image path="foo" /></protection_domain>
<protection_domain name="test50"><program_image path="foo" /></protection_domain>
<protection_domain name="test51"><program_image path="foo" /></protection_domain>
<protection_domain name="test52"><program_image path="foo" /></protection_domain>
<protection_domain name="test53"><program_image path="foo" /></protection_domain>
<protection_domain name="test54"><program_image path="foo" /></protection_domain>
<protection_domain name="test55"><program_image path="foo" /></protection_domain>
<protection_domain name="test56"><program_image path="foo" /></protection_domain>
<protection_domain name="test57"><program_image path="foo" /></protection_domain>
<protection_domain name="test58"><program_image path="foo" /></protection_domain>
<protection_domain name="test59"><program_image path="foo" /></protection_domain>
<protection_domain name="test60"><program_image path="foo" /></protection_domain>
<protection_domain name="test61"><program_image path="foo" /></protection_domain>
<protection_domain name="test62"><program_image path="foo" /></protection_domain>
<protection_domain name="test63"><program_image path="foo" /></protection_domain>
</system>