| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Only check for availability of Lem library if actually trying to build
an Isabelle heap image.
|
|
|
|
|
|
toolchain; use SAIL_RISCV instead to refer to sail-riscv.
|
|
|
|
Since Isabelle 2018, specifying the same directory both on the command
line and persistently in the user's ROOTS file is allowed, so we don't
have to choose between one or the other any more.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(which allows us to avoid a Coq bug where the proof isn't recorded
correctly)
|
|
|
|
|
|
|
|
Fixes some re-writer issues that was preventing RISC-V from building
with new flow-typing constraints. Unfortunately because the flow
typing now understands slightly more about boolean variables, the very
large nested case statements with matches predicates produced by the
string-matching end up causing a huge blowup in the overall
compilation time.
|
|
|
|
|
|
Also output termination measures in Sail printer
|
|
bool_of_bit and bit_of_bool in sail_lib
|
|
subrange_subrange_concat does a zero extension internally, so another
zero extension of its result is redundant and can lead to a type error
in Lem (because Lem's type system cannot calculate the length of the
intermediate result of subrange_subrange_concat).
|
|
Sizeof-rewriting could introduce extra arguments to functions that
instantiate_simple_equations could fill in with overly complicated
types, causing unification to fail when building lem.
|
|
|
|
It now includes updating the effects so that morally pure recursive
functions can be turned into this impure termination-by-assertion form.
|
|
|
|
This only applies to recursive functions and uses the termination measure
merely as a limit to the recursive call depth, rather than proving the
measure correct.
|
|
|
|
* 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
|
|
The inter-instruction semantics is responsible for correctly handling memory
writes without tags; the lifting to the state monad handles it as writing a
value with a zero tag bit.
|
|
Use E_read_memt for reading tagged memory, as in sail2_impl_base.lem,
and rename E_write_mem to E_write_memt, since it always writes a tag.
|
|
- 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.
|
|
It is used for nondeterministic choice, so Undefined might be
misleading.
|
|
- Fix pretty printing nested constraints
- Add flow typing for if condition then { throw exn }; ... blocks
- Add optimisations for bitvector concatenation in C
|
|
Lets one distinguish in a trace whether an instruction tried to read
tagged memory or just read data without caring about the tag; this is
useful for formulating predicates on traces.
|
|
|
