| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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 | |||
| 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-10-02 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-10-02 | Make undefined constant propagation stop at ex_int | Brian Campbell | |
| 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-28 | Use (K)Bindings from ast_util rather than making new ones | Brian Campbell | |
| 2017-09-28 | Add loops to monomorphisation | Brian Campbell | |
| 2017-09-28 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |