| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-25 | Generate ast.ml from ott file and update makefile. | Alasdair Armstrong | |
| Fix until loop not being counted as sugar | |||
| 2017-10-24 | More succinct syntax in new parser for externed valspecs which share | Alasdair Armstrong | |
| the same name between sail and the target | |||
| 2017-10-23 | Added effect set pretty printing for new parser | Alasdair Armstrong | |
| Also added some new utility functions in ast_util | |||
| 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-19 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments | Thomas Bauereiss | |
| 2017-10-19 | Fix pretty-printing of type abbreviation definitions with arguments | Thomas Bauereiss | |
| 2017-10-19 | Mangle names with '#' characters in Lem pretty-printing | Thomas Bauereiss | |
| 2017-10-19 | Rewrite undefined values, add type annotations to early returns | Thomas Bauereiss | |
| 2017-10-19 | Make some potentially non-terminating library functions terminate | Thomas Bauereiss | |
| 2017-10-19 | Preserve more type environment information during rewriting | Thomas Bauereiss | |
| Fixes a bug where resolving a type synonym failed in the Lem pretty-printer due to a missing type environment. | |||
| 2017-10-19 | Follow AST changes in (Lem) pretty-printers | Thomas Bauereiss | |
| 2017-10-18 | Fixes and updates to ocaml backend to compile aarch64_no_vector | Alasdair Armstrong | |
| 2017-10-13 | Fix some bugs that surfaced in the ASL export | Thomas Bauereiss | |
| - Bitvector pattern rewriting had stopped working due to a line of code being lost in some merge. - Fix a bug in early return rewriting that caused returns getting pulled out of if-statements to disappear. - There were some variable name clashes with keywords because doc_lem_id was not always called. - Ast_util.is_number failed to check for "int" and "nat" built-in types, causing pattern matching on natural number literals to fail. | |||
| 2017-10-13 | Add rewriting step for tuple-vector assignments | Thomas Bauereiss | |
| Assignments of the form "(v1, v2, v3) = vector" are common in ASL. They split the vector on the right-hand side into subvectors and assign those to the vectors in the tuple. The new rewriting step performs this splitting and replaces the right-hand side with the tuple of subvectors. The assignment is then handled by an existing rewriting step for tuple assignments. | |||
| 2017-10-13 | Add rewriting step for function effect propagation | Thomas Bauereiss | |
| Necessary for the Lem backend if effect checking is turned off in the type checker: the monad translation needs proper effect annotations. | |||
| 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 | |||
| 2017-10-13 | Improve debugging output | Thomas Bauereiss | |
| With -ddump_rewrite_ast, pretty-print Sail code after each rewriting step in addition to dumping the AST. | |||
| 2017-10-13 | Repeat and while loops in menhir parser and pretty printer | Alasdair Armstrong | |
| 2017-10-12 | Fixes pattern matching exact values ([:'n:]) on integer literals | Alasdair Armstrong | |
| Also improves flow typing in assert statements for ASL parser This patch does currently introduce a few test failures, probably due to the new way literals are handled in case statements, which needs to be investigated and fixed if possible. | |||
| 2017-10-10 | More improvements to menhir parser | Alasdair Armstrong | |
| 2017-10-10 | Fixes to menhir parser and pretty printer | Alasdair Armstrong | |
| 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-06 | Various improvements to menhir parser, and performance improvments for Z3 calls | Alasdair Armstrong | |
| New option -memo_z3 memoizes calls to the Z3 solver, and saves these results between calls to sail. This greatly increases the performance of sail when re-checking large specifications by about an order of magnitude. For example: time sail -no_effects prelude.sail aarch64_no_vector.sail real 0m4.391s user 0m0.856s sys 0m0.464s After running with -memo_z3 once, running again gives: time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail real 0m0.457s user 0m0.448s sys 0m0.008s Both the old and the new parser should now have better error messages where the location of the parse error is displayed visually in the error message and highlighted. | |||
| 2017-10-04 | Fixed a bug in vector concatenation l-expressions | Alasdair Armstrong | |
| The code for these is now rather ugly though... it needs to be cleaned up at some point Also various improvements to new menhir parser | |||
| 2017-10-04 | Add pretty printer for menhir parser | Alasdair Armstrong | |
| 2017-10-04 | Merge branch 'cleanup' into experiments | Alasdair Armstrong | |
| 2017-10-04 | Add pretty printing for while loops | Alasdair Armstrong | |
| 2017-10-04 | Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| experiments | |||
| 2017-10-03 | Fixes to new parser | Alasdair Armstrong | |
| 2017-10-03 | Fixed some loop bugs for ASL parser | Alasdair Armstrong | |
| 2017-09-29 | Support vector registers (other than bitvectors) | Thomas Bauereiss | |
| 2017-09-29 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments | Thomas Bauereiss | |
| 2017-09-29 | Some more refactoring of Sail library | Thomas Bauereiss | |
| - Remove start indices and indexing order from bitvector types. Instead add them as arguments to functions accessing/updating bitvectors. These arguments are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a "sizeof" rewriting pass. - Add a typeclass for bitvectors with a few basic functions (converting to/from bitlists, converting to an integer, getting and setting bits). Make both monads use this interface, so that they work with both the bitlist and the machine word representation of bitvectors. | |||
| 2017-09-29 | Add MIPS->Isabelle target to Makefile | Thomas Bauereiss | |
| 2017-09-27 | Add while-loops to Lem backend | Thomas Bauereiss | |
| 2017-09-27 | Fixed command line flag naming | Alasdair Armstrong | |
| 2017-09-26 | Added while-do and repeat-until loops to sail for translating ASL | Alasdair Armstrong | |
| 2017-09-21 | Refactored AST valspecs into single constructor | Alasdair Armstrong | |
| 2017-09-21 | Remove unused kind_def (KD_) nodes from AST | Alasdair Armstrong | |
| 2017-09-21 | Change NC_fixed to NC_equal to match NC_not_equal | Alasdair Armstrong | |
| also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway) | |||
| 2017-09-21 | Simplify AST by removing LB_val_explicit and replace LB_val_implicit with ↵ | Alasdair Armstrong | |
| just LB_val in AST also rename functions in rewriter.ml appropriately. | |||
| 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 | Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| experiments | |||
| 2017-09-14 | Fix bug in topological sorting | Thomas Bauereiss | |
| 2017-09-14 | Fix some more test cases | Thomas Bauereiss | |
| 2017-09-14 | Fix a regression when writing to a register via a reference in a vector such ↵ | Thomas Bauereiss | |
| as GPR This was wrongly translated as an update of the vector of references. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |