sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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-12-17	First bit of gluing mips onto interpreter and eventually ppcmem infrastructure	Kathy Gray

2015-12-14	Adding new location constructor for location of generated terms	Kathy Gray

2015-11-24	Add BE_escape effect when an E_exit is seen	Kathy Gray
	Close #20
2015-10-19	progress on lem backend	Christopher Pulte

2015-10-08	Add another internal let for Christopher	Kathy Gray

2015-10-07	Start expanding annot for more refined effect tracking	Kathy Gray

2015-09-30	Alias support for ocaml mode	Kathy Gray

2015-09-24	Parameterise the rewriter's for multiple different rewritings	Kathy Gray
	Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope
2015-08-06	Update analysis to merge states and values after branches taken due to ↵	Kathy Gray
	unknown conditions. Does not merge if one path has resulted in an exit
2015-07-24	Begin doing better analysis on case splits over unknowns	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-06-02	changes to compare and equality instances to make lem generate isabelle output	cp526

2015-06-02	Fix errors around ARM not being able to decode due to instruction_extractor ↵	Kathy Gray
	being very power-specific. Note: slight interface change to instruction_extractor
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-05-09	towards buildability - l2.ml and l2_parse.ml as regenerated with current Ott	Peter Sewell

2015-05-09	use less confusing Ott binary	Peter Sewell

2015-03-31	Fix int -> nat bug. Now something with type int cannot be used as something ↵	Kathy Gray
	of type nat (at least not without a >= 0 check)
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-03-15	Many changes:	Kathy Gray
	Split out specification specific memory and external functions Reduce the presence of big_int Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction Also some bug fixes exposed by above and running ARM second instruction
2015-02-24	Overloading formal relation	Kathy Gray

2015-02-18	All existing type rules in line with implementation (and no more red)	Kathy Gray
	Still to do: type rules for register aliases and relation for overloading selection
2015-02-18	expression type checking inline with rules, lexp still out of date; ↵	Kathy Gray
	overloading resolution not modelled
2015-02-17	Bring type rules more into modern state of type checker	Kathy Gray

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-01-26	update ott path	Kathy Gray

2015-01-23	remove dependency on having ott in ones path	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	More type rules	Kathy Gray

2014-12-09	Some of the type rules for expressions	Kathy Gray

2014-12-04	ott rules for type checking pattern match	Kathy Gray

2014-12-03	Type rules unto coercion now represented in ott	Kathy Gray

2014-11-28	full list of built-in functions in rudimentary manual	Kathy Gray

2014-11-27	Start having a manual of sorts. At least specify the built in functions	Kathy Gray
	(list not complete)
2014-09-30	Add type annotations to funcls to track effects and constraints from one ↵	Kathy Gray
	function-clause
2014-08-13	Kathy, Peter tweak Makefile for interactive demo and src/myocamlbuild.ml to ↵	Peter Sewell
	temporarily use other version of Lem
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-25	Start of setting a default order for literal vectors and for vector ↵	Kathy Gray
	shorthand syntax, needed for arm spec
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-07-08	Extend language to support register aliases and to support interrupts, traps ↵	Kathy Gray
	and the like.
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-25	Add support for actions that read just a slice or single bit of a register	Kathy Gray

2014-06-23	Get indexed vectors, particularly with default values, working	Kathy Gray

2014-06-12	Interpret when an unknown is inserted into the program by interp_exhaustive	Kathy Gray
	Short version of below; ready to hook interp_exhaustive up to something to test, but haven't yet. If an unknown value influences a pattern match within an expression, each passing pattern is found and the bodies strung together into a block with let expressions to bind the variables. In a function call, the cases are all collected but the support is not in place at the moment to evaluate them. If an unknown is the result of the cond expression in an if, the then and else case become a block. Unknowns within the interpreter propagate to more Unknowns; also for some but not all library functions yet.
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-29	Check constraints in power.sail; this required using big_int instead of int ↵	Kathy Gray
	to support 264. Note: now nat (short hand for range<0,infinity>) should only be used if you really mean a nat instead of a bounded number (i.e. range<0,232>)
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-08	Reduce redundant information in AST	Kathy Gray