For RISC-V platforms that do not provide machine instructions to count
leading and trailing zeros, this commit includes more efficient library
functions. For verification, we expose the bodies of the functions to
the proofs.
Kernel config options `CLZ_BUILTIN` and `CTZ_BUILTIN` allow selection of
whether compiler builtin functions should be used. These are only
supported on platforms where the builtin compiles to inline assembly. By
default, the options are on for all platforms except RISC-V.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.
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.
This changes the budget/remaining fields in scheduling contexts
to contain timer ticks, not number of abstract sel4ticks.
seL4_SchedControl_Configure now takes microseconds, not ticks.
This commit is plat-independant - the platform and arch specific
timer code follows in later commits.
Clang doesn't provide support for __attribute__((optimize ...)). There
are alternatives to provide the same functionality but due to how rarely
the kernel is compiled without optimisations, this can be added on
demand.
This fixes a problem with -O0 SMP builds on ARM visible as kernel
data aborts whenever the idle thread executes.
The idle thread receives no stack pointer. At -O2, this is fine
as the wfi() call is inlined and stack operations in idle_thread
are optimized out. At -O0, the stack operations remain and wfi()
is not inlined, resulting in stack accesses in the idle thread
that cause data aborts.
Forcing -O2 behaviour was deemed the simplest solution for now.
Giving the idle thread a stack would have had larger verification
ramifications for what is now a fairly uncommon use case.
The UL_CONST macro provides a way to declare a constant that may or may not have a UL
suffix. In the case of assembly the UL suffix will be an error to many assemblers and
is not needed.
When compiling the kernel as a whole program it is possible that these functions may
be inlined and not emitted in the resulting binary. However at the same time the
compiler may itself emit calls to these functions. Marking these functions as
externally visible tells the compiler that there may be more usages of them than
it sees immediately in the source code, in this cases usages that the compiler
itself is going to generate
This actually leads to better code. Copies of the halt loop inlined
in various places will instead be single instructions 'bl halt'. It's
also important for the translation validation to avoid having
pointless loops everywhere, especially inside the bodies of other
loops.
Add compatible prototypes for compiler builtins
__builtin_unreachable, __builtin_ctzl, __builtin_clzl,
and __builtin_popcountl.
The compiler ignores these, but they are necessary for the Isabelle
C parser to handle them. This is needed to drop DONT_TRANSLATE markers
from various functions which call these builtins.
config_default was intended to either evaluated to the passed configuration
value, or the a default value if the config didn't exist. For integer values
this does not actually work, and the default value always gets returned.
This commit reimplements the desired functionality as config_ternary, which
takes 3 arguments, a config to switch on and a desired true and false expansion
* commit 'ed95f84a438aea6365762a180cc493113e9282e0':
SELFOUR-413: changes for verification
SELFOUR-567: use seL4_CapRights_t from libsel4
SELFOUR-413: refactor libsel4 fault API
Split fault types into arch/generic
Prior to this commit faults were separate
per architecture. This commit extracts the common
fault types and introduces arch specific faults,
reducing code duplication across architectures.
Fixes a bug where previously MODEL_ID() was defined as:
`#define MODEL_ID(x) ( ((x & 0xf0000) >> 16) + (x & 0xf0) )`
This was incorrect because (1) it didn't take into account the conditional
nature of the extended_model_ID, and (2) it's actually shifting the
extended_model_ID into the low bits and keeping the model_ID in the high bits,
when it should be the other way around.
This patch also introduces a foundation for more sane testing of CPU vendor,
family, model and brand_ID.
The `VISIBLE` macro is designed to selectively inhibit the effects of GCC's
whole program and link-time optimisations. This is necessary when a C function
is only referenced from a context outside the compiler's visibility, e.g. an
assembly file. As far as I can determine, Clang's link-time optimisations
already account for this possibility and do not need to have this information
manually indicated to them (see, for example, Linux's compiler support headers).
In any event, `__attribute__((visibility("default")))` is not equivalent to
`__attribute__((externally_visible))`, but is instead for controlling symbol
visibility in a library-like setting. This commit removes this incorrect
expansion.
This macro allows for using the value of a CONFIG_ variable in situations
where it may not be defined. This could be due to it being a dependency
on another CONFIG_ variable that is not currently defined. This arrises
from code blocks like
if (config_set(CONFIG_FOO)) {
return CONFIG_VAR_DEPENDS_ON_FOO;
}
This will not compile when CONFIG_FOO is not set. Using
return config_default(CONFIG_VAR_DEPENDS_ON_FOO, 42);
Provides a way for this to be built
Some versions of GCC replace a struct copy with a call to 'memcpy',
which it is fully in its rights to do. Unfortunately on ARM platforms,
that have no direct calls to memcpy, the optimizer (in the presence
of -fwhole-program) drops the implementation of memcpy, even as it
is outputting calls to it.
Add the USED attribute prevents the optimizer from dropping the
function eagerly.
