init_freemem sets up available regions of memory for the hardware that
seL4 is booting on. Previously this function was duplicated across
architectures, with minor duplication.
This change provides a top-level init_freemem suitable for all
architectures.
- arm/riscv: change get_avail_p_reg to return whole p_reg array
- update all architectures to use new init_freemem.
- wrap init_freemem calls with arch_init_freemem for each arch, where
arch_init_freemem sets up the available and reserved regions of memory
which are passed to init_freemem.
The memory used for the irq cnode is never available to the user. As a
result this memory can be allocated statically, simplifying the
bootcode.
- remove allocation of irq cnode
- add static init
- generate irq cnode size from cmake for arm
- add static constants for riscv, x86 as there is no variability at the
moment.
This allows for arm headers to be generated for an arm platform
in include/plat/default that specifies the following:
- maxIRQ
- TIMER_CLOCK_HZ
- the timer header to use
- the interrupt controller header to use
This commit updates the ia32 build to pass the c-parser.
- replaces ++i with i++
- use void in functions with no parameters
- add a missing typecast
- remove a void cast of an unused variable
It does not provide any verification guarantees about ia32 code.
The SBI memory was mapped outside the kernel window. This would trigger
an instruction access fault on some hardware, when the bootloader has set
up PMP to protect the SBI memory. Instead of protecting a particular memory
region, the PMP locks the entire page table entry that covers the region.
The PADDR_LOAD and kernel base are adjusted to have the SBI memory
included in the kernel window. So that the SBI memory can be mapped as
part of the kernel image to a separate page table entry. This also
avoids the kernel to allocate untyped memory from the SBI region.
These files can be included normally using libsel4 include paths. This
removes situations where the same file is available under different
include paths due to symlinking into different directory structures.
The C parser produces abbreviations for local variables that depend on
the variable type and the order they appear in the source.
The signature for `get_avail_p_reg` on RISCV has a different type for
`i` than every other function, which causes issues when `hardware.h` is
included early in `kernel_all.c_pp`. Changing the type to `word_t`
avoids these issues.
Note that the auto-generated kernel_devices will differ slightly from
the ones present in the kernel until now. When devices have
registers that aren't page-aligned we now always set the appropriate
PPTR to be the start address of the device, while previously the PPTR
was sometimes page-aligned.
Specifically, this change to PPTRs affects:
- bcm2837 intc
- bcm2837 uart
- allwinnerA20 timer
* Also document the reason why the particular address for KS_LOG_PPTR was chosen.
This patch adds a pointer to the PD entry that sets the benchmark log frame.
