| Age | Commit message (Collapse) | Author |
|---|
|
cleanly
|
|
now) to avoid coverage noise.
|
|
|
|
|
|
port.
|
|
We should test before the first iteration in case 'to' starts out as
less than 'from'.
|
|
bit loose, but conservative.
|
|
|
|
|
|
|
|
If a SEE exception is not caught within the decoder, it is
an error in the Sail implementation or in the instruction set spec.
This change ensures that we promptly detect and unambiguously report
such errors.
|
|
null capability while some still refer to DDC. Special registers moved out of general capability register file. All capabilties initialised to null except those required for MIPS compatibility.
|
|
The code to do this is rather ugly. It would be nice to have a generic
callgraph representation we could just query and not use the rewriter
in a weird way to extract this info.
|
|
|
|
|
|
|
|
Prevents partial unfolding of Z.pow.
|
|
Uses simple method of printing the entire record, in lieu of any decent
record update syntax.
|
|
|
|
|
|
|
|
|
|
This change causes execution of AArch32 code or ASIMD code
to fail with an easily diagnosed error message of the form
UNIMPLEMENTED: xxx support
where xxx is either AArch32 or ASIMD.
Having a clear error message allows these to be detected by triaging
scripts.
To make the AArch32 detection part work, you also need to change
HaveAnyAArch32 to read like this instead of just returning false.
function HaveAnyAArch32 () =
return ((CFG_ID_AA64PFR0_EL1_EL0 == 0x2)
|| (CFG_ID_AA64PFR0_EL1_EL1 == 0x2)
|| (CFG_ID_AA64PFR0_EL1_EL2 == 0x2)
|| (CFG_ID_AA64PFR0_EL1_EL3 == 0x2))
|
|
Fixes handling of Replicate(x, 0).
|
|
Added assertions to check that length of bit operations
is sensible (i.e., consistent with type system).
|
|
read/maintain
|
|
vector_update_subrange wasn't setting its return length correctly
|
|
|
|
While trying to track down some strange behaviour, I added a lot
more try-catch blocks that I think will be useful in the future.
Also dropped spurious escape effects on primops.
Also, only advance PC if we executed an instruction.
|
|
Making the message more like archex messages simplifies tooling.
Plus, it is a better message.
|
|
It appears that primops that have the escape effect are required to
write to the have_exception flag so I am dropping the effect from
primops that don't actually escape.
|
|
|
|
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
|
