43 Commits

Author SHA1 Message Date
julia
f9eb65c9a5 tools: don't exclude device-tree reserved memory
... from the device UT listed by platform_gen. The kernel itself
does not care about this memory, and it is just given as device UT.

We also just remove the reserved array entirely from the return of
`get_physical_memory` since it only seems to be a footgun, it's
only used internally to affect what memory the kernel wants to use.

Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: julia <git.ts@trainwit.ch>
2025-10-16 11:05:15 +01:00
julia
97b25da8b1 tools: keep align-reserved memory in 'devices'
`align_memory()` in hardware.py both modifies the first normal memory
region to adjust the base of it for alignment, and adds an extra
reserved region to our list of reserved regions. This then feeds
through `get_addrspace_exclude` which inverts the regions given
and turns it into the available "device memory" at user-level.

    dev_mem = hardware.utils.memory.get_addrspace_exclude(
        list(reserved) + phys_mem + kernel_devs, config)

Anything as an argument to this is not given as "device memory" by
the kernel. (It does not precisely match how the kernel works).

However, since `align_memory()` has adjusted both the phys_mem up
(which *would* have added this region as "device" memory) but also
added it to "reserved" region, which then made it disappear entirely,
as "reserved" regions are not exposed to userspace.

However, this **does not** match the behaviour of the kernel, as it was
not reserved, so this behaviour did not match the untypeds given to
userspace. This commit solves this by removing the extra reserved
region being added for that memory.

PR #1426 worked around this issue by removing the alignment on AArch64.
Whilst this fixed the issue that microkit was seeing, it just masked
the underlying issue. Reverting that PR, then applying this fix,
results in the following platform_gen.yaml:

    devices:
    - end: 0x1000000
      start: 0x0
    - end: 0xff800000
      start: 0x3b400000
    - end: 0xff841000
      start: 0xff801000
    - end: 0x100000000000
      start: 0xff843000
    memory:
    - end: 0x3b400000
      start: 0x1000000

Note especially the device region from 0x0 to 0x1000000; which is the
combination of the 0x0 to 0x1000 reserved region, and the 0x1000 to
0x1000000 reserved by the kernel's alignment requirement. Previously,
the platform_gen.yaml reported only the 0x0 to 0x1000 region,

    devices:
    - end: 0x1000
      start: 0x0
    - end: 0xff800000
      start: 0x3b400000
    - end: 0xff841000
      start: 0xff801000
    - end: 0x100000000000
      start: 0xff843000
    memory:
    - end: 0x3b400000
      start: 0x1000000

I will be following this commit up with a PR to instead make the
alignment-reserved region into a new memory region, since there's not
any reason why userspace can't use this memory.

This has been tested on a few platforms with sel4test and with
microkit on the pi4B.

Signed-off-by: julia <git.ts@trainwit.ch>
2025-10-16 11:05:15 +01:00
Ivan-Velickovic
53ed1bef7b tools: fix kernel physBase alignment on AArch64
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
2025-03-13 19:01:05 +11:00
Kent McLeod
b657e50b66 RISC-V: reserve memory for SBI in device tree
Instead of special handling for the SBI region in the kernel, which can
be platform specific, treat it as a reserved memory region in the device
tree which is sufficient to prevent the kernel from turning the reserved
region into kernel untyped caps.

Signed-off-by: Kent McLeod <kent@kry10.com>
2025-03-03 14:35:04 +11:00
Ivan-Velickovic
1cbaeb97f0 platform_gen: only generate regions that are used
Right now the `platform_gen.json` and `platform_gen.yaml` files contain
regions that are not actually used by the kernel. This is fine for
`platform_gen.h` because they are guarded by #ifdefs with kernel config
defines but the same approach does not work for YAML and JSON.

So, this patch changes the Python scripts that generate this files so
that they only generate the regions that actually end up being used.

Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
2025-02-10 12:48:13 +11:00
Gerwin Klein
9a22e40b46 config.py: update comment to reflect kernel assert
The ELF loader may well be satisfied with a smaller alignment, but the
compile time assert in the kernel requires super section alignment for
physBase.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2024-06-30 12:45:37 +10:00
Gerwin Klein
c7822a1c1c config.py: fix SUPERSECTION_BITS for arm_hyp
This addresses #1186

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2024-06-30 12:45:37 +10:00
Ivan-Velickovic
e1bdd809b6 Output JSON for hardware configuration
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
2023-08-13 08:59:55 +10:00
Rafal Kolanski
65a1b457a4 make physBase a static inline function
For verification flexible w.r.t kernel placement in physical memory, we
need to relate physBase as a named constant to its abstract equivalent.
Unfortunately, apart from enums, the C programming language does not
have real constants. The C parser follows the C standard and requires
enums constants to be storable as int, meaning without major overhaul
enums are not sufficient for storing word_t-sized memory addresses.

Since the linker scripts can't deal with static inline functions
in the constants they need (KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE),
we provide the following preprocessor definitions for the linker
specifically:
* PHYS_BASE_RAW (the numerical value returned by physBase())
* KERNEL_ELF_BASE_RAW
* KERNEL_ELF_PADDR_BASE_RAW

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-03-07 14:29:14 +11:00
Ahmed Charles
c92b3b3163 Add __repr__ for WrappedNode
Signed-off-by: Ahmed Charles <acharles@outlook.com>
2022-07-20 16:37:33 +10:00
Axel Heider
c036e6c676 python: use KernelSel4Arch instead of KernelArch
Drop optional parameter 'arch' and make 'sel4arch' a required parameter
to avoid implicit assumptions.

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-12-03 10:26:41 +11:00
Axel Heider
e75d22bedd python: align imports
Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Axel Heider
88be9c1f7c python: add helper functions
Separate parameter collection from the actual file creation.

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Axel Heider
42736a335f python: avoid name conflicts with module name
Also cleanup/align variable naming.

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Axel Heider
f4e38b1e5b python: make Region parameter owner optional
Also ensure the description is created correctly.

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Axel Heider
a16ec5ef7f python: add type information
Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Axel Heider
a0c5020789 python: trivial script cleanup
Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Axel Heider
d31019ff0a python: cleanup devices_gen.h template
Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Axel Heider
bac15924ad python: clarify includes in devices_gen.h template
Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Axel Heider
94963c7bec python: update creator info comment
Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-11-14 11:44:00 +11:00
Kent McLeod
18a3fb3bae hardware.py: Create smaller UT at end of addresses
At the end of the physical address range, the last address isn't turned
into an UT object. The scripts generating the memory regions
unnecessarily round down to a small page size when they could instead
round down to the smallest UT size and this memory could be used for
smaller kernel objects.

Signed-off-by: Kent McLeod <kent@kry10.com>
2021-10-03 10:10:43 +11:00
Axel Heider
77fb21aa90 python: add __str__() for Region
- Provide a nicer string for debugging purposes.
- improve comments about the purpose of __repr__() and __str__()

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-09-27 23:09:24 +10:00
Axel Heider
7d7a404bff python: raise exceptions on errors
- A region can't be created from an invalid range
- A region might be too small to support the change. There is no trivial
  way to fix this.

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-09-27 20:49:56 +10:00
Bertrand Virfollet
b32b9568b2 tools: merge adjacent memory regions
Merge memory regions before checking for reserved areas

Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Bertrand Virfollet <bvirfollet@silicom.fr>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2021-09-08 07:53:53 +10:00
Axel Heider
da0aad0330 make kernel device frame handling more generic
The structure actually describes kernel frames and not kernel devices.
In most of the cases a peripherals will fit into one page, but some can
need more pages. On some platform there are no kernel devices at all.
Provides the macro NUM_KERNEL_DEVICE_FRAMES as simple way to find out if
there are mapping that hides the corner cases. This eventually allows
implementing a generic handling even on RISC-V without much overhead, so
the hack for HiFive/Spike can be removed.

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-08-27 21:15:11 +10:00
Axel Heider
048c84fb94 use explicit field names in generated code
Using explicit field name in the assignment states more clearly what the
generated code does. It is also more robust and allows the compiler to
catch potential inconsistencies in case the structure details change.

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-08-27 21:15:11 +10:00
Axel Heider
69204d0d2e trivial: break long lines in comment
Improve readability by breaking the line at around 80 chars.

Signed-off-by: Axel Heider <axelheider@gmx.de>
2021-08-27 21:15:11 +10:00
Gerwin Klein
7f562e1633 tools: consolidate RISC-V + Arm memory base logic
Co-authored-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Co-authored-by: Axel Heider <axel-h@users.noreply.github.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2021-08-24 18:04:43 +10:00
Gerwin Klein
2296484665 tools: add risc-v dtb interrupt parsing
Co-authored-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2021-08-24 18:04:43 +10:00
Axel Heider
d0a3b28005 risc-v: avoid warning about interrupt parsing
Avoid the warning 'WARNING:root:Not sure how to parse interrupts for
"/cpus/cpu@0/interrupt-controller"' when building for platform hifive.

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
2021-08-24 10:04:56 +10:00
Kent McLeod
379bf5abe3 hardware_gen.py: Address some warning messages
CMake treats any text output that is generated by tools during the
configuration phase as important if it isn't part of a message(STATUS)
command. Output generated by hardware_gen.py often shows up as warnings
about device tree properties that are usually uninformative. Resolving
some of the warning conditions removes these messages for most
platforms.

- Setting kernel_size in hardware.yml to 0x1000 to handle cases where
  the kernel only needs the first page of a device that has a
  device-tree definition larger than that.
- Remove status print about each Interrupt processed as it's usually not
  useful information.
- Only process IRQs for a selected kernel device if the rule for that
  device has any interrupt queries. This prevents warnings for IRQ
  controllers that the script doesn't know how to process when it
  doesn't need to.

Signed-off-by: Kent McLeod <kent@kry10.com>
2021-07-29 16:03:01 +10:00
Axel Heider
d1fb5c01a7 use '#pragma once' include guards
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
2021-06-20 11:53:58 +10:00
Axel Heider
d486bc0b5a Add i.MX6 Nitrogen6_SoloX board
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
2021-03-31 13:38:25 +10:00
Alistair Francis
0972c4e9a9 RISC-V: Replace mentions of BBL with OpenSBI
Signed-off-by: Alistair Francis <alistair.francis@wdc.com>
2021-03-09 11:20:57 +11:00
Curtis Millar
ab3d8c44cb riscv: Map devices with large pages on 32 & 64-bit
For 64-bit, this adds a 2nd-level page table for mapping devices using
2MiB frames instead of 1GiB frames.

The boot mapping and hardware header generator have also been fixed to
correctly report the number of large frames needed for devices rather
than only reporting the first. The frame size is also specified
correctly (rather than assuming mapping with 4KiB frames).

This likely fixes an issue whereby only the first 4KiB frame of a device
was reserved but the remaining region of that kernel device could be
mapped at user level.

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
2020-12-03 10:31:16 +11:00
Stefan O'Rear
a91e979c5a clang: Fix errors on zero kernel devices
"const TYPE *ptr" creates a non-const pointer to const data; for the
pointer itself to be rodata requires "TYPE *const ptr".

Taking the size of the pointer is caught by -Werror by default; suppress
that.

Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
2020-08-26 14:21:35 +10:00
Axel Heider
fb71ef926a tools: fix brackets in format parameters
Signed-off-by: Axel Heider <axelheider@gmx.de>
2020-06-02 23:41:15 +02:00
Gerwin Klein
79da079239 Convert license tags to SPDX identifiers
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
2020-03-09 13:21:49 +08:00
Simon Shields
0f61978058 hardware_gen: add elfloader CPUs output
outputs all CPUs described in the DT to the elfloader
header and also includes any devices in the seL4,elfoader-devices
property.
2019-12-16 14:29:05 +11:00
Simon Shields
7eb4147e43 hardware_gen: add elfloader output
The elfloader is going to start using devices based on the device tree.
Add an output method for hardware_gen.py that generates header files
that the elfloader can use. Currently they contain an array of
"devices", where each device has a compatiblity string and a series of
regions (represented simply as the physical address of the region).

For now, the elfloader only uses the serial device specified by the
stdout-path property in the DTB.
2019-12-11 13:50:26 +11:00
Victor Phan
66bc2b1724 rename KDEV_PPTR/PPTR_KDEV to KDEV_BASE
This is the virtual address for the start of the kernel device mapping
region.
2019-11-21 15:53:11 +11:00
Simon Shields
b5c56244f1 Create device untypeds at boot for all arches
Currently on x86 device untypeds are generated by passing the entire
address space minus any parts that are reserved by the kernel or that
are "real" memory (e.g. kernel image, physical RAM).

On ARM and RISC-V, device untypeds were generated at compile-time from
a device tree. This patch moves ARM and RISC-V to use the same approach
as x86, and moves the code from x86 into a common location that's
shared between the three architectures.

Co-Authored-By: Anna Lyons <anna@gh.st>
2019-11-12 16:20:07 +11:00
Simon Shields
75f2c54b42 tools: rewrite hardware_gen.py
This is almost a complete rewrite from the old hardware_gen.py.

It separates the 'parse DT' stage from the 'generate output'
devices more strictly, and is hopefully easier to understand and
easier to extend.

We also no longer generate the 'devices' list (in YAML)
or the dev_p_regs array (in C), as the kernel will implicitly
expose all non-RAM untypeds as devices.
2019-11-12 16:18:33 +11:00