| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-11 | Interpreter that understands assert | Kathy Gray | |
| 2016-01-07 | Add E_assert to basic rewriters | Kathy Gray | |
| 2016-01-06 | Add new assert expression to Sail | Kathy Gray | |
| This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified. | |||
| 2015-12-22 | More make file goo, and fixing a typo in run_with_elf | Kathy Gray | |
| 2015-12-22 | More gluing mips to interpreter | Kathy Gray | |
| 2015-12-22 | Add mips64 to get_elf in Makefile | Robert Norton | |
| 2015-12-21 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher | |
| 2015-12-21 | fixes, pp progress | Christopher | |
| 2015-12-17 | Remove external functions that the library provides, having added them to ↵ | Kathy Gray | |
| the type environment finally. (Also small cleaning of the new makefile) | |||
| 2015-12-16 | Fix a bug in checking vector accesses and ranges that was hiding some bugs, ↵ | Kathy Gray | |
| and causing some incorrect lem_ast generation in mips code | |||
| 2015-12-16 | rewriter and pp changes for generating ARM output | Christopher | |
| 2015-12-15 | better location information | Christopher | |
| 2015-12-14 | Adding new location constructor for location of generated terms | Kathy Gray | |
| 2015-12-10 | fix | Christopher | |
| 2015-12-09 | adapted for Kathy's lexp effect typing changes: register writes should be ↵ | Christopher | |
| correct now, fixes, pp | |||
| 2015-12-09 | Fix overlooked case of effect tagging for sub register writes. Close issue ↵ | Kathy Gray | |
| #23 again | |||
| 2015-12-08 | wreg effects and tags now proper for LEXP_field, LEXP_vector ↵ | Kathy Gray | |
| LEXP_vector_range for sub register writes. Closes issue #23 | |||
| 2015-12-08 | Some easy fixes to vector and list type inference. Closes issue #25 and ↵ | Kathy Gray | |
| issue #26 | |||
| 2015-12-07 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher | |
| 2015-12-07 | adapted pp for Kathy's effect type changes | Christopher | |
| 2015-12-07 | Interpreter working again with updated tag, effects, and types behaviour | Kathy Gray | |
| 2015-12-07 | Reading of register slices and bits should now be tagged and effect ↵ | Kathy Gray | |
| annotated properly, as well as field accesses. Writing of register slices and bits still look like writes of full registers from tags and effects (probably, if it works, it's an accident) WARNING: interpreter still not up to date with this change | |||
| 2015-12-04 | First bit of making tags and effects on sub vector accesses work for static ↵ | Kathy Gray | |
| compilation. So, it should be right for E_field, but isn't right for E_vector_access, and hasn't begun for E_vector_subrange Isn't right for any writes **WARNING** lem ast files generated from this may not have the proper behaviour on field accesses. | |||
| 2015-12-03 | added prompt.lem for connecting to concurrency model and ↵ | Christopher Pulte | |
| {power,armv8}_extras.lem; fixes | |||
| 2015-11-25 | non-working sail/mips interpreter integration for kathy to look at and ↵ | Robert Norton | |
| example mips elf file. | |||
| 2015-11-25 | fixes, pp | Christopher Pulte | |
| 2015-11-24 | Fixup effect equality bug introduced by adding e_escape | Kathy Gray | |
| 2015-11-24 | Add BE_escape effect when an E_exit is seen | Kathy Gray | |
| Close #20 | |||
| 2015-11-22 | do effect annotation updates more systematically, fix dedup | Christopher Pulte | |
| 2015-11-20 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-11-20 | no more unecessary variables from removing vector-concatenation pattern ↵ | Christopher Pulte | |
| matches, reset variable name counter for each function clause, fixes | |||
| 2015-11-20 | make the abis directory as well | Kathy Gray | |
| 2015-11-20 | fixes to get-elf to work on linux. Hope it works on Mac too. | Robert Norton | |
| 2015-11-19 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-11-19 | fixes for cumulative effect anotations | Christopher Pulte | |
| 2015-11-19 | Keep up with linksem | Kathy Gray | |
| 2015-11-19 | More makefile type | Kathy Gray | |
| 2015-11-19 | typo in make file | Kathy Gray | |
| 2015-11-18 | Update makefile for elf | Kathy Gray | |
| 2015-11-17 | Very nearly there sequential interpreter, just need to hook in the spec ↵ | Kathy Gray | |
| files for the different isas to support | |||
| 2015-11-13 | fixes, more pp | Christopher Pulte | |
| 2015-11-12 | Incorporating elf into sequential interpreter | Kathy Gray | |
| Fix an effect bug on aliased id | |||
| 2015-11-10 | fix case-expressions' newreturn | Christopher Pulte | |
| 2015-11-10 | rewriting fixes, syntactically correct lem syntax, number type errors remaining | Christopher Pulte | |
| 2015-11-10 | More tag refinement for lexp | Kathy Gray | |
| 2015-11-10 | Update tag for register write in nested lexp | Kathy Gray | |
| Also starting to try to get elf compiling for sequential interpreter | |||
| 2015-11-10 | Make first half of sequential interpreter driver compile again | Kathy Gray | |
| 2015-11-07 | fixes, no more uncessary variables, pp progress | Christopher Pulte | |
| 2015-11-06 | progress on generating function for read/writing register fields | Christopher Pulte | |
| 2015-11-06 | fixes | Christopher Pulte | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |