| Age | Commit message (Collapse) | Author |
|---|
|
|
|
resolving the difference in type parameters between the prompt and state
monads, and allowing a single output file to be used with either.
Normally, the type alias is to the prompt monad, but for HOL4 we use the
state monad.
|
|
|
|
In order to use up-to-date sequential CHERI model for test suite
|
|
|
|
hack. Also some minor code cleanups and comments.
|
|
sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount.
|
|
|
|
(still needs some Lem work on types before it will be useful)
|
|
The datatype package of HOL4 does not support the prompt monad, so this patch
restores the option to generate a model that only uses the state monad. Also
add a Makefile target cheri_sequential.lem in the cheri/ directory.
|
|
|
|
function getCapCursor to getCapAddr.
|
|
|
|
|
|
|
|
eq_bool this was preferred over eq_bit when compiling the match on bit in bit_to_bool... Fix is to overload == before including flow.sail but feels a bit inelegant.
|
|
|
|
First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.
Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.
Finally support for vector literals that are non-bitvectors has been
added.
|
|
Deactivate plugins of the datatype package except for the size plugin in order
to keep processing time reasonable. This is currently only needed for the big
AST datatypes, so we just patch this using a sed command.
|
|
|
|
- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
(used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI
|
|
|
|
|
|
|
|
|
|
intialising and dumping CHERI state. Somewhat working cheri sail2 model.
|
|
|
|
|
|
|
|
instructions into manual. Whitespace only.
|
|
individual instructions to go in CHERI documentation.
|
