| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-28 | Adapt theory imports for Isabelle 2018 | Thomas Bauereiss | |
| Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860 | |||
| 2018-06-11 | More efficient bitfield implementation | Alasdair Armstrong | |
| 2018-06-07 | Add a constant folding optimization pass | Alasdair | |
| 2018-06-06 | Factor utility functions for IR into separate file and struct update ↵ | Alasdair Armstrong | |
| optimizations. Move the utility functions for graph generation and pretty printing of intermediate representation instructions into a separate file, bytecode_util.ml, by analogy with ast_util.ml. Add an optimization pass that searches for specific patterns of struct updates and removes uncessary copying of the structs involved. With this optimisation pass the time taken for u-boot to run approx 57,000,000 instructions goes down from about 11-12 minutes to 8 minutes (about 120,000 IPS). | |||
| 2018-06-06 | Some additional fixes to C backend. Re-enable primitive optimizations. | Alasdair Armstrong | |
| Also add an additional -Oz3 flag that uses z3 to optimize some additional types. This is currently very experimental and doesn't fully work yet. | |||
| 2018-06-04 | Fix bug with function return types in C backend | Alasdair Armstrong | |
| 2018-05-09 | add loc for arm full. | Robert Norton | |
| 2018-05-09 | Add tests for Isabelle->OCaml generation for CHERI and AArch64 | Thomas Bauereiss | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |