| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-09 | Improvements to menhir pretty printer and ocaml backend | Alasdair Armstrong | |
| Menhir pretty printer can now print enough sail to be useful with ASL parser Fixity declarations are now preserved in the AST Menhir parser now runs without the Pre-lexer Ocaml backend now supports variant typedefs, as the machinery to generate arbitrary instances of variant types has been added to the -undefined_gen flag | |||
| 2017-10-06 | Remove BK_effect constructor | Alasdair Armstrong | |
| 2017-10-04 | Merge branch 'cleanup' into experiments | Alasdair Armstrong | |
| 2017-09-27 | Add while-loops to Lem backend | Thomas Bauereiss | |
| 2017-09-21 | Cleaning up the AST and removing redundant and/or unused nodes | Alasdair Armstrong | |
| 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-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-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-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-22 | Added basic support for pure record definitions and functional record | Alasdair Armstrong | |
| updates to the new typechecker | |||
| 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-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 | |
| 2017-07-27 | Add test cases for overlapping record field names | Alasdair Armstrong | |
| 2017-07-27 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| 2017-07-27 | Fixed bug with pattern synonyms in Cons and List patterns | Alasdair Armstrong | |
| 2017-07-27 | Fixed some bugs with existentials, and added test cases | Alasdair Armstrong | |
| 2017-07-26 | Improve rewriting of sizeof expressions | Thomas Bauereiss | |
| If some type-level variables in a sizeof expression in a function body cannot be directly extracted from the parameters of the function, add a new parameter for each unresolved parameter, and rewrite calls to the function accordingly | |||
| 2017-07-25 | Improved l-expressions | Alasdair Armstrong | |
| - Fixed a bug where some l-expressions which wrote registers wern't picking up register writes. - Can now write to registers with record types. e.g. ARM's ProcState record from ASL. | |||
| 2017-07-24 | Added cons patterns to sail | Alasdair Armstrong | |
| See test/typecheck/pass/cons_pattern.sail for an example. Also cleaned up the propagating effects code by making some of the variable names less verbose | |||
| 2017-07-18 | Added real number literals to sail, to better support full ASL translation | Alasdair Armstrong | |
| 2017-07-17 | Added pattern guards to sail | Alasdair Armstrong | |
| Introduces a when keyword for case statements, as the Pat_when constructor for pexp's in the AST. This allows us to write things like: typedef T = const union { int C1; int C2 } function int test ((int) x, (T) y) = switch y { case (C1(z)) when z == 0 -> 0 case (C1(z)) when z != 0 -> x quot z case (C2(z)) -> z } this should make translation from ASL's patterns much more straightforward | |||
| 2017-07-13 | Typechecker now inserts val specs into AST when it infers them | Alasdair Armstrong | |
| 2017-07-13 | Modified MIPS model so it typechecks with the new typechecker | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |