| Age | Commit message (Collapse) | Author |
|---|
|
|
|
- implement set_slice and set_slice_int
- lemmas for more constraints
- make real sqrt visible
- unfolding list membership needs andb and orb to be handled first
|
|
|
|
|
|
- hints for dotp
- handle exists separately when trying eauto to keep search depth low
- more uniform existential handling (i.e., we now handle all existentials
in the way we used to only handle existentials around atoms)
|
|
|
|
constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.
Also
- Don't simplify nexps before printing (note that we usually end up
needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
fill in metavariables (because manipulating the goal can interfere with
instantiating them)
- Update RISC-V patch
|
|
Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
|
|
Removes the need for the node type to have a valid Hash function
|
|
|
|
|
|
Several v8.4 tests were failing because they attempted to enter EL2 secure
mode (which is supported on v8.4 but not on v8.3).
This test detects an attempt to enter EL2 secure and reports an easily diagnosed
error message.
|
|
Uses previous stage to deal with (e.g.) guards.
New option -dcoq_warn_nonex tells you where all of the extra default
cases were added.
|
|
Use eauto so that user-added hints are more flexible,
example with Replicate in aarch64, dropped zbool to prevent slow
proof searches (and preprocessing deals with boolean comparisons now).
Report failed constraints after preprocessing;
Separate preprocessing tactic out.
|
|
interpreter implementations of same.
|
|
|
|
|
|
Makes CheckAndUpdateDescriptor respect endianness
|
|
|
|
update aarch64 model
|
|
|
|
|
|
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.
|
|
|
|
|
|
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.
|
|
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))
|
|
read/maintain
|
|
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.
|
|
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
|
|
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.
|
|
|
|
No functional change
|
|
|
|
Mostly improving error messages
|
|
|
|
|
|
Note that an alternative implementation choice is just to implement
them as SAIL functions manipulating a global variable.
Not sure which is better.
|
|
|
|
|
|
|
|
optimizations.
Move the utility functions for graph generation and pretty printing of
intermediate representation instructions into a separate file,
bytecode_util.ml, by analogy with ast_util.ml.
Add an optimization pass that searches for specific patterns of struct
updates and removes uncessary copying of the structs involved. With
this optimisation pass the time taken for u-boot to run approx
57,000,000 instructions goes down from about 11-12 minutes to 8
minutes (about 120,000 IPS).
|
|
Also add an additional -Oz3 flag that uses z3 to optimize some
additional types. This is currently very experimental and doesn't
fully work yet.
|
|
|
|
|
|
Worked around problem with the model where it tries to use bound variables
in patterns
|
|
|
