| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-31 | Added trace viewer application for traces produced by sail -ocaml_trace | Alasdair Armstrong | |
| See README file for how to set up and use | |||
| 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 | Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| experiments | |||
| 2017-10-26 | Unfold nexp abbreviations for pretty-printing | Thomas Bauereiss | |
| 2017-10-26 | Update val specs after rewriting functions | Thomas Bauereiss | |
| 2017-10-26 | Experiment with pretty-printing non-atomic nexps in Lem | Thomas Bauereiss | |
| 2017-10-26 | Updated ocaml backend so tracing instrumentation is optional. | Alasdair Armstrong | |
| Cleaned up the option list in sail.ml | |||
| 2017-10-25 | Allow mutually recursive functions | Thomas Bauereiss | |
| 2017-10-25 | Point sail/src makefile at ott file in language/ | Alasdair Armstrong | |
| 2017-10-25 | List.cons is too new | Brian Campbell | |
| 2017-10-25 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-10-25 | Generate ast.ml from ott file and update makefile. | Alasdair Armstrong | |
| Fix until loop not being counted as sugar | |||
| 2017-10-25 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-10-25 | Alternative low-memory version of barrier_kindCompare | Brian Campbell | |
| 2017-10-25 | Avoid name clash in generated Lem | Brian Campbell | |
| (complains due to added val spec) | |||
| 2017-10-24 | Make nexp simplifier handle recursion properly | Brian Campbell | |
| 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-24 | Print type annotations in Lem with type variables | Brian Campbell | |
| (includes variables for bitvector sizes) | |||
| 2017-10-24 | Limit quantifiers printed in Lem to type variables that actually | Brian Campbell | |
| appear in the output | |||
| 2017-10-24 | Handle existential types in Lem backend by stripping them and | Brian Campbell | |
| checking that the type variables visible in the output aren't existential | |||
| 2017-10-24 | Generate undefined_bitvector function when targeting machine words | Brian Campbell | |
| 2017-10-24 | Produce debug message when an expression can't be converted to a constraint | Brian Campbell | |
| 2017-10-24 | Remove special case for boolean (as opposed to bool) | Brian Campbell | |
| 2017-10-23 | Type check external casts | Brian Campbell | |
| 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-23 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 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-18 | Merge branch 'experiments' of Peter_Sewell/sail into mono-experiments | Brian Campbell | |
| (and fix up monomorphisation) | |||
| 2017-10-13 | Handle bitvector_access in constant propagation | Brian Campbell | |
| 2017-10-13 | Make Sail_values.repeat total, and remove duplicate | Brian Campbell | |
| 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 | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |