| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-07 | More OCaml test cases | Alasdair Armstrong | |
| Improved handling of try/catch Better handling of unprovable constraints when the environment contains false | |||
| 2017-12-06 | Add top-level pattern match guards internally | Brian Campbell | |
| Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next. | |||
| 2017-12-05 | Better support for exceptions in sail for ASL specs that need them. | Alasdair Armstrong | |
| 2017-12-05 | Update license headers for Sail source | Alasdair Armstrong | |
| 2017-11-27 | Split rewriter into separate rewriting library and rewrite passes | Alasdair Armstrong | |
| As discussed previously, we wanted to start refactoring the re-writer to make it a bit less monolithic, and in the future potentially break it into separate files for backend-specific rewrites and stuff. - rewriter.ml now contains the generic re-writing code - rewrites.ml contains the rewriting passes themselves It would be nice if the generic rewriting code didn't depend on the typechecker, because then it could be used in ASL parser on untyped code. | |||
| 2017-11-24 | Use unbound precision big_ints throughout sail. | Alasdair Armstrong | |
| Alastair's test cases revealed that using regular ints causes issues throughout sail, where all kinds of things can internally overflow in edge cases. This either causes crashes (e.g. int_of_string fails for big ints) or bizarre inexplicable behaviour. This patch switches the sail AST to use big_int rather than int, and updates everything accordingly. This touches everything and there may be bugs where I mistranslated things, and also n = m will still typecheck with big_ints but fail at runtime (ocaml seems to have decided that static typing is unnecessary for equality...), as it needs to be changed to eq_big_int. I also got rid of the old unused ocaml backend while I was updating things, so as to not have to fix it. | |||
| 2017-11-10 | Fixed some tricky typechecking bugs | Alasdair Armstrong | |
| 2017-11-01 | Support bitvector-size-parametric functions in Lem output | Brian Campbell | |
| Translates atom('n) types into itself('n) types that won't be erased Also exports more rewriting functions | |||
| 2017-10-24 | Generate undefined_bitvector function when targeting machine words | Brian Campbell | |
| 2017-10-19 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments | Thomas Bauereiss | |
| 2017-10-19 | Rewrite undefined values, add type annotations to early returns | Thomas Bauereiss | |
| 2017-10-18 | Fixes and updates to ocaml backend to compile aarch64_no_vector | Alasdair Armstrong | |
| 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-04 | Merge branch 'cleanup' into experiments | Alasdair Armstrong | |
| 2017-10-03 | Fixes to new parser | Alasdair Armstrong | |
| 2017-09-26 | Added while-do and repeat-until loops to sail for translating ASL | Alasdair Armstrong | |
| 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-08-17 | Add E_constraint support to re-writer | Alasdair Armstrong | |
| 2017-08-17 | Various sail fixes for ASL hexapod | 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-02 | Add debugging option to dump AST after rewriting steps | Thomas Bauereiss | |
| 2017-07-27 | Add cons patterns to pretty-printers | Thomas Bauereiss | |
| 2017-07-21 | Everything moved to new typechecker | Alasdair Armstrong | |
| Modified initial_check.ml so it no longer requires type_internal. It's still needs cleaned up in a few ways. Most of the things it's trying to do could be done nicer if we took some time to re-factor it, and some of the things should just be handled by the main typechecker, leaving it as a think layer between the parse_ast and the ast. Now that's done everything can be switched to the new typechecker and the _new suffixes were deleted from everything except the monomorphisation pass because I don't know the status of that. | |||
| 2017-07-21 | Switch to new typechecker (almost) | Thomas Bauereiss | |
| Initial typecheck still uses previous typechecker | |||
| 2017-07-12 | Add checks for variable identifiers in pattern subsumption | Thomas Bauereiss | |
| 2017-02-03 | fix headers | Peter Sewell | |
| 2016-09-19 | sail-to-lem progress | Christopher Pulte | |
| 2016-08-14 | Start adding form for (a,b,c) := foo() | Kathy Gray | |
| Not working yet | |||
| 2016-07-23 | Add a return exp form to Sail, supported in type checker and in interpreter. | Kathy Gray | |
| TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem | |||
| 2016-01-07 | Add E_assert to basic rewriters | Kathy Gray | |
| 2015-11-05 | some progress on lem backend: rewrite away mutable variable assignments, ↵ | Christopher Pulte | |
| rewrite for-loops, if/case-expressions to return updated variables | |||
| 2015-10-26 | Switch name set to name map to include type and expression data | Kathy Gray | |
| 2015-10-26 | Add variable set to rewriters | Kathy Gray | |
| 2015-10-19 | progress on lem backend | Christopher Pulte | |
| 2015-10-06 | added the preliminary lem output option that for now uses ocaml pp | Christopher Pulte | |
| 2015-10-04 | add find_updated_vars to support for-loops for lem or prover backend, add ↵ | Christopher Pulte | |
| normalise_exp exp that should transform expressions into a form where they can be embedded into monadic lem or prover definitions. Both untested | |||
| 2015-09-24 | Beginning of expression rewriter for ocaml | Kathy Gray | |
| 2015-09-24 | Parameterise the rewriter's for multiple different rewritings | Kathy Gray | |
| Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope | |||
| 2015-09-17 | Type checker checking on case splits properly, and dependency ↵ | Kathy Gray | |
| transformations restored :) | |||
| 2015-02-13 | Actually use new dependency information in generation of lem/etc. | Kathy Gray | |
| Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |