Before this change, options that were hidden from the cmake-gui due to
unsatisfied config_choice conditions were not recorded in
gen_config.{yaml,json,h}. After this change, these hidden options are
recorded as disabled.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Take advantage of the new --skip-unchanged option added to the
config_gen.py header generator to skip regenerating unchanged header
files which forced a rebuild of the entire project whenever CMake was
reconfigured.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
Compatibility with versions <3.10 is going away.
As it happens, we're not using any CMake features that have changed
between 3.7 and 3.16, so bump the lowest version to 3.16.
Also remove the minimum version statement from the platform config
files --- they're all very simple files that are version independent;
and the version is checked elsewhere anyway.
Also, Fix style issue
A commit to fix style to make the PR go through.
Signed-off-by: Peter Chubb <Peter.Chubb@unsw.edu.au>
With recent proof improvements the proofs now apply to further platforms
in the ARM and AARCH64 configurations.
Refactor the verified configs to build on one include file per major
architecture which is then used for each platform with potentially
modified settings. Add path argument to `cmake_script_build_kernel`
macro to accommodate inclusion from different locations in the file
system.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This should not have been added in commit ad4ea6cd. And since
commit c642a398 this is handled by a python script anyway.
Signed-off-by: Axel Heider <axel.heider@codasip.com>
Commit 6d439a4646, which added JSON configuration output, caused the
configuration headers to be generated at build-time instead of
configure-time. This broke CAmkES build systems which depend on
configuration headers in CAmkES files at configure-time.
This commit makes the configuration headers available at configure-time.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Add a `--form_file <file>` option to the bitfield generator for
printing a `/* generated from <file> */` message in a comment.
Use this option in cmake to provide the original source .bf file before
preprocessing so it's easier to find out where the corresponding
definitions are.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
gen_config.json provides a language-independent means of accessing the
kernel configuration. Before, gen_config.h was generated directly in
CMake. Now, gen_config.yaml is generated directly in CMake, and
gen_config.h and gen_config.json are derived from gen_config.yaml.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
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 directory-scoped varible is now used by config_option,
config_choice and config_string to set a created CMake cache variable as
advanced or not. An advanced variable is hidden by default in the CMake
configuration editors. Setting SEL4_CONFIG_DEFAULT_ADVANCED to ON will
cause variables to be advanced and not show up in the cache. Projects
can set this to limit the amount of options presented in the
config editor. Any cache variable can have this overridden by calling
mark_as_advanced(CLEAR config_name)
This leverages #!/usr/bin/env -S cmake -P to invoke a cmake
configuration file as a script that configures and builds a kernel in
the current directory with the configuration that was invoked. It is a
quick way for producing a kernel.elf or kernel_all_pp.c input file to
verification for a particular config.
Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).
INTERNAL implies FORCE but in some versions of CMake if a config option
has been passed in via a -D option the INTERNAL set doesn't override the
value when it should.
See: https://gitlab.kitware.com/cmake/cmake/issues/19015
INTERNAL does not imply FORCE for CACHE
- Minimise calls to external_process as this is more expensive than
using built-in CMake file operations.
- Update check_outfile_stale to also save the list of files it checks
for stale checks so if a config changes the list of files then the
output file will still be stale even if the input list of files are
older than it.
Our upcoming cmake styling tool requires any custom functions you want
styled nicely to be lower case. We only need to style these two nicely,
as they have kwargs we would like aligned.
Add kernel_platforms_string and kernel_platforms_list to tools/helpers.cmake.
kernel_platforms_string: concatenates all platform strings together into a
newline separated string.
kernel_platforms_list: returns a list of all kernel platforms.
Modified the behaviour of the EXACT_INPUT option within the
CPPFile helper function. Now named EXACT_NAME, the option
copies the input file to a temporary file. The name of the
temporary file is also passed in by the caller. This
step in necessary in getting the CPP step to correctly
depend on the targets given by the caller
(through EXTRA_DEPS). Also updated the CPP generation of the
kernel_all.i file to reflect the change.
REALPATH was unnecessary and results in resolving symlinks in the target, although
the working directory will not have its symlink resolved. This results in very strange
paths from the base directory (which is the working directory) to the target.
This is a new version of GenCPPCommand that uses an OBJECT library intermediate to get
cmake to do 'arbitrary' compilation (by adding the -E flag) where the result does not
need to be linkable. The advantage of this over the GenCPPCommand version is there is
no need for trying to manually invoke GCC with all the correct arguments lists.
As a macro this helper would not operate as expected if output and input were defined
as the same variable. Making a function and explicitly writing into the PARENT_SCOPE
fixes this and also makes the code simpler
This change makes values take on more intuitive and expected defaults when gradually
configuring the kernel, either programatically or through the graphic interfaces
TOPLEVELTYPES is not intended to be configurable by the user, rather is a reflection
on the types defined by the source. This changes the TOPLEVELTYPES argument to be
a property, allowing it to be constructed as a generator expression when generating
BF files. By being a property, and not something like a global property, it removes
the need to ensure that additions to TOPLEVELTYPES are done prior to any bitfield
target definitions.
Uses the COMMAND_EXPAND_LISTS flag to allow for generator expressions in parameters
to GenBFCommand. As lists are now being expanded the 'args' variable must also be
quoted.
Previously if a variable had unmet dependencies and had been hidden, by being made
an internal variable, it would not have been unhidden by the use of `option`. This
emulates the behaviour of `option` that we were wanting, but additionally using `FORCE`
to override the `INTERNAL` setting
Uses file(GENERATE) to directly create the contents of generated configuration files instead of
awkwardly using custom commands to echo the contents of multi line strings into files.
Newer versions of cmake provide a COMMAND_EXPAND_LISTS option that allows a quoted string,
such as "a;b" to be given to a COMMAND parameter and have it expand into multiple arguments.
Using this we can much more nicely generate some of our COMMAND invocations, at the cost of
requiring a more recent cmake version
The config_option helper was previously using cmake_dependent_option, which supposedly took
a value to set the option to in the case where it was disabled. However, this only sets
the value in the current function context, and not the cache. I do not understand why this
is the case and it seems to make that functionality completely useless. This commit simply
does the dependency checking itself and correctly sets the disabled value.
Instead of explicitly depending on Kernel_C.thy prior to generating proofs, this removes
the dependency check and leaves isabelle to check the dependency upon import.
