The check was not enforcing the minimum radix intended by 5fac9e8 and
still allowed a radix of 4 to be specified.
Signed-off-by: Craig McLaughlin <thecraigmclaughlin@gmail.com>
Previously accessing the ccnt_num_overflows
value using the NODE_STATE macro. In SMP
configurations, this looks for this value
in the system node state, however, it
resides in the cpu arch node state. This should
therefore be accessed using the ARCH_NODE_STATE.
Signed-off-by: Krishnan Winter <krishnanwinter1@gmail.com>
Add a glossary with seL4-specific terms and their
definitions.
Remove chapter number from bibliography
Tweak Makefile for glossary
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
This way common error codes can be in their own file.
To use, add the xmlns:xi="http://www.w3.org/2001/XInclude
attribute to the top level node and use:
<xi:include href="file-to-include.xml"/>
The content of the file will be included verbatim.
Include files must be complete XML documents, but without
<?xml version="1.0" ?> at the top. Practically this means
all nodes within the file need to be contained in one root
element.
Caveat: There is no proper dependency for Xincludes files in
the Makefile, so you need to do make clean after changing an
included XML file!
Signed-off-by: Indan Zupancic <indan@nul.nu>
This file was used by the previouse license checking tool, but is
ignored by the `reuse` tool. This means it is now obsolete.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add padding to keep vcpu struct packed on 32-bit platforms. This doesn't
change the size on 32-bit platforms, because the compiler would insert
padding itself. It does increase the size of the struct by one word
on 64-bit platforms, but it remains below 2^vcpuBits.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Currently the seL4_VCPUReg enum only defines the seL4_VCPUReg_VMPIDR_EL2
register when the kernel is configured for SMP. This register should be
available for unicore systems too as otherwise a user level VMM is not
able to control the value of MPIDR_EL1 that the guest VM reads.
Signed-off-by: Kent McLeod <kent@kry10.com>
Partially revert commit 70d1a5f792.
Can't include arch/machine.h because that will cause
a circular include dependency.
Signed-off-by: Indan Zupancic <indan@nul.nu>
The Odroid-C4 is supposed to have 4GB of DDR memory.
According to the SoC manual (S905X3 Revision 02) the
DDR region goes from 0x0 to 0xF57FFFFF in Table 7-1.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
The S905X3 manual (Revision 02) specifies the highest IRQ
to be 255 in section 7.10.2 of the manual.
This issue was encountered when trying to use the PCIe
device on the platform which uses IRQs higher than 250.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
The vcpu is not guaranteed to be associated with a TCB at this point,
so access to vcpuTCB must be guarded.
Fixes#1199
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
These calls can now be implemented via binding the /timer driver in the
elfloader's device tree configuration.
Signed-off-by: Kent McLeod <kent@kry10.com>
Proof artifact upload had name clashes for different artifacts from the
same job that previously would overwrite each other and with v4 actions
now error. This commit disambiguates the names.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
These files cannot be installed under the same names as those in the
source tree because the two named sel4arch.xml conflict. These cannot be
renamed in the source tree because of other projects which expect them
under their current names.
Commit cf80db7ef0 enabled them to be installed them under
non-conflicting names, but those names (sel4.xml, sel4-arch.xml,
sel4-sel4arch.xml) are confusing and too close to the original names.
This commit changes the names they are installed under to be more clear
and descriptive (object-api.xml, object-api-arch.xml,
object-api-sel4-arch.xml).
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Allow multiple overlay files to be specified. This supports custom
tooling support to add additional memory reserve regions to a platform.
Signed-off-by: Kent McLeod <kent@kry10.com>
Current verification model does not include lazy FPU switching, i.e. it
acts as if this function always returns true, so no FPU faults could be
produced. In order to guard against deriving a contradiction, we don't
allow the C parser to translate it.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Remove the space in the workflow name to ensure there are no side
effects when using it as an identifier.
Signed-off-by: Axel Heider <axelheider@gmx.de>
As in the other architectures, avoid unnecessary casts for the loop
counter by making it a word_t.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
GitHub has updated the LTS node.js version from 16 to 20 and is
starting to show warnings for node16 actions.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Mark CROSS_COMPILER_PREFIX as meaningful to gcc.cmake, so that it is
propagated for all cases where gcc.cmake used.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Test the PTE directly for being of page type and avoid ptr access to
ease verification in unmapPage.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The implementation of single-stepping on ARMv7 relies on instruction
mismatch breakpoints. The implementation sets one of the breakpoint
value registers (BVR) to NULL and configures the corresponding
breakpoint control register (BCR) to generate a debug exception for
instructions that are at any other virtual address. This is incorrect
as it means that when single-stepping is enabled, no progress will
ever be made by the thread, as every instruction will mismatch with
NULL and result in the generation of a debug exception.
This commit resolves this issue by setting the BVR to the LR of the
thread at the moment single stepping is configured. Then, when the
thread is permitted to execute again, the instruction pointed to by
the LR will be executed, but any other instruction will result in a
debug exception. It also changes the debug exception hander to
update the BVR to the new LR when a single-stepping execption occurs
so that we can step over multiple instructions before sending a debug
fault to the appropriate fault handler thread.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
- directly test for page PTE types instead of testing for invalid etc.
- remove unnecessary condition `resolve_ret.ptBitsLeft > PAGE_BITS`
(always true).
- reduce bitfield accesses via pointers to make verification easier.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- The failure condition `resolve_ret.ptBitsLeft > PAGE_BITS` prevented
larger page sizes from being flushed in VSpaceRoot invocations.
Instead of testing for number of bits left to resolve, simply check
the PTE whether it is a page or not.
- reduce bitfield accesses via pointers to make verification a bit
easier.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Bring the type of `i` into line with what the other architectures do
in this function. This makes it easier to re-use those proofs.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Type invLabel consistently as word_t, not sometimes as unsigned int.
This makes verification easier because it avoids unnecessary casts.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
