summaryrefslogtreecommitdiff
path: root/cheri/Makefile
AgeCommit message (Collapse)Author
2018-09-21Remove cheri and mips specs -- they now have their own repository.Robert Norton
2018-08-28Basic Makefile support for Coq generation from CHERIBrian Campbell
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
2018-07-27clean Makefile target to copy generated LaTeX to cheri-architecturePeter Sewell
2018-07-27Revert "wib" (mistaken delete of sail_latexcc)Peter Sewell
This reverts commit 4c84c70eafbbf9bea475e3264f21eedc3555021f.
2018-07-27wibPeter Sewell
2018-07-10Make HOL build properly again for all of the modelsBrian Campbell
2018-07-06add gcov option for cheri_c. Add cheri128_c target.Robert Norton
2018-07-02optimise cheri c build.Robert Norton
2018-06-28Add tagged memory to C rts to cheri can be compiled to CAlasdair Armstrong
2018-06-28Add option to build ocaml with bisect_ppx coverage support. Add cheri ↵Robert Norton
targets using this.
2018-06-26turn on warnings when compiling mips c then dial back ones that are ↵Robert Norton
triggered by generated code (probably false positives). Fix some warnings in rts.c
2018-05-17Clean up CHERI HOL generation a little tooBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
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.
2018-05-11Add Isabelle code generation for sequential CHERI modelThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
In order to use up-to-date sequential CHERI model for test suite
2018-05-09Tweaks for sequential CHERI in HOLBrian Campbell
2018-05-09Use latex support for generating cheri documentation and remove sed based ↵Robert Norton
hack. Also some minor code cleanups and comments.
2018-05-09Add targets for counting lines in mips, cheri and riscv. Can use either ↵Robert Norton
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.
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-07HOL script generation for library and CHERIBrian Campbell
(still needs some Lem work on types before it will be useful)
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
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.
2018-05-04Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERIBrian Campbell
2018-05-01Implement new CGetAddr instruction. Note that we should possibly rename ↵Robert Norton
function getCapCursor to getCapAddr.
2018-04-23Add a cheri128_trace target.Robert Norton
2018-04-12add a cheri_trace target for conveniently building a debug build.Robert Norton
2018-04-12Add implementations of CReadHwr and CWriteHwrRobert Norton
2018-04-04Fix another infinite loop in cast bit_to_bool. Following introduction of ↵Robert Norton
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.
2018-03-22Fix cheri MakefileAlasdair Armstrong
2018-03-22Fix C compilation for CHERI and MIPSAlasdair Armstrong
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.
2018-03-21Patch AST datatypes in generated Isabelle theoriesThomas Bauereiss
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.
2018-03-15Some CHERI compilation fixesThomas Bauereiss
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss
- 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
2018-03-14add extract of ccseal instruction.Robert Norton
2018-03-14Add extract of some new instructions for including into CHERI documentation.Robert Norton
2018-03-08rename mips_new_tc to mipsRobert Norton
2018-03-06finish port of cheri128 spec. to sail2.Robert Norton
2018-03-01Add support for read_tag and write_tag in sail_lib.ml. and support for ↵Robert Norton
intialising and dumping CHERI state. Somewhat working cheri sail2 model.
2018-03-01cheri wip.Robert Norton
2017-03-24Extract CGetLen from cheri sail.Robert Norton
2017-01-24first pass at cheri128 sail.Robert Norton
2016-07-27Normalise whitespace in cheri_insts.sail for cleaner extraction of ↵Robert Norton
instructions into manual. Whitespace only.
2016-07-26Add Makefile and marker comments in cheri sail file for extracting ↵Robert Norton
individual instructions to go in CHERI documentation.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 23:12:04 +0000