sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-02-03	fix headers	Peter Sewell

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	Add sizeof to sail. Documentation to follow	Kathy Gray

2016-03-16	add def to full lexer	Kathy Gray

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-02-17	actually support string types	Kathy Gray

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-12-18	Add negative literals such as -1. WARNING may not generate valid lem in the ↵	Kathy Gray
	presence of negative literals
2014-11-22	signed multiplication and quot	Kathy Gray

2014-11-21	Support signed and unsigned arithmetic	Kathy Gray

2014-08-26	small changes for arm	Kathy Gray

2014-08-05	missed file from last commit	Kathy Gray

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-25	Add support for memory barrier	Kathy Gray

2014-05-15	Missing cases in lexer and parser	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-02-28	Correct bug in parsing and handling a['a:'b] types	Kathy Gray

2014-02-05	Deinfixable colon	Gabriel Kerneis

2014-01-07	Lex bitzero and bitone literals	Gabriel Kerneis

2013-12-17	Remove spurious lexing tokens	Gabriel Kerneis

2013-12-16	lexer: inc and dec keywords	Gabriel Kerneis

2013-12-03	Syntax changes per discussion with Peter, as well as L2.ott document clean up.	Kathy Gray
	Could not at this time return lists to [\| \|] from [\|\| \|\|] as the parser cannot distinguish a cast with enum’s syntactic sugar from the start of a parenthesised list (i.e. ( [\|3\|] ) And there are still conflicts with moving enums to [3], so those changes can’t be pushed in with current parser technology.
2013-11-28	Updated syntax with working examples	Kathy Gray

2013-11-27	More front-end passes for type identifiers	Kathy Gray

2013-11-22	Syntax changes per discussions on Thursday.	Kathy Gray
	First pass parser to identify type names is in progress (current test files fail, will correct once pre-parser is in place)
2013-11-05	Parsing of infix operators	Gabriel Kerneis
	The interpreter is broken for infix calls (fails to find the relevant function, either internal or external).
2013-11-05	Support parsing for extern calls	Gabriel Kerneis

2013-09-26	Adding undefined	Kathy Gray
	Also interpreter now supports reading and writing of basic registers (i.e with no subranges yet)
2013-08-22	Pretty printer for whole AST; due to parenthesis not always being placed ↵	Kathy Gray
	where needed, what is generated may not parse
2013-08-19	Add loops and document optionnal else in conditional	Gabriel Kerneis
	Syntax: foreach id from exp (to\|downto) exp (by exp)? exp foreach and by are keywords; from, to and downto aren't.
2013-08-01	Lex and discard comments	Gabriel Kerneis

2013-07-30	More infix supported	Kathy Gray

2013-07-26	Remove white space/terminal tracking	Kathy Gray

2013-07-25	Clean trailing whitespace	Gabriel Kerneis

2013-07-24	Parser compiles and compiles some very small test programs.	Kathy Gray
	Output is only given in the event of a parse or lex failure (with poor reporting for now) There are still 10 shift/reduce conflicts that may need further investigating and a few syntax changes that need discussion.
2013-07-18	More parsing	Kathy Gray

2013-07-12	Parser in progress, and more src files for plumbing parsing, lexing and ↵	Kathy Gray
	eventual type checking together
2013-07-10	Fixes to grammar omissions (i.e. naming_scheme_opt and type_def vs tdef), ↵	Kathy Gray
	more token addition, and start of parsing
2013-07-05	More token corrections and additions based on l2_design notes.	Kathy Gray
	Lexer should now be complete
2013-07-04	Small updates to tokens; change comments to --; fix up id	Kathy Gray

2013-07-04	First addition of lexer and parser for L2, based on Lem parser and lexer.	Kathy Gray
	Not complete, does not compile