| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-04-09 | cheri: compute virtual address mod 2^64 when doing bounds check to avoid ↵ | Robert Norton | |
| failures with negative (i.e. large positive) offsets. | |||
| 2018-04-04 | Fix 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-27 | remove some unneeded else clauses. | Robert Norton | |
| 2018-03-22 | Fix cheri Makefile | Alasdair Armstrong | |
| 2018-03-22 | Fix C compilation for CHERI and MIPS | Alasdair 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-21 | Patch AST datatypes in generated Isabelle theories | Thomas 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-15 | Some CHERI compilation fixes | Thomas Bauereiss | |
| 2018-03-14 | Add and use execute_branch and execute_branch_pcc functions to align code ↵ | Robert Norton | |
| with existing MIPS and CHERI specs. | |||
| 2018-03-14 | rename EXTS and EXTZ to sign_extend and zero_extend because it is more ↵ | Robert Norton | |
| obviosu and to more closely match existing cheri pseudocode. | |||
| 2018-03-14 | Fix Lem generation for CHERI-MIPS and Aarch64 | Thomas 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-14 | minor cleanup of load -- we no longer need to separate out by access size ↵ | Robert Norton | |
| because the type checker is more clever. | |||
| 2018-03-14 | add extract of ccseal instruction. | Robert Norton | |
| 2018-03-14 | Add extract of some new instructions for including into CHERI documentation. | Robert Norton | |
| 2018-03-08 | rename mips_new_tc to mips | Robert Norton | |
| 2018-03-08 | make HighestSetBit return option now that it can type check. | Robert Norton | |
| 2018-03-07 | Fix cheri and mips following 1fe8f33fce5aaaaea82fc54b6d198ffc9d7e1eeb which ↵ | Robert Norton | |
| requires syntax change for unit constructors of union types. | |||
| 2018-03-06 | Add missing checks for permit_load and permit_store in capability load/store ↵ | Robert Norton | |
| instructions. Fixes fairly long-standing hole in architecture spotted by Kyndylan. | |||
| 2018-03-06 | Check tag of pcc in TranslatePC. This could happen after an ERET with ↵ | Robert Norton | |
| untagged EPCC. ISA says this results in undefined behaviour but it should probably not permit execution of code with untagged PCC. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |