| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-02-03 | fix headers | Peter Sewell | |
| 2016-08-05 | Fix list parsing and empty vector parsing | Kathy Gray | |
| Add div to library functions | |||
| 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-05-27 | Fix parsing of sizeof and some printing issues with let | Kathy Gray | |
| 2016-05-27 | Add sizeof to sail. Documentation to follow | Kathy Gray | |
| 2016-04-25 | Make interpreter able to read registers during translate address and decode. | Kathy Gray | |
| This is not yet connected to any model and not yet tested. Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ). | |||
| 2016-03-16 | more small fixes | 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-23 | Several fixes | Kathy Gray | |
| Improve printing for asl to sail readability; Add -o option for selecting the name of file generation; Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes | |||
| 2016-02-04 | add mod_s to lexer and parser | Kathy Gray | |
| 2016-01-06 | Add new assert expression to Sail | Kathy Gray | |
| This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified. | |||
| 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-05-13 | Add dynamic footprint dependency check event/outcome | Kathy Gray | |
| Also fix type checker bug in not reporting modifications to parameter values | |||
| 2015-04-08 | Fixes for power compilation reworking | Kathy Gray | |
| 2015-03-26 | Add subtraction to nexp grammar (removing the need to do a + (-1 * b)) | Kathy Gray | |
| Fix up parsing on 2** precedence Fix errors on type variables in function definition | |||
| 2015-01-12 | Add specialised support for numeric singleton types (i.e. what used to be ↵ | Kathy Gray | |
| range<'N,'N>) Non-sugar syntax is -- forall Nat 'N. atom<'N> Sugar syntax is -- [: 'N :] Also begin adding pp support for generating ocaml from ast types. | |||
| 2014-11-22 | signed multiplication and quot | Kathy Gray | |
| 2014-11-21 | Support signed and unsigned arithmetic | Kathy Gray | |
| 2014-08-27 | Changes to get another (slightly larger) executable running; | Kathy Gray | |
| adding executable as a test as well | |||
| 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-04 | Force end-of-input when parsing expression list | Gabriel Kerneis | |
| 2014-07-03 | Parse list of expressions in Sail_lib | Gabriel Kerneis | |
| 2014-07-03 | Introduce a Sail library | Gabriel Kerneis | |
| Used by the Power XML extraction tool. | |||
| 2014-06-26 | Adding better support for unspecified values in indexed vectors | Kathy Gray | |
| Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches | |||
| 2014-06-25 | Add support for memory barrier | Kathy Gray | |
| 2014-06-23 | Get indexed vectors, particularly with default values, working | Kathy Gray | |
| 2014-06-04 | Fixup type coercions and overloading | Kathy Gray | |
| Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions. Warning: test_power does not run as not all overloaded funcitons are implemented Warning: vector concatenation does not pretty print to sail source yet | |||
| 2014-05-19 | More parser comments (and remove one spurious atomic_) | Gabriel Kerneis | |
| 2014-05-15 | Check name_sect during parsing | Gabriel Kerneis | |
| 2014-05-15 | Questions and comments about parser | Gabriel Kerneis | |
| 2014-05-15 | Missing cases in lexer and parser | Gabriel Kerneis | |
| 2014-05-12 | Avoid pattern-matching warnings in pretty-printer | Gabriel Kerneis | |
| 2014-04-15 | Put conditional path information into constraint gathering so that checking ↵ | Kathy Gray | |
| uses appropriate information gleaned from pattern matching | |||
| 2014-04-08 | Reduce redundant information in AST | Kathy Gray | |
| 2014-04-01 | Fix parsing of nexp constraints | Gabriel Kerneis | |
| 2014-03-27 | Check simple constraints (i.e. ones using only constants). | Kathy Gray | |
| Changes syntax of tuple type from * to , so that nexps of the form 8 * 'n can be supported in the parser, which was apparently not true before. | |||
| 2014-03-26 | Steps towards solving constraints | Kathy Gray | |
| 2014-03-20 | Type bit[n] means bit[0..n-1] | Gabriel Kerneis | |
| 2014-03-18 | Add parser support for empty and one element vectors | Kathy Gray | |
| 2014-03-18 | More library functions for Power | Gabriel Kerneis | |
| 2014-03-07 | Treat registers as values when not being actively read or written to, so ↵ | Kathy Gray | |
| that we can have a vector of registers for example. Also, register types can be explicitly referenced. | |||
| 2014-03-04 | Various deinfix bugs | Gabriel Kerneis | |
| 2014-02-28 | Correct bug in parsing and handling a['a:'b] types | Kathy Gray | |
| 2014-02-18 | Adding explicit order to for loops | Kathy Gray | |
| 2014-02-05 | Replace symbolic link by actual file | Gabriel Kerneis | |
| 2014-02-05 | Fix type id parsing error ans associated type checking bugs in scattereds | Kathy Gray | |
| 2014-02-05 | Typechecking lets, concrete vectors, and function calls (minus effects) | Kathy Gray | |
| 2014-02-05 | Deinfixable colon | Gabriel Kerneis | |
| 2014-01-07 | Lex bitzero and bitone literals | Gabriel Kerneis | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |