sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-08-14	Start adding form for (a,b,c) := foo()	Kathy Gray
	Not working yet
2016-07-24	Make sure that all type constructors with unit type have a type union with ↵	Kathy Gray
	just an id (hopefully fixes Christopher issue).
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-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-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-06-15	Fix strange resulting type for functions with val spec, favouring the ↵	Kathy Gray
	declared return type when consistent instead of using the derived one.
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-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
2014-12-16	Fix bug on nat/type/order/effect variable binding	Kathy Gray
	Fix bug allowing function types in too many places
2014-09-30	Add type annotations to funcls to track effects and constraints from one ↵	Kathy Gray
	function-clause
2014-08-28	fixes to bugs exposed by arm model	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-18	Writing to concatenated aliases	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-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-14	More interface update for connecting externally (interp_interface provides ↵	Kathy Gray
	functions for connecting the interpreter to a memory model) Also adding default values to index vectors for supporting sparse vectors/maps
2014-04-28	Add support for overloading for better constraints, and for reducing the ↵	Kathy Gray
	number of coercions
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-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-03	Fixing assorted bugs. Adding ability to put a type on the identifier being ↵	Kathy Gray
	assigned to in assignments.
2014-02-28	Correct bug in parsing and handling a['a:'b] types	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-18	Adding explicit order to for loops	Kathy Gray

2014-02-05	Fix type id parsing error ans associated type checking bugs in scattereds	Kathy Gray

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-12-10	Fixed bug in interpreter	Kathy Gray

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-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-01	Moved metatheory grammars into l2_rules.ott	Kathy Gray
	Added val extern specification to language, parser, printer, and interpreter Added various def level type system support, expressions type system in place Except for assignment
2013-10-14	Fix pattern match so that P_id is selected when P_app has no parameters	Kathy Gray

2013-10-09	Adding memory writes. Cleaning up the let in the ott file to reflect what ↵	Kathy Gray
	actually parses
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-20	Set some initial kind environments; start pretty printing	Kathy Gray

2013-08-19	Translate foreach from Parse_ast to Ast	Gabriel Kerneis

2013-08-16	Full translation from parse_ast to ast; which includes kind checking and ↵	Kathy Gray
	pulling scattered defintiions together, with checking on name overlap and not "ending" definitions
2013-08-15	Checks up to scattered defs	Kathy Gray

2013-08-14	More cases translating from parse_ast to ast. Plus parser changes to syntax ↵	Kathy Gray
	to support type casts; syntax changes not yet reflected in ott file
2013-08-13	more translation from parse_ast to ast	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