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>

Type and ghost state annotations for verification.

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>

The rest of the code uses 9-bit irq width. Keep in sync here to ease
verification.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

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>

This is missing in commit e6fbbbb0

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Axel Heider <axelheider@gmx.de>

Since commit cf8be663 this is no longer needed.

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Cindy Liu <hcindyl@google.com>

Signed-off-by: Cindy Liu <hcindyl@google.com>

Use importlib.metadata to check the jinja2 version

Signed-off-by: Cindy Liu <hcindyl@google.com>

The kernel.elf file is occasionally more useful for debugging than the
final board image.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Birg <bbrcknl@github.com>

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>

Signed-off-by: Birg <bbrcknl@github.com>

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Axel Heider <axelheider@gmx.de>

Avoid the annoying style checker complaints.

Signed-off-by: Axel Heider <axelheider@gmx.de>

Support multiple architectures as parameter.

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Axel Heider <axelheider@gmx.de>

The default value is zero anyway.

Signed-off-by: Axel Heider <axelheider@gmx.de>

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>

This changes it to be a pure function, which eases verification

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

The assert() condition is checked two lines above

Signed-off-by: Axel Heider <axelheider@gmx.de>

Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>

Similarly to the U54-MC, the U74-MC has a S-core that does not run in
supervisor mode.

Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>

Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>

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>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>