Enforce the maximum possible integer size in the generated C headers
instead of doing this in CMake.

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>

There is no need for separate definitions, they define the same value.

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>

The L2 cache handling functions were copied from the ARM code in the
initial port, but they are not used on RISC-V. Remove them from the
code base, they can be brought back if a platform has an L2 cache that
needs to be maintained.

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>

Turns out the invariant 17109eb8 refers to is hard to prove
because it is not true, and the runtime check is necessary. This
assertion fails in sel4test SCHED_CONTEXT_0003 (Basic
api_sc_bind/UnbindObject testing).

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

- in decodeSchedControl_ConfigureFlags
- a minor tweak to aid verification.

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>

Easier to check this explicitly than prove the invariant.

Signed-off-by: Curtis Millar <curtis@curtism.me>

Previous "Kernel" showed up for the badge and main checks group, which
is not very informative.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

The badge now refers to the combined simulation + hw build + hw test +
deployment workflow.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Previously the `concurrency` statement also prevented concurrency
within the build matrix which we do not want.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

This commit pulls out a separate workflow for sel4test (simulation +
hardware runs) on pushes to master, and deploys a new default.xml to
sel4test-manifest when the test is successful.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

- Explain why restore_user_context() is not called in init_kernel()
directly.
- describe the parameters that init_kernel() expects.

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>

seL4Config.cmake is responsible for generating a valid
CMAKE_TOOLCHAIN_FILE and setting up platform config options at the start
of the build. The CMAKE_TOOLCHAIN_FILE variable has to be set before the
first cmake `project()` function is processed to take effect.
Previously this file was required to be imported in a CMake script
before the kernel's CMakeLists.txt could be processed. This prevented
the main CMakeLists.txt file from being used without an additional
configuration file:
cmake -G Ninja -C ../configs/ARM_verified.cmake ../

Now it is possible to do:
cmake -G Ninja -DKernelPlatform=imx6 -DKernelARMPlatform=sabre ../

This should make it easier to invoke CMake for building kernel
configurations from other build environments.

Because this file is now imported in the Kernel's CMakeLists.txt
context, there is no longer a requirement to save all the intermediate
settings into the cache and then read them out again.

Signed-off-by: Kent McLeod <kent@kry10.com>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>

Automatically keep verification-manifest in sync with
preprocess-equivalent changes.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

GCC < 10 and clang < 11 put uninitialized global variables into a
'COMMON' section unless '-fno-common' is specified. The linker will put
anything from 'COMMON' as the end of the '.bss' it nothing else is
specified in the linker script. Besides making the variable placement
look odd, this also tends to waste a page because we puts large aligned
block at the end. Eventually, GCC 10 and clang 11 made '-fno-common'
the default, see
- https://gcc.gnu.org/gcc-10/changes.html
- https://releases.llvm.org/11.0.0/tools/clang/docs/ReleaseNotes.html



Signed-off-by: Axel Heider <axelheider@gmx.de>

Add a comment to clearly state the functions are empty on purpose, but
they still need to be provided to support the generic code flow.

Signed-off-by: Axel Heider <axelheider@gmx.de>

The function setInterruptMode() is no longer in use, setIRQTrigger() is
used instead.

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Axel Heider <axelheider@gmx.de>

All architectures define paddr_t as word_t, but the actual definition of
word_t is specific to every architecture's word size. For this reason, a
dedicated format specifier for word_t has been introduced, it hides
all these detail.

Signed-off-by: Axel Heider <axelheider@gmx.de>

The functions insert_region() and create_rootserver_objects() are not
used outside of boot.c, so there is no reason to make it publicly
available.

Signed-off-by: Axel Heider <axelheider@gmx.de>

The field ksKernelEntry.core always exists, ensure it is properly set on
non-SMP configurations also.

Signed-off-by: Axel Heider <axelheider@gmx.de>

Replace the macro SMP_TERNARY(getCurrentCPUIndex(), 0) by the much
simpler macro CURRENT_CPU_INDEX() that does the same.

Signed-off-by: Axel Heider <axelheider@gmx.de>

CURRENT_CPU_INDEX() is supported to return a word_t. The C parser from
the verification toolchain requires declaring word_t constants without
casting integer values to word_t.

Signed-off-by: Axel Heider <axelheider@gmx.de>

This fixes a correctness and security issue where uncached user
mappings might see old data from before the clearMemory operation.

See also the discussion on GitHub issue #481

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>

Align the parameter naming within each architecture's file and also
across architectures.

Signed-off-by: Axel Heider <axelheider@gmx.de>

Trigger moved to pull_request_target, so event name is changing as well.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

More x86 boards have become available, so we can have one session
per mode and compiler.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

The link will probably go back to .html when the website is finished,
but this commit will avoid annoying test failures in the meantime.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

This switched the action from pull_request to pull_request_target,
because we need access to secrets. GITHUB_TOKEN permissions are
downgraded to PR-like permissions, and the action needs to be triggered
manually by labelling with label 'hw-test'.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Also merge create_device_untypeds() and create_kernel_untypeds() into
create_untypeds() to simplify the code.

Signed-off-by: Axel Heider <axelheider@gmx.de>

CMake treats any text output that is generated by tools during the
configuration phase as important if it isn't part of a message(STATUS)
command. Output generated by hardware_gen.py often shows up as warnings
about device tree properties that are usually uninformative. Resolving
some of the warning conditions removes these messages for most
platforms.

- Setting kernel_size in hardware.yml to 0x1000 to handle cases where
  the kernel only needs the first page of a device that has a
  device-tree definition larger than that.
- Remove status print about each Interrupt processed as it's usually not
  useful information.
- Only process IRQs for a selected kernel device if the rule for that
  device has any interrupt queries. This prevents warnings for IRQ
  controllers that the script doesn't know how to process when it
  doesn't need to.

Signed-off-by: Kent McLeod <kent@kry10.com>

The reason is that with separate workflow files allow different
triggers. In particular, we don't want to re-run all simulations
on all `labeled` triggers, but if we explicitly skip the simulation
job for those triggers, than previous simulation runs are not
shown any more in the GitHub check status, so failed runs will be
overlooked.

This should achieve both: no unnecessary runs, and visible status.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>