| Age | Commit message (Collapse) | Author |
|---|
|
Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging
|
|
|
|
|
|
|
|
This is interpreted as a set of bits that control various bits of output.
Bit 0 is print the PC on every cycle.
(It would probably be useful to standardise a few of these flags across
all models. Other candidates are accesses to physical memory, throwing
SAIL exceptions, current privilege level, ...)
|
|
|
|
|
|
|
|
|
|
- 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
|
|
targets using this.
|
|
Every Unix is subtly different.
|
|
Makes the generated undefined functions smaller, easier to read, and
avoids excessive memory usage in Coq (e.g., for large AST types).
|
|
If you don't exit immediately, the test will probably just jump off into the
weeds and stay there until it times out. So better to exit early.
But note that this is not all IMPDEF behaviour.
Most IMPDEF such as 'Are SHA3 crypto instructions available?' are already
being handled and either TRUE or FALSE is being returned.
So this is just for the stuff where we don't have a good answer at all.
|
|
|
|
|
|
|
|
The Arm spec uses the value 2.0^1000000 to represent infinity
so it is worth making real_power take logarithmic time.
|
|
|
|
graceful exit on reaching cycle limit. This aids coverage and valgrind instrumentation.
|
|
Implement square root function for rationals up to an arbitrary
precision, currently 30 decimal places. May need to increase this for
ARM tests.
|
|
No functional change
|
|
Use -DHAVE_SETCONFIG to enable __SetConfig support
|
|
|
|
This is now directly supported from SAIL so we can call the SAIL __SetConfig function
instead.
|
|
|
|
|
|
|
|
Registers can now be marked as configuration registers, for example:
register configuration CFG_RVBAR = 0x1300000
They work like ordinary registers except they can only be set by
functions with the 'configuration' effect and have no effect when
read. They also have an initialiser, like a let-binding. Internally
there is a new reg_dec constructor DEC_config. They are intended to
represent configuration parameters for the model, which can change
between runs, but don't change during execution. Currently they'll
only work when compiled to C. Internally registers can now have custom
effects for reads and writes rather than just rreg and wreg, so the
type signatures of Env.add_register and Env.get_register have changed,
as well as the Register lvar, so in the type checker we now write:
Env.add_register id read_effect write_effect typ
rather than
Env.add_register id typ
For the corresponding change to ASL parser there's a function
is_config in asl_to_sail.ml which controls what becomes a
configuration register for ARM. Some things we have to keep as
let-bindings because Sail can't handle them changing at runtime -
e.g. the length of vectors in other top-level definitions. Luckily
__SetConfig doesn't (yet) try to change those options.
Together these changes allow us to translate the ASL __SetConfig
function, which means we should get command-line option compatibility
with ArchEx for running the ARM conformance tests.
|
|
Mostly improving error messages
|
|
|
|
|
|
|
|
|
|
triggered by generated code (probably false positives). Fix some warnings in rts.c
|
|
Note that an alternative implementation choice is just to implement
them as SAIL functions manipulating a global variable.
Not sure which is better.
|
|
|
|
|
|
Necessary to prevent redundant clauses that Coq will reject
(There's still a problem if you use a variable rather than a wildcard,
see the test)
|
|
quite likely to exceed representable range of signed 64-bit integer (e.g. address starting 0x9...). Also make clear which values are displayed in hex vs. decimal.
|
|
access, and a cli option to control it.
|
|
|
|
|
|
privileges.
Also fix timer threshold comparison to be <= instead of <.
|
|
this a platform setting.
|
|
|
|
|
|
|
|
|
|
Remember and use fallthrough clauses instead of dropping them when the last
clause in a group has a guard
|
