| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | added the exmem effect for AArch64 store-exclusive | Shaked Flur | |
| 2017-03-23 | the interpreter/shallow expects little-endian memory-values | Shaked Flur | |
| 2016-11-15 | wrap state monad into list monoad for non-deterministic write exclusive ↵ | Christopher Pulte | |
| operations | |||
| 2016-11-14 | add option -lem_sequential for producing shallow embedding that refers to ↵ | Christopher Pulte | |
| state monad, library fixes | |||
| 2016-11-10 | rewrite state.lem | Christopher Pulte | |
| 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-25 | nicer lem output: no more unecessary 'unit' returns if if-expressions, ↵ | Christopher Pulte | |
| for-loops or case-expressions also return updated variables | |||
| 2016-09-23 | sail-to-lem progress | Christopher Pulte | |
| 2016-09-19 | sail-to-lem progress | Christopher Pulte | |
| 2016-09-07 | push some lem pp changes | Christopher Pulte | |
| 2016-07-12 | sail-to-lem and lem library fixes | Christopher | |
| 2015-12-21 | fixes, pp progress | Christopher | |
| 2015-12-09 | adapted for Kathy's lexp effect typing changes: register writes should be ↵ | Christopher | |
| correct now, fixes, pp | |||
| 2015-12-07 | adapted pp for Kathy's effect type changes | Christopher | |
| 2015-12-03 | added prompt.lem for connecting to concurrency model and ↵ | Christopher Pulte | |
| {power,armv8}_extras.lem; fixes | |||
| 2015-11-19 | fixes for cumulative effect anotations | Christopher Pulte | |
| 2015-11-13 | fixes, more pp | Christopher Pulte | |
| 2015-11-10 | rewriting fixes, syntactically correct lem syntax, number type errors remaining | Christopher Pulte | |
| 2015-11-06 | progress on generating function for read/writing register fields | Christopher Pulte | |
| 2015-11-05 | some progress on lem backend: rewrite away mutable variable assignments, ↵ | Christopher Pulte | |
| rewrite for-loops, if/case-expressions to return updated variables | |||
| 2015-10-28 | progress on lem backend: auto-generate read_register and write_register ↵ | Christopher Pulte | |
| functions, and state definition | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |