| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-11 | Update CHERI code extraction from Isabelle | Thomas Bauereiss | |
| Also use zero-initialised memory. Apparently some tests access unitialised memory, and the default behaviour of the Lem shallow embedding is to fail in this case. | |||
| 2018-07-09 | Simplify treating of undefined_bool in Lem library | Thomas Bauereiss | |
| Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list. | |||
| 2018-06-25 | Support bitlist representation in Sail2_string | Thomas Bauereiss | |
| 2018-06-22 | Fix Lem build of MIPS/CHERI | Thomas Bauereiss | |
| 2018-05-09 | Add tests for Isabelle->OCaml generation for CHERI and AArch64 | Thomas Bauereiss | |
| 2018-04-18 | Move a few printing functions to sail_values.lem | Thomas Bauereiss | |
| They are used in various specs and test cases. | |||
| 2018-03-21 | Fix Lem generation for MIPS | Thomas Bauereiss | |
| 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 | Add address to Write_tag outcome | Thomas Bauereiss | |
| The state monad currently assumes that tags are written to and read from properly aligned addresses (since it does not know the capability size used in the Sail model). This change allows the Sail model to pass in the aligned address(es) even if data is written to an unaligned address. There might be better ways to model tag writing, but this approach seems rather general. | |||
| 2018-03-08 | rename mips_new_tc to mips | Robert Norton | |
| 2018-03-08 | Remove files in mips directory prior to copying in files from mips_new_tc. ↵ | Robert Norton | |
| Hopefully thiis will help git to spot the rename and hence preserve history. | |||
| 2017-11-30 | match what rmem (ppcmem2) expects from ISA Makefiles | Shaked Flur | |
| 2017-07-26 | mips_extras.lem: fix references to Interp.V_foo | Jon French | |
| 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-03-23 | the interpreter/shallow expects little-endian memory-values | Shaked Flur | |
| 2016-11-30 | add new barrier kind for MIPS (only one for now). | Robert Norton | |
| 2016-10-22 | fixes following interface changes (type of instruction, name of barrier) | Robert Norton | |
| 2016-10-06 | move type definitions that both interpreter and shallow embedding use to ↵ | Christopher Pulte | |
| sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome | |||
| 2016-09-14 | Switch mips/cheri over to using memory ea/val for writes. Tag is now first ↵ | Robert Norton | |
| byte of value for capability writes. Still need TAGw for now but should kill eventually. | |||
| 2016-04-13 | add tagr and tagw in mips_extras (will need to change these to make tag ↵ | Robert Norton | |
| writes atomic) | |||
| 2016-02-03 | mips_extras.lem: fix typo in spelling of MEM_sync. | Robert Norton | |
| 2015-12-17 | First bit of gluing mips onto interpreter and eventually ppcmem infrastructure | Kathy Gray | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |