| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-07 | Declare prelude functions as extern | Thomas Bauereiss | |
| Also, rename a few functions for uniformity, e.g. bool_and -> and_bool | |||
| 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). | |||
| 2017-08-24 | Fix some bugs related to the CHERI spec | Thomas Bauereiss | |
| - Correctly pass exponentials to Z3 - Infer types of functional record updates - Support "def Nat" | |||
| 2017-07-20 | add new CNEXEQ instruction. | Robert Norton | |
| 2017-07-04 | change to cgettype -- returns -1 if not sealed instead of 0. | Robert Norton | |
| 2017-07-03 | Update to copytype and ccseal -- now use belt and braces approach when ↵ | Robert Norton | |
| handling unsealed capabilities by clearing tag and setting cursor to -1. Also CCSeal got an encoding. | |||
| 2017-06-22 | fix a typo spotted in CPtrCmp instruction -- CLEU was using signed ↵ | Robert Norton | |
| comparison instead of unsigned. | |||
| 2017-06-22 | revised ccopytype with check for offset being in bounds and clearing tag ↵ | Robert Norton | |
| instead of using magic value if unsealed. Also corresponding CCSeal instruction which degrades to a cmove if ct.tag is unset. | |||
| 2017-06-16 | prefer arithmetic on integers followed by cast to bit[64] in CCopyType. | Robert Norton | |
| 2017-06-16 | remove unnecessary local variable definitions copy and pasted from cbuildcap. | Robert Norton | |
| 2017-06-16 | fix previous commit so that it builds. | Robert Norton | |
| 2017-06-16 | implement new CBuildCap and CCopyType instrucitons for ISAv6. | Robert Norton | |
| 2017-05-26 | add cmovz and cmovn conditional capability move instructions new in ISAv6. | Robert Norton | |
| 2017-05-26 | Update ctoptr instruction to check that all of ct is within bounds of cb and ↵ | Robert Norton | |
| that cb is not sealed as per ISAv6. | |||
| 2017-05-26 | in ISAv6 cjr and cjalr are permitted on local capabilities. | Robert Norton | |
| 2017-05-26 | add support for the new ccall selector 1 implementation that directly ↵ | Robert Norton | |
| unseals capabilities. | |||
| 2017-05-24 | Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵ | Robert Norton | |
| data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result. | |||
| 2017-05-10 | Fix type error in CGetLen | Thomas Bauereiss | |
| For some reason, Lem did not like the call to "min" when exporting to Isabelle. Replacing "min" with an if-then-else expression solves this. This is also in line with the CHERI spec, which actually uses an if block. | |||
| 2017-05-10 | Further to Thomas's commit remove the duplicate declarations of max_otype ↵ | Robert Norton | |
| and have_cp2. | |||
| 2017-05-10 | Comment out duplicate definitions in cheri_types.sail | Thomas Bauereiss | |
| They are already defined in cheri_prelude_common.sail | |||
| 2017-04-27 | avoid out of bounds indicies in cheri128 decompression functions. | Robert Norton | |
| 2017-04-27 | remove undefined value from cheri 128 spec. The ocaml shallow embedding ↵ | Robert Norton | |
| cannot handle undef structs and the value should not be used (could be option type but wanted a similar interface to incCapOffset and setCapOffset). | |||
| 2017-04-27 | fix incorrect vector index in cheri128 spec. Should ideally have been caught ↵ | Robert Norton | |
| by type checker... | |||
| 2017-04-27 | reverse endianness of data when writing UART. Altera jtag uart is ↵ | Robert Norton | |
| little-endian and this change allows it to work when writing using store word (as done by FreeBSD driver) or sb (as done by cheri helloworld program). | |||
| 2017-04-25 | Add support for uart terminal. Also add read_bit_reg function for faster and ↵ | Robert Norton | |
| neater access to registers of single bit. | |||
| 2017-04-20 | work around ocaml shallow embedding problem with matching on big_ints by ↵ | Robert Norton | |
| restructuing switch as if | |||
| 2017-04-20 | XXX remove pattern match not handled correctly by ocaml embedding. | Robert Norton | |
| 2017-04-18 | change to spec. of CLC instruction -- clear tag instead of exception if ↵ | Robert Norton | |
| permit_load_cap not set. | |||
| 2017-04-03 | Rename TranslateAddress to TranslatePC and remove the accessType argument -- ↵ | Robert Norton | |
| it is only ever used for translating the PC. | |||
| 2017-03-30 | Fix to csetboundsexact (was untested, same fix previously applied to ↵ | Robert Norton | |
| csetbounds but not here). | |||
| 2017-03-30 | Apparently the tag is on the other end following endianness change so ↵ | Robert Norton | |
| include it in the reverse. | |||
| 2017-03-29 | change reqiured to work with little endian interpreter. | Robert Norton | |
| 2017-03-24 | Minor cleanup: remove unnecessary brances and use 'not' iso ~. | Robert Norton | |
| 2017-03-24 | Extract CGetLen from cheri sail. | Robert Norton | |
| 2017-02-20 | slight refactoring of the fast representable bounds check to aid ↵ | Robert Norton | |
| understanding and remove case where E>=44 causes indexes off end of address. | |||
| 2017-02-17 | use fast representable check for csetoffset as well as cincoffset. | Robert Norton | |
| 2017-02-10 | Don't update EPCC if EXL is already set. | Robert Norton | |
| 2017-02-08 | Implement fast representable bounds check as used on FPGA (cincoffset only ↵ | Robert Norton | |
| so far). | |||
| 2017-02-08 | Simplify unsigned vector comparison using <_u operator. | Robert Norton | |
| 2017-02-03 | fix header dates in new file. | Robert Norton | |
| 2017-02-03 | replace bit vector return types in getCapX functions with equivalent integer ↵ | Robert Norton | |
| range types. This removes quite a few uses of unsigned() in cheri intsruction pseudocode. Could potentially take things furter. | |||
| 2017-02-03 | fix headers | Peter Sewell | |
| 2017-01-31 | Round up to multiple of 4 when computing E (CHERI does this to improve ↵ | Robert Norton | |
| frequency). | |||
| 2017-01-27 | further attempt to work around matching bug -- seems to work. | Robert Norton | |
| 2017-01-26 | fix incorrect constant in calculation of representable boundary (should be B ↵ | Robert Norton | |
| - 2**12) | |||
| 2017-01-26 | remove dead code in getBase/getTop | Robert Norton | |
| 2017-01-26 | attempted work around for apparent sail bug with matching result of comparison | Robert Norton | |
| 2017-01-26 | don't forget to use absolute PC as offset in epcc in case where epcc is not ↵ | Robert Norton | |
| representable. | |||
| 2017-01-26 | c128: xor E with 48 when storing in memory so that null cap is all zeros but ↵ | Robert Norton | |
| has non-zero E (latest spec.) | |||
| 2017-01-26 | when using cursor instead of offset for bounds check we must remember to ↵ | Robert Norton | |
| check base as well as top. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |