| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-02 | Fix translation of repeat-until loops to Lem | Thomas Bauereiss | |
| 2017-10-31 | Pretty-print Sail assertions in Lem | Thomas Bauereiss | |
| Map to calls to monadic function assert_exp that throws an exception if the assertion is false | |||
| 2017-10-23 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-10-19 | Make some potentially non-terminating library functions terminate | Thomas Bauereiss | |
| 2017-10-02 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-09-29 | Support vector registers (other than bitvectors) | Thomas Bauereiss | |
| 2017-09-29 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments | Thomas Bauereiss | |
| 2017-09-29 | Some more refactoring of Sail library | Thomas Bauereiss | |
| - Remove start indices and indexing order from bitvector types. Instead add them as arguments to functions accessing/updating bitvectors. These arguments are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a "sizeof" rewriting pass. - Add a typeclass for bitvectors with a few basic functions (converting to/from bitlists, converting to an integer, getting and setting bits). Make both monads use this interface, so that they work with both the bitlist and the machine word representation of bitvectors. | |||
| 2017-09-28 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-09-27 | Add while-loops to Lem backend | Thomas Bauereiss | |
| 2017-09-04 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵ | Brian Campbell | |
| mono-experiments | |||
| 2017-09-02 | Remove dependency of state.lem on bitvector operations | Thomas Bauereiss | |
| 2017-08-28 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵ | Brian Campbell | |
| mono-experiments # Conflicts: # src/gen_lib/sail_values.lem | |||
| 2017-08-24 | Improve and simplify handling of mutable local variables | Thomas Bauereiss | |
| 2017-08-24 | Begin refactoring Sail library | Thomas Bauereiss | |
| - Add back support for bit list representation of bit vectors, for backwards compatibility in order to ease integration with the interpreter. For this purpose, split out a file sail_operators.lem from sail_values.lem, and add a variant sail_operators_mwords.lem for the machine word representation of bitvectors. Currently, Sail is hardcoded to use machine words for the sequential state monad, and bit lists for the free monad, but this could be turned into a command line flag. - Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem library. The wrappers make use of sizeof expressions to extract type information from bitvectors (length, start index) in order to pass it to the Lem functions. - Add early return support to the free monad, using a new constructor "Return of 'r". As with the sequential monad, functions with early return are wrapped into "catch_early_return", which extracts the return value at the end of the function execution. | |||
| 2017-08-23 | Update monomorphisation test script | Brian Campbell | |
| 2017-08-17 | Add support for register types other than bitvector to state monad | Thomas Bauereiss | |
| Make state monad parametric in register state, and generate a record with registers from the Sail spec | |||
| 2017-08-15 | Improve and simplify handling of mutable local variables | Thomas Bauereiss | |
| 2017-08-10 | Add support for early return to Lem backend | Thomas Bauereiss | |
| Implemented using the exception monad, by throwing and catching the return value | |||
| 2017-08-08 | Glue together Sail prelude and Lem library | Thomas Bauereiss | |
| 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 |