| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-08 | Add (most of) the bitvector cast insertion transformation | Brian Campbell | |
| to help Lem go from a general type `bits('n)` to a specific type `bits(16)` at a case split, and the other way around for a returned value. Doesn't handle function clause patterns yet | |||
| 2018-02-06 | Compile union types in C backend | Alasdair Armstrong | |
| 2018-02-02 | Add arithmetic shift right for aarch64 mono | Brian Campbell | |
| 2018-02-01 | More work on C compilation | Alasdair Armstrong | |
| Can now compile things like early returns. The same approach should work for exception handling as well. Once that's in place, just need to work a bit more on getting union types to work + the library of builtins, then we should be able to compile and run some of our specs via C. Also added some documentation in comments for the general approach taken when compiling (need many more though). | |||
| 2018-01-31 | More updates to C backend - matching and tuples | Alasdair Armstrong | |
| 2018-01-31 | Add wrappers around Lem operators using bitvector type class | Thomas Bauereiss | |
| Makes bitvector typeclass instance dictionaries disappear from generated Isabelle output. | |||
| 2018-01-31 | Split base definitions of Lem monads and further built-ins (e.g. loop ↵ | Thomas Bauereiss | |
| combinators) Add Isabelle-specific theories imported directly after monad definitions, but before other combinators. These theories contain lemmas that tell the function package how to deal with monadic binds in function definitions. | |||
| 2018-01-30 | Fix failing Lem tests | Alasdair Armstrong | |
| 2018-01-29 | Sync mono rewrites definitions with library | Brian Campbell | |
| 2018-01-29 | Shaked removing generation of now-uncessary uint dependency | Peter Sewell | |
| 2018-01-26 | Fixed loading ARM elf files | Alasdair Armstrong | |
| Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib | |||
| 2018-01-26 | One more mono rewrite | Brian Campbell | |
| 2018-01-22 | Update Lem shallow embedding to Sail2 | Thomas Bauereiss | |
| - Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators. | |||
| 2018-01-22 | Update and fix test suite | Alasdair Armstrong | |
| 2018-01-19 | Update monomorphisation for sail2 | Brian Campbell | |
| (no vector type start position, comment syntax) | |||
| 2018-01-18 | Merge remote-tracking branch 'origin/experiments' into sail2 | Alasdair Armstrong | |
| 2018-01-18 | Modified ocaml backend to use ocamlfind for linksem and lem | Alasdair Armstrong | |
| Fixed test cases for ocaml backend and interpreter | |||
| 2018-01-16 | Another useful monomorphisation rewrite | Brian Campbell | |
| 2018-01-12 | Merge remote-tracking branch 'origin/experiments' into sail2 | Alasdair Armstrong | |
| 2018-01-09 | More monomorphisation rewrites for aarch64 | Brian Campbell | |
| 2018-01-09 | Add some optional experimental rewrites to help with monomorphisation | Brian Campbell | |
| 2017-12-14 | An experimental version of sail without bitvector start indexes. | Alasdair Armstrong | |
| Works with the vector branch of asl_parser | |||
| 2017-12-14 | Merge remote-tracking branch 'origin/experiments' into interactive | Alasdair Armstrong | |
| 2017-12-13 | Cleanup code by fixing compiler warnings, and fix ocaml compilation | Alasdair Armstrong | |
| Add the ast.sed script we need to build sail. Currently we just need this to fix up the locations in the AST but it will be removed once we can share locations between ocaml and lem. | |||
| 2017-12-12 | Add a few helper functions for bit lists | Thomas Bauereiss | |
| 2017-12-07 | Support monomorphisation with set constrained integers | Brian Campbell | |
| Also, to support this, constant propagation for integer multiply, fix substitution of concrete values for nvars, size parameters in single argument functions, fix kind for itself, add eq_atom to prelude | |||
| 2017-12-06 | Merge remote branch 'experiments' into experiments | Thomas Bauereiss | |
| 2017-12-06 | Make AST after rewriting for Lem backend type-checkable | Thomas Bauereiss | |
| - Add support for some internal nodes to type checker - Add more explicit type annotations during rewriting - Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer; these will be resolved by the type checker during rewriting now | |||
| 2017-11-28 | Small update to trivial sizeof rewrites so we can handle all cases in | Alasdair Armstrong | |
| aarch64 vector instructions. There's maybe a better more general way to do this but I'm not sure what that would be. | |||
| 2017-11-27 | Compile assertions into OCaml | Alasdair Armstrong | |
| and_bool and or_bool now are treated specially in the ocaml backend, so that they have the correct short-circuiting behaviour. This is required so that assertions don't fail for the ARM spec for predicates that shouldn't be tested in certain circumstances, for example things like: IsAArch32() && AArch32_specific_predicate Also fixed an issue in the sail library for ocaml where greater than or equal to was being mapped to greater than. | |||
| 2017-11-21 | Expose entry point in elf_loader for Sail model | Alasdair Armstrong | |
| 2017-11-15 | Additional test case for OCaml backend | Alasdair Armstrong | |
| 2017-11-15 | Simplify flow typing code in typechecker | Alasdair Armstrong | |
| 2017-11-10 | Fixed ocaml backend so it correctly compiles registers passed by name. | Alasdair Armstrong | |
| Added a test case for this behavior | |||
| 2017-11-08 | Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| experiments | |||
| 2017-11-07 | Add builtin for reversing endianness | Thomas Bauereiss | |
| 2017-11-07 | Declare prelude functions as extern | Thomas Bauereiss | |
| Also, rename a few functions for uniformity, e.g. bool_and -> and_bool | |||
| 2017-11-03 | Fix ocaml test suite | Alasdair Armstrong | |
| 2017-10-31 | Improvements to register read tracing in ocaml backend | Alasdair Armstrong | |
| 2017-10-27 | Fixed some ocaml backend related bugs | Alasdair Armstrong | |
| 2017-10-26 | Fix a bug in Sail OCaml library | Alasdair Armstrong | |
| 2017-10-26 | Updated ocaml backend so tracing instrumentation is optional. | Alasdair Armstrong | |
| Cleaned up the option list in sail.ml | |||
| 2017-10-25 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-10-25 | Avoid name clash in generated Lem | Brian Campbell | |
| (complains due to added val spec) | |||
| 2017-10-23 | Added support for better tracing in ocaml backend | Alasdair Armstrong | |
| Fixed an issue in ast.ml with uneccessary type variables | |||
| 2017-10-23 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-10-18 | Fixes and updates to ocaml backend to compile aarch64_no_vector | Alasdair Armstrong | |
| 2017-10-18 | Mark more prelude functions extern | Brian Campbell | |
| 2017-10-13 | Name (bit)vector operations more explicitly | Thomas Bauereiss | |
| Moreover, add support for pretty-printing (to Lem) vector access/update operations for vectors with non-constant, but normalized start index. | |||
| 2017-10-13 | Add support for real numbers to Lem backend | Thomas Bauereiss | |
| Requires version of Lem with real number support, currently at https://bitbucket.org/bauereiss/lem/branch/reals | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |