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
For bitfields requiring sign extension, the generated specs are nicer to
work with in proofs. The proofs also support an updated `sign_extend`
specification (in the l4v repository) which has nicer properties.
This change also speeds up some bitfield proofs.
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.
For blocks and unions, generate only one write for each word, rather
than an update for each bitfield.
For verification, this speeds up some automatically generated proofs.
Dependencies can now be downloaded with:
pip install sel4-deps
Dependencies can be changed by modifying the setup.py script.
Information on how to update the package is in the setup.py script.
JIRA: SELFOUR-909
The lxml module relies on native libraries. When linting, pylint will
not load native libraries for security reasons. Thus, it can't find some
symbols exported by lxml, causing linting to fail. Whitelisting lxml
prevents this.
If `seL4_arch_invocations` is an empty list, this will cause `nSeL4ArchInvocationLabels`
to be declared as 0, rather than `nInvocationLabels` as intented. This change correctly
respects the behaviour of the 'first' variable, and does an explicit assignment to
`nSeL4ArchInvocationLabels` should it be the first (and only) member of the enum.
Closes#53
CONFIG_LIB_SEL4_PUBLIC_SYMBOLS=y will disable inlining for external
interfaces (except deprecated functions), thereby providing public
symbols for easy linkage with other languages.
This is a technical change to the proof mode of the bitfield
generator included in the seL4 source.
The postconditions of the generated specifications of the
*_ptr_set and *_ptr_new functions now describe the entire new
heap via (new_heap = hrs_mem_update (...) old_heap).
Previously they described the contents of various projections
of the heap, which is less precise.
If invocations are hidden behind config guards the count of how
many invocations there are will be wrong. The C compiler will
correctly assign the value with enum auto numbering, so there's
no need to override that here
Placing a config condition on the first define
in sel4arch.xml will fail as currently the first define
must start at the last define + 1 of the previous
invocation enum.
If this is ever required, autoconf.h will need to be passed
to the script so it can check config variables itself.
This reverts commit 5ee3971563. This backend was
previously used in an experiment towards libsel4 verification. That project has
since adopted a different strategy and this backend is now unused. Meanwhile
the backend has lagged behind breaking changes to AutoCorres. This commit
removes the backend to avoid confusion from users who believe it to be
functional.
The plan here is to move some of the proof script complexity embedded
in the text of the bitfield_gen utility into generic proof helpers in the
l4v repository that bitfield_gen can use more modularly. This is a simple
first step.
