Current verification model does not include lazy FPU switching, i.e. it
acts as if this function always returns true, so no FPU faults could be
produced. In order to guard against deriving a contradiction, we don't
allow the C parser to translate it.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
- directly test for page PTE types instead of testing for invalid etc.
- remove unnecessary condition `resolve_ret.ptBitsLeft > PAGE_BITS`
(always true).
- reduce bitfield accesses via pointers to make verification easier.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- The failure condition `resolve_ret.ptBitsLeft > PAGE_BITS` prevented
larger page sizes from being flushed in VSpaceRoot invocations.
Instead of testing for number of bits left to resolve, simply check
the PTE whether it is a page or not.
- reduce bitfield accesses via pointers to make verification a bit
easier.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
On AArch64, if this is int, we encounter a situation where we can't
prove equivalence with the abstract spec without an extra invariant that
the number of these registers isn't zero (to satisfy 32<->64 bit casts).
Sticking with word size will make sense on both 32 and 64 bit.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Arch_decodeInvocation takes a word_t length and then passes it to
functions that take an unsigned int length. This was OK on 32-bit where
these types are the same, but on 64-bit this is a downcast without a
range check. It isn't clear why this doesn't trip a compiler warning.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The comment that PRECISION is too low when the assert fails was wrong.
PRECISION should have no influence on it.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- make sure the tick count does not underflow
- make sure the tick count does not become 0 in the division, because
a value of 0 stops the timer.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Move the ksCurTime assertions out of setDeadline, because they are not
necessarily true there. Assert ksCurTime in setNextInterrupt instead.
We only know that the deadline being set is at least ksCurTime -
getTimerPrecision(), which can be slightly in the past (ksCurTime is
already slightly in the past, at kernel entry).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Previously, a refill would be ready if its head time
was at most getKernelWcetTicks after the current time.
This would mean that refill_unblock_check could
bring a refill's time forward, which violates an
invariant (namely that the time of the last refill
is at most the period from the time of the head refill).
Moreover, since the time to exit the kernel is always
less than the WCET, this might result in us running
a thread whose refill time is in the future, which
seems to violate the timing model.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
It is an invariant in the MCS kernel that scSporadic implies sc_active.
Make use of that invariant by avoiding an explicit check for sc_active,
but assert the invariant in debug mode so it fails quickly when new
code breaks the invariant.
Essentially reverts 56098195f2 now that the invariant is preserved,
but adjusts the assertion from 17109eb8c9 to actually express
the invariant.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Follow Arm's code where it tries to place traps and vector
code adjacently in a 4KiB page to optimise performance
(through spatial cache locality).
Closes#1091
Signed-off-by: Hesham Almatary <hesham.almatary@cl.cam.ac.uk>
The vspace (top level PT) cap had non-standard names which were a bit
confusing to reason about. The name conflict with capPTBasePtr also
spits out fully-qualified names in verification.
This commit updates all the field names of vspace_cap to start with
"capVS" and updates all the call sites.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Clearing the pending state only has an effect if the IRQ state is
active-and-pending, which happens for edge-triggered interrupts if
another edge happens on the IRQ line for the currently active
interrupt. This window is small enough to ignore, at worst user
space will get another notification, which is harmless.
If unnecessary notifications are unwanted, the pending state should
be cleared during seL4_IRQHandler_Ack(), as that covers a much bigger
window. However, edge-triggered interrupts are not expected to happen
often. Making all interrupt handling slightly faster and the code
simpler is the better trade-off.
Reading the GIC config word is very slow for GICv2, see pull #1107.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Verification sees macros as the preprocessed C code. On other arches, we
have checkVPAlignment, but on AArch64 we had IS_PAGE_ALIGNED only. Since
this was the only use, this commit also removes IS_PAGE_ALIGNED in
favour of checkVPAlignment.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
For verification purposes, use same arg names as other platforms, and
don't go through `_ptr_set_` from the bitfield generator (same as
RISC-V).
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Verification requires packed C structures for reasoning. While we
previously updated `struct vcpu` to be packed on AArch32, on AArch64
`struct gicVCpuIface` needs extra padding.
This extra padding now aligns a previously un-aligned field on AArch32,
meaning that needs to go away, and the comment there adjusted.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
These were marked DONT_TRANSLATE due to 32-bit `__asm__` blocks which
verification can't handle, which resulted in MODIFIES proofs not being
generated.
This commit adds the obvious MODIFIES proofs for machine ops: nothing
gets modified by reading hardware registers, and writing them only
changes state that isn't in the model.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Enable badged SMC capabilities to be revokable so that dynamic systems
can revoke badged capabilities that are handed out.
Signed-off-by: Kent McLeod <kent@kry10.com>
Provide seL4_BootInfoFrameSize (and seL4_BootInfoFrameBits) for
userland, to there is no longer a need to hard-code the 4 KiByte
assumption.
Signed-off-by: Axel Heider <axelheider@gmx.de>
C parser has issues with `return f(...)` when f's return type is void.
Rephrase `vcpu_hw_write_reg` to look like its AArch32 equivalent, using
`break` in the switch statement.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Verification infrastructure can only handle word-sized variable access
in __asm__ statements. The following functions use 32-bit access on a
64-bit arch and are now marked DONT_TRANSLATE:
* readCIDR
* writeCIDR
* readAFSR0
* writeAFSR0
* readAFSR1
* writeAFSR1
* readESR
* writeESR
* readISR
* vcpu_init_vtcr
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Add helper functions to get kernel image location. This removes any
dependencies from the rest of the code on symbols and defines. It
also avoid passing a parameter though various functions.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Currently getting the timestamp for RISC-V platforms uses the
`rdtime` pseudo-instruction which ends up invoking OpenSBI
and then accessing the CLINT memory-mapped `mtime` register.
This patch eliminates the use of `rdtime` in favour of
directly getting the timestamp for performance.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Now the vspace_cap is used for all vspace roots and all other page
tables are referred to by page table caps.
Signed-off-by: Kent McLeod <kent@kry10.com>
Remove the pde_t type and replace all usages with pte_t.
This doesn't remove the page directory cap type yet. Now the page
directory cap refers to a table of pte_t entries and is treated the same
as the object that a page table cap refers to.
Signed-off-by: Kent McLeod <kent@kry10.com>
This first commit only handles 4k pages.
4k pages are mapped using level 3 descriptor formats which annoyingly
have an opposite type definition (bit[1]) from all other levels. At all
other levels, a bit value of 0 is page and 1 is table. At level 3, a bit
value of 1 is page (and there is no bit value for a table).
This prevents us from using a single tagged-union type definition for
all page table descriptor definitions. For now we treat 4k pages as
special and try and push on ahead with the single type definition
anyway.
Signed-off-by: Kent McLeod <kent@kry10.com>
Guard the new implementation of 64-bit x86 guests behind a config
option. This is done so that existing projects that use x86_64 hosts
with ia32-bit guests can continue to be supported until either the old
feature is preferred to be deprecated, or support can be added to
support both simmultaneously.
Signed-off-by: Kent McLeod <kent@kry10.com>
This commit combines a number of smaller commits which do the following:
* Enter IA-32e mode when running a 64-bit host
* Handle additional general purpose registers in 64-bit mode
* Handle 64-bit specific MSR events
* Properly save and restore FS, GS, and Shadow GS registers
CCDC-GVSC DISTRIBUTION A. Approved for public release; distribution
unlimited. OPSEC#4481.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
__builtin_offsetof is not part of the verification C subset -- avoid
accidental use by not declaring a macro for it and filter out the
single use by explicitly marking it as invisible to verification.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Prefer compile_assert over _Static_assert. The latter is only available
in C11, and the verification demands C99.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Enable the timer only at initialization and since it is always
enabled. It is not needed to be re-enabled.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
