| Age | Commit message (Collapse) | Author |
|---|
|
Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
|
|
|
|
|
|
Makes CheckAndUpdateDescriptor respect endianness
|
|
|
|
|
|
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state. The previous behaviour can be
implemented as Sail code, if desired.
Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
|
|
|
|
- Initialise fault typ field of result record to avoid an unitialised read that
can lead to an early return with a fault. This looks like a bug in the ASL
specification (the ASL tests probably assume that this field is initialised
with Fault_None).
- In ZeroExtend_slice_append (one of the helper functions for monomorphisation
rewrites), use extzv instead of ZeroExtend. It allows not only extension,
but also truncation, and in AArch64_TranslationTableWalk the
ZeroExtend_slice_append function is used to construct a 52 bit physical address
using parts of the 64 bit input address.
- Use the Lem library function for reversing endianness
|
|
Worked around problem with the model where it tries to use bound variables
in patterns
|
|
|
|
|
|
Move mono_rewrites into lib
|
|
|
|
Mostly introducing type variables for regsize in valspecs
|
|
+ add additional lexp
+ update aarch64 mono demo source
- still needs support for tyvars from assignments in dependency analysis
|
|
|
|
|
|
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
|
|
They are used in various specs and test cases.
|
|
|
|
In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
|
|
- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
(used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI
|
|
|
|
|
|
|
|
|
|
|
