| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-11-27 | make outcome_s contain the instruction state pretty print rather than the ↵ | Christopher Pulte | |
| instruction state, factor out interpreter/shallow embedding value conversion | |||
| 2016-11-14 | add option -lem_sequential for producing shallow embedding that refers to ↵ | Christopher Pulte | |
| state monad, library fixes | |||
| 2016-10-21 | shallow embedding progress | Christopher Pulte | |
| 2016-10-19 | typeclass instances for converting between shallow and deep embedding | Christopher Pulte | |
| 2016-10-18 | Expose type environment after checking, for use in analysis | Kathy Gray | |
| 2016-10-11 | move armv8_extras and power_extras to idl/power and idlarm, fixes | Christopher Pulte | |
| 2016-10-10 | changed the way registers/register fields work, fixes, nicer names for new ↵ | Christopher Pulte | |
| letbound variables | |||
| 2016-10-06 | move type definitions that both interpreter and shallow embedding use to ↵ | Christopher Pulte | |
| sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome | |||
| 2016-09-07 | push some lem pp changes | Christopher Pulte | |
| 2016-06-02 | improve constraint range checking | 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-02-24 | Small mixups to get the initial check infrastructure working for full ast ↵ | Kathy Gray | |
| processing | |||
| 2015-12-21 | fixes, pp progress | Christopher | |
| 2015-12-09 | adapted for Kathy's lexp effect typing changes: register writes should be ↵ | Christopher | |
| correct now, fixes, pp | |||
| 2015-10-28 | progress on lem backend: auto-generate read_register and write_register ↵ | Christopher Pulte | |
| functions, and state definition | |||
| 2015-10-26 | add preliminary Sail_values.lem, adapt lem pp to recent Ocaml pp changes | Christopher Pulte | |
| 2015-10-20 | Fixing bugs in pretty printer to ocaml | Kathy Gray | |
| 2015-10-06 | added the preliminary lem output option that for now uses ocaml pp | Christopher Pulte | |
| 2015-10-06 | fix generated message to have correct file extension | Christopher Pulte | |
| 2015-09-29 | Boiler plate to generate an ml file from a sail spec. Now debugging the ↵ | Kathy Gray | |
| output of such | |||
| 2015-09-28 | basic untested ocaml boiler plate | Kathy Gray | |
| 2015-06-24 | Support new memory write events in the sail front end and pretty printer | Kathy Gray | |
| Events are eamem to signal the memory address to write to and wmv to pass the value to write | |||
| 2015-02-24 | Fix bug where type parameters weren't pushing down into the body of a ↵ | Kathy Gray | |
| function for good unification, especially for rewriting | |||
| 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 | |||
| 2015-02-04 | collect and carry around more data for dependency tracking | Kathy Gray | |
| 2014-12-11 | Add 2 ** n function; support providing type variables to other files when lexing | Kathy Gray | |
| 2014-09-11 | Adding support for extracting the information Christopher needs about an ↵ | Kathy Gray | |
| instruction | |||
| 2014-09-10 | reduce lem macro overhead for sail _ very slightly _ | Kathy Gray | |
| 2014-07-29 | A file can now declare that a default order is either inc or dec, and this ↵ | Kathy Gray | |
| will be reflected in short hand type syntax, inc is still the default if undeclared So: default order dec register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *) default order inc register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *) It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon. | |||
| 2014-07-14 | Initial support for aliases and exit through the type system and the ↵ | Kathy Gray | |
| interpreter. An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter. | |||
| 2014-07-03 | Introduce a Sail library | Gabriel Kerneis | |
| Used by the Power XML extraction tool. | |||
| 2014-06-12 | Add uint* to default type names for lexer | Gabriel Kerneis | |
| This is necessary to avoid a parse error. It might make sense to merge this list and the one in type_internal.ml somehow, to avoid duplication and similar bugs in the future. | |||
| 2014-03-31 | Extend constraint checking, and add casts for base of a vector shifts (i.e. ↵ | Kathy Gray | |
| from 0 to 32 etc, doesn't change order yet.). | |||
| 2014-03-26 | Steps towards solving constraints | Kathy Gray | |
| 2014-02-21 | Add type annotations to lem grammar, including printing out the annotated ↵ | Kathy Gray | |
| ast, and extending the interpreter to expect annotations. Annotations and locations are still not used by the interpreter. | |||
| 2014-02-03 | More type checking, including coercing 0 and 1 into bits when appropriate ↵ | Kathy Gray | |
| (in limited circumstances at the moment due to which expressions are actually checked, so test files should not yet be changed) | |||
| 2014-01-17 | Type check through type definitions and val specifications, building ↵ | Kathy Gray | |
| definition environment. Skipping function definition, let bind, and expression checking for this commit (to come). | |||
| 2013-11-28 | Updated syntax with working examples | Kathy Gray | |
| 2013-11-27 | More front-end passes for type identifiers | Kathy Gray | |
| 2013-11-07 | Port L2 to new Lem | Gabriel Kerneis | |
| Tests compile and run properly. There is a lot of hackery going on to workaround the rough edges of new Lem. Use at your own risk (you need the "library-format" branch of lem). | |||
| 2013-10-10 | Rename Ast to Interp_ast for the interpreter | Gabriel Kerneis | |
| 2013-09-09 | Fixes bugs in pretty printer to generate legal lem syntax; split ott grammar ↵ | Kathy Gray | |
| and rules for lem ast generation; created a new directory for the lem interpreter and moved the Lem ast to it. | |||
| 2013-09-09 | Pretty printer to Lem ast added; accessed by -lem_ast on the command line | Kathy Gray | |
| 2013-08-20 | Set some initial kind environments; start pretty printing | Kathy Gray | |
| 2013-08-08 | More forms converting from parse_ast to ast; also removed some annot aux ↵ | Kathy Gray | |
| homs for terms that only need locations and not full annotations | |||
| 2013-08-07 | Starting checks and translation from parse_ast to ast, including an internal ↵ | Kathy Gray | |
| representation of types to support unification; importing support modules from Lem including pp and util | |||
| 2013-08-01 | Lex and discard comments | Gabriel Kerneis | |
| 2013-07-31 | Adding reporting basic from Lem development, also adding basic error ↵ | Kathy Gray | |
| messages for syntax and lexical errors (i.e. syntax error and location information) | |||
| 2013-07-26 | Remove white space/terminal tracking | Kathy Gray | |
| 2013-07-25 | Clean trailing whitespace | Gabriel Kerneis | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |