| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-24 | Print tracking information for V_track, hopefully fix extern_vector_value, ↵ | Christopher Pulte | |
| fix sail_values bug. | |||
| 2017-03-23 | the interpreter/shallow expects little-endian memory-values | Shaked Flur | |
| 2017-02-03 | fix headers | Peter Sewell | |
| 2017-01-26 | christopher, kathy, peter: hacky experiment on nias_of_instruction | Peter Sewell | |
| 2017-01-24 | functionality for comparing handwritten analysis function with exhaustive ↵ | Christopher Pulte | |
| interpreter | |||
| 2017-01-14 | changes to enable interpreter exhaustive analysis in ppcmem again | Christopher Pulte | |
| 2016-12-09 | sail changes for making lem embedding Isabelle-friendlier | Christopher Pulte | |
| 2016-12-01 | move interpreter-specific types from Sail_impl_base to Interp_interface | Christopher Pulte | |
| 2016-11-30 | add new barrier kind for MIPS (only one for now). | Robert Norton | |
| 2016-11-27 | make outcome_s contain the instruction state pretty print rather than the ↵ | Christopher Pulte | |
| instruction state, factor out interpreter/shallow embedding value conversion | |||
| 2016-11-09 | move decode_error type back to Sail_impl_base for now | Christopher Pulte | |
| 2016-11-08 | fixes | Christopher Pulte | |
| 2016-11-07 | factor out regfp analysis types into etc/regfp.sail | Christopher Pulte | |
| 2016-10-25 | fix my decode_to_istate bug | Christopher Pulte | |
| 2016-10-21 | shallow embedding progress | Christopher Pulte | |
| 2016-10-20 | factor out instr_external_to_interp_value | Christopher Pulte | |
| 2016-10-20 | fix previous FromToInterpValue typeclass issue, factor out intpreter's ↵ | Christopher Pulte | |
| interp_value_to_instr_external | |||
| 2016-10-19 | fix | Christopher Pulte | |
| 2016-10-19 | remove effect list from instruction type | 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-30 | fixes, update isntruction_analysis for NIAs and DIA | Christopher Pulte | |
| 2016-09-21 | fixes | Christopher Pulte | |
| 2016-09-13 | Add optional address to memv events | Kathy Gray | |
| 2016-09-13 | add show functions, fix | Christopher Pulte | |
| 2016-09-13 | extern slice for instruction analysis | Kathy Gray | |
| 2016-09-09 | update instruction_analysis to support nias and instruction kind | Christopher Pulte | |
| 2016-09-02 | Extend type checking so that patterns with vector concatenation don't permit ↵ | Kathy Gray | |
| under specified vector lengths (at least for function patterns) Extend interpreter interface to have a function for Christopher's instruction analysis | |||
| 2016-08-17 | Fix pattern match bug in interp where vector accesses were using the wrong ↵ | Kathy Gray | |
| start index | |||
| 2016-07-25 | win | Kathy Gray | |
| 2016-07-25 | one more go | Kathy Gray | |
| 2016-07-25 | Actually fix stack for return | Kathy Gray | |
| 2016-07-23 | Add a return exp form to Sail, supported in type checker and in interpreter. | Kathy Gray | |
| TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem | |||
| 2016-06-07 | Fix issue in accessing fields and slices of registers during translate address | Kathy Gray | |
| 2016-06-03 | Fix bug exposed/introduced by properly handling vector starts in the type ↵ | Kathy Gray | |
| checker | |||
| 2016-05-04 | Correct register field/slice reading for decreasing reads for ↵ | Kathy Gray | |
| decode/translate_address/exhaustive. (Was previously correct for full register reads) | |||
| 2016-05-03 | write all or part of fields out of translate_address (instead of just all) | Kathy Gray | |
| fix bug in interp_to_value_helper | |||
| 2016-05-03 | Change decode and translate_address to support writing register events ↵ | Kathy Gray | |
| (although decode isn't pushed through yet). Note: this will break all builds | |||
| 2016-04-26 | Add more cases for translate_address to support enums | Kathy Gray | |
| 2016-04-26 | print error case on translate address | Kathy Gray | |
| 2016-04-25 | Make interpreter able to read registers during translate address and decode. | Kathy Gray | |
| This is not yet connected to any model and not yet tested. Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ). | |||
| 2016-04-18 | More fixes to interp with regards to warnings and debugging info | Kathy Gray | |
| 2016-04-12 | Reduce warnings for interpreter. Removed all pattern match warnings for ↵ | Kathy Gray | |
| interp_lib, interp_inter_imp, and printing_functions. | |||
| 2016-03-08 | Start task of setting up tagged memory in sequential interpreter | Kathy Gray | |
| 2016-02-02 | Get mips stuff hooked up with translate address. | Kathy Gray | |
| Note: this support is rather mips centric at the moment | |||
| 2016-02-02 | add translate_address functionality | Kathy Gray | |
| 2016-01-28 | Support exit and assert better in sequential interpreter and general ↵ | Kathy Gray | |
| interpreter interface | |||
| 2016-01-27 | Make mips build again | Kathy Gray | |
| Make quiet mode for sequential interpreter not print | |||
| 2016-01-26 | Fix some bugs in writing registers with slices in the sequential interpreter | Kathy Gray | |
| 2016-01-20 | Decoding a mips instruction :) | Kathy Gray | |
| Not executing yet as some previous commit has broken the interpreter's local assignment | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |