summaryrefslogtreecommitdiff
path: root/cheri/cheri_prelude_common.sail
AgeCommit message (Collapse)Author
2018-09-21Remove cheri and mips specs -- they now have their own repository.Robert Norton
2018-07-03cheri: refine lwl/lwr cap length checks to be exact. They were previously a ↵Robert Norton
bit loose, but conservative.
2018-07-03cheri: 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-06-04add missing semi colon in arichardsons patch.Robert Norton
2018-05-31Also dump the cap hwregs in dump_cp2_stateAlexander Richardson
Dump format is the same as for the cap GPRs with DEBUG CAP HWREG as the prefix
2018-05-10Document the register_inaccessible function.Robert Norton
2018-05-09Use latex support for generating cheri documentation and remove sed based ↵Robert Norton
hack. Also some minor code cleanups and comments.
2018-04-12implement new permit_unseal used for CUnseal instead of permit_seal.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 ↵Robert Norton
failures with negative (i.e. large positive) offsets.
2018-03-14Add and use execute_branch and execute_branch_pcc functions to align code ↵Robert Norton
with existing MIPS and CHERI specs.
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas 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-06Check 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-06finish port of cheri128 spec. to sail2.Robert Norton
2018-03-02remove workaround for #8 now that it is fixed.Robert Norton
2018-03-02work around bug in ocaml foreach generation -- end point not included in ↵Robert Norton
loop (see #8).
2018-03-02add a cp2_next_pc function to update cheri state in fde loop and a stub ↵Robert Norton
version for mips.
2018-03-02add space in cap dump format to match that expected by test framework.Robert Norton
2018-03-01Add 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-01cheri wip.Robert Norton
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-10-31work around interpreter crash by adding cast. Likely this kind of thing will ↵Robert Norton
be resolved by merge of new_tc branch.
2017-10-31cheri: 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-08-29Make Lem export of CHERI(-256) typecheckThomas 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-07-20add new CNEXEQ instruction.Robert Norton
2017-05-26add support for the new ccall selector 1 implementation that directly ↵Robert Norton
unseals capabilities.
2017-05-24Change 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-04-27reverse 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-25Add support for uart terminal. Also add read_bit_reg function for faster and ↵Robert Norton
neater access to registers of single bit.
2017-04-20XXX remove pattern match not handled correctly by ocaml embedding.Robert Norton
2017-04-03Rename TranslateAddress to TranslatePC and remove the accessType argument -- ↵Robert Norton
it is only ever used for translating the PC.
2017-03-30Apparently the tag is on the other end following endianness change so ↵Robert Norton
include it in the reverse.
2017-03-29change reqiured to work with little endian interpreter.Robert Norton
2017-03-24Minor cleanup: remove unnecessary brances and use 'not' iso ~.Robert Norton
2017-02-10Don't update EPCC if EXL is already set.Robert Norton
2017-02-03replace 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-03fix headersPeter Sewell
2017-01-26don't forget to use absolute PC as offset in epcc in case where epcc is not ↵Robert Norton
representable.
2017-01-26c128: 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-25fix error introduced in revised version of TranslateAddress -- absPC should ↵Robert Norton
be relative to base
2017-01-25merge cheri 256 and 128 together factoring out differing parts into separate ↵Robert Norton
cheri_prelude files.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 09:26:57 +0000