| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Define initial values for record types once instead of repeating them in
the initial register state.
|
|
|
|
Don't ask Z3 to simplify them, as flow typing might lead to different
results in different if-branches, for example, leading to type errors in
Lem.
|
|
|
|
|
|
Now supports mutual recursion, configuration registers (in the same way
as Lem), boolean constraints (but produces some ugly stuff that the solver
can't handle).
|
|
|
|
|
|
|
|
Copied from a corresponding case for E_block, so that this flow typing
still gets picked up after E_block has been rewritten away.
|
|
For example in RISC-V for the translation table walk:
$optimize unroll 2
val walk32 ...
function walk32 ...
would create two extra copies of the walk_32 function,
walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2
being recursive. Currently we only support the case where we have
$optimize unroll, directly followed by a valspec, then a function, but
this should be generalised in future.
This optimization nearly doubles the performance of RISC-V
It is implemented using a new Optimize.recheck rewrite that replaces
the ordinary recheck_defs pass. It uses a new typechecker
check_with_envs function that allows re-writes to utilise intermediate
typechecking environments to minimize the amount of AST checking that
occurs, for performance reasons.
Note that older Sail versions including the current OPAM release will
complain about the optimize pragma, so this cannot be used until they
become up to date with this change.
|
|
RISC-V
|
|
|
|
|
|
|
|
since riscv is no longer in this repository, and we use the RISC-V
duopod as an example, you need to build as:
make RISCV=directory manual.pdf
if directory is not equal to ../../sail-riscv (which is where it would
be if sail and sail-riscv are checked out in the same respository
together)
|
|
We should maybe just make the -latex option behavior the default to avoid this kind of thing
|
|
If we use the bitlist representation of bitvectors, the type argument in
type abbreviations such as "bits('n)" becomes dead, which confuses HOL;
as a workaround, expand type synonyms in this case.
|
|
Treat them as constants for now (with their initial value); in order to
support updates, we would have to embed them properly into the monads.
|
|
Don't wrap effectful expressions in E_internal_return
|
|
|
|
|
|
rewrite_defs_base_parallel j is the same as rewrite_defs_base
except it performs the re-writes in j parallel processes. Currently
only the trivial_sizeof re-write is parallelised this way with a
default of 4. This works on my machine (TM) but may fail elsewhere.
Because 2019 OCaml concurrency support is lacking, we use Unix.fork
and Marshal.to_channel to send the info from the child processes
performing the re-write back to the parent.
Also fix a missing case in pretty_print_lem
|
|
|
|
Bind loop bounds to type variables, and don't pull existential variables
out of context
|
|
|
|
We want to ensure that no_devices.sail and devices.sail have the same
effect footprint, because with a snapshot-type release in sail-arm, we
can't rebuild the spec with asl_to_sail every time we switch from
running elf binaries to booting OS's. This commit allows registers to
have arbitrary effects, so registers that are really representing
memory-mapped devices don't have to have the wmem/rmem effect.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
There are situations when we really want a more refined expression,
such as 8 * n instead of 64 (when we know n = 8 from a case split), but
we might not be able to generate it. For now we generate an underscore
and let Coq figure it out from the context.
|
|
|
|
Remove unused name schemes and DEF_kind
|
|
|
|
|
|
|
|
With the new comment syntax, Isabelle seems to barf on that comment,
apparently due to the backslashes.
|
|
|
|
Work on improving the formatting and quality of error messages
When sail is invoked with sail -i, any type errors now drop the user
down to the interactive prompt, with the interactive environment being
the environment at the point the type error occurred, this means the
typechecker state can be interactively queried in the interpreter to help
diagnose type errors.
|
|
Remove redundant variables in boolean existentials. A situation can occur
during re-writing when patterns are re-written into simpler guarded
patterns, with the guard containing a large conjunction. Often those
individual conjuncts have no meaning for flow typing, but we'll still
generate a large conjunct bool('p & 'q & 'r & 's ...) for the guard. Now
we can simplify that return type by combining all the type variables
that don't give us any information into a single one, which improves
performance as we can avoid passing all those variables to the
constraint solver.
|
