sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-10-06	Implement replicate_bits for mwords	Brian Campbell

2017-10-06	Fix constant propagation on multi-argument functions	Brian Campbell

2017-10-04	Fixed a bug in vector concatenation l-expressions	Alasdair Armstrong
	The code for these is now rather ugly though... it needs to be cleaned up at some point Also various improvements to new menhir parser
2017-10-04	Add pretty printer for menhir parser	Alasdair Armstrong

2017-10-04	Merge branch 'cleanup' into experiments	Alasdair Armstrong

2017-10-04	Add pretty printing for while loops	Alasdair Armstrong

2017-10-04	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-10-03	Fixes to new parser	Alasdair Armstrong

2017-10-03	Fixed some loop bugs for ASL parser	Alasdair Armstrong

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

2017-10-02	Make undefined constant propagation stop at ex_int	Brian Campbell

2017-09-29	Support vector registers (other than bitvectors)	Thomas Bauereiss

2017-09-29	fix those build errors	Christopher Pulte

2017-09-29	fix deep_shallow_convert, stop using interp_interface.instruction for most ↵	Christopher Pulte
	things, SF and CP bugfixing
2017-09-29	Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments	Thomas Bauereiss

2017-09-29	Some more refactoring of Sail library	Thomas Bauereiss
	- Remove start indices and indexing order from bitvector types. Instead add them as arguments to functions accessing/updating bitvectors. These arguments are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a "sizeof" rewriting pass. - Add a typeclass for bitvectors with a few basic functions (converting to/from bitlists, converting to an integer, getting and setting bits). Make both monads use this interface, so that they work with both the bitlist and the machine word representation of bitvectors.
2017-09-29	Add MIPS->Isabelle target to Makefile	Thomas Bauereiss

2017-09-28	Use (K)Bindings from ast_util rather than making new ones	Brian Campbell

2017-09-28	Add loops to monomorphisation	Brian Campbell

2017-09-28	Merge branch 'experiments' into mono-experiments	Brian Campbell

2017-09-28	Refine constructors during monomorphisation	Brian Campbell

2017-09-27	Add while-loops to Lem backend	Thomas Bauereiss

2017-09-27	Fixed command line flag naming	Alasdair Armstrong

2017-09-26	Remove obsolete existential removal code	Brian Campbell

2017-09-26	Added while-do and repeat-until loops to sail for translating ASL	Alasdair Armstrong

2017-09-26	Remove debugging statements included accidentally	Brian Campbell

2017-09-26	Add propagation of local assignments to monomorphisation	Brian Campbell

2017-09-26	fixes	Christopher Pulte

2017-09-21	Refactored AST valspecs into single constructor	Alasdair Armstrong

2017-09-21	Remove unused kind_def (KD_) nodes from AST	Alasdair Armstrong

2017-09-21	Change NC_fixed to NC_equal to match NC_not_equal	Alasdair Armstrong
	also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
2017-09-21	Simplify AST by removing LB_val_explicit and replace LB_val_implicit with ↵	Alasdair Armstrong
	just LB_val in AST also rename functions in rewriter.ml appropriately.
2017-09-21	Cleaning up the AST and removing redundant and/or unused nodes	Alasdair Armstrong

2017-09-21	Support more functions and vector construction in mono for hexapod	Brian Campbell

2017-09-21	Substitute into constraints to make assert work with mono	Brian Campbell

2017-09-21	Disable existential removal for now	Brian Campbell

2017-09-21	wib	Shaked Flur

2017-09-21	added a comment to the x86 lock'd read and write	Shaked Flur

2017-09-20	Handle let (exists 't...[:'t:]) 't = lit in mono	Brian Campbell

2017-09-20	add support for x86 lock prefix (also remove unused Read/Write_tag kind in ↵	Robert Norton
	etc/regfp.sail.
2017-09-20	Remove obsolete nexp refinement	Brian Campbell

2017-09-20	Support splitting on multiple variables in mono	Brian Campbell

2017-09-19	fix	Christopher Pulte

2017-09-19	Added additional case for tuple l-expressions to increase compatability for ASL.	Alasdair Armstrong

2017-09-18	Added additional utility functions in ast_util	Alasdair Armstrong
	Also fixed basic ocaml test suite
2017-09-18	Merge branch 'experiments' into mono-experiments	Brian Campbell

2017-09-15	x86: implement regfp analysis function (no control flow yet)	Robert Norton

2017-09-15	reinstate deep/shallow conversion	Christopher Pulte

2017-09-14	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-09-14	Two thirds of monomorphising union types with an existential	Brian Campbell
	Still need some way of picking the appropriate constructor