| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
|
|
|
|
Usually we want to unify on return types, but in the case of
constraint unification (especially during rewriting) we can find
ourselves in the situation where unifying too eagerly on a return
type like bool('p & 'q) can cause us to instantiate 'p and 'q in the
wrong order (as & should really respect commutativity and
associativity during typechecking to avoid being overly brittle).
Originally I simply avoided adding cases for unify on NC_and/NC_or
and similar to avoid these cases, but this lead to the undesirable
situation where identical types wouldn't unify with each other for
an empty set of goals, which should be a trivial property of the
unification functions.
The solution is therefore to identify type variables in ambiguous
positions, and remove them from the list of goals during
unification. All type variables still have to be resolved by the
time we finish checking each application, but this has the added
bonus of making order much less important when it comes to
instantiating type variables.
Currently I am overly conservative about what qualifies as
ambigious, but this set should be expanded
|
|
I guess that Sail became a bit more strict about typechecking variables in
the last few months.
|
|
Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues
|
|
* Improve type inference for numeric if statements (if_infer test)
* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)
* Canonicalise all numeric types in function arguments, which
triggers some weird edge cases between parametric polymorphism and
subtyping of numeric arguments
* Because of this eq_int, eq_range, and eq_atom etc become identical
* Avoid duplicating destruct_exist in Env
* Handle some odd subtyping cases better
|
|
- Completely remove the nexp = nexp syntax in favour of nexp ==
nexp. All our existing specs have already switched over. As part of
this fix every test that used the old syntax, and update the
generated aarch64 specs
- Remove the `type when constraint` syntax. It just makes changing the
parser in any way really awkward.
- Change the syntax for declaring new types with multiple type
parameters from:
type foo('a : Type) ('n : Int), constraint = ...
to
type foo('a: Type, 'n: Int), constraint = ...
This makes type declarations mimic function declarations, and makes
the syntax for declaring types match the syntax for using types, as
foo is used as foo(type, nexp). None of our specifications use types
with multiple type parameters so this change doesn't actually break
anything, other than some tests. The brackets around the type
parameters are now mandatory.
- Experiment with splitting Type/Order type parameters from Int type
parameters in the parser.
Currently in a type bar(x, y, z) all of x, y, and z could be either
numeric expressions, orders, or types. This means that in the parser
we are severely restricted in what we can parse in numeric
expressions because everything has to be parseable as a type (atyp)
- it also means we can't introduce boolean type
variables/expressions or other minisail features (like removing
ticks from type variables!) because we are heavily constrained by
what we can parse unambigiously due to how these different type
parameters can be mixed and interleaved.
There is now experimental syntax: vector::<'o, 'a>('n) <-->
vector('n, 'o, 'a) which splits the type argument list into two
between Type/Order-polymorphic arguments and Int-polymorphic
arguments. The exact choice of delimiters isn't set in stone - ::<
and > match generics in Rust. The obvious choices of < and > / [ and
] are ambigious in various ways.
Using this syntax right now triggers a warning.
- Fix undefined behaviour in C compilation when concatenating a
0-length vector with a 64-length vector.
|
|
|
|
|
|
|
|
- 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
|
|
|
