sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-11-02	Handle "undefined" type-level sizes in monomorphisation	Brian Campbell

2017-11-01	Support bitvector-size-parametric functions in Lem output	Brian Campbell
	Translates atom('n) types into itself('n) types that won't be erased Also exports more rewriting functions
2017-11-01	Fix some missing nexp simplification in Lem output	Brian Campbell

2017-10-31	Fixed wrong image for List-remove.svg	Alasdair Armstrong

2017-10-31	Added trace viewer application for traces produced by sail -ocaml_trace	Alasdair Armstrong
	See README file for how to set up and use
2017-10-31	Improvements to register read tracing in ocaml backend	Alasdair Armstrong

2017-10-27	Fixed some ocaml backend related bugs	Alasdair Armstrong

2017-10-26	Fix a bug in Sail OCaml library	Alasdair Armstrong

2017-10-26	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-10-26	Unfold nexp abbreviations for pretty-printing	Thomas Bauereiss

2017-10-26	Update val specs after rewriting functions	Thomas Bauereiss

2017-10-26	Experiment with pretty-printing non-atomic nexps in Lem	Thomas Bauereiss

2017-10-26	Updated ocaml backend so tracing instrumentation is optional.	Alasdair Armstrong
	Cleaned up the option list in sail.ml
2017-10-25	Allow mutually recursive functions	Thomas Bauereiss

2017-10-25	Point sail/src makefile at ott file in language/	Alasdair Armstrong

2017-10-25	List.cons is too new	Brian Campbell

2017-10-25	Merge branch 'experiments' into mono-experiments	Brian Campbell

2017-10-25	Generate ast.ml from ott file and update makefile.	Alasdair Armstrong
	Fix until loop not being counted as sugar
2017-10-25	Merge branch 'experiments' into mono-experiments	Brian Campbell

2017-10-25	Alternative low-memory version of barrier_kindCompare	Brian Campbell

2017-10-25	Avoid name clash in generated Lem	Brian Campbell
	(complains due to added val spec)
2017-10-25	ast.ml generated from l2.ott compiles with rest of ./src	Mark Wassell

2017-10-24	Make nexp simplifier handle recursion properly	Brian Campbell

2017-10-24	More succinct syntax in new parser for externed valspecs which share	Alasdair Armstrong
	the same name between sail and the target
2017-10-24	Print type annotations in Lem with type variables	Brian Campbell
	(includes variables for bitvector sizes)
2017-10-24	Limit quantifiers printed in Lem to type variables that actually	Brian Campbell
	appear in the output
2017-10-24	Handle existential types in Lem backend by stripping them and	Brian Campbell
	checking that the type variables visible in the output aren't existential
2017-10-24	Generate undefined_bitvector function when targeting machine words	Brian Campbell

2017-10-24	Produce debug message when an expression can't be converted to a constraint	Brian Campbell

2017-10-24	Remove special case for boolean (as opposed to bool)	Brian Campbell

2017-10-23	Type check external casts	Brian Campbell

2017-10-23	Added effect set pretty printing for new parser	Alasdair Armstrong
	Also added some new utility functions in ast_util
2017-10-23	Added support for better tracing in ocaml backend	Alasdair Armstrong
	Fixed an issue in ast.ml with uneccessary type variables
2017-10-23	Merge branch 'experiments' into mono-experiments	Brian Campbell

2017-10-23	Aligning Ott generated AST with actual ast.ml. Almost a drop-in replacement ↵	Mark Wassell
	but problem with aux introduced 'a type variables
2017-10-19	Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments	Thomas Bauereiss

2017-10-19	Fix pretty-printing of type abbreviation definitions with arguments	Thomas Bauereiss

2017-10-19	Mangle names with '#' characters in Lem pretty-printing	Thomas Bauereiss

2017-10-19	Rewrite undefined values, add type annotations to early returns	Thomas Bauereiss

2017-10-19	Make some potentially non-terminating library functions terminate	Thomas Bauereiss

2017-10-19	Preserve more type environment information during rewriting	Thomas Bauereiss
	Fixes a bug where resolving a type synonym failed in the Lem pretty-printer due to a missing type environment.
2017-10-19	Follow AST changes in (Lem) pretty-printers	Thomas Bauereiss

2017-10-18	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-10-18	Fixes and updates to ocaml backend to compile aarch64_no_vector	Alasdair Armstrong

2017-10-18	Mark more prelude functions extern	Brian Campbell

2017-10-18	Merge branch 'experiments' of Peter_Sewell/sail into mono-experiments	Brian Campbell
	(and fix up monomorphisation)
2017-10-17	Start of alignment of Ott definition with new implementation of type checker ↵	Mark Wassell
	and syntax changes
2017-10-13	Handle bitvector_access in constant propagation	Brian Campbell

2017-10-13	Make Sail_values.repeat total, and remove duplicate	Brian Campbell

2017-10-13	Fix some bugs that surfaced in the ASL export	Thomas Bauereiss
	- Bitvector pattern rewriting had stopped working due to a line of code being lost in some merge. - Fix a bug in early return rewriting that caused returns getting pulled out of if-statements to disappear. - There were some variable name clashes with keywords because doc_lem_id was not always called. - Ast_util.is_number failed to check for "int" and "nat" built-in types, causing pattern matching on natural number literals to fail.