| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2018-03-06 | overload shift operators so they can be used with integer shifts in cheri128 ↵ | Robert Norton | |
| definitions. | |||
| 2018-03-06 | finish port of cheri128 spec. to sail2. | Robert Norton | |
| 2018-03-02 | remove workaround for #8 now that it is fixed. | Robert Norton | |
| 2018-03-02 | work around bug in ocaml foreach generation -- end point not included in ↵ | Robert Norton | |
| loop (see #8). | |||
| 2018-03-02 | add a cp2_next_pc function to update cheri state in fde loop and a stub ↵ | Robert Norton | |
| version for mips. | |||
| 2018-03-02 | add space in cap dump format to match that expected by test framework. | Robert Norton | |
| 2018-03-02 | cheri tests expect reserved permission bits to be initialised to one. | Robert Norton | |
| 2018-03-01 | Add 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-01 | cheri wip. | Robert Norton | |
| 2018-02-06 | immediate for CIncOffsetImmediate must be treated as signed (fixes ↵ | Robert Norton | |
| test_cp2_rep_underflow). | |||
| 2017-12-06 | Make CHERI spec type-check again | Thomas Bauereiss | |
| 2017-11-30 | Merge branch 'master' into experiments | Alasdair Armstrong | |
| 2017-11-07 | Declare prelude functions as extern | Thomas Bauereiss | |
| Also, rename a few functions for uniformity, e.g. bool_and -> and_bool | |||
| 2017-11-01 | workaound for another odd interpreter error where top level let variable got ↵ | Robert Norton | |
| truncated to 64 bits... | |||
| 2017-10-31 | work around interpreter crash by adding cast. Likely this kind of thing will ↵ | Robert Norton | |
| be resolved by merge of new_tc branch. | |||
| 2017-10-31 | cheri: throw an exception if there is an attempt to access C26/IDC in the ↵ | Robert Norton | |
| delay slot of a ccall selector 1 call. | |||
| 2017-10-31 | cheri: ccall selector 1 should have a branch delay slot. TODO we need to ↵ | Robert Norton | |
| throw exception for access to IDC/C26 in branch delay slot. | |||
| 2017-10-24 | fix default cap value on cheri128 following previous changes -- E stored in ↵ | Robert Norton | |
| registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length. | |||
| 2017-10-23 | cheri: Null capability should have maximum length, because in cheri128 we ↵ | Robert Norton | |
| want all offsets to be representable. To maintain all-zeros as the in-memory representation of the null capability we xor memory bits with null capability when loading and storing. | |||
| 2017-10-16 | add CTestSubset instruction. | Robert Norton | |
| 2017-10-16 | add missing new encodings for CJR and CJALR. | Robert Norton | |
| 2017-10-16 | implement CMove as an alias for cmovz with zero register. | Robert Norton | |
| 2017-10-16 | add support for CIncOffsetImmediate and CSetBoundsImmediate. | Robert Norton | |
| 2017-10-16 | add support for capability branch null instructions. | Robert Norton | |
| 2017-10-13 | Add support for new cheri instruction encodings. The order of pattern ↵ | Robert Norton | |
| matching is now significant because register no. fields are re-used as additional function codes in operations with fewer operands so I pulled out all decode clauses to the beginning of file for easier rearranging. Old encodings can co-exist with new encodings as the only overlap is for recently added instructions which already use the new scheme. Eventually the old encodings will go away, however, and the opcode space may be reclaimed." | |||
| 2017-10-02 | cheri: fix swapped cmovz and cmovn. | Robert Norton | |
| 2017-08-29 | Make Lem export of CHERI(-256) typecheck | Thomas Bauereiss | |
| Note: The effect annotations of the execute function differ between CHERI and MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the initial declarations of ast, decode, and execute (with the right effects for MIPS). | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |