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.
Create new function "clz" which invokes __builtin_clz
Tell the C parser to not try translate it (DONT_TRANSLATE), but instead
to trust the spec we provide (FNSPEC+MODIFIES).
Squashed the fix by Anna Lyons:
rearrange CLZ in util.h and s/__builtin__clz/__builtin_clz/
