summaryrefslogtreecommitdiff
path: root/src/bitfield.ml
AgeCommit message (Collapse)Author
2019-02-08Add parameterization support for bitfields.Prashanth Mundkur
This supports the following syntax: type xlen : Int = 64 type ylen : Int = 1 type xlenbits = bits(xlen) bitfield Mstatus : xlenbits = { SD : xlen - ylen, SXL : xlen - ylen - 1 .. xlen - ylen - 3 }
2019-02-06Emacs mode understands relationships between Sail filesAlasdair
Allow a file sail.json in the same directory as the sail source file which contains the ordering and options needed for sail files involved in a specific ISA definition. I have an example for v8.5 in sail-arm. The interactive Sail process running within emacs then knows about the relationship between Sail files, so C-c C-l works for files in the ARM spec. Also added a C-c C-x command to jump to a type error. Requires yojson library to build interactive Sail.
2018-06-13Tracing instrumentation for C backendAlasdair Armstrong
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-02-21Create an update_field function for each field in a bitfield definitionAlasdair Armstrong
2018-02-20Allow overlapping bitfield field namesAlasdair Armstrong
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
2018-01-29Add rreg effect to _reg_deref in fix_val_specs rewriteThomas Bauereiss
The internal function _reg_deref is declared as pure, so that bitfield setters can be implemented as read-modify-write, while only having a wreg effect. However, for the Lem shallow embedding, the read step of those setters needs to be embedded into the monad. This could be special-cased in the Lem pretty printer, but then the pretty printer would have to replicate some logic of the letbind_effects rewriting step. It seems simplest to add the effect annotation early in the Lem rewriting pipeline, in the fix_val_specs step. This means that this rewriting step can only be used for other backends if these additional effects are acceptable.
2018-01-11Ocaml semantics can now run aarch64 hello world example using octapodAlasdair Armstrong
New testcase for bitfield syntax Updated to work with latest lem and linksem
2018-01-05Added bitfield syntax to replicate register bits typeAlasdair Armstrong
For example: bitfield cr : vector(8, dec, bit) = { CR0 : 7 .. 4, LT : 7, CR1 : 3 .. 2, CR2 : 1, CR3 : 0, } The difference this creates a newtype wrapper around the vector type, then generates getters and setters for all the fields once, rather than having to handle this construct separately in every backend.