Mark CROSS_COMPILER_PREFIX as meaningful to gcc.cmake, so that it is
propagated for all cases where gcc.cmake used.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Test the PTE directly for being of page type and avoid ptr access to
ease verification in unmapPage.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The implementation of single-stepping on ARMv7 relies on instruction
mismatch breakpoints. The implementation sets one of the breakpoint
value registers (BVR) to NULL and configures the corresponding
breakpoint control register (BCR) to generate a debug exception for
instructions that are at any other virtual address. This is incorrect
as it means that when single-stepping is enabled, no progress will
ever be made by the thread, as every instruction will mismatch with
NULL and result in the generation of a debug exception.
This commit resolves this issue by setting the BVR to the LR of the
thread at the moment single stepping is configured. Then, when the
thread is permitted to execute again, the instruction pointed to by
the LR will be executed, but any other instruction will result in a
debug exception. It also changes the debug exception hander to
update the BVR to the new LR when a single-stepping execption occurs
so that we can step over multiple instructions before sending a debug
fault to the appropriate fault handler thread.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
- 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>
Bring the type of `i` into line with what the other architectures do
in this function. This makes it easier to re-use those proofs.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Type invLabel consistently as word_t, not sometimes as unsigned int.
This makes verification easier because it avoids unnecessary casts.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The highest defined interrupt in the data sheet is 543 - 32 = 511.
This is important, because the code expects all IRQ numbers to fit into
9 bits (which 511 does, but 512 would not).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Refactor getMapRefForASID for verification into separate parts, because
the returned pointer doesn't exist as a concept in the executable spec.
Also avoid ptr_set functions to simplify heap reasoning.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The kernel.elf file is occasionally more useful for debugging than the
final board image.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
lr_num is assigned to from word_t, so should also be word_t rather than
unsigned int.
Signed-off-by: Rafal Kolanski <rafal.kolanski@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>
This insertion is not required, as the slot has just been cleared by
cteDelete. Avoiding the insertion simplifies verification.
Signed-off-by: Corey Lewis <corey.lewis@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>
Put MCS-only invocations into their own groups and files. This solves
the problem that doxygen gets confused by duplicate function names with
the same parameters.
MCS/non-MCS is distinguished by evaluating the <condition> field in the
API XML definition. If the condition evaluates to true when
CONFIG_KERNEL_MCS is set, it is an MCS-only method, otherwise it is
assumed to be non-MCS or present in both configs.
Fixes#558
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Disambiguate (for the reader) between normal and mcs versions of
SetSpace in the manual. This does not yet solve doxygen confusion.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
HTML_TIMESTAMP and LATEX_TIMESTAMP have been removed in more recent
doxygen versions. Since we are using the defaults, they are safe to
remove in our config file.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Different API groups may contain the same function name, for instance
IRQ_Control GetTrigger for RISC-V vs the same for ARM. Duplicate
function names with identical parameter lists confuse doxygen, leading
it to generate a single merged xml entry for both, which means one of
the entires will be missing and the other will be potentially wrong.
When the functions are placed in different files and different groups
at the same time, doxygen no longer is confused in all cases.
Therefore:
- generate a separate file for each API group
- generate a separate file group_defs.h that contains group definitions
and declares group nesting
Unfortunately, this does not seem to always work (e.g. the toplevel
MCS/non-MCS syscalls), so manual inspection is still necessary when
adding new calls and separate doxygen runs for duplicate function names
may be necessary. Generating separate files as above enables this
option, should it become necessary in the future.
Fixes#530
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
