This corrects the calculation of the L2 bitmap size to correctly handle cases where the
requested num priorities is not a clean multiple of the wordBits
This commit generalises 32 and 64 bit configuration for arm: 32bit uses
coprocessor access through mrc/mcr, 64bit system configuration through
msr,mrs
- SYSTEM_READ|WRITE_WORD: read or write configuration word
- SYSTEM_READ|WRITE_64 : read or write 64bits of configuration
`Arch_checkIRQ` already prints an error message in the case of x86. Printing the additional
error message is both unnecessary, confusing as the message makes no sense on x86. As the
error does make sense on ARM this commit moves the message to the arm `Arch_checkIRQ`
The CParser can't deduce modifies rules for functions without
definitions (like in8, out8 et al and interrupt handler functions).
This adds explicit modifies rules for these functions.
This provides a more robust and efficient implementation that only forces memory reloads
at explicit known points, instead of the over approximation of every time they are
accessed that is forced by volatile.
Adds a named constant of the IPC buffer size bits that can be used when checking the
size/alignment of an IPC buffer. This constant has a compile time assertion to ensure
it corresponds to the actual IPC buffer
This unifies the badge size of endpoints and notifications on 64-bit platforms to a
consistent 64-bits, and also changes the libsel4 definitions to match for both.
The maximum guard size was unnecessarily restricted to 18 bits as it is on 32-bit
platforms. This change increases it to the current maximum possible of 58 bits.
The 58-bit limitation exists due to the need to encode a guard+guardsize into a
single word for cnode invocations.
This data structure is meant to be the user visible format of the data for a cnode_cap,
yet it is defined in a kernel only bitfield file. Moving it to libsel4 opens up the
possibility of consolidating the definitions in libsel4
Zombie caps perform bit packing that relied on the log2(wordBits), which was being
hard coded to 5. Whilst 5 is the correct value on 32-bit platforms, it is incorrect
on 64-bit ones. This changes the previously hardcoded 5 to be the, already existing,
wordRadix definition.
This clock value isn't set consistently on some platforms due to software
rounding, so halting here tends to happen a lot. Instead print a warning
and continue on.
For example using a default Xilinx platform with a 33.333... MHz oscialltor
and a default bootloader the clock value will be somewhere in the range
99999000-100000000, which for most practical purposes is the same thing.
Since this register is written by software and doesn't have the precision to
fully represent common hardware oscillator frequencies, this check seems overly
strict anyway.
makeUserPDEPageTableInvalid and makeUserPDELargePageInvalid were both just creating the same
kind of thing, an invalid mapping, which really should be thought of as the third type of
PDE entry type.
Zero sized arrays are not a C standard extension supported by the C parser. This changes
to the older C90 style for variable length arrays of declaring an array of length 1, as
the C parser also does not suppor the C99 flexible array members.
Declares to a bootloader that we hare multiboot2 compliant and provides an additional
try_boot_sys_mbi2 function for processing a multiboot2 information header.
This abstracts the existing try_boot_sys into two portions, one which pulls data out
of a multiboot1 style information header, and one which performs generic booting
without being multiboot1 specific.
This creates a similar structure as ARM, where an `enum` is created with the `#define` values
from libsel4. Having these values as enum types provides a 'real' C symbol for verification.
RSDP validation was previously done directly in acpi_init. This splits the validation
into a seperate, publicly useable, function. The intention is for this to be used in
boot scenarios where an RSDP is given and does not need to be searched for.
The full RSDP is useful beyond just extracting the RSDT address out of it. In particular
this prepares us for being able to pass a copy of the RSDP to the rootserver.
The previous function signature might lead a user to believe that they were getting a
pointer to a useable acpi_rsdt_t structure. This was in fact not the case and was
actually returning the physical address, that may or may not be mapped in, of the rsdt
table. All of the other acpi *_scan functions would therefore immediately map in the physical
rsdt pointer they were given.
This commit changes acpi_init to return a boolean indicating whether it found a valid
rsdp, and then fills in a copy of the rsdp data. The copy is necessary as the rsdp
data may be at a temporary mapping.
As a result of changing acpi_init the boot code and state is changed to have a acpi_rsdt_t
instance that can be filled out.
This was previously a word_t type, presumably because when the function was originally
written irq_t was a word_t on the platform, this is a mistake and it is more correctly
an irq_t
Verification will guarantee that all usages of the parent cap_get* functions will
be correct and that this case does not happen. However, it is difficult to prove
that the `fail` cannot happen in isolation, and is ultimately not neccessary.
Split up the bit specific code into new folders and added 64-bit
support. Also, changed the device register sizes to be based off of
PAGE_BITS instead of a hardcoded number.
TIMER_CLOCK_HZ is set to the default clock rate from the ATF,
which is the same for both AARCH32 and AARCH64.It may require changes
to the FSBL to work correctly.
The Zynq UltraScale+ MPSoC (PLAT zynqmp) is a Multi-Processor SOC
made by Xilinx that has a quad-core Cortex-A53, a dual-core Cortex-R5
and an FPGA.
This adds 32-bit, single-core support on the the Cortex-A53 cluster.
This renames the previous irq_t enum into a platform_irq_t enum and provides irq_t
as a 'well defined' uint8_t typedef. Having irq_t be an integer type, and not an enum,
is necessary for consistency with verification. As part of explicitly defining irq_t
as an unsigned integer type the definition of irqInvalid is changed to prevent sign
extension leading to unexpected invalid comparisons.
Changes the name of paging structure entries to more clearly indicate the kind of object
they map to. Generally this is changing a `pde_small` to `pde_pt` to indicate that this
mapping refers to a page table, removing an inconsistency where `pde_large` indicated that
the mapping was for a large page. For the same reason the `ept_pde_4k` type is changed to
`ept_pde_pt` type to reflect what is present in the actual entry.
`pde_large` is left as 'large' and not explicitly given a size as code common between
ia32 and x86-64 manipulates these entities and 'large' is already a used abstraction
over the two potential page sizes so there is need to introduce a formal abstraction layer
and make the names in the structures more specific.
On the MCS kernel, Arch_migrateTCB is called in multiple places.
This commit moves the common code that is required when migrating a TCB
to a top level function to reduce boiler plate.
The VT-x implementation is not going to be verified at the moment, and so the code for
it needs to be hidden from verification, which we do by #ifdef'ing it out if the VT-x
is not enabled. As a result the VT-x configuration depends on a non verification target
The IOMMU implementation is not going to be verified at the moment, and so the code for
it needs to be hidden from verification, which we do by #ifdef'ing it out if the IOMMU
is not enabled. As a result the IOMMU configuration depends on a non verification target
