| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
- Use simplified monad type (e.g., without the with_aux constructors that are
not needed by the shallow embedding).
- Add support for registers with arbitrary types (e.g., records, enumerations,
vectors of vectors). Instead of using bit lists as the common representation
of register values at the monad interface, use a register_value type that is
generated per spec as a union of all register types that occur in the spec.
Conversion functions between register_value and concrete types are generated.
- Use the same representation of register references as the state monad, in
preparation of rebasing the state monad onto the prompt monad.
- Split out those types from sail_impl_base.lem that are used by the shallow
embedding into a new module sail_instr_kinds.lem, and import that. Removing
the dependency on Sail_impl_base from the shallow embedding avoids name clashes
between the different monad types.
Not yet done:
- Support for reading/writing register slices. Currently, a rewriting pass
pushes register slices in l-expressions to the right-hand side, turning a
write to a register slice into a read-modify-write. For interfacing with the
concurreny model, we will want to be more precise than that (in particular
since some specs represent register files as big single registers containing a
vector of bitvectors).
- Lemmas about the conversion functions to/from register_value should be
generated automatically.
|
|
|
|
Also update the main aarch64 (no_vector) spec with latest asl_parser
|
|
|
|
|
|
|
|
|
|
Useful for feature functions, e.g. HaveFP16Ext
|
|
|
|
Solves a problem where generated kids crept into type annotations during
rewriting and caused later typechecking passes to fail.
|
|
(still some work to do in AtomToItself rewrite, but should work despite
error messages)
|
|
|
|
|
|
Describes precisely the intermediate representation used in the C
backend in an ott grammar, and also removes several C-isms where raw C
code was inserted into the IR, so in theory this IR could be
interpreted by a small VM/interpreter or compiled to LLVM bytecode
etc. Currently the I_raw constructor for inserting C code is just used
for inserting GCC attributes, so it can safely be ignored.
Also augment and refactor the instruction type with an aux constructor
so location information can be propagated down to this level.
|
|
Option -ddump_flow_graphs when used with -c will create graphviz files
for each function in the specification with control and data
dependencies shown.
|
|
|
