| Age | Commit message (Collapse) | Author |
|---|
|
Can now handle when an instantiation introduces more polymorphism. We
can now deal with the case where, for example, a type variable gets
specialised in two two steps, e.g. 'a => list('a) => list(int). Also
handle the case where a Type-kinded type variable gets substituted
with an Int-polymorphic type, e.g. 'a => atom('n).
This also fixes an issue where specialisation would loop due to
generated type variable names. This was fixed by ensuring that when we
convert an instantiation to a string to name the newly specialised
definition, we ensure that any alpha-equivalent instantiations map to
the same name.
|
|
Currently ignored in the state monad
|
|
Add an Undefined outcome to the prompt monad that asks the environment for a
Boolean value. For the state monad, add fields for a random generator and a
seed (currently of type nat) to the state.
|
|
Rather than just using strings to represent literals, now use value
types from sail_lib.lem to represent them. This allows for expressions
to be evaluated at compile time, which will be useful for future
optimisations involving constant folding and propagation, and allows
the intermediate bytecode to be interpreted using the same lem
builtins that the shallow embedding uses.
To get this to work I had to tweak the build process slightly to allow
ml files to import lem files from gen_lib/. Hopefully this doesn't
break anything!
|
|
The rewriter ignored loops that were not contained within some let-binding,
which later caused the Lem pretty-printer to fail (see #8).
|
|
Fix for loop in interactive interpreter
Fixes #8
|
|
|
|
intialising and dumping CHERI state. Somewhat working cheri sail2 model.
|
|
One caveat still: Won't work if the polymorphic definition consists of
multiple function clauses, but this seems unlikely - and I added an
error message if this is the case.
Also fix a small flow typing bug
Fixes #7
|
|
Previously this did not result in an error, but would cause issues
with generated code.
Fixes #5
|
|
Fixes #6
|
|
Fix some issues where some early returns in functions would cause
memory leaks, and optimize struct updates so the struct is not copied
uneccesarily.
Also make C print_bits match ocaml version output, and update tests.
|
|
|
|
|
|
|
|
With these optimisations on, now get about 10x performance over OCaml.
|
|
entry_point overflows an ocaml int.
|
|
Fixes #4
|
|
The suffix _lemmas is more descriptive than _extras.
|
|
Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle. In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.
|
|
Fixed an issue with pattern matching on enums
Fixed an issue whereby fix_early_returns would cause memory leaks
Added optimizations for some of the builtins used in the decode
function. Optimizations are turned on with the -O flag.
|
|
|
|
|
|
to_get_slice_int in less confusing way. Add arithmetic shift right.
|
|
Add support for short-ciruiting and/or. I forgot about this in the
original ANF specification and not having it causes problems for the
ARM spec.
|
|
(plus some adjustments for the test case)
|
|
|
|
|
|
|
|
|
|
Now compiles to C and builds a working executable. Just need to
correctly implement all the library builtins (some are still stubs),
and it should work.
|
|
|
|
const progagation.
Needed to avoid negative bitvector sizes on aarch64
Also propagate values found from "if var = const ...", which is needed in
aarch64
|
|
|
|
Just need to implement builtins, fix-up a few re-write passes, and
integrate some kind of elf-loading and it should work.
|
|
|
|
|
|
|
|
(otherwise you end up with div(64,8) in output sizes!)
|
|
|
|
|
|
(so that we get enough type annotations for bitvectors)
|
|
Allows bitfields to share field names by generating accessors as
_get/set_name_field where name is the type name and field is the field
name rather than _get/set_field. They are still accessed and set using
just register.field() and register.field() = value.
Fixes #1
|
|
|
|
|
|
Isabelle does not like nested annotations like "((exp :: typ) :: typ)".
|
|
|
|
Turns out the __TakeColdReset function is actually in the v8.3 XML. I
went and looked for it, and it's there, it just wasn't being picked up
by ASL parser because it's not called from any instructions. I added a
new field to the json config files for ASL parser that can tell it
about any such special functions that it should guarantee to include.
Also fixed a bug in C loop compilation
|
|
Goes through the C compiler without any errors, but as we still don't
have all the requisite builtins it won't actually produce an
executable. There are still a few things that don't work properly,
such as vectors of non-bit types - but once those are fixed and the
Sail library is implemented fully it should work.
|
|
Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad. Add some
Isabelle lemmas about the monad lifting.
Also drop the "_embed" and "_sequential" suffixes from names of generated
files.
|
