| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-04 | Merge remote-tracking branch 'origin/master' into experiments | Alasdair Armstrong | |
| 2017-12-04 | renamed hgen to gen | Shaked Flur | |
| 2017-11-30 | Merge branch 'master' into experiments | Alasdair Armstrong | |
| 2017-11-30 | match what rmem (ppcmem2) expects from ISA Makefiles | Shaked Flur | |
| 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-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-12 | Work around warning in ocaml shallow embedding of mips caused by buggy code ↵ | Robert Norton | |
| generation for dubious casting enumeration to int. | |||
| 2017-08-17 | Merge remote-tracking branch 'origin' into mono-experiments | Brian Campbell | |
| # Conflicts: # src/type_internal.ml | |||
| 2017-08-15 | remove unneeded regs_out_in.hgen files. | Robert Norton | |
| 2017-07-27 | Merge branch 'master' into sail_new_tc | Alasdair Armstrong | |
| 2017-07-26 | mips_extras.lem: fix references to Interp.V_foo | Jon French | |
| 2017-06-21 | Pretty-print bitvector expressions | Thomas Bauereiss | |
| - Add case distinctions between bitvector types and vectors of other element types (e.g. registers) and use the corresponding operations (i.e. "bvslice", "bvaccess", etc for the former, and "slice", "access", etc for the latter) when pretty-printing expressions - Add type annotations to expressions when the type includes bitvectors with concretely known length - Update state.lem to use bitvectors (in the interface, at least; internally, bitvectors are still stored as bit lists for now, since that makes it easier to support storing different registers with different lengths) This has been tested with the CHERI-MIPS model with some success, but some things are still missing: - Bitvector patterns are not handled yet - Some bitvector length monomorphisation is needed in a few places of the model - Some type annotations are missing, because the (old) Sail type checker does not infer bitvector lengths in some instances where one would hope it to do that; this should be checked with the new type checker | |||
| 2017-06-02 | Add tag memory to Lem shallow embedding | Thomas Bauereiss | |
| 2017-05-24 | fixed missing _tag bits | Shaked Flur | |
| 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 | Add stubs for TAGw | Thomas Bauereiss | |
| Tagged memory seems to be currently missing in the Lem shallow embedding of (CHERI-)MIPS. | |||
| 2017-04-27 | also trace memory writes. | Robert Norton | |
| 2017-04-27 | fix cheri128 model referring to wrong registers and not capreg printing. | Robert Norton | |
| 2017-04-27 | need brackets around try ... with expression. | Robert Norton | |
| 2017-04-27 | add command line argument for setting undef values to all zero or all one. ↵ | Robert Norton | |
| Some tests intentionally produce undefined values (e.g. divide by zero) and this might be required for them to work. | |||
| 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 | extend the try around call to select to avoid gprof crashing with EINTR. | Robert Norton | |
| 2017-04-25 | replace memory representation with map of 1MB pages rather than map of ↵ | Robert Norton | |
| bytes. This makes loading binaries much quicker but doesn't seem to make a big difference to execution speed. | |||
| 2017-04-25 | Don't die if stdin gets closed (e.g. when running unit tests). | Robert Norton | |
| 2017-04-25 | support loading more than one raw file as anonymous arguments so that we can ↵ | Robert Norton | |
| load simboot + kernel. | |||
| 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-21 | it turns out zarith has a function for printing big_ints in hex. Remove the ↵ | Robert Norton | |
| dependency on ocaml uint library by using it. | |||
| 2017-04-21 | define some big_int literals in sail_values.ml to avoid lots of calls to ↵ | Robert Norton | |
| bit_int_of_int. Likely very little performance benefit but slightly more readable. | |||
| 2017-04-21 | remove unnecessary cast in incrementCP0Count (run every instruction) for ↵ | Robert Norton | |
| potential speedup. | |||
| 2017-04-20 | add support for cheri128 ocaml shallow embedding | Robert Norton | |
| 2017-04-20 | build a single run_embed.native with mips and cheri models linked and choose ↵ | Robert Norton | |
| between them using a command line switch. | |||
| 2017-04-20 | remove unsed code for elf file loading in run_embed. | Robert Norton | |
| 2017-04-20 | return zero for uninitialised memory in ocaml shallow embedding model. ↵ | Robert Norton | |
| Necessary to pass test_cp2_tagmem test. TODO make this configurable. | |||
| 2017-04-20 | add support for tagged memory functions in mips_extras_ml | Robert Norton | |
| 2017-04-18 | add workaround for sail shallow embedding problem concerning semantisc of ↵ | Robert Norton | |
| register reads. | |||
| 2017-04-18 | remove debug print. | Robert Norton | |
| 2017-04-07 | read from uninitialsed memory returns undef (required to pass ↵ | Robert Norton | |
| test_raw_cache_write_to_use test | |||
| 2017-04-06 | add support for address translation and exit handling in mips ocaml shallow ↵ | Robert Norton | |
| embedding test setup. | |||
| 2017-04-06 | Model now assumes memory is little endian so adjust extras file accordingly. | Robert Norton | |
| 2017-04-06 | Print registers in test suite compatible way. | Robert Norton | |
| 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-29 | change reqiured to work with little endian interpreter. | Robert Norton | |
| 2017-03-24 | Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵ | Robert Norton | |
| embedding. | |||
| 2017-03-24 | changes to allow generating ocaml that compiles. | Robert Norton | |
| 2017-03-23 | the interpreter/shallow expects little-endian memory-values | Shaked Flur | |
| 2017-02-03 | Now that 128-bit capabilities are supported we must be stricter about MIPS ↵ | Robert Norton | |
| alignment | |||
| 2017-02-03 | fix headers | Peter Sewell | |
| 2017-01-24 | first pass at cheri128 sail. | Robert Norton | |
| 2016-12-09 | sail changes for making lem embedding Isabelle-friendlier | Christopher Pulte | |
| 2016-12-08 | add target for building cheri_notlb.lem | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |