| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Make all backends behave the same when a catch block does not catch a
specific exception.
|
|
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
|
|
|
|
|
|
|
|
|
|
Fix pretty printer bug
|
|
|
|
now that cast insertion can handle RISC-V
Also inserts specs for casts in they're not present
|
|
otherwise the valspec rewriting will be inconsistent with the type
annotation. Note that the type checker will have introduced valspecs
where necessary.
|
|
# Conflicts:
# src/monomorphise.ml
|
|
|
|
|
|
It now pushes casts into lets and constructor applications, and so
supports the case needed for RISC-V.
|
|
|
|
|
|
|
|
|
|
Not ideal because it keeps everything that's not a function, but good
enough for quick tests extracted from arm.
|
|
|
|
|
|
|
|
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.
|
