| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-15 | Export utility functions from type_check.ml | Alasdair Armstrong | |
| 2017-08-15 | Menhir parser support for try/catch | Alasdair Armstrong | |
| 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-14 | Merge remote-tracking branch 'origin/master' into experiments | Alasdair Armstrong | |
| 2017-08-14 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| 2017-08-14 | Merge remote-tracking branch 'origin/mono-experiments' into experiments | Alasdair Armstrong | |
| 2017-08-14 | More constructs in menhir parser, plus support for both left and right infix ↵ | Alasdair Armstrong | |
| operators. | |||
| 2017-08-14 | add risc-v fence instruction as re-using MIPS sync for now. Also place ↵ | Robert Norton | |
| holders for FENCE.I and ECALL. | |||
| 2017-08-14 | Minor change to x86 specification. | Anthony Fox | |
| 2017-08-12 | Resolve ambiguity between negation of integers and bools | Thomas Bauereiss | |
| 2017-08-12 | Fix compilation issue for 32-bit systems | Thomas Bauereiss | |
| 2017-08-11 | further riscv rmem integration. | Robert Norton | |
| 2017-08-11 | Menhir for new parser, ocamlyacc for old | Brian Campbell | |
| 2017-08-11 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-08-11 | Make type checking just clever enough to solve 8*n = constant | Brian Campbell | |
| 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 operator support for test menhir parser | Alasdair Armstrong | |
| 2017-08-10 | Experimenting with alternate parser | Alasdair Armstrong | |
| 2017-08-10 | Add support for early return to Lem backend | Thomas Bauereiss | |
| Implemented using the exception monad, by throwing and catching the return value | |||
| 2017-08-10 | Disable menhir on this branch | Brian Campbell | |
| (until location information is updated) | |||
| 2017-08-10 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-08-10 | Existentials in Lem AST output | Brian Campbell | |
| 2017-08-10 | Experimental removal of existentials | Brian Campbell | |
| 2017-08-10 | Improved existentials and type synonyms | Alasdair Armstrong | |
| 2017-08-09 | Pretty-print some more type annotations | Thomas Bauereiss | |
| 2017-08-08 | Add infrastructure to play with new menhir parsers. | Alasdair Armstrong | |
| Added a copy of the current parser/lexer in parser2.mly and lexer2.mll. They can be used with the -new_parser flag. Currently they are just copies of the existing files. | |||
| 2017-08-08 | Switch to using menhir for sail parser in experiments branch | 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-08 | work on integrating risc-v model with rmem (incomplete). | Robert Norton | |
| 2017-08-08 | work around missing >=_u in sail. | Robert Norton | |
| 2017-08-08 | Glue together Sail prelude and Lem library | Thomas Bauereiss | |
| 2017-08-08 | Various fixes and improvements for the Lem pretty-printing | Thomas Bauereiss | |
| - Add some missing "wreg" effect annotations in the type checker - Improve pretty-printing of register type definitions: In addition to a "build" function, output an actual type definition, and some getter/setter functions for register fields - Fix a bug in sizeof rewriting that caused it to fail when rewriting nested calls of functions that contained sizeof expressions - Fix pretty-printing of user-defined union types with type variables (cf. test case option_either.sail) - Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to output more type annotations with bitvector lengths - Add (back) some support for specifying Lem bindings in val specs using "val extern ... foo = bar" - Misc bug fixes | |||
| 2017-08-08 | Add x86 decoder. | Anthony Fox | |
| 2017-08-08 | Add add_typ_var to mli file | Alastair Reid | |
| This function is used by asl_to_sail2.ml | |||
| 2017-08-07 | Improvements to existentials for ASL parser | Alasdair Armstrong | |
| 2017-08-07 | Fixed pretty printing of E_cons | Alasdair Armstrong | |
| 2017-08-07 | Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| sail_new_tc | |||
| 2017-08-07 | Fixed various issues regarding typechecking lists. | Alasdair Armstrong | |
| 2017-08-07 | Merged in acjf3/sail/sail_new_tc (pull request #2) | Anthony Fox | |
| Initial commit of x86 model (ported from L3). | |||
| 2017-08-07 | Initial commit of x86 model (ported from L3). | Anthony Fox | |
| 2017-08-04 | Various improvements for ASL generation | Alasdair Armstrong | |
| Fixed a bug where existential constraint's weren't used to solve function quantifiers correctly | |||
| 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 | Improve pretty-printing of register declaration and assignment | Thomas Bauereiss | |
| 2017-08-02 | Changed some aspects of the typechecker to better support ASL l-values | Alasdair Armstrong | |
| 2017-08-02 | Tune vector_subrange | Thomas Bauereiss | |
| 2017-08-02 | Add debugging option to dump AST after rewriting steps | Thomas Bauereiss | |
| 2017-08-02 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| 2017-08-02 | Modified loop typechecking code to generate a new type variable for the loop ↵ | Alasdair Armstrong | |
| index, seems to work better for complex cases in ASL | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |