| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-22 | Type quantification elimination working for hexapod spec | Alasdair Armstrong | |
| 2017-08-22 | More work on quantifier elimination | Alasdair Armstrong | |
| 2017-08-21 | More work on quantifier elimination pass | Alasdair Armstrong | |
| Also added a rewriting pass that removes the cast annotations and operator overloading declarations from the AST because they arn't supported by the interpreter. | |||
| 2017-08-21 | Modified sizeof rewriting pass so it can correctly deal with existentials. | Alasdair Armstrong | |
| Basically we needed to make the rewriting step for E_sizeof and E_constraint more aggressively try to rewrite those expressions from variables in scope, without adding new parameters to pass the type variables at runtime, as this can break in the presence of existential quantification. Still some cleanup to do in this code, but tests on the arm spec show that it now introduces the minimal amount of new parameters. | |||
| 2017-08-18 | Fixed a bug where sizeof re-writing fail for aliased type arguments | Alasdair Armstrong | |
| Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments | |||
| 2017-08-17 | Work on E_constraint removal pass and diagnosing bugs in E_sizeof removal pass | 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-15 | Improve and simplify handling of mutable local variables | Thomas Bauereiss | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |