* Add help texts for all CLI options.
* Point to the manual in file header.
* Remove obsolete `--multifile_base` and `--c_defs` options. The former
is unused and the logic for it was removed in the previous commit.
The latter is not referenced in the code and has no effect. `
* Remove unused `mode` variable.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The `--multifile_base` option is unused in the seL4 build and has
comments indicating that it is broken.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a user manual for the bitfield generator that documents syntax,
semantics and basic concepts. Should also be able to serve as main
spec for what the tool is supposed to do.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
For verification flexible w.r.t kernel placement in physical memory, we
need to relate physBase as a named constant to its abstract equivalent.
Unfortunately, apart from enums, the C programming language does not
have real constants. The C parser follows the C standard and requires
enums constants to be storable as int, meaning without major overhaul
enums are not sufficient for storing word_t-sized memory addresses.
Since the linker scripts can't deal with static inline functions
in the constants they need (KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE),
we provide the following preprocessor definitions for the linker
specifically:
* PHYS_BASE_RAW (the numerical value returned by physBase())
* KERNEL_ELF_BASE_RAW
* KERNEL_ELF_PADDR_BASE_RAW
Signed-off-by: Rafal Kolanski <rafal.kolanski@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 adds support for the Pine64 Quartz64 and other devices based on
the Rockchip RK3566. The platform support is adapted from the
Rockpro64 code, except that the RK356x has A55 cores, and adjusting
for the fact that the ARM Generic Timer is the only on-chip timer
available.
Signed-off-by: Peter S. Housel <housel@acm.org>
Remove redundant (and incorrect) reserved memory
definition for VideoCore memory. The reserved
memory area is defined in 'overlay-rpi4.dts'.
Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>
Signed-off-by: Hannu Lyytinen <hannu.lyytinen@unikie.com>
kernel,bcm2711: Fix RPI4 address mapping
Fix build error and warnings by removing GPIO mapping
from overlay. Also as a note, don't add 'serial1' or 'ethernet'
here, because 'serial1' is already mapped to sel4 kernel by
'chosen' block in 'overlay-rpi4.dts', and the translation for
the 'ethernet' is done with 'ranges' property.
Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>
kernel,bcm2711: Fix memory area overlay DTS
First fix is to change the memory area reserved for
the VideoCore from 64 -> 76 MB, as this is the default
value on RPi4. Using other values would require configuration
of the first stage bootloader with 'config.txt' file.
Second fix is separating the disjunct memory areas
to separate nodes, as the generator Python scripts
in 'kernel/tools/' etc discarded the first area below
1GB limit if all areas were defined in the same node.
The effect of different variations can be observed
during kernel build in the generated
'kernel/gen_headers/plat/machine/devices_gen.h' header.
Third fix is adding the reserved memory area for the
VideoCore memory to avoid any collisions.
Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>
There are cases that reasonably require non-ASCII characters in the
source code, hence tools/bitfield_gen.py must be able to handle them
correctly. This commit makes sure the bitfield generator consistently
opens all files with UTF-8 encoding.
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Bin Meng <bmeng.cn@gmail.com>
Generated from maaxboard-dcss-hdmi.dts (Avnet/linux-imx) for more
comprehensive device support. Updated overlay to align.
Signed-off-by: Mark Jenkinson <mark.jenkinson@capgemini.com>
Bring up-to-date with current proof style, make style consistent,
slightly increase proof parallelism.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
A tagged union can now optionally use multiple fields to indicate the
tag. These are called "sliced" tags in the code. The tag fields have to
be at the same position and width in each block of the tagged unions,
and all tag fields have to be within the same word.
When sliced tags are used, tag class masks cannot be used at the same
time for this tagged union.
In the `tagged_union` declaration, the values of such sliced tags
become tuples. For instance, if `x` and `y` are tag fields (declared in
blocks not shown here) with width 1 and 2, we can write:
tagged_union ex exType(x,y) {
tag ex1 (0,2)
tag ex2 (1,3)
}
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
this allows the template to be parsed with minijinja
which doesn't support namespaces or set (at this time).
Signed-off-by: matt rice <ratmice@gmail.com>
This commit adds a new device tree for the ultra96v2, adding
additional devices to give to userspace.
Signed-off-by: Robbie VanVossen <robert.vanvossen@dornerworks.com>
The memory mapping for the timer only uses 1K on AllwinnerA20, but
the minimum device mapping is 4K in seL4. Other devices within this
4K page (CCU and PIO) cannot be accessed in the userland.
Replace the kernel timer with the ARM generic timer on AllwinnerA20,
and remove the implementation for AllwinnerA20 specific timer in the
kernel. So we should have user access to those devices now.
Signed-off-by: Luca (Wei) Chen <wei@cvluca.com>
Makes it easeier to eyeball the difference between the beaglebone's spec
and (say) the beaglebone-black's spec.
Changed with `sed -re 's/<(.*)>/< \1 >/`
Signed-off-by: Stephen Sherratt <stephen@sherra.tt>
