Each architecture now only needs to describe the bounds of the three
memory regions: the 1:1 mapped physical memory region, the kernel ELF
region (which may or may not overlap the physical memory region) and the
device / kernel page table region.
The physical base address of the 1:1 mapped physcial memory region and
the kernel ELF region must also be specified.
The top of user addressable memory (where in the same virtual address
space as the kernel) is defined by USER_TOP.
The physic memory virtual mapping is described by PPTR_BASE and
PPTR_TOP. The base physical memory address is PADDR_BASE and is the
physical address used to map PPTR_BASE.
Don't use kernelBase when referring to the base of the 1:1 mapped
physical memory window.
The kernel ELF virtual address region is described by KERNEL_ELF_BASE
and extends until the virtual address of the symbol `ki_end` which is
created by the linker. KERNEL_ELF_PADDR_BASE is the base address of
the physical memory region used to map the kernel and is the address to
which KERNEL_ELF_BASE maps.
KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE do not need to be aligned to a
page size boundary as they are approriately truncated during boot by the
`map_kernel_window` function.
KDEV_BASE describes the base virtual address of the kernel device region
and the region is assumed to extend to the end of virtual memory.
Note: The offset between PPTR_BASE and PADDR_BASE is used to translate
the virtual address of all untyped objects to physical addresses. This
includes device untyped objects or frame objects where the virtual
address does not fall within the 1:1 mapped physical memory region.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Adapted musl printf implementation using our output abstraction.
Floating point specifiers are not supported in this adaptation.
Modified the code to also match our style and make it
less unnecessarily complex.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
Verification requires packed C structures for reasoning. The C parser
assumes uint64_t (unsigned long long) has 8-byte alignment, thus size of
struct vcpu should be a multiple of 8. As this was not the case, we add
an extra word_t (4 bytes) for padding.
This type of manual padding is naturally fragile and will break as soon
as any field of struct vcpu changes in size by < 8 bytes.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This register is visible to software executing at PL0 but not writeable.
Storing it in the VCPU context required custom save/restore handling as
it had to be explicitly handled when switching from a VCPU thread to a
non-VCPU thread so that it didn't become a channel. It is possible to
now update this register via seL4_TCB_WriteRegisters for software
executing at PL0.
This also fixes a bug where if a vcpu-thread is switched for a
non-vcpu-thread and then switched to a different vcpu-thread the
original vcpu-thread's copy of this register will get set to 0.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
The FPU enable/disable state is cached for all architectures, so
the RV64 FPU code is updated accordingly.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
lazyFPURestore is call during kernel exits. Then, the FPU is
enabled or disabled accordingly by chaning the SSTATUS
of the current thread. The SSTATUS will be written to the
physical SSTATUS CSR, and thus the FPU accesses will be
enabled or disabled.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
These functions are called by the arch-independent functions
to save and restore FPU state lazily.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
This changes the semantics if `isBlocked` to not include the 'inactive'
state when it returns true. The old semantics for isBlocked are provided
by `isStopped`.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
All time for an SC should be relative to its assigned core. Any
operations which may occur on an SC on a remote core must explicitly
refer to that core.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The starting and ready times for any SC should be relative to the core
on which the SC is running rather than the current core.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The thread_control_flag enum which defines which arguments should be
used to reconfigure the TCB should also be split into two sets of flags
as they are now applied to two different functions.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This ensures that verification are not required to prove problematic
combinations of updates to a TCB that aren't even permitted by the API.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
To prevent a contradiction, the C parser does not allow a function to
claim both what it modifies and possess a body that may modify something
else. Instruct the C parser to not translate it in order for the
MODIFIES clause to take precedence.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
It was 'type' on all other arches, but 't' on riscv. Being consistent
here means we can have the same proof for all arches.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This method is a no-op for the hifive platform as all of its interrupts
are positive-level triggered. But we expose the API so that the verified
configuration can include this API method to make it easier to support
different RISC-V platforms under verified configurations in the future.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
The seL4_UserException_Number field of the seL4_UserException_Msg is set
explicitly in setMRs_fault with the saved value of scause from when the
exceptioin was taken.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
The spec expects cap_get_archCapIsPhysical to return false for the
unreachable case. While we could prove that the case is unreachable in
all contexts the function is called, it needs fewer (=no) preconditions
when it provides a safe default instead.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This register is accessible from EL1 and affects whether Generic Timer
registers are accessible from EL0. When switching out of guests, the
kernel needs to restore the correct access for native threads.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Rights on frame caps differ somewhat between architectures, not entirely
in consistent ways. An example is handling write-only frame rights,
where riscv departs from x86. The vm_rights enumeration is not dictated
by hardware, hence we should strive towards consistency.
This change removes VMWriteOnly and makes riscv vm_rights and rights
masking match x86, to facilitate verification of riscv with reduced
proof changes. It does for the time being remove the ability for
write-only frames on riscv.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
vm_rights is an enumeration with 4 entries, which like on other
platforms requires 2 bits to store. Make riscv consistent with other
platforms.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Introduced a new config flag to enable
userError format strings to be written to the IPC buffer.
Another config bool has been introduced to toggle
printing the error out and this can also be set at runtime.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
The format string in userError is now written to
the IPC buffer for debugging purposes.
This requires an snprintf which reuses vprintf with
a new structure for handling how output is done.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
For other platforms, word_t is used for passing length and size
parameters and adapts to 32 and 64-bit platforms appropriately.
The riscv platforms stands out by using "unsigned int" unlike the
others.
Reduce usage of "unsigned int" to match the other 64-bit verification
target platform, x86 64-bit.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
The function arch_clean_invalidate_caches() is required by kernel
benchmarking feature. Add the function prototype as a placeholder, not
yet implemented.
Signed-off-by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>
encoding.h was for ISA simulators originally. It's copied from
riscv-tools which is deprecated. It becomes difficult to maintain the
file. Besides, we merely need 6 lines of code out of this large file. So
redefine what we need in hardware.h and remove encoding.h
The sptbr register is renamed to satp in RISCV privilege spec v1.10. We
kept using sptbr for old compiler versions. All compilers we use support
the new name now. There's no reason to keep the old name.
All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.
Couldn't pass seL4test on ARMv6 due to using FORCE_INLINE.
Replace to static inline will fix it and still got inlined.
Keep FORCE_INLINE for other platforms since inline is broken
on gcc and we have to make sure those functions got inlined.
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.
fastpath_call and fastpath_reply_recv got inlined into a single
function. This could cause loading unused code in cache and
additional jump instructions required in c_handle_syscall.
Added support for injecting remote IPI calls towards given VCPU's
on SMP configured systems. This introudcing a new type of
IpiRemoteCall and handlers for updating the vgic state on
incoming/outgoing IPI's.
Co-authored-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Added constant definitions for the VMPIDR (arm32) and VMPIDR_EL2
(arm64) registers. These being vcpu registers that can be
written, read, saved and restored. The 'Virtualization Multiprocessor
ID Register' (VMPIDR) is needed to program a vcpu's affinity during
initialisation. This is currently only exposed on SMP configurations.
Co-authored-by: Anna Lyons <anna@gh.st>
Truncation to 10 bits is therefore handled by bitfield generator, making
correspondence with more abstract verified specs easier, as they use a
10-bit word to represent IRQs on 32-bit ARM platforms.
C parser cascades up DONT_TRANSLATE blocking modifies proofs, unless
some kind of spec is provided. This makes the claim that the timer
register getters don't modify any global state, and the setters modify
only state verification does not care about.
The PGD constants refer to the top level mapping object used by the
kernel for its own private mappings. Userlevel cannot create any PGD
objects and so these constants don't belong in libsel4.
Configure the ability to trap on vcpu WFE/WFI calls. If enabled,
user-level would need to schedule a future interrupt when a given
vcpu invokes a WFE/WFI instruction. This otherwise leaving the
vcpu in a disabled state. An application can choose to
disable the trap if it doesn't want to handle the instruction and
schedule a future interrupt.
Added support for reading and writing additional virtual timer
registers for vcpu hw read and write accesses. These include the
compare value register (CNTV_CVAL) and offset register (CNTV_OFF),
each represented as two 32 bit (high and low) registers on aarch32 and
as single 64 bit registers on aarch64.
Added support for explicitly saving and restoring the virtual
timer registers when the vcpu is enabled and disabled. This
ensures when the vcpu is switched in and out, the virtual timer
registers are restored to a state that is consistent to when
it was last run.
By default the CNTVOFF register will be updated by the kernel to
accumulate the time the VCPU is not running. From the guest this will
result in the VCNT register not increasing when the VCPU is suspended.
This behavior can be turned off by disabling the
KernelArmVtimerUpdateVOffset config option.
