| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | |||
| 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-06 | Produce type signatures in Lem output | Brian Campbell | |
| Necessary for machine words due to the type variables Also add Size type classes for machine word bitvectors | |||
| 2017-10-06 | Implement replicate_bits for mwords | Brian Campbell | |
| 2017-10-06 | Fix constant propagation on multi-argument functions | Brian Campbell | |
| 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 | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |