summaryrefslogtreecommitdiff
path: root/cheri
AgeCommit message (Expand)Author
2018-05-21cheri: fix a bug in cfromptr: should give null result when value of rt is zer...Robert Norton
2018-05-18cheri: add support for clc with big immediate (clcbi). This is quite easily d...Robert Norton
2018-05-17Clean out old sequential filesBrian Campbell
2018-05-17Clean up CHERI HOL generation a little tooBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
2018-05-11Add Isabelle code generation for sequential CHERI modelThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
2018-05-10Document the register_inaccessible function.Robert Norton
2018-05-09Tweaks for sequential CHERI in HOLBrian Campbell
2018-05-09Use latex support for generating cheri documentation and remove sed based hac...Robert Norton
2018-05-09Add targets for counting lines in mips, cheri and riscv. Can use either slocc...Robert Norton
2018-05-09Remove start and end markers that are no longer needed now that sail has late...Robert Norton
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-07HOL script generation for library and CHERIBrian Campbell
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-05-04Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERIBrian Campbell
2018-05-01cheri128: remove unnecessary xor of E with 48. The zeroing of E in memory is ...Robert Norton
2018-05-01cheri256: minor optimisation -- factor out null_cap_bits as top level let.Robert Norton
2018-05-01cheri256: switch to using absolute address (cursor) instead of offset (relati...Robert Norton
2018-05-01remove unneeded commented out code.Robert Norton
2018-05-01Implement new CGetAddr instruction. Note that we should possibly rename funct...Robert Norton
2018-04-27Cheri ISA change in CTestSubset -- ignore sealed bits when testing for subset...Robert Norton
2018-04-23Add a cheri128_trace target.Robert Norton
2018-04-23Fix a discrepancy with spec. about which register number is reported for perm...Robert Norton
2018-04-23Fix a problem with 128-bit setCapBounds function revealed by CBuildCap test -...Robert Norton
2018-04-18fix bug in permissions test of ctestsubset.Robert Norton
2018-04-12remove cheri128 backwards compatibility hack that extended access_system_regs...Robert Norton
2018-04-12implement new permit_unseal used for CUnseal instead of permit_seal.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-09cheri: compute virtual address mod 2^64 when doing bounds check to avoid fail...Robert Norton
2018-04-04Fix another infinite loop in cast bit_to_bool. Following introduction of eq_b...Robert Norton
2018-03-27remove some unneeded else clauses.Robert Norton
2018-03-22Fix cheri MakefileAlasdair Armstrong
2018-03-22Fix C compilation for CHERI and MIPSAlasdair Armstrong
2018-03-21Patch AST datatypes in generated Isabelle theoriesThomas Bauereiss
2018-03-15Some CHERI compilation fixesThomas Bauereiss
2018-03-14Add and use execute_branch and execute_branch_pcc functions to align code wit...Robert Norton
2018-03-14rename EXTS and EXTZ to sign_extend and zero_extend because it is more obvios...Robert Norton
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss
2018-03-14minor cleanup of load -- we no longer need to separate out by access size bec...Robert Norton
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-08make HighestSetBit return option now that it can type check.Robert Norton
2018-03-07Fix cheri and mips following 1fe8f33fce5aaaaea82fc54b6d198ffc9d7e1eeb which r...Robert Norton
2018-03-06Add missing checks for permit_load and permit_store in capability load/store ...Robert Norton
2018-03-06Check tag of pcc in TranslatePC. This could happen after an ERET with untagge...Robert Norton
2018-03-06overload shift operators so they can be used with integer shifts in cheri128 ...Robert Norton
2018-03-06finish port of cheri128 spec. to sail2.Robert Norton