| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-02 | Use sail_lib.lem values in C backend | Alasdair Armstrong | |
| Rather than just using strings to represent literals, now use value types from sail_lib.lem to represent them. This allows for expressions to be evaluated at compile time, which will be useful for future optimisations involving constant folding and propagation, and allows the intermediate bytecode to be interpreted using the same lem builtins that the shallow embedding uses. To get this to work I had to tweak the build process slightly to allow ml files to import lem files from gen_lib/. Hopefully this doesn't break anything! | |||
| 2018-03-02 | Fix a bug in rewriting of loops for Lem backend | Thomas Bauereiss | |
| The rewriter ignored loops that were not contained within some let-binding, which later caused the Lem pretty-printer to fail (see #8). | |||
| 2018-03-02 | Add full aarch64_no_vector monomorphisation demo | Brian Campbell | |
| 2018-03-02 | remove workaround for #8 now that it is fixed. | Robert Norton | |
| 2018-03-02 | Fix off-by-one error in OCaml for loop compilation | Alasdair Armstrong | |
| Fix for loop in interactive interpreter Fixes #8 | |||
| 2018-03-02 | work around bug in ocaml foreach generation -- end point not included in ↵ | Robert Norton | |
| loop (see #8). | |||
| 2018-03-02 | add a cp2_next_pc function to update cheri state in fde loop and a stub ↵ | Robert Norton | |
| version for mips. | |||
| 2018-03-02 | add space in cap dump format to match that expected by test framework. | Robert Norton | |
| 2018-03-02 | cheri tests expect reserved permission bits to be initialised to one. | Robert Norton | |
| 2018-03-01 | Cleanup intermediate bytecode representation in C backend | Alasdair Armstrong | |
| 2018-03-01 | Add support for read_tag and write_tag in sail_lib.ml. and support for ↵ | Robert Norton | |
| intialising and dumping CHERI state. Somewhat working cheri sail2 model. | |||
| 2018-03-01 | fix typo in flow.sail | Robert Norton | |
| 2018-03-01 | cheri wip. | Robert Norton | |
| 2018-03-01 | Fix polymorphic functions annotations in OCaml compilation | Alasdair Armstrong | |
| One caveat still: Won't work if the polymorphic definition consists of multiple function clauses, but this seems unlikely - and I added an error message if this is the case. Also fix a small flow typing bug Fixes #7 | |||
| 2018-02-28 | Add check for if a function is redefining a val-spec | Alasdair Armstrong | |
| Previously this did not result in an error, but would cause issues with generated code. Fixes #5 | |||
| 2018-02-28 | Use topological sorting for OCaml backend | Thomas Bauereiss | |
| Fixes #6 | |||
| 2018-02-27 | Fix some bugs in C compilation, and optimise struct updates | Alasdair Armstrong | |
| Fix some issues where some early returns in functions would cause memory leaks, and optimize struct updates so the struct is not copied uneccesarily. Also make C print_bits match ocaml version output, and update tests. | |||
| 2018-02-27 | Get MIPS translated to Lem | Thomas Bauereiss | |
| 2018-02-27 | Make constant propagation of slicing more general | Brian Campbell | |
| 2018-02-27 | Lem/OCaml compatibility fixes | Brian Campbell | |
| 2018-02-26 | Add some obvious optimisations to C backend. | Alasdair Armstrong | |
| With these optimisations on, now get about 10x performance over OCaml. | |||
| 2018-02-26 | Last of the aarch64_no_vector monomorphisation replacements | Brian Campbell | |
| 2018-02-26 | work around linksem crashing when trying to print an elf file where ↵ | Robert Norton | |
| entry_point overflows an ocaml int. | |||
| 2018-02-26 | working sail2 mips spec (passes BERI tests). | Robert Norton | |
| 2018-02-26 | ADDU should sign extend 32-bit result. | Robert Norton | |
| 2018-02-26 | workaround sail2 not liking type synonyms as arguments to constructors (see #2). | Robert Norton | |
| 2018-02-26 | Fix SLTIU: note that immediate must be sign extended before unsigned comparison! | Robert Norton | |
| 2018-02-26 | Fix missing case in pattern completeness check | Alasdair Armstrong | |
| Fixes #4 | |||
| 2018-02-26 | Rename some Isabelle theories | Thomas Bauereiss | |
| The suffix _lemmas is more descriptive than _extras. | |||
| 2018-02-26 | Add/generate Isabelle lemmas about the monad lifting | Thomas Bauereiss | |
| Architecture-specific lemmas about concrete registers and types are generated and written to a file <prefix>_lemmas.thy, generic lemmas are in the theories *_extras.thy in lib/isabelle. In particular, State_extras contains simplification lemmas about the lifting from prompt to state monad. | |||
| 2018-02-24 | Fix C builtins | Alasdair Armstrong | |
| 2018-02-23 | Change links in README to point to github | Alasdair Armstrong | |
| Closes #3 | |||
| 2018-02-23 | Fix some bugs in C compilation | Alasdair Armstrong | |
| Fixed an issue with pattern matching on enums Fixed an issue whereby fix_early_returns would cause memory leaks Added optimizations for some of the builtins used in the decode function. Optimizations are turned on with the -O flag. | |||
| 2018-02-23 | Make mono test harness nicer | Brian Campbell | |
| 2018-02-23 | Allow guarded patterns rewrite to merge P_var patterns | Brian Campbell | |
| 2018-02-23 | Merge branch 'sail2' of github.com:rems-project/sail into sail2 | Robert Norton | |
| 2018-02-23 | Some tidy up of sail library - use extract_num from Big_int to implement ↵ | Robert Norton | |
| to_get_slice_int in less confusing way. Add arithmetic shift right. | |||
| 2018-02-23 | Change monomorphisation tests to proper output | Brian Campbell | |
| 2018-02-23 | test commit | Peter Sewell | |
| 2018-02-23 | Update more monomorphisation tests | Brian Campbell | |
| 2018-02-22 | More updates to C backend | Alasdair Armstrong | |
| Add support for short-ciruiting and/or. I forgot about this in the original ANF specification and not having it causes problems for the ARM spec. | |||
| 2018-02-22 | Curtail at more false assertions | Brian Campbell | |
| (plus some adjustments for the test case) | |||
| 2018-02-22 | Merge branch 'sail2' of github.com:rems-project/sail into sail2 | Robert Norton | |
| 2018-02-22 | wip | Robert Norton | |
| 2018-02-22 | Start resurrecting monomorphisation tests | Brian Campbell | |
| 2018-02-22 | Some Lem/OCaml compatibility fixes | Brian Campbell | |
| 2018-02-22 | Point merlin at pprint build | Brian Campbell | |
| 2018-02-21 | Can now compile aarch64/no_vector into C | Alasdair Armstrong | |
| Now compiles to C and builds a working executable. Just need to correctly implement all the library builtins (some are still stubs), and it should work. | |||
| 2018-02-21 | More aarch64 changes used in monomorphisation | Brian Campbell | |
| 2018-02-21 | Add more bitvector sizes for aarch64 | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |