| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-08 | Various fixes and improvements for the Lem pretty-printing | Thomas Bauereiss | |
| - Add some missing "wreg" effect annotations in the type checker - Improve pretty-printing of register type definitions: In addition to a "build" function, output an actual type definition, and some getter/setter functions for register fields - Fix a bug in sizeof rewriting that caused it to fail when rewriting nested calls of functions that contained sizeof expressions - Fix pretty-printing of user-defined union types with type variables (cf. test case option_either.sail) - Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to output more type annotations with bitvector lengths - Add (back) some support for specifying Lem bindings in val specs using "val extern ... foo = bar" - Misc bug fixes | |||
| 2017-08-02 | Improve pretty-printing of register declaration and assignment | Thomas Bauereiss | |
| 2017-08-02 | Add debugging option to dump AST after rewriting steps | Thomas Bauereiss | |
| 2017-08-01 | Fix some effect propagation bugs in rewriter | Thomas Bauereiss | |
| 2017-07-27 | Rewrite guarded patterns for Lem backend | Thomas Bauereiss | |
| 2017-07-27 | Add cons patterns to pretty-printers | Thomas Bauereiss | |
| 2017-07-26 | Improve rewriting of sizeof expressions | Thomas Bauereiss | |
| If some type-level variables in a sizeof expression in a function body cannot be directly extracted from the parameters of the function, add a new parameter for each unresolved parameter, and rewrite calls to the function accordingly | |||
| 2017-07-25 | Add partial support for rewriting of sizeof expressions | Thomas Bauereiss | |
| Tries to extract values of nexps from the (type annotations of) parameters passed to the function. This seems to correspond to the behaviour of the previous typechecker. | |||
| 2017-07-24 | Added cons patterns to sail | Alasdair Armstrong | |
| See test/typecheck/pass/cons_pattern.sail for an example. Also cleaned up the propagating effects code by making some of the variable names less verbose | |||
| 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-07-03 | Cleanup, and add support for variable bindings in bitvector patterns | Thomas Bauereiss | |
| 2017-06-29 | Rewrite bitvector patterns | Thomas Bauereiss | |
| Seems to work for CHERI-MIPS, but still a few things to be done, e.g. collecting let bindings for variables bound in bitvector patterns | |||
| 2017-03-24 | Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵ | Robert Norton | |
| embedding. | |||
| 2017-03-24 | changes to ocaml pp to allow mips->ocaml to compile | Robert Norton | |
| 2017-02-03 | fix headers | Peter Sewell | |
| 2016-11-08 | fixes | Christopher Pulte | |
| 2016-10-27 | more shallow embedding fixes | Christopher Pulte | |
| 2016-10-26 | shallow embedding fixes | Christopher Pulte | |
| 2016-10-13 | make sail-to-lem rewriting passes use dependency analysis, make dependency ↵ | Christopher Pulte | |
| analysis include type information, small pp fix | |||
| 2016-10-10 | changed the way registers/register fields work, fixes, nicer names for new ↵ | Christopher Pulte | |
| letbound variables | |||
| 2016-09-26 | nicer lem output: fewer unnecessary letbinds, monad binds and returns | Christopher Pulte | |
| 2016-09-25 | nicer lem output: no more unecessary 'unit' returns if if-expressions, ↵ | Christopher Pulte | |
| for-loops or case-expressions also return updated variables | |||
| 2016-09-24 | nicer lem output: fewer unecessary 'return's | Christopher Pulte | |
| 2016-09-19 | sail-to-lem progress | Christopher Pulte | |
| 2016-09-16 | fix | Christopher Pulte | |
| 2016-09-16 | make vector concatenation pattern removal deal with vector patterns of ↵ | Christopher Pulte | |
| unknown length (in the last item) | |||
| 2016-09-07 | push some lem pp changes | Christopher Pulte | |
| 2016-08-14 | Start adding form for (a,b,c) := foo() | Kathy Gray | |
| Not working yet | |||
| 2016-08-10 | Fix sizeof code generation to look at parameter bounds | Kathy Gray | |
| 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-07-20 | Make rewriter understand type abbreviations for removing internal_exp instances | Kathy Gray | |
| 2016-05-27 | Add sizeof to sail. Documentation to follow | Kathy Gray | |
| 2016-03-02 | Add new language feature to permit definitions of items of kind Nat, etc as ↵ | Kathy Gray | |
| well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required. | |||
| 2016-01-26 | move closer to power.sail -> power.ml output | Kathy Gray | |
| 2016-01-21 | Start splitting values/etc into int/big_int for ocaml generation | Kathy Gray | |
| 2016-01-14 | small edit to previous commit | Kathy Gray | |
| 2016-01-14 | Fix cumulative effects for circumstance when lifting variable introductions ↵ | Kathy Gray | |
| out of an if Note: this fixes the local cumulative effects for the e_assign and e_if, it may not properly propagate them to the context of the surrounding block | |||
| 2016-01-12 | Fix undefined nvar occurrences that were impacting ARM | Kathy Gray | |
| 2016-01-07 | Add E_assert to basic rewriters | Kathy Gray | |
| 2015-12-21 | fixes, pp progress | Christopher | |
| 2015-12-16 | rewriter and pp changes for generating ARM output | Christopher | |
| 2015-12-15 | better location information | Christopher | |
| 2015-12-10 | fix | Christopher | |
| 2015-12-09 | adapted for Kathy's lexp effect typing changes: register writes should be ↵ | Christopher | |
| correct now, fixes, pp | |||
| 2015-11-25 | fixes, pp | Christopher Pulte | |
| 2015-11-22 | do effect annotation updates more systematically, fix dedup | Christopher Pulte | |
| 2015-11-20 | no more unecessary variables from removing vector-concatenation pattern ↵ | Christopher Pulte | |
| matches, reset variable name counter for each function clause, fixes | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |