| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-28 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-09-28 | Refine constructors during monomorphisation | Brian Campbell | |
| 2017-09-27 | Add while-loops to Lem backend | Thomas Bauereiss | |
| 2017-09-19 | Added additional case for tuple l-expressions to increase compatability for ASL. | Alasdair Armstrong | |
| 2017-09-18 | Added additional utility functions in ast_util | Alasdair Armstrong | |
| Also fixed basic ocaml test suite | |||
| 2017-09-18 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-09-14 | Better failure reporting on mono tests | Brian Campbell | |
| 2017-09-14 | Fix some more test cases | Thomas Bauereiss | |
| 2017-09-13 | Work on improving Sail error messages | Alasdair Armstrong | |
| - Modified how sail type error messages are displayed. The typechecker, rather than immediately outputing a string has a datatype for error types, which are the pretty-printed using a PPrint pretty-printer. Needs more work for all the error messages. - Error messages now attempt to highlight the part of the file where the error occurred, by printing the line the error is on and highlighting where the error message is in red. Again, this needs to be made more robust, especially when the error messages span multiple lines. Other things - Improved new parser and lexer. Made the lexer & parser handling of colons simpler and more intuitive. - Added some more typechecking test cases | |||
| 2017-09-07 | Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| experiments | |||
| 2017-09-07 | Add ocaml run-time and updates to sail for ocaml backend | Alasdair Armstrong | |
| 2017-09-04 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵ | Brian Campbell | |
| mono-experiments | |||
| 2017-09-02 | Add command line flags to toggle sequential monad and native machine words | Thomas Bauereiss | |
| 2017-09-01 | Testing typedef generation for ocaml | Alasdair Armstrong | |
| 2017-09-01 | More test cases for ocaml backend | Alasdair Armstrong | |
| 2017-09-01 | Started work on test suite for ocaml backend | Alasdair Armstrong | |
| 2017-08-29 | Make Lem export of CHERI(-256) typecheck | Thomas Bauereiss | |
| Note: The effect annotations of the execute function differ between CHERI and MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the initial declarations of ast, decode, and execute (with the right effects for MIPS). | |||
| 2017-08-28 | Improve test output for monomorphisation | Brian Campbell | |
| 2017-08-28 | Update test script for gen_lib changes | Brian Campbell | |
| 2017-08-28 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵ | Brian Campbell | |
| mono-experiments # Conflicts: # src/gen_lib/sail_values.lem | |||
| 2017-08-24 | Begin refactoring Sail library | Thomas Bauereiss | |
| - Add back support for bit list representation of bit vectors, for backwards compatibility in order to ease integration with the interpreter. For this purpose, split out a file sail_operators.lem from sail_values.lem, and add a variant sail_operators_mwords.lem for the machine word representation of bitvectors. Currently, Sail is hardcoded to use machine words for the sequential state monad, and bit lists for the free monad, but this could be turned into a command line flag. - Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem library. The wrappers make use of sizeof expressions to extract type information from bitvectors (length, start index) in order to pass it to the Lem functions. - Add early return support to the free monad, using a new constructor "Return of 'r". As with the sequential monad, functions with early return are wrapped into "catch_early_return", which extracts the return value at the end of the function execution. | |||
| 2017-08-23 | Update monomorphisation test script | Brian Campbell | |
| 2017-08-23 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-08-22 | Adapt first part of union monomorphisation to existential types | Brian Campbell | |
| 2017-08-22 | Added basic support for pure record definitions and functional record | Alasdair Armstrong | |
| updates to the new typechecker | |||
| 2017-08-21 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-08-18 | Bit more monomorphisation testing | Brian Campbell | |
| 2017-08-18 | Fixed a bug where sizeof re-writing fail for aliased type arguments | Alasdair Armstrong | |
| Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments | |||
| 2017-08-17 | Fix two more test cases | Thomas Bauereiss | |
| 2017-08-17 | Add support for register types other than bitvector to state monad | Thomas Bauereiss | |
| Make state monad parametric in register state, and generate a record with registers from the Sail spec | |||
| 2017-08-17 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵ | Brian Campbell | |
| mono-experiments | |||
| 2017-08-16 | Very basic start to monomorphisation testing | Brian Campbell | |
| 2017-08-15 | Added exceptions and try/catch blocks to AST and typechecker in order | Alasdair Armstrong | |
| to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail. | |||
| 2017-08-10 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| Conflicts: src/pretty_print_common.ml | |||
| 2017-08-10 | Fix bug with subtyping in let bindings | Alasdair Armstrong | |
| 2017-08-10 | Improved existentials and type synonyms | Alasdair Armstrong | |
| 2017-08-08 | Fix Lem bindings in test cases | Thomas Bauereiss | |
| Add a test case with the MIPS spec using the TLB stub. Use the sequential monad for Lem testing for now; the free monad (in "prompt.lem") has not been updated for machine words yet. | |||
| 2017-08-07 | Fixed various issues regarding typechecking lists. | Alasdair Armstrong | |
| 2017-08-02 | Test for overloaded function with varying arities | Alasdair Armstrong | |
| 2017-08-02 | Fix run_tests.sh so it cleans up generated ml files when testing ocaml backend | Alasdair Armstrong | |
| 2017-08-02 | Tune vector_subrange | Thomas Bauereiss | |
| 2017-08-02 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| 2017-08-01 | Added ocaml generation to run_tests.sh | Alasdair Armstrong | |
| 2017-08-01 | Fixed a bug where type_synonyms were not being expanded properly when ↵ | Alasdair Armstrong | |
| considering possible casts | |||
| 2017-08-01 | Fixed a bug where as patterns weren't binding their variable correctly | Alasdair Armstrong | |
| 2017-08-01 | Added additional test for existentials | Alasdair Armstrong | |
| 2017-07-31 | Changed behavior of return to better match ASL | Alasdair Armstrong | |
| 2017-07-28 | Mips TLB existential example | Alasdair Armstrong | |
| 2017-07-28 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| 2017-07-27 | Some more test cases | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |