| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-07-31 | Remove old specs that have more up to date version | Alasdair | |
| Move outdated things into old subdirectory | |||
| 2018-09-21 | Remove cheri and mips specs -- they now have their own repository. | Robert Norton | |
| 2018-08-28 | Basic Makefile support for Coq generation from CHERI | Brian Campbell | |
| 2018-08-28 | Adapt theory imports for Isabelle 2018 | Thomas Bauereiss | |
| Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860 | |||
| 2018-07-27 | clean Makefile target to copy generated LaTeX to cheri-architecture | Peter Sewell | |
| 2018-07-27 | Revert "wib" (mistaken delete of sail_latexcc) | Peter Sewell | |
| This reverts commit 4c84c70eafbbf9bea475e3264f21eedc3555021f. | |||
| 2018-07-27 | wib | Peter Sewell | |
| 2018-07-27 | Check in snapshot of cheri latex | Alasdair Armstrong | |
| 2018-07-10 | Make HOL build properly again for all of the models | Brian Campbell | |
| 2018-07-06 | Change HighestSetBit into a form that can be handled by c backend. There are ↵ | Robert Norton | |
| still a few builtins missing before cheri128 will work. | |||
| 2018-07-06 | add gcov option for cheri_c. Add cheri128_c target. | Robert Norton | |
| 2018-07-03 | cheri: refine lwl/lwr cap length checks to be exact. They were previously a ↵ | Robert Norton | |
| bit loose, but conservative. | |||
| 2018-07-03 | cheri: update to register file semantics. Most instructions now treat c0 as ↵ | Robert Norton | |
| null capability while some still refer to DDC. Special registers moved out of general capability register file. All capabilties initialised to null except those required for MIPS compatibility. | |||
| 2018-07-02 | cheri: the default cap for 256-bits no longer has reserved bits set. | Robert Norton | |
| 2018-07-02 | optimise cheri c build. | Robert Norton | |
| 2018-06-28 | Add tagged memory to C rts to cheri can be compiled to C | Alasdair Armstrong | |
| 2018-06-28 | Add option to build ocaml with bisect_ppx coverage support. Add cheri ↵ | Robert Norton | |
| targets using this. | |||
| 2018-06-26 | turn 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-06-04 | add missing semi colon in arichardsons patch. | Robert Norton | |
| 2018-05-31 | Also dump the cap hwregs in dump_cp2_state | Alexander Richardson | |
| Dump format is the same as for the cap GPRs with DEBUG CAP HWREG as the prefix | |||
| 2018-05-21 | cheri: fix a bug in cfromptr: should give null result when value of rt is ↵ | Robert Norton | |
| zero not only when rt is the zero register (zr). | |||
| 2018-05-18 | cheri: add support for clc with big immediate (clcbi). This is quite easily ↵ | Robert Norton | |
| done by making it decode to same CLC ast node and extending length of immediate field to 16 bits. cscbi is not supported as the feeling is that it will not be needed. | |||
| 2018-05-17 | Clean out old sequential files | Brian Campbell | |
| 2018-05-17 | Clean up CHERI HOL generation a little too | Brian Campbell | |
| 2018-05-17 | Use 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-11 | Add Isabelle code generation for sequential CHERI model | Thomas Bauereiss | |
| 2018-05-11 | Merge branch 'sail2' into cheri-mono | Thomas Bauereiss | |
| In order to use up-to-date sequential CHERI model for test suite | |||
| 2018-05-10 | Document the register_inaccessible function. | Robert Norton | |
| 2018-05-09 | Tweaks for sequential CHERI in HOL | Brian Campbell | |
| 2018-05-09 | Use latex support for generating cheri documentation and remove sed based ↵ | Robert Norton | |
| hack. Also some minor code cleanups and comments. | |||
| 2018-05-09 | Add 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-09 | Remove start and end markers that are no longer needed now that sail has ↵ | Robert Norton | |
| latex output. | |||
| 2018-05-09 | Add tests for Isabelle->OCaml generation for CHERI and AArch64 | Thomas Bauereiss | |
| 2018-05-07 | HOL script generation for library and CHERI | Brian Campbell | |
| (still needs some Lem work on types before it will be useful) | |||
| 2018-05-04 | Add back purely sequential Lem generation | Thomas 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-04 | Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERI | Brian Campbell | |
| 2018-05-01 | cheri128: remove unnecessary xor of E with 48. The zeroing of E in memory is ↵ | Robert Norton | |
| achieved by xoring with null_cap_bits so this was only affecting register representation. | |||
| 2018-05-01 | cheri256: minor optimisation -- factor out null_cap_bits as top level let. | Robert Norton | |
| 2018-05-01 | cheri256: switch to using absolute address (cursor) instead of offset ↵ | Robert Norton | |
| (relative) representation in capability registers, making register and memory format the same and slightly simplifying code. Next step: use struct representation in registers eliminating many conversions between struct and bits? | |||
| 2018-05-01 | remove unneeded commented out code. | Robert Norton | |
| 2018-05-01 | Implement new CGetAddr instruction. Note that we should possibly rename ↵ | Robert Norton | |
| function getCapCursor to getCapAddr. | |||
| 2018-04-27 | Cheri ISA change in CTestSubset -- ignore sealed bits when testing for ↵ | Robert Norton | |
| subset (aids garbage collection). | |||
| 2018-04-23 | Add a cheri128_trace target. | Robert Norton | |
| 2018-04-23 | Fix a discrepancy with spec. about which register number is reported for ↵ | Robert Norton | |
| permissions failure in CBuildCap. | |||
| 2018-04-23 | Fix a problem with 128-bit setCapBounds function revealed by CBuildCap test ↵ | Robert Norton | |
| -- an assertion failure that new bounds are exact. The address of the new cap should have address=base (i.e. offset=0) but this was not being set. This was not previously visible because all other uses of setCapBounds already have address=newBase when calling. | |||
| 2018-04-18 | fix bug in permissions test of ctestsubset. | Robert Norton | |
| 2018-04-12 | remove cheri128 backwards compatibility hack that extended ↵ | Robert Norton | |
| access_system_regs perm into bits 14-11 -- it looks like spec is heading that way. | |||
| 2018-04-12 | implement new permit_unseal used for CUnseal instead of permit_seal. | Robert Norton | |
| 2018-04-12 | add a cheri_trace target for conveniently building a debug build. | Robert Norton | |
| 2018-04-12 | Add implementations of CReadHwr and CWriteHwr | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |